Term Rewriting System R:

   [x]
   half(0) -> 0
   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))
   lastbit(0) -> 0
   lastbit(s(0)) -> s(0)
   lastbit(s(s(x))) -> lastbit(x)
   conv(0) -> cons(nil, 0)
   conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))

Termination of R to be shown.


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


R contains the following Dependency Pairs: 


   LASTBIT(s(s(x))) -> LASTBIT(x)
   HALF(s(s(x))) -> HALF(x)
   CONV(s(x)) -> CONV(half(s(x)))
   CONV(s(x)) -> HALF(s(x))
   CONV(s(x)) -> LASTBIT(s(x))

Furthermore, R contains three SCCs.


SCC1:

LASTBIT(s(s(x))) -> LASTBIT(x)

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(s(x_1)) = 1 + x_1
POL(LASTBIT(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

   LASTBIT(s(s(x))) -> LASTBIT(x)



 This transformation is resulting in no new subcycles.


SCC2:

HALF(s(s(x))) -> HALF(x)

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(s(x_1)) = 1 + x_1
POL(HALF(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

   HALF(s(s(x))) -> HALF(x)



 This transformation is resulting in no new subcycles.


SCC3:

CONV(s(x)) -> CONV(half(s(x)))

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(s(x_1)) = 1 + x_1
POL(CONV(x_1)) = 1 + x_1
POL(half(x_1)) = x_1
POL(0) = 0

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   half(s(0)) -> 0
   half(s(s(x))) -> s(half(x))


 This transformation is resulting in no new subcycles.




Termination of R successfully shown.


Duration: 0.824 seconds.