Consider the TRS R consisting of the rewrite rules

1: f(X) -> cons(X,n__f(g(X)))
2: g(0) -> s(0)
3: g(s(X)) -> s(s(g(X)))
4: sel(0,cons(X,Y)) -> X
5: sel(s(X),cons(Y,Z)) -> sel(X,activate(Z))
6: f(X) -> n__f(X)
7: activate(n__f(X)) -> f(X)
8: activate(X) -> X

There are 5 dependency pairs:

9: F(X) -> G(X)
10: G(s(X)) -> G(X)
11: SEL(s(X),cons(Y,Z)) -> SEL(X,activate(Z))
12: SEL(s(X),cons(Y,Z)) -> ACTIVATE(Z)
13: ACTIVATE(n__f(X)) -> F(X)

The approximated dependency graph contains 2 SCCs:
{10}
and {11}.

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

- Consider the SCC {11}.
The usable rules are {1-3,6-8}.
By taking the polynomial interpretation
[0] = 1,
[activate](x) = 2x + 1,
[cons](x,y) = [f](x) = [g](x) = [n__f](x) = 2x + 2,
[SEL](x,y) = x + 1
and [s](x) = x + 2,
the rules in {1,3,6}
are weakly decreasing and
the rules in {2,7,8,11}
are strictly decreasing.

Hence the TRS is terminating.