MAYBE TRS: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U11(tt()) -> tt(), U21(tt()) -> tt(), U31(tt()) -> tt(), U42(tt()) -> tt(), isNatIList(V) -> U31(isNatList(activate(V))), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)), 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__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), U41(tt(), V2) -> U42(isNatIList(activate(V2))), U52(tt()) -> tt(), isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)), isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)), isNatList(n__nil()) -> tt(), U51(tt(), V2) -> U52(isNatList(activate(V2))), U62(tt()) -> tt(), U61(tt(), V2) -> U62(isNatIList(activate(V2))), U72(tt(), L) -> s(length(activate(L))), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> U11(isNatList(activate(V1))), isNat(n__s(V1)) -> U21(isNat(activate(V1))), U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N), length(nil()) -> 0(), nil() -> n__nil(), U81(tt()) -> nil(), U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)), U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)), U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U81(isNatIList(IL)), take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)} DP: Strict: { zeros#() -> cons#(0(), n__zeros()), zeros#() -> 0#(), isNatIList#(V) -> U31#(isNatList(activate(V))), isNatIList#(V) -> activate#(V), isNatIList#(V) -> isNatList#(activate(V)), isNatIList#(n__cons(V1, V2)) -> activate#(V2), isNatIList#(n__cons(V1, V2)) -> activate#(V1), isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)), isNatIList#(n__cons(V1, V2)) -> isNat#(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__cons(X1, X2)) -> cons#(activate(X1), X2), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__nil()) -> nil#(), U41#(tt(), V2) -> U42#(isNatIList(activate(V2))), U41#(tt(), V2) -> isNatIList#(activate(V2)), U41#(tt(), V2) -> activate#(V2), isNatList#(n__take(V1, V2)) -> activate#(V2), isNatList#(n__take(V1, V2)) -> activate#(V1), isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2)), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), U51#(tt(), V2) -> activate#(V2), U51#(tt(), V2) -> U52#(isNatList(activate(V2))), U51#(tt(), V2) -> isNatList#(activate(V2)), U61#(tt(), V2) -> isNatIList#(activate(V2)), U61#(tt(), V2) -> activate#(V2), U61#(tt(), V2) -> U62#(isNatIList(activate(V2))), U72#(tt(), L) -> activate#(L), U72#(tt(), L) -> s#(length(activate(L))), U72#(tt(), L) -> length#(activate(L)), isNat#(n__length(V1)) -> U11#(isNatList(activate(V1))), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1))), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), U71#(tt(), L, N) -> activate#(N), U71#(tt(), L, N) -> activate#(L), U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U71#(tt(), L, N) -> isNat#(activate(N)), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> isNatList#(activate(L)), length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), length#(nil()) -> 0#(), U81#(tt()) -> nil#(), U92#(tt(), IL, M, N) -> activate#(N), U92#(tt(), IL, M, N) -> activate#(M), U92#(tt(), IL, M, N) -> activate#(IL), U92#(tt(), IL, M, N) -> isNat#(activate(N)), U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U91#(tt(), IL, M, N) -> activate#(N), U91#(tt(), IL, M, N) -> activate#(M), U91#(tt(), IL, M, N) -> activate#(IL), U91#(tt(), IL, M, N) -> isNat#(activate(M)), U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> cons#(activate(N), n__take(activate(M), activate(IL))), U93#(tt(), IL, M, N) -> activate#(N), U93#(tt(), IL, M, N) -> activate#(M), U93#(tt(), IL, M, N) -> activate#(IL), take#(0(), IL) -> isNatIList#(IL), take#(0(), IL) -> U81#(isNatIList(IL)), take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), take#(s(M), cons(N, IL)) -> activate#(IL), take#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N)} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U11(tt()) -> tt(), U21(tt()) -> tt(), U31(tt()) -> tt(), U42(tt()) -> tt(), isNatIList(V) -> U31(isNatList(activate(V))), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)), 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__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), U41(tt(), V2) -> U42(isNatIList(activate(V2))), U52(tt()) -> tt(), isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)), isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)), isNatList(n__nil()) -> tt(), U51(tt(), V2) -> U52(isNatList(activate(V2))), U62(tt()) -> tt(), U61(tt(), V2) -> U62(isNatIList(activate(V2))), U72(tt(), L) -> s(length(activate(L))), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> U11(isNatList(activate(V1))), isNat(n__s(V1)) -> U21(isNat(activate(V1))), U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N), length(nil()) -> 0(), nil() -> n__nil(), U81(tt()) -> nil(), U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)), U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)), U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U81(isNatIList(IL)), take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)} EDG: { (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#()) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__s(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__length(X)) -> activate#(X)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (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__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#()) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__nil()) -> nil#()) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__s(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__length(X)) -> activate#(X)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__0()) -> 0#()) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X2)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X1)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__zeros()) -> zeros#()) (U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> activate#(IL)) (U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> activate#(M)) (U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> activate#(N)) (U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> cons#(activate(N), n__take(activate(M), activate(IL)))) (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__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#()) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1)))) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> U11#(isNatList(activate(V1)))) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1)))) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> U11#(isNatList(activate(V1)))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1)))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> U11#(isNatList(activate(V1)))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> activate#(V1)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> activate#(V2)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(V) -> isNatList#(activate(V))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(V) -> activate#(V)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(V) -> U31#(isNatList(activate(V)))) (U72#(tt(), L) -> length#(activate(L)), length#(nil()) -> 0#()) (U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N)) (U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L))) (U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> activate#(L)) (U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> activate#(V1)) (U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1)))) (U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> activate#(V1)) (U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> U11#(isNatList(activate(V1)))) (U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2))) (U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V1)) (U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V2)) (U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> isNatList#(activate(V))) (U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> activate#(V)) (U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> U31#(isNatList(activate(V)))) (U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2))) (U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V1)) (U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V2)) (U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> isNatList#(activate(V))) (U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> activate#(V)) (U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> U31#(isNatList(activate(V)))) (activate#(n__s(X)) -> activate#(X), activate#(n__nil()) -> nil#()) (activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__0()) -> 0#()) (activate#(n__s(X)) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (activate#(n__s(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X2)) (activate#(n__s(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__zeros()) -> zeros#()) (isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)), U41#(tt(), V2) -> activate#(V2)) (isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)), U41#(tt(), V2) -> isNatIList#(activate(V2))) (isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)), U41#(tt(), V2) -> U42#(isNatIList(activate(V2)))) (isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2)), U61#(tt(), V2) -> U62#(isNatIList(activate(V2)))) (isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2)), U61#(tt(), V2) -> activate#(V2)) (isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2)), U61#(tt(), V2) -> isNatIList#(activate(V2))) (U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U72#(tt(), L) -> length#(activate(L))) (U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U72#(tt(), L) -> s#(length(activate(L)))) (U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U72#(tt(), L) -> activate#(L)) (length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> isNat#(activate(N))) (length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L))) (length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> activate#(L)) (length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> activate#(N)) (U41#(tt(), V2) -> activate#(V2), activate#(n__nil()) -> nil#()) (U41#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (U41#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U41#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (U41#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (U41#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (U41#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (U41#(tt(), V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U41#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U41#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X2)) (U41#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X1)) (U41#(tt(), V2) -> activate#(V2), activate#(n__zeros()) -> zeros#()) (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__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#()) (U61#(tt(), V2) -> activate#(V2), activate#(n__nil()) -> nil#()) (U61#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (U61#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U61#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (U61#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (U61#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (U61#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (U61#(tt(), V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U61#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U61#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X2)) (U61#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X1)) (U61#(tt(), V2) -> activate#(V2), activate#(n__zeros()) -> zeros#()) (U92#(tt(), IL, M, N) -> activate#(N), activate#(n__nil()) -> nil#()) (U92#(tt(), IL, M, N) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (U92#(tt(), IL, M, N) -> activate#(N), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U92#(tt(), IL, M, N) -> activate#(N), activate#(n__s(X)) -> s#(activate(X))) (U92#(tt(), IL, M, N) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (U92#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> length#(activate(X))) (U92#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (U92#(tt(), IL, M, N) -> activate#(N), activate#(n__0()) -> 0#()) (U92#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U92#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X2)) (U92#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X1)) (U92#(tt(), IL, M, N) -> activate#(N), activate#(n__zeros()) -> zeros#()) (U93#(tt(), IL, M, N) -> activate#(N), activate#(n__nil()) -> nil#()) (U93#(tt(), IL, M, N) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (U93#(tt(), IL, M, N) -> activate#(N), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U93#(tt(), IL, M, N) -> activate#(N), activate#(n__s(X)) -> s#(activate(X))) (U93#(tt(), IL, M, N) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (U93#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> length#(activate(X))) (U93#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (U93#(tt(), IL, M, N) -> activate#(N), activate#(n__0()) -> 0#()) (U93#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U93#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X2)) (U93#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X1)) (U93#(tt(), IL, M, N) -> activate#(N), activate#(n__zeros()) -> zeros#()) (U71#(tt(), L, N) -> activate#(L), activate#(n__nil()) -> nil#()) (U71#(tt(), L, N) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (U71#(tt(), L, N) -> activate#(L), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U71#(tt(), L, N) -> activate#(L), activate#(n__s(X)) -> s#(activate(X))) (U71#(tt(), L, N) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (U71#(tt(), L, N) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (U71#(tt(), L, N) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (U71#(tt(), L, N) -> activate#(L), activate#(n__0()) -> 0#()) (U71#(tt(), L, N) -> activate#(L), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U71#(tt(), L, N) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X2)) (U71#(tt(), L, N) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X1)) (U71#(tt(), L, N) -> activate#(L), activate#(n__zeros()) -> zeros#()) (U92#(tt(), IL, M, N) -> activate#(M), activate#(n__nil()) -> nil#()) (U92#(tt(), IL, M, N) -> activate#(M), activate#(n__cons(X1, X2)) -> activate#(X1)) (U92#(tt(), IL, M, N) -> activate#(M), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U92#(tt(), IL, M, N) -> activate#(M), activate#(n__s(X)) -> s#(activate(X))) (U92#(tt(), IL, M, N) -> activate#(M), activate#(n__s(X)) -> activate#(X)) (U92#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> length#(activate(X))) (U92#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> activate#(X)) (U92#(tt(), IL, M, N) -> activate#(M), activate#(n__0()) -> 0#()) (U92#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U92#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> activate#(X2)) (U92#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> activate#(X1)) (U92#(tt(), IL, M, N) -> activate#(M), activate#(n__zeros()) -> zeros#()) (U93#(tt(), IL, M, N) -> activate#(M), activate#(n__nil()) -> nil#()) (U93#(tt(), IL, M, N) -> activate#(M), activate#(n__cons(X1, X2)) -> activate#(X1)) (U93#(tt(), IL, M, N) -> activate#(M), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U93#(tt(), IL, M, N) -> activate#(M), activate#(n__s(X)) -> s#(activate(X))) (U93#(tt(), IL, M, N) -> activate#(M), activate#(n__s(X)) -> activate#(X)) (U93#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> length#(activate(X))) (U93#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> activate#(X)) (U93#(tt(), IL, M, N) -> activate#(M), activate#(n__0()) -> 0#()) (U93#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U93#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> activate#(X2)) (U93#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> activate#(X1)) (U93#(tt(), IL, M, N) -> activate#(M), activate#(n__zeros()) -> zeros#()) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__nil()) -> nil#()) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__cons(X1, X2)) -> activate#(X1)) (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__s(X)) -> s#(activate(X))) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__s(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__length(X)) -> activate#(X)) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__0()) -> 0#()) (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__take(X1, X2)) -> activate#(X2)) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X1)) (U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__zeros()) -> zeros#()) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> activate#(V1)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> activate#(V2)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(V) -> isNatList#(activate(V))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(V) -> activate#(V)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(V) -> U31#(isNatList(activate(V)))) (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__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#()) (U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__zeros()) -> zeros#()) (U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X1)) (U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X2)) (U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__0()) -> 0#()) (U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> activate#(X)) (U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> length#(activate(X))) (U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__s(X)) -> activate#(X)) (U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__s(X)) -> s#(activate(X))) (U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__cons(X1, X2)) -> activate#(X1)) (U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__nil()) -> nil#()) (U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__zeros()) -> zeros#()) (U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X1)) (U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X2)) (U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__0()) -> 0#()) (U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> activate#(X)) (U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> length#(activate(X))) (U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__s(X)) -> activate#(X)) (U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__s(X)) -> s#(activate(X))) (U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__cons(X1, X2)) -> activate#(X1)) (U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__nil()) -> nil#()) (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__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#()) (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__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#()) (U72#(tt(), L) -> activate#(L), activate#(n__zeros()) -> zeros#()) (U72#(tt(), L) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X1)) (U72#(tt(), L) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X2)) (U72#(tt(), L) -> activate#(L), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U72#(tt(), L) -> activate#(L), activate#(n__0()) -> 0#()) (U72#(tt(), L) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (U72#(tt(), L) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (U72#(tt(), L) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (U72#(tt(), L) -> activate#(L), activate#(n__s(X)) -> s#(activate(X))) (U72#(tt(), L) -> activate#(L), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U72#(tt(), L) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (U72#(tt(), L) -> activate#(L), activate#(n__nil()) -> nil#()) (take#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N), U91#(tt(), IL, M, N) -> activate#(N)) (take#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N), U91#(tt(), IL, M, N) -> activate#(M)) (take#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N), U91#(tt(), IL, M, N) -> activate#(IL)) (take#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N), U91#(tt(), IL, M, N) -> isNat#(activate(M))) (take#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N), U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N))) (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__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#()) (U71#(tt(), L, N) -> activate#(N), activate#(n__zeros()) -> zeros#()) (U71#(tt(), L, N) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X1)) (U71#(tt(), L, N) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X2)) (U71#(tt(), L, N) -> activate#(N), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U71#(tt(), L, N) -> activate#(N), activate#(n__0()) -> 0#()) (U71#(tt(), L, N) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (U71#(tt(), L, N) -> activate#(N), activate#(n__length(X)) -> length#(activate(X))) (U71#(tt(), L, N) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (U71#(tt(), L, N) -> activate#(N), activate#(n__s(X)) -> s#(activate(X))) (U71#(tt(), L, N) -> activate#(N), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U71#(tt(), L, N) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (U71#(tt(), L, N) -> activate#(N), activate#(n__nil()) -> nil#()) (U51#(tt(), V2) -> activate#(V2), activate#(n__zeros()) -> zeros#()) (U51#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X1)) (U51#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> activate#(X2)) (U51#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U51#(tt(), V2) -> activate#(V2), activate#(n__0()) -> 0#()) (U51#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (U51#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (U51#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (U51#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> s#(activate(X))) (U51#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (U51#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (U51#(tt(), V2) -> activate#(V2), activate#(n__nil()) -> nil#()) (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__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#()) (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__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#()) (isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), U51#(tt(), V2) -> activate#(V2)) (isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), U51#(tt(), V2) -> U52#(isNatList(activate(V2)))) (isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), U51#(tt(), V2) -> isNatList#(activate(V2))) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(0(), IL) -> isNatIList#(IL)) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(0(), IL) -> U81#(isNatIList(IL))) (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#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N)) (activate#(n__length(X)) -> activate#(X), activate#(n__zeros()) -> zeros#()) (activate#(n__length(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X1)) (activate#(n__length(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X2)) (activate#(n__length(X)) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (activate#(n__length(X)) -> activate#(X), activate#(n__0()) -> 0#()) (activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__length(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__length(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (activate#(n__length(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__length(X)) -> activate#(X), activate#(n__nil()) -> nil#()) (U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__take(V1, V2)) -> activate#(V2)) (U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__take(V1, V2)) -> activate#(V1)) (U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2))) (U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1))) (U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2))) (U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> U11#(isNatList(activate(V1)))) (U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> activate#(V1)) (U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1)))) (U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> activate#(V1)) (U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> isNat#(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)) -> activate#(V1)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (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)) -> U51#(isNat(activate(V1)), activate(V2))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__length(V1)) -> U11#(isNatList(activate(V1)))) (U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__length(V1)) -> activate#(V1)) (U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1)))) (U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__s(V1)) -> activate#(V1)) (U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (take#(0(), IL) -> U81#(isNatIList(IL)), U81#(tt()) -> nil#()) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__take(V1, V2)) -> activate#(V2)) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__take(V1, V2)) -> activate#(V1)) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2))) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1))) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2))) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> U11#(isNatList(activate(V1)))) (isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1)))) (isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__take(V1, V2)) -> activate#(V2)) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__take(V1, V2)) -> activate#(V1)) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2))) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1))) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2))) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> activate#(L)) (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)) -> U71#(isNatList(activate(L)), activate(L), N)) (activate#(n__length(X)) -> length#(activate(X)), length#(nil()) -> 0#()) (U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> activate#(N)) (U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> activate#(M)) (U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> activate#(IL)) (U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> isNat#(activate(N))) (U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N))) (activate#(n__zeros()) -> zeros#(), zeros#() -> cons#(0(), n__zeros())) (activate#(n__zeros()) -> zeros#(), zeros#() -> 0#()) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__zeros()) -> zeros#()) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X1)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X2)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__0()) -> 0#()) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__length(X)) -> 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__s(X)) -> activate#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__nil()) -> nil#()) (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__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#()) (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__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#()) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> 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__s(X)) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#()) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__zeros()) -> zeros#()) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> activate#(X1)) (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)) -> take#(activate(X1), activate(X2))) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#()) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> activate#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(activate(X))) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#()) } SCCS: Scc: { isNatIList#(V) -> activate#(V), isNatIList#(V) -> isNatList#(activate(V)), isNatIList#(n__cons(V1, V2)) -> activate#(V2), isNatIList#(n__cons(V1, V2)) -> activate#(V1), isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)), isNatIList#(n__cons(V1, V2)) -> isNat#(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__cons(X1, X2)) -> activate#(X1), U41#(tt(), V2) -> isNatIList#(activate(V2)), U41#(tt(), V2) -> activate#(V2), isNatList#(n__take(V1, V2)) -> activate#(V2), isNatList#(n__take(V1, V2)) -> activate#(V1), isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2)), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), U51#(tt(), V2) -> activate#(V2), U51#(tt(), V2) -> isNatList#(activate(V2)), U61#(tt(), V2) -> isNatIList#(activate(V2)), U61#(tt(), V2) -> activate#(V2), U72#(tt(), L) -> activate#(L), U72#(tt(), L) -> length#(activate(L)), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), U71#(tt(), L, N) -> activate#(N), U71#(tt(), L, N) -> activate#(L), U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U71#(tt(), L, N) -> isNat#(activate(N)), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> isNatList#(activate(L)), length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U92#(tt(), IL, M, N) -> activate#(N), U92#(tt(), IL, M, N) -> activate#(M), U92#(tt(), IL, M, N) -> activate#(IL), U92#(tt(), IL, M, N) -> isNat#(activate(N)), U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U91#(tt(), IL, M, N) -> activate#(N), U91#(tt(), IL, M, N) -> activate#(M), U91#(tt(), IL, M, N) -> activate#(IL), U91#(tt(), IL, M, N) -> isNat#(activate(M)), U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> activate#(N), U93#(tt(), IL, M, N) -> activate#(M), U93#(tt(), IL, M, N) -> activate#(IL), take#(0(), IL) -> isNatIList#(IL), take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), take#(s(M), cons(N, IL)) -> activate#(IL), take#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N)} SCC: Strict: { isNatIList#(V) -> activate#(V), isNatIList#(V) -> isNatList#(activate(V)), isNatIList#(n__cons(V1, V2)) -> activate#(V2), isNatIList#(n__cons(V1, V2)) -> activate#(V1), isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)), isNatIList#(n__cons(V1, V2)) -> isNat#(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__cons(X1, X2)) -> activate#(X1), U41#(tt(), V2) -> isNatIList#(activate(V2)), U41#(tt(), V2) -> activate#(V2), isNatList#(n__take(V1, V2)) -> activate#(V2), isNatList#(n__take(V1, V2)) -> activate#(V1), isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2)), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), U51#(tt(), V2) -> activate#(V2), U51#(tt(), V2) -> isNatList#(activate(V2)), U61#(tt(), V2) -> isNatIList#(activate(V2)), U61#(tt(), V2) -> activate#(V2), U72#(tt(), L) -> activate#(L), U72#(tt(), L) -> length#(activate(L)), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), U71#(tt(), L, N) -> activate#(N), U71#(tt(), L, N) -> activate#(L), U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U71#(tt(), L, N) -> isNat#(activate(N)), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> isNatList#(activate(L)), length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U92#(tt(), IL, M, N) -> activate#(N), U92#(tt(), IL, M, N) -> activate#(M), U92#(tt(), IL, M, N) -> activate#(IL), U92#(tt(), IL, M, N) -> isNat#(activate(N)), U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U91#(tt(), IL, M, N) -> activate#(N), U91#(tt(), IL, M, N) -> activate#(M), U91#(tt(), IL, M, N) -> activate#(IL), U91#(tt(), IL, M, N) -> isNat#(activate(M)), U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> activate#(N), U93#(tt(), IL, M, N) -> activate#(M), U93#(tt(), IL, M, N) -> activate#(IL), take#(0(), IL) -> isNatIList#(IL), take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), take#(s(M), cons(N, IL)) -> activate#(IL), take#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N)} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U11(tt()) -> tt(), U21(tt()) -> tt(), U31(tt()) -> tt(), U42(tt()) -> tt(), isNatIList(V) -> U31(isNatList(activate(V))), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)), 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__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), U41(tt(), V2) -> U42(isNatIList(activate(V2))), U52(tt()) -> tt(), isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)), isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)), isNatList(n__nil()) -> tt(), U51(tt(), V2) -> U52(isNatList(activate(V2))), U62(tt()) -> tt(), U61(tt(), V2) -> U62(isNatIList(activate(V2))), U72(tt(), L) -> s(length(activate(L))), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> U11(isNatList(activate(V1))), isNat(n__s(V1)) -> U21(isNat(activate(V1))), U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N), length(nil()) -> 0(), nil() -> n__nil(), U81(tt()) -> nil(), U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)), U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)), U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U81(isNatIList(IL)), take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)} POLY: Argument Filtering: pi(take#) = [0,1], pi(take) = [0,1], pi(n__nil) = [], pi(n__cons) = [0,1], pi(n__s) = 0, pi(n__length) = 0, pi(n__0) = [], pi(n__take) = [0,1], pi(U93#) = [1,2,3], pi(U93) = [1,2,3], pi(U91#) = [1,2,3], pi(U91) = [1,2,3], pi(U92#) = [1,2,3], pi(U92) = [1,2,3], pi(U81) = [], pi(nil) = [], pi(length#) = 0, pi(length) = 0, pi(s) = 0, pi(U71#) = [1,2], pi(U71) = 1, pi(isNat#) = 0, pi(isNat) = [], pi(U72#) = 1, pi(U72) = 1, pi(U61#) = 1, pi(U61) = [], pi(U62) = [], pi(U51#) = 1, pi(U51) = [], pi(isNatList#) = 0, pi(isNatList) = [], pi(U52) = [], pi(U41#) = 1, pi(U41) = [], pi(activate#) = 0, pi(activate) = 0, pi(isNatIList#) = 0, pi(isNatIList) = [], pi(U42) = [], pi(U31) = [], pi(U21) = [], pi(U11) = [], pi(tt) = [], pi(zeros) = [], pi(n__zeros) = [], pi(0) = [], pi(cons) = [0,1] Usable Rules: {} Interpretation: [U93#](x0, x1, x2) = x0 + x1 + x2, [U91#](x0, x1, x2) = x0 + x1 + x2, [U92#](x0, x1, x2) = x0 + x1 + x2, [U71#](x0, x1) = x0 + x1, [take#](x0, x1) = x0 + x1 + 1, [n__cons](x0, x1) = x0 + x1, [n__take](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = x0 + x1, [0] = 0 Strict: { isNatIList#(V) -> activate#(V), isNatIList#(V) -> isNatList#(activate(V)), isNatIList#(n__cons(V1, V2)) -> activate#(V2), isNatIList#(n__cons(V1, V2)) -> activate#(V1), isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), 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__cons(X1, X2)) -> activate#(X1), U41#(tt(), V2) -> isNatIList#(activate(V2)), U41#(tt(), V2) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), U51#(tt(), V2) -> activate#(V2), U51#(tt(), V2) -> isNatList#(activate(V2)), U61#(tt(), V2) -> isNatIList#(activate(V2)), U61#(tt(), V2) -> activate#(V2), U72#(tt(), L) -> activate#(L), U72#(tt(), L) -> length#(activate(L)), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), U71#(tt(), L, N) -> activate#(N), U71#(tt(), L, N) -> activate#(L), U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U71#(tt(), L, N) -> isNat#(activate(N)), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> isNatList#(activate(L)), length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U92#(tt(), IL, M, N) -> activate#(N), U92#(tt(), IL, M, N) -> activate#(M), U92#(tt(), IL, M, N) -> activate#(IL), U92#(tt(), IL, M, N) -> isNat#(activate(N)), U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U91#(tt(), IL, M, N) -> activate#(N), U91#(tt(), IL, M, N) -> activate#(M), U91#(tt(), IL, M, N) -> activate#(IL), U91#(tt(), IL, M, N) -> isNat#(activate(M)), U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> activate#(N), U93#(tt(), IL, M, N) -> activate#(M), U93#(tt(), IL, M, N) -> activate#(IL)} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U11(tt()) -> tt(), U21(tt()) -> tt(), U31(tt()) -> tt(), U42(tt()) -> tt(), isNatIList(V) -> U31(isNatList(activate(V))), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)), 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__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), U41(tt(), V2) -> U42(isNatIList(activate(V2))), U52(tt()) -> tt(), isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)), isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)), isNatList(n__nil()) -> tt(), U51(tt(), V2) -> U52(isNatList(activate(V2))), U62(tt()) -> tt(), U61(tt(), V2) -> U62(isNatIList(activate(V2))), U72(tt(), L) -> s(length(activate(L))), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> U11(isNatList(activate(V1))), isNat(n__s(V1)) -> U21(isNat(activate(V1))), U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N), length(nil()) -> 0(), nil() -> n__nil(), U81(tt()) -> nil(), U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)), U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)), U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U81(isNatIList(IL)), take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)} EDG: { (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2))) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__s(V1)) -> activate#(V1)) (U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__length(V1)) -> activate#(V1)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2))) (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)) (U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> activate#(V1)) (U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> activate#(V1)) (U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2))) (U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)), U41#(tt(), V2) -> activate#(V2)) (isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)), U41#(tt(), V2) -> isNatIList#(activate(V2))) (isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), U51#(tt(), V2) -> isNatList#(activate(V2))) (isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), U51#(tt(), V2) -> activate#(V2)) (activate#(n__length(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (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__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> activate#(IL)) (U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> activate#(M)) (U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> activate#(N)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (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__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (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__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNat#(n__length(V1)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (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__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__cons(X1, X2)) -> activate#(X1)) (U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__s(X)) -> activate#(X)) (U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> length#(activate(X))) (U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> activate#(X)) (U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__cons(X1, X2)) -> activate#(X1)) (U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__s(X)) -> activate#(X)) (U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> length#(activate(X))) (U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> activate#(X)) (U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__cons(X1, X2)) -> activate#(X1)) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__s(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__length(X)) -> activate#(X)) (U91#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U72#(tt(), L) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (U72#(tt(), L) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (U72#(tt(), L) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (U72#(tt(), L) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (U72#(tt(), L) -> activate#(L), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (length#(cons(N, L)) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (length#(cons(N, L)) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (length#(cons(N, L)) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U92#(tt(), IL, M, N) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (U92#(tt(), IL, M, N) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (U92#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> length#(activate(X))) (U92#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (U92#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U93#(tt(), IL, M, N) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (U93#(tt(), IL, M, N) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (U93#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> length#(activate(X))) (U93#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (U93#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U41#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (U41#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (U41#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (U41#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (U41#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U51#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (U51#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (U51#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (U51#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (U51#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U61#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U61#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> activate#(X)) (U61#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (U61#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (U61#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (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__length(X)) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(activate(X))) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> 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__cons(X1, X2)) -> activate#(X1)) (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__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__cons(X1, X2)) -> activate#(X1)) (U71#(tt(), L, N) -> activate#(N), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U71#(tt(), L, N) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (U71#(tt(), L, N) -> activate#(N), activate#(n__length(X)) -> length#(activate(X))) (U71#(tt(), L, N) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (U71#(tt(), L, N) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (U71#(tt(), L, N) -> activate#(L), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U71#(tt(), L, N) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (U71#(tt(), L, N) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (U71#(tt(), L, N) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (U71#(tt(), L, N) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (U93#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U93#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> activate#(X)) (U93#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> length#(activate(X))) (U93#(tt(), IL, M, N) -> activate#(M), activate#(n__s(X)) -> activate#(X)) (U93#(tt(), IL, M, N) -> activate#(M), activate#(n__cons(X1, X2)) -> activate#(X1)) (U92#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (U92#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> activate#(X)) (U92#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> length#(activate(X))) (U92#(tt(), IL, M, N) -> activate#(M), activate#(n__s(X)) -> activate#(X)) (U92#(tt(), IL, M, N) -> activate#(M), activate#(n__cons(X1, X2)) -> activate#(X1)) (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__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__cons(X1, X2)) -> activate#(X1)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__length(X)) -> 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__cons(X1, X2)) -> activate#(X1)) (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__length(X)) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(activate(X))) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatIList#(V) -> activate#(V), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (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__cons(X1, X2)) -> activate#(X1)) (U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> activate#(N)) (U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> activate#(M)) (U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> activate#(IL)) (U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> isNat#(activate(N))) (U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N))) (activate#(n__s(X)) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> 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__cons(X1, X2)) -> activate#(X1)) (U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U72#(tt(), L) -> activate#(L)) (U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U72#(tt(), L) -> length#(activate(L))) (U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> activate#(V)) (U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> isNatList#(activate(V))) (U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V2)) (U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V1)) (U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2))) (U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> activate#(V)) (U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> isNatList#(activate(V))) (U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V2)) (U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V1)) (U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2))) (U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> activate#(V1)) (U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> activate#(V1)) (U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> activate#(L)) (U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L))) (U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N)) (length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> activate#(N)) (length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> activate#(L)) (length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L))) (length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> isNat#(activate(N))) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2))) (isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1)) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1))) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> activate#(L)) (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)) -> U71#(isNatList(activate(L)), activate(L), N)) } SCCS: Scc: { activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X)), activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), U51#(tt(), V2) -> activate#(V2), U51#(tt(), V2) -> isNatList#(activate(V2)), U72#(tt(), L) -> activate#(L), U72#(tt(), L) -> length#(activate(L)), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), U71#(tt(), L, N) -> activate#(N), U71#(tt(), L, N) -> activate#(L), U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U71#(tt(), L, N) -> isNat#(activate(N)), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> isNatList#(activate(L)), length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N)} Scc: {isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)), U41#(tt(), V2) -> isNatIList#(activate(V2))} SCC: Strict: { activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X)), activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), U51#(tt(), V2) -> activate#(V2), U51#(tt(), V2) -> isNatList#(activate(V2)), U72#(tt(), L) -> activate#(L), U72#(tt(), L) -> length#(activate(L)), isNat#(n__length(V1)) -> activate#(V1), isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), U71#(tt(), L, N) -> activate#(N), U71#(tt(), L, N) -> activate#(L), U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U71#(tt(), L, N) -> isNat#(activate(N)), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> isNatList#(activate(L)), length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N)} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U11(tt()) -> tt(), U21(tt()) -> tt(), U31(tt()) -> tt(), U42(tt()) -> tt(), isNatIList(V) -> U31(isNatList(activate(V))), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)), 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__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), U41(tt(), V2) -> U42(isNatIList(activate(V2))), U52(tt()) -> tt(), isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)), isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)), isNatList(n__nil()) -> tt(), U51(tt(), V2) -> U52(isNatList(activate(V2))), U62(tt()) -> tt(), U61(tt(), V2) -> U62(isNatIList(activate(V2))), U72(tt(), L) -> s(length(activate(L))), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> U11(isNatList(activate(V1))), isNat(n__s(V1)) -> U21(isNat(activate(V1))), U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N), length(nil()) -> 0(), nil() -> n__nil(), U81(tt()) -> nil(), U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)), U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)), U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U81(isNatIList(IL)), take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)} POLY: Argument Filtering: pi(take) = 1, pi(n__nil) = [], pi(n__cons) = [0,1], pi(n__s) = 0, pi(n__length) = [0], pi(n__0) = [], pi(n__take) = 1, pi(U93) = [1,3], pi(U91) = [1,3], pi(U92) = [1,3], pi(U81) = [], pi(nil) = [], pi(length#) = [0], pi(length) = [0], pi(s) = 0, pi(U71#) = [1,2], pi(U71) = [1], pi(isNat#) = [0], pi(isNat) = [], pi(U72#) = [1], pi(U72) = [1], pi(U61) = [], pi(U62) = [], pi(U51#) = [1], pi(U51) = [], pi(isNatList#) = [0], pi(isNatList) = [], pi(U52) = [], pi(U41) = [], pi(activate#) = [0], pi(activate) = 0, pi(isNatIList) = [], pi(U42) = [], pi(U31) = [], pi(U21) = [], pi(U11) = [], pi(tt) = [], pi(zeros) = [], pi(n__zeros) = [], pi(0) = [], pi(cons) = [0,1] Usable Rules: {} Interpretation: [U71#](x0, x1) = x0 + x1 + 1, [U72#](x0) = x0 + 1, [U51#](x0) = x0 + 1, [length#](x0) = x0 + 1, [isNat#](x0) = x0 + 1, [isNatList#](x0) = x0 + 1, [activate#](x0) = x0 + 1, [n__cons](x0, x1) = x0 + x1, [cons](x0, x1) = x0 + x1, [n__length](x0) = x0 + 1 Strict: { activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1), isNatList#(n__cons(V1, V2)) -> activate#(V2), isNatList#(n__cons(V1, V2)) -> activate#(V1), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), U51#(tt(), V2) -> activate#(V2), U51#(tt(), V2) -> isNatList#(activate(V2)), U72#(tt(), L) -> activate#(L), U72#(tt(), L) -> length#(activate(L)), isNat#(n__s(V1)) -> activate#(V1), isNat#(n__s(V1)) -> isNat#(activate(V1)), U71#(tt(), L, N) -> activate#(N), U71#(tt(), L, N) -> activate#(L), U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U71#(tt(), L, N) -> isNat#(activate(N)), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> isNatList#(activate(L)), length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N)} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U11(tt()) -> tt(), U21(tt()) -> tt(), U31(tt()) -> tt(), U42(tt()) -> tt(), isNatIList(V) -> U31(isNatList(activate(V))), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)), 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__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), U41(tt(), V2) -> U42(isNatIList(activate(V2))), U52(tt()) -> tt(), isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)), isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)), isNatList(n__nil()) -> tt(), U51(tt(), V2) -> U52(isNatList(activate(V2))), U62(tt()) -> tt(), U61(tt(), V2) -> U62(isNatIList(activate(V2))), U72(tt(), L) -> s(length(activate(L))), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> U11(isNatList(activate(V1))), isNat(n__s(V1)) -> U21(isNat(activate(V1))), U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N), length(nil()) -> 0(), nil() -> n__nil(), U81(tt()) -> nil(), U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)), U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)), U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U81(isNatIList(IL)), take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)} EDG: {(isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), U51#(tt(), V2) -> isNatList#(activate(V2))) (isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), U51#(tt(), V2) -> activate#(V2)) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (U71#(tt(), L, N) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (U71#(tt(), L, N) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2))) (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)) (U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1))) (U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2))) (U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> activate#(V1)) (U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> activate#(V2)) (U51#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (U51#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (U71#(tt(), L, N) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (U71#(tt(), L, N) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (U72#(tt(), L) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (U72#(tt(), L) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> activate#(X)) (isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> activate#(X1)) (U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> activate#(V1)) (U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> activate#(L)) (U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L))) (U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> activate#(X)) (isNat#(n__s(V1)) -> activate#(V1), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1)) (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1))) (U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U72#(tt(), L) -> activate#(L)) (U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U72#(tt(), L) -> length#(activate(L))) (length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> activate#(N)) (length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> activate#(L)) (length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L))) (length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> isNat#(activate(N)))} SCCS: Scc: {isNat#(n__s(V1)) -> isNat#(activate(V1))} Scc: { U72#(tt(), L) -> length#(activate(L)), U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N)} Scc: {isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), U51#(tt(), V2) -> isNatList#(activate(V2))} Scc: { activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)} SCC: Strict: {isNat#(n__s(V1)) -> isNat#(activate(V1))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U11(tt()) -> tt(), U21(tt()) -> tt(), U31(tt()) -> tt(), U42(tt()) -> tt(), isNatIList(V) -> U31(isNatList(activate(V))), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)), 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__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), U41(tt(), V2) -> U42(isNatIList(activate(V2))), U52(tt()) -> tt(), isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)), isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)), isNatList(n__nil()) -> tt(), U51(tt(), V2) -> U52(isNatList(activate(V2))), U62(tt()) -> tt(), U61(tt(), V2) -> U62(isNatIList(activate(V2))), U72(tt(), L) -> s(length(activate(L))), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> U11(isNatList(activate(V1))), isNat(n__s(V1)) -> U21(isNat(activate(V1))), U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N), length(nil()) -> 0(), nil() -> n__nil(), U81(tt()) -> nil(), U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)), U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)), U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U81(isNatIList(IL)), take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)} Fail SCC: Strict: { U72#(tt(), L) -> length#(activate(L)), U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N)} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U11(tt()) -> tt(), U21(tt()) -> tt(), U31(tt()) -> tt(), U42(tt()) -> tt(), isNatIList(V) -> U31(isNatList(activate(V))), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)), 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__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), U41(tt(), V2) -> U42(isNatIList(activate(V2))), U52(tt()) -> tt(), isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)), isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)), isNatList(n__nil()) -> tt(), U51(tt(), V2) -> U52(isNatList(activate(V2))), U62(tt()) -> tt(), U61(tt(), V2) -> U62(isNatIList(activate(V2))), U72(tt(), L) -> s(length(activate(L))), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> U11(isNatList(activate(V1))), isNat(n__s(V1)) -> U21(isNat(activate(V1))), U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N), length(nil()) -> 0(), nil() -> n__nil(), U81(tt()) -> nil(), U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)), U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)), U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U81(isNatIList(IL)), take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)} Fail SCC: Strict: {isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), U51#(tt(), V2) -> isNatList#(activate(V2))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U11(tt()) -> tt(), U21(tt()) -> tt(), U31(tt()) -> tt(), U42(tt()) -> tt(), isNatIList(V) -> U31(isNatList(activate(V))), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)), 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__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), U41(tt(), V2) -> U42(isNatIList(activate(V2))), U52(tt()) -> tt(), isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)), isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)), isNatList(n__nil()) -> tt(), U51(tt(), V2) -> U52(isNatList(activate(V2))), U62(tt()) -> tt(), U61(tt(), V2) -> U62(isNatIList(activate(V2))), U72(tt(), L) -> s(length(activate(L))), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> U11(isNatList(activate(V1))), isNat(n__s(V1)) -> U21(isNat(activate(V1))), U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N), length(nil()) -> 0(), nil() -> n__nil(), U81(tt()) -> nil(), U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)), U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)), U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U81(isNatIList(IL)), take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)} Fail SCC: Strict: { activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U11(tt()) -> tt(), U21(tt()) -> tt(), U31(tt()) -> tt(), U42(tt()) -> tt(), isNatIList(V) -> U31(isNatList(activate(V))), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)), 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__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), U41(tt(), V2) -> U42(isNatIList(activate(V2))), U52(tt()) -> tt(), isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)), isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)), isNatList(n__nil()) -> tt(), U51(tt(), V2) -> U52(isNatList(activate(V2))), U62(tt()) -> tt(), U61(tt(), V2) -> U62(isNatIList(activate(V2))), U72(tt(), L) -> s(length(activate(L))), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> U11(isNatList(activate(V1))), isNat(n__s(V1)) -> U21(isNat(activate(V1))), U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N), length(nil()) -> 0(), nil() -> n__nil(), U81(tt()) -> nil(), U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)), U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)), U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U81(isNatIList(IL)), take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)} SPSC: Simple Projection: pi(activate#) = 0 Strict: {activate#(n__cons(X1, X2)) -> activate#(X1)} EDG: {(activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1))} SCCS: Scc: {activate#(n__cons(X1, X2)) -> activate#(X1)} SCC: Strict: {activate#(n__cons(X1, X2)) -> activate#(X1)} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U11(tt()) -> tt(), U21(tt()) -> tt(), U31(tt()) -> tt(), U42(tt()) -> tt(), isNatIList(V) -> U31(isNatList(activate(V))), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)), 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__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), U41(tt(), V2) -> U42(isNatIList(activate(V2))), U52(tt()) -> tt(), isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)), isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)), isNatList(n__nil()) -> tt(), U51(tt(), V2) -> U52(isNatList(activate(V2))), U62(tt()) -> tt(), U61(tt(), V2) -> U62(isNatIList(activate(V2))), U72(tt(), L) -> s(length(activate(L))), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> U11(isNatList(activate(V1))), isNat(n__s(V1)) -> U21(isNat(activate(V1))), U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N), length(nil()) -> 0(), nil() -> n__nil(), U81(tt()) -> nil(), U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)), U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)), U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U81(isNatIList(IL)), take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)} SPSC: Simple Projection: pi(activate#) = 0 Strict: {} Qed SCC: Strict: {isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)), U41#(tt(), V2) -> isNatIList#(activate(V2))} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U11(tt()) -> tt(), U21(tt()) -> tt(), U31(tt()) -> tt(), U42(tt()) -> tt(), isNatIList(V) -> U31(isNatList(activate(V))), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)), 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__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), U41(tt(), V2) -> U42(isNatIList(activate(V2))), U52(tt()) -> tt(), isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)), isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)), isNatList(n__nil()) -> tt(), U51(tt(), V2) -> U52(isNatList(activate(V2))), U62(tt()) -> tt(), U61(tt(), V2) -> U62(isNatIList(activate(V2))), U72(tt(), L) -> s(length(activate(L))), isNat(n__0()) -> tt(), isNat(n__length(V1)) -> U11(isNatList(activate(V1))), isNat(n__s(V1)) -> U21(isNat(activate(V1))), U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)), s(X) -> n__s(X), length(X) -> n__length(X), length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N), length(nil()) -> 0(), nil() -> n__nil(), U81(tt()) -> nil(), U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)), U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)), U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> U81(isNatIList(IL)), take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)} Fail