YES
The TRS could be proven terminating. The proof took 1530 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (65ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (191ms).
| | – Problem 4 was processed with processor BackwardsNarrowing (2ms).
| | | – Problem 5 was processed with processor ForwardNarrowing (1ms).
| | | | – Problem 7 was processed with processor ForwardNarrowing (1ms).
| | | | | – Problem 8 was processed with processor ForwardNarrowing (1ms).
| | | – Problem 6 was processed with processor BackwardsNarrowing (0ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (137ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f_0#(f_0(f_0(a_1))) | → | f_1#(f_0(f_0(f_0(a_1)))) | | *top*_0#(f_0(f_0(a_1))) | → | f_0#(f_0(f_0(a_1))) |
| T(f_0(a_1)) | → | f_0#(a_1) | | *top*_0#(f_0(f_0(a_1))) | → | f_0#(f_0(a_1)) |
| *top*_0#(f_0(f_0(a_1))) | → | f_0#(a_1) | | *top*_0#(f_0(a_1)) | → | f_0#(a_1) |
| T(f_0(f_0(a_1))) | → | f_0#(f_0(a_1)) | | *top*_0#(a_1) | → | f_0#(a_1) |
| *top*_0#(a_1) | → | *top*_0#(f_0(a_1)) | | *top*_0#(f_0(a_1)) | → | f_0#(f_0(a_1)) |
| *top*_0#(f_0(a_1)) | → | *top*_0#(f_0(f_0(a_1))) | | *top*_0#(f_0(f_0(a_1))) | → | *top*_0#(f_0(f_0(f_0(a_1)))) |
| T(f_0(x_1)) | → | T(x_1) | | T(f_0(f_0(f_0(a_1)))) | → | f_0#(f_0(f_0(a_1))) |
Rewrite Rules
| *top*_0(a_1) | → | *top*_0(f_0(a_1)) | | *top*_0(f_0(a_1)) | → | *top*_0(f_0(f_0(a_1))) |
| *top*_0(f_0(f_0(a_1))) | → | *top*_0(f_0(f_0(f_0(a_1)))) | | f_0(f_0(f_0(a_1))) | → | f_1(f_0(f_0(f_0(a_1)))) |
| f_1(f_1(f_0(f_0(x)))) | → | c_0 | | f_1(f_0(f_0(f_0(x)))) | → | c_0 |
| f_1(f_1(f_1(f_0(x)))) | → | c_0 | | f_1(f_1(f_1(f_1(x)))) | → | c_0 |
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) = ∅
μ(f_0) = μ(*top*_0) = μ(f_0#) = μ(*top*_0#) = {1}
The following SCCs where found
| *top*_0#(f_0(a_1)) → *top*_0#(f_0(f_0(a_1))) | *top*_0#(f_0(f_0(a_1))) → *top*_0#(f_0(f_0(f_0(a_1)))) |
| *top*_0#(a_1) → *top*_0#(f_0(a_1)) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| *top*_0#(f_0(a_1)) | → | *top*_0#(f_0(f_0(a_1))) | | *top*_0#(f_0(f_0(a_1))) | → | *top*_0#(f_0(f_0(f_0(a_1)))) |
| *top*_0#(a_1) | → | *top*_0#(f_0(a_1)) |
Rewrite Rules
| *top*_0(a_1) | → | *top*_0(f_0(a_1)) | | *top*_0(f_0(a_1)) | → | *top*_0(f_0(f_0(a_1))) |
| *top*_0(f_0(f_0(a_1))) | → | *top*_0(f_0(f_0(f_0(a_1)))) | | f_0(f_0(f_0(a_1))) | → | f_1(f_0(f_0(f_0(a_1)))) |
| f_1(f_1(f_0(f_0(x)))) | → | c_0 | | f_1(f_0(f_0(f_0(x)))) | → | c_0 |
| f_1(f_1(f_1(f_0(x)))) | → | c_0 | | f_1(f_1(f_1(f_1(x)))) | → | c_0 |
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) = ∅
μ(f_0) = μ(*top*_0) = μ(*top*_0#) = μ(f_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 0
- *top*_0#(x): 2x
- a_1: 1
- c_0: 0
- f_0(x): 0
- f_1(x): 0
Standard Usable rules
| f_1(f_1(f_0(f_0(x)))) | → | c_0 | | f_1(f_0(f_0(f_0(x)))) | → | c_0 |
| f_1(f_1(f_1(f_1(x)))) | → | c_0 | | f_1(f_1(f_1(f_0(x)))) | → | c_0 |
| f_0(f_0(f_0(a_1))) | → | f_1(f_0(f_0(f_0(a_1)))) |
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)) |
Problem 4: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| *top*_0#(f_0(a_1)) | → | *top*_0#(f_0(f_0(a_1))) | | *top*_0#(f_0(f_0(a_1))) | → | *top*_0#(f_0(f_0(f_0(a_1)))) |
Rewrite Rules
| *top*_0(a_1) | → | *top*_0(f_0(a_1)) | | *top*_0(f_0(a_1)) | → | *top*_0(f_0(f_0(a_1))) |
| *top*_0(f_0(f_0(a_1))) | → | *top*_0(f_0(f_0(f_0(a_1)))) | | f_0(f_0(f_0(a_1))) | → | f_1(f_0(f_0(f_0(a_1)))) |
| f_1(f_1(f_0(f_0(x)))) | → | c_0 | | f_1(f_0(f_0(f_0(x)))) | → | c_0 |
| f_1(f_1(f_1(f_0(x)))) | → | c_0 | | f_1(f_1(f_1(f_1(x)))) | → | c_0 |
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) = ∅
μ(f_0) = μ(*top*_0) = μ(f_0#) = μ(*top*_0#) = {1}
The left-hand side of the rule *top*_0
#(f_0(a_1)) → *top*_0
#(f_0(f_0(a_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 *top*_0
#(f_0(a_1)) → *top*_0
#(f_0(f_0(a_1))) is deleted.
Problem 5: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| *top*_0#(f_0(a_1)) | → | *top*_0#(f_0(f_0(a_1))) | | *top*_0#(f_0(f_0(a_1))) | → | *top*_0#(f_1(f_0(f_0(f_0(a_1))))) |
Rewrite Rules
| *top*_0(a_1) | → | *top*_0(f_0(a_1)) | | *top*_0(f_0(a_1)) | → | *top*_0(f_0(f_0(a_1))) |
| *top*_0(f_0(f_0(a_1))) | → | *top*_0(f_0(f_0(f_0(a_1)))) | | f_0(f_0(f_0(a_1))) | → | f_1(f_0(f_0(f_0(a_1)))) |
| f_1(f_1(f_0(f_0(x)))) | → | c_0 | | f_1(f_0(f_0(f_0(x)))) | → | c_0 |
| f_1(f_1(f_1(f_0(x)))) | → | c_0 | | f_1(f_1(f_1(f_1(x)))) | → | c_0 |
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) = ∅
μ(f_0) = μ(*top*_0) = μ(*top*_0#) = μ(f_0#) = {1}
The right-hand side of the rule *top*_0
#(f_0(f_0(a_1))) → *top*_0
#(f_1(f_0(f_0(f_0(a_1))))) 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 |
|---|
| *top*_0#(c_0) | |
Thus, the rule *top*_0
#(f_0(f_0(a_1))) → *top*_0
#(f_1(f_0(f_0(f_0(a_1))))) is replaced by the following rules:
| *top*_0#(f_0(f_0(a_1))) → *top*_0#(c_0) |
Problem 7: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| *top*_0#(f_0(a_1)) | → | *top*_0#(f_0(f_0(a_1))) | | *top*_0#(f_0(f_0(a_1))) | → | *top*_0#(c_0) |
Rewrite Rules
| *top*_0(a_1) | → | *top*_0(f_0(a_1)) | | *top*_0(f_0(a_1)) | → | *top*_0(f_0(f_0(a_1))) |
| *top*_0(f_0(f_0(a_1))) | → | *top*_0(f_0(f_0(f_0(a_1)))) | | f_0(f_0(f_0(a_1))) | → | f_1(f_0(f_0(f_0(a_1)))) |
| f_1(f_1(f_0(f_0(x)))) | → | c_0 | | f_1(f_0(f_0(f_0(x)))) | → | c_0 |
| f_1(f_1(f_1(f_0(x)))) | → | c_0 | | f_1(f_1(f_1(f_1(x)))) | → | c_0 |
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) = ∅
μ(f_0) = μ(*top*_0) = μ(f_0#) = μ(*top*_0#) = {1}
The right-hand side of the rule *top*_0
#(f_0(f_0(a_1))) → *top*_0
#(c_0) 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 *top*_0
#(f_0(f_0(a_1))) → *top*_0
#(c_0) is deleted.
Problem 8: ForwardNarrowing
Dependency Pair Problem
Dependency Pairs
| *top*_0#(f_0(a_1)) | → | *top*_0#(f_0(f_0(a_1))) |
Rewrite Rules
| *top*_0(a_1) | → | *top*_0(f_0(a_1)) | | *top*_0(f_0(a_1)) | → | *top*_0(f_0(f_0(a_1))) |
| *top*_0(f_0(f_0(a_1))) | → | *top*_0(f_0(f_0(f_0(a_1)))) | | f_0(f_0(f_0(a_1))) | → | f_1(f_0(f_0(f_0(a_1)))) |
| f_1(f_1(f_0(f_0(x)))) | → | c_0 | | f_1(f_0(f_0(f_0(x)))) | → | c_0 |
| f_1(f_1(f_1(f_0(x)))) | → | c_0 | | f_1(f_1(f_1(f_1(x)))) | → | c_0 |
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) = ∅
μ(f_0) = μ(*top*_0) = μ(*top*_0#) = μ(f_0#) = {1}
The right-hand side of the rule *top*_0
#(f_0(a_1)) → *top*_0
#(f_0(f_0(a_1))) 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 *top*_0
#(f_0(a_1)) → *top*_0
#(f_0(f_0(a_1))) is deleted.
Problem 6: BackwardsNarrowing
Dependency Pair Problem
Dependency Pairs
| *top*_0#(f_0(f_0(a_1))) | → | *top*_0#(f_0(f_0(f_0(a_1)))) |
Rewrite Rules
| *top*_0(a_1) | → | *top*_0(f_0(a_1)) | | *top*_0(f_0(a_1)) | → | *top*_0(f_0(f_0(a_1))) |
| *top*_0(f_0(f_0(a_1))) | → | *top*_0(f_0(f_0(f_0(a_1)))) | | f_0(f_0(f_0(a_1))) | → | f_1(f_0(f_0(f_0(a_1)))) |
| f_1(f_1(f_0(f_0(x)))) | → | c_0 | | f_1(f_0(f_0(f_0(x)))) | → | c_0 |
| f_1(f_1(f_1(f_0(x)))) | → | c_0 | | f_1(f_1(f_1(f_1(x)))) | → | c_0 |
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) = ∅
μ(f_0) = μ(*top*_0) = μ(*top*_0#) = μ(f_0#) = {1}
The left-hand side of the rule *top*_0
#(f_0(f_0(a_1))) → *top*_0
#(f_0(f_0(f_0(a_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 *top*_0
#(f_0(f_0(a_1))) → *top*_0
#(f_0(f_0(f_0(a_1)))) is deleted.
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| *top*_0(a_1) | → | *top*_0(f_0(a_1)) | | *top*_0(f_0(a_1)) | → | *top*_0(f_0(f_0(a_1))) |
| *top*_0(f_0(f_0(a_1))) | → | *top*_0(f_0(f_0(f_0(a_1)))) | | f_0(f_0(f_0(a_1))) | → | f_1(f_0(f_0(f_0(a_1)))) |
| f_1(f_1(f_0(f_0(x)))) | → | c_0 | | f_1(f_0(f_0(f_0(x)))) | → | c_0 |
| f_1(f_1(f_1(f_0(x)))) | → | c_0 | | f_1(f_1(f_1(f_1(x)))) | → | c_0 |
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) = ∅
μ(f_0) = μ(*top*_0) = μ(*top*_0#) = μ(f_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 0
- T(x): x
- a_1: 0
- c_0: 0
- f_0(x): x + 1
- f_1(x): 0
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed: