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