YES

Problem:
 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)

Proof:
 DP Processor:
  DPs:
   terms#(N) -> sqr#(N)
  TRS:
   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)
  TDG Processor:
   DPs:
    terms#(N) -> sqr#(N)
   TRS:
    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)
   graph:
    
   Qed