Consider the TRS R consisting of the rewrite rules

1: terms(N) -> cons(recip(sqr(N)))
2: sqr(0) -> 0
3: sqr(s) -> s
4: dbl(0) -> 0
5: dbl(s) -> s
6: add(0,X) -> X
7: add(s,Y) -> s
8: first(0,X) -> nil
9: first(s,cons(Y)) -> cons(Y)

There is one dependency pair:

10: TERMS(N) -> SQR(N)

The approximated dependency graph contains no SCCs
and hence the TRS is trivially terminating.