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(n__s(X)))
4: first(X1,X2) -> n__first(X1,X2)
5: from(X) -> n__from(X)
6: s(X) -> n__s(X)
7: activate(n__first(X1,X2)) -> first(activate(X1),activate(X2))
8: activate(n__from(X)) -> from(activate(X))
9: activate(n__s(X)) -> s(activate(X))
10: activate(X) -> X

There are 8 dependency pairs:

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

The approximated dependency graph contains one SCC:
{11-14,16,18}.

- Consider the SCC {11-14,16,18}.
By taking the polynomial interpretation
[0] = [nil] = 1,
[activate](x) = [n__s](x) = [s](x) = x,
[ACTIVATE](x) = [from](x) = [n__from](x) = x + 1,
[first](x,y) = [FIRST](x,y) = [n__first](x,y) = x + y + 1
and [cons](x,y) = y,
the rules in {2-11,18}
are weakly decreasing and
the rules in {1,12-14,16}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {18}.
There are no usable rules.
By taking the polynomial interpretation
[ACTIVATE](x) = [n__s](x) = x + 1,
rule 18
is strictly decreasing.


Hence the TRS is terminating.