Term Rewriting System R:

   [x]
   +(p1, p1) -> p2
   +(p1, +(p2, p2)) -> p5
   +(p5, p5) -> p10
   +(+(x, y), z) -> +(x, +(y, z))
   +(p1, +(p1, x)) -> +(p2, x)
   +(p1, +(p2, +(p2, x))) -> +(p5, x)
   +(p2, p1) -> +(p1, p2)
   +(p2, +(p1, x)) -> +(p1, +(p2, x))
   +(p2, +(p2, p2)) -> +(p1, p5)
   +(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
   +(p5, p1) -> +(p1, p5)
   +(p5, +(p1, x)) -> +(p1, +(p5, x))
   +(p5, p2) -> +(p2, p5)
   +(p5, +(p2, x)) -> +(p2, +(p5, x))
   +(p5, +(p5, x)) -> +(p10, x)
   +(p10, p1) -> +(p1, p10)
   +(p10, +(p1, x)) -> +(p1, +(p10, x))
   +(p10, p2) -> +(p2, p10)
   +(p10, +(p2, x)) -> +(p2, +(p10, x))
   +(p10, p5) -> +(p5, p10)
   +(p10, +(p5, x)) -> +(p5, +(p10, x))

Termination of R to be shown.


Removing the following rules from R which fullfill a polynomial ordering: 

   +(p1, p1) -> p2
   +(p1, +(p2, p2)) -> p5
   +(p1, +(p1, x)) -> +(p2, x)
   +(p1, +(p2, +(p2, x))) -> +(p5, x)
   +(p2, +(p2, p2)) -> +(p1, p5)
   +(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))

where the Polynomial interpretation:
POL(p10) = 0
POL(p1) = 1
POL(z) = 0
POL(+(x_1, x_2)) = x_1 + x_2
POL(p5) = 0
POL(y) = 1
POL(p2) = 1
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   +(p5, p5) -> p10
   +(p5, +(p5, x)) -> +(p10, x)

where the Polynomial interpretation:
POL(p10) = 0
POL(z) = 0
POL(p1) = 0
POL(+(x_1, x_2)) = x_1 + x_2
POL(y) = 1
POL(p5) = 1
POL(p2) = 0
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   +(+(x, y), z) -> +(x, +(y, z))

where the Polynomial interpretation:
POL(p10) = 0
POL(p1) = 0
POL(z) = 0
POL(+(x_1, x_2)) = 1 + 2*x_1 + x_2
POL(p5) = 0
POL(y) = 2
POL(p2) = 0
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   +(p2, p1) -> +(p1, p2)
   +(p2, +(p1, x)) -> +(p1, +(p2, x))
   +(p5, p1) -> +(p1, p5)
   +(p5, +(p1, x)) -> +(p1, +(p5, x))
   +(p10, p1) -> +(p1, p10)
   +(p10, +(p1, x)) -> +(p1, +(p10, x))

where the Polynomial interpretation:
POL(p10) = 0
POL(p1) = 1
POL(+(x_1, x_2)) = 2 + x_1 + 2*x_2
POL(p5) = 0
POL(p2) = 0
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   +(p5, p2) -> +(p2, p5)
   +(p5, +(p2, x)) -> +(p2, +(p5, x))
   +(p10, p2) -> +(p2, p10)
   +(p10, +(p2, x)) -> +(p2, +(p10, x))

where the Polynomial interpretation:
POL(p10) = 0
POL(+(x_1, x_2)) = 2 + x_1 + 2*x_2
POL(p5) = 0
POL(p2) = 1
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   +(p10, p5) -> +(p5, p10)
   +(p10, +(p5, x)) -> +(p5, +(p10, x))

where the Polynomial interpretation:
POL(p10) = 0
POL(+(x_1, x_2)) = x_1 + 2*x_2
POL(p5) = 1
was used. 



All Rules of R can be deleted.



Termination of R successfully shown.


Duration: 0.564 seconds.