MAYBE
MAYBE
TRS:
 {
           active(incr(X)) -> incr(active(X)),
       active(incr(nil())) -> mark(nil()),
  active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
      active(cons(X1, X2)) -> cons(active(X1), X2),
              active(s(X)) -> s(active(X)),
            active(adx(X)) -> adx(active(X)),
        active(adx(nil())) -> mark(nil()),
   active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
           active(zeros()) -> mark(cons(0(), zeros())),
            active(nats()) -> mark(adx(zeros())),
           active(head(X)) -> head(active(X)),
  active(head(cons(X, L))) -> mark(X),
           active(tail(X)) -> tail(active(X)),
  active(tail(cons(X, L))) -> mark(L),
             incr(mark(X)) -> mark(incr(X)),
               incr(ok(X)) -> ok(incr(X)),
        cons(mark(X1), X2) -> mark(cons(X1, X2)),
      cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                s(mark(X)) -> mark(s(X)),
                  s(ok(X)) -> ok(s(X)),
              adx(mark(X)) -> mark(adx(X)),
                adx(ok(X)) -> ok(adx(X)),
             head(mark(X)) -> mark(head(X)),
               head(ok(X)) -> ok(head(X)),
             tail(mark(X)) -> mark(tail(X)),
               tail(ok(X)) -> ok(tail(X)),
             proper(nil()) -> ok(nil()),
           proper(incr(X)) -> incr(proper(X)),
      proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
              proper(s(X)) -> s(proper(X)),
            proper(adx(X)) -> adx(proper(X)),
           proper(zeros()) -> ok(zeros()),
            proper(nats()) -> ok(nats()),
               proper(0()) -> ok(0()),
           proper(head(X)) -> head(proper(X)),
           proper(tail(X)) -> tail(proper(X)),
              top(mark(X)) -> top(proper(X)),
                top(ok(X)) -> top(active(X))
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
             active(incr(X)) -> incr(active(X)),
         active(incr(nil())) -> mark(nil()),
    active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
        active(cons(X1, X2)) -> cons(active(X1), X2),
                active(s(X)) -> s(active(X)),
              active(adx(X)) -> adx(active(X)),
          active(adx(nil())) -> mark(nil()),
     active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
             active(zeros()) -> mark(cons(0(), zeros())),
              active(nats()) -> mark(adx(zeros())),
             active(head(X)) -> head(active(X)),
    active(head(cons(X, L))) -> mark(X),
             active(tail(X)) -> tail(active(X)),
    active(tail(cons(X, L))) -> mark(L),
               incr(mark(X)) -> mark(incr(X)),
                 incr(ok(X)) -> ok(incr(X)),
          cons(mark(X1), X2) -> mark(cons(X1, X2)),
        cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                  s(mark(X)) -> mark(s(X)),
                    s(ok(X)) -> ok(s(X)),
                adx(mark(X)) -> mark(adx(X)),
                  adx(ok(X)) -> ok(adx(X)),
               head(mark(X)) -> mark(head(X)),
                 head(ok(X)) -> ok(head(X)),
               tail(mark(X)) -> mark(tail(X)),
                 tail(ok(X)) -> ok(tail(X)),
               proper(nil()) -> ok(nil()),
             proper(incr(X)) -> incr(proper(X)),
        proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                proper(s(X)) -> s(proper(X)),
              proper(adx(X)) -> adx(proper(X)),
             proper(zeros()) -> ok(zeros()),
              proper(nats()) -> ok(nats()),
                 proper(0()) -> ok(0()),
             proper(head(X)) -> head(proper(X)),
             proper(tail(X)) -> tail(proper(X)),
                top(mark(X)) -> top(proper(X)),
                  top(ok(X)) -> top(active(X))
   }
  Fail