MAYBE
MAYBE
TRS:
 {
               incr(X) -> n__incr(X),
           incr(nil()) -> nil(),
      incr(cons(X, L)) -> cons(s(X), n__incr(activate(L))),
           activate(X) -> X,
  activate(n__incr(X)) -> incr(X),
   activate(n__adx(X)) -> adx(X),
  activate(n__zeros()) -> zeros(),
                adx(X) -> n__adx(X),
            adx(nil()) -> nil(),
       adx(cons(X, L)) -> incr(cons(X, n__adx(activate(L)))),
               zeros() -> cons(0(), n__zeros()),
               zeros() -> n__zeros(),
                nats() -> adx(zeros()),
      head(cons(X, L)) -> X,
      tail(cons(X, L)) -> activate(L)
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
                 incr(X) -> n__incr(X),
             incr(nil()) -> nil(),
        incr(cons(X, L)) -> cons(s(X), n__incr(activate(L))),
             activate(X) -> X,
    activate(n__incr(X)) -> incr(X),
     activate(n__adx(X)) -> adx(X),
    activate(n__zeros()) -> zeros(),
                  adx(X) -> n__adx(X),
              adx(nil()) -> nil(),
         adx(cons(X, L)) -> incr(cons(X, n__adx(activate(L)))),
                 zeros() -> cons(0(), n__zeros()),
                 zeros() -> n__zeros(),
                  nats() -> adx(zeros()),
        head(cons(X, L)) -> X,
        tail(cons(X, L)) -> activate(L)
   }
  Fail