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