YES
TRS:
 {          a__adx(X) -> adx(X),
   a__adx(cons(X, Y)) -> a__incr(cons(X, adx(Y))),
           a__zeros() -> cons(0(), zeros()),
           a__zeros() -> zeros(),
            a__nats() -> a__adx(a__zeros()),
            a__nats() -> nats(),
           a__incr(X) -> incr(X),
  a__incr(cons(X, Y)) -> cons(s(X), incr(Y)),
   mark(cons(X1, X2)) -> cons(X1, X2),
            mark(0()) -> 0(),
        mark(zeros()) -> a__zeros(),
           mark(s(X)) -> s(X),
        mark(incr(X)) -> a__incr(mark(X)),
         mark(adx(X)) -> a__adx(mark(X)),
         mark(nats()) -> a__nats(),
          mark(hd(X)) -> a__hd(mark(X)),
          mark(tl(X)) -> a__tl(mark(X)),
             a__hd(X) -> hd(X),
    a__hd(cons(X, Y)) -> mark(X),
             a__tl(X) -> tl(X),
    a__tl(cons(X, Y)) -> mark(Y)}
 DP:
  Strict:
   {a__adx#(cons(X, Y)) -> a__incr#(cons(X, adx(Y))),
             a__nats#() -> a__adx#(a__zeros()),
             a__nats#() -> a__zeros#(),
         mark#(zeros()) -> a__zeros#(),
         mark#(incr(X)) -> a__incr#(mark(X)),
         mark#(incr(X)) -> mark#(X),
          mark#(adx(X)) -> a__adx#(mark(X)),
          mark#(adx(X)) -> mark#(X),
          mark#(nats()) -> a__nats#(),
           mark#(hd(X)) -> mark#(X),
           mark#(hd(X)) -> a__hd#(mark(X)),
           mark#(tl(X)) -> mark#(X),
           mark#(tl(X)) -> a__tl#(mark(X)),
     a__hd#(cons(X, Y)) -> mark#(X),
     a__tl#(cons(X, Y)) -> mark#(Y)}
  Weak:
  {          a__adx(X) -> adx(X),
    a__adx(cons(X, Y)) -> a__incr(cons(X, adx(Y))),
            a__zeros() -> cons(0(), zeros()),
            a__zeros() -> zeros(),
             a__nats() -> a__adx(a__zeros()),
             a__nats() -> nats(),
            a__incr(X) -> incr(X),
   a__incr(cons(X, Y)) -> cons(s(X), incr(Y)),
    mark(cons(X1, X2)) -> cons(X1, X2),
             mark(0()) -> 0(),
         mark(zeros()) -> a__zeros(),
            mark(s(X)) -> s(X),
         mark(incr(X)) -> a__incr(mark(X)),
          mark(adx(X)) -> a__adx(mark(X)),
          mark(nats()) -> a__nats(),
           mark(hd(X)) -> a__hd(mark(X)),
           mark(tl(X)) -> a__tl(mark(X)),
              a__hd(X) -> hd(X),
     a__hd(cons(X, Y)) -> mark(X),
              a__tl(X) -> tl(X),
     a__tl(cons(X, Y)) -> mark(Y)}
  EDG:
   {(mark#(adx(X)) -> mark#(X), mark#(tl(X)) -> a__tl#(mark(X)))
    (mark#(adx(X)) -> mark#(X), mark#(tl(X)) -> mark#(X))
    (mark#(adx(X)) -> mark#(X), mark#(hd(X)) -> a__hd#(mark(X)))
    (mark#(adx(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
    (mark#(adx(X)) -> mark#(X), mark#(nats()) -> a__nats#())
    (mark#(adx(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
    (mark#(adx(X)) -> mark#(X), mark#(adx(X)) -> a__adx#(mark(X)))
    (mark#(adx(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
    (mark#(adx(X)) -> mark#(X), mark#(incr(X)) -> a__incr#(mark(X)))
    (mark#(adx(X)) -> mark#(X), mark#(zeros()) -> a__zeros#())
    (mark#(tl(X)) -> mark#(X), mark#(tl(X)) -> a__tl#(mark(X)))
    (mark#(tl(X)) -> mark#(X), mark#(tl(X)) -> mark#(X))
    (mark#(tl(X)) -> mark#(X), mark#(hd(X)) -> a__hd#(mark(X)))
    (mark#(tl(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
    (mark#(tl(X)) -> mark#(X), mark#(nats()) -> a__nats#())
    (mark#(tl(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
    (mark#(tl(X)) -> mark#(X), mark#(adx(X)) -> a__adx#(mark(X)))
    (mark#(tl(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
    (mark#(tl(X)) -> mark#(X), mark#(incr(X)) -> a__incr#(mark(X)))
    (mark#(tl(X)) -> mark#(X), mark#(zeros()) -> a__zeros#())
    (a__nats#() -> a__adx#(a__zeros()), a__adx#(cons(X, Y)) -> a__incr#(cons(X, adx(Y))))
    (mark#(adx(X)) -> a__adx#(mark(X)), a__adx#(cons(X, Y)) -> a__incr#(cons(X, adx(Y))))
    (mark#(tl(X)) -> a__tl#(mark(X)), a__tl#(cons(X, Y)) -> mark#(Y))
    (mark#(nats()) -> a__nats#(), a__nats#() -> a__adx#(a__zeros()))
    (mark#(nats()) -> a__nats#(), a__nats#() -> a__zeros#())
    (a__tl#(cons(X, Y)) -> mark#(Y), mark#(zeros()) -> a__zeros#())
    (a__tl#(cons(X, Y)) -> mark#(Y), mark#(incr(X)) -> a__incr#(mark(X)))
    (a__tl#(cons(X, Y)) -> mark#(Y), mark#(incr(X)) -> mark#(X))
    (a__tl#(cons(X, Y)) -> mark#(Y), mark#(adx(X)) -> a__adx#(mark(X)))
    (a__tl#(cons(X, Y)) -> mark#(Y), mark#(adx(X)) -> mark#(X))
    (a__tl#(cons(X, Y)) -> mark#(Y), mark#(nats()) -> a__nats#())
    (a__tl#(cons(X, Y)) -> mark#(Y), mark#(hd(X)) -> mark#(X))
    (a__tl#(cons(X, Y)) -> mark#(Y), mark#(hd(X)) -> a__hd#(mark(X)))
    (a__tl#(cons(X, Y)) -> mark#(Y), mark#(tl(X)) -> mark#(X))
    (a__tl#(cons(X, Y)) -> mark#(Y), mark#(tl(X)) -> a__tl#(mark(X)))
    (mark#(hd(X)) -> a__hd#(mark(X)), a__hd#(cons(X, Y)) -> mark#(X))
    (a__hd#(cons(X, Y)) -> mark#(X), mark#(zeros()) -> a__zeros#())
    (a__hd#(cons(X, Y)) -> mark#(X), mark#(incr(X)) -> a__incr#(mark(X)))
    (a__hd#(cons(X, Y)) -> mark#(X), mark#(incr(X)) -> mark#(X))
    (a__hd#(cons(X, Y)) -> mark#(X), mark#(adx(X)) -> a__adx#(mark(X)))
    (a__hd#(cons(X, Y)) -> mark#(X), mark#(adx(X)) -> mark#(X))
    (a__hd#(cons(X, Y)) -> mark#(X), mark#(nats()) -> a__nats#())
    (a__hd#(cons(X, Y)) -> mark#(X), mark#(hd(X)) -> mark#(X))
    (a__hd#(cons(X, Y)) -> mark#(X), mark#(hd(X)) -> a__hd#(mark(X)))
    (a__hd#(cons(X, Y)) -> mark#(X), mark#(tl(X)) -> mark#(X))
    (a__hd#(cons(X, Y)) -> mark#(X), mark#(tl(X)) -> a__tl#(mark(X)))
    (mark#(hd(X)) -> mark#(X), mark#(zeros()) -> a__zeros#())
    (mark#(hd(X)) -> mark#(X), mark#(incr(X)) -> a__incr#(mark(X)))
    (mark#(hd(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
    (mark#(hd(X)) -> mark#(X), mark#(adx(X)) -> a__adx#(mark(X)))
    (mark#(hd(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
    (mark#(hd(X)) -> mark#(X), mark#(nats()) -> a__nats#())
    (mark#(hd(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
    (mark#(hd(X)) -> mark#(X), mark#(hd(X)) -> a__hd#(mark(X)))
    (mark#(hd(X)) -> mark#(X), mark#(tl(X)) -> mark#(X))
    (mark#(hd(X)) -> mark#(X), mark#(tl(X)) -> a__tl#(mark(X)))
    (mark#(incr(X)) -> mark#(X), mark#(zeros()) -> a__zeros#())
    (mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> a__incr#(mark(X)))
    (mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
    (mark#(incr(X)) -> mark#(X), mark#(adx(X)) -> a__adx#(mark(X)))
    (mark#(incr(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
    (mark#(incr(X)) -> mark#(X), mark#(nats()) -> a__nats#())
    (mark#(incr(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
    (mark#(incr(X)) -> mark#(X), mark#(hd(X)) -> a__hd#(mark(X)))
    (mark#(incr(X)) -> mark#(X), mark#(tl(X)) -> mark#(X))
    (mark#(incr(X)) -> mark#(X), mark#(tl(X)) -> a__tl#(mark(X)))}
   SCCS:
    Scc:
     {    mark#(incr(X)) -> mark#(X),
           mark#(adx(X)) -> mark#(X),
            mark#(hd(X)) -> mark#(X),
            mark#(hd(X)) -> a__hd#(mark(X)),
            mark#(tl(X)) -> mark#(X),
            mark#(tl(X)) -> a__tl#(mark(X)),
      a__hd#(cons(X, Y)) -> mark#(X),
      a__tl#(cons(X, Y)) -> mark#(Y)}
    SCC:
     Strict:
      {    mark#(incr(X)) -> mark#(X),
            mark#(adx(X)) -> mark#(X),
             mark#(hd(X)) -> mark#(X),
             mark#(hd(X)) -> a__hd#(mark(X)),
             mark#(tl(X)) -> mark#(X),
             mark#(tl(X)) -> a__tl#(mark(X)),
       a__hd#(cons(X, Y)) -> mark#(X),
       a__tl#(cons(X, Y)) -> mark#(Y)}
     Weak:
     {          a__adx(X) -> adx(X),
       a__adx(cons(X, Y)) -> a__incr(cons(X, adx(Y))),
               a__zeros() -> cons(0(), zeros()),
               a__zeros() -> zeros(),
                a__nats() -> a__adx(a__zeros()),
                a__nats() -> nats(),
               a__incr(X) -> incr(X),
      a__incr(cons(X, Y)) -> cons(s(X), incr(Y)),
       mark(cons(X1, X2)) -> cons(X1, X2),
                mark(0()) -> 0(),
            mark(zeros()) -> a__zeros(),
               mark(s(X)) -> s(X),
            mark(incr(X)) -> a__incr(mark(X)),
             mark(adx(X)) -> a__adx(mark(X)),
             mark(nats()) -> a__nats(),
              mark(hd(X)) -> a__hd(mark(X)),
              mark(tl(X)) -> a__tl(mark(X)),
                 a__hd(X) -> hd(X),
        a__hd(cons(X, Y)) -> mark(X),
                 a__tl(X) -> tl(X),
        a__tl(cons(X, Y)) -> mark(Y)}
     POLY:
      Argument Filtering:
       pi(tl) = [0], pi(hd) = 0, pi(nats) = [], pi(a__tl#) = 0, pi(a__tl) = [0], pi(a__hd#) = 0, pi(a__hd) = 0, pi(mark#) = 0, pi(mark) = 0, pi(adx) = 0, pi(a__incr) = 0, pi(incr) = 0, pi(s) = [], pi(zeros) = [], pi(0) = [], pi(cons) = [0,1], pi(a__nats) = [], pi(a__zeros) = [], pi(a__adx) = 0
      Usable Rules:
       {}
      Interpretation:
       [cons](x0, x1) = x0 + x1,
       [tl](x0) = x0 + 1
      Strict:
       {    mark#(incr(X)) -> mark#(X),
             mark#(adx(X)) -> mark#(X),
              mark#(hd(X)) -> mark#(X),
              mark#(hd(X)) -> a__hd#(mark(X)),
        a__hd#(cons(X, Y)) -> mark#(X),
        a__tl#(cons(X, Y)) -> mark#(Y)}
      Weak:
       {          a__adx(X) -> adx(X),
         a__adx(cons(X, Y)) -> a__incr(cons(X, adx(Y))),
                 a__zeros() -> cons(0(), zeros()),
                 a__zeros() -> zeros(),
                  a__nats() -> a__adx(a__zeros()),
                  a__nats() -> nats(),
                 a__incr(X) -> incr(X),
        a__incr(cons(X, Y)) -> cons(s(X), incr(Y)),
         mark(cons(X1, X2)) -> cons(X1, X2),
                  mark(0()) -> 0(),
              mark(zeros()) -> a__zeros(),
                 mark(s(X)) -> s(X),
              mark(incr(X)) -> a__incr(mark(X)),
               mark(adx(X)) -> a__adx(mark(X)),
               mark(nats()) -> a__nats(),
                mark(hd(X)) -> a__hd(mark(X)),
                mark(tl(X)) -> a__tl(mark(X)),
                   a__hd(X) -> hd(X),
          a__hd(cons(X, Y)) -> mark(X),
                   a__tl(X) -> tl(X),
          a__tl(cons(X, Y)) -> mark(Y)}
      EDG:
       {(mark#(adx(X)) -> mark#(X), mark#(hd(X)) -> a__hd#(mark(X)))
        (mark#(adx(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
        (mark#(adx(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
        (mark#(adx(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
        (a__hd#(cons(X, Y)) -> mark#(X), mark#(hd(X)) -> a__hd#(mark(X)))
        (a__hd#(cons(X, Y)) -> mark#(X), mark#(hd(X)) -> mark#(X))
        (a__hd#(cons(X, Y)) -> mark#(X), mark#(adx(X)) -> mark#(X))
        (a__hd#(cons(X, Y)) -> mark#(X), mark#(incr(X)) -> mark#(X))
        (mark#(hd(X)) -> a__hd#(mark(X)), a__hd#(cons(X, Y)) -> mark#(X))
        (a__tl#(cons(X, Y)) -> mark#(Y), mark#(incr(X)) -> mark#(X))
        (a__tl#(cons(X, Y)) -> mark#(Y), mark#(adx(X)) -> mark#(X))
        (a__tl#(cons(X, Y)) -> mark#(Y), mark#(hd(X)) -> mark#(X))
        (a__tl#(cons(X, Y)) -> mark#(Y), mark#(hd(X)) -> a__hd#(mark(X)))
        (mark#(hd(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
        (mark#(hd(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
        (mark#(hd(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
        (mark#(hd(X)) -> mark#(X), mark#(hd(X)) -> a__hd#(mark(X)))
        (mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))
        (mark#(incr(X)) -> mark#(X), mark#(adx(X)) -> mark#(X))
        (mark#(incr(X)) -> mark#(X), mark#(hd(X)) -> mark#(X))
        (mark#(incr(X)) -> mark#(X), mark#(hd(X)) -> a__hd#(mark(X)))}
       SCCS:
        Scc:
         {    mark#(incr(X)) -> mark#(X),
               mark#(adx(X)) -> mark#(X),
                mark#(hd(X)) -> mark#(X),
                mark#(hd(X)) -> a__hd#(mark(X)),
          a__hd#(cons(X, Y)) -> mark#(X)}
        SCC:
         Strict:
          {    mark#(incr(X)) -> mark#(X),
                mark#(adx(X)) -> mark#(X),
                 mark#(hd(X)) -> mark#(X),
                 mark#(hd(X)) -> a__hd#(mark(X)),
           a__hd#(cons(X, Y)) -> mark#(X)}
         Weak:
         {          a__adx(X) -> adx(X),
           a__adx(cons(X, Y)) -> a__incr(cons(X, adx(Y))),
                   a__zeros() -> cons(0(), zeros()),
                   a__zeros() -> zeros(),
                    a__nats() -> a__adx(a__zeros()),
                    a__nats() -> nats(),
                   a__incr(X) -> incr(X),
          a__incr(cons(X, Y)) -> cons(s(X), incr(Y)),
           mark(cons(X1, X2)) -> cons(X1, X2),
                    mark(0()) -> 0(),
                mark(zeros()) -> a__zeros(),
                   mark(s(X)) -> s(X),
                mark(incr(X)) -> a__incr(mark(X)),
                 mark(adx(X)) -> a__adx(mark(X)),
                 mark(nats()) -> a__nats(),
                  mark(hd(X)) -> a__hd(mark(X)),
                  mark(tl(X)) -> a__tl(mark(X)),
                     a__hd(X) -> hd(X),
            a__hd(cons(X, Y)) -> mark(X),
                     a__tl(X) -> tl(X),
            a__tl(cons(X, Y)) -> mark(Y)}
         POLY:
          Argument Filtering:
           pi(tl) = 0, pi(hd) = [0], pi(nats) = [], pi(a__tl) = 0, pi(a__hd#) = [0], pi(a__hd) = [0], pi(mark#) = [0], pi(mark) = 0, pi(adx) = [0], pi(a__incr) = 0, pi(incr) = 0, pi(s) = 0, pi(zeros) = [], pi(0) = [], pi(cons) = [0,1], pi(a__nats) = [], pi(a__zeros) = [], pi(a__adx) = [0]
          Usable Rules:
           {}
          Interpretation:
           [a__hd#](x0) = x0 + 1,
           [mark#](x0) = x0 + 1,
           [cons](x0, x1) = x0 + x1,
           [hd](x0) = x0 + 1,
           [adx](x0) = x0 + 1
          Strict:
           {    mark#(incr(X)) -> mark#(X),
            a__hd#(cons(X, Y)) -> mark#(X)}
          Weak:
           {          a__adx(X) -> adx(X),
             a__adx(cons(X, Y)) -> a__incr(cons(X, adx(Y))),
                     a__zeros() -> cons(0(), zeros()),
                     a__zeros() -> zeros(),
                      a__nats() -> a__adx(a__zeros()),
                      a__nats() -> nats(),
                     a__incr(X) -> incr(X),
            a__incr(cons(X, Y)) -> cons(s(X), incr(Y)),
             mark(cons(X1, X2)) -> cons(X1, X2),
                      mark(0()) -> 0(),
                  mark(zeros()) -> a__zeros(),
                     mark(s(X)) -> s(X),
                  mark(incr(X)) -> a__incr(mark(X)),
                   mark(adx(X)) -> a__adx(mark(X)),
                   mark(nats()) -> a__nats(),
                    mark(hd(X)) -> a__hd(mark(X)),
                    mark(tl(X)) -> a__tl(mark(X)),
                       a__hd(X) -> hd(X),
              a__hd(cons(X, Y)) -> mark(X),
                       a__tl(X) -> tl(X),
              a__tl(cons(X, Y)) -> mark(Y)}
          EDG:
           {(a__hd#(cons(X, Y)) -> mark#(X), mark#(incr(X)) -> mark#(X))
            (mark#(incr(X)) -> mark#(X), mark#(incr(X)) -> mark#(X))}
           SCCS:
            Scc:
             {mark#(incr(X)) -> mark#(X)}
            SCC:
             Strict:
              {mark#(incr(X)) -> mark#(X)}
             Weak:
             {          a__adx(X) -> adx(X),
               a__adx(cons(X, Y)) -> a__incr(cons(X, adx(Y))),
                       a__zeros() -> cons(0(), zeros()),
                       a__zeros() -> zeros(),
                        a__nats() -> a__adx(a__zeros()),
                        a__nats() -> nats(),
                       a__incr(X) -> incr(X),
              a__incr(cons(X, Y)) -> cons(s(X), incr(Y)),
               mark(cons(X1, X2)) -> cons(X1, X2),
                        mark(0()) -> 0(),
                    mark(zeros()) -> a__zeros(),
                       mark(s(X)) -> s(X),
                    mark(incr(X)) -> a__incr(mark(X)),
                     mark(adx(X)) -> a__adx(mark(X)),
                     mark(nats()) -> a__nats(),
                      mark(hd(X)) -> a__hd(mark(X)),
                      mark(tl(X)) -> a__tl(mark(X)),
                         a__hd(X) -> hd(X),
                a__hd(cons(X, Y)) -> mark(X),
                         a__tl(X) -> tl(X),
                a__tl(cons(X, Y)) -> mark(Y)}
             SPSC:
              Simple Projection:
               pi(mark#) = 0
              Strict:
               {}
              Qed