WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: 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(z0,z1) -> c90() A__AND(tt(),z0) -> c89(MARK(z0)) A__FST(z0) -> c92() 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__HEAD(z0) -> c94() 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__ISLNAT(z0) -> c103() 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(nil()) -> c95() 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__ISLNATKIND(z0) -> c112() 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(nil()) -> c104() 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__ISNATURAL(z0) -> c117() 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__ISNATURALKIND(z0) -> c122() 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__ISPLNAT(z0) -> c125() 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__ISPLNATKIND(z0) -> c128() 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__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(z0) -> c134() 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__SPLITAT(z0,z1) -> c137() 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__TAIL(z0) -> c139() 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__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() A__U101(z0,z1,z2) -> c1() A__U101(tt(),z0,z1) -> c(A__U102(a__isNatural(z0),z1),A__ISNATURAL(z0)) A__U102(z0,z1) -> c3() A__U102(tt(),z0) -> c2(A__U103(a__isLNat(z0)),A__ISLNAT(z0)) A__U103(z0) -> c5() A__U103(tt()) -> c4() A__U11(z0,z1,z2) -> c8() 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__U111(z0,z1) -> c10() A__U111(tt(),z0) -> c9(A__U112(a__isLNat(z0)),A__ISLNAT(z0)) A__U112(z0) -> c12() A__U112(tt()) -> c11() A__U121(z0,z1) -> c14() A__U121(tt(),z0) -> c13(A__U122(a__isNatural(z0)),A__ISNATURAL(z0)) A__U122(z0) -> c16() A__U122(tt()) -> c15() A__U131(z0,z1,z2) -> c18() A__U131(tt(),z0,z1) -> c17(A__U132(a__isNatural(z0),z1),A__ISNATURAL(z0)) A__U132(z0,z1) -> c20() A__U132(tt(),z0) -> c19(A__U133(a__isLNat(z0)),A__ISLNAT(z0)) A__U133(z0) -> c22() A__U133(tt()) -> c21() A__U141(z0,z1,z2) -> c24() A__U141(tt(),z0,z1) -> c23(A__U142(a__isLNat(z0),z1),A__ISLNAT(z0)) A__U142(z0,z1) -> c26() A__U142(tt(),z0) -> c25(A__U143(a__isLNat(z0)),A__ISLNAT(z0)) A__U143(z0) -> c28() A__U143(tt()) -> c27() A__U151(z0,z1,z2) -> c30() A__U151(tt(),z0,z1) -> c29(A__U152(a__isNatural(z0),z1),A__ISNATURAL(z0)) A__U152(z0,z1) -> c32() A__U152(tt(),z0) -> c31(A__U153(a__isLNat(z0)),A__ISLNAT(z0)) A__U153(z0) -> c34() A__U153(tt()) -> c33() A__U161(z0,z1) -> c36() A__U161(tt(),z0) -> c35(MARK(z0)) A__U171(z0,z1,z2) -> c39() 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__U181(z0,z1) -> c41() A__U181(tt(),z0) -> c40(MARK(z0)) A__U191(z0,z1) -> c43() A__U191(tt(),z0) -> c42(MARK(z0)) A__U201(z0,z1,z2,z3) -> c46() 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__U202(z0,z1) -> c49() A__U202(pair(z0,z1),z2) -> c47(MARK(z2)) A__U202(pair(z0,z1),z2) -> c48(MARK(z1)) A__U21(z0,z1) -> c51() A__U21(tt(),z0) -> c50(MARK(z0)) A__U211(z0,z1) -> c53() A__U211(tt(),z0) -> c52(MARK(z0)) A__U221(z0,z1,z2) -> c56() 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__U31(z0,z1) -> c58() A__U31(tt(),z0) -> c57(MARK(z0)) A__U41(z0,z1,z2) -> c60() A__U41(tt(),z0,z1) -> c59(A__U42(a__isNatural(z0),z1),A__ISNATURAL(z0)) A__U42(z0,z1) -> c62() A__U42(tt(),z0) -> c61(A__U43(a__isLNat(z0)),A__ISLNAT(z0)) A__U43(z0) -> c64() A__U43(tt()) -> c63() A__U51(z0,z1,z2) -> c66() A__U51(tt(),z0,z1) -> c65(A__U52(a__isNatural(z0),z1),A__ISNATURAL(z0)) A__U52(z0,z1) -> c68() A__U52(tt(),z0) -> c67(A__U53(a__isLNat(z0)),A__ISLNAT(z0)) A__U53(z0) -> c70() A__U53(tt()) -> c69() A__U61(z0,z1) -> c72() A__U61(tt(),z0) -> c71(A__U62(a__isPLNat(z0)),A__ISPLNAT(z0)) A__U62(z0) -> c74() A__U62(tt()) -> c73() A__U71(z0,z1) -> c76() A__U71(tt(),z0) -> c75(A__U72(a__isNatural(z0)),A__ISNATURAL(z0)) A__U72(z0) -> c78() A__U72(tt()) -> c77() A__U81(z0,z1) -> c80() A__U81(tt(),z0) -> c79(A__U82(a__isPLNat(z0)),A__ISPLNAT(z0)) A__U82(z0) -> c82() A__U82(tt()) -> c81() A__U91(z0,z1) -> c84() A__U91(tt(),z0) -> c83(A__U92(a__isLNat(z0)),A__ISLNAT(z0)) A__U92(z0) -> c86() A__U92(tt()) -> c85() MARK(0()) -> c209() 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(U103(z0)) -> c145(A__U103(mark(z0)),MARK(z0)) MARK(U11(z0,z1,z2)) -> c147(A__U11(mark(z0),z1,z2),MARK(z0)) 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(U171(z0,z1,z2)) -> c166(A__U171(mark(z0),z1,z2),MARK(z0)) 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(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(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(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(and(z0,z1)) -> c194(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c204(MARK(z0)) MARK(fst(z0)) -> c177(A__FST(mark(z0)),MARK(z0)) MARK(head(z0)) -> c167(A__HEAD(mark(z0)),MARK(z0)) MARK(isLNat(z0)) -> c146(A__ISLNAT(z0)) MARK(isLNatKind(z0)) -> c196(A__ISLNATKIND(z0)) MARK(isNatural(z0)) -> c144(A__ISNATURAL(z0)) MARK(isNaturalKind(z0)) -> c195(A__ISNATURALKIND(z0)) MARK(isPLNat(z0)) -> c187(A__ISPLNAT(z0)) MARK(isPLNatKind(z0)) -> c197(A__ISPLNATKIND(z0)) MARK(natsFrom(z0)) -> c165(A__NATSFROM(mark(z0)),MARK(z0)) MARK(nil()) -> c208() MARK(pair(z0,z1)) -> c206(MARK(z0)) MARK(pair(z0,z1)) -> c207(MARK(z1)) MARK(s(z0)) -> c205(MARK(z0)) 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(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(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(tt()) -> c203() - Weak TRS: a__U101(z0,z1,z2) -> U101(z0,z1,z2) a__U101(tt(),z0,z1) -> a__U102(a__isNatural(z0),z1) a__U102(z0,z1) -> U102(z0,z1) a__U102(tt(),z0) -> a__U103(a__isLNat(z0)) a__U103(z0) -> U103(z0) a__U103(tt()) -> tt() a__U11(z0,z1,z2) -> U11(z0,z1,z2) a__U11(tt(),z0,z1) -> a__snd(a__splitAt(mark(z0),mark(z1))) a__U111(z0,z1) -> U111(z0,z1) a__U111(tt(),z0) -> a__U112(a__isLNat(z0)) a__U112(z0) -> U112(z0) a__U112(tt()) -> tt() a__U121(z0,z1) -> U121(z0,z1) a__U121(tt(),z0) -> a__U122(a__isNatural(z0)) a__U122(z0) -> U122(z0) a__U122(tt()) -> tt() a__U131(z0,z1,z2) -> U131(z0,z1,z2) a__U131(tt(),z0,z1) -> a__U132(a__isNatural(z0),z1) a__U132(z0,z1) -> U132(z0,z1) a__U132(tt(),z0) -> a__U133(a__isLNat(z0)) a__U133(z0) -> U133(z0) a__U133(tt()) -> tt() a__U141(z0,z1,z2) -> U141(z0,z1,z2) a__U141(tt(),z0,z1) -> a__U142(a__isLNat(z0),z1) a__U142(z0,z1) -> U142(z0,z1) a__U142(tt(),z0) -> a__U143(a__isLNat(z0)) a__U143(z0) -> U143(z0) a__U143(tt()) -> tt() a__U151(z0,z1,z2) -> U151(z0,z1,z2) a__U151(tt(),z0,z1) -> a__U152(a__isNatural(z0),z1) a__U152(z0,z1) -> U152(z0,z1) a__U152(tt(),z0) -> a__U153(a__isLNat(z0)) a__U153(z0) -> U153(z0) a__U153(tt()) -> tt() a__U161(z0,z1) -> U161(z0,z1) a__U161(tt(),z0) -> cons(mark(z0),natsFrom(s(z0))) a__U171(z0,z1,z2) -> U171(z0,z1,z2) a__U171(tt(),z0,z1) -> a__head(a__afterNth(mark(z0),mark(z1))) a__U181(z0,z1) -> U181(z0,z1) a__U181(tt(),z0) -> mark(z0) a__U191(z0,z1) -> U191(z0,z1) a__U191(tt(),z0) -> pair(nil(),mark(z0)) a__U201(z0,z1,z2,z3) -> U201(z0,z1,z2,z3) a__U201(tt(),z0,z1,z2) -> a__U202(a__splitAt(mark(z0),mark(z2)),z1) a__U202(z0,z1) -> U202(z0,z1) a__U202(pair(z0,z1),z2) -> pair(cons(mark(z2),z0),mark(z1)) a__U21(z0,z1) -> U21(z0,z1) a__U21(tt(),z0) -> mark(z0) a__U211(z0,z1) -> U211(z0,z1) a__U211(tt(),z0) -> mark(z0) a__U221(z0,z1,z2) -> U221(z0,z1,z2) a__U221(tt(),z0,z1) -> a__fst(a__splitAt(mark(z0),mark(z1))) a__U31(z0,z1) -> U31(z0,z1) a__U31(tt(),z0) -> mark(z0) a__U41(z0,z1,z2) -> U41(z0,z1,z2) a__U41(tt(),z0,z1) -> a__U42(a__isNatural(z0),z1) a__U42(z0,z1) -> U42(z0,z1) a__U42(tt(),z0) -> a__U43(a__isLNat(z0)) a__U43(z0) -> U43(z0) a__U43(tt()) -> tt() a__U51(z0,z1,z2) -> U51(z0,z1,z2) a__U51(tt(),z0,z1) -> a__U52(a__isNatural(z0),z1) a__U52(z0,z1) -> U52(z0,z1) a__U52(tt(),z0) -> a__U53(a__isLNat(z0)) a__U53(z0) -> U53(z0) a__U53(tt()) -> tt() a__U61(z0,z1) -> U61(z0,z1) a__U61(tt(),z0) -> a__U62(a__isPLNat(z0)) a__U62(z0) -> U62(z0) a__U62(tt()) -> tt() a__U71(z0,z1) -> U71(z0,z1) a__U71(tt(),z0) -> a__U72(a__isNatural(z0)) a__U72(z0) -> U72(z0) a__U72(tt()) -> tt() a__U81(z0,z1) -> U81(z0,z1) a__U81(tt(),z0) -> a__U82(a__isPLNat(z0)) a__U82(z0) -> U82(z0) a__U82(tt()) -> tt() a__U91(z0,z1) -> U91(z0,z1) a__U91(tt(),z0) -> a__U92(a__isLNat(z0)) a__U92(z0) -> U92(z0) a__U92(tt()) -> tt() 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(z0,z1) -> and(z0,z1) a__and(tt(),z0) -> mark(z0) a__fst(z0) -> fst(z0) a__fst(pair(z0,z1)) -> a__U21(a__and(a__and(a__isLNat(z0),isLNatKind(z0)),and(isLNat(z1),isLNatKind(z1))) ,z0) a__head(z0) -> head(z0) a__head(cons(z0,z1)) -> a__U31(a__and(a__and(a__isNatural(z0),isNaturalKind(z0)) ,and(isLNat(z1),isLNatKind(z1))) ,z0) a__isLNat(z0) -> isLNat(z0) 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(nil()) -> tt() 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__isLNatKind(z0) -> isLNatKind(z0) 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(nil()) -> tt() 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__isNatural(z0) -> isNatural(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__isNaturalKind(z0) -> isNaturalKind(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__isPLNat(z0) -> isPLNat(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__isPLNatKind(z0) -> isPLNatKind(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__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(z0) -> snd(z0) a__snd(pair(z0,z1)) -> a__U181(a__and(a__and(a__isLNat(z0),isLNatKind(z0)),and(isLNat(z1),isLNatKind(z1))) ,z1) a__splitAt(z0,z1) -> splitAt(z0,z1) 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__tail(z0) -> tail(z0) a__tail(cons(z0,z1)) -> a__U211(a__and(a__and(a__isNatural(z0),isNaturalKind(z0)) ,and(isLNat(z1),isLNatKind(z1))) ,z1) 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(0()) -> 0() mark(U101(z0,z1,z2)) -> a__U101(mark(z0),z1,z2) mark(U102(z0,z1)) -> a__U102(mark(z0),z1) mark(U103(z0)) -> a__U103(mark(z0)) mark(U11(z0,z1,z2)) -> a__U11(mark(z0),z1,z2) 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(U171(z0,z1,z2)) -> a__U171(mark(z0),z1,z2) 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(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(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(afterNth(z0,z1)) -> a__afterNth(mark(z0),mark(z1)) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(fst(z0)) -> a__fst(mark(z0)) mark(head(z0)) -> a__head(mark(z0)) mark(isLNat(z0)) -> a__isLNat(z0) mark(isLNatKind(z0)) -> a__isLNatKind(z0) mark(isNatural(z0)) -> a__isNatural(z0) mark(isNaturalKind(z0)) -> a__isNaturalKind(z0) mark(isPLNat(z0)) -> a__isPLNat(z0) mark(isPLNatKind(z0)) -> a__isPLNatKind(z0) mark(natsFrom(z0)) -> a__natsFrom(mark(z0)) mark(nil()) -> nil() mark(pair(z0,z1)) -> pair(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) mark(snd(z0)) -> a__snd(mark(z0)) mark(splitAt(z0,z1)) -> a__splitAt(mark(z0),mark(z1)) mark(tail(z0)) -> a__tail(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(tt()) -> tt() - Signature: {A__AFTERNTH/2,A__AND/2,A__FST/1,A__HEAD/1,A__ISLNAT/1,A__ISLNATKIND/1,A__ISNATURAL/1,A__ISNATURALKIND/1 ,A__ISPLNAT/1,A__ISPLNATKIND/1,A__NATSFROM/1,A__SEL/2,A__SND/1,A__SPLITAT/2,A__TAIL/1,A__TAKE/2,A__U101/3 ,A__U102/2,A__U103/1,A__U11/3,A__U111/2,A__U112/1,A__U121/2,A__U122/1,A__U131/3,A__U132/2,A__U133/1 ,A__U141/3,A__U142/2,A__U143/1,A__U151/3,A__U152/2,A__U153/1,A__U161/2,A__U171/3,A__U181/2,A__U191/2 ,A__U201/4,A__U202/2,A__U21/2,A__U211/2,A__U221/3,A__U31/2,A__U41/3,A__U42/2,A__U43/1,A__U51/3,A__U52/2 ,A__U53/1,A__U61/2,A__U62/1,A__U71/2,A__U72/1,A__U81/2,A__U82/1,A__U91/2,A__U92/1,MARK/1,a__U101/3,a__U102/2 ,a__U103/1,a__U11/3,a__U111/2,a__U112/1,a__U121/2,a__U122/1,a__U131/3,a__U132/2,a__U133/1,a__U141/3 ,a__U142/2,a__U143/1,a__U151/3,a__U152/2,a__U153/1,a__U161/2,a__U171/3,a__U181/2,a__U191/2,a__U201/4 ,a__U202/2,a__U21/2,a__U211/2,a__U221/3,a__U31/2,a__U41/3,a__U42/2,a__U43/1,a__U51/3,a__U52/2,a__U53/1 ,a__U61/2,a__U62/1,a__U71/2,a__U72/1,a__U81/2,a__U82/1,a__U91/2,a__U92/1,a__afterNth/2,a__and/2,a__fst/1 ,a__head/1,a__isLNat/1,a__isLNatKind/1,a__isNatural/1,a__isNaturalKind/1,a__isPLNat/1,a__isPLNatKind/1 ,a__natsFrom/1,a__sel/2,a__snd/1,a__splitAt/2,a__tail/1,a__take/2,mark/1} / {0/0,U101/3,U102/2,U103/1,U11/3 ,U111/2,U112/1,U121/2,U122/1,U131/3,U132/2,U133/1,U141/3,U142/2,U143/1,U151/3,U152/2,U153/1,U161/2,U171/3 ,U181/2,U191/2,U201/4,U202/2,U21/2,U211/2,U221/3,U31/2,U41/3,U42/2,U43/1,U51/3,U52/2,U53/1,U61/2,U62/1,U71/2 ,U72/1,U81/2,U82/1,U91/2,U92/1,afterNth/2,and/2,c/2,c1/0,c10/0,c100/2,c101/2,c102/3,c103/0,c104/0,c105/2 ,c106/2,c107/1,c108/1,c109/1,c11/0,c110/1,c111/2,c112/0,c113/0,c114/2,c115/2,c116/3,c117/0,c118/0,c119/1 ,c12/0,c120/1,c121/2,c122/0,c123/3,c124/3,c125/0,c126/2,c127/2,c128/0,c129/3,c13/2,c130/0,c131/4,c132/0 ,c133/4,c134/0,c135/3,c136/4,c137/0,c138/4,c139/0,c14/0,c140/4,c141/0,c142/2,c143/2,c144/1,c145/2,c146/1 ,c147/2,c148/2,c149/2,c15/0,c150/2,c151/2,c152/2,c153/2,c154/2,c155/2,c156/2,c157/2,c158/2,c159/2,c16/0 ,c160/2,c161/2,c162/2,c163/2,c164/2,c165/2,c166/2,c167/2,c168/2,c169/2,c17/2,c170/2,c171/2,c172/2,c173/2 ,c174/2,c175/2,c176/2,c177/2,c178/2,c179/2,c18/0,c180/2,c181/2,c182/2,c183/2,c184/2,c185/2,c186/2,c187/1 ,c188/2,c189/2,c19/2,c190/2,c191/2,c192/2,c193/2,c194/2,c195/1,c196/1,c197/1,c198/2,c199/2,c2/2,c20/0,c200/2 ,c201/2,c202/2,c203/0,c204/1,c205/1,c206/1,c207/1,c208/0,c209/0,c21/0,c22/0,c23/2,c24/0,c25/2,c26/0,c27/0 ,c28/0,c29/2,c3/0,c30/0,c31/2,c32/0,c33/0,c34/0,c35/1,c36/0,c37/3,c38/3,c39/0,c4/0,c40/1,c41/0,c42/1,c43/0 ,c44/3,c45/3,c46/0,c47/1,c48/1,c49/0,c5/0,c50/1,c51/0,c52/1,c53/0,c54/3,c55/3,c56/0,c57/1,c58/0,c59/2,c6/3 ,c60/0,c61/2,c62/0,c63/0,c64/0,c65/2,c66/0,c67/2,c68/0,c69/0,c7/3,c70/0,c71/2,c72/0,c73/0,c74/0,c75/2,c76/0 ,c77/0,c78/0,c79/2,c8/0,c80/0,c81/0,c82/0,c83/2,c84/0,c85/0,c86/0,c87/4,c88/0,c89/1,c9/2,c90/0,c91/4,c92/0 ,c93/4,c94/0,c95/0,c96/3,c97/3,c98/2,c99/2,cons/2,fst/1,head/1,isLNat/1,isLNatKind/1,isNatural/1 ,isNaturalKind/1,isPLNat/1,isPLNatKind/1,natsFrom/1,nil/0,pair/2,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2 ,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AFTERNTH,A__AND,A__FST,A__HEAD,A__ISLNAT,A__ISLNATKIND ,A__ISNATURAL,A__ISNATURALKIND,A__ISPLNAT,A__ISPLNATKIND,A__NATSFROM,A__SEL,A__SND,A__SPLITAT,A__TAIL ,A__TAKE,A__U101,A__U102,A__U103,A__U11,A__U111,A__U112,A__U121,A__U122,A__U131,A__U132,A__U133,A__U141 ,A__U142,A__U143,A__U151,A__U152,A__U153,A__U161,A__U171,A__U181,A__U191,A__U201,A__U202,A__U21,A__U211 ,A__U221,A__U31,A__U41,A__U42,A__U43,A__U51,A__U52,A__U53,A__U61,A__U62,A__U71,A__U72,A__U81,A__U82,A__U91 ,A__U92,MARK,a__U101,a__U102,a__U103,a__U11,a__U111,a__U112,a__U121,a__U122,a__U131,a__U132,a__U133,a__U141 ,a__U142,a__U143,a__U151,a__U152,a__U153,a__U161,a__U171,a__U181,a__U191,a__U201,a__U202,a__U21,a__U211 ,a__U221,a__U31,a__U41,a__U42,a__U43,a__U51,a__U52,a__U53,a__U61,a__U62,a__U71,a__U72,a__U81,a__U82,a__U91 ,a__U92,a__afterNth,a__and,a__fst,a__head,a__isLNat,a__isLNatKind,a__isNatural,a__isNaturalKind,a__isPLNat ,a__isPLNatKind,a__natsFrom,a__sel,a__snd,a__splitAt,a__tail,a__take,mark} and constructors {0,U101,U102 ,U103,U11,U111,U112,U121,U122,U131,U132,U133,U141,U142,U143,U151,U152,U153,U161,U171,U181,U191,U201,U202,U21 ,U211,U221,U31,U41,U42,U43,U51,U52,U53,U61,U62,U71,U72,U81,U82,U91,U92,afterNth,and,c,c1,c10,c100,c101,c102 ,c103,c104,c105,c106,c107,c108,c109,c11,c110,c111,c112,c113,c114,c115,c116,c117,c118,c119,c12,c120,c121,c122 ,c123,c124,c125,c126,c127,c128,c129,c13,c130,c131,c132,c133,c134,c135,c136,c137,c138,c139,c14,c140,c141,c142 ,c143,c144,c145,c146,c147,c148,c149,c15,c150,c151,c152,c153,c154,c155,c156,c157,c158,c159,c16,c160,c161,c162 ,c163,c164,c165,c166,c167,c168,c169,c17,c170,c171,c172,c173,c174,c175,c176,c177,c178,c179,c18,c180,c181,c182 ,c183,c184,c185,c186,c187,c188,c189,c19,c190,c191,c192,c193,c194,c195,c196,c197,c198,c199,c2,c20,c200,c201 ,c202,c203,c204,c205,c206,c207,c208,c209,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36 ,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45,c46,c47,c48,c49,c5,c50,c51,c52,c53,c54,c55,c56,c57,c58,c59,c6,c60 ,c61,c62,c63,c64,c65,c66,c67,c68,c69,c7,c70,c71,c72,c73,c74,c75,c76,c77,c78,c79,c8,c80,c81,c82,c83,c84,c85 ,c86,c87,c88,c89,c9,c90,c91,c92,c93,c94,c95,c96,c97,c98,c99,cons,fst,head,isLNat,isLNatKind,isNatural ,isNaturalKind,isPLNat,isPLNatKind,natsFrom,nil,pair,s,sel,snd,splitAt,tail,take,tt} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: 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(z0,z1) -> c90() A__AND(tt(),z0) -> c89(MARK(z0)) A__FST(z0) -> c92() 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__HEAD(z0) -> c94() 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__ISLNAT(z0) -> c103() 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(nil()) -> c95() 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__ISLNATKIND(z0) -> c112() 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(nil()) -> c104() 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__ISNATURAL(z0) -> c117() 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__ISNATURALKIND(z0) -> c122() 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__ISPLNAT(z0) -> c125() 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__ISPLNATKIND(z0) -> c128() 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__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(z0) -> c134() 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__SPLITAT(z0,z1) -> c137() 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__TAIL(z0) -> c139() 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__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() A__U101(z0,z1,z2) -> c1() A__U101(tt(),z0,z1) -> c(A__U102(a__isNatural(z0),z1),A__ISNATURAL(z0)) A__U102(z0,z1) -> c3() A__U102(tt(),z0) -> c2(A__U103(a__isLNat(z0)),A__ISLNAT(z0)) A__U103(z0) -> c5() A__U103(tt()) -> c4() A__U11(z0,z1,z2) -> c8() 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__U111(z0,z1) -> c10() A__U111(tt(),z0) -> c9(A__U112(a__isLNat(z0)),A__ISLNAT(z0)) A__U112(z0) -> c12() A__U112(tt()) -> c11() A__U121(z0,z1) -> c14() A__U121(tt(),z0) -> c13(A__U122(a__isNatural(z0)),A__ISNATURAL(z0)) A__U122(z0) -> c16() A__U122(tt()) -> c15() A__U131(z0,z1,z2) -> c18() A__U131(tt(),z0,z1) -> c17(A__U132(a__isNatural(z0),z1),A__ISNATURAL(z0)) A__U132(z0,z1) -> c20() A__U132(tt(),z0) -> c19(A__U133(a__isLNat(z0)),A__ISLNAT(z0)) A__U133(z0) -> c22() A__U133(tt()) -> c21() A__U141(z0,z1,z2) -> c24() A__U141(tt(),z0,z1) -> c23(A__U142(a__isLNat(z0),z1),A__ISLNAT(z0)) A__U142(z0,z1) -> c26() A__U142(tt(),z0) -> c25(A__U143(a__isLNat(z0)),A__ISLNAT(z0)) A__U143(z0) -> c28() A__U143(tt()) -> c27() A__U151(z0,z1,z2) -> c30() A__U151(tt(),z0,z1) -> c29(A__U152(a__isNatural(z0),z1),A__ISNATURAL(z0)) A__U152(z0,z1) -> c32() A__U152(tt(),z0) -> c31(A__U153(a__isLNat(z0)),A__ISLNAT(z0)) A__U153(z0) -> c34() A__U153(tt()) -> c33() A__U161(z0,z1) -> c36() A__U161(tt(),z0) -> c35(MARK(z0)) A__U171(z0,z1,z2) -> c39() 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__U181(z0,z1) -> c41() A__U181(tt(),z0) -> c40(MARK(z0)) A__U191(z0,z1) -> c43() A__U191(tt(),z0) -> c42(MARK(z0)) A__U201(z0,z1,z2,z3) -> c46() 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__U202(z0,z1) -> c49() A__U202(pair(z0,z1),z2) -> c47(MARK(z2)) A__U202(pair(z0,z1),z2) -> c48(MARK(z1)) A__U21(z0,z1) -> c51() A__U21(tt(),z0) -> c50(MARK(z0)) A__U211(z0,z1) -> c53() A__U211(tt(),z0) -> c52(MARK(z0)) A__U221(z0,z1,z2) -> c56() 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__U31(z0,z1) -> c58() A__U31(tt(),z0) -> c57(MARK(z0)) A__U41(z0,z1,z2) -> c60() A__U41(tt(),z0,z1) -> c59(A__U42(a__isNatural(z0),z1),A__ISNATURAL(z0)) A__U42(z0,z1) -> c62() A__U42(tt(),z0) -> c61(A__U43(a__isLNat(z0)),A__ISLNAT(z0)) A__U43(z0) -> c64() A__U43(tt()) -> c63() A__U51(z0,z1,z2) -> c66() A__U51(tt(),z0,z1) -> c65(A__U52(a__isNatural(z0),z1),A__ISNATURAL(z0)) A__U52(z0,z1) -> c68() A__U52(tt(),z0) -> c67(A__U53(a__isLNat(z0)),A__ISLNAT(z0)) A__U53(z0) -> c70() A__U53(tt()) -> c69() A__U61(z0,z1) -> c72() A__U61(tt(),z0) -> c71(A__U62(a__isPLNat(z0)),A__ISPLNAT(z0)) A__U62(z0) -> c74() A__U62(tt()) -> c73() A__U71(z0,z1) -> c76() A__U71(tt(),z0) -> c75(A__U72(a__isNatural(z0)),A__ISNATURAL(z0)) A__U72(z0) -> c78() A__U72(tt()) -> c77() A__U81(z0,z1) -> c80() A__U81(tt(),z0) -> c79(A__U82(a__isPLNat(z0)),A__ISPLNAT(z0)) A__U82(z0) -> c82() A__U82(tt()) -> c81() A__U91(z0,z1) -> c84() A__U91(tt(),z0) -> c83(A__U92(a__isLNat(z0)),A__ISLNAT(z0)) A__U92(z0) -> c86() A__U92(tt()) -> c85() MARK(0()) -> c209() 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(U103(z0)) -> c145(A__U103(mark(z0)),MARK(z0)) MARK(U11(z0,z1,z2)) -> c147(A__U11(mark(z0),z1,z2),MARK(z0)) 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(U171(z0,z1,z2)) -> c166(A__U171(mark(z0),z1,z2),MARK(z0)) 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(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(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(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(and(z0,z1)) -> c194(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c204(MARK(z0)) MARK(fst(z0)) -> c177(A__FST(mark(z0)),MARK(z0)) MARK(head(z0)) -> c167(A__HEAD(mark(z0)),MARK(z0)) MARK(isLNat(z0)) -> c146(A__ISLNAT(z0)) MARK(isLNatKind(z0)) -> c196(A__ISLNATKIND(z0)) MARK(isNatural(z0)) -> c144(A__ISNATURAL(z0)) MARK(isNaturalKind(z0)) -> c195(A__ISNATURALKIND(z0)) MARK(isPLNat(z0)) -> c187(A__ISPLNAT(z0)) MARK(isPLNatKind(z0)) -> c197(A__ISPLNATKIND(z0)) MARK(natsFrom(z0)) -> c165(A__NATSFROM(mark(z0)),MARK(z0)) MARK(nil()) -> c208() MARK(pair(z0,z1)) -> c206(MARK(z0)) MARK(pair(z0,z1)) -> c207(MARK(z1)) MARK(s(z0)) -> c205(MARK(z0)) 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(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(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(tt()) -> c203() - Weak TRS: a__U101(z0,z1,z2) -> U101(z0,z1,z2) a__U101(tt(),z0,z1) -> a__U102(a__isNatural(z0),z1) a__U102(z0,z1) -> U102(z0,z1) a__U102(tt(),z0) -> a__U103(a__isLNat(z0)) a__U103(z0) -> U103(z0) a__U103(tt()) -> tt() a__U11(z0,z1,z2) -> U11(z0,z1,z2) a__U11(tt(),z0,z1) -> a__snd(a__splitAt(mark(z0),mark(z1))) a__U111(z0,z1) -> U111(z0,z1) a__U111(tt(),z0) -> a__U112(a__isLNat(z0)) a__U112(z0) -> U112(z0) a__U112(tt()) -> tt() a__U121(z0,z1) -> U121(z0,z1) a__U121(tt(),z0) -> a__U122(a__isNatural(z0)) a__U122(z0) -> U122(z0) a__U122(tt()) -> tt() a__U131(z0,z1,z2) -> U131(z0,z1,z2) a__U131(tt(),z0,z1) -> a__U132(a__isNatural(z0),z1) a__U132(z0,z1) -> U132(z0,z1) a__U132(tt(),z0) -> a__U133(a__isLNat(z0)) a__U133(z0) -> U133(z0) a__U133(tt()) -> tt() a__U141(z0,z1,z2) -> U141(z0,z1,z2) a__U141(tt(),z0,z1) -> a__U142(a__isLNat(z0),z1) a__U142(z0,z1) -> U142(z0,z1) a__U142(tt(),z0) -> a__U143(a__isLNat(z0)) a__U143(z0) -> U143(z0) a__U143(tt()) -> tt() a__U151(z0,z1,z2) -> U151(z0,z1,z2) a__U151(tt(),z0,z1) -> a__U152(a__isNatural(z0),z1) a__U152(z0,z1) -> U152(z0,z1) a__U152(tt(),z0) -> a__U153(a__isLNat(z0)) a__U153(z0) -> U153(z0) a__U153(tt()) -> tt() a__U161(z0,z1) -> U161(z0,z1) a__U161(tt(),z0) -> cons(mark(z0),natsFrom(s(z0))) a__U171(z0,z1,z2) -> U171(z0,z1,z2) a__U171(tt(),z0,z1) -> a__head(a__afterNth(mark(z0),mark(z1))) a__U181(z0,z1) -> U181(z0,z1) a__U181(tt(),z0) -> mark(z0) a__U191(z0,z1) -> U191(z0,z1) a__U191(tt(),z0) -> pair(nil(),mark(z0)) a__U201(z0,z1,z2,z3) -> U201(z0,z1,z2,z3) a__U201(tt(),z0,z1,z2) -> a__U202(a__splitAt(mark(z0),mark(z2)),z1) a__U202(z0,z1) -> U202(z0,z1) a__U202(pair(z0,z1),z2) -> pair(cons(mark(z2),z0),mark(z1)) a__U21(z0,z1) -> U21(z0,z1) a__U21(tt(),z0) -> mark(z0) a__U211(z0,z1) -> U211(z0,z1) a__U211(tt(),z0) -> mark(z0) a__U221(z0,z1,z2) -> U221(z0,z1,z2) a__U221(tt(),z0,z1) -> a__fst(a__splitAt(mark(z0),mark(z1))) a__U31(z0,z1) -> U31(z0,z1) a__U31(tt(),z0) -> mark(z0) a__U41(z0,z1,z2) -> U41(z0,z1,z2) a__U41(tt(),z0,z1) -> a__U42(a__isNatural(z0),z1) a__U42(z0,z1) -> U42(z0,z1) a__U42(tt(),z0) -> a__U43(a__isLNat(z0)) a__U43(z0) -> U43(z0) a__U43(tt()) -> tt() a__U51(z0,z1,z2) -> U51(z0,z1,z2) a__U51(tt(),z0,z1) -> a__U52(a__isNatural(z0),z1) a__U52(z0,z1) -> U52(z0,z1) a__U52(tt(),z0) -> a__U53(a__isLNat(z0)) a__U53(z0) -> U53(z0) a__U53(tt()) -> tt() a__U61(z0,z1) -> U61(z0,z1) a__U61(tt(),z0) -> a__U62(a__isPLNat(z0)) a__U62(z0) -> U62(z0) a__U62(tt()) -> tt() a__U71(z0,z1) -> U71(z0,z1) a__U71(tt(),z0) -> a__U72(a__isNatural(z0)) a__U72(z0) -> U72(z0) a__U72(tt()) -> tt() a__U81(z0,z1) -> U81(z0,z1) a__U81(tt(),z0) -> a__U82(a__isPLNat(z0)) a__U82(z0) -> U82(z0) a__U82(tt()) -> tt() a__U91(z0,z1) -> U91(z0,z1) a__U91(tt(),z0) -> a__U92(a__isLNat(z0)) a__U92(z0) -> U92(z0) a__U92(tt()) -> tt() 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(z0,z1) -> and(z0,z1) a__and(tt(),z0) -> mark(z0) a__fst(z0) -> fst(z0) a__fst(pair(z0,z1)) -> a__U21(a__and(a__and(a__isLNat(z0),isLNatKind(z0)),and(isLNat(z1),isLNatKind(z1))) ,z0) a__head(z0) -> head(z0) a__head(cons(z0,z1)) -> a__U31(a__and(a__and(a__isNatural(z0),isNaturalKind(z0)) ,and(isLNat(z1),isLNatKind(z1))) ,z0) a__isLNat(z0) -> isLNat(z0) 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(nil()) -> tt() 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__isLNatKind(z0) -> isLNatKind(z0) 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(nil()) -> tt() 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__isNatural(z0) -> isNatural(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__isNaturalKind(z0) -> isNaturalKind(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__isPLNat(z0) -> isPLNat(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__isPLNatKind(z0) -> isPLNatKind(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__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(z0) -> snd(z0) a__snd(pair(z0,z1)) -> a__U181(a__and(a__and(a__isLNat(z0),isLNatKind(z0)),and(isLNat(z1),isLNatKind(z1))) ,z1) a__splitAt(z0,z1) -> splitAt(z0,z1) 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__tail(z0) -> tail(z0) a__tail(cons(z0,z1)) -> a__U211(a__and(a__and(a__isNatural(z0),isNaturalKind(z0)) ,and(isLNat(z1),isLNatKind(z1))) ,z1) 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(0()) -> 0() mark(U101(z0,z1,z2)) -> a__U101(mark(z0),z1,z2) mark(U102(z0,z1)) -> a__U102(mark(z0),z1) mark(U103(z0)) -> a__U103(mark(z0)) mark(U11(z0,z1,z2)) -> a__U11(mark(z0),z1,z2) 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(U171(z0,z1,z2)) -> a__U171(mark(z0),z1,z2) 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(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(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(afterNth(z0,z1)) -> a__afterNth(mark(z0),mark(z1)) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(fst(z0)) -> a__fst(mark(z0)) mark(head(z0)) -> a__head(mark(z0)) mark(isLNat(z0)) -> a__isLNat(z0) mark(isLNatKind(z0)) -> a__isLNatKind(z0) mark(isNatural(z0)) -> a__isNatural(z0) mark(isNaturalKind(z0)) -> a__isNaturalKind(z0) mark(isPLNat(z0)) -> a__isPLNat(z0) mark(isPLNatKind(z0)) -> a__isPLNatKind(z0) mark(natsFrom(z0)) -> a__natsFrom(mark(z0)) mark(nil()) -> nil() mark(pair(z0,z1)) -> pair(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) mark(snd(z0)) -> a__snd(mark(z0)) mark(splitAt(z0,z1)) -> a__splitAt(mark(z0),mark(z1)) mark(tail(z0)) -> a__tail(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(tt()) -> tt() - Signature: {A__AFTERNTH/2,A__AND/2,A__FST/1,A__HEAD/1,A__ISLNAT/1,A__ISLNATKIND/1,A__ISNATURAL/1,A__ISNATURALKIND/1 ,A__ISPLNAT/1,A__ISPLNATKIND/1,A__NATSFROM/1,A__SEL/2,A__SND/1,A__SPLITAT/2,A__TAIL/1,A__TAKE/2,A__U101/3 ,A__U102/2,A__U103/1,A__U11/3,A__U111/2,A__U112/1,A__U121/2,A__U122/1,A__U131/3,A__U132/2,A__U133/1 ,A__U141/3,A__U142/2,A__U143/1,A__U151/3,A__U152/2,A__U153/1,A__U161/2,A__U171/3,A__U181/2,A__U191/2 ,A__U201/4,A__U202/2,A__U21/2,A__U211/2,A__U221/3,A__U31/2,A__U41/3,A__U42/2,A__U43/1,A__U51/3,A__U52/2 ,A__U53/1,A__U61/2,A__U62/1,A__U71/2,A__U72/1,A__U81/2,A__U82/1,A__U91/2,A__U92/1,MARK/1,a__U101/3,a__U102/2 ,a__U103/1,a__U11/3,a__U111/2,a__U112/1,a__U121/2,a__U122/1,a__U131/3,a__U132/2,a__U133/1,a__U141/3 ,a__U142/2,a__U143/1,a__U151/3,a__U152/2,a__U153/1,a__U161/2,a__U171/3,a__U181/2,a__U191/2,a__U201/4 ,a__U202/2,a__U21/2,a__U211/2,a__U221/3,a__U31/2,a__U41/3,a__U42/2,a__U43/1,a__U51/3,a__U52/2,a__U53/1 ,a__U61/2,a__U62/1,a__U71/2,a__U72/1,a__U81/2,a__U82/1,a__U91/2,a__U92/1,a__afterNth/2,a__and/2,a__fst/1 ,a__head/1,a__isLNat/1,a__isLNatKind/1,a__isNatural/1,a__isNaturalKind/1,a__isPLNat/1,a__isPLNatKind/1 ,a__natsFrom/1,a__sel/2,a__snd/1,a__splitAt/2,a__tail/1,a__take/2,mark/1} / {0/0,U101/3,U102/2,U103/1,U11/3 ,U111/2,U112/1,U121/2,U122/1,U131/3,U132/2,U133/1,U141/3,U142/2,U143/1,U151/3,U152/2,U153/1,U161/2,U171/3 ,U181/2,U191/2,U201/4,U202/2,U21/2,U211/2,U221/3,U31/2,U41/3,U42/2,U43/1,U51/3,U52/2,U53/1,U61/2,U62/1,U71/2 ,U72/1,U81/2,U82/1,U91/2,U92/1,afterNth/2,and/2,c/2,c1/0,c10/0,c100/2,c101/2,c102/3,c103/0,c104/0,c105/2 ,c106/2,c107/1,c108/1,c109/1,c11/0,c110/1,c111/2,c112/0,c113/0,c114/2,c115/2,c116/3,c117/0,c118/0,c119/1 ,c12/0,c120/1,c121/2,c122/0,c123/3,c124/3,c125/0,c126/2,c127/2,c128/0,c129/3,c13/2,c130/0,c131/4,c132/0 ,c133/4,c134/0,c135/3,c136/4,c137/0,c138/4,c139/0,c14/0,c140/4,c141/0,c142/2,c143/2,c144/1,c145/2,c146/1 ,c147/2,c148/2,c149/2,c15/0,c150/2,c151/2,c152/2,c153/2,c154/2,c155/2,c156/2,c157/2,c158/2,c159/2,c16/0 ,c160/2,c161/2,c162/2,c163/2,c164/2,c165/2,c166/2,c167/2,c168/2,c169/2,c17/2,c170/2,c171/2,c172/2,c173/2 ,c174/2,c175/2,c176/2,c177/2,c178/2,c179/2,c18/0,c180/2,c181/2,c182/2,c183/2,c184/2,c185/2,c186/2,c187/1 ,c188/2,c189/2,c19/2,c190/2,c191/2,c192/2,c193/2,c194/2,c195/1,c196/1,c197/1,c198/2,c199/2,c2/2,c20/0,c200/2 ,c201/2,c202/2,c203/0,c204/1,c205/1,c206/1,c207/1,c208/0,c209/0,c21/0,c22/0,c23/2,c24/0,c25/2,c26/0,c27/0 ,c28/0,c29/2,c3/0,c30/0,c31/2,c32/0,c33/0,c34/0,c35/1,c36/0,c37/3,c38/3,c39/0,c4/0,c40/1,c41/0,c42/1,c43/0 ,c44/3,c45/3,c46/0,c47/1,c48/1,c49/0,c5/0,c50/1,c51/0,c52/1,c53/0,c54/3,c55/3,c56/0,c57/1,c58/0,c59/2,c6/3 ,c60/0,c61/2,c62/0,c63/0,c64/0,c65/2,c66/0,c67/2,c68/0,c69/0,c7/3,c70/0,c71/2,c72/0,c73/0,c74/0,c75/2,c76/0 ,c77/0,c78/0,c79/2,c8/0,c80/0,c81/0,c82/0,c83/2,c84/0,c85/0,c86/0,c87/4,c88/0,c89/1,c9/2,c90/0,c91/4,c92/0 ,c93/4,c94/0,c95/0,c96/3,c97/3,c98/2,c99/2,cons/2,fst/1,head/1,isLNat/1,isLNatKind/1,isNatural/1 ,isNaturalKind/1,isPLNat/1,isPLNatKind/1,natsFrom/1,nil/0,pair/2,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2 ,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AFTERNTH,A__AND,A__FST,A__HEAD,A__ISLNAT,A__ISLNATKIND ,A__ISNATURAL,A__ISNATURALKIND,A__ISPLNAT,A__ISPLNATKIND,A__NATSFROM,A__SEL,A__SND,A__SPLITAT,A__TAIL ,A__TAKE,A__U101,A__U102,A__U103,A__U11,A__U111,A__U112,A__U121,A__U122,A__U131,A__U132,A__U133,A__U141 ,A__U142,A__U143,A__U151,A__U152,A__U153,A__U161,A__U171,A__U181,A__U191,A__U201,A__U202,A__U21,A__U211 ,A__U221,A__U31,A__U41,A__U42,A__U43,A__U51,A__U52,A__U53,A__U61,A__U62,A__U71,A__U72,A__U81,A__U82,A__U91 ,A__U92,MARK,a__U101,a__U102,a__U103,a__U11,a__U111,a__U112,a__U121,a__U122,a__U131,a__U132,a__U133,a__U141 ,a__U142,a__U143,a__U151,a__U152,a__U153,a__U161,a__U171,a__U181,a__U191,a__U201,a__U202,a__U21,a__U211 ,a__U221,a__U31,a__U41,a__U42,a__U43,a__U51,a__U52,a__U53,a__U61,a__U62,a__U71,a__U72,a__U81,a__U82,a__U91 ,a__U92,a__afterNth,a__and,a__fst,a__head,a__isLNat,a__isLNatKind,a__isNatural,a__isNaturalKind,a__isPLNat ,a__isPLNatKind,a__natsFrom,a__sel,a__snd,a__splitAt,a__tail,a__take,mark} and constructors {0,U101,U102 ,U103,U11,U111,U112,U121,U122,U131,U132,U133,U141,U142,U143,U151,U152,U153,U161,U171,U181,U191,U201,U202,U21 ,U211,U221,U31,U41,U42,U43,U51,U52,U53,U61,U62,U71,U72,U81,U82,U91,U92,afterNth,and,c,c1,c10,c100,c101,c102 ,c103,c104,c105,c106,c107,c108,c109,c11,c110,c111,c112,c113,c114,c115,c116,c117,c118,c119,c12,c120,c121,c122 ,c123,c124,c125,c126,c127,c128,c129,c13,c130,c131,c132,c133,c134,c135,c136,c137,c138,c139,c14,c140,c141,c142 ,c143,c144,c145,c146,c147,c148,c149,c15,c150,c151,c152,c153,c154,c155,c156,c157,c158,c159,c16,c160,c161,c162 ,c163,c164,c165,c166,c167,c168,c169,c17,c170,c171,c172,c173,c174,c175,c176,c177,c178,c179,c18,c180,c181,c182 ,c183,c184,c185,c186,c187,c188,c189,c19,c190,c191,c192,c193,c194,c195,c196,c197,c198,c199,c2,c20,c200,c201 ,c202,c203,c204,c205,c206,c207,c208,c209,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36 ,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45,c46,c47,c48,c49,c5,c50,c51,c52,c53,c54,c55,c56,c57,c58,c59,c6,c60 ,c61,c62,c63,c64,c65,c66,c67,c68,c69,c7,c70,c71,c72,c73,c74,c75,c76,c77,c78,c79,c8,c80,c81,c82,c83,c84,c85 ,c86,c87,c88,c89,c9,c90,c91,c92,c93,c94,c95,c96,c97,c98,c99,cons,fst,head,isLNat,isLNatKind,isNatural ,isNaturalKind,isPLNat,isPLNatKind,natsFrom,nil,pair,s,sel,snd,splitAt,tail,take,tt} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: 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(z0,z1) -> c90() A__AND(tt(),z0) -> c89(MARK(z0)) A__FST(z0) -> c92() 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__HEAD(z0) -> c94() 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__ISLNAT(z0) -> c103() 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(nil()) -> c95() 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__ISLNATKIND(z0) -> c112() 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(nil()) -> c104() 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__ISNATURAL(z0) -> c117() 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__ISNATURALKIND(z0) -> c122() 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__ISPLNAT(z0) -> c125() 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__ISPLNATKIND(z0) -> c128() 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__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(z0) -> c134() 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__SPLITAT(z0,z1) -> c137() 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__TAIL(z0) -> c139() 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__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() A__U101(z0,z1,z2) -> c1() A__U101(tt(),z0,z1) -> c(A__U102(a__isNatural(z0),z1),A__ISNATURAL(z0)) A__U102(z0,z1) -> c3() A__U102(tt(),z0) -> c2(A__U103(a__isLNat(z0)),A__ISLNAT(z0)) A__U103(z0) -> c5() A__U103(tt()) -> c4() A__U11(z0,z1,z2) -> c8() 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__U111(z0,z1) -> c10() A__U111(tt(),z0) -> c9(A__U112(a__isLNat(z0)),A__ISLNAT(z0)) A__U112(z0) -> c12() A__U112(tt()) -> c11() A__U121(z0,z1) -> c14() A__U121(tt(),z0) -> c13(A__U122(a__isNatural(z0)),A__ISNATURAL(z0)) A__U122(z0) -> c16() A__U122(tt()) -> c15() A__U131(z0,z1,z2) -> c18() A__U131(tt(),z0,z1) -> c17(A__U132(a__isNatural(z0),z1),A__ISNATURAL(z0)) A__U132(z0,z1) -> c20() A__U132(tt(),z0) -> c19(A__U133(a__isLNat(z0)),A__ISLNAT(z0)) A__U133(z0) -> c22() A__U133(tt()) -> c21() A__U141(z0,z1,z2) -> c24() A__U141(tt(),z0,z1) -> c23(A__U142(a__isLNat(z0),z1),A__ISLNAT(z0)) A__U142(z0,z1) -> c26() A__U142(tt(),z0) -> c25(A__U143(a__isLNat(z0)),A__ISLNAT(z0)) A__U143(z0) -> c28() A__U143(tt()) -> c27() A__U151(z0,z1,z2) -> c30() A__U151(tt(),z0,z1) -> c29(A__U152(a__isNatural(z0),z1),A__ISNATURAL(z0)) A__U152(z0,z1) -> c32() A__U152(tt(),z0) -> c31(A__U153(a__isLNat(z0)),A__ISLNAT(z0)) A__U153(z0) -> c34() A__U153(tt()) -> c33() A__U161(z0,z1) -> c36() A__U161(tt(),z0) -> c35(MARK(z0)) A__U171(z0,z1,z2) -> c39() 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__U181(z0,z1) -> c41() A__U181(tt(),z0) -> c40(MARK(z0)) A__U191(z0,z1) -> c43() A__U191(tt(),z0) -> c42(MARK(z0)) A__U201(z0,z1,z2,z3) -> c46() 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__U202(z0,z1) -> c49() A__U202(pair(z0,z1),z2) -> c47(MARK(z2)) A__U202(pair(z0,z1),z2) -> c48(MARK(z1)) A__U21(z0,z1) -> c51() A__U21(tt(),z0) -> c50(MARK(z0)) A__U211(z0,z1) -> c53() A__U211(tt(),z0) -> c52(MARK(z0)) A__U221(z0,z1,z2) -> c56() 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__U31(z0,z1) -> c58() A__U31(tt(),z0) -> c57(MARK(z0)) A__U41(z0,z1,z2) -> c60() A__U41(tt(),z0,z1) -> c59(A__U42(a__isNatural(z0),z1),A__ISNATURAL(z0)) A__U42(z0,z1) -> c62() A__U42(tt(),z0) -> c61(A__U43(a__isLNat(z0)),A__ISLNAT(z0)) A__U43(z0) -> c64() A__U43(tt()) -> c63() A__U51(z0,z1,z2) -> c66() A__U51(tt(),z0,z1) -> c65(A__U52(a__isNatural(z0),z1),A__ISNATURAL(z0)) A__U52(z0,z1) -> c68() A__U52(tt(),z0) -> c67(A__U53(a__isLNat(z0)),A__ISLNAT(z0)) A__U53(z0) -> c70() A__U53(tt()) -> c69() A__U61(z0,z1) -> c72() A__U61(tt(),z0) -> c71(A__U62(a__isPLNat(z0)),A__ISPLNAT(z0)) A__U62(z0) -> c74() A__U62(tt()) -> c73() A__U71(z0,z1) -> c76() A__U71(tt(),z0) -> c75(A__U72(a__isNatural(z0)),A__ISNATURAL(z0)) A__U72(z0) -> c78() A__U72(tt()) -> c77() A__U81(z0,z1) -> c80() A__U81(tt(),z0) -> c79(A__U82(a__isPLNat(z0)),A__ISPLNAT(z0)) A__U82(z0) -> c82() A__U82(tt()) -> c81() A__U91(z0,z1) -> c84() A__U91(tt(),z0) -> c83(A__U92(a__isLNat(z0)),A__ISLNAT(z0)) A__U92(z0) -> c86() A__U92(tt()) -> c85() MARK(0()) -> c209() 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(U103(z0)) -> c145(A__U103(mark(z0)),MARK(z0)) MARK(U11(z0,z1,z2)) -> c147(A__U11(mark(z0),z1,z2),MARK(z0)) 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(U171(z0,z1,z2)) -> c166(A__U171(mark(z0),z1,z2),MARK(z0)) 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(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(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(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(and(z0,z1)) -> c194(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c204(MARK(z0)) MARK(fst(z0)) -> c177(A__FST(mark(z0)),MARK(z0)) MARK(head(z0)) -> c167(A__HEAD(mark(z0)),MARK(z0)) MARK(isLNat(z0)) -> c146(A__ISLNAT(z0)) MARK(isLNatKind(z0)) -> c196(A__ISLNATKIND(z0)) MARK(isNatural(z0)) -> c144(A__ISNATURAL(z0)) MARK(isNaturalKind(z0)) -> c195(A__ISNATURALKIND(z0)) MARK(isPLNat(z0)) -> c187(A__ISPLNAT(z0)) MARK(isPLNatKind(z0)) -> c197(A__ISPLNATKIND(z0)) MARK(natsFrom(z0)) -> c165(A__NATSFROM(mark(z0)),MARK(z0)) MARK(nil()) -> c208() MARK(pair(z0,z1)) -> c206(MARK(z0)) MARK(pair(z0,z1)) -> c207(MARK(z1)) MARK(s(z0)) -> c205(MARK(z0)) 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(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(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(tt()) -> c203() - Weak TRS: a__U101(z0,z1,z2) -> U101(z0,z1,z2) a__U101(tt(),z0,z1) -> a__U102(a__isNatural(z0),z1) a__U102(z0,z1) -> U102(z0,z1) a__U102(tt(),z0) -> a__U103(a__isLNat(z0)) a__U103(z0) -> U103(z0) a__U103(tt()) -> tt() a__U11(z0,z1,z2) -> U11(z0,z1,z2) a__U11(tt(),z0,z1) -> a__snd(a__splitAt(mark(z0),mark(z1))) a__U111(z0,z1) -> U111(z0,z1) a__U111(tt(),z0) -> a__U112(a__isLNat(z0)) a__U112(z0) -> U112(z0) a__U112(tt()) -> tt() a__U121(z0,z1) -> U121(z0,z1) a__U121(tt(),z0) -> a__U122(a__isNatural(z0)) a__U122(z0) -> U122(z0) a__U122(tt()) -> tt() a__U131(z0,z1,z2) -> U131(z0,z1,z2) a__U131(tt(),z0,z1) -> a__U132(a__isNatural(z0),z1) a__U132(z0,z1) -> U132(z0,z1) a__U132(tt(),z0) -> a__U133(a__isLNat(z0)) a__U133(z0) -> U133(z0) a__U133(tt()) -> tt() a__U141(z0,z1,z2) -> U141(z0,z1,z2) a__U141(tt(),z0,z1) -> a__U142(a__isLNat(z0),z1) a__U142(z0,z1) -> U142(z0,z1) a__U142(tt(),z0) -> a__U143(a__isLNat(z0)) a__U143(z0) -> U143(z0) a__U143(tt()) -> tt() a__U151(z0,z1,z2) -> U151(z0,z1,z2) a__U151(tt(),z0,z1) -> a__U152(a__isNatural(z0),z1) a__U152(z0,z1) -> U152(z0,z1) a__U152(tt(),z0) -> a__U153(a__isLNat(z0)) a__U153(z0) -> U153(z0) a__U153(tt()) -> tt() a__U161(z0,z1) -> U161(z0,z1) a__U161(tt(),z0) -> cons(mark(z0),natsFrom(s(z0))) a__U171(z0,z1,z2) -> U171(z0,z1,z2) a__U171(tt(),z0,z1) -> a__head(a__afterNth(mark(z0),mark(z1))) a__U181(z0,z1) -> U181(z0,z1) a__U181(tt(),z0) -> mark(z0) a__U191(z0,z1) -> U191(z0,z1) a__U191(tt(),z0) -> pair(nil(),mark(z0)) a__U201(z0,z1,z2,z3) -> U201(z0,z1,z2,z3) a__U201(tt(),z0,z1,z2) -> a__U202(a__splitAt(mark(z0),mark(z2)),z1) a__U202(z0,z1) -> U202(z0,z1) a__U202(pair(z0,z1),z2) -> pair(cons(mark(z2),z0),mark(z1)) a__U21(z0,z1) -> U21(z0,z1) a__U21(tt(),z0) -> mark(z0) a__U211(z0,z1) -> U211(z0,z1) a__U211(tt(),z0) -> mark(z0) a__U221(z0,z1,z2) -> U221(z0,z1,z2) a__U221(tt(),z0,z1) -> a__fst(a__splitAt(mark(z0),mark(z1))) a__U31(z0,z1) -> U31(z0,z1) a__U31(tt(),z0) -> mark(z0) a__U41(z0,z1,z2) -> U41(z0,z1,z2) a__U41(tt(),z0,z1) -> a__U42(a__isNatural(z0),z1) a__U42(z0,z1) -> U42(z0,z1) a__U42(tt(),z0) -> a__U43(a__isLNat(z0)) a__U43(z0) -> U43(z0) a__U43(tt()) -> tt() a__U51(z0,z1,z2) -> U51(z0,z1,z2) a__U51(tt(),z0,z1) -> a__U52(a__isNatural(z0),z1) a__U52(z0,z1) -> U52(z0,z1) a__U52(tt(),z0) -> a__U53(a__isLNat(z0)) a__U53(z0) -> U53(z0) a__U53(tt()) -> tt() a__U61(z0,z1) -> U61(z0,z1) a__U61(tt(),z0) -> a__U62(a__isPLNat(z0)) a__U62(z0) -> U62(z0) a__U62(tt()) -> tt() a__U71(z0,z1) -> U71(z0,z1) a__U71(tt(),z0) -> a__U72(a__isNatural(z0)) a__U72(z0) -> U72(z0) a__U72(tt()) -> tt() a__U81(z0,z1) -> U81(z0,z1) a__U81(tt(),z0) -> a__U82(a__isPLNat(z0)) a__U82(z0) -> U82(z0) a__U82(tt()) -> tt() a__U91(z0,z1) -> U91(z0,z1) a__U91(tt(),z0) -> a__U92(a__isLNat(z0)) a__U92(z0) -> U92(z0) a__U92(tt()) -> tt() 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(z0,z1) -> and(z0,z1) a__and(tt(),z0) -> mark(z0) a__fst(z0) -> fst(z0) a__fst(pair(z0,z1)) -> a__U21(a__and(a__and(a__isLNat(z0),isLNatKind(z0)),and(isLNat(z1),isLNatKind(z1))) ,z0) a__head(z0) -> head(z0) a__head(cons(z0,z1)) -> a__U31(a__and(a__and(a__isNatural(z0),isNaturalKind(z0)) ,and(isLNat(z1),isLNatKind(z1))) ,z0) a__isLNat(z0) -> isLNat(z0) 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(nil()) -> tt() 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__isLNatKind(z0) -> isLNatKind(z0) 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(nil()) -> tt() 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__isNatural(z0) -> isNatural(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__isNaturalKind(z0) -> isNaturalKind(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__isPLNat(z0) -> isPLNat(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__isPLNatKind(z0) -> isPLNatKind(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__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(z0) -> snd(z0) a__snd(pair(z0,z1)) -> a__U181(a__and(a__and(a__isLNat(z0),isLNatKind(z0)),and(isLNat(z1),isLNatKind(z1))) ,z1) a__splitAt(z0,z1) -> splitAt(z0,z1) 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__tail(z0) -> tail(z0) a__tail(cons(z0,z1)) -> a__U211(a__and(a__and(a__isNatural(z0),isNaturalKind(z0)) ,and(isLNat(z1),isLNatKind(z1))) ,z1) 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(0()) -> 0() mark(U101(z0,z1,z2)) -> a__U101(mark(z0),z1,z2) mark(U102(z0,z1)) -> a__U102(mark(z0),z1) mark(U103(z0)) -> a__U103(mark(z0)) mark(U11(z0,z1,z2)) -> a__U11(mark(z0),z1,z2) 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(U171(z0,z1,z2)) -> a__U171(mark(z0),z1,z2) 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(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(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(afterNth(z0,z1)) -> a__afterNth(mark(z0),mark(z1)) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(fst(z0)) -> a__fst(mark(z0)) mark(head(z0)) -> a__head(mark(z0)) mark(isLNat(z0)) -> a__isLNat(z0) mark(isLNatKind(z0)) -> a__isLNatKind(z0) mark(isNatural(z0)) -> a__isNatural(z0) mark(isNaturalKind(z0)) -> a__isNaturalKind(z0) mark(isPLNat(z0)) -> a__isPLNat(z0) mark(isPLNatKind(z0)) -> a__isPLNatKind(z0) mark(natsFrom(z0)) -> a__natsFrom(mark(z0)) mark(nil()) -> nil() mark(pair(z0,z1)) -> pair(mark(z0),mark(z1)) mark(s(z0)) -> s(mark(z0)) mark(sel(z0,z1)) -> a__sel(mark(z0),mark(z1)) mark(snd(z0)) -> a__snd(mark(z0)) mark(splitAt(z0,z1)) -> a__splitAt(mark(z0),mark(z1)) mark(tail(z0)) -> a__tail(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(tt()) -> tt() - Signature: {A__AFTERNTH/2,A__AND/2,A__FST/1,A__HEAD/1,A__ISLNAT/1,A__ISLNATKIND/1,A__ISNATURAL/1,A__ISNATURALKIND/1 ,A__ISPLNAT/1,A__ISPLNATKIND/1,A__NATSFROM/1,A__SEL/2,A__SND/1,A__SPLITAT/2,A__TAIL/1,A__TAKE/2,A__U101/3 ,A__U102/2,A__U103/1,A__U11/3,A__U111/2,A__U112/1,A__U121/2,A__U122/1,A__U131/3,A__U132/2,A__U133/1 ,A__U141/3,A__U142/2,A__U143/1,A__U151/3,A__U152/2,A__U153/1,A__U161/2,A__U171/3,A__U181/2,A__U191/2 ,A__U201/4,A__U202/2,A__U21/2,A__U211/2,A__U221/3,A__U31/2,A__U41/3,A__U42/2,A__U43/1,A__U51/3,A__U52/2 ,A__U53/1,A__U61/2,A__U62/1,A__U71/2,A__U72/1,A__U81/2,A__U82/1,A__U91/2,A__U92/1,MARK/1,a__U101/3,a__U102/2 ,a__U103/1,a__U11/3,a__U111/2,a__U112/1,a__U121/2,a__U122/1,a__U131/3,a__U132/2,a__U133/1,a__U141/3 ,a__U142/2,a__U143/1,a__U151/3,a__U152/2,a__U153/1,a__U161/2,a__U171/3,a__U181/2,a__U191/2,a__U201/4 ,a__U202/2,a__U21/2,a__U211/2,a__U221/3,a__U31/2,a__U41/3,a__U42/2,a__U43/1,a__U51/3,a__U52/2,a__U53/1 ,a__U61/2,a__U62/1,a__U71/2,a__U72/1,a__U81/2,a__U82/1,a__U91/2,a__U92/1,a__afterNth/2,a__and/2,a__fst/1 ,a__head/1,a__isLNat/1,a__isLNatKind/1,a__isNatural/1,a__isNaturalKind/1,a__isPLNat/1,a__isPLNatKind/1 ,a__natsFrom/1,a__sel/2,a__snd/1,a__splitAt/2,a__tail/1,a__take/2,mark/1} / {0/0,U101/3,U102/2,U103/1,U11/3 ,U111/2,U112/1,U121/2,U122/1,U131/3,U132/2,U133/1,U141/3,U142/2,U143/1,U151/3,U152/2,U153/1,U161/2,U171/3 ,U181/2,U191/2,U201/4,U202/2,U21/2,U211/2,U221/3,U31/2,U41/3,U42/2,U43/1,U51/3,U52/2,U53/1,U61/2,U62/1,U71/2 ,U72/1,U81/2,U82/1,U91/2,U92/1,afterNth/2,and/2,c/2,c1/0,c10/0,c100/2,c101/2,c102/3,c103/0,c104/0,c105/2 ,c106/2,c107/1,c108/1,c109/1,c11/0,c110/1,c111/2,c112/0,c113/0,c114/2,c115/2,c116/3,c117/0,c118/0,c119/1 ,c12/0,c120/1,c121/2,c122/0,c123/3,c124/3,c125/0,c126/2,c127/2,c128/0,c129/3,c13/2,c130/0,c131/4,c132/0 ,c133/4,c134/0,c135/3,c136/4,c137/0,c138/4,c139/0,c14/0,c140/4,c141/0,c142/2,c143/2,c144/1,c145/2,c146/1 ,c147/2,c148/2,c149/2,c15/0,c150/2,c151/2,c152/2,c153/2,c154/2,c155/2,c156/2,c157/2,c158/2,c159/2,c16/0 ,c160/2,c161/2,c162/2,c163/2,c164/2,c165/2,c166/2,c167/2,c168/2,c169/2,c17/2,c170/2,c171/2,c172/2,c173/2 ,c174/2,c175/2,c176/2,c177/2,c178/2,c179/2,c18/0,c180/2,c181/2,c182/2,c183/2,c184/2,c185/2,c186/2,c187/1 ,c188/2,c189/2,c19/2,c190/2,c191/2,c192/2,c193/2,c194/2,c195/1,c196/1,c197/1,c198/2,c199/2,c2/2,c20/0,c200/2 ,c201/2,c202/2,c203/0,c204/1,c205/1,c206/1,c207/1,c208/0,c209/0,c21/0,c22/0,c23/2,c24/0,c25/2,c26/0,c27/0 ,c28/0,c29/2,c3/0,c30/0,c31/2,c32/0,c33/0,c34/0,c35/1,c36/0,c37/3,c38/3,c39/0,c4/0,c40/1,c41/0,c42/1,c43/0 ,c44/3,c45/3,c46/0,c47/1,c48/1,c49/0,c5/0,c50/1,c51/0,c52/1,c53/0,c54/3,c55/3,c56/0,c57/1,c58/0,c59/2,c6/3 ,c60/0,c61/2,c62/0,c63/0,c64/0,c65/2,c66/0,c67/2,c68/0,c69/0,c7/3,c70/0,c71/2,c72/0,c73/0,c74/0,c75/2,c76/0 ,c77/0,c78/0,c79/2,c8/0,c80/0,c81/0,c82/0,c83/2,c84/0,c85/0,c86/0,c87/4,c88/0,c89/1,c9/2,c90/0,c91/4,c92/0 ,c93/4,c94/0,c95/0,c96/3,c97/3,c98/2,c99/2,cons/2,fst/1,head/1,isLNat/1,isLNatKind/1,isNatural/1 ,isNaturalKind/1,isPLNat/1,isPLNatKind/1,natsFrom/1,nil/0,pair/2,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2 ,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AFTERNTH,A__AND,A__FST,A__HEAD,A__ISLNAT,A__ISLNATKIND ,A__ISNATURAL,A__ISNATURALKIND,A__ISPLNAT,A__ISPLNATKIND,A__NATSFROM,A__SEL,A__SND,A__SPLITAT,A__TAIL ,A__TAKE,A__U101,A__U102,A__U103,A__U11,A__U111,A__U112,A__U121,A__U122,A__U131,A__U132,A__U133,A__U141 ,A__U142,A__U143,A__U151,A__U152,A__U153,A__U161,A__U171,A__U181,A__U191,A__U201,A__U202,A__U21,A__U211 ,A__U221,A__U31,A__U41,A__U42,A__U43,A__U51,A__U52,A__U53,A__U61,A__U62,A__U71,A__U72,A__U81,A__U82,A__U91 ,A__U92,MARK,a__U101,a__U102,a__U103,a__U11,a__U111,a__U112,a__U121,a__U122,a__U131,a__U132,a__U133,a__U141 ,a__U142,a__U143,a__U151,a__U152,a__U153,a__U161,a__U171,a__U181,a__U191,a__U201,a__U202,a__U21,a__U211 ,a__U221,a__U31,a__U41,a__U42,a__U43,a__U51,a__U52,a__U53,a__U61,a__U62,a__U71,a__U72,a__U81,a__U82,a__U91 ,a__U92,a__afterNth,a__and,a__fst,a__head,a__isLNat,a__isLNatKind,a__isNatural,a__isNaturalKind,a__isPLNat ,a__isPLNatKind,a__natsFrom,a__sel,a__snd,a__splitAt,a__tail,a__take,mark} and constructors {0,U101,U102 ,U103,U11,U111,U112,U121,U122,U131,U132,U133,U141,U142,U143,U151,U152,U153,U161,U171,U181,U191,U201,U202,U21 ,U211,U221,U31,U41,U42,U43,U51,U52,U53,U61,U62,U71,U72,U81,U82,U91,U92,afterNth,and,c,c1,c10,c100,c101,c102 ,c103,c104,c105,c106,c107,c108,c109,c11,c110,c111,c112,c113,c114,c115,c116,c117,c118,c119,c12,c120,c121,c122 ,c123,c124,c125,c126,c127,c128,c129,c13,c130,c131,c132,c133,c134,c135,c136,c137,c138,c139,c14,c140,c141,c142 ,c143,c144,c145,c146,c147,c148,c149,c15,c150,c151,c152,c153,c154,c155,c156,c157,c158,c159,c16,c160,c161,c162 ,c163,c164,c165,c166,c167,c168,c169,c17,c170,c171,c172,c173,c174,c175,c176,c177,c178,c179,c18,c180,c181,c182 ,c183,c184,c185,c186,c187,c188,c189,c19,c190,c191,c192,c193,c194,c195,c196,c197,c198,c199,c2,c20,c200,c201 ,c202,c203,c204,c205,c206,c207,c208,c209,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36 ,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45,c46,c47,c48,c49,c5,c50,c51,c52,c53,c54,c55,c56,c57,c58,c59,c6,c60 ,c61,c62,c63,c64,c65,c66,c67,c68,c69,c7,c70,c71,c72,c73,c74,c75,c76,c77,c78,c79,c8,c80,c81,c82,c83,c84,c85 ,c86,c87,c88,c89,c9,c90,c91,c92,c93,c94,c95,c96,c97,c98,c99,cons,fst,head,isLNat,isLNatKind,isNatural ,isNaturalKind,isPLNat,isPLNatKind,natsFrom,nil,pair,s,sel,snd,splitAt,tail,take,tt} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: A__ISLNATKIND(x){x -> tail(x)} = A__ISLNATKIND(tail(x)) ->^+ c110(A__ISLNATKIND(x)) = C[A__ISLNATKIND(x) = A__ISLNATKIND(x){}] WORST_CASE(Omega(n^1),?)