Term Rewriting System R:

   [x, y, z]
   c(0, x) -> x
   c(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))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   *'(8, 2) -> C(1, 8)
   *'(5, 6) -> C(3, 0)
   *'(6, 9) -> C(5, 4)
   *'(5, 2) -> C(1, 0)
   *'(9, 8) -> C(7, 2)
   *'(8, 6) -> C(4, 8)
   *'(x, c(y, z)) -> C(*(x, y), *(x, z))
   *'(x, c(y, z)) -> *'(x, y)
   *'(x, c(y, z)) -> *'(x, z)
   *'(3, 7) -> C(2, 1)
   *'(8, 7) -> C(5, 6)
   *'(4, 4) -> C(1, 6)
   *'(4, 9) -> C(3, 6)
   *'(5, 8) -> C(4, 0)
   *'(9, 3) -> C(2, 7)
   *'(6, 7) -> C(4, 2)
   *'(8, 5) -> C(4, 0)
   *'(8, 9) -> C(7, 2)
   *'(2, 6) -> C(1, 2)
   *'(9, 2) -> C(1, 8)
   *'(9, 9) -> C(8, 1)
   *'(6, 3) -> C(1, 8)
   *'(8, 4) -> C(3, 2)
   *'(7, 6) -> C(4, 2)
   *'(3, 8) -> C(2, 4)
   *'(7, 2) -> C(1, 4)
   *'(9, 5) -> C(4, 5)
   *'(6, 8) -> C(4, 8)
   *'(6, 6) -> C(3, 6)
   *'(2, 9) -> C(1, 8)
   *'(6, 5) -> C(3, 0)
   *'(3, 6) -> C(1, 8)
   *'(3, 5) -> C(1, 5)
   *'(5, 3) -> C(1, 5)
   *'(8, 3) -> C(2, 4)
   *'(2, 7) -> C(1, 4)
   *'(7, 4) -> C(2, 8)
   *'(2, 8) -> C(1, 6)
   *'(2, 5) -> C(1, 0)
   *'(4, 6) -> C(2, 4)
   *'(3, 4) -> C(1, 2)
   *'(4, 8) -> C(3, 2)
   *'(4, 5) -> C(2, 0)
   *'(6, 4) -> C(2, 4)
   *'(6, 2) -> C(1, 2)
   *'(7, 9) -> C(6, 3)
   *'(7, 7) -> C(4, 9)
   *'(7, 8) -> C(5, 6)
   *'(c(x, y), z) -> C(*(x, z), *(y, z))
   *'(c(x, y), z) -> *'(x, z)
   *'(c(x, y), z) -> *'(y, z)
   *'(9, 4) -> C(3, 6)
   *'(5, 9) -> C(4, 5)
   *'(8, 8) -> C(6, 4)
   *'(5, 4) -> C(2, 0)
   *'(4, 3) -> C(1, 2)
   *'(5, 5) -> C(2, 5)
   *'(3, 9) -> C(2, 7)
   *'(7, 3) -> C(2, 1)
   *'(9, 6) -> C(5, 4)
   *'(5, 7) -> C(3, 5)
   *'(4, 7) -> C(2, 8)
   *'(9, 7) -> C(6, 3)
   *'(7, 5) -> C(3, 5)
   C(x, c(y, z)) -> C(+(x, y), z)
   C(x, c(y, z)) -> +'(x, y)
   +'(2, 9) -> C(1, 1)
   +'(x, c(y, z)) -> C(y, +(x, z))
   +'(x, c(y, z)) -> +'(x, z)
   +'(7, 5) -> C(1, 2)
   +'(7, 4) -> C(1, 1)
   +'(5, 9) -> C(1, 4)
   +'(9, 4) -> C(1, 3)
   +'(7, 6) -> C(1, 3)
   +'(3, 8) -> C(1, 1)
   +'(5, 8) -> C(1, 3)
   +'(8, 5) -> C(1, 3)
   +'(2, 8) -> C(1, 0)
   +'(c(x, y), z) -> C(x, +(y, z))
   +'(c(x, y), z) -> +'(y, z)
   +'(4, 8) -> C(1, 2)
   +'(5, 5) -> C(1, 0)
   +'(9, 6) -> C(1, 5)
   +'(6, 9) -> C(1, 5)
   +'(9, 5) -> C(1, 4)
   +'(3, 7) -> C(1, 0)
   +'(9, 3) -> C(1, 2)
   +'(7, 3) -> C(1, 0)
   +'(7, 8) -> C(1, 5)
   +'(6, 7) -> C(1, 3)
   +'(8, 3) -> C(1, 1)
   +'(6, 4) -> C(1, 0)
   +'(9, 9) -> C(1, 8)
   +'(6, 5) -> C(1, 1)
   +'(5, 6) -> C(1, 1)
   +'(4, 6) -> C(1, 0)
   +'(4, 9) -> C(1, 3)
   +'(6, 6) -> C(1, 2)
   +'(8, 8) -> C(1, 6)
   +'(9, 1) -> C(1, 0)
   +'(8, 2) -> C(1, 0)
   +'(8, 6) -> C(1, 4)
   +'(6, 8) -> C(1, 4)
   +'(9, 2) -> C(1, 1)
   +'(9, 8) -> C(1, 7)
   +'(9, 7) -> C(1, 6)
   +'(7, 9) -> C(1, 6)
   +'(8, 7) -> C(1, 5)
   +'(8, 9) -> C(1, 7)
   +'(7, 7) -> C(1, 4)
   +'(4, 7) -> C(1, 1)
   +'(8, 4) -> C(1, 2)
   +'(1, 9) -> C(1, 0)
   +'(5, 7) -> C(1, 2)
   +'(3, 9) -> C(1, 2)

Furthermore, R contains two SCCs.


SCC1:

+'(c(x, y), z) -> +'(y, z)
+'(c(x, y), z) -> C(x, +(y, z))
+'(x, c(y, z)) -> +'(x, z)
+'(x, c(y, z)) -> C(y, +(x, z))
C(x, c(y, z)) -> +'(x, y)
C(x, c(y, z)) -> C(+(x, y), z)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(6) = 0
POL(3) = 0
POL(5) = 0
POL(+'(x_1, x_2)) = x_1 + x_2
POL(c(x_1, x_2)) = x_1 + x_2
POL(+(x_1, x_2)) = x_1 + x_2
POL(0) = 0
POL(9) = 0
POL(C(x_1, x_2)) = x_1 + x_2
POL(4) = 0
POL(8) = 0
POL(1) = 0
POL(7) = 0
POL(2) = 0

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   *(8, 2) -> c(1, 8)
   *(0, 1) -> 0
   *(7, 1) -> 7
   *(5, 6) -> c(3, 0)
   *(1, 9) -> 9
   *(6, 9) -> c(5, 4)
   *(5, 2) -> c(1, 0)
   *(1, 1) -> 1
   *(9, 8) -> c(7, 2)
   *(3, 2) -> 6
   *(8, 6) -> c(4, 8)
   *(x, c(y, z)) -> c(*(x, y), *(x, z))
   *(3, 7) -> c(2, 1)
   *(8, 7) -> c(5, 6)
   *(4, 4) -> c(1, 6)
   *(4, 9) -> c(3, 6)
   *(5, 8) -> c(4, 0)
   *(9, 3) -> c(2, 7)
   *(6, 7) -> c(4, 2)
   *(0, 8) -> 0
   *(4, 0) -> 0
   *(5, 1) -> 5
   *(8, 0) -> 0
   *(9, 1) -> 9
   *(3, 1) -> 3
   *(8, 5) -> c(4, 0)
   *(8, 1) -> 8
   *(8, 9) -> c(7, 2)
   *(6, 1) -> 6
   *(0, 0) -> 0
   *(2, 4) -> 8
   *(2, 0) -> 0
   *(0, 7) -> 0
   *(4, 2) -> 8
   *(2, 6) -> c(1, 2)
   *(9, 2) -> c(1, 8)
   *(9, 9) -> c(8, 1)
   *(4, 1) -> 4
   *(6, 3) -> c(1, 8)
   *(8, 4) -> c(3, 2)
   *(7, 6) -> c(4, 2)
   *(2, 3) -> 6
   *(3, 8) -> c(2, 4)
   *(7, 2) -> c(1, 4)
   *(9, 5) -> c(4, 5)
   *(6, 8) -> c(4, 8)
   *(6, 6) -> c(3, 6)
   *(2, 9) -> c(1, 8)
   *(3, 3) -> 9
   *(6, 5) -> c(3, 0)
   *(3, 6) -> c(1, 8)
   *(1, 6) -> 6
   *(5, 0) -> 0
   *(2, 2) -> 4
   *(3, 5) -> c(1, 5)
   *(2, 1) -> 2
   *(5, 3) -> c(1, 5)
   *(8, 3) -> c(2, 4)
   *(2, 7) -> c(1, 4)
   *(7, 4) -> c(2, 8)
   *(2, 8) -> c(1, 6)
   *(2, 5) -> c(1, 0)
   *(0, 2) -> 0
   *(3, 0) -> 0
   *(4, 6) -> c(2, 4)
   *(0, 9) -> 0
   *(1, 4) -> 4
   *(1, 7) -> 7
   *(1, 2) -> 2
   *(3, 4) -> c(1, 2)
   *(0, 3) -> 0
   *(4, 8) -> c(3, 2)
   *(4, 5) -> c(2, 0)
   *(6, 4) -> c(2, 4)
   *(6, 2) -> c(1, 2)
   *(7, 9) -> c(6, 3)
   *(1, 3) -> 3
   *(7, 0) -> 0
   *(1, 8) -> 8
   *(1, 5) -> 5
   *(0, 5) -> 0
   *(7, 7) -> c(4, 9)
   *(7, 8) -> c(5, 6)
   *(c(x, y), z) -> c(*(x, z), *(y, z))
   *(9, 4) -> c(3, 6)
   *(5, 9) -> c(4, 5)
   *(8, 8) -> c(6, 4)
   *(1, 0) -> 0
   *(5, 4) -> c(2, 0)
   *(4, 3) -> c(1, 2)
   *(5, 5) -> c(2, 5)
   *(9, 0) -> 0
   *(0, 4) -> 0
   *(0, 6) -> 0
   *(3, 9) -> c(2, 7)
   *(7, 3) -> c(2, 1)
   *(6, 0) -> 0
   *(9, 6) -> c(5, 4)
   *(5, 7) -> c(3, 5)
   *(4, 7) -> c(2, 8)
   *(9, 7) -> c(6, 3)
   *(7, 5) -> c(3, 5)


 This transformation is resulting in one new subcycle:


SCC1.MRR1:

+'(c(x, y), z) -> C(x, +(y, z))
+'(x, c(y, z)) -> +'(x, z)
C(x, c(y, z)) -> +'(x, y)
C(x, c(y, z)) -> C(+(x, y), z)
+'(x, c(y, z)) -> C(y, +(x, z))
+'(c(x, y), z) -> +'(y, z)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(6) = 1
POL(3) = 1
POL(5) = 1
POL(+'(x_1, x_2)) = x_1 + x_2
POL(c(x_1, x_2)) = x_1 + x_2
POL(+(x_1, x_2)) = x_1 + x_2
POL(0) = 0
POL(9) = 1
POL(C(x_1, x_2)) = x_1 + x_2
POL(4) = 1
POL(8) = 1
POL(1) = 1
POL(7) = 1
POL(2) = 1

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   +(4, 4) -> 8
   +(5, 2) -> 7
   +(2, 4) -> 6
   +(2, 5) -> 7
   +(1, 7) -> 8
   +(2, 8) -> c(1, 0)
   +(2, 2) -> 4
   +(5, 5) -> c(1, 0)
   +(1, 8) -> 9
   +(4, 3) -> 7
   +(3, 7) -> c(1, 0)
   +(7, 1) -> 8
   +(2, 6) -> 8
   +(6, 1) -> 7
   +(2, 1) -> 3
   +(7, 3) -> c(1, 0)
   +(1, 5) -> 6
   +(2, 7) -> 9
   +(3, 2) -> 5
   +(1, 6) -> 7
   +(6, 4) -> c(1, 0)
   +(3, 1) -> 4
   +(4, 6) -> c(1, 0)
   +(8, 1) -> 9
   +(1, 4) -> 5
   +(3, 4) -> 7
   +(4, 5) -> 9
   +(3, 5) -> 8
   +(5, 3) -> 8
   +(3, 3) -> 6
   +(9, 1) -> c(1, 0)
   +(4, 2) -> 6
   +(8, 2) -> c(1, 0)
   +(1, 1) -> 2
   +(6, 3) -> 9
   +(5, 4) -> 9
   +(1, 2) -> 3
   +(4, 1) -> 5
   +(6, 2) -> 8
   +(1, 3) -> 4
   +(7, 2) -> 9
   +(1, 9) -> c(1, 0)
   +(5, 1) -> 6
   +(3, 6) -> 9
   +(2, 3) -> 5


 This transformation is resulting in one new subcycle:


SCC1.MRR1.MRR1:

+'(c(x, y), z) -> +'(y, z)
+'(x, c(y, z)) -> +'(x, z)
+'(x, c(y, z)) -> C(y, +(x, z))
C(x, c(y, z)) -> +'(x, y)
C(x, c(y, z)) -> C(+(x, y), z)
+'(c(x, y), z) -> C(x, +(y, z))

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(6) = 0
POL(3) = 0
POL(5) = 0
POL(+'(x_1, x_2)) = x_1 + x_2
POL(c(x_1, x_2)) = x_1 + x_2
POL(+(x_1, x_2)) = x_1 + x_2
POL(0) = 0
POL(9) = 1
POL(C(x_1, x_2)) = x_1 + x_2
POL(4) = 0
POL(8) = 0
POL(1) = 0
POL(7) = 0
POL(2) = 0

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   +(2, 9) -> c(1, 1)
   +(5, 9) -> c(1, 4)
   +(9, 4) -> c(1, 3)
   +(9, 6) -> c(1, 5)
   +(6, 9) -> c(1, 5)
   +(9, 5) -> c(1, 4)
   +(9, 3) -> c(1, 2)
   +(9, 9) -> c(1, 8)
   +(4, 9) -> c(1, 3)
   +(9, 2) -> c(1, 1)
   +(9, 8) -> c(1, 7)
   +(9, 7) -> c(1, 6)
   +(7, 9) -> c(1, 6)
   +(8, 9) -> c(1, 7)
   +(3, 9) -> c(1, 2)


 This transformation is resulting in one new subcycle:


SCC1.MRR1.MRR1.MRR1:

+'(c(x, y), z) -> C(x, +(y, z))
+'(x, c(y, z)) -> +'(x, z)
C(x, c(y, z)) -> +'(x, y)
C(x, c(y, z)) -> C(+(x, y), z)
+'(x, c(y, z)) -> C(y, +(x, z))
+'(c(x, y), z) -> +'(y, z)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(6) = 0
POL(3) = 0
POL(5) = 0
POL(+'(x_1, x_2)) = x_1 + x_2
POL(c(x_1, x_2)) = x_1 + x_2
POL(+(x_1, x_2)) = x_1 + x_2
POL(0) = 0
POL(9) = 0
POL(C(x_1, x_2)) = x_1 + x_2
POL(4) = 0
POL(8) = 0
POL(1) = 0
POL(7) = 1
POL(2) = 0

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   +(7, 5) -> c(1, 2)
   +(7, 4) -> c(1, 1)
   +(7, 6) -> c(1, 3)
   +(7, 8) -> c(1, 5)
   +(6, 7) -> c(1, 3)
   +(8, 7) -> c(1, 5)
   +(7, 7) -> c(1, 4)
   +(4, 7) -> c(1, 1)
   +(5, 7) -> c(1, 2)


 This transformation is resulting in one new subcycle:


SCC1.MRR1.MRR1.MRR1.MRR1:

+'(c(x, y), z) -> +'(y, z)
+'(x, c(y, z)) -> +'(x, z)
+'(x, c(y, z)) -> C(y, +(x, z))
C(x, c(y, z)) -> +'(x, y)
C(x, c(y, z)) -> C(+(x, y), z)
+'(c(x, y), z) -> C(x, +(y, z))

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(6) = 0
POL(3) = 0
POL(5) = 1
POL(+'(x_1, x_2)) = x_1 + x_2
POL(c(x_1, x_2)) = x_1 + x_2
POL(+(x_1, x_2)) = x_1 + x_2
POL(0) = 0
POL(9) = 0
POL(C(x_1, x_2)) = x_1 + x_2
POL(4) = 0
POL(8) = 0
POL(1) = 0
POL(7) = 0
POL(2) = 0

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   +(5, 8) -> c(1, 3)
   +(8, 5) -> c(1, 3)
   +(6, 5) -> c(1, 1)
   +(5, 6) -> c(1, 1)


 This transformation is resulting in one new subcycle:


SCC1.MRR1.MRR1.MRR1.MRR1.MRR1:

+'(c(x, y), z) -> C(x, +(y, z))
+'(x, c(y, z)) -> +'(x, z)
C(x, c(y, z)) -> +'(x, y)
C(x, c(y, z)) -> C(+(x, y), z)
+'(x, c(y, z)) -> C(y, +(x, z))
+'(c(x, y), z) -> +'(y, z)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(6) = 0
POL(3) = 1
POL(5) = 0
POL(+'(x_1, x_2)) = x_1 + x_2
POL(c(x_1, x_2)) = x_1 + x_2
POL(+(x_1, x_2)) = x_1 + x_2
POL(0) = 0
POL(9) = 0
POL(C(x_1, x_2)) = x_1 + x_2
POL(4) = 0
POL(8) = 0
POL(1) = 0
POL(7) = 0
POL(2) = 0

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   +(3, 8) -> c(1, 1)
   +(8, 3) -> c(1, 1)


 This transformation is resulting in one new subcycle:


SCC1.MRR1.MRR1.MRR1.MRR1.MRR1.MRR1:

+'(c(x, y), z) -> +'(y, z)
+'(x, c(y, z)) -> +'(x, z)
+'(x, c(y, z)) -> C(y, +(x, z))
C(x, c(y, z)) -> +'(x, y)
C(x, c(y, z)) -> C(+(x, y), z)
+'(c(x, y), z) -> C(x, +(y, z))

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(6) = 0
POL(3) = 0
POL(5) = 0
POL(+'(x_1, x_2)) = x_1 + x_2
POL(c(x_1, x_2)) = x_1 + x_2
POL(+(x_1, x_2)) = x_1 + x_2
POL(0) = 0
POL(9) = 0
POL(C(x_1, x_2)) = x_1 + x_2
POL(4) = 0
POL(8) = 1
POL(1) = 0
POL(7) = 0
POL(2) = 0

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   +(4, 8) -> c(1, 2)
   +(8, 8) -> c(1, 6)
   +(8, 6) -> c(1, 4)
   +(6, 8) -> c(1, 4)
   +(8, 4) -> c(1, 2)


 This transformation is resulting in one new subcycle:


SCC1.MRR1.MRR1.MRR1.MRR1.MRR1.MRR1.MRR1:

+'(c(x, y), z) -> C(x, +(y, z))
+'(x, c(y, z)) -> +'(x, z)
C(x, c(y, z)) -> +'(x, y)
C(x, c(y, z)) -> C(+(x, y), z)
+'(x, c(y, z)) -> C(y, +(x, z))
+'(c(x, y), z) -> +'(y, z)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(6) = 1
POL(3) = 0
POL(5) = 0
POL(+'(x_1, x_2)) = x_1 + x_2
POL(c(x_1, x_2)) = x_1 + x_2
POL(+(x_1, x_2)) = x_1 + x_2
POL(0) = 0
POL(9) = 0
POL(C(x_1, x_2)) = x_1 + x_2
POL(4) = 0
POL(8) = 0
POL(1) = 0
POL(7) = 0
POL(2) = 0

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   +(6, 6) -> c(1, 2)


 This transformation is resulting in one new subcycle:


SCC1.MRR1.MRR1.MRR1.MRR1.MRR1.MRR1.MRR1.MRR1:

+'(c(x, y), z) -> +'(y, z)
+'(x, c(y, z)) -> +'(x, z)
+'(x, c(y, z)) -> C(y, +(x, z))
C(x, c(y, z)) -> +'(x, y)
C(x, c(y, z)) -> C(+(x, y), z)
+'(c(x, y), z) -> C(x, +(y, z))

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(6) = 0
POL(3) = 0
POL(5) = 0
POL(+'(x_1, x_2)) = x_1 + x_2
POL(c(x_1, x_2)) = 1 + x_1 + x_2
POL(+(x_1, x_2)) = x_1 + x_2
POL(0) = 0
POL(9) = 0
POL(C(x_1, x_2)) = x_1 + x_2
POL(4) = 0
POL(8) = 0
POL(1) = 0
POL(7) = 0
POL(2) = 0

The following Dependency Pairs can be deleted:

   +'(c(x, y), z) -> +'(y, z)
   +'(x, c(y, z)) -> +'(x, z)
   +'(x, c(y, z)) -> C(y, +(x, z))
   C(x, c(y, z)) -> +'(x, y)
   C(x, c(y, z)) -> C(+(x, y), z)
   +'(c(x, y), z) -> C(x, +(y, z))



 This transformation is resulting in no new subcycles.


SCC2:

*'(c(x, y), z) -> *'(y, z)
*'(c(x, y), z) -> *'(x, z)
*'(x, c(y, z)) -> *'(x, z)
*'(x, c(y, z)) -> *'(x, y)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(*'(x_1, x_2)) = 1 + x_1 + x_2
POL(c(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   *'(c(x, y), z) -> *'(y, z)
   *'(c(x, y), z) -> *'(x, z)
   *'(x, c(y, z)) -> *'(x, z)
   *'(x, c(y, z)) -> *'(x, y)



 This transformation is resulting in no new subcycles.




Termination of R successfully shown.


Duration: 27.780 seconds.