MAYBE
MAYBE
TRS:
 {
                      sqr(X) -> n__sqr(X),
                    sqr(0()) -> 0(),
                   sqr(s(X)) ->
  s(n__add(n__sqr(activate(X)), n__dbl(activate(X)))),
                    terms(N) -> cons(recip(sqr(N)), n__terms(n__s(N))),
                    terms(X) -> n__terms(X),
                        s(X) -> n__s(X),
                 activate(X) -> X,
       activate(n__terms(X)) -> terms(activate(X)),
           activate(n__s(X)) -> s(X),
    activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)),
         activate(n__sqr(X)) -> sqr(activate(X)),
         activate(n__dbl(X)) -> dbl(activate(X)),
  activate(n__first(X1, X2)) -> first(activate(X1), activate(X2)),
                      dbl(X) -> n__dbl(X),
                    dbl(0()) -> 0(),
                   dbl(s(X)) -> s(n__s(n__dbl(activate(X)))),
                 add(X1, X2) -> n__add(X1, X2),
                 add(0(), X) -> X,
                add(s(X), Y) -> s(n__add(activate(X), Y)),
               first(X1, X2) -> n__first(X1, X2),
               first(0(), X) -> nil(),
     first(s(X), cons(Y, Z)) -> cons(Y, n__first(activate(X), activate(Z)))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                        sqr(X) -> n__sqr(X),
                      sqr(0()) -> 0(),
                     sqr(s(X)) ->
    s(n__add(n__sqr(activate(X)), n__dbl(activate(X)))),
                      terms(N) -> cons(recip(sqr(N)), n__terms(n__s(N))),
                      terms(X) -> n__terms(X),
                          s(X) -> n__s(X),
                   activate(X) -> X,
         activate(n__terms(X)) -> terms(activate(X)),
             activate(n__s(X)) -> s(X),
      activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)),
           activate(n__sqr(X)) -> sqr(activate(X)),
           activate(n__dbl(X)) -> dbl(activate(X)),
    activate(n__first(X1, X2)) -> first(activate(X1), activate(X2)),
                        dbl(X) -> n__dbl(X),
                      dbl(0()) -> 0(),
                     dbl(s(X)) -> s(n__s(n__dbl(activate(X)))),
                   add(X1, X2) -> n__add(X1, X2),
                   add(0(), X) -> X,
                  add(s(X), Y) -> s(n__add(activate(X), Y)),
                 first(X1, X2) -> n__first(X1, X2),
                 first(0(), X) -> nil(),
       first(s(X), cons(Y, Z)) -> cons(Y, n__first(activate(X), activate(Z)))
   }
  Fail