MAYBE
Time: 13.016227
TRS:
 {            adx mark X -> mark adx X,
                adx ok X -> ok adx X,
            active adx X -> adx active X,
   active adx cons(X, Y) -> mark incr cons(X, adx Y),
          active zeros() -> mark cons(0(), zeros()),
           active nats() -> mark adx zeros(),
           active incr X -> incr active X,
  active incr cons(X, Y) -> mark cons(s X, incr Y),
             active hd X -> hd active X,
    active hd cons(X, Y) -> mark X,
             active tl X -> tl active X,
    active tl cons(X, Y) -> mark Y,
      cons(ok X1, ok X2) -> ok cons(X1, X2),
                  s ok X -> ok s X,
             incr mark X -> mark incr X,
               incr ok X -> ok incr X,
               hd mark X -> mark hd X,
                 hd ok X -> ok hd X,
               tl mark X -> mark tl X,
                 tl ok X -> ok tl X,
            proper adx X -> adx proper X,
          proper zeros() -> ok zeros(),
           proper nats() -> ok nats(),
     proper cons(X1, X2) -> cons(proper X1, proper X2),
              proper 0() -> ok 0(),
              proper s X -> s proper X,
           proper incr X -> incr proper X,
             proper hd X -> hd proper X,
             proper tl X -> tl proper X,
              top mark X -> top proper X,
                top ok X -> top active X}
 DP:
  DP:
   {            adx# mark X -> adx# X,
                  adx# ok X -> adx# X,
              active# adx X -> adx# active X,
              active# adx X -> active# X,
     active# adx cons(X, Y) -> adx# Y,
     active# adx cons(X, Y) -> cons#(X, adx Y),
     active# adx cons(X, Y) -> incr# cons(X, adx Y),
            active# zeros() -> cons#(0(), zeros()),
             active# nats() -> adx# zeros(),
             active# incr X -> active# X,
             active# incr X -> incr# active X,
    active# incr cons(X, Y) -> cons#(s X, incr Y),
    active# incr cons(X, Y) -> s# X,
    active# incr cons(X, Y) -> incr# Y,
               active# hd X -> active# X,
               active# hd X -> hd# active X,
               active# tl X -> active# X,
               active# tl X -> tl# active X,
        cons#(ok X1, ok X2) -> cons#(X1, X2),
                    s# ok X -> s# X,
               incr# mark X -> incr# X,
                 incr# ok X -> incr# X,
                 hd# mark X -> hd# X,
                   hd# ok X -> hd# X,
                 tl# mark X -> tl# X,
                   tl# ok X -> tl# X,
              proper# adx X -> adx# proper X,
              proper# adx 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# incr X -> incr# proper X,
             proper# incr X -> proper# X,
               proper# hd X -> hd# proper X,
               proper# hd X -> proper# X,
               proper# tl X -> tl# proper X,
               proper# tl 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:
  {            adx mark X -> mark adx X,
                 adx ok X -> ok adx X,
             active adx X -> adx active X,
    active adx cons(X, Y) -> mark incr cons(X, adx Y),
           active zeros() -> mark cons(0(), zeros()),
            active nats() -> mark adx zeros(),
            active incr X -> incr active X,
   active incr cons(X, Y) -> mark cons(s X, incr Y),
              active hd X -> hd active X,
     active hd cons(X, Y) -> mark X,
              active tl X -> tl active X,
     active tl cons(X, Y) -> mark Y,
       cons(ok X1, ok X2) -> ok cons(X1, X2),
                   s ok X -> ok s X,
              incr mark X -> mark incr X,
                incr ok X -> ok incr X,
                hd mark X -> mark hd X,
                  hd ok X -> ok hd X,
                tl mark X -> mark tl X,
                  tl ok X -> ok tl X,
             proper adx X -> adx proper X,
           proper zeros() -> ok zeros(),
            proper nats() -> ok nats(),
      proper cons(X1, X2) -> cons(proper X1, proper X2),
               proper 0() -> ok 0(),
               proper s X -> s proper X,
            proper incr X -> incr proper X,
              proper hd X -> hd proper X,
              proper tl X -> tl proper X,
               top mark X -> top proper X,
                 top ok X -> top active X}
  UR:
   {            adx mark X -> mark adx X,
                  adx ok X -> ok adx X,
              active adx X -> adx active X,
     active adx cons(X, Y) -> mark incr cons(X, adx Y),
            active zeros() -> mark cons(0(), zeros()),
             active nats() -> mark adx zeros(),
             active incr X -> incr active X,
    active incr cons(X, Y) -> mark cons(s X, incr Y),
               active hd X -> hd active X,
      active hd cons(X, Y) -> mark X,
               active tl X -> tl active X,
      active tl cons(X, Y) -> mark Y,
        cons(ok X1, ok X2) -> ok cons(X1, X2),
                    s ok X -> ok s X,
               incr mark X -> mark incr X,
                 incr ok X -> ok incr X,
                 hd mark X -> mark hd X,
                   hd ok X -> ok hd X,
                 tl mark X -> mark tl X,
                   tl ok X -> ok tl X,
              proper adx X -> adx proper X,
            proper zeros() -> ok zeros(),
             proper nats() -> ok nats(),
       proper cons(X1, X2) -> cons(proper X1, proper X2),
                proper 0() -> ok 0(),
                proper s X -> s proper X,
             proper incr X -> incr proper X,
               proper hd X -> hd proper X,
               proper tl X -> tl proper X}
   EDG:
    {
     (active# incr cons(X, Y) -> cons#(s X, incr Y), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (adx# mark X -> adx# X, adx# ok X -> adx# X)
     (adx# mark X -> adx# X, adx# mark X -> adx# X)
     (active# adx X -> active# X, active# tl X -> tl# active X)
     (active# adx X -> active# X, active# tl X -> active# X)
     (active# adx X -> active# X, active# hd X -> hd# active X)
     (active# adx X -> active# X, active# hd X -> active# X)
     (active# adx X -> active# X, active# incr cons(X, Y) -> incr# Y)
     (active# adx X -> active# X, active# incr cons(X, Y) -> s# X)
     (active# adx X -> active# X, active# incr cons(X, Y) -> cons#(s X, incr Y))
     (active# adx X -> active# X, active# incr X -> incr# active X)
     (active# adx X -> active# X, active# incr 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, Y) -> incr# cons(X, adx Y))
     (active# adx X -> active# X, active# adx cons(X, Y) -> cons#(X, adx Y))
     (active# adx X -> active# X, active# adx cons(X, Y) -> adx# Y)
     (active# adx X -> active# X, active# adx X -> active# X)
     (active# adx X -> active# X, active# adx X -> adx# active X)
     (active# incr cons(X, Y) -> s# X, s# ok X -> s# X)
     (active# tl X -> active# X, active# tl X -> tl# active X)
     (active# tl X -> active# X, active# tl X -> active# X)
     (active# tl X -> active# X, active# hd X -> hd# active X)
     (active# tl X -> active# X, active# hd X -> active# X)
     (active# tl X -> active# X, active# incr cons(X, Y) -> incr# Y)
     (active# tl X -> active# X, active# incr cons(X, Y) -> s# X)
     (active# tl X -> active# X, active# incr cons(X, Y) -> cons#(s X, incr Y))
     (active# tl X -> active# X, active# incr X -> incr# active X)
     (active# tl X -> active# X, active# incr X -> active# X)
     (active# tl X -> active# X, active# nats() -> adx# zeros())
     (active# tl X -> active# X, active# zeros() -> cons#(0(), zeros()))
     (active# tl X -> active# X, active# adx cons(X, Y) -> incr# cons(X, adx Y))
     (active# tl X -> active# X, active# adx cons(X, Y) -> cons#(X, adx Y))
     (active# tl X -> active# X, active# adx cons(X, Y) -> adx# Y)
     (active# tl X -> active# X, active# adx X -> active# X)
     (active# tl X -> active# X, active# adx X -> adx# active X)
     (incr# mark X -> incr# X, incr# ok X -> incr# X)
     (incr# mark X -> incr# X, incr# mark X -> incr# X)
     (hd# mark X -> hd# X, hd# ok X -> hd# X)
     (hd# mark X -> hd# X, hd# mark X -> hd# X)
     (tl# mark X -> tl# X, tl# ok X -> tl# X)
     (tl# mark X -> tl# X, tl# mark X -> tl# X)
     (proper# adx X -> proper# X, proper# tl X -> proper# X)
     (proper# adx X -> proper# X, proper# tl X -> tl# proper X)
     (proper# adx X -> proper# X, proper# hd X -> proper# X)
     (proper# adx X -> proper# X, proper# hd X -> hd# proper X)
     (proper# adx X -> proper# X, proper# incr X -> proper# X)
     (proper# adx X -> proper# X, proper# incr X -> incr# proper X)
     (proper# adx X -> proper# X, proper# s X -> proper# X)
     (proper# adx X -> proper# X, proper# s X -> s# proper X)
     (proper# adx X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# adx X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# adx X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# adx X -> proper# X, proper# adx X -> proper# X)
     (proper# adx X -> proper# X, proper# adx X -> adx# proper X)
     (proper# incr X -> proper# X, proper# tl X -> proper# X)
     (proper# incr X -> proper# X, proper# tl X -> tl# proper X)
     (proper# incr X -> proper# X, proper# hd X -> proper# X)
     (proper# incr X -> proper# X, proper# hd X -> hd# 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# s X -> proper# X)
     (proper# incr X -> proper# X, proper# s X -> s# 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# incr X -> proper# X, proper# adx X -> proper# X)
     (proper# incr X -> proper# X, proper# adx X -> adx# proper X)
     (proper# tl X -> proper# X, proper# tl X -> proper# X)
     (proper# tl X -> proper# X, proper# tl X -> tl# proper X)
     (proper# tl X -> proper# X, proper# hd X -> proper# X)
     (proper# tl X -> proper# X, proper# hd X -> hd# proper X)
     (proper# tl X -> proper# X, proper# incr X -> proper# X)
     (proper# tl X -> proper# X, proper# incr X -> incr# proper X)
     (proper# tl X -> proper# X, proper# s X -> proper# X)
     (proper# tl X -> proper# X, proper# s X -> s# proper X)
     (proper# tl X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# tl X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# tl X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# tl X -> proper# X, proper# adx X -> proper# X)
     (proper# tl X -> proper# X, proper# adx X -> adx# proper X)
     (top# ok X -> active# X, active# tl X -> tl# active X)
     (top# ok X -> active# X, active# tl X -> active# X)
     (top# ok X -> active# X, active# hd X -> hd# active X)
     (top# ok X -> active# X, active# hd X -> active# X)
     (top# ok X -> active# X, active# incr cons(X, Y) -> incr# Y)
     (top# ok X -> active# X, active# incr cons(X, Y) -> s# X)
     (top# ok X -> active# X, active# incr cons(X, Y) -> cons#(s X, incr Y))
     (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# nats() -> adx# zeros())
     (top# ok X -> active# X, active# zeros() -> cons#(0(), zeros()))
     (top# ok X -> active# X, active# adx cons(X, Y) -> incr# cons(X, adx Y))
     (top# ok X -> active# X, active# adx cons(X, Y) -> cons#(X, adx Y))
     (top# ok X -> active# X, active# adx cons(X, Y) -> adx# Y)
     (top# ok X -> active# X, active# adx X -> active# X)
     (top# ok X -> active# X, active# adx X -> adx# active X)
     (proper# cons(X1, X2) -> proper# X2, proper# tl X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# tl X -> tl# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# hd X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# hd X -> hd# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# incr X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# incr X -> incr# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X2, proper# adx X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# adx X -> adx# proper X)
     (active# incr X -> incr# active X, incr# ok X -> incr# X)
     (active# incr X -> incr# active X, incr# mark X -> incr# X)
     (active# tl X -> tl# active X, tl# ok X -> tl# X)
     (active# tl X -> tl# active X, tl# mark X -> tl# X)
     (proper# s X -> s# proper X, s# ok X -> s# X)
     (proper# hd X -> hd# proper X, hd# ok X -> hd# X)
     (proper# hd X -> hd# proper X, hd# mark X -> hd# 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)
     (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# adx cons(X, Y) -> adx# Y, adx# ok X -> adx# X)
     (active# adx cons(X, Y) -> adx# Y, adx# mark X -> adx# X)
     (active# incr cons(X, Y) -> incr# Y, incr# mark X -> incr# X)
     (active# incr cons(X, Y) -> incr# Y, incr# ok X -> incr# X)
     (active# adx cons(X, Y) -> incr# cons(X, adx Y), incr# mark X -> incr# X)
     (active# adx cons(X, Y) -> incr# cons(X, adx Y), incr# ok X -> incr# X)
     (proper# cons(X1, X2) -> proper# X1, proper# adx X -> adx# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# adx X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# incr X -> incr# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# incr X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# hd X -> hd# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# hd X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# tl X -> tl# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# tl 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# tl X -> tl# proper X, tl# mark X -> tl# X)
     (proper# tl X -> tl# proper X, tl# ok X -> tl# X)
     (proper# incr X -> incr# proper X, incr# mark X -> incr# X)
     (proper# incr X -> incr# proper X, incr# ok X -> incr# X)
     (proper# adx X -> adx# proper X, adx# mark X -> adx# X)
     (proper# adx X -> adx# proper X, adx# ok X -> adx# X)
     (active# hd X -> hd# active X, hd# mark X -> hd# X)
     (active# hd X -> hd# active X, hd# ok X -> hd# X)
     (active# adx X -> adx# active X, adx# mark X -> adx# X)
     (active# adx X -> adx# active X, adx# ok X -> adx# X)
     (top# mark X -> proper# X, proper# adx X -> adx# proper X)
     (top# mark X -> proper# X, proper# adx X -> proper# X)
     (top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# s X -> s# proper X)
     (top# mark X -> proper# X, proper# s X -> proper# X)
     (top# mark X -> proper# X, proper# incr X -> incr# proper X)
     (top# mark X -> proper# X, proper# incr X -> proper# X)
     (top# mark X -> proper# X, proper# hd X -> hd# proper X)
     (top# mark X -> proper# X, proper# hd X -> proper# X)
     (top# mark X -> proper# X, proper# tl X -> tl# proper X)
     (top# mark X -> proper# X, proper# tl X -> proper# X)
     (proper# hd X -> proper# X, proper# adx X -> adx# proper X)
     (proper# hd X -> proper# X, proper# adx X -> proper# X)
     (proper# hd X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# hd X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# hd X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# hd X -> proper# X, proper# s X -> s# proper X)
     (proper# hd X -> proper# X, proper# s X -> proper# X)
     (proper# hd X -> proper# X, proper# incr X -> incr# proper X)
     (proper# hd X -> proper# X, proper# incr X -> proper# X)
     (proper# hd X -> proper# X, proper# hd X -> hd# proper X)
     (proper# hd X -> proper# X, proper# hd X -> proper# X)
     (proper# hd X -> proper# X, proper# tl X -> tl# proper X)
     (proper# hd X -> proper# X, proper# tl X -> proper# X)
     (proper# s X -> proper# X, proper# adx X -> adx# proper X)
     (proper# s X -> proper# X, proper# adx 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# s X -> s# proper X)
     (proper# s X -> proper# X, proper# s X -> proper# X)
     (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# hd X -> hd# proper X)
     (proper# s X -> proper# X, proper# hd X -> proper# X)
     (proper# s X -> proper# X, proper# tl X -> tl# proper X)
     (proper# s X -> proper# X, proper# tl X -> proper# X)
     (tl# ok X -> tl# X, tl# mark X -> tl# X)
     (tl# ok X -> tl# X, tl# ok X -> tl# X)
     (hd# ok X -> hd# X, hd# mark X -> hd# X)
     (hd# ok X -> hd# X, hd# ok X -> hd# X)
     (incr# ok X -> incr# X, incr# mark X -> incr# X)
     (incr# ok X -> incr# X, incr# ok X -> incr# X)
     (s# ok X -> s# X, s# ok X -> s# X)
     (active# hd X -> active# X, active# adx X -> adx# active X)
     (active# hd X -> active# X, active# adx X -> active# X)
     (active# hd X -> active# X, active# adx cons(X, Y) -> adx# Y)
     (active# hd X -> active# X, active# adx cons(X, Y) -> cons#(X, adx Y))
     (active# hd X -> active# X, active# adx cons(X, Y) -> incr# cons(X, adx Y))
     (active# hd X -> active# X, active# zeros() -> cons#(0(), zeros()))
     (active# hd X -> active# X, active# nats() -> adx# zeros())
     (active# hd X -> active# X, active# incr X -> active# X)
     (active# hd X -> active# X, active# incr X -> incr# active X)
     (active# hd X -> active# X, active# incr cons(X, Y) -> cons#(s X, incr Y))
     (active# hd X -> active# X, active# incr cons(X, Y) -> s# X)
     (active# hd X -> active# X, active# incr cons(X, Y) -> incr# Y)
     (active# hd X -> active# X, active# hd X -> active# X)
     (active# hd X -> active# X, active# hd X -> hd# active X)
     (active# hd X -> active# X, active# tl X -> active# X)
     (active# hd X -> active# X, active# tl X -> tl# active X)
     (active# incr X -> active# X, active# adx X -> adx# active X)
     (active# incr X -> active# X, active# adx X -> active# X)
     (active# incr X -> active# X, active# adx cons(X, Y) -> adx# Y)
     (active# incr X -> active# X, active# adx cons(X, Y) -> cons#(X, adx Y))
     (active# incr X -> active# X, active# adx cons(X, Y) -> incr# cons(X, adx Y))
     (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# incr X -> active# X)
     (active# incr X -> active# X, active# incr X -> incr# active X)
     (active# incr X -> active# X, active# incr cons(X, Y) -> cons#(s X, incr Y))
     (active# incr X -> active# X, active# incr cons(X, Y) -> s# X)
     (active# incr X -> active# X, active# incr cons(X, Y) -> incr# Y)
     (active# incr X -> active# X, active# hd X -> active# X)
     (active# incr X -> active# X, active# hd X -> hd# active X)
     (active# incr X -> active# X, active# tl X -> active# X)
     (active# incr X -> active# X, active# tl X -> tl# active X)
     (adx# ok X -> adx# X, adx# mark X -> adx# X)
     (adx# ok X -> adx# X, adx# ok X -> adx# X)
     (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# adx cons(X, Y) -> cons#(X, adx Y), cons#(ok X1, ok X2) -> cons#(X1, X2))
    }
    STATUS:
     arrows: 0.871823
     SCCS (9):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       {       proper# adx X -> proper# X,
        proper# cons(X1, X2) -> proper# X1,
        proper# cons(X1, X2) -> proper# X2,
                 proper# s X -> proper# X,
              proper# incr X -> proper# X,
                proper# hd X -> proper# X,
                proper# tl X -> proper# X}
      Scc:
       { active# adx X -> active# X,
        active# incr X -> active# X,
          active# hd X -> active# X,
          active# tl X -> active# X}
      Scc:
       {tl# mark X -> tl# X,
          tl# ok X -> tl# X}
      Scc:
       {hd# mark X -> hd# X,
          hd# ok X -> hd# X}
      Scc:
       {s# ok X -> s# X}
      Scc:
       {incr# mark X -> incr# X,
          incr# ok X -> incr# X}
      Scc:
       {adx# mark X -> adx# X,
          adx# ok X -> adx# X}
      Scc:
       {cons#(ok X1, ok X2) -> cons#(X1, X2)}
      
      SCC (2):
       Strict:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Weak:
       {            adx mark X -> mark adx X,
                      adx ok X -> ok adx X,
                  active adx X -> adx active X,
         active adx cons(X, Y) -> mark incr cons(X, adx Y),
                active zeros() -> mark cons(0(), zeros()),
                 active nats() -> mark adx zeros(),
                 active incr X -> incr active X,
        active incr cons(X, Y) -> mark cons(s X, incr Y),
                   active hd X -> hd active X,
          active hd cons(X, Y) -> mark X,
                   active tl X -> tl active X,
          active tl cons(X, Y) -> mark Y,
            cons(ok X1, ok X2) -> ok cons(X1, X2),
                        s ok X -> ok s X,
                   incr mark X -> mark incr X,
                     incr ok X -> ok incr X,
                     hd mark X -> mark hd X,
                       hd ok X -> ok hd X,
                     tl mark X -> mark tl X,
                       tl ok X -> ok tl X,
                  proper adx X -> adx proper X,
                proper zeros() -> ok zeros(),
                 proper nats() -> ok nats(),
           proper cons(X1, X2) -> cons(proper X1, proper X2),
                    proper 0() -> ok 0(),
                    proper s X -> s proper X,
                 proper incr X -> incr proper X,
                   proper hd X -> hd proper X,
                   proper tl X -> tl proper X,
                    top mark X -> top proper X,
                      top ok X -> top active X}
       Open
      
      
      SCC (7):
       Strict:
        {       proper# adx X -> proper# X,
         proper# cons(X1, X2) -> proper# X1,
         proper# cons(X1, X2) -> proper# X2,
                  proper# s X -> proper# X,
               proper# incr X -> proper# X,
                 proper# hd X -> proper# X,
                 proper# tl X -> proper# X}
       Weak:
       {            adx mark X -> mark adx X,
                      adx ok X -> ok adx X,
                  active adx X -> adx active X,
         active adx cons(X, Y) -> mark incr cons(X, adx Y),
                active zeros() -> mark cons(0(), zeros()),
                 active nats() -> mark adx zeros(),
                 active incr X -> incr active X,
        active incr cons(X, Y) -> mark cons(s X, incr Y),
                   active hd X -> hd active X,
          active hd cons(X, Y) -> mark X,
                   active tl X -> tl active X,
          active tl cons(X, Y) -> mark Y,
            cons(ok X1, ok X2) -> ok cons(X1, X2),
                        s ok X -> ok s X,
                   incr mark X -> mark incr X,
                     incr ok X -> ok incr X,
                     hd mark X -> mark hd X,
                       hd ok X -> ok hd X,
                     tl mark X -> mark tl X,
                       tl ok X -> ok tl X,
                  proper adx X -> adx proper X,
                proper zeros() -> ok zeros(),
                 proper nats() -> ok nats(),
           proper cons(X1, X2) -> cons(proper X1, proper X2),
                    proper 0() -> ok 0(),
                    proper s X -> s proper X,
                 proper incr X -> incr proper X,
                   proper hd X -> hd proper X,
                   proper tl X -> tl proper X,
                    top mark X -> top proper X,
                      top ok X -> top active X}
       Open
      
      
      
      
      
      SCC (4):
       Strict:
        { active# adx X -> active# X,
         active# incr X -> active# X,
           active# hd X -> active# X,
           active# tl X -> active# X}
       Weak:
       {            adx mark X -> mark adx X,
                      adx ok X -> ok adx X,
                  active adx X -> adx active X,
         active adx cons(X, Y) -> mark incr cons(X, adx Y),
                active zeros() -> mark cons(0(), zeros()),
                 active nats() -> mark adx zeros(),
                 active incr X -> incr active X,
        active incr cons(X, Y) -> mark cons(s X, incr Y),
                   active hd X -> hd active X,
          active hd cons(X, Y) -> mark X,
                   active tl X -> tl active X,
          active tl cons(X, Y) -> mark Y,
            cons(ok X1, ok X2) -> ok cons(X1, X2),
                        s ok X -> ok s X,
                   incr mark X -> mark incr X,
                     incr ok X -> ok incr X,
                     hd mark X -> mark hd X,
                       hd ok X -> ok hd X,
                     tl mark X -> mark tl X,
                       tl ok X -> ok tl X,
                  proper adx X -> adx proper X,
                proper zeros() -> ok zeros(),
                 proper nats() -> ok nats(),
           proper cons(X1, X2) -> cons(proper X1, proper X2),
                    proper 0() -> ok 0(),
                    proper s X -> s proper X,
                 proper incr X -> incr proper X,
                   proper hd X -> hd proper X,
                   proper tl X -> tl proper X,
                    top mark X -> top proper X,
                      top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        {tl# mark X -> tl# X,
           tl# ok X -> tl# X}
       Weak:
       {            adx mark X -> mark adx X,
                      adx ok X -> ok adx X,
                  active adx X -> adx active X,
         active adx cons(X, Y) -> mark incr cons(X, adx Y),
                active zeros() -> mark cons(0(), zeros()),
                 active nats() -> mark adx zeros(),
                 active incr X -> incr active X,
        active incr cons(X, Y) -> mark cons(s X, incr Y),
                   active hd X -> hd active X,
          active hd cons(X, Y) -> mark X,
                   active tl X -> tl active X,
          active tl cons(X, Y) -> mark Y,
            cons(ok X1, ok X2) -> ok cons(X1, X2),
                        s ok X -> ok s X,
                   incr mark X -> mark incr X,
                     incr ok X -> ok incr X,
                     hd mark X -> mark hd X,
                       hd ok X -> ok hd X,
                     tl mark X -> mark tl X,
                       tl ok X -> ok tl X,
                  proper adx X -> adx proper X,
                proper zeros() -> ok zeros(),
                 proper nats() -> ok nats(),
           proper cons(X1, X2) -> cons(proper X1, proper X2),
                    proper 0() -> ok 0(),
                    proper s X -> s proper X,
                 proper incr X -> incr proper X,
                   proper hd X -> hd proper X,
                   proper tl X -> tl proper X,
                    top mark X -> top proper X,
                      top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        {hd# mark X -> hd# X,
           hd# ok X -> hd# X}
       Weak:
       {            adx mark X -> mark adx X,
                      adx ok X -> ok adx X,
                  active adx X -> adx active X,
         active adx cons(X, Y) -> mark incr cons(X, adx Y),
                active zeros() -> mark cons(0(), zeros()),
                 active nats() -> mark adx zeros(),
                 active incr X -> incr active X,
        active incr cons(X, Y) -> mark cons(s X, incr Y),
                   active hd X -> hd active X,
          active hd cons(X, Y) -> mark X,
                   active tl X -> tl active X,
          active tl cons(X, Y) -> mark Y,
            cons(ok X1, ok X2) -> ok cons(X1, X2),
                        s ok X -> ok s X,
                   incr mark X -> mark incr X,
                     incr ok X -> ok incr X,
                     hd mark X -> mark hd X,
                       hd ok X -> ok hd X,
                     tl mark X -> mark tl X,
                       tl ok X -> ok tl X,
                  proper adx X -> adx proper X,
                proper zeros() -> ok zeros(),
                 proper nats() -> ok nats(),
           proper cons(X1, X2) -> cons(proper X1, proper X2),
                    proper 0() -> ok 0(),
                    proper s X -> s proper X,
                 proper incr X -> incr proper X,
                   proper hd X -> hd proper X,
                   proper tl X -> tl proper X,
                    top mark X -> top proper X,
                      top ok X -> top active X}
       Open
      
      
      SCC (1):
       Strict:
        {s# ok X -> s# X}
       Weak:
       {            adx mark X -> mark adx X,
                      adx ok X -> ok adx X,
                  active adx X -> adx active X,
         active adx cons(X, Y) -> mark incr cons(X, adx Y),
                active zeros() -> mark cons(0(), zeros()),
                 active nats() -> mark adx zeros(),
                 active incr X -> incr active X,
        active incr cons(X, Y) -> mark cons(s X, incr Y),
                   active hd X -> hd active X,
          active hd cons(X, Y) -> mark X,
                   active tl X -> tl active X,
          active tl cons(X, Y) -> mark Y,
            cons(ok X1, ok X2) -> ok cons(X1, X2),
                        s ok X -> ok s X,
                   incr mark X -> mark incr X,
                     incr ok X -> ok incr X,
                     hd mark X -> mark hd X,
                       hd ok X -> ok hd X,
                     tl mark X -> mark tl X,
                       tl ok X -> ok tl X,
                  proper adx X -> adx proper X,
                proper zeros() -> ok zeros(),
                 proper nats() -> ok nats(),
           proper cons(X1, X2) -> cons(proper X1, proper X2),
                    proper 0() -> ok 0(),
                    proper s X -> s proper X,
                 proper incr X -> incr proper X,
                   proper hd X -> hd proper X,
                   proper tl X -> tl 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:
       {            adx mark X -> mark adx X,
                      adx ok X -> ok adx X,
                  active adx X -> adx active X,
         active adx cons(X, Y) -> mark incr cons(X, adx Y),
                active zeros() -> mark cons(0(), zeros()),
                 active nats() -> mark adx zeros(),
                 active incr X -> incr active X,
        active incr cons(X, Y) -> mark cons(s X, incr Y),
                   active hd X -> hd active X,
          active hd cons(X, Y) -> mark X,
                   active tl X -> tl active X,
          active tl cons(X, Y) -> mark Y,
            cons(ok X1, ok X2) -> ok cons(X1, X2),
                        s ok X -> ok s X,
                   incr mark X -> mark incr X,
                     incr ok X -> ok incr X,
                     hd mark X -> mark hd X,
                       hd ok X -> ok hd X,
                     tl mark X -> mark tl X,
                       tl ok X -> ok tl X,
                  proper adx X -> adx proper X,
                proper zeros() -> ok zeros(),
                 proper nats() -> ok nats(),
           proper cons(X1, X2) -> cons(proper X1, proper X2),
                    proper 0() -> ok 0(),
                    proper s X -> s proper X,
                 proper incr X -> incr proper X,
                   proper hd X -> hd proper X,
                   proper tl X -> tl 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:
       {            adx mark X -> mark adx X,
                      adx ok X -> ok adx X,
                  active adx X -> adx active X,
         active adx cons(X, Y) -> mark incr cons(X, adx Y),
                active zeros() -> mark cons(0(), zeros()),
                 active nats() -> mark adx zeros(),
                 active incr X -> incr active X,
        active incr cons(X, Y) -> mark cons(s X, incr Y),
                   active hd X -> hd active X,
          active hd cons(X, Y) -> mark X,
                   active tl X -> tl active X,
          active tl cons(X, Y) -> mark Y,
            cons(ok X1, ok X2) -> ok cons(X1, X2),
                        s ok X -> ok s X,
                   incr mark X -> mark incr X,
                     incr ok X -> ok incr X,
                     hd mark X -> mark hd X,
                       hd ok X -> ok hd X,
                     tl mark X -> mark tl X,
                       tl ok X -> ok tl X,
                  proper adx X -> adx proper X,
                proper zeros() -> ok zeros(),
                 proper nats() -> ok nats(),
           proper cons(X1, X2) -> cons(proper X1, proper X2),
                    proper 0() -> ok 0(),
                    proper s X -> s proper X,
                 proper incr X -> incr proper X,
                   proper hd X -> hd proper X,
                   proper tl X -> tl proper X,
                    top mark X -> top proper X,
                      top ok X -> top active X}
       Open
      
      
      
      SCC (1):
       Strict:
        {cons#(ok X1, ok X2) -> cons#(X1, X2)}
       Weak:
       {            adx mark X -> mark adx X,
                      adx ok X -> ok adx X,
                  active adx X -> adx active X,
         active adx cons(X, Y) -> mark incr cons(X, adx Y),
                active zeros() -> mark cons(0(), zeros()),
                 active nats() -> mark adx zeros(),
                 active incr X -> incr active X,
        active incr cons(X, Y) -> mark cons(s X, incr Y),
                   active hd X -> hd active X,
          active hd cons(X, Y) -> mark X,
                   active tl X -> tl active X,
          active tl cons(X, Y) -> mark Y,
            cons(ok X1, ok X2) -> ok cons(X1, X2),
                        s ok X -> ok s X,
                   incr mark X -> mark incr X,
                     incr ok X -> ok incr X,
                     hd mark X -> mark hd X,
                       hd ok X -> ok hd X,
                     tl mark X -> mark tl X,
                       tl ok X -> ok tl X,
                  proper adx X -> adx proper X,
                proper zeros() -> ok zeros(),
                 proper nats() -> ok nats(),
           proper cons(X1, X2) -> cons(proper X1, proper X2),
                    proper 0() -> ok 0(),
                    proper s X -> s proper X,
                 proper incr X -> incr proper X,
                   proper hd X -> hd proper X,
                   proper tl X -> tl proper X,
                    top mark X -> top proper X,
                      top ok X -> top active X}
       Open