YES

We show the termination of the TRS R:

  terms(N) -> cons(recip(sqr(N)))
  sqr(|0|()) -> |0|()
  sqr(s()) -> s()
  dbl(|0|()) -> |0|()
  dbl(s()) -> s()
  add(|0|(),X) -> X
  add(s(),Y) -> s()
  first(|0|(),X) -> nil()
  first(s(),cons(Y)) -> cons(Y)

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: terms#(N) -> sqr#(N)

and R consists of:

r1: terms(N) -> cons(recip(sqr(N)))
r2: sqr(|0|()) -> |0|()
r3: sqr(s()) -> s()
r4: dbl(|0|()) -> |0|()
r5: dbl(s()) -> s()
r6: add(|0|(),X) -> X
r7: add(s(),Y) -> s()
r8: first(|0|(),X) -> nil()
r9: first(s(),cons(Y)) -> cons(Y)

The estimated dependency graph contains the following SCCs:

  (no SCCs)