YES
The TRS could be proven terminating. The proof took 2334 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (103ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (167ms).
| – Problem 3 was processed with processor BackwardsNarrowing (9ms).
| | – Problem 4 was processed with processor BackwardsNarrowing (1ms).
| | | – Problem 5 was processed with processor BackwardsNarrowing (0ms).
| | | | – Problem 6 was processed with processor BackwardsNarrowing (1ms).
| | | | | – Problem 7 was processed with processor BackwardsNarrowing (1ms).
| | | | | | – Problem 8 was processed with processor BackwardsNarrowing (1ms).
| | | | | | | – Problem 9 was processed with processor BackwardsNarrowing (0ms).
| | | | | | | | – Problem 10 was processed with processor BackwardsNarrowing (0ms).
| | | | | | | | | – Problem 11 was processed with processor BackwardsNarrowing (6ms).
| | | | | | | | | | – Problem 12 was processed with processor BackwardsNarrowing (0ms).
| | | | | | | | | | | – Problem 13 was processed with processor BackwardsNarrowing (0ms).
| | | | | | | | | | | | – Problem 14 was processed with processor BackwardInstantiation (0ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| T(cons_0(x_1, x_2)) | → | T(x_1) | | *top*_0#(inf_1(x)) | → | T(x) |
| T(inf_1(x_1)) | → | T(x_1) | | s_0#(inf_1(x)) | → | cons_0#(x, inf_1(s_0(x))) |
| cons_0#(x0, inf_1(x)) | → | cons_1#(x0, cons_0(x, inf_1(s_0(x)))) | | s_0#(inf_1(x)) | → | T(x) |
| T(s_0(x_1)) | → | T(x_1) | | cons_0#(inf_1(x), x0) | → | cons_0#(x, inf_1(s_0(x))) |
| *top*_0#(inf_1(x)) | → | cons_0#(x, inf_1(s_0(x))) | | s_0#(inf_1(x)) | → | s_0#(cons_0(x, inf_1(s_0(x)))) |
| *top*_0#(inf_1(x)) | → | *top*_0#(cons_0(x, inf_1(s_0(x)))) | | T(cons_0(x_1, x_2)) | → | T(x_2) |
| cons_0#(inf_1(x), x0) | → | cons_0#(cons_0(x, inf_1(s_0(x))), x0) | | T(s_0(x)) | → | s_0#(x) |
| T(cons_0(x, inf_1(s_0(x)))) | → | cons_0#(x, inf_1(s_0(x))) | | cons_0#(inf_1(x), x0) | → | T(x) |
Rewrite Rules
| cons_1(x, cons_1(y, z)) | → | big_0 | | cons_1(x, cons_0(y, z)) | → | big_0 |
| *top*_0(inf_1(x)) | → | *top*_0(cons_0(x, inf_1(s_0(x)))) | | s_0(inf_1(x)) | → | s_0(cons_0(x, inf_1(s_0(x)))) |
| cons_0(inf_1(x), x0) | → | cons_0(cons_0(x, inf_1(s_0(x))), x0) | | cons_0(x0, inf_1(x)) | → | cons_1(x0, cons_0(x, inf_1(s_0(x)))) |
Original Signature
Termination of terms over the following signature is verified: inf_1, cons_1, big_0, cons_0, *top*_0, s_0
Strategy
Context-sensitive strategy:
μ(T) = μ(cons_1#) = μ(inf_1) = μ(cons_1) = μ(big_0) = ∅
μ(s_0#) = μ(*top*_0) = μ(*top*_0#) = μ(s_0) = {1}
μ(cons_0#) = μ(cons_0) = {1, 2}
The following SCCs where found
| *top*_0#(inf_1(x)) → *top*_0#(cons_0(x, inf_1(s_0(x)))) |
| T(cons_0(x_1, x_2)) → T(x_1) | T(cons_0(x_1, x_2)) → T(x_2) |
| T(inf_1(x_1)) → T(x_1) | cons_0#(inf_1(x), x0) → cons_0#(cons_0(x, inf_1(s_0(x))), x0) |
| s_0#(inf_1(x)) → cons_0#(x, inf_1(s_0(x))) | s_0#(inf_1(x)) → T(x) |
| T(s_0(x_1)) → T(x_1) | cons_0#(inf_1(x), x0) → cons_0#(x, inf_1(s_0(x))) |
| T(s_0(x)) → s_0#(x) | T(cons_0(x, inf_1(s_0(x)))) → cons_0#(x, inf_1(s_0(x))) |
| s_0#(inf_1(x)) → s_0#(cons_0(x, inf_1(s_0(x)))) | cons_0#(inf_1(x), x0) → T(x) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| *top*_0#(inf_1(x)) | → | *top*_0#(cons_0(x, inf_1(s_0(x)))) |
Rewrite Rules
| cons_1(x, cons_1(y, z)) | → | big_0 | | cons_1(x, cons_0(y, z)) | → | big_0 |
| *top*_0(inf_1(x)) | → | *top*_0(cons_0(x, inf_1(s_0(x)))) | | s_0(inf_1(x)) | → | s_0(cons_0(x, inf_1(s_0(x)))) |
| cons_0(inf_1(x), x0) | → | cons_0(cons_0(x, inf_1(s_0(x))), x0) | | cons_0(x0, inf_1(x)) | → | cons_1(x0, cons_0(x, inf_1(s_0(x)))) |
Original Signature
Termination of terms over the following signature is verified: inf_1, cons_1, big_0, cons_0, *top*_0, s_0
Strategy
Context-sensitive strategy:
μ(T) = μ(cons_1#) = μ(inf_1) = μ(cons_1) = μ(big_0) = ∅
μ(s_0#) = μ(*top*_0) = μ(s_0) = μ(*top*_0#) = {1}
μ(cons_0#) = μ(cons_0) = {1, 2}
Polynomial Interpretation
- *top*_0(x): 0
- *top*_0#(x): 2x
- big_0: 0
- cons_0(x,y): 0
- cons_1(x,y): 0
- inf_1(x): 2x + 1
- s_0(x): 1
Standard Usable rules
| cons_0(x0, inf_1(x)) | → | cons_1(x0, cons_0(x, inf_1(s_0(x)))) | | s_0(inf_1(x)) | → | s_0(cons_0(x, inf_1(s_0(x)))) |
| cons_1(x, cons_1(y, z)) | → | big_0 | | cons_0(inf_1(x), x0) | → | cons_0(cons_0(x, inf_1(s_0(x))), x0) |
| *top*_0(inf_1(x)) | → | *top*_0(cons_0(x, inf_1(s_0(x)))) | | cons_1(x, cons_0(y, z)) | → | big_0 |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| *top*_0#(inf_1(x)) | → | *top*_0#(cons_0(x, inf_1(s_0(x)))) |
Problem 3: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| T(cons_0(x_1, x_2)) | → | T(x_1) | | T(cons_0(x_1, x_2)) | → | T(x_2) |
| T(inf_1(x_1)) | → | T(x_1) | | cons_0#(inf_1(x), x0) | → | cons_0#(cons_0(x, inf_1(s_0(x))), x0) |
| s_0#(inf_1(x)) | → | cons_0#(x, inf_1(s_0(x))) | | s_0#(inf_1(x)) | → | T(x) |
| T(s_0(x_1)) | → | T(x_1) | | cons_0#(inf_1(x), x0) | → | cons_0#(x, inf_1(s_0(x))) |
| T(s_0(x)) | → | s_0#(x) | | T(cons_0(x, inf_1(s_0(x)))) | → | cons_0#(x, inf_1(s_0(x))) |
| s_0#(inf_1(x)) | → | s_0#(cons_0(x, inf_1(s_0(x)))) | | cons_0#(inf_1(x), x0) | → | T(x) |
Rewrite Rules
| cons_1(x, cons_1(y, z)) | → | big_0 | | cons_1(x, cons_0(y, z)) | → | big_0 |
| *top*_0(inf_1(x)) | → | *top*_0(cons_0(x, inf_1(s_0(x)))) | | s_0(inf_1(x)) | → | s_0(cons_0(x, inf_1(s_0(x)))) |
| cons_0(inf_1(x), x0) | → | cons_0(cons_0(x, inf_1(s_0(x))), x0) | | cons_0(x0, inf_1(x)) | → | cons_1(x0, cons_0(x, inf_1(s_0(x)))) |
Original Signature
Termination of terms over the following signature is verified: inf_1, cons_1, big_0, cons_0, *top*_0, s_0
Strategy
Context-sensitive strategy:
μ(T) = μ(cons_1#) = μ(inf_1) = μ(cons_1) = μ(big_0) = ∅
μ(s_0#) = μ(*top*_0) = μ(s_0) = μ(*top*_0#) = {1}
μ(cons_0#) = μ(cons_0) = {1, 2}
The left-hand side of the rule s_0
#(inf_1(
x)) → cons_0
#(
x, inf_1(s_0(
x))) is backward 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 s_0
#(inf_1(
x)) → cons_0
#(
x, inf_1(s_0(
x))) is deleted.
Problem 4: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| T(cons_0(x_1, x_2)) | → | T(x_1) | | T(cons_0(x_1, x_2)) | → | T(x_2) |
| T(inf_1(x_1)) | → | T(x_1) | | cons_0#(inf_1(x), x0) | → | cons_0#(cons_0(x, inf_1(s_0(x))), x0) |
| s_0#(inf_1(x)) | → | T(x) | | T(s_0(x_1)) | → | T(x_1) |
| cons_0#(inf_1(x), x0) | → | cons_0#(x, inf_1(s_0(x))) | | T(s_0(x)) | → | s_0#(x) |
| s_0#(inf_1(x)) | → | s_0#(cons_0(x, inf_1(s_0(x)))) | | T(cons_0(x, inf_1(s_0(x)))) | → | cons_0#(x, inf_1(s_0(x))) |
| cons_0#(inf_1(x), x0) | → | T(x) |
Rewrite Rules
| cons_1(x, cons_1(y, z)) | → | big_0 | | cons_1(x, cons_0(y, z)) | → | big_0 |
| *top*_0(inf_1(x)) | → | *top*_0(cons_0(x, inf_1(s_0(x)))) | | s_0(inf_1(x)) | → | s_0(cons_0(x, inf_1(s_0(x)))) |
| cons_0(inf_1(x), x0) | → | cons_0(cons_0(x, inf_1(s_0(x))), x0) | | cons_0(x0, inf_1(x)) | → | cons_1(x0, cons_0(x, inf_1(s_0(x)))) |
Original Signature
Termination of terms over the following signature is verified: inf_1, cons_1, cons_0, big_0, *top*_0, s_0
Strategy
Context-sensitive strategy:
μ(T) = μ(cons_1#) = μ(inf_1) = μ(cons_1) = μ(big_0) = ∅
μ(s_0#) = μ(*top*_0) = μ(*top*_0#) = μ(s_0) = {1}
μ(cons_0#) = μ(cons_0) = {1, 2}
The left-hand side of the rule cons_0
#(inf_1(
x),
x0) → cons_0
#(cons_0(
x, inf_1(s_0(
x))),
x0) is backward 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 cons_0
#(inf_1(
x),
x0) → cons_0
#(cons_0(
x, inf_1(s_0(
x))),
x0) is deleted.
Problem 5: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| T(cons_0(x_1, x_2)) | → | T(x_1) | | T(cons_0(x_1, x_2)) | → | T(x_2) |
| T(inf_1(x_1)) | → | T(x_1) | | s_0#(inf_1(x)) | → | T(x) |
| T(s_0(x_1)) | → | T(x_1) | | cons_0#(inf_1(x), x0) | → | cons_0#(x, inf_1(s_0(x))) |
| T(s_0(x)) | → | s_0#(x) | | T(cons_0(x, inf_1(s_0(x)))) | → | cons_0#(x, inf_1(s_0(x))) |
| s_0#(inf_1(x)) | → | s_0#(cons_0(x, inf_1(s_0(x)))) | | cons_0#(inf_1(x), x0) | → | T(x) |
Rewrite Rules
| cons_1(x, cons_1(y, z)) | → | big_0 | | cons_1(x, cons_0(y, z)) | → | big_0 |
| *top*_0(inf_1(x)) | → | *top*_0(cons_0(x, inf_1(s_0(x)))) | | s_0(inf_1(x)) | → | s_0(cons_0(x, inf_1(s_0(x)))) |
| cons_0(inf_1(x), x0) | → | cons_0(cons_0(x, inf_1(s_0(x))), x0) | | cons_0(x0, inf_1(x)) | → | cons_1(x0, cons_0(x, inf_1(s_0(x)))) |
Original Signature
Termination of terms over the following signature is verified: inf_1, cons_1, big_0, cons_0, *top*_0, s_0
Strategy
Context-sensitive strategy:
μ(T) = μ(cons_1#) = μ(inf_1) = μ(cons_1) = μ(big_0) = ∅
μ(s_0#) = μ(*top*_0) = μ(s_0) = μ(*top*_0#) = {1}
μ(cons_0#) = μ(cons_0) = {1, 2}
The left-hand side of the rule s_0
#(inf_1(
x)) → T(
x) is backward 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 s_0
#(inf_1(
x)) → T(
x) is deleted.
Problem 6: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| T(cons_0(x_1, x_2)) | → | T(x_1) | | T(cons_0(x_1, x_2)) | → | T(x_2) |
| T(inf_1(x_1)) | → | T(x_1) | | T(s_0(x_1)) | → | T(x_1) |
| cons_0#(inf_1(x), x0) | → | cons_0#(x, inf_1(s_0(x))) | | T(s_0(x)) | → | s_0#(x) |
| s_0#(inf_1(x)) | → | s_0#(cons_0(x, inf_1(s_0(x)))) | | T(cons_0(x, inf_1(s_0(x)))) | → | cons_0#(x, inf_1(s_0(x))) |
| cons_0#(inf_1(x), x0) | → | T(x) |
Rewrite Rules
| cons_1(x, cons_1(y, z)) | → | big_0 | | cons_1(x, cons_0(y, z)) | → | big_0 |
| *top*_0(inf_1(x)) | → | *top*_0(cons_0(x, inf_1(s_0(x)))) | | s_0(inf_1(x)) | → | s_0(cons_0(x, inf_1(s_0(x)))) |
| cons_0(inf_1(x), x0) | → | cons_0(cons_0(x, inf_1(s_0(x))), x0) | | cons_0(x0, inf_1(x)) | → | cons_1(x0, cons_0(x, inf_1(s_0(x)))) |
Original Signature
Termination of terms over the following signature is verified: inf_1, cons_1, cons_0, big_0, *top*_0, s_0
Strategy
Context-sensitive strategy:
μ(T) = μ(cons_1#) = μ(inf_1) = μ(cons_1) = μ(big_0) = ∅
μ(s_0#) = μ(*top*_0) = μ(*top*_0#) = μ(s_0) = {1}
μ(cons_0#) = μ(cons_0) = {1, 2}
The left-hand side of the rule cons_0
#(inf_1(
x),
x0) → cons_0
#(
x, inf_1(s_0(
x))) is backward 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 cons_0
#(inf_1(
x),
x0) → cons_0
#(
x, inf_1(s_0(
x))) is deleted.
Problem 7: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| T(cons_0(x_1, x_2)) | → | T(x_1) | | T(cons_0(x_1, x_2)) | → | T(x_2) |
| T(inf_1(x_1)) | → | T(x_1) | | T(s_0(x_1)) | → | T(x_1) |
| T(s_0(x)) | → | s_0#(x) | | T(cons_0(x, inf_1(s_0(x)))) | → | cons_0#(x, inf_1(s_0(x))) |
| s_0#(inf_1(x)) | → | s_0#(cons_0(x, inf_1(s_0(x)))) | | cons_0#(inf_1(x), x0) | → | T(x) |
Rewrite Rules
| cons_1(x, cons_1(y, z)) | → | big_0 | | cons_1(x, cons_0(y, z)) | → | big_0 |
| *top*_0(inf_1(x)) | → | *top*_0(cons_0(x, inf_1(s_0(x)))) | | s_0(inf_1(x)) | → | s_0(cons_0(x, inf_1(s_0(x)))) |
| cons_0(inf_1(x), x0) | → | cons_0(cons_0(x, inf_1(s_0(x))), x0) | | cons_0(x0, inf_1(x)) | → | cons_1(x0, cons_0(x, inf_1(s_0(x)))) |
Original Signature
Termination of terms over the following signature is verified: inf_1, cons_1, big_0, cons_0, *top*_0, s_0
Strategy
Context-sensitive strategy:
μ(T) = μ(cons_1#) = μ(inf_1) = μ(cons_1) = μ(big_0) = ∅
μ(s_0#) = μ(*top*_0) = μ(s_0) = μ(*top*_0#) = {1}
μ(cons_0#) = μ(cons_0) = {1, 2}
The left-hand side of the rule s_0
#(inf_1(
x)) → s_0
#(cons_0(
x, inf_1(s_0(
x)))) is backward 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 s_0
#(inf_1(
x)) → s_0
#(cons_0(
x, inf_1(s_0(
x)))) is deleted.
Problem 8: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| T(cons_0(x_1, x_2)) | → | T(x_1) | | T(cons_0(x_1, x_2)) | → | T(x_2) |
| T(inf_1(x_1)) | → | T(x_1) | | T(s_0(x_1)) | → | T(x_1) |
| T(s_0(x)) | → | s_0#(x) | | T(cons_0(x, inf_1(s_0(x)))) | → | cons_0#(x, inf_1(s_0(x))) |
| cons_0#(inf_1(x), x0) | → | T(x) |
Rewrite Rules
| cons_1(x, cons_1(y, z)) | → | big_0 | | cons_1(x, cons_0(y, z)) | → | big_0 |
| *top*_0(inf_1(x)) | → | *top*_0(cons_0(x, inf_1(s_0(x)))) | | s_0(inf_1(x)) | → | s_0(cons_0(x, inf_1(s_0(x)))) |
| cons_0(inf_1(x), x0) | → | cons_0(cons_0(x, inf_1(s_0(x))), x0) | | cons_0(x0, inf_1(x)) | → | cons_1(x0, cons_0(x, inf_1(s_0(x)))) |
Original Signature
Termination of terms over the following signature is verified: inf_1, cons_1, cons_0, big_0, *top*_0, s_0
Strategy
Context-sensitive strategy:
μ(T) = μ(cons_1#) = μ(inf_1) = μ(cons_1) = μ(big_0) = ∅
μ(s_0#) = μ(*top*_0) = μ(*top*_0#) = μ(s_0) = {1}
μ(cons_0#) = μ(cons_0) = {1, 2}
The left-hand side of the rule cons_0
#(inf_1(
x),
x0) → T(
x) is backward 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 cons_0
#(inf_1(
x),
x0) → T(
x) is deleted.
Problem 9: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| T(cons_0(x_1, x_2)) | → | T(x_1) | | T(cons_0(x_1, x_2)) | → | T(x_2) |
| T(inf_1(x_1)) | → | T(x_1) | | T(s_0(x_1)) | → | T(x_1) |
| T(s_0(x)) | → | s_0#(x) | | T(cons_0(x, inf_1(s_0(x)))) | → | cons_0#(x, inf_1(s_0(x))) |
Rewrite Rules
| cons_1(x, cons_1(y, z)) | → | big_0 | | cons_1(x, cons_0(y, z)) | → | big_0 |
| *top*_0(inf_1(x)) | → | *top*_0(cons_0(x, inf_1(s_0(x)))) | | s_0(inf_1(x)) | → | s_0(cons_0(x, inf_1(s_0(x)))) |
| cons_0(inf_1(x), x0) | → | cons_0(cons_0(x, inf_1(s_0(x))), x0) | | cons_0(x0, inf_1(x)) | → | cons_1(x0, cons_0(x, inf_1(s_0(x)))) |
Original Signature
Termination of terms over the following signature is verified: inf_1, cons_1, big_0, cons_0, *top*_0, s_0
Strategy
Context-sensitive strategy:
μ(T) = μ(cons_1#) = μ(inf_1) = μ(cons_1) = μ(big_0) = ∅
μ(s_0#) = μ(*top*_0) = μ(s_0) = μ(*top*_0#) = {1}
μ(cons_0#) = μ(cons_0) = {1, 2}
The left-hand side of the rule T(cons_0(
x_1,
x_2)) → T(
x_1) is backward 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 T(cons_0(
x_1,
x_2)) → T(
x_1) is deleted.
Problem 10: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| T(cons_0(x_1, x_2)) | → | T(x_2) | | T(inf_1(x_1)) | → | T(x_1) |
| T(s_0(x_1)) | → | T(x_1) | | T(s_0(x)) | → | s_0#(x) |
| T(cons_0(x, inf_1(s_0(x)))) | → | cons_0#(x, inf_1(s_0(x))) |
Rewrite Rules
| cons_1(x, cons_1(y, z)) | → | big_0 | | cons_1(x, cons_0(y, z)) | → | big_0 |
| *top*_0(inf_1(x)) | → | *top*_0(cons_0(x, inf_1(s_0(x)))) | | s_0(inf_1(x)) | → | s_0(cons_0(x, inf_1(s_0(x)))) |
| cons_0(inf_1(x), x0) | → | cons_0(cons_0(x, inf_1(s_0(x))), x0) | | cons_0(x0, inf_1(x)) | → | cons_1(x0, cons_0(x, inf_1(s_0(x)))) |
Original Signature
Termination of terms over the following signature is verified: inf_1, cons_1, cons_0, big_0, *top*_0, s_0
Strategy
Context-sensitive strategy:
μ(T) = μ(cons_1#) = μ(inf_1) = μ(cons_1) = μ(big_0) = ∅
μ(s_0#) = μ(*top*_0) = μ(*top*_0#) = μ(s_0) = {1}
μ(cons_0#) = μ(cons_0) = {1, 2}
The left-hand side of the rule T(cons_0(
x_1,
x_2)) → T(
x_2) is backward 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 T(cons_0(
x_1,
x_2)) → T(
x_2) is deleted.
Problem 11: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| T(inf_1(x_1)) | → | T(x_1) | | T(s_0(x_1)) | → | T(x_1) |
| T(s_0(x)) | → | s_0#(x) | | T(cons_0(x, inf_1(s_0(x)))) | → | cons_0#(x, inf_1(s_0(x))) |
Rewrite Rules
| cons_1(x, cons_1(y, z)) | → | big_0 | | cons_1(x, cons_0(y, z)) | → | big_0 |
| *top*_0(inf_1(x)) | → | *top*_0(cons_0(x, inf_1(s_0(x)))) | | s_0(inf_1(x)) | → | s_0(cons_0(x, inf_1(s_0(x)))) |
| cons_0(inf_1(x), x0) | → | cons_0(cons_0(x, inf_1(s_0(x))), x0) | | cons_0(x0, inf_1(x)) | → | cons_1(x0, cons_0(x, inf_1(s_0(x)))) |
Original Signature
Termination of terms over the following signature is verified: inf_1, cons_1, big_0, cons_0, *top*_0, s_0
Strategy
Context-sensitive strategy:
μ(T) = μ(cons_1#) = μ(inf_1) = μ(cons_1) = μ(big_0) = ∅
μ(s_0#) = μ(*top*_0) = μ(s_0) = μ(*top*_0#) = {1}
μ(cons_0#) = μ(cons_0) = {1, 2}
The left-hand side of the rule T(inf_1(
x_1)) → T(
x_1) is backward 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 T(inf_1(
x_1)) → T(
x_1) is deleted.
Problem 12: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| T(s_0(x_1)) | → | T(x_1) | | T(s_0(x)) | → | s_0#(x) |
| T(cons_0(x, inf_1(s_0(x)))) | → | cons_0#(x, inf_1(s_0(x))) |
Rewrite Rules
| cons_1(x, cons_1(y, z)) | → | big_0 | | cons_1(x, cons_0(y, z)) | → | big_0 |
| *top*_0(inf_1(x)) | → | *top*_0(cons_0(x, inf_1(s_0(x)))) | | s_0(inf_1(x)) | → | s_0(cons_0(x, inf_1(s_0(x)))) |
| cons_0(inf_1(x), x0) | → | cons_0(cons_0(x, inf_1(s_0(x))), x0) | | cons_0(x0, inf_1(x)) | → | cons_1(x0, cons_0(x, inf_1(s_0(x)))) |
Original Signature
Termination of terms over the following signature is verified: inf_1, cons_1, cons_0, big_0, *top*_0, s_0
Strategy
Context-sensitive strategy:
μ(T) = μ(cons_1#) = μ(inf_1) = μ(cons_1) = μ(big_0) = ∅
μ(s_0#) = μ(*top*_0) = μ(*top*_0#) = μ(s_0) = {1}
μ(cons_0#) = μ(cons_0) = {1, 2}
The left-hand side of the rule T(s_0(
x_1)) → T(
x_1) is backward 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 T(s_0(
x_1)) → T(
x_1) is deleted.
Problem 13: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| T(s_0(x)) | → | s_0#(x) | | T(cons_0(x, inf_1(s_0(x)))) | → | cons_0#(x, inf_1(s_0(x))) |
Rewrite Rules
| cons_1(x, cons_1(y, z)) | → | big_0 | | cons_1(x, cons_0(y, z)) | → | big_0 |
| *top*_0(inf_1(x)) | → | *top*_0(cons_0(x, inf_1(s_0(x)))) | | s_0(inf_1(x)) | → | s_0(cons_0(x, inf_1(s_0(x)))) |
| cons_0(inf_1(x), x0) | → | cons_0(cons_0(x, inf_1(s_0(x))), x0) | | cons_0(x0, inf_1(x)) | → | cons_1(x0, cons_0(x, inf_1(s_0(x)))) |
Original Signature
Termination of terms over the following signature is verified: inf_1, cons_1, big_0, cons_0, *top*_0, s_0
Strategy
Context-sensitive strategy:
μ(T) = μ(cons_1#) = μ(inf_1) = μ(cons_1) = μ(big_0) = ∅
μ(s_0#) = μ(*top*_0) = μ(s_0) = μ(*top*_0#) = {1}
μ(cons_0#) = μ(cons_0) = {1, 2}
The left-hand side of the rule T(s_0(
x)) → s_0
#(
x) is backward 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 T(s_0(
x)) → s_0
#(
x) is deleted.
Problem 14: BackwardInstantiation
Dependency Pair Problem
Dependency Pairs
| T(cons_0(x, inf_1(s_0(x)))) | → | cons_0#(x, inf_1(s_0(x))) |
Rewrite Rules
| cons_1(x, cons_1(y, z)) | → | big_0 | | cons_1(x, cons_0(y, z)) | → | big_0 |
| *top*_0(inf_1(x)) | → | *top*_0(cons_0(x, inf_1(s_0(x)))) | | s_0(inf_1(x)) | → | s_0(cons_0(x, inf_1(s_0(x)))) |
| cons_0(inf_1(x), x0) | → | cons_0(cons_0(x, inf_1(s_0(x))), x0) | | cons_0(x0, inf_1(x)) | → | cons_1(x0, cons_0(x, inf_1(s_0(x)))) |
Original Signature
Termination of terms over the following signature is verified: inf_1, cons_1, cons_0, big_0, *top*_0, s_0
Strategy
Context-sensitive strategy:
μ(T) = μ(cons_1#) = μ(inf_1) = μ(cons_1) = μ(big_0) = ∅
μ(s_0#) = μ(*top*_0) = μ(*top*_0#) = μ(s_0) = {1}
μ(cons_0#) = μ(cons_0) = {1, 2}
Instantiation
For all potential predecessors l → r of the rule T(cons_0(
x, inf_1(s_0(
x)))) → cons_0
#(
x, inf_1(s_0(
x))) on dependency pair chains it holds that:
- T(cons_0(x, inf_1(s_0(x)))) matches r,
- all variables of T(cons_0(x, inf_1(s_0(x)))) are embedded in constructor contexts, i.e., each subterm of T(cons_0(x, inf_1(s_0(x)))), containing a variable is rooted by a constructor symbol.
Thus, T(cons_0(
x, inf_1(s_0(
x)))) → cons_0
#(
x, inf_1(s_0(
x))) is replaced by instances determined through the above matching. These instances are: