KILLED proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF). (0) CpxRelTRS ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: A__U101(tt, z0, z1) -> c(A__U102(a__isNatural(z0), z1), A__ISNATURAL(z0)) A__U101(z0, z1, z2) -> c1 A__U102(tt, z0) -> c2(A__U103(a__isLNat(z0)), A__ISLNAT(z0)) A__U102(z0, z1) -> c3 A__U103(tt) -> c4 A__U103(z0) -> c5 A__U11(tt, z0, z1) -> c6(A__SND(a__splitAt(mark(z0), mark(z1))), A__SPLITAT(mark(z0), mark(z1)), MARK(z0)) A__U11(tt, z0, z1) -> c7(A__SND(a__splitAt(mark(z0), mark(z1))), A__SPLITAT(mark(z0), mark(z1)), MARK(z1)) A__U11(z0, z1, z2) -> c8 A__U111(tt, z0) -> c9(A__U112(a__isLNat(z0)), A__ISLNAT(z0)) A__U111(z0, z1) -> c10 A__U112(tt) -> c11 A__U112(z0) -> c12 A__U121(tt, z0) -> c13(A__U122(a__isNatural(z0)), A__ISNATURAL(z0)) A__U121(z0, z1) -> c14 A__U122(tt) -> c15 A__U122(z0) -> c16 A__U131(tt, z0, z1) -> c17(A__U132(a__isNatural(z0), z1), A__ISNATURAL(z0)) A__U131(z0, z1, z2) -> c18 A__U132(tt, z0) -> c19(A__U133(a__isLNat(z0)), A__ISLNAT(z0)) A__U132(z0, z1) -> c20 A__U133(tt) -> c21 A__U133(z0) -> c22 A__U141(tt, z0, z1) -> c23(A__U142(a__isLNat(z0), z1), A__ISLNAT(z0)) A__U141(z0, z1, z2) -> c24 A__U142(tt, z0) -> c25(A__U143(a__isLNat(z0)), A__ISLNAT(z0)) A__U142(z0, z1) -> c26 A__U143(tt) -> c27 A__U143(z0) -> c28 A__U151(tt, z0, z1) -> c29(A__U152(a__isNatural(z0), z1), A__ISNATURAL(z0)) A__U151(z0, z1, z2) -> c30 A__U152(tt, z0) -> c31(A__U153(a__isLNat(z0)), A__ISLNAT(z0)) A__U152(z0, z1) -> c32 A__U153(tt) -> c33 A__U153(z0) -> c34 A__U161(tt, z0) -> c35(MARK(z0)) A__U161(z0, z1) -> c36 A__U171(tt, z0, z1) -> c37(A__HEAD(a__afterNth(mark(z0), mark(z1))), A__AFTERNTH(mark(z0), mark(z1)), MARK(z0)) A__U171(tt, z0, z1) -> c38(A__HEAD(a__afterNth(mark(z0), mark(z1))), A__AFTERNTH(mark(z0), mark(z1)), MARK(z1)) A__U171(z0, z1, z2) -> c39 A__U181(tt, z0) -> c40(MARK(z0)) A__U181(z0, z1) -> c41 A__U191(tt, z0) -> c42(MARK(z0)) A__U191(z0, z1) -> c43 A__U201(tt, z0, z1, z2) -> c44(A__U202(a__splitAt(mark(z0), mark(z2)), z1), A__SPLITAT(mark(z0), mark(z2)), MARK(z0)) A__U201(tt, z0, z1, z2) -> c45(A__U202(a__splitAt(mark(z0), mark(z2)), z1), A__SPLITAT(mark(z0), mark(z2)), MARK(z2)) A__U201(z0, z1, z2, z3) -> c46 A__U202(pair(z0, z1), z2) -> c47(MARK(z2)) A__U202(pair(z0, z1), z2) -> c48(MARK(z1)) A__U202(z0, z1) -> c49 A__U21(tt, z0) -> c50(MARK(z0)) A__U21(z0, z1) -> c51 A__U211(tt, z0) -> c52(MARK(z0)) A__U211(z0, z1) -> c53 A__U221(tt, z0, z1) -> c54(A__FST(a__splitAt(mark(z0), mark(z1))), A__SPLITAT(mark(z0), mark(z1)), MARK(z0)) A__U221(tt, z0, z1) -> c55(A__FST(a__splitAt(mark(z0), mark(z1))), A__SPLITAT(mark(z0), mark(z1)), MARK(z1)) A__U221(z0, z1, z2) -> c56 A__U31(tt, z0) -> c57(MARK(z0)) A__U31(z0, z1) -> c58 A__U41(tt, z0, z1) -> c59(A__U42(a__isNatural(z0), z1), A__ISNATURAL(z0)) A__U41(z0, z1, z2) -> c60 A__U42(tt, z0) -> c61(A__U43(a__isLNat(z0)), A__ISLNAT(z0)) A__U42(z0, z1) -> c62 A__U43(tt) -> c63 A__U43(z0) -> c64 A__U51(tt, z0, z1) -> c65(A__U52(a__isNatural(z0), z1), A__ISNATURAL(z0)) A__U51(z0, z1, z2) -> c66 A__U52(tt, z0) -> c67(A__U53(a__isLNat(z0)), A__ISLNAT(z0)) A__U52(z0, z1) -> c68 A__U53(tt) -> c69 A__U53(z0) -> c70 A__U61(tt, z0) -> c71(A__U62(a__isPLNat(z0)), A__ISPLNAT(z0)) A__U61(z0, z1) -> c72 A__U62(tt) -> c73 A__U62(z0) -> c74 A__U71(tt, z0) -> c75(A__U72(a__isNatural(z0)), A__ISNATURAL(z0)) A__U71(z0, z1) -> c76 A__U72(tt) -> c77 A__U72(z0) -> c78 A__U81(tt, z0) -> c79(A__U82(a__isPLNat(z0)), A__ISPLNAT(z0)) A__U81(z0, z1) -> c80 A__U82(tt) -> c81 A__U82(z0) -> c82 A__U91(tt, z0) -> c83(A__U92(a__isLNat(z0)), A__ISLNAT(z0)) A__U91(z0, z1) -> c84 A__U92(tt) -> c85 A__U92(z0) -> c86 A__AFTERNTH(z0, z1) -> c87(A__U11(a__and(a__and(a__isNatural(z0), isNaturalKind(z0)), and(isLNat(z1), isLNatKind(z1))), z0, z1), A__AND(a__and(a__isNatural(z0), isNaturalKind(z0)), and(isLNat(z1), isLNatKind(z1))), A__AND(a__isNatural(z0), isNaturalKind(z0)), A__ISNATURAL(z0)) A__AFTERNTH(z0, z1) -> c88 A__AND(tt, z0) -> c89(MARK(z0)) A__AND(z0, z1) -> c90 A__FST(pair(z0, z1)) -> c91(A__U21(a__and(a__and(a__isLNat(z0), isLNatKind(z0)), and(isLNat(z1), isLNatKind(z1))), z0), A__AND(a__and(a__isLNat(z0), isLNatKind(z0)), and(isLNat(z1), isLNatKind(z1))), A__AND(a__isLNat(z0), isLNatKind(z0)), A__ISLNAT(z0)) A__FST(z0) -> c92 A__HEAD(cons(z0, z1)) -> c93(A__U31(a__and(a__and(a__isNatural(z0), isNaturalKind(z0)), and(isLNat(z1), isLNatKind(z1))), z0), A__AND(a__and(a__isNatural(z0), isNaturalKind(z0)), and(isLNat(z1), isLNatKind(z1))), A__AND(a__isNatural(z0), isNaturalKind(z0)), A__ISNATURAL(z0)) A__HEAD(z0) -> c94 A__ISLNAT(nil) -> c95 A__ISLNAT(afterNth(z0, z1)) -> c96(A__U41(a__and(a__isNaturalKind(z0), isLNatKind(z1)), z0, z1), A__AND(a__isNaturalKind(z0), isLNatKind(z1)), A__ISNATURALKIND(z0)) A__ISLNAT(cons(z0, z1)) -> c97(A__U51(a__and(a__isNaturalKind(z0), isLNatKind(z1)), z0, z1), A__AND(a__isNaturalKind(z0), isLNatKind(z1)), A__ISNATURALKIND(z0)) A__ISLNAT(fst(z0)) -> c98(A__U61(a__isPLNatKind(z0), z0), A__ISPLNATKIND(z0)) A__ISLNAT(natsFrom(z0)) -> c99(A__U71(a__isNaturalKind(z0), z0), A__ISNATURALKIND(z0)) A__ISLNAT(snd(z0)) -> c100(A__U81(a__isPLNatKind(z0), z0), A__ISPLNATKIND(z0)) A__ISLNAT(tail(z0)) -> c101(A__U91(a__isLNatKind(z0), z0), A__ISLNATKIND(z0)) A__ISLNAT(take(z0, z1)) -> c102(A__U101(a__and(a__isNaturalKind(z0), isLNatKind(z1)), z0, z1), A__AND(a__isNaturalKind(z0), isLNatKind(z1)), A__ISNATURALKIND(z0)) A__ISLNAT(z0) -> c103 A__ISLNATKIND(nil) -> c104 A__ISLNATKIND(afterNth(z0, z1)) -> c105(A__AND(a__isNaturalKind(z0), isLNatKind(z1)), A__ISNATURALKIND(z0)) A__ISLNATKIND(cons(z0, z1)) -> c106(A__AND(a__isNaturalKind(z0), isLNatKind(z1)), A__ISNATURALKIND(z0)) A__ISLNATKIND(fst(z0)) -> c107(A__ISPLNATKIND(z0)) A__ISLNATKIND(natsFrom(z0)) -> c108(A__ISNATURALKIND(z0)) A__ISLNATKIND(snd(z0)) -> c109(A__ISPLNATKIND(z0)) A__ISLNATKIND(tail(z0)) -> c110(A__ISLNATKIND(z0)) A__ISLNATKIND(take(z0, z1)) -> c111(A__AND(a__isNaturalKind(z0), isLNatKind(z1)), A__ISNATURALKIND(z0)) A__ISLNATKIND(z0) -> c112 A__ISNATURAL(0) -> c113 A__ISNATURAL(head(z0)) -> c114(A__U111(a__isLNatKind(z0), z0), A__ISLNATKIND(z0)) A__ISNATURAL(s(z0)) -> c115(A__U121(a__isNaturalKind(z0), z0), A__ISNATURALKIND(z0)) A__ISNATURAL(sel(z0, z1)) -> c116(A__U131(a__and(a__isNaturalKind(z0), isLNatKind(z1)), z0, z1), A__AND(a__isNaturalKind(z0), isLNatKind(z1)), A__ISNATURALKIND(z0)) A__ISNATURAL(z0) -> c117 A__ISNATURALKIND(0) -> c118 A__ISNATURALKIND(head(z0)) -> c119(A__ISLNATKIND(z0)) A__ISNATURALKIND(s(z0)) -> c120(A__ISNATURALKIND(z0)) A__ISNATURALKIND(sel(z0, z1)) -> c121(A__AND(a__isNaturalKind(z0), isLNatKind(z1)), A__ISNATURALKIND(z0)) A__ISNATURALKIND(z0) -> c122 A__ISPLNAT(pair(z0, z1)) -> c123(A__U141(a__and(a__isLNatKind(z0), isLNatKind(z1)), z0, z1), A__AND(a__isLNatKind(z0), isLNatKind(z1)), A__ISLNATKIND(z0)) A__ISPLNAT(splitAt(z0, z1)) -> c124(A__U151(a__and(a__isNaturalKind(z0), isLNatKind(z1)), z0, z1), A__AND(a__isNaturalKind(z0), isLNatKind(z1)), A__ISNATURALKIND(z0)) A__ISPLNAT(z0) -> c125 A__ISPLNATKIND(pair(z0, z1)) -> c126(A__AND(a__isLNatKind(z0), isLNatKind(z1)), A__ISLNATKIND(z0)) A__ISPLNATKIND(splitAt(z0, z1)) -> c127(A__AND(a__isNaturalKind(z0), isLNatKind(z1)), A__ISNATURALKIND(z0)) A__ISPLNATKIND(z0) -> c128 A__NATSFROM(z0) -> c129(A__U161(a__and(a__isNatural(z0), isNaturalKind(z0)), z0), A__AND(a__isNatural(z0), isNaturalKind(z0)), A__ISNATURAL(z0)) A__NATSFROM(z0) -> c130 A__SEL(z0, z1) -> c131(A__U171(a__and(a__and(a__isNatural(z0), isNaturalKind(z0)), and(isLNat(z1), isLNatKind(z1))), z0, z1), A__AND(a__and(a__isNatural(z0), isNaturalKind(z0)), and(isLNat(z1), isLNatKind(z1))), A__AND(a__isNatural(z0), isNaturalKind(z0)), A__ISNATURAL(z0)) A__SEL(z0, z1) -> c132 A__SND(pair(z0, z1)) -> c133(A__U181(a__and(a__and(a__isLNat(z0), isLNatKind(z0)), and(isLNat(z1), isLNatKind(z1))), z1), A__AND(a__and(a__isLNat(z0), isLNatKind(z0)), and(isLNat(z1), isLNatKind(z1))), A__AND(a__isLNat(z0), isLNatKind(z0)), A__ISLNAT(z0)) A__SND(z0) -> c134 A__SPLITAT(0, z0) -> c135(A__U191(a__and(a__isLNat(z0), isLNatKind(z0)), z0), A__AND(a__isLNat(z0), isLNatKind(z0)), A__ISLNAT(z0)) A__SPLITAT(s(z0), cons(z1, z2)) -> c136(A__U201(a__and(a__and(a__isNatural(z0), isNaturalKind(z0)), and(and(isNatural(z1), isNaturalKind(z1)), and(isLNat(z2), isLNatKind(z2)))), z0, z1, z2), A__AND(a__and(a__isNatural(z0), isNaturalKind(z0)), and(and(isNatural(z1), isNaturalKind(z1)), and(isLNat(z2), isLNatKind(z2)))), A__AND(a__isNatural(z0), isNaturalKind(z0)), A__ISNATURAL(z0)) A__SPLITAT(z0, z1) -> c137 A__TAIL(cons(z0, z1)) -> c138(A__U211(a__and(a__and(a__isNatural(z0), isNaturalKind(z0)), and(isLNat(z1), isLNatKind(z1))), z1), A__AND(a__and(a__isNatural(z0), isNaturalKind(z0)), and(isLNat(z1), isLNatKind(z1))), A__AND(a__isNatural(z0), isNaturalKind(z0)), A__ISNATURAL(z0)) A__TAIL(z0) -> c139 A__TAKE(z0, z1) -> c140(A__U221(a__and(a__and(a__isNatural(z0), isNaturalKind(z0)), and(isLNat(z1), isLNatKind(z1))), z0, z1), A__AND(a__and(a__isNatural(z0), isNaturalKind(z0)), and(isLNat(z1), isLNatKind(z1))), A__AND(a__isNatural(z0), isNaturalKind(z0)), A__ISNATURAL(z0)) A__TAKE(z0, z1) -> c141 MARK(U101(z0, z1, z2)) -> c142(A__U101(mark(z0), z1, z2), MARK(z0)) MARK(U102(z0, z1)) -> c143(A__U102(mark(z0), z1), MARK(z0)) MARK(isNatural(z0)) -> c144(A__ISNATURAL(z0)) MARK(U103(z0)) -> c145(A__U103(mark(z0)), MARK(z0)) MARK(isLNat(z0)) -> c146(A__ISLNAT(z0)) MARK(U11(z0, z1, z2)) -> c147(A__U11(mark(z0), z1, z2), MARK(z0)) MARK(snd(z0)) -> c148(A__SND(mark(z0)), MARK(z0)) MARK(splitAt(z0, z1)) -> c149(A__SPLITAT(mark(z0), mark(z1)), MARK(z0)) MARK(splitAt(z0, z1)) -> c150(A__SPLITAT(mark(z0), mark(z1)), MARK(z1)) MARK(U111(z0, z1)) -> c151(A__U111(mark(z0), z1), MARK(z0)) MARK(U112(z0)) -> c152(A__U112(mark(z0)), MARK(z0)) MARK(U121(z0, z1)) -> c153(A__U121(mark(z0), z1), MARK(z0)) MARK(U122(z0)) -> c154(A__U122(mark(z0)), MARK(z0)) MARK(U131(z0, z1, z2)) -> c155(A__U131(mark(z0), z1, z2), MARK(z0)) MARK(U132(z0, z1)) -> c156(A__U132(mark(z0), z1), MARK(z0)) MARK(U133(z0)) -> c157(A__U133(mark(z0)), MARK(z0)) MARK(U141(z0, z1, z2)) -> c158(A__U141(mark(z0), z1, z2), MARK(z0)) MARK(U142(z0, z1)) -> c159(A__U142(mark(z0), z1), MARK(z0)) MARK(U143(z0)) -> c160(A__U143(mark(z0)), MARK(z0)) MARK(U151(z0, z1, z2)) -> c161(A__U151(mark(z0), z1, z2), MARK(z0)) MARK(U152(z0, z1)) -> c162(A__U152(mark(z0), z1), MARK(z0)) MARK(U153(z0)) -> c163(A__U153(mark(z0)), MARK(z0)) MARK(U161(z0, z1)) -> c164(A__U161(mark(z0), z1), MARK(z0)) MARK(natsFrom(z0)) -> c165(A__NATSFROM(mark(z0)), MARK(z0)) MARK(U171(z0, z1, z2)) -> c166(A__U171(mark(z0), z1, z2), MARK(z0)) MARK(head(z0)) -> c167(A__HEAD(mark(z0)), MARK(z0)) MARK(afterNth(z0, z1)) -> c168(A__AFTERNTH(mark(z0), mark(z1)), MARK(z0)) MARK(afterNth(z0, z1)) -> c169(A__AFTERNTH(mark(z0), mark(z1)), MARK(z1)) MARK(U181(z0, z1)) -> c170(A__U181(mark(z0), z1), MARK(z0)) MARK(U191(z0, z1)) -> c171(A__U191(mark(z0), z1), MARK(z0)) MARK(U201(z0, z1, z2, z3)) -> c172(A__U201(mark(z0), z1, z2, z3), MARK(z0)) MARK(U202(z0, z1)) -> c173(A__U202(mark(z0), z1), MARK(z0)) MARK(U21(z0, z1)) -> c174(A__U21(mark(z0), z1), MARK(z0)) MARK(U211(z0, z1)) -> c175(A__U211(mark(z0), z1), MARK(z0)) MARK(U221(z0, z1, z2)) -> c176(A__U221(mark(z0), z1, z2), MARK(z0)) MARK(fst(z0)) -> c177(A__FST(mark(z0)), MARK(z0)) MARK(U31(z0, z1)) -> c178(A__U31(mark(z0), z1), MARK(z0)) MARK(U41(z0, z1, z2)) -> c179(A__U41(mark(z0), z1, z2), MARK(z0)) MARK(U42(z0, z1)) -> c180(A__U42(mark(z0), z1), MARK(z0)) MARK(U43(z0)) -> c181(A__U43(mark(z0)), MARK(z0)) MARK(U51(z0, z1, z2)) -> c182(A__U51(mark(z0), z1, z2), MARK(z0)) MARK(U52(z0, z1)) -> c183(A__U52(mark(z0), z1), MARK(z0)) MARK(U53(z0)) -> c184(A__U53(mark(z0)), MARK(z0)) MARK(U61(z0, z1)) -> c185(A__U61(mark(z0), z1), MARK(z0)) MARK(U62(z0)) -> c186(A__U62(mark(z0)), MARK(z0)) MARK(isPLNat(z0)) -> c187(A__ISPLNAT(z0)) MARK(U71(z0, z1)) -> c188(A__U71(mark(z0), z1), MARK(z0)) MARK(U72(z0)) -> c189(A__U72(mark(z0)), MARK(z0)) MARK(U81(z0, z1)) -> c190(A__U81(mark(z0), z1), MARK(z0)) MARK(U82(z0)) -> c191(A__U82(mark(z0)), MARK(z0)) MARK(U91(z0, z1)) -> c192(A__U91(mark(z0), z1), MARK(z0)) MARK(U92(z0)) -> c193(A__U92(mark(z0)), MARK(z0)) MARK(and(z0, z1)) -> c194(A__AND(mark(z0), z1), MARK(z0)) MARK(isNaturalKind(z0)) -> c195(A__ISNATURALKIND(z0)) MARK(isLNatKind(z0)) -> c196(A__ISLNATKIND(z0)) MARK(isPLNatKind(z0)) -> c197(A__ISPLNATKIND(z0)) MARK(tail(z0)) -> c198(A__TAIL(mark(z0)), MARK(z0)) MARK(take(z0, z1)) -> c199(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c200(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(sel(z0, z1)) -> c201(A__SEL(mark(z0), mark(z1)), MARK(z0)) MARK(sel(z0, z1)) -> c202(A__SEL(mark(z0), mark(z1)), MARK(z1)) MARK(tt) -> c203 MARK(cons(z0, z1)) -> c204(MARK(z0)) MARK(s(z0)) -> c205(MARK(z0)) MARK(pair(z0, z1)) -> c206(MARK(z0)) MARK(pair(z0, z1)) -> c207(MARK(z1)) MARK(nil) -> c208 MARK(0) -> c209 The (relative) TRS S consists of the following rules: a__U101(tt, z0, z1) -> a__U102(a__isNatural(z0), z1) a__U101(z0, z1, z2) -> U101(z0, z1, z2) a__U102(tt, z0) -> a__U103(a__isLNat(z0)) a__U102(z0, z1) -> U102(z0, z1) a__U103(tt) -> tt a__U103(z0) -> U103(z0) a__U11(tt, z0, z1) -> a__snd(a__splitAt(mark(z0), mark(z1))) a__U11(z0, z1, z2) -> U11(z0, z1, z2) a__U111(tt, z0) -> a__U112(a__isLNat(z0)) a__U111(z0, z1) -> U111(z0, z1) a__U112(tt) -> tt a__U112(z0) -> U112(z0) a__U121(tt, z0) -> a__U122(a__isNatural(z0)) a__U121(z0, z1) -> U121(z0, z1) a__U122(tt) -> tt a__U122(z0) -> U122(z0) a__U131(tt, z0, z1) -> a__U132(a__isNatural(z0), z1) a__U131(z0, z1, z2) -> U131(z0, z1, z2) a__U132(tt, z0) -> a__U133(a__isLNat(z0)) a__U132(z0, z1) -> U132(z0, z1) a__U133(tt) -> tt a__U133(z0) -> U133(z0) a__U141(tt, z0, z1) -> a__U142(a__isLNat(z0), z1) a__U141(z0, z1, z2) -> U141(z0, z1, z2) a__U142(tt, z0) -> a__U143(a__isLNat(z0)) a__U142(z0, z1) -> U142(z0, z1) a__U143(tt) -> tt a__U143(z0) -> U143(z0) a__U151(tt, z0, z1) -> a__U152(a__isNatural(z0), z1) a__U151(z0, z1, z2) -> U151(z0, z1, z2) a__U152(tt, z0) -> a__U153(a__isLNat(z0)) a__U152(z0, z1) -> U152(z0, z1) a__U153(tt) -> tt a__U153(z0) -> U153(z0) a__U161(tt, z0) -> cons(mark(z0), natsFrom(s(z0))) a__U161(z0, z1) -> U161(z0, z1) a__U171(tt, z0, z1) -> a__head(a__afterNth(mark(z0), mark(z1))) a__U171(z0, z1, z2) -> U171(z0, z1, z2) a__U181(tt, z0) -> mark(z0) a__U181(z0, z1) -> U181(z0, z1) a__U191(tt, z0) -> pair(nil, mark(z0)) a__U191(z0, z1) -> U191(z0, z1) a__U201(tt, z0, z1, z2) -> a__U202(a__splitAt(mark(z0), mark(z2)), z1) a__U201(z0, z1, z2, z3) -> U201(z0, z1, z2, z3) a__U202(pair(z0, z1), z2) -> pair(cons(mark(z2), z0), mark(z1)) a__U202(z0, z1) -> U202(z0, z1) a__U21(tt, z0) -> mark(z0) a__U21(z0, z1) -> U21(z0, z1) a__U211(tt, z0) -> mark(z0) a__U211(z0, z1) -> U211(z0, z1) a__U221(tt, z0, z1) -> a__fst(a__splitAt(mark(z0), mark(z1))) a__U221(z0, z1, z2) -> U221(z0, z1, z2) a__U31(tt, z0) -> mark(z0) a__U31(z0, z1) -> U31(z0, z1) a__U41(tt, z0, z1) -> a__U42(a__isNatural(z0), z1) a__U41(z0, z1, z2) -> U41(z0, z1, z2) a__U42(tt, z0) -> a__U43(a__isLNat(z0)) a__U42(z0, z1) -> U42(z0, z1) a__U43(tt) -> tt a__U43(z0) -> U43(z0) a__U51(tt, z0, z1) -> a__U52(a__isNatural(z0), z1) a__U51(z0, z1, z2) -> U51(z0, z1, z2) a__U52(tt, z0) -> a__U53(a__isLNat(z0)) a__U52(z0, z1) -> U52(z0, z1) a__U53(tt) -> tt a__U53(z0) -> U53(z0) a__U61(tt, z0) -> a__U62(a__isPLNat(z0)) a__U61(z0, z1) -> U61(z0, z1) a__U62(tt) -> tt a__U62(z0) -> U62(z0) a__U71(tt, z0) -> a__U72(a__isNatural(z0)) a__U71(z0, z1) -> U71(z0, z1) a__U72(tt) -> tt a__U72(z0) -> U72(z0) a__U81(tt, z0) -> a__U82(a__isPLNat(z0)) a__U81(z0, z1) -> U81(z0, z1) a__U82(tt) -> tt a__U82(z0) -> U82(z0) a__U91(tt, z0) -> a__U92(a__isLNat(z0)) a__U91(z0, z1) -> U91(z0, z1) a__U92(tt) -> tt a__U92(z0) -> U92(z0) a__afterNth(z0, z1) -> a__U11(a__and(a__and(a__isNatural(z0), isNaturalKind(z0)), and(isLNat(z1), isLNatKind(z1))), z0, z1) a__afterNth(z0, z1) -> afterNth(z0, z1) a__and(tt, z0) -> mark(z0) a__and(z0, z1) -> and(z0, z1) a__fst(pair(z0, z1)) -> a__U21(a__and(a__and(a__isLNat(z0), isLNatKind(z0)), and(isLNat(z1), isLNatKind(z1))), z0) a__fst(z0) -> fst(z0) a__head(cons(z0, z1)) -> a__U31(a__and(a__and(a__isNatural(z0), isNaturalKind(z0)), and(isLNat(z1), isLNatKind(z1))), z0) a__head(z0) -> head(z0) a__isLNat(nil) -> tt a__isLNat(afterNth(z0, z1)) -> a__U41(a__and(a__isNaturalKind(z0), isLNatKind(z1)), z0, z1) a__isLNat(cons(z0, z1)) -> a__U51(a__and(a__isNaturalKind(z0), isLNatKind(z1)), z0, z1) a__isLNat(fst(z0)) -> a__U61(a__isPLNatKind(z0), z0) a__isLNat(natsFrom(z0)) -> a__U71(a__isNaturalKind(z0), z0) a__isLNat(snd(z0)) -> a__U81(a__isPLNatKind(z0), z0) a__isLNat(tail(z0)) -> a__U91(a__isLNatKind(z0), z0) a__isLNat(take(z0, z1)) -> a__U101(a__and(a__isNaturalKind(z0), isLNatKind(z1)), z0, z1) a__isLNat(z0) -> isLNat(z0) a__isLNatKind(nil) -> tt a__isLNatKind(afterNth(z0, z1)) -> a__and(a__isNaturalKind(z0), isLNatKind(z1)) a__isLNatKind(cons(z0, z1)) -> a__and(a__isNaturalKind(z0), isLNatKind(z1)) a__isLNatKind(fst(z0)) -> a__isPLNatKind(z0) a__isLNatKind(natsFrom(z0)) -> a__isNaturalKind(z0) a__isLNatKind(snd(z0)) -> a__isPLNatKind(z0) a__isLNatKind(tail(z0)) -> a__isLNatKind(z0) a__isLNatKind(take(z0, z1)) -> a__and(a__isNaturalKind(z0), isLNatKind(z1)) a__isLNatKind(z0) -> isLNatKind(z0) a__isNatural(0) -> tt a__isNatural(head(z0)) -> a__U111(a__isLNatKind(z0), z0) a__isNatural(s(z0)) -> a__U121(a__isNaturalKind(z0), z0) a__isNatural(sel(z0, z1)) -> a__U131(a__and(a__isNaturalKind(z0), isLNatKind(z1)), z0, z1) a__isNatural(z0) -> isNatural(z0) a__isNaturalKind(0) -> tt a__isNaturalKind(head(z0)) -> a__isLNatKind(z0) a__isNaturalKind(s(z0)) -> a__isNaturalKind(z0) a__isNaturalKind(sel(z0, z1)) -> a__and(a__isNaturalKind(z0), isLNatKind(z1)) a__isNaturalKind(z0) -> isNaturalKind(z0) a__isPLNat(pair(z0, z1)) -> a__U141(a__and(a__isLNatKind(z0), isLNatKind(z1)), z0, z1) a__isPLNat(splitAt(z0, z1)) -> a__U151(a__and(a__isNaturalKind(z0), isLNatKind(z1)), z0, z1) a__isPLNat(z0) -> isPLNat(z0) a__isPLNatKind(pair(z0, z1)) -> a__and(a__isLNatKind(z0), isLNatKind(z1)) a__isPLNatKind(splitAt(z0, z1)) -> a__and(a__isNaturalKind(z0), isLNatKind(z1)) a__isPLNatKind(z0) -> isPLNatKind(z0) a__natsFrom(z0) -> a__U161(a__and(a__isNatural(z0), isNaturalKind(z0)), z0) a__natsFrom(z0) -> natsFrom(z0) a__sel(z0, z1) -> a__U171(a__and(a__and(a__isNatural(z0), isNaturalKind(z0)), and(isLNat(z1), isLNatKind(z1))), z0, z1) a__sel(z0, z1) -> sel(z0, z1) a__snd(pair(z0, z1)) -> a__U181(a__and(a__and(a__isLNat(z0), isLNatKind(z0)), and(isLNat(z1), isLNatKind(z1))), z1) a__snd(z0) -> snd(z0) a__splitAt(0, z0) -> a__U191(a__and(a__isLNat(z0), isLNatKind(z0)), z0) a__splitAt(s(z0), cons(z1, z2)) -> a__U201(a__and(a__and(a__isNatural(z0), isNaturalKind(z0)), and(and(isNatural(z1), isNaturalKind(z1)), and(isLNat(z2), isLNatKind(z2)))), z0, z1, z2) a__splitAt(z0, z1) -> splitAt(z0, z1) a__tail(cons(z0, z1)) -> a__U211(a__and(a__and(a__isNatural(z0), isNaturalKind(z0)), and(isLNat(z1), isLNatKind(z1))), z1) a__tail(z0) -> tail(z0) a__take(z0, z1) -> a__U221(a__and(a__and(a__isNatural(z0), isNaturalKind(z0)), and(isLNat(z1), isLNatKind(z1))), z0, z1) a__take(z0, z1) -> take(z0, z1) mark(U101(z0, z1, z2)) -> a__U101(mark(z0), z1, z2) mark(U102(z0, z1)) -> a__U102(mark(z0), z1) mark(isNatural(z0)) -> a__isNatural(z0) mark(U103(z0)) -> a__U103(mark(z0)) mark(isLNat(z0)) -> a__isLNat(z0) mark(U11(z0, z1, z2)) -> a__U11(mark(z0), z1, z2) mark(snd(z0)) -> a__snd(mark(z0)) mark(splitAt(z0, z1)) -> a__splitAt(mark(z0), mark(z1)) mark(U111(z0, z1)) -> a__U111(mark(z0), z1) mark(U112(z0)) -> a__U112(mark(z0)) mark(U121(z0, z1)) -> a__U121(mark(z0), z1) mark(U122(z0)) -> a__U122(mark(z0)) mark(U131(z0, z1, z2)) -> a__U131(mark(z0), z1, z2) mark(U132(z0, z1)) -> a__U132(mark(z0), z1) mark(U133(z0)) -> a__U133(mark(z0)) mark(U141(z0, z1, z2)) -> a__U141(mark(z0), z1, z2) mark(U142(z0, z1)) -> a__U142(mark(z0), z1) mark(U143(z0)) -> a__U143(mark(z0)) mark(U151(z0, z1, z2)) -> a__U151(mark(z0), z1, z2) mark(U152(z0, z1)) -> a__U152(mark(z0), z1) mark(U153(z0)) -> a__U153(mark(z0)) mark(U161(z0, z1)) -> a__U161(mark(z0), z1) mark(natsFrom(z0)) -> a__natsFrom(mark(z0)) mark(U171(z0, z1, z2)) -> a__U171(mark(z0), z1, z2) mark(head(z0)) -> a__head(mark(z0)) mark(afterNth(z0, z1)) -> a__afterNth(mark(z0), mark(z1)) mark(U181(z0, z1)) -> a__U181(mark(z0), z1) mark(U191(z0, z1)) -> a__U191(mark(z0), z1) mark(U201(z0, z1, z2, z3)) -> a__U201(mark(z0), z1, z2, z3) mark(U202(z0, z1)) -> a__U202(mark(z0), z1) mark(U21(z0, z1)) -> a__U21(mark(z0), z1) mark(U211(z0, z1)) -> a__U211(mark(z0), z1) mark(U221(z0, z1, z2)) -> a__U221(mark(z0), z1, z2) mark(fst(z0)) -> a__fst(mark(z0)) mark(U31(z0, z1)) -> a__U31(mark(z0), z1) mark(U41(z0, z1, z2)) -> a__U41(mark(z0), z1, z2) mark(U42(z0, z1)) -> a__U42(mark(z0), z1) mark(U43(z0)) -> a__U43(mark(z0)) mark(U51(z0, z1, z2)) -> a__U51(mark(z0), z1, z2) mark(U52(z0, z1)) -> a__U52(mark(z0), z1) mark(U53(z0)) -> a__U53(mark(z0)) mark(U61(z0, z1)) -> a__U61(mark(z0), z1) mark(U62(z0)) -> a__U62(mark(z0)) mark(isPLNat(z0)) -> a__isPLNat(z0) mark(U71(z0, z1)) -> a__U71(mark(z0), z1) mark(U72(z0)) -> a__U72(mark(z0)) mark(U81(z0, z1)) -> a__U81(mark(z0), z1) mark(U82(z0)) -> a__U82(mark(z0)) mark(U91(z0, z1)) -> a__U91(mark(z0), z1) mark(U92(z0)) -> a__U92(mark(z0)) mark(and(z0, z1)) -> a__and(mark(z0), z1) mark(isNaturalKind(z0)) -> a__isNaturalKind(z0) mark(isLNatKind(z0)) -> a__isLNatKind(z0) mark(isPLNatKind(z0)) -> a__isPLNatKind(z0) mark(tail(z0)) -> a__tail(mark(z0)) mark(take(z0, z1)) -> a__take(mark(z0), mark(z1)) mark(sel(z0, z1)) -> a__sel(mark(z0), mark(z1)) mark(tt) -> tt mark(cons(z0, z1)) -> cons(mark(z0), z1) mark(s(z0)) -> s(mark(z0)) mark(pair(z0, z1)) -> pair(mark(z0), mark(z1)) mark(nil) -> nil mark(0) -> 0 Rewrite Strategy: INNERMOST