YES
The TRS could be proven terminating. The proof took 534 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (4ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (169ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (208ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| f#(g(x)) | → | f#(x) | | f'#(s(x), y, y) | → | f'#(y, x, s(x)) |
| f#(g(x)) | → | f#(f(x)) |
Rewrite Rules
| f(g(x)) | → | g(f(f(x))) | | f(h(x)) | → | h(g(x)) |
| f'(s(x), y, y) | → | f'(y, x, s(x)) |
Original Signature
Termination of terms over the following signature is verified: f, f', g, s, h
Strategy
The following SCCs where found
| f#(g(x)) → f#(x) | f#(g(x)) → f#(f(x)) |
| f'#(s(x), y, y) → f'#(y, x, s(x)) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| f#(g(x)) | → | f#(x) | | f#(g(x)) | → | f#(f(x)) |
Rewrite Rules
| f(g(x)) | → | g(f(f(x))) | | f(h(x)) | → | h(g(x)) |
| f'(s(x), y, y) | → | f'(y, x, s(x)) |
Original Signature
Termination of terms over the following signature is verified: f, f', g, s, h
Strategy
Polynomial Interpretation
- f(x): x
- f#(x): 2x
- f'(x,y,z): 0
- g(x): 2x + 1
- h(x): 0
- s(x): 0
Improved Usable rules
| f(h(x)) | → | h(g(x)) | | f(g(x)) | → | g(f(f(x))) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f#(g(x)) | → | f#(x) | | f#(g(x)) | → | f#(f(x)) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| f'#(s(x), y, y) | → | f'#(y, x, s(x)) |
Rewrite Rules
| f(g(x)) | → | g(f(f(x))) | | f(h(x)) | → | h(g(x)) |
| f'(s(x), y, y) | → | f'(y, x, s(x)) |
Original Signature
Termination of terms over the following signature is verified: f, f', g, s, h
Strategy
Polynomial Interpretation
- f(x): 0
- f'(x,y,z): 0
- f'#(x,y,z): z + y + 2x
- g(x): 0
- h(x): 0
- s(x): 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:
| f'#(s(x), y, y) | → | f'#(y, x, s(x)) |