MAYBE
TRS:
 {         active(incr(X)) -> incr(active(X)),
       active(incr(nil())) -> mark(nil()),
  active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
      active(cons(X1, X2)) -> cons(active(X1), X2),
              active(s(X)) -> s(active(X)),
            active(adx(X)) -> adx(active(X)),
        active(adx(nil())) -> mark(nil()),
   active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
           active(zeros()) -> mark(cons(0(), zeros())),
            active(nats()) -> mark(adx(zeros())),
           active(head(X)) -> head(active(X)),
  active(head(cons(X, L))) -> mark(X),
           active(tail(X)) -> tail(active(X)),
  active(tail(cons(X, L))) -> mark(L),
             incr(mark(X)) -> mark(incr(X)),
               incr(ok(X)) -> ok(incr(X)),
        cons(mark(X1), X2) -> mark(cons(X1, X2)),
      cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                s(mark(X)) -> mark(s(X)),
                  s(ok(X)) -> ok(s(X)),
              adx(mark(X)) -> mark(adx(X)),
                adx(ok(X)) -> ok(adx(X)),
             head(mark(X)) -> mark(head(X)),
               head(ok(X)) -> ok(head(X)),
             tail(mark(X)) -> mark(tail(X)),
               tail(ok(X)) -> ok(tail(X)),
             proper(nil()) -> ok(nil()),
           proper(incr(X)) -> incr(proper(X)),
      proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
              proper(s(X)) -> s(proper(X)),
            proper(adx(X)) -> adx(proper(X)),
           proper(zeros()) -> ok(zeros()),
            proper(nats()) -> ok(nats()),
               proper(0()) -> ok(0()),
           proper(head(X)) -> head(proper(X)),
           proper(tail(X)) -> tail(proper(X)),
              top(mark(X)) -> top(proper(X)),
                top(ok(X)) -> top(active(X))}
 DP:
  Strict:
   {         active#(incr(X)) -> active#(X),
             active#(incr(X)) -> incr#(active(X)),
    active#(incr(cons(X, L))) -> incr#(L),
    active#(incr(cons(X, L))) -> cons#(s(X), incr(L)),
    active#(incr(cons(X, L))) -> s#(X),
        active#(cons(X1, X2)) -> active#(X1),
        active#(cons(X1, X2)) -> cons#(active(X1), X2),
                active#(s(X)) -> active#(X),
                active#(s(X)) -> s#(active(X)),
              active#(adx(X)) -> active#(X),
              active#(adx(X)) -> adx#(active(X)),
     active#(adx(cons(X, L))) -> incr#(cons(X, adx(L))),
     active#(adx(cons(X, L))) -> cons#(X, adx(L)),
     active#(adx(cons(X, L))) -> adx#(L),
             active#(zeros()) -> cons#(0(), zeros()),
              active#(nats()) -> adx#(zeros()),
             active#(head(X)) -> active#(X),
             active#(head(X)) -> head#(active(X)),
             active#(tail(X)) -> active#(X),
             active#(tail(X)) -> tail#(active(X)),
               incr#(mark(X)) -> incr#(X),
                 incr#(ok(X)) -> incr#(X),
          cons#(mark(X1), X2) -> cons#(X1, X2),
        cons#(ok(X1), ok(X2)) -> cons#(X1, X2),
                  s#(mark(X)) -> s#(X),
                    s#(ok(X)) -> s#(X),
                adx#(mark(X)) -> adx#(X),
                  adx#(ok(X)) -> adx#(X),
               head#(mark(X)) -> head#(X),
                 head#(ok(X)) -> head#(X),
               tail#(mark(X)) -> tail#(X),
                 tail#(ok(X)) -> tail#(X),
             proper#(incr(X)) -> incr#(proper(X)),
             proper#(incr(X)) -> proper#(X),
        proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)),
        proper#(cons(X1, X2)) -> proper#(X1),
        proper#(cons(X1, X2)) -> proper#(X2),
                proper#(s(X)) -> s#(proper(X)),
                proper#(s(X)) -> proper#(X),
              proper#(adx(X)) -> adx#(proper(X)),
              proper#(adx(X)) -> proper#(X),
             proper#(head(X)) -> head#(proper(X)),
             proper#(head(X)) -> proper#(X),
             proper#(tail(X)) -> tail#(proper(X)),
             proper#(tail(X)) -> proper#(X),
                top#(mark(X)) -> proper#(X),
                top#(mark(X)) -> top#(proper(X)),
                  top#(ok(X)) -> active#(X),
                  top#(ok(X)) -> top#(active(X))}
  Weak:
  {         active(incr(X)) -> incr(active(X)),
        active(incr(nil())) -> mark(nil()),
   active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
       active(cons(X1, X2)) -> cons(active(X1), X2),
               active(s(X)) -> s(active(X)),
             active(adx(X)) -> adx(active(X)),
         active(adx(nil())) -> mark(nil()),
    active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
            active(zeros()) -> mark(cons(0(), zeros())),
             active(nats()) -> mark(adx(zeros())),
            active(head(X)) -> head(active(X)),
   active(head(cons(X, L))) -> mark(X),
            active(tail(X)) -> tail(active(X)),
   active(tail(cons(X, L))) -> mark(L),
              incr(mark(X)) -> mark(incr(X)),
                incr(ok(X)) -> ok(incr(X)),
         cons(mark(X1), X2) -> mark(cons(X1, X2)),
       cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                 s(mark(X)) -> mark(s(X)),
                   s(ok(X)) -> ok(s(X)),
               adx(mark(X)) -> mark(adx(X)),
                 adx(ok(X)) -> ok(adx(X)),
              head(mark(X)) -> mark(head(X)),
                head(ok(X)) -> ok(head(X)),
              tail(mark(X)) -> mark(tail(X)),
                tail(ok(X)) -> ok(tail(X)),
              proper(nil()) -> ok(nil()),
            proper(incr(X)) -> incr(proper(X)),
       proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
               proper(s(X)) -> s(proper(X)),
             proper(adx(X)) -> adx(proper(X)),
            proper(zeros()) -> ok(zeros()),
             proper(nats()) -> ok(nats()),
                proper(0()) -> ok(0()),
            proper(head(X)) -> head(proper(X)),
            proper(tail(X)) -> tail(proper(X)),
               top(mark(X)) -> top(proper(X)),
                 top(ok(X)) -> top(active(X))}
  EDG:
   {
    (active#(incr(cons(X, L))) -> s#(X), s#(ok(X)) -> s#(X))
    (active#(incr(cons(X, L))) -> s#(X), s#(mark(X)) -> s#(X))
    (active#(adx(X)) -> active#(X), active#(tail(X)) -> tail#(active(X)))
    (active#(adx(X)) -> active#(X), active#(tail(X)) -> active#(X))
    (active#(adx(X)) -> active#(X), active#(head(X)) -> head#(active(X)))
    (active#(adx(X)) -> active#(X), active#(head(X)) -> active#(X))
    (active#(adx(X)) -> active#(X), active#(nats()) -> adx#(zeros()))
    (active#(adx(X)) -> active#(X), active#(zeros()) -> cons#(0(), zeros()))
    (active#(adx(X)) -> active#(X), active#(adx(cons(X, L))) -> adx#(L))
    (active#(adx(X)) -> active#(X), active#(adx(cons(X, L))) -> cons#(X, adx(L)))
    (active#(adx(X)) -> active#(X), active#(adx(cons(X, L))) -> incr#(cons(X, adx(L))))
    (active#(adx(X)) -> active#(X), active#(adx(X)) -> adx#(active(X)))
    (active#(adx(X)) -> active#(X), active#(adx(X)) -> active#(X))
    (active#(adx(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(adx(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(adx(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(adx(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (active#(adx(X)) -> active#(X), active#(incr(cons(X, L))) -> s#(X))
    (active#(adx(X)) -> active#(X), active#(incr(cons(X, L))) -> cons#(s(X), incr(L)))
    (active#(adx(X)) -> active#(X), active#(incr(cons(X, L))) -> incr#(L))
    (active#(adx(X)) -> active#(X), active#(incr(X)) -> incr#(active(X)))
    (active#(adx(X)) -> active#(X), active#(incr(X)) -> active#(X))
    (active#(tail(X)) -> active#(X), active#(tail(X)) -> tail#(active(X)))
    (active#(tail(X)) -> active#(X), active#(tail(X)) -> active#(X))
    (active#(tail(X)) -> active#(X), active#(head(X)) -> head#(active(X)))
    (active#(tail(X)) -> active#(X), active#(head(X)) -> active#(X))
    (active#(tail(X)) -> active#(X), active#(nats()) -> adx#(zeros()))
    (active#(tail(X)) -> active#(X), active#(zeros()) -> cons#(0(), zeros()))
    (active#(tail(X)) -> active#(X), active#(adx(cons(X, L))) -> adx#(L))
    (active#(tail(X)) -> active#(X), active#(adx(cons(X, L))) -> cons#(X, adx(L)))
    (active#(tail(X)) -> active#(X), active#(adx(cons(X, L))) -> incr#(cons(X, adx(L))))
    (active#(tail(X)) -> active#(X), active#(adx(X)) -> adx#(active(X)))
    (active#(tail(X)) -> active#(X), active#(adx(X)) -> active#(X))
    (active#(tail(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(tail(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(tail(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(tail(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (active#(tail(X)) -> active#(X), active#(incr(cons(X, L))) -> s#(X))
    (active#(tail(X)) -> active#(X), active#(incr(cons(X, L))) -> cons#(s(X), incr(L)))
    (active#(tail(X)) -> active#(X), active#(incr(cons(X, L))) -> incr#(L))
    (active#(tail(X)) -> active#(X), active#(incr(X)) -> incr#(active(X)))
    (active#(tail(X)) -> active#(X), active#(incr(X)) -> active#(X))
    (incr#(ok(X)) -> incr#(X), incr#(ok(X)) -> incr#(X))
    (incr#(ok(X)) -> incr#(X), incr#(mark(X)) -> incr#(X))
    (s#(ok(X)) -> s#(X), s#(ok(X)) -> s#(X))
    (s#(ok(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (adx#(ok(X)) -> adx#(X), adx#(ok(X)) -> adx#(X))
    (adx#(ok(X)) -> adx#(X), adx#(mark(X)) -> adx#(X))
    (head#(ok(X)) -> head#(X), head#(ok(X)) -> head#(X))
    (head#(ok(X)) -> head#(X), head#(mark(X)) -> head#(X))
    (tail#(ok(X)) -> tail#(X), tail#(ok(X)) -> tail#(X))
    (tail#(ok(X)) -> tail#(X), tail#(mark(X)) -> tail#(X))
    (proper#(s(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(tail(X)) -> tail#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(head(X)) -> head#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(adx(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(adx(X)) -> adx#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(s(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(incr(X)) -> incr#(proper(X)))
    (proper#(head(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))
    (proper#(head(X)) -> proper#(X), proper#(tail(X)) -> tail#(proper(X)))
    (proper#(head(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
    (proper#(head(X)) -> proper#(X), proper#(head(X)) -> head#(proper(X)))
    (proper#(head(X)) -> proper#(X), proper#(adx(X)) -> proper#(X))
    (proper#(head(X)) -> proper#(X), proper#(adx(X)) -> adx#(proper(X)))
    (proper#(head(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(head(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(head(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(head(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(head(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(head(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
    (proper#(head(X)) -> proper#(X), proper#(incr(X)) -> incr#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(tail(X)) -> tail#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(head(X)) -> head#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(adx(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(adx(X)) -> adx#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
    (top#(mark(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
    (top#(mark(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (top#(mark(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(incr(X)) -> incr#(proper(X)))
    (active#(incr(X)) -> incr#(active(X)), incr#(ok(X)) -> incr#(X))
    (active#(incr(X)) -> incr#(active(X)), incr#(mark(X)) -> incr#(X))
    (active#(adx(X)) -> adx#(active(X)), adx#(ok(X)) -> adx#(X))
    (active#(adx(X)) -> adx#(active(X)), adx#(mark(X)) -> adx#(X))
    (active#(tail(X)) -> tail#(active(X)), tail#(ok(X)) -> tail#(X))
    (active#(tail(X)) -> tail#(active(X)), tail#(mark(X)) -> tail#(X))
    (proper#(s(X)) -> s#(proper(X)), s#(ok(X)) -> s#(X))
    (proper#(s(X)) -> s#(proper(X)), s#(mark(X)) -> s#(X))
    (proper#(head(X)) -> head#(proper(X)), head#(ok(X)) -> head#(X))
    (proper#(head(X)) -> head#(proper(X)), head#(mark(X)) -> head#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X)))
    (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> active#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> top#(proper(X)))
    (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> proper#(X))
    (active#(adx(cons(X, L))) -> incr#(cons(X, adx(L))), incr#(ok(X)) -> incr#(X))
    (active#(adx(cons(X, L))) -> incr#(cons(X, adx(L))), incr#(mark(X)) -> incr#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(tail(X)) -> tail#(active(X)))
    (active#(cons(X1, X2)) -> active#(X1), active#(tail(X)) -> active#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(head(X)) -> head#(active(X)))
    (active#(cons(X1, X2)) -> active#(X1), active#(head(X)) -> active#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(nats()) -> adx#(zeros()))
    (active#(cons(X1, X2)) -> active#(X1), active#(zeros()) -> cons#(0(), zeros()))
    (active#(cons(X1, X2)) -> active#(X1), active#(adx(cons(X, L))) -> adx#(L))
    (active#(cons(X1, X2)) -> active#(X1), active#(adx(cons(X, L))) -> cons#(X, adx(L)))
    (active#(cons(X1, X2)) -> active#(X1), active#(adx(cons(X, L))) -> incr#(cons(X, adx(L))))
    (active#(cons(X1, X2)) -> active#(X1), active#(adx(X)) -> adx#(active(X)))
    (active#(cons(X1, X2)) -> active#(X1), active#(adx(X)) -> active#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> s#(active(X)))
    (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
    (active#(cons(X1, X2)) -> active#(X1), active#(incr(cons(X, L))) -> s#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(incr(cons(X, L))) -> cons#(s(X), incr(L)))
    (active#(cons(X1, X2)) -> active#(X1), active#(incr(cons(X, L))) -> incr#(L))
    (active#(cons(X1, X2)) -> active#(X1), active#(incr(X)) -> incr#(active(X)))
    (active#(cons(X1, X2)) -> active#(X1), active#(incr(X)) -> active#(X))
    (active#(adx(cons(X, L))) -> cons#(X, adx(L)), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (active#(adx(cons(X, L))) -> cons#(X, adx(L)), cons#(mark(X1), X2) -> cons#(X1, X2))
    (active#(cons(X1, X2)) -> cons#(active(X1), X2), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (active#(cons(X1, X2)) -> cons#(active(X1), X2), cons#(mark(X1), X2) -> cons#(X1, X2))
    (active#(adx(cons(X, L))) -> adx#(L), adx#(ok(X)) -> adx#(X))
    (active#(adx(cons(X, L))) -> adx#(L), adx#(mark(X)) -> adx#(X))
    (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
    (cons#(ok(X1), ok(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
    (cons#(ok(X1), ok(X2)) -> cons#(X1, X2), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (active#(incr(cons(X, L))) -> incr#(L), incr#(mark(X)) -> incr#(X))
    (active#(incr(cons(X, L))) -> incr#(L), incr#(ok(X)) -> incr#(X))
    (proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)), cons#(mark(X1), X2) -> cons#(X1, X2))
    (proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (active#(incr(cons(X, L))) -> cons#(s(X), incr(L)), cons#(mark(X1), X2) -> cons#(X1, X2))
    (active#(incr(cons(X, L))) -> cons#(s(X), incr(L)), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(incr(X)) -> incr#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(incr(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(adx(X)) -> adx#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(adx(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(head(X)) -> head#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(head(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(tail(X)) -> tail#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(tail(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(incr(X)) -> incr#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(incr(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(adx(X)) -> adx#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(adx(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(head(X)) -> head#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(head(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(tail(X)) -> tail#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(tail(X)) -> proper#(X))
    (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> proper#(X))
    (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> top#(proper(X)))
    (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> active#(X))
    (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> top#(active(X)))
    (proper#(tail(X)) -> tail#(proper(X)), tail#(mark(X)) -> tail#(X))
    (proper#(tail(X)) -> tail#(proper(X)), tail#(ok(X)) -> tail#(X))
    (proper#(adx(X)) -> adx#(proper(X)), adx#(mark(X)) -> adx#(X))
    (proper#(adx(X)) -> adx#(proper(X)), adx#(ok(X)) -> adx#(X))
    (proper#(incr(X)) -> incr#(proper(X)), incr#(mark(X)) -> incr#(X))
    (proper#(incr(X)) -> incr#(proper(X)), incr#(ok(X)) -> incr#(X))
    (active#(head(X)) -> head#(active(X)), head#(mark(X)) -> head#(X))
    (active#(head(X)) -> head#(active(X)), head#(ok(X)) -> head#(X))
    (active#(s(X)) -> s#(active(X)), s#(mark(X)) -> s#(X))
    (active#(s(X)) -> s#(active(X)), s#(ok(X)) -> s#(X))
    (top#(ok(X)) -> active#(X), active#(incr(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(incr(X)) -> incr#(active(X)))
    (top#(ok(X)) -> active#(X), active#(incr(cons(X, L))) -> incr#(L))
    (top#(ok(X)) -> active#(X), active#(incr(cons(X, L))) -> cons#(s(X), incr(L)))
    (top#(ok(X)) -> active#(X), active#(incr(cons(X, L))) -> s#(X))
    (top#(ok(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (top#(ok(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (top#(ok(X)) -> active#(X), active#(s(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (top#(ok(X)) -> active#(X), active#(adx(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(adx(X)) -> adx#(active(X)))
    (top#(ok(X)) -> active#(X), active#(adx(cons(X, L))) -> incr#(cons(X, adx(L))))
    (top#(ok(X)) -> active#(X), active#(adx(cons(X, L))) -> cons#(X, adx(L)))
    (top#(ok(X)) -> active#(X), active#(adx(cons(X, L))) -> adx#(L))
    (top#(ok(X)) -> active#(X), active#(zeros()) -> cons#(0(), zeros()))
    (top#(ok(X)) -> active#(X), active#(nats()) -> adx#(zeros()))
    (top#(ok(X)) -> active#(X), active#(head(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(head(X)) -> head#(active(X)))
    (top#(ok(X)) -> active#(X), active#(tail(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(tail(X)) -> tail#(active(X)))
    (proper#(tail(X)) -> proper#(X), proper#(incr(X)) -> incr#(proper(X)))
    (proper#(tail(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
    (proper#(tail(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(tail(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(tail(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(tail(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(tail(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(tail(X)) -> proper#(X), proper#(adx(X)) -> adx#(proper(X)))
    (proper#(tail(X)) -> proper#(X), proper#(adx(X)) -> proper#(X))
    (proper#(tail(X)) -> proper#(X), proper#(head(X)) -> head#(proper(X)))
    (proper#(tail(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
    (proper#(tail(X)) -> proper#(X), proper#(tail(X)) -> tail#(proper(X)))
    (proper#(tail(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))
    (proper#(adx(X)) -> proper#(X), proper#(incr(X)) -> incr#(proper(X)))
    (proper#(adx(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
    (proper#(adx(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(adx(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(adx(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(adx(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(adx(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(adx(X)) -> proper#(X), proper#(adx(X)) -> adx#(proper(X)))
    (proper#(adx(X)) -> proper#(X), proper#(adx(X)) -> proper#(X))
    (proper#(adx(X)) -> proper#(X), proper#(head(X)) -> head#(proper(X)))
    (proper#(adx(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
    (proper#(adx(X)) -> proper#(X), proper#(tail(X)) -> tail#(proper(X)))
    (proper#(adx(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))
    (proper#(incr(X)) -> proper#(X), proper#(incr(X)) -> incr#(proper(X)))
    (proper#(incr(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
    (proper#(incr(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(incr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(incr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(incr(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(incr(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(incr(X)) -> proper#(X), proper#(adx(X)) -> adx#(proper(X)))
    (proper#(incr(X)) -> proper#(X), proper#(adx(X)) -> proper#(X))
    (proper#(incr(X)) -> proper#(X), proper#(head(X)) -> head#(proper(X)))
    (proper#(incr(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
    (proper#(incr(X)) -> proper#(X), proper#(tail(X)) -> tail#(proper(X)))
    (proper#(incr(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))
    (tail#(mark(X)) -> tail#(X), tail#(mark(X)) -> tail#(X))
    (tail#(mark(X)) -> tail#(X), tail#(ok(X)) -> tail#(X))
    (head#(mark(X)) -> head#(X), head#(mark(X)) -> head#(X))
    (head#(mark(X)) -> head#(X), head#(ok(X)) -> head#(X))
    (adx#(mark(X)) -> adx#(X), adx#(mark(X)) -> adx#(X))
    (adx#(mark(X)) -> adx#(X), adx#(ok(X)) -> adx#(X))
    (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X))
    (incr#(mark(X)) -> incr#(X), incr#(mark(X)) -> incr#(X))
    (incr#(mark(X)) -> incr#(X), incr#(ok(X)) -> incr#(X))
    (active#(head(X)) -> active#(X), active#(incr(X)) -> active#(X))
    (active#(head(X)) -> active#(X), active#(incr(X)) -> incr#(active(X)))
    (active#(head(X)) -> active#(X), active#(incr(cons(X, L))) -> incr#(L))
    (active#(head(X)) -> active#(X), active#(incr(cons(X, L))) -> cons#(s(X), incr(L)))
    (active#(head(X)) -> active#(X), active#(incr(cons(X, L))) -> s#(X))
    (active#(head(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (active#(head(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(head(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(head(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(head(X)) -> active#(X), active#(adx(X)) -> active#(X))
    (active#(head(X)) -> active#(X), active#(adx(X)) -> adx#(active(X)))
    (active#(head(X)) -> active#(X), active#(adx(cons(X, L))) -> incr#(cons(X, adx(L))))
    (active#(head(X)) -> active#(X), active#(adx(cons(X, L))) -> cons#(X, adx(L)))
    (active#(head(X)) -> active#(X), active#(adx(cons(X, L))) -> adx#(L))
    (active#(head(X)) -> active#(X), active#(zeros()) -> cons#(0(), zeros()))
    (active#(head(X)) -> active#(X), active#(nats()) -> adx#(zeros()))
    (active#(head(X)) -> active#(X), active#(head(X)) -> active#(X))
    (active#(head(X)) -> active#(X), active#(head(X)) -> head#(active(X)))
    (active#(head(X)) -> active#(X), active#(tail(X)) -> active#(X))
    (active#(head(X)) -> active#(X), active#(tail(X)) -> tail#(active(X)))
    (active#(s(X)) -> active#(X), active#(incr(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(incr(X)) -> incr#(active(X)))
    (active#(s(X)) -> active#(X), active#(incr(cons(X, L))) -> incr#(L))
    (active#(s(X)) -> active#(X), active#(incr(cons(X, L))) -> cons#(s(X), incr(L)))
    (active#(s(X)) -> active#(X), active#(incr(cons(X, L))) -> s#(X))
    (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(s(X)) -> active#(X), active#(adx(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(adx(X)) -> adx#(active(X)))
    (active#(s(X)) -> active#(X), active#(adx(cons(X, L))) -> incr#(cons(X, adx(L))))
    (active#(s(X)) -> active#(X), active#(adx(cons(X, L))) -> cons#(X, adx(L)))
    (active#(s(X)) -> active#(X), active#(adx(cons(X, L))) -> adx#(L))
    (active#(s(X)) -> active#(X), active#(zeros()) -> cons#(0(), zeros()))
    (active#(s(X)) -> active#(X), active#(nats()) -> adx#(zeros()))
    (active#(s(X)) -> active#(X), active#(head(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(head(X)) -> head#(active(X)))
    (active#(s(X)) -> active#(X), active#(tail(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(tail(X)) -> tail#(active(X)))
    (active#(incr(X)) -> active#(X), active#(incr(X)) -> active#(X))
    (active#(incr(X)) -> active#(X), active#(incr(X)) -> incr#(active(X)))
    (active#(incr(X)) -> active#(X), active#(incr(cons(X, L))) -> incr#(L))
    (active#(incr(X)) -> active#(X), active#(incr(cons(X, L))) -> cons#(s(X), incr(L)))
    (active#(incr(X)) -> active#(X), active#(incr(cons(X, L))) -> s#(X))
    (active#(incr(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (active#(incr(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(incr(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(incr(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(incr(X)) -> active#(X), active#(adx(X)) -> active#(X))
    (active#(incr(X)) -> active#(X), active#(adx(X)) -> adx#(active(X)))
    (active#(incr(X)) -> active#(X), active#(adx(cons(X, L))) -> incr#(cons(X, adx(L))))
    (active#(incr(X)) -> active#(X), active#(adx(cons(X, L))) -> cons#(X, adx(L)))
    (active#(incr(X)) -> active#(X), active#(adx(cons(X, L))) -> adx#(L))
    (active#(incr(X)) -> active#(X), active#(zeros()) -> cons#(0(), zeros()))
    (active#(incr(X)) -> active#(X), active#(nats()) -> adx#(zeros()))
    (active#(incr(X)) -> active#(X), active#(head(X)) -> active#(X))
    (active#(incr(X)) -> active#(X), active#(head(X)) -> head#(active(X)))
    (active#(incr(X)) -> active#(X), active#(tail(X)) -> active#(X))
    (active#(incr(X)) -> active#(X), active#(tail(X)) -> tail#(active(X)))
   }
   SCCS:
    Scc:
     {top#(mark(X)) -> top#(proper(X)),
        top#(ok(X)) -> top#(active(X))}
    Scc:
     {     proper#(incr(X)) -> proper#(X),
      proper#(cons(X1, X2)) -> proper#(X1),
      proper#(cons(X1, X2)) -> proper#(X2),
              proper#(s(X)) -> proper#(X),
            proper#(adx(X)) -> proper#(X),
           proper#(head(X)) -> proper#(X),
           proper#(tail(X)) -> proper#(X)}
    Scc:
     {tail#(mark(X)) -> tail#(X),
        tail#(ok(X)) -> tail#(X)}
    Scc:
     {head#(mark(X)) -> head#(X),
        head#(ok(X)) -> head#(X)}
    Scc:
     {adx#(mark(X)) -> adx#(X),
        adx#(ok(X)) -> adx#(X)}
    Scc:
     {s#(mark(X)) -> s#(X),
        s#(ok(X)) -> s#(X)}
    Scc:
     {  cons#(mark(X1), X2) -> cons#(X1, X2),
      cons#(ok(X1), ok(X2)) -> cons#(X1, X2)}
    Scc:
     {incr#(mark(X)) -> incr#(X),
        incr#(ok(X)) -> incr#(X)}
    Scc:
     {     active#(incr(X)) -> active#(X),
      active#(cons(X1, X2)) -> active#(X1),
              active#(s(X)) -> active#(X),
            active#(adx(X)) -> active#(X),
           active#(head(X)) -> active#(X),
           active#(tail(X)) -> active#(X)}
    SCC:
     Strict:
      {top#(mark(X)) -> top#(proper(X)),
         top#(ok(X)) -> top#(active(X))}
     Weak:
     {         active(incr(X)) -> incr(active(X)),
           active(incr(nil())) -> mark(nil()),
      active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
          active(cons(X1, X2)) -> cons(active(X1), X2),
                  active(s(X)) -> s(active(X)),
                active(adx(X)) -> adx(active(X)),
            active(adx(nil())) -> mark(nil()),
       active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
               active(zeros()) -> mark(cons(0(), zeros())),
                active(nats()) -> mark(adx(zeros())),
               active(head(X)) -> head(active(X)),
      active(head(cons(X, L))) -> mark(X),
               active(tail(X)) -> tail(active(X)),
      active(tail(cons(X, L))) -> mark(L),
                 incr(mark(X)) -> mark(incr(X)),
                   incr(ok(X)) -> ok(incr(X)),
            cons(mark(X1), X2) -> mark(cons(X1, X2)),
          cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                    s(mark(X)) -> mark(s(X)),
                      s(ok(X)) -> ok(s(X)),
                  adx(mark(X)) -> mark(adx(X)),
                    adx(ok(X)) -> ok(adx(X)),
                 head(mark(X)) -> mark(head(X)),
                   head(ok(X)) -> ok(head(X)),
                 tail(mark(X)) -> mark(tail(X)),
                   tail(ok(X)) -> ok(tail(X)),
                 proper(nil()) -> ok(nil()),
               proper(incr(X)) -> incr(proper(X)),
          proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                  proper(s(X)) -> s(proper(X)),
                proper(adx(X)) -> adx(proper(X)),
               proper(zeros()) -> ok(zeros()),
                proper(nats()) -> ok(nats()),
                   proper(0()) -> ok(0()),
               proper(head(X)) -> head(proper(X)),
               proper(tail(X)) -> tail(proper(X)),
                  top(mark(X)) -> top(proper(X)),
                    top(ok(X)) -> top(active(X))}
     Fail
    SCC:
     Strict:
      {     proper#(incr(X)) -> proper#(X),
       proper#(cons(X1, X2)) -> proper#(X1),
       proper#(cons(X1, X2)) -> proper#(X2),
               proper#(s(X)) -> proper#(X),
             proper#(adx(X)) -> proper#(X),
            proper#(head(X)) -> proper#(X),
            proper#(tail(X)) -> proper#(X)}
     Weak:
     {         active(incr(X)) -> incr(active(X)),
           active(incr(nil())) -> mark(nil()),
      active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
          active(cons(X1, X2)) -> cons(active(X1), X2),
                  active(s(X)) -> s(active(X)),
                active(adx(X)) -> adx(active(X)),
            active(adx(nil())) -> mark(nil()),
       active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
               active(zeros()) -> mark(cons(0(), zeros())),
                active(nats()) -> mark(adx(zeros())),
               active(head(X)) -> head(active(X)),
      active(head(cons(X, L))) -> mark(X),
               active(tail(X)) -> tail(active(X)),
      active(tail(cons(X, L))) -> mark(L),
                 incr(mark(X)) -> mark(incr(X)),
                   incr(ok(X)) -> ok(incr(X)),
            cons(mark(X1), X2) -> mark(cons(X1, X2)),
          cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                    s(mark(X)) -> mark(s(X)),
                      s(ok(X)) -> ok(s(X)),
                  adx(mark(X)) -> mark(adx(X)),
                    adx(ok(X)) -> ok(adx(X)),
                 head(mark(X)) -> mark(head(X)),
                   head(ok(X)) -> ok(head(X)),
                 tail(mark(X)) -> mark(tail(X)),
                   tail(ok(X)) -> ok(tail(X)),
                 proper(nil()) -> ok(nil()),
               proper(incr(X)) -> incr(proper(X)),
          proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                  proper(s(X)) -> s(proper(X)),
                proper(adx(X)) -> adx(proper(X)),
               proper(zeros()) -> ok(zeros()),
                proper(nats()) -> ok(nats()),
                   proper(0()) -> ok(0()),
               proper(head(X)) -> head(proper(X)),
               proper(tail(X)) -> tail(proper(X)),
                  top(mark(X)) -> top(proper(X)),
                    top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(proper#) = 0
      Strict:
       {     proper#(incr(X)) -> proper#(X),
        proper#(cons(X1, X2)) -> proper#(X1),
        proper#(cons(X1, X2)) -> proper#(X2),
                proper#(s(X)) -> proper#(X),
              proper#(adx(X)) -> proper#(X),
             proper#(tail(X)) -> proper#(X)}
      EDG:
       {(proper#(incr(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))
        (proper#(incr(X)) -> proper#(X), proper#(adx(X)) -> proper#(X))
        (proper#(incr(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(incr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(incr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(incr(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
        (proper#(adx(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))
        (proper#(adx(X)) -> proper#(X), proper#(adx(X)) -> proper#(X))
        (proper#(adx(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(adx(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(adx(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(adx(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(tail(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(adx(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(incr(X)) -> proper#(X))
        (proper#(tail(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
        (proper#(tail(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(tail(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(tail(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(tail(X)) -> proper#(X), proper#(adx(X)) -> proper#(X))
        (proper#(tail(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))
        (proper#(s(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
        (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(s(X)) -> proper#(X), proper#(adx(X)) -> proper#(X))
        (proper#(s(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(incr(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(adx(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(tail(X)) -> proper#(X))}
       SCCS:
        Scc:
         {     proper#(incr(X)) -> proper#(X),
          proper#(cons(X1, X2)) -> proper#(X1),
          proper#(cons(X1, X2)) -> proper#(X2),
                  proper#(s(X)) -> proper#(X),
                proper#(adx(X)) -> proper#(X),
               proper#(tail(X)) -> proper#(X)}
        SCC:
         Strict:
          {     proper#(incr(X)) -> proper#(X),
           proper#(cons(X1, X2)) -> proper#(X1),
           proper#(cons(X1, X2)) -> proper#(X2),
                   proper#(s(X)) -> proper#(X),
                 proper#(adx(X)) -> proper#(X),
                proper#(tail(X)) -> proper#(X)}
         Weak:
         {         active(incr(X)) -> incr(active(X)),
               active(incr(nil())) -> mark(nil()),
          active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
              active(cons(X1, X2)) -> cons(active(X1), X2),
                      active(s(X)) -> s(active(X)),
                    active(adx(X)) -> adx(active(X)),
                active(adx(nil())) -> mark(nil()),
           active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
                   active(zeros()) -> mark(cons(0(), zeros())),
                    active(nats()) -> mark(adx(zeros())),
                   active(head(X)) -> head(active(X)),
          active(head(cons(X, L))) -> mark(X),
                   active(tail(X)) -> tail(active(X)),
          active(tail(cons(X, L))) -> mark(L),
                     incr(mark(X)) -> mark(incr(X)),
                       incr(ok(X)) -> ok(incr(X)),
                cons(mark(X1), X2) -> mark(cons(X1, X2)),
              cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                        s(mark(X)) -> mark(s(X)),
                          s(ok(X)) -> ok(s(X)),
                      adx(mark(X)) -> mark(adx(X)),
                        adx(ok(X)) -> ok(adx(X)),
                     head(mark(X)) -> mark(head(X)),
                       head(ok(X)) -> ok(head(X)),
                     tail(mark(X)) -> mark(tail(X)),
                       tail(ok(X)) -> ok(tail(X)),
                     proper(nil()) -> ok(nil()),
                   proper(incr(X)) -> incr(proper(X)),
              proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(s(X)) -> s(proper(X)),
                    proper(adx(X)) -> adx(proper(X)),
                   proper(zeros()) -> ok(zeros()),
                    proper(nats()) -> ok(nats()),
                       proper(0()) -> ok(0()),
                   proper(head(X)) -> head(proper(X)),
                   proper(tail(X)) -> tail(proper(X)),
                      top(mark(X)) -> top(proper(X)),
                        top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(proper#) = 0
          Strict:
           {     proper#(incr(X)) -> proper#(X),
            proper#(cons(X1, X2)) -> proper#(X1),
            proper#(cons(X1, X2)) -> proper#(X2),
                    proper#(s(X)) -> proper#(X),
                 proper#(tail(X)) -> proper#(X)}
          EDG:
           {(proper#(s(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))
            (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
            (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
            (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(s(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(tail(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(incr(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X2), proper#(incr(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X2), proper#(tail(X)) -> proper#(X))
            (proper#(tail(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
            (proper#(tail(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(tail(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
            (proper#(tail(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
            (proper#(tail(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))
            (proper#(incr(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
            (proper#(incr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(incr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
            (proper#(incr(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
            (proper#(incr(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))}
           SCCS:
            Scc:
             {     proper#(incr(X)) -> proper#(X),
              proper#(cons(X1, X2)) -> proper#(X1),
              proper#(cons(X1, X2)) -> proper#(X2),
                      proper#(s(X)) -> proper#(X),
                   proper#(tail(X)) -> proper#(X)}
            SCC:
             Strict:
              {     proper#(incr(X)) -> proper#(X),
               proper#(cons(X1, X2)) -> proper#(X1),
               proper#(cons(X1, X2)) -> proper#(X2),
                       proper#(s(X)) -> proper#(X),
                    proper#(tail(X)) -> proper#(X)}
             Weak:
             {         active(incr(X)) -> incr(active(X)),
                   active(incr(nil())) -> mark(nil()),
              active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
                  active(cons(X1, X2)) -> cons(active(X1), X2),
                          active(s(X)) -> s(active(X)),
                        active(adx(X)) -> adx(active(X)),
                    active(adx(nil())) -> mark(nil()),
               active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
                       active(zeros()) -> mark(cons(0(), zeros())),
                        active(nats()) -> mark(adx(zeros())),
                       active(head(X)) -> head(active(X)),
              active(head(cons(X, L))) -> mark(X),
                       active(tail(X)) -> tail(active(X)),
              active(tail(cons(X, L))) -> mark(L),
                         incr(mark(X)) -> mark(incr(X)),
                           incr(ok(X)) -> ok(incr(X)),
                    cons(mark(X1), X2) -> mark(cons(X1, X2)),
                  cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                            s(mark(X)) -> mark(s(X)),
                              s(ok(X)) -> ok(s(X)),
                          adx(mark(X)) -> mark(adx(X)),
                            adx(ok(X)) -> ok(adx(X)),
                         head(mark(X)) -> mark(head(X)),
                           head(ok(X)) -> ok(head(X)),
                         tail(mark(X)) -> mark(tail(X)),
                           tail(ok(X)) -> ok(tail(X)),
                         proper(nil()) -> ok(nil()),
                       proper(incr(X)) -> incr(proper(X)),
                  proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(s(X)) -> s(proper(X)),
                        proper(adx(X)) -> adx(proper(X)),
                       proper(zeros()) -> ok(zeros()),
                        proper(nats()) -> ok(nats()),
                           proper(0()) -> ok(0()),
                       proper(head(X)) -> head(proper(X)),
                       proper(tail(X)) -> tail(proper(X)),
                          top(mark(X)) -> top(proper(X)),
                            top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(proper#) = 0
              Strict:
               {     proper#(incr(X)) -> proper#(X),
                proper#(cons(X1, X2)) -> proper#(X1),
                proper#(cons(X1, X2)) -> proper#(X2),
                        proper#(s(X)) -> proper#(X)}
              EDG:
               {(proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
                (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(s(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
                (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
                (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(cons(X1, X2)) -> proper#(X2), proper#(incr(X)) -> proper#(X))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(incr(X)) -> proper#(X))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                (proper#(incr(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
                (proper#(incr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(incr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
                (proper#(incr(X)) -> proper#(X), proper#(s(X)) -> proper#(X))}
               SCCS:
                Scc:
                 {     proper#(incr(X)) -> proper#(X),
                  proper#(cons(X1, X2)) -> proper#(X1),
                  proper#(cons(X1, X2)) -> proper#(X2),
                          proper#(s(X)) -> proper#(X)}
                SCC:
                 Strict:
                  {     proper#(incr(X)) -> proper#(X),
                   proper#(cons(X1, X2)) -> proper#(X1),
                   proper#(cons(X1, X2)) -> proper#(X2),
                           proper#(s(X)) -> proper#(X)}
                 Weak:
                 {         active(incr(X)) -> incr(active(X)),
                       active(incr(nil())) -> mark(nil()),
                  active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
                      active(cons(X1, X2)) -> cons(active(X1), X2),
                              active(s(X)) -> s(active(X)),
                            active(adx(X)) -> adx(active(X)),
                        active(adx(nil())) -> mark(nil()),
                   active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
                           active(zeros()) -> mark(cons(0(), zeros())),
                            active(nats()) -> mark(adx(zeros())),
                           active(head(X)) -> head(active(X)),
                  active(head(cons(X, L))) -> mark(X),
                           active(tail(X)) -> tail(active(X)),
                  active(tail(cons(X, L))) -> mark(L),
                             incr(mark(X)) -> mark(incr(X)),
                               incr(ok(X)) -> ok(incr(X)),
                        cons(mark(X1), X2) -> mark(cons(X1, X2)),
                      cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                s(mark(X)) -> mark(s(X)),
                                  s(ok(X)) -> ok(s(X)),
                              adx(mark(X)) -> mark(adx(X)),
                                adx(ok(X)) -> ok(adx(X)),
                             head(mark(X)) -> mark(head(X)),
                               head(ok(X)) -> ok(head(X)),
                             tail(mark(X)) -> mark(tail(X)),
                               tail(ok(X)) -> ok(tail(X)),
                             proper(nil()) -> ok(nil()),
                           proper(incr(X)) -> incr(proper(X)),
                      proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                              proper(s(X)) -> s(proper(X)),
                            proper(adx(X)) -> adx(proper(X)),
                           proper(zeros()) -> ok(zeros()),
                            proper(nats()) -> ok(nats()),
                               proper(0()) -> ok(0()),
                           proper(head(X)) -> head(proper(X)),
                           proper(tail(X)) -> tail(proper(X)),
                              top(mark(X)) -> top(proper(X)),
                                top(ok(X)) -> top(active(X))}
                 SPSC:
                  Simple Projection:
                   pi(proper#) = 0
                  Strict:
                   {     proper#(incr(X)) -> proper#(X),
                    proper#(cons(X1, X2)) -> proper#(X1),
                            proper#(s(X)) -> proper#(X)}
                  EDG:
                   {(proper#(incr(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                    (proper#(incr(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(incr(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
                    (proper#(s(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
                    (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(incr(X)) -> proper#(X))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))}
                   SCCS:
                    Scc:
                     {     proper#(incr(X)) -> proper#(X),
                      proper#(cons(X1, X2)) -> proper#(X1),
                              proper#(s(X)) -> proper#(X)}
                    SCC:
                     Strict:
                      {     proper#(incr(X)) -> proper#(X),
                       proper#(cons(X1, X2)) -> proper#(X1),
                               proper#(s(X)) -> proper#(X)}
                     Weak:
                     {         active(incr(X)) -> incr(active(X)),
                           active(incr(nil())) -> mark(nil()),
                      active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
                          active(cons(X1, X2)) -> cons(active(X1), X2),
                                  active(s(X)) -> s(active(X)),
                                active(adx(X)) -> adx(active(X)),
                            active(adx(nil())) -> mark(nil()),
                       active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
                               active(zeros()) -> mark(cons(0(), zeros())),
                                active(nats()) -> mark(adx(zeros())),
                               active(head(X)) -> head(active(X)),
                      active(head(cons(X, L))) -> mark(X),
                               active(tail(X)) -> tail(active(X)),
                      active(tail(cons(X, L))) -> mark(L),
                                 incr(mark(X)) -> mark(incr(X)),
                                   incr(ok(X)) -> ok(incr(X)),
                            cons(mark(X1), X2) -> mark(cons(X1, X2)),
                          cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                    s(mark(X)) -> mark(s(X)),
                                      s(ok(X)) -> ok(s(X)),
                                  adx(mark(X)) -> mark(adx(X)),
                                    adx(ok(X)) -> ok(adx(X)),
                                 head(mark(X)) -> mark(head(X)),
                                   head(ok(X)) -> ok(head(X)),
                                 tail(mark(X)) -> mark(tail(X)),
                                   tail(ok(X)) -> ok(tail(X)),
                                 proper(nil()) -> ok(nil()),
                               proper(incr(X)) -> incr(proper(X)),
                          proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                  proper(s(X)) -> s(proper(X)),
                                proper(adx(X)) -> adx(proper(X)),
                               proper(zeros()) -> ok(zeros()),
                                proper(nats()) -> ok(nats()),
                                   proper(0()) -> ok(0()),
                               proper(head(X)) -> head(proper(X)),
                               proper(tail(X)) -> tail(proper(X)),
                                  top(mark(X)) -> top(proper(X)),
                                    top(ok(X)) -> top(active(X))}
                     SPSC:
                      Simple Projection:
                       pi(proper#) = 0
                      Strict:
                       {proper#(incr(X)) -> proper#(X),
                           proper#(s(X)) -> proper#(X)}
                      EDG:
                       {(proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                        (proper#(s(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
                        (proper#(incr(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
                        (proper#(incr(X)) -> proper#(X), proper#(s(X)) -> proper#(X))}
                       SCCS:
                        Scc:
                         {proper#(incr(X)) -> proper#(X),
                             proper#(s(X)) -> proper#(X)}
                        SCC:
                         Strict:
                          {proper#(incr(X)) -> proper#(X),
                              proper#(s(X)) -> proper#(X)}
                         Weak:
                         {         active(incr(X)) -> incr(active(X)),
                               active(incr(nil())) -> mark(nil()),
                          active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
                              active(cons(X1, X2)) -> cons(active(X1), X2),
                                      active(s(X)) -> s(active(X)),
                                    active(adx(X)) -> adx(active(X)),
                                active(adx(nil())) -> mark(nil()),
                           active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
                                   active(zeros()) -> mark(cons(0(), zeros())),
                                    active(nats()) -> mark(adx(zeros())),
                                   active(head(X)) -> head(active(X)),
                          active(head(cons(X, L))) -> mark(X),
                                   active(tail(X)) -> tail(active(X)),
                          active(tail(cons(X, L))) -> mark(L),
                                     incr(mark(X)) -> mark(incr(X)),
                                       incr(ok(X)) -> ok(incr(X)),
                                cons(mark(X1), X2) -> mark(cons(X1, X2)),
                              cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                        s(mark(X)) -> mark(s(X)),
                                          s(ok(X)) -> ok(s(X)),
                                      adx(mark(X)) -> mark(adx(X)),
                                        adx(ok(X)) -> ok(adx(X)),
                                     head(mark(X)) -> mark(head(X)),
                                       head(ok(X)) -> ok(head(X)),
                                     tail(mark(X)) -> mark(tail(X)),
                                       tail(ok(X)) -> ok(tail(X)),
                                     proper(nil()) -> ok(nil()),
                                   proper(incr(X)) -> incr(proper(X)),
                              proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                      proper(s(X)) -> s(proper(X)),
                                    proper(adx(X)) -> adx(proper(X)),
                                   proper(zeros()) -> ok(zeros()),
                                    proper(nats()) -> ok(nats()),
                                       proper(0()) -> ok(0()),
                                   proper(head(X)) -> head(proper(X)),
                                   proper(tail(X)) -> tail(proper(X)),
                                      top(mark(X)) -> top(proper(X)),
                                        top(ok(X)) -> top(active(X))}
                         SPSC:
                          Simple Projection:
                           pi(proper#) = 0
                          Strict:
                           {proper#(s(X)) -> proper#(X)}
                          EDG:
                           {(proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))}
                           SCCS:
                            Scc:
                             {proper#(s(X)) -> proper#(X)}
                            SCC:
                             Strict:
                              {proper#(s(X)) -> proper#(X)}
                             Weak:
                             {         active(incr(X)) -> incr(active(X)),
                                   active(incr(nil())) -> mark(nil()),
                              active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
                                  active(cons(X1, X2)) -> cons(active(X1), X2),
                                          active(s(X)) -> s(active(X)),
                                        active(adx(X)) -> adx(active(X)),
                                    active(adx(nil())) -> mark(nil()),
                               active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
                                       active(zeros()) -> mark(cons(0(), zeros())),
                                        active(nats()) -> mark(adx(zeros())),
                                       active(head(X)) -> head(active(X)),
                              active(head(cons(X, L))) -> mark(X),
                                       active(tail(X)) -> tail(active(X)),
                              active(tail(cons(X, L))) -> mark(L),
                                         incr(mark(X)) -> mark(incr(X)),
                                           incr(ok(X)) -> ok(incr(X)),
                                    cons(mark(X1), X2) -> mark(cons(X1, X2)),
                                  cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                            s(mark(X)) -> mark(s(X)),
                                              s(ok(X)) -> ok(s(X)),
                                          adx(mark(X)) -> mark(adx(X)),
                                            adx(ok(X)) -> ok(adx(X)),
                                         head(mark(X)) -> mark(head(X)),
                                           head(ok(X)) -> ok(head(X)),
                                         tail(mark(X)) -> mark(tail(X)),
                                           tail(ok(X)) -> ok(tail(X)),
                                         proper(nil()) -> ok(nil()),
                                       proper(incr(X)) -> incr(proper(X)),
                                  proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                          proper(s(X)) -> s(proper(X)),
                                        proper(adx(X)) -> adx(proper(X)),
                                       proper(zeros()) -> ok(zeros()),
                                        proper(nats()) -> ok(nats()),
                                           proper(0()) -> ok(0()),
                                       proper(head(X)) -> head(proper(X)),
                                       proper(tail(X)) -> tail(proper(X)),
                                          top(mark(X)) -> top(proper(X)),
                                            top(ok(X)) -> top(active(X))}
                             SPSC:
                              Simple Projection:
                               pi(proper#) = 0
                              Strict:
                               {}
                              Qed
    SCC:
     Strict:
      {tail#(mark(X)) -> tail#(X),
         tail#(ok(X)) -> tail#(X)}
     Weak:
     {         active(incr(X)) -> incr(active(X)),
           active(incr(nil())) -> mark(nil()),
      active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
          active(cons(X1, X2)) -> cons(active(X1), X2),
                  active(s(X)) -> s(active(X)),
                active(adx(X)) -> adx(active(X)),
            active(adx(nil())) -> mark(nil()),
       active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
               active(zeros()) -> mark(cons(0(), zeros())),
                active(nats()) -> mark(adx(zeros())),
               active(head(X)) -> head(active(X)),
      active(head(cons(X, L))) -> mark(X),
               active(tail(X)) -> tail(active(X)),
      active(tail(cons(X, L))) -> mark(L),
                 incr(mark(X)) -> mark(incr(X)),
                   incr(ok(X)) -> ok(incr(X)),
            cons(mark(X1), X2) -> mark(cons(X1, X2)),
          cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                    s(mark(X)) -> mark(s(X)),
                      s(ok(X)) -> ok(s(X)),
                  adx(mark(X)) -> mark(adx(X)),
                    adx(ok(X)) -> ok(adx(X)),
                 head(mark(X)) -> mark(head(X)),
                   head(ok(X)) -> ok(head(X)),
                 tail(mark(X)) -> mark(tail(X)),
                   tail(ok(X)) -> ok(tail(X)),
                 proper(nil()) -> ok(nil()),
               proper(incr(X)) -> incr(proper(X)),
          proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                  proper(s(X)) -> s(proper(X)),
                proper(adx(X)) -> adx(proper(X)),
               proper(zeros()) -> ok(zeros()),
                proper(nats()) -> ok(nats()),
                   proper(0()) -> ok(0()),
               proper(head(X)) -> head(proper(X)),
               proper(tail(X)) -> tail(proper(X)),
                  top(mark(X)) -> top(proper(X)),
                    top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(tail#) = 0
      Strict:
       {tail#(ok(X)) -> tail#(X)}
      EDG:
       {(tail#(ok(X)) -> tail#(X), tail#(ok(X)) -> tail#(X))}
       SCCS:
        Scc:
         {tail#(ok(X)) -> tail#(X)}
        SCC:
         Strict:
          {tail#(ok(X)) -> tail#(X)}
         Weak:
         {         active(incr(X)) -> incr(active(X)),
               active(incr(nil())) -> mark(nil()),
          active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
              active(cons(X1, X2)) -> cons(active(X1), X2),
                      active(s(X)) -> s(active(X)),
                    active(adx(X)) -> adx(active(X)),
                active(adx(nil())) -> mark(nil()),
           active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
                   active(zeros()) -> mark(cons(0(), zeros())),
                    active(nats()) -> mark(adx(zeros())),
                   active(head(X)) -> head(active(X)),
          active(head(cons(X, L))) -> mark(X),
                   active(tail(X)) -> tail(active(X)),
          active(tail(cons(X, L))) -> mark(L),
                     incr(mark(X)) -> mark(incr(X)),
                       incr(ok(X)) -> ok(incr(X)),
                cons(mark(X1), X2) -> mark(cons(X1, X2)),
              cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                        s(mark(X)) -> mark(s(X)),
                          s(ok(X)) -> ok(s(X)),
                      adx(mark(X)) -> mark(adx(X)),
                        adx(ok(X)) -> ok(adx(X)),
                     head(mark(X)) -> mark(head(X)),
                       head(ok(X)) -> ok(head(X)),
                     tail(mark(X)) -> mark(tail(X)),
                       tail(ok(X)) -> ok(tail(X)),
                     proper(nil()) -> ok(nil()),
                   proper(incr(X)) -> incr(proper(X)),
              proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(s(X)) -> s(proper(X)),
                    proper(adx(X)) -> adx(proper(X)),
                   proper(zeros()) -> ok(zeros()),
                    proper(nats()) -> ok(nats()),
                       proper(0()) -> ok(0()),
                   proper(head(X)) -> head(proper(X)),
                   proper(tail(X)) -> tail(proper(X)),
                      top(mark(X)) -> top(proper(X)),
                        top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(tail#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {head#(mark(X)) -> head#(X),
         head#(ok(X)) -> head#(X)}
     Weak:
     {         active(incr(X)) -> incr(active(X)),
           active(incr(nil())) -> mark(nil()),
      active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
          active(cons(X1, X2)) -> cons(active(X1), X2),
                  active(s(X)) -> s(active(X)),
                active(adx(X)) -> adx(active(X)),
            active(adx(nil())) -> mark(nil()),
       active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
               active(zeros()) -> mark(cons(0(), zeros())),
                active(nats()) -> mark(adx(zeros())),
               active(head(X)) -> head(active(X)),
      active(head(cons(X, L))) -> mark(X),
               active(tail(X)) -> tail(active(X)),
      active(tail(cons(X, L))) -> mark(L),
                 incr(mark(X)) -> mark(incr(X)),
                   incr(ok(X)) -> ok(incr(X)),
            cons(mark(X1), X2) -> mark(cons(X1, X2)),
          cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                    s(mark(X)) -> mark(s(X)),
                      s(ok(X)) -> ok(s(X)),
                  adx(mark(X)) -> mark(adx(X)),
                    adx(ok(X)) -> ok(adx(X)),
                 head(mark(X)) -> mark(head(X)),
                   head(ok(X)) -> ok(head(X)),
                 tail(mark(X)) -> mark(tail(X)),
                   tail(ok(X)) -> ok(tail(X)),
                 proper(nil()) -> ok(nil()),
               proper(incr(X)) -> incr(proper(X)),
          proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                  proper(s(X)) -> s(proper(X)),
                proper(adx(X)) -> adx(proper(X)),
               proper(zeros()) -> ok(zeros()),
                proper(nats()) -> ok(nats()),
                   proper(0()) -> ok(0()),
               proper(head(X)) -> head(proper(X)),
               proper(tail(X)) -> tail(proper(X)),
                  top(mark(X)) -> top(proper(X)),
                    top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(head#) = 0
      Strict:
       {head#(ok(X)) -> head#(X)}
      EDG:
       {(head#(ok(X)) -> head#(X), head#(ok(X)) -> head#(X))}
       SCCS:
        Scc:
         {head#(ok(X)) -> head#(X)}
        SCC:
         Strict:
          {head#(ok(X)) -> head#(X)}
         Weak:
         {         active(incr(X)) -> incr(active(X)),
               active(incr(nil())) -> mark(nil()),
          active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
              active(cons(X1, X2)) -> cons(active(X1), X2),
                      active(s(X)) -> s(active(X)),
                    active(adx(X)) -> adx(active(X)),
                active(adx(nil())) -> mark(nil()),
           active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
                   active(zeros()) -> mark(cons(0(), zeros())),
                    active(nats()) -> mark(adx(zeros())),
                   active(head(X)) -> head(active(X)),
          active(head(cons(X, L))) -> mark(X),
                   active(tail(X)) -> tail(active(X)),
          active(tail(cons(X, L))) -> mark(L),
                     incr(mark(X)) -> mark(incr(X)),
                       incr(ok(X)) -> ok(incr(X)),
                cons(mark(X1), X2) -> mark(cons(X1, X2)),
              cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                        s(mark(X)) -> mark(s(X)),
                          s(ok(X)) -> ok(s(X)),
                      adx(mark(X)) -> mark(adx(X)),
                        adx(ok(X)) -> ok(adx(X)),
                     head(mark(X)) -> mark(head(X)),
                       head(ok(X)) -> ok(head(X)),
                     tail(mark(X)) -> mark(tail(X)),
                       tail(ok(X)) -> ok(tail(X)),
                     proper(nil()) -> ok(nil()),
                   proper(incr(X)) -> incr(proper(X)),
              proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(s(X)) -> s(proper(X)),
                    proper(adx(X)) -> adx(proper(X)),
                   proper(zeros()) -> ok(zeros()),
                    proper(nats()) -> ok(nats()),
                       proper(0()) -> ok(0()),
                   proper(head(X)) -> head(proper(X)),
                   proper(tail(X)) -> tail(proper(X)),
                      top(mark(X)) -> top(proper(X)),
                        top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(head#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {adx#(mark(X)) -> adx#(X),
         adx#(ok(X)) -> adx#(X)}
     Weak:
     {         active(incr(X)) -> incr(active(X)),
           active(incr(nil())) -> mark(nil()),
      active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
          active(cons(X1, X2)) -> cons(active(X1), X2),
                  active(s(X)) -> s(active(X)),
                active(adx(X)) -> adx(active(X)),
            active(adx(nil())) -> mark(nil()),
       active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
               active(zeros()) -> mark(cons(0(), zeros())),
                active(nats()) -> mark(adx(zeros())),
               active(head(X)) -> head(active(X)),
      active(head(cons(X, L))) -> mark(X),
               active(tail(X)) -> tail(active(X)),
      active(tail(cons(X, L))) -> mark(L),
                 incr(mark(X)) -> mark(incr(X)),
                   incr(ok(X)) -> ok(incr(X)),
            cons(mark(X1), X2) -> mark(cons(X1, X2)),
          cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                    s(mark(X)) -> mark(s(X)),
                      s(ok(X)) -> ok(s(X)),
                  adx(mark(X)) -> mark(adx(X)),
                    adx(ok(X)) -> ok(adx(X)),
                 head(mark(X)) -> mark(head(X)),
                   head(ok(X)) -> ok(head(X)),
                 tail(mark(X)) -> mark(tail(X)),
                   tail(ok(X)) -> ok(tail(X)),
                 proper(nil()) -> ok(nil()),
               proper(incr(X)) -> incr(proper(X)),
          proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                  proper(s(X)) -> s(proper(X)),
                proper(adx(X)) -> adx(proper(X)),
               proper(zeros()) -> ok(zeros()),
                proper(nats()) -> ok(nats()),
                   proper(0()) -> ok(0()),
               proper(head(X)) -> head(proper(X)),
               proper(tail(X)) -> tail(proper(X)),
                  top(mark(X)) -> top(proper(X)),
                    top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(adx#) = 0
      Strict:
       {adx#(ok(X)) -> adx#(X)}
      EDG:
       {(adx#(ok(X)) -> adx#(X), adx#(ok(X)) -> adx#(X))}
       SCCS:
        Scc:
         {adx#(ok(X)) -> adx#(X)}
        SCC:
         Strict:
          {adx#(ok(X)) -> adx#(X)}
         Weak:
         {         active(incr(X)) -> incr(active(X)),
               active(incr(nil())) -> mark(nil()),
          active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
              active(cons(X1, X2)) -> cons(active(X1), X2),
                      active(s(X)) -> s(active(X)),
                    active(adx(X)) -> adx(active(X)),
                active(adx(nil())) -> mark(nil()),
           active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
                   active(zeros()) -> mark(cons(0(), zeros())),
                    active(nats()) -> mark(adx(zeros())),
                   active(head(X)) -> head(active(X)),
          active(head(cons(X, L))) -> mark(X),
                   active(tail(X)) -> tail(active(X)),
          active(tail(cons(X, L))) -> mark(L),
                     incr(mark(X)) -> mark(incr(X)),
                       incr(ok(X)) -> ok(incr(X)),
                cons(mark(X1), X2) -> mark(cons(X1, X2)),
              cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                        s(mark(X)) -> mark(s(X)),
                          s(ok(X)) -> ok(s(X)),
                      adx(mark(X)) -> mark(adx(X)),
                        adx(ok(X)) -> ok(adx(X)),
                     head(mark(X)) -> mark(head(X)),
                       head(ok(X)) -> ok(head(X)),
                     tail(mark(X)) -> mark(tail(X)),
                       tail(ok(X)) -> ok(tail(X)),
                     proper(nil()) -> ok(nil()),
                   proper(incr(X)) -> incr(proper(X)),
              proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(s(X)) -> s(proper(X)),
                    proper(adx(X)) -> adx(proper(X)),
                   proper(zeros()) -> ok(zeros()),
                    proper(nats()) -> ok(nats()),
                       proper(0()) -> ok(0()),
                   proper(head(X)) -> head(proper(X)),
                   proper(tail(X)) -> tail(proper(X)),
                      top(mark(X)) -> top(proper(X)),
                        top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(adx#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {s#(mark(X)) -> s#(X),
         s#(ok(X)) -> s#(X)}
     Weak:
     {         active(incr(X)) -> incr(active(X)),
           active(incr(nil())) -> mark(nil()),
      active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
          active(cons(X1, X2)) -> cons(active(X1), X2),
                  active(s(X)) -> s(active(X)),
                active(adx(X)) -> adx(active(X)),
            active(adx(nil())) -> mark(nil()),
       active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
               active(zeros()) -> mark(cons(0(), zeros())),
                active(nats()) -> mark(adx(zeros())),
               active(head(X)) -> head(active(X)),
      active(head(cons(X, L))) -> mark(X),
               active(tail(X)) -> tail(active(X)),
      active(tail(cons(X, L))) -> mark(L),
                 incr(mark(X)) -> mark(incr(X)),
                   incr(ok(X)) -> ok(incr(X)),
            cons(mark(X1), X2) -> mark(cons(X1, X2)),
          cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                    s(mark(X)) -> mark(s(X)),
                      s(ok(X)) -> ok(s(X)),
                  adx(mark(X)) -> mark(adx(X)),
                    adx(ok(X)) -> ok(adx(X)),
                 head(mark(X)) -> mark(head(X)),
                   head(ok(X)) -> ok(head(X)),
                 tail(mark(X)) -> mark(tail(X)),
                   tail(ok(X)) -> ok(tail(X)),
                 proper(nil()) -> ok(nil()),
               proper(incr(X)) -> incr(proper(X)),
          proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                  proper(s(X)) -> s(proper(X)),
                proper(adx(X)) -> adx(proper(X)),
               proper(zeros()) -> ok(zeros()),
                proper(nats()) -> ok(nats()),
                   proper(0()) -> ok(0()),
               proper(head(X)) -> head(proper(X)),
               proper(tail(X)) -> tail(proper(X)),
                  top(mark(X)) -> top(proper(X)),
                    top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(s#) = 0
      Strict:
       {s#(ok(X)) -> s#(X)}
      EDG:
       {(s#(ok(X)) -> s#(X), s#(ok(X)) -> s#(X))}
       SCCS:
        Scc:
         {s#(ok(X)) -> s#(X)}
        SCC:
         Strict:
          {s#(ok(X)) -> s#(X)}
         Weak:
         {         active(incr(X)) -> incr(active(X)),
               active(incr(nil())) -> mark(nil()),
          active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
              active(cons(X1, X2)) -> cons(active(X1), X2),
                      active(s(X)) -> s(active(X)),
                    active(adx(X)) -> adx(active(X)),
                active(adx(nil())) -> mark(nil()),
           active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
                   active(zeros()) -> mark(cons(0(), zeros())),
                    active(nats()) -> mark(adx(zeros())),
                   active(head(X)) -> head(active(X)),
          active(head(cons(X, L))) -> mark(X),
                   active(tail(X)) -> tail(active(X)),
          active(tail(cons(X, L))) -> mark(L),
                     incr(mark(X)) -> mark(incr(X)),
                       incr(ok(X)) -> ok(incr(X)),
                cons(mark(X1), X2) -> mark(cons(X1, X2)),
              cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                        s(mark(X)) -> mark(s(X)),
                          s(ok(X)) -> ok(s(X)),
                      adx(mark(X)) -> mark(adx(X)),
                        adx(ok(X)) -> ok(adx(X)),
                     head(mark(X)) -> mark(head(X)),
                       head(ok(X)) -> ok(head(X)),
                     tail(mark(X)) -> mark(tail(X)),
                       tail(ok(X)) -> ok(tail(X)),
                     proper(nil()) -> ok(nil()),
                   proper(incr(X)) -> incr(proper(X)),
              proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(s(X)) -> s(proper(X)),
                    proper(adx(X)) -> adx(proper(X)),
                   proper(zeros()) -> ok(zeros()),
                    proper(nats()) -> ok(nats()),
                       proper(0()) -> ok(0()),
                   proper(head(X)) -> head(proper(X)),
                   proper(tail(X)) -> tail(proper(X)),
                      top(mark(X)) -> top(proper(X)),
                        top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(s#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {  cons#(mark(X1), X2) -> cons#(X1, X2),
       cons#(ok(X1), ok(X2)) -> cons#(X1, X2)}
     Weak:
     {         active(incr(X)) -> incr(active(X)),
           active(incr(nil())) -> mark(nil()),
      active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
          active(cons(X1, X2)) -> cons(active(X1), X2),
                  active(s(X)) -> s(active(X)),
                active(adx(X)) -> adx(active(X)),
            active(adx(nil())) -> mark(nil()),
       active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
               active(zeros()) -> mark(cons(0(), zeros())),
                active(nats()) -> mark(adx(zeros())),
               active(head(X)) -> head(active(X)),
      active(head(cons(X, L))) -> mark(X),
               active(tail(X)) -> tail(active(X)),
      active(tail(cons(X, L))) -> mark(L),
                 incr(mark(X)) -> mark(incr(X)),
                   incr(ok(X)) -> ok(incr(X)),
            cons(mark(X1), X2) -> mark(cons(X1, X2)),
          cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                    s(mark(X)) -> mark(s(X)),
                      s(ok(X)) -> ok(s(X)),
                  adx(mark(X)) -> mark(adx(X)),
                    adx(ok(X)) -> ok(adx(X)),
                 head(mark(X)) -> mark(head(X)),
                   head(ok(X)) -> ok(head(X)),
                 tail(mark(X)) -> mark(tail(X)),
                   tail(ok(X)) -> ok(tail(X)),
                 proper(nil()) -> ok(nil()),
               proper(incr(X)) -> incr(proper(X)),
          proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                  proper(s(X)) -> s(proper(X)),
                proper(adx(X)) -> adx(proper(X)),
               proper(zeros()) -> ok(zeros()),
                proper(nats()) -> ok(nats()),
                   proper(0()) -> ok(0()),
               proper(head(X)) -> head(proper(X)),
               proper(tail(X)) -> tail(proper(X)),
                  top(mark(X)) -> top(proper(X)),
                    top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(cons#) = 0
      Strict:
       {cons#(mark(X1), X2) -> cons#(X1, X2)}
      EDG:
       {(cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))}
       SCCS:
        Scc:
         {cons#(mark(X1), X2) -> cons#(X1, X2)}
        SCC:
         Strict:
          {cons#(mark(X1), X2) -> cons#(X1, X2)}
         Weak:
         {         active(incr(X)) -> incr(active(X)),
               active(incr(nil())) -> mark(nil()),
          active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
              active(cons(X1, X2)) -> cons(active(X1), X2),
                      active(s(X)) -> s(active(X)),
                    active(adx(X)) -> adx(active(X)),
                active(adx(nil())) -> mark(nil()),
           active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
                   active(zeros()) -> mark(cons(0(), zeros())),
                    active(nats()) -> mark(adx(zeros())),
                   active(head(X)) -> head(active(X)),
          active(head(cons(X, L))) -> mark(X),
                   active(tail(X)) -> tail(active(X)),
          active(tail(cons(X, L))) -> mark(L),
                     incr(mark(X)) -> mark(incr(X)),
                       incr(ok(X)) -> ok(incr(X)),
                cons(mark(X1), X2) -> mark(cons(X1, X2)),
              cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                        s(mark(X)) -> mark(s(X)),
                          s(ok(X)) -> ok(s(X)),
                      adx(mark(X)) -> mark(adx(X)),
                        adx(ok(X)) -> ok(adx(X)),
                     head(mark(X)) -> mark(head(X)),
                       head(ok(X)) -> ok(head(X)),
                     tail(mark(X)) -> mark(tail(X)),
                       tail(ok(X)) -> ok(tail(X)),
                     proper(nil()) -> ok(nil()),
                   proper(incr(X)) -> incr(proper(X)),
              proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(s(X)) -> s(proper(X)),
                    proper(adx(X)) -> adx(proper(X)),
                   proper(zeros()) -> ok(zeros()),
                    proper(nats()) -> ok(nats()),
                       proper(0()) -> ok(0()),
                   proper(head(X)) -> head(proper(X)),
                   proper(tail(X)) -> tail(proper(X)),
                      top(mark(X)) -> top(proper(X)),
                        top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(cons#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {incr#(mark(X)) -> incr#(X),
         incr#(ok(X)) -> incr#(X)}
     Weak:
     {         active(incr(X)) -> incr(active(X)),
           active(incr(nil())) -> mark(nil()),
      active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
          active(cons(X1, X2)) -> cons(active(X1), X2),
                  active(s(X)) -> s(active(X)),
                active(adx(X)) -> adx(active(X)),
            active(adx(nil())) -> mark(nil()),
       active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
               active(zeros()) -> mark(cons(0(), zeros())),
                active(nats()) -> mark(adx(zeros())),
               active(head(X)) -> head(active(X)),
      active(head(cons(X, L))) -> mark(X),
               active(tail(X)) -> tail(active(X)),
      active(tail(cons(X, L))) -> mark(L),
                 incr(mark(X)) -> mark(incr(X)),
                   incr(ok(X)) -> ok(incr(X)),
            cons(mark(X1), X2) -> mark(cons(X1, X2)),
          cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                    s(mark(X)) -> mark(s(X)),
                      s(ok(X)) -> ok(s(X)),
                  adx(mark(X)) -> mark(adx(X)),
                    adx(ok(X)) -> ok(adx(X)),
                 head(mark(X)) -> mark(head(X)),
                   head(ok(X)) -> ok(head(X)),
                 tail(mark(X)) -> mark(tail(X)),
                   tail(ok(X)) -> ok(tail(X)),
                 proper(nil()) -> ok(nil()),
               proper(incr(X)) -> incr(proper(X)),
          proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                  proper(s(X)) -> s(proper(X)),
                proper(adx(X)) -> adx(proper(X)),
               proper(zeros()) -> ok(zeros()),
                proper(nats()) -> ok(nats()),
                   proper(0()) -> ok(0()),
               proper(head(X)) -> head(proper(X)),
               proper(tail(X)) -> tail(proper(X)),
                  top(mark(X)) -> top(proper(X)),
                    top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(incr#) = 0
      Strict:
       {incr#(ok(X)) -> incr#(X)}
      EDG:
       {(incr#(ok(X)) -> incr#(X), incr#(ok(X)) -> incr#(X))}
       SCCS:
        Scc:
         {incr#(ok(X)) -> incr#(X)}
        SCC:
         Strict:
          {incr#(ok(X)) -> incr#(X)}
         Weak:
         {         active(incr(X)) -> incr(active(X)),
               active(incr(nil())) -> mark(nil()),
          active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
              active(cons(X1, X2)) -> cons(active(X1), X2),
                      active(s(X)) -> s(active(X)),
                    active(adx(X)) -> adx(active(X)),
                active(adx(nil())) -> mark(nil()),
           active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
                   active(zeros()) -> mark(cons(0(), zeros())),
                    active(nats()) -> mark(adx(zeros())),
                   active(head(X)) -> head(active(X)),
          active(head(cons(X, L))) -> mark(X),
                   active(tail(X)) -> tail(active(X)),
          active(tail(cons(X, L))) -> mark(L),
                     incr(mark(X)) -> mark(incr(X)),
                       incr(ok(X)) -> ok(incr(X)),
                cons(mark(X1), X2) -> mark(cons(X1, X2)),
              cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                        s(mark(X)) -> mark(s(X)),
                          s(ok(X)) -> ok(s(X)),
                      adx(mark(X)) -> mark(adx(X)),
                        adx(ok(X)) -> ok(adx(X)),
                     head(mark(X)) -> mark(head(X)),
                       head(ok(X)) -> ok(head(X)),
                     tail(mark(X)) -> mark(tail(X)),
                       tail(ok(X)) -> ok(tail(X)),
                     proper(nil()) -> ok(nil()),
                   proper(incr(X)) -> incr(proper(X)),
              proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(s(X)) -> s(proper(X)),
                    proper(adx(X)) -> adx(proper(X)),
                   proper(zeros()) -> ok(zeros()),
                    proper(nats()) -> ok(nats()),
                       proper(0()) -> ok(0()),
                   proper(head(X)) -> head(proper(X)),
                   proper(tail(X)) -> tail(proper(X)),
                      top(mark(X)) -> top(proper(X)),
                        top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(incr#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {     active#(incr(X)) -> active#(X),
       active#(cons(X1, X2)) -> active#(X1),
               active#(s(X)) -> active#(X),
             active#(adx(X)) -> active#(X),
            active#(head(X)) -> active#(X),
            active#(tail(X)) -> active#(X)}
     Weak:
     {         active(incr(X)) -> incr(active(X)),
           active(incr(nil())) -> mark(nil()),
      active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
          active(cons(X1, X2)) -> cons(active(X1), X2),
                  active(s(X)) -> s(active(X)),
                active(adx(X)) -> adx(active(X)),
            active(adx(nil())) -> mark(nil()),
       active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
               active(zeros()) -> mark(cons(0(), zeros())),
                active(nats()) -> mark(adx(zeros())),
               active(head(X)) -> head(active(X)),
      active(head(cons(X, L))) -> mark(X),
               active(tail(X)) -> tail(active(X)),
      active(tail(cons(X, L))) -> mark(L),
                 incr(mark(X)) -> mark(incr(X)),
                   incr(ok(X)) -> ok(incr(X)),
            cons(mark(X1), X2) -> mark(cons(X1, X2)),
          cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                    s(mark(X)) -> mark(s(X)),
                      s(ok(X)) -> ok(s(X)),
                  adx(mark(X)) -> mark(adx(X)),
                    adx(ok(X)) -> ok(adx(X)),
                 head(mark(X)) -> mark(head(X)),
                   head(ok(X)) -> ok(head(X)),
                 tail(mark(X)) -> mark(tail(X)),
                   tail(ok(X)) -> ok(tail(X)),
                 proper(nil()) -> ok(nil()),
               proper(incr(X)) -> incr(proper(X)),
          proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                  proper(s(X)) -> s(proper(X)),
                proper(adx(X)) -> adx(proper(X)),
               proper(zeros()) -> ok(zeros()),
                proper(nats()) -> ok(nats()),
                   proper(0()) -> ok(0()),
               proper(head(X)) -> head(proper(X)),
               proper(tail(X)) -> tail(proper(X)),
                  top(mark(X)) -> top(proper(X)),
                    top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(active#) = 0
      Strict:
       {     active#(incr(X)) -> active#(X),
        active#(cons(X1, X2)) -> active#(X1),
                active#(s(X)) -> active#(X),
              active#(adx(X)) -> active#(X),
             active#(tail(X)) -> active#(X)}
      EDG:
       {(active#(s(X)) -> active#(X), active#(tail(X)) -> active#(X))
        (active#(s(X)) -> active#(X), active#(adx(X)) -> active#(X))
        (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
        (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
        (active#(s(X)) -> active#(X), active#(incr(X)) -> active#(X))
        (active#(tail(X)) -> active#(X), active#(tail(X)) -> active#(X))
        (active#(tail(X)) -> active#(X), active#(adx(X)) -> active#(X))
        (active#(tail(X)) -> active#(X), active#(s(X)) -> active#(X))
        (active#(tail(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
        (active#(tail(X)) -> active#(X), active#(incr(X)) -> active#(X))
        (active#(cons(X1, X2)) -> active#(X1), active#(incr(X)) -> active#(X))
        (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
        (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
        (active#(cons(X1, X2)) -> active#(X1), active#(adx(X)) -> active#(X))
        (active#(cons(X1, X2)) -> active#(X1), active#(tail(X)) -> active#(X))
        (active#(adx(X)) -> active#(X), active#(incr(X)) -> active#(X))
        (active#(adx(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
        (active#(adx(X)) -> active#(X), active#(s(X)) -> active#(X))
        (active#(adx(X)) -> active#(X), active#(adx(X)) -> active#(X))
        (active#(adx(X)) -> active#(X), active#(tail(X)) -> active#(X))
        (active#(incr(X)) -> active#(X), active#(incr(X)) -> active#(X))
        (active#(incr(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
        (active#(incr(X)) -> active#(X), active#(s(X)) -> active#(X))
        (active#(incr(X)) -> active#(X), active#(adx(X)) -> active#(X))
        (active#(incr(X)) -> active#(X), active#(tail(X)) -> active#(X))}
       SCCS:
        Scc:
         {     active#(incr(X)) -> active#(X),
          active#(cons(X1, X2)) -> active#(X1),
                  active#(s(X)) -> active#(X),
                active#(adx(X)) -> active#(X),
               active#(tail(X)) -> active#(X)}
        SCC:
         Strict:
          {     active#(incr(X)) -> active#(X),
           active#(cons(X1, X2)) -> active#(X1),
                   active#(s(X)) -> active#(X),
                 active#(adx(X)) -> active#(X),
                active#(tail(X)) -> active#(X)}
         Weak:
         {         active(incr(X)) -> incr(active(X)),
               active(incr(nil())) -> mark(nil()),
          active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
              active(cons(X1, X2)) -> cons(active(X1), X2),
                      active(s(X)) -> s(active(X)),
                    active(adx(X)) -> adx(active(X)),
                active(adx(nil())) -> mark(nil()),
           active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
                   active(zeros()) -> mark(cons(0(), zeros())),
                    active(nats()) -> mark(adx(zeros())),
                   active(head(X)) -> head(active(X)),
          active(head(cons(X, L))) -> mark(X),
                   active(tail(X)) -> tail(active(X)),
          active(tail(cons(X, L))) -> mark(L),
                     incr(mark(X)) -> mark(incr(X)),
                       incr(ok(X)) -> ok(incr(X)),
                cons(mark(X1), X2) -> mark(cons(X1, X2)),
              cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                        s(mark(X)) -> mark(s(X)),
                          s(ok(X)) -> ok(s(X)),
                      adx(mark(X)) -> mark(adx(X)),
                        adx(ok(X)) -> ok(adx(X)),
                     head(mark(X)) -> mark(head(X)),
                       head(ok(X)) -> ok(head(X)),
                     tail(mark(X)) -> mark(tail(X)),
                       tail(ok(X)) -> ok(tail(X)),
                     proper(nil()) -> ok(nil()),
                   proper(incr(X)) -> incr(proper(X)),
              proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(s(X)) -> s(proper(X)),
                    proper(adx(X)) -> adx(proper(X)),
                   proper(zeros()) -> ok(zeros()),
                    proper(nats()) -> ok(nats()),
                       proper(0()) -> ok(0()),
                   proper(head(X)) -> head(proper(X)),
                   proper(tail(X)) -> tail(proper(X)),
                      top(mark(X)) -> top(proper(X)),
                        top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(active#) = 0
          Strict:
           {     active#(incr(X)) -> active#(X),
            active#(cons(X1, X2)) -> active#(X1),
                    active#(s(X)) -> active#(X),
                 active#(tail(X)) -> active#(X)}
          EDG:
           {(active#(s(X)) -> active#(X), active#(tail(X)) -> active#(X))
            (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
            (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
            (active#(s(X)) -> active#(X), active#(incr(X)) -> active#(X))
            (active#(cons(X1, X2)) -> active#(X1), active#(tail(X)) -> active#(X))
            (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
            (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
            (active#(cons(X1, X2)) -> active#(X1), active#(incr(X)) -> active#(X))
            (active#(tail(X)) -> active#(X), active#(incr(X)) -> active#(X))
            (active#(tail(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
            (active#(tail(X)) -> active#(X), active#(s(X)) -> active#(X))
            (active#(tail(X)) -> active#(X), active#(tail(X)) -> active#(X))
            (active#(incr(X)) -> active#(X), active#(incr(X)) -> active#(X))
            (active#(incr(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
            (active#(incr(X)) -> active#(X), active#(s(X)) -> active#(X))
            (active#(incr(X)) -> active#(X), active#(tail(X)) -> active#(X))}
           SCCS:
            Scc:
             {     active#(incr(X)) -> active#(X),
              active#(cons(X1, X2)) -> active#(X1),
                      active#(s(X)) -> active#(X),
                   active#(tail(X)) -> active#(X)}
            SCC:
             Strict:
              {     active#(incr(X)) -> active#(X),
               active#(cons(X1, X2)) -> active#(X1),
                       active#(s(X)) -> active#(X),
                    active#(tail(X)) -> active#(X)}
             Weak:
             {         active(incr(X)) -> incr(active(X)),
                   active(incr(nil())) -> mark(nil()),
              active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
                  active(cons(X1, X2)) -> cons(active(X1), X2),
                          active(s(X)) -> s(active(X)),
                        active(adx(X)) -> adx(active(X)),
                    active(adx(nil())) -> mark(nil()),
               active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
                       active(zeros()) -> mark(cons(0(), zeros())),
                        active(nats()) -> mark(adx(zeros())),
                       active(head(X)) -> head(active(X)),
              active(head(cons(X, L))) -> mark(X),
                       active(tail(X)) -> tail(active(X)),
              active(tail(cons(X, L))) -> mark(L),
                         incr(mark(X)) -> mark(incr(X)),
                           incr(ok(X)) -> ok(incr(X)),
                    cons(mark(X1), X2) -> mark(cons(X1, X2)),
                  cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                            s(mark(X)) -> mark(s(X)),
                              s(ok(X)) -> ok(s(X)),
                          adx(mark(X)) -> mark(adx(X)),
                            adx(ok(X)) -> ok(adx(X)),
                         head(mark(X)) -> mark(head(X)),
                           head(ok(X)) -> ok(head(X)),
                         tail(mark(X)) -> mark(tail(X)),
                           tail(ok(X)) -> ok(tail(X)),
                         proper(nil()) -> ok(nil()),
                       proper(incr(X)) -> incr(proper(X)),
                  proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(s(X)) -> s(proper(X)),
                        proper(adx(X)) -> adx(proper(X)),
                       proper(zeros()) -> ok(zeros()),
                        proper(nats()) -> ok(nats()),
                           proper(0()) -> ok(0()),
                       proper(head(X)) -> head(proper(X)),
                       proper(tail(X)) -> tail(proper(X)),
                          top(mark(X)) -> top(proper(X)),
                            top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(active#) = 0
              Strict:
               {     active#(incr(X)) -> active#(X),
                active#(cons(X1, X2)) -> active#(X1),
                        active#(s(X)) -> active#(X)}
              EDG:
               {(active#(incr(X)) -> active#(X), active#(s(X)) -> active#(X))
                (active#(incr(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
                (active#(incr(X)) -> active#(X), active#(incr(X)) -> active#(X))
                (active#(s(X)) -> active#(X), active#(incr(X)) -> active#(X))
                (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
                (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
                (active#(cons(X1, X2)) -> active#(X1), active#(incr(X)) -> active#(X))
                (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
                (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))}
               SCCS:
                Scc:
                 {     active#(incr(X)) -> active#(X),
                  active#(cons(X1, X2)) -> active#(X1),
                          active#(s(X)) -> active#(X)}
                SCC:
                 Strict:
                  {     active#(incr(X)) -> active#(X),
                   active#(cons(X1, X2)) -> active#(X1),
                           active#(s(X)) -> active#(X)}
                 Weak:
                 {         active(incr(X)) -> incr(active(X)),
                       active(incr(nil())) -> mark(nil()),
                  active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
                      active(cons(X1, X2)) -> cons(active(X1), X2),
                              active(s(X)) -> s(active(X)),
                            active(adx(X)) -> adx(active(X)),
                        active(adx(nil())) -> mark(nil()),
                   active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
                           active(zeros()) -> mark(cons(0(), zeros())),
                            active(nats()) -> mark(adx(zeros())),
                           active(head(X)) -> head(active(X)),
                  active(head(cons(X, L))) -> mark(X),
                           active(tail(X)) -> tail(active(X)),
                  active(tail(cons(X, L))) -> mark(L),
                             incr(mark(X)) -> mark(incr(X)),
                               incr(ok(X)) -> ok(incr(X)),
                        cons(mark(X1), X2) -> mark(cons(X1, X2)),
                      cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                s(mark(X)) -> mark(s(X)),
                                  s(ok(X)) -> ok(s(X)),
                              adx(mark(X)) -> mark(adx(X)),
                                adx(ok(X)) -> ok(adx(X)),
                             head(mark(X)) -> mark(head(X)),
                               head(ok(X)) -> ok(head(X)),
                             tail(mark(X)) -> mark(tail(X)),
                               tail(ok(X)) -> ok(tail(X)),
                             proper(nil()) -> ok(nil()),
                           proper(incr(X)) -> incr(proper(X)),
                      proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                              proper(s(X)) -> s(proper(X)),
                            proper(adx(X)) -> adx(proper(X)),
                           proper(zeros()) -> ok(zeros()),
                            proper(nats()) -> ok(nats()),
                               proper(0()) -> ok(0()),
                           proper(head(X)) -> head(proper(X)),
                           proper(tail(X)) -> tail(proper(X)),
                              top(mark(X)) -> top(proper(X)),
                                top(ok(X)) -> top(active(X))}
                 SPSC:
                  Simple Projection:
                   pi(active#) = 0
                  Strict:
                   {active#(incr(X)) -> active#(X),
                       active#(s(X)) -> active#(X)}
                  EDG:
                   {(active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
                    (active#(s(X)) -> active#(X), active#(incr(X)) -> active#(X))
                    (active#(incr(X)) -> active#(X), active#(incr(X)) -> active#(X))
                    (active#(incr(X)) -> active#(X), active#(s(X)) -> active#(X))}
                   SCCS:
                    Scc:
                     {active#(incr(X)) -> active#(X),
                         active#(s(X)) -> active#(X)}
                    SCC:
                     Strict:
                      {active#(incr(X)) -> active#(X),
                          active#(s(X)) -> active#(X)}
                     Weak:
                     {         active(incr(X)) -> incr(active(X)),
                           active(incr(nil())) -> mark(nil()),
                      active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
                          active(cons(X1, X2)) -> cons(active(X1), X2),
                                  active(s(X)) -> s(active(X)),
                                active(adx(X)) -> adx(active(X)),
                            active(adx(nil())) -> mark(nil()),
                       active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
                               active(zeros()) -> mark(cons(0(), zeros())),
                                active(nats()) -> mark(adx(zeros())),
                               active(head(X)) -> head(active(X)),
                      active(head(cons(X, L))) -> mark(X),
                               active(tail(X)) -> tail(active(X)),
                      active(tail(cons(X, L))) -> mark(L),
                                 incr(mark(X)) -> mark(incr(X)),
                                   incr(ok(X)) -> ok(incr(X)),
                            cons(mark(X1), X2) -> mark(cons(X1, X2)),
                          cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                    s(mark(X)) -> mark(s(X)),
                                      s(ok(X)) -> ok(s(X)),
                                  adx(mark(X)) -> mark(adx(X)),
                                    adx(ok(X)) -> ok(adx(X)),
                                 head(mark(X)) -> mark(head(X)),
                                   head(ok(X)) -> ok(head(X)),
                                 tail(mark(X)) -> mark(tail(X)),
                                   tail(ok(X)) -> ok(tail(X)),
                                 proper(nil()) -> ok(nil()),
                               proper(incr(X)) -> incr(proper(X)),
                          proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                  proper(s(X)) -> s(proper(X)),
                                proper(adx(X)) -> adx(proper(X)),
                               proper(zeros()) -> ok(zeros()),
                                proper(nats()) -> ok(nats()),
                                   proper(0()) -> ok(0()),
                               proper(head(X)) -> head(proper(X)),
                               proper(tail(X)) -> tail(proper(X)),
                                  top(mark(X)) -> top(proper(X)),
                                    top(ok(X)) -> top(active(X))}
                     SPSC:
                      Simple Projection:
                       pi(active#) = 0
                      Strict:
                       {active#(s(X)) -> active#(X)}
                      EDG:
                       {(active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))}
                       SCCS:
                        Scc:
                         {active#(s(X)) -> active#(X)}
                        SCC:
                         Strict:
                          {active#(s(X)) -> active#(X)}
                         Weak:
                         {         active(incr(X)) -> incr(active(X)),
                               active(incr(nil())) -> mark(nil()),
                          active(incr(cons(X, L))) -> mark(cons(s(X), incr(L))),
                              active(cons(X1, X2)) -> cons(active(X1), X2),
                                      active(s(X)) -> s(active(X)),
                                    active(adx(X)) -> adx(active(X)),
                                active(adx(nil())) -> mark(nil()),
                           active(adx(cons(X, L))) -> mark(incr(cons(X, adx(L)))),
                                   active(zeros()) -> mark(cons(0(), zeros())),
                                    active(nats()) -> mark(adx(zeros())),
                                   active(head(X)) -> head(active(X)),
                          active(head(cons(X, L))) -> mark(X),
                                   active(tail(X)) -> tail(active(X)),
                          active(tail(cons(X, L))) -> mark(L),
                                     incr(mark(X)) -> mark(incr(X)),
                                       incr(ok(X)) -> ok(incr(X)),
                                cons(mark(X1), X2) -> mark(cons(X1, X2)),
                              cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                        s(mark(X)) -> mark(s(X)),
                                          s(ok(X)) -> ok(s(X)),
                                      adx(mark(X)) -> mark(adx(X)),
                                        adx(ok(X)) -> ok(adx(X)),
                                     head(mark(X)) -> mark(head(X)),
                                       head(ok(X)) -> ok(head(X)),
                                     tail(mark(X)) -> mark(tail(X)),
                                       tail(ok(X)) -> ok(tail(X)),
                                     proper(nil()) -> ok(nil()),
                                   proper(incr(X)) -> incr(proper(X)),
                              proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                      proper(s(X)) -> s(proper(X)),
                                    proper(adx(X)) -> adx(proper(X)),
                                   proper(zeros()) -> ok(zeros()),
                                    proper(nats()) -> ok(nats()),
                                       proper(0()) -> ok(0()),
                                   proper(head(X)) -> head(proper(X)),
                                   proper(tail(X)) -> tail(proper(X)),
                                      top(mark(X)) -> top(proper(X)),
                                        top(ok(X)) -> top(active(X))}
                         SPSC:
                          Simple Projection:
                           pi(active#) = 0
                          Strict:
                           {}
                          Qed