Consider the TRS R consisting of the rewrite rules

1: terms(N) -> cons(recip(sqr(N)),n__terms(s(N)))
2: sqr(0) -> 0
3: sqr(s(X)) -> s(add(sqr(X),dbl(X)))
4: dbl(0) -> 0
5: dbl(s(X)) -> s(s(dbl(X)))
6: add(0,X) -> X
7: add(s(X),Y) -> s(add(X,Y))
8: first(0,X) -> nil
9: first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z)))
10: terms(X) -> n__terms(X)
11: first(X1,X2) -> n__first(X1,X2)
12: activate(n__terms(X)) -> terms(X)
13: activate(n__first(X1,X2)) -> first(X1,X2)
14: activate(X) -> X

There are 9 dependency pairs:

15: TERMS(N) -> SQR(N)
16: SQR(s(X)) -> ADD(sqr(X),dbl(X))
17: SQR(s(X)) -> SQR(X)
18: SQR(s(X)) -> DBL(X)
19: DBL(s(X)) -> DBL(X)
20: ADD(s(X),Y) -> ADD(X,Y)
21: FIRST(s(X),cons(Y,Z)) -> ACTIVATE(Z)
22: ACTIVATE(n__terms(X)) -> TERMS(X)
23: ACTIVATE(n__first(X1,X2)) -> FIRST(X1,X2)

The approximated dependency graph contains 4 SCCs:
{20},
{19},
{17}
and {21,23}.

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

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

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

- Consider the SCC {21,23}.
There are no usable rules.
By taking the polynomial interpretation
[ACTIVATE](x) = [s](x) = x + 1
and [cons](x,y) = [FIRST](x,y) = [n__first](x,y) = x + y + 1,
the rules in {21,23}
are strictly decreasing.

Hence the TRS is terminating.