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