MAYBE
MAYBE
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
 }
 DUP: We consider a duplicating system.
  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
   }
  Fail