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