(0) Obligation:
Generalized rewrite system (where rules with free variables on rhs are allowed):
The TRS R consists of the following rules:
U12(tt) → snd(splitAt(N, XS))
U22(tt) → X
U32(tt) → N
U42(tt) → head(afterNth(N, XS))
U52(tt) → Y
U63(tt) → U64(splitAt(N, XS))
U64(pair(YS, ZS)) → pair(cons(X), ZS)
U72(tt) → XS
U82(tt) → fst(splitAt(N, XS))
U11(tt) → U12(tt)
U21(tt) → U22(tt)
U31(tt) → U32(tt)
U41(tt) → U42(tt)
U51(tt) → U52(tt)
U61(tt) → U62(tt)
U62(tt) → U63(tt)
U71(tt) → U72(tt)
U81(tt) → U82(tt)
afterNth(N, XS) → U11(tt)
fst(pair(X, Y)) → U21(tt)
head(cons(N)) → U31(tt)
natsFrom(N) → cons(N)
sel(N, XS) → U41(tt)
snd(pair(X, Y)) → U51(tt)
splitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X)) → U61(tt)
tail(cons(N)) → U71(tt)
take(N, XS) → U81(tt)