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