Term Rewriting System R:

   [X, XS]
   zeros -> cons(0, zeros)
   tail(cons(X, XS)) -> XS

Termination of R to be shown.


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

   tail(cons(X, XS)) -> XS

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


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


   ZEROS -> ZEROS

Furthermore, R contains one SCC.


SCC1:

ZEROS -> ZEROS

Found an infinite P-chain over R:
P = ZEROS -> ZEROS
R = []
s = ZEROS evaluates to t = ZEROS
Thus, s starts an infinite reduction.


Non-Termination of R could be shown.

Duration: 0.413 seconds.