Consider the TRS R consisting of the rewrite rules

1: 2nd(cons1(X,cons(Y,Z))) -> Y
2: 2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1)))
3: from(X) -> cons(X,n__from(s(X)))
4: from(X) -> n__from(X)
5: activate(n__from(X)) -> from(X)
6: activate(X) -> X

There are 3 dependency pairs:

7: 2nd#(cons(X,X1)) -> 2nd#(cons1(X,activate(X1)))
8: 2nd#(cons(X,X1)) -> ACTIVATE(X1)
9: ACTIVATE(n__from(X)) -> FROM(X)

The approximated dependency graph contains no SCCs
and hence the TRS is trivially terminating.