Consider the TRS R consisting of the rewrite rules

1: first(0,X) -> nil
2: first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z)))
3: from(X) -> cons(X,n__from(s(X)))
4: first(X1,X2) -> n__first(X1,X2)
5: from(X) -> n__from(X)
6: activate(n__first(X1,X2)) -> first(X1,X2)
7: activate(n__from(X)) -> from(X)
8: activate(X) -> X

There are 3 dependency pairs:

9: FIRST(s(X),cons(Y,Z)) -> ACTIVATE(Z)
10: ACTIVATE(n__first(X1,X2)) -> FIRST(X1,X2)
11: ACTIVATE(n__from(X)) -> FROM(X)

The approximated dependency graph contains one SCC:
{9,10}.

- Consider the SCC {9,10}.
There are no usable rules.
By taking the polynomial interpretation
[ACTIVATE](x) = [s](x) = x + 1
and [cons](x,y) = [FIRST](x,y) = [n__first](x,y) = x + y + 1,
the rules in {9,10}
are strictly decreasing.

Hence the TRS is terminating.