Consider the TRS R consisting of the rewrite rules

1: from(X) -> cons(X,n__from(n__s(X)))
2: after(0,XS) -> XS
3: after(s(N),cons(X,XS)) -> after(N,activate(XS))
4: from(X) -> n__from(X)
5: s(X) -> n__s(X)
6: activate(n__from(X)) -> from(activate(X))
7: activate(n__s(X)) -> s(activate(X))
8: activate(X) -> X

There are 6 dependency pairs:

9: AFTER(s(N),cons(X,XS)) -> AFTER(N,activate(XS))
10: AFTER(s(N),cons(X,XS)) -> ACTIVATE(XS)
11: ACTIVATE(n__from(X)) -> FROM(activate(X))
12: ACTIVATE(n__from(X)) -> ACTIVATE(X)
13: ACTIVATE(n__s(X)) -> S(activate(X))
14: ACTIVATE(n__s(X)) -> ACTIVATE(X)

The approximated dependency graph contains 2 SCCs:
{12,14}
and {9}.

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

- Consider the SCC {9}.
The usable rules are {1,4-8}.
By taking the polynomial interpretation
[activate](x) = [AFTER](x,y) = [cons](x,y) = [from](x) = [n__from](x) = [n__s](x) = [s](x) = x + 1,
the rules in {1,4-7}
are weakly decreasing and
the rules in {8,9}
are strictly decreasing.

Hence the TRS is terminating.