YES Termination Proof using AProVETerm Rewriting System R:
[N, X, XS, YS, ZS, Y]
U11(tt, N, X, XS) -> U12(splitAt(N, XS), X)
U12(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
afterNth(N, XS) -> snd(splitAt(N, XS))
and(tt, X) -> X
fst(pair(X, Y)) -> X
head(cons(N, XS)) -> N
natsFrom(N) -> cons(N, natsFrom(s(N)))
sel(N, XS) -> head(afterNth(N, XS))
snd(pair(X, Y)) -> Y
splitAt(0, XS) -> pair(nil, XS)
splitAt(s(N), cons(X, XS)) -> U11(tt, N, X, XS)
tail(cons(N, XS)) -> XS
take(N, XS) -> fst(splitAt(N, XS))

Termination of R to be shown. 



   R
     ↳Orthogonal Check



This CSR is orthogonal, so it is sufficient to show innermost termination. 


   R
     ↳OrthoCSR
       →TRS1
         ↳CSR to TRS Transformation




Zantema-Transformation successful.
Replacement map:
and(1, 2)
splitAt(1, 2)
natsFrom(1)
U12(1, 2)
take(1, 2)
tail(1)
sel(1, 2)
U11(1, 2, 3, 4)
afterNth(1, 2)
pair(1, 2)
cons(1, 2)
snd(1)
s(1)
fst(1)
head(1)

Old CSR:

U11(tt, N, X, XS) -> U12(splitAt(N, XS), X)
U12(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
afterNth(N, XS) -> snd(splitAt(N, XS))
and(tt, X) -> X
fst(pair(X, Y)) -> X
head(cons(N, XS)) -> N
natsFrom(N) -> cons(N, natsFrom(s(N)))
sel(N, XS) -> head(afterNth(N, XS))
snd(pair(X, Y)) -> Y
splitAt(0, XS) -> pair(nil, XS)
splitAt(s(N), cons(X, XS)) -> U11(tt, N, X, XS)
tail(cons(N, XS)) -> XS
take(N, XS) -> fst(splitAt(N, XS))

new TRS:

U11(tt, N, X, XS) -> U12(splitAt(a(N), a(XS)), a(X))
U12(pair(YS, ZS), X) -> pair(cons(a(X), YS), ZS)
splitAt(0, XS) -> pair(nil, XS)
splitAt(s(N), cons(X, XS)) -> U11(tt, N, X, a(XS))
a(natsFrom(x0)) -> natsFrom(x0)
afterNth(N, XS) -> snd(splitAt(N, XS))
snd(pair(X, Y)) -> Y
and(tt, X) -> a(X)
fst(pair(X, Y)) -> X
head(cons(N, XS)) -> N
natsFrom(N) -> cons(N, natsFrom(s(N)))
natsFrom(x0) -> natsFrom(x0)
sel(N, XS) -> head(afterNth(N, XS))
tail(cons(N, XS)) -> a(XS)
take(N, XS) -> fst(splitAt(N, XS))



   R
     ↳OrthoCSR
       →TRS1
         ↳CSRtoTRS
           →TRS2
             ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

U11'(tt, N, X, XS) -> U12'(splitAt(a(N), a(XS)), a(X))
U11'(tt, N, X, XS) -> SPLITAT(a(N), a(XS))
U11'(tt, N, X, XS) -> A(N)
U11'(tt, N, X, XS) -> A(XS)
U11'(tt, N, X, XS) -> A(X)
U12'(pair(YS, ZS), X) -> A(X)
SPLITAT(s(N), cons(X, XS)) -> U11'(tt, N, X, a(XS))
SPLITAT(s(N), cons(X, XS)) -> A(XS)
A(natsFrom(x0)) -> NATSFROM(x0)
AFTERNTH(N, XS) -> SND(splitAt(N, XS))
AFTERNTH(N, XS) -> SPLITAT(N, XS)
AND(tt, X) -> A(X)
SEL(N, XS) -> HEAD(afterNth(N, XS))
SEL(N, XS) -> AFTERNTH(N, XS)
TAIL(cons(N, XS)) -> A(XS)
TAKE(N, XS) -> FST(splitAt(N, XS))
TAKE(N, XS) -> SPLITAT(N, XS)

Furthermore, R contains one SCC. 


   R
     ↳OrthoCSR
       →TRS1
         ↳CSRtoTRS
           →TRS2
             ↳DPs
             ...
               →DP Problem 1
                 ↳Negative Polynomial Order


Dependency Pairs:

SPLITAT(s(N), cons(X, XS)) -> U11'(tt, N, X, a(XS))
U11'(tt, N, X, XS) -> SPLITAT(a(N), a(XS))


Rules:


U11(tt, N, X, XS) -> U12(splitAt(a(N), a(XS)), a(X))
U12(pair(YS, ZS), X) -> pair(cons(a(X), YS), ZS)
splitAt(0, XS) -> pair(nil, XS)
splitAt(s(N), cons(X, XS)) -> U11(tt, N, X, a(XS))
a(natsFrom(x0)) -> natsFrom(x0)
afterNth(N, XS) -> snd(splitAt(N, XS))
snd(pair(X, Y)) -> Y
and(tt, X) -> a(X)
fst(pair(X, Y)) -> X
head(cons(N, XS)) -> N
natsFrom(N) -> cons(N, natsFrom(s(N)))
natsFrom(x0) -> natsFrom(x0)
sel(N, XS) -> head(afterNth(N, XS))
tail(cons(N, XS)) -> a(XS)
take(N, XS) -> fst(splitAt(N, XS))





The following Dependency Pair can be strictly oriented using the given order.

SPLITAT(s(N), cons(X, XS)) -> U11'(tt, N, X, a(XS))


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

a(natsFrom(x0)) -> natsFrom(x0)
natsFrom(N) -> cons(N, natsFrom(s(N)))
natsFrom(x0) -> natsFrom(x0)


Used ordering:
Polynomial Order with Interpretation:

POL( SPLITAT(x1, x2) ) = x1


POL( s(x1) ) = 1


POL( U11'(x1, ..., x4) ) = 0


POL( a(x1) ) = 0


POL( natsFrom(x1) ) = 0


POL( cons(x1, x2) ) = 0


POL( natsFrom(x1) ) = 0



This results in one new DP problem. 


   R
     ↳OrthoCSR
       →TRS1
         ↳CSRtoTRS
           →TRS2
             ↳DPs
             ...
               →DP Problem 2
                 ↳Dependency Graph


Dependency Pair:

U11'(tt, N, X, XS) -> SPLITAT(a(N), a(XS))


Rules:


U11(tt, N, X, XS) -> U12(splitAt(a(N), a(XS)), a(X))
U12(pair(YS, ZS), X) -> pair(cons(a(X), YS), ZS)
splitAt(0, XS) -> pair(nil, XS)
splitAt(s(N), cons(X, XS)) -> U11(tt, N, X, a(XS))
a(natsFrom(x0)) -> natsFrom(x0)
afterNth(N, XS) -> snd(splitAt(N, XS))
snd(pair(X, Y)) -> Y
and(tt, X) -> a(X)
fst(pair(X, Y)) -> X
head(cons(N, XS)) -> N
natsFrom(N) -> cons(N, natsFrom(s(N)))
natsFrom(x0) -> natsFrom(x0)
sel(N, XS) -> head(afterNth(N, XS))
tail(cons(N, XS)) -> a(XS)
take(N, XS) -> fst(splitAt(N, XS))





Using the Dependency Graph resulted in no new DP problems.

Termination of R successfully shown.
Duration:
0:06 minutes