MAYBE
MAYBE
TRS:
 {
               mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                   mark(recip(X)) -> active(recip(mark(X))),
                     mark(sqr(X)) -> active(sqr(mark(X))),
                   mark(terms(X)) -> active(terms(mark(X))),
                       mark(s(X)) -> active(s(X)),
                        mark(0()) -> active(0()),
                mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                     mark(dbl(X)) -> active(dbl(mark(X))),
                      mark(nil()) -> active(nil()),
              mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
               cons(X1, mark(X2)) -> cons(X1, X2),
             cons(X1, active(X2)) -> cons(X1, X2),
               cons(mark(X1), X2) -> cons(X1, X2),
             cons(active(X1), X2) -> cons(X1, X2),
                   recip(mark(X)) -> recip(X),
                 recip(active(X)) -> recip(X),
                     sqr(mark(X)) -> sqr(X),
                   sqr(active(X)) -> sqr(X),
                   terms(mark(X)) -> terms(X),
                 terms(active(X)) -> terms(X),
                       s(mark(X)) -> s(X),
                     s(active(X)) -> s(X),
                active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))),
                 active(sqr(0())) -> mark(0()),
                 active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))),
             active(add(s(X), Y)) -> mark(s(add(X, Y))),
              active(add(0(), X)) -> mark(X),
                active(dbl(s(X))) -> mark(s(s(dbl(X)))),
                 active(dbl(0())) -> mark(0()),
  active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
            active(first(0(), X)) -> mark(nil()),
                add(X1, mark(X2)) -> add(X1, X2),
              add(X1, active(X2)) -> add(X1, X2),
                add(mark(X1), X2) -> add(X1, X2),
              add(active(X1), X2) -> add(X1, X2),
                     dbl(mark(X)) -> dbl(X),
                   dbl(active(X)) -> dbl(X),
              first(X1, mark(X2)) -> first(X1, X2),
            first(X1, active(X2)) -> first(X1, X2),
              first(mark(X1), X2) -> first(X1, X2),
            first(active(X1), X2) -> first(X1, X2)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                 mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                     mark(recip(X)) -> active(recip(mark(X))),
                       mark(sqr(X)) -> active(sqr(mark(X))),
                     mark(terms(X)) -> active(terms(mark(X))),
                         mark(s(X)) -> active(s(X)),
                          mark(0()) -> active(0()),
                  mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                       mark(dbl(X)) -> active(dbl(mark(X))),
                        mark(nil()) -> active(nil()),
                mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                 cons(X1, mark(X2)) -> cons(X1, X2),
               cons(X1, active(X2)) -> cons(X1, X2),
                 cons(mark(X1), X2) -> cons(X1, X2),
               cons(active(X1), X2) -> cons(X1, X2),
                     recip(mark(X)) -> recip(X),
                   recip(active(X)) -> recip(X),
                       sqr(mark(X)) -> sqr(X),
                     sqr(active(X)) -> sqr(X),
                     terms(mark(X)) -> terms(X),
                   terms(active(X)) -> terms(X),
                         s(mark(X)) -> s(X),
                       s(active(X)) -> s(X),
                  active(sqr(s(X))) -> mark(s(add(sqr(X), dbl(X)))),
                   active(sqr(0())) -> mark(0()),
                   active(terms(N)) -> mark(cons(recip(sqr(N)), terms(s(N)))),
               active(add(s(X), Y)) -> mark(s(add(X, Y))),
                active(add(0(), X)) -> mark(X),
                  active(dbl(s(X))) -> mark(s(s(dbl(X)))),
                   active(dbl(0())) -> mark(0()),
    active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
              active(first(0(), X)) -> mark(nil()),
                  add(X1, mark(X2)) -> add(X1, X2),
                add(X1, active(X2)) -> add(X1, X2),
                  add(mark(X1), X2) -> add(X1, X2),
                add(active(X1), X2) -> add(X1, X2),
                       dbl(mark(X)) -> dbl(X),
                     dbl(active(X)) -> dbl(X),
                first(X1, mark(X2)) -> first(X1, X2),
              first(X1, active(X2)) -> first(X1, X2),
                first(mark(X1), X2) -> first(X1, X2),
              first(active(X1), X2) -> first(X1, X2)
   }
  Fail