MAYBE Time: 28.101875 TRS: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), a__length X -> length X, a__length cons(N, L) -> a__U11(a__and(a__isNatList L, isNat N), L), a__length nil() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark s X -> s mark X, mark tt() -> tt(), mark length X -> a__length mark X, mark isNatIList X -> a__isNatIList X, mark nil() -> nil(), mark isNatList X -> a__isNatList X, mark isNat X -> a__isNat X, mark U11(X1, X2) -> a__U11(mark X1, X2), mark and(X1, X2) -> a__and(mark X1, X2), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), L) -> s a__length mark L, a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__isNat X -> isNat X, a__isNat 0() -> tt(), a__isNat s V1 -> a__isNat V1, a__isNat length V1 -> a__isNatList V1, a__isNatList X -> isNatList X, a__isNatList cons(V1, V2) -> a__and(a__isNat V1, isNatList V2), a__isNatList nil() -> tt(), a__isNatIList X -> isNatIList X, a__isNatIList V -> a__isNatList V, a__isNatIList cons(V1, V2) -> a__and(a__isNat V1, isNatIList V2), a__isNatIList zeros() -> tt()} DP: DP: { a__length# cons(N, L) -> a__U11#(a__and(a__isNatList L, isNat N), L), a__length# cons(N, L) -> a__and#(a__isNatList L, isNat N), a__length# cons(N, L) -> a__isNatList# L, mark# cons(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#(), mark# s X -> mark# X, mark# length X -> a__length# mark X, mark# length X -> mark# X, mark# isNatIList X -> a__isNatIList# X, mark# isNatList X -> a__isNatList# X, mark# isNat X -> a__isNat# X, mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2), mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2), a__U11#(tt(), L) -> a__length# mark L, a__U11#(tt(), L) -> mark# L, a__and#(tt(), X) -> mark# X, a__isNat# s V1 -> a__isNat# V1, a__isNat# length V1 -> a__isNatList# V1, a__isNatList# cons(V1, V2) -> a__and#(a__isNat V1, isNatList V2), a__isNatList# cons(V1, V2) -> a__isNat# V1, a__isNatIList# V -> a__isNatList# V, a__isNatIList# cons(V1, V2) -> a__and#(a__isNat V1, isNatIList V2), a__isNatIList# cons(V1, V2) -> a__isNat# V1} TRS: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), a__length X -> length X, a__length cons(N, L) -> a__U11(a__and(a__isNatList L, isNat N), L), a__length nil() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark s X -> s mark X, mark tt() -> tt(), mark length X -> a__length mark X, mark isNatIList X -> a__isNatIList X, mark nil() -> nil(), mark isNatList X -> a__isNatList X, mark isNat X -> a__isNat X, mark U11(X1, X2) -> a__U11(mark X1, X2), mark and(X1, X2) -> a__and(mark X1, X2), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), L) -> s a__length mark L, a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__isNat X -> isNat X, a__isNat 0() -> tt(), a__isNat s V1 -> a__isNat V1, a__isNat length V1 -> a__isNatList V1, a__isNatList X -> isNatList X, a__isNatList cons(V1, V2) -> a__and(a__isNat V1, isNatList V2), a__isNatList nil() -> tt(), a__isNatIList X -> isNatIList X, a__isNatIList V -> a__isNatList V, a__isNatIList cons(V1, V2) -> a__and(a__isNat V1, isNatIList V2), a__isNatIList zeros() -> tt()} EDG: {(mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(tt(), X) -> mark# X) (a__U11#(tt(), L) -> mark# L, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__U11#(tt(), L) -> mark# L, mark# and(X1, X2) -> mark# X1) (a__U11#(tt(), L) -> mark# L, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (a__U11#(tt(), L) -> mark# L, mark# U11(X1, X2) -> mark# X1) (a__U11#(tt(), L) -> mark# L, mark# isNat X -> a__isNat# X) (a__U11#(tt(), L) -> mark# L, mark# isNatList X -> a__isNatList# X) (a__U11#(tt(), L) -> mark# L, mark# isNatIList X -> a__isNatIList# X) (a__U11#(tt(), L) -> mark# L, mark# length X -> mark# X) (a__U11#(tt(), L) -> mark# L, mark# length X -> a__length# mark X) (a__U11#(tt(), L) -> mark# L, mark# s X -> mark# X) (a__U11#(tt(), L) -> mark# L, mark# zeros() -> a__zeros#()) (a__U11#(tt(), L) -> mark# L, mark# cons(X1, X2) -> mark# X1) (a__isNatList# cons(V1, V2) -> a__and#(a__isNat V1, isNatList V2), a__and#(tt(), 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# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# s X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# isNat X -> a__isNat# X) (mark# s X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# s X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# s X -> mark# X, mark# length X -> mark# X) (mark# s X -> mark# X, mark# length X -> a__length# mark X) (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) (mark# isNatIList X -> a__isNatIList# X, a__isNatIList# cons(V1, V2) -> a__isNat# V1) (mark# isNatIList X -> a__isNatIList# X, a__isNatIList# cons(V1, V2) -> a__and#(a__isNat V1, isNatIList V2)) (mark# isNatIList X -> a__isNatIList# X, a__isNatIList# V -> a__isNatList# V) (mark# isNat X -> a__isNat# X, a__isNat# length V1 -> a__isNatList# V1) (mark# isNat X -> a__isNat# X, a__isNat# s V1 -> a__isNat# V1) (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# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# cons(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# cons(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# cons(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (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) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# and(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# and(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# and(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (a__isNat# length V1 -> a__isNatList# V1, a__isNatList# cons(V1, V2) -> a__isNat# V1) (a__isNat# length V1 -> a__isNatList# V1, a__isNatList# cons(V1, V2) -> a__and#(a__isNat V1, isNatList V2)) (a__isNatIList# cons(V1, V2) -> a__isNat# V1, a__isNat# length V1 -> a__isNatList# V1) (a__isNatIList# cons(V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNat# V1) (mark# length X -> a__length# mark X, a__length# cons(N, L) -> a__isNatList# L) (mark# length X -> a__length# mark X, a__length# cons(N, L) -> a__and#(a__isNatList L, isNat N)) (mark# length X -> a__length# mark X, a__length# cons(N, L) -> a__U11#(a__and(a__isNatList L, isNat N), L)) (a__U11#(tt(), L) -> a__length# mark L, a__length# cons(N, L) -> a__U11#(a__and(a__isNatList L, isNat N), L)) (a__U11#(tt(), L) -> a__length# mark L, a__length# cons(N, L) -> a__and#(a__isNatList L, isNat N)) (a__U11#(tt(), L) -> a__length# mark L, a__length# cons(N, L) -> a__isNatList# L) (a__isNatIList# V -> a__isNatList# V, a__isNatList# cons(V1, V2) -> a__and#(a__isNat V1, isNatList V2)) (a__isNatIList# V -> a__isNatList# V, a__isNatList# cons(V1, V2) -> a__isNat# V1) (a__length# cons(N, L) -> a__U11#(a__and(a__isNatList L, isNat N), L), a__U11#(tt(), L) -> a__length# mark L) (a__length# cons(N, L) -> a__U11#(a__and(a__isNatList L, isNat N), L), a__U11#(tt(), L) -> mark# L) (a__isNatList# cons(V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNat# V1) (a__isNatList# cons(V1, V2) -> a__isNat# V1, a__isNat# length V1 -> a__isNatList# V1) (a__isNat# s V1 -> a__isNat# V1, a__isNat# s V1 -> a__isNat# V1) (a__isNat# s V1 -> a__isNat# V1, a__isNat# length V1 -> a__isNatList# V1) (mark# U11(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U11(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# U11(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U11(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U11(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U11(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# zeros() -> a__zeros#()) (a__and#(tt(), X) -> mark# X, mark# s X -> mark# X) (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# isNatIList X -> a__isNatIList# X) (a__and#(tt(), X) -> mark# X, mark# isNatList X -> a__isNatList# X) (a__and#(tt(), X) -> mark# X, mark# isNat X -> a__isNat# X) (a__and#(tt(), X) -> mark# X, mark# U11(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# isNatList X -> a__isNatList# X, a__isNatList# cons(V1, V2) -> a__and#(a__isNat V1, isNatList V2)) (mark# isNatList X -> a__isNatList# X, a__isNatList# cons(V1, V2) -> a__isNat# V1) (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# length X -> a__length# mark X) (mark# length X -> mark# X, mark# length X -> mark# X) (mark# length X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# length X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# length X -> mark# X, mark# isNat X -> a__isNat# X) (mark# length X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (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)) (a__isNatIList# cons(V1, V2) -> a__and#(a__isNat V1, isNatIList V2), a__and#(tt(), X) -> mark# X) (a__length# cons(N, L) -> a__and#(a__isNatList L, isNat N), a__and#(tt(), X) -> mark# X) (a__length# cons(N, L) -> a__isNatList# L, a__isNatList# cons(V1, V2) -> a__and#(a__isNat V1, isNatList V2)) (a__length# cons(N, L) -> a__isNatList# L, a__isNatList# cons(V1, V2) -> a__isNat# V1) (mark# U11(X1, X2) -> a__U11#(mark X1, X2), a__U11#(tt(), L) -> a__length# mark L) (mark# U11(X1, X2) -> a__U11#(mark X1, X2), a__U11#(tt(), L) -> mark# L)} STATUS: arrows: 0.812800 SCCS (1): Scc: { a__length# cons(N, L) -> a__U11#(a__and(a__isNatList L, isNat N), L), a__length# cons(N, L) -> a__and#(a__isNatList L, isNat N), a__length# cons(N, L) -> a__isNatList# L, mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X, mark# length X -> a__length# mark X, mark# length X -> mark# X, mark# isNatIList X -> a__isNatIList# X, mark# isNatList X -> a__isNatList# X, mark# isNat X -> a__isNat# X, mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2), mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2), a__U11#(tt(), L) -> a__length# mark L, a__U11#(tt(), L) -> mark# L, a__and#(tt(), X) -> mark# X, a__isNat# s V1 -> a__isNat# V1, a__isNat# length V1 -> a__isNatList# V1, a__isNatList# cons(V1, V2) -> a__and#(a__isNat V1, isNatList V2), a__isNatList# cons(V1, V2) -> a__isNat# V1, a__isNatIList# V -> a__isNatList# V, a__isNatIList# cons(V1, V2) -> a__and#(a__isNat V1, isNatIList V2), a__isNatIList# cons(V1, V2) -> a__isNat# V1} SCC (24): Strict: { a__length# cons(N, L) -> a__U11#(a__and(a__isNatList L, isNat N), L), a__length# cons(N, L) -> a__and#(a__isNatList L, isNat N), a__length# cons(N, L) -> a__isNatList# L, mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X, mark# length X -> a__length# mark X, mark# length X -> mark# X, mark# isNatIList X -> a__isNatIList# X, mark# isNatList X -> a__isNatList# X, mark# isNat X -> a__isNat# X, mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2), mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2), a__U11#(tt(), L) -> a__length# mark L, a__U11#(tt(), L) -> mark# L, a__and#(tt(), X) -> mark# X, a__isNat# s V1 -> a__isNat# V1, a__isNat# length V1 -> a__isNatList# V1, a__isNatList# cons(V1, V2) -> a__and#(a__isNat V1, isNatList V2), a__isNatList# cons(V1, V2) -> a__isNat# V1, a__isNatIList# V -> a__isNatList# V, a__isNatIList# cons(V1, V2) -> a__and#(a__isNat V1, isNatIList V2), a__isNatIList# cons(V1, V2) -> a__isNat# V1} Weak: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), a__length X -> length X, a__length cons(N, L) -> a__U11(a__and(a__isNatList L, isNat N), L), a__length nil() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark s X -> s mark X, mark tt() -> tt(), mark length X -> a__length mark X, mark isNatIList X -> a__isNatIList X, mark nil() -> nil(), mark isNatList X -> a__isNatList X, mark isNat X -> a__isNat X, mark U11(X1, X2) -> a__U11(mark X1, X2), mark and(X1, X2) -> a__and(mark X1, X2), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), L) -> s a__length mark L, a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__isNat X -> isNat X, a__isNat 0() -> tt(), a__isNat s V1 -> a__isNat V1, a__isNat length V1 -> a__isNatList V1, a__isNatList X -> isNatList X, a__isNatList cons(V1, V2) -> a__and(a__isNat V1, isNatList V2), a__isNatList nil() -> tt(), a__isNatIList X -> isNatIList X, a__isNatIList V -> a__isNatList V, a__isNatIList cons(V1, V2) -> a__and(a__isNat V1, isNatIList V2), a__isNatIList zeros() -> tt()} Open