MAYBE MAYBE TRS: { U102(tt()) -> U103(isLNatKind()), isNaturalKind() -> tt(), isNaturalKind() -> U211(isLNatKind()), isNaturalKind() -> U221(isNaturalKind()), isNaturalKind() -> U231(isNaturalKind()), U101(tt()) -> U102(isNaturalKind()), U103(tt()) -> U104(isLNatKind()), isLNatKind() -> tt(), isLNatKind() -> U111(isNaturalKind()), isLNatKind() -> U121(isNaturalKind()), isLNatKind() -> U131(isPLNatKind()), isLNatKind() -> U141(isNaturalKind()), isLNatKind() -> U151(isPLNatKind()), isLNatKind() -> U161(isLNatKind()), isLNatKind() -> U171(isNaturalKind()), U104(tt()) -> U105(isNatural()), U105(tt()) -> U106(isLNat()), isNatural() -> tt(), isNatural() -> U181(isLNatKind()), isNatural() -> U191(isNaturalKind()), isNatural() -> U201(isNaturalKind()), U106(tt()) -> tt(), isLNat() -> U101(isNaturalKind()), isLNat() -> tt(), isLNat() -> U41(isNaturalKind()), isLNat() -> U51(isNaturalKind()), isLNat() -> U61(isPLNatKind()), isLNat() -> U71(isNaturalKind()), isLNat() -> U81(isPLNatKind()), isLNat() -> U91(isLNatKind()), U12(tt()) -> U13(isLNat()), U11(tt()) -> U12(isNaturalKind()), U112(tt()) -> tt(), U111(tt()) -> U112(isLNatKind()), U13(tt()) -> U14(isLNatKind()), U122(tt()) -> tt(), U121(tt()) -> U122(isLNatKind()), U14(tt()) -> snd(splitAt(N, XS)), U131(tt()) -> tt(), snd(pair(X, Y)) -> U301(isLNat()), splitAt(0(), XS) -> U311(isLNat()), splitAt(s(N), cons(X)) -> U321(isNatural()), U141(tt()) -> tt(), U151(tt()) -> tt(), U161(tt()) -> tt(), U172(tt()) -> tt(), U171(tt()) -> U172(isLNatKind()), U182(tt()) -> U183(isLNat()), U181(tt()) -> U182(isLNatKind()), U183(tt()) -> tt(), U192(tt()) -> U193(isNatural()), U191(tt()) -> U192(isNaturalKind()), U193(tt()) -> tt(), U202(tt()) -> U203(isLNatKind()), U201(tt()) -> U202(isNaturalKind()), U203(tt()) -> U204(isLNatKind()), U204(tt()) -> U205(isNatural()), U205(tt()) -> U206(isLNat()), U206(tt()) -> tt(), U22(tt()) -> U23(isLNat()), U21(tt()) -> U22(isLNatKind()), U211(tt()) -> tt(), U23(tt()) -> U24(isLNatKind()), U221(tt()) -> tt(), U24(tt()) -> X, U232(tt()) -> tt(), U231(tt()) -> U232(isLNatKind()), U242(tt()) -> U243(isLNatKind()), U241(tt()) -> U242(isLNatKind()), U243(tt()) -> U244(isLNatKind()), U244(tt()) -> U245(isLNat()), U245(tt()) -> U246(isLNat()), U246(tt()) -> tt(), U252(tt()) -> U253(isLNatKind()), U251(tt()) -> U252(isNaturalKind()), U253(tt()) -> U254(isLNatKind()), U254(tt()) -> U255(isNatural()), U255(tt()) -> U256(isLNat()), U256(tt()) -> tt(), U262(tt()) -> tt(), U261(tt()) -> U262(isLNatKind()), U272(tt()) -> tt(), U271(tt()) -> U272(isLNatKind()), U282(tt()) -> cons(N), U281(tt()) -> U282(isNaturalKind()), U292(tt()) -> U293(isLNat()), U291(tt()) -> U292(isNaturalKind()), U293(tt()) -> U294(isLNatKind()), U294(tt()) -> head(afterNth(N, XS)), head(cons(N)) -> U31(isNatural()), afterNth(N, XS) -> U11(isNatural()), U302(tt()) -> U303(isLNat()), U301(tt()) -> U302(isLNatKind()), U303(tt()) -> U304(isLNatKind()), U304(tt()) -> Y, U32(tt()) -> U33(isLNat()), U31(tt()) -> U32(isNaturalKind()), U312(tt()) -> pair(nil(), XS), U311(tt()) -> U312(isLNatKind()), U33(tt()) -> U34(isLNatKind()), U322(tt()) -> U323(isNatural()), U321(tt()) -> U322(isNaturalKind()), U323(tt()) -> U324(isNaturalKind()), U324(tt()) -> U325(isLNat()), U325(tt()) -> U326(isLNatKind()), U326(tt()) -> U327(splitAt(N, XS)), U327(pair(YS, ZS)) -> pair(cons(X), ZS), U34(tt()) -> N, U332(tt()) -> U333(isLNat()), U331(tt()) -> U332(isNaturalKind()), U333(tt()) -> U334(isLNatKind()), U334(tt()) -> XS, U342(tt()) -> U343(isLNat()), U341(tt()) -> U342(isNaturalKind()), U343(tt()) -> U344(isLNatKind()), U344(tt()) -> fst(splitAt(N, XS)), fst(pair(X, Y)) -> U21(isLNat()), U42(tt()) -> U43(isLNatKind()), U41(tt()) -> U42(isNaturalKind()), U43(tt()) -> U44(isLNatKind()), U44(tt()) -> U45(isNatural()), U45(tt()) -> U46(isLNat()), U46(tt()) -> tt(), U52(tt()) -> U53(isLNatKind()), U51(tt()) -> U52(isNaturalKind()), U53(tt()) -> U54(isLNatKind()), U54(tt()) -> U55(isNatural()), U55(tt()) -> U56(isLNat()), U56(tt()) -> tt(), U62(tt()) -> U63(isPLNat()), isPLNatKind() -> U261(isLNatKind()), isPLNatKind() -> U271(isNaturalKind()), U61(tt()) -> U62(isPLNatKind()), U63(tt()) -> tt(), isPLNat() -> U241(isLNatKind()), isPLNat() -> U251(isNaturalKind()), U72(tt()) -> U73(isNatural()), U71(tt()) -> U72(isNaturalKind()), U73(tt()) -> tt(), U82(tt()) -> U83(isPLNat()), U81(tt()) -> U82(isPLNatKind()), U83(tt()) -> tt(), U92(tt()) -> U93(isLNat()), U91(tt()) -> U92(isLNatKind()), U93(tt()) -> tt(), natsFrom(N) -> U281(isNatural()), sel(N, XS) -> U291(isNatural()), tail(cons(N)) -> U331(isNatural()), take(N, XS) -> U341(isNatural()) } DUP: We consider a duplicating system. Trs: { U102(tt()) -> U103(isLNatKind()), isNaturalKind() -> tt(), isNaturalKind() -> U211(isLNatKind()), isNaturalKind() -> U221(isNaturalKind()), isNaturalKind() -> U231(isNaturalKind()), U101(tt()) -> U102(isNaturalKind()), U103(tt()) -> U104(isLNatKind()), isLNatKind() -> tt(), isLNatKind() -> U111(isNaturalKind()), isLNatKind() -> U121(isNaturalKind()), isLNatKind() -> U131(isPLNatKind()), isLNatKind() -> U141(isNaturalKind()), isLNatKind() -> U151(isPLNatKind()), isLNatKind() -> U161(isLNatKind()), isLNatKind() -> U171(isNaturalKind()), U104(tt()) -> U105(isNatural()), U105(tt()) -> U106(isLNat()), isNatural() -> tt(), isNatural() -> U181(isLNatKind()), isNatural() -> U191(isNaturalKind()), isNatural() -> U201(isNaturalKind()), U106(tt()) -> tt(), isLNat() -> U101(isNaturalKind()), isLNat() -> tt(), isLNat() -> U41(isNaturalKind()), isLNat() -> U51(isNaturalKind()), isLNat() -> U61(isPLNatKind()), isLNat() -> U71(isNaturalKind()), isLNat() -> U81(isPLNatKind()), isLNat() -> U91(isLNatKind()), U12(tt()) -> U13(isLNat()), U11(tt()) -> U12(isNaturalKind()), U112(tt()) -> tt(), U111(tt()) -> U112(isLNatKind()), U13(tt()) -> U14(isLNatKind()), U122(tt()) -> tt(), U121(tt()) -> U122(isLNatKind()), U14(tt()) -> snd(splitAt(N, XS)), U131(tt()) -> tt(), snd(pair(X, Y)) -> U301(isLNat()), splitAt(0(), XS) -> U311(isLNat()), splitAt(s(N), cons(X)) -> U321(isNatural()), U141(tt()) -> tt(), U151(tt()) -> tt(), U161(tt()) -> tt(), U172(tt()) -> tt(), U171(tt()) -> U172(isLNatKind()), U182(tt()) -> U183(isLNat()), U181(tt()) -> U182(isLNatKind()), U183(tt()) -> tt(), U192(tt()) -> U193(isNatural()), U191(tt()) -> U192(isNaturalKind()), U193(tt()) -> tt(), U202(tt()) -> U203(isLNatKind()), U201(tt()) -> U202(isNaturalKind()), U203(tt()) -> U204(isLNatKind()), U204(tt()) -> U205(isNatural()), U205(tt()) -> U206(isLNat()), U206(tt()) -> tt(), U22(tt()) -> U23(isLNat()), U21(tt()) -> U22(isLNatKind()), U211(tt()) -> tt(), U23(tt()) -> U24(isLNatKind()), U221(tt()) -> tt(), U24(tt()) -> X, U232(tt()) -> tt(), U231(tt()) -> U232(isLNatKind()), U242(tt()) -> U243(isLNatKind()), U241(tt()) -> U242(isLNatKind()), U243(tt()) -> U244(isLNatKind()), U244(tt()) -> U245(isLNat()), U245(tt()) -> U246(isLNat()), U246(tt()) -> tt(), U252(tt()) -> U253(isLNatKind()), U251(tt()) -> U252(isNaturalKind()), U253(tt()) -> U254(isLNatKind()), U254(tt()) -> U255(isNatural()), U255(tt()) -> U256(isLNat()), U256(tt()) -> tt(), U262(tt()) -> tt(), U261(tt()) -> U262(isLNatKind()), U272(tt()) -> tt(), U271(tt()) -> U272(isLNatKind()), U282(tt()) -> cons(N), U281(tt()) -> U282(isNaturalKind()), U292(tt()) -> U293(isLNat()), U291(tt()) -> U292(isNaturalKind()), U293(tt()) -> U294(isLNatKind()), U294(tt()) -> head(afterNth(N, XS)), head(cons(N)) -> U31(isNatural()), afterNth(N, XS) -> U11(isNatural()), U302(tt()) -> U303(isLNat()), U301(tt()) -> U302(isLNatKind()), U303(tt()) -> U304(isLNatKind()), U304(tt()) -> Y, U32(tt()) -> U33(isLNat()), U31(tt()) -> U32(isNaturalKind()), U312(tt()) -> pair(nil(), XS), U311(tt()) -> U312(isLNatKind()), U33(tt()) -> U34(isLNatKind()), U322(tt()) -> U323(isNatural()), U321(tt()) -> U322(isNaturalKind()), U323(tt()) -> U324(isNaturalKind()), U324(tt()) -> U325(isLNat()), U325(tt()) -> U326(isLNatKind()), U326(tt()) -> U327(splitAt(N, XS)), U327(pair(YS, ZS)) -> pair(cons(X), ZS), U34(tt()) -> N, U332(tt()) -> U333(isLNat()), U331(tt()) -> U332(isNaturalKind()), U333(tt()) -> U334(isLNatKind()), U334(tt()) -> XS, U342(tt()) -> U343(isLNat()), U341(tt()) -> U342(isNaturalKind()), U343(tt()) -> U344(isLNatKind()), U344(tt()) -> fst(splitAt(N, XS)), fst(pair(X, Y)) -> U21(isLNat()), U42(tt()) -> U43(isLNatKind()), U41(tt()) -> U42(isNaturalKind()), U43(tt()) -> U44(isLNatKind()), U44(tt()) -> U45(isNatural()), U45(tt()) -> U46(isLNat()), U46(tt()) -> tt(), U52(tt()) -> U53(isLNatKind()), U51(tt()) -> U52(isNaturalKind()), U53(tt()) -> U54(isLNatKind()), U54(tt()) -> U55(isNatural()), U55(tt()) -> U56(isLNat()), U56(tt()) -> tt(), U62(tt()) -> U63(isPLNat()), isPLNatKind() -> U261(isLNatKind()), isPLNatKind() -> U271(isNaturalKind()), U61(tt()) -> U62(isPLNatKind()), U63(tt()) -> tt(), isPLNat() -> U241(isLNatKind()), isPLNat() -> U251(isNaturalKind()), U72(tt()) -> U73(isNatural()), U71(tt()) -> U72(isNaturalKind()), U73(tt()) -> tt(), U82(tt()) -> U83(isPLNat()), U81(tt()) -> U82(isPLNatKind()), U83(tt()) -> tt(), U92(tt()) -> U93(isLNat()), U91(tt()) -> U92(isLNatKind()), U93(tt()) -> tt(), natsFrom(N) -> U281(isNatural()), sel(N, XS) -> U291(isNatural()), tail(cons(N)) -> U331(isNatural()), take(N, XS) -> U341(isNatural()) } Fail