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