Term Rewriting System R:

   [x, y, z, u]
   f(j(x, y), y) -> g(f(x, k(y)))
   f(x, h1(y, z)) -> h2(0, x, h1(y, z))
   g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
   h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
   i(f(x, h(y))) -> y
   i(h2(s(x), y, h1(x, z))) -> z
   k(h(x)) -> h1(0, x)
   k(h1(x, y)) -> h1(s(x), y)

Termination of R to be shown.


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

   f(j(x, y), y) -> g(f(x, k(y)))
   h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
   i(f(x, h(y))) -> y
   i(h2(s(x), y, h1(x, z))) -> z

where the Polynomial interpretation:
POL(g(x_1)) = x_1
POL(s(x_1)) = x_1
POL(i(x_1)) = 1 + x_1
POL(k(x_1)) = x_1
POL(h2(x_1, x_2, x_3)) = x_1 + x_2 + x_3
POL(h(x_1)) = x_1
POL(f(x_1, x_2)) = x_1 + x_2
POL(0) = 0
POL(j(x_1, x_2)) = 1 + x_1 + x_2
POL(h1(x_1, x_2)) = x_1 + x_2
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: 

   f(x, h1(y, z)) -> h2(0, x, h1(y, z))

where the Polynomial interpretation:
POL(g(x_1)) = x_1
POL(s(x_1)) = x_1
POL(k(x_1)) = x_1
POL(h2(x_1, x_2, x_3)) = x_1 + x_2 + x_3
POL(h(x_1)) = x_1
POL(f(x_1, x_2)) = 1 + x_1 + x_2
POL(0) = 0
POL(h1(x_1, x_2)) = x_1 + x_2
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: 

   g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))

where the Polynomial interpretation:
POL(g(x_1)) = 1 + x_1
POL(s(x_1)) = x_1
POL(k(x_1)) = x_1
POL(h2(x_1, x_2, x_3)) = x_1 + x_2 + x_3
POL(h(x_1)) = x_1
POL(0) = 0
POL(h1(x_1, x_2)) = x_1 + x_2
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: 

   k(h(x)) -> h1(0, x)

where the Polynomial interpretation:
POL(s(x_1)) = x_1
POL(k(x_1)) = x_1
POL(h(x_1)) = 1 + x_1
POL(0) = 0
POL(h1(x_1, x_2)) = x_1 + x_2
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: 

   k(h1(x, y)) -> h1(s(x), y)

where the Polynomial interpretation:
POL(s(x_1)) = x_1
POL(k(x_1)) = 1 + x_1
POL(h1(x_1, x_2)) = x_1 + x_2
was used. 



All Rules of R can be deleted.



Termination of R successfully shown.


Duration: 0.503 seconds.