Consider the TRS R consisting of the rewrite rules

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

There are 5 dependency pairs:

11: FIRST(s(X),cons(Y,Z)) -> ACTIVATE(Z)
12: SEL(s(X),cons(Y,Z)) -> SEL(X,activate(Z))
13: SEL(s(X),cons(Y,Z)) -> ACTIVATE(Z)
14: ACTIVATE(n__from(X)) -> FROM(X)
15: ACTIVATE(n__first(X1,X2)) -> FIRST(X1,X2)

The approximated dependency graph contains 2 SCCs:
{11,15}
and {12}.

- Consider the SCC {11,15}.
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 {11,15}
are strictly decreasing.

- Consider the SCC {12}.
The usable rules are {1-3,6-10}.
By taking the polynomial interpretation
[0] = [nil] = 1,
[n__from](x) = x,
[activate](x) = [from](x) = [s](x) = [SEL](x,y) = x + 1,
[first](x,y) = [n__first](x,y) = x + y + 1
and [cons](x,y) = y,
the rules in {1,3,7,8}
are weakly decreasing and
the rules in {2,6,9,10,12}
are strictly decreasing.

Hence the TRS is terminating.