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