Term Rewriting System R:

   [m, n, r]
   p(m, n, s(r)) -> p(m, r, n)
   p(m, s(n), 0) -> p(0, n, m)
   p(m, 0, 0) -> m

Termination of R to be shown.


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

   p(m, n, s(r)) -> p(m, r, n)
   p(m, s(n), 0) -> p(0, n, m)
   p(m, 0, 0) -> m

where the Polynomial interpretation:
POL(s(x_1)) = 1 + x_1
POL(0) = 0
POL(p(x_1, x_2, x_3)) = 2 + x_1 + x_2 + x_3
was used. 



All Rules of R can be deleted.



Termination of R successfully shown.


Duration: 0.363 seconds.