(0) Obligation:
Generalized rewrite system (where rules with free variables on rhs are allowed):
The TRS R consists of the following rules:
U14(tt) → snd(splitAt(N, XS))
U24(tt) → X
U282(tt) → cons(N)
U294(tt) → head(afterNth(N, XS))
U304(tt) → Y
U312(tt) → pair(nil, XS)
U326(tt) → U327(splitAt(N, XS))
U327(pair(YS, ZS)) → pair(cons(X), ZS)
U334(tt) → XS
U34(tt) → N
U344(tt) → fst(splitAt(N, XS))
U101(tt) → U102(isNaturalKind)
U102(tt) → U103(isLNatKind)
U103(tt) → U104(isLNatKind)
U104(tt) → U105(isNatural)
U105(tt) → U106(isLNat)
U106(tt) → tt
U11(tt) → U12(isNaturalKind)
U111(tt) → U112(isLNatKind)
U112(tt) → tt
U12(tt) → U13(isLNat)
U121(tt) → U122(isLNatKind)
U122(tt) → tt
U13(tt) → U14(isLNatKind)
U131(tt) → tt
U141(tt) → tt
U151(tt) → tt
U161(tt) → tt
U171(tt) → U172(isLNatKind)
U172(tt) → tt
U181(tt) → U182(isLNatKind)
U182(tt) → U183(isLNat)
U183(tt) → tt
U191(tt) → U192(isNaturalKind)
U192(tt) → U193(isNatural)
U193(tt) → tt
U201(tt) → U202(isNaturalKind)
U202(tt) → U203(isLNatKind)
U203(tt) → U204(isLNatKind)
U204(tt) → U205(isNatural)
U205(tt) → U206(isLNat)
U206(tt) → tt
U21(tt) → U22(isLNatKind)
U211(tt) → tt
U22(tt) → U23(isLNat)
U221(tt) → tt
U23(tt) → U24(isLNatKind)
U231(tt) → U232(isLNatKind)
U232(tt) → tt
U241(tt) → U242(isLNatKind)
U242(tt) → U243(isLNatKind)
U243(tt) → U244(isLNatKind)
U244(tt) → U245(isLNat)
U245(tt) → U246(isLNat)
U246(tt) → tt
U251(tt) → U252(isNaturalKind)
U252(tt) → U253(isLNatKind)
U253(tt) → U254(isLNatKind)
U254(tt) → U255(isNatural)
U255(tt) → U256(isLNat)
U256(tt) → tt
U261(tt) → U262(isLNatKind)
U262(tt) → tt
U271(tt) → U272(isLNatKind)
U272(tt) → tt
U281(tt) → U282(isNaturalKind)
U291(tt) → U292(isNaturalKind)
U292(tt) → U293(isLNat)
U293(tt) → U294(isLNatKind)
U301(tt) → U302(isLNatKind)
U302(tt) → U303(isLNat)
U303(tt) → U304(isLNatKind)
U31(tt) → U32(isNaturalKind)
U311(tt) → U312(isLNatKind)
U32(tt) → U33(isLNat)
U321(tt) → U322(isNaturalKind)
U322(tt) → U323(isNatural)
U323(tt) → U324(isNaturalKind)
U324(tt) → U325(isLNat)
U325(tt) → U326(isLNatKind)
U33(tt) → U34(isLNatKind)
U331(tt) → U332(isNaturalKind)
U332(tt) → U333(isLNat)
U333(tt) → U334(isLNatKind)
U341(tt) → U342(isNaturalKind)
U342(tt) → U343(isLNat)
U343(tt) → U344(isLNatKind)
U41(tt) → U42(isNaturalKind)
U42(tt) → U43(isLNatKind)
U43(tt) → U44(isLNatKind)
U44(tt) → U45(isNatural)
U45(tt) → U46(isLNat)
U46(tt) → tt
U51(tt) → U52(isNaturalKind)
U52(tt) → U53(isLNatKind)
U53(tt) → U54(isLNatKind)
U54(tt) → U55(isNatural)
U55(tt) → U56(isLNat)
U56(tt) → tt
U61(tt) → U62(isPLNatKind)
U62(tt) → U63(isPLNat)
U63(tt) → tt
U71(tt) → U72(isNaturalKind)
U72(tt) → U73(isNatural)
U73(tt) → tt
U81(tt) → U82(isPLNatKind)
U82(tt) → U83(isPLNat)
U83(tt) → tt
U91(tt) → U92(isLNatKind)
U92(tt) → U93(isLNat)
U93(tt) → tt
afterNth(N, XS) → U11(isNatural)
fst(pair(X, Y)) → U21(isLNat)
head(cons(N)) → U31(isNatural)
isLNat → tt
isLNat → U41(isNaturalKind)
isLNat → U51(isNaturalKind)
isLNat → U61(isPLNatKind)
isLNat → U71(isNaturalKind)
isLNat → U81(isPLNatKind)
isLNat → U91(isLNatKind)
isLNat → U101(isNaturalKind)
isLNatKind → tt
isLNatKind → U111(isNaturalKind)
isLNatKind → U121(isNaturalKind)
isLNatKind → U131(isPLNatKind)
isLNatKind → U141(isNaturalKind)
isLNatKind → U151(isPLNatKind)
isLNatKind → U161(isLNatKind)
isLNatKind → U171(isNaturalKind)
isNatural → tt
isNatural → U181(isLNatKind)
isNatural → U191(isNaturalKind)
isNatural → U201(isNaturalKind)
isNaturalKind → tt
isNaturalKind → U211(isLNatKind)
isNaturalKind → U221(isNaturalKind)
isNaturalKind → U231(isNaturalKind)
isPLNat → U241(isLNatKind)
isPLNat → U251(isNaturalKind)
isPLNatKind → U261(isLNatKind)
isPLNatKind → U271(isNaturalKind)
natsFrom(N) → U281(isNatural)
sel(N, XS) → U291(isNatural)
snd(pair(X, Y)) → U301(isLNat)
splitAt(0, XS) → U311(isLNat)
splitAt(s(N), cons(X)) → U321(isNatural)
tail(cons(N)) → U331(isNatural)
take(N, XS) → U341(isNatural)
(1) CritRuleProof (EQUIVALENT transformation)
The rule U14(tt) → snd(splitAt(N, XS)) contains free variables in its right-hand side. Hence the TRS is not-terminating.
(2) NO