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