MAYBE TRS: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length(nil()) -> 0(), activate(X) -> X, activate(n__zeros()) -> zeros(), activate(n__take(X1, X2)) -> take(X1, X2), activate(n__0()) -> 0(), activate(n__length(X)) -> length(X), activate(n__s(X)) -> s(X), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(X1, X2), U11(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U21(tt()) -> nil(), U31(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> isNatList(activate(V1)), isNat(n__s(V1)) -> isNat(activate(V1)), isNatList(X) -> n__isNatList(X), isNatList(n__take(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList(n__nil()) -> tt(), isNatIList(X) -> n__isNatIList(X), isNatIList(V) -> isNatList(activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U21(isNatIList(IL)), take(s(M), cons(N, IL)) -> U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)} DP: Strict: { zeros#() -> cons#(0(), n__zeros()), zeros#() -> 0#(), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N)), length#(cons(N, L)) -> isNatList#(activate(L)), length#(nil()) -> 0#(), activate#(n__zeros()) -> zeros#(), activate#(n__take(X1, X2)) -> take#(X1, X2), activate#(n__0()) -> 0#(), activate#(n__length(X)) -> length#(X), activate#(n__s(X)) -> s#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__cons(X1, X2)) -> cons#(X1, X2), activate#(n__nil()) -> nil#(), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), U11#(tt(), L) -> s#(length(activate(L))), U11#(tt(), L) -> length#(activate(L)), U11#(tt(), L) -> activate#(L), U21#(tt()) -> nil#(), U31#(tt(), IL, M, N) -> cons#(activate(N), n__take(activate(M), activate(IL))), U31#(tt(), IL, M, N) -> activate#(N), U31#(tt(), IL, M, N) -> activate#(M), U31#(tt(), IL, M, N) -> activate#(IL), and#(tt(), X) -> activate#(X), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNatList#(n__take(V1, V2)) -> activate#(V1), isNatList#(n__take(V1, V2)) -> activate#(V2), isNatList#(n__take(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNatIList#(V) -> activate#(V), isNatIList#(V) -> isNatList#(activate(V)), isNatIList#(n__cons(V1, V2)) -> activate#(V1), isNatIList#(n__cons(V1, V2)) -> activate#(V2), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), take#(0(), IL) -> U21#(isNatIList(IL)), take#(0(), IL) -> isNatIList#(IL), take#(s(M), cons(N, IL)) -> activate#(IL), take#(s(M), cons(N, IL)) -> U31#(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N), take#(s(M), cons(N, IL)) -> and#(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), take#(s(M), cons(N, IL)) -> isNat#(M), take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length(nil()) -> 0(), activate(X) -> X, activate(n__zeros()) -> zeros(), activate(n__take(X1, X2)) -> take(X1, X2), activate(n__0()) -> 0(), activate(n__length(X)) -> length(X), activate(n__s(X)) -> s(X), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(X1, X2), U11(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U21(tt()) -> nil(), U31(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> isNatList(activate(V1)), isNat(n__s(V1)) -> isNat(activate(V1)), isNatList(X) -> n__isNatList(X), isNatList(n__take(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList(n__nil()) -> tt(), isNatIList(X) -> n__isNatIList(X), isNatIList(V) -> isNatList(activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U21(isNatIList(IL)), take(s(M), cons(N, IL)) -> U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)} EDG: { (isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), and#(tt(), X) -> activate#(X)) (isNatIList#(V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatIList#(V) -> activate#(V), activate#(n__isNat(X)) -> isNat#(X)) (isNatIList#(V) -> activate#(V), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatIList#(V) -> activate#(V), activate#(n__nil()) -> nil#()) (isNatIList#(V) -> activate#(V), activate#(n__cons(X1, X2)) -> cons#(X1, X2)) (isNatIList#(V) -> activate#(V), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatIList#(V) -> activate#(V), activate#(n__s(X)) -> s#(X)) (isNatIList#(V) -> activate#(V), activate#(n__length(X)) -> length#(X)) (isNatIList#(V) -> activate#(V), activate#(n__0()) -> 0#()) (isNatIList#(V) -> activate#(V), activate#(n__take(X1, X2)) -> take#(X1, X2)) (isNatIList#(V) -> activate#(V), activate#(n__zeros()) -> zeros#()) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__isNat(X)) -> isNat#(X)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__isNatList(X)) -> isNatList#(X)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__nil()) -> nil#()) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__cons(X1, X2)) -> cons#(X1, X2)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__isNatIList(X)) -> isNatIList#(X)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__s(X)) -> s#(X)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> length#(X)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__0()) -> 0#()) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> take#(X1, X2)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__zeros()) -> zeros#()) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__isNatList(X)) -> isNatList#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__nil()) -> nil#()) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(X1, X2)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(X1, X2)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#()) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(X1, X2)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(X1, X2)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#()) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(X1, X2)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(X1, X2)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (U11#(tt(), L) -> activate#(L), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U11#(tt(), L) -> activate#(L), activate#(n__isNat(X)) -> isNat#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__isNatList(X)) -> isNatList#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__nil()) -> nil#()) (U11#(tt(), L) -> activate#(L), activate#(n__cons(X1, X2)) -> cons#(X1, X2)) (U11#(tt(), L) -> activate#(L), activate#(n__isNatIList(X)) -> isNatIList#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__s(X)) -> s#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__length(X)) -> length#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__0()) -> 0#()) (U11#(tt(), L) -> activate#(L), activate#(n__take(X1, X2)) -> take#(X1, X2)) (U11#(tt(), L) -> activate#(L), activate#(n__zeros()) -> zeros#()) (length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N)), and#(tt(), X) -> activate#(X)) (activate#(n__zeros()) -> zeros#(), zeros#() -> 0#()) (activate#(n__zeros()) -> zeros#(), zeros#() -> cons#(0(), n__zeros())) (activate#(n__length(X)) -> length#(X), length#(nil()) -> 0#()) (activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> isNatList#(activate(L))) (activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N))) (activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L))) (activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> activate#(L)) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(n__cons(V1, V2)) -> activate#(V2)) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(n__cons(V1, V2)) -> activate#(V1)) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(V) -> isNatList#(activate(V))) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(V) -> activate#(V)) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2)))) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1))) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__take(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__take(V1, V2)) -> activate#(V2)) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__take(V1, V2)) -> activate#(V1)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__isNat(X)) -> isNat#(X)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__isNatList(X)) -> isNatList#(X)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__nil()) -> nil#()) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__cons(X1, X2)) -> cons#(X1, X2)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__isNatIList(X)) -> isNatIList#(X)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__s(X)) -> s#(X)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> length#(X)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__0()) -> 0#()) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(X1, X2)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__zeros()) -> zeros#()) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__and(X1, X2)) -> and#(X1, X2)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__isNat(X)) -> isNat#(X)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__isNatList(X)) -> isNatList#(X)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__nil()) -> nil#()) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__cons(X1, X2)) -> cons#(X1, X2)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__isNatIList(X)) -> isNatIList#(X)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__s(X)) -> s#(X)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__length(X)) -> length#(X)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__0()) -> 0#()) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(X1, X2)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__zeros()) -> zeros#()) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#()) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(X1, X2)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(X1, X2)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__zeros()) -> zeros#()) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#()) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(X1, X2)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(X1, X2)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__zeros()) -> zeros#()) (take#(s(M), cons(N, IL)) -> isNat#(M), isNat#(n__s(V1)) -> isNat#(activate(V1))) (take#(s(M), cons(N, IL)) -> isNat#(M), isNat#(n__s(V1)) -> activate#(V1)) (take#(s(M), cons(N, IL)) -> isNat#(M), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (take#(s(M), cons(N, IL)) -> isNat#(M), isNat#(n__length(V1)) -> activate#(V1)) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2)))) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1))) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__take(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__take(V1, V2)) -> activate#(V2)) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__take(V1, V2)) -> activate#(V1)) (isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> activate#(V2)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> activate#(V1)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(V) -> isNatList#(activate(V))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(V) -> activate#(V)) (U11#(tt(), L) -> length#(activate(L)), length#(nil()) -> 0#()) (U11#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L))) (U11#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N))) (U11#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L))) (U11#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> activate#(L)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(V1, V2)) -> activate#(V1)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(V1, V2)) -> activate#(V2)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2)))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (take#(0(), IL) -> U21#(isNatIList(IL)), U21#(tt()) -> nil#()) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__take(V1, V2)) -> activate#(V1)) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__take(V1, V2)) -> activate#(V2)) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__take(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1))) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2)))) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__zeros()) -> zeros#()) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> take#(X1, X2)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__0()) -> 0#()) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> length#(X)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__s(X)) -> s#(X)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__isNatIList(X)) -> isNatIList#(X)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__cons(X1, X2)) -> cons#(X1, X2)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__nil()) -> nil#()) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__isNatList(X)) -> isNatList#(X)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__isNat(X)) -> isNat#(X)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__zeros()) -> zeros#()) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(X1, X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(X1, X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#()) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (take#(s(M), cons(N, IL)) -> and#(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), and#(tt(), X) -> activate#(X)) (take#(s(M), cons(N, IL)) -> U31#(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N), U31#(tt(), IL, M, N) -> cons#(activate(N), n__take(activate(M), activate(IL)))) (take#(s(M), cons(N, IL)) -> U31#(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N), U31#(tt(), IL, M, N) -> activate#(N)) (take#(s(M), cons(N, IL)) -> U31#(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N), U31#(tt(), IL, M, N) -> activate#(M)) (take#(s(M), cons(N, IL)) -> U31#(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N), U31#(tt(), IL, M, N) -> activate#(IL)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(V) -> activate#(V)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(V) -> isNatList#(activate(V))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> activate#(V1)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> activate#(V2)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (and#(tt(), X) -> activate#(X), activate#(n__zeros()) -> zeros#()) (and#(tt(), X) -> activate#(X), activate#(n__take(X1, X2)) -> take#(X1, X2)) (and#(tt(), X) -> activate#(X), activate#(n__0()) -> 0#()) (and#(tt(), X) -> activate#(X), activate#(n__length(X)) -> length#(X)) (and#(tt(), X) -> activate#(X), activate#(n__s(X)) -> s#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__cons(X1, X2)) -> cons#(X1, X2)) (and#(tt(), X) -> activate#(X), activate#(n__nil()) -> nil#()) (and#(tt(), X) -> activate#(X), activate#(n__isNatList(X)) -> isNatList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(X1, X2)) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__length(V1)) -> activate#(V1)) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> activate#(V1)) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> isNat#(activate(V1))) (activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X)) (activate#(n__take(X1, X2)) -> take#(X1, X2), take#(0(), IL) -> U21#(isNatIList(IL))) (activate#(n__take(X1, X2)) -> take#(X1, X2), take#(0(), IL) -> isNatIList#(IL)) (activate#(n__take(X1, X2)) -> take#(X1, X2), take#(s(M), cons(N, IL)) -> activate#(IL)) (activate#(n__take(X1, X2)) -> take#(X1, X2), take#(s(M), cons(N, IL)) -> U31#(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)) (activate#(n__take(X1, X2)) -> take#(X1, X2), take#(s(M), cons(N, IL)) -> and#(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N)))) (activate#(n__take(X1, X2)) -> take#(X1, X2), take#(s(M), cons(N, IL)) -> isNat#(M)) (activate#(n__take(X1, X2)) -> take#(X1, X2), take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL))) (length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), U11#(tt(), L) -> s#(length(activate(L)))) (length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), U11#(tt(), L) -> length#(activate(L))) (length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), U11#(tt(), L) -> activate#(L)) (length#(cons(N, L)) -> activate#(L), activate#(n__zeros()) -> zeros#()) (length#(cons(N, L)) -> activate#(L), activate#(n__take(X1, X2)) -> take#(X1, X2)) (length#(cons(N, L)) -> activate#(L), activate#(n__0()) -> 0#()) (length#(cons(N, L)) -> activate#(L), activate#(n__length(X)) -> length#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__s(X)) -> s#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__isNatIList(X)) -> isNatIList#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__cons(X1, X2)) -> cons#(X1, X2)) (length#(cons(N, L)) -> activate#(L), activate#(n__nil()) -> nil#()) (length#(cons(N, L)) -> activate#(L), activate#(n__isNatList(X)) -> isNatList#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__isNat(X)) -> isNat#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(X1, X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(X1, X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#()) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(X1, X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(X1, X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__nil()) -> nil#()) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatList(X)) -> isNatList#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), and#(tt(), X) -> activate#(X)) (isNatList#(n__take(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), and#(tt(), X) -> activate#(X)) } SCCS: Scc: { length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N)), length#(cons(N, L)) -> isNatList#(activate(L)), activate#(n__take(X1, X2)) -> take#(X1, X2), activate#(n__length(X)) -> length#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), U11#(tt(), L) -> length#(activate(L)), U11#(tt(), L) -> activate#(L), U31#(tt(), IL, M, N) -> activate#(N), U31#(tt(), IL, M, N) -> activate#(M), U31#(tt(), IL, M, N) -> activate#(IL), and#(tt(), X) -> activate#(X), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNatList#(n__take(V1, V2)) -> activate#(V1), isNatList#(n__take(V1, V2)) -> activate#(V2), isNatList#(n__take(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNatIList#(V) -> activate#(V), isNatIList#(V) -> isNatList#(activate(V)), isNatIList#(n__cons(V1, V2)) -> activate#(V1), isNatIList#(n__cons(V1, V2)) -> activate#(V2), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), take#(0(), IL) -> isNatIList#(IL), take#(s(M), cons(N, IL)) -> activate#(IL), take#(s(M), cons(N, IL)) -> U31#(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N), take#(s(M), cons(N, IL)) -> and#(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), take#(s(M), cons(N, IL)) -> isNat#(M), take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL))} SCC: Strict: { length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N)), length#(cons(N, L)) -> isNatList#(activate(L)), activate#(n__take(X1, X2)) -> take#(X1, X2), activate#(n__length(X)) -> length#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), U11#(tt(), L) -> length#(activate(L)), U11#(tt(), L) -> activate#(L), U31#(tt(), IL, M, N) -> activate#(N), U31#(tt(), IL, M, N) -> activate#(M), U31#(tt(), IL, M, N) -> activate#(IL), and#(tt(), X) -> activate#(X), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNatList#(n__take(V1, V2)) -> activate#(V1), isNatList#(n__take(V1, V2)) -> activate#(V2), isNatList#(n__take(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNatIList#(V) -> activate#(V), isNatIList#(V) -> isNatList#(activate(V)), isNatIList#(n__cons(V1, V2)) -> activate#(V1), isNatIList#(n__cons(V1, V2)) -> activate#(V2), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), take#(0(), IL) -> isNatIList#(IL), take#(s(M), cons(N, IL)) -> activate#(IL), take#(s(M), cons(N, IL)) -> U31#(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N), take#(s(M), cons(N, IL)) -> and#(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), take#(s(M), cons(N, IL)) -> isNat#(M), take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length(nil()) -> 0(), activate(X) -> X, activate(n__zeros()) -> zeros(), activate(n__take(X1, X2)) -> take(X1, X2), activate(n__0()) -> 0(), activate(n__length(X)) -> length(X), activate(n__s(X)) -> s(X), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(X1, X2), U11(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U21(tt()) -> nil(), U31(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> isNatList(activate(V1)), isNat(n__s(V1)) -> isNat(activate(V1)), isNatList(X) -> n__isNatList(X), isNatList(n__take(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList(n__nil()) -> tt(), isNatIList(X) -> n__isNatIList(X), isNatIList(V) -> isNatList(activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U21(isNatIList(IL)), take(s(M), cons(N, IL)) -> U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)} POLY: Argument Filtering: pi(n__and) = 1, pi(take#) = [0,1], pi(take) = [0,1], pi(n__isNat) = 0, pi(n__isNatList) = 0, pi(n__nil) = [], pi(n__cons) = [0,1], pi(n__isNatIList) = 0, pi(isNatIList#) = 0, pi(isNatIList) = 0, pi(n__s) = 0, pi(n__length) = 0, pi(isNatList#) = 0, pi(isNatList) = 0, pi(n__0) = [], pi(isNat#) = 0, pi(isNat) = 0, pi(and#) = 1, pi(and) = 1, pi(U31#) = [1,2,3], pi(U31) = [1,2,3], pi(n__take) = [0,1], pi(U21) = [], pi(nil) = [], pi(tt) = [], pi(U11#) = 1, pi(U11) = 1, pi(activate#) = 0, pi(activate) = 0, pi(length#) = 0, pi(length) = 0, pi(s) = 0, pi(zeros) = [], pi(n__zeros) = [], pi(0) = [], pi(cons) = [0,1] Usable Rules: {} Interpretation: [U31#](x0, x1, x2) = x0 + x1 + x2, [take#](x0, x1) = x0 + x1, [n__cons](x0, x1) = x0 + x1, [n__take](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = x0 + x1, [0] = 0 Strict: { length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N)), length#(cons(N, L)) -> isNatList#(activate(L)), activate#(n__length(X)) -> length#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), U11#(tt(), L) -> length#(activate(L)), U11#(tt(), L) -> activate#(L), U31#(tt(), IL, M, N) -> activate#(N), U31#(tt(), IL, M, N) -> activate#(M), U31#(tt(), IL, M, N) -> activate#(IL), and#(tt(), X) -> activate#(X), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNatIList#(V) -> activate#(V), isNatIList#(V) -> isNatList#(activate(V)), isNatIList#(n__cons(V1, V2)) -> activate#(V1), isNatIList#(n__cons(V1, V2)) -> activate#(V2), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), take#(0(), IL) -> isNatIList#(IL), take#(s(M), cons(N, IL)) -> activate#(IL), take#(s(M), cons(N, IL)) -> U31#(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N), take#(s(M), cons(N, IL)) -> and#(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), take#(s(M), cons(N, IL)) -> isNat#(M), take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length(nil()) -> 0(), activate(X) -> X, activate(n__zeros()) -> zeros(), activate(n__take(X1, X2)) -> take(X1, X2), activate(n__0()) -> 0(), activate(n__length(X)) -> length(X), activate(n__s(X)) -> s(X), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(X1, X2), U11(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U21(tt()) -> nil(), U31(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> isNatList(activate(V1)), isNat(n__s(V1)) -> isNat(activate(V1)), isNatList(X) -> n__isNatList(X), isNatList(n__take(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList(n__nil()) -> tt(), isNatIList(X) -> n__isNatIList(X), isNatIList(V) -> isNatList(activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U21(isNatIList(IL)), take(s(M), cons(N, IL)) -> U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)} EDG: { (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(n__cons(V1, V2)) -> activate#(V2)) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(n__cons(V1, V2)) -> activate#(V1)) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(V) -> isNatList#(activate(V))) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(V) -> activate#(V)) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> isNat#(activate(V1))) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> activate#(V1)) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__length(V1)) -> activate#(V1)) (activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X)) (isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), and#(tt(), X) -> activate#(X)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__isNat(X)) -> isNat#(X)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__isNatList(X)) -> isNatList#(X)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__isNatIList(X)) -> isNatIList#(X)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> length#(X)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> activate#(V2)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> activate#(V1)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(V) -> isNatList#(activate(V))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(V) -> activate#(V)) (take#(s(M), cons(N, IL)) -> U31#(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N), U31#(tt(), IL, M, N) -> activate#(IL)) (take#(s(M), cons(N, IL)) -> U31#(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N), U31#(tt(), IL, M, N) -> activate#(M)) (take#(s(M), cons(N, IL)) -> U31#(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N), U31#(tt(), IL, M, N) -> activate#(N)) (length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N)), and#(tt(), X) -> activate#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatList(X)) -> isNatList#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U11#(tt(), L) -> activate#(L), activate#(n__isNat(X)) -> isNat#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__isNatList(X)) -> isNatList#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__isNatIList(X)) -> isNatIList#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__length(X)) -> length#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(X)) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2)))) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2)))) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (take#(s(M), cons(N, IL)) -> isNat#(M), isNat#(n__s(V1)) -> isNat#(activate(V1))) (take#(s(M), cons(N, IL)) -> isNat#(M), isNat#(n__s(V1)) -> activate#(V1)) (take#(s(M), cons(N, IL)) -> isNat#(M), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (take#(s(M), cons(N, IL)) -> isNat#(M), isNat#(n__length(V1)) -> activate#(V1)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2)))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (U11#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> activate#(L)) (U11#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L))) (U11#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N))) (U11#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(V) -> activate#(V)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(V) -> isNatList#(activate(V))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> activate#(V1)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> activate#(V2)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> length#(X)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__isNatIList(X)) -> isNatIList#(X)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__isNatList(X)) -> isNatList#(X)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__isNat(X)) -> isNat#(X)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (take#(s(M), cons(N, IL)) -> and#(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), and#(tt(), X) -> activate#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__length(X)) -> length#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__isNatIList(X)) -> isNatIList#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__isNatList(X)) -> isNatList#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__isNat(X)) -> isNat#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__isNatList(X)) -> isNatList#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), U11#(tt(), L) -> length#(activate(L))) (length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), U11#(tt(), L) -> activate#(L)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__length(X)) -> length#(X)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__isNatIList(X)) -> isNatIList#(X)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__isNatList(X)) -> isNatList#(X)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__isNat(X)) -> isNat#(X)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> length#(X)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__isNatIList(X)) -> isNatIList#(X)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__isNatList(X)) -> isNatList#(X)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__isNat(X)) -> isNat#(X)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatIList#(V) -> activate#(V), activate#(n__length(X)) -> length#(X)) (isNatIList#(V) -> activate#(V), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatIList#(V) -> activate#(V), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatIList#(V) -> activate#(V), activate#(n__isNat(X)) -> isNat#(X)) (isNatIList#(V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), and#(tt(), X) -> activate#(X)) (and#(tt(), X) -> activate#(X), activate#(n__length(X)) -> length#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNatList(X)) -> isNatList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(X1, X2)) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2)))) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> activate#(L)) (activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L))) (activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N))) (activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> isNatList#(activate(L))) } SCCS: Scc: { length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N)), length#(cons(N, L)) -> isNatList#(activate(L)), activate#(n__length(X)) -> length#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), U11#(tt(), L) -> length#(activate(L)), U11#(tt(), L) -> activate#(L), and#(tt(), X) -> activate#(X), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNatIList#(V) -> activate#(V), isNatIList#(V) -> isNatList#(activate(V)), isNatIList#(n__cons(V1, V2)) -> activate#(V1), isNatIList#(n__cons(V1, V2)) -> activate#(V2), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1))} SCC: Strict: { length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N)), length#(cons(N, L)) -> isNatList#(activate(L)), activate#(n__length(X)) -> length#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), U11#(tt(), L) -> length#(activate(L)), U11#(tt(), L) -> activate#(L), and#(tt(), X) -> activate#(X), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNatIList#(V) -> activate#(V), isNatIList#(V) -> isNatList#(activate(V)), isNatIList#(n__cons(V1, V2)) -> activate#(V1), isNatIList#(n__cons(V1, V2)) -> activate#(V2), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length(nil()) -> 0(), activate(X) -> X, activate(n__zeros()) -> zeros(), activate(n__take(X1, X2)) -> take(X1, X2), activate(n__0()) -> 0(), activate(n__length(X)) -> length(X), activate(n__s(X)) -> s(X), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(X1, X2), U11(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U21(tt()) -> nil(), U31(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> isNatList(activate(V1)), isNat(n__s(V1)) -> isNat(activate(V1)), isNatList(X) -> n__isNatList(X), isNatList(n__take(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList(n__nil()) -> tt(), isNatIList(X) -> n__isNatIList(X), isNatIList(V) -> isNatList(activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U21(isNatIList(IL)), take(s(M), cons(N, IL)) -> U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)} POLY: Argument Filtering: pi(n__and) = 1, pi(take) = [1], pi(n__isNat) = 0, pi(n__isNatList) = 0, pi(n__nil) = [], pi(n__cons) = [0,1], pi(n__isNatIList) = [0], pi(isNatIList#) = [0], pi(isNatIList) = [0], pi(n__s) = 0, pi(n__length) = 0, pi(isNatList#) = 0, pi(isNatList) = 0, pi(n__0) = [], pi(isNat#) = 0, pi(isNat) = 0, pi(and#) = 1, pi(and) = 1, pi(U31) = [1,3], pi(n__take) = [1], pi(U21) = [], pi(nil) = [], pi(tt) = [], pi(U11#) = 1, pi(U11) = 1, pi(activate#) = 0, pi(activate) = 0, pi(length#) = 0, pi(length) = 0, pi(s) = 0, pi(zeros) = [], pi(n__zeros) = [], pi(0) = [], pi(cons) = [0,1] Usable Rules: {} Interpretation: [isNatIList#](x0) = x0 + 1, [n__cons](x0, x1) = x0 + x1, [cons](x0, x1) = x0 + x1, [n__isNatIList](x0) = x0 + 1 Strict: { length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N)), length#(cons(N, L)) -> isNatList#(activate(L)), activate#(n__length(X)) -> length#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), U11#(tt(), L) -> length#(activate(L)), U11#(tt(), L) -> activate#(L), and#(tt(), X) -> activate#(X), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length(nil()) -> 0(), activate(X) -> X, activate(n__zeros()) -> zeros(), activate(n__take(X1, X2)) -> take(X1, X2), activate(n__0()) -> 0(), activate(n__length(X)) -> length(X), activate(n__s(X)) -> s(X), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(X1, X2), U11(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U21(tt()) -> nil(), U31(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> isNatList(activate(V1)), isNat(n__s(V1)) -> isNat(activate(V1)), isNatList(X) -> n__isNatList(X), isNatList(n__take(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList(n__nil()) -> tt(), isNatIList(X) -> n__isNatIList(X), isNatIList(V) -> isNatList(activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U21(isNatIList(IL)), take(s(M), cons(N, IL)) -> U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)} EDG: {(isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2)))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X)) (length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), U11#(tt(), L) -> activate#(L)) (length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), U11#(tt(), L) -> length#(activate(L))) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__isNatList(X)) -> isNatList#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(X)) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> isNat#(activate(V1))) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> activate#(V1)) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__length(V1)) -> activate#(V1)) (length#(cons(N, L)) -> activate#(L), activate#(n__and(X1, X2)) -> and#(X1, X2)) (length#(cons(N, L)) -> activate#(L), activate#(n__isNat(X)) -> isNat#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__isNatList(X)) -> isNatList#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__isNatIList(X)) -> isNatIList#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__length(X)) -> length#(X)) (isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), and#(tt(), X) -> activate#(X)) (isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), and#(tt(), X) -> activate#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__length(X)) -> length#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__isNatIList(X)) -> isNatIList#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__isNatList(X)) -> isNatList#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__isNat(X)) -> isNat#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__and(X1, X2)) -> and#(X1, X2)) (and#(tt(), X) -> activate#(X), activate#(n__length(X)) -> length#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNatList(X)) -> isNatList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(X1, X2)) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2)))) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> activate#(L)) (activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L))) (activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N))) (activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> isNatList#(activate(L))) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatList(X)) -> isNatList#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N)), and#(tt(), X) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U11#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> activate#(L)) (U11#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L))) (U11#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N))) (U11#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L))) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2)))) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)))} SCCS: Scc: { length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N)), length#(cons(N, L)) -> isNatList#(activate(L)), activate#(n__length(X)) -> length#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), U11#(tt(), L) -> length#(activate(L)), U11#(tt(), L) -> activate#(L), and#(tt(), X) -> activate#(X), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))} SCC: Strict: { length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N)), length#(cons(N, L)) -> isNatList#(activate(L)), activate#(n__length(X)) -> length#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), U11#(tt(), L) -> length#(activate(L)), U11#(tt(), L) -> activate#(L), and#(tt(), X) -> activate#(X), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length(nil()) -> 0(), activate(X) -> X, activate(n__zeros()) -> zeros(), activate(n__take(X1, X2)) -> take(X1, X2), activate(n__0()) -> 0(), activate(n__length(X)) -> length(X), activate(n__s(X)) -> s(X), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(X1, X2), U11(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U21(tt()) -> nil(), U31(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> isNatList(activate(V1)), isNat(n__s(V1)) -> isNat(activate(V1)), isNatList(X) -> n__isNatList(X), isNatList(n__take(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList(n__nil()) -> tt(), isNatIList(X) -> n__isNatIList(X), isNatIList(V) -> isNatList(activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U21(isNatIList(IL)), take(s(M), cons(N, IL)) -> U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)} POLY: Argument Filtering: pi(n__and) = 1, pi(take) = 1, pi(n__isNat) = 0, pi(n__isNatList) = 0, pi(n__nil) = [], pi(n__cons) = [0,1], pi(n__isNatIList) = 0, pi(isNatIList#) = 0, pi(isNatIList) = 0, pi(n__s) = 0, pi(n__length) = [0], pi(isNatList#) = 0, pi(isNatList) = 0, pi(n__0) = [], pi(isNat#) = 0, pi(isNat) = 0, pi(and#) = 1, pi(and) = 1, pi(U31) = [1,3], pi(n__take) = 1, pi(U21) = [], pi(nil) = [], pi(tt) = [], pi(U11#) = 1, pi(U11) = [1], pi(activate#) = 0, pi(activate) = 0, pi(length#) = 0, pi(length) = [0], pi(s) = 0, pi(zeros) = [], pi(n__zeros) = [], pi(0) = [], pi(cons) = [0,1] Usable Rules: {} Interpretation: [n__cons](x0, x1) = x0 + x1, [cons](x0, x1) = x0 + x1, [n__length](x0) = x0 + 1 Strict: { length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N)), length#(cons(N, L)) -> isNatList#(activate(L)), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), U11#(tt(), L) -> length#(activate(L)), U11#(tt(), L) -> activate#(L), and#(tt(), X) -> activate#(X), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length(nil()) -> 0(), activate(X) -> X, activate(n__zeros()) -> zeros(), activate(n__take(X1, X2)) -> take(X1, X2), activate(n__0()) -> 0(), activate(n__length(X)) -> length(X), activate(n__s(X)) -> s(X), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(X1, X2), U11(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U21(tt()) -> nil(), U31(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> isNatList(activate(V1)), isNat(n__s(V1)) -> isNat(activate(V1)), isNatList(X) -> n__isNatList(X), isNatList(n__take(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList(n__nil()) -> tt(), isNatIList(X) -> n__isNatIList(X), isNatIList(V) -> isNatList(activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U21(isNatIList(IL)), take(s(M), cons(N, IL)) -> U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)} EDG: {(activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2)))) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(X1, X2)) (and#(tt(), X) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNatList(X)) -> isNatList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (U11#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L))) (U11#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N))) (U11#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L))) (U11#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> activate#(L)) (length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), U11#(tt(), L) -> activate#(L)) (length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), U11#(tt(), L) -> length#(activate(L))) (activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U11#(tt(), L) -> activate#(L), activate#(n__isNat(X)) -> isNat#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__isNatList(X)) -> isNatList#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), and#(tt(), X) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatList(X)) -> isNatList#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), and#(tt(), X) -> activate#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__isNatIList(X)) -> isNatIList#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__isNatList(X)) -> isNatList#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__isNat(X)) -> isNat#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__and(X1, X2)) -> and#(X1, X2)) (length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N)), and#(tt(), X) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2)))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> activate#(V1)) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> isNat#(activate(V1))) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))))} SCCS: Scc: { activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))} Scc: {length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), U11#(tt(), L) -> length#(activate(L))} SCC: Strict: { activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length(nil()) -> 0(), activate(X) -> X, activate(n__zeros()) -> zeros(), activate(n__take(X1, X2)) -> take(X1, X2), activate(n__0()) -> 0(), activate(n__length(X)) -> length(X), activate(n__s(X)) -> s(X), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(X1, X2), U11(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U21(tt()) -> nil(), U31(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> isNatList(activate(V1)), isNat(n__s(V1)) -> isNat(activate(V1)), isNatList(X) -> n__isNatList(X), isNatList(n__take(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList(n__nil()) -> tt(), isNatIList(X) -> n__isNatIList(X), isNatIList(V) -> isNatList(activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U21(isNatIList(IL)), take(s(M), cons(N, IL)) -> U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)} POLY: Argument Filtering: pi(n__and) = [0,1], pi(take) = [0,1], pi(n__isNat) = 0, pi(n__isNatList) = [0], pi(n__nil) = [], pi(n__cons) = [0,1], pi(n__isNatIList) = [0], pi(isNatIList#) = [0], pi(isNatIList) = [0], pi(n__s) = 0, pi(n__length) = [0], pi(isNatList#) = [0], pi(isNatList) = [0], pi(n__0) = [], pi(isNat#) = 0, pi(isNat) = 0, pi(and#) = 1, pi(and) = [0,1], pi(U31) = [1,2,3], pi(n__take) = [0,1], pi(U21) = 0, pi(nil) = [], pi(tt) = [], pi(U11) = [1], pi(activate#) = 0, pi(activate) = 0, pi(length) = [0], pi(s) = 0, pi(zeros) = [], pi(n__zeros) = [], pi(0) = [], pi(cons) = [0,1] Usable Rules: {} Interpretation: [isNatIList#](x0) = x0 + 1, [isNatList#](x0) = x0 + 1, [n__and](x0, x1) = x0 + x1, [n__cons](x0, x1) = x0 + x1, [n__isNatList](x0) = x0 + 1, [n__isNatIList](x0) = x0 + 1 Strict: { activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length(nil()) -> 0(), activate(X) -> X, activate(n__zeros()) -> zeros(), activate(n__take(X1, X2)) -> take(X1, X2), activate(n__0()) -> 0(), activate(n__length(X)) -> length(X), activate(n__s(X)) -> s(X), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(X1, X2), U11(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U21(tt()) -> nil(), U31(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> isNatList(activate(V1)), isNat(n__s(V1)) -> isNat(activate(V1)), isNatList(X) -> n__isNatList(X), isNatList(n__take(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList(n__nil()) -> tt(), isNatIList(X) -> n__isNatIList(X), isNatIList(V) -> isNatList(activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U21(isNatIList(IL)), take(s(M), cons(N, IL)) -> U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)} EDG: {(activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2)))) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(X1, X2)) (and#(tt(), X) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNatList(X)) -> isNatList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), and#(tt(), X) -> activate#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatList(X)) -> isNatList#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), and#(tt(), X) -> activate#(X)) (activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X)) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> activate#(V1)) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> isNat#(activate(V1))) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))))} SCCS: Scc: { activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))} SCC: Strict: { activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length(nil()) -> 0(), activate(X) -> X, activate(n__zeros()) -> zeros(), activate(n__take(X1, X2)) -> take(X1, X2), activate(n__0()) -> 0(), activate(n__length(X)) -> length(X), activate(n__s(X)) -> s(X), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(X1, X2), U11(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U21(tt()) -> nil(), U31(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> isNatList(activate(V1)), isNat(n__s(V1)) -> isNat(activate(V1)), isNatList(X) -> n__isNatList(X), isNatList(n__take(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList(n__nil()) -> tt(), isNatIList(X) -> n__isNatIList(X), isNatIList(V) -> isNatList(activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U21(isNatIList(IL)), take(s(M), cons(N, IL)) -> U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)} POLY: Argument Filtering: pi(n__and) = 1, pi(take) = [], pi(n__isNat) = [0], pi(n__isNatList) = [], pi(n__nil) = [], pi(n__cons) = [], pi(n__isNatIList) = [], pi(isNatIList#) = [], pi(isNatIList) = [], pi(n__s) = 0, pi(n__length) = [], pi(isNatList#) = [], pi(isNatList) = [], pi(n__0) = [], pi(isNat#) = 0, pi(isNat) = [0], pi(and#) = 1, pi(and) = 1, pi(U31) = [], pi(n__take) = [], pi(U21) = [], pi(nil) = [], pi(tt) = [], pi(U11) = [], pi(activate#) = 0, pi(activate) = 0, pi(length) = [], pi(s) = 0, pi(zeros) = [], pi(n__zeros) = [], pi(0) = [], pi(cons) = [] Usable Rules: {} Interpretation: [isNatIList#] = 0, [isNatList#] = 0, [n__isNat](x0) = x0 + 1, [n__isNatList] = 0, [n__isNatIList] = 0 Strict: { activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length(nil()) -> 0(), activate(X) -> X, activate(n__zeros()) -> zeros(), activate(n__take(X1, X2)) -> take(X1, X2), activate(n__0()) -> 0(), activate(n__length(X)) -> length(X), activate(n__s(X)) -> s(X), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(X1, X2), U11(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U21(tt()) -> nil(), U31(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> isNatList(activate(V1)), isNat(n__s(V1)) -> isNat(activate(V1)), isNatList(X) -> n__isNatList(X), isNatList(n__take(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList(n__nil()) -> tt(), isNatIList(X) -> n__isNatIList(X), isNatIList(V) -> isNatList(activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U21(isNatIList(IL)), take(s(M), cons(N, IL)) -> U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)} EDG: {(activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2)))) (isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), and#(tt(), X) -> activate#(X)) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatList(X)) -> isNatList#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X)) (isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), and#(tt(), X) -> activate#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNatList(X)) -> isNatList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(X1, X2)) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))))} SCCS: Scc: {isNat#(n__s(V1)) -> isNat#(activate(V1))} Scc: { activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))} SCC: Strict: {isNat#(n__s(V1)) -> isNat#(activate(V1))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length(nil()) -> 0(), activate(X) -> X, activate(n__zeros()) -> zeros(), activate(n__take(X1, X2)) -> take(X1, X2), activate(n__0()) -> 0(), activate(n__length(X)) -> length(X), activate(n__s(X)) -> s(X), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(X1, X2), U11(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U21(tt()) -> nil(), U31(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> isNatList(activate(V1)), isNat(n__s(V1)) -> isNat(activate(V1)), isNatList(X) -> n__isNatList(X), isNatList(n__take(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList(n__nil()) -> tt(), isNatIList(X) -> n__isNatIList(X), isNatIList(V) -> isNatList(activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U21(isNatIList(IL)), take(s(M), cons(N, IL)) -> U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)} Fail SCC: Strict: { activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length(nil()) -> 0(), activate(X) -> X, activate(n__zeros()) -> zeros(), activate(n__take(X1, X2)) -> take(X1, X2), activate(n__0()) -> 0(), activate(n__length(X)) -> length(X), activate(n__s(X)) -> s(X), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(X1, X2), U11(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U21(tt()) -> nil(), U31(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> isNatList(activate(V1)), isNat(n__s(V1)) -> isNat(activate(V1)), isNatList(X) -> n__isNatList(X), isNatList(n__take(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList(n__nil()) -> tt(), isNatIList(X) -> n__isNatIList(X), isNatIList(V) -> isNatList(activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U21(isNatIList(IL)), take(s(M), cons(N, IL)) -> U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)} POLY: Argument Filtering: pi(n__and) = [0,1], pi(take) = [], pi(n__isNat) = [], pi(n__isNatList) = [], pi(n__nil) = [], pi(n__cons) = [], pi(n__isNatIList) = [], pi(isNatIList#) = [], pi(isNatIList) = [], pi(n__s) = [], pi(n__length) = [], pi(isNatList#) = [], pi(isNatList) = [], pi(n__0) = [], pi(isNat) = [], pi(and#) = 1, pi(and) = [], pi(U31) = [], pi(n__take) = [], pi(U21) = [], pi(nil) = [], pi(tt) = [], pi(U11) = [], pi(activate#) = 0, pi(activate) = [], pi(length) = [], pi(s) = [], pi(zeros) = [], pi(n__zeros) = [], pi(0) = [], pi(cons) = [] Usable Rules: {} Interpretation: [isNatIList#] = 0, [isNatList#] = 0, [n__and](x0, x1) = x0 + x1 + 1, [n__isNatList] = 0, [n__isNatIList] = 0 Strict: { activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), and#(tt(), X) -> activate#(X), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length(nil()) -> 0(), activate(X) -> X, activate(n__zeros()) -> zeros(), activate(n__take(X1, X2)) -> take(X1, X2), activate(n__0()) -> 0(), activate(n__length(X)) -> length(X), activate(n__s(X)) -> s(X), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(X1, X2), U11(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U21(tt()) -> nil(), U31(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> isNatList(activate(V1)), isNat(n__s(V1)) -> isNat(activate(V1)), isNatList(X) -> n__isNatList(X), isNatList(n__take(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList(n__nil()) -> tt(), isNatIList(X) -> n__isNatIList(X), isNatIList(V) -> isNatList(activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U21(isNatIList(IL)), take(s(M), cons(N, IL)) -> U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)} EDG: {(activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2)))) (isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), and#(tt(), X) -> activate#(X)) (isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), and#(tt(), X) -> activate#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))))} SCCS: Scc: { activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), and#(tt(), X) -> activate#(X), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))} SCC: Strict: { activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__isNatList(X)) -> isNatList#(X), and#(tt(), X) -> activate#(X), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length(nil()) -> 0(), activate(X) -> X, activate(n__zeros()) -> zeros(), activate(n__take(X1, X2)) -> take(X1, X2), activate(n__0()) -> 0(), activate(n__length(X)) -> length(X), activate(n__s(X)) -> s(X), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(X1, X2), U11(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U21(tt()) -> nil(), U31(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> isNatList(activate(V1)), isNat(n__s(V1)) -> isNat(activate(V1)), isNatList(X) -> n__isNatList(X), isNatList(n__take(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList(n__nil()) -> tt(), isNatIList(X) -> n__isNatIList(X), isNatIList(V) -> isNatList(activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U21(isNatIList(IL)), take(s(M), cons(N, IL)) -> U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)} Fail SCC: Strict: {length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L)), U11#(tt(), L) -> length#(activate(L))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U11(and(isNatList(activate(L)), n__isNat(N)), activate(L)), length(nil()) -> 0(), activate(X) -> X, activate(n__zeros()) -> zeros(), activate(n__take(X1, X2)) -> take(X1, X2), activate(n__0()) -> 0(), activate(n__length(X)) -> length(X), activate(n__s(X)) -> s(X), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(X1, X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(X1, X2), U11(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U21(tt()) -> nil(), U31(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> isNatList(activate(V1)), isNat(n__s(V1)) -> isNat(activate(V1)), isNatList(X) -> n__isNatList(X), isNatList(n__take(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), isNatList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatList(activate(V2))), isNatList(n__nil()) -> tt(), isNatIList(X) -> n__isNatIList(X), isNatIList(V) -> isNatList(activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> and(isNat(activate(V1)), n__isNatIList(activate(V2))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U21(isNatIList(IL)), take(s(M), cons(N, IL)) -> U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)} Fail