Term Rewriting System R:

   [X, Y, Z, X1]
   2nd(cons1(X, cons(Y, Z))) -> Y
   2nd(cons(X, X1)) -> 2nd(cons1(X, activate(X1)))
   from(X) -> cons(X, n__from(s(X)))
   from(X) -> n__from(X)
   activate(n__from(X)) -> from(X)
   activate(X) -> X

Termination of R to be shown.


R contains the following Dependency Pairs: 


   2ND(cons(X, X1)) -> 2ND(cons1(X, activate(X1)))
   2ND(cons(X, X1)) -> ACTIVATE(X1)
   ACTIVATE(n__from(X)) -> FROM(X)

R contains no SCCs.




Termination of R successfully shown.


Duration: 0.465 seconds.