YES

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

Proof:
 DP Processor:
  DPs:
   terms#(N) -> sqr#(N)
   sqr#(s(X)) -> dbl#(X)
   sqr#(s(X)) -> sqr#(X)
   sqr#(s(X)) -> add#(sqr(X),dbl(X))
   dbl#(s(X)) -> dbl#(X)
   add#(s(X),Y) -> add#(X,Y)
  TRS:
   terms(N) -> cons(recip(sqr(N)))
   sqr(0()) -> 0()
   sqr(s(X)) -> s(add(sqr(X),dbl(X)))
   dbl(0()) -> 0()
   dbl(s(X)) -> s(s(dbl(X)))
   add(0(),X) -> X
   add(s(X),Y) -> s(add(X,Y))
   first(0(),X) -> nil()
   first(s(X),cons(Y)) -> cons(Y)
  LPO Processor:
   argument filtering:
    pi(terms) = []
    pi(sqr) = [0]
    pi(recip) = 0
    pi(cons) = []
    pi(0) = []
    pi(s) = [0]
    pi(dbl) = [0]
    pi(add) = [0,1]
    pi(first) = [1]
    pi(nil) = []
    pi(terms#) = [0]
    pi(sqr#) = [0]
    pi(dbl#) = 0
    pi(add#) = [0]
   precedence:
    terms# > sqr# > first > sqr > dbl > add ~ terms > add# ~ dbl# ~ nil ~ s ~ 0 ~ cons ~ recip
   problem:
    DPs:
     
    TRS:
     terms(N) -> cons(recip(sqr(N)))
     sqr(0()) -> 0()
     sqr(s(X)) -> s(add(sqr(X),dbl(X)))
     dbl(0()) -> 0()
     dbl(s(X)) -> s(s(dbl(X)))
     add(0(),X) -> X
     add(s(X),Y) -> s(add(X,Y))
     first(0(),X) -> nil()
     first(s(X),cons(Y)) -> cons(Y)
   Qed