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