YES
TRS:
 {                  sqr(0()) -> 0(),
                   sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                    terms(N) -> cons(recip(sqr(N)), n__terms(n__s(N))),
                    terms(X) -> n__terms(X),
                        s(X) -> n__s(X),
                 add(0(), X) -> X,
                add(s(X), Y) -> s(add(X, Y)),
                    dbl(0()) -> 0(),
                   dbl(s(X)) -> s(s(dbl(X))),
               first(X1, X2) -> n__first(X1, X2),
               first(0(), X) -> nil(),
     first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
                 activate(X) -> X,
       activate(n__terms(X)) -> terms(activate(X)),
           activate(n__s(X)) -> s(activate(X)),
  activate(n__first(X1, X2)) -> first(activate(X1), activate(X2))}
 DP:
  Strict:
   {                 sqr#(s(X)) -> sqr#(X),
                     sqr#(s(X)) -> s#(add(sqr(X), dbl(X))),
                     sqr#(s(X)) -> add#(sqr(X), dbl(X)),
                     sqr#(s(X)) -> dbl#(X),
                      terms#(N) -> sqr#(N),
                  add#(s(X), Y) -> s#(add(X, Y)),
                  add#(s(X), Y) -> add#(X, Y),
                     dbl#(s(X)) -> s#(s(dbl(X))),
                     dbl#(s(X)) -> s#(dbl(X)),
                     dbl#(s(X)) -> dbl#(X),
       first#(s(X), cons(Y, Z)) -> activate#(Z),
         activate#(n__terms(X)) -> terms#(activate(X)),
         activate#(n__terms(X)) -> activate#(X),
             activate#(n__s(X)) -> s#(activate(X)),
             activate#(n__s(X)) -> activate#(X),
    activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)),
    activate#(n__first(X1, X2)) -> activate#(X1),
    activate#(n__first(X1, X2)) -> activate#(X2)}
  Weak:
  {                  sqr(0()) -> 0(),
                    sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                     terms(N) -> cons(recip(sqr(N)), n__terms(n__s(N))),
                     terms(X) -> n__terms(X),
                         s(X) -> n__s(X),
                  add(0(), X) -> X,
                 add(s(X), Y) -> s(add(X, Y)),
                     dbl(0()) -> 0(),
                    dbl(s(X)) -> s(s(dbl(X))),
                first(X1, X2) -> n__first(X1, X2),
                first(0(), X) -> nil(),
      first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
                  activate(X) -> X,
        activate(n__terms(X)) -> terms(activate(X)),
            activate(n__s(X)) -> s(activate(X)),
   activate(n__first(X1, X2)) -> first(activate(X1), activate(X2))}
  EDG:
   {(activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)), first#(s(X), cons(Y, Z)) -> activate#(Z))
    (sqr#(s(X)) -> dbl#(X), dbl#(s(X)) -> dbl#(X))
    (sqr#(s(X)) -> dbl#(X), dbl#(s(X)) -> s#(dbl(X)))
    (sqr#(s(X)) -> dbl#(X), dbl#(s(X)) -> s#(s(dbl(X))))
    (activate#(n__terms(X)) -> activate#(X), activate#(n__first(X1, X2)) -> activate#(X2))
    (activate#(n__terms(X)) -> activate#(X), activate#(n__first(X1, X2)) -> activate#(X1))
    (activate#(n__terms(X)) -> activate#(X), activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)))
    (activate#(n__terms(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
    (activate#(n__terms(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__terms(X)) -> activate#(X), activate#(n__terms(X)) -> activate#(X))
    (activate#(n__terms(X)) -> activate#(X), activate#(n__terms(X)) -> terms#(activate(X)))
    (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)) -> s#(add(sqr(X), dbl(X))))
    (terms#(N) -> sqr#(N), sqr#(s(X)) -> sqr#(X))
    (activate#(n__first(X1, X2)) -> activate#(X2), activate#(n__terms(X)) -> terms#(activate(X)))
    (activate#(n__first(X1, X2)) -> activate#(X2), activate#(n__terms(X)) -> activate#(X))
    (activate#(n__first(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__first(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> activate#(X))
    (activate#(n__first(X1, X2)) -> activate#(X2), activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)))
    (activate#(n__first(X1, X2)) -> activate#(X2), activate#(n__first(X1, X2)) -> activate#(X1))
    (activate#(n__first(X1, X2)) -> activate#(X2), activate#(n__first(X1, X2)) -> activate#(X2))
    (add#(s(X), Y) -> add#(X, Y), add#(s(X), Y) -> s#(add(X, Y)))
    (add#(s(X), Y) -> add#(X, Y), add#(s(X), Y) -> add#(X, Y))
    (activate#(n__s(X)) -> activate#(X), activate#(n__terms(X)) -> terms#(activate(X)))
    (activate#(n__s(X)) -> activate#(X), activate#(n__terms(X)) -> activate#(X))
    (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
    (activate#(n__s(X)) -> activate#(X), activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)))
    (activate#(n__s(X)) -> activate#(X), activate#(n__first(X1, X2)) -> activate#(X1))
    (activate#(n__s(X)) -> activate#(X), activate#(n__first(X1, X2)) -> activate#(X2))
    (dbl#(s(X)) -> dbl#(X), dbl#(s(X)) -> s#(s(dbl(X))))
    (dbl#(s(X)) -> dbl#(X), dbl#(s(X)) -> s#(dbl(X)))
    (dbl#(s(X)) -> dbl#(X), dbl#(s(X)) -> dbl#(X))
    (sqr#(s(X)) -> sqr#(X), sqr#(s(X)) -> sqr#(X))
    (sqr#(s(X)) -> sqr#(X), sqr#(s(X)) -> s#(add(sqr(X), dbl(X))))
    (sqr#(s(X)) -> sqr#(X), sqr#(s(X)) -> add#(sqr(X), dbl(X)))
    (sqr#(s(X)) -> sqr#(X), sqr#(s(X)) -> dbl#(X))
    (sqr#(s(X)) -> add#(sqr(X), dbl(X)), add#(s(X), Y) -> s#(add(X, Y)))
    (sqr#(s(X)) -> add#(sqr(X), dbl(X)), add#(s(X), Y) -> add#(X, Y))
    (activate#(n__terms(X)) -> terms#(activate(X)), terms#(N) -> sqr#(N))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__terms(X)) -> terms#(activate(X)))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__terms(X)) -> activate#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__s(X)) -> s#(activate(X)))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__s(X)) -> activate#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__first(X1, X2)) -> activate#(X1))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__first(X1, X2)) -> activate#(X2))
    (activate#(n__first(X1, X2)) -> activate#(X1), activate#(n__terms(X)) -> terms#(activate(X)))
    (activate#(n__first(X1, X2)) -> activate#(X1), activate#(n__terms(X)) -> activate#(X))
    (activate#(n__first(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__first(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X))
    (activate#(n__first(X1, X2)) -> activate#(X1), activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)))
    (activate#(n__first(X1, X2)) -> activate#(X1), activate#(n__first(X1, X2)) -> activate#(X1))
    (activate#(n__first(X1, X2)) -> activate#(X1), activate#(n__first(X1, X2)) -> activate#(X2))}
   SCCS:
    Scc:
     {   first#(s(X), cons(Y, Z)) -> activate#(Z),
           activate#(n__terms(X)) -> activate#(X),
               activate#(n__s(X)) -> activate#(X),
      activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)),
      activate#(n__first(X1, X2)) -> activate#(X1),
      activate#(n__first(X1, X2)) -> activate#(X2)}
    Scc:
     {dbl#(s(X)) -> dbl#(X)}
    Scc:
     {add#(s(X), Y) -> add#(X, Y)}
    Scc:
     {sqr#(s(X)) -> sqr#(X)}
    SCC:
     Strict:
      {   first#(s(X), cons(Y, Z)) -> activate#(Z),
            activate#(n__terms(X)) -> activate#(X),
                activate#(n__s(X)) -> activate#(X),
       activate#(n__first(X1, X2)) -> first#(activate(X1), activate(X2)),
       activate#(n__first(X1, X2)) -> activate#(X1),
       activate#(n__first(X1, X2)) -> activate#(X2)}
     Weak:
     {                  sqr(0()) -> 0(),
                       sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                        terms(N) -> cons(recip(sqr(N)), n__terms(n__s(N))),
                        terms(X) -> n__terms(X),
                            s(X) -> n__s(X),
                     add(0(), X) -> X,
                    add(s(X), Y) -> s(add(X, Y)),
                        dbl(0()) -> 0(),
                       dbl(s(X)) -> s(s(dbl(X))),
                   first(X1, X2) -> n__first(X1, X2),
                   first(0(), X) -> nil(),
         first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
                     activate(X) -> X,
           activate(n__terms(X)) -> terms(activate(X)),
               activate(n__s(X)) -> s(activate(X)),
      activate(n__first(X1, X2)) -> first(activate(X1), activate(X2))}
     POLY:
      Argument Filtering:
       pi(activate#) = 0, pi(activate) = 0, pi(n__first) = [0,1], pi(first#) = 1, pi(first) = [0,1], pi(nil) = [], pi(dbl) = [], pi(add) = [], pi(s) = 0, pi(0) = [], pi(terms) = 0, pi(n__s) = 0, pi(n__terms) = 0, pi(sqr) = [], pi(recip) = [], pi(cons) = 1
      Usable Rules:
       {}
      Interpretation:
       [n__first](x0, x1) = x0 + x1 + 1
      Strict:
       {first#(s(X), cons(Y, Z)) -> activate#(Z),
          activate#(n__terms(X)) -> activate#(X),
              activate#(n__s(X)) -> activate#(X)}
      Weak:
       {                  sqr(0()) -> 0(),
                         sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                          terms(N) -> cons(recip(sqr(N)), n__terms(n__s(N))),
                          terms(X) -> n__terms(X),
                              s(X) -> n__s(X),
                       add(0(), X) -> X,
                      add(s(X), Y) -> s(add(X, Y)),
                          dbl(0()) -> 0(),
                         dbl(s(X)) -> s(s(dbl(X))),
                     first(X1, X2) -> n__first(X1, X2),
                     first(0(), X) -> nil(),
           first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
                       activate(X) -> X,
             activate(n__terms(X)) -> terms(activate(X)),
                 activate(n__s(X)) -> s(activate(X)),
        activate(n__first(X1, X2)) -> first(activate(X1), activate(X2))}
      EDG:
       {(activate#(n__terms(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
        (activate#(n__terms(X)) -> activate#(X), activate#(n__terms(X)) -> activate#(X))
        (activate#(n__s(X)) -> activate#(X), activate#(n__terms(X)) -> activate#(X))
        (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
        (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__terms(X)) -> activate#(X))
        (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__s(X)) -> activate#(X))}
       SCCS:
        Scc:
         {activate#(n__terms(X)) -> activate#(X),
              activate#(n__s(X)) -> activate#(X)}
        SCC:
         Strict:
          {activate#(n__terms(X)) -> activate#(X),
               activate#(n__s(X)) -> activate#(X)}
         Weak:
         {                  sqr(0()) -> 0(),
                           sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                            terms(N) -> cons(recip(sqr(N)), n__terms(n__s(N))),
                            terms(X) -> n__terms(X),
                                s(X) -> n__s(X),
                         add(0(), X) -> X,
                        add(s(X), Y) -> s(add(X, Y)),
                            dbl(0()) -> 0(),
                           dbl(s(X)) -> s(s(dbl(X))),
                       first(X1, X2) -> n__first(X1, X2),
                       first(0(), X) -> nil(),
             first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
                         activate(X) -> X,
               activate(n__terms(X)) -> terms(activate(X)),
                   activate(n__s(X)) -> s(activate(X)),
          activate(n__first(X1, X2)) -> first(activate(X1), activate(X2))}
         SPSC:
          Simple Projection:
           pi(activate#) = 0
          Strict:
           {activate#(n__s(X)) -> activate#(X)}
          EDG:
           {(activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))}
           SCCS:
            Scc:
             {activate#(n__s(X)) -> activate#(X)}
            SCC:
             Strict:
              {activate#(n__s(X)) -> activate#(X)}
             Weak:
             {                  sqr(0()) -> 0(),
                               sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                                terms(N) -> cons(recip(sqr(N)), n__terms(n__s(N))),
                                terms(X) -> n__terms(X),
                                    s(X) -> n__s(X),
                             add(0(), X) -> X,
                            add(s(X), Y) -> s(add(X, Y)),
                                dbl(0()) -> 0(),
                               dbl(s(X)) -> s(s(dbl(X))),
                           first(X1, X2) -> n__first(X1, X2),
                           first(0(), X) -> nil(),
                 first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
                             activate(X) -> X,
                   activate(n__terms(X)) -> terms(activate(X)),
                       activate(n__s(X)) -> s(activate(X)),
              activate(n__first(X1, X2)) -> first(activate(X1), activate(X2))}
             SPSC:
              Simple Projection:
               pi(activate#) = 0
              Strict:
               {}
              Qed
    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)), n__terms(n__s(N))),
                        terms(X) -> n__terms(X),
                            s(X) -> n__s(X),
                     add(0(), X) -> X,
                    add(s(X), Y) -> s(add(X, Y)),
                        dbl(0()) -> 0(),
                       dbl(s(X)) -> s(s(dbl(X))),
                   first(X1, X2) -> n__first(X1, X2),
                   first(0(), X) -> nil(),
         first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
                     activate(X) -> X,
           activate(n__terms(X)) -> terms(activate(X)),
               activate(n__s(X)) -> s(activate(X)),
      activate(n__first(X1, X2)) -> first(activate(X1), activate(X2))}
     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)), n__terms(n__s(N))),
                        terms(X) -> n__terms(X),
                            s(X) -> n__s(X),
                     add(0(), X) -> X,
                    add(s(X), Y) -> s(add(X, Y)),
                        dbl(0()) -> 0(),
                       dbl(s(X)) -> s(s(dbl(X))),
                   first(X1, X2) -> n__first(X1, X2),
                   first(0(), X) -> nil(),
         first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
                     activate(X) -> X,
           activate(n__terms(X)) -> terms(activate(X)),
               activate(n__s(X)) -> s(activate(X)),
      activate(n__first(X1, X2)) -> first(activate(X1), activate(X2))}
     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)), n__terms(n__s(N))),
                        terms(X) -> n__terms(X),
                            s(X) -> n__s(X),
                     add(0(), X) -> X,
                    add(s(X), Y) -> s(add(X, Y)),
                        dbl(0()) -> 0(),
                       dbl(s(X)) -> s(s(dbl(X))),
                   first(X1, X2) -> n__first(X1, X2),
                   first(0(), X) -> nil(),
         first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
                     activate(X) -> X,
           activate(n__terms(X)) -> terms(activate(X)),
               activate(n__s(X)) -> s(activate(X)),
      activate(n__first(X1, X2)) -> first(activate(X1), activate(X2))}
     SPSC:
      Simple Projection:
       pi(sqr#) = 0
      Strict:
       {}
      Qed