MAYBE
TRS:
 {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
       cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
              incr(mark(X)) -> mark(incr(X)),
                incr(ok(X)) -> ok(incr(X)),
       active(cons(X1, X2)) -> cons(active(X1), X2),
            active(incr(X)) -> incr(active(X)),
  active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
             active(nats()) -> mark(cons(0(), incr(nats()))),
             active(odds()) -> mark(incr(pairs())),
            active(pairs()) -> mark(cons(0(), incr(odds()))),
               active(s(X)) -> s(active(X)),
            active(head(X)) -> head(active(X)),
  active(head(cons(X, XS))) -> mark(X),
            active(tail(X)) -> tail(active(X)),
  active(tail(cons(X, XS))) -> mark(XS),
                 s(mark(X)) -> mark(s(X)),
                   s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                proper(0()) -> ok(0()),
            proper(incr(X)) -> incr(proper(X)),
             proper(nats()) -> ok(nats()),
             proper(odds()) -> ok(odds()),
            proper(pairs()) -> ok(pairs()),
               proper(s(X)) -> s(proper(X)),
            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:
   {       cons#(mark(X1), X2) -> cons#(X1, X2),
         cons#(ok(X1), ok(X2)) -> cons#(X1, X2),
                incr#(mark(X)) -> incr#(X),
                  incr#(ok(X)) -> incr#(X),
         active#(cons(X1, X2)) -> cons#(active(X1), X2),
         active#(cons(X1, X2)) -> active#(X1),
              active#(incr(X)) -> incr#(active(X)),
              active#(incr(X)) -> active#(X),
    active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS)),
    active#(incr(cons(X, XS))) -> incr#(XS),
    active#(incr(cons(X, XS))) -> s#(X),
               active#(nats()) -> cons#(0(), incr(nats())),
               active#(nats()) -> incr#(nats()),
               active#(odds()) -> incr#(pairs()),
              active#(pairs()) -> cons#(0(), incr(odds())),
              active#(pairs()) -> incr#(odds()),
                 active#(s(X)) -> active#(X),
                 active#(s(X)) -> s#(active(X)),
              active#(head(X)) -> active#(X),
              active#(head(X)) -> head#(active(X)),
              active#(tail(X)) -> active#(X),
              active#(tail(X)) -> tail#(active(X)),
                   s#(mark(X)) -> s#(X),
                     s#(ok(X)) -> s#(X),
                head#(mark(X)) -> head#(X),
                  head#(ok(X)) -> head#(X),
                tail#(mark(X)) -> tail#(X),
                  tail#(ok(X)) -> tail#(X),
         proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)),
         proper#(cons(X1, X2)) -> proper#(X1),
         proper#(cons(X1, X2)) -> proper#(X2),
              proper#(incr(X)) -> incr#(proper(X)),
              proper#(incr(X)) -> proper#(X),
                 proper#(s(X)) -> s#(proper(X)),
                 proper#(s(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:
  {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
        cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
               incr(mark(X)) -> mark(incr(X)),
                 incr(ok(X)) -> ok(incr(X)),
        active(cons(X1, X2)) -> cons(active(X1), X2),
             active(incr(X)) -> incr(active(X)),
   active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
              active(nats()) -> mark(cons(0(), incr(nats()))),
              active(odds()) -> mark(incr(pairs())),
             active(pairs()) -> mark(cons(0(), incr(odds()))),
                active(s(X)) -> s(active(X)),
             active(head(X)) -> head(active(X)),
   active(head(cons(X, XS))) -> mark(X),
             active(tail(X)) -> tail(active(X)),
   active(tail(cons(X, XS))) -> mark(XS),
                  s(mark(X)) -> mark(s(X)),
                    s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                 proper(0()) -> ok(0()),
             proper(incr(X)) -> incr(proper(X)),
              proper(nats()) -> ok(nats()),
              proper(odds()) -> ok(odds()),
             proper(pairs()) -> ok(pairs()),
                proper(s(X)) -> s(proper(X)),
             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:
   {
    (proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)), cons#(mark(X1), X2) -> cons#(X1, X2))
    (active#(incr(cons(X, XS))) -> incr#(XS), incr#(ok(X)) -> incr#(X))
    (active#(incr(cons(X, XS))) -> incr#(XS), incr#(mark(X)) -> incr#(X))
    (incr#(ok(X)) -> incr#(X), incr#(ok(X)) -> incr#(X))
    (incr#(ok(X)) -> incr#(X), incr#(mark(X)) -> incr#(X))
    (active#(incr(cons(X, XS))) -> s#(X), s#(ok(X)) -> s#(X))
    (active#(incr(cons(X, XS))) -> s#(X), s#(mark(X)) -> s#(X))
    (active#(head(X)) -> active#(X), active#(tail(X)) -> tail#(active(X)))
    (active#(head(X)) -> active#(X), active#(tail(X)) -> active#(X))
    (active#(head(X)) -> active#(X), active#(head(X)) -> head#(active(X)))
    (active#(head(X)) -> active#(X), active#(head(X)) -> active#(X))
    (active#(head(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(head(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(head(X)) -> active#(X), active#(pairs()) -> incr#(odds()))
    (active#(head(X)) -> active#(X), active#(pairs()) -> cons#(0(), incr(odds())))
    (active#(head(X)) -> active#(X), active#(odds()) -> incr#(pairs()))
    (active#(head(X)) -> active#(X), active#(nats()) -> incr#(nats()))
    (active#(head(X)) -> active#(X), active#(nats()) -> cons#(0(), incr(nats())))
    (active#(head(X)) -> active#(X), active#(incr(cons(X, XS))) -> s#(X))
    (active#(head(X)) -> active#(X), active#(incr(cons(X, XS))) -> incr#(XS))
    (active#(head(X)) -> active#(X), active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS)))
    (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#(cons(X1, X2)) -> active#(X1))
    (active#(head(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X))
    (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (head#(mark(X)) -> head#(X), head#(ok(X)) -> head#(X))
    (head#(mark(X)) -> head#(X), head#(mark(X)) -> head#(X))
    (tail#(mark(X)) -> tail#(X), tail#(ok(X)) -> tail#(X))
    (tail#(mark(X)) -> tail#(X), tail#(mark(X)) -> tail#(X))
    (proper#(incr(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))
    (proper#(incr(X)) -> proper#(X), proper#(tail(X)) -> tail#(proper(X)))
    (proper#(incr(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
    (proper#(incr(X)) -> proper#(X), proper#(head(X)) -> head#(proper(X)))
    (proper#(incr(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(incr(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(incr(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
    (proper#(incr(X)) -> proper#(X), proper#(incr(X)) -> incr#(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#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (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#(s(X)) -> proper#(X))
    (proper#(head(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(head(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
    (proper#(head(X)) -> proper#(X), proper#(incr(X)) -> incr#(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)))
    (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#(s(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(incr(X)) -> incr#(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)))
    (active#(incr(X)) -> incr#(active(X)), incr#(ok(X)) -> incr#(X))
    (active#(incr(X)) -> incr#(active(X)), incr#(mark(X)) -> incr#(X))
    (active#(head(X)) -> head#(active(X)), head#(ok(X)) -> head#(X))
    (active#(head(X)) -> head#(active(X)), head#(mark(X)) -> head#(X))
    (proper#(incr(X)) -> incr#(proper(X)), incr#(ok(X)) -> incr#(X))
    (proper#(incr(X)) -> incr#(proper(X)), incr#(mark(X)) -> incr#(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#(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))
    (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))
    (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#(s(X)) -> s#(active(X)))
    (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(pairs()) -> incr#(odds()))
    (active#(cons(X1, X2)) -> active#(X1), active#(pairs()) -> cons#(0(), incr(odds())))
    (active#(cons(X1, X2)) -> active#(X1), active#(odds()) -> incr#(pairs()))
    (active#(cons(X1, X2)) -> active#(X1), active#(nats()) -> incr#(nats()))
    (active#(cons(X1, X2)) -> active#(X1), active#(nats()) -> cons#(0(), incr(nats())))
    (active#(cons(X1, X2)) -> active#(X1), active#(incr(cons(X, XS))) -> s#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(incr(cons(X, XS))) -> incr#(XS))
    (active#(cons(X1, X2)) -> active#(X1), active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS)))
    (active#(cons(X1, X2)) -> active#(X1), active#(incr(X)) -> active#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(incr(X)) -> incr#(active(X)))
    (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
    (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (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#(incr(X)) -> incr#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(incr(X)) -> proper#(X))
    (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#(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))
    (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))
    (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#(incr(X)) -> incr#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(incr(X)) -> proper#(X))
    (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#(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#(s(X)) -> s#(proper(X)), s#(mark(X)) -> s#(X))
    (proper#(s(X)) -> s#(proper(X)), s#(ok(X)) -> s#(X))
    (active#(tail(X)) -> tail#(active(X)), tail#(mark(X)) -> tail#(X))
    (active#(tail(X)) -> tail#(active(X)), tail#(ok(X)) -> tail#(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#(cons(X1, X2)) -> cons#(active(X1), X2))
    (top#(ok(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (top#(ok(X)) -> active#(X), active#(incr(X)) -> incr#(active(X)))
    (top#(ok(X)) -> active#(X), active#(incr(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS)))
    (top#(ok(X)) -> active#(X), active#(incr(cons(X, XS))) -> incr#(XS))
    (top#(ok(X)) -> active#(X), active#(incr(cons(X, XS))) -> s#(X))
    (top#(ok(X)) -> active#(X), active#(nats()) -> cons#(0(), incr(nats())))
    (top#(ok(X)) -> active#(X), active#(nats()) -> incr#(nats()))
    (top#(ok(X)) -> active#(X), active#(odds()) -> incr#(pairs()))
    (top#(ok(X)) -> active#(X), active#(pairs()) -> cons#(0(), incr(odds())))
    (top#(ok(X)) -> active#(X), active#(pairs()) -> incr#(odds()))
    (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#(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#(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#(incr(X)) -> incr#(proper(X)))
    (proper#(tail(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
    (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#(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#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (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#(incr(X)) -> incr#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(incr(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(head(X)) -> head#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(tail(X)) -> tail#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))
    (tail#(ok(X)) -> tail#(X), tail#(mark(X)) -> tail#(X))
    (tail#(ok(X)) -> tail#(X), tail#(ok(X)) -> tail#(X))
    (head#(ok(X)) -> head#(X), head#(mark(X)) -> head#(X))
    (head#(ok(X)) -> head#(X), head#(ok(X)) -> head#(X))
    (s#(ok(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (s#(ok(X)) -> s#(X), s#(ok(X)) -> s#(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(X)) -> incr#(active(X)))
    (active#(tail(X)) -> active#(X), active#(incr(X)) -> active#(X))
    (active#(tail(X)) -> active#(X), active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS)))
    (active#(tail(X)) -> active#(X), active#(incr(cons(X, XS))) -> incr#(XS))
    (active#(tail(X)) -> active#(X), active#(incr(cons(X, XS))) -> s#(X))
    (active#(tail(X)) -> active#(X), active#(nats()) -> cons#(0(), incr(nats())))
    (active#(tail(X)) -> active#(X), active#(nats()) -> incr#(nats()))
    (active#(tail(X)) -> active#(X), active#(odds()) -> incr#(pairs()))
    (active#(tail(X)) -> active#(X), active#(pairs()) -> cons#(0(), incr(odds())))
    (active#(tail(X)) -> active#(X), active#(pairs()) -> incr#(odds()))
    (active#(tail(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(tail(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(tail(X)) -> active#(X), active#(head(X)) -> active#(X))
    (active#(tail(X)) -> active#(X), active#(head(X)) -> head#(active(X)))
    (active#(tail(X)) -> active#(X), active#(tail(X)) -> active#(X))
    (active#(tail(X)) -> active#(X), active#(tail(X)) -> tail#(active(X)))
    (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (active#(s(X)) -> active#(X), active#(incr(X)) -> incr#(active(X)))
    (active#(s(X)) -> active#(X), active#(incr(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS)))
    (active#(s(X)) -> active#(X), active#(incr(cons(X, XS))) -> incr#(XS))
    (active#(s(X)) -> active#(X), active#(incr(cons(X, XS))) -> s#(X))
    (active#(s(X)) -> active#(X), active#(nats()) -> cons#(0(), incr(nats())))
    (active#(s(X)) -> active#(X), active#(nats()) -> incr#(nats()))
    (active#(s(X)) -> active#(X), active#(odds()) -> incr#(pairs()))
    (active#(s(X)) -> active#(X), active#(pairs()) -> cons#(0(), incr(odds())))
    (active#(s(X)) -> active#(X), active#(pairs()) -> incr#(odds()))
    (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#(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#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(incr(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (active#(incr(X)) -> active#(X), active#(incr(X)) -> incr#(active(X)))
    (active#(incr(X)) -> active#(X), active#(incr(X)) -> active#(X))
    (active#(incr(X)) -> active#(X), active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS)))
    (active#(incr(X)) -> active#(X), active#(incr(cons(X, XS))) -> incr#(XS))
    (active#(incr(X)) -> active#(X), active#(incr(cons(X, XS))) -> s#(X))
    (active#(incr(X)) -> active#(X), active#(nats()) -> cons#(0(), incr(nats())))
    (active#(incr(X)) -> active#(X), active#(nats()) -> incr#(nats()))
    (active#(incr(X)) -> active#(X), active#(odds()) -> incr#(pairs()))
    (active#(incr(X)) -> active#(X), active#(pairs()) -> cons#(0(), incr(odds())))
    (active#(incr(X)) -> active#(X), active#(pairs()) -> incr#(odds()))
    (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#(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)))
    (incr#(mark(X)) -> incr#(X), incr#(mark(X)) -> incr#(X))
    (incr#(mark(X)) -> incr#(X), incr#(ok(X)) -> incr#(X))
    (active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS)), cons#(mark(X1), X2) -> cons#(X1, X2))
    (active#(incr(cons(X, XS))) -> cons#(s(X), incr(XS)), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
   }
   SCCS:
    Scc:
     {top#(mark(X)) -> top#(proper(X)),
        top#(ok(X)) -> top#(active(X))}
    Scc:
     {proper#(cons(X1, X2)) -> proper#(X1),
      proper#(cons(X1, X2)) -> proper#(X2),
           proper#(incr(X)) -> proper#(X),
              proper#(s(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:
     {s#(mark(X)) -> s#(X),
        s#(ok(X)) -> s#(X)}
    Scc:
     {active#(cons(X1, X2)) -> active#(X1),
           active#(incr(X)) -> active#(X),
              active#(s(X)) -> active#(X),
           active#(head(X)) -> active#(X),
           active#(tail(X)) -> active#(X)}
    Scc:
     {incr#(mark(X)) -> incr#(X),
        incr#(ok(X)) -> incr#(X)}
    Scc:
     {  cons#(mark(X1), X2) -> cons#(X1, X2),
      cons#(ok(X1), ok(X2)) -> cons#(X1, X2)}
    SCC:
     Strict:
      {top#(mark(X)) -> top#(proper(X)),
         top#(ok(X)) -> top#(active(X))}
     Weak:
     {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
           cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                  incr(mark(X)) -> mark(incr(X)),
                    incr(ok(X)) -> ok(incr(X)),
           active(cons(X1, X2)) -> cons(active(X1), X2),
                active(incr(X)) -> incr(active(X)),
      active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                 active(nats()) -> mark(cons(0(), incr(nats()))),
                 active(odds()) -> mark(incr(pairs())),
                active(pairs()) -> mark(cons(0(), incr(odds()))),
                   active(s(X)) -> s(active(X)),
                active(head(X)) -> head(active(X)),
      active(head(cons(X, XS))) -> mark(X),
                active(tail(X)) -> tail(active(X)),
      active(tail(cons(X, XS))) -> mark(XS),
                     s(mark(X)) -> mark(s(X)),
                       s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                    proper(0()) -> ok(0()),
                proper(incr(X)) -> incr(proper(X)),
                 proper(nats()) -> ok(nats()),
                 proper(odds()) -> ok(odds()),
                proper(pairs()) -> ok(pairs()),
                   proper(s(X)) -> s(proper(X)),
                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#(cons(X1, X2)) -> proper#(X1),
       proper#(cons(X1, X2)) -> proper#(X2),
            proper#(incr(X)) -> proper#(X),
               proper#(s(X)) -> proper#(X),
            proper#(head(X)) -> proper#(X),
            proper#(tail(X)) -> proper#(X)}
     Weak:
     {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
           cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                  incr(mark(X)) -> mark(incr(X)),
                    incr(ok(X)) -> ok(incr(X)),
           active(cons(X1, X2)) -> cons(active(X1), X2),
                active(incr(X)) -> incr(active(X)),
      active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                 active(nats()) -> mark(cons(0(), incr(nats()))),
                 active(odds()) -> mark(incr(pairs())),
                active(pairs()) -> mark(cons(0(), incr(odds()))),
                   active(s(X)) -> s(active(X)),
                active(head(X)) -> head(active(X)),
      active(head(cons(X, XS))) -> mark(X),
                active(tail(X)) -> tail(active(X)),
      active(tail(cons(X, XS))) -> mark(XS),
                     s(mark(X)) -> mark(s(X)),
                       s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                    proper(0()) -> ok(0()),
                proper(incr(X)) -> incr(proper(X)),
                 proper(nats()) -> ok(nats()),
                 proper(odds()) -> ok(odds()),
                proper(pairs()) -> ok(pairs()),
                   proper(s(X)) -> s(proper(X)),
                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#(cons(X1, X2)) -> proper#(X1),
        proper#(cons(X1, X2)) -> proper#(X2),
             proper#(incr(X)) -> proper#(X),
             proper#(head(X)) -> proper#(X),
             proper#(tail(X)) -> proper#(X)}
      EDG:
       {(proper#(head(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))
        (proper#(head(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
        (proper#(head(X)) -> proper#(X), proper#(incr(X)) -> 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#(cons(X1, X2)) -> proper#(X1), proper#(tail(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(head(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#(X2))
        (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#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(incr(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(head(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(tail(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#(incr(X)) -> proper#(X))
        (proper#(tail(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
        (proper#(tail(X)) -> proper#(X), proper#(tail(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#(incr(X)) -> proper#(X))
        (proper#(incr(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
        (proper#(incr(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))}
       SCCS:
        Scc:
         {proper#(cons(X1, X2)) -> proper#(X1),
          proper#(cons(X1, X2)) -> proper#(X2),
               proper#(incr(X)) -> proper#(X),
               proper#(head(X)) -> proper#(X),
               proper#(tail(X)) -> proper#(X)}
        SCC:
         Strict:
          {proper#(cons(X1, X2)) -> proper#(X1),
           proper#(cons(X1, X2)) -> proper#(X2),
                proper#(incr(X)) -> proper#(X),
                proper#(head(X)) -> proper#(X),
                proper#(tail(X)) -> proper#(X)}
         Weak:
         {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
               cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                      incr(mark(X)) -> mark(incr(X)),
                        incr(ok(X)) -> ok(incr(X)),
               active(cons(X1, X2)) -> cons(active(X1), X2),
                    active(incr(X)) -> incr(active(X)),
          active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                     active(nats()) -> mark(cons(0(), incr(nats()))),
                     active(odds()) -> mark(incr(pairs())),
                    active(pairs()) -> mark(cons(0(), incr(odds()))),
                       active(s(X)) -> s(active(X)),
                    active(head(X)) -> head(active(X)),
          active(head(cons(X, XS))) -> mark(X),
                    active(tail(X)) -> tail(active(X)),
          active(tail(cons(X, XS))) -> mark(XS),
                         s(mark(X)) -> mark(s(X)),
                           s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                        proper(0()) -> ok(0()),
                    proper(incr(X)) -> incr(proper(X)),
                     proper(nats()) -> ok(nats()),
                     proper(odds()) -> ok(odds()),
                    proper(pairs()) -> ok(pairs()),
                       proper(s(X)) -> s(proper(X)),
                    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#(cons(X1, X2)) -> proper#(X1),
            proper#(cons(X1, X2)) -> proper#(X2),
                 proper#(incr(X)) -> proper#(X),
                 proper#(tail(X)) -> proper#(X)}
          EDG:
           {(proper#(tail(X)) -> proper#(X), 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#(X2))
            (proper#(tail(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(cons(X1, X2)) -> proper#(X2), proper#(tail(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#(X2))
            (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#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(incr(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(tail(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#(incr(X)) -> proper#(X))
            (proper#(incr(X)) -> proper#(X), proper#(tail(X)) -> proper#(X))}
           SCCS:
            Scc:
             {proper#(cons(X1, X2)) -> proper#(X1),
              proper#(cons(X1, X2)) -> proper#(X2),
                   proper#(incr(X)) -> proper#(X),
                   proper#(tail(X)) -> proper#(X)}
            SCC:
             Strict:
              {proper#(cons(X1, X2)) -> proper#(X1),
               proper#(cons(X1, X2)) -> proper#(X2),
                    proper#(incr(X)) -> proper#(X),
                    proper#(tail(X)) -> proper#(X)}
             Weak:
             {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
                   cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                          incr(mark(X)) -> mark(incr(X)),
                            incr(ok(X)) -> ok(incr(X)),
                   active(cons(X1, X2)) -> cons(active(X1), X2),
                        active(incr(X)) -> incr(active(X)),
              active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                         active(nats()) -> mark(cons(0(), incr(nats()))),
                         active(odds()) -> mark(incr(pairs())),
                        active(pairs()) -> mark(cons(0(), incr(odds()))),
                           active(s(X)) -> s(active(X)),
                        active(head(X)) -> head(active(X)),
              active(head(cons(X, XS))) -> mark(X),
                        active(tail(X)) -> tail(active(X)),
              active(tail(cons(X, XS))) -> mark(XS),
                             s(mark(X)) -> mark(s(X)),
                               s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                            proper(0()) -> ok(0()),
                        proper(incr(X)) -> incr(proper(X)),
                         proper(nats()) -> ok(nats()),
                         proper(odds()) -> ok(odds()),
                        proper(pairs()) -> ok(pairs()),
                           proper(s(X)) -> s(proper(X)),
                        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#(cons(X1, X2)) -> proper#(X1),
                proper#(cons(X1, X2)) -> proper#(X2),
                     proper#(tail(X)) -> proper#(X)}
              EDG:
               {(proper#(cons(X1, X2)) -> proper#(X1), proper#(tail(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#(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#(tail(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#(tail(X)) -> proper#(X))}
               SCCS:
                Scc:
                 {proper#(cons(X1, X2)) -> proper#(X1),
                  proper#(cons(X1, X2)) -> proper#(X2),
                       proper#(tail(X)) -> proper#(X)}
                SCC:
                 Strict:
                  {proper#(cons(X1, X2)) -> proper#(X1),
                   proper#(cons(X1, X2)) -> proper#(X2),
                        proper#(tail(X)) -> proper#(X)}
                 Weak:
                 {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
                       cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                              incr(mark(X)) -> mark(incr(X)),
                                incr(ok(X)) -> ok(incr(X)),
                       active(cons(X1, X2)) -> cons(active(X1), X2),
                            active(incr(X)) -> incr(active(X)),
                  active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                             active(nats()) -> mark(cons(0(), incr(nats()))),
                             active(odds()) -> mark(incr(pairs())),
                            active(pairs()) -> mark(cons(0(), incr(odds()))),
                               active(s(X)) -> s(active(X)),
                            active(head(X)) -> head(active(X)),
                  active(head(cons(X, XS))) -> mark(X),
                            active(tail(X)) -> tail(active(X)),
                  active(tail(cons(X, XS))) -> mark(XS),
                                 s(mark(X)) -> mark(s(X)),
                                   s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                proper(0()) -> ok(0()),
                            proper(incr(X)) -> incr(proper(X)),
                             proper(nats()) -> ok(nats()),
                             proper(odds()) -> ok(odds()),
                            proper(pairs()) -> ok(pairs()),
                               proper(s(X)) -> s(proper(X)),
                            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#(cons(X1, X2)) -> proper#(X1),
                    proper#(cons(X1, X2)) -> proper#(X2)}
                  EDG:
                   {(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#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))}
                   SCCS:
                    Scc:
                     {proper#(cons(X1, X2)) -> proper#(X1),
                      proper#(cons(X1, X2)) -> proper#(X2)}
                    SCC:
                     Strict:
                      {proper#(cons(X1, X2)) -> proper#(X1),
                       proper#(cons(X1, X2)) -> proper#(X2)}
                     Weak:
                     {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
                           cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                  incr(mark(X)) -> mark(incr(X)),
                                    incr(ok(X)) -> ok(incr(X)),
                           active(cons(X1, X2)) -> cons(active(X1), X2),
                                active(incr(X)) -> incr(active(X)),
                      active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                                 active(nats()) -> mark(cons(0(), incr(nats()))),
                                 active(odds()) -> mark(incr(pairs())),
                                active(pairs()) -> mark(cons(0(), incr(odds()))),
                                   active(s(X)) -> s(active(X)),
                                active(head(X)) -> head(active(X)),
                      active(head(cons(X, XS))) -> mark(X),
                                active(tail(X)) -> tail(active(X)),
                      active(tail(cons(X, XS))) -> mark(XS),
                                     s(mark(X)) -> mark(s(X)),
                                       s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                    proper(0()) -> ok(0()),
                                proper(incr(X)) -> incr(proper(X)),
                                 proper(nats()) -> ok(nats()),
                                 proper(odds()) -> ok(odds()),
                                proper(pairs()) -> ok(pairs()),
                                   proper(s(X)) -> s(proper(X)),
                                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#(cons(X1, X2)) -> proper#(X2)}
                      EDG:
                       {(proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))}
                       SCCS:
                        Scc:
                         {proper#(cons(X1, X2)) -> proper#(X2)}
                        SCC:
                         Strict:
                          {proper#(cons(X1, X2)) -> proper#(X2)}
                         Weak:
                         {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
                               cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                      incr(mark(X)) -> mark(incr(X)),
                                        incr(ok(X)) -> ok(incr(X)),
                               active(cons(X1, X2)) -> cons(active(X1), X2),
                                    active(incr(X)) -> incr(active(X)),
                          active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                                     active(nats()) -> mark(cons(0(), incr(nats()))),
                                     active(odds()) -> mark(incr(pairs())),
                                    active(pairs()) -> mark(cons(0(), incr(odds()))),
                                       active(s(X)) -> s(active(X)),
                                    active(head(X)) -> head(active(X)),
                          active(head(cons(X, XS))) -> mark(X),
                                    active(tail(X)) -> tail(active(X)),
                          active(tail(cons(X, XS))) -> mark(XS),
                                         s(mark(X)) -> mark(s(X)),
                                           s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                        proper(0()) -> ok(0()),
                                    proper(incr(X)) -> incr(proper(X)),
                                     proper(nats()) -> ok(nats()),
                                     proper(odds()) -> ok(odds()),
                                    proper(pairs()) -> ok(pairs()),
                                       proper(s(X)) -> s(proper(X)),
                                    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:
     {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
           cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                  incr(mark(X)) -> mark(incr(X)),
                    incr(ok(X)) -> ok(incr(X)),
           active(cons(X1, X2)) -> cons(active(X1), X2),
                active(incr(X)) -> incr(active(X)),
      active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                 active(nats()) -> mark(cons(0(), incr(nats()))),
                 active(odds()) -> mark(incr(pairs())),
                active(pairs()) -> mark(cons(0(), incr(odds()))),
                   active(s(X)) -> s(active(X)),
                active(head(X)) -> head(active(X)),
      active(head(cons(X, XS))) -> mark(X),
                active(tail(X)) -> tail(active(X)),
      active(tail(cons(X, XS))) -> mark(XS),
                     s(mark(X)) -> mark(s(X)),
                       s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                    proper(0()) -> ok(0()),
                proper(incr(X)) -> incr(proper(X)),
                 proper(nats()) -> ok(nats()),
                 proper(odds()) -> ok(odds()),
                proper(pairs()) -> ok(pairs()),
                   proper(s(X)) -> s(proper(X)),
                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:
         {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
               cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                      incr(mark(X)) -> mark(incr(X)),
                        incr(ok(X)) -> ok(incr(X)),
               active(cons(X1, X2)) -> cons(active(X1), X2),
                    active(incr(X)) -> incr(active(X)),
          active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                     active(nats()) -> mark(cons(0(), incr(nats()))),
                     active(odds()) -> mark(incr(pairs())),
                    active(pairs()) -> mark(cons(0(), incr(odds()))),
                       active(s(X)) -> s(active(X)),
                    active(head(X)) -> head(active(X)),
          active(head(cons(X, XS))) -> mark(X),
                    active(tail(X)) -> tail(active(X)),
          active(tail(cons(X, XS))) -> mark(XS),
                         s(mark(X)) -> mark(s(X)),
                           s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                        proper(0()) -> ok(0()),
                    proper(incr(X)) -> incr(proper(X)),
                     proper(nats()) -> ok(nats()),
                     proper(odds()) -> ok(odds()),
                    proper(pairs()) -> ok(pairs()),
                       proper(s(X)) -> s(proper(X)),
                    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:
     {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
           cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                  incr(mark(X)) -> mark(incr(X)),
                    incr(ok(X)) -> ok(incr(X)),
           active(cons(X1, X2)) -> cons(active(X1), X2),
                active(incr(X)) -> incr(active(X)),
      active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                 active(nats()) -> mark(cons(0(), incr(nats()))),
                 active(odds()) -> mark(incr(pairs())),
                active(pairs()) -> mark(cons(0(), incr(odds()))),
                   active(s(X)) -> s(active(X)),
                active(head(X)) -> head(active(X)),
      active(head(cons(X, XS))) -> mark(X),
                active(tail(X)) -> tail(active(X)),
      active(tail(cons(X, XS))) -> mark(XS),
                     s(mark(X)) -> mark(s(X)),
                       s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                    proper(0()) -> ok(0()),
                proper(incr(X)) -> incr(proper(X)),
                 proper(nats()) -> ok(nats()),
                 proper(odds()) -> ok(odds()),
                proper(pairs()) -> ok(pairs()),
                   proper(s(X)) -> s(proper(X)),
                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:
         {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
               cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                      incr(mark(X)) -> mark(incr(X)),
                        incr(ok(X)) -> ok(incr(X)),
               active(cons(X1, X2)) -> cons(active(X1), X2),
                    active(incr(X)) -> incr(active(X)),
          active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                     active(nats()) -> mark(cons(0(), incr(nats()))),
                     active(odds()) -> mark(incr(pairs())),
                    active(pairs()) -> mark(cons(0(), incr(odds()))),
                       active(s(X)) -> s(active(X)),
                    active(head(X)) -> head(active(X)),
          active(head(cons(X, XS))) -> mark(X),
                    active(tail(X)) -> tail(active(X)),
          active(tail(cons(X, XS))) -> mark(XS),
                         s(mark(X)) -> mark(s(X)),
                           s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                        proper(0()) -> ok(0()),
                    proper(incr(X)) -> incr(proper(X)),
                     proper(nats()) -> ok(nats()),
                     proper(odds()) -> ok(odds()),
                    proper(pairs()) -> ok(pairs()),
                       proper(s(X)) -> s(proper(X)),
                    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:
      {s#(mark(X)) -> s#(X),
         s#(ok(X)) -> s#(X)}
     Weak:
     {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
           cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                  incr(mark(X)) -> mark(incr(X)),
                    incr(ok(X)) -> ok(incr(X)),
           active(cons(X1, X2)) -> cons(active(X1), X2),
                active(incr(X)) -> incr(active(X)),
      active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                 active(nats()) -> mark(cons(0(), incr(nats()))),
                 active(odds()) -> mark(incr(pairs())),
                active(pairs()) -> mark(cons(0(), incr(odds()))),
                   active(s(X)) -> s(active(X)),
                active(head(X)) -> head(active(X)),
      active(head(cons(X, XS))) -> mark(X),
                active(tail(X)) -> tail(active(X)),
      active(tail(cons(X, XS))) -> mark(XS),
                     s(mark(X)) -> mark(s(X)),
                       s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                    proper(0()) -> ok(0()),
                proper(incr(X)) -> incr(proper(X)),
                 proper(nats()) -> ok(nats()),
                 proper(odds()) -> ok(odds()),
                proper(pairs()) -> ok(pairs()),
                   proper(s(X)) -> s(proper(X)),
                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:
         {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
               cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                      incr(mark(X)) -> mark(incr(X)),
                        incr(ok(X)) -> ok(incr(X)),
               active(cons(X1, X2)) -> cons(active(X1), X2),
                    active(incr(X)) -> incr(active(X)),
          active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                     active(nats()) -> mark(cons(0(), incr(nats()))),
                     active(odds()) -> mark(incr(pairs())),
                    active(pairs()) -> mark(cons(0(), incr(odds()))),
                       active(s(X)) -> s(active(X)),
                    active(head(X)) -> head(active(X)),
          active(head(cons(X, XS))) -> mark(X),
                    active(tail(X)) -> tail(active(X)),
          active(tail(cons(X, XS))) -> mark(XS),
                         s(mark(X)) -> mark(s(X)),
                           s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                        proper(0()) -> ok(0()),
                    proper(incr(X)) -> incr(proper(X)),
                     proper(nats()) -> ok(nats()),
                     proper(odds()) -> ok(odds()),
                    proper(pairs()) -> ok(pairs()),
                       proper(s(X)) -> s(proper(X)),
                    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:
      {active#(cons(X1, X2)) -> active#(X1),
            active#(incr(X)) -> active#(X),
               active#(s(X)) -> active#(X),
            active#(head(X)) -> active#(X),
            active#(tail(X)) -> active#(X)}
     Weak:
     {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
           cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                  incr(mark(X)) -> mark(incr(X)),
                    incr(ok(X)) -> ok(incr(X)),
           active(cons(X1, X2)) -> cons(active(X1), X2),
                active(incr(X)) -> incr(active(X)),
      active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                 active(nats()) -> mark(cons(0(), incr(nats()))),
                 active(odds()) -> mark(incr(pairs())),
                active(pairs()) -> mark(cons(0(), incr(odds()))),
                   active(s(X)) -> s(active(X)),
                active(head(X)) -> head(active(X)),
      active(head(cons(X, XS))) -> mark(X),
                active(tail(X)) -> tail(active(X)),
      active(tail(cons(X, XS))) -> mark(XS),
                     s(mark(X)) -> mark(s(X)),
                       s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                    proper(0()) -> ok(0()),
                proper(incr(X)) -> incr(proper(X)),
                 proper(nats()) -> ok(nats()),
                 proper(odds()) -> ok(odds()),
                proper(pairs()) -> ok(pairs()),
                   proper(s(X)) -> s(proper(X)),
                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#(cons(X1, X2)) -> active#(X1),
             active#(incr(X)) -> active#(X),
                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#(incr(X)) -> active#(X))
        (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
        (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#(incr(X)) -> active#(X))
        (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
        (active#(tail(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
        (active#(tail(X)) -> active#(X), active#(incr(X)) -> active#(X))
        (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#(cons(X1, X2)) -> active#(X1))
        (active#(incr(X)) -> active#(X), active#(incr(X)) -> active#(X))
        (active#(incr(X)) -> active#(X), active#(s(X)) -> active#(X))
        (active#(incr(X)) -> active#(X), active#(tail(X)) -> active#(X))}
       SCCS:
        Scc:
         {active#(cons(X1, X2)) -> active#(X1),
               active#(incr(X)) -> active#(X),
                  active#(s(X)) -> active#(X),
               active#(tail(X)) -> active#(X)}
        SCC:
         Strict:
          {active#(cons(X1, X2)) -> active#(X1),
                active#(incr(X)) -> active#(X),
                   active#(s(X)) -> active#(X),
                active#(tail(X)) -> active#(X)}
         Weak:
         {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
               cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                      incr(mark(X)) -> mark(incr(X)),
                        incr(ok(X)) -> ok(incr(X)),
               active(cons(X1, X2)) -> cons(active(X1), X2),
                    active(incr(X)) -> incr(active(X)),
          active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                     active(nats()) -> mark(cons(0(), incr(nats()))),
                     active(odds()) -> mark(incr(pairs())),
                    active(pairs()) -> mark(cons(0(), incr(odds()))),
                       active(s(X)) -> s(active(X)),
                    active(head(X)) -> head(active(X)),
          active(head(cons(X, XS))) -> mark(X),
                    active(tail(X)) -> tail(active(X)),
          active(tail(cons(X, XS))) -> mark(XS),
                         s(mark(X)) -> mark(s(X)),
                           s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                        proper(0()) -> ok(0()),
                    proper(incr(X)) -> incr(proper(X)),
                     proper(nats()) -> ok(nats()),
                     proper(odds()) -> ok(odds()),
                    proper(pairs()) -> ok(pairs()),
                       proper(s(X)) -> s(proper(X)),
                    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#(cons(X1, X2)) -> active#(X1),
                 active#(incr(X)) -> active#(X),
                 active#(tail(X)) -> active#(X)}
          EDG:
           {(active#(incr(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#(tail(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
            (active#(tail(X)) -> active#(X), active#(incr(X)) -> active#(X))
            (active#(tail(X)) -> active#(X), active#(tail(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#(cons(X1, X2)) -> active#(X1), active#(tail(X)) -> active#(X))}
           SCCS:
            Scc:
             {active#(cons(X1, X2)) -> active#(X1),
                   active#(incr(X)) -> active#(X),
                   active#(tail(X)) -> active#(X)}
            SCC:
             Strict:
              {active#(cons(X1, X2)) -> active#(X1),
                    active#(incr(X)) -> active#(X),
                    active#(tail(X)) -> active#(X)}
             Weak:
             {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
                   cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                          incr(mark(X)) -> mark(incr(X)),
                            incr(ok(X)) -> ok(incr(X)),
                   active(cons(X1, X2)) -> cons(active(X1), X2),
                        active(incr(X)) -> incr(active(X)),
              active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                         active(nats()) -> mark(cons(0(), incr(nats()))),
                         active(odds()) -> mark(incr(pairs())),
                        active(pairs()) -> mark(cons(0(), incr(odds()))),
                           active(s(X)) -> s(active(X)),
                        active(head(X)) -> head(active(X)),
              active(head(cons(X, XS))) -> mark(X),
                        active(tail(X)) -> tail(active(X)),
              active(tail(cons(X, XS))) -> mark(XS),
                             s(mark(X)) -> mark(s(X)),
                               s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                            proper(0()) -> ok(0()),
                        proper(incr(X)) -> incr(proper(X)),
                         proper(nats()) -> ok(nats()),
                         proper(odds()) -> ok(odds()),
                        proper(pairs()) -> ok(pairs()),
                           proper(s(X)) -> s(proper(X)),
                        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#(cons(X1, X2)) -> active#(X1),
                     active#(incr(X)) -> active#(X)}
              EDG:
               {(active#(cons(X1, X2)) -> active#(X1), active#(incr(X)) -> active#(X))
                (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
                (active#(incr(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
                (active#(incr(X)) -> active#(X), active#(incr(X)) -> active#(X))}
               SCCS:
                Scc:
                 {active#(cons(X1, X2)) -> active#(X1),
                       active#(incr(X)) -> active#(X)}
                SCC:
                 Strict:
                  {active#(cons(X1, X2)) -> active#(X1),
                        active#(incr(X)) -> active#(X)}
                 Weak:
                 {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
                       cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                              incr(mark(X)) -> mark(incr(X)),
                                incr(ok(X)) -> ok(incr(X)),
                       active(cons(X1, X2)) -> cons(active(X1), X2),
                            active(incr(X)) -> incr(active(X)),
                  active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                             active(nats()) -> mark(cons(0(), incr(nats()))),
                             active(odds()) -> mark(incr(pairs())),
                            active(pairs()) -> mark(cons(0(), incr(odds()))),
                               active(s(X)) -> s(active(X)),
                            active(head(X)) -> head(active(X)),
                  active(head(cons(X, XS))) -> mark(X),
                            active(tail(X)) -> tail(active(X)),
                  active(tail(cons(X, XS))) -> mark(XS),
                                 s(mark(X)) -> mark(s(X)),
                                   s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                proper(0()) -> ok(0()),
                            proper(incr(X)) -> incr(proper(X)),
                             proper(nats()) -> ok(nats()),
                             proper(odds()) -> ok(odds()),
                            proper(pairs()) -> ok(pairs()),
                               proper(s(X)) -> s(proper(X)),
                            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)}
                  EDG:
                   {(active#(incr(X)) -> active#(X), active#(incr(X)) -> active#(X))}
                   SCCS:
                    Scc:
                     {active#(incr(X)) -> active#(X)}
                    SCC:
                     Strict:
                      {active#(incr(X)) -> active#(X)}
                     Weak:
                     {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
                           cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                  incr(mark(X)) -> mark(incr(X)),
                                    incr(ok(X)) -> ok(incr(X)),
                           active(cons(X1, X2)) -> cons(active(X1), X2),
                                active(incr(X)) -> incr(active(X)),
                      active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                                 active(nats()) -> mark(cons(0(), incr(nats()))),
                                 active(odds()) -> mark(incr(pairs())),
                                active(pairs()) -> mark(cons(0(), incr(odds()))),
                                   active(s(X)) -> s(active(X)),
                                active(head(X)) -> head(active(X)),
                      active(head(cons(X, XS))) -> mark(X),
                                active(tail(X)) -> tail(active(X)),
                      active(tail(cons(X, XS))) -> mark(XS),
                                     s(mark(X)) -> mark(s(X)),
                                       s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                    proper(0()) -> ok(0()),
                                proper(incr(X)) -> incr(proper(X)),
                                 proper(nats()) -> ok(nats()),
                                 proper(odds()) -> ok(odds()),
                                proper(pairs()) -> ok(pairs()),
                                   proper(s(X)) -> s(proper(X)),
                                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
    SCC:
     Strict:
      {incr#(mark(X)) -> incr#(X),
         incr#(ok(X)) -> incr#(X)}
     Weak:
     {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
           cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                  incr(mark(X)) -> mark(incr(X)),
                    incr(ok(X)) -> ok(incr(X)),
           active(cons(X1, X2)) -> cons(active(X1), X2),
                active(incr(X)) -> incr(active(X)),
      active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                 active(nats()) -> mark(cons(0(), incr(nats()))),
                 active(odds()) -> mark(incr(pairs())),
                active(pairs()) -> mark(cons(0(), incr(odds()))),
                   active(s(X)) -> s(active(X)),
                active(head(X)) -> head(active(X)),
      active(head(cons(X, XS))) -> mark(X),
                active(tail(X)) -> tail(active(X)),
      active(tail(cons(X, XS))) -> mark(XS),
                     s(mark(X)) -> mark(s(X)),
                       s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                    proper(0()) -> ok(0()),
                proper(incr(X)) -> incr(proper(X)),
                 proper(nats()) -> ok(nats()),
                 proper(odds()) -> ok(odds()),
                proper(pairs()) -> ok(pairs()),
                   proper(s(X)) -> s(proper(X)),
                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:
         {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
               cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                      incr(mark(X)) -> mark(incr(X)),
                        incr(ok(X)) -> ok(incr(X)),
               active(cons(X1, X2)) -> cons(active(X1), X2),
                    active(incr(X)) -> incr(active(X)),
          active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                     active(nats()) -> mark(cons(0(), incr(nats()))),
                     active(odds()) -> mark(incr(pairs())),
                    active(pairs()) -> mark(cons(0(), incr(odds()))),
                       active(s(X)) -> s(active(X)),
                    active(head(X)) -> head(active(X)),
          active(head(cons(X, XS))) -> mark(X),
                    active(tail(X)) -> tail(active(X)),
          active(tail(cons(X, XS))) -> mark(XS),
                         s(mark(X)) -> mark(s(X)),
                           s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                        proper(0()) -> ok(0()),
                    proper(incr(X)) -> incr(proper(X)),
                     proper(nats()) -> ok(nats()),
                     proper(odds()) -> ok(odds()),
                    proper(pairs()) -> ok(pairs()),
                       proper(s(X)) -> s(proper(X)),
                    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:
      {  cons#(mark(X1), X2) -> cons#(X1, X2),
       cons#(ok(X1), ok(X2)) -> cons#(X1, X2)}
     Weak:
     {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
           cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                  incr(mark(X)) -> mark(incr(X)),
                    incr(ok(X)) -> ok(incr(X)),
           active(cons(X1, X2)) -> cons(active(X1), X2),
                active(incr(X)) -> incr(active(X)),
      active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                 active(nats()) -> mark(cons(0(), incr(nats()))),
                 active(odds()) -> mark(incr(pairs())),
                active(pairs()) -> mark(cons(0(), incr(odds()))),
                   active(s(X)) -> s(active(X)),
                active(head(X)) -> head(active(X)),
      active(head(cons(X, XS))) -> mark(X),
                active(tail(X)) -> tail(active(X)),
      active(tail(cons(X, XS))) -> mark(XS),
                     s(mark(X)) -> mark(s(X)),
                       s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                    proper(0()) -> ok(0()),
                proper(incr(X)) -> incr(proper(X)),
                 proper(nats()) -> ok(nats()),
                 proper(odds()) -> ok(odds()),
                proper(pairs()) -> ok(pairs()),
                   proper(s(X)) -> s(proper(X)),
                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:
         {       cons(mark(X1), X2) -> mark(cons(X1, X2)),
               cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                      incr(mark(X)) -> mark(incr(X)),
                        incr(ok(X)) -> ok(incr(X)),
               active(cons(X1, X2)) -> cons(active(X1), X2),
                    active(incr(X)) -> incr(active(X)),
          active(incr(cons(X, XS))) -> mark(cons(s(X), incr(XS))),
                     active(nats()) -> mark(cons(0(), incr(nats()))),
                     active(odds()) -> mark(incr(pairs())),
                    active(pairs()) -> mark(cons(0(), incr(odds()))),
                       active(s(X)) -> s(active(X)),
                    active(head(X)) -> head(active(X)),
          active(head(cons(X, XS))) -> mark(X),
                    active(tail(X)) -> tail(active(X)),
          active(tail(cons(X, XS))) -> mark(XS),
                         s(mark(X)) -> mark(s(X)),
                           s(ok(X)) -> ok(s(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(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                        proper(0()) -> ok(0()),
                    proper(incr(X)) -> incr(proper(X)),
                     proper(nats()) -> ok(nats()),
                     proper(odds()) -> ok(odds()),
                    proper(pairs()) -> ok(pairs()),
                       proper(s(X)) -> s(proper(X)),
                    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