NO
The TRS could be proven non-terminating. The proof took 155 ms.
The following reduction sequence is a witness for non-termination:
f#(d) →* f#(d)
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (5ms).
| – Problem 2 was processed with processor ForwardNarrowing (1ms).
| | – Problem 3 was processed with processor ForwardNarrowing (1ms).
| | | – Problem 4 was processed with processor ForwardNarrowing (1ms).
| | | | – Problem 5 remains open; application of the following processors failed [ForwardNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (0ms), Propagation (1ms), ForwardNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (0ms), Propagation (1ms)].
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f#(d) | → | a# | | f#(d) | → | f#(a) |
| a# | → | b# | | a# | → | U21#(b) |
Rewrite Rules
| b | → | g(d) | | f(d) | → | f(a) |
| a | → | U21(b) | | U21(g(x)) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, b, a
Strategy
Context-sensitive strategy:
μ(T) = μ(d) = μ(b) = μ(a) = μ(b#) = μ(a#) = ∅
μ(f) = μ(g) = μ(f#) = μ(U21#) = μ(U21) = {1}
The following SCCs where found
Problem 2: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| b | → | g(d) | | f(d) | → | f(a) |
| a | → | U21(b) | | U21(g(x)) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, b, a
Strategy
Context-sensitive strategy:
μ(T) = μ(d) = μ(b) = μ(a) = μ(b#) = μ(a#) = ∅
μ(f) = μ(g) = μ(f#) = μ(U21#) = μ(U21) = {1}
The right-hand side of the rule f
#(d) → f
#(a) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| f#(U21(b)) | |
Thus, the rule f
#(d) → f
#(a) is replaced by the following rules:
Problem 3: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| b | → | g(d) | | f(d) | → | f(a) |
| a | → | U21(b) | | U21(g(x)) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, b, a
Strategy
Context-sensitive strategy:
μ(T) = μ(d) = μ(b) = μ(a) = μ(b#) = μ(a#) = ∅
μ(f) = μ(g) = μ(f#) = μ(U21#) = μ(U21) = {1}
The right-hand side of the rule f
#(d) → f
#(
U21(b)) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| f#(U21(g(d))) | |
Thus, the rule f
#(d) → f
#(
U21(b)) is replaced by the following rules:
Problem 4: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| b | → | g(d) | | f(d) | → | f(a) |
| a | → | U21(b) | | U21(g(x)) | → | x |
Original Signature
Termination of terms over the following signature is verified: f, g, d, b, a
Strategy
Context-sensitive strategy:
μ(T) = μ(d) = μ(b) = μ(a) = μ(b#) = μ(a#) = ∅
μ(f) = μ(g) = μ(f#) = μ(U21#) = μ(U21) = {1}
The right-hand side of the rule f
#(d) → f
#(
U21(g(d))) is narrowed to the following relevant and irrelevant terms (a narrowing is irrelevant if by dropping it the correctness (and completeness) of the processor is not influenced).
| Relevant Terms | Irrelevant Terms |
|---|
| f#(d) | |
Thus, the rule f
#(d) → f
#(
U21(g(d))) is replaced by the following rules: