MAYBE TRS: { and(tt(), T) -> T, isNatList(n__cons(N, L)) -> and(isNat(activate(N)), isNatList(activate(L))), isNatList(n__nil()) -> tt(), isNatList(n__take(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__s(X)) -> s(activate(X)), activate(n__length(X)) -> length(activate(X)), activate(n__zeros()) -> zeros(), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)), isNatIList(IL) -> isNatList(activate(IL)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), isNat(n__0()) -> tt(), isNat(n__s(N)) -> isNat(activate(N)), isNat(n__length(L)) -> isNatList(activate(L)), cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1(tt()) -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1(isNatIList(IL)), take(s(M), cons(N, IL)) -> uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate(N), n__take(activate(M), activate(IL))), s(X) -> n__s(X), uLength(tt(), L) -> s(length(activate(L))), length(X) -> n__length(X), length(cons(N, L)) -> uLength(and(isNat(N), isNatList(activate(L))), activate(L))} DP: Strict: { isNatList#(n__cons(N, L)) -> and#(isNat(activate(N)), isNatList(activate(L))), isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(N), isNatList#(n__cons(N, L)) -> activate#(L), isNatList#(n__cons(N, L)) -> isNat#(activate(N)), isNatList#(n__take(N, IL)) -> and#(isNat(activate(N)), isNatIList(activate(IL))), isNatList#(n__take(N, IL)) -> activate#(IL), isNatList#(n__take(N, IL)) -> activate#(N), isNatList#(n__take(N, IL)) -> isNatIList#(activate(IL)), isNatList#(n__take(N, IL)) -> isNat#(activate(N)), activate#(n__0()) -> 0#(), activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)), activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X)), activate#(n__zeros()) -> zeros#(), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2), activate#(n__nil()) -> nil#(), activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), isNatIList#(IL) -> isNatList#(activate(IL)), isNatIList#(IL) -> activate#(IL), isNatIList#(n__cons(N, IL)) -> and#(isNat(activate(N)), isNatIList(activate(IL))), isNatIList#(n__cons(N, IL)) -> activate#(IL), isNatIList#(n__cons(N, IL)) -> activate#(N), isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> isNat#(activate(N)), isNat#(n__s(N)) -> activate#(N), isNat#(n__s(N)) -> isNat#(activate(N)), isNat#(n__length(L)) -> isNatList#(activate(L)), isNat#(n__length(L)) -> activate#(L), zeros#() -> cons#(0(), n__zeros()), zeros#() -> 0#(), uTake1#(tt()) -> nil#(), take#(0(), IL) -> isNatIList#(IL), take#(0(), IL) -> uTake1#(isNatIList(IL)), take#(s(M), cons(N, IL)) -> and#(isNat(N), isNatIList(activate(IL))), take#(s(M), cons(N, IL)) -> and#(isNat(M), and(isNat(N), isNatIList(activate(IL)))), take#(s(M), cons(N, IL)) -> activate#(IL), take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), take#(s(M), cons(N, IL)) -> isNat#(N), take#(s(M), cons(N, IL)) -> isNat#(M), take#(s(M), cons(N, IL)) -> uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), uTake2#(tt(), M, N, IL) -> activate#(IL), uTake2#(tt(), M, N, IL) -> activate#(N), uTake2#(tt(), M, N, IL) -> activate#(M), uTake2#(tt(), M, N, IL) -> cons#(activate(N), n__take(activate(M), activate(IL))), uLength#(tt(), L) -> activate#(L), uLength#(tt(), L) -> s#(length(activate(L))), uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> and#(isNat(N), isNatList(activate(L))), length#(cons(N, L)) -> isNatList#(activate(L)), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> isNat#(N), length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L))} Weak: { and(tt(), T) -> T, isNatList(n__cons(N, L)) -> and(isNat(activate(N)), isNatList(activate(L))), isNatList(n__nil()) -> tt(), isNatList(n__take(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__s(X)) -> s(activate(X)), activate(n__length(X)) -> length(activate(X)), activate(n__zeros()) -> zeros(), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)), isNatIList(IL) -> isNatList(activate(IL)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), isNat(n__0()) -> tt(), isNat(n__s(N)) -> isNat(activate(N)), isNat(n__length(L)) -> isNatList(activate(L)), cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1(tt()) -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1(isNatIList(IL)), take(s(M), cons(N, IL)) -> uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate(N), n__take(activate(M), activate(IL))), s(X) -> n__s(X), uLength(tt(), L) -> s(length(activate(L))), length(X) -> n__length(X), length(cons(N, L)) -> uLength(and(isNat(N), isNatList(activate(L))), activate(L))} EDG: { (length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L)), uLength#(tt(), L) -> length#(activate(L))) (length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L)), uLength#(tt(), L) -> s#(length(activate(L)))) (length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L)), uLength#(tt(), L) -> activate#(L)) (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__nil()) -> nil#()) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__zeros()) -> zeros#()) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__length(X)) -> activate#(X)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> activate#(X)) (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__0()) -> 0#()) (isNatIList#(n__cons(N, IL)) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatIList#(n__cons(N, IL)) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatIList#(n__cons(N, IL)) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatIList#(n__cons(N, IL)) -> activate#(IL), activate#(n__nil()) -> nil#()) (isNatIList#(n__cons(N, IL)) -> activate#(IL), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatIList#(n__cons(N, IL)) -> activate#(IL), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatIList#(n__cons(N, IL)) -> activate#(IL), activate#(n__zeros()) -> zeros#()) (isNatIList#(n__cons(N, IL)) -> activate#(IL), activate#(n__length(X)) -> length#(activate(X))) (isNatIList#(n__cons(N, IL)) -> activate#(IL), activate#(n__length(X)) -> activate#(X)) (isNatIList#(n__cons(N, IL)) -> activate#(IL), activate#(n__s(X)) -> s#(activate(X))) (isNatIList#(n__cons(N, IL)) -> activate#(IL), activate#(n__s(X)) -> activate#(X)) (isNatIList#(n__cons(N, IL)) -> activate#(IL), activate#(n__0()) -> 0#()) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X2)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X1)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__nil()) -> nil#()) (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__zeros()) -> zeros#()) (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__length(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__s(X)) -> activate#(X)) (take#(s(M), cons(N, IL)) -> activate#(IL), 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__nil()) -> nil#()) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__zeros()) -> zeros#()) (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__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__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__nil()) -> nil#()) (activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__s(X)) -> activate#(X), activate#(n__zeros()) -> zeros#()) (activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X))) (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__0()) -> 0#()) (take#(s(M), cons(N, IL)) -> uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), uTake2#(tt(), M, N, IL) -> cons#(activate(N), n__take(activate(M), activate(IL)))) (take#(s(M), cons(N, IL)) -> uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), uTake2#(tt(), M, N, IL) -> activate#(M)) (take#(s(M), cons(N, IL)) -> uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), uTake2#(tt(), M, N, IL) -> activate#(N)) (take#(s(M), cons(N, IL)) -> uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), uTake2#(tt(), M, N, IL) -> activate#(IL)) (uTake2#(tt(), M, N, IL) -> activate#(M), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (uTake2#(tt(), M, N, IL) -> activate#(M), activate#(n__take(X1, X2)) -> activate#(X2)) (uTake2#(tt(), M, N, IL) -> activate#(M), activate#(n__take(X1, X2)) -> activate#(X1)) (uTake2#(tt(), M, N, IL) -> activate#(M), activate#(n__nil()) -> nil#()) (uTake2#(tt(), M, N, IL) -> activate#(M), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (uTake2#(tt(), M, N, IL) -> activate#(M), activate#(n__cons(X1, X2)) -> activate#(X1)) (uTake2#(tt(), M, N, IL) -> activate#(M), activate#(n__zeros()) -> zeros#()) (uTake2#(tt(), M, N, IL) -> activate#(M), activate#(n__length(X)) -> length#(activate(X))) (uTake2#(tt(), M, N, IL) -> activate#(M), activate#(n__length(X)) -> activate#(X)) (uTake2#(tt(), M, N, IL) -> activate#(M), activate#(n__s(X)) -> s#(activate(X))) (uTake2#(tt(), M, N, IL) -> activate#(M), activate#(n__s(X)) -> activate#(X)) (uTake2#(tt(), M, N, IL) -> activate#(M), activate#(n__0()) -> 0#()) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L))) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> isNat#(N)) (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)) -> and#(isNat(N), isNatList(activate(L)))) (isNat#(n__length(L)) -> activate#(L), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNat#(n__length(L)) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X2)) (isNat#(n__length(L)) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X1)) (isNat#(n__length(L)) -> activate#(L), activate#(n__nil()) -> nil#()) (isNat#(n__length(L)) -> activate#(L), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNat#(n__length(L)) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNat#(n__length(L)) -> activate#(L), activate#(n__zeros()) -> zeros#()) (isNat#(n__length(L)) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (isNat#(n__length(L)) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (isNat#(n__length(L)) -> activate#(L), activate#(n__s(X)) -> s#(activate(X))) (isNat#(n__length(L)) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (isNat#(n__length(L)) -> activate#(L), activate#(n__0()) -> 0#()) (length#(cons(N, L)) -> activate#(L), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (length#(cons(N, L)) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X2)) (length#(cons(N, L)) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X1)) (length#(cons(N, L)) -> activate#(L), activate#(n__nil()) -> nil#()) (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__zeros()) -> zeros#()) (length#(cons(N, L)) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (length#(cons(N, L)) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__s(X)) -> s#(activate(X))) (length#(cons(N, L)) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__0()) -> 0#()) (isNat#(n__length(L)) -> isNatList#(activate(L)), isNatList#(n__take(N, IL)) -> isNat#(activate(N))) (isNat#(n__length(L)) -> isNatList#(activate(L)), isNatList#(n__take(N, IL)) -> isNatIList#(activate(IL))) (isNat#(n__length(L)) -> isNatList#(activate(L)), isNatList#(n__take(N, IL)) -> activate#(N)) (isNat#(n__length(L)) -> isNatList#(activate(L)), isNatList#(n__take(N, IL)) -> activate#(IL)) (isNat#(n__length(L)) -> isNatList#(activate(L)), isNatList#(n__take(N, IL)) -> and#(isNat(activate(N)), isNatIList(activate(IL)))) (isNat#(n__length(L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> isNat#(activate(N))) (isNat#(n__length(L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(L)) (isNat#(n__length(L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(N)) (isNat#(n__length(L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> isNatList#(activate(L))) (isNat#(n__length(L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> and#(isNat(activate(N)), isNatList(activate(L)))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(N, IL)) -> isNat#(activate(N))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(N, IL)) -> isNatIList#(activate(IL))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(N, IL)) -> activate#(N)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(N, IL)) -> activate#(IL)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(N, IL)) -> and#(isNat(activate(N)), isNatIList(activate(IL)))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> isNat#(activate(N))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(L)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(N)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> isNatList#(activate(L))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> and#(isNat(activate(N)), isNatList(activate(L)))) (isNatList#(n__take(N, IL)) -> isNat#(activate(N)), isNat#(n__length(L)) -> activate#(L)) (isNatList#(n__take(N, IL)) -> isNat#(activate(N)), isNat#(n__length(L)) -> isNatList#(activate(L))) (isNatList#(n__take(N, IL)) -> isNat#(activate(N)), isNat#(n__s(N)) -> isNat#(activate(N))) (isNatList#(n__take(N, IL)) -> isNat#(activate(N)), isNat#(n__s(N)) -> activate#(N)) (isNat#(n__s(N)) -> isNat#(activate(N)), isNat#(n__length(L)) -> activate#(L)) (isNat#(n__s(N)) -> isNat#(activate(N)), isNat#(n__length(L)) -> isNatList#(activate(L))) (isNat#(n__s(N)) -> isNat#(activate(N)), isNat#(n__s(N)) -> isNat#(activate(N))) (isNat#(n__s(N)) -> isNat#(activate(N)), isNat#(n__s(N)) -> activate#(N)) (isNatIList#(IL) -> isNatList#(activate(IL)), isNatList#(n__take(N, IL)) -> isNat#(activate(N))) (isNatIList#(IL) -> isNatList#(activate(IL)), isNatList#(n__take(N, IL)) -> isNatIList#(activate(IL))) (isNatIList#(IL) -> isNatList#(activate(IL)), isNatList#(n__take(N, IL)) -> activate#(N)) (isNatIList#(IL) -> isNatList#(activate(IL)), isNatList#(n__take(N, IL)) -> activate#(IL)) (isNatIList#(IL) -> isNatList#(activate(IL)), isNatList#(n__take(N, IL)) -> and#(isNat(activate(N)), isNatIList(activate(IL)))) (isNatIList#(IL) -> isNatList#(activate(IL)), isNatList#(n__cons(N, L)) -> isNat#(activate(N))) (isNatIList#(IL) -> isNatList#(activate(IL)), isNatList#(n__cons(N, L)) -> activate#(L)) (isNatIList#(IL) -> isNatList#(activate(IL)), isNatList#(n__cons(N, L)) -> activate#(N)) (isNatIList#(IL) -> isNatList#(activate(IL)), isNatList#(n__cons(N, L)) -> isNatList#(activate(L))) (isNatIList#(IL) -> isNatList#(activate(IL)), isNatList#(n__cons(N, L)) -> and#(isNat(activate(N)), isNatList(activate(L)))) (take#(0(), IL) -> uTake1#(isNatIList(IL)), uTake1#(tt()) -> nil#()) (activate#(n__zeros()) -> zeros#(), zeros#() -> 0#()) (activate#(n__zeros()) -> zeros#(), zeros#() -> cons#(0(), n__zeros())) (isNatList#(n__take(N, IL)) -> activate#(N), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatList#(n__take(N, IL)) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatList#(n__take(N, IL)) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatList#(n__take(N, IL)) -> activate#(N), activate#(n__nil()) -> nil#()) (isNatList#(n__take(N, IL)) -> activate#(N), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatList#(n__take(N, IL)) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__take(N, IL)) -> activate#(N), activate#(n__zeros()) -> zeros#()) (isNatList#(n__take(N, IL)) -> activate#(N), activate#(n__length(X)) -> length#(activate(X))) (isNatList#(n__take(N, IL)) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (isNatList#(n__take(N, IL)) -> activate#(N), activate#(n__s(X)) -> s#(activate(X))) (isNatList#(n__take(N, IL)) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (isNatList#(n__take(N, IL)) -> activate#(N), activate#(n__0()) -> 0#()) (isNat#(n__s(N)) -> activate#(N), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNat#(n__s(N)) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X2)) (isNat#(n__s(N)) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X1)) (isNat#(n__s(N)) -> activate#(N), activate#(n__nil()) -> nil#()) (isNat#(n__s(N)) -> activate#(N), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNat#(n__s(N)) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNat#(n__s(N)) -> activate#(N), activate#(n__zeros()) -> zeros#()) (isNat#(n__s(N)) -> activate#(N), activate#(n__length(X)) -> length#(activate(X))) (isNat#(n__s(N)) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (isNat#(n__s(N)) -> activate#(N), activate#(n__s(X)) -> s#(activate(X))) (isNat#(n__s(N)) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (isNat#(n__s(N)) -> activate#(N), activate#(n__0()) -> 0#()) (uTake2#(tt(), M, N, IL) -> activate#(N), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (uTake2#(tt(), M, N, IL) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X2)) (uTake2#(tt(), M, N, IL) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X1)) (uTake2#(tt(), M, N, IL) -> activate#(N), activate#(n__nil()) -> nil#()) (uTake2#(tt(), M, N, IL) -> activate#(N), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (uTake2#(tt(), M, N, IL) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (uTake2#(tt(), M, N, IL) -> activate#(N), activate#(n__zeros()) -> zeros#()) (uTake2#(tt(), M, N, IL) -> activate#(N), activate#(n__length(X)) -> length#(activate(X))) (uTake2#(tt(), M, N, IL) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (uTake2#(tt(), M, N, IL) -> activate#(N), activate#(n__s(X)) -> s#(activate(X))) (uTake2#(tt(), M, N, IL) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (uTake2#(tt(), M, N, IL) -> activate#(N), activate#(n__0()) -> 0#()) (length#(cons(N, L)) -> isNat#(N), isNat#(n__s(N)) -> activate#(N)) (length#(cons(N, L)) -> isNat#(N), isNat#(n__s(N)) -> isNat#(activate(N))) (length#(cons(N, L)) -> isNat#(N), isNat#(n__length(L)) -> isNatList#(activate(L))) (length#(cons(N, L)) -> isNat#(N), isNat#(n__length(L)) -> activate#(L)) (take#(s(M), cons(N, IL)) -> isNat#(N), isNat#(n__s(N)) -> activate#(N)) (take#(s(M), cons(N, IL)) -> isNat#(N), isNat#(n__s(N)) -> isNat#(activate(N))) (take#(s(M), cons(N, IL)) -> isNat#(N), isNat#(n__length(L)) -> isNatList#(activate(L))) (take#(s(M), cons(N, IL)) -> isNat#(N), isNat#(n__length(L)) -> activate#(L)) (isNatIList#(n__cons(N, IL)) -> activate#(N), activate#(n__0()) -> 0#()) (isNatIList#(n__cons(N, IL)) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (isNatIList#(n__cons(N, IL)) -> activate#(N), activate#(n__s(X)) -> s#(activate(X))) (isNatIList#(n__cons(N, IL)) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (isNatIList#(n__cons(N, IL)) -> activate#(N), activate#(n__length(X)) -> length#(activate(X))) (isNatIList#(n__cons(N, IL)) -> activate#(N), activate#(n__zeros()) -> zeros#()) (isNatIList#(n__cons(N, IL)) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatIList#(n__cons(N, IL)) -> activate#(N), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatIList#(n__cons(N, IL)) -> activate#(N), activate#(n__nil()) -> nil#()) (isNatIList#(n__cons(N, IL)) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatIList#(n__cons(N, IL)) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatIList#(n__cons(N, IL)) -> activate#(N), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__0()) -> 0#()) (isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__s(X)) -> s#(activate(X))) (isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__length(X)) -> length#(activate(X))) (isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__zeros()) -> zeros#()) (isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__nil()) -> nil#()) (isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(IL) -> isNatList#(activate(IL))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(IL) -> activate#(IL)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> and#(isNat(activate(N)), isNatIList(activate(IL)))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> activate#(IL)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> activate#(N)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> isNat#(activate(N))) (isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(IL) -> isNatList#(activate(IL))) (isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(IL) -> activate#(IL)) (isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> and#(isNat(activate(N)), isNatIList(activate(IL)))) (isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> activate#(IL)) (isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> activate#(N)) (isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL))) (isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> isNat#(activate(N))) (isNatList#(n__take(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(IL) -> isNatList#(activate(IL))) (isNatList#(n__take(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(IL) -> activate#(IL)) (isNatList#(n__take(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> and#(isNat(activate(N)), isNatIList(activate(IL)))) (isNatList#(n__take(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> activate#(IL)) (isNatList#(n__take(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> activate#(N)) (isNatList#(n__take(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL))) (isNatList#(n__take(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> isNat#(activate(N))) (isNatIList#(n__cons(N, IL)) -> isNat#(activate(N)), isNat#(n__s(N)) -> activate#(N)) (isNatIList#(n__cons(N, IL)) -> isNat#(activate(N)), isNat#(n__s(N)) -> isNat#(activate(N))) (isNatIList#(n__cons(N, IL)) -> isNat#(activate(N)), isNat#(n__length(L)) -> isNatList#(activate(L))) (isNatIList#(n__cons(N, IL)) -> isNat#(activate(N)), isNat#(n__length(L)) -> activate#(L)) (isNatList#(n__cons(N, L)) -> isNat#(activate(N)), isNat#(n__s(N)) -> activate#(N)) (isNatList#(n__cons(N, L)) -> isNat#(activate(N)), isNat#(n__s(N)) -> isNat#(activate(N))) (isNatList#(n__cons(N, L)) -> isNat#(activate(N)), isNat#(n__length(L)) -> isNatList#(activate(L))) (isNatList#(n__cons(N, L)) -> isNat#(activate(N)), isNat#(n__length(L)) -> activate#(L)) (uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> and#(isNat(N), isNatList(activate(L)))) (uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L))) (uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> activate#(L)) (uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNat#(N)) (uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L))) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> and#(isNat(activate(N)), isNatList(activate(L)))) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> isNatList#(activate(L))) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(N)) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(L)) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> isNat#(activate(N))) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(N, IL)) -> and#(isNat(activate(N)), isNatIList(activate(IL)))) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(N, IL)) -> activate#(IL)) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(N, IL)) -> activate#(N)) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(N, IL)) -> isNatIList#(activate(IL))) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(N, IL)) -> isNat#(activate(N))) (uLength#(tt(), L) -> activate#(L), activate#(n__0()) -> 0#()) (uLength#(tt(), L) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (uLength#(tt(), L) -> activate#(L), activate#(n__s(X)) -> s#(activate(X))) (uLength#(tt(), L) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (uLength#(tt(), L) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (uLength#(tt(), L) -> activate#(L), activate#(n__zeros()) -> zeros#()) (uLength#(tt(), L) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (uLength#(tt(), L) -> activate#(L), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (uLength#(tt(), L) -> activate#(L), activate#(n__nil()) -> nil#()) (uLength#(tt(), L) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X1)) (uLength#(tt(), L) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X2)) (uLength#(tt(), L) -> activate#(L), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatList#(n__cons(N, L)) -> activate#(L), activate#(n__0()) -> 0#()) (isNatList#(n__cons(N, L)) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (isNatList#(n__cons(N, L)) -> activate#(L), activate#(n__s(X)) -> s#(activate(X))) (isNatList#(n__cons(N, L)) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (isNatList#(n__cons(N, L)) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (isNatList#(n__cons(N, L)) -> activate#(L), activate#(n__zeros()) -> zeros#()) (isNatList#(n__cons(N, L)) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(N, L)) -> activate#(L), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatList#(n__cons(N, L)) -> activate#(L), activate#(n__nil()) -> nil#()) (isNatList#(n__cons(N, L)) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(N, L)) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatList#(n__cons(N, L)) -> activate#(L), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (take#(s(M), cons(N, IL)) -> isNat#(M), isNat#(n__s(N)) -> activate#(N)) (take#(s(M), cons(N, IL)) -> isNat#(M), isNat#(n__s(N)) -> isNat#(activate(N))) (take#(s(M), cons(N, IL)) -> isNat#(M), isNat#(n__length(L)) -> isNatList#(activate(L))) (take#(s(M), cons(N, IL)) -> isNat#(M), isNat#(n__length(L)) -> activate#(L)) (activate#(n__length(X)) -> activate#(X), activate#(n__0()) -> 0#()) (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__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__zeros()) -> zeros#()) (activate#(n__length(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__length(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (activate#(n__length(X)) -> activate#(X), activate#(n__nil()) -> nil#()) (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__cons(X1, X2)) -> activate#(X1), activate#(n__0()) -> 0#()) (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__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__zeros()) -> zeros#()) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__nil()) -> nil#()) (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))) (uTake2#(tt(), M, N, IL) -> activate#(IL), activate#(n__0()) -> 0#()) (uTake2#(tt(), M, N, IL) -> activate#(IL), activate#(n__s(X)) -> activate#(X)) (uTake2#(tt(), M, N, IL) -> activate#(IL), activate#(n__s(X)) -> s#(activate(X))) (uTake2#(tt(), M, N, IL) -> activate#(IL), activate#(n__length(X)) -> activate#(X)) (uTake2#(tt(), M, N, IL) -> activate#(IL), activate#(n__length(X)) -> length#(activate(X))) (uTake2#(tt(), M, N, IL) -> activate#(IL), activate#(n__zeros()) -> zeros#()) (uTake2#(tt(), M, N, IL) -> activate#(IL), activate#(n__cons(X1, X2)) -> activate#(X1)) (uTake2#(tt(), M, N, IL) -> activate#(IL), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (uTake2#(tt(), M, N, IL) -> activate#(IL), activate#(n__nil()) -> nil#()) (uTake2#(tt(), M, N, IL) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X1)) (uTake2#(tt(), M, N, IL) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X2)) (uTake2#(tt(), M, N, IL) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(IL) -> isNatList#(activate(IL))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(IL) -> activate#(IL)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(N, IL)) -> and#(isNat(activate(N)), isNatIList(activate(IL)))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(N, IL)) -> activate#(IL)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(N, IL)) -> activate#(N)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(N, IL)) -> isNat#(activate(N))) (isNatIList#(IL) -> activate#(IL), activate#(n__0()) -> 0#()) (isNatIList#(IL) -> activate#(IL), activate#(n__s(X)) -> activate#(X)) (isNatIList#(IL) -> activate#(IL), activate#(n__s(X)) -> s#(activate(X))) (isNatIList#(IL) -> activate#(IL), activate#(n__length(X)) -> activate#(X)) (isNatIList#(IL) -> activate#(IL), activate#(n__length(X)) -> length#(activate(X))) (isNatIList#(IL) -> activate#(IL), activate#(n__zeros()) -> zeros#()) (isNatIList#(IL) -> activate#(IL), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatIList#(IL) -> activate#(IL), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatIList#(IL) -> activate#(IL), activate#(n__nil()) -> nil#()) (isNatIList#(IL) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatIList#(IL) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatIList#(IL) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (isNatList#(n__take(N, IL)) -> activate#(IL), activate#(n__0()) -> 0#()) (isNatList#(n__take(N, IL)) -> activate#(IL), activate#(n__s(X)) -> activate#(X)) (isNatList#(n__take(N, IL)) -> activate#(IL), activate#(n__s(X)) -> s#(activate(X))) (isNatList#(n__take(N, IL)) -> activate#(IL), activate#(n__length(X)) -> activate#(X)) (isNatList#(n__take(N, IL)) -> activate#(IL), activate#(n__length(X)) -> length#(activate(X))) (isNatList#(n__take(N, IL)) -> activate#(IL), activate#(n__zeros()) -> zeros#()) (isNatList#(n__take(N, IL)) -> activate#(IL), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__take(N, IL)) -> activate#(IL), activate#(n__cons(X1, X2)) -> cons#(activate(X1), X2)) (isNatList#(n__take(N, IL)) -> activate#(IL), activate#(n__nil()) -> nil#()) (isNatList#(n__take(N, IL)) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X1)) (isNatList#(n__take(N, IL)) -> activate#(IL), activate#(n__take(X1, X2)) -> activate#(X2)) (isNatList#(n__take(N, IL)) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2))) (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) -> uTake1#(isNatIList(IL))) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(s(M), cons(N, IL)) -> and#(isNat(N), isNatIList(activate(IL)))) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(s(M), cons(N, IL)) -> and#(isNat(M), and(isNat(N), 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)) -> isNatIList#(activate(IL))) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(s(M), cons(N, IL)) -> isNat#(N)) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(s(M), cons(N, IL)) -> isNat#(M)) (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(s(M), cons(N, IL)) -> uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))) } SCCS: Scc: { isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(N), isNatList#(n__cons(N, L)) -> activate#(L), isNatList#(n__cons(N, L)) -> isNat#(activate(N)), isNatList#(n__take(N, IL)) -> activate#(IL), isNatList#(n__take(N, IL)) -> activate#(N), isNatList#(n__take(N, IL)) -> isNatIList#(activate(IL)), isNatList#(n__take(N, IL)) -> isNat#(activate(N)), activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X)), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), isNatIList#(IL) -> isNatList#(activate(IL)), isNatIList#(IL) -> activate#(IL), isNatIList#(n__cons(N, IL)) -> activate#(IL), isNatIList#(n__cons(N, IL)) -> activate#(N), isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> isNat#(activate(N)), isNat#(n__s(N)) -> activate#(N), isNat#(n__s(N)) -> isNat#(activate(N)), isNat#(n__length(L)) -> isNatList#(activate(L)), isNat#(n__length(L)) -> activate#(L), take#(0(), IL) -> isNatIList#(IL), take#(s(M), cons(N, IL)) -> activate#(IL), take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), take#(s(M), cons(N, IL)) -> isNat#(N), take#(s(M), cons(N, IL)) -> isNat#(M), take#(s(M), cons(N, IL)) -> uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), uTake2#(tt(), M, N, IL) -> activate#(IL), uTake2#(tt(), M, N, IL) -> activate#(N), uTake2#(tt(), M, N, IL) -> activate#(M), uLength#(tt(), L) -> activate#(L), uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L)), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> isNat#(N), length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L))} SCC: Strict: { isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(N), isNatList#(n__cons(N, L)) -> activate#(L), isNatList#(n__cons(N, L)) -> isNat#(activate(N)), isNatList#(n__take(N, IL)) -> activate#(IL), isNatList#(n__take(N, IL)) -> activate#(N), isNatList#(n__take(N, IL)) -> isNatIList#(activate(IL)), isNatList#(n__take(N, IL)) -> isNat#(activate(N)), activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X)), activate#(n__cons(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), isNatIList#(IL) -> isNatList#(activate(IL)), isNatIList#(IL) -> activate#(IL), isNatIList#(n__cons(N, IL)) -> activate#(IL), isNatIList#(n__cons(N, IL)) -> activate#(N), isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> isNat#(activate(N)), isNat#(n__s(N)) -> activate#(N), isNat#(n__s(N)) -> isNat#(activate(N)), isNat#(n__length(L)) -> isNatList#(activate(L)), isNat#(n__length(L)) -> activate#(L), take#(0(), IL) -> isNatIList#(IL), take#(s(M), cons(N, IL)) -> activate#(IL), take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), take#(s(M), cons(N, IL)) -> isNat#(N), take#(s(M), cons(N, IL)) -> isNat#(M), take#(s(M), cons(N, IL)) -> uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), uTake2#(tt(), M, N, IL) -> activate#(IL), uTake2#(tt(), M, N, IL) -> activate#(N), uTake2#(tt(), M, N, IL) -> activate#(M), uLength#(tt(), L) -> activate#(L), uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L)), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> isNat#(N), length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L))} Weak: { and(tt(), T) -> T, isNatList(n__cons(N, L)) -> and(isNat(activate(N)), isNatList(activate(L))), isNatList(n__nil()) -> tt(), isNatList(n__take(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__s(X)) -> s(activate(X)), activate(n__length(X)) -> length(activate(X)), activate(n__zeros()) -> zeros(), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)), isNatIList(IL) -> isNatList(activate(IL)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), isNat(n__0()) -> tt(), isNat(n__s(N)) -> isNat(activate(N)), isNat(n__length(L)) -> isNatList(activate(L)), cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1(tt()) -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1(isNatIList(IL)), take(s(M), cons(N, IL)) -> uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate(N), n__take(activate(M), activate(IL))), s(X) -> n__s(X), uLength(tt(), L) -> s(length(activate(L))), length(X) -> n__length(X), length(cons(N, L)) -> uLength(and(isNat(N), isNatList(activate(L))), activate(L))} POLY: Argument Filtering: pi(length#) = 0, pi(length) = 0, pi(uLength#) = 1, pi(uLength) = 1, pi(s) = 0, pi(uTake2#) = [1,2,3], pi(uTake2) = [1,2,3], pi(nil) = [], pi(take#) = [0,1], pi(take) = [0,1], pi(uTake1) = [], pi(zeros) = [], pi(0) = [], pi(cons) = [0,1], pi(n__take) = [0,1], pi(n__nil) = [], pi(n__cons) = [0,1], pi(n__zeros) = [], pi(n__length) = 0, pi(n__s) = 0, pi(n__0) = [], pi(isNat#) = 0, pi(isNat) = [], pi(isNatIList#) = 0, pi(isNatIList) = [], pi(activate#) = 0, pi(activate) = 0, pi(isNatList#) = 0, pi(isNatList) = [], pi(tt) = [], pi(and) = [] Usable Rules: {} Interpretation: [uTake2#](x0, x1, x2) = x0 + x1 + x2, [take#](x0, x1) = x0 + x1, [cons](x0, x1) = x0 + x1, [n__take](x0, x1) = x0 + x1 + 1, [n__cons](x0, x1) = x0 + x1, [0] = 0 Strict: { isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(N), isNatList#(n__cons(N, L)) -> activate#(L), isNatList#(n__cons(N, L)) -> isNat#(activate(N)), activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X)), activate#(n__cons(X1, X2)) -> activate#(X1), isNatIList#(IL) -> isNatList#(activate(IL)), isNatIList#(IL) -> activate#(IL), isNatIList#(n__cons(N, IL)) -> activate#(IL), isNatIList#(n__cons(N, IL)) -> activate#(N), isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> isNat#(activate(N)), isNat#(n__s(N)) -> activate#(N), isNat#(n__s(N)) -> isNat#(activate(N)), isNat#(n__length(L)) -> isNatList#(activate(L)), isNat#(n__length(L)) -> activate#(L), take#(0(), IL) -> isNatIList#(IL), take#(s(M), cons(N, IL)) -> activate#(IL), take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), take#(s(M), cons(N, IL)) -> isNat#(N), take#(s(M), cons(N, IL)) -> isNat#(M), take#(s(M), cons(N, IL)) -> uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), uTake2#(tt(), M, N, IL) -> activate#(IL), uTake2#(tt(), M, N, IL) -> activate#(N), uTake2#(tt(), M, N, IL) -> activate#(M), uLength#(tt(), L) -> activate#(L), uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L)), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> isNat#(N), length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L))} Weak: { and(tt(), T) -> T, isNatList(n__cons(N, L)) -> and(isNat(activate(N)), isNatList(activate(L))), isNatList(n__nil()) -> tt(), isNatList(n__take(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__s(X)) -> s(activate(X)), activate(n__length(X)) -> length(activate(X)), activate(n__zeros()) -> zeros(), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)), isNatIList(IL) -> isNatList(activate(IL)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), isNat(n__0()) -> tt(), isNat(n__s(N)) -> isNat(activate(N)), isNat(n__length(L)) -> isNatList(activate(L)), cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1(tt()) -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1(isNatIList(IL)), take(s(M), cons(N, IL)) -> uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate(N), n__take(activate(M), activate(IL))), s(X) -> n__s(X), uLength(tt(), L) -> s(length(activate(L))), length(X) -> n__length(X), length(cons(N, L)) -> uLength(and(isNat(N), isNatList(activate(L))), activate(L))} EDG: { (isNat#(n__length(L)) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNat#(n__length(L)) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (isNat#(n__length(L)) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (isNat#(n__length(L)) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (length#(cons(N, L)) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (length#(cons(N, L)) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (length#(cons(N, L)) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (take#(s(M), cons(N, IL)) -> uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), uTake2#(tt(), M, N, IL) -> activate#(M)) (take#(s(M), cons(N, IL)) -> uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), uTake2#(tt(), M, N, IL) -> activate#(N)) (take#(s(M), cons(N, IL)) -> uTake2#(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), uTake2#(tt(), M, N, IL) -> activate#(IL)) (isNatIList#(n__cons(N, IL)) -> activate#(IL), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatIList#(n__cons(N, IL)) -> activate#(IL), activate#(n__length(X)) -> length#(activate(X))) (isNatIList#(n__cons(N, IL)) -> activate#(IL), activate#(n__length(X)) -> activate#(X)) (isNatIList#(n__cons(N, IL)) -> activate#(IL), activate#(n__s(X)) -> activate#(X)) (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__length(X)) -> length#(activate(X))) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__length(X)) -> activate#(X)) (take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__s(X)) -> activate#(X)) (take#(s(M), cons(N, IL)) -> isNat#(M), isNat#(n__length(L)) -> activate#(L)) (take#(s(M), cons(N, IL)) -> isNat#(M), isNat#(n__length(L)) -> isNatList#(activate(L))) (take#(s(M), cons(N, IL)) -> isNat#(M), isNat#(n__s(N)) -> isNat#(activate(N))) (take#(s(M), cons(N, IL)) -> isNat#(M), isNat#(n__s(N)) -> activate#(N)) (length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L)), uLength#(tt(), L) -> length#(activate(L))) (length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L)), uLength#(tt(), L) -> activate#(L)) (isNatIList#(n__cons(N, IL)) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatIList#(n__cons(N, IL)) -> activate#(N), activate#(n__length(X)) -> length#(activate(X))) (isNatIList#(n__cons(N, IL)) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (isNatIList#(n__cons(N, IL)) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (take#(s(M), cons(N, IL)) -> isNat#(N), isNat#(n__length(L)) -> activate#(L)) (take#(s(M), cons(N, IL)) -> isNat#(N), isNat#(n__length(L)) -> isNatList#(activate(L))) (take#(s(M), cons(N, IL)) -> isNat#(N), isNat#(n__s(N)) -> isNat#(activate(N))) (take#(s(M), cons(N, IL)) -> isNat#(N), isNat#(n__s(N)) -> activate#(N)) (length#(cons(N, L)) -> isNat#(N), isNat#(n__length(L)) -> activate#(L)) (length#(cons(N, L)) -> isNat#(N), isNat#(n__length(L)) -> isNatList#(activate(L))) (length#(cons(N, L)) -> isNat#(N), isNat#(n__s(N)) -> isNat#(activate(N))) (length#(cons(N, L)) -> isNat#(N), isNat#(n__s(N)) -> activate#(N)) (activate#(n__length(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X)) (activate#(n__length(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> isNat#(activate(N))) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(L)) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(N)) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> isNatList#(activate(L))) (uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L))) (uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNat#(N)) (uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> activate#(L)) (uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L))) (isNatList#(n__cons(N, L)) -> isNat#(activate(N)), isNat#(n__length(L)) -> activate#(L)) (isNatList#(n__cons(N, L)) -> isNat#(activate(N)), isNat#(n__length(L)) -> isNatList#(activate(L))) (isNatList#(n__cons(N, L)) -> isNat#(activate(N)), isNat#(n__s(N)) -> isNat#(activate(N))) (isNatList#(n__cons(N, L)) -> isNat#(activate(N)), isNat#(n__s(N)) -> activate#(N)) (isNat#(n__s(N)) -> isNat#(activate(N)), isNat#(n__length(L)) -> activate#(L)) (isNat#(n__s(N)) -> isNat#(activate(N)), isNat#(n__length(L)) -> isNatList#(activate(L))) (isNat#(n__s(N)) -> isNat#(activate(N)), isNat#(n__s(N)) -> isNat#(activate(N))) (isNat#(n__s(N)) -> isNat#(activate(N)), isNat#(n__s(N)) -> activate#(N)) (isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> isNat#(activate(N))) (isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL))) (isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> activate#(N)) (isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> activate#(IL)) (isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(IL) -> activate#(IL)) (isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(IL) -> isNatList#(activate(IL))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(IL) -> isNatList#(activate(IL))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(IL) -> activate#(IL)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> activate#(IL)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> activate#(N)) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL))) (take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(N, IL)) -> isNat#(activate(N))) (isNatIList#(IL) -> isNatList#(activate(IL)), isNatList#(n__cons(N, L)) -> isNatList#(activate(L))) (isNatIList#(IL) -> isNatList#(activate(IL)), isNatList#(n__cons(N, L)) -> activate#(N)) (isNatIList#(IL) -> isNatList#(activate(IL)), isNatList#(n__cons(N, L)) -> activate#(L)) (isNatIList#(IL) -> isNatList#(activate(IL)), isNatList#(n__cons(N, L)) -> isNat#(activate(N))) (isNatIList#(n__cons(N, IL)) -> isNat#(activate(N)), isNat#(n__s(N)) -> activate#(N)) (isNatIList#(n__cons(N, IL)) -> isNat#(activate(N)), isNat#(n__s(N)) -> isNat#(activate(N))) (isNatIList#(n__cons(N, IL)) -> isNat#(activate(N)), isNat#(n__length(L)) -> isNatList#(activate(L))) (isNatIList#(n__cons(N, IL)) -> isNat#(activate(N)), isNat#(n__length(L)) -> activate#(L)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> isNatList#(activate(L))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(N)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(L)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> isNat#(activate(N))) (isNat#(n__length(L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> isNatList#(activate(L))) (isNat#(n__length(L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(N)) (isNat#(n__length(L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(L)) (isNat#(n__length(L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> isNat#(activate(N))) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> isNatList#(activate(L))) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> activate#(L)) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> isNat#(N)) (activate#(n__length(X)) -> length#(activate(X)), length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L))) (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X)) (activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X))) (activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)) (uTake2#(tt(), M, N, IL) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (uTake2#(tt(), M, N, IL) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (uTake2#(tt(), M, N, IL) -> activate#(N), activate#(n__length(X)) -> length#(activate(X))) (uTake2#(tt(), M, N, IL) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNat#(n__s(N)) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (isNat#(n__s(N)) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (isNat#(n__s(N)) -> activate#(N), activate#(n__length(X)) -> length#(activate(X))) (isNat#(n__s(N)) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__length(X)) -> activate#(X)) (isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__length(X)) -> length#(activate(X))) (isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (uTake2#(tt(), M, N, IL) -> activate#(M), activate#(n__s(X)) -> activate#(X)) (uTake2#(tt(), M, N, IL) -> activate#(M), activate#(n__length(X)) -> activate#(X)) (uTake2#(tt(), M, N, IL) -> activate#(M), activate#(n__length(X)) -> length#(activate(X))) (uTake2#(tt(), M, N, IL) -> activate#(M), activate#(n__cons(X1, X2)) -> activate#(X1)) (uTake2#(tt(), M, N, IL) -> activate#(IL), activate#(n__s(X)) -> activate#(X)) (uTake2#(tt(), M, N, IL) -> activate#(IL), activate#(n__length(X)) -> activate#(X)) (uTake2#(tt(), M, N, IL) -> activate#(IL), activate#(n__length(X)) -> length#(activate(X))) (uTake2#(tt(), M, N, IL) -> activate#(IL), activate#(n__cons(X1, X2)) -> activate#(X1)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(IL) -> isNatList#(activate(IL))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(IL) -> activate#(IL)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(N, IL)) -> activate#(IL)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(N, IL)) -> activate#(N)) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL))) (take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(N, IL)) -> isNat#(activate(N))) (isNatIList#(IL) -> activate#(IL), activate#(n__s(X)) -> activate#(X)) (isNatIList#(IL) -> activate#(IL), activate#(n__length(X)) -> activate#(X)) (isNatIList#(IL) -> activate#(IL), activate#(n__length(X)) -> length#(activate(X))) (isNatIList#(IL) -> activate#(IL), 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)) -> 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__cons(X1, X2)) -> activate#(X1)) (uLength#(tt(), L) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (uLength#(tt(), L) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (uLength#(tt(), L) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (uLength#(tt(), L) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(N, L)) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (isNatList#(n__cons(N, L)) -> activate#(L), activate#(n__length(X)) -> activate#(X)) (isNatList#(n__cons(N, L)) -> activate#(L), activate#(n__length(X)) -> length#(activate(X))) (isNatList#(n__cons(N, L)) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) } SCCS: Scc: {isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL))} Scc: { isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(N), isNatList#(n__cons(N, L)) -> activate#(L), isNatList#(n__cons(N, L)) -> isNat#(activate(N)), activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X)), activate#(n__cons(X1, X2)) -> activate#(X1), isNat#(n__s(N)) -> activate#(N), isNat#(n__s(N)) -> isNat#(activate(N)), isNat#(n__length(L)) -> isNatList#(activate(L)), isNat#(n__length(L)) -> activate#(L), uLength#(tt(), L) -> activate#(L), uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L)), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> isNat#(N), length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L))} SCC: Strict: {isNatIList#(n__cons(N, IL)) -> isNatIList#(activate(IL))} Weak: { and(tt(), T) -> T, isNatList(n__cons(N, L)) -> and(isNat(activate(N)), isNatList(activate(L))), isNatList(n__nil()) -> tt(), isNatList(n__take(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__s(X)) -> s(activate(X)), activate(n__length(X)) -> length(activate(X)), activate(n__zeros()) -> zeros(), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)), isNatIList(IL) -> isNatList(activate(IL)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), isNat(n__0()) -> tt(), isNat(n__s(N)) -> isNat(activate(N)), isNat(n__length(L)) -> isNatList(activate(L)), cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1(tt()) -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1(isNatIList(IL)), take(s(M), cons(N, IL)) -> uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate(N), n__take(activate(M), activate(IL))), s(X) -> n__s(X), uLength(tt(), L) -> s(length(activate(L))), length(X) -> n__length(X), length(cons(N, L)) -> uLength(and(isNat(N), isNatList(activate(L))), activate(L))} Fail SCC: Strict: { isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(N), isNatList#(n__cons(N, L)) -> activate#(L), isNatList#(n__cons(N, L)) -> isNat#(activate(N)), activate#(n__s(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X)), activate#(n__cons(X1, X2)) -> activate#(X1), isNat#(n__s(N)) -> activate#(N), isNat#(n__s(N)) -> isNat#(activate(N)), isNat#(n__length(L)) -> isNatList#(activate(L)), isNat#(n__length(L)) -> activate#(L), uLength#(tt(), L) -> activate#(L), uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L)), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> isNat#(N), length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L))} Weak: { and(tt(), T) -> T, isNatList(n__cons(N, L)) -> and(isNat(activate(N)), isNatList(activate(L))), isNatList(n__nil()) -> tt(), isNatList(n__take(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__s(X)) -> s(activate(X)), activate(n__length(X)) -> length(activate(X)), activate(n__zeros()) -> zeros(), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)), isNatIList(IL) -> isNatList(activate(IL)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), isNat(n__0()) -> tt(), isNat(n__s(N)) -> isNat(activate(N)), isNat(n__length(L)) -> isNatList(activate(L)), cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1(tt()) -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1(isNatIList(IL)), take(s(M), cons(N, IL)) -> uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate(N), n__take(activate(M), activate(IL))), s(X) -> n__s(X), uLength(tt(), L) -> s(length(activate(L))), length(X) -> n__length(X), length(cons(N, L)) -> uLength(and(isNat(N), isNatList(activate(L))), activate(L))} POLY: Argument Filtering: pi(length#) = 0, pi(length) = [0], pi(uLength#) = 1, pi(uLength) = [1], pi(s) = 0, pi(uTake2) = [2,3], pi(nil) = [], pi(take) = 1, pi(uTake1) = [], pi(zeros) = [], pi(0) = [], pi(cons) = [0,1], pi(n__take) = 1, pi(n__nil) = [], pi(n__cons) = [0,1], pi(n__zeros) = [], pi(n__length) = [0], pi(n__s) = 0, pi(n__0) = [], pi(isNat#) = 0, pi(isNat) = [], pi(isNatIList) = [], pi(activate#) = 0, pi(activate) = 0, pi(isNatList#) = 0, pi(isNatList) = [], pi(tt) = [], pi(and) = [] Usable Rules: {} Interpretation: [cons](x0, x1) = x0 + x1, [n__cons](x0, x1) = x0 + x1, [n__length](x0) = x0 + 1 Strict: { isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(N), isNatList#(n__cons(N, L)) -> activate#(L), isNatList#(n__cons(N, L)) -> isNat#(activate(N)), activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1), isNat#(n__s(N)) -> activate#(N), isNat#(n__s(N)) -> isNat#(activate(N)), uLength#(tt(), L) -> activate#(L), uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L)), length#(cons(N, L)) -> activate#(L), length#(cons(N, L)) -> isNat#(N), length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L))} Weak: { and(tt(), T) -> T, isNatList(n__cons(N, L)) -> and(isNat(activate(N)), isNatList(activate(L))), isNatList(n__nil()) -> tt(), isNatList(n__take(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__s(X)) -> s(activate(X)), activate(n__length(X)) -> length(activate(X)), activate(n__zeros()) -> zeros(), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)), isNatIList(IL) -> isNatList(activate(IL)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), isNat(n__0()) -> tt(), isNat(n__s(N)) -> isNat(activate(N)), isNat(n__length(L)) -> isNatList(activate(L)), cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1(tt()) -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1(isNatIList(IL)), take(s(M), cons(N, IL)) -> uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate(N), n__take(activate(M), activate(IL))), s(X) -> n__s(X), uLength(tt(), L) -> s(length(activate(L))), length(X) -> n__length(X), length(cons(N, L)) -> uLength(and(isNat(N), isNatList(activate(L))), activate(L))} EDG: {(isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(N, L)) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (length#(cons(N, L)) -> isNat#(N), isNat#(n__s(N)) -> isNat#(activate(N))) (length#(cons(N, L)) -> isNat#(N), isNat#(n__s(N)) -> activate#(N)) (uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L))) (uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNat#(N)) (uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> activate#(L)) (uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L))) (isNatList#(n__cons(N, L)) -> isNat#(activate(N)), isNat#(n__s(N)) -> isNat#(activate(N))) (isNatList#(n__cons(N, L)) -> isNat#(activate(N)), isNat#(n__s(N)) -> activate#(N)) (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(N, L)) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (isNatList#(n__cons(N, L)) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (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)) (uLength#(tt(), L) -> activate#(L), activate#(n__s(X)) -> activate#(X)) (uLength#(tt(), L) -> activate#(L), activate#(n__cons(X1, X2)) -> activate#(X1)) (length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L)), uLength#(tt(), L) -> activate#(L)) (length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L)), uLength#(tt(), L) -> length#(activate(L))) (isNat#(n__s(N)) -> isNat#(activate(N)), isNat#(n__s(N)) -> activate#(N)) (isNat#(n__s(N)) -> isNat#(activate(N)), isNat#(n__s(N)) -> isNat#(activate(N))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> isNatList#(activate(L))) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(N)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(L)) (length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> isNat#(activate(N))) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> isNatList#(activate(L))) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(N)) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> activate#(L)) (isNatList#(n__cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(N, L)) -> isNat#(activate(N))) (isNat#(n__s(N)) -> activate#(N), activate#(n__s(X)) -> activate#(X)) (isNat#(n__s(N)) -> activate#(N), 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))} SCCS: Scc: { uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L))} Scc: {isNat#(n__s(N)) -> isNat#(activate(N))} Scc: { activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)} Scc: {isNatList#(n__cons(N, L)) -> isNatList#(activate(L))} SCC: Strict: { uLength#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> uLength#(and(isNat(N), isNatList(activate(L))), activate(L))} Weak: { and(tt(), T) -> T, isNatList(n__cons(N, L)) -> and(isNat(activate(N)), isNatList(activate(L))), isNatList(n__nil()) -> tt(), isNatList(n__take(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__s(X)) -> s(activate(X)), activate(n__length(X)) -> length(activate(X)), activate(n__zeros()) -> zeros(), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)), isNatIList(IL) -> isNatList(activate(IL)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), isNat(n__0()) -> tt(), isNat(n__s(N)) -> isNat(activate(N)), isNat(n__length(L)) -> isNatList(activate(L)), cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1(tt()) -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1(isNatIList(IL)), take(s(M), cons(N, IL)) -> uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate(N), n__take(activate(M), activate(IL))), s(X) -> n__s(X), uLength(tt(), L) -> s(length(activate(L))), length(X) -> n__length(X), length(cons(N, L)) -> uLength(and(isNat(N), isNatList(activate(L))), activate(L))} Fail SCC: Strict: {isNat#(n__s(N)) -> isNat#(activate(N))} Weak: { and(tt(), T) -> T, isNatList(n__cons(N, L)) -> and(isNat(activate(N)), isNatList(activate(L))), isNatList(n__nil()) -> tt(), isNatList(n__take(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__s(X)) -> s(activate(X)), activate(n__length(X)) -> length(activate(X)), activate(n__zeros()) -> zeros(), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)), isNatIList(IL) -> isNatList(activate(IL)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), isNat(n__0()) -> tt(), isNat(n__s(N)) -> isNat(activate(N)), isNat(n__length(L)) -> isNatList(activate(L)), cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1(tt()) -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1(isNatIList(IL)), take(s(M), cons(N, IL)) -> uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate(N), n__take(activate(M), activate(IL))), s(X) -> n__s(X), uLength(tt(), L) -> s(length(activate(L))), length(X) -> n__length(X), length(cons(N, L)) -> uLength(and(isNat(N), isNatList(activate(L))), activate(L))} Fail SCC: Strict: { activate#(n__s(X)) -> activate#(X), activate#(n__cons(X1, X2)) -> activate#(X1)} Weak: { and(tt(), T) -> T, isNatList(n__cons(N, L)) -> and(isNat(activate(N)), isNatList(activate(L))), isNatList(n__nil()) -> tt(), isNatList(n__take(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__s(X)) -> s(activate(X)), activate(n__length(X)) -> length(activate(X)), activate(n__zeros()) -> zeros(), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)), isNatIList(IL) -> isNatList(activate(IL)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), isNat(n__0()) -> tt(), isNat(n__s(N)) -> isNat(activate(N)), isNat(n__length(L)) -> isNatList(activate(L)), cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1(tt()) -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1(isNatIList(IL)), take(s(M), cons(N, IL)) -> uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate(N), n__take(activate(M), activate(IL))), s(X) -> n__s(X), uLength(tt(), L) -> s(length(activate(L))), length(X) -> n__length(X), length(cons(N, L)) -> uLength(and(isNat(N), isNatList(activate(L))), activate(L))} 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: { and(tt(), T) -> T, isNatList(n__cons(N, L)) -> and(isNat(activate(N)), isNatList(activate(L))), isNatList(n__nil()) -> tt(), isNatList(n__take(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__s(X)) -> s(activate(X)), activate(n__length(X)) -> length(activate(X)), activate(n__zeros()) -> zeros(), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)), isNatIList(IL) -> isNatList(activate(IL)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), isNat(n__0()) -> tt(), isNat(n__s(N)) -> isNat(activate(N)), isNat(n__length(L)) -> isNatList(activate(L)), cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1(tt()) -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1(isNatIList(IL)), take(s(M), cons(N, IL)) -> uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate(N), n__take(activate(M), activate(IL))), s(X) -> n__s(X), uLength(tt(), L) -> s(length(activate(L))), length(X) -> n__length(X), length(cons(N, L)) -> uLength(and(isNat(N), isNatList(activate(L))), activate(L))} SPSC: Simple Projection: pi(activate#) = 0 Strict: {} Qed SCC: Strict: {isNatList#(n__cons(N, L)) -> isNatList#(activate(L))} Weak: { and(tt(), T) -> T, isNatList(n__cons(N, L)) -> and(isNat(activate(N)), isNatList(activate(L))), isNatList(n__nil()) -> tt(), isNatList(n__take(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), activate(X) -> X, activate(n__0()) -> 0(), activate(n__s(X)) -> s(activate(X)), activate(n__length(X)) -> length(activate(X)), activate(n__zeros()) -> zeros(), activate(n__cons(X1, X2)) -> cons(activate(X1), X2), activate(n__nil()) -> nil(), activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)), isNatIList(IL) -> isNatList(activate(IL)), isNatIList(n__zeros()) -> tt(), isNatIList(n__cons(N, IL)) -> and(isNat(activate(N)), isNatIList(activate(IL))), isNat(n__0()) -> tt(), isNat(n__s(N)) -> isNat(activate(N)), isNat(n__length(L)) -> isNatList(activate(L)), cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1(tt()) -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1(isNatIList(IL)), take(s(M), cons(N, IL)) -> uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL)), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate(N), n__take(activate(M), activate(IL))), s(X) -> n__s(X), uLength(tt(), L) -> s(length(activate(L))), length(X) -> n__length(X), length(cons(N, L)) -> uLength(and(isNat(N), isNatList(activate(L))), activate(L))} Fail