MAYBE 0.08/0.19 MAYBE 0.08/0.19 0.08/0.19 Problem: 0.08/0.19 U11(tt(),N,X,XS) -> U12(splitAt(activate(N),activate(XS)),activate(X)) 0.08/0.19 U12(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS) 0.08/0.19 afterNth(N,XS) -> snd(splitAt(N,XS)) 0.08/0.19 and(tt(),X) -> activate(X) 0.08/0.19 fst(pair(X,Y)) -> X 0.08/0.19 head(cons(N,XS)) -> N 0.08/0.19 natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) 0.08/0.19 sel(N,XS) -> head(afterNth(N,XS)) 0.08/0.19 snd(pair(X,Y)) -> Y 0.08/0.19 splitAt(0(),XS) -> pair(nil(),XS) 0.08/0.19 splitAt(s(N),cons(X,XS)) -> U11(tt(),N,X,activate(XS)) 0.08/0.19 tail(cons(N,XS)) -> activate(XS) 0.08/0.19 take(N,XS) -> fst(splitAt(N,XS)) 0.08/0.19 natsFrom(X) -> n__natsFrom(X) 0.08/0.19 s(X) -> n__s(X) 0.08/0.19 activate(n__natsFrom(X)) -> natsFrom(activate(X)) 0.08/0.19 activate(n__s(X)) -> s(activate(X)) 0.08/0.19 activate(X) -> X 0.08/0.19 0.08/0.19 Proof: 0.08/0.19 Open 0.08/0.19 EOF