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