Consider the TRS R consisting of the rewrite rules

1: from(X) -> cons(X,n__from(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: activate(n__from(X)) -> from(X)
6: activate(X) -> X

There are 3 dependency pairs:

7: AFTER(s(N),cons(X,XS)) -> AFTER(N,activate(XS))
8: AFTER(s(N),cons(X,XS)) -> ACTIVATE(XS)
9: ACTIVATE(n__from(X)) -> FROM(X)

The approximated dependency graph contains one SCC:
{7}.

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

Hence the TRS is terminating.