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