Term Rewriting System R:

   [x, y, z]
   norm(nil) -> 0
   norm(g(x, y)) -> s(norm(x))
   f(x, nil) -> g(nil, x)
   f(x, g(y, z)) -> g(f(x, y), z)
   rem(nil, y) -> nil
   rem(g(x, y), 0) -> g(x, y)
   rem(g(x, y), s(z)) -> rem(x, z)

Termination of R to be shown.


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

   norm(nil) -> 0

where the Polynomial interpretation:
POL(g(x_1, x_2)) = x_1 + x_2
POL(nil) = 0
POL(s(x_1)) = x_1
POL(norm(x_1)) = 1 + x_1
POL(rem(x_1, x_2)) = x_1 + x_2
POL(f(x_1, x_2)) = x_1 + x_2
POL(0) = 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: 

   norm(g(x, y)) -> s(norm(x))
   rem(g(x, y), s(z)) -> rem(x, z)

where the Polynomial interpretation:
POL(nil) = 0
POL(g(x_1, x_2)) = 1 + x_1 + x_2
POL(s(x_1)) = x_1
POL(norm(x_1)) = x_1
POL(rem(x_1, x_2)) = x_1 + x_2
POL(f(x_1, x_2)) = 1 + x_1 + x_2
POL(0) = 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: 

   f(x, nil) -> g(nil, x)

where the Polynomial interpretation:
POL(g(x_1, x_2)) = x_1 + x_2
POL(nil) = 0
POL(rem(x_1, x_2)) = x_1 + x_2
POL(f(x_1, x_2)) = 1 + x_1 + x_2
POL(0) = 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: 

   f(x, g(y, z)) -> g(f(x, y), z)

where the Polynomial interpretation:
POL(nil) = 0
POL(g(x_1, x_2)) = 1 + x_1 + x_2
POL(rem(x_1, x_2)) = x_1 + x_2
POL(f(x_1, x_2)) = x_1 + 2*x_2
POL(0) = 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: 

   rem(nil, y) -> nil

where the Polynomial interpretation:
POL(g(x_1, x_2)) = x_1 + x_2
POL(nil) = 1
POL(rem(x_1, x_2)) = 2*x_1 + x_2
POL(0) = 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: 

   rem(g(x, y), 0) -> g(x, y)

where the Polynomial interpretation:
POL(g(x_1, x_2)) = x_1 + x_2
POL(rem(x_1, x_2)) = 1 + x_1 + x_2
POL(0) = 0
was used. 



All Rules of R can be deleted.



Termination of R successfully shown.


Duration: 0.459 seconds.