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(activate(X1), activate(X2)), activate(n__0()) -> 0(), activate(n__length(X)) -> length(activate(X)), activate(n__s(X)) -> s(activate(X)), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(activate(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(n__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)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), activate#(n__0()) -> 0#(), activate#(n__length(X)) -> length#(activate(X)), activate#(n__length(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)), activate#(n__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__nil()) -> nil#(), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(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(n__isNat(M), n__isNat(N))), activate(IL), M, N), take#(s(M), cons(N, IL)) -> and#(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), 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(activate(X1), activate(X2)), activate(n__0()) -> 0(), activate(n__length(X)) -> length(activate(X)), activate(n__s(X)) -> s(activate(X)), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(activate(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(n__isNat(M), n__isNat(N))), activate(IL), M, N)} EDG: { (length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N)), and#(tt(), X) -> activate#(X)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__and(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__cons(X1, X2)) -> cons#(activate(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)) -> activate#(X)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__s(X)) -> s#(activate(X))) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> length#(activate(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#(activate(X1), activate(X2))) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X2)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X1)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__zeros()) -> zeros#()) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> activate#(X1)) (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__nil()) -> nil#()) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__zeros()) -> zeros#()) (take#(s(M), cons(N, IL)) -> U31#(and(isNatIList(activate(IL)), n__and(n__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(n__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(n__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(n__isNat(M), n__isNat(N))), activate(IL), M, N), U31#(tt(), IL, M, N) -> cons#(activate(N), n__take(activate(M), activate(IL)))) (length#(cons(N, L)) -> activate#(L), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (length#(cons(N, L)) -> activate#(L), activate#(n__and(X1, X2)) -> activate#(X1)) (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__nil()) -> nil#()) (length#(cons(N, L)) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (length#(cons(N, L)) -> activate#(L), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (length#(cons(N, L)) -> activate#(L), activate#(n__isNatIList(X)) -> isNatIList#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__s(X)) -> s#(activate(X))) (length#(cons(N, L)) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (length#(cons(N, L)) -> activate#(L), activate#(n__0()) -> 0#()) (length#(cons(N, L)) -> activate#(L), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (length#(cons(N, L)) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X2)) (length#(cons(N, L)) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X1)) (length#(cons(N, L)) -> activate#(L), activate#(n__zeros()) -> zeros#()) (isNatIList#(V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatIList#(V) -> activate#(V), activate#(n__and(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (isNatIList#(V) -> activate#(V), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatIList#(V) -> activate#(V), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatIList#(V) -> activate#(V), activate#(n__s(X)) -> activate#(X)) (isNatIList#(V) -> activate#(V), activate#(n__s(X)) -> s#(activate(X))) (isNatIList#(V) -> activate#(V), activate#(n__length(X)) -> activate#(X)) (isNatIList#(V) -> activate#(V), activate#(n__length(X)) -> length#(activate(X))) (isNatIList#(V) -> activate#(V), activate#(n__0()) -> 0#()) (isNatIList#(V) -> activate#(V), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatIList#(V) -> activate#(V), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatIList#(V) -> activate#(V), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatIList#(V) -> activate#(V), activate#(n__zeros()) -> zeros#()) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X2)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(activate(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)) -> activate#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(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#(activate(X1), activate(X2))) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(activate(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)) -> activate#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(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#(activate(X1), activate(X2))) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (activate#(n__and(X1, X2)) -> and#(activate(X1), X2), and#(tt(), X) -> activate#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__s(X)) -> activate#(X), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__nil()) -> nil#()) (activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__s(X)) -> activate#(X), activate#(n__0()) -> 0#()) (activate#(n__s(X)) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (activate#(n__s(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X2)) (activate#(n__s(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__zeros()) -> zeros#()) (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)) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> activate#(X1)) (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__nil()) -> nil#()) (and#(tt(), X) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (and#(tt(), X) -> activate#(X), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (and#(tt(), X) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (and#(tt(), X) -> activate#(X), activate#(n__s(X)) -> s#(activate(X))) (and#(tt(), X) -> activate#(X), activate#(n__length(X)) -> activate#(X)) (and#(tt(), X) -> activate#(X), activate#(n__length(X)) -> length#(activate(X))) (and#(tt(), X) -> activate#(X), activate#(n__0()) -> 0#()) (and#(tt(), X) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (and#(tt(), X) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X2)) (and#(tt(), X) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X1)) (and#(tt(), X) -> activate#(X), activate#(n__zeros()) -> zeros#()) (take#(s(M), cons(N, IL)) -> and#(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), and#(tt(), X) -> activate#(X)) (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)) (activate#(n__length(X)) -> length#(activate(X)), length#(nil()) -> 0#()) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> isNatList#(activate(L))) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N))) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L))) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> activate#(L)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__and(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__cons(X1, X2)) -> cons#(activate(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)) -> activate#(X)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__s(X)) -> s#(activate(X))) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> activate#(X)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> length#(activate(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#(activate(X1), activate(X2))) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X2)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X1)) (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#(activate(X1), X2)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__and(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__cons(X1, X2)) -> cons#(activate(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)) -> activate#(X)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__s(X)) -> s#(activate(X))) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__length(X)) -> activate#(X)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__length(X)) -> length#(activate(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#(activate(X1), activate(X2))) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X2)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X1)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__zeros()) -> zeros#()) (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)) (isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), and#(tt(), X) -> activate#(X)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__nil()) -> nil#()) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__length(X)) -> activate#(X)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__0()) -> 0#()) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X2)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X1)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__zeros()) -> zeros#()) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__nil()) -> nil#()) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__length(X)) -> activate#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__0()) -> 0#()) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X2)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X1)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__zeros()) -> zeros#()) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__zeros()) -> zeros#()) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> activate#(X1)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> activate#(X2)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__0()) -> 0#()) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> length#(activate(X))) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> activate#(X)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__s(X)) -> s#(activate(X))) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__s(X)) -> activate#(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#(activate(X1), X2)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__cons(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__zeros()) -> zeros#()) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X1)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X2)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__0()) -> 0#()) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__length(X)) -> activate#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__nil()) -> nil#()) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(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)) (activate#(n__zeros()) -> zeros#(), zeros#() -> cons#(0(), n__zeros())) (activate#(n__zeros()) -> zeros#(), zeros#() -> 0#()) (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#()) (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))) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__zeros()) -> zeros#()) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__take(X1, X2)) -> activate#(X1)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__take(X1, X2)) -> activate#(X2)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__0()) -> 0#()) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__length(X)) -> activate#(X)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> activate#(X)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__nil()) -> nil#()) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (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))) (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__isNatIList(X)) -> isNatIList#(X), isNatIList#(V) -> activate#(V)) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(V) -> isNatList#(activate(V))) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(n__cons(V1, V2)) -> activate#(V1)) (activate#(n__isNatIList(X)) -> isNatIList#(X), isNatIList#(n__cons(V1, V2)) -> activate#(V2)) (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)) -> isNat#(activate(V1))) (activate#(n__length(X)) -> activate#(X), activate#(n__zeros()) -> zeros#()) (activate#(n__length(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X1)) (activate#(n__length(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X2)) (activate#(n__length(X)) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (activate#(n__length(X)) -> activate#(X), activate#(n__0()) -> 0#()) (activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__length(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (activate#(n__length(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__length(X)) -> activate#(X), activate#(n__nil()) -> nil#()) (activate#(n__length(X)) -> activate#(X), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__length(X)) -> activate#(X), activate#(n__and(X1, X2)) -> and#(activate(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)) -> activate#(X1)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> activate#(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#(activate(X1), X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> activate#(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#(activate(X1), X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U11#(tt(), L) -> activate#(L), activate#(n__zeros()) -> zeros#()) (U11#(tt(), L) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X1)) (U11#(tt(), L) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X2)) (U11#(tt(), L) -> activate#(L), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U11#(tt(), L) -> activate#(L), activate#(n__0()) -> 0#()) (U11#(tt(), L) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (U11#(tt(), L) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__s(X)) -> s#(activate(X))) (U11#(tt(), L) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__isNatIList(X)) -> isNatIList#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U11#(tt(), L) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (U11#(tt(), L) -> activate#(L), activate#(n__nil()) -> nil#()) (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)) -> activate#(X1)) (U11#(tt(), L) -> activate#(L), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__zeros()) -> zeros#()) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#()) (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)) -> activate#(X1)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__zeros()) -> zeros#()) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#()) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> activate#(X1)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(0(), IL) -> U21#(isNatIList(IL))) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(0(), IL) -> isNatIList#(IL)) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(s(M), cons(N, IL)) -> activate#(IL)) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(s(M), cons(N, IL)) -> U31#(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(s(M), cons(N, IL)) -> and#(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N)))) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(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)) } 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)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), activate#(n__length(X)) -> length#(activate(X)), activate#(n__length(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(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(n__isNat(M), n__isNat(N))), activate(IL), M, N), take#(s(M), cons(N, IL)) -> and#(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), 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)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), activate#(n__length(X)) -> length#(activate(X)), activate#(n__length(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(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(n__isNat(M), n__isNat(N))), activate(IL), M, N), take#(s(M), cons(N, IL)) -> and#(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), 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(activate(X1), activate(X2)), activate(n__0()) -> 0(), activate(n__length(X)) -> length(activate(X)), activate(n__s(X)) -> s(activate(X)), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(activate(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(n__isNat(M), n__isNat(N))), activate(IL), M, N)} POLY: Argument Filtering: pi(n__and) = [0,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) = [0,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 + 1, [n__and](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__take(X1, X2)) -> take#(activate(X1), activate(X2)), activate#(n__length(X)) -> length#(activate(X)), activate#(n__length(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(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))} 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(activate(X1), activate(X2)), activate(n__0()) -> 0(), activate(n__length(X)) -> length(activate(X)), activate(n__s(X)) -> s(activate(X)), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(activate(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(n__isNat(M), n__isNat(N))), activate(IL), M, N)} EDG: { (length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N)), and#(tt(), X) -> activate#(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__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)) (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)) (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)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> activate#(X1)) (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__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (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__cons(X1, X2)) -> activate#(X1)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (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__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__and(X1, X2)) -> activate#(X1)) (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__cons(X1, X2)) -> activate#(X1)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__isNatIList(X)) -> isNatIList#(X)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__s(X)) -> activate#(X)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> activate#(X)) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> length#(activate(X))) (U31#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (activate#(n__and(X1, X2)) -> and#(activate(X1), X2), and#(tt(), X) -> activate#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__length(X)) -> activate#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (activate#(n__length(X)) -> activate#(X), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__length(X)) -> activate#(X), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__length(X)) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__length(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__length(X)) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (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)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__and(X1, X2)) -> activate#(X1)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__isNat(X)) -> isNat#(X)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__isNatList(X)) -> isNatList#(X)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__cons(X1, X2)) -> activate#(X1)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__isNatIList(X)) -> isNatIList#(X)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__s(X)) -> activate#(X)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> activate#(X)) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> length#(activate(X))) (U31#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U11#(tt(), L) -> activate#(L), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U11#(tt(), L) -> activate#(L), activate#(n__and(X1, X2)) -> activate#(X1)) (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__cons(X1, X2)) -> activate#(X1)) (U11#(tt(), L) -> activate#(L), activate#(n__isNatIList(X)) -> isNatIList#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (U11#(tt(), L) -> activate#(L), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), and#(tt(), X) -> activate#(X)) (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__take(X1, X2)) -> take#(activate(X1), activate(X2))) (length#(cons(N, L)) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (length#(cons(N, L)) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__isNatIList(X)) -> isNatIList#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (length#(cons(N, L)) -> activate#(L), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (and#(tt(), X) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (and#(tt(), X) -> activate#(X), activate#(n__length(X)) -> length#(activate(X))) (and#(tt(), X) -> activate#(X), activate#(n__length(X)) -> activate#(X)) (and#(tt(), X) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(activate(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__s(X)) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatIList#(V) -> activate#(V), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatIList#(V) -> activate#(V), activate#(n__length(X)) -> length#(activate(X))) (isNatIList#(V) -> activate#(V), activate#(n__length(X)) -> activate#(X)) (isNatIList#(V) -> activate#(V), activate#(n__s(X)) -> activate#(X)) (isNatIList#(V) -> activate#(V), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatIList#(V) -> activate#(V), activate#(n__cons(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (isNatIList#(V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__length(X)) -> activate#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> length#(activate(X))) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__isNatIList(X)) -> isNatIList#(X)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__isNatList(X)) -> isNatList#(X)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__isNat(X)) -> isNat#(X)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__and(X1, X2)) -> activate#(X1)) (U31#(tt(), IL, M, N) -> activate#(N), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatList(X)) -> isNatList#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(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))) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> activate#(L)) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L))) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N))) (activate#(n__length(X)) -> length#(activate(X)), 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))) (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)) } 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#(activate(X)), activate#(n__length(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(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#(activate(X)), activate#(n__length(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(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(activate(X1), activate(X2)), activate(n__0()) -> 0(), activate(n__length(X)) -> length(activate(X)), activate(n__s(X)) -> s(activate(X)), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(activate(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(n__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) = [], 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__and](x0, x1) = x0 + x1, [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#(activate(X)), activate#(n__length(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(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(activate(X1), activate(X2)), activate(n__0()) -> 0(), activate(n__length(X)) -> length(activate(X)), activate(n__s(X)) -> s(activate(X)), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(activate(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(n__isNat(M), n__isNat(N))), activate(IL), M, N)} EDG: { (U11#(tt(), L) -> activate#(L), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U11#(tt(), L) -> activate#(L), activate#(n__and(X1, X2)) -> activate#(X1)) (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__cons(X1, X2)) -> activate#(X1)) (U11#(tt(), L) -> activate#(L), activate#(n__isNatIList(X)) -> isNatIList#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (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__cons(X1, X2)) -> activate#(X1)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(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))) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> activate#(X1)) (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__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), and#(tt(), X) -> activate#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__length(X)) -> activate#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__length(X)) -> length#(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)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> isNatList#(activate(L))) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N))) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> U11#(and(isNatList(activate(L)), n__isNat(N)), activate(L))) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> activate#(L)) (activate#(n__s(X)) -> activate#(X), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__s(X)) -> activate#(X), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X))) (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__and(X1, X2)) -> and#(activate(X1), X2), and#(tt(), X) -> activate#(X)) (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))) (and#(tt(), X) -> activate#(X), activate#(n__length(X)) -> length#(activate(X))) (and#(tt(), X) -> activate#(X), activate#(n__length(X)) -> activate#(X)) (and#(tt(), X) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(activate(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__isNatIList(X)) -> isNatIList#(X), isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2)))) (activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__length(X)) -> activate#(X), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__length(X)) -> activate#(X), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (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))) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__length(X)) -> activate#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2))), and#(tt(), X) -> activate#(X)) (length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNat(N)), and#(tt(), X) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> activate#(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)) -> activate#(X1)) (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)) -> activate#(X1)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (length#(cons(N, L)) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (length#(cons(N, L)) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__isNatIList(X)) -> isNatIList#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (length#(cons(N, L)) -> activate#(L), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) } 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#(activate(X)), activate#(n__length(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(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#(activate(X)), activate#(n__length(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(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(activate(X1), activate(X2)), activate(n__0()) -> 0(), activate(n__length(X)) -> length(activate(X)), activate(n__s(X)) -> s(activate(X)), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(activate(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(n__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#) = [0,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(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: [and#](x0, x1) = x0 + x1, [n__and](x0, x1) = x0 + x1, [n__cons](x0, x1) = x0 + x1, [cons](x0, x1) = x0 + x1, [n__length](x0) = x0 + 1, [tt] = 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__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(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(activate(X1), activate(X2)), activate(n__0()) -> 0(), activate(n__length(X)) -> length(activate(X)), activate(n__s(X)) -> s(activate(X)), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(activate(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(n__isNat(M), n__isNat(N))), activate(IL), M, N)} EDG: {(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)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__s(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__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (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__cons(X1, X2)) -> activate#(X1)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__s(X)) -> activate#(X), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (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#(activate(X1), X2)) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> activate#(X1)) (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__cons(X1, X2)) -> activate#(X1)) (and#(tt(), X) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U11#(tt(), L) -> activate#(L), activate#(n__and(X1, X2)) -> activate#(X1)) (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__cons(X1, X2)) -> activate#(X1)) (U11#(tt(), L) -> activate#(L), activate#(n__isNatIList(X)) -> isNatIList#(X)) (U11#(tt(), L) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (isNatIList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatIList(activate(V2))), and#(tt(), X) -> activate#(X)) (activate#(n__and(X1, X2)) -> and#(activate(X1), X2), and#(tt(), X) -> activate#(X)) (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__s(X)) -> activate#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__isNatIList(X)) -> isNatIList#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (length#(cons(N, L)) -> activate#(L), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (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)))) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> activate#(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)) -> activate#(X1)) (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)) -> activate#(X1)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(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__s(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__cons(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(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)))} SCCS: Scc: { activate#(n__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(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__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(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(activate(X1), activate(X2)), activate(n__0()) -> 0(), activate(n__length(X)) -> length(activate(X)), activate(n__s(X)) -> s(activate(X)), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(activate(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(n__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) = [], 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__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(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(activate(X1), activate(X2)), activate(n__0()) -> 0(), activate(n__length(X)) -> length(activate(X)), activate(n__s(X)) -> s(activate(X)), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(activate(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(n__isNat(M), n__isNat(N))), activate(IL), M, N)} EDG: {(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__and(X1, X2)) -> and#(activate(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)) (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)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatIList(X)) -> isNatIList#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(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__s(X)) -> activate#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (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)) -> activate#(X1)) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (activate#(n__isNatList(X)) -> isNatList#(X), isNatList#(n__cons(V1, V2)) -> and#(isNat(activate(V1)), n__isNatList(activate(V2)))) (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNatList(X)) -> isNatList#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__and(X1, X2)) -> and#(activate(X1), X2))} SCCS: Scc: { activate#(n__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(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__s(X)) -> activate#(X), activate#(n__isNatIList(X)) -> isNatIList#(X), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatList(X)) -> isNatList#(X), activate#(n__isNat(X)) -> isNat#(X), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(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(activate(X1), activate(X2)), activate(n__0()) -> 0(), activate(n__length(X)) -> length(activate(X)), activate(n__s(X)) -> s(activate(X)), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(activate(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(n__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(activate(X1), activate(X2)), activate(n__0()) -> 0(), activate(n__length(X)) -> length(activate(X)), activate(n__s(X)) -> s(activate(X)), activate(n__isNatIList(X)) -> isNatIList(X), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__isNatList(X)) -> isNatList(X), activate(n__isNat(X)) -> isNat(X), activate(n__and(X1, X2)) -> and(activate(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(n__isNat(M), n__isNat(N))), activate(IL), M, N)} Fail