MAYBE
Time: 1.179872
TRS:
 {            mark nil() -> active nil(),
             mark incr X -> active incr mark X,
       mark cons(X1, X2) -> active cons(mark X1, X2),
                mark s X -> active s mark X,
              mark adx X -> active adx mark X,
            mark zeros() -> active zeros(),
             mark nats() -> active nats(),
                mark 0() -> active 0(),
             mark head X -> active head mark X,
             mark tail X -> active tail mark X,
       active incr nil() -> mark nil(),
  active incr cons(X, L) -> mark cons(s X, incr L),
        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 cons(X, L) -> mark X,
  active tail cons(X, L) -> mark L,
             incr mark X -> incr X,
           incr active X -> incr X,
       cons(X1, mark X2) -> cons(X1, X2),
     cons(X1, active X2) -> cons(X1, X2),
       cons(mark X1, X2) -> cons(X1, X2),
     cons(active X1, X2) -> cons(X1, X2),
                s mark X -> s X,
              s active X -> s X,
              adx mark X -> adx X,
            adx active X -> adx X,
             head mark X -> head X,
           head active X -> head X,
             tail mark X -> tail X,
           tail active X -> tail X}
 DP:
  DP:
   {            mark# nil() -> active# nil(),
               mark# incr X -> mark# X,
               mark# incr X -> active# incr mark X,
               mark# incr X -> incr# mark X,
         mark# cons(X1, X2) -> mark# X1,
         mark# cons(X1, X2) -> active# cons(mark X1, X2),
         mark# cons(X1, X2) -> cons#(mark X1, X2),
                  mark# s X -> mark# X,
                  mark# s X -> active# s mark X,
                  mark# s X -> s# mark X,
                mark# adx X -> mark# X,
                mark# adx X -> active# adx mark X,
                mark# adx X -> adx# mark X,
              mark# zeros() -> active# zeros(),
               mark# nats() -> active# nats(),
                  mark# 0() -> active# 0(),
               mark# head X -> mark# X,
               mark# head X -> active# head mark X,
               mark# head X -> head# mark X,
               mark# tail X -> mark# X,
               mark# tail X -> active# tail mark X,
               mark# tail X -> tail# mark X,
         active# incr nil() -> mark# nil(),
    active# incr cons(X, L) -> mark# cons(s X, incr L),
    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# adx nil() -> mark# nil(),
     active# adx cons(X, L) -> mark# incr cons(X, adx L),
     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() -> mark# cons(0(), zeros()),
            active# zeros() -> cons#(0(), zeros()),
             active# nats() -> mark# adx zeros(),
             active# nats() -> adx# zeros(),
    active# head cons(X, L) -> mark# X,
    active# tail cons(X, L) -> mark# L,
               incr# mark X -> incr# X,
             incr# active X -> incr# X,
         cons#(X1, mark X2) -> cons#(X1, X2),
       cons#(X1, active X2) -> cons#(X1, X2),
         cons#(mark X1, X2) -> cons#(X1, X2),
       cons#(active X1, X2) -> cons#(X1, X2),
                  s# mark X -> s# X,
                s# active X -> s# X,
                adx# mark X -> adx# X,
              adx# active X -> adx# X,
               head# mark X -> head# X,
             head# active X -> head# X,
               tail# mark X -> tail# X,
             tail# active X -> tail# X}
  TRS:
  {            mark nil() -> active nil(),
              mark incr X -> active incr mark X,
        mark cons(X1, X2) -> active cons(mark X1, X2),
                 mark s X -> active s mark X,
               mark adx X -> active adx mark X,
             mark zeros() -> active zeros(),
              mark nats() -> active nats(),
                 mark 0() -> active 0(),
              mark head X -> active head mark X,
              mark tail X -> active tail mark X,
        active incr nil() -> mark nil(),
   active incr cons(X, L) -> mark cons(s X, incr L),
         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 cons(X, L) -> mark X,
   active tail cons(X, L) -> mark L,
              incr mark X -> incr X,
            incr active X -> incr X,
        cons(X1, mark X2) -> cons(X1, X2),
      cons(X1, active X2) -> cons(X1, X2),
        cons(mark X1, X2) -> cons(X1, X2),
      cons(active X1, X2) -> cons(X1, X2),
                 s mark X -> s X,
               s active X -> s X,
               adx mark X -> adx X,
             adx active X -> adx X,
              head mark X -> head X,
            head active X -> head X,
              tail mark X -> tail X,
            tail active X -> tail X}
  UR:
   {            mark nil() -> active nil(),
               mark incr X -> active incr mark X,
         mark cons(X1, X2) -> active cons(mark X1, X2),
                  mark s X -> active s mark X,
                mark adx X -> active adx mark X,
              mark zeros() -> active zeros(),
               mark nats() -> active nats(),
                  mark 0() -> active 0(),
               mark head X -> active head mark X,
               mark tail X -> active tail mark X,
         active incr nil() -> mark nil(),
    active incr cons(X, L) -> mark cons(s X, incr L),
          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 cons(X, L) -> mark X,
    active tail cons(X, L) -> mark L,
               incr mark X -> incr X,
             incr active X -> incr X,
         cons(X1, mark X2) -> cons(X1, X2),
       cons(X1, active X2) -> cons(X1, X2),
         cons(mark X1, X2) -> cons(X1, X2),
       cons(active X1, X2) -> cons(X1, X2),
                  s mark X -> s X,
                s active X -> s X,
                adx mark X -> adx X,
              adx active X -> adx X,
               head mark X -> head X,
             head active X -> head X,
               tail mark X -> tail X,
             tail active X -> tail X}
   EDG:
    {
     (mark# zeros() -> active# zeros(), active# tail cons(X, L) -> mark# L)
     (mark# zeros() -> active# zeros(), active# head cons(X, L) -> mark# X)
     (mark# zeros() -> active# zeros(), active# nats() -> adx# zeros())
     (mark# zeros() -> active# zeros(), active# nats() -> mark# adx zeros())
     (mark# zeros() -> active# zeros(), active# zeros() -> cons#(0(), zeros()))
     (mark# zeros() -> active# zeros(), active# zeros() -> mark# cons(0(), zeros()))
     (mark# zeros() -> active# zeros(), active# adx cons(X, L) -> adx# L)
     (mark# zeros() -> active# zeros(), active# adx cons(X, L) -> cons#(X, adx L))
     (mark# zeros() -> active# zeros(), active# adx cons(X, L) -> incr# cons(X, adx L))
     (mark# zeros() -> active# zeros(), active# adx cons(X, L) -> mark# incr cons(X, adx L))
     (mark# zeros() -> active# zeros(), active# adx nil() -> mark# nil())
     (mark# zeros() -> active# zeros(), active# incr cons(X, L) -> s# X)
     (mark# zeros() -> active# zeros(), active# incr cons(X, L) -> cons#(s X, incr L))
     (mark# zeros() -> active# zeros(), active# incr cons(X, L) -> incr# L)
     (mark# zeros() -> active# zeros(), active# incr cons(X, L) -> mark# cons(s X, incr L))
     (mark# zeros() -> active# zeros(), active# incr nil() -> mark# nil())
     (mark# 0() -> active# 0(), active# tail cons(X, L) -> mark# L)
     (mark# 0() -> active# 0(), active# head cons(X, L) -> mark# X)
     (mark# 0() -> active# 0(), active# nats() -> adx# zeros())
     (mark# 0() -> active# 0(), active# nats() -> mark# adx zeros())
     (mark# 0() -> active# 0(), active# zeros() -> cons#(0(), zeros()))
     (mark# 0() -> active# 0(), active# zeros() -> mark# cons(0(), zeros()))
     (mark# 0() -> active# 0(), active# adx cons(X, L) -> adx# L)
     (mark# 0() -> active# 0(), active# adx cons(X, L) -> cons#(X, adx L))
     (mark# 0() -> active# 0(), active# adx cons(X, L) -> incr# cons(X, adx L))
     (mark# 0() -> active# 0(), active# adx cons(X, L) -> mark# incr cons(X, adx L))
     (mark# 0() -> active# 0(), active# adx nil() -> mark# nil())
     (mark# 0() -> active# 0(), active# incr cons(X, L) -> s# X)
     (mark# 0() -> active# 0(), active# incr cons(X, L) -> cons#(s X, incr L))
     (mark# 0() -> active# 0(), active# incr cons(X, L) -> incr# L)
     (mark# 0() -> active# 0(), active# incr cons(X, L) -> mark# cons(s X, incr L))
     (mark# 0() -> active# 0(), active# incr nil() -> mark# nil())
     (active# adx nil() -> mark# nil(), mark# tail X -> tail# mark X)
     (active# adx nil() -> mark# nil(), mark# tail X -> active# tail mark X)
     (active# adx nil() -> mark# nil(), mark# tail X -> mark# X)
     (active# adx nil() -> mark# nil(), mark# head X -> head# mark X)
     (active# adx nil() -> mark# nil(), mark# head X -> active# head mark X)
     (active# adx nil() -> mark# nil(), mark# head X -> mark# X)
     (active# adx nil() -> mark# nil(), mark# 0() -> active# 0())
     (active# adx nil() -> mark# nil(), mark# nats() -> active# nats())
     (active# adx nil() -> mark# nil(), mark# zeros() -> active# zeros())
     (active# adx nil() -> mark# nil(), mark# adx X -> adx# mark X)
     (active# adx nil() -> mark# nil(), mark# adx X -> active# adx mark X)
     (active# adx nil() -> mark# nil(), mark# adx X -> mark# X)
     (active# adx nil() -> mark# nil(), mark# s X -> s# mark X)
     (active# adx nil() -> mark# nil(), mark# s X -> active# s mark X)
     (active# adx nil() -> mark# nil(), mark# s X -> mark# X)
     (active# adx nil() -> mark# nil(), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# adx nil() -> mark# nil(), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# adx nil() -> mark# nil(), mark# cons(X1, X2) -> mark# X1)
     (active# adx nil() -> mark# nil(), mark# incr X -> incr# mark X)
     (active# adx nil() -> mark# nil(), mark# incr X -> active# incr mark X)
     (active# adx nil() -> mark# nil(), mark# incr X -> mark# X)
     (active# adx nil() -> mark# nil(), mark# nil() -> active# nil())
     (mark# incr X -> mark# X, mark# tail X -> tail# mark X)
     (mark# incr X -> mark# X, mark# tail X -> active# tail mark X)
     (mark# incr X -> mark# X, mark# tail X -> mark# X)
     (mark# incr X -> mark# X, mark# head X -> head# mark X)
     (mark# incr X -> mark# X, mark# head X -> active# head mark X)
     (mark# incr X -> mark# X, mark# head X -> mark# X)
     (mark# incr X -> mark# X, mark# 0() -> active# 0())
     (mark# incr X -> mark# X, mark# nats() -> active# nats())
     (mark# incr X -> mark# X, mark# zeros() -> active# zeros())
     (mark# incr X -> mark# X, mark# adx X -> adx# mark X)
     (mark# incr X -> mark# X, mark# adx X -> active# adx mark X)
     (mark# incr X -> mark# X, mark# adx X -> mark# X)
     (mark# incr X -> mark# X, mark# s X -> s# mark X)
     (mark# incr X -> mark# X, mark# s X -> active# s mark X)
     (mark# incr X -> mark# X, mark# s X -> mark# X)
     (mark# incr X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# incr X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# incr X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# incr X -> mark# X, mark# incr X -> incr# mark X)
     (mark# incr X -> mark# X, mark# incr X -> active# incr mark X)
     (mark# incr X -> mark# X, mark# incr X -> mark# X)
     (mark# incr X -> mark# X, mark# nil() -> active# nil())
     (mark# adx X -> mark# X, mark# tail X -> tail# mark X)
     (mark# adx X -> mark# X, mark# tail X -> active# tail mark X)
     (mark# adx X -> mark# X, mark# tail X -> mark# X)
     (mark# adx X -> mark# X, mark# head X -> head# mark X)
     (mark# adx X -> mark# X, mark# head X -> active# head mark X)
     (mark# adx X -> mark# X, mark# head X -> mark# X)
     (mark# adx X -> mark# X, mark# 0() -> active# 0())
     (mark# adx X -> mark# X, mark# nats() -> active# nats())
     (mark# adx X -> mark# X, mark# zeros() -> active# zeros())
     (mark# adx X -> mark# X, mark# adx X -> adx# mark X)
     (mark# adx X -> mark# X, mark# adx X -> active# adx mark X)
     (mark# adx X -> mark# X, mark# adx X -> mark# X)
     (mark# adx X -> mark# X, mark# s X -> s# mark X)
     (mark# adx X -> mark# X, mark# s X -> active# s mark X)
     (mark# adx X -> mark# X, mark# s X -> mark# X)
     (mark# adx X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# adx X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# adx X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# adx X -> mark# X, mark# incr X -> incr# mark X)
     (mark# adx X -> mark# X, mark# incr X -> active# incr mark X)
     (mark# adx X -> mark# X, mark# incr X -> mark# X)
     (mark# adx X -> mark# X, mark# nil() -> active# nil())
     (mark# tail X -> mark# X, mark# tail X -> tail# mark X)
     (mark# tail X -> mark# X, mark# tail X -> active# tail mark X)
     (mark# tail X -> mark# X, mark# tail X -> mark# X)
     (mark# tail X -> mark# X, mark# head X -> head# mark X)
     (mark# tail X -> mark# X, mark# head X -> active# head mark X)
     (mark# tail X -> mark# X, mark# head X -> mark# X)
     (mark# tail X -> mark# X, mark# 0() -> active# 0())
     (mark# tail X -> mark# X, mark# nats() -> active# nats())
     (mark# tail X -> mark# X, mark# zeros() -> active# zeros())
     (mark# tail X -> mark# X, mark# adx X -> adx# mark X)
     (mark# tail X -> mark# X, mark# adx X -> active# adx mark X)
     (mark# tail X -> mark# X, mark# adx X -> mark# X)
     (mark# tail X -> mark# X, mark# s X -> s# mark X)
     (mark# tail X -> mark# X, mark# s X -> active# s mark X)
     (mark# tail X -> mark# X, mark# s X -> mark# X)
     (mark# tail X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# tail X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# tail X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# tail X -> mark# X, mark# incr X -> incr# mark X)
     (mark# tail X -> mark# X, mark# incr X -> active# incr mark X)
     (mark# tail X -> mark# X, mark# incr X -> mark# X)
     (mark# tail X -> mark# X, mark# nil() -> active# nil())
     (active# head cons(X, L) -> mark# X, mark# tail X -> tail# mark X)
     (active# head cons(X, L) -> mark# X, mark# tail X -> active# tail mark X)
     (active# head cons(X, L) -> mark# X, mark# tail X -> mark# X)
     (active# head cons(X, L) -> mark# X, mark# head X -> head# mark X)
     (active# head cons(X, L) -> mark# X, mark# head X -> active# head mark X)
     (active# head cons(X, L) -> mark# X, mark# head X -> mark# X)
     (active# head cons(X, L) -> mark# X, mark# 0() -> active# 0())
     (active# head cons(X, L) -> mark# X, mark# nats() -> active# nats())
     (active# head cons(X, L) -> mark# X, mark# zeros() -> active# zeros())
     (active# head cons(X, L) -> mark# X, mark# adx X -> adx# mark X)
     (active# head cons(X, L) -> mark# X, mark# adx X -> active# adx mark X)
     (active# head cons(X, L) -> mark# X, mark# adx X -> mark# X)
     (active# head cons(X, L) -> mark# X, mark# s X -> s# mark X)
     (active# head cons(X, L) -> mark# X, mark# s X -> active# s mark X)
     (active# head cons(X, L) -> mark# X, mark# s X -> mark# X)
     (active# head cons(X, L) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# head cons(X, L) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# head cons(X, L) -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (active# head cons(X, L) -> mark# X, mark# incr X -> incr# mark X)
     (active# head cons(X, L) -> mark# X, mark# incr X -> active# incr mark X)
     (active# head cons(X, L) -> mark# X, mark# incr X -> mark# X)
     (active# head cons(X, L) -> mark# X, mark# nil() -> active# nil())
     (incr# active X -> incr# X, incr# active X -> incr# X)
     (incr# active X -> incr# X, incr# mark X -> incr# X)
     (s# active X -> s# X, s# active X -> s# X)
     (s# active X -> s# X, s# mark X -> s# X)
     (adx# active X -> adx# X, adx# active X -> adx# X)
     (adx# active X -> adx# X, adx# mark X -> adx# X)
     (head# active X -> head# X, head# active X -> head# X)
     (head# active X -> head# X, head# mark X -> head# X)
     (tail# active X -> tail# X, tail# active X -> tail# X)
     (tail# active X -> tail# X, tail# mark X -> tail# X)
     (mark# s X -> active# s mark X, active# tail cons(X, L) -> mark# L)
     (mark# s X -> active# s mark X, active# head cons(X, L) -> mark# X)
     (mark# s X -> active# s mark X, active# nats() -> adx# zeros())
     (mark# s X -> active# s mark X, active# nats() -> mark# adx zeros())
     (mark# s X -> active# s mark X, active# zeros() -> cons#(0(), zeros()))
     (mark# s X -> active# s mark X, active# zeros() -> mark# cons(0(), zeros()))
     (mark# s X -> active# s mark X, active# adx cons(X, L) -> adx# L)
     (mark# s X -> active# s mark X, active# adx cons(X, L) -> cons#(X, adx L))
     (mark# s X -> active# s mark X, active# adx cons(X, L) -> incr# cons(X, adx L))
     (mark# s X -> active# s mark X, active# adx cons(X, L) -> mark# incr cons(X, adx L))
     (mark# s X -> active# s mark X, active# adx nil() -> mark# nil())
     (mark# s X -> active# s mark X, active# incr cons(X, L) -> s# X)
     (mark# s X -> active# s mark X, active# incr cons(X, L) -> cons#(s X, incr L))
     (mark# s X -> active# s mark X, active# incr cons(X, L) -> incr# L)
     (mark# s X -> active# s mark X, active# incr cons(X, L) -> mark# cons(s X, incr L))
     (mark# s X -> active# s mark X, active# incr nil() -> mark# nil())
     (mark# head X -> active# head mark X, active# tail cons(X, L) -> mark# L)
     (mark# head X -> active# head mark X, active# head cons(X, L) -> mark# X)
     (mark# head X -> active# head mark X, active# nats() -> adx# zeros())
     (mark# head X -> active# head mark X, active# nats() -> mark# adx zeros())
     (mark# head X -> active# head mark X, active# zeros() -> cons#(0(), zeros()))
     (mark# head X -> active# head mark X, active# zeros() -> mark# cons(0(), zeros()))
     (mark# head X -> active# head mark X, active# adx cons(X, L) -> adx# L)
     (mark# head X -> active# head mark X, active# adx cons(X, L) -> cons#(X, adx L))
     (mark# head X -> active# head mark X, active# adx cons(X, L) -> incr# cons(X, adx L))
     (mark# head X -> active# head mark X, active# adx cons(X, L) -> mark# incr cons(X, adx L))
     (mark# head X -> active# head mark X, active# adx nil() -> mark# nil())
     (mark# head X -> active# head mark X, active# incr cons(X, L) -> s# X)
     (mark# head X -> active# head mark X, active# incr cons(X, L) -> cons#(s X, incr L))
     (mark# head X -> active# head mark X, active# incr cons(X, L) -> incr# L)
     (mark# head X -> active# head mark X, active# incr cons(X, L) -> mark# cons(s X, incr L))
     (mark# head X -> active# head mark X, active# incr nil() -> mark# nil())
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# tail X -> tail# mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# tail X -> active# tail mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# tail X -> mark# X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# head X -> head# mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# head X -> active# head mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# head X -> mark# X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# 0() -> active# 0())
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# nats() -> active# nats())
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# zeros() -> active# zeros())
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# adx X -> adx# mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# adx X -> active# adx mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# adx X -> mark# X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# s X -> s# mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# s X -> active# s mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# s X -> mark# X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# cons(X1, X2) -> mark# X1)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# incr X -> incr# mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# incr X -> active# incr mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# incr X -> mark# X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# nil() -> active# nil())
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# tail cons(X, L) -> mark# L)
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# head cons(X, L) -> mark# X)
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# nats() -> adx# zeros())
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# nats() -> mark# adx zeros())
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# zeros() -> cons#(0(), zeros()))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# zeros() -> mark# cons(0(), zeros()))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# adx cons(X, L) -> adx# L)
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# adx cons(X, L) -> cons#(X, adx L))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# adx cons(X, L) -> incr# cons(X, adx L))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# adx cons(X, L) -> mark# incr cons(X, adx L))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# adx nil() -> mark# nil())
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr cons(X, L) -> s# X)
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr cons(X, L) -> cons#(s X, incr L))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr cons(X, L) -> incr# L)
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr cons(X, L) -> mark# cons(s X, incr L))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr nil() -> mark# nil())
     (active# adx cons(X, L) -> cons#(X, adx L), cons#(active X1, X2) -> cons#(X1, X2))
     (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#(X1, active X2) -> cons#(X1, X2))
     (active# adx cons(X, L) -> cons#(X, adx L), cons#(X1, mark X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (active# incr cons(X, L) -> incr# L, incr# active X -> incr# X)
     (active# incr cons(X, L) -> incr# L, incr# mark X -> incr# X)
     (active# tail cons(X, L) -> mark# L, mark# tail X -> tail# mark X)
     (active# tail cons(X, L) -> mark# L, mark# tail X -> active# tail mark X)
     (active# tail cons(X, L) -> mark# L, mark# tail X -> mark# X)
     (active# tail cons(X, L) -> mark# L, mark# head X -> head# mark X)
     (active# tail cons(X, L) -> mark# L, mark# head X -> active# head mark X)
     (active# tail cons(X, L) -> mark# L, mark# head X -> mark# X)
     (active# tail cons(X, L) -> mark# L, mark# 0() -> active# 0())
     (active# tail cons(X, L) -> mark# L, mark# nats() -> active# nats())
     (active# tail cons(X, L) -> mark# L, mark# zeros() -> active# zeros())
     (active# tail cons(X, L) -> mark# L, mark# adx X -> adx# mark X)
     (active# tail cons(X, L) -> mark# L, mark# adx X -> active# adx mark X)
     (active# tail cons(X, L) -> mark# L, mark# adx X -> mark# X)
     (active# tail cons(X, L) -> mark# L, mark# s X -> s# mark X)
     (active# tail cons(X, L) -> mark# L, mark# s X -> active# s mark X)
     (active# tail cons(X, L) -> mark# L, mark# s X -> mark# X)
     (active# tail cons(X, L) -> mark# L, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# tail cons(X, L) -> mark# L, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# tail cons(X, L) -> mark# L, mark# cons(X1, X2) -> mark# X1)
     (active# tail cons(X, L) -> mark# L, mark# incr X -> incr# mark X)
     (active# tail cons(X, L) -> mark# L, mark# incr X -> active# incr mark X)
     (active# tail cons(X, L) -> mark# L, mark# incr X -> mark# X)
     (active# tail cons(X, L) -> mark# L, mark# nil() -> active# nil())
     (active# adx cons(X, L) -> incr# cons(X, adx L), incr# active X -> incr# X)
     (active# adx cons(X, L) -> incr# cons(X, adx L), incr# mark X -> incr# X)
     (mark# incr X -> incr# mark X, incr# active X -> incr# X)
     (mark# incr X -> incr# mark X, incr# mark X -> incr# X)
     (mark# adx X -> adx# mark X, adx# active X -> adx# X)
     (mark# adx X -> adx# mark X, adx# mark X -> adx# X)
     (mark# tail X -> tail# mark X, tail# active X -> tail# X)
     (mark# tail X -> tail# mark X, tail# mark X -> tail# X)
     (mark# head X -> head# mark X, head# mark X -> head# X)
     (mark# head X -> head# mark X, head# active X -> head# X)
     (mark# s X -> s# mark X, s# mark X -> s# X)
     (mark# s X -> s# mark X, s# active X -> s# X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# nil() -> active# nil())
     (active# zeros() -> mark# cons(0(), zeros()), mark# incr X -> mark# X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# incr X -> active# incr mark X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# incr X -> incr# mark X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> mark# X1)
     (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# zeros() -> mark# cons(0(), zeros()), mark# s X -> mark# X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# s X -> active# s mark X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# s X -> s# mark X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# adx X -> mark# X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# adx X -> active# adx mark X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# adx X -> adx# mark X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# zeros() -> active# zeros())
     (active# zeros() -> mark# cons(0(), zeros()), mark# nats() -> active# nats())
     (active# zeros() -> mark# cons(0(), zeros()), mark# 0() -> active# 0())
     (active# zeros() -> mark# cons(0(), zeros()), mark# head X -> mark# X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# head X -> active# head mark X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# head X -> head# mark X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# tail X -> mark# X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# tail X -> active# tail mark X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# tail X -> tail# mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# nil() -> active# nil())
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# incr X -> mark# X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# incr X -> active# incr mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# incr X -> incr# mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# cons(X1, X2) -> mark# X1)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# s X -> mark# X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# s X -> active# s mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# s X -> s# mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# adx X -> mark# X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# adx X -> active# adx mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# adx X -> adx# mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# zeros() -> active# zeros())
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# nats() -> active# nats())
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# 0() -> active# 0())
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# head X -> mark# X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# head X -> active# head mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# head X -> head# mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# tail X -> mark# X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# tail X -> active# tail mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# tail X -> tail# mark X)
     (active# adx cons(X, L) -> adx# L, adx# mark X -> adx# X)
     (active# adx cons(X, L) -> adx# L, adx# active X -> adx# X)
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> mark# X1, mark# nil() -> active# nil())
     (mark# cons(X1, X2) -> mark# X1, mark# incr X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# incr X -> active# incr mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# incr X -> incr# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# adx X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# adx X -> active# adx mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# adx X -> adx# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# zeros() -> active# zeros())
     (mark# cons(X1, X2) -> mark# X1, mark# nats() -> active# nats())
     (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0())
     (mark# cons(X1, X2) -> mark# X1, mark# head X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# head X -> active# head mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# head X -> head# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# tail X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# tail X -> active# tail mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# tail X -> tail# mark X)
     (active# zeros() -> cons#(0(), zeros()), cons#(X1, mark X2) -> cons#(X1, X2))
     (active# zeros() -> cons#(0(), zeros()), cons#(X1, active X2) -> cons#(X1, X2))
     (active# zeros() -> cons#(0(), zeros()), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# zeros() -> cons#(0(), zeros()), cons#(active X1, X2) -> cons#(X1, X2))
     (active# incr cons(X, L) -> cons#(s X, incr L), cons#(X1, mark X2) -> cons#(X1, X2))
     (active# incr cons(X, L) -> cons#(s X, incr L), cons#(X1, active X2) -> cons#(X1, X2))
     (active# incr cons(X, L) -> cons#(s X, incr L), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# incr cons(X, L) -> cons#(s X, incr L), cons#(active X1, X2) -> cons#(X1, X2))
     (active# nats() -> mark# adx zeros(), mark# nil() -> active# nil())
     (active# nats() -> mark# adx zeros(), mark# incr X -> mark# X)
     (active# nats() -> mark# adx zeros(), mark# incr X -> active# incr mark X)
     (active# nats() -> mark# adx zeros(), mark# incr X -> incr# mark X)
     (active# nats() -> mark# adx zeros(), mark# cons(X1, X2) -> mark# X1)
     (active# nats() -> mark# adx zeros(), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# nats() -> mark# adx zeros(), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# nats() -> mark# adx zeros(), mark# s X -> mark# X)
     (active# nats() -> mark# adx zeros(), mark# s X -> active# s mark X)
     (active# nats() -> mark# adx zeros(), mark# s X -> s# mark X)
     (active# nats() -> mark# adx zeros(), mark# adx X -> mark# X)
     (active# nats() -> mark# adx zeros(), mark# adx X -> active# adx mark X)
     (active# nats() -> mark# adx zeros(), mark# adx X -> adx# mark X)
     (active# nats() -> mark# adx zeros(), mark# zeros() -> active# zeros())
     (active# nats() -> mark# adx zeros(), mark# nats() -> active# nats())
     (active# nats() -> mark# adx zeros(), mark# 0() -> active# 0())
     (active# nats() -> mark# adx zeros(), mark# head X -> mark# X)
     (active# nats() -> mark# adx zeros(), mark# head X -> active# head mark X)
     (active# nats() -> mark# adx zeros(), mark# head X -> head# mark X)
     (active# nats() -> mark# adx zeros(), mark# tail X -> mark# X)
     (active# nats() -> mark# adx zeros(), mark# tail X -> active# tail mark X)
     (active# nats() -> mark# adx zeros(), mark# tail X -> tail# mark X)
     (mark# tail X -> active# tail mark X, active# incr nil() -> mark# nil())
     (mark# tail X -> active# tail mark X, active# incr cons(X, L) -> mark# cons(s X, incr L))
     (mark# tail X -> active# tail mark X, active# incr cons(X, L) -> incr# L)
     (mark# tail X -> active# tail mark X, active# incr cons(X, L) -> cons#(s X, incr L))
     (mark# tail X -> active# tail mark X, active# incr cons(X, L) -> s# X)
     (mark# tail X -> active# tail mark X, active# adx nil() -> mark# nil())
     (mark# tail X -> active# tail mark X, active# adx cons(X, L) -> mark# incr cons(X, adx L))
     (mark# tail X -> active# tail mark X, active# adx cons(X, L) -> incr# cons(X, adx L))
     (mark# tail X -> active# tail mark X, active# adx cons(X, L) -> cons#(X, adx L))
     (mark# tail X -> active# tail mark X, active# adx cons(X, L) -> adx# L)
     (mark# tail X -> active# tail mark X, active# zeros() -> mark# cons(0(), zeros()))
     (mark# tail X -> active# tail mark X, active# zeros() -> cons#(0(), zeros()))
     (mark# tail X -> active# tail mark X, active# nats() -> mark# adx zeros())
     (mark# tail X -> active# tail mark X, active# nats() -> adx# zeros())
     (mark# tail X -> active# tail mark X, active# head cons(X, L) -> mark# X)
     (mark# tail X -> active# tail mark X, active# tail cons(X, L) -> mark# L)
     (mark# adx X -> active# adx mark X, active# incr nil() -> mark# nil())
     (mark# adx X -> active# adx mark X, active# incr cons(X, L) -> mark# cons(s X, incr L))
     (mark# adx X -> active# adx mark X, active# incr cons(X, L) -> incr# L)
     (mark# adx X -> active# adx mark X, active# incr cons(X, L) -> cons#(s X, incr L))
     (mark# adx X -> active# adx mark X, active# incr cons(X, L) -> s# X)
     (mark# adx X -> active# adx mark X, active# adx nil() -> mark# nil())
     (mark# adx X -> active# adx mark X, active# adx cons(X, L) -> mark# incr cons(X, adx L))
     (mark# adx X -> active# adx mark X, active# adx cons(X, L) -> incr# cons(X, adx L))
     (mark# adx X -> active# adx mark X, active# adx cons(X, L) -> cons#(X, adx L))
     (mark# adx X -> active# adx mark X, active# adx cons(X, L) -> adx# L)
     (mark# adx X -> active# adx mark X, active# zeros() -> mark# cons(0(), zeros()))
     (mark# adx X -> active# adx mark X, active# zeros() -> cons#(0(), zeros()))
     (mark# adx X -> active# adx mark X, active# nats() -> mark# adx zeros())
     (mark# adx X -> active# adx mark X, active# nats() -> adx# zeros())
     (mark# adx X -> active# adx mark X, active# head cons(X, L) -> mark# X)
     (mark# adx X -> active# adx mark X, active# tail cons(X, L) -> mark# L)
     (mark# incr X -> active# incr mark X, active# incr nil() -> mark# nil())
     (mark# incr X -> active# incr mark X, active# incr cons(X, L) -> mark# cons(s X, incr L))
     (mark# incr X -> active# incr mark X, active# incr cons(X, L) -> incr# L)
     (mark# incr X -> active# incr mark X, active# incr cons(X, L) -> cons#(s X, incr L))
     (mark# incr X -> active# incr mark X, active# incr cons(X, L) -> s# X)
     (mark# incr X -> active# incr mark X, active# adx nil() -> mark# nil())
     (mark# incr X -> active# incr mark X, active# adx cons(X, L) -> mark# incr cons(X, adx L))
     (mark# incr X -> active# incr mark X, active# adx cons(X, L) -> incr# cons(X, adx L))
     (mark# incr X -> active# incr mark X, active# adx cons(X, L) -> cons#(X, adx L))
     (mark# incr X -> active# incr mark X, active# adx cons(X, L) -> adx# L)
     (mark# incr X -> active# incr mark X, active# zeros() -> mark# cons(0(), zeros()))
     (mark# incr X -> active# incr mark X, active# zeros() -> cons#(0(), zeros()))
     (mark# incr X -> active# incr mark X, active# nats() -> mark# adx zeros())
     (mark# incr X -> active# incr mark X, active# nats() -> adx# zeros())
     (mark# incr X -> active# incr mark X, active# head cons(X, L) -> mark# X)
     (mark# incr X -> active# incr mark X, active# tail cons(X, L) -> mark# L)
     (tail# mark X -> tail# X, tail# mark X -> tail# X)
     (tail# mark X -> tail# X, tail# active X -> tail# X)
     (head# mark X -> head# X, head# mark X -> head# X)
     (head# mark X -> head# X, head# active X -> head# X)
     (adx# mark X -> adx# X, adx# mark X -> adx# X)
     (adx# mark X -> adx# X, adx# active X -> adx# X)
     (s# mark X -> s# X, s# mark X -> s# X)
     (s# mark X -> s# X, s# active X -> s# X)
     (incr# mark X -> incr# X, incr# mark X -> incr# X)
     (incr# mark X -> incr# X, incr# active X -> incr# X)
     (active# incr cons(X, L) -> s# X, s# mark X -> s# X)
     (active# incr cons(X, L) -> s# X, s# active X -> s# X)
     (mark# head X -> mark# X, mark# nil() -> active# nil())
     (mark# head X -> mark# X, mark# incr X -> mark# X)
     (mark# head X -> mark# X, mark# incr X -> active# incr mark X)
     (mark# head X -> mark# X, mark# incr X -> incr# mark X)
     (mark# head X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# head X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# head X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# head X -> mark# X, mark# s X -> mark# X)
     (mark# head X -> mark# X, mark# s X -> active# s mark X)
     (mark# head X -> mark# X, mark# s X -> s# mark X)
     (mark# head X -> mark# X, mark# adx X -> mark# X)
     (mark# head X -> mark# X, mark# adx X -> active# adx mark X)
     (mark# head X -> mark# X, mark# adx X -> adx# mark X)
     (mark# head X -> mark# X, mark# zeros() -> active# zeros())
     (mark# head X -> mark# X, mark# nats() -> active# nats())
     (mark# head X -> mark# X, mark# 0() -> active# 0())
     (mark# head X -> mark# X, mark# head X -> mark# X)
     (mark# head X -> mark# X, mark# head X -> active# head mark X)
     (mark# head X -> mark# X, mark# head X -> head# mark X)
     (mark# head X -> mark# X, mark# tail X -> mark# X)
     (mark# head X -> mark# X, mark# tail X -> active# tail mark X)
     (mark# head X -> mark# X, mark# tail X -> tail# mark X)
     (mark# s X -> mark# X, mark# nil() -> active# nil())
     (mark# s X -> mark# X, mark# incr X -> mark# X)
     (mark# s X -> mark# X, mark# incr X -> active# incr mark X)
     (mark# s X -> mark# X, mark# incr X -> incr# mark X)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# s X -> mark# X, mark# s X -> active# s mark X)
     (mark# s X -> mark# X, mark# s X -> s# mark X)
     (mark# s X -> mark# X, mark# adx X -> mark# X)
     (mark# s X -> mark# X, mark# adx X -> active# adx mark X)
     (mark# s X -> mark# X, mark# adx X -> adx# mark X)
     (mark# s X -> mark# X, mark# zeros() -> active# zeros())
     (mark# s X -> mark# X, mark# nats() -> active# nats())
     (mark# s X -> mark# X, mark# 0() -> active# 0())
     (mark# s X -> mark# X, mark# head X -> mark# X)
     (mark# s X -> mark# X, mark# head X -> active# head mark X)
     (mark# s X -> mark# X, mark# head X -> head# mark X)
     (mark# s X -> mark# X, mark# tail X -> mark# X)
     (mark# s X -> mark# X, mark# tail X -> active# tail mark X)
     (mark# s X -> mark# X, mark# tail X -> tail# mark X)
     (active# nats() -> adx# zeros(), adx# mark X -> adx# X)
     (active# nats() -> adx# zeros(), adx# active X -> adx# X)
     (active# incr nil() -> mark# nil(), mark# nil() -> active# nil())
     (active# incr nil() -> mark# nil(), mark# incr X -> mark# X)
     (active# incr nil() -> mark# nil(), mark# incr X -> active# incr mark X)
     (active# incr nil() -> mark# nil(), mark# incr X -> incr# mark X)
     (active# incr nil() -> mark# nil(), mark# cons(X1, X2) -> mark# X1)
     (active# incr nil() -> mark# nil(), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# incr nil() -> mark# nil(), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# incr nil() -> mark# nil(), mark# s X -> mark# X)
     (active# incr nil() -> mark# nil(), mark# s X -> active# s mark X)
     (active# incr nil() -> mark# nil(), mark# s X -> s# mark X)
     (active# incr nil() -> mark# nil(), mark# adx X -> mark# X)
     (active# incr nil() -> mark# nil(), mark# adx X -> active# adx mark X)
     (active# incr nil() -> mark# nil(), mark# adx X -> adx# mark X)
     (active# incr nil() -> mark# nil(), mark# zeros() -> active# zeros())
     (active# incr nil() -> mark# nil(), mark# nats() -> active# nats())
     (active# incr nil() -> mark# nil(), mark# 0() -> active# 0())
     (active# incr nil() -> mark# nil(), mark# head X -> mark# X)
     (active# incr nil() -> mark# nil(), mark# head X -> active# head mark X)
     (active# incr nil() -> mark# nil(), mark# head X -> head# mark X)
     (active# incr nil() -> mark# nil(), mark# tail X -> mark# X)
     (active# incr nil() -> mark# nil(), mark# tail X -> active# tail mark X)
     (active# incr nil() -> mark# nil(), mark# tail X -> tail# mark X)
     (mark# nats() -> active# nats(), active# incr nil() -> mark# nil())
     (mark# nats() -> active# nats(), active# incr cons(X, L) -> mark# cons(s X, incr L))
     (mark# nats() -> active# nats(), active# incr cons(X, L) -> incr# L)
     (mark# nats() -> active# nats(), active# incr cons(X, L) -> cons#(s X, incr L))
     (mark# nats() -> active# nats(), active# incr cons(X, L) -> s# X)
     (mark# nats() -> active# nats(), active# adx nil() -> mark# nil())
     (mark# nats() -> active# nats(), active# adx cons(X, L) -> mark# incr cons(X, adx L))
     (mark# nats() -> active# nats(), active# adx cons(X, L) -> incr# cons(X, adx L))
     (mark# nats() -> active# nats(), active# adx cons(X, L) -> cons#(X, adx L))
     (mark# nats() -> active# nats(), active# adx cons(X, L) -> adx# L)
     (mark# nats() -> active# nats(), active# zeros() -> mark# cons(0(), zeros()))
     (mark# nats() -> active# nats(), active# zeros() -> cons#(0(), zeros()))
     (mark# nats() -> active# nats(), active# nats() -> mark# adx zeros())
     (mark# nats() -> active# nats(), active# nats() -> adx# zeros())
     (mark# nats() -> active# nats(), active# head cons(X, L) -> mark# X)
     (mark# nats() -> active# nats(), active# tail cons(X, L) -> mark# L)
     (mark# nil() -> active# nil(), active# incr nil() -> mark# nil())
     (mark# nil() -> active# nil(), active# incr cons(X, L) -> mark# cons(s X, incr L))
     (mark# nil() -> active# nil(), active# incr cons(X, L) -> incr# L)
     (mark# nil() -> active# nil(), active# incr cons(X, L) -> cons#(s X, incr L))
     (mark# nil() -> active# nil(), active# incr cons(X, L) -> s# X)
     (mark# nil() -> active# nil(), active# adx nil() -> mark# nil())
     (mark# nil() -> active# nil(), active# adx cons(X, L) -> mark# incr cons(X, adx L))
     (mark# nil() -> active# nil(), active# adx cons(X, L) -> incr# cons(X, adx L))
     (mark# nil() -> active# nil(), active# adx cons(X, L) -> cons#(X, adx L))
     (mark# nil() -> active# nil(), active# adx cons(X, L) -> adx# L)
     (mark# nil() -> active# nil(), active# zeros() -> mark# cons(0(), zeros()))
     (mark# nil() -> active# nil(), active# zeros() -> cons#(0(), zeros()))
     (mark# nil() -> active# nil(), active# nats() -> mark# adx zeros())
     (mark# nil() -> active# nil(), active# nats() -> adx# zeros())
     (mark# nil() -> active# nil(), active# head cons(X, L) -> mark# X)
     (mark# nil() -> active# nil(), active# tail cons(X, L) -> mark# L)
    }
    EDG:
     {
      (mark# zeros() -> active# zeros(), active# zeros() -> cons#(0(), zeros()))
      (mark# zeros() -> active# zeros(), active# zeros() -> mark# cons(0(), zeros()))
      (active# adx nil() -> mark# nil(), mark# nil() -> active# nil())
      (mark# incr X -> mark# X, mark# tail X -> tail# mark X)
      (mark# incr X -> mark# X, mark# tail X -> active# tail mark X)
      (mark# incr X -> mark# X, mark# tail X -> mark# X)
      (mark# incr X -> mark# X, mark# head X -> head# mark X)
      (mark# incr X -> mark# X, mark# head X -> active# head mark X)
      (mark# incr X -> mark# X, mark# head X -> mark# X)
      (mark# incr X -> mark# X, mark# 0() -> active# 0())
      (mark# incr X -> mark# X, mark# nats() -> active# nats())
      (mark# incr X -> mark# X, mark# zeros() -> active# zeros())
      (mark# incr X -> mark# X, mark# adx X -> adx# mark X)
      (mark# incr X -> mark# X, mark# adx X -> active# adx mark X)
      (mark# incr X -> mark# X, mark# adx X -> mark# X)
      (mark# incr X -> mark# X, mark# s X -> s# mark X)
      (mark# incr X -> mark# X, mark# s X -> active# s mark X)
      (mark# incr X -> mark# X, mark# s X -> mark# X)
      (mark# incr X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# incr X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# incr X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# incr X -> mark# X, mark# incr X -> incr# mark X)
      (mark# incr X -> mark# X, mark# incr X -> active# incr mark X)
      (mark# incr X -> mark# X, mark# incr X -> mark# X)
      (mark# incr X -> mark# X, mark# nil() -> active# nil())
      (mark# adx X -> mark# X, mark# tail X -> tail# mark X)
      (mark# adx X -> mark# X, mark# tail X -> active# tail mark X)
      (mark# adx X -> mark# X, mark# tail X -> mark# X)
      (mark# adx X -> mark# X, mark# head X -> head# mark X)
      (mark# adx X -> mark# X, mark# head X -> active# head mark X)
      (mark# adx X -> mark# X, mark# head X -> mark# X)
      (mark# adx X -> mark# X, mark# 0() -> active# 0())
      (mark# adx X -> mark# X, mark# nats() -> active# nats())
      (mark# adx X -> mark# X, mark# zeros() -> active# zeros())
      (mark# adx X -> mark# X, mark# adx X -> adx# mark X)
      (mark# adx X -> mark# X, mark# adx X -> active# adx mark X)
      (mark# adx X -> mark# X, mark# adx X -> mark# X)
      (mark# adx X -> mark# X, mark# s X -> s# mark X)
      (mark# adx X -> mark# X, mark# s X -> active# s mark X)
      (mark# adx X -> mark# X, mark# s X -> mark# X)
      (mark# adx X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# adx X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# adx X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# adx X -> mark# X, mark# incr X -> incr# mark X)
      (mark# adx X -> mark# X, mark# incr X -> active# incr mark X)
      (mark# adx X -> mark# X, mark# incr X -> mark# X)
      (mark# adx X -> mark# X, mark# nil() -> active# nil())
      (mark# tail X -> mark# X, mark# tail X -> tail# mark X)
      (mark# tail X -> mark# X, mark# tail X -> active# tail mark X)
      (mark# tail X -> mark# X, mark# tail X -> mark# X)
      (mark# tail X -> mark# X, mark# head X -> head# mark X)
      (mark# tail X -> mark# X, mark# head X -> active# head mark X)
      (mark# tail X -> mark# X, mark# head X -> mark# X)
      (mark# tail X -> mark# X, mark# 0() -> active# 0())
      (mark# tail X -> mark# X, mark# nats() -> active# nats())
      (mark# tail X -> mark# X, mark# zeros() -> active# zeros())
      (mark# tail X -> mark# X, mark# adx X -> adx# mark X)
      (mark# tail X -> mark# X, mark# adx X -> active# adx mark X)
      (mark# tail X -> mark# X, mark# adx X -> mark# X)
      (mark# tail X -> mark# X, mark# s X -> s# mark X)
      (mark# tail X -> mark# X, mark# s X -> active# s mark X)
      (mark# tail X -> mark# X, mark# s X -> mark# X)
      (mark# tail X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# tail X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# tail X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# tail X -> mark# X, mark# incr X -> incr# mark X)
      (mark# tail X -> mark# X, mark# incr X -> active# incr mark X)
      (mark# tail X -> mark# X, mark# incr X -> mark# X)
      (mark# tail X -> mark# X, mark# nil() -> active# nil())
      (active# head cons(X, L) -> mark# X, mark# tail X -> tail# mark X)
      (active# head cons(X, L) -> mark# X, mark# tail X -> active# tail mark X)
      (active# head cons(X, L) -> mark# X, mark# tail X -> mark# X)
      (active# head cons(X, L) -> mark# X, mark# head X -> head# mark X)
      (active# head cons(X, L) -> mark# X, mark# head X -> active# head mark X)
      (active# head cons(X, L) -> mark# X, mark# head X -> mark# X)
      (active# head cons(X, L) -> mark# X, mark# 0() -> active# 0())
      (active# head cons(X, L) -> mark# X, mark# nats() -> active# nats())
      (active# head cons(X, L) -> mark# X, mark# zeros() -> active# zeros())
      (active# head cons(X, L) -> mark# X, mark# adx X -> adx# mark X)
      (active# head cons(X, L) -> mark# X, mark# adx X -> active# adx mark X)
      (active# head cons(X, L) -> mark# X, mark# adx X -> mark# X)
      (active# head cons(X, L) -> mark# X, mark# s X -> s# mark X)
      (active# head cons(X, L) -> mark# X, mark# s X -> active# s mark X)
      (active# head cons(X, L) -> mark# X, mark# s X -> mark# X)
      (active# head cons(X, L) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (active# head cons(X, L) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (active# head cons(X, L) -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (active# head cons(X, L) -> mark# X, mark# incr X -> incr# mark X)
      (active# head cons(X, L) -> mark# X, mark# incr X -> active# incr mark X)
      (active# head cons(X, L) -> mark# X, mark# incr X -> mark# X)
      (active# head cons(X, L) -> mark# X, mark# nil() -> active# nil())
      (incr# active X -> incr# X, incr# active X -> incr# X)
      (incr# active X -> incr# X, incr# mark X -> incr# X)
      (s# active X -> s# X, s# active X -> s# X)
      (s# active X -> s# X, s# mark X -> s# X)
      (adx# active X -> adx# X, adx# active X -> adx# X)
      (adx# active X -> adx# X, adx# mark X -> adx# X)
      (head# active X -> head# X, head# active X -> head# X)
      (head# active X -> head# X, head# mark X -> head# X)
      (tail# active X -> tail# X, tail# active X -> tail# X)
      (tail# active X -> tail# X, tail# mark X -> tail# X)
      (mark# s X -> active# s mark X, active# tail cons(X, L) -> mark# L)
      (mark# s X -> active# s mark X, active# head cons(X, L) -> mark# X)
      (mark# s X -> active# s mark X, active# adx cons(X, L) -> adx# L)
      (mark# s X -> active# s mark X, active# adx cons(X, L) -> cons#(X, adx L))
      (mark# s X -> active# s mark X, active# adx cons(X, L) -> incr# cons(X, adx L))
      (mark# s X -> active# s mark X, active# adx cons(X, L) -> mark# incr cons(X, adx L))
      (mark# s X -> active# s mark X, active# adx nil() -> mark# nil())
      (mark# s X -> active# s mark X, active# incr cons(X, L) -> s# X)
      (mark# s X -> active# s mark X, active# incr cons(X, L) -> cons#(s X, incr L))
      (mark# s X -> active# s mark X, active# incr cons(X, L) -> incr# L)
      (mark# s X -> active# s mark X, active# incr cons(X, L) -> mark# cons(s X, incr L))
      (mark# s X -> active# s mark X, active# incr nil() -> mark# nil())
      (mark# head X -> active# head mark X, active# tail cons(X, L) -> mark# L)
      (mark# head X -> active# head mark X, active# head cons(X, L) -> mark# X)
      (mark# head X -> active# head mark X, active# adx cons(X, L) -> adx# L)
      (mark# head X -> active# head mark X, active# adx cons(X, L) -> cons#(X, adx L))
      (mark# head X -> active# head mark X, active# adx cons(X, L) -> incr# cons(X, adx L))
      (mark# head X -> active# head mark X, active# adx cons(X, L) -> mark# incr cons(X, adx L))
      (mark# head X -> active# head mark X, active# adx nil() -> mark# nil())
      (mark# head X -> active# head mark X, active# incr cons(X, L) -> s# X)
      (mark# head X -> active# head mark X, active# incr cons(X, L) -> cons#(s X, incr L))
      (mark# head X -> active# head mark X, active# incr cons(X, L) -> incr# L)
      (mark# head X -> active# head mark X, active# incr cons(X, L) -> mark# cons(s X, incr L))
      (mark# head X -> active# head mark X, active# incr nil() -> mark# nil())
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# tail X -> tail# mark X)
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# tail X -> active# tail mark X)
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# tail X -> mark# X)
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# head X -> head# mark X)
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# head X -> active# head mark X)
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# head X -> mark# X)
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# adx X -> adx# mark X)
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# adx X -> active# adx mark X)
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# adx X -> mark# X)
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# s X -> s# mark X)
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# s X -> active# s mark X)
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# s X -> mark# X)
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# cons(X1, X2) -> cons#(mark X1, X2))
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# cons(X1, X2) -> mark# X1)
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# incr X -> incr# mark X)
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# incr X -> active# incr mark X)
      (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# incr X -> mark# X)
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# tail cons(X, L) -> mark# L)
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# head cons(X, L) -> mark# X)
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# adx cons(X, L) -> adx# L)
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# adx cons(X, L) -> cons#(X, adx L))
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# adx cons(X, L) -> incr# cons(X, adx L))
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# adx cons(X, L) -> mark# incr cons(X, adx L))
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# adx nil() -> mark# nil())
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr cons(X, L) -> s# X)
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr cons(X, L) -> cons#(s X, incr L))
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr cons(X, L) -> incr# L)
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr cons(X, L) -> mark# cons(s X, incr L))
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# incr nil() -> mark# nil())
      (active# adx cons(X, L) -> cons#(X, adx L), cons#(X1, active X2) -> cons#(X1, X2))
      (active# adx cons(X, L) -> cons#(X, adx L), cons#(X1, mark X2) -> cons#(X1, X2))
      (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
      (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
      (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
      (cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
      (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
      (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
      (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
      (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
      (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
      (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
      (active# tail cons(X, L) -> mark# L, mark# tail X -> tail# mark X)
      (active# tail cons(X, L) -> mark# L, mark# tail X -> active# tail mark X)
      (active# tail cons(X, L) -> mark# L, mark# tail X -> mark# X)
      (active# tail cons(X, L) -> mark# L, mark# head X -> head# mark X)
      (active# tail cons(X, L) -> mark# L, mark# head X -> active# head mark X)
      (active# tail cons(X, L) -> mark# L, mark# head X -> mark# X)
      (active# tail cons(X, L) -> mark# L, mark# 0() -> active# 0())
      (active# tail cons(X, L) -> mark# L, mark# nats() -> active# nats())
      (active# tail cons(X, L) -> mark# L, mark# zeros() -> active# zeros())
      (active# tail cons(X, L) -> mark# L, mark# adx X -> adx# mark X)
      (active# tail cons(X, L) -> mark# L, mark# adx X -> active# adx mark X)
      (active# tail cons(X, L) -> mark# L, mark# adx X -> mark# X)
      (active# tail cons(X, L) -> mark# L, mark# s X -> s# mark X)
      (active# tail cons(X, L) -> mark# L, mark# s X -> active# s mark X)
      (active# tail cons(X, L) -> mark# L, mark# s X -> mark# X)
      (active# tail cons(X, L) -> mark# L, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (active# tail cons(X, L) -> mark# L, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (active# tail cons(X, L) -> mark# L, mark# cons(X1, X2) -> mark# X1)
      (active# tail cons(X, L) -> mark# L, mark# incr X -> incr# mark X)
      (active# tail cons(X, L) -> mark# L, mark# incr X -> active# incr mark X)
      (active# tail cons(X, L) -> mark# L, mark# incr X -> mark# X)
      (active# tail cons(X, L) -> mark# L, mark# nil() -> active# nil())
      (active# adx cons(X, L) -> incr# cons(X, adx L), incr# active X -> incr# X)
      (active# adx cons(X, L) -> incr# cons(X, adx L), incr# mark X -> incr# X)
      (mark# incr X -> incr# mark X, incr# active X -> incr# X)
      (mark# incr X -> incr# mark X, incr# mark X -> incr# X)
      (mark# adx X -> adx# mark X, adx# active X -> adx# X)
      (mark# adx X -> adx# mark X, adx# mark X -> adx# X)
      (mark# tail X -> tail# mark X, tail# active X -> tail# X)
      (mark# tail X -> tail# mark X, tail# mark X -> tail# X)
      (mark# head X -> head# mark X, head# mark X -> head# X)
      (mark# head X -> head# mark X, head# active X -> head# X)
      (mark# s X -> s# mark X, s# mark X -> s# X)
      (mark# s X -> s# mark X, s# active X -> s# X)
      (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> mark# X1)
      (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> cons#(mark X1, X2))
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# incr X -> mark# X)
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# incr X -> active# incr mark X)
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# incr X -> incr# mark X)
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# cons(X1, X2) -> mark# X1)
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# cons(X1, X2) -> cons#(mark X1, X2))
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# s X -> mark# X)
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# s X -> active# s mark X)
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# s X -> s# mark X)
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# adx X -> mark# X)
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# adx X -> active# adx mark X)
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# adx X -> adx# mark X)
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# head X -> mark# X)
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# head X -> active# head mark X)
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# head X -> head# mark X)
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# tail X -> mark# X)
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# tail X -> active# tail mark X)
      (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# tail X -> tail# mark X)
      (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
      (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
      (cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
      (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
      (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
      (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
      (cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
      (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
      (mark# cons(X1, X2) -> mark# X1, mark# nil() -> active# nil())
      (mark# cons(X1, X2) -> mark# X1, mark# incr X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# incr X -> active# incr mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# incr X -> incr# mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
      (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# adx X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# adx X -> active# adx mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# adx X -> adx# mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# zeros() -> active# zeros())
      (mark# cons(X1, X2) -> mark# X1, mark# nats() -> active# nats())
      (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0())
      (mark# cons(X1, X2) -> mark# X1, mark# head X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# head X -> active# head mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# head X -> head# mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# tail X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# tail X -> active# tail mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# tail X -> tail# mark X)
      (active# incr cons(X, L) -> cons#(s X, incr L), cons#(X1, mark X2) -> cons#(X1, X2))
      (active# incr cons(X, L) -> cons#(s X, incr L), cons#(X1, active X2) -> cons#(X1, X2))
      (active# incr cons(X, L) -> cons#(s X, incr L), cons#(mark X1, X2) -> cons#(X1, X2))
      (active# incr cons(X, L) -> cons#(s X, incr L), cons#(active X1, X2) -> cons#(X1, X2))
      (active# nats() -> mark# adx zeros(), mark# adx X -> mark# X)
      (active# nats() -> mark# adx zeros(), mark# adx X -> active# adx mark X)
      (active# nats() -> mark# adx zeros(), mark# adx X -> adx# mark X)
      (mark# tail X -> active# tail mark X, active# incr nil() -> mark# nil())
      (mark# tail X -> active# tail mark X, active# incr cons(X, L) -> mark# cons(s X, incr L))
      (mark# tail X -> active# tail mark X, active# incr cons(X, L) -> incr# L)
      (mark# tail X -> active# tail mark X, active# incr cons(X, L) -> cons#(s X, incr L))
      (mark# tail X -> active# tail mark X, active# incr cons(X, L) -> s# X)
      (mark# tail X -> active# tail mark X, active# adx nil() -> mark# nil())
      (mark# tail X -> active# tail mark X, active# adx cons(X, L) -> mark# incr cons(X, adx L))
      (mark# tail X -> active# tail mark X, active# adx cons(X, L) -> incr# cons(X, adx L))
      (mark# tail X -> active# tail mark X, active# adx cons(X, L) -> cons#(X, adx L))
      (mark# tail X -> active# tail mark X, active# adx cons(X, L) -> adx# L)
      (mark# tail X -> active# tail mark X, active# head cons(X, L) -> mark# X)
      (mark# tail X -> active# tail mark X, active# tail cons(X, L) -> mark# L)
      (mark# adx X -> active# adx mark X, active# incr nil() -> mark# nil())
      (mark# adx X -> active# adx mark X, active# incr cons(X, L) -> mark# cons(s X, incr L))
      (mark# adx X -> active# adx mark X, active# incr cons(X, L) -> incr# L)
      (mark# adx X -> active# adx mark X, active# incr cons(X, L) -> cons#(s X, incr L))
      (mark# adx X -> active# adx mark X, active# incr cons(X, L) -> s# X)
      (mark# adx X -> active# adx mark X, active# adx nil() -> mark# nil())
      (mark# adx X -> active# adx mark X, active# adx cons(X, L) -> mark# incr cons(X, adx L))
      (mark# adx X -> active# adx mark X, active# adx cons(X, L) -> incr# cons(X, adx L))
      (mark# adx X -> active# adx mark X, active# adx cons(X, L) -> cons#(X, adx L))
      (mark# adx X -> active# adx mark X, active# adx cons(X, L) -> adx# L)
      (mark# adx X -> active# adx mark X, active# head cons(X, L) -> mark# X)
      (mark# adx X -> active# adx mark X, active# tail cons(X, L) -> mark# L)
      (mark# incr X -> active# incr mark X, active# incr nil() -> mark# nil())
      (mark# incr X -> active# incr mark X, active# incr cons(X, L) -> mark# cons(s X, incr L))
      (mark# incr X -> active# incr mark X, active# incr cons(X, L) -> incr# L)
      (mark# incr X -> active# incr mark X, active# incr cons(X, L) -> cons#(s X, incr L))
      (mark# incr X -> active# incr mark X, active# incr cons(X, L) -> s# X)
      (mark# incr X -> active# incr mark X, active# adx nil() -> mark# nil())
      (mark# incr X -> active# incr mark X, active# adx cons(X, L) -> mark# incr cons(X, adx L))
      (mark# incr X -> active# incr mark X, active# adx cons(X, L) -> incr# cons(X, adx L))
      (mark# incr X -> active# incr mark X, active# adx cons(X, L) -> cons#(X, adx L))
      (mark# incr X -> active# incr mark X, active# adx cons(X, L) -> adx# L)
      (mark# incr X -> active# incr mark X, active# head cons(X, L) -> mark# X)
      (mark# incr X -> active# incr mark X, active# tail cons(X, L) -> mark# L)
      (tail# mark X -> tail# X, tail# mark X -> tail# X)
      (tail# mark X -> tail# X, tail# active X -> tail# X)
      (head# mark X -> head# X, head# mark X -> head# X)
      (head# mark X -> head# X, head# active X -> head# X)
      (adx# mark X -> adx# X, adx# mark X -> adx# X)
      (adx# mark X -> adx# X, adx# active X -> adx# X)
      (s# mark X -> s# X, s# mark X -> s# X)
      (s# mark X -> s# X, s# active X -> s# X)
      (incr# mark X -> incr# X, incr# mark X -> incr# X)
      (incr# mark X -> incr# X, incr# active X -> incr# X)
      (mark# head X -> mark# X, mark# nil() -> active# nil())
      (mark# head X -> mark# X, mark# incr X -> mark# X)
      (mark# head X -> mark# X, mark# incr X -> active# incr mark X)
      (mark# head X -> mark# X, mark# incr X -> incr# mark X)
      (mark# head X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# head X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# head X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# head X -> mark# X, mark# s X -> mark# X)
      (mark# head X -> mark# X, mark# s X -> active# s mark X)
      (mark# head X -> mark# X, mark# s X -> s# mark X)
      (mark# head X -> mark# X, mark# adx X -> mark# X)
      (mark# head X -> mark# X, mark# adx X -> active# adx mark X)
      (mark# head X -> mark# X, mark# adx X -> adx# mark X)
      (mark# head X -> mark# X, mark# zeros() -> active# zeros())
      (mark# head X -> mark# X, mark# nats() -> active# nats())
      (mark# head X -> mark# X, mark# 0() -> active# 0())
      (mark# head X -> mark# X, mark# head X -> mark# X)
      (mark# head X -> mark# X, mark# head X -> active# head mark X)
      (mark# head X -> mark# X, mark# head X -> head# mark X)
      (mark# head X -> mark# X, mark# tail X -> mark# X)
      (mark# head X -> mark# X, mark# tail X -> active# tail mark X)
      (mark# head X -> mark# X, mark# tail X -> tail# mark X)
      (mark# s X -> mark# X, mark# nil() -> active# nil())
      (mark# s X -> mark# X, mark# incr X -> mark# X)
      (mark# s X -> mark# X, mark# incr X -> active# incr mark X)
      (mark# s X -> mark# X, mark# incr X -> incr# mark X)
      (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# s X -> mark# X, mark# s X -> mark# X)
      (mark# s X -> mark# X, mark# s X -> active# s mark X)
      (mark# s X -> mark# X, mark# s X -> s# mark X)
      (mark# s X -> mark# X, mark# adx X -> mark# X)
      (mark# s X -> mark# X, mark# adx X -> active# adx mark X)
      (mark# s X -> mark# X, mark# adx X -> adx# mark X)
      (mark# s X -> mark# X, mark# zeros() -> active# zeros())
      (mark# s X -> mark# X, mark# nats() -> active# nats())
      (mark# s X -> mark# X, mark# 0() -> active# 0())
      (mark# s X -> mark# X, mark# head X -> mark# X)
      (mark# s X -> mark# X, mark# head X -> active# head mark X)
      (mark# s X -> mark# X, mark# head X -> head# mark X)
      (mark# s X -> mark# X, mark# tail X -> mark# X)
      (mark# s X -> mark# X, mark# tail X -> active# tail mark X)
      (mark# s X -> mark# X, mark# tail X -> tail# mark X)
      (active# incr nil() -> mark# nil(), mark# nil() -> active# nil())
      (mark# nats() -> active# nats(), active# nats() -> mark# adx zeros())
      (mark# nats() -> active# nats(), active# nats() -> adx# zeros())
     }
     STATUS:
      arrows: 0.869822
      SCCS (7):
       Scc:
        {           mark# incr X -> mark# X,
                    mark# incr X -> active# incr mark X,
              mark# cons(X1, X2) -> mark# X1,
              mark# cons(X1, X2) -> active# cons(mark X1, X2),
                       mark# s X -> mark# X,
                       mark# s X -> active# s mark X,
                     mark# adx X -> mark# X,
                     mark# adx X -> active# adx mark X,
                   mark# zeros() -> active# zeros(),
                    mark# nats() -> active# nats(),
                    mark# head X -> mark# X,
                    mark# head X -> active# head mark X,
                    mark# tail X -> mark# X,
                    mark# tail X -> active# tail mark X,
         active# incr cons(X, L) -> mark# cons(s X, incr L),
          active# adx cons(X, L) -> mark# incr cons(X, adx L),
                 active# zeros() -> mark# cons(0(), zeros()),
                  active# nats() -> mark# adx zeros(),
         active# head cons(X, L) -> mark# X,
         active# tail cons(X, L) -> mark# L}
       Scc:
        {  tail# mark X -> tail# X,
         tail# active X -> tail# X}
       Scc:
        {  head# mark X -> head# X,
         head# active X -> head# X}
       Scc:
        {  adx# mark X -> adx# X,
         adx# active X -> adx# X}
       Scc:
        {  s# mark X -> s# X,
         s# active X -> s# X}
       Scc:
        {  cons#(X1, mark X2) -> cons#(X1, X2),
         cons#(X1, active X2) -> cons#(X1, X2),
           cons#(mark X1, X2) -> cons#(X1, X2),
         cons#(active X1, X2) -> cons#(X1, X2)}
       Scc:
        {  incr# mark X -> incr# X,
         incr# active X -> incr# X}
       
       SCC (20):
        Strict:
         {           mark# incr X -> mark# X,
                     mark# incr X -> active# incr mark X,
               mark# cons(X1, X2) -> mark# X1,
               mark# cons(X1, X2) -> active# cons(mark X1, X2),
                        mark# s X -> mark# X,
                        mark# s X -> active# s mark X,
                      mark# adx X -> mark# X,
                      mark# adx X -> active# adx mark X,
                    mark# zeros() -> active# zeros(),
                     mark# nats() -> active# nats(),
                     mark# head X -> mark# X,
                     mark# head X -> active# head mark X,
                     mark# tail X -> mark# X,
                     mark# tail X -> active# tail mark X,
          active# incr cons(X, L) -> mark# cons(s X, incr L),
           active# adx cons(X, L) -> mark# incr cons(X, adx L),
                  active# zeros() -> mark# cons(0(), zeros()),
                   active# nats() -> mark# adx zeros(),
          active# head cons(X, L) -> mark# X,
          active# tail cons(X, L) -> mark# L}
        Weak:
        {            mark nil() -> active nil(),
                    mark incr X -> active incr mark X,
              mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark s X -> active s mark X,
                     mark adx X -> active adx mark X,
                   mark zeros() -> active zeros(),
                    mark nats() -> active nats(),
                       mark 0() -> active 0(),
                    mark head X -> active head mark X,
                    mark tail X -> active tail mark X,
              active incr nil() -> mark nil(),
         active incr cons(X, L) -> mark cons(s X, incr L),
               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 cons(X, L) -> mark X,
         active tail cons(X, L) -> mark L,
                    incr mark X -> incr X,
                  incr active X -> incr X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                       s mark X -> s X,
                     s active X -> s X,
                     adx mark X -> adx X,
                   adx active X -> adx X,
                    head mark X -> head X,
                  head active X -> head X,
                    tail mark X -> tail X,
                  tail active X -> tail X}
        Open
       
       
       SCC (2):
        Strict:
         {  tail# mark X -> tail# X,
          tail# active X -> tail# X}
        Weak:
        {            mark nil() -> active nil(),
                    mark incr X -> active incr mark X,
              mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark s X -> active s mark X,
                     mark adx X -> active adx mark X,
                   mark zeros() -> active zeros(),
                    mark nats() -> active nats(),
                       mark 0() -> active 0(),
                    mark head X -> active head mark X,
                    mark tail X -> active tail mark X,
              active incr nil() -> mark nil(),
         active incr cons(X, L) -> mark cons(s X, incr L),
               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 cons(X, L) -> mark X,
         active tail cons(X, L) -> mark L,
                    incr mark X -> incr X,
                  incr active X -> incr X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                       s mark X -> s X,
                     s active X -> s X,
                     adx mark X -> adx X,
                   adx active X -> adx X,
                    head mark X -> head X,
                  head active X -> head X,
                    tail mark X -> tail X,
                  tail active X -> tail X}
        Open
       
       SCC (2):
        Strict:
         {  head# mark X -> head# X,
          head# active X -> head# X}
        Weak:
        {            mark nil() -> active nil(),
                    mark incr X -> active incr mark X,
              mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark s X -> active s mark X,
                     mark adx X -> active adx mark X,
                   mark zeros() -> active zeros(),
                    mark nats() -> active nats(),
                       mark 0() -> active 0(),
                    mark head X -> active head mark X,
                    mark tail X -> active tail mark X,
              active incr nil() -> mark nil(),
         active incr cons(X, L) -> mark cons(s X, incr L),
               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 cons(X, L) -> mark X,
         active tail cons(X, L) -> mark L,
                    incr mark X -> incr X,
                  incr active X -> incr X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                       s mark X -> s X,
                     s active X -> s X,
                     adx mark X -> adx X,
                   adx active X -> adx X,
                    head mark X -> head X,
                  head active X -> head X,
                    tail mark X -> tail X,
                  tail active X -> tail X}
        Open
       
       
       
       SCC (2):
        Strict:
         {  adx# mark X -> adx# X,
          adx# active X -> adx# X}
        Weak:
        {            mark nil() -> active nil(),
                    mark incr X -> active incr mark X,
              mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark s X -> active s mark X,
                     mark adx X -> active adx mark X,
                   mark zeros() -> active zeros(),
                    mark nats() -> active nats(),
                       mark 0() -> active 0(),
                    mark head X -> active head mark X,
                    mark tail X -> active tail mark X,
              active incr nil() -> mark nil(),
         active incr cons(X, L) -> mark cons(s X, incr L),
               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 cons(X, L) -> mark X,
         active tail cons(X, L) -> mark L,
                    incr mark X -> incr X,
                  incr active X -> incr X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                       s mark X -> s X,
                     s active X -> s X,
                     adx mark X -> adx X,
                   adx active X -> adx X,
                    head mark X -> head X,
                  head active X -> head X,
                    tail mark X -> tail X,
                  tail active X -> tail X}
        Open
       
       SCC (2):
        Strict:
         {  s# mark X -> s# X,
          s# active X -> s# X}
        Weak:
        {            mark nil() -> active nil(),
                    mark incr X -> active incr mark X,
              mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark s X -> active s mark X,
                     mark adx X -> active adx mark X,
                   mark zeros() -> active zeros(),
                    mark nats() -> active nats(),
                       mark 0() -> active 0(),
                    mark head X -> active head mark X,
                    mark tail X -> active tail mark X,
              active incr nil() -> mark nil(),
         active incr cons(X, L) -> mark cons(s X, incr L),
               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 cons(X, L) -> mark X,
         active tail cons(X, L) -> mark L,
                    incr mark X -> incr X,
                  incr active X -> incr X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                       s mark X -> s X,
                     s active X -> s X,
                     adx mark X -> adx X,
                   adx active X -> adx X,
                    head mark X -> head X,
                  head active X -> head X,
                    tail mark X -> tail X,
                  tail active X -> tail X}
        Open
       
       
       
       
       
       
       
       SCC (4):
        Strict:
         {  cons#(X1, mark X2) -> cons#(X1, X2),
          cons#(X1, active X2) -> cons#(X1, X2),
            cons#(mark X1, X2) -> cons#(X1, X2),
          cons#(active X1, X2) -> cons#(X1, X2)}
        Weak:
        {            mark nil() -> active nil(),
                    mark incr X -> active incr mark X,
              mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark s X -> active s mark X,
                     mark adx X -> active adx mark X,
                   mark zeros() -> active zeros(),
                    mark nats() -> active nats(),
                       mark 0() -> active 0(),
                    mark head X -> active head mark X,
                    mark tail X -> active tail mark X,
              active incr nil() -> mark nil(),
         active incr cons(X, L) -> mark cons(s X, incr L),
               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 cons(X, L) -> mark X,
         active tail cons(X, L) -> mark L,
                    incr mark X -> incr X,
                  incr active X -> incr X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                       s mark X -> s X,
                     s active X -> s X,
                     adx mark X -> adx X,
                   adx active X -> adx X,
                    head mark X -> head X,
                  head active X -> head X,
                    tail mark X -> tail X,
                  tail active X -> tail X}
        Open
       
       
       SCC (2):
        Strict:
         {  incr# mark X -> incr# X,
          incr# active X -> incr# X}
        Weak:
        {            mark nil() -> active nil(),
                    mark incr X -> active incr mark X,
              mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark s X -> active s mark X,
                     mark adx X -> active adx mark X,
                   mark zeros() -> active zeros(),
                    mark nats() -> active nats(),
                       mark 0() -> active 0(),
                    mark head X -> active head mark X,
                    mark tail X -> active tail mark X,
              active incr nil() -> mark nil(),
         active incr cons(X, L) -> mark cons(s X, incr L),
               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 cons(X, L) -> mark X,
         active tail cons(X, L) -> mark L,
                    incr mark X -> incr X,
                  incr active X -> incr X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                       s mark X -> s X,
                     s active X -> s X,
                     adx mark X -> adx X,
                   adx active X -> adx X,
                    head mark X -> head X,
                  head active X -> head X,
                    tail mark X -> tail X,
                  tail active X -> tail X}
        Open