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: half(0) -> 0
11: half(s(0)) -> 0
12: half(s(s(X))) -> s(half(X))
13: half(dbl(X)) -> X
14: terms(X) -> n__terms(X)
15: first(X1,X2) -> n__first(X1,X2)
16: activate(n__terms(X)) -> terms(X)
17: activate(n__first(X1,X2)) -> first(X1,X2)
18: activate(X) -> X

There are 10 dependency pairs:

19: TERMS(N) -> SQR(N)
20: SQR(s(X)) -> ADD(sqr(X),dbl(X))
21: SQR(s(X)) -> SQR(X)
22: SQR(s(X)) -> DBL(X)
23: DBL(s(X)) -> DBL(X)
24: ADD(s(X),Y) -> ADD(X,Y)
25: FIRST(s(X),cons(Y,Z)) -> ACTIVATE(Z)
26: HALF(s(s(X))) -> HALF(X)
27: ACTIVATE(n__terms(X)) -> TERMS(X)
28: ACTIVATE(n__first(X1,X2)) -> FIRST(X1,X2)

The approximated dependency graph contains 5 SCCs:
{24},
{23},
{26},
{21}
and {25,28}.

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

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

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

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

- Consider the SCC {25,28}.
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 {25,28}
are strictly decreasing.

Hence the TRS is terminating.