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)}
 RUF:
  Strict:
   {              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(),
             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))),
                     0() -> n__0(),
                    s(X) -> n__s(X)}
  Weak:
   {}
  DP:
   Strict:
    {     adx#(cons(X, Y)) -> activate#(X),
          adx#(cons(X, Y)) -> activate#(Y),
          adx#(cons(X, Y)) -> incr#(cons(activate(X), n__adx(activate(Y)))),
         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#(cons(X, Y)) -> activate#(X),
         incr#(cons(X, Y)) -> activate#(Y)}
   Weak:
   {              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(),
             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))),
                     0() -> n__0(),
                    s(X) -> n__s(X)}
   EDG:
    {(activate#(n__adx(X)) -> adx#(X), adx#(cons(X, Y)) -> incr#(cons(activate(X), n__adx(activate(Y)))))
     (activate#(n__adx(X)) -> adx#(X), adx#(cons(X, Y)) -> activate#(Y))
     (activate#(n__adx(X)) -> adx#(X), adx#(cons(X, Y)) -> activate#(X))
     (adx#(cons(X, Y)) -> activate#(Y), activate#(n__adx(X)) -> adx#(X))
     (adx#(cons(X, Y)) -> activate#(Y), activate#(n__incr(X)) -> incr#(X))
     (adx#(cons(X, Y)) -> activate#(Y), activate#(n__s(X)) -> s#(X))
     (adx#(cons(X, Y)) -> activate#(Y), activate#(n__zeros()) -> zeros#())
     (adx#(cons(X, Y)) -> activate#(Y), activate#(n__0()) -> 0#())
     (adx#(cons(X, Y)) -> incr#(cons(activate(X), n__adx(activate(Y)))), incr#(cons(X, Y)) -> activate#(Y))
     (adx#(cons(X, Y)) -> incr#(cons(activate(X), n__adx(activate(Y)))), incr#(cons(X, Y)) -> activate#(X))
     (incr#(cons(X, Y)) -> activate#(Y), activate#(n__0()) -> 0#())
     (incr#(cons(X, Y)) -> activate#(Y), activate#(n__zeros()) -> zeros#())
     (incr#(cons(X, Y)) -> activate#(Y), activate#(n__s(X)) -> s#(X))
     (incr#(cons(X, Y)) -> activate#(Y), activate#(n__incr(X)) -> incr#(X))
     (incr#(cons(X, Y)) -> activate#(Y), activate#(n__adx(X)) -> adx#(X))
     (incr#(cons(X, Y)) -> activate#(X), activate#(n__0()) -> 0#())
     (incr#(cons(X, Y)) -> activate#(X), activate#(n__zeros()) -> zeros#())
     (incr#(cons(X, Y)) -> activate#(X), activate#(n__s(X)) -> s#(X))
     (incr#(cons(X, Y)) -> activate#(X), activate#(n__incr(X)) -> incr#(X))
     (incr#(cons(X, Y)) -> activate#(X), activate#(n__adx(X)) -> adx#(X))
     (activate#(n__incr(X)) -> incr#(X), incr#(cons(X, Y)) -> activate#(X))
     (activate#(n__incr(X)) -> incr#(X), incr#(cons(X, Y)) -> activate#(Y))
     (adx#(cons(X, Y)) -> activate#(X), activate#(n__0()) -> 0#())
     (adx#(cons(X, Y)) -> activate#(X), activate#(n__zeros()) -> zeros#())
     (adx#(cons(X, Y)) -> activate#(X), activate#(n__s(X)) -> s#(X))
     (adx#(cons(X, Y)) -> activate#(X), activate#(n__incr(X)) -> incr#(X))
     (adx#(cons(X, Y)) -> activate#(X), activate#(n__adx(X)) -> adx#(X))}
    SCCS:
     Scc:
      {     adx#(cons(X, Y)) -> activate#(X),
            adx#(cons(X, Y)) -> activate#(Y),
            adx#(cons(X, Y)) -> incr#(cons(activate(X), n__adx(activate(Y)))),
       activate#(n__incr(X)) -> incr#(X),
        activate#(n__adx(X)) -> adx#(X),
           incr#(cons(X, Y)) -> activate#(X),
           incr#(cons(X, Y)) -> activate#(Y)}
     SCC:
      Strict:
       {     adx#(cons(X, Y)) -> activate#(X),
             adx#(cons(X, Y)) -> activate#(Y),
             adx#(cons(X, Y)) -> incr#(cons(activate(X), n__adx(activate(Y)))),
        activate#(n__incr(X)) -> incr#(X),
         activate#(n__adx(X)) -> adx#(X),
            incr#(cons(X, Y)) -> activate#(X),
            incr#(cons(X, Y)) -> activate#(Y)}
      Weak:
      {              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(),
                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))),
                        0() -> n__0(),
                       s(X) -> n__s(X)}
      POLY:
       Argument Filtering:
        pi(s) = [], pi(0) = [], pi(n__adx) = [0], pi(incr#) = 0, pi(incr) = 0, pi(n__incr) = 0, pi(activate#) = 0, pi(activate) = 0, pi(n__s) = [], pi(n__zeros) = [], pi(n__0) = [], pi(cons) = [0,1], pi(zeros) = [], pi(adx#) = [0], pi(adx) = [0]
       Usable Rules:
        {}
       Interpretation:
        [adx#](x0) = x0 + 1,
        [cons](x0, x1) = x0 + x1,
        [n__adx](x0) = x0 + 1
       Strict:
        {     adx#(cons(X, Y)) -> incr#(cons(activate(X), n__adx(activate(Y)))),
         activate#(n__incr(X)) -> incr#(X),
          activate#(n__adx(X)) -> adx#(X),
             incr#(cons(X, Y)) -> activate#(X),
             incr#(cons(X, Y)) -> activate#(Y)}
       Weak:
        {              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(),
                  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))),
                          0() -> n__0(),
                         s(X) -> n__s(X)}
       EDG:
        {(activate#(n__adx(X)) -> adx#(X), adx#(cons(X, Y)) -> incr#(cons(activate(X), n__adx(activate(Y)))))
         (incr#(cons(X, Y)) -> activate#(Y), activate#(n__adx(X)) -> adx#(X))
         (incr#(cons(X, Y)) -> activate#(Y), activate#(n__incr(X)) -> incr#(X))
         (adx#(cons(X, Y)) -> incr#(cons(activate(X), n__adx(activate(Y)))), incr#(cons(X, Y)) -> activate#(X))
         (adx#(cons(X, Y)) -> incr#(cons(activate(X), n__adx(activate(Y)))), incr#(cons(X, Y)) -> activate#(Y))
         (incr#(cons(X, Y)) -> activate#(X), activate#(n__incr(X)) -> incr#(X))
         (incr#(cons(X, Y)) -> activate#(X), activate#(n__adx(X)) -> adx#(X))
         (activate#(n__incr(X)) -> incr#(X), incr#(cons(X, Y)) -> activate#(X))
         (activate#(n__incr(X)) -> incr#(X), incr#(cons(X, Y)) -> activate#(Y))}
        SCCS:
         Scc:
          {     adx#(cons(X, Y)) -> incr#(cons(activate(X), n__adx(activate(Y)))),
           activate#(n__incr(X)) -> incr#(X),
            activate#(n__adx(X)) -> adx#(X),
               incr#(cons(X, Y)) -> activate#(X),
               incr#(cons(X, Y)) -> activate#(Y)}
         SCC:
          Strict:
           {     adx#(cons(X, Y)) -> incr#(cons(activate(X), n__adx(activate(Y)))),
            activate#(n__incr(X)) -> incr#(X),
             activate#(n__adx(X)) -> adx#(X),
                incr#(cons(X, Y)) -> activate#(X),
                incr#(cons(X, Y)) -> activate#(Y)}
          Weak:
          {              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(),
                    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))),
                            0() -> n__0(),
                           s(X) -> n__s(X)}
          Fail