Termination w.r.t. Q proof of /tmp/tmpF8E4Wd/LISTUTILITIES_nokinds

Termination w.r.t. Q of the given QTRS could not be shown:

0 QTRS

↳1 DependencyPairsProof (⇔)

↳2 QDP

↳3 DependencyGraphProof (⇔)

↳4 QDP

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

U101(tt, N, XS) → fst(splitAt(activate(N), activate(XS)))
U11(tt, N, XS) → snd(splitAt(activate(N), activate(XS)))
U21(tt, X) → activate(X)
U31(tt, N) → activate(N)
U41(tt, N) → cons(activate(N), n__natsFrom(s(activate(N))))
U51(tt, N, XS) → head(afterNth(activate(N), activate(XS)))
U61(tt, Y) → activate(Y)
U71(tt, XS) → pair(nil, activate(XS))
U81(tt, N, X, XS) → U82(splitAt(activate(N), activate(XS)), activate(X))
U82(pair(YS, ZS), X) → pair(cons(activate(X), YS), ZS)
U91(tt, XS) → activate(XS)
afterNth(N, XS) → U11(and(isNatural(N), n__isLNat(XS)), N, XS)
and(tt, X) → activate(X)
fst(pair(X, Y)) → U21(and(isLNat(X), n__isLNat(Y)), X)
head(cons(N, XS)) → U31(and(isNatural(N), n__isLNat(activate(XS))), N)
isLNat(n__nil) → tt
isLNat(n__afterNth(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
isLNat(n__cons(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
isLNat(n__fst(V1)) → isPLNat(activate(V1))
isLNat(n__natsFrom(V1)) → isNatural(activate(V1))
isLNat(n__snd(V1)) → isPLNat(activate(V1))
isLNat(n__tail(V1)) → isLNat(activate(V1))
isLNat(n__take(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
isNatural(n__0) → tt
isNatural(n__head(V1)) → isLNat(activate(V1))
isNatural(n__s(V1)) → isNatural(activate(V1))
isNatural(n__sel(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
isPLNat(n__pair(V1, V2)) → and(isLNat(activate(V1)), n__isLNat(activate(V2)))
isPLNat(n__splitAt(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
natsFrom(N) → U41(isNatural(N), N)
sel(N, XS) → U51(and(isNatural(N), n__isLNat(XS)), N, XS)
snd(pair(X, Y)) → U61(and(isLNat(X), n__isLNat(Y)), Y)
splitAt(0, XS) → U71(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U81(and(isNatural(N), n__and(isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS))
tail(cons(N, XS)) → U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))
take(N, XS) → U101(and(isNatural(N), n__isLNat(XS)), N, XS)
natsFrom(X) → n__natsFrom(X)
isLNat(X) → n__isLNat(X)
nil → n__nil
afterNth(X1, X2) → n__afterNth(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
fst(X) → n__fst(X)
snd(X) → n__snd(X)
tail(X) → n__tail(X)
take(X1, X2) → n__take(X1, X2)
0 → n__0
head(X) → n__head(X)
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
pair(X1, X2) → n__pair(X1, X2)
splitAt(X1, X2) → n__splitAt(X1, X2)
and(X1, X2) → n__and(X1, X2)
activate(n__natsFrom(X)) → natsFrom(X)
activate(n__isLNat(X)) → isLNat(X)
activate(n__nil) → nil
activate(n__afterNth(X1, X2)) → afterNth(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__fst(X)) → fst(X)
activate(n__snd(X)) → snd(X)
activate(n__tail(X)) → tail(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__head(X)) → head(X)
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(n__pair(X1, X2)) → pair(X1, X2)
activate(n__splitAt(X1, X2)) → splitAt(X1, X2)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U101¹(tt, N, XS) → FST(splitAt(activate(N), activate(XS)))
U101¹(tt, N, XS) → SPLITAT(activate(N), activate(XS))
U101¹(tt, N, XS) → ACTIVATE(N)
U101¹(tt, N, XS) → ACTIVATE(XS)
U11¹(tt, N, XS) → SND(splitAt(activate(N), activate(XS)))
U11¹(tt, N, XS) → SPLITAT(activate(N), activate(XS))
U11¹(tt, N, XS) → ACTIVATE(N)
U11¹(tt, N, XS) → ACTIVATE(XS)
U21¹(tt, X) → ACTIVATE(X)
U31¹(tt, N) → ACTIVATE(N)
U41¹(tt, N) → CONS(activate(N), n__natsFrom(s(activate(N))))
U41¹(tt, N) → ACTIVATE(N)
U41¹(tt, N) → S(activate(N))
U51¹(tt, N, XS) → HEAD(afterNth(activate(N), activate(XS)))
U51¹(tt, N, XS) → AFTERNTH(activate(N), activate(XS))
U51¹(tt, N, XS) → ACTIVATE(N)
U51¹(tt, N, XS) → ACTIVATE(XS)
U61¹(tt, Y) → ACTIVATE(Y)
U71¹(tt, XS) → PAIR(nil, activate(XS))
U71¹(tt, XS) → NIL
U71¹(tt, XS) → ACTIVATE(XS)
U81¹(tt, N, X, XS) → U82¹(splitAt(activate(N), activate(XS)), activate(X))
U81¹(tt, N, X, XS) → SPLITAT(activate(N), activate(XS))
U81¹(tt, N, X, XS) → ACTIVATE(N)
U81¹(tt, N, X, XS) → ACTIVATE(XS)
U81¹(tt, N, X, XS) → ACTIVATE(X)
U82¹(pair(YS, ZS), X) → PAIR(cons(activate(X), YS), ZS)
U82¹(pair(YS, ZS), X) → CONS(activate(X), YS)
U82¹(pair(YS, ZS), X) → ACTIVATE(X)
U91¹(tt, XS) → ACTIVATE(XS)
AFTERNTH(N, XS) → U11¹(and(isNatural(N), n__isLNat(XS)), N, XS)
AFTERNTH(N, XS) → AND(isNatural(N), n__isLNat(XS))
AFTERNTH(N, XS) → ISNATURAL(N)
AND(tt, X) → ACTIVATE(X)
FST(pair(X, Y)) → U21¹(and(isLNat(X), n__isLNat(Y)), X)
FST(pair(X, Y)) → AND(isLNat(X), n__isLNat(Y))
FST(pair(X, Y)) → ISLNAT(X)
HEAD(cons(N, XS)) → U31¹(and(isNatural(N), n__isLNat(activate(XS))), N)
HEAD(cons(N, XS)) → AND(isNatural(N), n__isLNat(activate(XS)))
HEAD(cons(N, XS)) → ISNATURAL(N)
HEAD(cons(N, XS)) → ACTIVATE(XS)
ISLNAT(n__afterNth(V1, V2)) → AND(isNatural(activate(V1)), n__isLNat(activate(V2)))
ISLNAT(n__afterNth(V1, V2)) → ISNATURAL(activate(V1))
ISLNAT(n__afterNth(V1, V2)) → ACTIVATE(V1)
ISLNAT(n__afterNth(V1, V2)) → ACTIVATE(V2)
ISLNAT(n__cons(V1, V2)) → AND(isNatural(activate(V1)), n__isLNat(activate(V2)))
ISLNAT(n__cons(V1, V2)) → ISNATURAL(activate(V1))
ISLNAT(n__cons(V1, V2)) → ACTIVATE(V1)
ISLNAT(n__cons(V1, V2)) → ACTIVATE(V2)
ISLNAT(n__fst(V1)) → ISPLNAT(activate(V1))
ISLNAT(n__fst(V1)) → ACTIVATE(V1)
ISLNAT(n__natsFrom(V1)) → ISNATURAL(activate(V1))
ISLNAT(n__natsFrom(V1)) → ACTIVATE(V1)
ISLNAT(n__snd(V1)) → ISPLNAT(activate(V1))
ISLNAT(n__snd(V1)) → ACTIVATE(V1)
ISLNAT(n__tail(V1)) → ISLNAT(activate(V1))
ISLNAT(n__tail(V1)) → ACTIVATE(V1)
ISLNAT(n__take(V1, V2)) → AND(isNatural(activate(V1)), n__isLNat(activate(V2)))
ISLNAT(n__take(V1, V2)) → ISNATURAL(activate(V1))
ISLNAT(n__take(V1, V2)) → ACTIVATE(V1)
ISLNAT(n__take(V1, V2)) → ACTIVATE(V2)
ISNATURAL(n__head(V1)) → ISLNAT(activate(V1))
ISNATURAL(n__head(V1)) → ACTIVATE(V1)
ISNATURAL(n__s(V1)) → ISNATURAL(activate(V1))
ISNATURAL(n__s(V1)) → ACTIVATE(V1)
ISNATURAL(n__sel(V1, V2)) → AND(isNatural(activate(V1)), n__isLNat(activate(V2)))
ISNATURAL(n__sel(V1, V2)) → ISNATURAL(activate(V1))
ISNATURAL(n__sel(V1, V2)) → ACTIVATE(V1)
ISNATURAL(n__sel(V1, V2)) → ACTIVATE(V2)
ISPLNAT(n__pair(V1, V2)) → AND(isLNat(activate(V1)), n__isLNat(activate(V2)))
ISPLNAT(n__pair(V1, V2)) → ISLNAT(activate(V1))
ISPLNAT(n__pair(V1, V2)) → ACTIVATE(V1)
ISPLNAT(n__pair(V1, V2)) → ACTIVATE(V2)
ISPLNAT(n__splitAt(V1, V2)) → AND(isNatural(activate(V1)), n__isLNat(activate(V2)))
ISPLNAT(n__splitAt(V1, V2)) → ISNATURAL(activate(V1))
ISPLNAT(n__splitAt(V1, V2)) → ACTIVATE(V1)
ISPLNAT(n__splitAt(V1, V2)) → ACTIVATE(V2)
NATSFROM(N) → U41¹(isNatural(N), N)
NATSFROM(N) → ISNATURAL(N)
SEL(N, XS) → U51¹(and(isNatural(N), n__isLNat(XS)), N, XS)
SEL(N, XS) → AND(isNatural(N), n__isLNat(XS))
SEL(N, XS) → ISNATURAL(N)
SND(pair(X, Y)) → U61¹(and(isLNat(X), n__isLNat(Y)), Y)
SND(pair(X, Y)) → AND(isLNat(X), n__isLNat(Y))
SND(pair(X, Y)) → ISLNAT(X)
SPLITAT(0, XS) → U71¹(isLNat(XS), XS)
SPLITAT(0, XS) → ISLNAT(XS)
SPLITAT(s(N), cons(X, XS)) → U81¹(and(isNatural(N), n__and(isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS))
SPLITAT(s(N), cons(X, XS)) → AND(isNatural(N), n__and(isNatural(X), n__isLNat(activate(XS))))
SPLITAT(s(N), cons(X, XS)) → ISNATURAL(N)
SPLITAT(s(N), cons(X, XS)) → ISNATURAL(X)
SPLITAT(s(N), cons(X, XS)) → ACTIVATE(XS)
TAIL(cons(N, XS)) → U91¹(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))
TAIL(cons(N, XS)) → AND(isNatural(N), n__isLNat(activate(XS)))
TAIL(cons(N, XS)) → ISNATURAL(N)
TAIL(cons(N, XS)) → ACTIVATE(XS)
TAKE(N, XS) → U101¹(and(isNatural(N), n__isLNat(XS)), N, XS)
TAKE(N, XS) → AND(isNatural(N), n__isLNat(XS))
TAKE(N, XS) → ISNATURAL(N)
ACTIVATE(n__natsFrom(X)) → NATSFROM(X)
ACTIVATE(n__isLNat(X)) → ISLNAT(X)
ACTIVATE(n__nil) → NIL
ACTIVATE(n__afterNth(X1, X2)) → AFTERNTH(X1, X2)
ACTIVATE(n__cons(X1, X2)) → CONS(X1, X2)
ACTIVATE(n__fst(X)) → FST(X)
ACTIVATE(n__snd(X)) → SND(X)
ACTIVATE(n__tail(X)) → TAIL(X)
ACTIVATE(n__take(X1, X2)) → TAKE(X1, X2)
ACTIVATE(n__0) → 0¹
ACTIVATE(n__head(X)) → HEAD(X)
ACTIVATE(n__s(X)) → S(X)
ACTIVATE(n__sel(X1, X2)) → SEL(X1, X2)
ACTIVATE(n__pair(X1, X2)) → PAIR(X1, X2)
ACTIVATE(n__splitAt(X1, X2)) → SPLITAT(X1, X2)
ACTIVATE(n__and(X1, X2)) → AND(X1, X2)

The TRS R consists of the following rules:

U101(tt, N, XS) → fst(splitAt(activate(N), activate(XS)))
U11(tt, N, XS) → snd(splitAt(activate(N), activate(XS)))
U21(tt, X) → activate(X)
U31(tt, N) → activate(N)
U41(tt, N) → cons(activate(N), n__natsFrom(s(activate(N))))
U51(tt, N, XS) → head(afterNth(activate(N), activate(XS)))
U61(tt, Y) → activate(Y)
U71(tt, XS) → pair(nil, activate(XS))
U81(tt, N, X, XS) → U82(splitAt(activate(N), activate(XS)), activate(X))
U82(pair(YS, ZS), X) → pair(cons(activate(X), YS), ZS)
U91(tt, XS) → activate(XS)
afterNth(N, XS) → U11(and(isNatural(N), n__isLNat(XS)), N, XS)
and(tt, X) → activate(X)
fst(pair(X, Y)) → U21(and(isLNat(X), n__isLNat(Y)), X)
head(cons(N, XS)) → U31(and(isNatural(N), n__isLNat(activate(XS))), N)
isLNat(n__nil) → tt
isLNat(n__afterNth(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
isLNat(n__cons(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
isLNat(n__fst(V1)) → isPLNat(activate(V1))
isLNat(n__natsFrom(V1)) → isNatural(activate(V1))
isLNat(n__snd(V1)) → isPLNat(activate(V1))
isLNat(n__tail(V1)) → isLNat(activate(V1))
isLNat(n__take(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
isNatural(n__0) → tt
isNatural(n__head(V1)) → isLNat(activate(V1))
isNatural(n__s(V1)) → isNatural(activate(V1))
isNatural(n__sel(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
isPLNat(n__pair(V1, V2)) → and(isLNat(activate(V1)), n__isLNat(activate(V2)))
isPLNat(n__splitAt(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
natsFrom(N) → U41(isNatural(N), N)
sel(N, XS) → U51(and(isNatural(N), n__isLNat(XS)), N, XS)
snd(pair(X, Y)) → U61(and(isLNat(X), n__isLNat(Y)), Y)
splitAt(0, XS) → U71(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U81(and(isNatural(N), n__and(isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS))
tail(cons(N, XS)) → U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))
take(N, XS) → U101(and(isNatural(N), n__isLNat(XS)), N, XS)
natsFrom(X) → n__natsFrom(X)
isLNat(X) → n__isLNat(X)
nil → n__nil
afterNth(X1, X2) → n__afterNth(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
fst(X) → n__fst(X)
snd(X) → n__snd(X)
tail(X) → n__tail(X)
take(X1, X2) → n__take(X1, X2)
0 → n__0
head(X) → n__head(X)
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
pair(X1, X2) → n__pair(X1, X2)
splitAt(X1, X2) → n__splitAt(X1, X2)
and(X1, X2) → n__and(X1, X2)
activate(n__natsFrom(X)) → natsFrom(X)
activate(n__isLNat(X)) → isLNat(X)
activate(n__nil) → nil
activate(n__afterNth(X1, X2)) → afterNth(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__fst(X)) → fst(X)
activate(n__snd(X)) → snd(X)
activate(n__tail(X)) → tail(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__head(X)) → head(X)
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(n__pair(X1, X2)) → pair(X1, X2)
activate(n__splitAt(X1, X2)) → splitAt(X1, X2)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 11 less nodes.

(4) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FST(pair(X, Y)) → U21¹(and(isLNat(X), n__isLNat(Y)), X)
U21¹(tt, X) → ACTIVATE(X)
ACTIVATE(n__natsFrom(X)) → NATSFROM(X)
NATSFROM(N) → U41¹(isNatural(N), N)
U41¹(tt, N) → ACTIVATE(N)
ACTIVATE(n__isLNat(X)) → ISLNAT(X)
ISLNAT(n__afterNth(V1, V2)) → AND(isNatural(activate(V1)), n__isLNat(activate(V2)))
AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__afterNth(X1, X2)) → AFTERNTH(X1, X2)
AFTERNTH(N, XS) → U11¹(and(isNatural(N), n__isLNat(XS)), N, XS)
U11¹(tt, N, XS) → SND(splitAt(activate(N), activate(XS)))
SND(pair(X, Y)) → U61¹(and(isLNat(X), n__isLNat(Y)), Y)
U61¹(tt, Y) → ACTIVATE(Y)
ACTIVATE(n__fst(X)) → FST(X)
FST(pair(X, Y)) → AND(isLNat(X), n__isLNat(Y))
FST(pair(X, Y)) → ISLNAT(X)
ISLNAT(n__afterNth(V1, V2)) → ISNATURAL(activate(V1))
ISNATURAL(n__head(V1)) → ISLNAT(activate(V1))
ISLNAT(n__afterNth(V1, V2)) → ACTIVATE(V1)
ACTIVATE(n__snd(X)) → SND(X)
SND(pair(X, Y)) → AND(isLNat(X), n__isLNat(Y))
SND(pair(X, Y)) → ISLNAT(X)
ISLNAT(n__afterNth(V1, V2)) → ACTIVATE(V2)
ACTIVATE(n__tail(X)) → TAIL(X)
TAIL(cons(N, XS)) → U91¹(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))
U91¹(tt, XS) → ACTIVATE(XS)
ACTIVATE(n__take(X1, X2)) → TAKE(X1, X2)
TAKE(N, XS) → U101¹(and(isNatural(N), n__isLNat(XS)), N, XS)
U101¹(tt, N, XS) → FST(splitAt(activate(N), activate(XS)))
U101¹(tt, N, XS) → SPLITAT(activate(N), activate(XS))
SPLITAT(0, XS) → U71¹(isLNat(XS), XS)
U71¹(tt, XS) → ACTIVATE(XS)
ACTIVATE(n__head(X)) → HEAD(X)
HEAD(cons(N, XS)) → U31¹(and(isNatural(N), n__isLNat(activate(XS))), N)
U31¹(tt, N) → ACTIVATE(N)
ACTIVATE(n__sel(X1, X2)) → SEL(X1, X2)
SEL(N, XS) → U51¹(and(isNatural(N), n__isLNat(XS)), N, XS)
U51¹(tt, N, XS) → HEAD(afterNth(activate(N), activate(XS)))
HEAD(cons(N, XS)) → AND(isNatural(N), n__isLNat(activate(XS)))
HEAD(cons(N, XS)) → ISNATURAL(N)
ISNATURAL(n__head(V1)) → ACTIVATE(V1)
ACTIVATE(n__splitAt(X1, X2)) → SPLITAT(X1, X2)
SPLITAT(0, XS) → ISLNAT(XS)
ISLNAT(n__cons(V1, V2)) → AND(isNatural(activate(V1)), n__isLNat(activate(V2)))
ISLNAT(n__cons(V1, V2)) → ISNATURAL(activate(V1))
ISNATURAL(n__s(V1)) → ISNATURAL(activate(V1))
ISNATURAL(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__and(X1, X2)) → AND(X1, X2)
ISNATURAL(n__sel(V1, V2)) → AND(isNatural(activate(V1)), n__isLNat(activate(V2)))
ISNATURAL(n__sel(V1, V2)) → ISNATURAL(activate(V1))
ISNATURAL(n__sel(V1, V2)) → ACTIVATE(V1)
ISNATURAL(n__sel(V1, V2)) → ACTIVATE(V2)
ISLNAT(n__cons(V1, V2)) → ACTIVATE(V1)
ISLNAT(n__cons(V1, V2)) → ACTIVATE(V2)
ISLNAT(n__fst(V1)) → ISPLNAT(activate(V1))
ISPLNAT(n__pair(V1, V2)) → AND(isLNat(activate(V1)), n__isLNat(activate(V2)))
ISPLNAT(n__pair(V1, V2)) → ISLNAT(activate(V1))
ISLNAT(n__fst(V1)) → ACTIVATE(V1)
ISLNAT(n__natsFrom(V1)) → ISNATURAL(activate(V1))
ISLNAT(n__natsFrom(V1)) → ACTIVATE(V1)
ISLNAT(n__snd(V1)) → ISPLNAT(activate(V1))
ISPLNAT(n__pair(V1, V2)) → ACTIVATE(V1)
ISPLNAT(n__pair(V1, V2)) → ACTIVATE(V2)
ISPLNAT(n__splitAt(V1, V2)) → AND(isNatural(activate(V1)), n__isLNat(activate(V2)))
ISPLNAT(n__splitAt(V1, V2)) → ISNATURAL(activate(V1))
ISPLNAT(n__splitAt(V1, V2)) → ACTIVATE(V1)
ISPLNAT(n__splitAt(V1, V2)) → ACTIVATE(V2)
ISLNAT(n__snd(V1)) → ACTIVATE(V1)
ISLNAT(n__tail(V1)) → ISLNAT(activate(V1))
ISLNAT(n__tail(V1)) → ACTIVATE(V1)
ISLNAT(n__take(V1, V2)) → AND(isNatural(activate(V1)), n__isLNat(activate(V2)))
ISLNAT(n__take(V1, V2)) → ISNATURAL(activate(V1))
ISLNAT(n__take(V1, V2)) → ACTIVATE(V1)
ISLNAT(n__take(V1, V2)) → ACTIVATE(V2)
SPLITAT(s(N), cons(X, XS)) → U81¹(and(isNatural(N), n__and(isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS))
U81¹(tt, N, X, XS) → U82¹(splitAt(activate(N), activate(XS)), activate(X))
U82¹(pair(YS, ZS), X) → ACTIVATE(X)
U81¹(tt, N, X, XS) → SPLITAT(activate(N), activate(XS))
SPLITAT(s(N), cons(X, XS)) → AND(isNatural(N), n__and(isNatural(X), n__isLNat(activate(XS))))
SPLITAT(s(N), cons(X, XS)) → ISNATURAL(N)
SPLITAT(s(N), cons(X, XS)) → ISNATURAL(X)
SPLITAT(s(N), cons(X, XS)) → ACTIVATE(XS)
U81¹(tt, N, X, XS) → ACTIVATE(N)
U81¹(tt, N, X, XS) → ACTIVATE(XS)
U81¹(tt, N, X, XS) → ACTIVATE(X)
HEAD(cons(N, XS)) → ACTIVATE(XS)
U51¹(tt, N, XS) → AFTERNTH(activate(N), activate(XS))
AFTERNTH(N, XS) → AND(isNatural(N), n__isLNat(XS))
AFTERNTH(N, XS) → ISNATURAL(N)
U51¹(tt, N, XS) → ACTIVATE(N)
U51¹(tt, N, XS) → ACTIVATE(XS)
SEL(N, XS) → AND(isNatural(N), n__isLNat(XS))
SEL(N, XS) → ISNATURAL(N)
U101¹(tt, N, XS) → ACTIVATE(N)
U101¹(tt, N, XS) → ACTIVATE(XS)
TAKE(N, XS) → AND(isNatural(N), n__isLNat(XS))
TAKE(N, XS) → ISNATURAL(N)
TAIL(cons(N, XS)) → AND(isNatural(N), n__isLNat(activate(XS)))
TAIL(cons(N, XS)) → ISNATURAL(N)
TAIL(cons(N, XS)) → ACTIVATE(XS)
U11¹(tt, N, XS) → SPLITAT(activate(N), activate(XS))
U11¹(tt, N, XS) → ACTIVATE(N)
U11¹(tt, N, XS) → ACTIVATE(XS)
NATSFROM(N) → ISNATURAL(N)

The TRS R consists of the following rules:

U101(tt, N, XS) → fst(splitAt(activate(N), activate(XS)))
U11(tt, N, XS) → snd(splitAt(activate(N), activate(XS)))
U21(tt, X) → activate(X)
U31(tt, N) → activate(N)
U41(tt, N) → cons(activate(N), n__natsFrom(s(activate(N))))
U51(tt, N, XS) → head(afterNth(activate(N), activate(XS)))
U61(tt, Y) → activate(Y)
U71(tt, XS) → pair(nil, activate(XS))
U81(tt, N, X, XS) → U82(splitAt(activate(N), activate(XS)), activate(X))
U82(pair(YS, ZS), X) → pair(cons(activate(X), YS), ZS)
U91(tt, XS) → activate(XS)
afterNth(N, XS) → U11(and(isNatural(N), n__isLNat(XS)), N, XS)
and(tt, X) → activate(X)
fst(pair(X, Y)) → U21(and(isLNat(X), n__isLNat(Y)), X)
head(cons(N, XS)) → U31(and(isNatural(N), n__isLNat(activate(XS))), N)
isLNat(n__nil) → tt
isLNat(n__afterNth(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
isLNat(n__cons(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
isLNat(n__fst(V1)) → isPLNat(activate(V1))
isLNat(n__natsFrom(V1)) → isNatural(activate(V1))
isLNat(n__snd(V1)) → isPLNat(activate(V1))
isLNat(n__tail(V1)) → isLNat(activate(V1))
isLNat(n__take(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
isNatural(n__0) → tt
isNatural(n__head(V1)) → isLNat(activate(V1))
isNatural(n__s(V1)) → isNatural(activate(V1))
isNatural(n__sel(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
isPLNat(n__pair(V1, V2)) → and(isLNat(activate(V1)), n__isLNat(activate(V2)))
isPLNat(n__splitAt(V1, V2)) → and(isNatural(activate(V1)), n__isLNat(activate(V2)))
natsFrom(N) → U41(isNatural(N), N)
sel(N, XS) → U51(and(isNatural(N), n__isLNat(XS)), N, XS)
snd(pair(X, Y)) → U61(and(isLNat(X), n__isLNat(Y)), Y)
splitAt(0, XS) → U71(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U81(and(isNatural(N), n__and(isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS))
tail(cons(N, XS)) → U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))
take(N, XS) → U101(and(isNatural(N), n__isLNat(XS)), N, XS)
natsFrom(X) → n__natsFrom(X)
isLNat(X) → n__isLNat(X)
nil → n__nil
afterNth(X1, X2) → n__afterNth(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
fst(X) → n__fst(X)
snd(X) → n__snd(X)
tail(X) → n__tail(X)
take(X1, X2) → n__take(X1, X2)
0 → n__0
head(X) → n__head(X)
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
pair(X1, X2) → n__pair(X1, X2)
splitAt(X1, X2) → n__splitAt(X1, X2)
and(X1, X2) → n__and(X1, X2)
activate(n__natsFrom(X)) → natsFrom(X)
activate(n__isLNat(X)) → isLNat(X)
activate(n__nil) → nil
activate(n__afterNth(X1, X2)) → afterNth(X1, X2)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__fst(X)) → fst(X)
activate(n__snd(X)) → snd(X)
activate(n__tail(X)) → tail(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__head(X)) → head(X)
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(n__pair(X1, X2)) → pair(X1, X2)
activate(n__splitAt(X1, X2)) → splitAt(X1, X2)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.