MAYBE
Time: 0.375979
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:
  DP:
   {      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}
  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}
  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))
    (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# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
    (active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (active# 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)
    (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))
    (active# incr cons(X, XS) -> incr# XS, incr# mark X -> incr# X)
    (active# incr cons(X, XS) -> incr# XS, incr# ok X -> incr# 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# 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))
    (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)
    (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 -> 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))
   }
   EDG:
    {(proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# 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# head X -> head# proper X, head# ok 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)
     (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# ok X -> tail# 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)
     (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))}
    EDG:
     {(proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
      (active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
      (active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
      (active# 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# head X -> head# proper X, head# ok 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)
      (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# ok X -> tail# 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)
      (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))}
     STATUS:
      arrows: 0.986479
      SCCS (1):
       Scc:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       
       
       
       
       
       
       
       SCC (2):
        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}
        Open