(VAR IL L M N V V1 V2 X X1 X2 X3 X4 ) (RULES active(zeros) -> mark(cons(0, zeros)) active(U11(tt, V1)) -> mark(U12(isNatList(V1))) active(U12(tt)) -> mark(tt) active(U21(tt, V1)) -> mark(U22(isNat(V1))) active(U22(tt)) -> mark(tt) active(U31(tt, V)) -> mark(U32(isNatList(V))) active(U32(tt)) -> mark(tt) active(U41(tt, V1, V2)) -> mark(U42(isNat(V1), V2)) active(U42(tt, V2)) -> mark(U43(isNatIList(V2))) active(U43(tt)) -> mark(tt) active(U51(tt, V1, V2)) -> mark(U52(isNat(V1), V2)) active(U52(tt, V2)) -> mark(U53(isNatList(V2))) active(U53(tt)) -> mark(tt) active(U61(tt, V1, V2)) -> mark(U62(isNat(V1), V2)) active(U62(tt, V2)) -> mark(U63(isNatIList(V2))) active(U63(tt)) -> mark(tt) active(U71(tt, L)) -> mark(s(length(L))) active(U81(tt)) -> mark(nil) active(U91(tt, IL, M, N)) -> mark(cons(N, take(M, IL))) active(and(tt, X)) -> mark(X) active(isNat(0)) -> mark(tt) active(isNat(length(V1))) -> mark(U11(isNatIListKind(V1), V1)) active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V)) active(isNatIList(zeros)) -> mark(tt) active(isNatIList(cons(V1, V2))) -> mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) active(isNatIListKind(nil)) -> mark(tt) active(isNatIListKind(zeros)) -> mark(tt) active(isNatIListKind(cons(V1, V2))) -> mark(and(isNatKind(V1), isNatIListKind(V2))) active(isNatIListKind(take(V1, V2))) -> mark(and(isNatKind(V1), isNatIListKind(V2))) active(isNatKind(0)) -> mark(tt) active(isNatKind(length(V1))) -> mark(isNatIListKind(V1)) active(isNatKind(s(V1))) -> mark(isNatKind(V1)) active(isNatList(nil)) -> mark(tt) active(isNatList(cons(V1, V2))) -> mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) active(isNatList(take(V1, V2))) -> mark(U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) active(length(nil)) -> mark(0) active(length(cons(N, L))) -> mark(U71(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)) active(take(0, IL)) -> mark(U81(and(isNatIList(IL), isNatIListKind(IL)))) active(take(s(M), cons(N, IL))) -> mark(U91(and(and(isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), IL, M, N)) mark(zeros) -> active(zeros) mark(cons(X1, X2)) -> active(cons(mark(X1), X2)) mark(0) -> active(0) mark(U11(X1, X2)) -> active(U11(mark(X1), X2)) mark(tt) -> active(tt) mark(U12(X)) -> active(U12(mark(X))) mark(isNatList(X)) -> active(isNatList(X)) mark(U21(X1, X2)) -> active(U21(mark(X1), X2)) mark(U22(X)) -> active(U22(mark(X))) mark(isNat(X)) -> active(isNat(X)) mark(U31(X1, X2)) -> active(U31(mark(X1), X2)) mark(U32(X)) -> active(U32(mark(X))) mark(U41(X1, X2, X3)) -> active(U41(mark(X1), X2, X3)) mark(U42(X1, X2)) -> active(U42(mark(X1), X2)) mark(U43(X)) -> active(U43(mark(X))) mark(isNatIList(X)) -> active(isNatIList(X)) mark(U51(X1, X2, X3)) -> active(U51(mark(X1), X2, X3)) mark(U52(X1, X2)) -> active(U52(mark(X1), X2)) mark(U53(X)) -> active(U53(mark(X))) mark(U61(X1, X2, X3)) -> active(U61(mark(X1), X2, X3)) mark(U62(X1, X2)) -> active(U62(mark(X1), X2)) mark(U63(X)) -> active(U63(mark(X))) mark(U71(X1, X2)) -> active(U71(mark(X1), X2)) mark(s(X)) -> active(s(mark(X))) mark(length(X)) -> active(length(mark(X))) mark(U81(X)) -> active(U81(mark(X))) mark(nil) -> active(nil) mark(U91(X1, X2, X3, X4)) -> active(U91(mark(X1), X2, X3, X4)) mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))) mark(and(X1, X2)) -> active(and(mark(X1), X2)) mark(isNatIListKind(X)) -> active(isNatIListKind(X)) mark(isNatKind(X)) -> active(isNatKind(X)) cons(mark(X1), X2) -> cons(X1, X2) cons(X1, mark(X2)) -> cons(X1, X2) cons(active(X1), X2) -> cons(X1, X2) cons(X1, active(X2)) -> cons(X1, X2) U11(mark(X1), X2) -> U11(X1, X2) U11(X1, mark(X2)) -> U11(X1, X2) U11(active(X1), X2) -> U11(X1, X2) U11(X1, active(X2)) -> U11(X1, X2) U12(mark(X)) -> U12(X) U12(active(X)) -> U12(X) isNatList(mark(X)) -> isNatList(X) isNatList(active(X)) -> isNatList(X) U21(mark(X1), X2) -> U21(X1, X2) U21(X1, mark(X2)) -> U21(X1, X2) U21(active(X1), X2) -> U21(X1, X2) U21(X1, active(X2)) -> U21(X1, X2) U22(mark(X)) -> U22(X) U22(active(X)) -> U22(X) isNat(mark(X)) -> isNat(X) isNat(active(X)) -> isNat(X) U31(mark(X1), X2) -> U31(X1, X2) U31(X1, mark(X2)) -> U31(X1, X2) U31(active(X1), X2) -> U31(X1, X2) U31(X1, active(X2)) -> U31(X1, X2) U32(mark(X)) -> U32(X) U32(active(X)) -> U32(X) U41(mark(X1), X2, X3) -> U41(X1, X2, X3) U41(X1, mark(X2), X3) -> U41(X1, X2, X3) U41(X1, X2, mark(X3)) -> U41(X1, X2, X3) U41(active(X1), X2, X3) -> U41(X1, X2, X3) U41(X1, active(X2), X3) -> U41(X1, X2, X3) U41(X1, X2, active(X3)) -> U41(X1, X2, X3) U42(mark(X1), X2) -> U42(X1, X2) U42(X1, mark(X2)) -> U42(X1, X2) U42(active(X1), X2) -> U42(X1, X2) U42(X1, active(X2)) -> U42(X1, X2) U43(mark(X)) -> U43(X) U43(active(X)) -> U43(X) isNatIList(mark(X)) -> isNatIList(X) isNatIList(active(X)) -> isNatIList(X) U51(mark(X1), X2, X3) -> U51(X1, X2, X3) U51(X1, mark(X2), X3) -> U51(X1, X2, X3) U51(X1, X2, mark(X3)) -> U51(X1, X2, X3) U51(active(X1), X2, X3) -> U51(X1, X2, X3) U51(X1, active(X2), X3) -> U51(X1, X2, X3) U51(X1, X2, active(X3)) -> U51(X1, X2, X3) U52(mark(X1), X2) -> U52(X1, X2) U52(X1, mark(X2)) -> U52(X1, X2) U52(active(X1), X2) -> U52(X1, X2) U52(X1, active(X2)) -> U52(X1, X2) U53(mark(X)) -> U53(X) U53(active(X)) -> U53(X) U61(mark(X1), X2, X3) -> U61(X1, X2, X3) U61(X1, mark(X2), X3) -> U61(X1, X2, X3) U61(X1, X2, mark(X3)) -> U61(X1, X2, X3) U61(active(X1), X2, X3) -> U61(X1, X2, X3) U61(X1, active(X2), X3) -> U61(X1, X2, X3) U61(X1, X2, active(X3)) -> U61(X1, X2, X3) U62(mark(X1), X2) -> U62(X1, X2) U62(X1, mark(X2)) -> U62(X1, X2) U62(active(X1), X2) -> U62(X1, X2) U62(X1, active(X2)) -> U62(X1, X2) U63(mark(X)) -> U63(X) U63(active(X)) -> U63(X) U71(mark(X1), X2) -> U71(X1, X2) U71(X1, mark(X2)) -> U71(X1, X2) U71(active(X1), X2) -> U71(X1, X2) U71(X1, active(X2)) -> U71(X1, X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) length(mark(X)) -> length(X) length(active(X)) -> length(X) U81(mark(X)) -> U81(X) U81(active(X)) -> U81(X) U91(mark(X1), X2, X3, X4) -> U91(X1, X2, X3, X4) U91(X1, mark(X2), X3, X4) -> U91(X1, X2, X3, X4) U91(X1, X2, mark(X3), X4) -> U91(X1, X2, X3, X4) U91(X1, X2, X3, mark(X4)) -> U91(X1, X2, X3, X4) U91(active(X1), X2, X3, X4) -> U91(X1, X2, X3, X4) U91(X1, active(X2), X3, X4) -> U91(X1, X2, X3, X4) U91(X1, X2, active(X3), X4) -> U91(X1, X2, X3, X4) U91(X1, X2, X3, active(X4)) -> U91(X1, X2, X3, X4) take(mark(X1), X2) -> take(X1, X2) take(X1, mark(X2)) -> take(X1, X2) take(active(X1), X2) -> take(X1, X2) take(X1, active(X2)) -> take(X1, X2) and(mark(X1), X2) -> and(X1, X2) and(X1, mark(X2)) -> and(X1, X2) and(active(X1), X2) -> and(X1, X2) and(X1, active(X2)) -> and(X1, X2) isNatIListKind(mark(X)) -> isNatIListKind(X) isNatIListKind(active(X)) -> isNatIListKind(X) isNatKind(mark(X)) -> isNatKind(X) isNatKind(active(X)) -> isNatKind(X) )