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)

There are 6 dependency pairs:

10: TERMS(N) -> SQR(N)
11: SQR(s(X)) -> ADD(sqr(X),dbl(X))
12: SQR(s(X)) -> SQR(X)
13: SQR(s(X)) -> DBL(X)
14: DBL(s(X)) -> DBL(X)
15: ADD(s(X),Y) -> ADD(X,Y)

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

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

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

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

Hence the TRS is terminating.