Consider the TRS R consisting of the rewrite rules

1: f(X) -> cons(X,n__f(n__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: g(X) -> n__g(X)
8: activate(n__f(X)) -> f(activate(X))
9: activate(n__g(X)) -> g(activate(X))
10: activate(X) -> X

There are 7 dependency pairs:

11: G(s(X)) -> G(X)
12: SEL(s(X),cons(Y,Z)) -> SEL(X,activate(Z))
13: SEL(s(X),cons(Y,Z)) -> ACTIVATE(Z)
14: ACTIVATE(n__f(X)) -> F(activate(X))
15: ACTIVATE(n__f(X)) -> ACTIVATE(X)
16: ACTIVATE(n__g(X)) -> G(activate(X))
17: ACTIVATE(n__g(X)) -> ACTIVATE(X)

The approximated dependency graph contains 3 SCCs:
{11},
{15,17}
and {12}.

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

- Consider the SCC {15,17}.
There are no usable rules.
By taking the polynomial interpretation
[ACTIVATE](x) = [n__f](x) = [n__g](x) = x + 1,
the rules in {15,17}
are strictly decreasing.

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

Hence the TRS is terminating.