YES
The TRS could be proven terminating. The proof took 774 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (62ms).
| – Problem 2 was processed with processor PolynomialLinearRange4 (178ms).
| | – Problem 5 was processed with processor PolynomialLinearRange4 (130ms).
| | | – Problem 7 was processed with processor DependencyGraph (10ms).
| – Problem 3 was processed with processor PolynomialLinearRange4 (157ms).
| – Problem 4 was processed with processor PolynomialLinearRange4 (63ms).
| | – Problem 6 was processed with processor PolynomialLinearRange4 (17ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f_1#(g_1(a_0)) | → | s_0#(g_1(b_0)) | | T(g_1(x)) | → | g_1#(x) |
| *top*_0#(g_1(x)) | → | *top*_0#(f_0(g_1(x))) | | f_1#(g_1(a_0)) | → | f_0#(s_0(g_1(b_0))) |
| g_1#(x) | → | f_1#(g_1(x)) | | f_1#(g_1(a_0)) | → | g_1#(b_0) |
| T(f_0(g_1(x))) | → | f_0#(g_1(x)) | | *top*_0#(g_1(x)) | → | f_0#(g_1(x)) |
| T(g_1(x_1)) | → | T(x_1) | | T(g_1(x)) | → | g_1#(x) |
| s_0#(g_1(x)) | → | f_0#(g_1(x)) | | *top*_0#(g_1(x)) | → | g_1#(x) |
| s_0#(g_1(x)) | → | s_0#(f_0(g_1(x))) | | s_0#(g_1(x)) | → | g_1#(x) |
| f_0#(g_1(x)) | → | f_1#(f_0(g_1(x))) | | T(f_0(x_1)) | → | T(x_1) |
Rewrite Rules
| f_1(g_1(a_0)) | → | f_0(s_0(g_1(b_0))) | | f_1(f_0(x)) | → | b_0 |
| f_1(f_1(x)) | → | b_0 | | g_1(x) | → | f_1(g_1(x)) |
| *top*_0(g_1(x)) | → | *top*_0(f_0(g_1(x))) | | f_0(g_1(x)) | → | f_1(f_0(g_1(x))) |
| s_0(g_1(x)) | → | s_0(f_0(g_1(x))) |
Original Signature
Termination of terms over the following signature is verified: f_0, a_0, *top*_0, g_1, b_0, f_1, s_0
Strategy
Context-sensitive strategy:
μ(f_1#) = μ(b_0) = μ(g_1#) = μ(T) = μ(a_0) = μ(g_1) = μ(f_1) = ∅
μ(s_0#) = μ(f_0#) = μ(f_0) = μ(*top*_0) = μ(s_0) = μ(*top*_0#) = {1}
The following SCCs where found
| *top*_0#(g_1(x)) → *top*_0#(f_0(g_1(x))) |
| T(g_1(x_1)) → T(x_1) | T(f_0(x_1)) → T(x_1) |
| f_1#(g_1(a_0)) → s_0#(g_1(b_0)) | g_1#(x) → f_1#(g_1(x)) |
| f_1#(g_1(a_0)) → g_1#(b_0) | s_0#(g_1(x)) → s_0#(f_0(g_1(x))) |
| s_0#(g_1(x)) → g_1#(x) |
Problem 2: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| f_1#(g_1(a_0)) | → | s_0#(g_1(b_0)) | | g_1#(x) | → | f_1#(g_1(x)) |
| f_1#(g_1(a_0)) | → | g_1#(b_0) | | s_0#(g_1(x)) | → | s_0#(f_0(g_1(x))) |
| s_0#(g_1(x)) | → | g_1#(x) |
Rewrite Rules
| f_1(g_1(a_0)) | → | f_0(s_0(g_1(b_0))) | | f_1(f_0(x)) | → | b_0 |
| f_1(f_1(x)) | → | b_0 | | g_1(x) | → | f_1(g_1(x)) |
| *top*_0(g_1(x)) | → | *top*_0(f_0(g_1(x))) | | f_0(g_1(x)) | → | f_1(f_0(g_1(x))) |
| s_0(g_1(x)) | → | s_0(f_0(g_1(x))) |
Original Signature
Termination of terms over the following signature is verified: f_0, a_0, *top*_0, g_1, b_0, f_1, s_0
Strategy
Context-sensitive strategy:
μ(f_1#) = μ(b_0) = μ(g_1#) = μ(T) = μ(a_0) = μ(g_1) = μ(f_1) = ∅
μ(s_0#) = μ(f_0#) = μ(f_0) = μ(*top*_0) = μ(s_0) = μ(*top*_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 0
- a_0: 1
- b_0: 0
- f_0(x): 0
- f_1(x): 0
- f_1#(x): 2x + 1
- g_1(x): 1
- g_1#(x): 3
- s_0(x): 2x
- s_0#(x): 2x + 1
Standard Usable rules
| g_1(x) | → | f_1(g_1(x)) | | f_1(f_0(x)) | → | b_0 |
| f_1(g_1(a_0)) | → | f_0(s_0(g_1(b_0))) | | f_1(f_1(x)) | → | b_0 |
| s_0(g_1(x)) | → | s_0(f_0(g_1(x))) | | f_0(g_1(x)) | → | f_1(f_0(g_1(x))) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| s_0#(g_1(x)) | → | s_0#(f_0(g_1(x))) |
Problem 5: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| f_1#(g_1(a_0)) | → | s_0#(g_1(b_0)) | | g_1#(x) | → | f_1#(g_1(x)) |
| f_1#(g_1(a_0)) | → | g_1#(b_0) | | s_0#(g_1(x)) | → | g_1#(x) |
Rewrite Rules
| f_1(g_1(a_0)) | → | f_0(s_0(g_1(b_0))) | | f_1(f_0(x)) | → | b_0 |
| f_1(f_1(x)) | → | b_0 | | g_1(x) | → | f_1(g_1(x)) |
| *top*_0(g_1(x)) | → | *top*_0(f_0(g_1(x))) | | f_0(g_1(x)) | → | f_1(f_0(g_1(x))) |
| s_0(g_1(x)) | → | s_0(f_0(g_1(x))) |
Original Signature
Termination of terms over the following signature is verified: f_0, a_0, *top*_0, g_1, b_0, f_1, s_0
Strategy
Context-sensitive strategy:
μ(f_1#) = μ(b_0) = μ(g_1#) = μ(T) = μ(a_0) = μ(g_1) = μ(f_1) = ∅
μ(s_0#) = μ(f_0#) = μ(f_0) = μ(*top*_0) = μ(s_0) = μ(*top*_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 0
- a_0: 1
- b_0: 0
- f_0(x): 0
- f_1(x): 0
- f_1#(x): x + 1
- g_1(x): 2x
- g_1#(x): 2x + 2
- s_0(x): 0
- s_0#(x): x + 2
Standard Usable rules
| g_1(x) | → | f_1(g_1(x)) | | f_1(f_0(x)) | → | b_0 |
| f_1(g_1(a_0)) | → | f_0(s_0(g_1(b_0))) | | f_1(f_1(x)) | → | b_0 |
| s_0(g_1(x)) | → | s_0(f_0(g_1(x))) | | f_0(g_1(x)) | → | f_1(f_0(g_1(x))) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f_1#(g_1(a_0)) | → | s_0#(g_1(b_0)) | | g_1#(x) | → | f_1#(g_1(x)) |
| f_1#(g_1(a_0)) | → | g_1#(b_0) |
Problem 7: DependencyGraph
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| f_1(g_1(a_0)) | → | f_0(s_0(g_1(b_0))) | | f_1(f_0(x)) | → | b_0 |
| f_1(f_1(x)) | → | b_0 | | g_1(x) | → | f_1(g_1(x)) |
| *top*_0(g_1(x)) | → | *top*_0(f_0(g_1(x))) | | f_0(g_1(x)) | → | f_1(f_0(g_1(x))) |
| s_0(g_1(x)) | → | s_0(f_0(g_1(x))) |
Original Signature
Termination of terms over the following signature is verified: f_0, a_0, *top*_0, g_1, b_0, f_1, s_0
Strategy
Context-sensitive strategy:
μ(f_1#) = μ(b_0) = μ(g_1#) = μ(T) = μ(a_0) = μ(g_1) = μ(f_1) = ∅
μ(s_0#) = μ(f_0#) = μ(f_0) = μ(*top*_0) = μ(s_0) = μ(*top*_0#) = {1}
There are no SCCs!
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| *top*_0#(g_1(x)) | → | *top*_0#(f_0(g_1(x))) |
Rewrite Rules
| f_1(g_1(a_0)) | → | f_0(s_0(g_1(b_0))) | | f_1(f_0(x)) | → | b_0 |
| f_1(f_1(x)) | → | b_0 | | g_1(x) | → | f_1(g_1(x)) |
| *top*_0(g_1(x)) | → | *top*_0(f_0(g_1(x))) | | f_0(g_1(x)) | → | f_1(f_0(g_1(x))) |
| s_0(g_1(x)) | → | s_0(f_0(g_1(x))) |
Original Signature
Termination of terms over the following signature is verified: f_0, a_0, *top*_0, g_1, b_0, f_1, s_0
Strategy
Context-sensitive strategy:
μ(f_1#) = μ(b_0) = μ(g_1#) = μ(T) = μ(a_0) = μ(g_1) = μ(f_1) = ∅
μ(s_0#) = μ(f_0#) = μ(f_0) = μ(*top*_0) = μ(s_0) = μ(*top*_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 0
- *top*_0#(x): x
- a_0: 1
- b_0: 1
- f_0(x): 2
- f_1(x): 2
- g_1(x): 3
- s_0(x): 0
Standard Usable rules
| g_1(x) | → | f_1(g_1(x)) | | f_1(f_0(x)) | → | b_0 |
| f_1(g_1(a_0)) | → | f_0(s_0(g_1(b_0))) | | f_1(f_1(x)) | → | b_0 |
| s_0(g_1(x)) | → | s_0(f_0(g_1(x))) | | f_0(g_1(x)) | → | f_1(f_0(g_1(x))) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| *top*_0#(g_1(x)) | → | *top*_0#(f_0(g_1(x))) |
Problem 4: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| T(g_1(x_1)) | → | T(x_1) | | T(f_0(x_1)) | → | T(x_1) |
Rewrite Rules
| f_1(g_1(a_0)) | → | f_0(s_0(g_1(b_0))) | | f_1(f_0(x)) | → | b_0 |
| f_1(f_1(x)) | → | b_0 | | g_1(x) | → | f_1(g_1(x)) |
| *top*_0(g_1(x)) | → | *top*_0(f_0(g_1(x))) | | f_0(g_1(x)) | → | f_1(f_0(g_1(x))) |
| s_0(g_1(x)) | → | s_0(f_0(g_1(x))) |
Original Signature
Termination of terms over the following signature is verified: f_0, a_0, *top*_0, g_1, b_0, f_1, s_0
Strategy
Context-sensitive strategy:
μ(f_1#) = μ(b_0) = μ(g_1#) = μ(T) = μ(a_0) = μ(g_1) = μ(f_1) = ∅
μ(s_0#) = μ(f_0#) = μ(f_0) = μ(*top*_0) = μ(s_0) = μ(*top*_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 0
- T(x): 3x
- a_0: 0
- b_0: 0
- f_0(x): x + 1
- f_1(x): 0
- g_1(x): 3x
- s_0(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:
Problem 6: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
Rewrite Rules
| f_1(g_1(a_0)) | → | f_0(s_0(g_1(b_0))) | | f_1(f_0(x)) | → | b_0 |
| f_1(f_1(x)) | → | b_0 | | g_1(x) | → | f_1(g_1(x)) |
| *top*_0(g_1(x)) | → | *top*_0(f_0(g_1(x))) | | f_0(g_1(x)) | → | f_1(f_0(g_1(x))) |
| s_0(g_1(x)) | → | s_0(f_0(g_1(x))) |
Original Signature
Termination of terms over the following signature is verified: f_0, a_0, *top*_0, g_1, b_0, f_1, s_0
Strategy
Context-sensitive strategy:
μ(f_1#) = μ(b_0) = μ(g_1#) = μ(T) = μ(a_0) = μ(g_1) = μ(f_1) = ∅
μ(s_0#) = μ(f_0#) = μ(f_0) = μ(*top*_0) = μ(s_0) = μ(*top*_0#) = {1}
Polynomial Interpretation
- *top*_0(x): 0
- T(x): x + 1
- a_0: 0
- b_0: 0
- f_0(x): 0
- f_1(x): 0
- g_1(x): x + 1
- s_0(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: