YES
The TRS could be proven terminating. The proof took 1312 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (119ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (180ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (155ms).
| | – Problem 5 was processed with processor BackwardsNarrowing (1ms).
| | | – Problem 7 was processed with processor ForwardNarrowing (3ms).
| | | – Problem 8 was processed with processor BackwardsNarrowing (0ms).
| – Problem 4 was processed with processor PolynomialLinearRange4 (85ms).
| | – Problem 6 was processed with processor PolynomialLinearRange4 (16ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| T(f_0(x_1, x_2)) | → | T(x_2) | | T(f_0(x_1, x_2)) | → | T(x_1) |
| T(f_1(x, y)) | → | f_1#(x, y) | | *top*_0#(a_1) | → | *top*_0#(f_0(a_1, a_1)) |
| *top*_0#(a_1) | → | f_0#(a_1, a_1) | | f_0#(x0, a_1) | → | f_1#(x0, f_0(a_1, a_1)) |
| T(f_0(a_1, a_1)) | → | f_0#(a_1, a_1) | | f_0#(a_1, x0) | → | f_1#(f_0(a_1, a_1), x0) |
| T(f_1(x_1, x_2)) | → | T(x_2) | | T(f_0(x, y)) | → | f_0#(x, y) |
| f_1#(x, f_1(y, z)) | → | f_1#(f_1(x, y), z) | | f_1#(x, f_0(y, z)) | → | f_1#(f_0(x, y), z) |
| T(f_1(x_1, x_2)) | → | T(x_1) | | f_1#(x, f_0(y, z)) | → | f_1#(f_1(x, y), z) |
| f_1#(x, f_1(y, z)) | → | f_1#(f_0(x, y), z) |
Rewrite Rules
| f_1(f_1(x, y), z) | → | c_0 | | f_1(f_0(x, y), z) | → | c_0 |
| f_1(x, f_1(y, z)) | → | f_1(f_0(x, y), z) | | f_1(x, f_1(y, z)) | → | f_1(f_1(x, y), z) |
| f_1(x, f_0(y, z)) | → | f_1(f_1(x, y), z) | | f_1(x, f_0(y, z)) | → | f_1(f_0(x, y), z) |
| *top*_0(a_1) | → | *top*_0(f_0(a_1, a_1)) | | f_0(a_1, x0) | → | f_1(f_0(a_1, a_1), x0) |
| f_0(x0, a_1) | → | f_1(x0, f_0(a_1, a_1)) |
Original Signature
Termination of terms over the following signature is verified: f_0, a_1, *top*_0, c_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(a_1) = μ(c_0) = μ(f_1) = ∅
μ(*top*_0) = μ(*top*_0#) = {1}
μ(f_0) = μ(f_0#) = {1, 2}
The following SCCs where found
| *top*_0#(a_1) → *top*_0#(f_0(a_1, a_1)) |
| f_1#(x, f_1(y, z)) → f_1#(f_1(x, y), z) | f_1#(x, f_0(y, z)) → f_1#(f_0(x, y), z) |
| f_1#(x, f_0(y, z)) → f_1#(f_1(x, y), z) | f_1#(x, f_1(y, z)) → f_1#(f_0(x, y), z) |
| T(f_0(x_1, x_2)) → T(x_2) | T(f_0(x_1, x_2)) → T(x_1) |
| T(f_1(x_1, x_2)) → T(x_1) | T(f_1(x_1, x_2)) → T(x_2) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| *top*_0#(a_1) | → | *top*_0#(f_0(a_1, a_1)) |
Rewrite Rules
| f_1(f_1(x, y), z) | → | c_0 | | f_1(f_0(x, y), z) | → | c_0 |
| f_1(x, f_1(y, z)) | → | f_1(f_0(x, y), z) | | f_1(x, f_1(y, z)) | → | f_1(f_1(x, y), z) |
| f_1(x, f_0(y, z)) | → | f_1(f_1(x, y), z) | | f_1(x, f_0(y, z)) | → | f_1(f_0(x, y), z) |
| *top*_0(a_1) | → | *top*_0(f_0(a_1, a_1)) | | f_0(a_1, x0) | → | f_1(f_0(a_1, a_1), x0) |
| f_0(x0, a_1) | → | f_1(x0, f_0(a_1, a_1)) |
Original Signature
Termination of terms over the following signature is verified: f_0, a_1, *top*_0, c_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(a_1) = μ(c_0) = μ(f_1) = ∅
μ(*top*_0) = μ(*top*_0#) = {1}
μ(f_0) = μ(f_0#) = {1, 2}
Polynomial Interpretation
- *top*_0(x): 0
- *top*_0#(x): 2x + 1
- a_1: 1
- c_0: 0
- f_0(x,y): 0
- f_1(x,y): 0
Standard Usable rules
| f_1(x, f_1(y, z)) | → | f_1(f_0(x, y), z) | | f_1(x, f_0(y, z)) | → | f_1(f_1(x, y), z) |
| f_1(x, f_0(y, z)) | → | f_1(f_0(x, y), z) | | f_0(a_1, x0) | → | f_1(f_0(a_1, a_1), x0) |
| f_1(f_1(x, y), z) | → | c_0 | | f_1(x, f_1(y, z)) | → | f_1(f_1(x, y), z) |
| f_0(x0, a_1) | → | f_1(x0, f_0(a_1, a_1)) | | f_1(f_0(x, y), z) | → | c_0 |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| *top*_0#(a_1) | → | *top*_0#(f_0(a_1, a_1)) |
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| f_1#(x, f_1(y, z)) | → | f_1#(f_1(x, y), z) | | f_1#(x, f_0(y, z)) | → | f_1#(f_0(x, y), z) |
| f_1#(x, f_0(y, z)) | → | f_1#(f_1(x, y), z) | | f_1#(x, f_1(y, z)) | → | f_1#(f_0(x, y), z) |
Rewrite Rules
| f_1(f_1(x, y), z) | → | c_0 | | f_1(f_0(x, y), z) | → | c_0 |
| f_1(x, f_1(y, z)) | → | f_1(f_0(x, y), z) | | f_1(x, f_1(y, z)) | → | f_1(f_1(x, y), z) |
| f_1(x, f_0(y, z)) | → | f_1(f_1(x, y), z) | | f_1(x, f_0(y, z)) | → | f_1(f_0(x, y), z) |
| *top*_0(a_1) | → | *top*_0(f_0(a_1, a_1)) | | f_0(a_1, x0) | → | f_1(f_0(a_1, a_1), x0) |
| f_0(x0, a_1) | → | f_1(x0, f_0(a_1, a_1)) |
Original Signature
Termination of terms over the following signature is verified: f_0, a_1, *top*_0, c_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(a_1) = μ(c_0) = μ(f_1) = ∅
μ(*top*_0) = μ(*top*_0#) = {1}
μ(f_0) = μ(f_0#) = {1, 2}
Polynomial Interpretation
- *top*_0(x): 0
- a_1: 0
- c_0: 0
- f_0(x,y): 2y + 2
- f_1(x,y): y
- f_1#(x,y): y
Standard Usable rules
| f_1(x, f_0(y, z)) | → | f_1(f_1(x, y), z) | | f_1(x, f_1(y, z)) | → | f_1(f_0(x, y), z) |
| f_0(a_1, x0) | → | f_1(f_0(a_1, a_1), x0) | | f_1(x, f_0(y, z)) | → | f_1(f_0(x, y), z) |
| f_1(x, f_1(y, z)) | → | f_1(f_1(x, y), z) | | f_1(f_1(x, y), z) | → | c_0 |
| f_0(x0, a_1) | → | f_1(x0, f_0(a_1, a_1)) | | f_1(f_0(x, y), z) | → | c_0 |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f_1#(x, f_0(y, z)) | → | f_1#(f_0(x, y), z) | | f_1#(x, f_0(y, z)) | → | f_1#(f_1(x, y), z) |
Problem 5: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| f_1#(x, f_1(y, z)) | → | f_1#(f_1(x, y), z) | | f_1#(x, f_1(y, z)) | → | f_1#(f_0(x, y), z) |
Rewrite Rules
| f_1(f_1(x, y), z) | → | c_0 | | f_1(f_0(x, y), z) | → | c_0 |
| f_1(x, f_1(y, z)) | → | f_1(f_0(x, y), z) | | f_1(x, f_1(y, z)) | → | f_1(f_1(x, y), z) |
| f_1(x, f_0(y, z)) | → | f_1(f_1(x, y), z) | | f_1(x, f_0(y, z)) | → | f_1(f_0(x, y), z) |
| *top*_0(a_1) | → | *top*_0(f_0(a_1, a_1)) | | f_0(a_1, x0) | → | f_1(f_0(a_1, a_1), x0) |
| f_0(x0, a_1) | → | f_1(x0, f_0(a_1, a_1)) |
Original Signature
Termination of terms over the following signature is verified: f_0, a_1, *top*_0, c_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(a_1) = μ(c_0) = μ(f_1) = ∅
μ(*top*_0) = μ(*top*_0#) = {1}
μ(f_0) = μ(f_0#) = {1, 2}
The left-hand side of the rule f_1
#(
x, f_1(
y,
z)) → f_1
#(f_1(
x,
y),
z) 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 f_1
#(
x, f_1(
y,
z)) → f_1
#(f_1(
x,
y),
z) is deleted.
Problem 7: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| f_1#(x, f_1(y, z)) | → | f_1#(f_0(x, y), z) |
Rewrite Rules
| f_1(f_1(x, y), z) | → | c_0 | | f_1(f_0(x, y), z) | → | c_0 |
| f_1(x, f_1(y, z)) | → | f_1(f_0(x, y), z) | | f_1(x, f_1(y, z)) | → | f_1(f_1(x, y), z) |
| f_1(x, f_0(y, z)) | → | f_1(f_1(x, y), z) | | f_1(x, f_0(y, z)) | → | f_1(f_0(x, y), z) |
| *top*_0(a_1) | → | *top*_0(f_0(a_1, a_1)) | | f_0(a_1, x0) | → | f_1(f_0(a_1, a_1), x0) |
| f_0(x0, a_1) | → | f_1(x0, f_0(a_1, a_1)) |
Original Signature
Termination of terms over the following signature is verified: f_0, a_1, *top*_0, c_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(a_1) = μ(c_0) = μ(f_1) = ∅
μ(*top*_0) = μ(*top*_0#) = {1}
μ(f_0) = μ(f_0#) = {1, 2}
The right-hand side of the rule f_1
#(
x, f_1(
y,
z)) → f_1
#(f_0(
x,
y),
z) 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 f_1
#(
x, f_1(
y,
z)) → f_1
#(f_0(
x,
y),
z) is deleted.
Problem 8: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| f_1#(x, f_1(y, z)) | → | f_1#(f_0(x, y), z) |
Rewrite Rules
| f_1(f_1(x, y), z) | → | c_0 | | f_1(f_0(x, y), z) | → | c_0 |
| f_1(x, f_1(y, z)) | → | f_1(f_0(x, y), z) | | f_1(x, f_1(y, z)) | → | f_1(f_1(x, y), z) |
| f_1(x, f_0(y, z)) | → | f_1(f_1(x, y), z) | | f_1(x, f_0(y, z)) | → | f_1(f_0(x, y), z) |
| *top*_0(a_1) | → | *top*_0(f_0(a_1, a_1)) | | f_0(a_1, x0) | → | f_1(f_0(a_1, a_1), x0) |
| f_0(x0, a_1) | → | f_1(x0, f_0(a_1, a_1)) |
Original Signature
Termination of terms over the following signature is verified: f_0, a_1, *top*_0, c_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(a_1) = μ(c_0) = μ(f_1) = ∅
μ(*top*_0) = μ(*top*_0#) = {1}
μ(f_0) = μ(f_0#) = {1, 2}
The left-hand side of the rule f_1
#(
x, f_1(
y,
z)) → f_1
#(f_0(
x,
y),
z) 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 f_1
#(
x, f_1(
y,
z)) → f_1
#(f_0(
x,
y),
z) is deleted.
Problem 4: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| T(f_0(x_1, x_2)) | → | T(x_2) | | T(f_0(x_1, x_2)) | → | T(x_1) |
| T(f_1(x_1, x_2)) | → | T(x_1) | | T(f_1(x_1, x_2)) | → | T(x_2) |
Rewrite Rules
| f_1(f_1(x, y), z) | → | c_0 | | f_1(f_0(x, y), z) | → | c_0 |
| f_1(x, f_1(y, z)) | → | f_1(f_0(x, y), z) | | f_1(x, f_1(y, z)) | → | f_1(f_1(x, y), z) |
| f_1(x, f_0(y, z)) | → | f_1(f_1(x, y), z) | | f_1(x, f_0(y, z)) | → | f_1(f_0(x, y), z) |
| *top*_0(a_1) | → | *top*_0(f_0(a_1, a_1)) | | f_0(a_1, x0) | → | f_1(f_0(a_1, a_1), x0) |
| f_0(x0, a_1) | → | f_1(x0, f_0(a_1, a_1)) |
Original Signature
Termination of terms over the following signature is verified: f_0, a_1, *top*_0, c_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(a_1) = μ(c_0) = μ(f_1) = ∅
μ(*top*_0) = μ(*top*_0#) = {1}
μ(f_0) = μ(f_0#) = {1, 2}
Polynomial Interpretation
- *top*_0(x): 0
- T(x): 3x
- a_1: 0
- c_0: 0
- f_0(x,y): y + x + 1
- f_1(x,y): y + 3x
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| T(f_0(x_1, x_2)) | → | T(x_2) | | T(f_0(x_1, x_2)) | → | T(x_1) |
Problem 6: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| T(f_1(x_1, x_2)) | → | T(x_1) | | T(f_1(x_1, x_2)) | → | T(x_2) |
Rewrite Rules
| f_1(f_1(x, y), z) | → | c_0 | | f_1(f_0(x, y), z) | → | c_0 |
| f_1(x, f_1(y, z)) | → | f_1(f_0(x, y), z) | | f_1(x, f_1(y, z)) | → | f_1(f_1(x, y), z) |
| f_1(x, f_0(y, z)) | → | f_1(f_1(x, y), z) | | f_1(x, f_0(y, z)) | → | f_1(f_0(x, y), z) |
| *top*_0(a_1) | → | *top*_0(f_0(a_1, a_1)) | | f_0(a_1, x0) | → | f_1(f_0(a_1, a_1), x0) |
| f_0(x0, a_1) | → | f_1(x0, f_0(a_1, a_1)) |
Original Signature
Termination of terms over the following signature is verified: f_0, a_1, *top*_0, c_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(a_1) = μ(c_0) = μ(f_1) = ∅
μ(*top*_0) = μ(*top*_0#) = {1}
μ(f_0) = μ(f_0#) = {1, 2}
Polynomial Interpretation
- *top*_0(x): 0
- T(x): 2x
- a_1: 0
- c_0: 0
- f_0(x,y): 0
- f_1(x,y): 2y + 2x + 1
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| T(f_1(x_1, x_2)) | → | T(x_1) | | T(f_1(x_1, x_2)) | → | T(x_2) |