Term Rewriting System R:

   [x, y]
   intlist(nil) -> nil
   intlist(cons(x, y)) -> cons(s(x), intlist(y))
   int(0, 0) -> cons(0, nil)
   int(0, s(y)) -> cons(0, int(s(0), s(y)))
   int(s(x), 0) -> nil
   int(s(x), s(y)) -> intlist(int(x, y))

Innermost Termination of R to be shown.


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

   int(0, 0) -> cons(0, nil)
   int(s(x), 0) -> nil

where the Polynomial interpretation:
POL(nil) = 0
POL(s(x_1)) = x_1
POL(intlist(x_1)) = x_1
POL(int(x_1, x_2)) = 1 + x_1 + x_2
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.


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

   intlist(nil) -> nil

where the Polynomial interpretation:
POL(nil) = 1
POL(s(x_1)) = 2*x_1
POL(intlist(x_1)) = 2*x_1
POL(int(x_1, x_2)) = x_1 + x_2
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.


R contains the following Dependency Pairs: 


   INT(s(x), s(y)) -> INTLIST(int(x, y))
   INT(s(x), s(y)) -> INT(x, y)
   INT(0, s(y)) -> INT(s(0), s(y))
   INTLIST(cons(x, y)) -> INTLIST(y)

Furthermore, R contains two SCCs.


SCC1:

INTLIST(cons(x, y)) -> INTLIST(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(INTLIST(x_1)) = 1 + x_1
POL(cons(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   INTLIST(cons(x, y)) -> INTLIST(y)



 This transformation is resulting in no new subcycles.


SCC2:

INT(0, s(y)) -> INT(s(0), s(y))
INT(s(x), s(y)) -> INT(x, y)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(s(x_1)) = 1 + x_1
POL(INT(x_1, x_2)) = x_2
POL(0) = 0

 resulting in no subcycles.




Innermost Termination of R successfully shown.


Duration: 0.671 seconds.