Term Rewriting System R:

   [X, Y]
   nats -> adx(zeros)
   zeros -> cons(0, zeros)
   incr(cons(X, Y)) -> cons(s(X), incr(Y))
   adx(cons(X, Y)) -> incr(cons(X, adx(Y)))
   hd(cons(X, Y)) -> X
   tl(cons(X, Y)) -> Y

Termination of R to be shown.


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

   nats -> adx(zeros)
   hd(cons(X, Y)) -> X

where the Polynomial interpretation:
POL(s(x_1)) = x_1
POL(nats) = 1
POL(adx(x_1)) = x_1
POL(hd(x_1)) = 1 + x_1
POL(tl(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.


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

   tl(cons(X, Y)) -> Y

where the Polynomial interpretation:
POL(s(x_1)) = x_1
POL(adx(x_1)) = x_1
POL(tl(x_1)) = 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, Y)) -> INCR(Y)
   ADX(cons(X, Y)) -> INCR(cons(X, adx(Y)))
   ADX(cons(X, Y)) -> ADX(Y)
   ZEROS -> ZEROS

Furthermore, R contains three SCCs.


SCC1:

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

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, Y)) -> INCR(Y)



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