(COMMENT generated from Maude module 'LISTUTILITIES' by 'complete-noand' transformation)
(VAR N V1 V2 X XS Y YS ZS Z)
(STRATEGY CONTEXTSENSITIVE

(U101 1)
(U102 1)
(U103 1)
(U104 1)
(U105 1)
(U106 1)
(U11 1)
(U111 1)
(U112 1)
(U12 1)
(U121 1)
(U122 1)
(U13 1)
(U131 1)
(U14 1)
(U141 1)
(U151 1)
(U161 1)
(U171 1)
(U172 1)
(U181 1)
(U182 1)
(U183 1)
(U191 1)
(U192 1)
(U193 1)
(U201 1)
(U202 1)
(U203 1)
(U204 1)
(U205 1)
(U206 1)
(U21 1)
(U211 1)
(U22 1)
(U221 1)
(U23 1)
(U231 1)
(U232 1)
(U24 1)
(U241 1)
(U242 1)
(U243 1)
(U244 1)
(U245 1)
(U246 1)
(U251 1)
(U252 1)
(U253 1)
(U254 1)
(U255 1)
(U256 1)
(U261 1)
(U262 1)
(U271 1)
(U272 1)
(U281 1)
(U282 1)
(U291 1)
(U292 1)
(U293 1)
(U294 1)
(U301 1)
(U302 1)
(U303 1)
(U304 1)
(U31 1)
(U311 1)
(U312 1)
(U32 1)
(U321 1)
(U322 1)
(U323 1)
(U324 1)
(U325 1)
(U326 1)
(U327 1)
(U33 1)
(U331 1)
(U332 1)
(U333 1)
(U334 1)
(U34 1)
(U341 1)
(U342 1)
(U343 1)
(U344 1)
(U41 1)
(U42 1)
(U43 1)
(U44 1)
(U45 1)
(U46 1)
(U51 1)
(U52 1)
(U53 1)
(U54 1)
(U55 1)
(U56 1)
(U61 1)
(U62 1)
(U63 1)
(U71 1)
(U72 1)
(U73 1)
(U81 1)
(U82 1)
(U83 1)
(U91 1)
(U92 1)
(U93 1)

(cons 1)


(isLNat )
(isLNatKind )
(isNatural )
(isNaturalKind )
(isPLNat )
(isPLNatKind )









)
(RULES
U101(tt,V1,V2) -> U102(isNaturalKind(V1),V1,V2)

U102(tt,V1,V2) -> U103(isLNatKind(V2),V1,V2)

U103(tt,V1,V2) -> U104(isLNatKind(V2),V1,V2)

U104(tt,V1,V2) -> U105(isNatural(V1),V2)

U105(tt,V2) -> U106(isLNat(V2))

U106(tt) -> tt

U11(tt,N,XS) -> U12(isNaturalKind(N),N,XS)

U111(tt,V2) -> U112(isLNatKind(V2))

U112(tt) -> tt

U12(tt,N,XS) -> U13(isLNat(XS),N,XS)

U121(tt,V2) -> U122(isLNatKind(V2))

U122(tt) -> tt

U13(tt,N,XS) -> U14(isLNatKind(XS),N,XS)

U131(tt) -> tt

U14(tt,N,XS) -> snd(splitAt(N,XS))

U141(tt) -> tt

U151(tt) -> tt

U161(tt) -> tt

U171(tt,V2) -> U172(isLNatKind(V2))

U172(tt) -> tt

U181(tt,V1) -> U182(isLNatKind(V1),V1)

U182(tt,V1) -> U183(isLNat(V1))

U183(tt) -> tt

U191(tt,V1) -> U192(isNaturalKind(V1),V1)

U192(tt,V1) -> U193(isNatural(V1))

U193(tt) -> tt

U201(tt,V1,V2) -> U202(isNaturalKind(V1),V1,V2)

U202(tt,V1,V2) -> U203(isLNatKind(V2),V1,V2)

U203(tt,V1,V2) -> U204(isLNatKind(V2),V1,V2)

U204(tt,V1,V2) -> U205(isNatural(V1),V2)

U205(tt,V2) -> U206(isLNat(V2))

U206(tt) -> tt

U21(tt,X,Y) -> U22(isLNatKind(X),X,Y)

U211(tt) -> tt

U22(tt,X,Y) -> U23(isLNat(Y),X,Y)

U221(tt) -> tt

U23(tt,X,Y) -> U24(isLNatKind(Y),X)

U231(tt,V2) -> U232(isLNatKind(V2))

U232(tt) -> tt

U24(tt,X) -> X

U241(tt,V1,V2) -> U242(isLNatKind(V1),V1,V2)

U242(tt,V1,V2) -> U243(isLNatKind(V2),V1,V2)

U243(tt,V1,V2) -> U244(isLNatKind(V2),V1,V2)

U244(tt,V1,V2) -> U245(isLNat(V1),V2)

U245(tt,V2) -> U246(isLNat(V2))

U246(tt) -> tt

U251(tt,V1,V2) -> U252(isNaturalKind(V1),V1,V2)

U252(tt,V1,V2) -> U253(isLNatKind(V2),V1,V2)

U253(tt,V1,V2) -> U254(isLNatKind(V2),V1,V2)

U254(tt,V1,V2) -> U255(isNatural(V1),V2)

U255(tt,V2) -> U256(isLNat(V2))

U256(tt) -> tt

U261(tt,V2) -> U262(isLNatKind(V2))

U262(tt) -> tt

U271(tt,V2) -> U272(isLNatKind(V2))

U272(tt) -> tt

U281(tt,N) -> U282(isNaturalKind(N),N)

U282(tt,N) -> cons(N,natsFrom(s(N)))

U291(tt,N,XS) -> U292(isNaturalKind(N),N,XS)

U292(tt,N,XS) -> U293(isLNat(XS),N,XS)

U293(tt,N,XS) -> U294(isLNatKind(XS),N,XS)

U294(tt,N,XS) -> head(afterNth(N,XS))

U301(tt,X,Y) -> U302(isLNatKind(X),Y)

U302(tt,Y) -> U303(isLNat(Y),Y)

U303(tt,Y) -> U304(isLNatKind(Y),Y)

U304(tt,Y) -> Y

U31(tt,N,XS) -> U32(isNaturalKind(N),N,XS)

U311(tt,XS) -> U312(isLNatKind(XS),XS)

U312(tt,XS) -> pair(nil,XS)

U32(tt,N,XS) -> U33(isLNat(XS),N,XS)

U321(tt,N,X,XS) -> U322(isNaturalKind(N),N,X,XS)

U322(tt,N,X,XS) -> U323(isNatural(X),N,X,XS)

U323(tt,N,X,XS) -> U324(isNaturalKind(X),N,X,XS)

U324(tt,N,X,XS) -> U325(isLNat(XS),N,X,XS)

U325(tt,N,X,XS) -> U326(isLNatKind(XS),N,X,XS)

U326(tt,N,X,XS) -> U327(splitAt(N,XS),X)

U327(pair(YS,ZS),X) -> pair(cons(X,YS),ZS)

U33(tt,N,XS) -> U34(isLNatKind(XS),N)

U331(tt,N,XS) -> U332(isNaturalKind(N),XS)

U332(tt,XS) -> U333(isLNat(XS),XS)

U333(tt,XS) -> U334(isLNatKind(XS),XS)

U334(tt,XS) -> XS

U34(tt,N) -> N

U341(tt,N,XS) -> U342(isNaturalKind(N),N,XS)

U342(tt,N,XS) -> U343(isLNat(XS),N,XS)

U343(tt,N,XS) -> U344(isLNatKind(XS),N,XS)

U344(tt,N,XS) -> fst(splitAt(N,XS))

U41(tt,V1,V2) -> U42(isNaturalKind(V1),V1,V2)

U42(tt,V1,V2) -> U43(isLNatKind(V2),V1,V2)

U43(tt,V1,V2) -> U44(isLNatKind(V2),V1,V2)

U44(tt,V1,V2) -> U45(isNatural(V1),V2)

U45(tt,V2) -> U46(isLNat(V2))

U46(tt) -> tt

U51(tt,V1,V2) -> U52(isNaturalKind(V1),V1,V2)

U52(tt,V1,V2) -> U53(isLNatKind(V2),V1,V2)

U53(tt,V1,V2) -> U54(isLNatKind(V2),V1,V2)

U54(tt,V1,V2) -> U55(isNatural(V1),V2)

U55(tt,V2) -> U56(isLNat(V2))

U56(tt) -> tt

U61(tt,V1) -> U62(isPLNatKind(V1),V1)

U62(tt,V1) -> U63(isPLNat(V1))

U63(tt) -> tt

U71(tt,V1) -> U72(isNaturalKind(V1),V1)

U72(tt,V1) -> U73(isNatural(V1))

U73(tt) -> tt

U81(tt,V1) -> U82(isPLNatKind(V1),V1)

U82(tt,V1) -> U83(isPLNat(V1))

U83(tt) -> tt

U91(tt,V1) -> U92(isLNatKind(V1),V1)

U92(tt,V1) -> U93(isLNat(V1))

U93(tt) -> tt

afterNth(N,XS) -> U11(isNatural(N),N,XS)

fst(pair(X,Y)) -> U21(isLNat(X),X,Y)

head(cons(N,XS)) -> U31(isNatural(N),N,XS)

isLNat(nil) -> tt

isLNat(afterNth(V1,V2)) -> U41(isNaturalKind(V1),V1,V2)

isLNat(cons(V1,V2)) -> U51(isNaturalKind(V1),V1,V2)

isLNat(fst(V1)) -> U61(isPLNatKind(V1),V1)

isLNat(natsFrom(V1)) -> U71(isNaturalKind(V1),V1)

isLNat(snd(V1)) -> U81(isPLNatKind(V1),V1)

isLNat(tail(V1)) -> U91(isLNatKind(V1),V1)

isLNat(take(V1,V2)) -> U101(isNaturalKind(V1),V1,V2)

isLNatKind(nil) -> tt

isLNatKind(afterNth(V1,V2)) -> U111(isNaturalKind(V1),V2)

isLNatKind(cons(V1,V2)) -> U121(isNaturalKind(V1),V2)

isLNatKind(fst(V1)) -> U131(isPLNatKind(V1))

isLNatKind(natsFrom(V1)) -> U141(isNaturalKind(V1))

isLNatKind(snd(V1)) -> U151(isPLNatKind(V1))

isLNatKind(tail(V1)) -> U161(isLNatKind(V1))

isLNatKind(take(V1,V2)) -> U171(isNaturalKind(V1),V2)

isNatural(0) -> tt

isNatural(head(V1)) -> U181(isLNatKind(V1),V1)

isNatural(s(V1)) -> U191(isNaturalKind(V1),V1)

isNatural(sel(V1,V2)) -> U201(isNaturalKind(V1),V1,V2)

isNaturalKind(0) -> tt

isNaturalKind(head(V1)) -> U211(isLNatKind(V1))

isNaturalKind(s(V1)) -> U221(isNaturalKind(V1))

isNaturalKind(sel(V1,V2)) -> U231(isNaturalKind(V1),V2)

isPLNat(pair(V1,V2)) -> U241(isLNatKind(V1),V1,V2)

isPLNat(splitAt(V1,V2)) -> U251(isNaturalKind(V1),V1,V2)

isPLNatKind(pair(V1,V2)) -> U261(isLNatKind(V1),V2)

isPLNatKind(splitAt(V1,V2)) -> U271(isNaturalKind(V1),V2)

natsFrom(N) -> U281(isNatural(N),N)

sel(N,XS) -> U291(isNatural(N),N,XS)

snd(pair(X,Y)) -> U301(isLNat(X),X,Y)

splitAt(0,XS) -> U311(isLNat(XS),XS)

splitAt(s(N),cons(X,XS)) -> U321(isNatural(N),N,X,XS)

tail(cons(N,XS)) -> U331(isNatural(N),N,XS)

take(N,XS) -> U341(isNatural(N),N,XS)
)