YES
The TRS could be proven terminating. The proof took 1537 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (189ms).
| – Problem 2 was processed with processor SubtermCriterion (1ms).
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (411ms).
| | – Problem 5 was processed with processor DependencyGraph (23ms).
| | | – Problem 7 was processed with processor PolynomialLinearRange4iUR (116ms).
| | | – Problem 8 was processed with processor PolynomialLinearRange4iUR (72ms).
| | | | – Problem 11 was processed with processor PolynomialLinearRange4iUR (9ms).
| – Problem 4 was processed with processor PolynomialLinearRange4iUR (289ms).
| | – Problem 6 was processed with processor DependencyGraph (10ms).
| | | – Problem 9 was processed with processor PolynomialLinearRange4iUR (151ms).
| | | – Problem 10 was processed with processor PolynomialLinearRange4iUR (24ms).
| | | | – Problem 12 was processed with processor PolynomialLinearRange4iUR (10ms).
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| -#(I(x), O(y)) | → | -#(x, y) | | +#(O(x), O(y)) | → | O#(+(x, y)) |
| *#(I(x), y) | → | O#(*(x, y)) | | *#(I(x), y) | → | +#(O(*(x, y)), y) |
| -#(O(x), I(y)) | → | -#(x, y) | | +#(O(x), O(y)) | → | +#(x, y) |
| *#(I(x), y) | → | *#(x, y) | | +#(I(x), I(y)) | → | O#(+(+(x, y), I(0))) |
| -#(O(x), O(y)) | → | O#(-(x, y)) | | -#(O(x), I(y)) | → | -#(-(x, y), I(1)) |
| -#(O(x), O(y)) | → | -#(x, y) | | -#(I(x), I(y)) | → | -#(x, y) |
| +#(I(x), I(y)) | → | +#(x, y) | | *#(O(x), y) | → | *#(x, y) |
| *#(O(x), y) | → | O#(*(x, y)) | | +#(I(x), O(y)) | → | +#(x, y) |
| +#(O(x), I(y)) | → | +#(x, y) | | +#(I(x), I(y)) | → | +#(+(x, y), I(0)) |
| -#(I(x), I(y)) | → | O#(-(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) | | -(x, 0) | → | x |
| -(0, x) | → | 0 | | -(O(x), O(y)) | → | O(-(x, y)) |
| -(O(x), I(y)) | → | I(-(-(x, y), I(1))) | | -(I(x), O(y)) | → | I(-(x, y)) |
| -(I(x), I(y)) | → | O(-(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 1, 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) |
| -#(I(x), O(y)) → -#(x, y) | -#(O(x), I(y)) → -#(-(x, y), I(1)) |
| -#(O(x), O(y)) → -#(x, y) | -#(I(x), I(y)) → -#(x, y) |
| -#(O(x), I(y)) → -#(x, y) |
Problem 2: 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) | | -(x, 0) | → | x |
| -(0, x) | → | 0 | | -(O(x), O(y)) | → | O(-(x, y)) |
| -(O(x), I(y)) | → | I(-(-(x, y), I(1))) | | -(I(x), O(y)) | → | I(-(x, y)) |
| -(I(x), I(y)) | → | O(-(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 1, 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) |
Problem 3: 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) | | -(x, 0) | → | x |
| -(0, x) | → | 0 | | -(O(x), O(y)) | → | O(-(x, y)) |
| -(O(x), I(y)) | → | I(-(-(x, y), I(1))) | | -(I(x), O(y)) | → | I(-(x, y)) |
| -(I(x), I(y)) | → | O(-(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, *, +, O, I, -
Strategy
Polynomial Interpretation
- *(x,y): 0
- +(x,y): 0
- +#(x,y): y
- -(x,y): 0
- 0: 0
- 1: 0
- I(x): 2x + 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: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| +#(I(x), O(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) | | -(x, 0) | → | x |
| -(0, x) | → | 0 | | -(O(x), O(y)) | → | O(-(x, y)) |
| -(O(x), I(y)) | → | I(-(-(x, y), I(1))) | | -(I(x), O(y)) | → | I(-(x, y)) |
| -(I(x), I(y)) | → | O(-(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, *, +, O, I, -
Strategy
The following SCCs where found
| +#(I(x), I(y)) → +#(+(x, y), I(0)) |
| +#(I(x), O(y)) → +#(x, y) | +#(O(x), O(y)) → +#(x, y) |
Problem 7: 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) | | -(x, 0) | → | x |
| -(0, x) | → | 0 | | -(O(x), O(y)) | → | O(-(x, y)) |
| -(O(x), I(y)) | → | I(-(-(x, y), I(1))) | | -(I(x), O(y)) | → | I(-(x, y)) |
| -(I(x), I(y)) | → | O(-(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, *, +, O, I, -
Strategy
Polynomial Interpretation
- *(x,y): 0
- +(x,y): y + x
- +#(x,y): 2y + x
- -(x,y): 0
- 0: 0
- 1: 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 8: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| +#(I(x), O(y)) | → | +#(x, y) | | +#(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) | | -(x, 0) | → | x |
| -(0, x) | → | 0 | | -(O(x), O(y)) | → | O(-(x, y)) |
| -(O(x), I(y)) | → | I(-(-(x, y), I(1))) | | -(I(x), O(y)) | → | I(-(x, y)) |
| -(I(x), I(y)) | → | O(-(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, *, +, O, I, -
Strategy
Polynomial Interpretation
- *(x,y): 0
- +(x,y): 0
- +#(x,y): x
- -(x,y): 0
- 0: 0
- 1: 0
- I(x): x
- O(x): x + 1
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| +#(O(x), O(y)) | → | +#(x, y) |
Problem 11: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| +#(I(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) | | -(x, 0) | → | x |
| -(0, x) | → | 0 | | -(O(x), O(y)) | → | O(-(x, y)) |
| -(O(x), I(y)) | → | I(-(-(x, y), I(1))) | | -(I(x), O(y)) | → | I(-(x, y)) |
| -(I(x), I(y)) | → | O(-(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, *, +, O, I, -
Strategy
Polynomial Interpretation
- *(x,y): 0
- +(x,y): 0
- +#(x,y): y + 1
- -(x,y): 0
- 0: 0
- 1: 0
- I(x): 3
- O(x): x + 2
There are no 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) |
Problem 4: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| -#(I(x), O(y)) | → | -#(x, y) | | -#(O(x), I(y)) | → | -#(-(x, y), I(1)) |
| -#(O(x), O(y)) | → | -#(x, y) | | -#(I(x), I(y)) | → | -#(x, y) |
| -#(O(x), I(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) | | -(x, 0) | → | x |
| -(0, x) | → | 0 | | -(O(x), O(y)) | → | O(-(x, y)) |
| -(O(x), I(y)) | → | I(-(-(x, y), I(1))) | | -(I(x), O(y)) | → | I(-(x, y)) |
| -(I(x), I(y)) | → | O(-(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, *, +, O, I, -
Strategy
Polynomial Interpretation
- *(x,y): 0
- +(x,y): 0
- -(x,y): 2x
- -#(x,y): 2y
- 0: 1
- 1: 0
- I(x): 2x + 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 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| -#(I(x), O(y)) | → | -#(x, y) | | -#(O(x), O(y)) | → | -#(x, y) |
| -#(O(x), I(y)) | → | -#(-(x, y), I(1)) |
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) | | -(x, 0) | → | x |
| -(0, x) | → | 0 | | -(O(x), O(y)) | → | O(-(x, y)) |
| -(O(x), I(y)) | → | I(-(-(x, y), I(1))) | | -(I(x), O(y)) | → | I(-(x, y)) |
| -(I(x), I(y)) | → | O(-(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, *, +, O, I, -
Strategy
The following SCCs where found
| -#(I(x), O(y)) → -#(x, y) | -#(O(x), O(y)) → -#(x, y) |
| -#(O(x), I(y)) → -#(-(x, y), I(1)) |
Problem 9: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| -#(O(x), I(y)) | → | -#(-(x, y), I(1)) |
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) | | -(x, 0) | → | x |
| -(0, x) | → | 0 | | -(O(x), O(y)) | → | O(-(x, y)) |
| -(O(x), I(y)) | → | I(-(-(x, y), I(1))) | | -(I(x), O(y)) | → | I(-(x, y)) |
| -(I(x), I(y)) | → | O(-(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, *, +, O, I, -
Strategy
Polynomial Interpretation
- *(x,y): 0
- +(x,y): 0
- -(x,y): x
- -#(x,y): x
- 0: 2
- 1: 1
- I(x): x + 1
- O(x): x + 1
Improved Usable rules
| -(I(x), I(y)) | → | O(-(x, y)) | | -(O(x), I(y)) | → | I(-(-(x, y), I(1))) |
| -(x, 0) | → | x | | O(0) | → | 0 |
| -(I(x), O(y)) | → | I(-(x, y)) | | -(O(x), O(y)) | → | O(-(x, y)) |
| -(0, x) | → | 0 |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| -#(O(x), I(y)) | → | -#(-(x, y), I(1)) |
Problem 10: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| -#(I(x), O(y)) | → | -#(x, y) | | -#(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) | | -(x, 0) | → | x |
| -(0, x) | → | 0 | | -(O(x), O(y)) | → | O(-(x, y)) |
| -(O(x), I(y)) | → | I(-(-(x, y), I(1))) | | -(I(x), O(y)) | → | I(-(x, y)) |
| -(I(x), I(y)) | → | O(-(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, *, +, O, I, -
Strategy
Polynomial Interpretation
- *(x,y): 0
- +(x,y): 0
- -(x,y): 0
- -#(x,y): 3y + x + 1
- 0: 0
- 1: 0
- I(x): 2x + 1
- O(x): 3x
There are no 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) |
Problem 12: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| -#(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) | | -(x, 0) | → | x |
| -(0, x) | → | 0 | | -(O(x), O(y)) | → | O(-(x, y)) |
| -(O(x), I(y)) | → | I(-(-(x, y), I(1))) | | -(I(x), O(y)) | → | I(-(x, y)) |
| -(I(x), I(y)) | → | O(-(x, y)) |
Original Signature
Termination of terms over the following signature is verified: 1, 0, *, +, O, I, -
Strategy
Polynomial Interpretation
- *(x,y): 0
- +(x,y): 0
- -(x,y): 0
- -#(x,y): 2x + 1
- 0: 0
- 1: 0
- I(x): 0
- O(x): 2x + 1
There are no usable rules
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| -#(O(x), O(y)) | → | -#(x, y) |