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)
  Arctic Interpretation Processor:
   dimension: 1
   interpretation:
    [sqr#](x0) = x0,
    
    [terms#](x0) = 8x0 + 2,
    
    [nil] = 0,
    
    [first](x0, x1) = 3x0 + 1x1 + 1,
    
    [add](x0, x1) = 4x0 + 1x1 + 11,
    
    [dbl](x0) = 3x0 + 0,
    
    [s] = 0,
    
    [0] = 0,
    
    [cons](x0) = 3x0,
    
    [recip](x0) = 2x0,
    
    [sqr](x0) = 2x0,
    
    [terms](x0) = 8x0 + 0
   orientation:
    terms#(N) = 8N + 2 >= N = sqr#(N)
    
    terms(N) = 8N + 0 >= 7N = cons(recip(sqr(N)))
    
    sqr(0()) = 2 >= 0 = 0()
    
    sqr(s()) = 2 >= 0 = s()
    
    dbl(0()) = 3 >= 0 = 0()
    
    dbl(s()) = 3 >= 0 = s()
    
    add(0(),X) = 1X + 11 >= X = X
    
    add(s(),Y) = 1Y + 11 >= 0 = s()
    
    first(0(),X) = 1X + 3 >= 0 = nil()
    
    first(s(),cons(Y)) = 4Y + 3 >= 3Y = cons(Y)
   problem:
    DPs:
     
    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)
   Qed