YES
The TRS could be proven terminating. The proof took 508 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (44ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (101ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (171ms).
| | – Problem 4 was processed with processor DependencyGraph (1ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| *top*_0#(f_1(i_1(x))) | → | T(x) | | i_1#(x) | → | h_1#(x) |
| h_1#(x) | → | f_1#(h_1(x)) | | T(i_1(x)) | → | i_1#(x) |
| T(i_1(x_1)) | → | T(x_1) | | f_0#(f_1(i_1(x))) | → | f_1#(x) |
| *top*_0#(f_1(i_1(x))) | → | *top*_0#(x) | | T(h_1(x_1)) | → | T(x_1) |
| f_1#(h_1(x)) | → | f_1#(i_1(x)) | | T(h_1(x)) | → | h_1#(x) |
| f_1#(i_1(x)) | → | T(x) |
Rewrite Rules
| f_1(h_1(x)) | → | f_1(i_1(x)) | | h_1(x) | → | f_1(h_1(x)) |
| *top*_0(f_1(i_1(x))) | → | *top*_0(x) | | f_0(f_1(i_1(x))) | → | f_1(x) |
| f_1(i_1(x)) | → | x | | i_1(x) | → | h_1(x) |
Original Signature
Termination of terms over the following signature is verified: f_0, i_1, h_1, *top*_0, f_1
Strategy
Context-sensitive strategy:
μ(h_1#) = μ(T) = μ(i_1) = μ(f_1#) = μ(h_1) = μ(f_1) = μ(i_1#) = ∅
μ(f_0) = μ(*top*_0) = μ(f_0#) = μ(*top*_0#) = {1}
The following SCCs where found
| i_1#(x) → h_1#(x) | h_1#(x) → f_1#(h_1(x)) |
| T(i_1(x)) → i_1#(x) | T(i_1(x_1)) → T(x_1) |
| T(h_1(x_1)) → T(x_1) | f_1#(h_1(x)) → f_1#(i_1(x)) |
| T(h_1(x)) → h_1#(x) | f_1#(i_1(x)) → T(x) |
| *top*_0#(f_1(i_1(x))) → *top*_0#(x) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| *top*_0#(f_1(i_1(x))) | → | *top*_0#(x) |
Rewrite Rules
| f_1(h_1(x)) | → | f_1(i_1(x)) | | h_1(x) | → | f_1(h_1(x)) |
| *top*_0(f_1(i_1(x))) | → | *top*_0(x) | | f_0(f_1(i_1(x))) | → | f_1(x) |
| f_1(i_1(x)) | → | x | | i_1(x) | → | h_1(x) |
Original Signature
Termination of terms over the following signature is verified: f_0, i_1, h_1, *top*_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(h_1#) = μ(i_1) = μ(f_1#) = μ(h_1) = μ(f_1) = μ(i_1#) = ∅
μ(f_0) = μ(*top*_0) = μ(*top*_0#) = μ(f_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 0
- *top*_0#(x): 2x
- f_0(x): 0
- f_1(x): x
- h_1(x): x + 1
- i_1(x): x + 1
Standard Usable rules
| f_1(i_1(x)) | → | x | | h_1(x) | → | f_1(h_1(x)) |
| *top*_0(f_1(i_1(x))) | → | *top*_0(x) | | f_1(h_1(x)) | → | f_1(i_1(x)) |
| i_1(x) | → | h_1(x) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| *top*_0#(f_1(i_1(x))) | → | *top*_0#(x) |
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| i_1#(x) | → | h_1#(x) | | h_1#(x) | → | f_1#(h_1(x)) |
| T(i_1(x)) | → | i_1#(x) | | T(i_1(x_1)) | → | T(x_1) |
| T(h_1(x_1)) | → | T(x_1) | | f_1#(h_1(x)) | → | f_1#(i_1(x)) |
| T(h_1(x)) | → | h_1#(x) | | f_1#(i_1(x)) | → | T(x) |
Rewrite Rules
| f_1(h_1(x)) | → | f_1(i_1(x)) | | h_1(x) | → | f_1(h_1(x)) |
| *top*_0(f_1(i_1(x))) | → | *top*_0(x) | | f_0(f_1(i_1(x))) | → | f_1(x) |
| f_1(i_1(x)) | → | x | | i_1(x) | → | h_1(x) |
Original Signature
Termination of terms over the following signature is verified: f_0, i_1, h_1, *top*_0, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(h_1#) = μ(i_1) = μ(f_1#) = μ(h_1) = μ(f_1) = μ(i_1#) = ∅
μ(f_0) = μ(*top*_0) = μ(*top*_0#) = μ(f_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 1
- T(x): 2x + 1
- f_0(x): 0
- f_1(x): x
- f_1#(x): 2x
- h_1(x): x + 1
- h_1#(x): 2x + 2
- i_1(x): x + 1
- i_1#(x): 2x + 3
Standard Usable rules
| f_1(i_1(x)) | → | x | | h_1(x) | → | f_1(h_1(x)) |
| *top*_0(f_1(i_1(x))) | → | *top*_0(x) | | f_1(h_1(x)) | → | f_1(i_1(x)) |
| i_1(x) | → | h_1(x) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| i_1#(x) | → | h_1#(x) | | T(i_1(x_1)) | → | T(x_1) |
| T(h_1(x_1)) | → | T(x_1) | | T(h_1(x)) | → | h_1#(x) |
| f_1#(i_1(x)) | → | T(x) |
Problem 4: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| T(i_1(x)) | → | i_1#(x) | | h_1#(x) | → | f_1#(h_1(x)) |
| f_1#(h_1(x)) | → | f_1#(i_1(x)) |
Rewrite Rules
| f_1(h_1(x)) | → | f_1(i_1(x)) | | h_1(x) | → | f_1(h_1(x)) |
| *top*_0(f_1(i_1(x))) | → | *top*_0(x) | | f_0(f_1(i_1(x))) | → | f_1(x) |
| f_1(i_1(x)) | → | x | | i_1(x) | → | h_1(x) |
Original Signature
Termination of terms over the following signature is verified: f_0, i_1, h_1, *top*_0, f_1
Strategy
Context-sensitive strategy:
μ(h_1#) = μ(T) = μ(i_1) = μ(f_1#) = μ(h_1) = μ(f_1) = μ(i_1#) = ∅
μ(f_0) = μ(*top*_0) = μ(f_0#) = μ(*top*_0#) = {1}
There are no SCCs!