YES
TRS:
 {            sqr(0()) -> 0(),
             sqr(s(X)) -> s(add(sqr(X), dbl(X))),
              terms(N) -> cons(recip(sqr(N))),
           add(0(), X) -> X,
          add(s(X), Y) -> s(add(X, Y)),
              dbl(0()) -> 0(),
             dbl(s(X)) -> s(s(dbl(X))),
         first(0(), X) -> nil(),
  first(s(X), cons(Y)) -> cons(Y)}
 DP:
  Strict:
   {   sqr#(s(X)) -> sqr#(X),
       sqr#(s(X)) -> add#(sqr(X), dbl(X)),
       sqr#(s(X)) -> dbl#(X),
        terms#(N) -> sqr#(N),
    add#(s(X), Y) -> add#(X, Y),
       dbl#(s(X)) -> dbl#(X)}
  Weak:
  {            sqr(0()) -> 0(),
              sqr(s(X)) -> s(add(sqr(X), dbl(X))),
               terms(N) -> cons(recip(sqr(N))),
            add(0(), X) -> X,
           add(s(X), Y) -> s(add(X, Y)),
               dbl(0()) -> 0(),
              dbl(s(X)) -> s(s(dbl(X))),
          first(0(), X) -> nil(),
   first(s(X), cons(Y)) -> cons(Y)}
  EDG:
   {(terms#(N) -> sqr#(N), sqr#(s(X)) -> dbl#(X))
    (terms#(N) -> sqr#(N), sqr#(s(X)) -> add#(sqr(X), dbl(X)))
    (terms#(N) -> sqr#(N), sqr#(s(X)) -> sqr#(X))
    (sqr#(s(X)) -> sqr#(X), sqr#(s(X)) -> dbl#(X))
    (sqr#(s(X)) -> sqr#(X), sqr#(s(X)) -> add#(sqr(X), dbl(X)))
    (sqr#(s(X)) -> sqr#(X), sqr#(s(X)) -> sqr#(X))
    (dbl#(s(X)) -> dbl#(X), dbl#(s(X)) -> dbl#(X))
    (sqr#(s(X)) -> dbl#(X), dbl#(s(X)) -> dbl#(X))
    (sqr#(s(X)) -> add#(sqr(X), dbl(X)), add#(s(X), Y) -> add#(X, Y))
    (add#(s(X), Y) -> add#(X, Y), add#(s(X), Y) -> add#(X, Y))}
   SCCS:
    Scc:
     {dbl#(s(X)) -> dbl#(X)}
    Scc:
     {add#(s(X), Y) -> add#(X, Y)}
    Scc:
     {sqr#(s(X)) -> sqr#(X)}
    SCC:
     Strict:
      {dbl#(s(X)) -> dbl#(X)}
     Weak:
     {            sqr(0()) -> 0(),
                 sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                  terms(N) -> cons(recip(sqr(N))),
               add(0(), X) -> X,
              add(s(X), Y) -> s(add(X, Y)),
                  dbl(0()) -> 0(),
                 dbl(s(X)) -> s(s(dbl(X))),
             first(0(), X) -> nil(),
      first(s(X), cons(Y)) -> cons(Y)}
     SPSC:
      Simple Projection:
       pi(dbl#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {add#(s(X), Y) -> add#(X, Y)}
     Weak:
     {            sqr(0()) -> 0(),
                 sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                  terms(N) -> cons(recip(sqr(N))),
               add(0(), X) -> X,
              add(s(X), Y) -> s(add(X, Y)),
                  dbl(0()) -> 0(),
                 dbl(s(X)) -> s(s(dbl(X))),
             first(0(), X) -> nil(),
      first(s(X), cons(Y)) -> cons(Y)}
     SPSC:
      Simple Projection:
       pi(add#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {sqr#(s(X)) -> sqr#(X)}
     Weak:
     {            sqr(0()) -> 0(),
                 sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                  terms(N) -> cons(recip(sqr(N))),
               add(0(), X) -> X,
              add(s(X), Y) -> s(add(X, Y)),
                  dbl(0()) -> 0(),
                 dbl(s(X)) -> s(s(dbl(X))),
             first(0(), X) -> nil(),
      first(s(X), cons(Y)) -> cons(Y)}
     SPSC:
      Simple Projection:
       pi(sqr#) = 0
      Strict:
       {}
      Qed