YES
The TRS could be proven terminating. The proof took 548 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (31ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (150ms).
| | – Problem 3 was processed with processor DependencyGraph (1ms).
| | | – Problem 4 was processed with processor PolynomialLinearRange4 (19ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f_1#(x, x) | → | f_1#(i_0(x), g_1(g_1(x))) | | g_1#(x) | → | T(x) |
| T(g_1(x_1)) | → | T(x_1) | | T(g_1(x)) | → | g_1#(x) |
| T(g_1(g_1(x))) | → | g_1#(g_1(x)) | | f_1#(x, i_0(x)) | → | f_1#(x, x) |
| f_1#(x, y) | → | T(x) | | T(i_0(x_1)) | → | T(x_1) |
Rewrite Rules
| f_1(x, x) | → | f_1(i_0(x), g_1(g_1(x))) | | f_1(x, y) | → | x |
| g_1(x) | → | i_0(x) | | f_1(x, i_0(x)) | → | f_1(x, x) |
| f_1(i_0(x), i_0(g_1(x))) | → | a_0 |
Original Signature
Termination of terms over the following signature is verified: i_0, a_0, g_1, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(a_0) = μ(g_1) = μ(g_1#) = μ(f_1) = ∅
μ(i_0) = {1}
The following SCCs where found
| g_1#(x) → T(x) | T(g_1(x_1)) → T(x_1) |
| T(g_1(x)) → g_1#(x) | T(g_1(g_1(x))) → g_1#(g_1(x)) |
| T(i_0(x_1)) → T(x_1) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| g_1#(x) | → | T(x) | | T(g_1(x_1)) | → | T(x_1) |
| T(g_1(x)) | → | g_1#(x) | | T(g_1(g_1(x))) | → | g_1#(g_1(x)) |
| T(i_0(x_1)) | → | T(x_1) |
Rewrite Rules
| f_1(x, x) | → | f_1(i_0(x), g_1(g_1(x))) | | f_1(x, y) | → | x |
| g_1(x) | → | i_0(x) | | f_1(x, i_0(x)) | → | f_1(x, x) |
| f_1(i_0(x), i_0(g_1(x))) | → | a_0 |
Original Signature
Termination of terms over the following signature is verified: i_0, a_0, g_1, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(a_0) = μ(f_1#) = μ(g_1) = μ(g_1#) = μ(f_1) = ∅
μ(i_0) = {1}
Polynomial Interpretation
- T(x): x
- a_0: 0
- f_1(x,y): x
- g_1(x): 2x + 1
- g_1#(x): 2x + 1
- i_0(x): x
Standard Usable rules
| f_1(i_0(x), i_0(g_1(x))) | → | a_0 | | g_1(x) | → | i_0(x) |
| f_1(x, i_0(x)) | → | f_1(x, x) | | f_1(x, y) | → | x |
| f_1(x, x) | → | f_1(i_0(x), g_1(g_1(x))) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| T(g_1(x_1)) | → | T(x_1) | | g_1#(x) | → | T(x) |
Problem 3: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| T(g_1(g_1(x))) | → | g_1#(g_1(x)) | | T(g_1(x)) | → | g_1#(x) |
| T(i_0(x_1)) | → | T(x_1) |
Rewrite Rules
| f_1(x, x) | → | f_1(i_0(x), g_1(g_1(x))) | | f_1(x, y) | → | x |
| g_1(x) | → | i_0(x) | | f_1(x, i_0(x)) | → | f_1(x, x) |
| f_1(i_0(x), i_0(g_1(x))) | → | a_0 |
Original Signature
Termination of terms over the following signature is verified: i_0, a_0, g_1, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(f_1#) = μ(a_0) = μ(g_1) = μ(g_1#) = μ(f_1) = ∅
μ(i_0) = {1}
The following SCCs where found
Problem 4: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| f_1(x, x) | → | f_1(i_0(x), g_1(g_1(x))) | | f_1(x, y) | → | x |
| g_1(x) | → | i_0(x) | | f_1(x, i_0(x)) | → | f_1(x, x) |
| f_1(i_0(x), i_0(g_1(x))) | → | a_0 |
Original Signature
Termination of terms over the following signature is verified: i_0, a_0, g_1, f_1
Strategy
Context-sensitive strategy:
μ(T) = μ(a_0) = μ(f_1#) = μ(g_1) = μ(g_1#) = μ(f_1) = ∅
μ(i_0) = {1}
Polynomial Interpretation
- T(x): x
- a_0: 0
- f_1(x,y): 0
- g_1(x): 0
- i_0(x): x + 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: