Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following 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)

The replacement map contains the following entries:

U101: {1}
tt: empty set
U102: {1}
isNaturalKind: empty set
U103: {1}
isLNatKind: empty set
U104: {1}
U105: {1}
isNatural: empty set
U106: {1}
isLNat: empty set
U11: {1}
U12: {1}
U111: {1}
U112: {1}
U13: {1}
U121: {1}
U122: {1}
U14: {1}
U131: {1}
snd: {1}
splitAt: {1, 2}
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}
U22: {1}
U211: {1}
U23: {1}
U221: {1}
U24: {1}
U231: {1}
U232: {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}
cons: {1}
natsFrom: {1}
s: {1}
U291: {1}
U292: {1}
U293: {1}
U294: {1}
head: {1}
afterNth: {1, 2}
U301: {1}
U302: {1}
U303: {1}
U304: {1}
U31: {1}
U32: {1}
U311: {1}
U312: {1}
pair: {1, 2}
nil: empty set
U33: {1}
U321: {1}
U322: {1}
U323: {1}
U324: {1}
U325: {1}
U326: {1}
U327: {1}
U34: {1}
U331: {1}
U332: {1}
U333: {1}
U334: {1}
U341: {1}
U342: {1}
U343: {1}
U344: {1}
fst: {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}
isPLNatKind: empty set
U63: {1}
isPLNat: empty set
U71: {1}
U72: {1}
U73: {1}
U81: {1}
U82: {1}
U83: {1}
U91: {1}
U92: {1}
U93: {1}
tail: {1}
take: {1, 2}
0: empty set
sel: {1, 2}


↳ CSR
  ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following 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)

The replacement map contains the following entries:

U101: {1}
tt: empty set
U102: {1}
isNaturalKind: empty set
U103: {1}
isLNatKind: empty set
U104: {1}
U105: {1}
isNatural: empty set
U106: {1}
isLNat: empty set
U11: {1}
U12: {1}
U111: {1}
U112: {1}
U13: {1}
U121: {1}
U122: {1}
U14: {1}
U131: {1}
snd: {1}
splitAt: {1, 2}
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}
U22: {1}
U211: {1}
U23: {1}
U221: {1}
U24: {1}
U231: {1}
U232: {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}
cons: {1}
natsFrom: {1}
s: {1}
U291: {1}
U292: {1}
U293: {1}
U294: {1}
head: {1}
afterNth: {1, 2}
U301: {1}
U302: {1}
U303: {1}
U304: {1}
U31: {1}
U32: {1}
U311: {1}
U312: {1}
pair: {1, 2}
nil: empty set
U33: {1}
U321: {1}
U322: {1}
U323: {1}
U324: {1}
U325: {1}
U326: {1}
U327: {1}
U34: {1}
U331: {1}
U332: {1}
U333: {1}
U334: {1}
U341: {1}
U342: {1}
U343: {1}
U344: {1}
fst: {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}
isPLNatKind: empty set
U63: {1}
isPLNat: empty set
U71: {1}
U72: {1}
U73: {1}
U81: {1}
U82: {1}
U83: {1}
U91: {1}
U92: {1}
U93: {1}
tail: {1}
take: {1, 2}
0: empty set
sel: {1, 2}

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U106, U112, U122, U131, snd, splitAt, U141, U151, U161, U172, U183, U193, U206, U211, U221, U232, U246, U256, U262, U272, natsFrom, s, head, afterNth, pair, fst, U46, U56, U63, U73, U83, U93, tail, take, sel, U1061, U1121, U1221, SND, SPLITAT, U1721, U1831, U1931, U2061, U2321, U2461, U2561, U2621, U2721, HEAD, AFTERNTH, FST, U461, U561, U631, U731, U831, U931, U1311, U1411, U1511, U1611, U2111, U2211, NATSFROM, SEL, TAIL, TAKE} are replacing on all positions.
For all symbols f in {U101, U102, U103, U104, U105, U11, U12, U111, U13, U121, U14, U171, U181, U182, U191, U192, U201, U202, U203, U204, U205, U21, U22, U23, U24, U231, U241, U242, U243, U244, U245, U251, U252, U253, U254, U255, U261, U271, U281, U282, cons, U291, U292, U293, U294, U301, U302, U303, U304, U31, U32, U311, U312, U33, U321, U322, U323, U324, U325, U326, U327, U34, U331, U332, U333, U334, U341, U342, U343, U344, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U81, U82, U91, U92, U1021, U1011, U1031, U1041, U1051, U121, U111, U1111, U131, U1211, U141, U1711, U1821, U1811, U1921, U1911, U2021, U2011, U2031, U2041, U2051, U221, U211, U231, U241, U2311, U2421, U2411, U2431, U2441, U2451, U2521, U2511, U2531, U2541, U2551, U2611, U2711, U2821, U2811, U2921, U2911, U2931, U2941, U3021, U3011, U3031, U3041, U321, U311, U3121, U3111, U331, U3221, U3211, U3231, U3241, U3251, U3261, U3271, U341, U3321, U3311, U3331, U3341, U3421, U3411, U3431, U3441, U421, U411, U431, U441, U451, U521, U511, U531, U541, U551, U621, U611, U721, U711, U821, U811, U921, U911} we have µ(f) = {1}.
The symbols in {isNaturalKind, isLNatKind, isNatural, isLNat, isPLNatKind, isPLNat, ISNATURALKIND, ISLNATKIND, ISNATURAL, ISLNAT, ISPLNATKIND, ISPLNAT, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

U1011(tt, V1, V2) → U1021(isNaturalKind(V1), V1, V2)
U1011(tt, V1, V2) → ISNATURALKIND(V1)
U1021(tt, V1, V2) → U1031(isLNatKind(V2), V1, V2)
U1021(tt, V1, V2) → ISLNATKIND(V2)
U1031(tt, V1, V2) → U1041(isLNatKind(V2), V1, V2)
U1031(tt, V1, V2) → ISLNATKIND(V2)
U1041(tt, V1, V2) → U1051(isNatural(V1), V2)
U1041(tt, V1, V2) → ISNATURAL(V1)
U1051(tt, V2) → U1061(isLNat(V2))
U1051(tt, V2) → ISLNAT(V2)
U111(tt, N, XS) → U121(isNaturalKind(N), N, XS)
U111(tt, N, XS) → ISNATURALKIND(N)
U1111(tt, V2) → U1121(isLNatKind(V2))
U1111(tt, V2) → ISLNATKIND(V2)
U121(tt, N, XS) → U131(isLNat(XS), N, XS)
U121(tt, N, XS) → ISLNAT(XS)
U1211(tt, V2) → U1221(isLNatKind(V2))
U1211(tt, V2) → ISLNATKIND(V2)
U131(tt, N, XS) → U141(isLNatKind(XS), N, XS)
U131(tt, N, XS) → ISLNATKIND(XS)
U141(tt, N, XS) → SND(splitAt(N, XS))
U141(tt, N, XS) → SPLITAT(N, XS)
U1711(tt, V2) → U1721(isLNatKind(V2))
U1711(tt, V2) → ISLNATKIND(V2)
U1811(tt, V1) → U1821(isLNatKind(V1), V1)
U1811(tt, V1) → ISLNATKIND(V1)
U1821(tt, V1) → U1831(isLNat(V1))
U1821(tt, V1) → ISLNAT(V1)
U1911(tt, V1) → U1921(isNaturalKind(V1), V1)
U1911(tt, V1) → ISNATURALKIND(V1)
U1921(tt, V1) → U1931(isNatural(V1))
U1921(tt, V1) → ISNATURAL(V1)
U2011(tt, V1, V2) → U2021(isNaturalKind(V1), V1, V2)
U2011(tt, V1, V2) → ISNATURALKIND(V1)
U2021(tt, V1, V2) → U2031(isLNatKind(V2), V1, V2)
U2021(tt, V1, V2) → ISLNATKIND(V2)
U2031(tt, V1, V2) → U2041(isLNatKind(V2), V1, V2)
U2031(tt, V1, V2) → ISLNATKIND(V2)
U2041(tt, V1, V2) → U2051(isNatural(V1), V2)
U2041(tt, V1, V2) → ISNATURAL(V1)
U2051(tt, V2) → U2061(isLNat(V2))
U2051(tt, V2) → ISLNAT(V2)
U211(tt, X, Y) → U221(isLNatKind(X), X, Y)
U211(tt, X, Y) → ISLNATKIND(X)
U221(tt, X, Y) → U231(isLNat(Y), X, Y)
U221(tt, X, Y) → ISLNAT(Y)
U231(tt, X, Y) → U241(isLNatKind(Y), X)
U231(tt, X, Y) → ISLNATKIND(Y)
U2311(tt, V2) → U2321(isLNatKind(V2))
U2311(tt, V2) → ISLNATKIND(V2)
U2411(tt, V1, V2) → U2421(isLNatKind(V1), V1, V2)
U2411(tt, V1, V2) → ISLNATKIND(V1)
U2421(tt, V1, V2) → U2431(isLNatKind(V2), V1, V2)
U2421(tt, V1, V2) → ISLNATKIND(V2)
U2431(tt, V1, V2) → U2441(isLNatKind(V2), V1, V2)
U2431(tt, V1, V2) → ISLNATKIND(V2)
U2441(tt, V1, V2) → U2451(isLNat(V1), V2)
U2441(tt, V1, V2) → ISLNAT(V1)
U2451(tt, V2) → U2461(isLNat(V2))
U2451(tt, V2) → ISLNAT(V2)
U2511(tt, V1, V2) → U2521(isNaturalKind(V1), V1, V2)
U2511(tt, V1, V2) → ISNATURALKIND(V1)
U2521(tt, V1, V2) → U2531(isLNatKind(V2), V1, V2)
U2521(tt, V1, V2) → ISLNATKIND(V2)
U2531(tt, V1, V2) → U2541(isLNatKind(V2), V1, V2)
U2531(tt, V1, V2) → ISLNATKIND(V2)
U2541(tt, V1, V2) → U2551(isNatural(V1), V2)
U2541(tt, V1, V2) → ISNATURAL(V1)
U2551(tt, V2) → U2561(isLNat(V2))
U2551(tt, V2) → ISLNAT(V2)
U2611(tt, V2) → U2621(isLNatKind(V2))
U2611(tt, V2) → ISLNATKIND(V2)
U2711(tt, V2) → U2721(isLNatKind(V2))
U2711(tt, V2) → ISLNATKIND(V2)
U2811(tt, N) → U2821(isNaturalKind(N), N)
U2811(tt, N) → ISNATURALKIND(N)
U2911(tt, N, XS) → U2921(isNaturalKind(N), N, XS)
U2911(tt, N, XS) → ISNATURALKIND(N)
U2921(tt, N, XS) → U2931(isLNat(XS), N, XS)
U2921(tt, N, XS) → ISLNAT(XS)
U2931(tt, N, XS) → U2941(isLNatKind(XS), N, XS)
U2931(tt, N, XS) → ISLNATKIND(XS)
U2941(tt, N, XS) → HEAD(afterNth(N, XS))
U2941(tt, N, XS) → AFTERNTH(N, XS)
U3011(tt, X, Y) → U3021(isLNatKind(X), Y)
U3011(tt, X, Y) → ISLNATKIND(X)
U3021(tt, Y) → U3031(isLNat(Y), Y)
U3021(tt, Y) → ISLNAT(Y)
U3031(tt, Y) → U3041(isLNatKind(Y), Y)
U3031(tt, Y) → ISLNATKIND(Y)
U311(tt, N, XS) → U321(isNaturalKind(N), N, XS)
U311(tt, N, XS) → ISNATURALKIND(N)
U3111(tt, XS) → U3121(isLNatKind(XS), XS)
U3111(tt, XS) → ISLNATKIND(XS)
U321(tt, N, XS) → U331(isLNat(XS), N, XS)
U321(tt, N, XS) → ISLNAT(XS)
U3211(tt, N, X, XS) → U3221(isNaturalKind(N), N, X, XS)
U3211(tt, N, X, XS) → ISNATURALKIND(N)
U3221(tt, N, X, XS) → U3231(isNatural(X), N, X, XS)
U3221(tt, N, X, XS) → ISNATURAL(X)
U3231(tt, N, X, XS) → U3241(isNaturalKind(X), N, X, XS)
U3231(tt, N, X, XS) → ISNATURALKIND(X)
U3241(tt, N, X, XS) → U3251(isLNat(XS), N, X, XS)
U3241(tt, N, X, XS) → ISLNAT(XS)
U3251(tt, N, X, XS) → U3261(isLNatKind(XS), N, X, XS)
U3251(tt, N, X, XS) → ISLNATKIND(XS)
U3261(tt, N, X, XS) → U3271(splitAt(N, XS), X)
U3261(tt, N, X, XS) → SPLITAT(N, XS)
U331(tt, N, XS) → U341(isLNatKind(XS), N)
U331(tt, N, XS) → ISLNATKIND(XS)
U3311(tt, N, XS) → U3321(isNaturalKind(N), XS)
U3311(tt, N, XS) → ISNATURALKIND(N)
U3321(tt, XS) → U3331(isLNat(XS), XS)
U3321(tt, XS) → ISLNAT(XS)
U3331(tt, XS) → U3341(isLNatKind(XS), XS)
U3331(tt, XS) → ISLNATKIND(XS)
U3411(tt, N, XS) → U3421(isNaturalKind(N), N, XS)
U3411(tt, N, XS) → ISNATURALKIND(N)
U3421(tt, N, XS) → U3431(isLNat(XS), N, XS)
U3421(tt, N, XS) → ISLNAT(XS)
U3431(tt, N, XS) → U3441(isLNatKind(XS), N, XS)
U3431(tt, N, XS) → ISLNATKIND(XS)
U3441(tt, N, XS) → FST(splitAt(N, XS))
U3441(tt, N, XS) → SPLITAT(N, XS)
U411(tt, V1, V2) → U421(isNaturalKind(V1), V1, V2)
U411(tt, V1, V2) → ISNATURALKIND(V1)
U421(tt, V1, V2) → U431(isLNatKind(V2), V1, V2)
U421(tt, V1, V2) → ISLNATKIND(V2)
U431(tt, V1, V2) → U441(isLNatKind(V2), V1, V2)
U431(tt, V1, V2) → ISLNATKIND(V2)
U441(tt, V1, V2) → U451(isNatural(V1), V2)
U441(tt, V1, V2) → ISNATURAL(V1)
U451(tt, V2) → U461(isLNat(V2))
U451(tt, V2) → ISLNAT(V2)
U511(tt, V1, V2) → U521(isNaturalKind(V1), V1, V2)
U511(tt, V1, V2) → ISNATURALKIND(V1)
U521(tt, V1, V2) → U531(isLNatKind(V2), V1, V2)
U521(tt, V1, V2) → ISLNATKIND(V2)
U531(tt, V1, V2) → U541(isLNatKind(V2), V1, V2)
U531(tt, V1, V2) → ISLNATKIND(V2)
U541(tt, V1, V2) → U551(isNatural(V1), V2)
U541(tt, V1, V2) → ISNATURAL(V1)
U551(tt, V2) → U561(isLNat(V2))
U551(tt, V2) → ISLNAT(V2)
U611(tt, V1) → U621(isPLNatKind(V1), V1)
U611(tt, V1) → ISPLNATKIND(V1)
U621(tt, V1) → U631(isPLNat(V1))
U621(tt, V1) → ISPLNAT(V1)
U711(tt, V1) → U721(isNaturalKind(V1), V1)
U711(tt, V1) → ISNATURALKIND(V1)
U721(tt, V1) → U731(isNatural(V1))
U721(tt, V1) → ISNATURAL(V1)
U811(tt, V1) → U821(isPLNatKind(V1), V1)
U811(tt, V1) → ISPLNATKIND(V1)
U821(tt, V1) → U831(isPLNat(V1))
U821(tt, V1) → ISPLNAT(V1)
U911(tt, V1) → U921(isLNatKind(V1), V1)
U911(tt, V1) → ISLNATKIND(V1)
U921(tt, V1) → U931(isLNat(V1))
U921(tt, V1) → ISLNAT(V1)
AFTERNTH(N, XS) → U111(isNatural(N), N, XS)
AFTERNTH(N, XS) → ISNATURAL(N)
FST(pair(X, Y)) → U211(isLNat(X), X, Y)
FST(pair(X, Y)) → ISLNAT(X)
HEAD(cons(N, XS)) → U311(isNatural(N), N, XS)
HEAD(cons(N, XS)) → ISNATURAL(N)
ISLNAT(afterNth(V1, V2)) → U411(isNaturalKind(V1), V1, V2)
ISLNAT(afterNth(V1, V2)) → ISNATURALKIND(V1)
ISLNAT(cons(V1, V2)) → U511(isNaturalKind(V1), V1, V2)
ISLNAT(cons(V1, V2)) → ISNATURALKIND(V1)
ISLNAT(fst(V1)) → U611(isPLNatKind(V1), V1)
ISLNAT(fst(V1)) → ISPLNATKIND(V1)
ISLNAT(natsFrom(V1)) → U711(isNaturalKind(V1), V1)
ISLNAT(natsFrom(V1)) → ISNATURALKIND(V1)
ISLNAT(snd(V1)) → U811(isPLNatKind(V1), V1)
ISLNAT(snd(V1)) → ISPLNATKIND(V1)
ISLNAT(tail(V1)) → U911(isLNatKind(V1), V1)
ISLNAT(tail(V1)) → ISLNATKIND(V1)
ISLNAT(take(V1, V2)) → U1011(isNaturalKind(V1), V1, V2)
ISLNAT(take(V1, V2)) → ISNATURALKIND(V1)
ISLNATKIND(afterNth(V1, V2)) → U1111(isNaturalKind(V1), V2)
ISLNATKIND(afterNth(V1, V2)) → ISNATURALKIND(V1)
ISLNATKIND(cons(V1, V2)) → U1211(isNaturalKind(V1), V2)
ISLNATKIND(cons(V1, V2)) → ISNATURALKIND(V1)
ISLNATKIND(fst(V1)) → U1311(isPLNatKind(V1))
ISLNATKIND(fst(V1)) → ISPLNATKIND(V1)
ISLNATKIND(natsFrom(V1)) → U1411(isNaturalKind(V1))
ISLNATKIND(natsFrom(V1)) → ISNATURALKIND(V1)
ISLNATKIND(snd(V1)) → U1511(isPLNatKind(V1))
ISLNATKIND(snd(V1)) → ISPLNATKIND(V1)
ISLNATKIND(tail(V1)) → U1611(isLNatKind(V1))
ISLNATKIND(tail(V1)) → ISLNATKIND(V1)
ISLNATKIND(take(V1, V2)) → U1711(isNaturalKind(V1), V2)
ISLNATKIND(take(V1, V2)) → ISNATURALKIND(V1)
ISNATURAL(head(V1)) → U1811(isLNatKind(V1), V1)
ISNATURAL(head(V1)) → ISLNATKIND(V1)
ISNATURAL(s(V1)) → U1911(isNaturalKind(V1), V1)
ISNATURAL(s(V1)) → ISNATURALKIND(V1)
ISNATURAL(sel(V1, V2)) → U2011(isNaturalKind(V1), V1, V2)
ISNATURAL(sel(V1, V2)) → ISNATURALKIND(V1)
ISNATURALKIND(head(V1)) → U2111(isLNatKind(V1))
ISNATURALKIND(head(V1)) → ISLNATKIND(V1)
ISNATURALKIND(s(V1)) → U2211(isNaturalKind(V1))
ISNATURALKIND(s(V1)) → ISNATURALKIND(V1)
ISNATURALKIND(sel(V1, V2)) → U2311(isNaturalKind(V1), V2)
ISNATURALKIND(sel(V1, V2)) → ISNATURALKIND(V1)
ISPLNAT(pair(V1, V2)) → U2411(isLNatKind(V1), V1, V2)
ISPLNAT(pair(V1, V2)) → ISLNATKIND(V1)
ISPLNAT(splitAt(V1, V2)) → U2511(isNaturalKind(V1), V1, V2)
ISPLNAT(splitAt(V1, V2)) → ISNATURALKIND(V1)
ISPLNATKIND(pair(V1, V2)) → U2611(isLNatKind(V1), V2)
ISPLNATKIND(pair(V1, V2)) → ISLNATKIND(V1)
ISPLNATKIND(splitAt(V1, V2)) → U2711(isNaturalKind(V1), V2)
ISPLNATKIND(splitAt(V1, V2)) → ISNATURALKIND(V1)
NATSFROM(N) → U2811(isNatural(N), N)
NATSFROM(N) → ISNATURAL(N)
SEL(N, XS) → U2911(isNatural(N), N, XS)
SEL(N, XS) → ISNATURAL(N)
SND(pair(X, Y)) → U3011(isLNat(X), X, Y)
SND(pair(X, Y)) → ISLNAT(X)
SPLITAT(0, XS) → U3111(isLNat(XS), XS)
SPLITAT(0, XS) → ISLNAT(XS)
SPLITAT(s(N), cons(X, XS)) → U3211(isNatural(N), N, X, XS)
SPLITAT(s(N), cons(X, XS)) → ISNATURAL(N)
TAIL(cons(N, XS)) → U3311(isNatural(N), N, XS)
TAIL(cons(N, XS)) → ISNATURAL(N)
TAKE(N, XS) → U3411(isNatural(N), N, XS)
TAKE(N, XS) → ISNATURAL(N)

The collapsing dependency pairs are DPc:

U141(tt, N, XS) → N
U141(tt, N, XS) → XS
U241(tt, X) → X
U2821(tt, N) → N
U2941(tt, N, XS) → N
U2941(tt, N, XS) → XS
U3041(tt, Y) → Y
U3121(tt, XS) → XS
U3261(tt, N, X, XS) → N
U3261(tt, N, X, XS) → XS
U3271(pair(YS, ZS), X) → X
U3341(tt, XS) → XS
U341(tt, N) → N
U3441(tt, N, XS) → N
U3441(tt, N, XS) → XS


The hidden terms of R are:

natsFrom(s(N))

Every hiding context is built from:

s on positions {1}
natsFrom on positions {1}

Hence, the new unhiding pairs DPu are :

U141(tt, N, XS) → U(N)
U141(tt, N, XS) → U(XS)
U241(tt, X) → U(X)
U2821(tt, N) → U(N)
U2941(tt, N, XS) → U(N)
U2941(tt, N, XS) → U(XS)
U3041(tt, Y) → U(Y)
U3121(tt, XS) → U(XS)
U3261(tt, N, X, XS) → U(N)
U3261(tt, N, X, XS) → U(XS)
U3271(pair(YS, ZS), X) → U(X)
U3341(tt, XS) → U(XS)
U341(tt, N) → U(N)
U3441(tt, N, XS) → U(N)
U3441(tt, N, XS) → U(XS)
U(s(x_0)) → U(x_0)
U(natsFrom(x_0)) → U(x_0)
U(natsFrom(s(N))) → NATSFROM(s(N))

The TRS R consists of the following 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)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 4 SCCs with 149 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U106, U112, U122, U131, snd, splitAt, U141, U151, U161, U172, U183, U193, U206, U211, U221, U232, U246, U256, U262, U272, natsFrom, s, head, afterNth, pair, fst, U46, U56, U63, U73, U83, U93, tail, take, sel} are replacing on all positions.
For all symbols f in {U101, U102, U103, U104, U105, U11, U12, U111, U13, U121, U14, U171, U181, U182, U191, U192, U201, U202, U203, U204, U205, U21, U22, U23, U24, U231, U241, U242, U243, U244, U245, U251, U252, U253, U254, U255, U261, U271, U281, U282, cons, U291, U292, U293, U294, U301, U302, U303, U304, U31, U32, U311, U312, U33, U321, U322, U323, U324, U325, U326, U327, U34, U331, U332, U333, U334, U341, U342, U343, U344, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U81, U82, U91, U92, U1111, U2311, U1211, U2611, U1711, U2711} we have µ(f) = {1}.
The symbols in {isNaturalKind, isLNatKind, isNatural, isLNat, isPLNatKind, isPLNat, ISLNATKIND, ISNATURALKIND, ISPLNATKIND} are not replacing on any position.

The TRS P consists of the following rules:

ISNATURALKIND(head(V1)) → ISLNATKIND(V1)
ISLNATKIND(afterNth(V1, V2)) → U1111(isNaturalKind(V1), V2)
U1111(tt, V2) → ISLNATKIND(V2)
ISLNATKIND(afterNth(V1, V2)) → ISNATURALKIND(V1)
ISNATURALKIND(s(V1)) → ISNATURALKIND(V1)
ISNATURALKIND(sel(V1, V2)) → U2311(isNaturalKind(V1), V2)
U2311(tt, V2) → ISLNATKIND(V2)
ISLNATKIND(cons(V1, V2)) → U1211(isNaturalKind(V1), V2)
U1211(tt, V2) → ISLNATKIND(V2)
ISLNATKIND(cons(V1, V2)) → ISNATURALKIND(V1)
ISNATURALKIND(sel(V1, V2)) → ISNATURALKIND(V1)
ISLNATKIND(fst(V1)) → ISPLNATKIND(V1)
ISPLNATKIND(pair(V1, V2)) → U2611(isLNatKind(V1), V2)
U2611(tt, V2) → ISLNATKIND(V2)
ISLNATKIND(natsFrom(V1)) → ISNATURALKIND(V1)
ISLNATKIND(snd(V1)) → ISPLNATKIND(V1)
ISPLNATKIND(pair(V1, V2)) → ISLNATKIND(V1)
ISLNATKIND(tail(V1)) → ISLNATKIND(V1)
ISLNATKIND(take(V1, V2)) → U1711(isNaturalKind(V1), V2)
U1711(tt, V2) → ISLNATKIND(V2)
ISLNATKIND(take(V1, V2)) → ISNATURALKIND(V1)
ISPLNATKIND(splitAt(V1, V2)) → U2711(isNaturalKind(V1), V2)
U2711(tt, V2) → ISLNATKIND(V2)
ISPLNATKIND(splitAt(V1, V2)) → ISNATURALKIND(V1)

The TRS R consists of the following 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)

Q is empty.

The following rules are not useable and can be deleted:

U101(tt, x0, x1) → U102(isNaturalKind(x0), x0, x1)
U102(tt, x0, x1) → U103(isLNatKind(x1), x0, x1)
U103(tt, x0, x1) → U104(isLNatKind(x1), x0, x1)
U104(tt, x0, x1) → U105(isNatural(x0), x1)
U105(tt, x0) → U106(isLNat(x0))
U106(tt) → tt
U11(tt, x0, x1) → U12(isNaturalKind(x0), x0, x1)
U12(tt, x0, x1) → U13(isLNat(x1), x0, x1)
U13(tt, x0, x1) → U14(isLNatKind(x1), x0, x1)
U14(tt, x0, x1) → snd(splitAt(x0, x1))
U181(tt, x0) → U182(isLNatKind(x0), x0)
U182(tt, x0) → U183(isLNat(x0))
U183(tt) → tt
U191(tt, x0) → U192(isNaturalKind(x0), x0)
U192(tt, x0) → U193(isNatural(x0))
U193(tt) → tt
U201(tt, x0, x1) → U202(isNaturalKind(x0), x0, x1)
U202(tt, x0, x1) → U203(isLNatKind(x1), x0, x1)
U203(tt, x0, x1) → U204(isLNatKind(x1), x0, x1)
U204(tt, x0, x1) → U205(isNatural(x0), x1)
U205(tt, x0) → U206(isLNat(x0))
U206(tt) → tt
U21(tt, x0, x1) → U22(isLNatKind(x0), x0, x1)
U22(tt, x0, x1) → U23(isLNat(x1), x0, x1)
U23(tt, x0, x1) → U24(isLNatKind(x1), x0)
U24(tt, x0) → x0
U241(tt, x0, x1) → U242(isLNatKind(x0), x0, x1)
U242(tt, x0, x1) → U243(isLNatKind(x1), x0, x1)
U243(tt, x0, x1) → U244(isLNatKind(x1), x0, x1)
U244(tt, x0, x1) → U245(isLNat(x0), x1)
U245(tt, x0) → U246(isLNat(x0))
U246(tt) → tt
U251(tt, x0, x1) → U252(isNaturalKind(x0), x0, x1)
U252(tt, x0, x1) → U253(isLNatKind(x1), x0, x1)
U253(tt, x0, x1) → U254(isLNatKind(x1), x0, x1)
U254(tt, x0, x1) → U255(isNatural(x0), x1)
U255(tt, x0) → U256(isLNat(x0))
U256(tt) → tt
U281(tt, x0) → U282(isNaturalKind(x0), x0)
U282(tt, x0) → cons(x0, natsFrom(s(x0)))
U291(tt, x0, x1) → U292(isNaturalKind(x0), x0, x1)
U292(tt, x0, x1) → U293(isLNat(x1), x0, x1)
U293(tt, x0, x1) → U294(isLNatKind(x1), x0, x1)
U294(tt, x0, x1) → head(afterNth(x0, x1))
U301(tt, x0, x1) → U302(isLNatKind(x0), x1)
U302(tt, x0) → U303(isLNat(x0), x0)
U303(tt, x0) → U304(isLNatKind(x0), x0)
U304(tt, x0) → x0
U31(tt, x0, x1) → U32(isNaturalKind(x0), x0, x1)
U311(tt, x0) → U312(isLNatKind(x0), x0)
U312(tt, x0) → pair(nil, x0)
U32(tt, x0, x1) → U33(isLNat(x1), x0, x1)
U321(tt, x0, x1, x2) → U322(isNaturalKind(x0), x0, x1, x2)
U322(tt, x0, x1, x2) → U323(isNatural(x1), x0, x1, x2)
U323(tt, x0, x1, x2) → U324(isNaturalKind(x1), x0, x1, x2)
U324(tt, x0, x1, x2) → U325(isLNat(x2), x0, x1, x2)
U325(tt, x0, x1, x2) → U326(isLNatKind(x2), x0, x1, x2)
U326(tt, x0, x1, x2) → U327(splitAt(x0, x2), x1)
U327(pair(x0, x1), x2) → pair(cons(x2, x0), x1)
U33(tt, x0, x1) → U34(isLNatKind(x1), x0)
U331(tt, x0, x1) → U332(isNaturalKind(x0), x1)
U332(tt, x0) → U333(isLNat(x0), x0)
U333(tt, x0) → U334(isLNatKind(x0), x0)
U334(tt, x0) → x0
U34(tt, x0) → x0
U341(tt, x0, x1) → U342(isNaturalKind(x0), x0, x1)
U342(tt, x0, x1) → U343(isLNat(x1), x0, x1)
U343(tt, x0, x1) → U344(isLNatKind(x1), x0, x1)
U344(tt, x0, x1) → fst(splitAt(x0, x1))
U41(tt, x0, x1) → U42(isNaturalKind(x0), x0, x1)
U42(tt, x0, x1) → U43(isLNatKind(x1), x0, x1)
U43(tt, x0, x1) → U44(isLNatKind(x1), x0, x1)
U44(tt, x0, x1) → U45(isNatural(x0), x1)
U45(tt, x0) → U46(isLNat(x0))
U46(tt) → tt
U51(tt, x0, x1) → U52(isNaturalKind(x0), x0, x1)
U52(tt, x0, x1) → U53(isLNatKind(x1), x0, x1)
U53(tt, x0, x1) → U54(isLNatKind(x1), x0, x1)
U54(tt, x0, x1) → U55(isNatural(x0), x1)
U55(tt, x0) → U56(isLNat(x0))
U56(tt) → tt
U61(tt, x0) → U62(isPLNatKind(x0), x0)
U62(tt, x0) → U63(isPLNat(x0))
U63(tt) → tt
U71(tt, x0) → U72(isNaturalKind(x0), x0)
U72(tt, x0) → U73(isNatural(x0))
U73(tt) → tt
U81(tt, x0) → U82(isPLNatKind(x0), x0)
U82(tt, x0) → U83(isPLNat(x0))
U83(tt) → tt
U91(tt, x0) → U92(isLNatKind(x0), x0)
U92(tt, x0) → U93(isLNat(x0))
U93(tt) → tt
afterNth(x0, x1) → U11(isNatural(x0), x0, x1)
fst(pair(x0, x1)) → U21(isLNat(x0), x0, x1)
head(cons(x0, x1)) → U31(isNatural(x0), x0, x1)
isLNat(nil) → tt
isLNat(afterNth(x0, x1)) → U41(isNaturalKind(x0), x0, x1)
isLNat(cons(x0, x1)) → U51(isNaturalKind(x0), x0, x1)
isLNat(fst(x0)) → U61(isPLNatKind(x0), x0)
isLNat(natsFrom(x0)) → U71(isNaturalKind(x0), x0)
isLNat(snd(x0)) → U81(isPLNatKind(x0), x0)
isLNat(tail(x0)) → U91(isLNatKind(x0), x0)
isLNat(take(x0, x1)) → U101(isNaturalKind(x0), x0, x1)
isNatural(0) → tt
isNatural(head(x0)) → U181(isLNatKind(x0), x0)
isNatural(s(x0)) → U191(isNaturalKind(x0), x0)
isNatural(sel(x0, x1)) → U201(isNaturalKind(x0), x0, x1)
isPLNat(pair(x0, x1)) → U241(isLNatKind(x0), x0, x1)
isPLNat(splitAt(x0, x1)) → U251(isNaturalKind(x0), x0, x1)
natsFrom(x0) → U281(isNatural(x0), x0)
sel(x0, x1) → U291(isNatural(x0), x0, x1)
snd(pair(x0, x1)) → U301(isLNat(x0), x0, x1)
splitAt(0, x0) → U311(isLNat(x0), x0)
splitAt(s(x0), cons(x1, x2)) → U321(isNatural(x0), x0, x1, x2)
tail(cons(x0, x1)) → U331(isNatural(x0), x0, x1)
take(x0, x1) → U341(isNatural(x0), x0, x1)


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {head, U211, afterNth, s, U221, sel, U232, U122, fst, U131, pair, natsFrom, U141, snd, U151, splitAt, U272, tail, U161, take, U172, U262, U112} are replacing on all positions.
For all symbols f in {U111, U231, cons, U121, U261, U271, U171, U1111, U2311, U1211, U2611, U1711, U2711} we have µ(f) = {1}.
The symbols in {isNaturalKind, isLNatKind, isPLNatKind, ISLNATKIND, ISNATURALKIND, ISPLNATKIND} are not replacing on any position.

The TRS P consists of the following rules:

ISNATURALKIND(head(V1)) → ISLNATKIND(V1)
ISLNATKIND(afterNth(V1, V2)) → U1111(isNaturalKind(V1), V2)
U1111(tt, V2) → ISLNATKIND(V2)
ISLNATKIND(afterNth(V1, V2)) → ISNATURALKIND(V1)
ISNATURALKIND(s(V1)) → ISNATURALKIND(V1)
ISNATURALKIND(sel(V1, V2)) → U2311(isNaturalKind(V1), V2)
U2311(tt, V2) → ISLNATKIND(V2)
ISLNATKIND(cons(V1, V2)) → U1211(isNaturalKind(V1), V2)
U1211(tt, V2) → ISLNATKIND(V2)
ISLNATKIND(cons(V1, V2)) → ISNATURALKIND(V1)
ISNATURALKIND(sel(V1, V2)) → ISNATURALKIND(V1)
ISLNATKIND(fst(V1)) → ISPLNATKIND(V1)
ISPLNATKIND(pair(V1, V2)) → U2611(isLNatKind(V1), V2)
U2611(tt, V2) → ISLNATKIND(V2)
ISLNATKIND(natsFrom(V1)) → ISNATURALKIND(V1)
ISLNATKIND(snd(V1)) → ISPLNATKIND(V1)
ISPLNATKIND(pair(V1, V2)) → ISLNATKIND(V1)
ISLNATKIND(tail(V1)) → ISLNATKIND(V1)
ISLNATKIND(take(V1, V2)) → U1711(isNaturalKind(V1), V2)
U1711(tt, V2) → ISLNATKIND(V2)
ISLNATKIND(take(V1, V2)) → ISNATURALKIND(V1)
ISPLNATKIND(splitAt(V1, V2)) → U2711(isNaturalKind(V1), V2)
U2711(tt, V2) → ISLNATKIND(V2)
ISPLNATKIND(splitAt(V1, V2)) → ISNATURALKIND(V1)

The TRS R consists of the following rules:

isNaturalKind(0) → tt
isNaturalKind(head(V1)) → U211(isLNatKind(V1))
isLNatKind(nil) → tt
isLNatKind(afterNth(V1, V2)) → U111(isNaturalKind(V1), V2)
isNaturalKind(s(V1)) → U221(isNaturalKind(V1))
isNaturalKind(sel(V1, V2)) → U231(isNaturalKind(V1), V2)
U231(tt, V2) → U232(isLNatKind(V2))
isLNatKind(cons(V1, V2)) → U121(isNaturalKind(V1), V2)
U121(tt, V2) → U122(isLNatKind(V2))
isLNatKind(fst(V1)) → U131(isPLNatKind(V1))
isPLNatKind(pair(V1, V2)) → U261(isLNatKind(V1), V2)
isLNatKind(natsFrom(V1)) → U141(isNaturalKind(V1))
U141(tt) → tt
isLNatKind(snd(V1)) → U151(isPLNatKind(V1))
isPLNatKind(splitAt(V1, V2)) → U271(isNaturalKind(V1), V2)
U271(tt, V2) → U272(isLNatKind(V2))
isLNatKind(tail(V1)) → U161(isLNatKind(V1))
isLNatKind(take(V1, V2)) → U171(isNaturalKind(V1), V2)
U171(tt, V2) → U172(isLNatKind(V2))
U172(tt) → tt
U161(tt) → tt
U272(tt) → tt
U151(tt) → tt
U261(tt, V2) → U262(isLNatKind(V2))
U262(tt) → tt
U131(tt) → tt
U122(tt) → tt
U232(tt) → tt
U221(tt) → tt
U111(tt, V2) → U112(isLNatKind(V2))
U112(tt) → tt
U211(tt) → tt

Q is empty.

Using the order
Polynomial interpretation with max and min functions [25]:

POL(0) = 1   
POL(ISLNATKIND(x1)) = x1   
POL(ISNATURALKIND(x1)) = 1 + x1   
POL(ISPLNATKIND(x1)) = x1   
POL(U111(x1, x2)) = x2   
POL(U1111(x1, x2)) = 1 + x2   
POL(U112(x1)) = x1   
POL(U121(x1, x2)) = x2   
POL(U1211(x1, x2)) = x2   
POL(U122(x1)) = x1   
POL(U131(x1)) = x1   
POL(U141(x1)) = x1   
POL(U151(x1)) = 1   
POL(U161(x1)) = 1 + x1   
POL(U171(x1, x2)) = x2   
POL(U1711(x1, x2)) = x2   
POL(U172(x1)) = x1   
POL(U211(x1)) = 1   
POL(U221(x1)) = 1 + x1   
POL(U231(x1, x2)) = 1 + x1 + x2   
POL(U2311(x1, x2)) = x2   
POL(U232(x1)) = 1   
POL(U261(x1, x2)) = x1 + x2   
POL(U2611(x1, x2)) = x2   
POL(U262(x1)) = x1   
POL(U271(x1, x2)) = x2   
POL(U2711(x1, x2)) = x2   
POL(U272(x1)) = x1   
POL(afterNth(x1, x2)) = 1 + x1 + x2   
POL(cons(x1, x2)) = 1 + x1 + x2   
POL(fst(x1)) = x1   
POL(head(x1)) = 1 + x1   
POL(isLNatKind(x1)) = x1   
POL(isNaturalKind(x1)) = 1 + x1   
POL(isPLNatKind(x1)) = x1   
POL(natsFrom(x1)) = 1 + x1   
POL(nil) = 1   
POL(pair(x1, x2)) = 1 + x1 + x2   
POL(s(x1)) = 1 + x1   
POL(sel(x1, x2)) = 1 + x1 + x2   
POL(snd(x1)) = 1 + x1   
POL(splitAt(x1, x2)) = 1 + x1 + x2   
POL(tail(x1)) = 1 + x1   
POL(take(x1, x2)) = 1 + x1 + x2   
POL(tt) = 1   

the following usable rules

isNaturalKind(0) → tt
isNaturalKind(head(V1)) → U211(isLNatKind(V1))
isNaturalKind(s(V1)) → U221(isNaturalKind(V1))
isNaturalKind(sel(V1, V2)) → U231(isNaturalKind(V1), V2)
U211(tt) → tt
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)
U111(tt, V2) → U112(isLNatKind(V2))
U112(tt) → tt
U121(tt, V2) → U122(isLNatKind(V2))
U122(tt) → tt
U131(tt) → tt
isPLNatKind(pair(V1, V2)) → U261(isLNatKind(V1), V2)
isPLNatKind(splitAt(V1, V2)) → U271(isNaturalKind(V1), V2)
U261(tt, V2) → U262(isLNatKind(V2))
U262(tt) → tt
U271(tt, V2) → U272(isLNatKind(V2))
U272(tt) → tt
U141(tt) → tt
U151(tt) → tt
U161(tt) → tt
U171(tt, V2) → U172(isLNatKind(V2))
U172(tt) → tt
U221(tt) → tt
U231(tt, V2) → U232(isLNatKind(V2))
U232(tt) → tt

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

ISNATURALKIND(head(V1)) → ISLNATKIND(V1)
U1111(tt, V2) → ISLNATKIND(V2)
ISNATURALKIND(s(V1)) → ISNATURALKIND(V1)
ISNATURALKIND(sel(V1, V2)) → U2311(isNaturalKind(V1), V2)
ISLNATKIND(cons(V1, V2)) → U1211(isNaturalKind(V1), V2)
ISNATURALKIND(sel(V1, V2)) → ISNATURALKIND(V1)
ISPLNATKIND(pair(V1, V2)) → U2611(isLNatKind(V1), V2)
ISLNATKIND(snd(V1)) → ISPLNATKIND(V1)
ISPLNATKIND(pair(V1, V2)) → ISLNATKIND(V1)
ISLNATKIND(tail(V1)) → ISLNATKIND(V1)
ISLNATKIND(take(V1, V2)) → U1711(isNaturalKind(V1), V2)
ISPLNATKIND(splitAt(V1, V2)) → U2711(isNaturalKind(V1), V2)

could be oriented strictly and thus removed.
The pairs

ISLNATKIND(afterNth(V1, V2)) → U1111(isNaturalKind(V1), V2)
ISLNATKIND(afterNth(V1, V2)) → ISNATURALKIND(V1)
U2311(tt, V2) → ISLNATKIND(V2)
U1211(tt, V2) → ISLNATKIND(V2)
ISLNATKIND(cons(V1, V2)) → ISNATURALKIND(V1)
ISLNATKIND(fst(V1)) → ISPLNATKIND(V1)
U2611(tt, V2) → ISLNATKIND(V2)
ISLNATKIND(natsFrom(V1)) → ISNATURALKIND(V1)
U1711(tt, V2) → ISLNATKIND(V2)
ISLNATKIND(take(V1, V2)) → ISNATURALKIND(V1)
U2711(tt, V2) → ISLNATKIND(V2)
ISPLNATKIND(splitAt(V1, V2)) → ISNATURALKIND(V1)

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {head, U211, afterNth, s, U221, sel, U232, U122, fst, U131, pair, natsFrom, U141, snd, U151, splitAt, U272, tail, U161, take, U172, U262, U112} are replacing on all positions.
For all symbols f in {U111, U231, cons, U121, U261, U271, U171, U1111, U2311, U1211, U2611, U1711, U2711} we have µ(f) = {1}.
The symbols in {isNaturalKind, isLNatKind, isPLNatKind, ISLNATKIND, ISNATURALKIND, ISPLNATKIND} are not replacing on any position.

The TRS P consists of the following rules:

ISLNATKIND(afterNth(V1, V2)) → U1111(isNaturalKind(V1), V2)
ISLNATKIND(afterNth(V1, V2)) → ISNATURALKIND(V1)
U2311(tt, V2) → ISLNATKIND(V2)
U1211(tt, V2) → ISLNATKIND(V2)
ISLNATKIND(cons(V1, V2)) → ISNATURALKIND(V1)
ISLNATKIND(fst(V1)) → ISPLNATKIND(V1)
U2611(tt, V2) → ISLNATKIND(V2)
ISLNATKIND(natsFrom(V1)) → ISNATURALKIND(V1)
U1711(tt, V2) → ISLNATKIND(V2)
ISLNATKIND(take(V1, V2)) → ISNATURALKIND(V1)
U2711(tt, V2) → ISLNATKIND(V2)
ISPLNATKIND(splitAt(V1, V2)) → ISNATURALKIND(V1)

The TRS R consists of the following rules:

isNaturalKind(0) → tt
isNaturalKind(head(V1)) → U211(isLNatKind(V1))
isLNatKind(nil) → tt
isLNatKind(afterNth(V1, V2)) → U111(isNaturalKind(V1), V2)
isNaturalKind(s(V1)) → U221(isNaturalKind(V1))
isNaturalKind(sel(V1, V2)) → U231(isNaturalKind(V1), V2)
U231(tt, V2) → U232(isLNatKind(V2))
isLNatKind(cons(V1, V2)) → U121(isNaturalKind(V1), V2)
U121(tt, V2) → U122(isLNatKind(V2))
isLNatKind(fst(V1)) → U131(isPLNatKind(V1))
isPLNatKind(pair(V1, V2)) → U261(isLNatKind(V1), V2)
isLNatKind(natsFrom(V1)) → U141(isNaturalKind(V1))
U141(tt) → tt
isLNatKind(snd(V1)) → U151(isPLNatKind(V1))
isPLNatKind(splitAt(V1, V2)) → U271(isNaturalKind(V1), V2)
U271(tt, V2) → U272(isLNatKind(V2))
isLNatKind(tail(V1)) → U161(isLNatKind(V1))
isLNatKind(take(V1, V2)) → U171(isNaturalKind(V1), V2)
U171(tt, V2) → U172(isLNatKind(V2))
U172(tt) → tt
U161(tt) → tt
U272(tt) → tt
U151(tt) → tt
U261(tt, V2) → U262(isLNatKind(V2))
U262(tt) → tt
U131(tt) → tt
U122(tt) → tt
U232(tt) → tt
U221(tt) → tt
U111(tt, V2) → U112(isLNatKind(V2))
U112(tt) → tt
U211(tt) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 12 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U106, U112, U122, U131, snd, splitAt, U141, U151, U161, U172, U183, U193, U206, U211, U221, U232, U246, U256, U262, U272, natsFrom, s, head, afterNth, pair, fst, U46, U56, U63, U73, U83, U93, tail, take, sel} are replacing on all positions.
For all symbols f in {U101, U102, U103, U104, U105, U11, U12, U111, U13, U121, U14, U171, U181, U182, U191, U192, U201, U202, U203, U204, U205, U21, U22, U23, U24, U231, U241, U242, U243, U244, U245, U251, U252, U253, U254, U255, U261, U271, U281, U282, cons, U291, U292, U293, U294, U301, U302, U303, U304, U31, U32, U311, U312, U33, U321, U322, U323, U324, U325, U326, U327, U34, U331, U332, U333, U334, U341, U342, U343, U344, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U81, U82, U91, U92, U1031, U1021, U1041, U1051, U411, U421, U431, U441, U451, U511, U521, U531, U541, U551, U611, U621, U2411, U2421, U2431, U2441, U2451, U711, U721, U1811, U1821, U811, U821, U2511, U2521, U2531, U2541, U2551, U911, U921, U1011, U1911, U1921, U2011, U2021, U2031, U2041, U2051} we have µ(f) = {1}.
The symbols in {isNaturalKind, isLNatKind, isNatural, isLNat, isPLNatKind, isPLNat, ISLNAT, ISPLNAT, ISNATURAL} are not replacing on any position.

The TRS P consists of the following rules:

U1021(tt, V1, V2) → U1031(isLNatKind(V2), V1, V2)
U1031(tt, V1, V2) → U1041(isLNatKind(V2), V1, V2)
U1041(tt, V1, V2) → U1051(isNatural(V1), V2)
U1051(tt, V2) → ISLNAT(V2)
ISLNAT(afterNth(V1, V2)) → U411(isNaturalKind(V1), V1, V2)
U411(tt, V1, V2) → U421(isNaturalKind(V1), V1, V2)
U421(tt, V1, V2) → U431(isLNatKind(V2), V1, V2)
U431(tt, V1, V2) → U441(isLNatKind(V2), V1, V2)
U441(tt, V1, V2) → U451(isNatural(V1), V2)
U451(tt, V2) → ISLNAT(V2)
ISLNAT(cons(V1, V2)) → U511(isNaturalKind(V1), V1, V2)
U511(tt, V1, V2) → U521(isNaturalKind(V1), V1, V2)
U521(tt, V1, V2) → U531(isLNatKind(V2), V1, V2)
U531(tt, V1, V2) → U541(isLNatKind(V2), V1, V2)
U541(tt, V1, V2) → U551(isNatural(V1), V2)
U551(tt, V2) → ISLNAT(V2)
ISLNAT(fst(V1)) → U611(isPLNatKind(V1), V1)
U611(tt, V1) → U621(isPLNatKind(V1), V1)
U621(tt, V1) → ISPLNAT(V1)
ISPLNAT(pair(V1, V2)) → U2411(isLNatKind(V1), V1, V2)
U2411(tt, V1, V2) → U2421(isLNatKind(V1), V1, V2)
U2421(tt, V1, V2) → U2431(isLNatKind(V2), V1, V2)
U2431(tt, V1, V2) → U2441(isLNatKind(V2), V1, V2)
U2441(tt, V1, V2) → U2451(isLNat(V1), V2)
U2451(tt, V2) → ISLNAT(V2)
ISLNAT(natsFrom(V1)) → U711(isNaturalKind(V1), V1)
U711(tt, V1) → U721(isNaturalKind(V1), V1)
U721(tt, V1) → ISNATURAL(V1)
ISNATURAL(head(V1)) → U1811(isLNatKind(V1), V1)
U1811(tt, V1) → U1821(isLNatKind(V1), V1)
U1821(tt, V1) → ISLNAT(V1)
ISLNAT(snd(V1)) → U811(isPLNatKind(V1), V1)
U811(tt, V1) → U821(isPLNatKind(V1), V1)
U821(tt, V1) → ISPLNAT(V1)
ISPLNAT(splitAt(V1, V2)) → U2511(isNaturalKind(V1), V1, V2)
U2511(tt, V1, V2) → U2521(isNaturalKind(V1), V1, V2)
U2521(tt, V1, V2) → U2531(isLNatKind(V2), V1, V2)
U2531(tt, V1, V2) → U2541(isLNatKind(V2), V1, V2)
U2541(tt, V1, V2) → U2551(isNatural(V1), V2)
U2551(tt, V2) → ISLNAT(V2)
ISLNAT(tail(V1)) → U911(isLNatKind(V1), V1)
U911(tt, V1) → U921(isLNatKind(V1), V1)
U921(tt, V1) → ISLNAT(V1)
ISLNAT(take(V1, V2)) → U1011(isNaturalKind(V1), V1, V2)
U1011(tt, V1, V2) → U1021(isNaturalKind(V1), V1, V2)
U2541(tt, V1, V2) → ISNATURAL(V1)
ISNATURAL(s(V1)) → U1911(isNaturalKind(V1), V1)
U1911(tt, V1) → U1921(isNaturalKind(V1), V1)
U1921(tt, V1) → ISNATURAL(V1)
ISNATURAL(sel(V1, V2)) → U2011(isNaturalKind(V1), V1, V2)
U2011(tt, V1, V2) → U2021(isNaturalKind(V1), V1, V2)
U2021(tt, V1, V2) → U2031(isLNatKind(V2), V1, V2)
U2031(tt, V1, V2) → U2041(isLNatKind(V2), V1, V2)
U2041(tt, V1, V2) → U2051(isNatural(V1), V2)
U2051(tt, V2) → ISLNAT(V2)
U2041(tt, V1, V2) → ISNATURAL(V1)
U2441(tt, V1, V2) → ISLNAT(V1)
U541(tt, V1, V2) → ISNATURAL(V1)
U441(tt, V1, V2) → ISNATURAL(V1)
U1041(tt, V1, V2) → ISNATURAL(V1)

The TRS R consists of the following 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)

Q is empty.

The following rules are not useable and can be deleted:

U11(tt, x0, x1) → U12(isNaturalKind(x0), x0, x1)
U12(tt, x0, x1) → U13(isLNat(x1), x0, x1)
U13(tt, x0, x1) → U14(isLNatKind(x1), x0, x1)
U14(tt, x0, x1) → snd(splitAt(x0, x1))
U21(tt, x0, x1) → U22(isLNatKind(x0), x0, x1)
U22(tt, x0, x1) → U23(isLNat(x1), x0, x1)
U23(tt, x0, x1) → U24(isLNatKind(x1), x0)
U24(tt, x0) → x0
U281(tt, x0) → U282(isNaturalKind(x0), x0)
U282(tt, x0) → cons(x0, natsFrom(s(x0)))
U291(tt, x0, x1) → U292(isNaturalKind(x0), x0, x1)
U292(tt, x0, x1) → U293(isLNat(x1), x0, x1)
U293(tt, x0, x1) → U294(isLNatKind(x1), x0, x1)
U294(tt, x0, x1) → head(afterNth(x0, x1))
U301(tt, x0, x1) → U302(isLNatKind(x0), x1)
U302(tt, x0) → U303(isLNat(x0), x0)
U303(tt, x0) → U304(isLNatKind(x0), x0)
U304(tt, x0) → x0
U31(tt, x0, x1) → U32(isNaturalKind(x0), x0, x1)
U311(tt, x0) → U312(isLNatKind(x0), x0)
U312(tt, x0) → pair(nil, x0)
U32(tt, x0, x1) → U33(isLNat(x1), x0, x1)
U321(tt, x0, x1, x2) → U322(isNaturalKind(x0), x0, x1, x2)
U322(tt, x0, x1, x2) → U323(isNatural(x1), x0, x1, x2)
U323(tt, x0, x1, x2) → U324(isNaturalKind(x1), x0, x1, x2)
U324(tt, x0, x1, x2) → U325(isLNat(x2), x0, x1, x2)
U325(tt, x0, x1, x2) → U326(isLNatKind(x2), x0, x1, x2)
U326(tt, x0, x1, x2) → U327(splitAt(x0, x2), x1)
U327(pair(x0, x1), x2) → pair(cons(x2, x0), x1)
U33(tt, x0, x1) → U34(isLNatKind(x1), x0)
U331(tt, x0, x1) → U332(isNaturalKind(x0), x1)
U332(tt, x0) → U333(isLNat(x0), x0)
U333(tt, x0) → U334(isLNatKind(x0), x0)
U334(tt, x0) → x0
U34(tt, x0) → x0
U341(tt, x0, x1) → U342(isNaturalKind(x0), x0, x1)
U342(tt, x0, x1) → U343(isLNat(x1), x0, x1)
U343(tt, x0, x1) → U344(isLNatKind(x1), x0, x1)
U344(tt, x0, x1) → fst(splitAt(x0, x1))
afterNth(x0, x1) → U11(isNatural(x0), x0, x1)
fst(pair(x0, x1)) → U21(isLNat(x0), x0, x1)
head(cons(x0, x1)) → U31(isNatural(x0), x0, x1)
natsFrom(x0) → U281(isNatural(x0), x0)
sel(x0, x1) → U291(isNatural(x0), x0, x1)
snd(pair(x0, x1)) → U301(isLNat(x0), x0, x1)
splitAt(0, x0) → U311(isLNat(x0), x0)
splitAt(s(x0), cons(x1, x2)) → U321(isNatural(x0), x0, x1, x2)
tail(cons(x0, x1)) → U331(isNatural(x0), x0, x1)
take(x0, x1) → U341(isNatural(x0), x0, x1)


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {afterNth, head, U211, s, U221, sel, U232, fst, U131, pair, natsFrom, U141, snd, U151, splitAt, U272, tail, U161, take, U172, U262, U122, U112, U183, U193, U206, U56, U63, U73, U83, U256, U93, U106, U246, U46} are replacing on all positions.
For all symbols f in {U111, cons, U121, U231, U261, U271, U171, U181, U182, U41, U42, U43, U44, U45, U191, U192, U201, U202, U203, U204, U205, U51, U52, U53, U54, U55, U61, U62, U241, U242, U243, U244, U245, U71, U72, U81, U82, U251, U252, U253, U254, U255, U91, U92, U101, U102, U103, U104, U105, U1031, U1021, U1041, U1051, U411, U421, U431, U441, U451, U511, U521, U531, U541, U551, U611, U621, U2411, U2421, U2431, U2441, U2451, U711, U721, U1811, U1821, U811, U821, U2511, U2521, U2531, U2541, U2551, U911, U921, U1011, U1911, U1921, U2011, U2021, U2031, U2041, U2051} we have µ(f) = {1}.
The symbols in {isLNatKind, isNaturalKind, isPLNatKind, isNatural, isLNat, isPLNat, ISLNAT, ISPLNAT, ISNATURAL} are not replacing on any position.

The TRS P consists of the following rules:

U1021(tt, V1, V2) → U1031(isLNatKind(V2), V1, V2)
U1031(tt, V1, V2) → U1041(isLNatKind(V2), V1, V2)
U1041(tt, V1, V2) → U1051(isNatural(V1), V2)
U1051(tt, V2) → ISLNAT(V2)
ISLNAT(afterNth(V1, V2)) → U411(isNaturalKind(V1), V1, V2)
U411(tt, V1, V2) → U421(isNaturalKind(V1), V1, V2)
U421(tt, V1, V2) → U431(isLNatKind(V2), V1, V2)
U431(tt, V1, V2) → U441(isLNatKind(V2), V1, V2)
U441(tt, V1, V2) → U451(isNatural(V1), V2)
U451(tt, V2) → ISLNAT(V2)
ISLNAT(cons(V1, V2)) → U511(isNaturalKind(V1), V1, V2)
U511(tt, V1, V2) → U521(isNaturalKind(V1), V1, V2)
U521(tt, V1, V2) → U531(isLNatKind(V2), V1, V2)
U531(tt, V1, V2) → U541(isLNatKind(V2), V1, V2)
U541(tt, V1, V2) → U551(isNatural(V1), V2)
U551(tt, V2) → ISLNAT(V2)
ISLNAT(fst(V1)) → U611(isPLNatKind(V1), V1)
U611(tt, V1) → U621(isPLNatKind(V1), V1)
U621(tt, V1) → ISPLNAT(V1)
ISPLNAT(pair(V1, V2)) → U2411(isLNatKind(V1), V1, V2)
U2411(tt, V1, V2) → U2421(isLNatKind(V1), V1, V2)
U2421(tt, V1, V2) → U2431(isLNatKind(V2), V1, V2)
U2431(tt, V1, V2) → U2441(isLNatKind(V2), V1, V2)
U2441(tt, V1, V2) → U2451(isLNat(V1), V2)
U2451(tt, V2) → ISLNAT(V2)
ISLNAT(natsFrom(V1)) → U711(isNaturalKind(V1), V1)
U711(tt, V1) → U721(isNaturalKind(V1), V1)
U721(tt, V1) → ISNATURAL(V1)
ISNATURAL(head(V1)) → U1811(isLNatKind(V1), V1)
U1811(tt, V1) → U1821(isLNatKind(V1), V1)
U1821(tt, V1) → ISLNAT(V1)
ISLNAT(snd(V1)) → U811(isPLNatKind(V1), V1)
U811(tt, V1) → U821(isPLNatKind(V1), V1)
U821(tt, V1) → ISPLNAT(V1)
ISPLNAT(splitAt(V1, V2)) → U2511(isNaturalKind(V1), V1, V2)
U2511(tt, V1, V2) → U2521(isNaturalKind(V1), V1, V2)
U2521(tt, V1, V2) → U2531(isLNatKind(V2), V1, V2)
U2531(tt, V1, V2) → U2541(isLNatKind(V2), V1, V2)
U2541(tt, V1, V2) → U2551(isNatural(V1), V2)
U2551(tt, V2) → ISLNAT(V2)
ISLNAT(tail(V1)) → U911(isLNatKind(V1), V1)
U911(tt, V1) → U921(isLNatKind(V1), V1)
U921(tt, V1) → ISLNAT(V1)
ISLNAT(take(V1, V2)) → U1011(isNaturalKind(V1), V1, V2)
U1011(tt, V1, V2) → U1021(isNaturalKind(V1), V1, V2)
U2541(tt, V1, V2) → ISNATURAL(V1)
ISNATURAL(s(V1)) → U1911(isNaturalKind(V1), V1)
U1911(tt, V1) → U1921(isNaturalKind(V1), V1)
U1921(tt, V1) → ISNATURAL(V1)
ISNATURAL(sel(V1, V2)) → U2011(isNaturalKind(V1), V1, V2)
U2011(tt, V1, V2) → U2021(isNaturalKind(V1), V1, V2)
U2021(tt, V1, V2) → U2031(isLNatKind(V2), V1, V2)
U2031(tt, V1, V2) → U2041(isLNatKind(V2), V1, V2)
U2041(tt, V1, V2) → U2051(isNatural(V1), V2)
U2051(tt, V2) → ISLNAT(V2)
U2041(tt, V1, V2) → ISNATURAL(V1)
U2441(tt, V1, V2) → ISLNAT(V1)
U541(tt, V1, V2) → ISNATURAL(V1)
U441(tt, V1, V2) → ISNATURAL(V1)
U1041(tt, V1, V2) → ISNATURAL(V1)

The TRS R consists of the following rules:

isLNatKind(nil) → tt
isLNatKind(afterNth(V1, V2)) → U111(isNaturalKind(V1), V2)
isNaturalKind(0) → tt
isNaturalKind(head(V1)) → U211(isLNatKind(V1))
isLNatKind(cons(V1, V2)) → U121(isNaturalKind(V1), V2)
isNaturalKind(s(V1)) → U221(isNaturalKind(V1))
isNaturalKind(sel(V1, V2)) → U231(isNaturalKind(V1), V2)
U231(tt, V2) → U232(isLNatKind(V2))
isLNatKind(fst(V1)) → U131(isPLNatKind(V1))
isPLNatKind(pair(V1, V2)) → U261(isLNatKind(V1), V2)
isLNatKind(natsFrom(V1)) → U141(isNaturalKind(V1))
U141(tt) → tt
isLNatKind(snd(V1)) → U151(isPLNatKind(V1))
isPLNatKind(splitAt(V1, V2)) → U271(isNaturalKind(V1), V2)
U271(tt, V2) → U272(isLNatKind(V2))
isLNatKind(tail(V1)) → U161(isLNatKind(V1))
isLNatKind(take(V1, V2)) → U171(isNaturalKind(V1), V2)
U171(tt, V2) → U172(isLNatKind(V2))
U172(tt) → tt
U161(tt) → tt
U272(tt) → tt
U151(tt) → tt
U261(tt, V2) → U262(isLNatKind(V2))
U262(tt) → tt
U131(tt) → tt
U232(tt) → tt
U221(tt) → tt
U121(tt, V2) → U122(isLNatKind(V2))
U122(tt) → tt
U211(tt) → tt
U111(tt, V2) → U112(isLNatKind(V2))
U112(tt) → tt
isNatural(0) → tt
isNatural(head(V1)) → U181(isLNatKind(V1), V1)
U181(tt, V1) → U182(isLNatKind(V1), V1)
U182(tt, V1) → U183(isLNat(V1))
isLNat(nil) → tt
isLNat(afterNth(V1, V2)) → U41(isNaturalKind(V1), V1, V2)
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)
isNatural(s(V1)) → U191(isNaturalKind(V1), V1)
U191(tt, V1) → U192(isNaturalKind(V1), V1)
U192(tt, V1) → U193(isNatural(V1))
isNatural(sel(V1, V2)) → U201(isNaturalKind(V1), V1, V2)
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))
isLNat(cons(V1, V2)) → U51(isNaturalKind(V1), V1, V2)
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))
isLNat(fst(V1)) → U61(isPLNatKind(V1), V1)
U61(tt, V1) → U62(isPLNatKind(V1), V1)
U62(tt, V1) → U63(isPLNat(V1))
isPLNat(pair(V1, V2)) → U241(isLNatKind(V1), V1, V2)
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)
isLNat(natsFrom(V1)) → U71(isNaturalKind(V1), V1)
U71(tt, V1) → U72(isNaturalKind(V1), V1)
U72(tt, V1) → U73(isNatural(V1))
U73(tt) → tt
isLNat(snd(V1)) → U81(isPLNatKind(V1), V1)
U81(tt, V1) → U82(isPLNatKind(V1), V1)
U82(tt, V1) → U83(isPLNat(V1))
isPLNat(splitAt(V1, V2)) → U251(isNaturalKind(V1), V1, V2)
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))
isLNat(tail(V1)) → U91(isLNatKind(V1), V1)
U91(tt, V1) → U92(isLNatKind(V1), V1)
U92(tt, V1) → U93(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNaturalKind(V1), V1, V2)
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
U93(tt) → tt
U256(tt) → tt
U83(tt) → tt
U245(tt, V2) → U246(isLNat(V2))
U246(tt) → tt
U63(tt) → tt
U56(tt) → tt
U206(tt) → tt
U193(tt) → tt
U45(tt, V2) → U46(isLNat(V2))
U46(tt) → tt
U183(tt) → tt

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 0   
POL(ISLNAT(x1)) = 2·x1   
POL(ISNATURAL(x1)) = 2·x1   
POL(ISPLNAT(x1)) = 1 + x1   
POL(U101(x1, x2, x3)) = 1 + x2 + 2·x3   
POL(U1011(x1, x2, x3)) = 1 + 2·x2 + 2·x3   
POL(U102(x1, x2, x3)) = x1 + 2·x3   
POL(U1021(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U103(x1, x2, x3)) = 2·x1 + 2·x3   
POL(U1031(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U104(x1, x2, x3)) = x1 + 2·x3   
POL(U1041(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U105(x1, x2)) = x2   
POL(U1051(x1, x2)) = 2·x2   
POL(U106(x1)) = 0   
POL(U111(x1, x2)) = 0   
POL(U112(x1)) = x1   
POL(U121(x1, x2)) = 0   
POL(U122(x1)) = x1   
POL(U131(x1)) = 2·x1   
POL(U141(x1)) = 0   
POL(U151(x1)) = 0   
POL(U161(x1)) = 2·x1   
POL(U171(x1, x2)) = 0   
POL(U172(x1)) = 2·x1   
POL(U181(x1, x2)) = 2·x2   
POL(U1811(x1, x2)) = 1 + 2·x2   
POL(U182(x1, x2)) = 2·x2   
POL(U1821(x1, x2)) = 2·x2   
POL(U183(x1)) = 0   
POL(U191(x1, x2)) = 2 + 2·x2   
POL(U1911(x1, x2)) = 2 + 2·x2   
POL(U192(x1, x2)) = 2 + x2   
POL(U1921(x1, x2)) = 2 + 2·x2   
POL(U193(x1)) = 2   
POL(U201(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U2011(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + 2·x3   
POL(U202(x1, x2, x3)) = x2   
POL(U2021(x1, x2, x3)) = 2 + 2·x2 + 2·x3   
POL(U203(x1, x2, x3)) = x1 + x2   
POL(U2031(x1, x2, x3)) = 2 + 2·x2 + 2·x3   
POL(U204(x1, x2, x3)) = 2·x1   
POL(U2041(x1, x2, x3)) = 1 + 2·x2 + 2·x3   
POL(U205(x1, x2)) = 0   
POL(U2051(x1, x2)) = 2·x2   
POL(U206(x1)) = 0   
POL(U211(x1)) = 1 + 2·x1   
POL(U221(x1)) = 2·x1   
POL(U231(x1, x2)) = 2 + x1 + x2   
POL(U232(x1)) = 2 + 2·x1   
POL(U241(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U2411(x1, x2, x3)) = 1 + 2·x2 + 2·x3   
POL(U242(x1, x2, x3)) = x1 + 2·x2 + 2·x3   
POL(U2421(x1, x2, x3)) = 1 + 2·x2 + 2·x3   
POL(U243(x1, x2, x3)) = x1 + x2 + 2·x3   
POL(U2431(x1, x2, x3)) = 1 + 2·x2 + 2·x3   
POL(U244(x1, x2, x3)) = 2·x1 + x2 + 2·x3   
POL(U2441(x1, x2, x3)) = 1 + 2·x2 + 2·x3   
POL(U245(x1, x2)) = x2   
POL(U2451(x1, x2)) = 2·x2   
POL(U246(x1)) = 0   
POL(U251(x1, x2, x3)) = 2 + x2 + 2·x3   
POL(U2511(x1, x2, x3)) = 1 + 2·x2 + 2·x3   
POL(U252(x1, x2, x3)) = 2 + x3   
POL(U2521(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U253(x1, x2, x3)) = 2 + x1 + x3   
POL(U2531(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U254(x1, x2, x3)) = 2 + x3   
POL(U2541(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U255(x1, x2)) = x2   
POL(U2551(x1, x2)) = 2·x2   
POL(U256(x1)) = 0   
POL(U261(x1, x2)) = 0   
POL(U262(x1)) = 0   
POL(U271(x1, x2)) = 0   
POL(U272(x1)) = x1   
POL(U41(x1, x2, x3)) = 2 + x2 + 2·x3   
POL(U411(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + 2·x3   
POL(U42(x1, x2, x3)) = 2 + x2 + 2·x3   
POL(U421(x1, x2, x3)) = 1 + 2·x2 + 2·x3   
POL(U43(x1, x2, x3)) = 2 + x1 + x2 + 2·x3   
POL(U431(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U44(x1, x2, x3)) = 2 + 2·x1 + 2·x3   
POL(U441(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U45(x1, x2)) = 2 + 2·x2   
POL(U451(x1, x2)) = 2·x2   
POL(U46(x1)) = 1 + x1   
POL(U51(x1, x2, x3)) = 2·x2 + 2·x3   
POL(U511(x1, x2, x3)) = 2 + 2·x2 + 2·x3   
POL(U52(x1, x2, x3)) = x2 + 2·x3   
POL(U521(x1, x2, x3)) = 2 + 2·x2 + 2·x3   
POL(U53(x1, x2, x3)) = 0   
POL(U531(x1, x2, x3)) = 2 + 2·x2 + 2·x3   
POL(U54(x1, x2, x3)) = 0   
POL(U541(x1, x2, x3)) = 2 + 2·x2 + 2·x3   
POL(U55(x1, x2)) = 0   
POL(U551(x1, x2)) = 1 + 2·x2   
POL(U56(x1)) = 0   
POL(U61(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(U611(x1, x2)) = 2 + x2   
POL(U62(x1, x2)) = 1 + x2   
POL(U621(x1, x2)) = 1 + x2   
POL(U63(x1)) = 0   
POL(U71(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(U711(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(U72(x1, x2)) = 2   
POL(U721(x1, x2)) = 2·x2   
POL(U73(x1)) = 1   
POL(U81(x1, x2)) = 1 + 2·x1   
POL(U811(x1, x2)) = 2 + x2   
POL(U82(x1, x2)) = 1   
POL(U821(x1, x2)) = 1 + x2   
POL(U83(x1)) = 0   
POL(U91(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(U911(x1, x2)) = 2 + 2·x2   
POL(U92(x1, x2)) = 1 + x1 + x2   
POL(U921(x1, x2)) = 1 + 2·x2   
POL(U93(x1)) = 1   
POL(afterNth(x1, x2)) = 2 + 2·x1 + x2   
POL(cons(x1, x2)) = 2 + x1 + x2   
POL(fst(x1)) = 1 + x1   
POL(head(x1)) = 1 + x1   
POL(isLNat(x1)) = 2·x1   
POL(isLNatKind(x1)) = 0   
POL(isNatural(x1)) = 2·x1   
POL(isNaturalKind(x1)) = x1   
POL(isPLNat(x1)) = 2 + 2·x1   
POL(isPLNatKind(x1)) = 0   
POL(natsFrom(x1)) = 1 + 2·x1   
POL(nil) = 0   
POL(pair(x1, x2)) = 2·x1 + 2·x2   
POL(s(x1)) = 2 + 2·x1   
POL(sel(x1, x2)) = 2 + 2·x1 + x2   
POL(snd(x1)) = 1 + x1   
POL(splitAt(x1, x2)) = 2·x1 + 2·x2   
POL(tail(x1)) = 2 + 2·x1   
POL(take(x1, x2)) = 1 + x1 + 2·x2   
POL(tt) = 0   

the following usable rules

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)
U111(tt, V2) → U112(isLNatKind(V2))
U112(tt) → tt
isNaturalKind(0) → tt
isNaturalKind(head(V1)) → U211(isLNatKind(V1))
isNaturalKind(s(V1)) → U221(isNaturalKind(V1))
isNaturalKind(sel(V1, V2)) → U231(isNaturalKind(V1), V2)
U211(tt) → tt
U221(tt) → tt
U231(tt, V2) → U232(isLNatKind(V2))
U232(tt) → tt
U121(tt, V2) → U122(isLNatKind(V2))
U122(tt) → tt
U131(tt) → tt
isPLNatKind(pair(V1, V2)) → U261(isLNatKind(V1), V2)
isPLNatKind(splitAt(V1, V2)) → U271(isNaturalKind(V1), V2)
U261(tt, V2) → U262(isLNatKind(V2))
U262(tt) → tt
U271(tt, V2) → U272(isLNatKind(V2))
U272(tt) → tt
U141(tt) → tt
U151(tt) → tt
U161(tt) → tt
U171(tt, V2) → U172(isLNatKind(V2))
U172(tt) → tt
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)
U181(tt, V1) → U182(isLNatKind(V1), V1)
U182(tt, V1) → U183(isLNat(V1))
U183(tt) → tt
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)
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
isPLNat(pair(V1, V2)) → U241(isLNatKind(V1), V1, V2)
isPLNat(splitAt(V1, V2)) → U251(isNaturalKind(V1), V1, V2)
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
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
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
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

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

ISLNAT(afterNth(V1, V2)) → U411(isNaturalKind(V1), V1, V2)
U411(tt, V1, V2) → U421(isNaturalKind(V1), V1, V2)
U421(tt, V1, V2) → U431(isLNatKind(V2), V1, V2)
ISLNAT(cons(V1, V2)) → U511(isNaturalKind(V1), V1, V2)
U541(tt, V1, V2) → U551(isNatural(V1), V2)
U551(tt, V2) → ISLNAT(V2)
U611(tt, V1) → U621(isPLNatKind(V1), V1)
U2441(tt, V1, V2) → U2451(isLNat(V1), V2)
ISLNAT(natsFrom(V1)) → U711(isNaturalKind(V1), V1)
U711(tt, V1) → U721(isNaturalKind(V1), V1)
ISNATURAL(head(V1)) → U1811(isLNatKind(V1), V1)
U1811(tt, V1) → U1821(isLNatKind(V1), V1)
U811(tt, V1) → U821(isPLNatKind(V1), V1)
U2511(tt, V1, V2) → U2521(isNaturalKind(V1), V1, V2)
ISLNAT(tail(V1)) → U911(isLNatKind(V1), V1)
U911(tt, V1) → U921(isLNatKind(V1), V1)
U921(tt, V1) → ISLNAT(V1)
ISLNAT(take(V1, V2)) → U1011(isNaturalKind(V1), V1, V2)
U1011(tt, V1, V2) → U1021(isNaturalKind(V1), V1, V2)
ISNATURAL(s(V1)) → U1911(isNaturalKind(V1), V1)
U1921(tt, V1) → ISNATURAL(V1)
ISNATURAL(sel(V1, V2)) → U2011(isNaturalKind(V1), V1, V2)
U2031(tt, V1, V2) → U2041(isLNatKind(V2), V1, V2)
U2041(tt, V1, V2) → U2051(isNatural(V1), V2)
U2041(tt, V1, V2) → ISNATURAL(V1)
U2441(tt, V1, V2) → ISLNAT(V1)
U541(tt, V1, V2) → ISNATURAL(V1)

could be oriented strictly and thus removed.
The pairs

U1021(tt, V1, V2) → U1031(isLNatKind(V2), V1, V2)
U1031(tt, V1, V2) → U1041(isLNatKind(V2), V1, V2)
U1041(tt, V1, V2) → U1051(isNatural(V1), V2)
U1051(tt, V2) → ISLNAT(V2)
U431(tt, V1, V2) → U441(isLNatKind(V2), V1, V2)
U441(tt, V1, V2) → U451(isNatural(V1), V2)
U451(tt, V2) → ISLNAT(V2)
U511(tt, V1, V2) → U521(isNaturalKind(V1), V1, V2)
U521(tt, V1, V2) → U531(isLNatKind(V2), V1, V2)
U531(tt, V1, V2) → U541(isLNatKind(V2), V1, V2)
ISLNAT(fst(V1)) → U611(isPLNatKind(V1), V1)
U621(tt, V1) → ISPLNAT(V1)
ISPLNAT(pair(V1, V2)) → U2411(isLNatKind(V1), V1, V2)
U2411(tt, V1, V2) → U2421(isLNatKind(V1), V1, V2)
U2421(tt, V1, V2) → U2431(isLNatKind(V2), V1, V2)
U2431(tt, V1, V2) → U2441(isLNatKind(V2), V1, V2)
U2451(tt, V2) → ISLNAT(V2)
U721(tt, V1) → ISNATURAL(V1)
U1821(tt, V1) → ISLNAT(V1)
ISLNAT(snd(V1)) → U811(isPLNatKind(V1), V1)
U821(tt, V1) → ISPLNAT(V1)
ISPLNAT(splitAt(V1, V2)) → U2511(isNaturalKind(V1), V1, V2)
U2521(tt, V1, V2) → U2531(isLNatKind(V2), V1, V2)
U2531(tt, V1, V2) → U2541(isLNatKind(V2), V1, V2)
U2541(tt, V1, V2) → U2551(isNatural(V1), V2)
U2551(tt, V2) → ISLNAT(V2)
U2541(tt, V1, V2) → ISNATURAL(V1)
U1911(tt, V1) → U1921(isNaturalKind(V1), V1)
U2011(tt, V1, V2) → U2021(isNaturalKind(V1), V1, V2)
U2021(tt, V1, V2) → U2031(isLNatKind(V2), V1, V2)
U2051(tt, V2) → ISLNAT(V2)
U441(tt, V1, V2) → ISNATURAL(V1)
U1041(tt, V1, V2) → ISNATURAL(V1)

could only be oriented weakly and must be analyzed further.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSUsableRulesProof
              ↳ QCSDP
                ↳ QCSDPReductionPairProof
                  ↳ QCSDP
                    ↳ QCSDependencyGraphProof
          ↳ QCSDP
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {afterNth, head, U211, s, U221, sel, U232, fst, U131, pair, natsFrom, U141, snd, U151, splitAt, U272, tail, U161, take, U172, U262, U122, U112, U183, U193, U206, U56, U63, U73, U83, U256, U93, U106, U246, U46} are replacing on all positions.
For all symbols f in {U111, cons, U121, U231, U261, U271, U171, U181, U182, U41, U42, U43, U44, U45, U191, U192, U201, U202, U203, U204, U205, U51, U52, U53, U54, U55, U61, U62, U241, U242, U243, U244, U245, U71, U72, U81, U82, U251, U252, U253, U254, U255, U91, U92, U101, U102, U103, U104, U105, U1031, U1021, U1041, U1051, U441, U431, U451, U521, U511, U531, U541, U611, U621, U2411, U2421, U2431, U2441, U2451, U721, U1821, U811, U821, U2511, U2531, U2521, U2541, U2551, U1921, U1911, U2021, U2011, U2031, U2051} we have µ(f) = {1}.
The symbols in {isLNatKind, isNaturalKind, isPLNatKind, isNatural, isLNat, isPLNat, ISLNAT, ISPLNAT, ISNATURAL} are not replacing on any position.

The TRS P consists of the following rules:

U1021(tt, V1, V2) → U1031(isLNatKind(V2), V1, V2)
U1031(tt, V1, V2) → U1041(isLNatKind(V2), V1, V2)
U1041(tt, V1, V2) → U1051(isNatural(V1), V2)
U1051(tt, V2) → ISLNAT(V2)
U431(tt, V1, V2) → U441(isLNatKind(V2), V1, V2)
U441(tt, V1, V2) → U451(isNatural(V1), V2)
U451(tt, V2) → ISLNAT(V2)
U511(tt, V1, V2) → U521(isNaturalKind(V1), V1, V2)
U521(tt, V1, V2) → U531(isLNatKind(V2), V1, V2)
U531(tt, V1, V2) → U541(isLNatKind(V2), V1, V2)
ISLNAT(fst(V1)) → U611(isPLNatKind(V1), V1)
U621(tt, V1) → ISPLNAT(V1)
ISPLNAT(pair(V1, V2)) → U2411(isLNatKind(V1), V1, V2)
U2411(tt, V1, V2) → U2421(isLNatKind(V1), V1, V2)
U2421(tt, V1, V2) → U2431(isLNatKind(V2), V1, V2)
U2431(tt, V1, V2) → U2441(isLNatKind(V2), V1, V2)
U2451(tt, V2) → ISLNAT(V2)
U721(tt, V1) → ISNATURAL(V1)
U1821(tt, V1) → ISLNAT(V1)
ISLNAT(snd(V1)) → U811(isPLNatKind(V1), V1)
U821(tt, V1) → ISPLNAT(V1)
ISPLNAT(splitAt(V1, V2)) → U2511(isNaturalKind(V1), V1, V2)
U2521(tt, V1, V2) → U2531(isLNatKind(V2), V1, V2)
U2531(tt, V1, V2) → U2541(isLNatKind(V2), V1, V2)
U2541(tt, V1, V2) → U2551(isNatural(V1), V2)
U2551(tt, V2) → ISLNAT(V2)
U2541(tt, V1, V2) → ISNATURAL(V1)
U1911(tt, V1) → U1921(isNaturalKind(V1), V1)
U2011(tt, V1, V2) → U2021(isNaturalKind(V1), V1, V2)
U2021(tt, V1, V2) → U2031(isLNatKind(V2), V1, V2)
U2051(tt, V2) → ISLNAT(V2)
U441(tt, V1, V2) → ISNATURAL(V1)
U1041(tt, V1, V2) → ISNATURAL(V1)

The TRS R consists of the following rules:

isLNatKind(nil) → tt
isLNatKind(afterNth(V1, V2)) → U111(isNaturalKind(V1), V2)
isNaturalKind(0) → tt
isNaturalKind(head(V1)) → U211(isLNatKind(V1))
isLNatKind(cons(V1, V2)) → U121(isNaturalKind(V1), V2)
isNaturalKind(s(V1)) → U221(isNaturalKind(V1))
isNaturalKind(sel(V1, V2)) → U231(isNaturalKind(V1), V2)
U231(tt, V2) → U232(isLNatKind(V2))
isLNatKind(fst(V1)) → U131(isPLNatKind(V1))
isPLNatKind(pair(V1, V2)) → U261(isLNatKind(V1), V2)
isLNatKind(natsFrom(V1)) → U141(isNaturalKind(V1))
U141(tt) → tt
isLNatKind(snd(V1)) → U151(isPLNatKind(V1))
isPLNatKind(splitAt(V1, V2)) → U271(isNaturalKind(V1), V2)
U271(tt, V2) → U272(isLNatKind(V2))
isLNatKind(tail(V1)) → U161(isLNatKind(V1))
isLNatKind(take(V1, V2)) → U171(isNaturalKind(V1), V2)
U171(tt, V2) → U172(isLNatKind(V2))
U172(tt) → tt
U161(tt) → tt
U272(tt) → tt
U151(tt) → tt
U261(tt, V2) → U262(isLNatKind(V2))
U262(tt) → tt
U131(tt) → tt
U232(tt) → tt
U221(tt) → tt
U121(tt, V2) → U122(isLNatKind(V2))
U122(tt) → tt
U211(tt) → tt
U111(tt, V2) → U112(isLNatKind(V2))
U112(tt) → tt
isNatural(0) → tt
isNatural(head(V1)) → U181(isLNatKind(V1), V1)
U181(tt, V1) → U182(isLNatKind(V1), V1)
U182(tt, V1) → U183(isLNat(V1))
isLNat(nil) → tt
isLNat(afterNth(V1, V2)) → U41(isNaturalKind(V1), V1, V2)
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)
isNatural(s(V1)) → U191(isNaturalKind(V1), V1)
U191(tt, V1) → U192(isNaturalKind(V1), V1)
U192(tt, V1) → U193(isNatural(V1))
isNatural(sel(V1, V2)) → U201(isNaturalKind(V1), V1, V2)
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))
isLNat(cons(V1, V2)) → U51(isNaturalKind(V1), V1, V2)
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))
isLNat(fst(V1)) → U61(isPLNatKind(V1), V1)
U61(tt, V1) → U62(isPLNatKind(V1), V1)
U62(tt, V1) → U63(isPLNat(V1))
isPLNat(pair(V1, V2)) → U241(isLNatKind(V1), V1, V2)
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)
isLNat(natsFrom(V1)) → U71(isNaturalKind(V1), V1)
U71(tt, V1) → U72(isNaturalKind(V1), V1)
U72(tt, V1) → U73(isNatural(V1))
U73(tt) → tt
isLNat(snd(V1)) → U81(isPLNatKind(V1), V1)
U81(tt, V1) → U82(isPLNatKind(V1), V1)
U82(tt, V1) → U83(isPLNat(V1))
isPLNat(splitAt(V1, V2)) → U251(isNaturalKind(V1), V1, V2)
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))
isLNat(tail(V1)) → U91(isLNatKind(V1), V1)
U91(tt, V1) → U92(isLNatKind(V1), V1)
U92(tt, V1) → U93(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNaturalKind(V1), V1, V2)
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
U93(tt) → tt
U256(tt) → tt
U83(tt) → tt
U245(tt, V2) → U246(isLNat(V2))
U246(tt) → tt
U63(tt) → tt
U56(tt) → tt
U206(tt) → tt
U193(tt) → tt
U45(tt, V2) → U46(isLNat(V2))
U46(tt) → tt
U183(tt) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 31 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U106, U112, U122, U131, snd, splitAt, U141, U151, U161, U172, U183, U193, U206, U211, U221, U232, U246, U256, U262, U272, natsFrom, s, head, afterNth, pair, fst, U46, U56, U63, U73, U83, U93, tail, take, sel, NATSFROM} are replacing on all positions.
For all symbols f in {U101, U102, U103, U104, U105, U11, U12, U111, U13, U121, U14, U171, U181, U182, U191, U192, U201, U202, U203, U204, U205, U21, U22, U23, U24, U231, U241, U242, U243, U244, U245, U251, U252, U253, U254, U255, U261, U271, U281, U282, cons, U291, U292, U293, U294, U301, U302, U303, U304, U31, U32, U311, U312, U33, U321, U322, U323, U324, U325, U326, U327, U34, U331, U332, U333, U334, U341, U342, U343, U344, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U81, U82, U91, U92, U2811, U2821} we have µ(f) = {1}.
The symbols in {isNaturalKind, isLNatKind, isNatural, isLNat, isPLNatKind, isPLNat, U} are not replacing on any position.

The TRS P consists of the following rules:

NATSFROM(N) → U2811(isNatural(N), N)
U2811(tt, N) → U2821(isNaturalKind(N), N)
U2821(tt, N) → U(N)
U(s(x_0)) → U(x_0)
U(natsFrom(x_0)) → U(x_0)
U(natsFrom(s(N))) → NATSFROM(s(N))

The TRS R consists of the following 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)

Q is empty.

We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


U(s(x_0)) → U(x_0)
U(natsFrom(x_0)) → U(x_0)
U(natsFrom(s(N))) → NATSFROM(s(N))
The remaining pairs can at least be oriented weakly.

NATSFROM(N) → U2811(isNatural(N), N)
U2811(tt, N) → U2821(isNaturalKind(N), N)
U2821(tt, N) → U(N)
Used ordering: Combined order from the following AFS and order.
U2811(x1, x2)  =  x2
NATSFROM(x1)  =  x1
U2821(x1, x2)  =  x2
U(x1)  =  x1

Subterm Order


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
              ↳ QCSDP
                ↳ QCSDependencyGraphProof
          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {U106, U112, U122, U131, snd, splitAt, U141, U151, U161, U172, U183, U193, U206, U211, U221, U232, U246, U256, U262, U272, natsFrom, s, head, afterNth, pair, fst, U46, U56, U63, U73, U83, U93, tail, take, sel, NATSFROM} are replacing on all positions.
For all symbols f in {U101, U102, U103, U104, U105, U11, U12, U111, U13, U121, U14, U171, U181, U182, U191, U192, U201, U202, U203, U204, U205, U21, U22, U23, U24, U231, U241, U242, U243, U244, U245, U251, U252, U253, U254, U255, U261, U271, U281, U282, cons, U291, U292, U293, U294, U301, U302, U303, U304, U31, U32, U311, U312, U33, U321, U322, U323, U324, U325, U326, U327, U34, U331, U332, U333, U334, U341, U342, U343, U344, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U81, U82, U91, U92, U2811, U2821} we have µ(f) = {1}.
The symbols in {isNaturalKind, isLNatKind, isNatural, isLNat, isPLNatKind, isPLNat, U} are not replacing on any position.

The TRS P consists of the following rules:

NATSFROM(N) → U2811(isNatural(N), N)
U2811(tt, N) → U2821(isNaturalKind(N), N)
U2821(tt, N) → U(N)

The TRS R consists of the following 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)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 3 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U106, U112, U122, U131, snd, splitAt, U141, U151, U161, U172, U183, U193, U206, U211, U221, U232, U246, U256, U262, U272, natsFrom, s, head, afterNth, pair, fst, U46, U56, U63, U73, U83, U93, tail, take, sel, SPLITAT} are replacing on all positions.
For all symbols f in {U101, U102, U103, U104, U105, U11, U12, U111, U13, U121, U14, U171, U181, U182, U191, U192, U201, U202, U203, U204, U205, U21, U22, U23, U24, U231, U241, U242, U243, U244, U245, U251, U252, U253, U254, U255, U261, U271, U281, U282, cons, U291, U292, U293, U294, U301, U302, U303, U304, U31, U32, U311, U312, U33, U321, U322, U323, U324, U325, U326, U327, U34, U331, U332, U333, U334, U341, U342, U343, U344, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U81, U82, U91, U92, U3251, U3241, U3261, U3211, U3221, U3231} we have µ(f) = {1}.
The symbols in {isNaturalKind, isLNatKind, isNatural, isLNat, isPLNatKind, isPLNat} are not replacing on any position.

The TRS P consists of the following rules:

U3241(tt, N, X, XS) → U3251(isLNat(XS), N, X, XS)
U3251(tt, N, X, XS) → U3261(isLNatKind(XS), N, X, XS)
U3261(tt, N, X, XS) → SPLITAT(N, XS)
SPLITAT(s(N), cons(X, XS)) → U3211(isNatural(N), N, X, XS)
U3211(tt, N, X, XS) → U3221(isNaturalKind(N), N, X, XS)
U3221(tt, N, X, XS) → U3231(isNatural(X), N, X, XS)
U3231(tt, N, X, XS) → U3241(isNaturalKind(X), N, X, XS)

The TRS R consists of the following 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)

Q is empty.

We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


SPLITAT(s(N), cons(X, XS)) → U3211(isNatural(N), N, X, XS)
The remaining pairs can at least be oriented weakly.

U3241(tt, N, X, XS) → U3251(isLNat(XS), N, X, XS)
U3251(tt, N, X, XS) → U3261(isLNatKind(XS), N, X, XS)
U3261(tt, N, X, XS) → SPLITAT(N, XS)
U3211(tt, N, X, XS) → U3221(isNaturalKind(N), N, X, XS)
U3221(tt, N, X, XS) → U3231(isNatural(X), N, X, XS)
U3231(tt, N, X, XS) → U3241(isNaturalKind(X), N, X, XS)
Used ordering: Combined order from the following AFS and order.
U3251(x1, x2, x3, x4)  =  x2
U3241(x1, x2, x3, x4)  =  x2
U3261(x1, x2, x3, x4)  =  x2
SPLITAT(x1, x2)  =  x1
U3211(x1, x2, x3, x4)  =  x2
U3221(x1, x2, x3, x4)  =  x2
U3231(x1, x2, x3, x4)  =  x2

Subterm Order


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ AND
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
          ↳ QCSDP
            ↳ QCSDPSubtermProof
              ↳ QCSDP
                ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {U106, U112, U122, U131, snd, splitAt, U141, U151, U161, U172, U183, U193, U206, U211, U221, U232, U246, U256, U262, U272, natsFrom, s, head, afterNth, pair, fst, U46, U56, U63, U73, U83, U93, tail, take, sel, SPLITAT} are replacing on all positions.
For all symbols f in {U101, U102, U103, U104, U105, U11, U12, U111, U13, U121, U14, U171, U181, U182, U191, U192, U201, U202, U203, U204, U205, U21, U22, U23, U24, U231, U241, U242, U243, U244, U245, U251, U252, U253, U254, U255, U261, U271, U281, U282, cons, U291, U292, U293, U294, U301, U302, U303, U304, U31, U32, U311, U312, U33, U321, U322, U323, U324, U325, U326, U327, U34, U331, U332, U333, U334, U341, U342, U343, U344, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U81, U82, U91, U92, U3251, U3241, U3261, U3221, U3211, U3231} we have µ(f) = {1}.
The symbols in {isNaturalKind, isLNatKind, isNatural, isLNat, isPLNatKind, isPLNat} are not replacing on any position.

The TRS P consists of the following rules:

U3241(tt, N, X, XS) → U3251(isLNat(XS), N, X, XS)
U3251(tt, N, X, XS) → U3261(isLNatKind(XS), N, X, XS)
U3261(tt, N, X, XS) → SPLITAT(N, XS)
U3211(tt, N, X, XS) → U3221(isNaturalKind(N), N, X, XS)
U3221(tt, N, X, XS) → U3231(isNatural(X), N, X, XS)
U3231(tt, N, X, XS) → U3241(isNaturalKind(X), N, X, XS)

The TRS R consists of the following 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)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 6 less nodes.