(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(