Term Rewriting System R:

   [X, XS, X1, X2]
   a__zeros -> cons(0, zeros)
   a__zeros -> zeros
   a__tail(cons(X, XS)) -> mark(XS)
   a__tail(X) -> tail(X)
   mark(zeros) -> a__zeros
   mark(tail(X)) -> a__tail(mark(X))
   mark(cons(X1, X2)) -> cons(mark(X1), X2)
   mark(0) -> 0

Termination of R to be shown.


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

   a__zeros -> cons(0, zeros)
   a__zeros -> zeros
   mark(0) -> 0

where the Polynomial interpretation:
POL(tail(x_1)) = 1 + x_1
POL(a__tail(x_1)) = 1 + x_1
POL(mark(x_1)) = 1 + x_1
POL(zeros) = 0
POL(0) = 0
POL(a__zeros) = 1
POL(cons(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: 

   a__tail(cons(X, XS)) -> mark(XS)

where the Polynomial interpretation:
POL(tail(x_1)) = 1 + x_1
POL(a__tail(x_1)) = 1 + x_1
POL(mark(x_1)) = x_1
POL(zeros) = 0
POL(a__zeros) = 0
POL(cons(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: 

   a__tail(X) -> tail(X)

where the Polynomial interpretation:
POL(tail(x_1)) = 1 + x_1
POL(a__tail(x_1)) = 2 + x_1
POL(mark(x_1)) = 2*x_1
POL(zeros) = 0
POL(a__zeros) = 0
POL(cons(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: 

   mark(zeros) -> a__zeros

where the Polynomial interpretation:
POL(tail(x_1)) = x_1
POL(a__tail(x_1)) = x_1
POL(mark(x_1)) = x_1
POL(zeros) = 1
POL(a__zeros) = 0
POL(cons(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: 

   mark(tail(X)) -> a__tail(mark(X))

where the Polynomial interpretation:
POL(tail(x_1)) = 1 + x_1
POL(a__tail(x_1)) = x_1
POL(mark(x_1)) = x_1
POL(cons(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: 

   mark(cons(X1, X2)) -> cons(mark(X1), X2)

where the Polynomial interpretation:
POL(mark(x_1)) = 2*x_1
POL(cons(x_1, x_2)) = 1 + x_1 + x_2
was used. 



All Rules of R can be deleted.



Termination of R successfully shown.


Duration: 0.441 seconds.