MAYBE

Problem:
 U11(tt(),N,XS) -> U12(tt(),activate(N),activate(XS))
 U12(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
 U21(tt(),X) -> U22(tt(),activate(X))
 U22(tt(),X) -> activate(X)
 U31(tt(),N) -> U32(tt(),activate(N))
 U32(tt(),N) -> activate(N)
 U41(tt(),N,XS) -> U42(tt(),activate(N),activate(XS))
 U42(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
 U51(tt(),Y) -> U52(tt(),activate(Y))
 U52(tt(),Y) -> activate(Y)
 U61(tt(),N,X,XS) -> U62(tt(),activate(N),activate(X),activate(XS))
 U62(tt(),N,X,XS) -> U63(tt(),activate(N),activate(X),activate(XS))
 U63(tt(),N,X,XS) -> U64(splitAt(activate(N),activate(XS)),activate(X))
 U64(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
 U71(tt(),XS) -> U72(tt(),activate(XS))
 U72(tt(),XS) -> activate(XS)
 U81(tt(),N,XS) -> U82(tt(),activate(N),activate(XS))
 U82(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
 afterNth(N,XS) -> U11(tt(),N,XS)
 fst(pair(X,Y)) -> U21(tt(),X)
 head(cons(N,XS)) -> U31(tt(),N)
 natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
 sel(N,XS) -> U41(tt(),N,XS)
 snd(pair(X,Y)) -> U51(tt(),Y)
 splitAt(0(),XS) -> pair(nil(),XS)
 splitAt(s(N),cons(X,XS)) -> U61(tt(),N,X,activate(XS))
 tail(cons(N,XS)) -> U71(tt(),activate(XS))
 take(N,XS) -> U81(tt(),N,XS)
 natsFrom(X) -> n__natsFrom(X)
 s(X) -> n__s(X)
 activate(n__natsFrom(X)) -> natsFrom(activate(X))
 activate(n__s(X)) -> s(activate(X))
 activate(X) -> X

Proof:
 Open