YES
TRS:
 {                 sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                    sqr(0()) -> 0(),
                    terms(N) -> cons(recip(sqr(N)), n__terms(s(N))),
                    terms(X) -> n__terms(X),
                add(s(X), Y) -> s(add(X, Y)),
                 add(0(), X) -> X,
                   dbl(s(X)) -> s(s(dbl(X))),
                    dbl(0()) -> 0(),
               first(X1, X2) -> n__first(X1, X2),
     first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
               first(0(), X) -> nil(),
                 activate(X) -> X,
       activate(n__terms(X)) -> terms(X),
  activate(n__first(X1, X2)) -> first(X1, X2),
               half(s(s(X))) -> s(half(X)),
                half(s(0())) -> 0(),
                   half(0()) -> 0(),
                half(dbl(X)) -> X}
 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),
       first#(s(X), cons(Y, Z)) -> activate#(Z),
         activate#(n__terms(X)) -> terms#(X),
    activate#(n__first(X1, X2)) -> first#(X1, X2),
                 half#(s(s(X))) -> half#(X)}
  Weak:
  {                 sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                     sqr(0()) -> 0(),
                     terms(N) -> cons(recip(sqr(N)), n__terms(s(N))),
                     terms(X) -> n__terms(X),
                 add(s(X), Y) -> s(add(X, Y)),
                  add(0(), X) -> X,
                    dbl(s(X)) -> s(s(dbl(X))),
                     dbl(0()) -> 0(),
                first(X1, X2) -> n__first(X1, X2),
      first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
                first(0(), X) -> nil(),
                  activate(X) -> X,
        activate(n__terms(X)) -> terms(X),
   activate(n__first(X1, X2)) -> first(X1, X2),
                half(s(s(X))) -> s(half(X)),
                 half(s(0())) -> 0(),
                    half(0()) -> 0(),
                 half(dbl(X)) -> X}
  EDG:
   {(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))
    (half#(s(s(X))) -> half#(X), half#(s(s(X))) -> half#(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))
    (activate#(n__first(X1, X2)) -> first#(X1, X2), first#(s(X), cons(Y, Z)) -> activate#(Z))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__terms(X)) -> terms#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__first(X1, X2)) -> first#(X1, X2))
    (activate#(n__terms(X)) -> terms#(X), terms#(N) -> sqr#(N))
    (sqr#(s(X)) -> dbl#(X), dbl#(s(X)) -> dbl#(X))
    (terms#(N) -> sqr#(N), sqr#(s(X)) -> sqr#(X))
    (terms#(N) -> sqr#(N), sqr#(s(X)) -> add#(sqr(X), dbl(X)))
    (terms#(N) -> sqr#(N), sqr#(s(X)) -> dbl#(X))}
   SCCS:
    Scc:
     {half#(s(s(X))) -> half#(X)}
    Scc:
     {   first#(s(X), cons(Y, Z)) -> activate#(Z),
      activate#(n__first(X1, X2)) -> first#(X1, X2)}
    Scc:
     {dbl#(s(X)) -> dbl#(X)}
    Scc:
     {add#(s(X), Y) -> add#(X, Y)}
    Scc:
     {sqr#(s(X)) -> sqr#(X)}
    SCC:
     Strict:
      {half#(s(s(X))) -> half#(X)}
     Weak:
     {                 sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                        sqr(0()) -> 0(),
                        terms(N) -> cons(recip(sqr(N)), n__terms(s(N))),
                        terms(X) -> n__terms(X),
                    add(s(X), Y) -> s(add(X, Y)),
                     add(0(), X) -> X,
                       dbl(s(X)) -> s(s(dbl(X))),
                        dbl(0()) -> 0(),
                   first(X1, X2) -> n__first(X1, X2),
         first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
                   first(0(), X) -> nil(),
                     activate(X) -> X,
           activate(n__terms(X)) -> terms(X),
      activate(n__first(X1, X2)) -> first(X1, X2),
                   half(s(s(X))) -> s(half(X)),
                    half(s(0())) -> 0(),
                       half(0()) -> 0(),
                    half(dbl(X)) -> X}
     SPSC:
      Simple Projection:
       pi(half#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {   first#(s(X), cons(Y, Z)) -> activate#(Z),
       activate#(n__first(X1, X2)) -> first#(X1, X2)}
     Weak:
     {                 sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                        sqr(0()) -> 0(),
                        terms(N) -> cons(recip(sqr(N)), n__terms(s(N))),
                        terms(X) -> n__terms(X),
                    add(s(X), Y) -> s(add(X, Y)),
                     add(0(), X) -> X,
                       dbl(s(X)) -> s(s(dbl(X))),
                        dbl(0()) -> 0(),
                   first(X1, X2) -> n__first(X1, X2),
         first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
                   first(0(), X) -> nil(),
                     activate(X) -> X,
           activate(n__terms(X)) -> terms(X),
      activate(n__first(X1, X2)) -> first(X1, X2),
                   half(s(s(X))) -> s(half(X)),
                    half(s(0())) -> 0(),
                       half(0()) -> 0(),
                    half(dbl(X)) -> X}
     SPSC:
      Simple Projection:
       pi(activate#) = 0, pi(first#) = 1
      Strict:
       {first#(s(X), cons(Y, Z)) -> activate#(Z)}
      EDG:
       {}
       SCCS:
        
        Qed
    SCC:
     Strict:
      {dbl#(s(X)) -> dbl#(X)}
     Weak:
     {                 sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                        sqr(0()) -> 0(),
                        terms(N) -> cons(recip(sqr(N)), n__terms(s(N))),
                        terms(X) -> n__terms(X),
                    add(s(X), Y) -> s(add(X, Y)),
                     add(0(), X) -> X,
                       dbl(s(X)) -> s(s(dbl(X))),
                        dbl(0()) -> 0(),
                   first(X1, X2) -> n__first(X1, X2),
         first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
                   first(0(), X) -> nil(),
                     activate(X) -> X,
           activate(n__terms(X)) -> terms(X),
      activate(n__first(X1, X2)) -> first(X1, X2),
                   half(s(s(X))) -> s(half(X)),
                    half(s(0())) -> 0(),
                       half(0()) -> 0(),
                    half(dbl(X)) -> X}
     SPSC:
      Simple Projection:
       pi(dbl#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {add#(s(X), Y) -> add#(X, Y)}
     Weak:
     {                 sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                        sqr(0()) -> 0(),
                        terms(N) -> cons(recip(sqr(N)), n__terms(s(N))),
                        terms(X) -> n__terms(X),
                    add(s(X), Y) -> s(add(X, Y)),
                     add(0(), X) -> X,
                       dbl(s(X)) -> s(s(dbl(X))),
                        dbl(0()) -> 0(),
                   first(X1, X2) -> n__first(X1, X2),
         first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
                   first(0(), X) -> nil(),
                     activate(X) -> X,
           activate(n__terms(X)) -> terms(X),
      activate(n__first(X1, X2)) -> first(X1, X2),
                   half(s(s(X))) -> s(half(X)),
                    half(s(0())) -> 0(),
                       half(0()) -> 0(),
                    half(dbl(X)) -> X}
     SPSC:
      Simple Projection:
       pi(add#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {sqr#(s(X)) -> sqr#(X)}
     Weak:
     {                 sqr(s(X)) -> s(add(sqr(X), dbl(X))),
                        sqr(0()) -> 0(),
                        terms(N) -> cons(recip(sqr(N)), n__terms(s(N))),
                        terms(X) -> n__terms(X),
                    add(s(X), Y) -> s(add(X, Y)),
                     add(0(), X) -> X,
                       dbl(s(X)) -> s(s(dbl(X))),
                        dbl(0()) -> 0(),
                   first(X1, X2) -> n__first(X1, X2),
         first(s(X), cons(Y, Z)) -> cons(Y, n__first(X, activate(Z))),
                   first(0(), X) -> nil(),
                     activate(X) -> X,
           activate(n__terms(X)) -> terms(X),
      activate(n__first(X1, X2)) -> first(X1, X2),
                   half(s(s(X))) -> s(half(X)),
                    half(s(0())) -> 0(),
                       half(0()) -> 0(),
                    half(dbl(X)) -> X}
     SPSC:
      Simple Projection:
       pi(sqr#) = 0
      Strict:
       {}
      Qed