MAYBE
MAYBE
TRS:
 {
            a__adx(X) -> adx(X),
   a__adx(cons(X, Y)) -> a__incr(cons(X, adx(Y))),
           a__zeros() -> cons(0(), zeros()),
           a__zeros() -> zeros(),
            a__nats() -> a__adx(a__zeros()),
            a__nats() -> nats(),
           a__incr(X) -> incr(X),
  a__incr(cons(X, Y)) -> cons(s(X), incr(Y)),
   mark(cons(X1, X2)) -> cons(X1, X2),
            mark(0()) -> 0(),
        mark(zeros()) -> a__zeros(),
           mark(s(X)) -> s(X),
        mark(incr(X)) -> a__incr(mark(X)),
         mark(adx(X)) -> a__adx(mark(X)),
         mark(nats()) -> a__nats(),
          mark(hd(X)) -> a__hd(mark(X)),
          mark(tl(X)) -> a__tl(mark(X)),
             a__hd(X) -> hd(X),
    a__hd(cons(X, Y)) -> mark(X),
             a__tl(X) -> tl(X),
    a__tl(cons(X, Y)) -> mark(Y)
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
              a__adx(X) -> adx(X),
     a__adx(cons(X, Y)) -> a__incr(cons(X, adx(Y))),
             a__zeros() -> cons(0(), zeros()),
             a__zeros() -> zeros(),
              a__nats() -> a__adx(a__zeros()),
              a__nats() -> nats(),
             a__incr(X) -> incr(X),
    a__incr(cons(X, Y)) -> cons(s(X), incr(Y)),
     mark(cons(X1, X2)) -> cons(X1, X2),
              mark(0()) -> 0(),
          mark(zeros()) -> a__zeros(),
             mark(s(X)) -> s(X),
          mark(incr(X)) -> a__incr(mark(X)),
           mark(adx(X)) -> a__adx(mark(X)),
           mark(nats()) -> a__nats(),
            mark(hd(X)) -> a__hd(mark(X)),
            mark(tl(X)) -> a__tl(mark(X)),
               a__hd(X) -> hd(X),
      a__hd(cons(X, Y)) -> mark(X),
               a__tl(X) -> tl(X),
      a__tl(cons(X, Y)) -> mark(Y)
   }
  Fail