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