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