MAYBE Time: 0.036026 TRS: { incr X -> n__incr X, incr nil() -> nil(), incr cons(X, L) -> cons(s X, n__incr activate L), activate X -> X, activate n__incr X -> incr X, activate n__adx X -> adx X, activate n__zeros() -> zeros(), adx X -> n__adx X, adx nil() -> nil(), adx cons(X, L) -> incr cons(X, n__adx activate L), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), nats() -> adx zeros(), head cons(X, L) -> X, tail cons(X, L) -> activate L} DP: DP: { incr# cons(X, L) -> activate# L, activate# n__incr X -> incr# X, activate# n__adx X -> adx# X, activate# n__zeros() -> zeros#(), adx# cons(X, L) -> incr# cons(X, n__adx activate L), adx# cons(X, L) -> activate# L, nats#() -> adx# zeros(), nats#() -> zeros#(), tail# cons(X, L) -> activate# L} TRS: { incr X -> n__incr X, incr nil() -> nil(), incr cons(X, L) -> cons(s X, n__incr activate L), activate X -> X, activate n__incr X -> incr X, activate n__adx X -> adx X, activate n__zeros() -> zeros(), adx X -> n__adx X, adx nil() -> nil(), adx cons(X, L) -> incr cons(X, n__adx activate L), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), nats() -> adx zeros(), head cons(X, L) -> X, tail cons(X, L) -> activate L} UR: { incr X -> n__incr X, incr nil() -> nil(), incr cons(X, L) -> cons(s X, n__incr activate L), activate X -> X, activate n__incr X -> incr X, activate n__adx X -> adx X, activate n__zeros() -> zeros(), adx X -> n__adx X, adx nil() -> nil(), adx cons(X, L) -> incr cons(X, n__adx activate L), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros()} EDG: {(activate# n__adx X -> adx# X, adx# cons(X, L) -> activate# L) (activate# n__adx X -> adx# X, adx# cons(X, L) -> incr# cons(X, n__adx activate L)) (nats#() -> adx# zeros(), adx# cons(X, L) -> activate# L) (nats#() -> adx# zeros(), adx# cons(X, L) -> incr# cons(X, n__adx activate L)) (adx# cons(X, L) -> activate# L, activate# n__zeros() -> zeros#()) (adx# cons(X, L) -> activate# L, activate# n__adx X -> adx# X) (adx# cons(X, L) -> activate# L, activate# n__incr X -> incr# X) (tail# cons(X, L) -> activate# L, activate# n__incr X -> incr# X) (tail# cons(X, L) -> activate# L, activate# n__adx X -> adx# X) (tail# cons(X, L) -> activate# L, activate# n__zeros() -> zeros#()) (incr# cons(X, L) -> activate# L, activate# n__incr X -> incr# X) (incr# cons(X, L) -> activate# L, activate# n__adx X -> adx# X) (incr# cons(X, L) -> activate# L, activate# n__zeros() -> zeros#()) (adx# cons(X, L) -> incr# cons(X, n__adx activate L), incr# cons(X, L) -> activate# L) (activate# n__incr X -> incr# X, incr# cons(X, L) -> activate# L)} STATUS: arrows: 0.814815 SCCS (1): Scc: { incr# cons(X, L) -> activate# L, activate# n__incr X -> incr# X, activate# n__adx X -> adx# X, adx# cons(X, L) -> incr# cons(X, n__adx activate L), adx# cons(X, L) -> activate# L} SCC (5): Strict: { incr# cons(X, L) -> activate# L, activate# n__incr X -> incr# X, activate# n__adx X -> adx# X, adx# cons(X, L) -> incr# cons(X, n__adx activate L), adx# cons(X, L) -> activate# L} Weak: { incr X -> n__incr X, incr nil() -> nil(), incr cons(X, L) -> cons(s X, n__incr activate L), activate X -> X, activate n__incr X -> incr X, activate n__adx X -> adx X, activate n__zeros() -> zeros(), adx X -> n__adx X, adx nil() -> nil(), adx cons(X, L) -> incr cons(X, n__adx activate L), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), nats() -> adx zeros(), head cons(X, L) -> X, tail cons(X, L) -> activate L} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0, [incr](x0) = x0, [s](x0) = 0, [n__incr](x0) = x0, [activate](x0) = x0, [adx](x0) = x0 + 1, [n__adx](x0) = x0 + 1, [head](x0) = 0, [tail](x0) = 0, [nil] = 1, [zeros] = 0, [nats] = 0, [0] = 0, [n__zeros] = 0, [incr#](x0) = x0, [activate#](x0) = x0, [adx#](x0) = x0 + 1 Strict: adx# cons(X, L) -> activate# L 1 + 0X + 1L >= 0 + 1L adx# cons(X, L) -> incr# cons(X, n__adx activate L) 1 + 0X + 1L >= 1 + 0X + 1L activate# n__adx X -> adx# X 1 + 1X >= 1 + 1X activate# n__incr X -> incr# X 0 + 1X >= 0 + 1X incr# cons(X, L) -> activate# L 0 + 0X + 1L >= 0 + 1L Weak: tail cons(X, L) -> activate L 0 + 0X + 0L >= 0 + 1L head cons(X, L) -> X 0 + 0X + 0L >= 1X nats() -> adx zeros() 0 >= 1 zeros() -> n__zeros() 0 >= 0 zeros() -> cons(0(), n__zeros()) 0 >= 0 adx cons(X, L) -> incr cons(X, n__adx activate L) 1 + 0X + 1L >= 1 + 0X + 1L adx nil() -> nil() 2 >= 1 adx X -> n__adx X 1 + 1X >= 1 + 1X activate n__zeros() -> zeros() 0 >= 0 activate n__adx X -> adx X 1 + 1X >= 1 + 1X activate n__incr X -> incr X 0 + 1X >= 0 + 1X activate X -> X 0 + 1X >= 1X incr cons(X, L) -> cons(s X, n__incr activate L) 0 + 0X + 1L >= 0 + 0X + 1L incr nil() -> nil() 1 >= 1 incr X -> n__incr X 0 + 1X >= 0 + 1X SCCS (1): Scc: { incr# cons(X, L) -> activate# L, activate# n__incr X -> incr# X, activate# n__adx X -> adx# X, adx# cons(X, L) -> incr# cons(X, n__adx activate L)} SCC (4): Strict: { incr# cons(X, L) -> activate# L, activate# n__incr X -> incr# X, activate# n__adx X -> adx# X, adx# cons(X, L) -> incr# cons(X, n__adx activate L)} Weak: { incr X -> n__incr X, incr nil() -> nil(), incr cons(X, L) -> cons(s X, n__incr activate L), activate X -> X, activate n__incr X -> incr X, activate n__adx X -> adx X, activate n__zeros() -> zeros(), adx X -> n__adx X, adx nil() -> nil(), adx cons(X, L) -> incr cons(X, n__adx activate L), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), nats() -> adx zeros(), head cons(X, L) -> X, tail cons(X, L) -> activate L} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0, [incr](x0) = x0 + 1, [s](x0) = 0, [n__incr](x0) = x0 + 1, [activate](x0) = 0, [adx](x0) = x0 + 1, [n__adx](x0) = 0, [head](x0) = 0, [tail](x0) = 0, [nil] = 1, [zeros] = 0, [nats] = 0, [0] = 0, [n__zeros] = 0, [incr#](x0) = x0, [activate#](x0) = x0, [adx#](x0) = 0 Strict: adx# cons(X, L) -> incr# cons(X, n__adx activate L) 0 + 0X + 0L >= 0 + 0X + 0L activate# n__adx X -> adx# X 0 + 0X >= 0 + 0X activate# n__incr X -> incr# X 1 + 1X >= 0 + 1X incr# cons(X, L) -> activate# L 0 + 0X + 1L >= 0 + 1L Weak: tail cons(X, L) -> activate L 0 + 0X + 0L >= 0 + 0L head cons(X, L) -> X 0 + 0X + 0L >= 1X nats() -> adx zeros() 0 >= 1 zeros() -> n__zeros() 0 >= 0 zeros() -> cons(0(), n__zeros()) 0 >= 0 adx cons(X, L) -> incr cons(X, n__adx activate L) 1 + 0X + 1L >= 1 + 0X + 0L adx nil() -> nil() 2 >= 1 adx X -> n__adx X 1 + 1X >= 0 + 0X activate n__zeros() -> zeros() 0 >= 0 activate n__adx X -> adx X 0 + 0X >= 1 + 1X activate n__incr X -> incr X 0 + 0X >= 1 + 1X activate X -> X 0 + 0X >= 1X incr cons(X, L) -> cons(s X, n__incr activate L) 1 + 0X + 1L >= 1 + 0X + 0L incr nil() -> nil() 2 >= 1 incr X -> n__incr X 1 + 1X >= 1 + 1X SCCS (1): Scc: { incr# cons(X, L) -> activate# L, activate# n__adx X -> adx# X, adx# cons(X, L) -> incr# cons(X, n__adx activate L)} SCC (3): Strict: { incr# cons(X, L) -> activate# L, activate# n__adx X -> adx# X, adx# cons(X, L) -> incr# cons(X, n__adx activate L)} Weak: { incr X -> n__incr X, incr nil() -> nil(), incr cons(X, L) -> cons(s X, n__incr activate L), activate X -> X, activate n__incr X -> incr X, activate n__adx X -> adx X, activate n__zeros() -> zeros(), adx X -> n__adx X, adx nil() -> nil(), adx cons(X, L) -> incr cons(X, n__adx activate L), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), nats() -> adx zeros(), head cons(X, L) -> X, tail cons(X, L) -> activate L} Fail