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, V1, V2) → U102(isNatural(activate(V1)), activate(V2))
U102(tt, V2) → U103(isLNat(activate(V2)))
U103(tt) → tt
U11(tt, N, XS) → snd(splitAt(activate(N), activate(XS)))
U111(tt, V1) → U112(isLNat(activate(V1)))
U112(tt) → tt
U121(tt, V1) → U122(isNatural(activate(V1)))
U122(tt) → tt
U131(tt, V1, V2) → U132(isNatural(activate(V1)), activate(V2))
U132(tt, V2) → U133(isLNat(activate(V2)))
U133(tt) → tt
U141(tt, V1, V2) → U142(isLNat(activate(V1)), activate(V2))
U142(tt, V2) → U143(isLNat(activate(V2)))
U143(tt) → tt
U151(tt, V1, V2) → U152(isNatural(activate(V1)), activate(V2))
U152(tt, V2) → U153(isLNat(activate(V2)))
U153(tt) → tt
U161(tt, N) → cons(activate(N), n__natsFrom(n__s(activate(N))))
U171(tt, N, XS) → head(afterNth(activate(N), activate(XS)))
U181(tt, Y) → activate(Y)
U191(tt, XS) → pair(nil, activate(XS))
U201(tt, N, X, XS) → U202(splitAt(activate(N), activate(XS)), activate(X))
U202(pair(YS, ZS), X) → pair(cons(activate(X), YS), ZS)
U21(tt, X) → activate(X)
U211(tt, XS) → activate(XS)
U221(tt, N, XS) → fst(splitAt(activate(N), activate(XS)))
U31(tt, N) → activate(N)
U41(tt, V1, V2) → U42(isNatural(activate(V1)), activate(V2))
U42(tt, V2) → U43(isLNat(activate(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNatural(activate(V1)), activate(V2))
U52(tt, V2) → U53(isLNat(activate(V2)))
U53(tt) → tt
U61(tt, V1) → U62(isPLNat(activate(V1)))
U62(tt) → tt
U71(tt, V1) → U72(isNatural(activate(V1)))
U72(tt) → tt
U81(tt, V1) → U82(isPLNat(activate(V1)))
U82(tt) → tt
U91(tt, V1) → U92(isLNat(activate(V1)))
U92(tt) → tt
afterNth(N, XS) → U11(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
and(tt, X) → activate(X)
fst(pair(X, Y)) → U21(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X)
head(cons(N, XS)) → U31(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N)
isLNat(n__nil) → tt
isLNat(n__afterNth(V1, V2)) → U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isLNat(n__cons(V1, V2)) → U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isLNat(n__fst(V1)) → U61(isPLNatKind(activate(V1)), activate(V1))
isLNat(n__natsFrom(V1)) → U71(isNaturalKind(activate(V1)), activate(V1))
isLNat(n__snd(V1)) → U81(isPLNatKind(activate(V1)), activate(V1))
isLNat(n__tail(V1)) → U91(isLNatKind(activate(V1)), activate(V1))
isLNat(n__take(V1, V2)) → U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isLNatKind(n__nil) → tt
isLNatKind(n__afterNth(V1, V2)) → and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
isLNatKind(n__cons(V1, V2)) → and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
isLNatKind(n__fst(V1)) → isPLNatKind(activate(V1))
isLNatKind(n__natsFrom(V1)) → isNaturalKind(activate(V1))
isLNatKind(n__snd(V1)) → isPLNatKind(activate(V1))
isLNatKind(n__tail(V1)) → isLNatKind(activate(V1))
isLNatKind(n__take(V1, V2)) → and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
isNatural(n__0) → tt
isNatural(n__head(V1)) → U111(isLNatKind(activate(V1)), activate(V1))
isNatural(n__s(V1)) → U121(isNaturalKind(activate(V1)), activate(V1))
isNatural(n__sel(V1, V2)) → U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isNaturalKind(n__0) → tt
isNaturalKind(n__head(V1)) → isLNatKind(activate(V1))
isNaturalKind(n__s(V1)) → isNaturalKind(activate(V1))
isNaturalKind(n__sel(V1, V2)) → and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
isPLNat(n__pair(V1, V2)) → U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isPLNat(n__splitAt(V1, V2)) → U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isPLNatKind(n__pair(V1, V2)) → and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))
isPLNatKind(n__splitAt(V1, V2)) → and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
natsFrom(N) → U161(and(isNatural(N), n__isNaturalKind(N)), N)
sel(N, XS) → U171(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
snd(pair(X, Y)) → U181(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y)
splitAt(0, XS) → U191(and(isLNat(XS), n__isLNatKind(XS)), XS)
splitAt(s(N), cons(X, XS)) → U201(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS))
tail(cons(N, XS)) → U211(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS))
take(N, XS) → U221(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
natsFrom(X) → n__natsFrom(X)
s(X) → n__s(X)
isNaturalKind(X) → n__isNaturalKind(X)
and(X1, X2) → n__and(X1, X2)
isLNat(X) → n__isLNat(X)
isLNatKind(X) → n__isLNatKind(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)
sel(X1, X2) → n__sel(X1, X2)
pair(X1, X2) → n__pair(X1, X2)
splitAt(X1, X2) → n__splitAt(X1, X2)
isNatural(X) → n__isNatural(X)
activate(n__natsFrom(X)) → natsFrom(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__isNaturalKind(X)) → isNaturalKind(X)
activate(n__and(X1, X2)) → and(activate(X1), X2)
activate(n__isLNat(X)) → isLNat(X)
activate(n__isLNatKind(X)) → isLNatKind(X)
activate(n__nil) → nil
activate(n__afterNth(X1, X2)) → afterNth(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__fst(X)) → fst(activate(X))
activate(n__snd(X)) → snd(activate(X))
activate(n__tail(X)) → tail(activate(X))
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__head(X)) → head(activate(X))
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(n__pair(X1, X2)) → pair(activate(X1), activate(X2))
activate(n__splitAt(X1, X2)) → splitAt(activate(X1), activate(X2))
activate(n__isNatural(X)) → isNatural(X)
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:

U1011(tt, V1, V2) → U1021(isNatural(activate(V1)), activate(V2))
U1011(tt, V1, V2) → ISNATURAL(activate(V1))
U1011(tt, V1, V2) → ACTIVATE(V1)
U1011(tt, V1, V2) → ACTIVATE(V2)
U1021(tt, V2) → U1031(isLNat(activate(V2)))
U1021(tt, V2) → ISLNAT(activate(V2))
U1021(tt, V2) → ACTIVATE(V2)
U111(tt, N, XS) → SND(splitAt(activate(N), activate(XS)))
U111(tt, N, XS) → SPLITAT(activate(N), activate(XS))
U111(tt, N, XS) → ACTIVATE(N)
U111(tt, N, XS) → ACTIVATE(XS)
U1111(tt, V1) → U1121(isLNat(activate(V1)))
U1111(tt, V1) → ISLNAT(activate(V1))
U1111(tt, V1) → ACTIVATE(V1)
U1211(tt, V1) → U1221(isNatural(activate(V1)))
U1211(tt, V1) → ISNATURAL(activate(V1))
U1211(tt, V1) → ACTIVATE(V1)
U1311(tt, V1, V2) → U1321(isNatural(activate(V1)), activate(V2))
U1311(tt, V1, V2) → ISNATURAL(activate(V1))
U1311(tt, V1, V2) → ACTIVATE(V1)
U1311(tt, V1, V2) → ACTIVATE(V2)
U1321(tt, V2) → U1331(isLNat(activate(V2)))
U1321(tt, V2) → ISLNAT(activate(V2))
U1321(tt, V2) → ACTIVATE(V2)
U1411(tt, V1, V2) → U1421(isLNat(activate(V1)), activate(V2))
U1411(tt, V1, V2) → ISLNAT(activate(V1))
U1411(tt, V1, V2) → ACTIVATE(V1)
U1411(tt, V1, V2) → ACTIVATE(V2)
U1421(tt, V2) → U1431(isLNat(activate(V2)))
U1421(tt, V2) → ISLNAT(activate(V2))
U1421(tt, V2) → ACTIVATE(V2)
U1511(tt, V1, V2) → U1521(isNatural(activate(V1)), activate(V2))
U1511(tt, V1, V2) → ISNATURAL(activate(V1))
U1511(tt, V1, V2) → ACTIVATE(V1)
U1511(tt, V1, V2) → ACTIVATE(V2)
U1521(tt, V2) → U1531(isLNat(activate(V2)))
U1521(tt, V2) → ISLNAT(activate(V2))
U1521(tt, V2) → ACTIVATE(V2)
U1611(tt, N) → CONS(activate(N), n__natsFrom(n__s(activate(N))))
U1611(tt, N) → ACTIVATE(N)
U1711(tt, N, XS) → HEAD(afterNth(activate(N), activate(XS)))
U1711(tt, N, XS) → AFTERNTH(activate(N), activate(XS))
U1711(tt, N, XS) → ACTIVATE(N)
U1711(tt, N, XS) → ACTIVATE(XS)
U1811(tt, Y) → ACTIVATE(Y)
U1911(tt, XS) → PAIR(nil, activate(XS))
U1911(tt, XS) → NIL
U1911(tt, XS) → ACTIVATE(XS)
U2011(tt, N, X, XS) → U2021(splitAt(activate(N), activate(XS)), activate(X))
U2011(tt, N, X, XS) → SPLITAT(activate(N), activate(XS))
U2011(tt, N, X, XS) → ACTIVATE(N)
U2011(tt, N, X, XS) → ACTIVATE(XS)
U2011(tt, N, X, XS) → ACTIVATE(X)
U2021(pair(YS, ZS), X) → PAIR(cons(activate(X), YS), ZS)
U2021(pair(YS, ZS), X) → CONS(activate(X), YS)
U2021(pair(YS, ZS), X) → ACTIVATE(X)
U211(tt, X) → ACTIVATE(X)
U2111(tt, XS) → ACTIVATE(XS)
U2211(tt, N, XS) → FST(splitAt(activate(N), activate(XS)))
U2211(tt, N, XS) → SPLITAT(activate(N), activate(XS))
U2211(tt, N, XS) → ACTIVATE(N)
U2211(tt, N, XS) → ACTIVATE(XS)
U311(tt, N) → ACTIVATE(N)
U411(tt, V1, V2) → U421(isNatural(activate(V1)), activate(V2))
U411(tt, V1, V2) → ISNATURAL(activate(V1))
U411(tt, V1, V2) → ACTIVATE(V1)
U411(tt, V1, V2) → ACTIVATE(V2)
U421(tt, V2) → U431(isLNat(activate(V2)))
U421(tt, V2) → ISLNAT(activate(V2))
U421(tt, V2) → ACTIVATE(V2)
U511(tt, V1, V2) → U521(isNatural(activate(V1)), activate(V2))
U511(tt, V1, V2) → ISNATURAL(activate(V1))
U511(tt, V1, V2) → ACTIVATE(V1)
U511(tt, V1, V2) → ACTIVATE(V2)
U521(tt, V2) → U531(isLNat(activate(V2)))
U521(tt, V2) → ISLNAT(activate(V2))
U521(tt, V2) → ACTIVATE(V2)
U611(tt, V1) → U621(isPLNat(activate(V1)))
U611(tt, V1) → ISPLNAT(activate(V1))
U611(tt, V1) → ACTIVATE(V1)
U711(tt, V1) → U721(isNatural(activate(V1)))
U711(tt, V1) → ISNATURAL(activate(V1))
U711(tt, V1) → ACTIVATE(V1)
U811(tt, V1) → U821(isPLNat(activate(V1)))
U811(tt, V1) → ISPLNAT(activate(V1))
U811(tt, V1) → ACTIVATE(V1)
U911(tt, V1) → U921(isLNat(activate(V1)))
U911(tt, V1) → ISLNAT(activate(V1))
U911(tt, V1) → ACTIVATE(V1)
AFTERNTH(N, XS) → U111(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
AFTERNTH(N, XS) → AND(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS)))
AFTERNTH(N, XS) → AND(isNatural(N), n__isNaturalKind(N))
AFTERNTH(N, XS) → ISNATURAL(N)
AND(tt, X) → ACTIVATE(X)
FST(pair(X, Y)) → U211(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X)
FST(pair(X, Y)) → AND(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y)))
FST(pair(X, Y)) → AND(isLNat(X), n__isLNatKind(X))
FST(pair(X, Y)) → ISLNAT(X)
HEAD(cons(N, XS)) → U311(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N)
HEAD(cons(N, XS)) → AND(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))
HEAD(cons(N, XS)) → AND(isNatural(N), n__isNaturalKind(N))
HEAD(cons(N, XS)) → ISNATURAL(N)
HEAD(cons(N, XS)) → ACTIVATE(XS)
ISLNAT(n__afterNth(V1, V2)) → U411(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
ISLNAT(n__afterNth(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISLNAT(n__afterNth(V1, V2)) → ISNATURALKIND(activate(V1))
ISLNAT(n__afterNth(V1, V2)) → ACTIVATE(V1)
ISLNAT(n__afterNth(V1, V2)) → ACTIVATE(V2)
ISLNAT(n__cons(V1, V2)) → U511(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
ISLNAT(n__cons(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISLNAT(n__cons(V1, V2)) → ISNATURALKIND(activate(V1))
ISLNAT(n__cons(V1, V2)) → ACTIVATE(V1)
ISLNAT(n__cons(V1, V2)) → ACTIVATE(V2)
ISLNAT(n__fst(V1)) → U611(isPLNatKind(activate(V1)), activate(V1))
ISLNAT(n__fst(V1)) → ISPLNATKIND(activate(V1))
ISLNAT(n__fst(V1)) → ACTIVATE(V1)
ISLNAT(n__natsFrom(V1)) → U711(isNaturalKind(activate(V1)), activate(V1))
ISLNAT(n__natsFrom(V1)) → ISNATURALKIND(activate(V1))
ISLNAT(n__natsFrom(V1)) → ACTIVATE(V1)
ISLNAT(n__snd(V1)) → U811(isPLNatKind(activate(V1)), activate(V1))
ISLNAT(n__snd(V1)) → ISPLNATKIND(activate(V1))
ISLNAT(n__snd(V1)) → ACTIVATE(V1)
ISLNAT(n__tail(V1)) → U911(isLNatKind(activate(V1)), activate(V1))
ISLNAT(n__tail(V1)) → ISLNATKIND(activate(V1))
ISLNAT(n__tail(V1)) → ACTIVATE(V1)
ISLNAT(n__take(V1, V2)) → U1011(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
ISLNAT(n__take(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISLNAT(n__take(V1, V2)) → ISNATURALKIND(activate(V1))
ISLNAT(n__take(V1, V2)) → ACTIVATE(V1)
ISLNAT(n__take(V1, V2)) → ACTIVATE(V2)
ISLNATKIND(n__afterNth(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISLNATKIND(n__afterNth(V1, V2)) → ISNATURALKIND(activate(V1))
ISLNATKIND(n__afterNth(V1, V2)) → ACTIVATE(V1)
ISLNATKIND(n__afterNth(V1, V2)) → ACTIVATE(V2)
ISLNATKIND(n__cons(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISLNATKIND(n__cons(V1, V2)) → ISNATURALKIND(activate(V1))
ISLNATKIND(n__cons(V1, V2)) → ACTIVATE(V1)
ISLNATKIND(n__cons(V1, V2)) → ACTIVATE(V2)
ISLNATKIND(n__fst(V1)) → ISPLNATKIND(activate(V1))
ISLNATKIND(n__fst(V1)) → ACTIVATE(V1)
ISLNATKIND(n__natsFrom(V1)) → ISNATURALKIND(activate(V1))
ISLNATKIND(n__natsFrom(V1)) → ACTIVATE(V1)
ISLNATKIND(n__snd(V1)) → ISPLNATKIND(activate(V1))
ISLNATKIND(n__snd(V1)) → ACTIVATE(V1)
ISLNATKIND(n__tail(V1)) → ISLNATKIND(activate(V1))
ISLNATKIND(n__tail(V1)) → ACTIVATE(V1)
ISLNATKIND(n__take(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISLNATKIND(n__take(V1, V2)) → ISNATURALKIND(activate(V1))
ISLNATKIND(n__take(V1, V2)) → ACTIVATE(V1)
ISLNATKIND(n__take(V1, V2)) → ACTIVATE(V2)
ISNATURAL(n__head(V1)) → U1111(isLNatKind(activate(V1)), activate(V1))
ISNATURAL(n__head(V1)) → ISLNATKIND(activate(V1))
ISNATURAL(n__head(V1)) → ACTIVATE(V1)
ISNATURAL(n__s(V1)) → U1211(isNaturalKind(activate(V1)), activate(V1))
ISNATURAL(n__s(V1)) → ISNATURALKIND(activate(V1))
ISNATURAL(n__s(V1)) → ACTIVATE(V1)
ISNATURAL(n__sel(V1, V2)) → U1311(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
ISNATURAL(n__sel(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISNATURAL(n__sel(V1, V2)) → ISNATURALKIND(activate(V1))
ISNATURAL(n__sel(V1, V2)) → ACTIVATE(V1)
ISNATURAL(n__sel(V1, V2)) → ACTIVATE(V2)
ISNATURALKIND(n__head(V1)) → ISLNATKIND(activate(V1))
ISNATURALKIND(n__head(V1)) → ACTIVATE(V1)
ISNATURALKIND(n__s(V1)) → ISNATURALKIND(activate(V1))
ISNATURALKIND(n__s(V1)) → ACTIVATE(V1)
ISNATURALKIND(n__sel(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISNATURALKIND(n__sel(V1, V2)) → ISNATURALKIND(activate(V1))
ISNATURALKIND(n__sel(V1, V2)) → ACTIVATE(V1)
ISNATURALKIND(n__sel(V1, V2)) → ACTIVATE(V2)
ISPLNAT(n__pair(V1, V2)) → U1411(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
ISPLNAT(n__pair(V1, V2)) → AND(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))
ISPLNAT(n__pair(V1, V2)) → ISLNATKIND(activate(V1))
ISPLNAT(n__pair(V1, V2)) → ACTIVATE(V1)
ISPLNAT(n__pair(V1, V2)) → ACTIVATE(V2)
ISPLNAT(n__splitAt(V1, V2)) → U1511(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
ISPLNAT(n__splitAt(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISPLNAT(n__splitAt(V1, V2)) → ISNATURALKIND(activate(V1))
ISPLNAT(n__splitAt(V1, V2)) → ACTIVATE(V1)
ISPLNAT(n__splitAt(V1, V2)) → ACTIVATE(V2)
ISPLNATKIND(n__pair(V1, V2)) → AND(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))
ISPLNATKIND(n__pair(V1, V2)) → ISLNATKIND(activate(V1))
ISPLNATKIND(n__pair(V1, V2)) → ACTIVATE(V1)
ISPLNATKIND(n__pair(V1, V2)) → ACTIVATE(V2)
ISPLNATKIND(n__splitAt(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISPLNATKIND(n__splitAt(V1, V2)) → ISNATURALKIND(activate(V1))
ISPLNATKIND(n__splitAt(V1, V2)) → ACTIVATE(V1)
ISPLNATKIND(n__splitAt(V1, V2)) → ACTIVATE(V2)
NATSFROM(N) → U1611(and(isNatural(N), n__isNaturalKind(N)), N)
NATSFROM(N) → AND(isNatural(N), n__isNaturalKind(N))
NATSFROM(N) → ISNATURAL(N)
SEL(N, XS) → U1711(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
SEL(N, XS) → AND(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS)))
SEL(N, XS) → AND(isNatural(N), n__isNaturalKind(N))
SEL(N, XS) → ISNATURAL(N)
SND(pair(X, Y)) → U1811(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y)
SND(pair(X, Y)) → AND(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y)))
SND(pair(X, Y)) → AND(isLNat(X), n__isLNatKind(X))
SND(pair(X, Y)) → ISLNAT(X)
SPLITAT(0, XS) → U1911(and(isLNat(XS), n__isLNatKind(XS)), XS)
SPLITAT(0, XS) → AND(isLNat(XS), n__isLNatKind(XS))
SPLITAT(0, XS) → ISLNAT(XS)
SPLITAT(s(N), cons(X, XS)) → U2011(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS))
SPLITAT(s(N), cons(X, XS)) → AND(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))))
SPLITAT(s(N), cons(X, XS)) → AND(isNatural(N), n__isNaturalKind(N))
SPLITAT(s(N), cons(X, XS)) → ISNATURAL(N)
SPLITAT(s(N), cons(X, XS)) → ACTIVATE(XS)
TAIL(cons(N, XS)) → U2111(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS))
TAIL(cons(N, XS)) → AND(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))
TAIL(cons(N, XS)) → AND(isNatural(N), n__isNaturalKind(N))
TAIL(cons(N, XS)) → ISNATURAL(N)
TAIL(cons(N, XS)) → ACTIVATE(XS)
TAKE(N, XS) → U2211(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
TAKE(N, XS) → AND(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS)))
TAKE(N, XS) → AND(isNatural(N), n__isNaturalKind(N))
TAKE(N, XS) → ISNATURAL(N)
ACTIVATE(n__natsFrom(X)) → NATSFROM(activate(X))
ACTIVATE(n__natsFrom(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → S(activate(X))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__isNaturalKind(X)) → ISNATURALKIND(X)
ACTIVATE(n__and(X1, X2)) → AND(activate(X1), X2)
ACTIVATE(n__and(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__isLNat(X)) → ISLNAT(X)
ACTIVATE(n__isLNatKind(X)) → ISLNATKIND(X)
ACTIVATE(n__nil) → NIL
ACTIVATE(n__afterNth(X1, X2)) → AFTERNTH(activate(X1), activate(X2))
ACTIVATE(n__afterNth(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__afterNth(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__cons(X1, X2)) → CONS(activate(X1), X2)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__fst(X)) → FST(activate(X))
ACTIVATE(n__fst(X)) → ACTIVATE(X)
ACTIVATE(n__snd(X)) → SND(activate(X))
ACTIVATE(n__snd(X)) → ACTIVATE(X)
ACTIVATE(n__tail(X)) → TAIL(activate(X))
ACTIVATE(n__tail(X)) → ACTIVATE(X)
ACTIVATE(n__take(X1, X2)) → TAKE(activate(X1), activate(X2))
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__0) → 01
ACTIVATE(n__head(X)) → HEAD(activate(X))
ACTIVATE(n__head(X)) → ACTIVATE(X)
ACTIVATE(n__sel(X1, X2)) → SEL(activate(X1), activate(X2))
ACTIVATE(n__sel(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__sel(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__pair(X1, X2)) → PAIR(activate(X1), activate(X2))
ACTIVATE(n__pair(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__pair(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__splitAt(X1, X2)) → SPLITAT(activate(X1), activate(X2))
ACTIVATE(n__splitAt(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__splitAt(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__isNatural(X)) → ISNATURAL(X)

The TRS R consists of the following rules:

U101(tt, V1, V2) → U102(isNatural(activate(V1)), activate(V2))
U102(tt, V2) → U103(isLNat(activate(V2)))
U103(tt) → tt
U11(tt, N, XS) → snd(splitAt(activate(N), activate(XS)))
U111(tt, V1) → U112(isLNat(activate(V1)))
U112(tt) → tt
U121(tt, V1) → U122(isNatural(activate(V1)))
U122(tt) → tt
U131(tt, V1, V2) → U132(isNatural(activate(V1)), activate(V2))
U132(tt, V2) → U133(isLNat(activate(V2)))
U133(tt) → tt
U141(tt, V1, V2) → U142(isLNat(activate(V1)), activate(V2))
U142(tt, V2) → U143(isLNat(activate(V2)))
U143(tt) → tt
U151(tt, V1, V2) → U152(isNatural(activate(V1)), activate(V2))
U152(tt, V2) → U153(isLNat(activate(V2)))
U153(tt) → tt
U161(tt, N) → cons(activate(N), n__natsFrom(n__s(activate(N))))
U171(tt, N, XS) → head(afterNth(activate(N), activate(XS)))
U181(tt, Y) → activate(Y)
U191(tt, XS) → pair(nil, activate(XS))
U201(tt, N, X, XS) → U202(splitAt(activate(N), activate(XS)), activate(X))
U202(pair(YS, ZS), X) → pair(cons(activate(X), YS), ZS)
U21(tt, X) → activate(X)
U211(tt, XS) → activate(XS)
U221(tt, N, XS) → fst(splitAt(activate(N), activate(XS)))
U31(tt, N) → activate(N)
U41(tt, V1, V2) → U42(isNatural(activate(V1)), activate(V2))
U42(tt, V2) → U43(isLNat(activate(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNatural(activate(V1)), activate(V2))
U52(tt, V2) → U53(isLNat(activate(V2)))
U53(tt) → tt
U61(tt, V1) → U62(isPLNat(activate(V1)))
U62(tt) → tt
U71(tt, V1) → U72(isNatural(activate(V1)))
U72(tt) → tt
U81(tt, V1) → U82(isPLNat(activate(V1)))
U82(tt) → tt
U91(tt, V1) → U92(isLNat(activate(V1)))
U92(tt) → tt
afterNth(N, XS) → U11(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
and(tt, X) → activate(X)
fst(pair(X, Y)) → U21(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X)
head(cons(N, XS)) → U31(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N)
isLNat(n__nil) → tt
isLNat(n__afterNth(V1, V2)) → U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isLNat(n__cons(V1, V2)) → U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isLNat(n__fst(V1)) → U61(isPLNatKind(activate(V1)), activate(V1))
isLNat(n__natsFrom(V1)) → U71(isNaturalKind(activate(V1)), activate(V1))
isLNat(n__snd(V1)) → U81(isPLNatKind(activate(V1)), activate(V1))
isLNat(n__tail(V1)) → U91(isLNatKind(activate(V1)), activate(V1))
isLNat(n__take(V1, V2)) → U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isLNatKind(n__nil) → tt
isLNatKind(n__afterNth(V1, V2)) → and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
isLNatKind(n__cons(V1, V2)) → and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
isLNatKind(n__fst(V1)) → isPLNatKind(activate(V1))
isLNatKind(n__natsFrom(V1)) → isNaturalKind(activate(V1))
isLNatKind(n__snd(V1)) → isPLNatKind(activate(V1))
isLNatKind(n__tail(V1)) → isLNatKind(activate(V1))
isLNatKind(n__take(V1, V2)) → and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
isNatural(n__0) → tt
isNatural(n__head(V1)) → U111(isLNatKind(activate(V1)), activate(V1))
isNatural(n__s(V1)) → U121(isNaturalKind(activate(V1)), activate(V1))
isNatural(n__sel(V1, V2)) → U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isNaturalKind(n__0) → tt
isNaturalKind(n__head(V1)) → isLNatKind(activate(V1))
isNaturalKind(n__s(V1)) → isNaturalKind(activate(V1))
isNaturalKind(n__sel(V1, V2)) → and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
isPLNat(n__pair(V1, V2)) → U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isPLNat(n__splitAt(V1, V2)) → U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isPLNatKind(n__pair(V1, V2)) → and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))
isPLNatKind(n__splitAt(V1, V2)) → and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
natsFrom(N) → U161(and(isNatural(N), n__isNaturalKind(N)), N)
sel(N, XS) → U171(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
snd(pair(X, Y)) → U181(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y)
splitAt(0, XS) → U191(and(isLNat(XS), n__isLNatKind(XS)), XS)
splitAt(s(N), cons(X, XS)) → U201(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS))
tail(cons(N, XS)) → U211(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS))
take(N, XS) → U221(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
natsFrom(X) → n__natsFrom(X)
s(X) → n__s(X)
isNaturalKind(X) → n__isNaturalKind(X)
and(X1, X2) → n__and(X1, X2)
isLNat(X) → n__isLNat(X)
isLNatKind(X) → n__isLNatKind(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)
sel(X1, X2) → n__sel(X1, X2)
pair(X1, X2) → n__pair(X1, X2)
splitAt(X1, X2) → n__splitAt(X1, X2)
isNatural(X) → n__isNatural(X)
activate(n__natsFrom(X)) → natsFrom(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__isNaturalKind(X)) → isNaturalKind(X)
activate(n__and(X1, X2)) → and(activate(X1), X2)
activate(n__isLNat(X)) → isLNat(X)
activate(n__isLNatKind(X)) → isLNatKind(X)
activate(n__nil) → nil
activate(n__afterNth(X1, X2)) → afterNth(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__fst(X)) → fst(activate(X))
activate(n__snd(X)) → snd(activate(X))
activate(n__tail(X)) → tail(activate(X))
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__head(X)) → head(activate(X))
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(n__pair(X1, X2)) → pair(activate(X1), activate(X2))
activate(n__splitAt(X1, X2)) → splitAt(activate(X1), activate(X2))
activate(n__isNatural(X)) → isNatural(X)
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 22 less nodes.

(4) Obligation:

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

U1021(tt, V2) → ISLNAT(activate(V2))
ISLNAT(n__afterNth(V1, V2)) → U411(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
U411(tt, V1, V2) → U421(isNatural(activate(V1)), activate(V2))
U421(tt, V2) → ISLNAT(activate(V2))
ISLNAT(n__afterNth(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__natsFrom(X)) → NATSFROM(activate(X))
NATSFROM(N) → U1611(and(isNatural(N), n__isNaturalKind(N)), N)
U1611(tt, N) → ACTIVATE(N)
ACTIVATE(n__natsFrom(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__isNaturalKind(X)) → ISNATURALKIND(X)
ISNATURALKIND(n__head(V1)) → ISLNATKIND(activate(V1))
ISLNATKIND(n__afterNth(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISLNATKIND(n__afterNth(V1, V2)) → ISNATURALKIND(activate(V1))
ISNATURALKIND(n__head(V1)) → ACTIVATE(V1)
ACTIVATE(n__and(X1, X2)) → AND(activate(X1), X2)
ACTIVATE(n__and(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__isLNat(X)) → ISLNAT(X)
ISLNAT(n__afterNth(V1, V2)) → ISNATURALKIND(activate(V1))
ISNATURALKIND(n__s(V1)) → ISNATURALKIND(activate(V1))
ISNATURALKIND(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__isLNatKind(X)) → ISLNATKIND(X)
ISLNATKIND(n__afterNth(V1, V2)) → ACTIVATE(V1)
ACTIVATE(n__afterNth(X1, X2)) → AFTERNTH(activate(X1), activate(X2))
AFTERNTH(N, XS) → U111(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
U111(tt, N, XS) → SND(splitAt(activate(N), activate(XS)))
SND(pair(X, Y)) → U1811(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y)
U1811(tt, Y) → ACTIVATE(Y)
ACTIVATE(n__afterNth(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__afterNth(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__fst(X)) → FST(activate(X))
FST(pair(X, Y)) → U211(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X)
U211(tt, X) → ACTIVATE(X)
ACTIVATE(n__fst(X)) → ACTIVATE(X)
ACTIVATE(n__snd(X)) → SND(activate(X))
SND(pair(X, Y)) → AND(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y)))
SND(pair(X, Y)) → AND(isLNat(X), n__isLNatKind(X))
SND(pair(X, Y)) → ISLNAT(X)
ISLNAT(n__afterNth(V1, V2)) → ACTIVATE(V1)
ACTIVATE(n__snd(X)) → ACTIVATE(X)
ACTIVATE(n__tail(X)) → TAIL(activate(X))
TAIL(cons(N, XS)) → U2111(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS))
U2111(tt, XS) → ACTIVATE(XS)
ACTIVATE(n__tail(X)) → ACTIVATE(X)
ACTIVATE(n__take(X1, X2)) → TAKE(activate(X1), activate(X2))
TAKE(N, XS) → U2211(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
U2211(tt, N, XS) → FST(splitAt(activate(N), activate(XS)))
FST(pair(X, Y)) → AND(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y)))
FST(pair(X, Y)) → AND(isLNat(X), n__isLNatKind(X))
FST(pair(X, Y)) → ISLNAT(X)
ISLNAT(n__afterNth(V1, V2)) → ACTIVATE(V2)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__head(X)) → HEAD(activate(X))
HEAD(cons(N, XS)) → U311(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N)
U311(tt, N) → ACTIVATE(N)
ACTIVATE(n__head(X)) → ACTIVATE(X)
ACTIVATE(n__sel(X1, X2)) → SEL(activate(X1), activate(X2))
SEL(N, XS) → U1711(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
U1711(tt, N, XS) → HEAD(afterNth(activate(N), activate(XS)))
HEAD(cons(N, XS)) → AND(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))
HEAD(cons(N, XS)) → AND(isNatural(N), n__isNaturalKind(N))
HEAD(cons(N, XS)) → ISNATURAL(N)
ISNATURAL(n__head(V1)) → U1111(isLNatKind(activate(V1)), activate(V1))
U1111(tt, V1) → ISLNAT(activate(V1))
ISLNAT(n__cons(V1, V2)) → U511(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
U511(tt, V1, V2) → U521(isNatural(activate(V1)), activate(V2))
U521(tt, V2) → ISLNAT(activate(V2))
ISLNAT(n__cons(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISLNAT(n__cons(V1, V2)) → ISNATURALKIND(activate(V1))
ISNATURALKIND(n__sel(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISNATURALKIND(n__sel(V1, V2)) → ISNATURALKIND(activate(V1))
ISNATURALKIND(n__sel(V1, V2)) → ACTIVATE(V1)
ACTIVATE(n__sel(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__sel(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__pair(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__pair(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__splitAt(X1, X2)) → SPLITAT(activate(X1), activate(X2))
SPLITAT(0, XS) → U1911(and(isLNat(XS), n__isLNatKind(XS)), XS)
U1911(tt, XS) → ACTIVATE(XS)
ACTIVATE(n__splitAt(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__splitAt(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__isNatural(X)) → ISNATURAL(X)
ISNATURAL(n__head(V1)) → ISLNATKIND(activate(V1))
ISLNATKIND(n__afterNth(V1, V2)) → ACTIVATE(V2)
ISLNATKIND(n__cons(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISLNATKIND(n__cons(V1, V2)) → ISNATURALKIND(activate(V1))
ISNATURALKIND(n__sel(V1, V2)) → ACTIVATE(V2)
ISLNATKIND(n__cons(V1, V2)) → ACTIVATE(V1)
ISLNATKIND(n__cons(V1, V2)) → ACTIVATE(V2)
ISLNATKIND(n__fst(V1)) → ISPLNATKIND(activate(V1))
ISPLNATKIND(n__pair(V1, V2)) → AND(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))
ISPLNATKIND(n__pair(V1, V2)) → ISLNATKIND(activate(V1))
ISLNATKIND(n__fst(V1)) → ACTIVATE(V1)
ISLNATKIND(n__natsFrom(V1)) → ISNATURALKIND(activate(V1))
ISLNATKIND(n__natsFrom(V1)) → ACTIVATE(V1)
ISLNATKIND(n__snd(V1)) → ISPLNATKIND(activate(V1))
ISPLNATKIND(n__pair(V1, V2)) → ACTIVATE(V1)
ISPLNATKIND(n__pair(V1, V2)) → ACTIVATE(V2)
ISPLNATKIND(n__splitAt(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISPLNATKIND(n__splitAt(V1, V2)) → ISNATURALKIND(activate(V1))
ISPLNATKIND(n__splitAt(V1, V2)) → ACTIVATE(V1)
ISPLNATKIND(n__splitAt(V1, V2)) → ACTIVATE(V2)
ISLNATKIND(n__snd(V1)) → ACTIVATE(V1)
ISLNATKIND(n__tail(V1)) → ISLNATKIND(activate(V1))
ISLNATKIND(n__tail(V1)) → ACTIVATE(V1)
ISLNATKIND(n__take(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISLNATKIND(n__take(V1, V2)) → ISNATURALKIND(activate(V1))
ISLNATKIND(n__take(V1, V2)) → ACTIVATE(V1)
ISLNATKIND(n__take(V1, V2)) → ACTIVATE(V2)
ISNATURAL(n__head(V1)) → ACTIVATE(V1)
ISNATURAL(n__s(V1)) → U1211(isNaturalKind(activate(V1)), activate(V1))
U1211(tt, V1) → ISNATURAL(activate(V1))
ISNATURAL(n__s(V1)) → ISNATURALKIND(activate(V1))
ISNATURAL(n__s(V1)) → ACTIVATE(V1)
ISNATURAL(n__sel(V1, V2)) → U1311(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
U1311(tt, V1, V2) → U1321(isNatural(activate(V1)), activate(V2))
U1321(tt, V2) → ISLNAT(activate(V2))
ISLNAT(n__cons(V1, V2)) → ACTIVATE(V1)
ISLNAT(n__cons(V1, V2)) → ACTIVATE(V2)
ISLNAT(n__fst(V1)) → U611(isPLNatKind(activate(V1)), activate(V1))
U611(tt, V1) → ISPLNAT(activate(V1))
ISPLNAT(n__pair(V1, V2)) → U1411(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
U1411(tt, V1, V2) → U1421(isLNat(activate(V1)), activate(V2))
U1421(tt, V2) → ISLNAT(activate(V2))
ISLNAT(n__fst(V1)) → ISPLNATKIND(activate(V1))
ISLNAT(n__fst(V1)) → ACTIVATE(V1)
ISLNAT(n__natsFrom(V1)) → U711(isNaturalKind(activate(V1)), activate(V1))
U711(tt, V1) → ISNATURAL(activate(V1))
ISNATURAL(n__sel(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISNATURAL(n__sel(V1, V2)) → ISNATURALKIND(activate(V1))
ISNATURAL(n__sel(V1, V2)) → ACTIVATE(V1)
ISNATURAL(n__sel(V1, V2)) → ACTIVATE(V2)
U711(tt, V1) → ACTIVATE(V1)
ISLNAT(n__natsFrom(V1)) → ISNATURALKIND(activate(V1))
ISLNAT(n__natsFrom(V1)) → ACTIVATE(V1)
ISLNAT(n__snd(V1)) → U811(isPLNatKind(activate(V1)), activate(V1))
U811(tt, V1) → ISPLNAT(activate(V1))
ISPLNAT(n__pair(V1, V2)) → AND(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))
ISPLNAT(n__pair(V1, V2)) → ISLNATKIND(activate(V1))
ISPLNAT(n__pair(V1, V2)) → ACTIVATE(V1)
ISPLNAT(n__pair(V1, V2)) → ACTIVATE(V2)
ISPLNAT(n__splitAt(V1, V2)) → U1511(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
U1511(tt, V1, V2) → U1521(isNatural(activate(V1)), activate(V2))
U1521(tt, V2) → ISLNAT(activate(V2))
ISLNAT(n__snd(V1)) → ISPLNATKIND(activate(V1))
ISLNAT(n__snd(V1)) → ACTIVATE(V1)
ISLNAT(n__tail(V1)) → U911(isLNatKind(activate(V1)), activate(V1))
U911(tt, V1) → ISLNAT(activate(V1))
ISLNAT(n__tail(V1)) → ISLNATKIND(activate(V1))
ISLNAT(n__tail(V1)) → ACTIVATE(V1)
ISLNAT(n__take(V1, V2)) → U1011(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
U1011(tt, V1, V2) → U1021(isNatural(activate(V1)), activate(V2))
U1021(tt, V2) → ACTIVATE(V2)
U1011(tt, V1, V2) → ISNATURAL(activate(V1))
U1011(tt, V1, V2) → ACTIVATE(V1)
U1011(tt, V1, V2) → ACTIVATE(V2)
ISLNAT(n__take(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISLNAT(n__take(V1, V2)) → ISNATURALKIND(activate(V1))
ISLNAT(n__take(V1, V2)) → ACTIVATE(V1)
ISLNAT(n__take(V1, V2)) → ACTIVATE(V2)
U911(tt, V1) → ACTIVATE(V1)
U1521(tt, V2) → ACTIVATE(V2)
U1511(tt, V1, V2) → ISNATURAL(activate(V1))
U1511(tt, V1, V2) → ACTIVATE(V1)
U1511(tt, V1, V2) → ACTIVATE(V2)
ISPLNAT(n__splitAt(V1, V2)) → AND(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
ISPLNAT(n__splitAt(V1, V2)) → ISNATURALKIND(activate(V1))
ISPLNAT(n__splitAt(V1, V2)) → ACTIVATE(V1)
ISPLNAT(n__splitAt(V1, V2)) → ACTIVATE(V2)
U811(tt, V1) → ACTIVATE(V1)
U1421(tt, V2) → ACTIVATE(V2)
U1411(tt, V1, V2) → ISLNAT(activate(V1))
U1411(tt, V1, V2) → ACTIVATE(V1)
U1411(tt, V1, V2) → ACTIVATE(V2)
U611(tt, V1) → ACTIVATE(V1)
U1321(tt, V2) → ACTIVATE(V2)
U1311(tt, V1, V2) → ISNATURAL(activate(V1))
U1311(tt, V1, V2) → ACTIVATE(V1)
U1311(tt, V1, V2) → ACTIVATE(V2)
U1211(tt, V1) → ACTIVATE(V1)
SPLITAT(0, XS) → AND(isLNat(XS), n__isLNatKind(XS))
SPLITAT(0, XS) → ISLNAT(XS)
SPLITAT(s(N), cons(X, XS)) → U2011(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS))
U2011(tt, N, X, XS) → U2021(splitAt(activate(N), activate(XS)), activate(X))
U2021(pair(YS, ZS), X) → ACTIVATE(X)
U2011(tt, N, X, XS) → SPLITAT(activate(N), activate(XS))
SPLITAT(s(N), cons(X, XS)) → AND(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))))
SPLITAT(s(N), cons(X, XS)) → AND(isNatural(N), n__isNaturalKind(N))
SPLITAT(s(N), cons(X, XS)) → ISNATURAL(N)
SPLITAT(s(N), cons(X, XS)) → ACTIVATE(XS)
U2011(tt, N, X, XS) → ACTIVATE(N)
U2011(tt, N, X, XS) → ACTIVATE(XS)
U2011(tt, N, X, XS) → ACTIVATE(X)
U521(tt, V2) → ACTIVATE(V2)
U511(tt, V1, V2) → ISNATURAL(activate(V1))
U511(tt, V1, V2) → ACTIVATE(V1)
U511(tt, V1, V2) → ACTIVATE(V2)
U1111(tt, V1) → ACTIVATE(V1)
HEAD(cons(N, XS)) → ACTIVATE(XS)
U1711(tt, N, XS) → AFTERNTH(activate(N), activate(XS))
AFTERNTH(N, XS) → AND(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS)))
AFTERNTH(N, XS) → AND(isNatural(N), n__isNaturalKind(N))
AFTERNTH(N, XS) → ISNATURAL(N)
U1711(tt, N, XS) → ACTIVATE(N)
U1711(tt, N, XS) → ACTIVATE(XS)
SEL(N, XS) → AND(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS)))
SEL(N, XS) → AND(isNatural(N), n__isNaturalKind(N))
SEL(N, XS) → ISNATURAL(N)
U2211(tt, N, XS) → SPLITAT(activate(N), activate(XS))
U2211(tt, N, XS) → ACTIVATE(N)
U2211(tt, N, XS) → ACTIVATE(XS)
TAKE(N, XS) → AND(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS)))
TAKE(N, XS) → AND(isNatural(N), n__isNaturalKind(N))
TAKE(N, XS) → ISNATURAL(N)
TAIL(cons(N, XS)) → AND(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))
TAIL(cons(N, XS)) → AND(isNatural(N), n__isNaturalKind(N))
TAIL(cons(N, XS)) → ISNATURAL(N)
TAIL(cons(N, XS)) → ACTIVATE(XS)
U111(tt, N, XS) → SPLITAT(activate(N), activate(XS))
U111(tt, N, XS) → ACTIVATE(N)
U111(tt, N, XS) → ACTIVATE(XS)
NATSFROM(N) → AND(isNatural(N), n__isNaturalKind(N))
NATSFROM(N) → ISNATURAL(N)
U421(tt, V2) → ACTIVATE(V2)
U411(tt, V1, V2) → ISNATURAL(activate(V1))
U411(tt, V1, V2) → ACTIVATE(V1)
U411(tt, V1, V2) → ACTIVATE(V2)

The TRS R consists of the following rules:

U101(tt, V1, V2) → U102(isNatural(activate(V1)), activate(V2))
U102(tt, V2) → U103(isLNat(activate(V2)))
U103(tt) → tt
U11(tt, N, XS) → snd(splitAt(activate(N), activate(XS)))
U111(tt, V1) → U112(isLNat(activate(V1)))
U112(tt) → tt
U121(tt, V1) → U122(isNatural(activate(V1)))
U122(tt) → tt
U131(tt, V1, V2) → U132(isNatural(activate(V1)), activate(V2))
U132(tt, V2) → U133(isLNat(activate(V2)))
U133(tt) → tt
U141(tt, V1, V2) → U142(isLNat(activate(V1)), activate(V2))
U142(tt, V2) → U143(isLNat(activate(V2)))
U143(tt) → tt
U151(tt, V1, V2) → U152(isNatural(activate(V1)), activate(V2))
U152(tt, V2) → U153(isLNat(activate(V2)))
U153(tt) → tt
U161(tt, N) → cons(activate(N), n__natsFrom(n__s(activate(N))))
U171(tt, N, XS) → head(afterNth(activate(N), activate(XS)))
U181(tt, Y) → activate(Y)
U191(tt, XS) → pair(nil, activate(XS))
U201(tt, N, X, XS) → U202(splitAt(activate(N), activate(XS)), activate(X))
U202(pair(YS, ZS), X) → pair(cons(activate(X), YS), ZS)
U21(tt, X) → activate(X)
U211(tt, XS) → activate(XS)
U221(tt, N, XS) → fst(splitAt(activate(N), activate(XS)))
U31(tt, N) → activate(N)
U41(tt, V1, V2) → U42(isNatural(activate(V1)), activate(V2))
U42(tt, V2) → U43(isLNat(activate(V2)))
U43(tt) → tt
U51(tt, V1, V2) → U52(isNatural(activate(V1)), activate(V2))
U52(tt, V2) → U53(isLNat(activate(V2)))
U53(tt) → tt
U61(tt, V1) → U62(isPLNat(activate(V1)))
U62(tt) → tt
U71(tt, V1) → U72(isNatural(activate(V1)))
U72(tt) → tt
U81(tt, V1) → U82(isPLNat(activate(V1)))
U82(tt) → tt
U91(tt, V1) → U92(isLNat(activate(V1)))
U92(tt) → tt
afterNth(N, XS) → U11(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
and(tt, X) → activate(X)
fst(pair(X, Y)) → U21(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X)
head(cons(N, XS)) → U31(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N)
isLNat(n__nil) → tt
isLNat(n__afterNth(V1, V2)) → U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isLNat(n__cons(V1, V2)) → U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isLNat(n__fst(V1)) → U61(isPLNatKind(activate(V1)), activate(V1))
isLNat(n__natsFrom(V1)) → U71(isNaturalKind(activate(V1)), activate(V1))
isLNat(n__snd(V1)) → U81(isPLNatKind(activate(V1)), activate(V1))
isLNat(n__tail(V1)) → U91(isLNatKind(activate(V1)), activate(V1))
isLNat(n__take(V1, V2)) → U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isLNatKind(n__nil) → tt
isLNatKind(n__afterNth(V1, V2)) → and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
isLNatKind(n__cons(V1, V2)) → and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
isLNatKind(n__fst(V1)) → isPLNatKind(activate(V1))
isLNatKind(n__natsFrom(V1)) → isNaturalKind(activate(V1))
isLNatKind(n__snd(V1)) → isPLNatKind(activate(V1))
isLNatKind(n__tail(V1)) → isLNatKind(activate(V1))
isLNatKind(n__take(V1, V2)) → and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
isNatural(n__0) → tt
isNatural(n__head(V1)) → U111(isLNatKind(activate(V1)), activate(V1))
isNatural(n__s(V1)) → U121(isNaturalKind(activate(V1)), activate(V1))
isNatural(n__sel(V1, V2)) → U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isNaturalKind(n__0) → tt
isNaturalKind(n__head(V1)) → isLNatKind(activate(V1))
isNaturalKind(n__s(V1)) → isNaturalKind(activate(V1))
isNaturalKind(n__sel(V1, V2)) → and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
isPLNat(n__pair(V1, V2)) → U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isPLNat(n__splitAt(V1, V2)) → U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))
isPLNatKind(n__pair(V1, V2)) → and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))
isPLNatKind(n__splitAt(V1, V2)) → and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))
natsFrom(N) → U161(and(isNatural(N), n__isNaturalKind(N)), N)
sel(N, XS) → U171(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
snd(pair(X, Y)) → U181(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y)
splitAt(0, XS) → U191(and(isLNat(XS), n__isLNatKind(XS)), XS)
splitAt(s(N), cons(X, XS)) → U201(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS))
tail(cons(N, XS)) → U211(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS))
take(N, XS) → U221(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)
natsFrom(X) → n__natsFrom(X)
s(X) → n__s(X)
isNaturalKind(X) → n__isNaturalKind(X)
and(X1, X2) → n__and(X1, X2)
isLNat(X) → n__isLNat(X)
isLNatKind(X) → n__isLNatKind(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)
sel(X1, X2) → n__sel(X1, X2)
pair(X1, X2) → n__pair(X1, X2)
splitAt(X1, X2) → n__splitAt(X1, X2)
isNatural(X) → n__isNatural(X)
activate(n__natsFrom(X)) → natsFrom(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__isNaturalKind(X)) → isNaturalKind(X)
activate(n__and(X1, X2)) → and(activate(X1), X2)
activate(n__isLNat(X)) → isLNat(X)
activate(n__isLNatKind(X)) → isLNatKind(X)
activate(n__nil) → nil
activate(n__afterNth(X1, X2)) → afterNth(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__fst(X)) → fst(activate(X))
activate(n__snd(X)) → snd(activate(X))
activate(n__tail(X)) → tail(activate(X))
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__head(X)) → head(activate(X))
activate(n__sel(X1, X2)) → sel(activate(X1), activate(X2))
activate(n__pair(X1, X2)) → pair(activate(X1), activate(X2))
activate(n__splitAt(X1, X2)) → splitAt(activate(X1), activate(X2))
activate(n__isNatural(X)) → isNatural(X)
activate(X) → X

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