Consider the TRS R consisting of the rewrite rules

1: terms(N) -> cons(recip(sqr(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)) -> cons(Y)
10: half(0) -> 0
11: half(s(0)) -> 0
12: half(s(s(X))) -> s(half(X))
13: half(dbl(X)) -> X

There are 7 dependency pairs:

14: TERMS(N) -> SQR(N)
15: SQR(s(X)) -> ADD(sqr(X),dbl(X))
16: SQR(s(X)) -> SQR(X)
17: SQR(s(X)) -> DBL(X)
18: DBL(s(X)) -> DBL(X)
19: ADD(s(X),Y) -> ADD(X,Y)
20: HALF(s(s(X))) -> HALF(X)

The approximated dependency graph contains 4 SCCs:
{19},
{18},
{20}
and {16}.

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

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

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

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

Hence the TRS is terminating.