MAYBE
TRS:
 {                 sqr(s(X)) -> s(n__add(sqr(activate(X)), dbl(activate(X)))),
                    sqr(0()) -> 0(),
                        s(X) -> n__s(X),
                    terms(N) -> cons(recip(sqr(N)), n__terms(s(N))),
                    terms(X) -> n__terms(X),
                 activate(X) -> X,
       activate(n__terms(X)) -> terms(X),
    activate(n__add(X1, X2)) -> add(X1, X2),
           activate(n__s(X)) -> s(X),
         activate(n__dbl(X)) -> dbl(X),
  activate(n__first(X1, X2)) -> first(X1, X2),
                      dbl(X) -> n__dbl(X),
                   dbl(s(X)) -> s(n__s(n__dbl(activate(X)))),
                    dbl(0()) -> 0(),
                 add(X1, X2) -> n__add(X1, X2),
                add(s(X), Y) -> s(n__add(activate(X), Y)),
                 add(0(), X) -> X,
               first(X1, X2) -> n__first(X1, X2),
     first(s(X), cons(Y, Z)) -> cons(Y, n__first(activate(X), activate(Z))),
               first(0(), X) -> nil()}
 DP:
  Strict:
   {                 sqr#(s(X)) -> sqr#(activate(X)),
                     sqr#(s(X)) -> s#(n__add(sqr(activate(X)), dbl(activate(X)))),
                     sqr#(s(X)) -> activate#(X),
                     sqr#(s(X)) -> dbl#(activate(X)),
                      terms#(N) -> sqr#(N),
                      terms#(N) -> s#(N),
         activate#(n__terms(X)) -> terms#(X),
      activate#(n__add(X1, X2)) -> add#(X1, X2),
             activate#(n__s(X)) -> s#(X),
           activate#(n__dbl(X)) -> dbl#(X),
    activate#(n__first(X1, X2)) -> first#(X1, X2),
                     dbl#(s(X)) -> s#(n__s(n__dbl(activate(X)))),
                     dbl#(s(X)) -> activate#(X),
                  add#(s(X), Y) -> s#(n__add(activate(X), Y)),
                  add#(s(X), Y) -> activate#(X),
       first#(s(X), cons(Y, Z)) -> activate#(X),
       first#(s(X), cons(Y, Z)) -> activate#(Z)}
  Weak:
  {                 sqr(s(X)) -> s(n__add(sqr(activate(X)), dbl(activate(X)))),
                     sqr(0()) -> 0(),
                         s(X) -> n__s(X),
                     terms(N) -> cons(recip(sqr(N)), n__terms(s(N))),
                     terms(X) -> n__terms(X),
                  activate(X) -> X,
        activate(n__terms(X)) -> terms(X),
     activate(n__add(X1, X2)) -> add(X1, X2),
            activate(n__s(X)) -> s(X),
          activate(n__dbl(X)) -> dbl(X),
   activate(n__first(X1, X2)) -> first(X1, X2),
                       dbl(X) -> n__dbl(X),
                    dbl(s(X)) -> s(n__s(n__dbl(activate(X)))),
                     dbl(0()) -> 0(),
                  add(X1, X2) -> n__add(X1, X2),
                 add(s(X), Y) -> s(n__add(activate(X), Y)),
                  add(0(), X) -> X,
                first(X1, X2) -> n__first(X1, X2),
      first(s(X), cons(Y, Z)) -> cons(Y, n__first(activate(X), activate(Z))),
                first(0(), X) -> nil()}
  EDG:
   {(activate#(n__first(X1, X2)) -> first#(X1, X2), first#(s(X), cons(Y, Z)) -> activate#(Z))
    (activate#(n__first(X1, X2)) -> first#(X1, X2), first#(s(X), cons(Y, Z)) -> activate#(X))
    (sqr#(s(X)) -> dbl#(activate(X)), dbl#(s(X)) -> activate#(X))
    (sqr#(s(X)) -> dbl#(activate(X)), dbl#(s(X)) -> s#(n__s(n__dbl(activate(X)))))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__first(X1, X2)) -> first#(X1, X2))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__dbl(X)) -> dbl#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__s(X)) -> s#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__terms(X)) -> terms#(X))
    (activate#(n__terms(X)) -> terms#(X), terms#(N) -> s#(N))
    (activate#(n__terms(X)) -> terms#(X), terms#(N) -> sqr#(N))
    (activate#(n__dbl(X)) -> dbl#(X), dbl#(s(X)) -> activate#(X))
    (activate#(n__dbl(X)) -> dbl#(X), dbl#(s(X)) -> s#(n__s(n__dbl(activate(X)))))
    (add#(s(X), Y) -> activate#(X), activate#(n__first(X1, X2)) -> first#(X1, X2))
    (add#(s(X), Y) -> activate#(X), activate#(n__dbl(X)) -> dbl#(X))
    (add#(s(X), Y) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (add#(s(X), Y) -> activate#(X), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (add#(s(X), Y) -> activate#(X), activate#(n__terms(X)) -> terms#(X))
    (terms#(N) -> sqr#(N), sqr#(s(X)) -> dbl#(activate(X)))
    (terms#(N) -> sqr#(N), sqr#(s(X)) -> activate#(X))
    (terms#(N) -> sqr#(N), sqr#(s(X)) -> s#(n__add(sqr(activate(X)), dbl(activate(X)))))
    (terms#(N) -> sqr#(N), sqr#(s(X)) -> sqr#(activate(X)))
    (first#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__terms(X)) -> terms#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (first#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__dbl(X)) -> dbl#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__first(X1, X2)) -> first#(X1, X2))
    (dbl#(s(X)) -> activate#(X), activate#(n__terms(X)) -> terms#(X))
    (dbl#(s(X)) -> activate#(X), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (dbl#(s(X)) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (dbl#(s(X)) -> activate#(X), activate#(n__dbl(X)) -> dbl#(X))
    (dbl#(s(X)) -> activate#(X), activate#(n__first(X1, X2)) -> first#(X1, X2))
    (sqr#(s(X)) -> activate#(X), activate#(n__terms(X)) -> terms#(X))
    (sqr#(s(X)) -> activate#(X), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (sqr#(s(X)) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (sqr#(s(X)) -> activate#(X), activate#(n__dbl(X)) -> dbl#(X))
    (sqr#(s(X)) -> activate#(X), activate#(n__first(X1, X2)) -> first#(X1, X2))
    (sqr#(s(X)) -> sqr#(activate(X)), sqr#(s(X)) -> sqr#(activate(X)))
    (sqr#(s(X)) -> sqr#(activate(X)), sqr#(s(X)) -> s#(n__add(sqr(activate(X)), dbl(activate(X)))))
    (sqr#(s(X)) -> sqr#(activate(X)), sqr#(s(X)) -> activate#(X))
    (sqr#(s(X)) -> sqr#(activate(X)), sqr#(s(X)) -> dbl#(activate(X)))
    (activate#(n__add(X1, X2)) -> add#(X1, X2), add#(s(X), Y) -> s#(n__add(activate(X), Y)))
    (activate#(n__add(X1, X2)) -> add#(X1, X2), add#(s(X), Y) -> activate#(X))}
   SCCS:
    Scc:
     {                 sqr#(s(X)) -> sqr#(activate(X)),
                       sqr#(s(X)) -> activate#(X),
                       sqr#(s(X)) -> dbl#(activate(X)),
                        terms#(N) -> sqr#(N),
           activate#(n__terms(X)) -> terms#(X),
        activate#(n__add(X1, X2)) -> add#(X1, X2),
             activate#(n__dbl(X)) -> dbl#(X),
      activate#(n__first(X1, X2)) -> first#(X1, X2),
                       dbl#(s(X)) -> activate#(X),
                    add#(s(X), Y) -> activate#(X),
         first#(s(X), cons(Y, Z)) -> activate#(X),
         first#(s(X), cons(Y, Z)) -> activate#(Z)}
    SCC:
     Strict:
      {                 sqr#(s(X)) -> sqr#(activate(X)),
                        sqr#(s(X)) -> activate#(X),
                        sqr#(s(X)) -> dbl#(activate(X)),
                         terms#(N) -> sqr#(N),
            activate#(n__terms(X)) -> terms#(X),
         activate#(n__add(X1, X2)) -> add#(X1, X2),
              activate#(n__dbl(X)) -> dbl#(X),
       activate#(n__first(X1, X2)) -> first#(X1, X2),
                        dbl#(s(X)) -> activate#(X),
                     add#(s(X), Y) -> activate#(X),
          first#(s(X), cons(Y, Z)) -> activate#(X),
          first#(s(X), cons(Y, Z)) -> activate#(Z)}
     Weak:
     {                 sqr(s(X)) -> s(n__add(sqr(activate(X)), dbl(activate(X)))),
                        sqr(0()) -> 0(),
                            s(X) -> n__s(X),
                        terms(N) -> cons(recip(sqr(N)), n__terms(s(N))),
                        terms(X) -> n__terms(X),
                     activate(X) -> X,
           activate(n__terms(X)) -> terms(X),
        activate(n__add(X1, X2)) -> add(X1, X2),
               activate(n__s(X)) -> s(X),
             activate(n__dbl(X)) -> dbl(X),
      activate(n__first(X1, X2)) -> first(X1, X2),
                          dbl(X) -> n__dbl(X),
                       dbl(s(X)) -> s(n__s(n__dbl(activate(X)))),
                        dbl(0()) -> 0(),
                     add(X1, X2) -> n__add(X1, X2),
                    add(s(X), Y) -> s(n__add(activate(X), Y)),
                     add(0(), X) -> X,
                   first(X1, X2) -> n__first(X1, X2),
         first(s(X), cons(Y, Z)) -> cons(Y, n__first(activate(X), activate(Z))),
                   first(0(), X) -> nil()}
     POLY:
      Argument Filtering:
       pi(n__first) = [0,1], pi(first#) = [0,1], pi(first) = [0,1], pi(nil) = [], pi(add#) = [0], pi(add) = [0,1], pi(n__dbl) = 0, pi(n__s) = 0, pi(dbl#) = 0, pi(dbl) = 0, pi(activate#) = 0, pi(activate) = 0, pi(n__add) = [0,1], pi(0) = [], pi(terms#) = 0, pi(terms) = 0, pi(s) = 0, pi(n__terms) = 0, pi(sqr#) = 0, pi(sqr) = [], pi(recip) = [], pi(cons) = 1
      Usable Rules:
       {}
      Interpretation:
       [first#](x0, x1) = x0 + x1,
       [add#](x0) = x0 + 1,
       [n__first](x0, x1) = x0 + x1,
       [n__add](x0, x1) = x0 + x1 + 1
      Strict:
       {                 sqr#(s(X)) -> sqr#(activate(X)),
                         sqr#(s(X)) -> activate#(X),
                         sqr#(s(X)) -> dbl#(activate(X)),
                          terms#(N) -> sqr#(N),
             activate#(n__terms(X)) -> terms#(X),
          activate#(n__add(X1, X2)) -> add#(X1, X2),
               activate#(n__dbl(X)) -> dbl#(X),
        activate#(n__first(X1, X2)) -> first#(X1, X2),
                         dbl#(s(X)) -> activate#(X),
           first#(s(X), cons(Y, Z)) -> activate#(X),
           first#(s(X), cons(Y, Z)) -> activate#(Z)}
      Weak:
       {                 sqr(s(X)) -> s(n__add(sqr(activate(X)), dbl(activate(X)))),
                          sqr(0()) -> 0(),
                              s(X) -> n__s(X),
                          terms(N) -> cons(recip(sqr(N)), n__terms(s(N))),
                          terms(X) -> n__terms(X),
                       activate(X) -> X,
             activate(n__terms(X)) -> terms(X),
          activate(n__add(X1, X2)) -> add(X1, X2),
                 activate(n__s(X)) -> s(X),
               activate(n__dbl(X)) -> dbl(X),
        activate(n__first(X1, X2)) -> first(X1, X2),
                            dbl(X) -> n__dbl(X),
                         dbl(s(X)) -> s(n__s(n__dbl(activate(X)))),
                          dbl(0()) -> 0(),
                       add(X1, X2) -> n__add(X1, X2),
                      add(s(X), Y) -> s(n__add(activate(X), Y)),
                       add(0(), X) -> X,
                     first(X1, X2) -> n__first(X1, X2),
           first(s(X), cons(Y, Z)) -> cons(Y, n__first(activate(X), activate(Z))),
                     first(0(), X) -> nil()}
      EDG:
       {(sqr#(s(X)) -> activate#(X), activate#(n__first(X1, X2)) -> first#(X1, X2))
        (sqr#(s(X)) -> activate#(X), activate#(n__dbl(X)) -> dbl#(X))
        (sqr#(s(X)) -> activate#(X), activate#(n__add(X1, X2)) -> add#(X1, X2))
        (sqr#(s(X)) -> activate#(X), activate#(n__terms(X)) -> terms#(X))
        (activate#(n__dbl(X)) -> dbl#(X), dbl#(s(X)) -> activate#(X))
        (first#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__first(X1, X2)) -> first#(X1, X2))
        (first#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__dbl(X)) -> dbl#(X))
        (first#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__add(X1, X2)) -> add#(X1, X2))
        (first#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__terms(X)) -> terms#(X))
        (sqr#(s(X)) -> sqr#(activate(X)), sqr#(s(X)) -> dbl#(activate(X)))
        (sqr#(s(X)) -> sqr#(activate(X)), sqr#(s(X)) -> activate#(X))
        (sqr#(s(X)) -> sqr#(activate(X)), sqr#(s(X)) -> sqr#(activate(X)))
        (activate#(n__first(X1, X2)) -> first#(X1, X2), first#(s(X), cons(Y, Z)) -> activate#(X))
        (activate#(n__first(X1, X2)) -> first#(X1, X2), first#(s(X), cons(Y, Z)) -> activate#(Z))
        (sqr#(s(X)) -> dbl#(activate(X)), dbl#(s(X)) -> activate#(X))
        (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__terms(X)) -> terms#(X))
        (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__add(X1, X2)) -> add#(X1, X2))
        (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__dbl(X)) -> dbl#(X))
        (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__first(X1, X2)) -> first#(X1, X2))
        (dbl#(s(X)) -> activate#(X), activate#(n__terms(X)) -> terms#(X))
        (dbl#(s(X)) -> activate#(X), activate#(n__add(X1, X2)) -> add#(X1, X2))
        (dbl#(s(X)) -> activate#(X), activate#(n__dbl(X)) -> dbl#(X))
        (dbl#(s(X)) -> activate#(X), activate#(n__first(X1, X2)) -> first#(X1, X2))
        (activate#(n__terms(X)) -> terms#(X), terms#(N) -> sqr#(N))
        (terms#(N) -> sqr#(N), sqr#(s(X)) -> sqr#(activate(X)))
        (terms#(N) -> sqr#(N), sqr#(s(X)) -> activate#(X))
        (terms#(N) -> sqr#(N), sqr#(s(X)) -> dbl#(activate(X)))}
       SCCS:
        Scc:
         {                 sqr#(s(X)) -> sqr#(activate(X)),
                           sqr#(s(X)) -> activate#(X),
                           sqr#(s(X)) -> dbl#(activate(X)),
                            terms#(N) -> sqr#(N),
               activate#(n__terms(X)) -> terms#(X),
                 activate#(n__dbl(X)) -> dbl#(X),
          activate#(n__first(X1, X2)) -> first#(X1, X2),
                           dbl#(s(X)) -> activate#(X),
             first#(s(X), cons(Y, Z)) -> activate#(X),
             first#(s(X), cons(Y, Z)) -> activate#(Z)}
        SCC:
         Strict:
          {                 sqr#(s(X)) -> sqr#(activate(X)),
                            sqr#(s(X)) -> activate#(X),
                            sqr#(s(X)) -> dbl#(activate(X)),
                             terms#(N) -> sqr#(N),
                activate#(n__terms(X)) -> terms#(X),
                  activate#(n__dbl(X)) -> dbl#(X),
           activate#(n__first(X1, X2)) -> first#(X1, X2),
                            dbl#(s(X)) -> activate#(X),
              first#(s(X), cons(Y, Z)) -> activate#(X),
              first#(s(X), cons(Y, Z)) -> activate#(Z)}
         Weak:
         {                 sqr(s(X)) -> s(n__add(sqr(activate(X)), dbl(activate(X)))),
                            sqr(0()) -> 0(),
                                s(X) -> n__s(X),
                            terms(N) -> cons(recip(sqr(N)), n__terms(s(N))),
                            terms(X) -> n__terms(X),
                         activate(X) -> X,
               activate(n__terms(X)) -> terms(X),
            activate(n__add(X1, X2)) -> add(X1, X2),
                   activate(n__s(X)) -> s(X),
                 activate(n__dbl(X)) -> dbl(X),
          activate(n__first(X1, X2)) -> first(X1, X2),
                              dbl(X) -> n__dbl(X),
                           dbl(s(X)) -> s(n__s(n__dbl(activate(X)))),
                            dbl(0()) -> 0(),
                         add(X1, X2) -> n__add(X1, X2),
                        add(s(X), Y) -> s(n__add(activate(X), Y)),
                         add(0(), X) -> X,
                       first(X1, X2) -> n__first(X1, X2),
             first(s(X), cons(Y, Z)) -> cons(Y, n__first(activate(X), activate(Z))),
                       first(0(), X) -> nil()}
         POLY:
          Argument Filtering:
           pi(n__first) = [0,1], pi(first#) = [0,1], pi(first) = [0,1], pi(nil) = [], pi(add) = [1], pi(n__dbl) = 0, pi(n__s) = 0, pi(dbl#) = 0, pi(dbl) = [0], pi(activate#) = [0], pi(activate) = [0], pi(n__add) = 1, pi(0) = [], pi(terms#) = [0], pi(terms) = [0], pi(s) = [0], pi(n__terms) = 0, pi(sqr#) = 0, pi(sqr) = [], pi(recip) = [], pi(cons) = 1
          Usable Rules:
           {}
          Interpretation:
           [first#](x0, x1) = x0 + x1 + 1,
           [activate#](x0) = x0 + 1,
           [terms#](x0) = x0 + 1,
           [n__first](x0, x1) = x0 + x1,
           [activate](x0) = x0 + 1,
           [s](x0) = x0 + 1
          Strict:
           {                 sqr#(s(X)) -> sqr#(activate(X)),
                             sqr#(s(X)) -> activate#(X),
                             sqr#(s(X)) -> dbl#(activate(X)),
                 activate#(n__terms(X)) -> terms#(X),
            activate#(n__first(X1, X2)) -> first#(X1, X2),
                             dbl#(s(X)) -> activate#(X)}
          Weak:
           {                 sqr(s(X)) -> s(n__add(sqr(activate(X)), dbl(activate(X)))),
                              sqr(0()) -> 0(),
                                  s(X) -> n__s(X),
                              terms(N) -> cons(recip(sqr(N)), n__terms(s(N))),
                              terms(X) -> n__terms(X),
                           activate(X) -> X,
                 activate(n__terms(X)) -> terms(X),
              activate(n__add(X1, X2)) -> add(X1, X2),
                     activate(n__s(X)) -> s(X),
                   activate(n__dbl(X)) -> dbl(X),
            activate(n__first(X1, X2)) -> first(X1, X2),
                                dbl(X) -> n__dbl(X),
                             dbl(s(X)) -> s(n__s(n__dbl(activate(X)))),
                              dbl(0()) -> 0(),
                           add(X1, X2) -> n__add(X1, X2),
                          add(s(X), Y) -> s(n__add(activate(X), Y)),
                           add(0(), X) -> X,
                         first(X1, X2) -> n__first(X1, X2),
               first(s(X), cons(Y, Z)) -> cons(Y, n__first(activate(X), activate(Z))),
                         first(0(), X) -> nil()}
          EDG:
           {(sqr#(s(X)) -> sqr#(activate(X)), sqr#(s(X)) -> dbl#(activate(X)))
            (sqr#(s(X)) -> sqr#(activate(X)), sqr#(s(X)) -> activate#(X))
            (sqr#(s(X)) -> sqr#(activate(X)), sqr#(s(X)) -> sqr#(activate(X)))
            (sqr#(s(X)) -> dbl#(activate(X)), dbl#(s(X)) -> activate#(X))
            (dbl#(s(X)) -> activate#(X), activate#(n__terms(X)) -> terms#(X))
            (dbl#(s(X)) -> activate#(X), activate#(n__first(X1, X2)) -> first#(X1, X2))
            (sqr#(s(X)) -> activate#(X), activate#(n__terms(X)) -> terms#(X))
            (sqr#(s(X)) -> activate#(X), activate#(n__first(X1, X2)) -> first#(X1, X2))}
           SCCS:
            Scc:
             {sqr#(s(X)) -> sqr#(activate(X))}
            SCC:
             Strict:
              {sqr#(s(X)) -> sqr#(activate(X))}
             Weak:
             {                 sqr(s(X)) -> s(n__add(sqr(activate(X)), dbl(activate(X)))),
                                sqr(0()) -> 0(),
                                    s(X) -> n__s(X),
                                terms(N) -> cons(recip(sqr(N)), n__terms(s(N))),
                                terms(X) -> n__terms(X),
                             activate(X) -> X,
                   activate(n__terms(X)) -> terms(X),
                activate(n__add(X1, X2)) -> add(X1, X2),
                       activate(n__s(X)) -> s(X),
                     activate(n__dbl(X)) -> dbl(X),
              activate(n__first(X1, X2)) -> first(X1, X2),
                                  dbl(X) -> n__dbl(X),
                               dbl(s(X)) -> s(n__s(n__dbl(activate(X)))),
                                dbl(0()) -> 0(),
                             add(X1, X2) -> n__add(X1, X2),
                            add(s(X), Y) -> s(n__add(activate(X), Y)),
                             add(0(), X) -> X,
                           first(X1, X2) -> n__first(X1, X2),
                 first(s(X), cons(Y, Z)) -> cons(Y, n__first(activate(X), activate(Z))),
                           first(0(), X) -> nil()}
             Fail