NO
The TRS could be proven non-terminating. The proof took 3826 ms.
The following reduction sequence is a witness for non-termination:
a__f#(b, b) →* a__f#(b, b)
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (64ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (1295ms).
| | – Problem 3 was processed with processor DependencyGraph (4ms).
| | | – Problem 4 was processed with processor BackwardInstantiation (4ms).
| | | | – Problem 5 was processed with processor Propagation (2ms).
| | | | | – Problem 6 was processed with processor ForwardNarrowing (5ms).
| | | | | | – Problem 7 was processed with processor ForwardNarrowing (3ms).
| | | | | | | – Problem 8 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | – Problem 9 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | – Problem 10 was processed with processor ForwardNarrowing (4ms).
| | | | | | | | | | – Problem 11 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | | | – Problem 12 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | | | | – Problem 13 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | | | | | – Problem 14 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | | | | | | – Problem 15 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | – Problem 16 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | – Problem 17 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | | – Problem 18 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | | | | | | | | | | – Problem 19 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | | | | – Problem 20 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | | | | | | | | | | | | – Problem 21 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | | | | | | – Problem 22 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | | | | | | | | | | | | | | – Problem 23 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | | | | | | | | | | | | | | | – Problem 24 was processed with processor ForwardNarrowing (3ms).
| | | | | | | | | | | | | | | | | | | | | | | | – Problem 25 was processed with processor BackwardInstantiation (3ms).
| | | | | | | | | | | | | | | | | | | | | | | | | – Problem 26 was processed with processor Propagation (2ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 27 was processed with processor ForwardNarrowing (2ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 28 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 29 was processed with processor ForwardNarrowing (1ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 30 was processed with processor BackwardInstantiation (2ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 31 was processed with processor Propagation (3ms).
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | – Problem 32 remains open; application of the following processors failed [].
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | mark#(a) | → | a__a# |
| a__h#(X) | → | mark#(X) | | mark#(g(X1, X2)) | → | a__g#(mark(X1), X2) |
| mark#(f(X1, X2)) | → | a__f#(mark(X1), X2) | | a__h#(X) | → | a__g#(mark(X), X) |
| a__f#(X, X) | → | a__a# | | mark#(h(X)) | → | mark#(X) |
| mark#(g(X1, X2)) | → | mark#(X1) | | a__f#(X, X) | → | a__h#(a__a) |
| mark#(h(X)) | → | a__h#(mark(X)) | | mark#(f(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, a__f, h
Strategy
The following SCCs where found
| a__g#(a, X) → a__f#(b, X) | a__h#(X) → mark#(X) |
| mark#(g(X1, X2)) → a__g#(mark(X1), X2) | mark#(f(X1, X2)) → a__f#(mark(X1), X2) |
| a__h#(X) → a__g#(mark(X), X) | mark#(g(X1, X2)) → mark#(X1) |
| mark#(h(X)) → mark#(X) | a__f#(X, X) → a__h#(a__a) |
| mark#(h(X)) → a__h#(mark(X)) | mark#(f(X1, X2)) → mark#(X1) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__h#(X) | → | mark#(X) |
| mark#(g(X1, X2)) | → | a__g#(mark(X1), X2) | | mark#(f(X1, X2)) | → | a__f#(mark(X1), X2) |
| a__h#(X) | → | a__g#(mark(X), X) | | mark#(g(X1, X2)) | → | mark#(X1) |
| mark#(h(X)) | → | mark#(X) | | a__f#(X, X) | → | a__h#(a__a) |
| mark#(h(X)) | → | a__h#(mark(X)) | | mark#(f(X1, X2)) | → | mark#(X1) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, a__f, h
Strategy
Polynomial Interpretation
- a: 0
- a__a: 0
- a__f(x,y): x + 2
- a__f#(x,y): 0
- a__g(x,y): y + x + 2
- a__g#(x,y): 0
- a__h(x): 2x + 2
- a__h#(x): 2x
- b: 0
- f(x,y): x + 2
- g(x,y): y + x + 2
- h(x): 2x + 2
- mark(x): x
- mark#(x): x
Improved Usable rules
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | b |
| a__h(X) | → | a__g(mark(X), X) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| a__f(X1, X2) | → | f(X1, X2) | | a__h(X) | → | h(X) |
| mark(b) | → | b | | a__g(a, X) | → | a__f(b, X) |
| mark(f(X1, X2)) | → | a__f(mark(X1), X2) | | a__f(X, X) | → | a__h(a__a) |
| mark(a) | → | a__a | | mark(h(X)) | → | a__h(mark(X)) |
| a__a | → | a |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| mark#(g(X1, X2)) | → | a__g#(mark(X1), X2) | | mark#(f(X1, X2)) | → | a__f#(mark(X1), X2) |
| mark#(h(X)) | → | mark#(X) | | mark#(g(X1, X2)) | → | mark#(X1) |
| mark#(h(X)) | → | a__h#(mark(X)) | | mark#(f(X1, X2)) | → | mark#(X1) |
Problem 3: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__h#(X) | → | mark#(X) |
| a__h#(X) | → | a__g#(mark(X), X) | | a__f#(X, X) | → | a__h#(a__a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, h, a__f
Strategy
The following SCCs where found
| a__g#(a, X) → a__f#(b, X) | a__h#(X) → a__g#(mark(X), X) |
| a__f#(X, X) → a__h#(a__a) |
Problem 4: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__h#(X) | → | a__g#(mark(X), X) |
| a__f#(X, X) | → | a__h#(a__a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, h, a__f
Strategy
Instantiation
For all potential predecessors l → r of the rule a__h
#(
X) → a__g
#(mark(
X),
X) on dependency pair chains it holds that:
- a__h#(X) matches r,
- all variables of a__h#(X) are embedded in constructor contexts, i.e., each subterm of a__h#(X), containing a variable is rooted by a constructor symbol.
Thus, a__h
#(
X) → a__g
#(mark(
X),
X) is replaced by instances determined through the above matching. These instances are:
| a__h#(a__a) → a__g#(mark(a__a), a__a) |
Problem 5: Propagation
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__h#(a__a) | → | a__g#(mark(a__a), a__a) |
| a__f#(X, X) | → | a__h#(a__a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, a__f, h
Strategy
The dependency pairs a__f
#(
X,
X) → a__h
#(a__a) and a__h
#(a__a) → a__g
#(mark(a__a), a__a) are consolidated into the rule a__f
#(
X,
X) → a__g
#(mark(a__a), a__a) .
This is possible as
- all subterms of a__h#(a__a) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in a__h#(a__a), but non-replacing in both a__f#(X, X) and a__g#(mark(a__a), a__a)
The dependency pairs a__f
#(
X,
X) → a__h
#(a__a) and a__h
#(a__a) → a__g
#(mark(a__a), a__a) are consolidated into the rule a__f
#(
X,
X) → a__g
#(mark(a__a), a__a) .
This is possible as
- all subterms of a__h#(a__a) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in a__h#(a__a), but non-replacing in both a__f#(X, X) and a__g#(mark(a__a), a__a)
The dependency pairs a__f
#(
X,
X) → a__h
#(a__a) and a__h
#(a__a) → a__g
#(mark(a__a), a__a) are consolidated into the rule a__f
#(
X,
X) → a__g
#(mark(a__a), a__a) .
This is possible as
- all subterms of a__h#(a__a) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in a__h#(a__a), but non-replacing in both a__f#(X, X) and a__g#(mark(a__a), a__a)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| a__h#(a__a) → a__g#(mark(a__a), a__a) | a__f#(X, X) → a__g#(mark(a__a), a__a) |
| a__f#(X, X) → a__h#(a__a) | |
Problem 6: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(mark(a__a), a__a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, h, a__f
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(mark(a__a), a__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 |
|---|
| a__g#(mark(a), a__a) | |
| a__g#(mark(a__a), a) | |
| a__g#(mark(b), a__a) | |
| a__g#(mark(a__a), b) | |
Thus, the rule a__f
#(
X,
X) → a__g
#(mark(a__a), a__a) is replaced by the following rules:
| a__f#(X, X) → a__g#(mark(b), a__a) | a__f#(X, X) → a__g#(mark(a), a__a) |
| a__f#(X, X) → a__g#(mark(a__a), b) | a__f#(X, X) → a__g#(mark(a__a), a) |
Problem 7: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(mark(b), a__a) |
| a__f#(X, X) | → | a__g#(mark(a), a__a) | | a__f#(X, X) | → | a__g#(mark(a__a), b) |
| a__f#(X, X) | → | a__g#(mark(a__a), a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, a__f, h
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(mark(b), a__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 |
|---|
| a__g#(b, a__a) | |
| a__g#(mark(b), b) | |
| a__g#(mark(b), a) | |
Thus, the rule a__f
#(
X,
X) → a__g
#(mark(b), a__a) is replaced by the following rules:
| a__f#(X, X) → a__g#(mark(b), b) | a__f#(X, X) → a__g#(mark(b), a) |
| a__f#(X, X) → a__g#(b, a__a) |
Problem 8: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(mark(a), a__a) |
| a__f#(X, X) | → | a__g#(mark(b), b) | | a__f#(X, X) | → | a__g#(mark(b), a) |
| a__f#(X, X) | → | a__g#(mark(a__a), b) | | a__f#(X, X) | → | a__g#(b, a__a) |
| a__f#(X, X) | → | a__g#(mark(a__a), a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, h, a__f
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(mark(b), 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 |
|---|
| a__g#(b, b) | |
Thus, the rule a__f
#(
X,
X) → a__g
#(mark(b), b) is replaced by the following rules:
| a__f#(X, X) → a__g#(b, b) |
Problem 9: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(mark(a), a__a) |
| a__f#(X, X) | → | a__g#(b, b) | | a__f#(X, X) | → | a__g#(mark(b), a) |
| a__f#(X, X) | → | a__g#(mark(a__a), b) | | a__f#(X, X) | → | a__g#(b, a__a) |
| a__f#(X, X) | → | a__g#(mark(a__a), a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, a__f, h
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(mark(a), a__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 |
|---|
| a__g#(mark(a), a) | |
| a__g#(mark(a), b) | |
| a__g#(a__a, a__a) | |
Thus, the rule a__f
#(
X,
X) → a__g
#(mark(a), a__a) is replaced by the following rules:
| a__f#(X, X) → a__g#(mark(a), a) | a__f#(X, X) → a__g#(mark(a), b) |
| a__f#(X, X) → a__g#(a__a, a__a) |
Problem 10: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(mark(a), a) |
| a__f#(X, X) | → | a__g#(mark(a), b) | | a__f#(X, X) | → | a__g#(a__a, a__a) |
| a__f#(X, X) | → | a__g#(b, b) | | a__f#(X, X) | → | a__g#(mark(b), a) |
| a__f#(X, X) | → | a__g#(mark(a__a), b) | | a__f#(X, X) | → | a__g#(b, a__a) |
| a__f#(X, X) | → | a__g#(mark(a__a), a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, h, a__f
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(a__a, a__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 |
|---|
| a__g#(a, a__a) | |
| a__g#(a__a, a) | |
| a__g#(b, a__a) | |
| a__g#(a__a, b) | |
Thus, the rule a__f
#(
X,
X) → a__g
#(a__a, a__a) is replaced by the following rules:
| a__f#(X, X) → a__g#(a__a, b) | a__f#(X, X) → a__g#(a__a, a) |
| a__f#(X, X) → a__g#(b, a__a) | a__f#(X, X) → a__g#(a, a__a) |
Problem 11: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(mark(a), b) |
| a__f#(X, X) | → | a__g#(mark(a), a) | | a__f#(X, X) | → | a__g#(a__a, b) |
| a__f#(X, X) | → | a__g#(b, b) | | a__f#(X, X) | → | a__g#(mark(b), a) |
| a__f#(X, X) | → | a__g#(a__a, a) | | a__f#(X, X) | → | a__g#(mark(a__a), b) |
| a__f#(X, X) | → | a__g#(b, a__a) | | a__f#(X, X) | → | a__g#(a, a__a) |
| a__f#(X, X) | → | a__g#(mark(a__a), a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, a__f, h
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(a__a, 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 |
|---|
| a__g#(b, b) | |
| a__g#(a, b) | |
Thus, the rule a__f
#(
X,
X) → a__g
#(a__a, b) is replaced by the following rules:
| a__f#(X, X) → a__g#(b, b) | a__f#(X, X) → a__g#(a, b) |
Problem 12: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(mark(a), a) |
| a__f#(X, X) | → | a__g#(mark(a), b) | | a__f#(X, X) | → | a__g#(b, b) |
| a__f#(X, X) | → | a__g#(a__a, a) | | a__f#(X, X) | → | a__g#(mark(b), a) |
| a__f#(X, X) | → | a__g#(mark(a__a), b) | | a__f#(X, X) | → | a__g#(a, a__a) |
| a__f#(X, X) | → | a__g#(b, a__a) | | a__f#(X, X) | → | a__g#(mark(a__a), a) |
| a__f#(X, X) | → | a__g#(a, b) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, h, a__f
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(mark(a), 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 |
|---|
| a__g#(a__a, b) | |
Thus, the rule a__f
#(
X,
X) → a__g
#(mark(a), b) is replaced by the following rules:
| a__f#(X, X) → a__g#(a__a, b) |
Problem 13: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(mark(a), a) |
| a__f#(X, X) | → | a__g#(a__a, b) | | a__f#(X, X) | → | a__g#(b, b) |
| a__f#(X, X) | → | a__g#(mark(b), a) | | a__f#(X, X) | → | a__g#(a__a, a) |
| a__f#(X, X) | → | a__g#(mark(a__a), b) | | a__f#(X, X) | → | a__g#(b, a__a) |
| a__f#(X, X) | → | a__g#(a, a__a) | | a__f#(X, X) | → | a__g#(a, b) |
| a__f#(X, X) | → | a__g#(mark(a__a), a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, a__f, h
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(a__a, 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 |
|---|
| a__g#(b, b) | |
| a__g#(a, b) | |
Thus, the rule a__f
#(
X,
X) → a__g
#(a__a, b) is replaced by the following rules:
| a__f#(X, X) → a__g#(b, b) | a__f#(X, X) → a__g#(a, b) |
Problem 14: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(mark(a), a) |
| a__f#(X, X) | → | a__g#(b, b) | | a__f#(X, X) | → | a__g#(a__a, a) |
| a__f#(X, X) | → | a__g#(mark(b), a) | | a__f#(X, X) | → | a__g#(mark(a__a), b) |
| a__f#(X, X) | → | a__g#(a, a__a) | | a__f#(X, X) | → | a__g#(b, a__a) |
| a__f#(X, X) | → | a__g#(mark(a__a), a) | | a__f#(X, X) | → | a__g#(a, b) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, h, a__f
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(mark(a), 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 |
|---|
| a__g#(a__a, a) | |
Thus, the rule a__f
#(
X,
X) → a__g
#(mark(a), a) is replaced by the following rules:
| a__f#(X, X) → a__g#(a__a, a) |
Problem 15: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(b, b) |
| a__f#(X, X) | → | a__g#(mark(b), a) | | a__f#(X, X) | → | a__g#(a__a, a) |
| a__f#(X, X) | → | a__g#(mark(a__a), b) | | a__f#(X, X) | → | a__g#(b, a__a) |
| a__f#(X, X) | → | a__g#(a, a__a) | | a__f#(X, X) | → | a__g#(a, b) |
| a__f#(X, X) | → | a__g#(mark(a__a), a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, a__f, h
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(b, 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 |
|---|
Thus, the rule a__f
#(
X,
X) → a__g
#(b, b) is deleted.
Problem 16: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(a__a, a) |
| a__f#(X, X) | → | a__g#(mark(b), a) | | a__f#(X, X) | → | a__g#(mark(a__a), b) |
| a__f#(X, X) | → | a__g#(a, a__a) | | a__f#(X, X) | → | a__g#(b, a__a) |
| a__f#(X, X) | → | a__g#(mark(a__a), a) | | a__f#(X, X) | → | a__g#(a, b) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, h, a__f
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(mark(b), 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 |
|---|
| a__g#(b, a) | |
Thus, the rule a__f
#(
X,
X) → a__g
#(mark(b), a) is replaced by the following rules:
| a__f#(X, X) → a__g#(b, a) |
Problem 17: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(b, a) |
| a__f#(X, X) | → | a__g#(a__a, a) | | a__f#(X, X) | → | a__g#(mark(a__a), b) |
| a__f#(X, X) | → | a__g#(b, a__a) | | a__f#(X, X) | → | a__g#(a, a__a) |
| a__f#(X, X) | → | a__g#(a, b) | | a__f#(X, X) | → | a__g#(mark(a__a), a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, a__f, h
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(b, 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 |
|---|
Thus, the rule a__f
#(
X,
X) → a__g
#(b, a) is deleted.
Problem 18: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(a__a, a) |
| a__f#(X, X) | → | a__g#(mark(a__a), b) | | a__f#(X, X) | → | a__g#(a, a__a) |
| a__f#(X, X) | → | a__g#(b, a__a) | | a__f#(X, X) | → | a__g#(mark(a__a), a) |
| a__f#(X, X) | → | a__g#(a, b) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, h, a__f
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(a__a, 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 |
|---|
| a__g#(b, a) | |
| a__g#(a, a) | |
Thus, the rule a__f
#(
X,
X) → a__g
#(a__a, a) is replaced by the following rules:
| a__f#(X, X) → a__g#(b, a) | a__f#(X, X) → a__g#(a, a) |
Problem 19: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(b, a) |
| a__f#(X, X) | → | a__g#(a, a) | | a__f#(X, X) | → | a__g#(mark(a__a), b) |
| a__f#(X, X) | → | a__g#(b, a__a) | | a__f#(X, X) | → | a__g#(a, a__a) |
| a__f#(X, X) | → | a__g#(a, b) | | a__f#(X, X) | → | a__g#(mark(a__a), a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, a__f, h
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(b, 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 |
|---|
Thus, the rule a__f
#(
X,
X) → a__g
#(b, a) is deleted.
Problem 20: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(a, a) |
| a__f#(X, X) | → | a__g#(mark(a__a), b) | | a__f#(X, X) | → | a__g#(a, a__a) |
| a__f#(X, X) | → | a__g#(b, a__a) | | a__f#(X, X) | → | a__g#(mark(a__a), a) |
| a__f#(X, X) | → | a__g#(a, b) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, h, a__f
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(mark(a__a), 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 |
|---|
| a__g#(mark(b), b) | |
| a__g#(mark(a), b) | |
Thus, the rule a__f
#(
X,
X) → a__g
#(mark(a__a), b) is replaced by the following rules:
| a__f#(X, X) → a__g#(mark(a), b) | a__f#(X, X) → a__g#(mark(b), b) |
Problem 21: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(mark(a), b) |
| a__f#(X, X) | → | a__g#(mark(b), b) | | a__f#(X, X) | → | a__g#(a, a) |
| a__f#(X, X) | → | a__g#(b, a__a) | | a__f#(X, X) | → | a__g#(a, a__a) |
| a__f#(X, X) | → | a__g#(a, b) | | a__f#(X, X) | → | a__g#(mark(a__a), a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, a__f, h
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(mark(a), 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 |
|---|
| a__g#(a__a, b) | |
Thus, the rule a__f
#(
X,
X) → a__g
#(mark(a), b) is replaced by the following rules:
| a__f#(X, X) → a__g#(a__a, b) |
Problem 22: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(a__a, b) |
| a__f#(X, X) | → | a__g#(mark(b), b) | | a__f#(X, X) | → | a__g#(a, a) |
| a__f#(X, X) | → | a__g#(a, a__a) | | a__f#(X, X) | → | a__g#(b, a__a) |
| a__f#(X, X) | → | a__g#(mark(a__a), a) | | a__f#(X, X) | → | a__g#(a, b) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, h, a__f
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(a__a, 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 |
|---|
| a__g#(b, b) | |
| a__g#(a, b) | |
Thus, the rule a__f
#(
X,
X) → a__g
#(a__a, b) is replaced by the following rules:
| a__f#(X, X) → a__g#(b, b) | a__f#(X, X) → a__g#(a, b) |
Problem 23: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(mark(b), b) |
| a__f#(X, X) | → | a__g#(a, a) | | a__f#(X, X) | → | a__g#(b, b) |
| a__f#(X, X) | → | a__g#(b, a__a) | | a__f#(X, X) | → | a__g#(a, a__a) |
| a__f#(X, X) | → | a__g#(a, b) | | a__f#(X, X) | → | a__g#(mark(a__a), a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, a__f, h
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(mark(b), 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 |
|---|
| a__g#(b, b) | |
Thus, the rule a__f
#(
X,
X) → a__g
#(mark(b), b) is replaced by the following rules:
| a__f#(X, X) → a__g#(b, b) |
Problem 24: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(b, b) |
| a__f#(X, X) | → | a__g#(a, a) | | a__f#(X, X) | → | a__g#(a, a__a) |
| a__f#(X, X) | → | a__g#(b, a__a) | | a__f#(X, X) | → | a__g#(mark(a__a), a) |
| a__f#(X, X) | → | a__g#(a, b) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, h, a__f
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__g
#(b, 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 |
|---|
Thus, the rule a__f
#(
X,
X) → a__g
#(b, b) is deleted.
Problem 25: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| a__g#(a, X) | → | a__f#(b, X) | | a__f#(X, X) | → | a__g#(a, a) |
| a__f#(X, X) | → | a__g#(a, a__a) | | a__f#(X, X) | → | a__g#(a, b) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, h, a__f
Strategy
Instantiation
For all potential predecessors l → r of the rule a__g
#(a,
X) → a__f
#(b,
X) on dependency pair chains it holds that:
- a__g#(a, X) matches r,
- all variables of a__g#(a, X) are embedded in constructor contexts, i.e., each subterm of a__g#(a, X), containing a variable is rooted by a constructor symbol.
Thus, a__g
#(a,
X) → a__f
#(b,
X) is replaced by instances determined through the above matching. These instances are:
| a__g#(a, b) → a__f#(b, b) | a__g#(a, a) → a__f#(b, a) |
| a__g#(a, a__a) → a__f#(b, a__a) |
Problem 26: Propagation
Dependency Pair Problem
Dependency Pairs
| a__g#(a, b) | → | a__f#(b, b) | | a__g#(a, a) | → | a__f#(b, a) |
| a__g#(a, a__a) | → | a__f#(b, a__a) | | a__f#(X, X) | → | a__g#(a, a) |
| a__f#(X, X) | → | a__g#(a, a__a) | | a__f#(X, X) | → | a__g#(a, b) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, a__f, h
Strategy
The dependency pairs a__f
#(
X,
X) → a__g
#(a, a) and a__g
#(a, a) → a__f
#(b, a) are consolidated into the rule a__f
#(
X,
X) → a__f
#(b, a) .
This is possible as
- all subterms of a__g#(a, a) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in a__g#(a, a), but non-replacing in both a__f#(X, X) and a__f#(b, a)
The dependency pairs a__f
#(
X,
X) → a__g
#(a, a) and a__g
#(a, a) → a__f
#(b, a) are consolidated into the rule a__f
#(
X,
X) → a__f
#(b, a) .
This is possible as
- all subterms of a__g#(a, a) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in a__g#(a, a), but non-replacing in both a__f#(X, X) and a__f#(b, a)
The dependency pairs a__f
#(
X,
X) → a__g
#(a, b) and a__g
#(a, b) → a__f
#(b, b) are consolidated into the rule a__f
#(
X,
X) → a__f
#(b, b) .
This is possible as
- all subterms of a__g#(a, b) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in a__g#(a, b), but non-replacing in both a__f#(X, X) and a__f#(b, b)
The dependency pairs a__f
#(
X,
X) → a__g
#(a, b) and a__g
#(a, b) → a__f
#(b, b) are consolidated into the rule a__f
#(
X,
X) → a__f
#(b, b) .
This is possible as
- all subterms of a__g#(a, b) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in a__g#(a, b), but non-replacing in both a__f#(X, X) and a__f#(b, b)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| a__g#(a, b) → a__f#(b, b) | a__f#(X, X) → a__f#(b, b) |
| a__g#(a, a) → a__f#(b, a) | a__f#(X, X) → a__f#(b, a) |
| a__f#(X, X) → a__g#(a, a) | |
| a__f#(X, X) → a__g#(a, b) | |
Problem 27: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, a__a) | → | a__f#(b, a__a) | | a__f#(X, X) | → | a__f#(b, b) |
| a__f#(X, X) | → | a__g#(a, a__a) | | a__f#(X, X) | → | a__f#(b, a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, h, a__f
Strategy
The right-hand side of the rule a__g
#(a, a__a) → a__f
#(b, a__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 |
|---|
| a__f#(b, b) | |
| a__f#(b, a) | |
Thus, the rule a__g
#(a, a__a) → a__f
#(b, a__a) is replaced by the following rules:
| a__g#(a, a__a) → a__f#(b, a) | a__g#(a, a__a) → a__f#(b, b) |
Problem 28: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__g#(a, a__a) | → | a__f#(b, a) | | a__f#(X, X) | → | a__f#(b, b) |
| a__g#(a, a__a) | → | a__f#(b, b) | | a__f#(X, X) | → | a__f#(b, a) |
| a__f#(X, X) | → | a__g#(a, a__a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, a__f, h
Strategy
The right-hand side of the rule a__g
#(a, a__a) → a__f
#(b, 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 |
|---|
Thus, the rule a__g
#(a, a__a) → a__f
#(b, a) is deleted.
Problem 29: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| a__f#(X, X) | → | a__f#(b, b) | | a__g#(a, a__a) | → | a__f#(b, b) |
| a__f#(X, X) | → | a__g#(a, a__a) | | a__f#(X, X) | → | a__f#(b, a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, h, a__f
Strategy
The right-hand side of the rule a__f
#(
X,
X) → a__f
#(b, 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 |
|---|
Thus, the rule a__f
#(
X,
X) → a__f
#(b, a) is deleted.
Problem 30: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| a__f#(X, X) | → | a__f#(b, b) | | a__g#(a, a__a) | → | a__f#(b, b) |
| a__f#(X, X) | → | a__g#(a, a__a) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, a__f, h
Strategy
Instantiation
For all potential predecessors l → r of the rule a__f
#(
X,
X) → a__f
#(b, b) on dependency pair chains it holds that:
- a__f#(X, X) matches r,
- all variables of a__f#(X, X) are embedded in constructor contexts, i.e., each subterm of a__f#(X, X), containing a variable is rooted by a constructor symbol.
Thus, a__f
#(
X,
X) → a__f
#(b, b) is replaced by instances determined through the above matching. These instances are:
| a__f#(b, b) → a__f#(b, b) |
Instantiation
For all potential predecessors l → r of the rule a__f
#(
X,
X) → a__g
#(a, a__a) on dependency pair chains it holds that:
- a__f#(X, X) matches r,
- all variables of a__f#(X, X) are embedded in constructor contexts, i.e., each subterm of a__f#(X, X), containing a variable is rooted by a constructor symbol.
Thus, a__f
#(
X,
X) → a__g
#(a, a__a) is replaced by instances determined through the above matching. These instances are:
| a__f#(b, b) → a__g#(a, a__a) |
Problem 31: Propagation
Dependency Pair Problem
Dependency Pairs
| a__f#(b, b) | → | a__f#(b, b) | | a__f#(b, b) | → | a__g#(a, a__a) |
| a__g#(a, a__a) | → | a__f#(b, b) |
Rewrite Rules
| a__h(X) | → | a__g(mark(X), X) | | a__g(a, X) | → | a__f(b, X) |
| a__f(X, X) | → | a__h(a__a) | | a__a | → | b |
| mark(h(X)) | → | a__h(mark(X)) | | mark(g(X1, X2)) | → | a__g(mark(X1), X2) |
| mark(a) | → | a__a | | mark(f(X1, X2)) | → | a__f(mark(X1), X2) |
| mark(b) | → | b | | a__h(X) | → | h(X) |
| a__g(X1, X2) | → | g(X1, X2) | | a__a | → | a |
| a__f(X1, X2) | → | f(X1, X2) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, mark, a__a, a__h, a__g, h, a__f
Strategy
The dependency pairs a__f
#(b, b) → a__f
#(b, b) and a__f
#(b, b) → a__f
#(b, b) are consolidated into the rule a__f
#(b, b) → a__f
#(b, b) .
This is possible as
- all subterms of a__f#(b, b) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in a__f#(b, b), but non-replacing in both a__f#(b, b) and a__f#(b, b)
The dependency pairs a__f
#(b, b) → a__g
#(a, a__a) and a__g
#(a, a__a) → a__f
#(b, b) are consolidated into the rule a__f
#(b, b) → a__f
#(b, b) .
This is possible as
- all subterms of a__g#(a, a__a) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in a__g#(a, a__a), but non-replacing in both a__f#(b, b) and a__f#(b, b)
The dependency pairs a__f
#(b, b) → a__g
#(a, a__a) and a__g
#(a, a__a) → a__f
#(b, b) are consolidated into the rule a__f
#(b, b) → a__f
#(b, b) .
This is possible as
- all subterms of a__g#(a, a__a) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in a__g#(a, a__a), but non-replacing in both a__f#(b, b) and a__f#(b, b)
The dependency pairs a__f
#(b, b) → a__g
#(a, a__a) and a__g
#(a, a__a) → a__f
#(b, b) are consolidated into the rule a__f
#(b, b) → a__f
#(b, b) .
This is possible as
- all subterms of a__g#(a, a__a) containing variables are rooted by a constructor symbol,
- there is no variable that is replacing in a__g#(a, a__a), but non-replacing in both a__f#(b, b) and a__f#(b, b)
Summary
| Removed Dependency Pairs | Added Dependency Pairs |
|---|
| a__f#(b, b) → a__f#(b, b) | a__f#(b, b) → a__f#(b, b) |
| a__f#(b, b) → a__g#(a, a__a) | |
| a__g#(a, a__a) → a__f#(b, b) | |