Termination w.r.t. Q proof of /tmp/tmpptvFIl/LISTUTILITIES_complete-noand

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(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U102(tt, V1, V2) → U103(isLNatKind(activate(V2)), activate(V1), activate(V2))
U103(tt, V1, V2) → U104(isLNatKind(activate(V2)), activate(V1), activate(V2))
U104(tt, V1, V2) → U105(isNatural(activate(V1)), activate(V2))
U105(tt, V2) → U106(isLNat(activate(V2)))
U106(tt) → tt
U11(tt, N, XS) → U12(isNaturalKind(activate(N)), activate(N), activate(XS))
U111(tt, V2) → U112(isLNatKind(activate(V2)))
U112(tt) → tt
U12(tt, N, XS) → U13(isLNat(activate(XS)), activate(N), activate(XS))
U121(tt, V2) → U122(isLNatKind(activate(V2)))
U122(tt) → tt
U13(tt, N, XS) → U14(isLNatKind(activate(XS)), activate(N), activate(XS))
U131(tt) → tt
U14(tt, N, XS) → snd(splitAt(activate(N), activate(XS)))
U141(tt) → tt
U151(tt) → tt
U161(tt) → tt
U171(tt, V2) → U172(isLNatKind(activate(V2)))
U172(tt) → tt
U181(tt, V1) → U182(isLNatKind(activate(V1)), activate(V1))
U182(tt, V1) → U183(isLNat(activate(V1)))
U183(tt) → tt
U191(tt, V1) → U192(isNaturalKind(activate(V1)), activate(V1))
U192(tt, V1) → U193(isNatural(activate(V1)))
U193(tt) → tt
U201(tt, V1, V2) → U202(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U202(tt, V1, V2) → U203(isLNatKind(activate(V2)), activate(V1), activate(V2))
U203(tt, V1, V2) → U204(isLNatKind(activate(V2)), activate(V1), activate(V2))
U204(tt, V1, V2) → U205(isNatural(activate(V1)), activate(V2))
U205(tt, V2) → U206(isLNat(activate(V2)))
U206(tt) → tt
U21(tt, X, Y) → U22(isLNatKind(activate(X)), activate(X), activate(Y))
U211(tt) → tt
U22(tt, X, Y) → U23(isLNat(activate(Y)), activate(X), activate(Y))
U221(tt) → tt
U23(tt, X, Y) → U24(isLNatKind(activate(Y)), activate(X))
U231(tt, V2) → U232(isLNatKind(activate(V2)))
U232(tt) → tt
U24(tt, X) → activate(X)
U241(tt, V1, V2) → U242(isLNatKind(activate(V1)), activate(V1), activate(V2))
U242(tt, V1, V2) → U243(isLNatKind(activate(V2)), activate(V1), activate(V2))
U243(tt, V1, V2) → U244(isLNatKind(activate(V2)), activate(V1), activate(V2))
U244(tt, V1, V2) → U245(isLNat(activate(V1)), activate(V2))
U245(tt, V2) → U246(isLNat(activate(V2)))
U246(tt) → tt
U251(tt, V1, V2) → U252(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U252(tt, V1, V2) → U253(isLNatKind(activate(V2)), activate(V1), activate(V2))
U253(tt, V1, V2) → U254(isLNatKind(activate(V2)), activate(V1), activate(V2))
U254(tt, V1, V2) → U255(isNatural(activate(V1)), activate(V2))
U255(tt, V2) → U256(isLNat(activate(V2)))
U256(tt) → tt
U261(tt, V2) → U262(isLNatKind(activate(V2)))
U262(tt) → tt
U271(tt, V2) → U272(isLNatKind(activate(V2)))
U272(tt) → tt
U281(tt, N) → U282(isNaturalKind(activate(N)), activate(N))
U282(tt, N) → cons(activate(N), n__natsFrom(n__s(activate(N))))
U291(tt, N, XS) → U292(isNaturalKind(activate(N)), activate(N), activate(XS))
U292(tt, N, XS) → U293(isLNat(activate(XS)), activate(N), activate(XS))
U293(tt, N, XS) → U294(isLNatKind(activate(XS)), activate(N), activate(XS))
U294(tt, N, XS) → head(afterNth(activate(N), activate(XS)))
U301(tt, X, Y) → U302(isLNatKind(activate(X)), activate(Y))
U302(tt, Y) → U303(isLNat(activate(Y)), activate(Y))
U303(tt, Y) → U304(isLNatKind(activate(Y)), activate(Y))
U304(tt, Y) → activate(Y)
U31(tt, N, XS) → U32(isNaturalKind(activate(N)), activate(N), activate(XS))
U311(tt, XS) → U312(isLNatKind(activate(XS)), activate(XS))
U312(tt, XS) → pair(nil, activate(XS))
U32(tt, N, XS) → U33(isLNat(activate(XS)), activate(N), activate(XS))
U321(tt, N, X, XS) → U322(isNaturalKind(activate(N)), activate(N), activate(X), activate(XS))
U322(tt, N, X, XS) → U323(isNatural(activate(X)), activate(N), activate(X), activate(XS))
U323(tt, N, X, XS) → U324(isNaturalKind(activate(X)), activate(N), activate(X), activate(XS))
U324(tt, N, X, XS) → U325(isLNat(activate(XS)), activate(N), activate(X), activate(XS))
U325(tt, N, X, XS) → U326(isLNatKind(activate(XS)), activate(N), activate(X), activate(XS))
U326(tt, N, X, XS) → U327(splitAt(activate(N), activate(XS)), activate(X))
U327(pair(YS, ZS), X) → pair(cons(activate(X), YS), ZS)
U33(tt, N, XS) → U34(isLNatKind(activate(XS)), activate(N))
U331(tt, N, XS) → U332(isNaturalKind(activate(N)), activate(XS))
U332(tt, XS) → U333(isLNat(activate(XS)), activate(XS))
U333(tt, XS) → U334(isLNatKind(activate(XS)), activate(XS))
U334(tt, XS) → activate(XS)
U34(tt, N) → activate(N)
U341(tt, N, XS) → U342(isNaturalKind(activate(N)), activate(N), activate(XS))
U342(tt, N, XS) → U343(isLNat(activate(XS)), activate(N), activate(XS))
U343(tt, N, XS) → U344(isLNatKind(activate(XS)), activate(N), activate(XS))
U344(tt, N, XS) → fst(splitAt(activate(N), activate(XS)))
U41(tt, V1, V2) → U42(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isLNatKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isLNatKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isNatural(activate(V1)), activate(V2))
U45(tt, V2) → U46(isLNat(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isLNatKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isLNatKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNatural(activate(V1)), activate(V2))
U55(tt, V2) → U56(isLNat(activate(V2)))
U56(tt) → tt
U61(tt, V1) → U62(isPLNatKind(activate(V1)), activate(V1))
U62(tt, V1) → U63(isPLNat(activate(V1)))
U63(tt) → tt
U71(tt, V1) → U72(isNaturalKind(activate(V1)), activate(V1))
U72(tt, V1) → U73(isNatural(activate(V1)))
U73(tt) → tt
U81(tt, V1) → U82(isPLNatKind(activate(V1)), activate(V1))
U82(tt, V1) → U83(isPLNat(activate(V1)))
U83(tt) → tt
U91(tt, V1) → U92(isLNatKind(activate(V1)), activate(V1))
U92(tt, V1) → U93(isLNat(activate(V1)))
U93(tt) → tt
afterNth(N, XS) → U11(isNatural(N), N, XS)
fst(pair(X, Y)) → U21(isLNat(X), X, Y)
head(cons(N, XS)) → U31(isNatural(N), N, activate(XS))
isLNat(n__nil) → tt
isLNat(n__afterNth(V1, V2)) → U41(isNaturalKind(activate(V1)), activate(V1), activate(V2))
isLNat(n__cons(V1, V2)) → U51(isNaturalKind(activate(V1)), 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(isNaturalKind(activate(V1)), activate(V1), activate(V2))
isLNatKind(n__nil) → tt
isLNatKind(n__afterNth(V1, V2)) → U111(isNaturalKind(activate(V1)), activate(V2))
isLNatKind(n__cons(V1, V2)) → U121(isNaturalKind(activate(V1)), activate(V2))
isLNatKind(n__fst(V1)) → U131(isPLNatKind(activate(V1)))
isLNatKind(n__natsFrom(V1)) → U141(isNaturalKind(activate(V1)))
isLNatKind(n__snd(V1)) → U151(isPLNatKind(activate(V1)))
isLNatKind(n__tail(V1)) → U161(isLNatKind(activate(V1)))
isLNatKind(n__take(V1, V2)) → U171(isNaturalKind(activate(V1)), activate(V2))
isNatural(n__0) → tt
isNatural(n__head(V1)) → U181(isLNatKind(activate(V1)), activate(V1))
isNatural(n__s(V1)) → U191(isNaturalKind(activate(V1)), activate(V1))
isNatural(n__sel(V1, V2)) → U201(isNaturalKind(activate(V1)), activate(V1), activate(V2))
isNaturalKind(n__0) → tt
isNaturalKind(n__head(V1)) → U211(isLNatKind(activate(V1)))
isNaturalKind(n__s(V1)) → U221(isNaturalKind(activate(V1)))
isNaturalKind(n__sel(V1, V2)) → U231(isNaturalKind(activate(V1)), activate(V2))
isPLNat(n__pair(V1, V2)) → U241(isLNatKind(activate(V1)), activate(V1), activate(V2))
isPLNat(n__splitAt(V1, V2)) → U251(isNaturalKind(activate(V1)), activate(V1), activate(V2))
isPLNatKind(n__pair(V1, V2)) → U261(isLNatKind(activate(V1)), activate(V2))
isPLNatKind(n__splitAt(V1, V2)) → U271(isNaturalKind(activate(V1)), activate(V2))
natsFrom(N) → U281(isNatural(N), N)
sel(N, XS) → U291(isNatural(N), N, XS)
snd(pair(X, Y)) → U301(isLNat(X), X, Y)
splitAt(0, XS) → U311(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U321(isNatural(N), N, X, activate(XS))
tail(cons(N, XS)) → U331(isNatural(N), N, activate(XS))
take(N, XS) → U341(isNatural(N), N, XS)
natsFrom(X) → n__natsFrom(X)
s(X) → n__s(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)
activate(n__natsFrom(X)) → natsFrom(activate(X))
activate(n__s(X)) → s(activate(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(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, V1, V2) → U102¹(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U101¹(tt, V1, V2) → ISNATURALKIND(activate(V1))
U101¹(tt, V1, V2) → ACTIVATE(V1)
U101¹(tt, V1, V2) → ACTIVATE(V2)
U102¹(tt, V1, V2) → U103¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U102¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U102¹(tt, V1, V2) → ACTIVATE(V2)
U102¹(tt, V1, V2) → ACTIVATE(V1)
U103¹(tt, V1, V2) → U104¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U103¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U103¹(tt, V1, V2) → ACTIVATE(V2)
U103¹(tt, V1, V2) → ACTIVATE(V1)
U104¹(tt, V1, V2) → U105¹(isNatural(activate(V1)), activate(V2))
U104¹(tt, V1, V2) → ISNATURAL(activate(V1))
U104¹(tt, V1, V2) → ACTIVATE(V1)
U104¹(tt, V1, V2) → ACTIVATE(V2)
U105¹(tt, V2) → U106¹(isLNat(activate(V2)))
U105¹(tt, V2) → ISLNAT(activate(V2))
U105¹(tt, V2) → ACTIVATE(V2)
U11¹(tt, N, XS) → U12¹(isNaturalKind(activate(N)), activate(N), activate(XS))
U11¹(tt, N, XS) → ISNATURALKIND(activate(N))
U11¹(tt, N, XS) → ACTIVATE(N)
U11¹(tt, N, XS) → ACTIVATE(XS)
U111¹(tt, V2) → U112¹(isLNatKind(activate(V2)))
U111¹(tt, V2) → ISLNATKIND(activate(V2))
U111¹(tt, V2) → ACTIVATE(V2)
U12¹(tt, N, XS) → U13¹(isLNat(activate(XS)), activate(N), activate(XS))
U12¹(tt, N, XS) → ISLNAT(activate(XS))
U12¹(tt, N, XS) → ACTIVATE(XS)
U12¹(tt, N, XS) → ACTIVATE(N)
U121¹(tt, V2) → U122¹(isLNatKind(activate(V2)))
U121¹(tt, V2) → ISLNATKIND(activate(V2))
U121¹(tt, V2) → ACTIVATE(V2)
U13¹(tt, N, XS) → U14¹(isLNatKind(activate(XS)), activate(N), activate(XS))
U13¹(tt, N, XS) → ISLNATKIND(activate(XS))
U13¹(tt, N, XS) → ACTIVATE(XS)
U13¹(tt, N, XS) → ACTIVATE(N)
U14¹(tt, N, XS) → SND(splitAt(activate(N), activate(XS)))
U14¹(tt, N, XS) → SPLITAT(activate(N), activate(XS))
U14¹(tt, N, XS) → ACTIVATE(N)
U14¹(tt, N, XS) → ACTIVATE(XS)
U171¹(tt, V2) → U172¹(isLNatKind(activate(V2)))
U171¹(tt, V2) → ISLNATKIND(activate(V2))
U171¹(tt, V2) → ACTIVATE(V2)
U181¹(tt, V1) → U182¹(isLNatKind(activate(V1)), activate(V1))
U181¹(tt, V1) → ISLNATKIND(activate(V1))
U181¹(tt, V1) → ACTIVATE(V1)
U182¹(tt, V1) → U183¹(isLNat(activate(V1)))
U182¹(tt, V1) → ISLNAT(activate(V1))
U182¹(tt, V1) → ACTIVATE(V1)
U191¹(tt, V1) → U192¹(isNaturalKind(activate(V1)), activate(V1))
U191¹(tt, V1) → ISNATURALKIND(activate(V1))
U191¹(tt, V1) → ACTIVATE(V1)
U192¹(tt, V1) → U193¹(isNatural(activate(V1)))
U192¹(tt, V1) → ISNATURAL(activate(V1))
U192¹(tt, V1) → ACTIVATE(V1)
U201¹(tt, V1, V2) → U202¹(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U201¹(tt, V1, V2) → ISNATURALKIND(activate(V1))
U201¹(tt, V1, V2) → ACTIVATE(V1)
U201¹(tt, V1, V2) → ACTIVATE(V2)
U202¹(tt, V1, V2) → U203¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U202¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U202¹(tt, V1, V2) → ACTIVATE(V2)
U202¹(tt, V1, V2) → ACTIVATE(V1)
U203¹(tt, V1, V2) → U204¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U203¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U203¹(tt, V1, V2) → ACTIVATE(V2)
U203¹(tt, V1, V2) → ACTIVATE(V1)
U204¹(tt, V1, V2) → U205¹(isNatural(activate(V1)), activate(V2))
U204¹(tt, V1, V2) → ISNATURAL(activate(V1))
U204¹(tt, V1, V2) → ACTIVATE(V1)
U204¹(tt, V1, V2) → ACTIVATE(V2)
U205¹(tt, V2) → U206¹(isLNat(activate(V2)))
U205¹(tt, V2) → ISLNAT(activate(V2))
U205¹(tt, V2) → ACTIVATE(V2)
U21¹(tt, X, Y) → U22¹(isLNatKind(activate(X)), activate(X), activate(Y))
U21¹(tt, X, Y) → ISLNATKIND(activate(X))
U21¹(tt, X, Y) → ACTIVATE(X)
U21¹(tt, X, Y) → ACTIVATE(Y)
U22¹(tt, X, Y) → U23¹(isLNat(activate(Y)), activate(X), activate(Y))
U22¹(tt, X, Y) → ISLNAT(activate(Y))
U22¹(tt, X, Y) → ACTIVATE(Y)
U22¹(tt, X, Y) → ACTIVATE(X)
U23¹(tt, X, Y) → U24¹(isLNatKind(activate(Y)), activate(X))
U23¹(tt, X, Y) → ISLNATKIND(activate(Y))
U23¹(tt, X, Y) → ACTIVATE(Y)
U23¹(tt, X, Y) → ACTIVATE(X)
U231¹(tt, V2) → U232¹(isLNatKind(activate(V2)))
U231¹(tt, V2) → ISLNATKIND(activate(V2))
U231¹(tt, V2) → ACTIVATE(V2)
U24¹(tt, X) → ACTIVATE(X)
U241¹(tt, V1, V2) → U242¹(isLNatKind(activate(V1)), activate(V1), activate(V2))
U241¹(tt, V1, V2) → ISLNATKIND(activate(V1))
U241¹(tt, V1, V2) → ACTIVATE(V1)
U241¹(tt, V1, V2) → ACTIVATE(V2)
U242¹(tt, V1, V2) → U243¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U242¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U242¹(tt, V1, V2) → ACTIVATE(V2)
U242¹(tt, V1, V2) → ACTIVATE(V1)
U243¹(tt, V1, V2) → U244¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U243¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U243¹(tt, V1, V2) → ACTIVATE(V2)
U243¹(tt, V1, V2) → ACTIVATE(V1)
U244¹(tt, V1, V2) → U245¹(isLNat(activate(V1)), activate(V2))
U244¹(tt, V1, V2) → ISLNAT(activate(V1))
U244¹(tt, V1, V2) → ACTIVATE(V1)
U244¹(tt, V1, V2) → ACTIVATE(V2)
U245¹(tt, V2) → U246¹(isLNat(activate(V2)))
U245¹(tt, V2) → ISLNAT(activate(V2))
U245¹(tt, V2) → ACTIVATE(V2)
U251¹(tt, V1, V2) → U252¹(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U251¹(tt, V1, V2) → ISNATURALKIND(activate(V1))
U251¹(tt, V1, V2) → ACTIVATE(V1)
U251¹(tt, V1, V2) → ACTIVATE(V2)
U252¹(tt, V1, V2) → U253¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U252¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U252¹(tt, V1, V2) → ACTIVATE(V2)
U252¹(tt, V1, V2) → ACTIVATE(V1)
U253¹(tt, V1, V2) → U254¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U253¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U253¹(tt, V1, V2) → ACTIVATE(V2)
U253¹(tt, V1, V2) → ACTIVATE(V1)
U254¹(tt, V1, V2) → U255¹(isNatural(activate(V1)), activate(V2))
U254¹(tt, V1, V2) → ISNATURAL(activate(V1))
U254¹(tt, V1, V2) → ACTIVATE(V1)
U254¹(tt, V1, V2) → ACTIVATE(V2)
U255¹(tt, V2) → U256¹(isLNat(activate(V2)))
U255¹(tt, V2) → ISLNAT(activate(V2))
U255¹(tt, V2) → ACTIVATE(V2)
U261¹(tt, V2) → U262¹(isLNatKind(activate(V2)))
U261¹(tt, V2) → ISLNATKIND(activate(V2))
U261¹(tt, V2) → ACTIVATE(V2)
U271¹(tt, V2) → U272¹(isLNatKind(activate(V2)))
U271¹(tt, V2) → ISLNATKIND(activate(V2))
U271¹(tt, V2) → ACTIVATE(V2)
U281¹(tt, N) → U282¹(isNaturalKind(activate(N)), activate(N))
U281¹(tt, N) → ISNATURALKIND(activate(N))
U281¹(tt, N) → ACTIVATE(N)
U282¹(tt, N) → CONS(activate(N), n__natsFrom(n__s(activate(N))))
U282¹(tt, N) → ACTIVATE(N)
U291¹(tt, N, XS) → U292¹(isNaturalKind(activate(N)), activate(N), activate(XS))
U291¹(tt, N, XS) → ISNATURALKIND(activate(N))
U291¹(tt, N, XS) → ACTIVATE(N)
U291¹(tt, N, XS) → ACTIVATE(XS)
U292¹(tt, N, XS) → U293¹(isLNat(activate(XS)), activate(N), activate(XS))
U292¹(tt, N, XS) → ISLNAT(activate(XS))
U292¹(tt, N, XS) → ACTIVATE(XS)
U292¹(tt, N, XS) → ACTIVATE(N)
U293¹(tt, N, XS) → U294¹(isLNatKind(activate(XS)), activate(N), activate(XS))
U293¹(tt, N, XS) → ISLNATKIND(activate(XS))
U293¹(tt, N, XS) → ACTIVATE(XS)
U293¹(tt, N, XS) → ACTIVATE(N)
U294¹(tt, N, XS) → HEAD(afterNth(activate(N), activate(XS)))
U294¹(tt, N, XS) → AFTERNTH(activate(N), activate(XS))
U294¹(tt, N, XS) → ACTIVATE(N)
U294¹(tt, N, XS) → ACTIVATE(XS)
U301¹(tt, X, Y) → U302¹(isLNatKind(activate(X)), activate(Y))
U301¹(tt, X, Y) → ISLNATKIND(activate(X))
U301¹(tt, X, Y) → ACTIVATE(X)
U301¹(tt, X, Y) → ACTIVATE(Y)
U302¹(tt, Y) → U303¹(isLNat(activate(Y)), activate(Y))
U302¹(tt, Y) → ISLNAT(activate(Y))
U302¹(tt, Y) → ACTIVATE(Y)
U303¹(tt, Y) → U304¹(isLNatKind(activate(Y)), activate(Y))
U303¹(tt, Y) → ISLNATKIND(activate(Y))
U303¹(tt, Y) → ACTIVATE(Y)
U304¹(tt, Y) → ACTIVATE(Y)
U31¹(tt, N, XS) → U32¹(isNaturalKind(activate(N)), activate(N), activate(XS))
U31¹(tt, N, XS) → ISNATURALKIND(activate(N))
U31¹(tt, N, XS) → ACTIVATE(N)
U31¹(tt, N, XS) → ACTIVATE(XS)
U311¹(tt, XS) → U312¹(isLNatKind(activate(XS)), activate(XS))
U311¹(tt, XS) → ISLNATKIND(activate(XS))
U311¹(tt, XS) → ACTIVATE(XS)
U312¹(tt, XS) → PAIR(nil, activate(XS))
U312¹(tt, XS) → NIL
U312¹(tt, XS) → ACTIVATE(XS)
U32¹(tt, N, XS) → U33¹(isLNat(activate(XS)), activate(N), activate(XS))
U32¹(tt, N, XS) → ISLNAT(activate(XS))
U32¹(tt, N, XS) → ACTIVATE(XS)
U32¹(tt, N, XS) → ACTIVATE(N)
U321¹(tt, N, X, XS) → U322¹(isNaturalKind(activate(N)), activate(N), activate(X), activate(XS))
U321¹(tt, N, X, XS) → ISNATURALKIND(activate(N))
U321¹(tt, N, X, XS) → ACTIVATE(N)
U321¹(tt, N, X, XS) → ACTIVATE(X)
U321¹(tt, N, X, XS) → ACTIVATE(XS)
U322¹(tt, N, X, XS) → U323¹(isNatural(activate(X)), activate(N), activate(X), activate(XS))
U322¹(tt, N, X, XS) → ISNATURAL(activate(X))
U322¹(tt, N, X, XS) → ACTIVATE(X)
U322¹(tt, N, X, XS) → ACTIVATE(N)
U322¹(tt, N, X, XS) → ACTIVATE(XS)
U323¹(tt, N, X, XS) → U324¹(isNaturalKind(activate(X)), activate(N), activate(X), activate(XS))
U323¹(tt, N, X, XS) → ISNATURALKIND(activate(X))
U323¹(tt, N, X, XS) → ACTIVATE(X)
U323¹(tt, N, X, XS) → ACTIVATE(N)
U323¹(tt, N, X, XS) → ACTIVATE(XS)
U324¹(tt, N, X, XS) → U325¹(isLNat(activate(XS)), activate(N), activate(X), activate(XS))
U324¹(tt, N, X, XS) → ISLNAT(activate(XS))
U324¹(tt, N, X, XS) → ACTIVATE(XS)
U324¹(tt, N, X, XS) → ACTIVATE(N)
U324¹(tt, N, X, XS) → ACTIVATE(X)
U325¹(tt, N, X, XS) → U326¹(isLNatKind(activate(XS)), activate(N), activate(X), activate(XS))
U325¹(tt, N, X, XS) → ISLNATKIND(activate(XS))
U325¹(tt, N, X, XS) → ACTIVATE(XS)
U325¹(tt, N, X, XS) → ACTIVATE(N)
U325¹(tt, N, X, XS) → ACTIVATE(X)
U326¹(tt, N, X, XS) → U327¹(splitAt(activate(N), activate(XS)), activate(X))
U326¹(tt, N, X, XS) → SPLITAT(activate(N), activate(XS))
U326¹(tt, N, X, XS) → ACTIVATE(N)
U326¹(tt, N, X, XS) → ACTIVATE(XS)
U326¹(tt, N, X, XS) → ACTIVATE(X)
U327¹(pair(YS, ZS), X) → PAIR(cons(activate(X), YS), ZS)
U327¹(pair(YS, ZS), X) → CONS(activate(X), YS)
U327¹(pair(YS, ZS), X) → ACTIVATE(X)
U33¹(tt, N, XS) → U34¹(isLNatKind(activate(XS)), activate(N))
U33¹(tt, N, XS) → ISLNATKIND(activate(XS))
U33¹(tt, N, XS) → ACTIVATE(XS)
U33¹(tt, N, XS) → ACTIVATE(N)
U331¹(tt, N, XS) → U332¹(isNaturalKind(activate(N)), activate(XS))
U331¹(tt, N, XS) → ISNATURALKIND(activate(N))
U331¹(tt, N, XS) → ACTIVATE(N)
U331¹(tt, N, XS) → ACTIVATE(XS)
U332¹(tt, XS) → U333¹(isLNat(activate(XS)), activate(XS))
U332¹(tt, XS) → ISLNAT(activate(XS))
U332¹(tt, XS) → ACTIVATE(XS)
U333¹(tt, XS) → U334¹(isLNatKind(activate(XS)), activate(XS))
U333¹(tt, XS) → ISLNATKIND(activate(XS))
U333¹(tt, XS) → ACTIVATE(XS)
U334¹(tt, XS) → ACTIVATE(XS)
U34¹(tt, N) → ACTIVATE(N)
U341¹(tt, N, XS) → U342¹(isNaturalKind(activate(N)), activate(N), activate(XS))
U341¹(tt, N, XS) → ISNATURALKIND(activate(N))
U341¹(tt, N, XS) → ACTIVATE(N)
U341¹(tt, N, XS) → ACTIVATE(XS)
U342¹(tt, N, XS) → U343¹(isLNat(activate(XS)), activate(N), activate(XS))
U342¹(tt, N, XS) → ISLNAT(activate(XS))
U342¹(tt, N, XS) → ACTIVATE(XS)
U342¹(tt, N, XS) → ACTIVATE(N)
U343¹(tt, N, XS) → U344¹(isLNatKind(activate(XS)), activate(N), activate(XS))
U343¹(tt, N, XS) → ISLNATKIND(activate(XS))
U343¹(tt, N, XS) → ACTIVATE(XS)
U343¹(tt, N, XS) → ACTIVATE(N)
U344¹(tt, N, XS) → FST(splitAt(activate(N), activate(XS)))
U344¹(tt, N, XS) → SPLITAT(activate(N), activate(XS))
U344¹(tt, N, XS) → ACTIVATE(N)
U344¹(tt, N, XS) → ACTIVATE(XS)
U41¹(tt, V1, V2) → U42¹(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U41¹(tt, V1, V2) → ISNATURALKIND(activate(V1))
U41¹(tt, V1, V2) → ACTIVATE(V1)
U41¹(tt, V1, V2) → ACTIVATE(V2)
U42¹(tt, V1, V2) → U43¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U42¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U42¹(tt, V1, V2) → ACTIVATE(V2)
U42¹(tt, V1, V2) → ACTIVATE(V1)
U43¹(tt, V1, V2) → U44¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U43¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U43¹(tt, V1, V2) → ACTIVATE(V2)
U43¹(tt, V1, V2) → ACTIVATE(V1)
U44¹(tt, V1, V2) → U45¹(isNatural(activate(V1)), activate(V2))
U44¹(tt, V1, V2) → ISNATURAL(activate(V1))
U44¹(tt, V1, V2) → ACTIVATE(V1)
U44¹(tt, V1, V2) → ACTIVATE(V2)
U45¹(tt, V2) → U46¹(isLNat(activate(V2)))
U45¹(tt, V2) → ISLNAT(activate(V2))
U45¹(tt, V2) → ACTIVATE(V2)
U51¹(tt, V1, V2) → U52¹(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U51¹(tt, V1, V2) → ISNATURALKIND(activate(V1))
U51¹(tt, V1, V2) → ACTIVATE(V1)
U51¹(tt, V1, V2) → ACTIVATE(V2)
U52¹(tt, V1, V2) → U53¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U52¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U52¹(tt, V1, V2) → ACTIVATE(V2)
U52¹(tt, V1, V2) → ACTIVATE(V1)
U53¹(tt, V1, V2) → U54¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U53¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U53¹(tt, V1, V2) → ACTIVATE(V2)
U53¹(tt, V1, V2) → ACTIVATE(V1)
U54¹(tt, V1, V2) → U55¹(isNatural(activate(V1)), activate(V2))
U54¹(tt, V1, V2) → ISNATURAL(activate(V1))
U54¹(tt, V1, V2) → ACTIVATE(V1)
U54¹(tt, V1, V2) → ACTIVATE(V2)
U55¹(tt, V2) → U56¹(isLNat(activate(V2)))
U55¹(tt, V2) → ISLNAT(activate(V2))
U55¹(tt, V2) → ACTIVATE(V2)
U61¹(tt, V1) → U62¹(isPLNatKind(activate(V1)), activate(V1))
U61¹(tt, V1) → ISPLNATKIND(activate(V1))
U61¹(tt, V1) → ACTIVATE(V1)
U62¹(tt, V1) → U63¹(isPLNat(activate(V1)))
U62¹(tt, V1) → ISPLNAT(activate(V1))
U62¹(tt, V1) → ACTIVATE(V1)
U71¹(tt, V1) → U72¹(isNaturalKind(activate(V1)), activate(V1))
U71¹(tt, V1) → ISNATURALKIND(activate(V1))
U71¹(tt, V1) → ACTIVATE(V1)
U72¹(tt, V1) → U73¹(isNatural(activate(V1)))
U72¹(tt, V1) → ISNATURAL(activate(V1))
U72¹(tt, V1) → ACTIVATE(V1)
U81¹(tt, V1) → U82¹(isPLNatKind(activate(V1)), activate(V1))
U81¹(tt, V1) → ISPLNATKIND(activate(V1))
U81¹(tt, V1) → ACTIVATE(V1)
U82¹(tt, V1) → U83¹(isPLNat(activate(V1)))
U82¹(tt, V1) → ISPLNAT(activate(V1))
U82¹(tt, V1) → ACTIVATE(V1)
U91¹(tt, V1) → U92¹(isLNatKind(activate(V1)), activate(V1))
U91¹(tt, V1) → ISLNATKIND(activate(V1))
U91¹(tt, V1) → ACTIVATE(V1)
U92¹(tt, V1) → U93¹(isLNat(activate(V1)))
U92¹(tt, V1) → ISLNAT(activate(V1))
U92¹(tt, V1) → ACTIVATE(V1)
AFTERNTH(N, XS) → U11¹(isNatural(N), N, XS)
AFTERNTH(N, XS) → ISNATURAL(N)
FST(pair(X, Y)) → U21¹(isLNat(X), X, Y)
FST(pair(X, Y)) → ISLNAT(X)
HEAD(cons(N, XS)) → U31¹(isNatural(N), N, activate(XS))
HEAD(cons(N, XS)) → ISNATURAL(N)
HEAD(cons(N, XS)) → ACTIVATE(XS)
ISLNAT(n__afterNth(V1, V2)) → U41¹(isNaturalKind(activate(V1)), activate(V1), 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)) → U51¹(isNaturalKind(activate(V1)), activate(V1), 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)) → U61¹(isPLNatKind(activate(V1)), activate(V1))
ISLNAT(n__fst(V1)) → ISPLNATKIND(activate(V1))
ISLNAT(n__fst(V1)) → ACTIVATE(V1)
ISLNAT(n__natsFrom(V1)) → U71¹(isNaturalKind(activate(V1)), activate(V1))
ISLNAT(n__natsFrom(V1)) → ISNATURALKIND(activate(V1))
ISLNAT(n__natsFrom(V1)) → ACTIVATE(V1)
ISLNAT(n__snd(V1)) → U81¹(isPLNatKind(activate(V1)), activate(V1))
ISLNAT(n__snd(V1)) → ISPLNATKIND(activate(V1))
ISLNAT(n__snd(V1)) → ACTIVATE(V1)
ISLNAT(n__tail(V1)) → U91¹(isLNatKind(activate(V1)), activate(V1))
ISLNAT(n__tail(V1)) → ISLNATKIND(activate(V1))
ISLNAT(n__tail(V1)) → ACTIVATE(V1)
ISLNAT(n__take(V1, V2)) → U101¹(isNaturalKind(activate(V1)), activate(V1), 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)) → U111¹(isNaturalKind(activate(V1)), 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)) → U121¹(isNaturalKind(activate(V1)), 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)) → U131¹(isPLNatKind(activate(V1)))
ISLNATKIND(n__fst(V1)) → ISPLNATKIND(activate(V1))
ISLNATKIND(n__fst(V1)) → ACTIVATE(V1)
ISLNATKIND(n__natsFrom(V1)) → U141¹(isNaturalKind(activate(V1)))
ISLNATKIND(n__natsFrom(V1)) → ISNATURALKIND(activate(V1))
ISLNATKIND(n__natsFrom(V1)) → ACTIVATE(V1)
ISLNATKIND(n__snd(V1)) → U151¹(isPLNatKind(activate(V1)))
ISLNATKIND(n__snd(V1)) → ISPLNATKIND(activate(V1))
ISLNATKIND(n__snd(V1)) → ACTIVATE(V1)
ISLNATKIND(n__tail(V1)) → U161¹(isLNatKind(activate(V1)))
ISLNATKIND(n__tail(V1)) → ISLNATKIND(activate(V1))
ISLNATKIND(n__tail(V1)) → ACTIVATE(V1)
ISLNATKIND(n__take(V1, V2)) → U171¹(isNaturalKind(activate(V1)), 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)) → U181¹(isLNatKind(activate(V1)), activate(V1))
ISNATURAL(n__head(V1)) → ISLNATKIND(activate(V1))
ISNATURAL(n__head(V1)) → ACTIVATE(V1)
ISNATURAL(n__s(V1)) → U191¹(isNaturalKind(activate(V1)), activate(V1))
ISNATURAL(n__s(V1)) → ISNATURALKIND(activate(V1))
ISNATURAL(n__s(V1)) → ACTIVATE(V1)
ISNATURAL(n__sel(V1, V2)) → U201¹(isNaturalKind(activate(V1)), activate(V1), 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)) → U211¹(isLNatKind(activate(V1)))
ISNATURALKIND(n__head(V1)) → ISLNATKIND(activate(V1))
ISNATURALKIND(n__head(V1)) → ACTIVATE(V1)
ISNATURALKIND(n__s(V1)) → U221¹(isNaturalKind(activate(V1)))
ISNATURALKIND(n__s(V1)) → ISNATURALKIND(activate(V1))
ISNATURALKIND(n__s(V1)) → ACTIVATE(V1)
ISNATURALKIND(n__sel(V1, V2)) → U231¹(isNaturalKind(activate(V1)), 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)) → U241¹(isLNatKind(activate(V1)), activate(V1), 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)) → U251¹(isNaturalKind(activate(V1)), activate(V1), 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)) → U261¹(isLNatKind(activate(V1)), 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)) → U271¹(isNaturalKind(activate(V1)), 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) → U281¹(isNatural(N), N)
NATSFROM(N) → ISNATURAL(N)
SEL(N, XS) → U291¹(isNatural(N), N, XS)
SEL(N, XS) → ISNATURAL(N)
SND(pair(X, Y)) → U301¹(isLNat(X), X, Y)
SND(pair(X, Y)) → ISLNAT(X)
SPLITAT(0, XS) → U311¹(isLNat(XS), XS)
SPLITAT(0, XS) → ISLNAT(XS)
SPLITAT(s(N), cons(X, XS)) → U321¹(isNatural(N), N, X, activate(XS))
SPLITAT(s(N), cons(X, XS)) → ISNATURAL(N)
SPLITAT(s(N), cons(X, XS)) → ACTIVATE(XS)
TAIL(cons(N, XS)) → U331¹(isNatural(N), N, activate(XS))
TAIL(cons(N, XS)) → ISNATURAL(N)
TAIL(cons(N, XS)) → ACTIVATE(XS)
TAKE(N, XS) → U341¹(isNatural(N), N, XS)
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__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) → 0¹
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)

The TRS R consists of the following rules:

U101(tt, V1, V2) → U102(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U102(tt, V1, V2) → U103(isLNatKind(activate(V2)), activate(V1), activate(V2))
U103(tt, V1, V2) → U104(isLNatKind(activate(V2)), activate(V1), activate(V2))
U104(tt, V1, V2) → U105(isNatural(activate(V1)), activate(V2))
U105(tt, V2) → U106(isLNat(activate(V2)))
U106(tt) → tt
U11(tt, N, XS) → U12(isNaturalKind(activate(N)), activate(N), activate(XS))
U111(tt, V2) → U112(isLNatKind(activate(V2)))
U112(tt) → tt
U12(tt, N, XS) → U13(isLNat(activate(XS)), activate(N), activate(XS))
U121(tt, V2) → U122(isLNatKind(activate(V2)))
U122(tt) → tt
U13(tt, N, XS) → U14(isLNatKind(activate(XS)), activate(N), activate(XS))
U131(tt) → tt
U14(tt, N, XS) → snd(splitAt(activate(N), activate(XS)))
U141(tt) → tt
U151(tt) → tt
U161(tt) → tt
U171(tt, V2) → U172(isLNatKind(activate(V2)))
U172(tt) → tt
U181(tt, V1) → U182(isLNatKind(activate(V1)), activate(V1))
U182(tt, V1) → U183(isLNat(activate(V1)))
U183(tt) → tt
U191(tt, V1) → U192(isNaturalKind(activate(V1)), activate(V1))
U192(tt, V1) → U193(isNatural(activate(V1)))
U193(tt) → tt
U201(tt, V1, V2) → U202(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U202(tt, V1, V2) → U203(isLNatKind(activate(V2)), activate(V1), activate(V2))
U203(tt, V1, V2) → U204(isLNatKind(activate(V2)), activate(V1), activate(V2))
U204(tt, V1, V2) → U205(isNatural(activate(V1)), activate(V2))
U205(tt, V2) → U206(isLNat(activate(V2)))
U206(tt) → tt
U21(tt, X, Y) → U22(isLNatKind(activate(X)), activate(X), activate(Y))
U211(tt) → tt
U22(tt, X, Y) → U23(isLNat(activate(Y)), activate(X), activate(Y))
U221(tt) → tt
U23(tt, X, Y) → U24(isLNatKind(activate(Y)), activate(X))
U231(tt, V2) → U232(isLNatKind(activate(V2)))
U232(tt) → tt
U24(tt, X) → activate(X)
U241(tt, V1, V2) → U242(isLNatKind(activate(V1)), activate(V1), activate(V2))
U242(tt, V1, V2) → U243(isLNatKind(activate(V2)), activate(V1), activate(V2))
U243(tt, V1, V2) → U244(isLNatKind(activate(V2)), activate(V1), activate(V2))
U244(tt, V1, V2) → U245(isLNat(activate(V1)), activate(V2))
U245(tt, V2) → U246(isLNat(activate(V2)))
U246(tt) → tt
U251(tt, V1, V2) → U252(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U252(tt, V1, V2) → U253(isLNatKind(activate(V2)), activate(V1), activate(V2))
U253(tt, V1, V2) → U254(isLNatKind(activate(V2)), activate(V1), activate(V2))
U254(tt, V1, V2) → U255(isNatural(activate(V1)), activate(V2))
U255(tt, V2) → U256(isLNat(activate(V2)))
U256(tt) → tt
U261(tt, V2) → U262(isLNatKind(activate(V2)))
U262(tt) → tt
U271(tt, V2) → U272(isLNatKind(activate(V2)))
U272(tt) → tt
U281(tt, N) → U282(isNaturalKind(activate(N)), activate(N))
U282(tt, N) → cons(activate(N), n__natsFrom(n__s(activate(N))))
U291(tt, N, XS) → U292(isNaturalKind(activate(N)), activate(N), activate(XS))
U292(tt, N, XS) → U293(isLNat(activate(XS)), activate(N), activate(XS))
U293(tt, N, XS) → U294(isLNatKind(activate(XS)), activate(N), activate(XS))
U294(tt, N, XS) → head(afterNth(activate(N), activate(XS)))
U301(tt, X, Y) → U302(isLNatKind(activate(X)), activate(Y))
U302(tt, Y) → U303(isLNat(activate(Y)), activate(Y))
U303(tt, Y) → U304(isLNatKind(activate(Y)), activate(Y))
U304(tt, Y) → activate(Y)
U31(tt, N, XS) → U32(isNaturalKind(activate(N)), activate(N), activate(XS))
U311(tt, XS) → U312(isLNatKind(activate(XS)), activate(XS))
U312(tt, XS) → pair(nil, activate(XS))
U32(tt, N, XS) → U33(isLNat(activate(XS)), activate(N), activate(XS))
U321(tt, N, X, XS) → U322(isNaturalKind(activate(N)), activate(N), activate(X), activate(XS))
U322(tt, N, X, XS) → U323(isNatural(activate(X)), activate(N), activate(X), activate(XS))
U323(tt, N, X, XS) → U324(isNaturalKind(activate(X)), activate(N), activate(X), activate(XS))
U324(tt, N, X, XS) → U325(isLNat(activate(XS)), activate(N), activate(X), activate(XS))
U325(tt, N, X, XS) → U326(isLNatKind(activate(XS)), activate(N), activate(X), activate(XS))
U326(tt, N, X, XS) → U327(splitAt(activate(N), activate(XS)), activate(X))
U327(pair(YS, ZS), X) → pair(cons(activate(X), YS), ZS)
U33(tt, N, XS) → U34(isLNatKind(activate(XS)), activate(N))
U331(tt, N, XS) → U332(isNaturalKind(activate(N)), activate(XS))
U332(tt, XS) → U333(isLNat(activate(XS)), activate(XS))
U333(tt, XS) → U334(isLNatKind(activate(XS)), activate(XS))
U334(tt, XS) → activate(XS)
U34(tt, N) → activate(N)
U341(tt, N, XS) → U342(isNaturalKind(activate(N)), activate(N), activate(XS))
U342(tt, N, XS) → U343(isLNat(activate(XS)), activate(N), activate(XS))
U343(tt, N, XS) → U344(isLNatKind(activate(XS)), activate(N), activate(XS))
U344(tt, N, XS) → fst(splitAt(activate(N), activate(XS)))
U41(tt, V1, V2) → U42(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isLNatKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isLNatKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isNatural(activate(V1)), activate(V2))
U45(tt, V2) → U46(isLNat(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isLNatKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isLNatKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNatural(activate(V1)), activate(V2))
U55(tt, V2) → U56(isLNat(activate(V2)))
U56(tt) → tt
U61(tt, V1) → U62(isPLNatKind(activate(V1)), activate(V1))
U62(tt, V1) → U63(isPLNat(activate(V1)))
U63(tt) → tt
U71(tt, V1) → U72(isNaturalKind(activate(V1)), activate(V1))
U72(tt, V1) → U73(isNatural(activate(V1)))
U73(tt) → tt
U81(tt, V1) → U82(isPLNatKind(activate(V1)), activate(V1))
U82(tt, V1) → U83(isPLNat(activate(V1)))
U83(tt) → tt
U91(tt, V1) → U92(isLNatKind(activate(V1)), activate(V1))
U92(tt, V1) → U93(isLNat(activate(V1)))
U93(tt) → tt
afterNth(N, XS) → U11(isNatural(N), N, XS)
fst(pair(X, Y)) → U21(isLNat(X), X, Y)
head(cons(N, XS)) → U31(isNatural(N), N, activate(XS))
isLNat(n__nil) → tt
isLNat(n__afterNth(V1, V2)) → U41(isNaturalKind(activate(V1)), activate(V1), activate(V2))
isLNat(n__cons(V1, V2)) → U51(isNaturalKind(activate(V1)), 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(isNaturalKind(activate(V1)), activate(V1), activate(V2))
isLNatKind(n__nil) → tt
isLNatKind(n__afterNth(V1, V2)) → U111(isNaturalKind(activate(V1)), activate(V2))
isLNatKind(n__cons(V1, V2)) → U121(isNaturalKind(activate(V1)), activate(V2))
isLNatKind(n__fst(V1)) → U131(isPLNatKind(activate(V1)))
isLNatKind(n__natsFrom(V1)) → U141(isNaturalKind(activate(V1)))
isLNatKind(n__snd(V1)) → U151(isPLNatKind(activate(V1)))
isLNatKind(n__tail(V1)) → U161(isLNatKind(activate(V1)))
isLNatKind(n__take(V1, V2)) → U171(isNaturalKind(activate(V1)), activate(V2))
isNatural(n__0) → tt
isNatural(n__head(V1)) → U181(isLNatKind(activate(V1)), activate(V1))
isNatural(n__s(V1)) → U191(isNaturalKind(activate(V1)), activate(V1))
isNatural(n__sel(V1, V2)) → U201(isNaturalKind(activate(V1)), activate(V1), activate(V2))
isNaturalKind(n__0) → tt
isNaturalKind(n__head(V1)) → U211(isLNatKind(activate(V1)))
isNaturalKind(n__s(V1)) → U221(isNaturalKind(activate(V1)))
isNaturalKind(n__sel(V1, V2)) → U231(isNaturalKind(activate(V1)), activate(V2))
isPLNat(n__pair(V1, V2)) → U241(isLNatKind(activate(V1)), activate(V1), activate(V2))
isPLNat(n__splitAt(V1, V2)) → U251(isNaturalKind(activate(V1)), activate(V1), activate(V2))
isPLNatKind(n__pair(V1, V2)) → U261(isLNatKind(activate(V1)), activate(V2))
isPLNatKind(n__splitAt(V1, V2)) → U271(isNaturalKind(activate(V1)), activate(V2))
natsFrom(N) → U281(isNatural(N), N)
sel(N, XS) → U291(isNatural(N), N, XS)
snd(pair(X, Y)) → U301(isLNat(X), X, Y)
splitAt(0, XS) → U311(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U321(isNatural(N), N, X, activate(XS))
tail(cons(N, XS)) → U331(isNatural(N), N, activate(XS))
take(N, XS) → U341(isNatural(N), N, XS)
natsFrom(X) → n__natsFrom(X)
s(X) → n__s(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)
activate(n__natsFrom(X)) → natsFrom(activate(X))
activate(n__s(X)) → s(activate(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(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 34 less nodes.

(4) Obligation:

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

U102¹(tt, V1, V2) → U103¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U103¹(tt, V1, V2) → U104¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U104¹(tt, V1, V2) → U105¹(isNatural(activate(V1)), activate(V2))
U105¹(tt, V2) → ISLNAT(activate(V2))
ISLNAT(n__afterNth(V1, V2)) → U41¹(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U41¹(tt, V1, V2) → U42¹(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U42¹(tt, V1, V2) → U43¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U43¹(tt, V1, V2) → U44¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U44¹(tt, V1, V2) → U45¹(isNatural(activate(V1)), activate(V2))
U45¹(tt, V2) → ISLNAT(activate(V2))
ISLNAT(n__afterNth(V1, V2)) → ISNATURALKIND(activate(V1))
ISNATURALKIND(n__head(V1)) → ISLNATKIND(activate(V1))
ISLNATKIND(n__afterNth(V1, V2)) → U111¹(isNaturalKind(activate(V1)), activate(V2))
U111¹(tt, V2) → ISLNATKIND(activate(V2))
ISLNATKIND(n__afterNth(V1, V2)) → ISNATURALKIND(activate(V1))
ISNATURALKIND(n__head(V1)) → ACTIVATE(V1)
ACTIVATE(n__natsFrom(X)) → NATSFROM(activate(X))
NATSFROM(N) → U281¹(isNatural(N), N)
U281¹(tt, N) → U282¹(isNaturalKind(activate(N)), activate(N))
U282¹(tt, N) → ACTIVATE(N)
ACTIVATE(n__natsFrom(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__afterNth(X1, X2)) → AFTERNTH(activate(X1), activate(X2))
AFTERNTH(N, XS) → U11¹(isNatural(N), N, XS)
U11¹(tt, N, XS) → U12¹(isNaturalKind(activate(N)), activate(N), activate(XS))
U12¹(tt, N, XS) → U13¹(isLNat(activate(XS)), activate(N), activate(XS))
U13¹(tt, N, XS) → U14¹(isLNatKind(activate(XS)), activate(N), activate(XS))
U14¹(tt, N, XS) → SND(splitAt(activate(N), activate(XS)))
SND(pair(X, Y)) → U301¹(isLNat(X), X, Y)
U301¹(tt, X, Y) → U302¹(isLNatKind(activate(X)), activate(Y))
U302¹(tt, Y) → U303¹(isLNat(activate(Y)), activate(Y))
U303¹(tt, Y) → U304¹(isLNatKind(activate(Y)), activate(Y))
U304¹(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)) → U21¹(isLNat(X), X, Y)
U21¹(tt, X, Y) → U22¹(isLNatKind(activate(X)), activate(X), activate(Y))
U22¹(tt, X, Y) → U23¹(isLNat(activate(Y)), activate(X), activate(Y))
U23¹(tt, X, Y) → U24¹(isLNatKind(activate(Y)), activate(X))
U24¹(tt, X) → ACTIVATE(X)
ACTIVATE(n__fst(X)) → ACTIVATE(X)
ACTIVATE(n__snd(X)) → SND(activate(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)) → U331¹(isNatural(N), N, activate(XS))
U331¹(tt, N, XS) → U332¹(isNaturalKind(activate(N)), activate(XS))
U332¹(tt, XS) → U333¹(isLNat(activate(XS)), activate(XS))
U333¹(tt, XS) → U334¹(isLNatKind(activate(XS)), activate(XS))
U334¹(tt, XS) → ACTIVATE(XS)
ACTIVATE(n__tail(X)) → ACTIVATE(X)
ACTIVATE(n__take(X1, X2)) → TAKE(activate(X1), activate(X2))
TAKE(N, XS) → U341¹(isNatural(N), N, XS)
U341¹(tt, N, XS) → U342¹(isNaturalKind(activate(N)), activate(N), activate(XS))
U342¹(tt, N, XS) → U343¹(isLNat(activate(XS)), activate(N), activate(XS))
U343¹(tt, N, XS) → U344¹(isLNatKind(activate(XS)), activate(N), activate(XS))
U344¹(tt, N, XS) → FST(splitAt(activate(N), activate(XS)))
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)) → U31¹(isNatural(N), N, activate(XS))
U31¹(tt, N, XS) → U32¹(isNaturalKind(activate(N)), activate(N), activate(XS))
U32¹(tt, N, XS) → U33¹(isLNat(activate(XS)), activate(N), activate(XS))
U33¹(tt, N, XS) → U34¹(isLNatKind(activate(XS)), activate(N))
U34¹(tt, N) → ACTIVATE(N)
ACTIVATE(n__head(X)) → ACTIVATE(X)
ACTIVATE(n__sel(X1, X2)) → SEL(activate(X1), activate(X2))
SEL(N, XS) → U291¹(isNatural(N), N, XS)
U291¹(tt, N, XS) → U292¹(isNaturalKind(activate(N)), activate(N), activate(XS))
U292¹(tt, N, XS) → U293¹(isLNat(activate(XS)), activate(N), activate(XS))
U293¹(tt, N, XS) → U294¹(isLNatKind(activate(XS)), activate(N), activate(XS))
U294¹(tt, N, XS) → HEAD(afterNth(activate(N), activate(XS)))
HEAD(cons(N, XS)) → ISNATURAL(N)
ISNATURAL(n__head(V1)) → U181¹(isLNatKind(activate(V1)), activate(V1))
U181¹(tt, V1) → U182¹(isLNatKind(activate(V1)), activate(V1))
U182¹(tt, V1) → ISLNAT(activate(V1))
ISLNAT(n__cons(V1, V2)) → U51¹(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U51¹(tt, V1, V2) → U52¹(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U52¹(tt, V1, V2) → U53¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U53¹(tt, V1, V2) → U54¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U54¹(tt, V1, V2) → U55¹(isNatural(activate(V1)), activate(V2))
U55¹(tt, V2) → ISLNAT(activate(V2))
ISLNAT(n__cons(V1, V2)) → ISNATURALKIND(activate(V1))
ISNATURALKIND(n__s(V1)) → ISNATURALKIND(activate(V1))
ISNATURALKIND(n__s(V1)) → 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) → U311¹(isLNat(XS), XS)
U311¹(tt, XS) → U312¹(isLNatKind(activate(XS)), activate(XS))
U312¹(tt, XS) → ACTIVATE(XS)
ACTIVATE(n__splitAt(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__splitAt(X1, X2)) → ACTIVATE(X2)
U311¹(tt, XS) → ISLNATKIND(activate(XS))
ISLNATKIND(n__afterNth(V1, V2)) → ACTIVATE(V1)
ISLNATKIND(n__afterNth(V1, V2)) → ACTIVATE(V2)
ISLNATKIND(n__cons(V1, V2)) → U121¹(isNaturalKind(activate(V1)), activate(V2))
U121¹(tt, V2) → ISLNATKIND(activate(V2))
ISLNATKIND(n__cons(V1, V2)) → ISNATURALKIND(activate(V1))
ISNATURALKIND(n__sel(V1, V2)) → U231¹(isNaturalKind(activate(V1)), activate(V2))
U231¹(tt, V2) → ISLNATKIND(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)) → U261¹(isLNatKind(activate(V1)), activate(V2))
U261¹(tt, V2) → ISLNATKIND(activate(V2))
ISLNATKIND(n__fst(V1)) → ACTIVATE(V1)
ISLNATKIND(n__natsFrom(V1)) → ISNATURALKIND(activate(V1))
ISNATURALKIND(n__sel(V1, V2)) → ISNATURALKIND(activate(V1))
ISNATURALKIND(n__sel(V1, V2)) → ACTIVATE(V1)
ISNATURALKIND(n__sel(V1, V2)) → ACTIVATE(V2)
ISLNATKIND(n__natsFrom(V1)) → ACTIVATE(V1)
ISLNATKIND(n__snd(V1)) → ISPLNATKIND(activate(V1))
ISPLNATKIND(n__pair(V1, V2)) → ISLNATKIND(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)) → U171¹(isNaturalKind(activate(V1)), activate(V2))
U171¹(tt, V2) → 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)
U171¹(tt, V2) → ACTIVATE(V2)
ISPLNATKIND(n__pair(V1, V2)) → ACTIVATE(V1)
ISPLNATKIND(n__pair(V1, V2)) → ACTIVATE(V2)
ISPLNATKIND(n__splitAt(V1, V2)) → U271¹(isNaturalKind(activate(V1)), activate(V2))
U271¹(tt, V2) → ISLNATKIND(activate(V2))
U271¹(tt, V2) → ACTIVATE(V2)
ISPLNATKIND(n__splitAt(V1, V2)) → ISNATURALKIND(activate(V1))
ISPLNATKIND(n__splitAt(V1, V2)) → ACTIVATE(V1)
ISPLNATKIND(n__splitAt(V1, V2)) → ACTIVATE(V2)
U261¹(tt, V2) → ACTIVATE(V2)
U231¹(tt, V2) → ACTIVATE(V2)
U121¹(tt, V2) → ACTIVATE(V2)
U311¹(tt, XS) → ACTIVATE(XS)
SPLITAT(0, XS) → ISLNAT(XS)
ISLNAT(n__cons(V1, V2)) → ACTIVATE(V1)
ISLNAT(n__cons(V1, V2)) → ACTIVATE(V2)
ISLNAT(n__fst(V1)) → U61¹(isPLNatKind(activate(V1)), activate(V1))
U61¹(tt, V1) → U62¹(isPLNatKind(activate(V1)), activate(V1))
U62¹(tt, V1) → ISPLNAT(activate(V1))
ISPLNAT(n__pair(V1, V2)) → U241¹(isLNatKind(activate(V1)), activate(V1), activate(V2))
U241¹(tt, V1, V2) → U242¹(isLNatKind(activate(V1)), activate(V1), activate(V2))
U242¹(tt, V1, V2) → U243¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U243¹(tt, V1, V2) → U244¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U244¹(tt, V1, V2) → U245¹(isLNat(activate(V1)), activate(V2))
U245¹(tt, V2) → ISLNAT(activate(V2))
ISLNAT(n__fst(V1)) → ISPLNATKIND(activate(V1))
ISLNAT(n__fst(V1)) → ACTIVATE(V1)
ISLNAT(n__natsFrom(V1)) → U71¹(isNaturalKind(activate(V1)), activate(V1))
U71¹(tt, V1) → U72¹(isNaturalKind(activate(V1)), activate(V1))
U72¹(tt, V1) → ISNATURAL(activate(V1))
ISNATURAL(n__head(V1)) → ISLNATKIND(activate(V1))
ISNATURAL(n__head(V1)) → ACTIVATE(V1)
ISNATURAL(n__s(V1)) → U191¹(isNaturalKind(activate(V1)), activate(V1))
U191¹(tt, V1) → U192¹(isNaturalKind(activate(V1)), activate(V1))
U192¹(tt, V1) → ISNATURAL(activate(V1))
ISNATURAL(n__s(V1)) → ISNATURALKIND(activate(V1))
ISNATURAL(n__s(V1)) → ACTIVATE(V1)
ISNATURAL(n__sel(V1, V2)) → U201¹(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U201¹(tt, V1, V2) → U202¹(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U202¹(tt, V1, V2) → U203¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U203¹(tt, V1, V2) → U204¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U204¹(tt, V1, V2) → U205¹(isNatural(activate(V1)), activate(V2))
U205¹(tt, V2) → ISLNAT(activate(V2))
ISLNAT(n__natsFrom(V1)) → ISNATURALKIND(activate(V1))
ISLNAT(n__natsFrom(V1)) → ACTIVATE(V1)
ISLNAT(n__snd(V1)) → U81¹(isPLNatKind(activate(V1)), activate(V1))
U81¹(tt, V1) → U82¹(isPLNatKind(activate(V1)), activate(V1))
U82¹(tt, V1) → ISPLNAT(activate(V1))
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)) → U251¹(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U251¹(tt, V1, V2) → U252¹(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U252¹(tt, V1, V2) → U253¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U253¹(tt, V1, V2) → U254¹(isLNatKind(activate(V2)), activate(V1), activate(V2))
U254¹(tt, V1, V2) → U255¹(isNatural(activate(V1)), activate(V2))
U255¹(tt, V2) → ISLNAT(activate(V2))
ISLNAT(n__snd(V1)) → ISPLNATKIND(activate(V1))
ISLNAT(n__snd(V1)) → ACTIVATE(V1)
ISLNAT(n__tail(V1)) → U91¹(isLNatKind(activate(V1)), activate(V1))
U91¹(tt, V1) → U92¹(isLNatKind(activate(V1)), activate(V1))
U92¹(tt, V1) → ISLNAT(activate(V1))
ISLNAT(n__tail(V1)) → ISLNATKIND(activate(V1))
ISLNAT(n__tail(V1)) → ACTIVATE(V1)
ISLNAT(n__take(V1, V2)) → U101¹(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U101¹(tt, V1, V2) → U102¹(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U102¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U102¹(tt, V1, V2) → ACTIVATE(V2)
U102¹(tt, V1, V2) → ACTIVATE(V1)
U101¹(tt, V1, V2) → ISNATURALKIND(activate(V1))
U101¹(tt, V1, V2) → ACTIVATE(V1)
U101¹(tt, V1, V2) → ACTIVATE(V2)
ISLNAT(n__take(V1, V2)) → ISNATURALKIND(activate(V1))
ISLNAT(n__take(V1, V2)) → ACTIVATE(V1)
ISLNAT(n__take(V1, V2)) → ACTIVATE(V2)
U92¹(tt, V1) → ACTIVATE(V1)
U91¹(tt, V1) → ISLNATKIND(activate(V1))
U91¹(tt, V1) → ACTIVATE(V1)
U255¹(tt, V2) → ACTIVATE(V2)
U254¹(tt, V1, V2) → ISNATURAL(activate(V1))
ISNATURAL(n__sel(V1, V2)) → ISNATURALKIND(activate(V1))
ISNATURAL(n__sel(V1, V2)) → ACTIVATE(V1)
ISNATURAL(n__sel(V1, V2)) → ACTIVATE(V2)
U254¹(tt, V1, V2) → ACTIVATE(V1)
U254¹(tt, V1, V2) → ACTIVATE(V2)
U253¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U253¹(tt, V1, V2) → ACTIVATE(V2)
U253¹(tt, V1, V2) → ACTIVATE(V1)
U252¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U252¹(tt, V1, V2) → ACTIVATE(V2)
U252¹(tt, V1, V2) → ACTIVATE(V1)
U251¹(tt, V1, V2) → ISNATURALKIND(activate(V1))
U251¹(tt, V1, V2) → ACTIVATE(V1)
U251¹(tt, V1, V2) → ACTIVATE(V2)
ISPLNAT(n__splitAt(V1, V2)) → ISNATURALKIND(activate(V1))
ISPLNAT(n__splitAt(V1, V2)) → ACTIVATE(V1)
ISPLNAT(n__splitAt(V1, V2)) → ACTIVATE(V2)
U82¹(tt, V1) → ACTIVATE(V1)
U81¹(tt, V1) → ISPLNATKIND(activate(V1))
U81¹(tt, V1) → ACTIVATE(V1)
U205¹(tt, V2) → ACTIVATE(V2)
U204¹(tt, V1, V2) → ISNATURAL(activate(V1))
U204¹(tt, V1, V2) → ACTIVATE(V1)
U204¹(tt, V1, V2) → ACTIVATE(V2)
U203¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U203¹(tt, V1, V2) → ACTIVATE(V2)
U203¹(tt, V1, V2) → ACTIVATE(V1)
U202¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U202¹(tt, V1, V2) → ACTIVATE(V2)
U202¹(tt, V1, V2) → ACTIVATE(V1)
U201¹(tt, V1, V2) → ISNATURALKIND(activate(V1))
U201¹(tt, V1, V2) → ACTIVATE(V1)
U201¹(tt, V1, V2) → ACTIVATE(V2)
U192¹(tt, V1) → ACTIVATE(V1)
U191¹(tt, V1) → ISNATURALKIND(activate(V1))
U191¹(tt, V1) → ACTIVATE(V1)
U72¹(tt, V1) → ACTIVATE(V1)
U71¹(tt, V1) → ISNATURALKIND(activate(V1))
U71¹(tt, V1) → ACTIVATE(V1)
U245¹(tt, V2) → ACTIVATE(V2)
U244¹(tt, V1, V2) → ISLNAT(activate(V1))
U244¹(tt, V1, V2) → ACTIVATE(V1)
U244¹(tt, V1, V2) → ACTIVATE(V2)
U243¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U243¹(tt, V1, V2) → ACTIVATE(V2)
U243¹(tt, V1, V2) → ACTIVATE(V1)
U242¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U242¹(tt, V1, V2) → ACTIVATE(V2)
U242¹(tt, V1, V2) → ACTIVATE(V1)
U241¹(tt, V1, V2) → ISLNATKIND(activate(V1))
U241¹(tt, V1, V2) → ACTIVATE(V1)
U241¹(tt, V1, V2) → ACTIVATE(V2)
U62¹(tt, V1) → ACTIVATE(V1)
U61¹(tt, V1) → ISPLNATKIND(activate(V1))
U61¹(tt, V1) → ACTIVATE(V1)
SPLITAT(s(N), cons(X, XS)) → U321¹(isNatural(N), N, X, activate(XS))
U321¹(tt, N, X, XS) → U322¹(isNaturalKind(activate(N)), activate(N), activate(X), activate(XS))
U322¹(tt, N, X, XS) → U323¹(isNatural(activate(X)), activate(N), activate(X), activate(XS))
U323¹(tt, N, X, XS) → U324¹(isNaturalKind(activate(X)), activate(N), activate(X), activate(XS))
U324¹(tt, N, X, XS) → U325¹(isLNat(activate(XS)), activate(N), activate(X), activate(XS))
U325¹(tt, N, X, XS) → U326¹(isLNatKind(activate(XS)), activate(N), activate(X), activate(XS))
U326¹(tt, N, X, XS) → U327¹(splitAt(activate(N), activate(XS)), activate(X))
U327¹(pair(YS, ZS), X) → ACTIVATE(X)
U326¹(tt, N, X, XS) → SPLITAT(activate(N), activate(XS))
SPLITAT(s(N), cons(X, XS)) → ISNATURAL(N)
SPLITAT(s(N), cons(X, XS)) → ACTIVATE(XS)
U326¹(tt, N, X, XS) → ACTIVATE(N)
U326¹(tt, N, X, XS) → ACTIVATE(XS)
U326¹(tt, N, X, XS) → ACTIVATE(X)
U325¹(tt, N, X, XS) → ISLNATKIND(activate(XS))
U325¹(tt, N, X, XS) → ACTIVATE(XS)
U325¹(tt, N, X, XS) → ACTIVATE(N)
U325¹(tt, N, X, XS) → ACTIVATE(X)
U324¹(tt, N, X, XS) → ISLNAT(activate(XS))
U324¹(tt, N, X, XS) → ACTIVATE(XS)
U324¹(tt, N, X, XS) → ACTIVATE(N)
U324¹(tt, N, X, XS) → ACTIVATE(X)
U323¹(tt, N, X, XS) → ISNATURALKIND(activate(X))
U323¹(tt, N, X, XS) → ACTIVATE(X)
U323¹(tt, N, X, XS) → ACTIVATE(N)
U323¹(tt, N, X, XS) → ACTIVATE(XS)
U322¹(tt, N, X, XS) → ISNATURAL(activate(X))
U322¹(tt, N, X, XS) → ACTIVATE(X)
U322¹(tt, N, X, XS) → ACTIVATE(N)
U322¹(tt, N, X, XS) → ACTIVATE(XS)
U321¹(tt, N, X, XS) → ISNATURALKIND(activate(N))
U321¹(tt, N, X, XS) → ACTIVATE(N)
U321¹(tt, N, X, XS) → ACTIVATE(X)
U321¹(tt, N, X, XS) → ACTIVATE(XS)
U55¹(tt, V2) → ACTIVATE(V2)
U54¹(tt, V1, V2) → ISNATURAL(activate(V1))
U54¹(tt, V1, V2) → ACTIVATE(V1)
U54¹(tt, V1, V2) → ACTIVATE(V2)
U53¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U53¹(tt, V1, V2) → ACTIVATE(V2)
U53¹(tt, V1, V2) → ACTIVATE(V1)
U52¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U52¹(tt, V1, V2) → ACTIVATE(V2)
U52¹(tt, V1, V2) → ACTIVATE(V1)
U51¹(tt, V1, V2) → ISNATURALKIND(activate(V1))
U51¹(tt, V1, V2) → ACTIVATE(V1)
U51¹(tt, V1, V2) → ACTIVATE(V2)
U182¹(tt, V1) → ACTIVATE(V1)
U181¹(tt, V1) → ISLNATKIND(activate(V1))
U181¹(tt, V1) → ACTIVATE(V1)
HEAD(cons(N, XS)) → ACTIVATE(XS)
U294¹(tt, N, XS) → AFTERNTH(activate(N), activate(XS))
AFTERNTH(N, XS) → ISNATURAL(N)
U294¹(tt, N, XS) → ACTIVATE(N)
U294¹(tt, N, XS) → ACTIVATE(XS)
U293¹(tt, N, XS) → ISLNATKIND(activate(XS))
U293¹(tt, N, XS) → ACTIVATE(XS)
U293¹(tt, N, XS) → ACTIVATE(N)
U292¹(tt, N, XS) → ISLNAT(activate(XS))
U292¹(tt, N, XS) → ACTIVATE(XS)
U292¹(tt, N, XS) → ACTIVATE(N)
U291¹(tt, N, XS) → ISNATURALKIND(activate(N))
U291¹(tt, N, XS) → ACTIVATE(N)
U291¹(tt, N, XS) → ACTIVATE(XS)
SEL(N, XS) → ISNATURAL(N)
U33¹(tt, N, XS) → ISLNATKIND(activate(XS))
U33¹(tt, N, XS) → ACTIVATE(XS)
U33¹(tt, N, XS) → ACTIVATE(N)
U32¹(tt, N, XS) → ISLNAT(activate(XS))
U32¹(tt, N, XS) → ACTIVATE(XS)
U32¹(tt, N, XS) → ACTIVATE(N)
U31¹(tt, N, XS) → ISNATURALKIND(activate(N))
U31¹(tt, N, XS) → ACTIVATE(N)
U31¹(tt, N, XS) → ACTIVATE(XS)
U344¹(tt, N, XS) → SPLITAT(activate(N), activate(XS))
U344¹(tt, N, XS) → ACTIVATE(N)
U344¹(tt, N, XS) → ACTIVATE(XS)
U343¹(tt, N, XS) → ISLNATKIND(activate(XS))
U343¹(tt, N, XS) → ACTIVATE(XS)
U343¹(tt, N, XS) → ACTIVATE(N)
U342¹(tt, N, XS) → ISLNAT(activate(XS))
U342¹(tt, N, XS) → ACTIVATE(XS)
U342¹(tt, N, XS) → ACTIVATE(N)
U341¹(tt, N, XS) → ISNATURALKIND(activate(N))
U341¹(tt, N, XS) → ACTIVATE(N)
U341¹(tt, N, XS) → ACTIVATE(XS)
TAKE(N, XS) → ISNATURAL(N)
U333¹(tt, XS) → ISLNATKIND(activate(XS))
U333¹(tt, XS) → ACTIVATE(XS)
U332¹(tt, XS) → ISLNAT(activate(XS))
U332¹(tt, XS) → ACTIVATE(XS)
U331¹(tt, N, XS) → ISNATURALKIND(activate(N))
U331¹(tt, N, XS) → ACTIVATE(N)
U331¹(tt, N, XS) → ACTIVATE(XS)
TAIL(cons(N, XS)) → ISNATURAL(N)
TAIL(cons(N, XS)) → ACTIVATE(XS)
U23¹(tt, X, Y) → ISLNATKIND(activate(Y))
U23¹(tt, X, Y) → ACTIVATE(Y)
U23¹(tt, X, Y) → ACTIVATE(X)
U22¹(tt, X, Y) → ISLNAT(activate(Y))
U22¹(tt, X, Y) → ACTIVATE(Y)
U22¹(tt, X, Y) → ACTIVATE(X)
U21¹(tt, X, Y) → ISLNATKIND(activate(X))
U21¹(tt, X, Y) → ACTIVATE(X)
U21¹(tt, X, Y) → ACTIVATE(Y)
U303¹(tt, Y) → ISLNATKIND(activate(Y))
U303¹(tt, Y) → ACTIVATE(Y)
U302¹(tt, Y) → ISLNAT(activate(Y))
U302¹(tt, Y) → ACTIVATE(Y)
U301¹(tt, X, Y) → ISLNATKIND(activate(X))
U301¹(tt, X, Y) → ACTIVATE(X)
U301¹(tt, X, Y) → ACTIVATE(Y)
U14¹(tt, N, XS) → SPLITAT(activate(N), activate(XS))
U14¹(tt, N, XS) → ACTIVATE(N)
U14¹(tt, N, XS) → ACTIVATE(XS)
U13¹(tt, N, XS) → ISLNATKIND(activate(XS))
U13¹(tt, N, XS) → ACTIVATE(XS)
U13¹(tt, N, XS) → ACTIVATE(N)
U12¹(tt, N, XS) → ISLNAT(activate(XS))
U12¹(tt, N, XS) → ACTIVATE(XS)
U12¹(tt, N, XS) → ACTIVATE(N)
U11¹(tt, N, XS) → ISNATURALKIND(activate(N))
U11¹(tt, N, XS) → ACTIVATE(N)
U11¹(tt, N, XS) → ACTIVATE(XS)
U281¹(tt, N) → ISNATURALKIND(activate(N))
U281¹(tt, N) → ACTIVATE(N)
NATSFROM(N) → ISNATURAL(N)
U111¹(tt, V2) → ACTIVATE(V2)
U45¹(tt, V2) → ACTIVATE(V2)
U44¹(tt, V1, V2) → ISNATURAL(activate(V1))
U44¹(tt, V1, V2) → ACTIVATE(V1)
U44¹(tt, V1, V2) → ACTIVATE(V2)
U43¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U43¹(tt, V1, V2) → ACTIVATE(V2)
U43¹(tt, V1, V2) → ACTIVATE(V1)
U42¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U42¹(tt, V1, V2) → ACTIVATE(V2)
U42¹(tt, V1, V2) → ACTIVATE(V1)
U41¹(tt, V1, V2) → ISNATURALKIND(activate(V1))
U41¹(tt, V1, V2) → ACTIVATE(V1)
U41¹(tt, V1, V2) → ACTIVATE(V2)
U105¹(tt, V2) → ACTIVATE(V2)
U104¹(tt, V1, V2) → ISNATURAL(activate(V1))
U104¹(tt, V1, V2) → ACTIVATE(V1)
U104¹(tt, V1, V2) → ACTIVATE(V2)
U103¹(tt, V1, V2) → ISLNATKIND(activate(V2))
U103¹(tt, V1, V2) → ACTIVATE(V2)
U103¹(tt, V1, V2) → ACTIVATE(V1)

The TRS R consists of the following rules:

U101(tt, V1, V2) → U102(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U102(tt, V1, V2) → U103(isLNatKind(activate(V2)), activate(V1), activate(V2))
U103(tt, V1, V2) → U104(isLNatKind(activate(V2)), activate(V1), activate(V2))
U104(tt, V1, V2) → U105(isNatural(activate(V1)), activate(V2))
U105(tt, V2) → U106(isLNat(activate(V2)))
U106(tt) → tt
U11(tt, N, XS) → U12(isNaturalKind(activate(N)), activate(N), activate(XS))
U111(tt, V2) → U112(isLNatKind(activate(V2)))
U112(tt) → tt
U12(tt, N, XS) → U13(isLNat(activate(XS)), activate(N), activate(XS))
U121(tt, V2) → U122(isLNatKind(activate(V2)))
U122(tt) → tt
U13(tt, N, XS) → U14(isLNatKind(activate(XS)), activate(N), activate(XS))
U131(tt) → tt
U14(tt, N, XS) → snd(splitAt(activate(N), activate(XS)))
U141(tt) → tt
U151(tt) → tt
U161(tt) → tt
U171(tt, V2) → U172(isLNatKind(activate(V2)))
U172(tt) → tt
U181(tt, V1) → U182(isLNatKind(activate(V1)), activate(V1))
U182(tt, V1) → U183(isLNat(activate(V1)))
U183(tt) → tt
U191(tt, V1) → U192(isNaturalKind(activate(V1)), activate(V1))
U192(tt, V1) → U193(isNatural(activate(V1)))
U193(tt) → tt
U201(tt, V1, V2) → U202(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U202(tt, V1, V2) → U203(isLNatKind(activate(V2)), activate(V1), activate(V2))
U203(tt, V1, V2) → U204(isLNatKind(activate(V2)), activate(V1), activate(V2))
U204(tt, V1, V2) → U205(isNatural(activate(V1)), activate(V2))
U205(tt, V2) → U206(isLNat(activate(V2)))
U206(tt) → tt
U21(tt, X, Y) → U22(isLNatKind(activate(X)), activate(X), activate(Y))
U211(tt) → tt
U22(tt, X, Y) → U23(isLNat(activate(Y)), activate(X), activate(Y))
U221(tt) → tt
U23(tt, X, Y) → U24(isLNatKind(activate(Y)), activate(X))
U231(tt, V2) → U232(isLNatKind(activate(V2)))
U232(tt) → tt
U24(tt, X) → activate(X)
U241(tt, V1, V2) → U242(isLNatKind(activate(V1)), activate(V1), activate(V2))
U242(tt, V1, V2) → U243(isLNatKind(activate(V2)), activate(V1), activate(V2))
U243(tt, V1, V2) → U244(isLNatKind(activate(V2)), activate(V1), activate(V2))
U244(tt, V1, V2) → U245(isLNat(activate(V1)), activate(V2))
U245(tt, V2) → U246(isLNat(activate(V2)))
U246(tt) → tt
U251(tt, V1, V2) → U252(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U252(tt, V1, V2) → U253(isLNatKind(activate(V2)), activate(V1), activate(V2))
U253(tt, V1, V2) → U254(isLNatKind(activate(V2)), activate(V1), activate(V2))
U254(tt, V1, V2) → U255(isNatural(activate(V1)), activate(V2))
U255(tt, V2) → U256(isLNat(activate(V2)))
U256(tt) → tt
U261(tt, V2) → U262(isLNatKind(activate(V2)))
U262(tt) → tt
U271(tt, V2) → U272(isLNatKind(activate(V2)))
U272(tt) → tt
U281(tt, N) → U282(isNaturalKind(activate(N)), activate(N))
U282(tt, N) → cons(activate(N), n__natsFrom(n__s(activate(N))))
U291(tt, N, XS) → U292(isNaturalKind(activate(N)), activate(N), activate(XS))
U292(tt, N, XS) → U293(isLNat(activate(XS)), activate(N), activate(XS))
U293(tt, N, XS) → U294(isLNatKind(activate(XS)), activate(N), activate(XS))
U294(tt, N, XS) → head(afterNth(activate(N), activate(XS)))
U301(tt, X, Y) → U302(isLNatKind(activate(X)), activate(Y))
U302(tt, Y) → U303(isLNat(activate(Y)), activate(Y))
U303(tt, Y) → U304(isLNatKind(activate(Y)), activate(Y))
U304(tt, Y) → activate(Y)
U31(tt, N, XS) → U32(isNaturalKind(activate(N)), activate(N), activate(XS))
U311(tt, XS) → U312(isLNatKind(activate(XS)), activate(XS))
U312(tt, XS) → pair(nil, activate(XS))
U32(tt, N, XS) → U33(isLNat(activate(XS)), activate(N), activate(XS))
U321(tt, N, X, XS) → U322(isNaturalKind(activate(N)), activate(N), activate(X), activate(XS))
U322(tt, N, X, XS) → U323(isNatural(activate(X)), activate(N), activate(X), activate(XS))
U323(tt, N, X, XS) → U324(isNaturalKind(activate(X)), activate(N), activate(X), activate(XS))
U324(tt, N, X, XS) → U325(isLNat(activate(XS)), activate(N), activate(X), activate(XS))
U325(tt, N, X, XS) → U326(isLNatKind(activate(XS)), activate(N), activate(X), activate(XS))
U326(tt, N, X, XS) → U327(splitAt(activate(N), activate(XS)), activate(X))
U327(pair(YS, ZS), X) → pair(cons(activate(X), YS), ZS)
U33(tt, N, XS) → U34(isLNatKind(activate(XS)), activate(N))
U331(tt, N, XS) → U332(isNaturalKind(activate(N)), activate(XS))
U332(tt, XS) → U333(isLNat(activate(XS)), activate(XS))
U333(tt, XS) → U334(isLNatKind(activate(XS)), activate(XS))
U334(tt, XS) → activate(XS)
U34(tt, N) → activate(N)
U341(tt, N, XS) → U342(isNaturalKind(activate(N)), activate(N), activate(XS))
U342(tt, N, XS) → U343(isLNat(activate(XS)), activate(N), activate(XS))
U343(tt, N, XS) → U344(isLNatKind(activate(XS)), activate(N), activate(XS))
U344(tt, N, XS) → fst(splitAt(activate(N), activate(XS)))
U41(tt, V1, V2) → U42(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U42(tt, V1, V2) → U43(isLNatKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2) → U44(isLNatKind(activate(V2)), activate(V1), activate(V2))
U44(tt, V1, V2) → U45(isNatural(activate(V1)), activate(V2))
U45(tt, V2) → U46(isLNat(activate(V2)))
U46(tt) → tt
U51(tt, V1, V2) → U52(isNaturalKind(activate(V1)), activate(V1), activate(V2))
U52(tt, V1, V2) → U53(isLNatKind(activate(V2)), activate(V1), activate(V2))
U53(tt, V1, V2) → U54(isLNatKind(activate(V2)), activate(V1), activate(V2))
U54(tt, V1, V2) → U55(isNatural(activate(V1)), activate(V2))
U55(tt, V2) → U56(isLNat(activate(V2)))
U56(tt) → tt
U61(tt, V1) → U62(isPLNatKind(activate(V1)), activate(V1))
U62(tt, V1) → U63(isPLNat(activate(V1)))
U63(tt) → tt
U71(tt, V1) → U72(isNaturalKind(activate(V1)), activate(V1))
U72(tt, V1) → U73(isNatural(activate(V1)))
U73(tt) → tt
U81(tt, V1) → U82(isPLNatKind(activate(V1)), activate(V1))
U82(tt, V1) → U83(isPLNat(activate(V1)))
U83(tt) → tt
U91(tt, V1) → U92(isLNatKind(activate(V1)), activate(V1))
U92(tt, V1) → U93(isLNat(activate(V1)))
U93(tt) → tt
afterNth(N, XS) → U11(isNatural(N), N, XS)
fst(pair(X, Y)) → U21(isLNat(X), X, Y)
head(cons(N, XS)) → U31(isNatural(N), N, activate(XS))
isLNat(n__nil) → tt
isLNat(n__afterNth(V1, V2)) → U41(isNaturalKind(activate(V1)), activate(V1), activate(V2))
isLNat(n__cons(V1, V2)) → U51(isNaturalKind(activate(V1)), 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(isNaturalKind(activate(V1)), activate(V1), activate(V2))
isLNatKind(n__nil) → tt
isLNatKind(n__afterNth(V1, V2)) → U111(isNaturalKind(activate(V1)), activate(V2))
isLNatKind(n__cons(V1, V2)) → U121(isNaturalKind(activate(V1)), activate(V2))
isLNatKind(n__fst(V1)) → U131(isPLNatKind(activate(V1)))
isLNatKind(n__natsFrom(V1)) → U141(isNaturalKind(activate(V1)))
isLNatKind(n__snd(V1)) → U151(isPLNatKind(activate(V1)))
isLNatKind(n__tail(V1)) → U161(isLNatKind(activate(V1)))
isLNatKind(n__take(V1, V2)) → U171(isNaturalKind(activate(V1)), activate(V2))
isNatural(n__0) → tt
isNatural(n__head(V1)) → U181(isLNatKind(activate(V1)), activate(V1))
isNatural(n__s(V1)) → U191(isNaturalKind(activate(V1)), activate(V1))
isNatural(n__sel(V1, V2)) → U201(isNaturalKind(activate(V1)), activate(V1), activate(V2))
isNaturalKind(n__0) → tt
isNaturalKind(n__head(V1)) → U211(isLNatKind(activate(V1)))
isNaturalKind(n__s(V1)) → U221(isNaturalKind(activate(V1)))
isNaturalKind(n__sel(V1, V2)) → U231(isNaturalKind(activate(V1)), activate(V2))
isPLNat(n__pair(V1, V2)) → U241(isLNatKind(activate(V1)), activate(V1), activate(V2))
isPLNat(n__splitAt(V1, V2)) → U251(isNaturalKind(activate(V1)), activate(V1), activate(V2))
isPLNatKind(n__pair(V1, V2)) → U261(isLNatKind(activate(V1)), activate(V2))
isPLNatKind(n__splitAt(V1, V2)) → U271(isNaturalKind(activate(V1)), activate(V2))
natsFrom(N) → U281(isNatural(N), N)
sel(N, XS) → U291(isNatural(N), N, XS)
snd(pair(X, Y)) → U301(isLNat(X), X, Y)
splitAt(0, XS) → U311(isLNat(XS), XS)
splitAt(s(N), cons(X, XS)) → U321(isNatural(N), N, X, activate(XS))
tail(cons(N, XS)) → U331(isNatural(N), N, activate(XS))
take(N, XS) → U341(isNatural(N), N, XS)
natsFrom(X) → n__natsFrom(X)
s(X) → n__s(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)
activate(n__natsFrom(X)) → natsFrom(activate(X))
activate(n__s(X)) → s(activate(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(X) → X

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