YES

The TRS could be proven terminating. The proof took 7591 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (4810ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (2127ms).
 |    | – Problem 5 was processed with processor DependencyGraph (4ms).
 |    |    | – Problem 6 was processed with processor PolynomialLinearRange4iUR (443ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 4 was processed with processor SubtermCriterion (1ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

+#(8, 3) → c#(1, 1)*#(9, 3) → c#(2, 7)
*#(9, 4) → c#(3, 6)*#(x, c(y, z)) → *#(x, z)
*#(5, 4) → c#(2, 0)+#(7, 6) → c#(1, 3)
+#(4, 7) → c#(1, 1)+#(2, 8) → c#(1, 0)
*#(6, 8) → c#(4, 8)*#(8, 5) → c#(4, 0)
*#(6, 4) → c#(2, 4)+#(3, 9) → c#(1, 2)
*#(4, 8) → c#(3, 2)*#(9, 8) → c#(7, 2)
*#(3, 4) → c#(1, 2)+#(9, 7) → c#(1, 6)
*#(2, 9) → c#(1, 8)+#(5, 5) → c#(1, 0)
*#(8, 2) → c#(1, 8)*#(7, 7) → c#(4, 9)
*#(2, 6) → c#(1, 2)+#(7, 4) → c#(1, 1)
*#(4, 5) → c#(2, 0)*#(7, 8) → c#(5, 6)
*#(c(x, y), z) → *#(y, z)*#(6, 3) → c#(1, 8)
+#(5, 8) → c#(1, 3)+#(8, 8) → c#(1, 6)
*#(3, 6) → c#(1, 8)*#(2, 8) → c#(1, 6)
*#(3, 7) → c#(2, 1)+#(6, 9) → c#(1, 5)
*#(9, 5) → c#(4, 5)+#(7, 9) → c#(1, 6)
*#(6, 6) → c#(3, 6)*#(x, c(y, z)) → c#(*(x, y), *(x, z))
*#(6, 7) → c#(4, 2)*#(4, 4) → c#(1, 6)
+#(4, 9) → c#(1, 3)*#(5, 5) → c#(2, 5)
+#(6, 4) → c#(1, 0)*#(7, 4) → c#(2, 8)
*#(8, 7) → c#(5, 6)c#(x, c(y, z)) → c#(+(x, y), z)
*#(7, 6) → c#(4, 2)+#(9, 2) → c#(1, 1)
+#(8, 6) → c#(1, 4)*#(2, 7) → c#(1, 4)
+#(4, 8) → c#(1, 2)+#(7, 5) → c#(1, 2)
*#(4, 6) → c#(2, 4)+#(2, 9) → c#(1, 1)
+#(7, 3) → c#(1, 0)*#(7, 3) → c#(2, 1)
+#(9, 3) → c#(1, 2)+#(6, 7) → c#(1, 3)
*#(c(x, y), z) → *#(x, z)*#(9, 2) → c#(1, 8)
+#(5, 9) → c#(1, 4)+#(9, 9) → c#(1, 8)
+#(6, 6) → c#(1, 2)*#(6, 2) → c#(1, 2)
+#(7, 8) → c#(1, 5)*#(9, 6) → c#(5, 4)
+#(6, 5) → c#(1, 1)+#(5, 6) → c#(1, 1)
*#(7, 9) → c#(6, 3)*#(2, 5) → c#(1, 0)
+#(3, 8) → c#(1, 1)*#(3, 8) → c#(2, 4)
*#(6, 9) → c#(5, 4)*#(4, 9) → c#(3, 6)
*#(6, 5) → c#(3, 0)*#(9, 9) → c#(8, 1)
*#(c(x, y), z) → c#(*(x, z), *(y, z))*#(5, 8) → c#(4, 0)
*#(8, 9) → c#(7, 2)+#(7, 7) → c#(1, 4)
*#(8, 6) → c#(4, 8)*#(5, 2) → c#(1, 0)
*#(5, 7) → c#(3, 5)+#(9, 1) → c#(1, 0)
*#(9, 7) → c#(6, 3)*#(x, c(y, z)) → *#(x, y)
*#(8, 8) → c#(6, 4)*#(4, 7) → c#(2, 8)
+#(c(x, y), z) → +#(y, z)+#(1, 9) → c#(1, 0)
+#(6, 8) → c#(1, 4)*#(7, 2) → c#(1, 4)
+#(4, 6) → c#(1, 0)+#(8, 4) → c#(1, 2)
*#(3, 5) → c#(1, 5)+#(x, c(y, z)) → c#(y, +(x, z))
*#(8, 3) → c#(2, 4)*#(5, 6) → c#(3, 0)
*#(5, 9) → c#(4, 5)+#(8, 2) → c#(1, 0)
c#(x, c(y, z)) → +#(x, y)+#(x, c(y, z)) → +#(x, z)
*#(5, 3) → c#(1, 5)+#(5, 7) → c#(1, 2)
+#(8, 9) → c#(1, 7)+#(9, 8) → c#(1, 7)
+#(9, 5) → c#(1, 4)*#(8, 4) → c#(3, 2)
+#(c(x, y), z) → c#(x, +(y, z))+#(8, 7) → c#(1, 5)
+#(8, 5) → c#(1, 3)+#(9, 4) → c#(1, 3)
*#(7, 5) → c#(3, 5)+#(9, 6) → c#(1, 5)
*#(4, 3) → c#(1, 2)*#(3, 9) → c#(2, 7)
+#(3, 7) → c#(1, 0)

Rewrite Rules

c(0, x) → xc(x, c(y, z)) → c(+(x, y), z)
+(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))
*(0, 0) → 0*(0, 1) → 0
*(0, 2) → 0*(0, 3) → 0
*(0, 4) → 0*(0, 5) → 0
*(0, 6) → 0*(0, 7) → 0
*(0, 8) → 0*(0, 9) → 0
*(1, 0) → 0*(1, 1) → 1
*(1, 2) → 2*(1, 3) → 3
*(1, 4) → 4*(1, 5) → 5
*(1, 6) → 6*(1, 7) → 7
*(1, 8) → 8*(1, 9) → 9
*(2, 0) → 0*(2, 1) → 2
*(2, 2) → 4*(2, 3) → 6
*(2, 4) → 8*(2, 5) → c(1, 0)
*(2, 6) → c(1, 2)*(2, 7) → c(1, 4)
*(2, 8) → c(1, 6)*(2, 9) → c(1, 8)
*(3, 0) → 0*(3, 1) → 3
*(3, 2) → 6*(3, 3) → 9
*(3, 4) → c(1, 2)*(3, 5) → c(1, 5)
*(3, 6) → c(1, 8)*(3, 7) → c(2, 1)
*(3, 8) → c(2, 4)*(3, 9) → c(2, 7)
*(4, 0) → 0*(4, 1) → 4
*(4, 2) → 8*(4, 3) → c(1, 2)
*(4, 4) → c(1, 6)*(4, 5) → c(2, 0)
*(4, 6) → c(2, 4)*(4, 7) → c(2, 8)
*(4, 8) → c(3, 2)*(4, 9) → c(3, 6)
*(5, 0) → 0*(5, 1) → 5
*(5, 2) → c(1, 0)*(5, 3) → c(1, 5)
*(5, 4) → c(2, 0)*(5, 5) → c(2, 5)
*(5, 6) → c(3, 0)*(5, 7) → c(3, 5)
*(5, 8) → c(4, 0)*(5, 9) → c(4, 5)
*(6, 0) → 0*(6, 1) → 6
*(6, 2) → c(1, 2)*(6, 3) → c(1, 8)
*(6, 4) → c(2, 4)*(6, 5) → c(3, 0)
*(6, 6) → c(3, 6)*(6, 7) → c(4, 2)
*(6, 8) → c(4, 8)*(6, 9) → c(5, 4)
*(7, 0) → 0*(7, 1) → 7
*(7, 2) → c(1, 4)*(7, 3) → c(2, 1)
*(7, 4) → c(2, 8)*(7, 5) → c(3, 5)
*(7, 6) → c(4, 2)*(7, 7) → c(4, 9)
*(7, 8) → c(5, 6)*(7, 9) → c(6, 3)
*(8, 0) → 0*(8, 1) → 8
*(8, 2) → c(1, 8)*(8, 3) → c(2, 4)
*(8, 4) → c(3, 2)*(8, 5) → c(4, 0)
*(8, 6) → c(4, 8)*(8, 7) → c(5, 6)
*(8, 8) → c(6, 4)*(8, 9) → c(7, 2)
*(9, 0) → 0*(9, 1) → 9
*(9, 2) → c(1, 8)*(9, 3) → c(2, 7)
*(9, 4) → c(3, 6)*(9, 5) → c(4, 5)
*(9, 6) → c(5, 4)*(9, 7) → c(6, 3)
*(9, 8) → c(7, 2)*(9, 9) → c(8, 1)
*(x, c(y, z)) → c(*(x, y), *(x, z))*(c(x, y), z) → c(*(x, z), *(y, z))

Original Signature

Termination of terms over the following signature is verified: c, *, +, 3, 2, 1, 0, 7, 6, 5, 4, 9, 8

Strategy

The following SCCs where found

*#(c(x, y), z) → *#(x, z)*#(x, c(y, z)) → *#(x, y)
*#(x, c(y, z)) → *#(x, z)*#(c(x, y), z) → *#(y, z)
c#(x, c(y, z)) → c#(+(x, y), z)+#(c(x, y), z) → +#(y, z)
c#(x, c(y, z)) → +#(x, y)+#(x, c(y, z)) → +#(x, z)
+#(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)
c#(x, c(y, z)) → +#(x, y)+#(x, c(y, z)) → +#(x, z)
+#(c(x, y), z) → c#(x, +(y, z))+#(x, c(y, z)) → c#(y, +(x, z))

Rewrite Rules

c(0, x) → xc(x, c(y, z)) → c(+(x, y), z)
+(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))
*(0, 0) → 0*(0, 1) → 0
*(0, 2) → 0*(0, 3) → 0
*(0, 4) → 0*(0, 5) → 0
*(0, 6) → 0*(0, 7) → 0
*(0, 8) → 0*(0, 9) → 0
*(1, 0) → 0*(1, 1) → 1
*(1, 2) → 2*(1, 3) → 3
*(1, 4) → 4*(1, 5) → 5
*(1, 6) → 6*(1, 7) → 7
*(1, 8) → 8*(1, 9) → 9
*(2, 0) → 0*(2, 1) → 2
*(2, 2) → 4*(2, 3) → 6
*(2, 4) → 8*(2, 5) → c(1, 0)
*(2, 6) → c(1, 2)*(2, 7) → c(1, 4)
*(2, 8) → c(1, 6)*(2, 9) → c(1, 8)
*(3, 0) → 0*(3, 1) → 3
*(3, 2) → 6*(3, 3) → 9
*(3, 4) → c(1, 2)*(3, 5) → c(1, 5)
*(3, 6) → c(1, 8)*(3, 7) → c(2, 1)
*(3, 8) → c(2, 4)*(3, 9) → c(2, 7)
*(4, 0) → 0*(4, 1) → 4
*(4, 2) → 8*(4, 3) → c(1, 2)
*(4, 4) → c(1, 6)*(4, 5) → c(2, 0)
*(4, 6) → c(2, 4)*(4, 7) → c(2, 8)
*(4, 8) → c(3, 2)*(4, 9) → c(3, 6)
*(5, 0) → 0*(5, 1) → 5
*(5, 2) → c(1, 0)*(5, 3) → c(1, 5)
*(5, 4) → c(2, 0)*(5, 5) → c(2, 5)
*(5, 6) → c(3, 0)*(5, 7) → c(3, 5)
*(5, 8) → c(4, 0)*(5, 9) → c(4, 5)
*(6, 0) → 0*(6, 1) → 6
*(6, 2) → c(1, 2)*(6, 3) → c(1, 8)
*(6, 4) → c(2, 4)*(6, 5) → c(3, 0)
*(6, 6) → c(3, 6)*(6, 7) → c(4, 2)
*(6, 8) → c(4, 8)*(6, 9) → c(5, 4)
*(7, 0) → 0*(7, 1) → 7
*(7, 2) → c(1, 4)*(7, 3) → c(2, 1)
*(7, 4) → c(2, 8)*(7, 5) → c(3, 5)
*(7, 6) → c(4, 2)*(7, 7) → c(4, 9)
*(7, 8) → c(5, 6)*(7, 9) → c(6, 3)
*(8, 0) → 0*(8, 1) → 8
*(8, 2) → c(1, 8)*(8, 3) → c(2, 4)
*(8, 4) → c(3, 2)*(8, 5) → c(4, 0)
*(8, 6) → c(4, 8)*(8, 7) → c(5, 6)
*(8, 8) → c(6, 4)*(8, 9) → c(7, 2)
*(9, 0) → 0*(9, 1) → 9
*(9, 2) → c(1, 8)*(9, 3) → c(2, 7)
*(9, 4) → c(3, 6)*(9, 5) → c(4, 5)
*(9, 6) → c(5, 4)*(9, 7) → c(6, 3)
*(9, 8) → c(7, 2)*(9, 9) → c(8, 1)
*(x, c(y, z)) → c(*(x, y), *(x, z))*(c(x, y), z) → c(*(x, z), *(y, z))

Original Signature

Termination of terms over the following signature is verified: c, *, +, 3, 2, 1, 0, 7, 6, 5, 4, 9, 8

Strategy

Polynomial Interpretation

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)+#(x, c(y, z)) → +#(x, z)
c#(x, c(y, z)) → +#(x, y)

Problem 5: 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

c(0, x) → xc(x, c(y, z)) → c(+(x, y), z)
+(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))
*(0, 0) → 0*(0, 1) → 0
*(0, 2) → 0*(0, 3) → 0
*(0, 4) → 0*(0, 5) → 0
*(0, 6) → 0*(0, 7) → 0
*(0, 8) → 0*(0, 9) → 0
*(1, 0) → 0*(1, 1) → 1
*(1, 2) → 2*(1, 3) → 3
*(1, 4) → 4*(1, 5) → 5
*(1, 6) → 6*(1, 7) → 7
*(1, 8) → 8*(1, 9) → 9
*(2, 0) → 0*(2, 1) → 2
*(2, 2) → 4*(2, 3) → 6
*(2, 4) → 8*(2, 5) → c(1, 0)
*(2, 6) → c(1, 2)*(2, 7) → c(1, 4)
*(2, 8) → c(1, 6)*(2, 9) → c(1, 8)
*(3, 0) → 0*(3, 1) → 3
*(3, 2) → 6*(3, 3) → 9
*(3, 4) → c(1, 2)*(3, 5) → c(1, 5)
*(3, 6) → c(1, 8)*(3, 7) → c(2, 1)
*(3, 8) → c(2, 4)*(3, 9) → c(2, 7)
*(4, 0) → 0*(4, 1) → 4
*(4, 2) → 8*(4, 3) → c(1, 2)
*(4, 4) → c(1, 6)*(4, 5) → c(2, 0)
*(4, 6) → c(2, 4)*(4, 7) → c(2, 8)
*(4, 8) → c(3, 2)*(4, 9) → c(3, 6)
*(5, 0) → 0*(5, 1) → 5
*(5, 2) → c(1, 0)*(5, 3) → c(1, 5)
*(5, 4) → c(2, 0)*(5, 5) → c(2, 5)
*(5, 6) → c(3, 0)*(5, 7) → c(3, 5)
*(5, 8) → c(4, 0)*(5, 9) → c(4, 5)
*(6, 0) → 0*(6, 1) → 6
*(6, 2) → c(1, 2)*(6, 3) → c(1, 8)
*(6, 4) → c(2, 4)*(6, 5) → c(3, 0)
*(6, 6) → c(3, 6)*(6, 7) → c(4, 2)
*(6, 8) → c(4, 8)*(6, 9) → c(5, 4)
*(7, 0) → 0*(7, 1) → 7
*(7, 2) → c(1, 4)*(7, 3) → c(2, 1)
*(7, 4) → c(2, 8)*(7, 5) → c(3, 5)
*(7, 6) → c(4, 2)*(7, 7) → c(4, 9)
*(7, 8) → c(5, 6)*(7, 9) → c(6, 3)
*(8, 0) → 0*(8, 1) → 8
*(8, 2) → c(1, 8)*(8, 3) → c(2, 4)
*(8, 4) → c(3, 2)*(8, 5) → c(4, 0)
*(8, 6) → c(4, 8)*(8, 7) → c(5, 6)
*(8, 8) → c(6, 4)*(8, 9) → c(7, 2)
*(9, 0) → 0*(9, 1) → 9
*(9, 2) → c(1, 8)*(9, 3) → c(2, 7)
*(9, 4) → c(3, 6)*(9, 5) → c(4, 5)
*(9, 6) → c(5, 4)*(9, 7) → c(6, 3)
*(9, 8) → c(7, 2)*(9, 9) → c(8, 1)
*(x, c(y, z)) → c(*(x, y), *(x, z))*(c(x, y), z) → c(*(x, z), *(y, z))

Original Signature

Termination of terms over the following signature is verified: c, *, +, 3, 2, 1, 0, 7, 6, 5, 4, 9, 8

Strategy

The following SCCs where found

c#(x, c(y, z)) → c#(+(x, y), z)

Problem 6: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

c#(x, c(y, z)) → c#(+(x, y), z)

Rewrite Rules

c(0, x) → xc(x, c(y, z)) → c(+(x, y), z)
+(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))
*(0, 0) → 0*(0, 1) → 0
*(0, 2) → 0*(0, 3) → 0
*(0, 4) → 0*(0, 5) → 0
*(0, 6) → 0*(0, 7) → 0
*(0, 8) → 0*(0, 9) → 0
*(1, 0) → 0*(1, 1) → 1
*(1, 2) → 2*(1, 3) → 3
*(1, 4) → 4*(1, 5) → 5
*(1, 6) → 6*(1, 7) → 7
*(1, 8) → 8*(1, 9) → 9
*(2, 0) → 0*(2, 1) → 2
*(2, 2) → 4*(2, 3) → 6
*(2, 4) → 8*(2, 5) → c(1, 0)
*(2, 6) → c(1, 2)*(2, 7) → c(1, 4)
*(2, 8) → c(1, 6)*(2, 9) → c(1, 8)
*(3, 0) → 0*(3, 1) → 3
*(3, 2) → 6*(3, 3) → 9
*(3, 4) → c(1, 2)*(3, 5) → c(1, 5)
*(3, 6) → c(1, 8)*(3, 7) → c(2, 1)
*(3, 8) → c(2, 4)*(3, 9) → c(2, 7)
*(4, 0) → 0*(4, 1) → 4
*(4, 2) → 8*(4, 3) → c(1, 2)
*(4, 4) → c(1, 6)*(4, 5) → c(2, 0)
*(4, 6) → c(2, 4)*(4, 7) → c(2, 8)
*(4, 8) → c(3, 2)*(4, 9) → c(3, 6)
*(5, 0) → 0*(5, 1) → 5
*(5, 2) → c(1, 0)*(5, 3) → c(1, 5)
*(5, 4) → c(2, 0)*(5, 5) → c(2, 5)
*(5, 6) → c(3, 0)*(5, 7) → c(3, 5)
*(5, 8) → c(4, 0)*(5, 9) → c(4, 5)
*(6, 0) → 0*(6, 1) → 6
*(6, 2) → c(1, 2)*(6, 3) → c(1, 8)
*(6, 4) → c(2, 4)*(6, 5) → c(3, 0)
*(6, 6) → c(3, 6)*(6, 7) → c(4, 2)
*(6, 8) → c(4, 8)*(6, 9) → c(5, 4)
*(7, 0) → 0*(7, 1) → 7
*(7, 2) → c(1, 4)*(7, 3) → c(2, 1)
*(7, 4) → c(2, 8)*(7, 5) → c(3, 5)
*(7, 6) → c(4, 2)*(7, 7) → c(4, 9)
*(7, 8) → c(5, 6)*(7, 9) → c(6, 3)
*(8, 0) → 0*(8, 1) → 8
*(8, 2) → c(1, 8)*(8, 3) → c(2, 4)
*(8, 4) → c(3, 2)*(8, 5) → c(4, 0)
*(8, 6) → c(4, 8)*(8, 7) → c(5, 6)
*(8, 8) → c(6, 4)*(8, 9) → c(7, 2)
*(9, 0) → 0*(9, 1) → 9
*(9, 2) → c(1, 8)*(9, 3) → c(2, 7)
*(9, 4) → c(3, 6)*(9, 5) → c(4, 5)
*(9, 6) → c(5, 4)*(9, 7) → c(6, 3)
*(9, 8) → c(7, 2)*(9, 9) → c(8, 1)
*(x, c(y, z)) → c(*(x, y), *(x, z))*(c(x, y), z) → c(*(x, z), *(y, z))

Original Signature

Termination of terms over the following signature is verified: c, *, +, 3, 2, 1, 0, 7, 6, 5, 4, 9, 8

Strategy

Polynomial Interpretation

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)

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

*#(c(x, y), z) → *#(x, z)*#(x, c(y, z)) → *#(x, y)
*#(x, c(y, z)) → *#(x, z)*#(c(x, y), z) → *#(y, z)

Rewrite Rules

c(0, x) → xc(x, c(y, z)) → c(+(x, y), z)
+(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))
*(0, 0) → 0*(0, 1) → 0
*(0, 2) → 0*(0, 3) → 0
*(0, 4) → 0*(0, 5) → 0
*(0, 6) → 0*(0, 7) → 0
*(0, 8) → 0*(0, 9) → 0
*(1, 0) → 0*(1, 1) → 1
*(1, 2) → 2*(1, 3) → 3
*(1, 4) → 4*(1, 5) → 5
*(1, 6) → 6*(1, 7) → 7
*(1, 8) → 8*(1, 9) → 9
*(2, 0) → 0*(2, 1) → 2
*(2, 2) → 4*(2, 3) → 6
*(2, 4) → 8*(2, 5) → c(1, 0)
*(2, 6) → c(1, 2)*(2, 7) → c(1, 4)
*(2, 8) → c(1, 6)*(2, 9) → c(1, 8)
*(3, 0) → 0*(3, 1) → 3
*(3, 2) → 6*(3, 3) → 9
*(3, 4) → c(1, 2)*(3, 5) → c(1, 5)
*(3, 6) → c(1, 8)*(3, 7) → c(2, 1)
*(3, 8) → c(2, 4)*(3, 9) → c(2, 7)
*(4, 0) → 0*(4, 1) → 4
*(4, 2) → 8*(4, 3) → c(1, 2)
*(4, 4) → c(1, 6)*(4, 5) → c(2, 0)
*(4, 6) → c(2, 4)*(4, 7) → c(2, 8)
*(4, 8) → c(3, 2)*(4, 9) → c(3, 6)
*(5, 0) → 0*(5, 1) → 5
*(5, 2) → c(1, 0)*(5, 3) → c(1, 5)
*(5, 4) → c(2, 0)*(5, 5) → c(2, 5)
*(5, 6) → c(3, 0)*(5, 7) → c(3, 5)
*(5, 8) → c(4, 0)*(5, 9) → c(4, 5)
*(6, 0) → 0*(6, 1) → 6
*(6, 2) → c(1, 2)*(6, 3) → c(1, 8)
*(6, 4) → c(2, 4)*(6, 5) → c(3, 0)
*(6, 6) → c(3, 6)*(6, 7) → c(4, 2)
*(6, 8) → c(4, 8)*(6, 9) → c(5, 4)
*(7, 0) → 0*(7, 1) → 7
*(7, 2) → c(1, 4)*(7, 3) → c(2, 1)
*(7, 4) → c(2, 8)*(7, 5) → c(3, 5)
*(7, 6) → c(4, 2)*(7, 7) → c(4, 9)
*(7, 8) → c(5, 6)*(7, 9) → c(6, 3)
*(8, 0) → 0*(8, 1) → 8
*(8, 2) → c(1, 8)*(8, 3) → c(2, 4)
*(8, 4) → c(3, 2)*(8, 5) → c(4, 0)
*(8, 6) → c(4, 8)*(8, 7) → c(5, 6)
*(8, 8) → c(6, 4)*(8, 9) → c(7, 2)
*(9, 0) → 0*(9, 1) → 9
*(9, 2) → c(1, 8)*(9, 3) → c(2, 7)
*(9, 4) → c(3, 6)*(9, 5) → c(4, 5)
*(9, 6) → c(5, 4)*(9, 7) → c(6, 3)
*(9, 8) → c(7, 2)*(9, 9) → c(8, 1)
*(x, c(y, z)) → c(*(x, y), *(x, z))*(c(x, y), z) → c(*(x, z), *(y, z))

Original Signature

Termination of terms over the following signature is verified: c, *, +, 3, 2, 1, 0, 7, 6, 5, 4, 9, 8

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

*#(c(x, y), z) → *#(x, z)*#(c(x, y), z) → *#(y, z)

Problem 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

*#(x, c(y, z)) → *#(x, y)*#(x, c(y, z)) → *#(x, z)

Rewrite Rules

c(0, x) → xc(x, c(y, z)) → c(+(x, y), z)
+(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))
*(0, 0) → 0*(0, 1) → 0
*(0, 2) → 0*(0, 3) → 0
*(0, 4) → 0*(0, 5) → 0
*(0, 6) → 0*(0, 7) → 0
*(0, 8) → 0*(0, 9) → 0
*(1, 0) → 0*(1, 1) → 1
*(1, 2) → 2*(1, 3) → 3
*(1, 4) → 4*(1, 5) → 5
*(1, 6) → 6*(1, 7) → 7
*(1, 8) → 8*(1, 9) → 9
*(2, 0) → 0*(2, 1) → 2
*(2, 2) → 4*(2, 3) → 6
*(2, 4) → 8*(2, 5) → c(1, 0)
*(2, 6) → c(1, 2)*(2, 7) → c(1, 4)
*(2, 8) → c(1, 6)*(2, 9) → c(1, 8)
*(3, 0) → 0*(3, 1) → 3
*(3, 2) → 6*(3, 3) → 9
*(3, 4) → c(1, 2)*(3, 5) → c(1, 5)
*(3, 6) → c(1, 8)*(3, 7) → c(2, 1)
*(3, 8) → c(2, 4)*(3, 9) → c(2, 7)
*(4, 0) → 0*(4, 1) → 4
*(4, 2) → 8*(4, 3) → c(1, 2)
*(4, 4) → c(1, 6)*(4, 5) → c(2, 0)
*(4, 6) → c(2, 4)*(4, 7) → c(2, 8)
*(4, 8) → c(3, 2)*(4, 9) → c(3, 6)
*(5, 0) → 0*(5, 1) → 5
*(5, 2) → c(1, 0)*(5, 3) → c(1, 5)
*(5, 4) → c(2, 0)*(5, 5) → c(2, 5)
*(5, 6) → c(3, 0)*(5, 7) → c(3, 5)
*(5, 8) → c(4, 0)*(5, 9) → c(4, 5)
*(6, 0) → 0*(6, 1) → 6
*(6, 2) → c(1, 2)*(6, 3) → c(1, 8)
*(6, 4) → c(2, 4)*(6, 5) → c(3, 0)
*(6, 6) → c(3, 6)*(6, 7) → c(4, 2)
*(6, 8) → c(4, 8)*(6, 9) → c(5, 4)
*(7, 0) → 0*(7, 1) → 7
*(7, 2) → c(1, 4)*(7, 3) → c(2, 1)
*(7, 4) → c(2, 8)*(7, 5) → c(3, 5)
*(7, 6) → c(4, 2)*(7, 7) → c(4, 9)
*(7, 8) → c(5, 6)*(7, 9) → c(6, 3)
*(8, 0) → 0*(8, 1) → 8
*(8, 2) → c(1, 8)*(8, 3) → c(2, 4)
*(8, 4) → c(3, 2)*(8, 5) → c(4, 0)
*(8, 6) → c(4, 8)*(8, 7) → c(5, 6)
*(8, 8) → c(6, 4)*(8, 9) → c(7, 2)
*(9, 0) → 0*(9, 1) → 9
*(9, 2) → c(1, 8)*(9, 3) → c(2, 7)
*(9, 4) → c(3, 6)*(9, 5) → c(4, 5)
*(9, 6) → c(5, 4)*(9, 7) → c(6, 3)
*(9, 8) → c(7, 2)*(9, 9) → c(8, 1)
*(x, c(y, z)) → c(*(x, y), *(x, z))*(c(x, y), z) → c(*(x, z), *(y, z))

Original Signature

Termination of terms over the following signature is verified: c, *, +, 3, 2, 1, 0, 7, 6, 5, 4, 9, 8

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

*#(x, c(y, z)) → *#(x, y)*#(x, c(y, z)) → *#(x, z)