Term Rewriting System R:

   [x, y, z]
   *(x, *(y, z)) -> *(otimes(x, y), z)
   *(1, y) -> y
   *(+(x, y), z) -> oplus(*(x, z), *(y, z))
   *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   *'(x, *(y, z)) -> *'(otimes(x, y), z)
   *'(+(x, y), z) -> *'(x, z)
   *'(+(x, y), z) -> *'(y, z)
   *'(x, oplus(y, z)) -> *'(x, y)
   *'(x, oplus(y, z)) -> *'(x, z)

Furthermore, R contains one SCC.


SCC1:

*'(x, oplus(y, z)) -> *'(x, z)
*'(+(x, y), z) -> *'(y, z)
*'(+(x, y), z) -> *'(x, z)
*'(x, oplus(y, z)) -> *'(x, y)
*'(x, *(y, z)) -> *'(otimes(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(*(x_1, x_2)) = x_1 + x_2
POL(oplus(x_1, x_2)) = 1 + x_1 + x_2
POL(otimes(x_1, x_2)) = x_1 + x_2
POL(*'(x_1, x_2)) = 1 + x_1 + x_2
POL(+(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   *'(x, oplus(y, z)) -> *'(x, z)
   *'(+(x, y), z) -> *'(y, z)
   *'(+(x, y), z) -> *'(x, z)
   *'(x, oplus(y, z)) -> *'(x, y)
   *'(x, *(y, z)) -> *'(otimes(x, y), z)



 This transformation is resulting in no new subcycles.




Termination of R successfully shown.


Duration: 0.534 seconds.