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