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)
  Usable Rule Processor:
   DPs:
    terms#(N) -> sqr#(N)
   TRS:
    
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     
    interpretation:
     [sqr#](x0) = 0,
     
     [terms#](x0) = x0 + 1
    orientation:
     terms#(N) = N + 1 >= 0 = sqr#(N)
    problem:
     DPs:
      
     TRS:
      
    Qed