MAYBE Time: 0.174521 TRS: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark tt() -> tt(), mark nil() -> nil(), mark s X -> s mark X, mark and(X1, X2) -> a__and(mark X1, X2), mark length X -> a__length mark X, a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__length X -> length X, a__length cons(N, L) -> s a__length mark L, a__length nil() -> 0()} DP: DP: { mark# cons(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#(), mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2), mark# length X -> mark# X, mark# length X -> a__length# mark X, a__and#(tt(), X) -> mark# X, a__length# cons(N, L) -> mark# L, a__length# cons(N, L) -> a__length# mark L} TRS: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark tt() -> tt(), mark nil() -> nil(), mark s X -> s mark X, mark and(X1, X2) -> a__and(mark X1, X2), mark length X -> a__length mark X, a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__length X -> length X, a__length cons(N, L) -> s a__length mark L, a__length nil() -> 0()} EDG: {(mark# cons(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# cons(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (a__length# cons(N, L) -> a__length# mark L, a__length# cons(N, L) -> a__length# mark L) (a__length# cons(N, L) -> a__length# mark L, a__length# cons(N, L) -> mark# L) (mark# s X -> mark# X, mark# length X -> a__length# mark X) (mark# s X -> mark# X, mark# length X -> mark# X) (mark# s X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# zeros() -> a__zeros#()) (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# length X -> a__length# mark X) (a__and#(tt(), X) -> mark# X, mark# length X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# s X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# zeros() -> a__zeros#()) (a__and#(tt(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# zeros() -> a__zeros#()) (mark# length X -> mark# X, mark# s X -> mark# X) (mark# length X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# length X -> mark# X, mark# length X -> mark# X) (mark# length X -> mark# X, mark# length X -> a__length# mark X) (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(tt(), X) -> mark# X) (mark# length X -> a__length# mark X, a__length# cons(N, L) -> mark# L) (mark# length X -> a__length# mark X, a__length# cons(N, L) -> a__length# mark L) (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (a__length# cons(N, L) -> mark# L, mark# cons(X1, X2) -> mark# X1) (a__length# cons(N, L) -> mark# L, mark# zeros() -> a__zeros#()) (a__length# cons(N, L) -> mark# L, mark# s X -> mark# X) (a__length# cons(N, L) -> mark# L, mark# and(X1, X2) -> mark# X1) (a__length# cons(N, L) -> mark# L, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__length# cons(N, L) -> mark# L, mark# length X -> mark# X) (a__length# cons(N, L) -> mark# L, mark# length X -> a__length# mark X)} STATUS: arrows: 0.530000 SCCS (1): Scc: { mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2), mark# length X -> mark# X, mark# length X -> a__length# mark X, a__and#(tt(), X) -> mark# X, a__length# cons(N, L) -> mark# L, a__length# cons(N, L) -> a__length# mark L} SCC (9): Strict: { mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2), mark# length X -> mark# X, mark# length X -> a__length# mark X, a__and#(tt(), X) -> mark# X, a__length# cons(N, L) -> mark# L, a__length# cons(N, L) -> a__length# mark L} Weak: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark tt() -> tt(), mark nil() -> nil(), mark s X -> s mark X, mark and(X1, X2) -> a__and(mark X1, X2), mark length X -> a__length mark X, a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__length X -> length X, a__length cons(N, L) -> s a__length mark L, a__length nil() -> 0()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [a__and](x0, x1) = x0 + x1 + 1, [and](x0, x1) = x0 + x1 + 1, [mark](x0) = x0, [a__length](x0) = x0, [s](x0) = x0, [length](x0) = x0, [0] = 0, [zeros] = 0, [a__zeros] = 0, [tt] = 0, [nil] = 0, [a__and#](x0, x1) = x0, [mark#](x0) = x0, [a__length#](x0) = x0 Strict: a__length# cons(N, L) -> a__length# mark L 0 + 1L + 1N >= 0 + 1L a__length# cons(N, L) -> mark# L 0 + 1L + 1N >= 0 + 1L a__and#(tt(), X) -> mark# X 0 + 1X >= 0 + 1X mark# length X -> a__length# mark X 0 + 1X >= 0 + 1X mark# length X -> mark# X 0 + 1X >= 0 + 1X mark# and(X1, X2) -> a__and#(mark X1, X2) 1 + 1X1 + 1X2 >= 0 + 0X1 + 1X2 mark# and(X1, X2) -> mark# X1 1 + 1X1 + 1X2 >= 0 + 1X1 mark# s X -> mark# X 0 + 1X >= 0 + 1X mark# cons(X1, X2) -> mark# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: a__length nil() -> 0() 0 >= 0 a__length cons(N, L) -> s a__length mark L 0 + 1L + 1N >= 0 + 1L a__length X -> length X 0 + 1X >= 0 + 1X a__and(tt(), X) -> mark X 1 + 1X >= 0 + 1X a__and(X1, X2) -> and(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 mark length X -> a__length mark X 0 + 1X >= 0 + 1X mark and(X1, X2) -> a__and(mark X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 mark s X -> s mark X 0 + 1X >= 0 + 1X mark nil() -> nil() 0 >= 0 mark tt() -> tt() 0 >= 0 mark zeros() -> a__zeros() 0 >= 0 mark 0() -> 0() 0 >= 0 mark cons(X1, X2) -> cons(mark X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 a__zeros() -> zeros() 0 >= 0 a__zeros() -> cons(0(), zeros()) 0 >= 0 SCCS (1): Scc: { mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X, mark# length X -> mark# X, mark# length X -> a__length# mark X, a__length# cons(N, L) -> mark# L, a__length# cons(N, L) -> a__length# mark L} SCC (6): Strict: { mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X, mark# length X -> mark# X, mark# length X -> a__length# mark X, a__length# cons(N, L) -> mark# L, a__length# cons(N, L) -> a__length# mark L} Weak: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark tt() -> tt(), mark nil() -> nil(), mark s X -> s mark X, mark and(X1, X2) -> a__and(mark X1, X2), mark length X -> a__length mark X, a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__length X -> length X, a__length cons(N, L) -> s a__length mark L, a__length nil() -> 0()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1 + 1, [a__and](x0, x1) = x0 + x1 + 1, [and](x0, x1) = x0 + x1 + 1, [mark](x0) = x0 + 1, [a__length](x0) = x0, [s](x0) = x0, [length](x0) = x0, [0] = 0, [zeros] = 0, [a__zeros] = 1, [tt] = 0, [nil] = 0, [mark#](x0) = x0 + 1, [a__length#](x0) = x0 Strict: a__length# cons(N, L) -> a__length# mark L 1 + 1L + 1N >= 1 + 1L a__length# cons(N, L) -> mark# L 1 + 1L + 1N >= 1 + 1L mark# length X -> a__length# mark X 1 + 1X >= 1 + 1X mark# length X -> mark# X 1 + 1X >= 1 + 1X mark# s X -> mark# X 1 + 1X >= 1 + 1X mark# cons(X1, X2) -> mark# X1 2 + 1X1 + 1X2 >= 1 + 1X1 Weak: a__length nil() -> 0() 0 >= 0 a__length cons(N, L) -> s a__length mark L 1 + 1L + 1N >= 1 + 1L a__length X -> length X 0 + 1X >= 0 + 1X a__and(tt(), X) -> mark X 1 + 1X >= 1 + 1X a__and(X1, X2) -> and(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 mark length X -> a__length mark X 1 + 1X >= 1 + 1X mark and(X1, X2) -> a__and(mark X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 mark s X -> s mark X 1 + 1X >= 1 + 1X mark nil() -> nil() 1 >= 0 mark tt() -> tt() 1 >= 0 mark zeros() -> a__zeros() 1 >= 1 mark 0() -> 0() 1 >= 0 mark cons(X1, X2) -> cons(mark X1, X2) 2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2 a__zeros() -> zeros() 1 >= 0 a__zeros() -> cons(0(), zeros()) 1 >= 1 SCCS (1): Scc: { mark# s X -> mark# X, mark# length X -> mark# X, mark# length X -> a__length# mark X, a__length# cons(N, L) -> mark# L, a__length# cons(N, L) -> a__length# mark L} SCC (5): Strict: { mark# s X -> mark# X, mark# length X -> mark# X, mark# length X -> a__length# mark X, a__length# cons(N, L) -> mark# L, a__length# cons(N, L) -> a__length# mark L} Weak: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark tt() -> tt(), mark nil() -> nil(), mark s X -> s mark X, mark and(X1, X2) -> a__and(mark X1, X2), mark length X -> a__length mark X, a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__length X -> length X, a__length cons(N, L) -> s a__length mark L, a__length nil() -> 0()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0, [a__and](x0, x1) = x0, [and](x0, x1) = x0, [mark](x0) = x0, [a__length](x0) = x0 + 1, [s](x0) = x0, [length](x0) = x0 + 1, [0] = 0, [zeros] = 0, [a__zeros] = 0, [tt] = 0, [nil] = 0, [mark#](x0) = x0, [a__length#](x0) = x0 Strict: a__length# cons(N, L) -> a__length# mark L 0 + 1L + 0N >= 0 + 1L a__length# cons(N, L) -> mark# L 0 + 1L + 0N >= 0 + 1L mark# length X -> a__length# mark X 1 + 1X >= 0 + 1X mark# length X -> mark# X 1 + 1X >= 0 + 1X mark# s X -> mark# X 0 + 1X >= 0 + 1X Weak: a__length nil() -> 0() 1 >= 0 a__length cons(N, L) -> s a__length mark L 1 + 1L + 0N >= 1 + 1L a__length X -> length X 1 + 1X >= 1 + 1X a__and(tt(), X) -> mark X 0 + 1X >= 0 + 1X a__and(X1, X2) -> and(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 mark length X -> a__length mark X 1 + 1X >= 1 + 1X mark and(X1, X2) -> a__and(mark X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 mark s X -> s mark X 0 + 1X >= 0 + 1X mark nil() -> nil() 0 >= 0 mark tt() -> tt() 0 >= 0 mark zeros() -> a__zeros() 0 >= 0 mark 0() -> 0() 0 >= 0 mark cons(X1, X2) -> cons(mark X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 a__zeros() -> zeros() 0 >= 0 a__zeros() -> cons(0(), zeros()) 0 >= 0 SCCS (2): Scc: {a__length# cons(N, L) -> a__length# mark L} Scc: {mark# s X -> mark# X} SCC (1): Strict: {a__length# cons(N, L) -> a__length# mark L} Weak: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark tt() -> tt(), mark nil() -> nil(), mark s X -> s mark X, mark and(X1, X2) -> a__and(mark X1, X2), mark length X -> a__length mark X, a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__length X -> length X, a__length cons(N, L) -> s a__length mark L, a__length nil() -> 0()} Fail SCC (1): Strict: {mark# s X -> mark# X} Weak: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark tt() -> tt(), mark nil() -> nil(), mark s X -> s mark X, mark and(X1, X2) -> a__and(mark X1, X2), mark length X -> a__length mark X, a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__length X -> length X, a__length cons(N, L) -> s a__length mark L, a__length nil() -> 0()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [a__and](x0, x1) = 0, [and](x0, x1) = 0, [mark](x0) = 0, [a__length](x0) = 0, [s](x0) = x0 + 1, [length](x0) = 0, [0] = 0, [zeros] = 0, [a__zeros] = 0, [tt] = 0, [nil] = 0, [mark#](x0) = x0 Strict: mark# s X -> mark# X 1 + 1X >= 0 + 1X Weak: a__length nil() -> 0() 0 >= 0 a__length cons(N, L) -> s a__length mark L 0 + 0L + 0N >= 1 + 0L a__length X -> length X 0 + 0X >= 0 + 0X a__and(tt(), X) -> mark X 0 + 0X >= 0 + 0X a__and(X1, X2) -> and(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark length X -> a__length mark X 0 + 0X >= 0 + 0X mark and(X1, X2) -> a__and(mark X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark s X -> s mark X 0 + 0X >= 1 + 0X mark nil() -> nil() 0 >= 0 mark tt() -> tt() 0 >= 0 mark zeros() -> a__zeros() 0 >= 0 mark 0() -> 0() 0 >= 0 mark cons(X1, X2) -> cons(mark X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 a__zeros() -> zeros() 0 >= 0 a__zeros() -> cons(0(), zeros()) 0 >= 0 Qed