Consider the TRS R consisting of the rewrite rules

1: from(X) -> cons(X,n__from(n__s(X)))
2: head(cons(X,XS)) -> X
3: 2nd(cons(X,XS)) -> head(activate(XS))
4: take(0,XS) -> nil
5: take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS)))
6: sel(0,cons(X,XS)) -> X
7: sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
8: from(X) -> n__from(X)
9: s(X) -> n__s(X)
10: take(X1,X2) -> n__take(X1,X2)
11: activate(n__from(X)) -> from(activate(X))
12: activate(n__s(X)) -> s(activate(X))
13: activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
14: activate(X) -> X

There are 12 dependency pairs:

15: 2nd#(cons(X,XS)) -> HEAD(activate(XS))
16: 2nd#(cons(X,XS)) -> ACTIVATE(XS)
17: TAKE(s(N),cons(X,XS)) -> ACTIVATE(XS)
18: SEL(s(N),cons(X,XS)) -> SEL(N,activate(XS))
19: SEL(s(N),cons(X,XS)) -> ACTIVATE(XS)
20: ACTIVATE(n__from(X)) -> FROM(activate(X))
21: ACTIVATE(n__from(X)) -> ACTIVATE(X)
22: ACTIVATE(n__s(X)) -> S(activate(X))
23: ACTIVATE(n__s(X)) -> ACTIVATE(X)
24: ACTIVATE(n__take(X1,X2)) -> TAKE(activate(X1),activate(X2))
25: ACTIVATE(n__take(X1,X2)) -> ACTIVATE(X1)
26: ACTIVATE(n__take(X1,X2)) -> ACTIVATE(X2)

The approximated dependency graph contains 2 SCCs:
{17,21,23-26}
and {18}.

- Consider the SCC {17,21,23-26}.
The usable rules are {1,4,5,8-14}.
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,
[n__take](x,y) = [take](x,y) = [TAKE](x,y) = x + y + 1
and [cons](x,y) = y,
the rules in {1,5,8-14,17,23}
are weakly decreasing and
the rules in {4,21,24-26}
are strictly decreasing.
There is one new SCC.

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


- Consider the SCC {18}.
The usable rules are {1,4,5,8-14}.
By taking the polynomial interpretation
[0] = [nil] = 1,
[activate](x) = x,
[cons](x,y) = [from](x) = [n__from](x) = [n__s](x) = [s](x) = [SEL](x,y) = x + 1
and [n__take](x,y) = [take](x,y) = x + y + 1,
the rules in {1,8-14}
are weakly decreasing and
the rules in {4,5,18}
are strictly decreasing.

Hence the TRS is terminating.