Term Rewriting System R:

   [X, L]
   incr(nil) -> nil
   incr(cons(X, L)) -> cons(s(X), incr(L))
   adx(nil) -> nil
   adx(cons(X, L)) -> incr(cons(X, adx(L)))
   nats -> adx(zeros)
   zeros -> cons(0, zeros)
   head(cons(X, L)) -> X
   tail(cons(X, L)) -> L

Termination of R to be shown.


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

   adx(nil) -> nil
   head(cons(X, L)) -> X

where the Polynomial interpretation:
POL(nil) = 1
POL(s(x_1)) = x_1
POL(tail(x_1)) = x_1
POL(nats) = 0
POL(adx(x_1)) = 2*x_1
POL(zeros) = 0
POL(0) = 0
POL(incr(x_1)) = x_1
POL(cons(x_1, x_2)) = x_1 + x_2
POL(head(x_1)) = 2 + x_1
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: 

   nats -> adx(zeros)
   tail(cons(X, L)) -> L

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


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


R contains the following Dependency Pairs: 


   INCR(cons(X, L)) -> INCR(L)
   ADX(cons(X, L)) -> INCR(cons(X, adx(L)))
   ADX(cons(X, L)) -> ADX(L)
   ZEROS -> ZEROS

Furthermore, R contains three SCCs.


SCC1:

INCR(cons(X, L)) -> INCR(L)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(INCR(x_1)) = 1 + x_1
POL(cons(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   INCR(cons(X, L)) -> INCR(L)



 This transformation is resulting in no new subcycles.


SCC2:

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.597 seconds.