MAYBE
Time: 0.745585
TRS:
 {         a__incr X -> incr X,
       a__incr nil() -> nil(),
  a__incr cons(X, L) -> cons(s mark X, incr L),
          mark nil() -> nil(),
   mark cons(X1, X2) -> cons(mark X1, X2),
            mark s X -> s mark X,
         mark incr X -> a__incr mark X,
          mark adx X -> a__adx mark X,
            mark 0() -> 0(),
        mark zeros() -> a__zeros(),
         mark nats() -> a__nats(),
         mark head X -> a__head mark X,
         mark tail X -> a__tail mark X,
            a__adx X -> adx X,
        a__adx nil() -> nil(),
   a__adx cons(X, L) -> a__incr cons(mark X, adx L),
          a__zeros() -> cons(0(), zeros()),
          a__zeros() -> zeros(),
           a__nats() -> a__adx a__zeros(),
           a__nats() -> nats(),
           a__head X -> head X,
  a__head cons(X, L) -> mark X,
           a__tail X -> tail X,
  a__tail cons(X, L) -> mark L}
 DP:
  DP:
   {a__incr# cons(X, L) -> mark# X,
     mark# cons(X1, X2) -> mark# X1,
              mark# s X -> mark# X,
           mark# incr X -> a__incr# mark X,
           mark# incr X -> mark# X,
            mark# adx X -> mark# X,
            mark# adx X -> a__adx# mark X,
          mark# zeros() -> a__zeros#(),
           mark# nats() -> a__nats#(),
           mark# head X -> mark# X,
           mark# head X -> a__head# mark X,
           mark# tail X -> mark# X,
           mark# tail X -> a__tail# mark X,
     a__adx# cons(X, L) -> a__incr# cons(mark X, adx L),
     a__adx# cons(X, L) -> mark# X,
             a__nats#() -> a__adx# a__zeros(),
             a__nats#() -> a__zeros#(),
    a__head# cons(X, L) -> mark# X,
    a__tail# cons(X, L) -> mark# L}
  TRS:
  {         a__incr X -> incr X,
        a__incr nil() -> nil(),
   a__incr cons(X, L) -> cons(s mark X, incr L),
           mark nil() -> nil(),
    mark cons(X1, X2) -> cons(mark X1, X2),
             mark s X -> s mark X,
          mark incr X -> a__incr mark X,
           mark adx X -> a__adx mark X,
             mark 0() -> 0(),
         mark zeros() -> a__zeros(),
          mark nats() -> a__nats(),
          mark head X -> a__head mark X,
          mark tail X -> a__tail mark X,
             a__adx X -> adx X,
         a__adx nil() -> nil(),
    a__adx cons(X, L) -> a__incr cons(mark X, adx L),
           a__zeros() -> cons(0(), zeros()),
           a__zeros() -> zeros(),
            a__nats() -> a__adx a__zeros(),
            a__nats() -> nats(),
            a__head X -> head X,
   a__head cons(X, L) -> mark X,
            a__tail X -> tail X,
   a__tail cons(X, L) -> mark L}
  UR:
   {         a__incr X -> incr X,
         a__incr nil() -> nil(),
    a__incr cons(X, L) -> cons(s mark X, incr L),
            mark nil() -> nil(),
     mark cons(X1, X2) -> cons(mark X1, X2),
              mark s X -> s mark X,
           mark incr X -> a__incr mark X,
            mark adx X -> a__adx mark X,
              mark 0() -> 0(),
          mark zeros() -> a__zeros(),
           mark nats() -> a__nats(),
           mark head X -> a__head mark X,
           mark tail X -> a__tail mark X,
              a__adx X -> adx X,
          a__adx nil() -> nil(),
     a__adx cons(X, L) -> a__incr cons(mark X, adx L),
            a__zeros() -> cons(0(), zeros()),
            a__zeros() -> zeros(),
             a__nats() -> a__adx a__zeros(),
             a__nats() -> nats(),
             a__head X -> head X,
    a__head cons(X, L) -> mark X,
             a__tail X -> tail X,
    a__tail cons(X, L) -> mark L}
   EDG:
    {(a__incr# cons(X, L) -> mark# X, mark# tail X -> a__tail# mark X)
     (a__incr# cons(X, L) -> mark# X, mark# tail X -> mark# X)
     (a__incr# cons(X, L) -> mark# X, mark# head X -> a__head# mark X)
     (a__incr# cons(X, L) -> mark# X, mark# head X -> mark# X)
     (a__incr# cons(X, L) -> mark# X, mark# nats() -> a__nats#())
     (a__incr# cons(X, L) -> mark# X, mark# zeros() -> a__zeros#())
     (a__incr# cons(X, L) -> mark# X, mark# adx X -> a__adx# mark X)
     (a__incr# cons(X, L) -> mark# X, mark# adx X -> mark# X)
     (a__incr# cons(X, L) -> mark# X, mark# incr X -> mark# X)
     (a__incr# cons(X, L) -> mark# X, mark# incr X -> a__incr# mark X)
     (a__incr# cons(X, L) -> mark# X, mark# s X -> mark# X)
     (a__incr# cons(X, L) -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# tail X -> a__tail# mark X)
     (mark# s X -> mark# X, mark# tail X -> mark# X)
     (mark# s X -> mark# X, mark# head X -> a__head# mark X)
     (mark# s X -> mark# X, mark# head X -> mark# X)
     (mark# s X -> mark# X, mark# nats() -> a__nats#())
     (mark# s X -> mark# X, mark# zeros() -> a__zeros#())
     (mark# s X -> mark# X, mark# adx X -> a__adx# mark X)
     (mark# s X -> mark# X, mark# adx X -> mark# X)
     (mark# s X -> mark# X, mark# incr X -> mark# X)
     (mark# s X -> mark# X, mark# incr X -> a__incr# mark X)
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# adx X -> mark# X, mark# tail X -> a__tail# mark X)
     (mark# adx X -> mark# X, mark# tail X -> mark# X)
     (mark# adx X -> mark# X, mark# head X -> a__head# mark X)
     (mark# adx X -> mark# X, mark# head X -> mark# X)
     (mark# adx X -> mark# X, mark# nats() -> a__nats#())
     (mark# adx X -> mark# X, mark# zeros() -> a__zeros#())
     (mark# adx X -> mark# X, mark# adx X -> a__adx# mark X)
     (mark# adx X -> mark# X, mark# adx X -> mark# X)
     (mark# adx X -> mark# X, mark# incr X -> mark# X)
     (mark# adx X -> mark# X, mark# incr X -> a__incr# mark X)
     (mark# adx X -> mark# X, mark# s X -> mark# X)
     (mark# adx X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# tail X -> mark# X, mark# tail X -> a__tail# mark X)
     (mark# tail X -> mark# X, mark# tail X -> mark# X)
     (mark# tail X -> mark# X, mark# head X -> a__head# mark X)
     (mark# tail X -> mark# X, mark# head X -> mark# X)
     (mark# tail X -> mark# X, mark# nats() -> a__nats#())
     (mark# tail X -> mark# X, mark# zeros() -> a__zeros#())
     (mark# tail X -> mark# X, mark# adx X -> a__adx# mark X)
     (mark# tail X -> mark# X, mark# adx X -> mark# X)
     (mark# tail X -> mark# X, mark# incr X -> mark# X)
     (mark# tail X -> mark# X, mark# incr X -> a__incr# mark X)
     (mark# tail X -> mark# X, mark# s X -> mark# X)
     (mark# tail X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__head# cons(X, L) -> mark# X, mark# tail X -> a__tail# mark X)
     (a__head# cons(X, L) -> mark# X, mark# tail X -> mark# X)
     (a__head# cons(X, L) -> mark# X, mark# head X -> a__head# mark X)
     (a__head# cons(X, L) -> mark# X, mark# head X -> mark# X)
     (a__head# cons(X, L) -> mark# X, mark# nats() -> a__nats#())
     (a__head# cons(X, L) -> mark# X, mark# zeros() -> a__zeros#())
     (a__head# cons(X, L) -> mark# X, mark# adx X -> a__adx# mark X)
     (a__head# cons(X, L) -> mark# X, mark# adx X -> mark# X)
     (a__head# cons(X, L) -> mark# X, mark# incr X -> mark# X)
     (a__head# cons(X, L) -> mark# X, mark# incr X -> a__incr# mark X)
     (a__head# cons(X, L) -> mark# X, mark# s X -> mark# X)
     (a__head# cons(X, L) -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# adx X -> a__adx# mark X, a__adx# cons(X, L) -> mark# X)
     (mark# adx X -> a__adx# mark X, a__adx# cons(X, L) -> a__incr# cons(mark X, adx L))
     (mark# tail X -> a__tail# mark X, a__tail# cons(X, L) -> mark# L)
     (mark# nats() -> a__nats#(), a__nats#() -> a__zeros#())
     (mark# nats() -> a__nats#(), a__nats#() -> a__adx# a__zeros())
     (a__adx# cons(X, L) -> a__incr# cons(mark X, adx L), a__incr# cons(X, L) -> mark# X)
     (a__tail# cons(X, L) -> mark# L, mark# cons(X1, X2) -> mark# X1)
     (a__tail# cons(X, L) -> mark# L, mark# s X -> mark# X)
     (a__tail# cons(X, L) -> mark# L, mark# incr X -> a__incr# mark X)
     (a__tail# cons(X, L) -> mark# L, mark# incr X -> mark# X)
     (a__tail# cons(X, L) -> mark# L, mark# adx X -> mark# X)
     (a__tail# cons(X, L) -> mark# L, mark# adx X -> a__adx# mark X)
     (a__tail# cons(X, L) -> mark# L, mark# zeros() -> a__zeros#())
     (a__tail# cons(X, L) -> mark# L, mark# nats() -> a__nats#())
     (a__tail# cons(X, L) -> mark# L, mark# head X -> mark# X)
     (a__tail# cons(X, L) -> mark# L, mark# head X -> a__head# mark X)
     (a__tail# cons(X, L) -> mark# L, mark# tail X -> mark# X)
     (a__tail# cons(X, L) -> mark# L, mark# tail X -> a__tail# mark X)
     (mark# head X -> a__head# mark X, a__head# cons(X, L) -> mark# X)
     (mark# incr X -> a__incr# mark X, a__incr# cons(X, L) -> mark# X)
     (a__adx# cons(X, L) -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__adx# cons(X, L) -> mark# X, mark# s X -> mark# X)
     (a__adx# cons(X, L) -> mark# X, mark# incr X -> a__incr# mark X)
     (a__adx# cons(X, L) -> mark# X, mark# incr X -> mark# X)
     (a__adx# cons(X, L) -> mark# X, mark# adx X -> mark# X)
     (a__adx# cons(X, L) -> mark# X, mark# adx X -> a__adx# mark X)
     (a__adx# cons(X, L) -> mark# X, mark# zeros() -> a__zeros#())
     (a__adx# cons(X, L) -> mark# X, mark# nats() -> a__nats#())
     (a__adx# cons(X, L) -> mark# X, mark# head X -> mark# X)
     (a__adx# cons(X, L) -> mark# X, mark# head X -> a__head# mark X)
     (a__adx# cons(X, L) -> mark# X, mark# tail X -> mark# X)
     (a__adx# cons(X, L) -> mark# X, mark# tail X -> a__tail# mark X)
     (mark# head X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# head X -> mark# X, mark# s X -> mark# X)
     (mark# head X -> mark# X, mark# incr X -> a__incr# mark X)
     (mark# head X -> mark# X, mark# incr X -> mark# X)
     (mark# head X -> mark# X, mark# adx X -> mark# X)
     (mark# head X -> mark# X, mark# adx X -> a__adx# mark X)
     (mark# head X -> mark# X, mark# zeros() -> a__zeros#())
     (mark# head X -> mark# X, mark# nats() -> a__nats#())
     (mark# head X -> mark# X, mark# head X -> mark# X)
     (mark# head X -> mark# X, mark# head X -> a__head# mark X)
     (mark# head X -> mark# X, mark# tail X -> mark# X)
     (mark# head X -> mark# X, mark# tail X -> a__tail# mark X)
     (mark# incr X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# incr X -> mark# X, mark# s X -> mark# X)
     (mark# incr X -> mark# X, mark# incr X -> a__incr# mark X)
     (mark# incr X -> mark# X, mark# incr X -> mark# X)
     (mark# incr X -> mark# X, mark# adx X -> mark# X)
     (mark# incr X -> mark# X, mark# adx X -> a__adx# mark X)
     (mark# incr X -> mark# X, mark# zeros() -> a__zeros#())
     (mark# incr X -> mark# X, mark# nats() -> a__nats#())
     (mark# incr X -> mark# X, mark# head X -> mark# X)
     (mark# incr X -> mark# X, mark# head X -> a__head# mark X)
     (mark# incr X -> mark# X, mark# tail X -> mark# X)
     (mark# incr X -> mark# X, mark# tail X -> a__tail# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# incr X -> a__incr# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# incr X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# adx X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# adx X -> a__adx# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
     (mark# cons(X1, X2) -> mark# X1, mark# nats() -> a__nats#())
     (mark# cons(X1, X2) -> mark# X1, mark# head X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# head X -> a__head# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# tail X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# tail X -> a__tail# mark X)
     (a__nats#() -> a__adx# a__zeros(), a__adx# cons(X, L) -> a__incr# cons(mark X, adx L))
     (a__nats#() -> a__adx# a__zeros(), a__adx# cons(X, L) -> mark# X)}
    EDG:
     {(a__incr# cons(X, L) -> mark# X, mark# tail X -> a__tail# mark X)
      (a__incr# cons(X, L) -> mark# X, mark# tail X -> mark# X)
      (a__incr# cons(X, L) -> mark# X, mark# head X -> a__head# mark X)
      (a__incr# cons(X, L) -> mark# X, mark# head X -> mark# X)
      (a__incr# cons(X, L) -> mark# X, mark# nats() -> a__nats#())
      (a__incr# cons(X, L) -> mark# X, mark# zeros() -> a__zeros#())
      (a__incr# cons(X, L) -> mark# X, mark# adx X -> a__adx# mark X)
      (a__incr# cons(X, L) -> mark# X, mark# adx X -> mark# X)
      (a__incr# cons(X, L) -> mark# X, mark# incr X -> mark# X)
      (a__incr# cons(X, L) -> mark# X, mark# incr X -> a__incr# mark X)
      (a__incr# cons(X, L) -> mark# X, mark# s X -> mark# X)
      (a__incr# cons(X, L) -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# s X -> mark# X, mark# tail X -> a__tail# mark X)
      (mark# s X -> mark# X, mark# tail X -> mark# X)
      (mark# s X -> mark# X, mark# head X -> a__head# mark X)
      (mark# s X -> mark# X, mark# head X -> mark# X)
      (mark# s X -> mark# X, mark# nats() -> a__nats#())
      (mark# s X -> mark# X, mark# zeros() -> a__zeros#())
      (mark# s X -> mark# X, mark# adx X -> a__adx# mark X)
      (mark# s X -> mark# X, mark# adx X -> mark# X)
      (mark# s X -> mark# X, mark# incr X -> mark# X)
      (mark# s X -> mark# X, mark# incr X -> a__incr# mark X)
      (mark# s X -> mark# X, mark# s X -> mark# X)
      (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# adx X -> mark# X, mark# tail X -> a__tail# mark X)
      (mark# adx X -> mark# X, mark# tail X -> mark# X)
      (mark# adx X -> mark# X, mark# head X -> a__head# mark X)
      (mark# adx X -> mark# X, mark# head X -> mark# X)
      (mark# adx X -> mark# X, mark# nats() -> a__nats#())
      (mark# adx X -> mark# X, mark# zeros() -> a__zeros#())
      (mark# adx X -> mark# X, mark# adx X -> a__adx# mark X)
      (mark# adx X -> mark# X, mark# adx X -> mark# X)
      (mark# adx X -> mark# X, mark# incr X -> mark# X)
      (mark# adx X -> mark# X, mark# incr X -> a__incr# mark X)
      (mark# adx X -> mark# X, mark# s X -> mark# X)
      (mark# adx X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# tail X -> mark# X, mark# tail X -> a__tail# mark X)
      (mark# tail X -> mark# X, mark# tail X -> mark# X)
      (mark# tail X -> mark# X, mark# head X -> a__head# mark X)
      (mark# tail X -> mark# X, mark# head X -> mark# X)
      (mark# tail X -> mark# X, mark# nats() -> a__nats#())
      (mark# tail X -> mark# X, mark# zeros() -> a__zeros#())
      (mark# tail X -> mark# X, mark# adx X -> a__adx# mark X)
      (mark# tail X -> mark# X, mark# adx X -> mark# X)
      (mark# tail X -> mark# X, mark# incr X -> mark# X)
      (mark# tail X -> mark# X, mark# incr X -> a__incr# mark X)
      (mark# tail X -> mark# X, mark# s X -> mark# X)
      (mark# tail X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (a__head# cons(X, L) -> mark# X, mark# tail X -> a__tail# mark X)
      (a__head# cons(X, L) -> mark# X, mark# tail X -> mark# X)
      (a__head# cons(X, L) -> mark# X, mark# head X -> a__head# mark X)
      (a__head# cons(X, L) -> mark# X, mark# head X -> mark# X)
      (a__head# cons(X, L) -> mark# X, mark# nats() -> a__nats#())
      (a__head# cons(X, L) -> mark# X, mark# zeros() -> a__zeros#())
      (a__head# cons(X, L) -> mark# X, mark# adx X -> a__adx# mark X)
      (a__head# cons(X, L) -> mark# X, mark# adx X -> mark# X)
      (a__head# cons(X, L) -> mark# X, mark# incr X -> mark# X)
      (a__head# cons(X, L) -> mark# X, mark# incr X -> a__incr# mark X)
      (a__head# cons(X, L) -> mark# X, mark# s X -> mark# X)
      (a__head# cons(X, L) -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# adx X -> a__adx# mark X, a__adx# cons(X, L) -> mark# X)
      (mark# adx X -> a__adx# mark X, a__adx# cons(X, L) -> a__incr# cons(mark X, adx L))
      (mark# tail X -> a__tail# mark X, a__tail# cons(X, L) -> mark# L)
      (mark# nats() -> a__nats#(), a__nats#() -> a__zeros#())
      (mark# nats() -> a__nats#(), a__nats#() -> a__adx# a__zeros())
      (a__adx# cons(X, L) -> a__incr# cons(mark X, adx L), a__incr# cons(X, L) -> mark# X)
      (a__tail# cons(X, L) -> mark# L, mark# cons(X1, X2) -> mark# X1)
      (a__tail# cons(X, L) -> mark# L, mark# s X -> mark# X)
      (a__tail# cons(X, L) -> mark# L, mark# incr X -> a__incr# mark X)
      (a__tail# cons(X, L) -> mark# L, mark# incr X -> mark# X)
      (a__tail# cons(X, L) -> mark# L, mark# adx X -> mark# X)
      (a__tail# cons(X, L) -> mark# L, mark# adx X -> a__adx# mark X)
      (a__tail# cons(X, L) -> mark# L, mark# zeros() -> a__zeros#())
      (a__tail# cons(X, L) -> mark# L, mark# nats() -> a__nats#())
      (a__tail# cons(X, L) -> mark# L, mark# head X -> mark# X)
      (a__tail# cons(X, L) -> mark# L, mark# head X -> a__head# mark X)
      (a__tail# cons(X, L) -> mark# L, mark# tail X -> mark# X)
      (a__tail# cons(X, L) -> mark# L, mark# tail X -> a__tail# mark X)
      (mark# head X -> a__head# mark X, a__head# cons(X, L) -> mark# X)
      (mark# incr X -> a__incr# mark X, a__incr# cons(X, L) -> mark# X)
      (a__adx# cons(X, L) -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (a__adx# cons(X, L) -> mark# X, mark# s X -> mark# X)
      (a__adx# cons(X, L) -> mark# X, mark# incr X -> a__incr# mark X)
      (a__adx# cons(X, L) -> mark# X, mark# incr X -> mark# X)
      (a__adx# cons(X, L) -> mark# X, mark# adx X -> mark# X)
      (a__adx# cons(X, L) -> mark# X, mark# adx X -> a__adx# mark X)
      (a__adx# cons(X, L) -> mark# X, mark# zeros() -> a__zeros#())
      (a__adx# cons(X, L) -> mark# X, mark# nats() -> a__nats#())
      (a__adx# cons(X, L) -> mark# X, mark# head X -> mark# X)
      (a__adx# cons(X, L) -> mark# X, mark# head X -> a__head# mark X)
      (a__adx# cons(X, L) -> mark# X, mark# tail X -> mark# X)
      (a__adx# cons(X, L) -> mark# X, mark# tail X -> a__tail# mark X)
      (mark# head X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# head X -> mark# X, mark# s X -> mark# X)
      (mark# head X -> mark# X, mark# incr X -> a__incr# mark X)
      (mark# head X -> mark# X, mark# incr X -> mark# X)
      (mark# head X -> mark# X, mark# adx X -> mark# X)
      (mark# head X -> mark# X, mark# adx X -> a__adx# mark X)
      (mark# head X -> mark# X, mark# zeros() -> a__zeros#())
      (mark# head X -> mark# X, mark# nats() -> a__nats#())
      (mark# head X -> mark# X, mark# head X -> mark# X)
      (mark# head X -> mark# X, mark# head X -> a__head# mark X)
      (mark# head X -> mark# X, mark# tail X -> mark# X)
      (mark# head X -> mark# X, mark# tail X -> a__tail# mark X)
      (mark# incr X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# incr X -> mark# X, mark# s X -> mark# X)
      (mark# incr X -> mark# X, mark# incr X -> a__incr# mark X)
      (mark# incr X -> mark# X, mark# incr X -> mark# X)
      (mark# incr X -> mark# X, mark# adx X -> mark# X)
      (mark# incr X -> mark# X, mark# adx X -> a__adx# mark X)
      (mark# incr X -> mark# X, mark# zeros() -> a__zeros#())
      (mark# incr X -> mark# X, mark# nats() -> a__nats#())
      (mark# incr X -> mark# X, mark# head X -> mark# X)
      (mark# incr X -> mark# X, mark# head X -> a__head# mark X)
      (mark# incr X -> mark# X, mark# tail X -> mark# X)
      (mark# incr X -> mark# X, mark# tail X -> a__tail# mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
      (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# incr X -> a__incr# mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# incr X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# adx X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# adx X -> a__adx# mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
      (mark# cons(X1, X2) -> mark# X1, mark# nats() -> a__nats#())
      (mark# cons(X1, X2) -> mark# X1, mark# head X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# head X -> a__head# mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# tail X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# tail X -> a__tail# mark X)
      (a__nats#() -> a__adx# a__zeros(), a__adx# cons(X, L) -> a__incr# cons(mark X, adx L))
      (a__nats#() -> a__adx# a__zeros(), a__adx# cons(X, L) -> mark# X)}
     EDG:
      {(a__incr# cons(X, L) -> mark# X, mark# tail X -> a__tail# mark X)
       (a__incr# cons(X, L) -> mark# X, mark# tail X -> mark# X)
       (a__incr# cons(X, L) -> mark# X, mark# head X -> a__head# mark X)
       (a__incr# cons(X, L) -> mark# X, mark# head X -> mark# X)
       (a__incr# cons(X, L) -> mark# X, mark# nats() -> a__nats#())
       (a__incr# cons(X, L) -> mark# X, mark# zeros() -> a__zeros#())
       (a__incr# cons(X, L) -> mark# X, mark# adx X -> a__adx# mark X)
       (a__incr# cons(X, L) -> mark# X, mark# adx X -> mark# X)
       (a__incr# cons(X, L) -> mark# X, mark# incr X -> mark# X)
       (a__incr# cons(X, L) -> mark# X, mark# incr X -> a__incr# mark X)
       (a__incr# cons(X, L) -> mark# X, mark# s X -> mark# X)
       (a__incr# cons(X, L) -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (mark# s X -> mark# X, mark# tail X -> a__tail# mark X)
       (mark# s X -> mark# X, mark# tail X -> mark# X)
       (mark# s X -> mark# X, mark# head X -> a__head# mark X)
       (mark# s X -> mark# X, mark# head X -> mark# X)
       (mark# s X -> mark# X, mark# nats() -> a__nats#())
       (mark# s X -> mark# X, mark# zeros() -> a__zeros#())
       (mark# s X -> mark# X, mark# adx X -> a__adx# mark X)
       (mark# s X -> mark# X, mark# adx X -> mark# X)
       (mark# s X -> mark# X, mark# incr X -> mark# X)
       (mark# s X -> mark# X, mark# incr X -> a__incr# mark X)
       (mark# s X -> mark# X, mark# s X -> mark# X)
       (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (mark# adx X -> mark# X, mark# tail X -> a__tail# mark X)
       (mark# adx X -> mark# X, mark# tail X -> mark# X)
       (mark# adx X -> mark# X, mark# head X -> a__head# mark X)
       (mark# adx X -> mark# X, mark# head X -> mark# X)
       (mark# adx X -> mark# X, mark# nats() -> a__nats#())
       (mark# adx X -> mark# X, mark# zeros() -> a__zeros#())
       (mark# adx X -> mark# X, mark# adx X -> a__adx# mark X)
       (mark# adx X -> mark# X, mark# adx X -> mark# X)
       (mark# adx X -> mark# X, mark# incr X -> mark# X)
       (mark# adx X -> mark# X, mark# incr X -> a__incr# mark X)
       (mark# adx X -> mark# X, mark# s X -> mark# X)
       (mark# adx X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (mark# tail X -> mark# X, mark# tail X -> a__tail# mark X)
       (mark# tail X -> mark# X, mark# tail X -> mark# X)
       (mark# tail X -> mark# X, mark# head X -> a__head# mark X)
       (mark# tail X -> mark# X, mark# head X -> mark# X)
       (mark# tail X -> mark# X, mark# nats() -> a__nats#())
       (mark# tail X -> mark# X, mark# zeros() -> a__zeros#())
       (mark# tail X -> mark# X, mark# adx X -> a__adx# mark X)
       (mark# tail X -> mark# X, mark# adx X -> mark# X)
       (mark# tail X -> mark# X, mark# incr X -> mark# X)
       (mark# tail X -> mark# X, mark# incr X -> a__incr# mark X)
       (mark# tail X -> mark# X, mark# s X -> mark# X)
       (mark# tail X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (a__head# cons(X, L) -> mark# X, mark# tail X -> a__tail# mark X)
       (a__head# cons(X, L) -> mark# X, mark# tail X -> mark# X)
       (a__head# cons(X, L) -> mark# X, mark# head X -> a__head# mark X)
       (a__head# cons(X, L) -> mark# X, mark# head X -> mark# X)
       (a__head# cons(X, L) -> mark# X, mark# nats() -> a__nats#())
       (a__head# cons(X, L) -> mark# X, mark# zeros() -> a__zeros#())
       (a__head# cons(X, L) -> mark# X, mark# adx X -> a__adx# mark X)
       (a__head# cons(X, L) -> mark# X, mark# adx X -> mark# X)
       (a__head# cons(X, L) -> mark# X, mark# incr X -> mark# X)
       (a__head# cons(X, L) -> mark# X, mark# incr X -> a__incr# mark X)
       (a__head# cons(X, L) -> mark# X, mark# s X -> mark# X)
       (a__head# cons(X, L) -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (mark# adx X -> a__adx# mark X, a__adx# cons(X, L) -> mark# X)
       (mark# adx X -> a__adx# mark X, a__adx# cons(X, L) -> a__incr# cons(mark X, adx L))
       (mark# tail X -> a__tail# mark X, a__tail# cons(X, L) -> mark# L)
       (mark# nats() -> a__nats#(), a__nats#() -> a__zeros#())
       (mark# nats() -> a__nats#(), a__nats#() -> a__adx# a__zeros())
       (a__adx# cons(X, L) -> a__incr# cons(mark X, adx L), a__incr# cons(X, L) -> mark# X)
       (a__tail# cons(X, L) -> mark# L, mark# cons(X1, X2) -> mark# X1)
       (a__tail# cons(X, L) -> mark# L, mark# s X -> mark# X)
       (a__tail# cons(X, L) -> mark# L, mark# incr X -> a__incr# mark X)
       (a__tail# cons(X, L) -> mark# L, mark# incr X -> mark# X)
       (a__tail# cons(X, L) -> mark# L, mark# adx X -> mark# X)
       (a__tail# cons(X, L) -> mark# L, mark# adx X -> a__adx# mark X)
       (a__tail# cons(X, L) -> mark# L, mark# zeros() -> a__zeros#())
       (a__tail# cons(X, L) -> mark# L, mark# nats() -> a__nats#())
       (a__tail# cons(X, L) -> mark# L, mark# head X -> mark# X)
       (a__tail# cons(X, L) -> mark# L, mark# head X -> a__head# mark X)
       (a__tail# cons(X, L) -> mark# L, mark# tail X -> mark# X)
       (a__tail# cons(X, L) -> mark# L, mark# tail X -> a__tail# mark X)
       (mark# head X -> a__head# mark X, a__head# cons(X, L) -> mark# X)
       (mark# incr X -> a__incr# mark X, a__incr# cons(X, L) -> mark# X)
       (a__adx# cons(X, L) -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (a__adx# cons(X, L) -> mark# X, mark# s X -> mark# X)
       (a__adx# cons(X, L) -> mark# X, mark# incr X -> a__incr# mark X)
       (a__adx# cons(X, L) -> mark# X, mark# incr X -> mark# X)
       (a__adx# cons(X, L) -> mark# X, mark# adx X -> mark# X)
       (a__adx# cons(X, L) -> mark# X, mark# adx X -> a__adx# mark X)
       (a__adx# cons(X, L) -> mark# X, mark# zeros() -> a__zeros#())
       (a__adx# cons(X, L) -> mark# X, mark# nats() -> a__nats#())
       (a__adx# cons(X, L) -> mark# X, mark# head X -> mark# X)
       (a__adx# cons(X, L) -> mark# X, mark# head X -> a__head# mark X)
       (a__adx# cons(X, L) -> mark# X, mark# tail X -> mark# X)
       (a__adx# cons(X, L) -> mark# X, mark# tail X -> a__tail# mark X)
       (mark# head X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (mark# head X -> mark# X, mark# s X -> mark# X)
       (mark# head X -> mark# X, mark# incr X -> a__incr# mark X)
       (mark# head X -> mark# X, mark# incr X -> mark# X)
       (mark# head X -> mark# X, mark# adx X -> mark# X)
       (mark# head X -> mark# X, mark# adx X -> a__adx# mark X)
       (mark# head X -> mark# X, mark# zeros() -> a__zeros#())
       (mark# head X -> mark# X, mark# nats() -> a__nats#())
       (mark# head X -> mark# X, mark# head X -> mark# X)
       (mark# head X -> mark# X, mark# head X -> a__head# mark X)
       (mark# head X -> mark# X, mark# tail X -> mark# X)
       (mark# head X -> mark# X, mark# tail X -> a__tail# mark X)
       (mark# incr X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (mark# incr X -> mark# X, mark# s X -> mark# X)
       (mark# incr X -> mark# X, mark# incr X -> a__incr# mark X)
       (mark# incr X -> mark# X, mark# incr X -> mark# X)
       (mark# incr X -> mark# X, mark# adx X -> mark# X)
       (mark# incr X -> mark# X, mark# adx X -> a__adx# mark X)
       (mark# incr X -> mark# X, mark# zeros() -> a__zeros#())
       (mark# incr X -> mark# X, mark# nats() -> a__nats#())
       (mark# incr X -> mark# X, mark# head X -> mark# X)
       (mark# incr X -> mark# X, mark# head X -> a__head# mark X)
       (mark# incr X -> mark# X, mark# tail X -> mark# X)
       (mark# incr X -> mark# X, mark# tail X -> a__tail# mark X)
       (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
       (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
       (mark# cons(X1, X2) -> mark# X1, mark# incr X -> a__incr# mark X)
       (mark# cons(X1, X2) -> mark# X1, mark# incr X -> mark# X)
       (mark# cons(X1, X2) -> mark# X1, mark# adx X -> mark# X)
       (mark# cons(X1, X2) -> mark# X1, mark# adx X -> a__adx# mark X)
       (mark# cons(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
       (mark# cons(X1, X2) -> mark# X1, mark# nats() -> a__nats#())
       (mark# cons(X1, X2) -> mark# X1, mark# head X -> mark# X)
       (mark# cons(X1, X2) -> mark# X1, mark# head X -> a__head# mark X)
       (mark# cons(X1, X2) -> mark# X1, mark# tail X -> mark# X)
       (mark# cons(X1, X2) -> mark# X1, mark# tail X -> a__tail# mark X)
       (a__nats#() -> a__adx# a__zeros(), a__adx# cons(X, L) -> a__incr# cons(mark X, adx L))
       (a__nats#() -> a__adx# a__zeros(), a__adx# cons(X, L) -> mark# X)}
      STATUS:
       arrows: 0.639889
       SCCS (1):
        Scc:
         {a__incr# cons(X, L) -> mark# X,
           mark# cons(X1, X2) -> mark# X1,
                    mark# s X -> mark# X,
                 mark# incr X -> a__incr# mark X,
                 mark# incr X -> mark# X,
                  mark# adx X -> mark# X,
                  mark# adx X -> a__adx# mark X,
                 mark# nats() -> a__nats#(),
                 mark# head X -> mark# X,
                 mark# head X -> a__head# mark X,
                 mark# tail X -> mark# X,
                 mark# tail X -> a__tail# mark X,
           a__adx# cons(X, L) -> a__incr# cons(mark X, adx L),
           a__adx# cons(X, L) -> mark# X,
                   a__nats#() -> a__adx# a__zeros(),
          a__head# cons(X, L) -> mark# X,
          a__tail# cons(X, L) -> mark# L}
        
        SCC (17):
         Strict:
          {a__incr# cons(X, L) -> mark# X,
            mark# cons(X1, X2) -> mark# X1,
                     mark# s X -> mark# X,
                  mark# incr X -> a__incr# mark X,
                  mark# incr X -> mark# X,
                   mark# adx X -> mark# X,
                   mark# adx X -> a__adx# mark X,
                  mark# nats() -> a__nats#(),
                  mark# head X -> mark# X,
                  mark# head X -> a__head# mark X,
                  mark# tail X -> mark# X,
                  mark# tail X -> a__tail# mark X,
            a__adx# cons(X, L) -> a__incr# cons(mark X, adx L),
            a__adx# cons(X, L) -> mark# X,
                    a__nats#() -> a__adx# a__zeros(),
           a__head# cons(X, L) -> mark# X,
           a__tail# cons(X, L) -> mark# L}
         Weak:
         {         a__incr X -> incr X,
               a__incr nil() -> nil(),
          a__incr cons(X, L) -> cons(s mark X, incr L),
                  mark nil() -> nil(),
           mark cons(X1, X2) -> cons(mark X1, X2),
                    mark s X -> s mark X,
                 mark incr X -> a__incr mark X,
                  mark adx X -> a__adx mark X,
                    mark 0() -> 0(),
                mark zeros() -> a__zeros(),
                 mark nats() -> a__nats(),
                 mark head X -> a__head mark X,
                 mark tail X -> a__tail mark X,
                    a__adx X -> adx X,
                a__adx nil() -> nil(),
           a__adx cons(X, L) -> a__incr cons(mark X, adx L),
                  a__zeros() -> cons(0(), zeros()),
                  a__zeros() -> zeros(),
                   a__nats() -> a__adx a__zeros(),
                   a__nats() -> nats(),
                   a__head X -> head X,
          a__head cons(X, L) -> mark X,
                   a__tail X -> tail X,
          a__tail cons(X, L) -> mark L}
         Open