MAYBE
MAYBE
TRS:
 {
              mark(adx(X)) -> active(adx(mark(X))),
             mark(zeros()) -> active(zeros()),
              mark(nats()) -> active(nats()),
        mark(cons(X1, X2)) -> active(cons(X1, X2)),
                 mark(0()) -> active(0()),
                mark(s(X)) -> active(s(X)),
             mark(incr(X)) -> active(incr(mark(X))),
               mark(hd(X)) -> active(hd(mark(X))),
               mark(tl(X)) -> active(tl(mark(X))),
              adx(mark(X)) -> adx(X),
            adx(active(X)) -> adx(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(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
    active(hd(cons(X, Y))) -> mark(X),
    active(tl(cons(X, Y))) -> mark(Y),
        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),
                s(mark(X)) -> s(X),
              s(active(X)) -> s(X),
             incr(mark(X)) -> incr(X),
           incr(active(X)) -> incr(X),
               hd(mark(X)) -> hd(X),
             hd(active(X)) -> hd(X),
               tl(mark(X)) -> tl(X),
             tl(active(X)) -> tl(X)
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
                mark(adx(X)) -> active(adx(mark(X))),
               mark(zeros()) -> active(zeros()),
                mark(nats()) -> active(nats()),
          mark(cons(X1, X2)) -> active(cons(X1, X2)),
                   mark(0()) -> active(0()),
                  mark(s(X)) -> active(s(X)),
               mark(incr(X)) -> active(incr(mark(X))),
                 mark(hd(X)) -> active(hd(mark(X))),
                 mark(tl(X)) -> active(tl(mark(X))),
                adx(mark(X)) -> adx(X),
              adx(active(X)) -> adx(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(cons(X, Y))) -> mark(cons(s(X), incr(Y))),
      active(hd(cons(X, Y))) -> mark(X),
      active(tl(cons(X, Y))) -> mark(Y),
          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),
                  s(mark(X)) -> s(X),
                s(active(X)) -> s(X),
               incr(mark(X)) -> incr(X),
             incr(active(X)) -> incr(X),
                 hd(mark(X)) -> hd(X),
               hd(active(X)) -> hd(X),
                 tl(mark(X)) -> tl(X),
               tl(active(X)) -> tl(X)
   }
  Fail