MAYBE
Time: 0.083421
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:
  DP:
   {         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}
  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}
  UR:
   {         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}
   EDG:
    {
     (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)
     (proper# cons(X1, X2) -> proper# X1, proper# tail X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# tail X -> tail# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# head X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# head X -> head# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# adx X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# adx X -> adx# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# 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# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X1, proper# incr X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# incr X -> incr# proper X)
     (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# incr cons(X, L) -> incr# L, incr# ok X -> incr# X)
     (active# incr cons(X, L) -> incr# L, incr# mark X -> incr# X)
     (active# incr cons(X, L) -> cons#(s X, incr L), 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))
     (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, 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)
     (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 -> 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)
     (active# adx cons(X, L) -> cons#(X, adx L), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# adx cons(X, L) -> cons#(X, adx L), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# adx cons(X, L) -> adx# L, adx# mark X -> adx# X)
     (active# adx cons(X, L) -> adx# L, adx# ok X -> adx# X)
     (cons#(mark X1, 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))
     (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# incr cons(X, L) -> incr# L)
     (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) -> s# 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))
     (active# cons(X1, X2) -> active# X1, active# s X -> active# X)
     (active# cons(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# cons(X1, X2) -> active# X1, active# adx X -> active# X)
     (active# cons(X1, X2) -> active# X1, active# adx X -> adx# active X)
     (active# cons(X1, X2) -> active# X1, active# adx cons(X, L) -> incr# cons(X, 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) -> adx# L)
     (active# cons(X1, X2) -> active# X1, active# zeros() -> cons#(0(), zeros()))
     (active# cons(X1, X2) -> active# X1, active# nats() -> adx# zeros())
     (active# cons(X1, X2) -> active# X1, active# head X -> active# X)
     (active# cons(X1, X2) -> active# X1, active# head X -> head# active X)
     (active# cons(X1, X2) -> active# X1, active# tail X -> active# X)
     (active# cons(X1, X2) -> active# X1, active# tail X -> tail# active 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)
     (active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
    }
    STATUS:
     arrows: 0.870054
     SCCS (9):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active 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:
       {      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:
       {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 (2):
       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}
       Open
      
      SCC (6):
       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}
       Open
      
      
      
      
      
      
      
      
      
      SCC (7):
       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}
       Open
      
      
      
      
      
      
      
      SCC (2):
       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}
       Open
      
      SCC (2):
       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}
       Open
      
      SCC (2):
       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}
       Open
      
      SCC (2):
       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}
       Open
      
      SCC (2):
       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}
       Open
      
      SCC (2):
       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}
       Open