MAYBE TRS: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12(tt()) -> tt(), isNatList(n__take(V1, V2)) -> U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), isNatList(n__cons(V1, V2)) -> U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), isNatList(n__nil()) -> tt(), 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__isNatIListKind(X)) -> isNatIListKind(X), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__and(X1, X2)) -> and(activate(X1), X2), activate(n__isNat(X)) -> isNat(X), activate(n__isNatKind(X)) -> isNatKind(X), U11(tt(), V1) -> U12(isNatList(activate(V1))), U22(tt()) -> tt(), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)), isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)), U21(tt(), V1) -> U22(isNat(activate(V1))), U32(tt()) -> tt(), U31(tt(), V) -> U32(isNatList(activate(V))), U42(tt(), V2) -> U43(isNatIList(activate(V2))), U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2)), U43(tt()) -> tt(), isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), U52(tt(), V2) -> U53(isNatList(activate(V2))), U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2)), U53(tt()) -> tt(), U62(tt(), V2) -> U63(isNatIList(activate(V2))), U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2)), U63(tt()) -> tt(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L)), length(nil()) -> 0(), U71(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U81(tt()) -> nil(), U91(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), isNatIListKind(X) -> n__isNatIListKind(X), isNatIListKind(n__zeros()) -> tt(), isNatIListKind(n__take(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatIListKind(n__cons(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatIListKind(n__nil()) -> tt(), isNatKind(X) -> n__isNatKind(X), isNatKind(n__0()) -> tt(), isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)), isNatKind(n__s(V1)) -> isNatKind(activate(V1)), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL))), take(s(M), cons(N, IL)) -> U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N)))), activate(IL), M, N)} DP: Strict: { zeros#() -> cons#(0(), n__zeros()), zeros#() -> 0#(), isNatList#(n__take(V1, V2)) -> activate#(V1), isNatList#(n__take(V1, V2)) -> activate#(V2), isNatList#(n__take(V1, V2)) -> U61#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), isNatList#(n__take(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatList#(n__take(V1, V2)) -> isNatKind#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), isNatList#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatList#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), 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)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X)), activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__nil()) -> nil#(), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2), activate#(n__isNat(X)) -> isNat#(X), activate#(n__isNatKind(X)) -> isNatKind#(X), U11#(tt(), V1) -> U12#(isNatList(activate(V1))), U11#(tt(), V1) -> isNatList#(activate(V1)), U11#(tt(), V1) -> activate#(V1), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)), activate(V1)), isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1)), U21#(tt(), V1) -> activate#(V1), U21#(tt(), V1) -> U22#(isNat(activate(V1))), U21#(tt(), V1) -> isNat#(activate(V1)), U31#(tt(), V) -> isNatList#(activate(V)), U31#(tt(), V) -> activate#(V), U31#(tt(), V) -> U32#(isNatList(activate(V))), U42#(tt(), V2) -> activate#(V2), U42#(tt(), V2) -> U43#(isNatIList(activate(V2))), U42#(tt(), V2) -> isNatIList#(activate(V2)), U41#(tt(), V1, V2) -> activate#(V1), U41#(tt(), V1, V2) -> activate#(V2), U41#(tt(), V1, V2) -> isNat#(activate(V1)), U41#(tt(), V1, V2) -> U42#(isNat(activate(V1)), activate(V2)), isNatIList#(V) -> activate#(V), isNatIList#(V) -> U31#(isNatIListKind(activate(V)), activate(V)), isNatIList#(V) -> isNatIListKind#(activate(V)), isNatIList#(n__cons(V1, V2)) -> activate#(V1), isNatIList#(n__cons(V1, V2)) -> activate#(V2), isNatIList#(n__cons(V1, V2)) -> U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), isNatIList#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatIList#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), U52#(tt(), V2) -> isNatList#(activate(V2)), U52#(tt(), V2) -> activate#(V2), U52#(tt(), V2) -> U53#(isNatList(activate(V2))), U51#(tt(), V1, V2) -> activate#(V1), U51#(tt(), V1, V2) -> activate#(V2), U51#(tt(), V1, V2) -> isNat#(activate(V1)), U51#(tt(), V1, V2) -> U52#(isNat(activate(V1)), activate(V2)), U62#(tt(), V2) -> activate#(V2), U62#(tt(), V2) -> isNatIList#(activate(V2)), U62#(tt(), V2) -> U63#(isNatIList(activate(V2))), U61#(tt(), V1, V2) -> activate#(V1), U61#(tt(), V1, V2) -> activate#(V2), U61#(tt(), V1, V2) -> isNat#(activate(V1)), U61#(tt(), V1, V2) -> U62#(isNat(activate(V1)), activate(V2)), length#(cons(N, L)) -> isNatList#(activate(L)), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> U71#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNatIListKind(activate(L))), length#(cons(N, L)) -> and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), length#(nil()) -> 0#(), U71#(tt(), L) -> activate#(L), U71#(tt(), L) -> s#(length(activate(L))), U71#(tt(), L) -> length#(activate(L)), U81#(tt()) -> nil#(), U91#(tt(), IL, M, N) -> cons#(activate(N), n__take(activate(M), activate(IL))), U91#(tt(), IL, M, N) -> activate#(N), U91#(tt(), IL, M, N) -> activate#(M), U91#(tt(), IL, M, N) -> activate#(IL), and#(tt(), X) -> activate#(X), isNatIListKind#(n__take(V1, V2)) -> activate#(V1), isNatIListKind#(n__take(V1, V2)) -> activate#(V2), isNatIListKind#(n__take(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatIListKind#(n__take(V1, V2)) -> isNatKind#(activate(V1)), isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), isNatIListKind#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatIListKind#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__length(V1)) -> activate#(V1), isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), take#(0(), IL) -> isNatIList#(IL), take#(0(), IL) -> U81#(and(isNatIList(IL), n__isNatIListKind(IL))), take#(0(), IL) -> and#(isNatIList(IL), n__isNatIListKind(IL)), take#(s(M), cons(N, IL)) -> activate#(IL), take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), take#(s(M), cons(N, IL)) -> U91#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N)))), activate(IL), M, N), take#(s(M), cons(N, IL)) -> and#(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), take#(s(M), cons(N, IL)) -> and#(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12(tt()) -> tt(), isNatList(n__take(V1, V2)) -> U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), isNatList(n__cons(V1, V2)) -> U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), isNatList(n__nil()) -> tt(), 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__isNatIListKind(X)) -> isNatIListKind(X), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__and(X1, X2)) -> and(activate(X1), X2), activate(n__isNat(X)) -> isNat(X), activate(n__isNatKind(X)) -> isNatKind(X), U11(tt(), V1) -> U12(isNatList(activate(V1))), U22(tt()) -> tt(), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)), isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)), U21(tt(), V1) -> U22(isNat(activate(V1))), U32(tt()) -> tt(), U31(tt(), V) -> U32(isNatList(activate(V))), U42(tt(), V2) -> U43(isNatIList(activate(V2))), U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2)), U43(tt()) -> tt(), isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), U52(tt(), V2) -> U53(isNatList(activate(V2))), U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2)), U53(tt()) -> tt(), U62(tt(), V2) -> U63(isNatIList(activate(V2))), U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2)), U63(tt()) -> tt(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L)), length(nil()) -> 0(), U71(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U81(tt()) -> nil(), U91(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), isNatIListKind(X) -> n__isNatIListKind(X), isNatIListKind(n__zeros()) -> tt(), isNatIListKind(n__take(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatIListKind(n__cons(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatIListKind(n__nil()) -> tt(), isNatKind(X) -> n__isNatKind(X), isNatKind(n__0()) -> tt(), isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)), isNatKind(n__s(V1)) -> isNatKind(activate(V1)), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL))), take(s(M), cons(N, IL)) -> U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N)))), activate(IL), M, N)} EDG: { (isNatList#(n__take(V1, V2)) -> U61#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), U61#(tt(), V1, V2) -> U62#(isNat(activate(V1)), activate(V2))) (isNatList#(n__take(V1, V2)) -> U61#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), U61#(tt(), V1, V2) -> isNat#(activate(V1))) (isNatList#(n__take(V1, V2)) -> U61#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), U61#(tt(), V1, V2) -> activate#(V2)) (isNatList#(n__take(V1, V2)) -> U61#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), U61#(tt(), V1, V2) -> activate#(V1)) (isNatIList#(n__cons(V1, V2)) -> U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), U41#(tt(), V1, V2) -> U42#(isNat(activate(V1)), activate(V2))) (isNatIList#(n__cons(V1, V2)) -> U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), U41#(tt(), V1, V2) -> isNat#(activate(V1))) (isNatIList#(n__cons(V1, V2)) -> U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), U41#(tt(), V1, V2) -> activate#(V2)) (isNatIList#(n__cons(V1, V2)) -> U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), U41#(tt(), V1, V2) -> activate#(V1)) (U31#(tt(), V) -> activate#(V), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U31#(tt(), V) -> activate#(V), activate#(n__isNat(X)) -> isNat#(X)) (U31#(tt(), V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U31#(tt(), V) -> activate#(V), activate#(n__and(X1, X2)) -> activate#(X1)) (U31#(tt(), V) -> activate#(V), activate#(n__nil()) -> nil#()) (U31#(tt(), V) -> activate#(V), activate#(n__cons(X1, X2)) -> activate#(X1)) (U31#(tt(), V) -> activate#(V), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U31#(tt(), V) -> activate#(V), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (U31#(tt(), V) -> activate#(V), activate#(n__s(X)) -> s#(activate(X))) (U31#(tt(), V) -> activate#(V), activate#(n__s(X)) -> activate#(X)) (U31#(tt(), V) -> activate#(V), activate#(n__length(X)) -> length#(activate(X))) (U31#(tt(), V) -> activate#(V), activate#(n__length(X)) -> activate#(X)) (U31#(tt(), V) -> activate#(V), activate#(n__0()) -> 0#()) (U31#(tt(), V) -> activate#(V), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U31#(tt(), V) -> activate#(V), activate#(n__take(X1, X2)) -> activate#(X2)) (U31#(tt(), V) -> activate#(V), activate#(n__take(X1, X2)) -> activate#(X1)) (U31#(tt(), V) -> activate#(V), activate#(n__zeros()) -> zeros#()) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__isNatKind(X)) -> isNatKind#(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)) -> and#(activate(X1), X2)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__nil()) -> nil#()) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__cons(X1, X2)) -> activate#(X1)) (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__isNatIListKind(X)) -> isNatIListKind#(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__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__0()) -> 0#()) (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__take(X1, X2)) -> activate#(X2)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__take(X1, X2)) -> activate#(X1)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__zeros()) -> zeros#()) (activate#(n__zeros()) -> zeros#(), zeros#() -> 0#()) (activate#(n__zeros()) -> zeros#(), zeros#() -> cons#(0(), n__zeros())) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> isNatKind#(activate(V1))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> activate#(V2)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> activate#(V1)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(V) -> isNatIListKind#(activate(V))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(V) -> U31#(isNatIListKind(activate(V)), activate(V))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(V) -> activate#(V)) (isNatList#(n__take(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), and#(tt(), X) -> activate#(X)) (isNatIList#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), and#(tt(), X) -> activate#(X)) (isNatIListKind#(n__take(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), and#(tt(), X) -> activate#(X)) (take#(s(M), cons(N, IL)) -> and#(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), and#(tt(), X) -> activate#(X)) (U71#(tt(), L) -> activate#(L), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U71#(tt(), L) -> activate#(L), activate#(n__isNat(X)) -> isNat#(X)) (U71#(tt(), L) -> activate#(L), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U71#(tt(), L) -> activate#(L), activate#(n__and(X1, X2)) -> activate#(X1)) (U71#(tt(), L) -> activate#(L), activate#(n__nil()) -> nil#()) (U71#(tt(), L) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (U71#(tt(), L) -> activate#(L), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U71#(tt(), L) -> activate#(L), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (U71#(tt(), L) -> activate#(L), activate#(n__s(X)) -> s#(activate(X))) (U71#(tt(), L) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (U71#(tt(), L) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (U71#(tt(), L) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (U71#(tt(), L) -> activate#(L), activate#(n__0()) -> 0#()) (U71#(tt(), L) -> activate#(L), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U71#(tt(), L) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X2)) (U71#(tt(), L) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X1)) (U71#(tt(), L) -> activate#(L), activate#(n__zeros()) -> zeros#()) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(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__nil()) -> nil#()) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (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__isNatIListKind(X)) -> isNatIListKind#(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__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__0()) -> 0#()) (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__take(X1, X2)) -> activate#(X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (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__isNatIListKind(X)) -> isNatIListKind#(X)) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (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__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#()) (U21#(tt(), V1) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U21#(tt(), V1) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (U21#(tt(), V1) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U21#(tt(), V1) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (U21#(tt(), V1) -> activate#(V1), activate#(n__nil()) -> nil#()) (U21#(tt(), V1) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (U21#(tt(), V1) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U21#(tt(), V1) -> activate#(V1), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (U21#(tt(), V1) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (U21#(tt(), V1) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (U21#(tt(), V1) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (U21#(tt(), V1) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (U21#(tt(), V1) -> activate#(V1), activate#(n__0()) -> 0#()) (U21#(tt(), V1) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U21#(tt(), V1) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X2)) (U21#(tt(), V1) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (U21#(tt(), V1) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(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)) -> 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__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__isNatIListKind(X)) -> isNatIListKind#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(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__length(X)) -> 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#()) (U61#(tt(), V1, V2) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U61#(tt(), V1, V2) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (U61#(tt(), V1, V2) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U61#(tt(), V1, V2) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (U61#(tt(), V1, V2) -> activate#(V1), activate#(n__nil()) -> nil#()) (U61#(tt(), V1, V2) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (U61#(tt(), V1, V2) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U61#(tt(), V1, V2) -> activate#(V1), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (U61#(tt(), V1, V2) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (U61#(tt(), V1, V2) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (U61#(tt(), V1, V2) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (U61#(tt(), V1, V2) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (U61#(tt(), V1, V2) -> activate#(V1), activate#(n__0()) -> 0#()) (U61#(tt(), V1, V2) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U61#(tt(), V1, V2) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X2)) (U61#(tt(), V1, V2) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (U61#(tt(), V1, V2) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#()) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__nil()) -> nil#()) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatKind#(n__s(V1)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__isNatKind(X)) -> isNatKind#(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)) -> and#(activate(X1), X2)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__nil()) -> nil#()) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (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__isNatIListKind(X)) -> isNatIListKind#(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__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__0()) -> 0#()) (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__take(X1, X2)) -> activate#(X2)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X1)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__zeros()) -> zeros#()) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(s(M), cons(N, IL)) -> and#(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))))) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(s(M), cons(N, IL)) -> and#(isNatIList(activate(IL)), n__isNatIListKind(activate(IL)))) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(s(M), cons(N, IL)) -> U91#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N)))), activate(IL), M, N)) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(s(M), cons(N, IL)) -> isNatIList#(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)) -> take#(activate(X1), activate(X2)), take#(0(), IL) -> and#(isNatIList(IL), n__isNatIListKind(IL))) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(0(), IL) -> U81#(and(isNatIList(IL), n__isNatIListKind(IL)))) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(0(), IL) -> isNatIList#(IL)) (isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), U21#(tt(), V1) -> isNat#(activate(V1))) (isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), U21#(tt(), V1) -> U22#(isNat(activate(V1)))) (isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), U21#(tt(), V1) -> activate#(V1)) (isNatIList#(V) -> U31#(isNatIListKind(activate(V)), activate(V)), U31#(tt(), V) -> U32#(isNatList(activate(V)))) (isNatIList#(V) -> U31#(isNatIListKind(activate(V)), activate(V)), U31#(tt(), V) -> activate#(V)) (isNatIList#(V) -> U31#(isNatIListKind(activate(V)), activate(V)), U31#(tt(), V) -> isNatList#(activate(V))) (U61#(tt(), V1, V2) -> U62#(isNat(activate(V1)), activate(V2)), U62#(tt(), V2) -> U63#(isNatIList(activate(V2)))) (U61#(tt(), V1, V2) -> U62#(isNat(activate(V1)), activate(V2)), U62#(tt(), V2) -> isNatIList#(activate(V2))) (U61#(tt(), V1, V2) -> U62#(isNat(activate(V1)), activate(V2)), U62#(tt(), V2) -> activate#(V2)) (take#(0(), IL) -> and#(isNatIList(IL), n__isNatIListKind(IL)), and#(tt(), X) -> activate#(X)) (length#(cons(N, L)) -> and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), and#(tt(), X) -> activate#(X)) (take#(s(M), cons(N, IL)) -> and#(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N)))), and#(tt(), X) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(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__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__isNatIListKind(X)) -> isNatIListKind#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(activate(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)) -> length#(activate(X))) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> 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#()) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__and(X1, X2)) -> activate#(X1)) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__nil()) -> nil#()) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X2)) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X1)) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__zeros()) -> zeros#()) (U52#(tt(), V2) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U52#(tt(), V2) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (U52#(tt(), V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U52#(tt(), V2) -> activate#(V2), activate#(n__and(X1, X2)) -> activate#(X1)) (U52#(tt(), V2) -> activate#(V2), activate#(n__nil()) -> nil#()) (U52#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (U52#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U52#(tt(), V2) -> activate#(V2), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (U52#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (U52#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (U52#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (U52#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (U52#(tt(), V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U52#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U52#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X2)) (U52#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X1)) (U52#(tt(), V2) -> activate#(V2), activate#(n__zeros()) -> zeros#()) (U62#(tt(), V2) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U62#(tt(), V2) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (U62#(tt(), V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U62#(tt(), V2) -> activate#(V2), activate#(n__and(X1, X2)) -> activate#(X1)) (U62#(tt(), V2) -> activate#(V2), activate#(n__nil()) -> nil#()) (U62#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (U62#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U62#(tt(), V2) -> activate#(V2), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (U62#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (U62#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (U62#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (U62#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (U62#(tt(), V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U62#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U62#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X2)) (U62#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X1)) (U62#(tt(), V2) -> activate#(V2), activate#(n__zeros()) -> zeros#()) (isNatIListKind#(n__take(V1, V2)) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> activate#(X1)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#()) (isNatIListKind#(n__take(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V2), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (isNatIListKind#(n__take(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (isNatIListKind#(n__take(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (isNatIListKind#(n__take(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatIListKind#(n__take(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V2), activate#(n__zeros()) -> zeros#()) (activate#(n__and(X1, X2)) -> and#(activate(X1), X2), and#(tt(), X) -> activate#(X)) (take#(0(), IL) -> U81#(and(isNatIList(IL), n__isNatIListKind(IL))), U81#(tt()) -> nil#()) (U71#(tt(), L) -> length#(activate(L)), length#(nil()) -> 0#()) (U71#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N)))) (U71#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNatIListKind(activate(L)))) (U71#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> U71#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L))) (U71#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> activate#(L)) (U71#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L))) (U52#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> isNatKind#(activate(V1))) (U52#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (U52#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) (U52#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (U52#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (U52#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__take(V1, V2)) -> isNatKind#(activate(V1))) (U52#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__take(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (U52#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__take(V1, V2)) -> U61#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) (U52#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__take(V1, V2)) -> activate#(V2)) (U52#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__take(V1, V2)) -> activate#(V1)) (U31#(tt(), V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> isNatKind#(activate(V1))) (U31#(tt(), V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (U31#(tt(), V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) (U31#(tt(), V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (U31#(tt(), V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (U31#(tt(), V) -> isNatList#(activate(V)), isNatList#(n__take(V1, V2)) -> isNatKind#(activate(V1))) (U31#(tt(), V) -> isNatList#(activate(V)), isNatList#(n__take(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (U31#(tt(), V) -> isNatList#(activate(V)), isNatList#(n__take(V1, V2)) -> U61#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) (U31#(tt(), V) -> isNatList#(activate(V)), isNatList#(n__take(V1, V2)) -> activate#(V2)) (U31#(tt(), V) -> isNatList#(activate(V)), isNatList#(n__take(V1, V2)) -> activate#(V1)) (isNatList#(n__take(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (isNatList#(n__take(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNatList#(n__take(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1))) (isNatList#(n__take(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__length(V1)) -> activate#(V1)) (U11#(tt(), V1) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> isNatKind#(activate(V1))) (U11#(tt(), V1) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (U11#(tt(), V1) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) (U11#(tt(), V1) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (U11#(tt(), V1) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (U11#(tt(), V1) -> isNatList#(activate(V1)), isNatList#(n__take(V1, V2)) -> isNatKind#(activate(V1))) (U11#(tt(), V1) -> isNatList#(activate(V1)), isNatList#(n__take(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (U11#(tt(), V1) -> isNatList#(activate(V1)), isNatList#(n__take(V1, V2)) -> U61#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) (U11#(tt(), V1) -> isNatList#(activate(V1)), isNatList#(n__take(V1, V2)) -> activate#(V2)) (U11#(tt(), V1) -> isNatList#(activate(V1)), isNatList#(n__take(V1, V2)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1))) (isNat#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__length(V1)) -> activate#(V1)) (U41#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (U41#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U41#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (U41#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatIListKind#(activate(V1))) (U41#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)), activate(V1))) (U41#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (U51#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (U51#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U51#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (U51#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatIListKind#(activate(V1))) (U51#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)), activate(V1))) (U51#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (isNatIListKind#(n__take(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (isNatIListKind#(n__take(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNatIListKind#(n__take(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1))) (isNatIListKind#(n__take(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__length(V1)) -> activate#(V1)) (isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatIListKind#(n__cons(V1, V2)) -> isNatKind#(activate(V1))) (isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatIListKind#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatIListKind#(n__cons(V1, V2)) -> activate#(V2)) (isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatIListKind#(n__cons(V1, V2)) -> activate#(V1)) (isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatIListKind#(n__take(V1, V2)) -> isNatKind#(activate(V1))) (isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatIListKind#(n__take(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatIListKind#(n__take(V1, V2)) -> activate#(V2)) (isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatIListKind#(n__take(V1, V2)) -> activate#(V1)) (activate#(n__length(X)) -> activate#(X), activate#(n__isNatKind(X)) -> isNatKind#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (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__nil()) -> nil#()) (activate#(n__length(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__length(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (activate#(n__length(X)) -> activate#(X), activate#(n__isNatIListKind(X)) -> isNatIListKind#(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__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__0()) -> 0#()) (activate#(n__length(X)) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (activate#(n__length(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X2)) (activate#(n__length(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X1)) (activate#(n__length(X)) -> activate#(X), activate#(n__zeros()) -> zeros#()) (activate#(n__isNatIListKind(X)) -> isNatIListKind#(X), isNatIListKind#(n__cons(V1, V2)) -> isNatKind#(activate(V1))) (activate#(n__isNatIListKind(X)) -> isNatIListKind#(X), isNatIListKind#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (activate#(n__isNatIListKind(X)) -> isNatIListKind#(X), isNatIListKind#(n__cons(V1, V2)) -> activate#(V2)) (activate#(n__isNatIListKind(X)) -> isNatIListKind#(X), isNatIListKind#(n__cons(V1, V2)) -> activate#(V1)) (activate#(n__isNatIListKind(X)) -> isNatIListKind#(X), isNatIListKind#(n__take(V1, V2)) -> isNatKind#(activate(V1))) (activate#(n__isNatIListKind(X)) -> isNatIListKind#(X), isNatIListKind#(n__take(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (activate#(n__isNatIListKind(X)) -> isNatIListKind#(X), isNatIListKind#(n__take(V1, V2)) -> activate#(V2)) (activate#(n__isNatIListKind(X)) -> isNatIListKind#(X), isNatIListKind#(n__take(V1, V2)) -> activate#(V1)) (activate#(n__isNatKind(X)) -> isNatKind#(X), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (activate#(n__isNatKind(X)) -> isNatKind#(X), isNatKind#(n__s(V1)) -> activate#(V1)) (activate#(n__isNatKind(X)) -> isNatKind#(X), isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1))) (activate#(n__isNatKind(X)) -> isNatKind#(X), isNatKind#(n__length(V1)) -> activate#(V1)) (take#(s(M), cons(N, IL)) -> U91#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N)))), activate(IL), M, N), U91#(tt(), IL, M, N) -> activate#(IL)) (take#(s(M), cons(N, IL)) -> U91#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N)))), activate(IL), M, N), U91#(tt(), IL, M, N) -> activate#(M)) (take#(s(M), cons(N, IL)) -> U91#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N)))), activate(IL), M, N), U91#(tt(), IL, M, N) -> activate#(N)) (take#(s(M), cons(N, IL)) -> U91#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N)))), activate(IL), M, N), U91#(tt(), IL, M, N) -> cons#(activate(N), n__take(activate(M), activate(IL)))) (and#(tt(), X) -> activate#(X), activate#(n__zeros()) -> zeros#()) (and#(tt(), X) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X1)) (and#(tt(), X) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X2)) (and#(tt(), X) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (and#(tt(), X) -> activate#(X), activate#(n__0()) -> 0#()) (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__s(X)) -> activate#(X)) (and#(tt(), X) -> activate#(X), activate#(n__s(X)) -> s#(activate(X))) (and#(tt(), X) -> activate#(X), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (and#(tt(), X) -> activate#(X), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (and#(tt(), X) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (and#(tt(), X) -> activate#(X), activate#(n__nil()) -> nil#()) (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)) (and#(tt(), X) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNatKind(X)) -> isNatKind#(X)) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__length(V1)) -> activate#(V1)) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)), activate(V1))) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__length(V1)) -> isNatIListKind#(activate(V1))) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> activate#(V1)) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (activate#(n__s(X)) -> activate#(X), activate#(n__zeros()) -> zeros#()) (activate#(n__s(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X2)) (activate#(n__s(X)) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (activate#(n__s(X)) -> activate#(X), activate#(n__0()) -> 0#()) (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__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__isNatIListKind(X)) -> isNatIListKind#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__nil()) -> nil#()) (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)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__length(V1)) -> activate#(V1)) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1))) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (isNatIListKind#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__length(V1)) -> activate#(V1)) (isNatIListKind#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1))) (isNatIListKind#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNatIListKind#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U61#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (U61#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)), activate(V1))) (U61#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatIListKind#(activate(V1))) (U61#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (U61#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U61#(tt(), V1, V2) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (isNatIList#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__length(V1)) -> activate#(V1)) (isNatIList#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1))) (isNatIList#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNatIList#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (U21#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (U21#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)), activate(V1))) (U21#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatIListKind#(activate(V1))) (U21#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (U21#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1))) (U21#(tt(), V1) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1))) (isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatIListKind#(n__take(V1, V2)) -> activate#(V1)) (isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatIListKind#(n__take(V1, V2)) -> activate#(V2)) (isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatIListKind#(n__take(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatIListKind#(n__take(V1, V2)) -> isNatKind#(activate(V1))) (isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatIListKind#(n__cons(V1, V2)) -> activate#(V1)) (isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatIListKind#(n__cons(V1, V2)) -> activate#(V2)) (isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatIListKind#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatIListKind#(n__cons(V1, V2)) -> isNatKind#(activate(V1))) (isNatList#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__length(V1)) -> activate#(V1)) (isNatList#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1))) (isNatList#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1)) (isNatList#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1))) (isNatIList#(V) -> isNatIListKind#(activate(V)), isNatIListKind#(n__take(V1, V2)) -> activate#(V1)) (isNatIList#(V) -> isNatIListKind#(activate(V)), isNatIListKind#(n__take(V1, V2)) -> activate#(V2)) (isNatIList#(V) -> isNatIListKind#(activate(V)), isNatIListKind#(n__take(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (isNatIList#(V) -> isNatIListKind#(activate(V)), isNatIListKind#(n__take(V1, V2)) -> isNatKind#(activate(V1))) (isNatIList#(V) -> isNatIListKind#(activate(V)), isNatIListKind#(n__cons(V1, V2)) -> activate#(V1)) (isNatIList#(V) -> isNatIListKind#(activate(V)), isNatIListKind#(n__cons(V1, V2)) -> activate#(V2)) (isNatIList#(V) -> isNatIListKind#(activate(V)), isNatIListKind#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (isNatIList#(V) -> isNatIListKind#(activate(V)), isNatIListKind#(n__cons(V1, V2)) -> isNatKind#(activate(V1))) (U62#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> activate#(V)) (U62#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> U31#(isNatIListKind(activate(V)), activate(V))) (U62#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> isNatIListKind#(activate(V))) (U62#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V1)) (U62#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V2)) (U62#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) (U62#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (U62#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> isNatKind#(activate(V1))) (U42#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> activate#(V)) (U42#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> U31#(isNatIListKind(activate(V)), activate(V))) (U42#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> isNatIListKind#(activate(V))) (U42#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V1)) (U42#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V2)) (U42#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) (U42#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (U42#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> isNatKind#(activate(V1))) (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)) -> U61#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(V1, V2)) -> isNatKind#(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)) -> U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> isNatKind#(activate(V1))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(V) -> activate#(V)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(V) -> U31#(isNatIListKind(activate(V)), activate(V))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(V) -> isNatIListKind#(activate(V))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> activate#(V1)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> activate#(V2)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> isNatKind#(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)) -> activate#(L)) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> U71#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L))) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNatIListKind(activate(L)))) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N)))) (activate#(n__length(X)) -> length#(activate(X)), length#(nil()) -> 0#()) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), activate#(n__zeros()) -> zeros#()) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#()) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#()) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> activate#(X1)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U61#(tt(), V1, V2) -> activate#(V2), activate#(n__zeros()) -> zeros#()) (U61#(tt(), V1, V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X1)) (U61#(tt(), V1, V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X2)) (U61#(tt(), V1, V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U61#(tt(), V1, V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U61#(tt(), V1, V2) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (U61#(tt(), V1, V2) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (U61#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (U61#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (U61#(tt(), V1, V2) -> activate#(V2), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (U61#(tt(), V1, V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U61#(tt(), V1, V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (U61#(tt(), V1, V2) -> activate#(V2), activate#(n__nil()) -> nil#()) (U61#(tt(), V1, V2) -> activate#(V2), activate#(n__and(X1, X2)) -> activate#(X1)) (U61#(tt(), V1, V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U61#(tt(), V1, V2) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (U61#(tt(), V1, V2) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__zeros()) -> zeros#()) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X1)) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X2)) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__nil()) -> nil#()) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__and(X1, X2)) -> activate#(X1)) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (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)) -> activate#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__s(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__isNatIListKind(X)) -> isNatIListKind#(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__and(X1, X2)) -> activate#(X1)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U42#(tt(), V2) -> activate#(V2), activate#(n__zeros()) -> zeros#()) (U42#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X1)) (U42#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X2)) (U42#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U42#(tt(), V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U42#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (U42#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (U42#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (U42#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (U42#(tt(), V2) -> activate#(V2), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (U42#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U42#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (U42#(tt(), V2) -> activate#(V2), activate#(n__nil()) -> nil#()) (U42#(tt(), V2) -> activate#(V2), activate#(n__and(X1, X2)) -> activate#(X1)) (U42#(tt(), V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U42#(tt(), V2) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (U42#(tt(), V2) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (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)) -> activate#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__s(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__isNatIListKind(X)) -> isNatIListKind#(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__and(X1, X2)) -> activate#(X1)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__zeros()) -> zeros#()) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> activate#(X1)) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> activate#(X2)) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__0()) -> 0#()) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> activate#(X)) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> length#(activate(X))) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__s(X)) -> activate#(X)) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__s(X)) -> s#(activate(X))) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__cons(X1, X2)) -> activate#(X1)) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__nil()) -> nil#()) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__and(X1, X2)) -> activate#(X1)) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__isNat(X)) -> isNat#(X)) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__isNatKind(X)) -> isNatKind#(X)) (length#(cons(N, L)) -> U71#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L)), U71#(tt(), L) -> activate#(L)) (length#(cons(N, L)) -> U71#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L)), U71#(tt(), L) -> s#(length(activate(L)))) (length#(cons(N, L)) -> U71#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L)), U71#(tt(), L) -> length#(activate(L))) (U51#(tt(), V1, V2) -> U52#(isNat(activate(V1)), activate(V2)), U52#(tt(), V2) -> isNatList#(activate(V2))) (U51#(tt(), V1, V2) -> U52#(isNat(activate(V1)), activate(V2)), U52#(tt(), V2) -> activate#(V2)) (U51#(tt(), V1, V2) -> U52#(isNat(activate(V1)), activate(V2)), U52#(tt(), V2) -> U53#(isNatList(activate(V2)))) (U41#(tt(), V1, V2) -> U42#(isNat(activate(V1)), activate(V2)), U42#(tt(), V2) -> activate#(V2)) (U41#(tt(), V1, V2) -> U42#(isNat(activate(V1)), activate(V2)), U42#(tt(), V2) -> U43#(isNatIList(activate(V2)))) (U41#(tt(), V1, V2) -> U42#(isNat(activate(V1)), activate(V2)), U42#(tt(), V2) -> isNatIList#(activate(V2))) (isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)), activate(V1)), U11#(tt(), V1) -> U12#(isNatList(activate(V1)))) (isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)), activate(V1)), U11#(tt(), V1) -> isNatList#(activate(V1))) (isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)), activate(V1)), U11#(tt(), V1) -> activate#(V1)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__zeros()) -> zeros#()) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X1)) (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)) -> take#(activate(X1), activate(X2))) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__0()) -> 0#()) (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__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__isNatIListKind(X)) -> isNatIListKind#(X)) (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__cons(X1, X2)) -> activate#(X1)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__nil()) -> nil#()) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1)) (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__isNat(X)) -> isNat#(X)) (activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__zeros()) -> zeros#()) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X1)) (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)) -> take#(activate(X1), activate(X2))) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__0()) -> 0#()) (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__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__isNatIListKind(X)) -> isNatIListKind#(X)) (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__cons(X1, X2)) -> activate#(X1)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__nil()) -> nil#()) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1)) (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__isNat(X)) -> isNat#(X)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNatKind#(n__length(V1)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (isNatKind#(n__length(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatKind#(n__length(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatKind#(n__length(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatKind#(n__length(V1)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatKind#(n__length(V1)) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (isNatKind#(n__length(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (isNatKind#(n__length(V1)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNatKind#(n__length(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNatKind#(n__length(V1)) -> activate#(V1), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (isNatKind#(n__length(V1)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatKind#(n__length(V1)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatKind#(n__length(V1)) -> activate#(V1), activate#(n__nil()) -> nil#()) (isNatKind#(n__length(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (isNatKind#(n__length(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatKind#(n__length(V1)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNatKind#(n__length(V1)) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (isNatIListKind#(n__take(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatIListKind#(n__take(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatIListKind#(n__take(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (isNatIListKind#(n__take(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNatIListKind#(n__take(V1, V2)) -> activate#(V1), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#()) (isNatIListKind#(n__take(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNatIListKind#(n__take(V1, V2)) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X2)) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__0()) -> 0#()) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__nil()) -> nil#()) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X2)) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__0()) -> 0#()) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__nil()) -> nil#()) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (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)) -> activate#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatIListKind(X)) -> isNatIListKind#(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__and(X1, X2)) -> activate#(X1)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U11#(tt(), V1) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (U11#(tt(), V1) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (U11#(tt(), V1) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X2)) (U11#(tt(), V1) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U11#(tt(), V1) -> activate#(V1), activate#(n__0()) -> 0#()) (U11#(tt(), V1) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (U11#(tt(), V1) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (U11#(tt(), V1) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (U11#(tt(), V1) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (U11#(tt(), V1) -> activate#(V1), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (U11#(tt(), V1) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U11#(tt(), V1) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (U11#(tt(), V1) -> activate#(V1), activate#(n__nil()) -> nil#()) (U11#(tt(), V1) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (U11#(tt(), V1) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U11#(tt(), V1) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X)) (U11#(tt(), V1) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (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)) -> take#(activate(X1), activate(X2))) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (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__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__isNatIListKind(X)) -> isNatIListKind#(X)) (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__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#()) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> activate#(X1)) (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__isNat(X)) -> isNat#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__isNatKind(X)) -> isNatKind#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__zeros()) -> zeros#()) (length#(cons(N, L)) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X1)) (length#(cons(N, L)) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X2)) (length#(cons(N, L)) -> activate#(L), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (length#(cons(N, L)) -> activate#(L), activate#(n__0()) -> 0#()) (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__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__isNatIListKind(X)) -> isNatIListKind#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (length#(cons(N, L)) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (length#(cons(N, L)) -> activate#(L), activate#(n__nil()) -> nil#()) (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)) (length#(cons(N, L)) -> activate#(L), activate#(n__isNat(X)) -> isNat#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNatIListKind#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), and#(tt(), X) -> activate#(X)) (length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNatIListKind(activate(L))), and#(tt(), X) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), and#(tt(), X) -> activate#(X)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__zeros()) -> zeros#()) (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__take(X1, X2)) -> 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)) -> activate#(IL), activate#(n__0()) -> 0#()) (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__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__isNatIListKind(X)) -> isNatIListKind#(X)) (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__cons(X1, X2)) -> activate#(X1)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__nil()) -> nil#()) (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__and(X1, X2)) -> and#(activate(X1), X2)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__isNat(X)) -> isNat#(X)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__isNatKind(X)) -> isNatKind#(X)) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__zeros()) -> zeros#()) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X1)) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X2)) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__0()) -> 0#()) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> activate#(X)) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> length#(activate(X))) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__s(X)) -> activate#(X)) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__s(X)) -> s#(activate(X))) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__cons(X1, X2)) -> activate#(X1)) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__nil()) -> nil#()) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__and(X1, X2)) -> activate#(X1)) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__isNat(X)) -> isNat#(X)) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNatIList#(V) -> activate#(V), activate#(n__zeros()) -> zeros#()) (isNatIList#(V) -> activate#(V), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatIList#(V) -> activate#(V), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatIList#(V) -> activate#(V), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatIList#(V) -> activate#(V), activate#(n__0()) -> 0#()) (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__s(X)) -> activate#(X)) (isNatIList#(V) -> activate#(V), activate#(n__s(X)) -> s#(activate(X))) (isNatIList#(V) -> activate#(V), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (isNatIList#(V) -> activate#(V), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatIList#(V) -> activate#(V), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatIList#(V) -> activate#(V), activate#(n__nil()) -> nil#()) (isNatIList#(V) -> activate#(V), activate#(n__and(X1, X2)) -> activate#(X1)) (isNatIList#(V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (isNatIList#(V) -> activate#(V), activate#(n__isNat(X)) -> isNat#(X)) (isNatIList#(V) -> activate#(V), activate#(n__isNatKind(X)) -> isNatKind#(X)) (isNatList#(n__cons(V1, V2)) -> U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), U51#(tt(), V1, V2) -> activate#(V1)) (isNatList#(n__cons(V1, V2)) -> U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), U51#(tt(), V1, V2) -> activate#(V2)) (isNatList#(n__cons(V1, V2)) -> U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), U51#(tt(), V1, V2) -> isNat#(activate(V1))) (isNatList#(n__cons(V1, V2)) -> U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), U51#(tt(), V1, V2) -> U52#(isNat(activate(V1)), activate(V2))) (U91#(tt(), IL, M, N) -> activate#(N), activate#(n__zeros()) -> zeros#()) (U91#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X1)) (U91#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X2)) (U91#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U91#(tt(), IL, M, N) -> activate#(N), activate#(n__0()) -> 0#()) (U91#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (U91#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> length#(activate(X))) (U91#(tt(), IL, M, N) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (U91#(tt(), IL, M, N) -> activate#(N), activate#(n__s(X)) -> s#(activate(X))) (U91#(tt(), IL, M, N) -> activate#(N), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X)) (U91#(tt(), IL, M, N) -> activate#(N), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U91#(tt(), IL, M, N) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (U91#(tt(), IL, M, N) -> activate#(N), activate#(n__nil()) -> nil#()) (U91#(tt(), IL, M, N) -> activate#(N), activate#(n__and(X1, X2)) -> activate#(X1)) (U91#(tt(), IL, M, N) -> activate#(N), activate#(n__and(X1, X2)) -> and#(activate(X1), X2)) (U91#(tt(), IL, M, N) -> activate#(N), activate#(n__isNat(X)) -> isNat#(X)) (U91#(tt(), IL, M, N) -> activate#(N), activate#(n__isNatKind(X)) -> isNatKind#(X)) } SCCS: Scc: { isNatList#(n__take(V1, V2)) -> activate#(V1), isNatList#(n__take(V1, V2)) -> activate#(V2), isNatList#(n__take(V1, V2)) -> U61#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), isNatList#(n__take(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatList#(n__take(V1, V2)) -> isNatKind#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), isNatList#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatList#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), 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)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X)), activate#(n__s(X)) -> activate#(X), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2), activate#(n__isNat(X)) -> isNat#(X), activate#(n__isNatKind(X)) -> isNatKind#(X), U11#(tt(), V1) -> isNatList#(activate(V1)), U11#(tt(), V1) -> activate#(V1), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)), activate(V1)), isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1)), U21#(tt(), V1) -> activate#(V1), U21#(tt(), V1) -> isNat#(activate(V1)), U31#(tt(), V) -> isNatList#(activate(V)), U31#(tt(), V) -> activate#(V), U42#(tt(), V2) -> activate#(V2), U42#(tt(), V2) -> isNatIList#(activate(V2)), U41#(tt(), V1, V2) -> activate#(V1), U41#(tt(), V1, V2) -> activate#(V2), U41#(tt(), V1, V2) -> isNat#(activate(V1)), U41#(tt(), V1, V2) -> U42#(isNat(activate(V1)), activate(V2)), isNatIList#(V) -> activate#(V), isNatIList#(V) -> U31#(isNatIListKind(activate(V)), activate(V)), isNatIList#(V) -> isNatIListKind#(activate(V)), isNatIList#(n__cons(V1, V2)) -> activate#(V1), isNatIList#(n__cons(V1, V2)) -> activate#(V2), isNatIList#(n__cons(V1, V2)) -> U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), isNatIList#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatIList#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), U52#(tt(), V2) -> isNatList#(activate(V2)), U52#(tt(), V2) -> activate#(V2), U51#(tt(), V1, V2) -> activate#(V1), U51#(tt(), V1, V2) -> activate#(V2), U51#(tt(), V1, V2) -> isNat#(activate(V1)), U51#(tt(), V1, V2) -> U52#(isNat(activate(V1)), activate(V2)), U62#(tt(), V2) -> activate#(V2), U62#(tt(), V2) -> isNatIList#(activate(V2)), U61#(tt(), V1, V2) -> activate#(V1), U61#(tt(), V1, V2) -> activate#(V2), U61#(tt(), V1, V2) -> isNat#(activate(V1)), U61#(tt(), V1, V2) -> U62#(isNat(activate(V1)), activate(V2)), length#(cons(N, L)) -> isNatList#(activate(L)), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> U71#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNatIListKind(activate(L))), length#(cons(N, L)) -> and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), U71#(tt(), L) -> activate#(L), U71#(tt(), L) -> length#(activate(L)), U91#(tt(), IL, M, N) -> activate#(N), U91#(tt(), IL, M, N) -> activate#(M), U91#(tt(), IL, M, N) -> activate#(IL), and#(tt(), X) -> activate#(X), isNatIListKind#(n__take(V1, V2)) -> activate#(V1), isNatIListKind#(n__take(V1, V2)) -> activate#(V2), isNatIListKind#(n__take(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatIListKind#(n__take(V1, V2)) -> isNatKind#(activate(V1)), isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), isNatIListKind#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatIListKind#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__length(V1)) -> activate#(V1), isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), take#(0(), IL) -> isNatIList#(IL), take#(0(), IL) -> and#(isNatIList(IL), n__isNatIListKind(IL)), take#(s(M), cons(N, IL)) -> activate#(IL), take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), take#(s(M), cons(N, IL)) -> U91#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N)))), activate(IL), M, N), take#(s(M), cons(N, IL)) -> and#(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), take#(s(M), cons(N, IL)) -> and#(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))))} SCC: Strict: { isNatList#(n__take(V1, V2)) -> activate#(V1), isNatList#(n__take(V1, V2)) -> activate#(V2), isNatList#(n__take(V1, V2)) -> U61#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), isNatList#(n__take(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatList#(n__take(V1, V2)) -> isNatKind#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), isNatList#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatList#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), 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)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X)), activate#(n__s(X)) -> activate#(X), activate#(n__isNatIListKind(X)) -> isNatIListKind#(X), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> activate#(X1), activate#(n__and(X1, X2)) -> and#(activate(X1), X2), activate#(n__isNat(X)) -> isNat#(X), activate#(n__isNatKind(X)) -> isNatKind#(X), U11#(tt(), V1) -> isNatList#(activate(V1)), U11#(tt(), V1) -> activate#(V1), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> U11#(isNatIListKind(activate(V1)), activate(V1)), isNat#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> U21#(isNatKind(activate(V1)), activate(V1)), isNat#(n__s(V1)) -> isNatKind#(activate(V1)), U21#(tt(), V1) -> activate#(V1), U21#(tt(), V1) -> isNat#(activate(V1)), U31#(tt(), V) -> isNatList#(activate(V)), U31#(tt(), V) -> activate#(V), U42#(tt(), V2) -> activate#(V2), U42#(tt(), V2) -> isNatIList#(activate(V2)), U41#(tt(), V1, V2) -> activate#(V1), U41#(tt(), V1, V2) -> activate#(V2), U41#(tt(), V1, V2) -> isNat#(activate(V1)), U41#(tt(), V1, V2) -> U42#(isNat(activate(V1)), activate(V2)), isNatIList#(V) -> activate#(V), isNatIList#(V) -> U31#(isNatIListKind(activate(V)), activate(V)), isNatIList#(V) -> isNatIListKind#(activate(V)), isNatIList#(n__cons(V1, V2)) -> activate#(V1), isNatIList#(n__cons(V1, V2)) -> activate#(V2), isNatIList#(n__cons(V1, V2)) -> U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), isNatIList#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatIList#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), U52#(tt(), V2) -> isNatList#(activate(V2)), U52#(tt(), V2) -> activate#(V2), U51#(tt(), V1, V2) -> activate#(V1), U51#(tt(), V1, V2) -> activate#(V2), U51#(tt(), V1, V2) -> isNat#(activate(V1)), U51#(tt(), V1, V2) -> U52#(isNat(activate(V1)), activate(V2)), U62#(tt(), V2) -> activate#(V2), U62#(tt(), V2) -> isNatIList#(activate(V2)), U61#(tt(), V1, V2) -> activate#(V1), U61#(tt(), V1, V2) -> activate#(V2), U61#(tt(), V1, V2) -> isNat#(activate(V1)), U61#(tt(), V1, V2) -> U62#(isNat(activate(V1)), activate(V2)), length#(cons(N, L)) -> isNatList#(activate(L)), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> U71#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L)), length#(cons(N, L)) -> and#(isNatList(activate(L)), n__isNatIListKind(activate(L))), length#(cons(N, L)) -> and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), U71#(tt(), L) -> activate#(L), U71#(tt(), L) -> length#(activate(L)), U91#(tt(), IL, M, N) -> activate#(N), U91#(tt(), IL, M, N) -> activate#(M), U91#(tt(), IL, M, N) -> activate#(IL), and#(tt(), X) -> activate#(X), isNatIListKind#(n__take(V1, V2)) -> activate#(V1), isNatIListKind#(n__take(V1, V2)) -> activate#(V2), isNatIListKind#(n__take(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatIListKind#(n__take(V1, V2)) -> isNatKind#(activate(V1)), isNatIListKind#(n__cons(V1, V2)) -> activate#(V1), isNatIListKind#(n__cons(V1, V2)) -> activate#(V2), isNatIListKind#(n__cons(V1, V2)) -> and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatIListKind#(n__cons(V1, V2)) -> isNatKind#(activate(V1)), isNatKind#(n__length(V1)) -> activate#(V1), isNatKind#(n__length(V1)) -> isNatIListKind#(activate(V1)), isNatKind#(n__s(V1)) -> activate#(V1), isNatKind#(n__s(V1)) -> isNatKind#(activate(V1)), take#(0(), IL) -> isNatIList#(IL), take#(0(), IL) -> and#(isNatIList(IL), n__isNatIListKind(IL)), take#(s(M), cons(N, IL)) -> activate#(IL), take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), take#(s(M), cons(N, IL)) -> U91#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N)))), activate(IL), M, N), take#(s(M), cons(N, IL)) -> and#(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), take#(s(M), cons(N, IL)) -> and#(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12(tt()) -> tt(), isNatList(n__take(V1, V2)) -> U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), isNatList(n__cons(V1, V2)) -> U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), isNatList(n__nil()) -> tt(), 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__isNatIListKind(X)) -> isNatIListKind(X), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__and(X1, X2)) -> and(activate(X1), X2), activate(n__isNat(X)) -> isNat(X), activate(n__isNatKind(X)) -> isNatKind(X), U11(tt(), V1) -> U12(isNatList(activate(V1))), U22(tt()) -> tt(), isNat(X) -> n__isNat(X), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)), isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)), U21(tt(), V1) -> U22(isNat(activate(V1))), U32(tt()) -> tt(), U31(tt(), V) -> U32(isNatList(activate(V))), U42(tt(), V2) -> U43(isNatIList(activate(V2))), U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2)), U43(tt()) -> tt(), isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)), U52(tt(), V2) -> U53(isNatList(activate(V2))), U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2)), U53(tt()) -> tt(), U62(tt(), V2) -> U63(isNatIList(activate(V2))), U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2)), U63(tt()) -> tt(), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L)), length(nil()) -> 0(), U71(tt(), L) -> s(length(activate(L))), nil() -> n__nil(), U81(tt()) -> nil(), U91(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), isNatIListKind(X) -> n__isNatIListKind(X), isNatIListKind(n__zeros()) -> tt(), isNatIListKind(n__take(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatIListKind(n__cons(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), isNatIListKind(n__nil()) -> tt(), isNatKind(X) -> n__isNatKind(X), isNatKind(n__0()) -> tt(), isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)), isNatKind(n__s(V1)) -> isNatKind(activate(V1)), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL))), take(s(M), cons(N, IL)) -> U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(n__and(n__isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N)))), activate(IL), M, N)} Fail