MAYBE 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(nil()) -> nil(), mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)), mark(length(X)) -> a__length(mark(X)), mark(isNatIList(X)) -> a__isNatIList(X), mark(isNatList(X)) -> a__isNatList(X), mark(isNat(X)) -> a__isNat(X), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(U11(X1, X2)) -> a__U11(mark(X1), X2), mark(U21(X)) -> a__U21(mark(X)), mark(U31(X1, X2, X3, X4)) -> a__U31(mark(X1), X2, X3, X4), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), L) -> s(a__length(mark(L))), a__U21(X) -> U21(X), a__U21(tt()) -> nil(), a__U31(X1, X2, X3, X4) -> U31(X1, X2, X3, X4), a__U31(tt(), IL, M, N) -> cons(mark(N), take(M, IL)), 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__isNatList(take(V1, V2)) -> a__and(a__isNat(V1), isNatIList(V2)), 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(), a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U21(a__isNatIList(IL)), a__take(s(M), cons(N, IL)) -> a__U31(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)} DP: 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#(zeros()) -> a__zeros#(), mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), 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#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), mark#(U11(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2), mark#(U21(X)) -> mark#(X), mark#(U21(X)) -> a__U21#(mark(X)), mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4), a__U11#(tt(), L) -> a__length#(mark(L)), a__U11#(tt(), L) -> mark#(L), a__U31#(tt(), IL, M, N) -> mark#(N), 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__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__isNatList#(take(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), a__take#(0(), IL) -> a__U21#(a__isNatIList(IL)), a__take#(0(), IL) -> a__isNatIList#(IL), a__take#(s(M), cons(N, IL)) -> a__U31#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N), a__take#(s(M), cons(N, IL)) -> a__and#(a__isNatIList(IL), and(isNat(M), isNat(N))), a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL)} 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(nil()) -> nil(), mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)), mark(length(X)) -> a__length(mark(X)), mark(isNatIList(X)) -> a__isNatIList(X), mark(isNatList(X)) -> a__isNatList(X), mark(isNat(X)) -> a__isNat(X), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(U11(X1, X2)) -> a__U11(mark(X1), X2), mark(U21(X)) -> a__U21(mark(X)), mark(U31(X1, X2, X3, X4)) -> a__U31(mark(X1), X2, X3, X4), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), L) -> s(a__length(mark(L))), a__U21(X) -> U21(X), a__U21(tt()) -> nil(), a__U31(X1, X2, X3, X4) -> U31(X1, X2, X3, X4), a__U31(tt(), IL, M, N) -> cons(mark(N), take(M, IL)), 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__isNatList(take(V1, V2)) -> a__and(a__isNat(V1), isNatIList(V2)), 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(), a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U21(a__isNatIList(IL)), a__take(s(M), cons(N, IL)) -> a__U31(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)} EDG: { (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)) (mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__and#(tt(), X) -> mark#(X)) (a__take#(0(), IL) -> a__isNatIList#(IL), a__isNatIList#(cons(V1, V2)) -> a__isNat#(V1)) (a__take#(0(), IL) -> a__isNatIList#(IL), a__isNatIList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (a__take#(0(), IL) -> a__isNatIList#(IL), a__isNatIList#(V) -> a__isNatList#(V)) (a__isNat#(s(V1)) -> 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__isNatList#(cons(V1, V2)) -> a__isNat#(V1), a__isNat#(length(V1)) -> a__isNatList#(V1)) (a__isNatList#(cons(V1, V2)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1)) (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)) (a__length#(cons(N, L)) -> a__and#(a__isNatList(L), isNat(N)), a__and#(tt(), X) -> mark#(X)) (a__isNatList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatList(V2)), a__and#(tt(), X) -> mark#(X)) (a__isNatIList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__and#(tt(), X) -> mark#(X)) (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(V1, V2)) -> a__isNat#(V1)) (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(V1, V2)) -> a__isNat#(V1)) (a__length#(cons(N, L)) -> a__isNatList#(L), a__isNatList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatList(V2))) (mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4), a__U31#(tt(), IL, M, N) -> mark#(N)) (mark#(length(X)) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (mark#(length(X)) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (mark#(length(X)) -> mark#(X), mark#(U21(X)) -> a__U21#(mark(X))) (mark#(length(X)) -> mark#(X), mark#(U21(X)) -> mark#(X)) (mark#(length(X)) -> mark#(X), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(length(X)) -> mark#(X), mark#(U11(X1, X2)) -> mark#(X1)) (mark#(length(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(length(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1)) (mark#(length(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X)) (mark#(length(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X)) (mark#(length(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(length(X)) -> mark#(X), mark#(length(X)) -> mark#(X)) (mark#(length(X)) -> mark#(X), mark#(length(X)) -> a__length#(mark(X))) (mark#(length(X)) -> mark#(X), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (mark#(length(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(length(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(length(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(length(X)) -> mark#(X), mark#(zeros()) -> a__zeros#()) (mark#(length(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(V1, V2)) -> a__isNat#(V1)) (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(V1, V2)) -> a__isNat#(V1)) (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatList(V2))) (mark#(U21(X)) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (mark#(U21(X)) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (mark#(U21(X)) -> mark#(X), mark#(U21(X)) -> a__U21#(mark(X))) (mark#(U21(X)) -> mark#(X), mark#(U21(X)) -> mark#(X)) (mark#(U21(X)) -> mark#(X), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(U21(X)) -> mark#(X), mark#(U11(X1, X2)) -> mark#(X1)) (mark#(U21(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U21(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U21(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U21(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X)) (mark#(U21(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(U21(X)) -> mark#(X), mark#(length(X)) -> mark#(X)) (mark#(U21(X)) -> mark#(X), mark#(length(X)) -> a__length#(mark(X))) (mark#(U21(X)) -> mark#(X), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (mark#(U21(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(U21(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(U21(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(U21(X)) -> mark#(X), mark#(zeros()) -> a__zeros#()) (mark#(U21(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (a__isNatIList#(V) -> a__isNatList#(V), a__isNatList#(take(V1, V2)) -> a__isNat#(V1)) (a__isNatIList#(V) -> a__isNatList#(V), a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (a__isNatIList#(V) -> a__isNatList#(V), a__isNatList#(cons(V1, V2)) -> a__isNat#(V1)) (a__isNatIList#(V) -> a__isNatList#(V), a__isNatList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatList(V2))) (mark#(take(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (mark#(take(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X1), mark#(U21(X)) -> a__U21#(mark(X))) (mark#(take(X1, X2)) -> mark#(X1), mark#(U21(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(take(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(take(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(length(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(length(X)) -> a__length#(mark(X))) (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2)) (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(zeros()) -> a__zeros#()) (mark#(take(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(U21(X)) -> a__U21#(mark(X))) (mark#(U11(X1, X2)) -> mark#(X1), mark#(U21(X)) -> mark#(X)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(length(X)) -> mark#(X)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(length(X)) -> a__length#(mark(X))) (mark#(U11(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (mark#(U11(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(U11(X1, X2)) -> mark#(X1), mark#(zeros()) -> a__zeros#()) (mark#(U11(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (a__take#(s(M), cons(N, IL)) -> a__U31#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N), a__U31#(tt(), IL, M, N) -> mark#(N)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(zeros()) -> a__zeros#()) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(length(X)) -> a__length#(mark(X))) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(length(X)) -> mark#(X)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(U21(X)) -> mark#(X)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(U21(X)) -> a__U21#(mark(X))) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (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#(take(X1, X2)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2)) (mark#(and(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (mark#(and(X1, X2)) -> mark#(X1), mark#(length(X)) -> a__length#(mark(X))) (mark#(and(X1, X2)) -> mark#(X1), mark#(length(X)) -> mark#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(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#(U11(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#(U21(X)) -> mark#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U21(X)) -> a__U21#(mark(X))) (mark#(and(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(zeros()) -> a__zeros#()) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (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#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(U11(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#(U21(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(U21(X)) -> a__U21#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (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#(take(X1, X2)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (a__and#(tt(), X) -> mark#(X), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (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#(and(X1, X2)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (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#(U21(X)) -> mark#(X)) (a__and#(tt(), X) -> mark#(X), mark#(U21(X)) -> a__U21#(mark(X))) (a__and#(tt(), X) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(s(V1)) -> a__isNat#(V1)) (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(length(V1)) -> a__isNatList#(V1)) (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(V) -> a__isNatList#(V)) (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#(cons(V1, V2)) -> a__isNat#(V1)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(zeros()) -> a__zeros#()) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (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#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(s(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X)) (mark#(s(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X)) (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(s(X)) -> mark#(X), mark#(U11(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(s(X)) -> mark#(X), mark#(U21(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(U21(X)) -> a__U21#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (a__U11#(tt(), L) -> mark#(L), mark#(cons(X1, X2)) -> mark#(X1)) (a__U11#(tt(), L) -> mark#(L), mark#(zeros()) -> a__zeros#()) (a__U11#(tt(), L) -> mark#(L), mark#(s(X)) -> mark#(X)) (a__U11#(tt(), L) -> mark#(L), mark#(take(X1, X2)) -> mark#(X1)) (a__U11#(tt(), L) -> mark#(L), mark#(take(X1, X2)) -> mark#(X2)) (a__U11#(tt(), L) -> mark#(L), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (a__U11#(tt(), L) -> mark#(L), mark#(length(X)) -> a__length#(mark(X))) (a__U11#(tt(), L) -> mark#(L), mark#(length(X)) -> mark#(X)) (a__U11#(tt(), L) -> mark#(L), mark#(isNatIList(X)) -> a__isNatIList#(X)) (a__U11#(tt(), L) -> mark#(L), mark#(isNatList(X)) -> a__isNatList#(X)) (a__U11#(tt(), L) -> mark#(L), mark#(isNat(X)) -> a__isNat#(X)) (a__U11#(tt(), L) -> mark#(L), mark#(and(X1, X2)) -> mark#(X1)) (a__U11#(tt(), L) -> mark#(L), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a__U11#(tt(), L) -> mark#(L), mark#(U11(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#(U21(X)) -> mark#(X)) (a__U11#(tt(), L) -> mark#(L), mark#(U21(X)) -> a__U21#(mark(X))) (a__U11#(tt(), L) -> mark#(L), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (a__U11#(tt(), L) -> mark#(L), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (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#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__and#(tt(), X) -> mark#(X)) (mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), a__take#(0(), IL) -> a__U21#(a__isNatIList(IL))) (mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), a__take#(0(), IL) -> a__isNatIList#(IL)) (mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), a__take#(s(M), cons(N, IL)) -> a__U31#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)) (mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), a__take#(s(M), cons(N, IL)) -> a__and#(a__isNatIList(IL), and(isNat(M), isNat(N)))) (mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL)) (mark#(take(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X2), mark#(zeros()) -> a__zeros#()) (mark#(take(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X2)) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (mark#(take(X1, X2)) -> mark#(X2), mark#(length(X)) -> a__length#(mark(X))) (mark#(take(X1, X2)) -> mark#(X2), mark#(length(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(isNatList(X)) -> a__isNatList#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(isNat(X)) -> a__isNat#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(take(X1, X2)) -> mark#(X2), mark#(U11(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X2), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(take(X1, X2)) -> mark#(X2), mark#(U21(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(U21(X)) -> a__U21#(mark(X))) (mark#(take(X1, X2)) -> mark#(X2), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X2), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (a__isNatList#(take(V1, V2)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1)) (a__isNatList#(take(V1, V2)) -> a__isNat#(V1), a__isNat#(length(V1)) -> a__isNatList#(V1)) (a__isNat#(length(V1)) -> a__isNatList#(V1), a__isNatList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatList(V2))) (a__isNat#(length(V1)) -> a__isNatList#(V1), a__isNatList#(cons(V1, V2)) -> a__isNat#(V1)) (a__isNat#(length(V1)) -> a__isNatList#(V1), a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (a__isNat#(length(V1)) -> a__isNatList#(V1), a__isNatList#(take(V1, V2)) -> a__isNat#(V1)) (a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(V) -> a__isNatList#(V)) (a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(V1, V2)) -> a__isNat#(V1)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(cons(X1, X2)) -> mark#(X1)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(zeros()) -> a__zeros#()) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(s(X)) -> mark#(X)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(take(X1, X2)) -> mark#(X1)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(take(X1, X2)) -> mark#(X2)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(length(X)) -> a__length#(mark(X))) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(length(X)) -> mark#(X)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(isNatIList(X)) -> a__isNatIList#(X)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(isNatList(X)) -> a__isNatList#(X)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(U11(X1, X2)) -> mark#(X1)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(U21(X)) -> mark#(X)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(U21(X)) -> a__U21#(mark(X))) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (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)) (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)) (a__take#(s(M), cons(N, IL)) -> a__and#(a__isNatIList(IL), and(isNat(M), isNat(N))), a__and#(tt(), X) -> mark#(X)) } SCCS: 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#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), 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#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), mark#(U11(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2), mark#(U21(X)) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4), a__U11#(tt(), L) -> a__length#(mark(L)), a__U11#(tt(), L) -> mark#(L), a__U31#(tt(), IL, M, N) -> mark#(N), 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__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__isNatList#(take(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), a__take#(0(), IL) -> a__isNatIList#(IL), a__take#(s(M), cons(N, IL)) -> a__U31#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N), a__take#(s(M), cons(N, IL)) -> a__and#(a__isNatIList(IL), and(isNat(M), isNat(N))), a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL)} SCC: 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#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), 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#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), mark#(U11(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2), mark#(U21(X)) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4), a__U11#(tt(), L) -> a__length#(mark(L)), a__U11#(tt(), L) -> mark#(L), a__U31#(tt(), IL, M, N) -> mark#(N), 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__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__isNatList#(take(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), a__take#(0(), IL) -> a__isNatIList#(IL), a__take#(s(M), cons(N, IL)) -> a__U31#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N), a__take#(s(M), cons(N, IL)) -> a__and#(a__isNatIList(IL), and(isNat(M), isNat(N))), a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL)} 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(nil()) -> nil(), mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)), mark(length(X)) -> a__length(mark(X)), mark(isNatIList(X)) -> a__isNatIList(X), mark(isNatList(X)) -> a__isNatList(X), mark(isNat(X)) -> a__isNat(X), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(U11(X1, X2)) -> a__U11(mark(X1), X2), mark(U21(X)) -> a__U21(mark(X)), mark(U31(X1, X2, X3, X4)) -> a__U31(mark(X1), X2, X3, X4), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), L) -> s(a__length(mark(L))), a__U21(X) -> U21(X), a__U21(tt()) -> nil(), a__U31(X1, X2, X3, X4) -> U31(X1, X2, X3, X4), a__U31(tt(), IL, M, N) -> cons(mark(N), take(M, IL)), 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__isNatList(take(V1, V2)) -> a__and(a__isNat(V1), isNatIList(V2)), 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(), a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U21(a__isNatIList(IL)), a__take(s(M), cons(N, IL)) -> a__U31(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)} POLY: Argument Filtering: pi(U31) = [0,1,2,3], pi(U21) = 0, pi(U11) = [0,1], pi(and) = [0,1], pi(a__take#) = 1, pi(a__take) = [0,1], pi(isNat) = [], pi(isNatList) = [], pi(isNatIList) = [], pi(a__isNatIList#) = [], pi(a__isNatIList) = [], pi(length) = [0], pi(a__isNatList#) = [], pi(a__isNatList) = [], pi(a__isNat#) = [], pi(a__isNat) = [], pi(a__and#) = 1, pi(a__and) = [0,1], pi(a__U31#) = [1,3], pi(a__U31) = [0,1,2,3], pi(take) = [0,1], pi(a__U21) = 0, pi(nil) = [], pi(tt) = [], pi(a__U11#) = [1], pi(a__U11) = [0,1], pi(mark#) = 0, pi(mark) = 0, pi(a__length#) = [0], pi(a__length) = [0], pi(s) = 0, pi(a__zeros) = [], pi(zeros) = [], pi(0) = [], pi(cons) = [0,1] Usable Rules: {} Interpretation: [a__U31#](x0, x1) = x0 + x1, [a__U11#](x0) = x0 + 1, [a__isNatIList#] = 0, [a__isNatList#] = 0, [a__isNat#] = 0, [a__length#](x0) = x0 + 1, [U31](x0, x1, x2, x3) = x0 + x1 + x2 + x3, [U11](x0, x1) = x0 + x1 + 1, [and](x0, x1) = x0 + x1, [take](x0, x1) = x0 + x1, [cons](x0, x1) = x0 + x1, [isNat] = 0, [isNatList] = 0, [isNatIList] = 0, [length](x0) = x0 + 1 Strict: { a__length#(cons(N, L)) -> a__U11#(a__and(a__isNatList(L), isNat(N)), L), mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), mark#(length(X)) -> a__length#(mark(X)), mark#(isNatIList(X)) -> a__isNatIList#(X), mark#(isNatList(X)) -> a__isNatList#(X), mark#(isNat(X)) -> a__isNat#(X), mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2), mark#(U21(X)) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4), a__U11#(tt(), L) -> a__length#(mark(L)), a__U31#(tt(), IL, M, N) -> mark#(N), 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__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__isNatList#(take(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), a__take#(0(), IL) -> a__isNatIList#(IL), a__take#(s(M), cons(N, IL)) -> a__U31#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N), a__take#(s(M), cons(N, IL)) -> a__and#(a__isNatIList(IL), and(isNat(M), isNat(N))), a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL)} 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(nil()) -> nil(), mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)), mark(length(X)) -> a__length(mark(X)), mark(isNatIList(X)) -> a__isNatIList(X), mark(isNatList(X)) -> a__isNatList(X), mark(isNat(X)) -> a__isNat(X), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(U11(X1, X2)) -> a__U11(mark(X1), X2), mark(U21(X)) -> a__U21(mark(X)), mark(U31(X1, X2, X3, X4)) -> a__U31(mark(X1), X2, X3, X4), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), L) -> s(a__length(mark(L))), a__U21(X) -> U21(X), a__U21(tt()) -> nil(), a__U31(X1, X2, X3, X4) -> U31(X1, X2, X3, X4), a__U31(tt(), IL, M, N) -> cons(mark(N), take(M, IL)), 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__isNatList(take(V1, V2)) -> a__and(a__isNat(V1), isNatIList(V2)), 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(), a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U21(a__isNatIList(IL)), a__take(s(M), cons(N, IL)) -> a__U31(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)} EDG: { (mark#(length(X)) -> a__length#(mark(X)), a__length#(cons(N, L)) -> a__U11#(a__and(a__isNatList(L), isNat(N)), L)) (mark#(take(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (mark#(take(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X1), mark#(U21(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(take(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(take(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(length(X)) -> a__length#(mark(X))) (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2)) (mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(U21(X)) -> mark#(X)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(length(X)) -> a__length#(mark(X))) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (a__isNat#(s(V1)) -> 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__isNatList#(cons(V1, V2)) -> a__isNat#(V1), a__isNat#(length(V1)) -> a__isNatList#(V1)) (a__isNatList#(cons(V1, V2)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1)) (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#(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)) (a__and#(tt(), X) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (a__and#(tt(), X) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(U21(X)) -> mark#(X)) (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)) -> a__and#(mark(X1), X2)) (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X)) (a__and#(tt(), X) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X)) (a__and#(tt(), X) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X)) (a__and#(tt(), X) -> mark#(X), mark#(length(X)) -> a__length#(mark(X))) (a__and#(tt(), X) -> mark#(X), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (a__and#(tt(), X) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (a__and#(tt(), X) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(s(X)) -> mark#(X)) (a__and#(tt(), X) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(U21(X)) -> mark#(X)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(isNatList(X)) -> a__isNatList#(X)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(isNatIList(X)) -> a__isNatIList#(X)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(length(X)) -> a__length#(mark(X))) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(take(X1, X2)) -> mark#(X2)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(take(X1, X2)) -> mark#(X1)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(s(X)) -> mark#(X)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL)) (mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), a__take#(s(M), cons(N, IL)) -> a__and#(a__isNatIList(IL), and(isNat(M), isNat(N)))) (mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), a__take#(s(M), cons(N, IL)) -> a__U31#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)) (mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), a__take#(0(), IL) -> a__isNatIList#(IL)) (a__isNatList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatList(V2)), a__and#(tt(), X) -> mark#(X)) (a__isNatIList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__and#(tt(), X) -> mark#(X)) (mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__and#(tt(), X) -> mark#(X)) (a__take#(0(), IL) -> a__isNatIList#(IL), a__isNatIList#(cons(V1, V2)) -> a__isNat#(V1)) (a__take#(0(), IL) -> a__isNatIList#(IL), a__isNatIList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (a__take#(0(), IL) -> a__isNatIList#(IL), a__isNatIList#(V) -> a__isNatList#(V)) (a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(V1, V2)) -> a__isNat#(V1)) (a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(V) -> a__isNatList#(V)) (a__take#(s(M), cons(N, IL)) -> a__U31#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N), a__U31#(tt(), IL, M, N) -> mark#(N)) (mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2), a__U11#(tt(), L) -> a__length#(mark(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__isNatIList#(V) -> a__isNatList#(V), a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (a__isNatIList#(V) -> a__isNatList#(V), a__isNatList#(take(V1, V2)) -> a__isNat#(V1)) (a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__and#(tt(), X) -> mark#(X)) (mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4), a__U31#(tt(), IL, M, N) -> mark#(N)) (mark#(take(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> mark#(X2)) (mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (mark#(take(X1, X2)) -> mark#(X2), mark#(length(X)) -> a__length#(mark(X))) (mark#(take(X1, X2)) -> mark#(X2), mark#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(isNatList(X)) -> a__isNatList#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(isNat(X)) -> a__isNat#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(take(X1, X2)) -> mark#(X2), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(take(X1, X2)) -> mark#(X2), mark#(U21(X)) -> mark#(X)) (mark#(take(X1, X2)) -> mark#(X2), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (mark#(take(X1, X2)) -> mark#(X2), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (a__length#(cons(N, L)) -> a__U11#(a__and(a__isNatList(L), isNat(N)), L), a__U11#(tt(), L) -> a__length#(mark(L))) (mark#(U21(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(U21(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(U21(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(U21(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(U21(X)) -> mark#(X), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (mark#(U21(X)) -> mark#(X), mark#(length(X)) -> a__length#(mark(X))) (mark#(U21(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(U21(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X)) (mark#(U21(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X)) (mark#(U21(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1)) (mark#(U21(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(U21(X)) -> mark#(X), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(U21(X)) -> mark#(X), mark#(U21(X)) -> mark#(X)) (mark#(U21(X)) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (mark#(U21(X)) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (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#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(V1, V2)) -> a__isNat#(V1)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (mark#(s(X)) -> mark#(X), mark#(length(X)) -> a__length#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(s(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X)) (mark#(s(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X)) (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(s(X)) -> mark#(X), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(s(X)) -> mark#(X), mark#(U21(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (a__isNatList#(take(V1, V2)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1)) (a__isNatList#(take(V1, V2)) -> a__isNat#(V1), a__isNat#(length(V1)) -> a__isNatList#(V1)) (a__isNat#(length(V1)) -> a__isNatList#(V1), a__isNatList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatList(V2))) (a__isNat#(length(V1)) -> a__isNatList#(V1), a__isNatList#(cons(V1, V2)) -> a__isNat#(V1)) (a__isNat#(length(V1)) -> a__isNatList#(V1), a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (a__isNat#(length(V1)) -> a__isNatList#(V1), a__isNatList#(take(V1, V2)) -> a__isNat#(V1)) (a__U11#(tt(), L) -> a__length#(mark(L)), a__length#(cons(N, L)) -> a__U11#(a__and(a__isNatList(L), isNat(N)), L)) (mark#(and(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2)) (mark#(and(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (mark#(and(X1, X2)) -> mark#(X1), mark#(length(X)) -> a__length#(mark(X))) (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(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#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U21(X)) -> mark#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (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#(take(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(length(X)) -> a__length#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(U21(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4)) (a__take#(s(M), cons(N, IL)) -> a__and#(a__isNatIList(IL), and(isNat(M), isNat(N))), a__and#(tt(), X) -> mark#(X)) } SCCS: Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), mark#(isNatIList(X)) -> a__isNatIList#(X), mark#(isNatList(X)) -> a__isNatList#(X), mark#(isNat(X)) -> a__isNat#(X), mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), mark#(U21(X)) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4), a__U31#(tt(), IL, M, N) -> mark#(N), 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__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__isNatList#(take(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), a__take#(0(), IL) -> a__isNatIList#(IL), a__take#(s(M), cons(N, IL)) -> a__U31#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N), a__take#(s(M), cons(N, IL)) -> a__and#(a__isNatIList(IL), and(isNat(M), isNat(N))), a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL)} Scc: {a__length#(cons(N, L)) -> a__U11#(a__and(a__isNatList(L), isNat(N)), L), a__U11#(tt(), L) -> a__length#(mark(L))} SCC: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(take(X1, X2)) -> mark#(X1), mark#(take(X1, X2)) -> mark#(X2), mark#(take(X1, X2)) -> a__take#(mark(X1), mark(X2)), mark#(isNatIList(X)) -> a__isNatIList#(X), mark#(isNatList(X)) -> a__isNatList#(X), mark#(isNat(X)) -> a__isNat#(X), mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), mark#(U21(X)) -> mark#(X), mark#(U31(X1, X2, X3, X4)) -> mark#(X1), mark#(U31(X1, X2, X3, X4)) -> a__U31#(mark(X1), X2, X3, X4), a__U31#(tt(), IL, M, N) -> mark#(N), 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__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__isNatList#(take(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), a__take#(0(), IL) -> a__isNatIList#(IL), a__take#(s(M), cons(N, IL)) -> a__U31#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N), a__take#(s(M), cons(N, IL)) -> a__and#(a__isNatIList(IL), and(isNat(M), isNat(N))), a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL)} 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(nil()) -> nil(), mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)), mark(length(X)) -> a__length(mark(X)), mark(isNatIList(X)) -> a__isNatIList(X), mark(isNatList(X)) -> a__isNatList(X), mark(isNat(X)) -> a__isNat(X), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(U11(X1, X2)) -> a__U11(mark(X1), X2), mark(U21(X)) -> a__U21(mark(X)), mark(U31(X1, X2, X3, X4)) -> a__U31(mark(X1), X2, X3, X4), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), L) -> s(a__length(mark(L))), a__U21(X) -> U21(X), a__U21(tt()) -> nil(), a__U31(X1, X2, X3, X4) -> U31(X1, X2, X3, X4), a__U31(tt(), IL, M, N) -> cons(mark(N), take(M, IL)), 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__isNatList(take(V1, V2)) -> a__and(a__isNat(V1), isNatIList(V2)), 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(), a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U21(a__isNatIList(IL)), a__take(s(M), cons(N, IL)) -> a__U31(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)} POLY: Argument Filtering: pi(U31) = [0,3], pi(U21) = [0], pi(U11) = [], pi(and) = [0,1], pi(a__take#) = [1], pi(a__take) = [0,1], pi(isNat) = [], pi(isNatList) = [], pi(isNatIList) = [], pi(a__isNatIList#) = [], pi(a__isNatIList) = [], pi(length) = [], pi(a__isNatList#) = [], pi(a__isNatList) = [], pi(a__isNat#) = [], pi(a__isNat) = [], pi(a__and#) = [1], pi(a__and) = [0,1], pi(a__U31#) = [3], pi(a__U31) = [0,3], pi(take) = [0,1], pi(a__U21) = [0], pi(nil) = [], pi(tt) = [], pi(a__U11) = [], pi(mark#) = [0], pi(mark) = 0, pi(a__length) = [], pi(s) = 0, pi(a__zeros) = [], pi(zeros) = [], pi(0) = [], pi(cons) = 0 Usable Rules: {} Interpretation: [a__U31#](x0) = x0 + 1, [a__take#](x0) = x0 + 1, [a__and#](x0) = x0 + 1, [a__isNatIList#] = 1, [a__isNatList#] = 1, [a__isNat#] = 1, [mark#](x0) = x0 + 1, [U31](x0, x1) = x0 + x1 + 1, [and](x0, x1) = x0 + x1, [take](x0, x1) = x0 + x1 + 1, [U21](x0) = x0 + 1, [isNat] = 0, [isNatList] = 0, [isNatIList] = 0 Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X), mark#(isNatList(X)) -> a__isNatList#(X), mark#(isNat(X)) -> a__isNat#(X), mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__U31#(tt(), IL, M, N) -> mark#(N), 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__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__isNatList#(take(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), a__take#(0(), IL) -> a__isNatIList#(IL), a__take#(s(M), cons(N, IL)) -> a__U31#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N), a__take#(s(M), cons(N, IL)) -> a__and#(a__isNatIList(IL), and(isNat(M), isNat(N))), a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL)} 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(nil()) -> nil(), mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)), mark(length(X)) -> a__length(mark(X)), mark(isNatIList(X)) -> a__isNatIList(X), mark(isNatList(X)) -> a__isNatList(X), mark(isNat(X)) -> a__isNat(X), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(U11(X1, X2)) -> a__U11(mark(X1), X2), mark(U21(X)) -> a__U21(mark(X)), mark(U31(X1, X2, X3, X4)) -> a__U31(mark(X1), X2, X3, X4), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), L) -> s(a__length(mark(L))), a__U21(X) -> U21(X), a__U21(tt()) -> nil(), a__U31(X1, X2, X3, X4) -> U31(X1, X2, X3, X4), a__U31(tt(), IL, M, N) -> cons(mark(N), take(M, IL)), 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__isNatList(take(V1, V2)) -> a__and(a__isNat(V1), isNatIList(V2)), 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(), a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U21(a__isNatIList(IL)), a__take(s(M), cons(N, IL)) -> a__U31(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)} EDG: {(a__take#(0(), IL) -> a__isNatIList#(IL), a__isNatIList#(cons(V1, V2)) -> a__isNat#(V1)) (a__take#(0(), IL) -> a__isNatIList#(IL), a__isNatIList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (a__take#(0(), IL) -> a__isNatIList#(IL), a__isNatIList#(V) -> a__isNatList#(V)) (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#(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#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(V1, V2)) -> a__isNat#(V1)) (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(V1, V2)) -> a__isNat#(V1)) (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatList(V2))) (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#(isNat(X)) -> a__isNat#(X)) (a__and#(tt(), X) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X)) (a__and#(tt(), X) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X)) (a__and#(tt(), X) -> mark#(X), mark#(s(X)) -> mark#(X)) (a__and#(tt(), X) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (a__isNat#(length(V1)) -> a__isNatList#(V1), a__isNatList#(take(V1, V2)) -> a__isNat#(V1)) (a__isNat#(length(V1)) -> a__isNatList#(V1), a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (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__isNatList#(take(V1, V2)) -> a__isNat#(V1), a__isNat#(length(V1)) -> a__isNatList#(V1)) (a__isNatList#(take(V1, V2)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1)) (a__isNatIList#(V) -> a__isNatList#(V), a__isNatList#(take(V1, V2)) -> a__isNat#(V1)) (a__isNatIList#(V) -> a__isNatList#(V), a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (a__isNatIList#(V) -> a__isNatList#(V), a__isNatList#(cons(V1, V2)) -> a__isNat#(V1)) (a__isNatIList#(V) -> a__isNatList#(V), a__isNatList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatList(V2))) (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#(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#(s(X)) -> mark#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__and#(tt(), X) -> mark#(X)) (a__take#(s(M), cons(N, IL)) -> a__and#(a__isNatIList(IL), and(isNat(M), isNat(N))), a__and#(tt(), X) -> mark#(X)) (a__take#(s(M), cons(N, IL)) -> a__U31#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N), a__U31#(tt(), IL, M, N) -> mark#(N)) (mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__and#(tt(), X) -> mark#(X)) (a__isNatIList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__and#(tt(), X) -> mark#(X)) (a__isNatList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatList(V2)), a__and#(tt(), X) -> 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#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a__isNatIList#(cons(V1, V2)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1)) (a__isNatIList#(cons(V1, V2)) -> a__isNat#(V1), a__isNat#(length(V1)) -> a__isNatList#(V1)) (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#(isNat(X)) -> a__isNat#(X), a__isNat#(s(V1)) -> a__isNat#(V1)) (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(length(V1)) -> a__isNatList#(V1)) (mark#(isNatIList(X)) -> a__isNatIList#(X), a__isNatIList#(V) -> a__isNatList#(V)) (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#(cons(V1, V2)) -> a__isNat#(V1)) (a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(V) -> a__isNatList#(V)) (a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (a__take#(s(M), cons(N, IL)) -> a__isNatIList#(IL), a__isNatIList#(cons(V1, V2)) -> a__isNat#(V1)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(cons(X1, X2)) -> mark#(X1)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(s(X)) -> mark#(X)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(isNatIList(X)) -> a__isNatIList#(X)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(isNatList(X)) -> a__isNatList#(X)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1)) (a__U31#(tt(), IL, M, N) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))} SCCS: Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X), mark#(isNatList(X)) -> a__isNatList#(X), mark#(isNat(X)) -> a__isNat#(X), mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), 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__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__isNatList#(take(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: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X), mark#(isNatList(X)) -> a__isNatList#(X), mark#(isNat(X)) -> a__isNat#(X), mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), 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__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__isNatList#(take(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(nil()) -> nil(), mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)), mark(length(X)) -> a__length(mark(X)), mark(isNatIList(X)) -> a__isNatIList(X), mark(isNatList(X)) -> a__isNatList(X), mark(isNat(X)) -> a__isNat(X), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(U11(X1, X2)) -> a__U11(mark(X1), X2), mark(U21(X)) -> a__U21(mark(X)), mark(U31(X1, X2, X3, X4)) -> a__U31(mark(X1), X2, X3, X4), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), L) -> s(a__length(mark(L))), a__U21(X) -> U21(X), a__U21(tt()) -> nil(), a__U31(X1, X2, X3, X4) -> U31(X1, X2, X3, X4), a__U31(tt(), IL, M, N) -> cons(mark(N), take(M, IL)), 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__isNatList(take(V1, V2)) -> a__and(a__isNat(V1), isNatIList(V2)), 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(), a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U21(a__isNatIList(IL)), a__take(s(M), cons(N, IL)) -> a__U31(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)} POLY: Argument Filtering: pi(U31) = [], pi(U21) = [], pi(U11) = [], pi(and) = [0,1], pi(a__take) = [], pi(isNat) = [], pi(isNatList) = [], pi(isNatIList) = [], pi(a__isNatIList#) = [], pi(a__isNatIList) = [], pi(length) = [], pi(a__isNatList#) = [], pi(a__isNatList) = [], pi(a__isNat#) = [], pi(a__isNat) = [], pi(a__and#) = 1, pi(a__and) = [], pi(a__U31) = [], pi(take) = [], pi(a__U21) = [], pi(nil) = [], pi(tt) = [], pi(a__U11) = [], pi(mark#) = 0, pi(mark) = [], pi(a__length) = [], pi(s) = 0, pi(a__zeros) = [], pi(zeros) = [], pi(0) = [], pi(cons) = 0 Usable Rules: {} Interpretation: [a__isNatIList#] = 0, [a__isNatList#] = 0, [a__isNat#] = 0, [and](x0, x1) = x0 + x1 + 1, [isNat] = 1, [isNatList] = 0, [isNatIList] = 0 Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X), mark#(isNatList(X)) -> a__isNatList#(X), 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__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__isNatList#(take(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(nil()) -> nil(), mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)), mark(length(X)) -> a__length(mark(X)), mark(isNatIList(X)) -> a__isNatIList(X), mark(isNatList(X)) -> a__isNatList(X), mark(isNat(X)) -> a__isNat(X), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(U11(X1, X2)) -> a__U11(mark(X1), X2), mark(U21(X)) -> a__U21(mark(X)), mark(U31(X1, X2, X3, X4)) -> a__U31(mark(X1), X2, X3, X4), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), L) -> s(a__length(mark(L))), a__U21(X) -> U21(X), a__U21(tt()) -> nil(), a__U31(X1, X2, X3, X4) -> U31(X1, X2, X3, X4), a__U31(tt(), IL, M, N) -> cons(mark(N), take(M, IL)), 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__isNatList(take(V1, V2)) -> a__and(a__isNat(V1), isNatIList(V2)), 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(), a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U21(a__isNatIList(IL)), a__take(s(M), cons(N, IL)) -> a__U31(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)} EDG: {(a__isNatIList#(V) -> a__isNatList#(V), a__isNatList#(take(V1, V2)) -> a__isNat#(V1)) (a__isNatIList#(V) -> a__isNatList#(V), a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (a__isNatIList#(V) -> a__isNatList#(V), a__isNatList#(cons(V1, V2)) -> a__isNat#(V1)) (a__isNatIList#(V) -> a__isNatList#(V), a__isNatList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatList(V2))) (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)) (a__and#(tt(), X) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X)) (a__and#(tt(), X) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X)) (a__and#(tt(), X) -> mark#(X), mark#(s(X)) -> mark#(X)) (a__and#(tt(), X) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (a__isNat#(length(V1)) -> a__isNatList#(V1), a__isNatList#(take(V1, V2)) -> a__isNat#(V1)) (a__isNat#(length(V1)) -> a__isNatList#(V1), a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (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__isNatList#(cons(V1, V2)) -> a__isNat#(V1), a__isNat#(length(V1)) -> a__isNatList#(V1)) (a__isNatList#(cons(V1, V2)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1)) (a__isNatList#(take(V1, V2)) -> a__isNat#(V1), a__isNat#(length(V1)) -> a__isNatList#(V1)) (a__isNatList#(take(V1, V2)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1)) (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)) (a__isNatIList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__and#(tt(), X) -> mark#(X)) (a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__and#(tt(), X) -> mark#(X)) (a__isNatList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatList(V2)), a__and#(tt(), X) -> mark#(X)) (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#(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#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(V1, V2)) -> a__isNat#(V1)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(s(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(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#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(isNatList(X)) -> a__isNatList#(X))} SCCS: Scc: { mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X), mark#(isNatList(X)) -> a__isNatList#(X), 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__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__isNatList#(take(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: Strict: { mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X), mark#(isNatList(X)) -> a__isNatList#(X), 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__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__isNatList#(take(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(nil()) -> nil(), mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)), mark(length(X)) -> a__length(mark(X)), mark(isNatIList(X)) -> a__isNatIList(X), mark(isNatList(X)) -> a__isNatList(X), mark(isNat(X)) -> a__isNat(X), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(U11(X1, X2)) -> a__U11(mark(X1), X2), mark(U21(X)) -> a__U21(mark(X)), mark(U31(X1, X2, X3, X4)) -> a__U31(mark(X1), X2, X3, X4), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), L) -> s(a__length(mark(L))), a__U21(X) -> U21(X), a__U21(tt()) -> nil(), a__U31(X1, X2, X3, X4) -> U31(X1, X2, X3, X4), a__U31(tt(), IL, M, N) -> cons(mark(N), take(M, IL)), 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__isNatList(take(V1, V2)) -> a__and(a__isNat(V1), isNatIList(V2)), 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(), a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U21(a__isNatIList(IL)), a__take(s(M), cons(N, IL)) -> a__U31(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)} POLY: Argument Filtering: pi(U31) = [], pi(U21) = [], pi(U11) = [], pi(and) = [], pi(a__take) = [], pi(isNat) = [], pi(isNatList) = [], pi(isNatIList) = [], pi(a__isNatIList#) = [], pi(a__isNatIList) = [], pi(length) = [], pi(a__isNatList#) = [], pi(a__isNatList) = [], pi(a__isNat#) = [], pi(a__isNat) = [], pi(a__and#) = 1, pi(a__and) = [], pi(a__U31) = [], pi(take) = [], pi(a__U21) = [], pi(nil) = [], pi(tt) = [], pi(a__U11) = [], pi(mark#) = 0, pi(mark) = [], pi(a__length) = [], pi(s) = 0, pi(a__zeros) = [], pi(zeros) = [], pi(0) = [], pi(cons) = [0] Usable Rules: {} Interpretation: [a__isNatIList#] = 0, [a__isNatList#] = 0, [a__isNat#] = 0, [cons](x0) = x0 + 1, [isNatList] = 0, [isNatIList] = 0 Strict: { mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X), mark#(isNatList(X)) -> a__isNatList#(X), 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__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__isNatList#(take(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(nil()) -> nil(), mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)), mark(length(X)) -> a__length(mark(X)), mark(isNatIList(X)) -> a__isNatIList(X), mark(isNatList(X)) -> a__isNatList(X), mark(isNat(X)) -> a__isNat(X), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(U11(X1, X2)) -> a__U11(mark(X1), X2), mark(U21(X)) -> a__U21(mark(X)), mark(U31(X1, X2, X3, X4)) -> a__U31(mark(X1), X2, X3, X4), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), L) -> s(a__length(mark(L))), a__U21(X) -> U21(X), a__U21(tt()) -> nil(), a__U31(X1, X2, X3, X4) -> U31(X1, X2, X3, X4), a__U31(tt(), IL, M, N) -> cons(mark(N), take(M, IL)), 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__isNatList(take(V1, V2)) -> a__and(a__isNat(V1), isNatIList(V2)), 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(), a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U21(a__isNatIList(IL)), a__take(s(M), cons(N, IL)) -> a__U31(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)} EDG: {(a__isNatList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatList(V2)), a__and#(tt(), X) -> mark#(X)) (a__isNatIList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__and#(tt(), X) -> mark#(X)) (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)) (a__and#(tt(), X) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X)) (a__and#(tt(), X) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X)) (a__and#(tt(), X) -> mark#(X), mark#(s(X)) -> mark#(X)) (a__isNat#(length(V1)) -> a__isNatList#(V1), a__isNatList#(take(V1, V2)) -> a__isNat#(V1)) (a__isNat#(length(V1)) -> a__isNatList#(V1), a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (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__isNatList#(take(V1, V2)) -> a__isNat#(V1), a__isNat#(length(V1)) -> a__isNatList#(V1)) (a__isNatList#(take(V1, V2)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1)) (a__isNatIList#(cons(V1, V2)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1)) (a__isNatIList#(cons(V1, V2)) -> a__isNat#(V1), a__isNat#(length(V1)) -> a__isNatList#(V1)) (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#(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#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (mark#(isNatList(X)) -> a__isNatList#(X), a__isNatList#(take(V1, V2)) -> a__isNat#(V1)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X)) (mark#(s(X)) -> mark#(X), mark#(isNatList(X)) -> a__isNatList#(X)) (a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__and#(tt(), X) -> mark#(X)) (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__isNatIList#(V) -> a__isNatList#(V), a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (a__isNatIList#(V) -> a__isNatList#(V), a__isNatList#(take(V1, V2)) -> a__isNat#(V1))} SCCS: Scc: { mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X), mark#(isNatList(X)) -> a__isNatList#(X), 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__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__isNatList#(take(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: Strict: { mark#(s(X)) -> mark#(X), mark#(isNatIList(X)) -> a__isNatIList#(X), mark#(isNatList(X)) -> a__isNatList#(X), 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__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__isNatList#(take(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(nil()) -> nil(), mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)), mark(length(X)) -> a__length(mark(X)), mark(isNatIList(X)) -> a__isNatIList(X), mark(isNatList(X)) -> a__isNatList(X), mark(isNat(X)) -> a__isNat(X), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(U11(X1, X2)) -> a__U11(mark(X1), X2), mark(U21(X)) -> a__U21(mark(X)), mark(U31(X1, X2, X3, X4)) -> a__U31(mark(X1), X2, X3, X4), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), L) -> s(a__length(mark(L))), a__U21(X) -> U21(X), a__U21(tt()) -> nil(), a__U31(X1, X2, X3, X4) -> U31(X1, X2, X3, X4), a__U31(tt(), IL, M, N) -> cons(mark(N), take(M, IL)), 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__isNatList(take(V1, V2)) -> a__and(a__isNat(V1), isNatIList(V2)), 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(), a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U21(a__isNatIList(IL)), a__take(s(M), cons(N, IL)) -> a__U31(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)} POLY: Argument Filtering: pi(U31) = [], pi(U21) = [], pi(U11) = [], pi(and) = [], pi(a__take) = [], pi(isNat) = [], pi(isNatList) = [0], pi(isNatIList) = [0], pi(a__isNatIList#) = [0], pi(a__isNatIList) = [], pi(length) = [0], pi(a__isNatList#) = [0], pi(a__isNatList) = [], pi(a__isNat#) = [0], pi(a__isNat) = [], pi(a__and#) = [1], pi(a__and) = [], pi(a__U31) = [], pi(take) = [0,1], pi(a__U21) = [], pi(nil) = [], pi(tt) = [], pi(a__U11) = [], pi(mark#) = [0], pi(mark) = [], pi(a__length) = [], pi(s) = [0], pi(a__zeros) = [], pi(zeros) = [], pi(0) = [], pi(cons) = [0,1] Usable Rules: {} Interpretation: [a__and#](x0) = x0 + 1, [a__isNatIList#](x0) = x0 + 1, [a__isNatList#](x0) = x0 + 1, [a__isNat#](x0) = x0 + 1, [mark#](x0) = x0 + 1, [take](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = x0 + x1 + 1, [isNatList](x0) = x0 + 1, [isNatIList](x0) = x0 + 1, [length](x0) = x0 + 1, [s](x0) = x0 + 1 Strict: { a__and#(tt(), X) -> mark#(X), a__isNatList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatList(V2)), a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__isNatIList#(V) -> a__isNatList#(V), a__isNatIList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))} 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(nil()) -> nil(), mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)), mark(length(X)) -> a__length(mark(X)), mark(isNatIList(X)) -> a__isNatIList(X), mark(isNatList(X)) -> a__isNatList(X), mark(isNat(X)) -> a__isNat(X), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(U11(X1, X2)) -> a__U11(mark(X1), X2), mark(U21(X)) -> a__U21(mark(X)), mark(U31(X1, X2, X3, X4)) -> a__U31(mark(X1), X2, X3, X4), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), L) -> s(a__length(mark(L))), a__U21(X) -> U21(X), a__U21(tt()) -> nil(), a__U31(X1, X2, X3, X4) -> U31(X1, X2, X3, X4), a__U31(tt(), IL, M, N) -> cons(mark(N), take(M, IL)), 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__isNatList(take(V1, V2)) -> a__and(a__isNat(V1), isNatIList(V2)), 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(), a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U21(a__isNatIList(IL)), a__take(s(M), cons(N, IL)) -> a__U31(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)} EDG: {(a__isNatList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatList(V2)), a__and#(tt(), X) -> mark#(X)) (a__isNatIList#(cons(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__and#(tt(), X) -> mark#(X)) (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#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2))) (a__isNatList#(take(V1, V2)) -> a__and#(a__isNat(V1), isNatIList(V2)), a__and#(tt(), X) -> mark#(X))} SCCS: Qed SCC: Strict: {a__length#(cons(N, L)) -> a__U11#(a__and(a__isNatList(L), isNat(N)), L), a__U11#(tt(), L) -> a__length#(mark(L))} 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(nil()) -> nil(), mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)), mark(length(X)) -> a__length(mark(X)), mark(isNatIList(X)) -> a__isNatIList(X), mark(isNatList(X)) -> a__isNatList(X), mark(isNat(X)) -> a__isNat(X), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(U11(X1, X2)) -> a__U11(mark(X1), X2), mark(U21(X)) -> a__U21(mark(X)), mark(U31(X1, X2, X3, X4)) -> a__U31(mark(X1), X2, X3, X4), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), L) -> s(a__length(mark(L))), a__U21(X) -> U21(X), a__U21(tt()) -> nil(), a__U31(X1, X2, X3, X4) -> U31(X1, X2, X3, X4), a__U31(tt(), IL, M, N) -> cons(mark(N), take(M, IL)), 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__isNatList(take(V1, V2)) -> a__and(a__isNat(V1), isNatIList(V2)), 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(), a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U21(a__isNatIList(IL)), a__take(s(M), cons(N, IL)) -> a__U31(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))), IL, M, N)} Fail