(VAR N XS X Y YS ZS)
(RULES 
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
U14(tt) -> snd(splitAt(N,XS))
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
U24(tt) -> X
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)
U282(tt) -> cons(N)
U291(tt) -> U292(isNaturalKind)
U292(tt) -> U293(isLNat)
U293(tt) -> U294(isLNatKind)
U294(tt) -> head(afterNth(N,XS))
U301(tt) -> U302(isLNatKind)
U302(tt) -> U303(isLNat)
U303(tt) -> U304(isLNatKind)
U304(tt) -> Y
U31(tt) -> U32(isNaturalKind)
U311(tt) -> U312(isLNatKind)
U312(tt) -> pair(nil,XS)
U32(tt) -> U33(isLNat)
U321(tt) -> U322(isNaturalKind)
U322(tt) -> U323(isNatural)
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)
U33(tt) -> U34(isLNatKind)
U331(tt) -> U332(isNaturalKind)
U332(tt) -> U333(isLNat)
U333(tt) -> U334(isLNatKind)
U334(tt) -> XS
U34(tt) -> N
U341(tt) -> U342(isNaturalKind)
U342(tt) -> U343(isLNat)
U343(tt) -> U344(isLNatKind)
U344(tt) -> fst(splitAt(N,XS))
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)
)