Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U11(tt, N, XS) → U12(isLNat(XS), N, XS)
U111(tt) → tt
U12(tt, N, XS) → snd(splitAt(N, XS))
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U161(tt, N) → cons(N, natsFrom(s(N)))
U171(tt, N, XS) → U172(isLNat(XS), N, XS)
U172(tt, N, XS) → head(afterNth(N, XS))
U181(tt, Y) → U182(isLNat(Y), Y)
U182(tt, Y) → Y
U191(tt, XS) → pair(nil, XS)
U201(tt, N, X, XS) → U202(isNatural(X), N, X, XS)
U202(tt, N, X, XS) → U203(isLNat(XS), N, X, XS)
U203(tt, N, X, XS) → U204(splitAt(N, XS), X)
U204(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U21(tt, X, Y) → U22(isLNat(Y), X)
U211(tt, XS) → U212(isLNat(XS), XS)
U212(tt, XS) → XS
U22(tt, X) → X
U221(tt, N, XS) → U222(isLNat(XS), N, XS)
U222(tt, N, XS) → fst(splitAt(N, XS))
U31(tt, N, XS) → U32(isLNat(XS), N)
U32(tt, N) → N
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(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(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
natsFrom(N) → U161(isNatural(N), N)
sel(N, XS) → U171(isNatural(N), N, XS)
snd(pair(X, Y)) → U181(isLNat(X), Y)
splitAt(0, XS) → U191(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U201(isNatural(N), N, X, XS)
tail(cons(N, XS)) → U211(isNatural(N), XS)
take(N, XS) → U221(isNatural(N), N, XS)

The replacement map contains the following entries:

U101: {1}
tt: empty set
U102: {1}
isLNat: empty set
U11: {1}
U12: {1}
U111: {1}
snd: {1}
splitAt: {1, 2}
U121: {1}
U131: {1}
U132: {1}
U141: {1}
U142: {1}
U151: {1}
U152: {1}
U161: {1}
cons: {1}
natsFrom: {1}
s: {1}
U171: {1}
U172: {1}
head: {1}
afterNth: {1, 2}
U181: {1}
U182: {1}
U191: {1}
pair: {1, 2}
nil: empty set
U201: {1}
U202: {1}
isNatural: empty set
U203: {1}
U204: {1}
U21: {1}
U22: {1}
U211: {1}
U212: {1}
U221: {1}
U222: {1}
fst: {1}
U31: {1}
U32: {1}
U41: {1}
U42: {1}
U51: {1}
U52: {1}
U61: {1}
U71: {1}
U81: {1}
U91: {1}
isPLNat: empty set
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, V2) → U102(isLNat(V2))
U102(tt) → tt
U11(tt, N, XS) → U12(isLNat(XS), N, XS)
U111(tt) → tt
U12(tt, N, XS) → snd(splitAt(N, XS))
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U161(tt, N) → cons(N, natsFrom(s(N)))
U171(tt, N, XS) → U172(isLNat(XS), N, XS)
U172(tt, N, XS) → head(afterNth(N, XS))
U181(tt, Y) → U182(isLNat(Y), Y)
U182(tt, Y) → Y
U191(tt, XS) → pair(nil, XS)
U201(tt, N, X, XS) → U202(isNatural(X), N, X, XS)
U202(tt, N, X, XS) → U203(isLNat(XS), N, X, XS)
U203(tt, N, X, XS) → U204(splitAt(N, XS), X)
U204(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U21(tt, X, Y) → U22(isLNat(Y), X)
U211(tt, XS) → U212(isLNat(XS), XS)
U212(tt, XS) → XS
U22(tt, X) → X
U221(tt, N, XS) → U222(isLNat(XS), N, XS)
U222(tt, N, XS) → fst(splitAt(N, XS))
U31(tt, N, XS) → U32(isLNat(XS), N)
U32(tt, N) → N
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(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(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
natsFrom(N) → U161(isNatural(N), N)
sel(N, XS) → U171(isNatural(N), N, XS)
snd(pair(X, Y)) → U181(isLNat(X), Y)
splitAt(0, XS) → U191(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U201(isNatural(N), N, X, XS)
tail(cons(N, XS)) → U211(isNatural(N), XS)
take(N, XS) → U221(isNatural(N), N, XS)

The replacement map contains the following entries:

U101: {1}
tt: empty set
U102: {1}
isLNat: empty set
U11: {1}
U12: {1}
U111: {1}
snd: {1}
splitAt: {1, 2}
U121: {1}
U131: {1}
U132: {1}
U141: {1}
U142: {1}
U151: {1}
U152: {1}
U161: {1}
cons: {1}
natsFrom: {1}
s: {1}
U171: {1}
U172: {1}
head: {1}
afterNth: {1, 2}
U181: {1}
U182: {1}
U191: {1}
pair: {1, 2}
nil: empty set
U201: {1}
U202: {1}
isNatural: empty set
U203: {1}
U204: {1}
U21: {1}
U22: {1}
U211: {1}
U212: {1}
U221: {1}
U222: {1}
fst: {1}
U31: {1}
U32: {1}
U41: {1}
U42: {1}
U51: {1}
U52: {1}
U61: {1}
U71: {1}
U81: {1}
U91: {1}
isPLNat: empty set
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 {U102, U111, snd, splitAt, U121, U132, U142, U152, natsFrom, s, head, afterNth, pair, fst, U42, U52, U61, U71, U81, U91, tail, take, sel, U1021, SND, SPLITAT, U1321, U1421, U1521, HEAD, AFTERNTH, FST, U421, U521, U611, U711, U811, U911, U1111, U1211, NATSFROM, SEL, TAIL, TAKE} are replacing on all positions.
For all symbols f in {U101, U11, U12, U131, U141, U151, U161, cons, U171, U172, U181, U182, U191, U201, U202, U203, U204, U21, U22, U211, U212, U221, U222, U31, U32, U41, U51, U1011, U121, U111, U1311, U1411, U1511, U1721, U1711, U1821, U1811, U2021, U2011, U2031, U2041, U221, U211, U2121, U2111, U2221, U2211, U321, U311, U411, U511, U1611, U1911} we have µ(f) = {1}.
The symbols in {isLNat, isNatural, isPLNat, ISLNAT, ISNATURAL, ISPLNAT, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DPo are:

U1011(tt, V2) → U1021(isLNat(V2))
U1011(tt, V2) → ISLNAT(V2)
U111(tt, N, XS) → U121(isLNat(XS), N, XS)
U111(tt, N, XS) → ISLNAT(XS)
U121(tt, N, XS) → SND(splitAt(N, XS))
U121(tt, N, XS) → SPLITAT(N, XS)
U1311(tt, V2) → U1321(isLNat(V2))
U1311(tt, V2) → ISLNAT(V2)
U1411(tt, V2) → U1421(isLNat(V2))
U1411(tt, V2) → ISLNAT(V2)
U1511(tt, V2) → U1521(isLNat(V2))
U1511(tt, V2) → ISLNAT(V2)
U1711(tt, N, XS) → U1721(isLNat(XS), N, XS)
U1711(tt, N, XS) → ISLNAT(XS)
U1721(tt, N, XS) → HEAD(afterNth(N, XS))
U1721(tt, N, XS) → AFTERNTH(N, XS)
U1811(tt, Y) → U1821(isLNat(Y), Y)
U1811(tt, Y) → ISLNAT(Y)
U2011(tt, N, X, XS) → U2021(isNatural(X), N, X, XS)
U2011(tt, N, X, XS) → ISNATURAL(X)
U2021(tt, N, X, XS) → U2031(isLNat(XS), N, X, XS)
U2021(tt, N, X, XS) → ISLNAT(XS)
U2031(tt, N, X, XS) → U2041(splitAt(N, XS), X)
U2031(tt, N, X, XS) → SPLITAT(N, XS)
U211(tt, X, Y) → U221(isLNat(Y), X)
U211(tt, X, Y) → ISLNAT(Y)
U2111(tt, XS) → U2121(isLNat(XS), XS)
U2111(tt, XS) → ISLNAT(XS)
U2211(tt, N, XS) → U2221(isLNat(XS), N, XS)
U2211(tt, N, XS) → ISLNAT(XS)
U2221(tt, N, XS) → FST(splitAt(N, XS))
U2221(tt, N, XS) → SPLITAT(N, XS)
U311(tt, N, XS) → U321(isLNat(XS), N)
U311(tt, N, XS) → ISLNAT(XS)
U411(tt, V2) → U421(isLNat(V2))
U411(tt, V2) → ISLNAT(V2)
U511(tt, V2) → U521(isLNat(V2))
U511(tt, V2) → ISLNAT(V2)
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(isNatural(V1), V2)
ISLNAT(afterNth(V1, V2)) → ISNATURAL(V1)
ISLNAT(cons(V1, V2)) → U511(isNatural(V1), V2)
ISLNAT(cons(V1, V2)) → ISNATURAL(V1)
ISLNAT(fst(V1)) → U611(isPLNat(V1))
ISLNAT(fst(V1)) → ISPLNAT(V1)
ISLNAT(natsFrom(V1)) → U711(isNatural(V1))
ISLNAT(natsFrom(V1)) → ISNATURAL(V1)
ISLNAT(snd(V1)) → U811(isPLNat(V1))
ISLNAT(snd(V1)) → ISPLNAT(V1)
ISLNAT(tail(V1)) → U911(isLNat(V1))
ISLNAT(tail(V1)) → ISLNAT(V1)
ISLNAT(take(V1, V2)) → U1011(isNatural(V1), V2)
ISLNAT(take(V1, V2)) → ISNATURAL(V1)
ISNATURAL(head(V1)) → U1111(isLNat(V1))
ISNATURAL(head(V1)) → ISLNAT(V1)
ISNATURAL(s(V1)) → U1211(isNatural(V1))
ISNATURAL(s(V1)) → ISNATURAL(V1)
ISNATURAL(sel(V1, V2)) → U1311(isNatural(V1), V2)
ISNATURAL(sel(V1, V2)) → ISNATURAL(V1)
ISPLNAT(pair(V1, V2)) → U1411(isLNat(V1), V2)
ISPLNAT(pair(V1, V2)) → ISLNAT(V1)
ISPLNAT(splitAt(V1, V2)) → U1511(isNatural(V1), V2)
ISPLNAT(splitAt(V1, V2)) → ISNATURAL(V1)
NATSFROM(N) → U1611(isNatural(N), N)
NATSFROM(N) → ISNATURAL(N)
SEL(N, XS) → U1711(isNatural(N), N, XS)
SEL(N, XS) → ISNATURAL(N)
SND(pair(X, Y)) → U1811(isLNat(X), Y)
SND(pair(X, Y)) → ISLNAT(X)
SPLITAT(0, XS) → U1911(isLNat(XS), XS)
SPLITAT(0, XS) → ISLNAT(XS)
SPLITAT(s(N), cons(X, XS)) → U2011(isNatural(N), N, X, XS)
SPLITAT(s(N), cons(X, XS)) → ISNATURAL(N)
TAIL(cons(N, XS)) → U2111(isNatural(N), XS)
TAIL(cons(N, XS)) → ISNATURAL(N)
TAKE(N, XS) → U2211(isNatural(N), N, XS)
TAKE(N, XS) → ISNATURAL(N)

The collapsing dependency pairs are DPc:

U121(tt, N, XS) → N
U121(tt, N, XS) → XS
U1611(tt, N) → N
U1721(tt, N, XS) → N
U1721(tt, N, XS) → XS
U1821(tt, Y) → Y
U1911(tt, XS) → XS
U2031(tt, N, X, XS) → N
U2031(tt, N, X, XS) → XS
U2041(pair(YS, ZS), X) → X
U2121(tt, XS) → XS
U221(tt, X) → X
U2221(tt, N, XS) → N
U2221(tt, N, XS) → XS
U321(tt, N) → N


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 :

U121(tt, N, XS) → U(N)
U121(tt, N, XS) → U(XS)
U1611(tt, N) → U(N)
U1721(tt, N, XS) → U(N)
U1721(tt, N, XS) → U(XS)
U1821(tt, Y) → U(Y)
U1911(tt, XS) → U(XS)
U2031(tt, N, X, XS) → U(N)
U2031(tt, N, X, XS) → U(XS)
U2041(pair(YS, ZS), X) → U(X)
U2121(tt, XS) → U(XS)
U221(tt, X) → U(X)
U2221(tt, N, XS) → U(N)
U2221(tt, N, XS) → U(XS)
U321(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, V2) → U102(isLNat(V2))
U102(tt) → tt
U11(tt, N, XS) → U12(isLNat(XS), N, XS)
U111(tt) → tt
U12(tt, N, XS) → snd(splitAt(N, XS))
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U161(tt, N) → cons(N, natsFrom(s(N)))
U171(tt, N, XS) → U172(isLNat(XS), N, XS)
U172(tt, N, XS) → head(afterNth(N, XS))
U181(tt, Y) → U182(isLNat(Y), Y)
U182(tt, Y) → Y
U191(tt, XS) → pair(nil, XS)
U201(tt, N, X, XS) → U202(isNatural(X), N, X, XS)
U202(tt, N, X, XS) → U203(isLNat(XS), N, X, XS)
U203(tt, N, X, XS) → U204(splitAt(N, XS), X)
U204(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U21(tt, X, Y) → U22(isLNat(Y), X)
U211(tt, XS) → U212(isLNat(XS), XS)
U212(tt, XS) → XS
U22(tt, X) → X
U221(tt, N, XS) → U222(isLNat(XS), N, XS)
U222(tt, N, XS) → fst(splitAt(N, XS))
U31(tt, N, XS) → U32(isLNat(XS), N)
U32(tt, N) → N
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(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(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
natsFrom(N) → U161(isNatural(N), N)
sel(N, XS) → U171(isNatural(N), N, XS)
snd(pair(X, Y)) → U181(isLNat(X), Y)
splitAt(0, XS) → U191(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U201(isNatural(N), N, X, XS)
tail(cons(N, XS)) → U211(isNatural(N), XS)
take(N, XS) → U221(isNatural(N), N, XS)

Q is empty.

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


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {U102, U111, snd, splitAt, U121, U132, U142, U152, natsFrom, s, head, afterNth, pair, fst, U42, U52, U61, U71, U81, U91, tail, take, sel} are replacing on all positions.
For all symbols f in {U101, U11, U12, U131, U141, U151, U161, cons, U171, U172, U181, U182, U191, U201, U202, U203, U204, U21, U22, U211, U212, U221, U222, U31, U32, U41, U51, U411, U511, U1311, U1411, U1011, U1511} we have µ(f) = {1}.
The symbols in {isLNat, isNatural, isPLNat, ISLNAT, ISNATURAL, ISPLNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISLNAT(afterNth(V1, V2)) → U411(isNatural(V1), V2)
U411(tt, V2) → ISLNAT(V2)
ISLNAT(afterNth(V1, V2)) → ISNATURAL(V1)
ISNATURAL(head(V1)) → ISLNAT(V1)
ISLNAT(cons(V1, V2)) → U511(isNatural(V1), V2)
U511(tt, V2) → ISLNAT(V2)
ISLNAT(cons(V1, V2)) → ISNATURAL(V1)
ISNATURAL(s(V1)) → ISNATURAL(V1)
ISNATURAL(sel(V1, V2)) → U1311(isNatural(V1), V2)
U1311(tt, V2) → ISLNAT(V2)
ISLNAT(fst(V1)) → ISPLNAT(V1)
ISPLNAT(pair(V1, V2)) → U1411(isLNat(V1), V2)
U1411(tt, V2) → ISLNAT(V2)
ISLNAT(natsFrom(V1)) → ISNATURAL(V1)
ISNATURAL(sel(V1, V2)) → ISNATURAL(V1)
ISLNAT(snd(V1)) → ISPLNAT(V1)
ISPLNAT(pair(V1, V2)) → ISLNAT(V1)
ISLNAT(tail(V1)) → ISLNAT(V1)
ISLNAT(take(V1, V2)) → U1011(isNatural(V1), V2)
U1011(tt, V2) → ISLNAT(V2)
ISLNAT(take(V1, V2)) → ISNATURAL(V1)
ISPLNAT(splitAt(V1, V2)) → U1511(isNatural(V1), V2)
U1511(tt, V2) → ISLNAT(V2)
ISPLNAT(splitAt(V1, V2)) → ISNATURAL(V1)

The TRS R consists of the following rules:

U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U11(tt, N, XS) → U12(isLNat(XS), N, XS)
U111(tt) → tt
U12(tt, N, XS) → snd(splitAt(N, XS))
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U161(tt, N) → cons(N, natsFrom(s(N)))
U171(tt, N, XS) → U172(isLNat(XS), N, XS)
U172(tt, N, XS) → head(afterNth(N, XS))
U181(tt, Y) → U182(isLNat(Y), Y)
U182(tt, Y) → Y
U191(tt, XS) → pair(nil, XS)
U201(tt, N, X, XS) → U202(isNatural(X), N, X, XS)
U202(tt, N, X, XS) → U203(isLNat(XS), N, X, XS)
U203(tt, N, X, XS) → U204(splitAt(N, XS), X)
U204(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U21(tt, X, Y) → U22(isLNat(Y), X)
U211(tt, XS) → U212(isLNat(XS), XS)
U212(tt, XS) → XS
U22(tt, X) → X
U221(tt, N, XS) → U222(isLNat(XS), N, XS)
U222(tt, N, XS) → fst(splitAt(N, XS))
U31(tt, N, XS) → U32(isLNat(XS), N)
U32(tt, N) → N
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(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(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
natsFrom(N) → U161(isNatural(N), N)
sel(N, XS) → U171(isNatural(N), N, XS)
snd(pair(X, Y)) → U181(isLNat(X), Y)
splitAt(0, XS) → U191(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U201(isNatural(N), N, X, XS)
tail(cons(N, XS)) → U211(isNatural(N), XS)
take(N, XS) → U221(isNatural(N), N, XS)

Q is empty.

The following rules are not useable and can be deleted:

U11(tt, x0, x1) → U12(isLNat(x1), x0, x1)
U12(tt, x0, x1) → snd(splitAt(x0, x1))
U161(tt, x0) → cons(x0, natsFrom(s(x0)))
U171(tt, x0, x1) → U172(isLNat(x1), x0, x1)
U172(tt, x0, x1) → head(afterNth(x0, x1))
U181(tt, x0) → U182(isLNat(x0), x0)
U182(tt, x0) → x0
U191(tt, x0) → pair(nil, x0)
U201(tt, x0, x1, x2) → U202(isNatural(x1), x0, x1, x2)
U202(tt, x0, x1, x2) → U203(isLNat(x2), x0, x1, x2)
U203(tt, x0, x1, x2) → U204(splitAt(x0, x2), x1)
U204(pair(x0, x1), x2) → pair(cons(x2, x0), x1)
U21(tt, x0, x1) → U22(isLNat(x1), x0)
U211(tt, x0) → U212(isLNat(x0), x0)
U212(tt, x0) → x0
U22(tt, x0) → x0
U221(tt, x0, x1) → U222(isLNat(x1), x0, x1)
U222(tt, x0, x1) → fst(splitAt(x0, x1))
U31(tt, x0, x1) → U32(isLNat(x1), x0)
U32(tt, x0) → x0
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) → U161(isNatural(x0), x0)
sel(x0, x1) → U171(isNatural(x0), x0, x1)
snd(pair(x0, x1)) → U181(isLNat(x0), x1)
splitAt(0, x0) → U191(isLNat(x0), x0)
splitAt(s(x0), cons(x1, x2)) → U201(isNatural(x0), x0, x1, x2)
tail(cons(x0, x1)) → U211(isNatural(x0), x1)
take(x0, x1) → U221(isNatural(x0), x0, x1)


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {head, U111, afterNth, s, U121, sel, U132, U52, fst, U61, pair, natsFrom, U71, snd, U81, splitAt, U152, tail, U91, take, U102, U142, U42} are replacing on all positions.
For all symbols f in {U41, U131, cons, U51, U141, U151, U101, U411, U511, U1311, U1411, U1011, U1511} we have µ(f) = {1}.
The symbols in {isNatural, isLNat, isPLNat, ISLNAT, ISNATURAL, ISPLNAT} are not replacing on any position.

The TRS P consists of the following rules:

ISLNAT(afterNth(V1, V2)) → U411(isNatural(V1), V2)
U411(tt, V2) → ISLNAT(V2)
ISLNAT(afterNth(V1, V2)) → ISNATURAL(V1)
ISNATURAL(head(V1)) → ISLNAT(V1)
ISLNAT(cons(V1, V2)) → U511(isNatural(V1), V2)
U511(tt, V2) → ISLNAT(V2)
ISLNAT(cons(V1, V2)) → ISNATURAL(V1)
ISNATURAL(s(V1)) → ISNATURAL(V1)
ISNATURAL(sel(V1, V2)) → U1311(isNatural(V1), V2)
U1311(tt, V2) → ISLNAT(V2)
ISLNAT(fst(V1)) → ISPLNAT(V1)
ISPLNAT(pair(V1, V2)) → U1411(isLNat(V1), V2)
U1411(tt, V2) → ISLNAT(V2)
ISLNAT(natsFrom(V1)) → ISNATURAL(V1)
ISNATURAL(sel(V1, V2)) → ISNATURAL(V1)
ISLNAT(snd(V1)) → ISPLNAT(V1)
ISPLNAT(pair(V1, V2)) → ISLNAT(V1)
ISLNAT(tail(V1)) → ISLNAT(V1)
ISLNAT(take(V1, V2)) → U1011(isNatural(V1), V2)
U1011(tt, V2) → ISLNAT(V2)
ISLNAT(take(V1, V2)) → ISNATURAL(V1)
ISPLNAT(splitAt(V1, V2)) → U1511(isNatural(V1), V2)
U1511(tt, V2) → ISLNAT(V2)
ISPLNAT(splitAt(V1, V2)) → ISNATURAL(V1)

The TRS R consists of the following rules:

isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isLNat(nil) → tt
isLNat(afterNth(V1, V2)) → U41(isNatural(V1), V2)
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
U131(tt, V2) → U132(isLNat(V2))
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
U51(tt, V2) → U52(isLNat(V2))
isLNat(fst(V1)) → U61(isPLNat(V1))
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isLNat(natsFrom(V1)) → U71(isNatural(V1))
U71(tt) → tt
isLNat(snd(V1)) → U81(isPLNat(V1))
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
U151(tt, V2) → U152(isLNat(V2))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U91(tt) → tt
U152(tt) → tt
U81(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U61(tt) → tt
U52(tt) → tt
U132(tt) → tt
U121(tt) → tt
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U111(tt) → tt

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 0   
POL(ISLNAT(x1)) = 2·x1   
POL(ISNATURAL(x1)) = x1   
POL(ISPLNAT(x1)) = 2 + x1   
POL(U101(x1, x2)) = 0   
POL(U1011(x1, x2)) = 2·x2   
POL(U102(x1)) = x1   
POL(U111(x1)) = x1   
POL(U121(x1)) = x1   
POL(U131(x1, x2)) = 2·x1   
POL(U1311(x1, x2)) = 2·x2   
POL(U132(x1)) = 0   
POL(U141(x1, x2)) = 2 + x1   
POL(U1411(x1, x2)) = 1 + 2·x2   
POL(U142(x1)) = 1   
POL(U151(x1, x2)) = 2 + x1   
POL(U1511(x1, x2)) = 1 + 2·x2   
POL(U152(x1)) = 1   
POL(U41(x1, x2)) = 2·x1   
POL(U411(x1, x2)) = 2·x2   
POL(U42(x1)) = x1   
POL(U51(x1, x2)) = 0   
POL(U511(x1, x2)) = 2·x2   
POL(U52(x1)) = 0   
POL(U61(x1)) = 0   
POL(U71(x1)) = x1   
POL(U81(x1)) = 0   
POL(U91(x1)) = 2·x1   
POL(afterNth(x1, x2)) = x1 + 2·x2   
POL(cons(x1, x2)) = 2·x1 + x2   
POL(fst(x1)) = 2 + 2·x1   
POL(head(x1)) = 2·x1   
POL(isLNat(x1)) = 0   
POL(isNatural(x1)) = 0   
POL(isPLNat(x1)) = 2   
POL(natsFrom(x1)) = 2 + 2·x1   
POL(nil) = 2   
POL(pair(x1, x2)) = 2·x1 + 2·x2   
POL(s(x1)) = 1 + 2·x1   
POL(sel(x1, x2)) = x1 + 2·x2   
POL(snd(x1)) = 2 + 2·x1   
POL(splitAt(x1, x2)) = x1 + 2·x2   
POL(tail(x1)) = 1 + x1   
POL(take(x1, x2)) = 2·x1 + x2   
POL(tt) = 0   

the following usable rules

isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
U111(tt) → tt
isLNat(nil) → tt
isLNat(afterNth(V1, V2)) → U41(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt) → tt
U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(tt) → tt

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

ISNATURAL(s(V1)) → ISNATURAL(V1)
ISLNAT(fst(V1)) → ISPLNAT(V1)
ISPLNAT(pair(V1, V2)) → U1411(isLNat(V1), V2)
U1411(tt, V2) → ISLNAT(V2)
ISLNAT(natsFrom(V1)) → ISNATURAL(V1)
ISLNAT(snd(V1)) → ISPLNAT(V1)
ISPLNAT(pair(V1, V2)) → ISLNAT(V1)
ISLNAT(tail(V1)) → ISLNAT(V1)
ISPLNAT(splitAt(V1, V2)) → U1511(isNatural(V1), V2)
U1511(tt, V2) → ISLNAT(V2)
ISPLNAT(splitAt(V1, V2)) → ISNATURAL(V1)

could be oriented strictly and thus removed.
The pairs

ISLNAT(afterNth(V1, V2)) → U411(isNatural(V1), V2)
U411(tt, V2) → ISLNAT(V2)
ISLNAT(afterNth(V1, V2)) → ISNATURAL(V1)
ISNATURAL(head(V1)) → ISLNAT(V1)
ISLNAT(cons(V1, V2)) → U511(isNatural(V1), V2)
U511(tt, V2) → ISLNAT(V2)
ISLNAT(cons(V1, V2)) → ISNATURAL(V1)
ISNATURAL(sel(V1, V2)) → U1311(isNatural(V1), V2)
U1311(tt, V2) → ISLNAT(V2)
ISNATURAL(sel(V1, V2)) → ISNATURAL(V1)
ISLNAT(take(V1, V2)) → U1011(isNatural(V1), V2)
U1011(tt, V2) → ISLNAT(V2)
ISLNAT(take(V1, V2)) → ISNATURAL(V1)

could only be oriented weakly and must be analyzed further.


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {head, U111, afterNth, s, U121, sel, U132, U52, fst, U61, pair, natsFrom, U71, snd, U81, splitAt, U152, tail, U91, take, U102, U142, U42} are replacing on all positions.
For all symbols f in {U41, U131, cons, U51, U141, U151, U101, U411, U511, U1311, U1011} we have µ(f) = {1}.
The symbols in {isNatural, isLNat, isPLNat, ISLNAT, ISNATURAL} are not replacing on any position.

The TRS P consists of the following rules:

ISLNAT(afterNth(V1, V2)) → U411(isNatural(V1), V2)
U411(tt, V2) → ISLNAT(V2)
ISLNAT(afterNth(V1, V2)) → ISNATURAL(V1)
ISNATURAL(head(V1)) → ISLNAT(V1)
ISLNAT(cons(V1, V2)) → U511(isNatural(V1), V2)
U511(tt, V2) → ISLNAT(V2)
ISLNAT(cons(V1, V2)) → ISNATURAL(V1)
ISNATURAL(sel(V1, V2)) → U1311(isNatural(V1), V2)
U1311(tt, V2) → ISLNAT(V2)
ISNATURAL(sel(V1, V2)) → ISNATURAL(V1)
ISLNAT(take(V1, V2)) → U1011(isNatural(V1), V2)
U1011(tt, V2) → ISLNAT(V2)
ISLNAT(take(V1, V2)) → ISNATURAL(V1)

The TRS R consists of the following rules:

isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isLNat(nil) → tt
isLNat(afterNth(V1, V2)) → U41(isNatural(V1), V2)
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
U131(tt, V2) → U132(isLNat(V2))
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
U51(tt, V2) → U52(isLNat(V2))
isLNat(fst(V1)) → U61(isPLNat(V1))
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isLNat(natsFrom(V1)) → U71(isNatural(V1))
U71(tt) → tt
isLNat(snd(V1)) → U81(isPLNat(V1))
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
U151(tt, V2) → U152(isLNat(V2))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U91(tt) → tt
U152(tt) → tt
U81(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U61(tt) → tt
U52(tt) → tt
U132(tt) → tt
U121(tt) → tt
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U111(tt) → tt

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(0) = 2   
POL(ISLNAT(x1)) = x1   
POL(ISNATURAL(x1)) = 2·x1   
POL(U101(x1, x2)) = 2   
POL(U1011(x1, x2)) = 2·x2   
POL(U102(x1)) = 0   
POL(U111(x1)) = 0   
POL(U121(x1)) = 2·x1   
POL(U131(x1, x2)) = 0   
POL(U1311(x1, x2)) = 1 + 2·x2   
POL(U132(x1)) = 0   
POL(U141(x1, x2)) = 2·x2   
POL(U142(x1)) = 0   
POL(U151(x1, x2)) = 1 + 2·x1   
POL(U152(x1)) = 0   
POL(U41(x1, x2)) = 1   
POL(U411(x1, x2)) = x2   
POL(U42(x1)) = 0   
POL(U51(x1, x2)) = 1   
POL(U511(x1, x2)) = 2·x2   
POL(U52(x1)) = 0   
POL(U61(x1)) = 2   
POL(U71(x1)) = x1   
POL(U81(x1)) = 0   
POL(U91(x1)) = x1   
POL(afterNth(x1, x2)) = 2·x1 + x2   
POL(cons(x1, x2)) = 2·x1 + 2·x2   
POL(fst(x1)) = 2 + x1   
POL(head(x1)) = 2·x1   
POL(isLNat(x1)) = 2   
POL(isNatural(x1)) = 0   
POL(isPLNat(x1)) = 2·x1   
POL(natsFrom(x1)) = 2   
POL(nil) = 1   
POL(pair(x1, x2)) = 2·x2   
POL(s(x1)) = 1 + x1   
POL(sel(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(snd(x1)) = 1 + x1   
POL(splitAt(x1, x2)) = 2 + x2   
POL(tail(x1)) = 2 + 2·x1   
POL(take(x1, x2)) = 2·x1 + 2·x2   
POL(tt) = 0   

the following usable rules

isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
U111(tt) → tt
isLNat(nil) → tt
isLNat(afterNth(V1, V2)) → U41(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt) → tt
U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(tt) → tt

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

ISNATURAL(sel(V1, V2)) → U1311(isNatural(V1), V2)
U1311(tt, V2) → ISLNAT(V2)
ISNATURAL(sel(V1, V2)) → ISNATURAL(V1)

could be oriented strictly and thus removed.
The pairs

ISLNAT(afterNth(V1, V2)) → U411(isNatural(V1), V2)
U411(tt, V2) → ISLNAT(V2)
ISLNAT(afterNth(V1, V2)) → ISNATURAL(V1)
ISNATURAL(head(V1)) → ISLNAT(V1)
ISLNAT(cons(V1, V2)) → U511(isNatural(V1), V2)
U511(tt, V2) → ISLNAT(V2)
ISLNAT(cons(V1, V2)) → ISNATURAL(V1)
ISLNAT(take(V1, V2)) → U1011(isNatural(V1), V2)
U1011(tt, V2) → ISLNAT(V2)
ISLNAT(take(V1, V2)) → ISNATURAL(V1)

could only be oriented weakly and must be analyzed further.


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {head, U111, afterNth, s, U121, sel, U132, U52, fst, U61, pair, natsFrom, U71, snd, U81, splitAt, U152, tail, U91, take, U102, U142, U42} are replacing on all positions.
For all symbols f in {U41, U131, cons, U51, U141, U151, U101, U411, U511, U1011} we have µ(f) = {1}.
The symbols in {isNatural, isLNat, isPLNat, ISLNAT, ISNATURAL} are not replacing on any position.

The TRS P consists of the following rules:

ISLNAT(afterNth(V1, V2)) → U411(isNatural(V1), V2)
U411(tt, V2) → ISLNAT(V2)
ISLNAT(afterNth(V1, V2)) → ISNATURAL(V1)
ISNATURAL(head(V1)) → ISLNAT(V1)
ISLNAT(cons(V1, V2)) → U511(isNatural(V1), V2)
U511(tt, V2) → ISLNAT(V2)
ISLNAT(cons(V1, V2)) → ISNATURAL(V1)
ISLNAT(take(V1, V2)) → U1011(isNatural(V1), V2)
U1011(tt, V2) → ISLNAT(V2)
ISLNAT(take(V1, V2)) → ISNATURAL(V1)

The TRS R consists of the following rules:

isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isLNat(nil) → tt
isLNat(afterNth(V1, V2)) → U41(isNatural(V1), V2)
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
U131(tt, V2) → U132(isLNat(V2))
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
U51(tt, V2) → U52(isLNat(V2))
isLNat(fst(V1)) → U61(isPLNat(V1))
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isLNat(natsFrom(V1)) → U71(isNatural(V1))
U71(tt) → tt
isLNat(snd(V1)) → U81(isPLNat(V1))
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
U151(tt, V2) → U152(isLNat(V2))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U91(tt) → tt
U152(tt) → tt
U81(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U61(tt) → tt
U52(tt) → tt
U132(tt) → tt
U121(tt) → tt
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U111(tt) → tt

Q is empty.

Using the order
Polynomial Order [21,25] with Interpretation:

POL( sel(x1, x2) ) = x1 + x2 + 2


POL( U142(x1) ) = max{0, -1}


POL( U511(x1, x2) ) = 2x2 + 1


POL( U102(x1) ) = 1


POL( U81(x1) ) = 1


POL( U1011(x1, x2) ) = 2x2 + 2


POL( take(x1, x2) ) = 2x1 + x2 + 2


POL( splitAt(x1, x2) ) = x1 + x2 + 2


POL( U51(x1, x2) ) = x2 + 1


POL( U131(x1, x2) ) = x2 + 1


POL( isPLNat(x1) ) = 2x1 + 1


POL( isNatural(x1) ) = max{0, 2x1 - 1}


POL( tt ) = max{0, -1}


POL( U52(x1) ) = max{0, -1}


POL( U91(x1) ) = 1


POL( U101(x1, x2) ) = 1


POL( pair(x1, x2) ) = x1 + 2x2 + 1


POL( s(x1) ) = 0


POL( U151(x1, x2) ) = max{0, -1}


POL( U152(x1) ) = max{0, -1}


POL( U111(x1) ) = 1


POL( U71(x1) ) = max{0, -1}


POL( natsFrom(x1) ) = x1 + 1


POL( nil ) = 2


POL( tail(x1) ) = 2x1 + 2


POL( afterNth(x1, x2) ) = x1 + 2x2 + 2


POL( snd(x1) ) = x1 + 2


POL( U61(x1) ) = max{0, -1}


POL( U121(x1) ) = max{0, -1}


POL( U141(x1, x2) ) = max{0, x1 - 1}


POL( head(x1) ) = 2x1 + 2


POL( ISNATURAL(x1) ) = max{0, x1 - 1}


POL( 0 ) = max{0, -1}


POL( cons(x1, x2) ) = x1 + 2x2 + 2


POL( U411(x1, x2) ) = 2x2 + 1


POL( U41(x1, x2) ) = max{0, -1}


POL( U42(x1) ) = max{0, -1}


POL( ISLNAT(x1) ) = 2x1 + 1


POL( fst(x1) ) = 2x1 + 1


POL( isLNat(x1) ) = max{0, x1 - 1}


POL( U132(x1) ) = max{0, -1}



the following usable rules

isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
U111(tt) → tt
isLNat(nil) → tt
isLNat(afterNth(V1, V2)) → U41(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(tt) → tt
U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(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(isNatural(V1), V2)
ISLNAT(afterNth(V1, V2)) → ISNATURAL(V1)
ISLNAT(cons(V1, V2)) → U511(isNatural(V1), V2)
ISLNAT(cons(V1, V2)) → ISNATURAL(V1)
ISLNAT(take(V1, V2)) → U1011(isNatural(V1), V2)
U1011(tt, V2) → ISLNAT(V2)
ISLNAT(take(V1, V2)) → ISNATURAL(V1)

could be oriented strictly and thus removed.
The pairs

U411(tt, V2) → ISLNAT(V2)
ISNATURAL(head(V1)) → ISLNAT(V1)
U511(tt, V2) → ISLNAT(V2)

could only be oriented weakly and must be analyzed further.


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {head, U111, afterNth, s, U121, sel, U132, U52, fst, U61, pair, natsFrom, U71, snd, U81, splitAt, U152, tail, U91, take, U102, U142, U42} are replacing on all positions.
For all symbols f in {U41, U131, cons, U51, U141, U151, U101, U411, U511} we have µ(f) = {1}.
The symbols in {isNatural, isLNat, isPLNat, ISLNAT, ISNATURAL} are not replacing on any position.

The TRS P consists of the following rules:

U411(tt, V2) → ISLNAT(V2)
ISNATURAL(head(V1)) → ISLNAT(V1)
U511(tt, V2) → ISLNAT(V2)

The TRS R consists of the following rules:

isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isLNat(nil) → tt
isLNat(afterNth(V1, V2)) → U41(isNatural(V1), V2)
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
U131(tt, V2) → U132(isLNat(V2))
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
U51(tt, V2) → U52(isLNat(V2))
isLNat(fst(V1)) → U61(isPLNat(V1))
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isLNat(natsFrom(V1)) → U71(isNatural(V1))
U71(tt) → tt
isLNat(snd(V1)) → U81(isPLNat(V1))
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
U151(tt, V2) → U152(isLNat(V2))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U91(tt) → tt
U152(tt) → tt
U81(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U61(tt) → tt
U52(tt) → tt
U132(tt) → tt
U121(tt) → tt
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U111(tt) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs.


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {U102, U111, snd, splitAt, U121, U132, U142, U152, natsFrom, s, head, afterNth, pair, fst, U42, U52, U61, U71, U81, U91, tail, take, sel, NATSFROM} are replacing on all positions.
For all symbols f in {U101, U11, U12, U131, U141, U151, U161, cons, U171, U172, U181, U182, U191, U201, U202, U203, U204, U21, U22, U211, U212, U221, U222, U31, U32, U41, U51, U1611} we have µ(f) = {1}.
The symbols in {isLNat, isNatural, isPLNat, U} are not replacing on any position.

The TRS P consists of the following rules:

NATSFROM(N) → U1611(isNatural(N), N)
U1611(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, V2) → U102(isLNat(V2))
U102(tt) → tt
U11(tt, N, XS) → U12(isLNat(XS), N, XS)
U111(tt) → tt
U12(tt, N, XS) → snd(splitAt(N, XS))
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U161(tt, N) → cons(N, natsFrom(s(N)))
U171(tt, N, XS) → U172(isLNat(XS), N, XS)
U172(tt, N, XS) → head(afterNth(N, XS))
U181(tt, Y) → U182(isLNat(Y), Y)
U182(tt, Y) → Y
U191(tt, XS) → pair(nil, XS)
U201(tt, N, X, XS) → U202(isNatural(X), N, X, XS)
U202(tt, N, X, XS) → U203(isLNat(XS), N, X, XS)
U203(tt, N, X, XS) → U204(splitAt(N, XS), X)
U204(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U21(tt, X, Y) → U22(isLNat(Y), X)
U211(tt, XS) → U212(isLNat(XS), XS)
U212(tt, XS) → XS
U22(tt, X) → X
U221(tt, N, XS) → U222(isLNat(XS), N, XS)
U222(tt, N, XS) → fst(splitAt(N, XS))
U31(tt, N, XS) → U32(isLNat(XS), N)
U32(tt, N) → N
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(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(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
natsFrom(N) → U161(isNatural(N), N)
sel(N, XS) → U171(isNatural(N), N, XS)
snd(pair(X, Y)) → U181(isLNat(X), Y)
splitAt(0, XS) → U191(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U201(isNatural(N), N, X, XS)
tail(cons(N, XS)) → U211(isNatural(N), XS)
take(N, XS) → U221(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) → U1611(isNatural(N), N)
U1611(tt, N) → U(N)
Used ordering: Combined order from the following AFS and order.
U1611(x1, x2)  =  x2
NATSFROM(x1)  =  x1
U(x1)  =  x1

Subterm Order


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {U102, U111, snd, splitAt, U121, U132, U142, U152, natsFrom, s, head, afterNth, pair, fst, U42, U52, U61, U71, U81, U91, tail, take, sel, NATSFROM} are replacing on all positions.
For all symbols f in {U101, U11, U12, U131, U141, U151, U161, cons, U171, U172, U181, U182, U191, U201, U202, U203, U204, U21, U22, U211, U212, U221, U222, U31, U32, U41, U51, U1611} we have µ(f) = {1}.
The symbols in {isLNat, isNatural, isPLNat, U} are not replacing on any position.

The TRS P consists of the following rules:

NATSFROM(N) → U1611(isNatural(N), N)
U1611(tt, N) → U(N)

The TRS R consists of the following rules:

U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U11(tt, N, XS) → U12(isLNat(XS), N, XS)
U111(tt) → tt
U12(tt, N, XS) → snd(splitAt(N, XS))
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U161(tt, N) → cons(N, natsFrom(s(N)))
U171(tt, N, XS) → U172(isLNat(XS), N, XS)
U172(tt, N, XS) → head(afterNth(N, XS))
U181(tt, Y) → U182(isLNat(Y), Y)
U182(tt, Y) → Y
U191(tt, XS) → pair(nil, XS)
U201(tt, N, X, XS) → U202(isNatural(X), N, X, XS)
U202(tt, N, X, XS) → U203(isLNat(XS), N, X, XS)
U203(tt, N, X, XS) → U204(splitAt(N, XS), X)
U204(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U21(tt, X, Y) → U22(isLNat(Y), X)
U211(tt, XS) → U212(isLNat(XS), XS)
U212(tt, XS) → XS
U22(tt, X) → X
U221(tt, N, XS) → U222(isLNat(XS), N, XS)
U222(tt, N, XS) → fst(splitAt(N, XS))
U31(tt, N, XS) → U32(isLNat(XS), N)
U32(tt, N) → N
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(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(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
natsFrom(N) → U161(isNatural(N), N)
sel(N, XS) → U171(isNatural(N), N, XS)
snd(pair(X, Y)) → U181(isLNat(X), Y)
splitAt(0, XS) → U191(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U201(isNatural(N), N, X, XS)
tail(cons(N, XS)) → U211(isNatural(N), XS)
take(N, XS) → U221(isNatural(N), N, XS)

Q is empty.

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


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {U102, U111, snd, splitAt, U121, U132, U142, U152, natsFrom, s, head, afterNth, pair, fst, U42, U52, U61, U71, U81, U91, tail, take, sel, SPLITAT} are replacing on all positions.
For all symbols f in {U101, U11, U12, U131, U141, U151, U161, cons, U171, U172, U181, U182, U191, U201, U202, U203, U204, U21, U22, U211, U212, U221, U222, U31, U32, U41, U51, U2021, U2011, U2031} we have µ(f) = {1}.
The symbols in {isLNat, isNatural, isPLNat} are not replacing on any position.

The TRS P consists of the following rules:

U2011(tt, N, X, XS) → U2021(isNatural(X), N, X, XS)
U2021(tt, N, X, XS) → U2031(isLNat(XS), N, X, XS)
U2031(tt, N, X, XS) → SPLITAT(N, XS)
SPLITAT(s(N), cons(X, XS)) → U2011(isNatural(N), N, X, XS)

The TRS R consists of the following rules:

U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U11(tt, N, XS) → U12(isLNat(XS), N, XS)
U111(tt) → tt
U12(tt, N, XS) → snd(splitAt(N, XS))
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U161(tt, N) → cons(N, natsFrom(s(N)))
U171(tt, N, XS) → U172(isLNat(XS), N, XS)
U172(tt, N, XS) → head(afterNth(N, XS))
U181(tt, Y) → U182(isLNat(Y), Y)
U182(tt, Y) → Y
U191(tt, XS) → pair(nil, XS)
U201(tt, N, X, XS) → U202(isNatural(X), N, X, XS)
U202(tt, N, X, XS) → U203(isLNat(XS), N, X, XS)
U203(tt, N, X, XS) → U204(splitAt(N, XS), X)
U204(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U21(tt, X, Y) → U22(isLNat(Y), X)
U211(tt, XS) → U212(isLNat(XS), XS)
U212(tt, XS) → XS
U22(tt, X) → X
U221(tt, N, XS) → U222(isLNat(XS), N, XS)
U222(tt, N, XS) → fst(splitAt(N, XS))
U31(tt, N, XS) → U32(isLNat(XS), N)
U32(tt, N) → N
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(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(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
natsFrom(N) → U161(isNatural(N), N)
sel(N, XS) → U171(isNatural(N), N, XS)
snd(pair(X, Y)) → U181(isLNat(X), Y)
splitAt(0, XS) → U191(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U201(isNatural(N), N, X, XS)
tail(cons(N, XS)) → U211(isNatural(N), XS)
take(N, XS) → U221(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)) → U2011(isNatural(N), N, X, XS)
The remaining pairs can at least be oriented weakly.

U2011(tt, N, X, XS) → U2021(isNatural(X), N, X, XS)
U2021(tt, N, X, XS) → U2031(isLNat(XS), N, X, XS)
U2031(tt, N, X, XS) → SPLITAT(N, XS)
Used ordering: Combined order from the following AFS and order.
U2021(x1, x2, x3, x4)  =  x2
U2011(x1, x2, x3, x4)  =  x2
U2031(x1, x2, x3, x4)  =  x2
SPLITAT(x1, x2)  =  x1

Subterm Order


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

Q-restricted context-sensitive dependency pair problem:
The symbols in {U102, U111, snd, splitAt, U121, U132, U142, U152, natsFrom, s, head, afterNth, pair, fst, U42, U52, U61, U71, U81, U91, tail, take, sel, SPLITAT} are replacing on all positions.
For all symbols f in {U101, U11, U12, U131, U141, U151, U161, cons, U171, U172, U181, U182, U191, U201, U202, U203, U204, U21, U22, U211, U212, U221, U222, U31, U32, U41, U51, U2021, U2011, U2031} we have µ(f) = {1}.
The symbols in {isLNat, isNatural, isPLNat} are not replacing on any position.

The TRS P consists of the following rules:

U2011(tt, N, X, XS) → U2021(isNatural(X), N, X, XS)
U2021(tt, N, X, XS) → U2031(isLNat(XS), N, X, XS)
U2031(tt, N, X, XS) → SPLITAT(N, XS)

The TRS R consists of the following rules:

U101(tt, V2) → U102(isLNat(V2))
U102(tt) → tt
U11(tt, N, XS) → U12(isLNat(XS), N, XS)
U111(tt) → tt
U12(tt, N, XS) → snd(splitAt(N, XS))
U121(tt) → tt
U131(tt, V2) → U132(isLNat(V2))
U132(tt) → tt
U141(tt, V2) → U142(isLNat(V2))
U142(tt) → tt
U151(tt, V2) → U152(isLNat(V2))
U152(tt) → tt
U161(tt, N) → cons(N, natsFrom(s(N)))
U171(tt, N, XS) → U172(isLNat(XS), N, XS)
U172(tt, N, XS) → head(afterNth(N, XS))
U181(tt, Y) → U182(isLNat(Y), Y)
U182(tt, Y) → Y
U191(tt, XS) → pair(nil, XS)
U201(tt, N, X, XS) → U202(isNatural(X), N, X, XS)
U202(tt, N, X, XS) → U203(isLNat(XS), N, X, XS)
U203(tt, N, X, XS) → U204(splitAt(N, XS), X)
U204(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U21(tt, X, Y) → U22(isLNat(Y), X)
U211(tt, XS) → U212(isLNat(XS), XS)
U212(tt, XS) → XS
U22(tt, X) → X
U221(tt, N, XS) → U222(isLNat(XS), N, XS)
U222(tt, N, XS) → fst(splitAt(N, XS))
U31(tt, N, XS) → U32(isLNat(XS), N)
U32(tt, N) → N
U41(tt, V2) → U42(isLNat(V2))
U42(tt) → tt
U51(tt, V2) → U52(isLNat(V2))
U52(tt) → tt
U61(tt) → tt
U71(tt) → tt
U81(tt) → tt
U91(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(isNatural(V1), V2)
isLNat(cons(V1, V2)) → U51(isNatural(V1), V2)
isLNat(fst(V1)) → U61(isPLNat(V1))
isLNat(natsFrom(V1)) → U71(isNatural(V1))
isLNat(snd(V1)) → U81(isPLNat(V1))
isLNat(tail(V1)) → U91(isLNat(V1))
isLNat(take(V1, V2)) → U101(isNatural(V1), V2)
isNatural(0) → tt
isNatural(head(V1)) → U111(isLNat(V1))
isNatural(s(V1)) → U121(isNatural(V1))
isNatural(sel(V1, V2)) → U131(isNatural(V1), V2)
isPLNat(pair(V1, V2)) → U141(isLNat(V1), V2)
isPLNat(splitAt(V1, V2)) → U151(isNatural(V1), V2)
natsFrom(N) → U161(isNatural(N), N)
sel(N, XS) → U171(isNatural(N), N, XS)
snd(pair(X, Y)) → U181(isLNat(X), Y)
splitAt(0, XS) → U191(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U201(isNatural(N), N, X, XS)
tail(cons(N, XS)) → U211(isNatural(N), XS)
take(N, XS) → U221(isNatural(N), N, XS)

Q is empty.

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