MAYBE
MAYBE
TRS:
 {
                adx(X) -> n__adx(X),
       adx(cons(X, Y)) -> incr(cons(activate(X), n__adx(activate(Y)))),
               zeros() -> cons(n__0(), n__zeros()),
               zeros() -> n__zeros(),
                nats() -> adx(zeros()),
           activate(X) -> X,
      activate(n__0()) -> 0(),
  activate(n__zeros()) -> zeros(),
     activate(n__s(X)) -> s(X),
  activate(n__incr(X)) -> incr(X),
   activate(n__adx(X)) -> adx(X),
               incr(X) -> n__incr(X),
      incr(cons(X, Y)) -> cons(n__s(activate(X)), n__incr(activate(Y))),
        hd(cons(X, Y)) -> activate(X),
        tl(cons(X, Y)) -> activate(Y),
                   0() -> n__0(),
                  s(X) -> n__s(X)
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
                  adx(X) -> n__adx(X),
         adx(cons(X, Y)) -> incr(cons(activate(X), n__adx(activate(Y)))),
                 zeros() -> cons(n__0(), n__zeros()),
                 zeros() -> n__zeros(),
                  nats() -> adx(zeros()),
             activate(X) -> X,
        activate(n__0()) -> 0(),
    activate(n__zeros()) -> zeros(),
       activate(n__s(X)) -> s(X),
    activate(n__incr(X)) -> incr(X),
     activate(n__adx(X)) -> adx(X),
                 incr(X) -> n__incr(X),
        incr(cons(X, Y)) -> cons(n__s(activate(X)), n__incr(activate(Y))),
          hd(cons(X, Y)) -> activate(X),
          tl(cons(X, Y)) -> activate(Y),
                     0() -> n__0(),
                    s(X) -> n__s(X)
   }
  Fail