MAYBE Time: 0.191165 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)} 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} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [a__incr](x0) = x0, [s](x0) = x0, [mark](x0) = x0, [incr](x0) = x0, [a__adx](x0) = x0, [adx](x0) = x0, [a__head](x0) = x0, [a__tail](x0) = x0 + 1, [head](x0) = x0, [tail](x0) = x0 + 1, [nil] = 0, [a__zeros] = 0, [a__nats] = 0, [0] = 0, [zeros] = 0, [nats] = 0, [a__incr#](x0) = x0, [mark#](x0) = x0, [a__adx#](x0) = x0, [a__head#](x0) = x0, [a__tail#](x0) = x0 + 1, [a__nats#] = 0 Strict: a__tail# cons(X, L) -> mark# L 1 + 1X + 1L >= 0 + 1L a__head# cons(X, L) -> mark# X 0 + 1X + 1L >= 0 + 1X a__nats#() -> a__adx# a__zeros() 0 >= 0 a__adx# cons(X, L) -> mark# X 0 + 1X + 1L >= 0 + 1X a__adx# cons(X, L) -> a__incr# cons(mark X, adx L) 0 + 1X + 1L >= 0 + 1X + 1L mark# tail X -> a__tail# mark X 1 + 1X >= 1 + 1X mark# tail X -> mark# X 1 + 1X >= 0 + 1X mark# head X -> a__head# mark X 0 + 1X >= 0 + 1X mark# head X -> mark# X 0 + 1X >= 0 + 1X mark# nats() -> a__nats#() 0 >= 0 mark# adx X -> a__adx# mark X 0 + 1X >= 0 + 1X mark# adx X -> mark# X 0 + 1X >= 0 + 1X mark# incr X -> mark# X 0 + 1X >= 0 + 1X mark# incr X -> a__incr# mark X 0 + 1X >= 0 + 1X mark# s X -> mark# X 0 + 1X >= 0 + 1X mark# cons(X1, X2) -> mark# X1 0 + 1X1 + 1X2 >= 0 + 1X1 a__incr# cons(X, L) -> mark# X 0 + 1X + 1L >= 0 + 1X Weak: a__tail cons(X, L) -> mark L 1 + 1X + 1L >= 0 + 1L a__tail X -> tail X 1 + 1X >= 1 + 1X a__head cons(X, L) -> mark X 0 + 1X + 1L >= 0 + 1X a__head X -> head X 0 + 1X >= 0 + 1X a__nats() -> nats() 0 >= 0 a__nats() -> a__adx a__zeros() 0 >= 0 a__zeros() -> zeros() 0 >= 0 a__zeros() -> cons(0(), zeros()) 0 >= 0 a__adx cons(X, L) -> a__incr cons(mark X, adx L) 0 + 1X + 1L >= 0 + 1X + 1L a__adx nil() -> nil() 0 >= 0 a__adx X -> adx X 0 + 1X >= 0 + 1X mark tail X -> a__tail mark X 1 + 1X >= 1 + 1X mark head X -> a__head mark X 0 + 1X >= 0 + 1X mark nats() -> a__nats() 0 >= 0 mark zeros() -> a__zeros() 0 >= 0 mark 0() -> 0() 0 >= 0 mark adx X -> a__adx mark X 0 + 1X >= 0 + 1X mark incr X -> a__incr mark X 0 + 1X >= 0 + 1X mark s X -> s mark X 0 + 1X >= 0 + 1X mark cons(X1, X2) -> cons(mark X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark nil() -> nil() 0 >= 0 a__incr cons(X, L) -> cons(s mark X, incr L) 0 + 1X + 1L >= 0 + 1X + 1L a__incr nil() -> nil() 0 >= 0 a__incr X -> incr X 0 + 1X >= 0 + 1X 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, 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} SCC (14): 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, 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} 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} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [a__incr](x0) = x0, [s](x0) = x0, [mark](x0) = x0, [incr](x0) = x0, [a__adx](x0) = x0, [adx](x0) = x0, [a__head](x0) = x0 + 1, [a__tail](x0) = x0, [head](x0) = x0 + 1, [tail](x0) = x0, [nil] = 0, [a__zeros] = 0, [a__nats] = 0, [0] = 0, [zeros] = 0, [nats] = 0, [a__incr#](x0) = x0, [mark#](x0) = x0, [a__adx#](x0) = x0, [a__head#](x0) = x0 + 1, [a__nats#] = 0 Strict: a__head# cons(X, L) -> mark# X 1 + 1X + 1L >= 0 + 1X a__nats#() -> a__adx# a__zeros() 0 >= 0 a__adx# cons(X, L) -> mark# X 0 + 1X + 1L >= 0 + 1X a__adx# cons(X, L) -> a__incr# cons(mark X, adx L) 0 + 1X + 1L >= 0 + 1X + 1L mark# head X -> a__head# mark X 1 + 1X >= 1 + 1X mark# head X -> mark# X 1 + 1X >= 0 + 1X mark# nats() -> a__nats#() 0 >= 0 mark# adx X -> a__adx# mark X 0 + 1X >= 0 + 1X mark# adx X -> mark# X 0 + 1X >= 0 + 1X mark# incr X -> mark# X 0 + 1X >= 0 + 1X mark# incr X -> a__incr# mark X 0 + 1X >= 0 + 1X mark# s X -> mark# X 0 + 1X >= 0 + 1X mark# cons(X1, X2) -> mark# X1 0 + 1X1 + 1X2 >= 0 + 1X1 a__incr# cons(X, L) -> mark# X 0 + 1X + 1L >= 0 + 1X Weak: a__tail cons(X, L) -> mark L 0 + 1X + 1L >= 0 + 1L a__tail X -> tail X 0 + 1X >= 0 + 1X a__head cons(X, L) -> mark X 1 + 1X + 1L >= 0 + 1X a__head X -> head X 1 + 1X >= 1 + 1X a__nats() -> nats() 0 >= 0 a__nats() -> a__adx a__zeros() 0 >= 0 a__zeros() -> zeros() 0 >= 0 a__zeros() -> cons(0(), zeros()) 0 >= 0 a__adx cons(X, L) -> a__incr cons(mark X, adx L) 0 + 1X + 1L >= 0 + 1X + 1L a__adx nil() -> nil() 0 >= 0 a__adx X -> adx X 0 + 1X >= 0 + 1X mark tail X -> a__tail mark X 0 + 1X >= 0 + 1X mark head X -> a__head mark X 1 + 1X >= 1 + 1X mark nats() -> a__nats() 0 >= 0 mark zeros() -> a__zeros() 0 >= 0 mark 0() -> 0() 0 >= 0 mark adx X -> a__adx mark X 0 + 1X >= 0 + 1X mark incr X -> a__incr mark X 0 + 1X >= 0 + 1X mark s X -> s mark X 0 + 1X >= 0 + 1X mark cons(X1, X2) -> cons(mark X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark nil() -> nil() 0 >= 0 a__incr cons(X, L) -> cons(s mark X, incr L) 0 + 1X + 1L >= 0 + 1X + 1L a__incr nil() -> nil() 0 >= 0 a__incr X -> incr X 0 + 1X >= 0 + 1X 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#(), 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()} SCC (11): 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#(), 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()} 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} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [a__incr](x0) = x0, [s](x0) = x0, [mark](x0) = x0, [incr](x0) = x0, [a__adx](x0) = x0, [adx](x0) = x0, [a__head](x0) = x0, [a__tail](x0) = x0, [head](x0) = x0, [tail](x0) = x0, [nil] = 0, [a__zeros] = 0, [a__nats] = 1, [0] = 0, [zeros] = 0, [nats] = 1, [a__incr#](x0) = x0, [mark#](x0) = x0, [a__adx#](x0) = x0, [a__nats#] = 1 Strict: a__nats#() -> a__adx# a__zeros() 1 >= 0 a__adx# cons(X, L) -> mark# X 0 + 1X + 1L >= 0 + 1X a__adx# cons(X, L) -> a__incr# cons(mark X, adx L) 0 + 1X + 1L >= 0 + 1X + 1L mark# nats() -> a__nats#() 1 >= 1 mark# adx X -> a__adx# mark X 0 + 1X >= 0 + 1X mark# adx X -> mark# X 0 + 1X >= 0 + 1X mark# incr X -> mark# X 0 + 1X >= 0 + 1X mark# incr X -> a__incr# mark X 0 + 1X >= 0 + 1X mark# s X -> mark# X 0 + 1X >= 0 + 1X mark# cons(X1, X2) -> mark# X1 0 + 1X1 + 1X2 >= 0 + 1X1 a__incr# cons(X, L) -> mark# X 0 + 1X + 1L >= 0 + 1X Weak: a__tail cons(X, L) -> mark L 0 + 1X + 1L >= 0 + 1L a__tail X -> tail X 0 + 1X >= 0 + 1X a__head cons(X, L) -> mark X 0 + 1X + 1L >= 0 + 1X a__head X -> head X 0 + 1X >= 0 + 1X a__nats() -> nats() 1 >= 1 a__nats() -> a__adx a__zeros() 1 >= 0 a__zeros() -> zeros() 0 >= 0 a__zeros() -> cons(0(), zeros()) 0 >= 0 a__adx cons(X, L) -> a__incr cons(mark X, adx L) 0 + 1X + 1L >= 0 + 1X + 1L a__adx nil() -> nil() 0 >= 0 a__adx X -> adx X 0 + 1X >= 0 + 1X mark tail X -> a__tail mark X 0 + 1X >= 0 + 1X mark head X -> a__head mark X 0 + 1X >= 0 + 1X mark nats() -> a__nats() 1 >= 1 mark zeros() -> a__zeros() 0 >= 0 mark 0() -> 0() 0 >= 0 mark adx X -> a__adx mark X 0 + 1X >= 0 + 1X mark incr X -> a__incr mark X 0 + 1X >= 0 + 1X mark s X -> s mark X 0 + 1X >= 0 + 1X mark cons(X1, X2) -> cons(mark X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark nil() -> nil() 0 >= 0 a__incr cons(X, L) -> cons(s mark X, incr L) 0 + 1X + 1L >= 0 + 1X + 1L a__incr nil() -> nil() 0 >= 0 a__incr X -> incr X 0 + 1X >= 0 + 1X 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, a__adx# cons(X, L) -> a__incr# cons(mark X, adx L), a__adx# cons(X, L) -> mark# X} SCC (9): 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, a__adx# cons(X, L) -> a__incr# cons(mark X, adx L), a__adx# cons(X, L) -> mark# X} 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} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [a__incr](x0) = x0, [s](x0) = x0, [mark](x0) = x0, [incr](x0) = x0, [a__adx](x0) = x0 + 1, [adx](x0) = x0 + 1, [a__head](x0) = x0, [a__tail](x0) = x0, [head](x0) = x0, [tail](x0) = x0, [nil] = 0, [a__zeros] = 0, [a__nats] = 1, [0] = 0, [zeros] = 0, [nats] = 1, [a__incr#](x0) = x0, [mark#](x0) = x0, [a__adx#](x0) = x0 + 1 Strict: a__adx# cons(X, L) -> mark# X 1 + 1X + 1L >= 0 + 1X a__adx# cons(X, L) -> a__incr# cons(mark X, adx L) 1 + 1X + 1L >= 1 + 1X + 1L mark# adx X -> a__adx# mark X 1 + 1X >= 1 + 1X mark# adx X -> mark# X 1 + 1X >= 0 + 1X mark# incr X -> mark# X 0 + 1X >= 0 + 1X mark# incr X -> a__incr# mark X 0 + 1X >= 0 + 1X mark# s X -> mark# X 0 + 1X >= 0 + 1X mark# cons(X1, X2) -> mark# X1 0 + 1X1 + 1X2 >= 0 + 1X1 a__incr# cons(X, L) -> mark# X 0 + 1X + 1L >= 0 + 1X Weak: a__tail cons(X, L) -> mark L 0 + 1X + 1L >= 0 + 1L a__tail X -> tail X 0 + 1X >= 0 + 1X a__head cons(X, L) -> mark X 0 + 1X + 1L >= 0 + 1X a__head X -> head X 0 + 1X >= 0 + 1X a__nats() -> nats() 1 >= 1 a__nats() -> a__adx a__zeros() 1 >= 1 a__zeros() -> zeros() 0 >= 0 a__zeros() -> cons(0(), zeros()) 0 >= 0 a__adx cons(X, L) -> a__incr cons(mark X, adx L) 1 + 1X + 1L >= 1 + 1X + 1L a__adx nil() -> nil() 1 >= 0 a__adx X -> adx X 1 + 1X >= 1 + 1X mark tail X -> a__tail mark X 0 + 1X >= 0 + 1X mark head X -> a__head mark X 0 + 1X >= 0 + 1X mark nats() -> a__nats() 1 >= 1 mark zeros() -> a__zeros() 0 >= 0 mark 0() -> 0() 0 >= 0 mark adx X -> a__adx mark X 1 + 1X >= 1 + 1X mark incr X -> a__incr mark X 0 + 1X >= 0 + 1X mark s X -> s mark X 0 + 1X >= 0 + 1X mark cons(X1, X2) -> cons(mark X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 mark nil() -> nil() 0 >= 0 a__incr cons(X, L) -> cons(s mark X, incr L) 0 + 1X + 1L >= 0 + 1X + 1L a__incr nil() -> nil() 0 >= 0 a__incr X -> incr X 0 + 1X >= 0 + 1X 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 -> a__adx# mark X, a__adx# cons(X, L) -> a__incr# cons(mark X, adx L)} SCC (7): 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 -> a__adx# mark X, a__adx# cons(X, L) -> a__incr# cons(mark X, adx 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} Fail