Note: the lazy semantics for cons are reflected by three changes to our evaluation rules: (i) cons(M,N) is a value for all expressions M,N. (ii) first(cons(M,N)) = M (iii) rest(cons(M,N)) = N let or := map x,y to if x then true else y; member := map x,s to if null?(s) then false else or(x = first(s), member(x, rest(s))); countup := map x to cons(x, countup(1+x)); in member (1, countup(0)) => let ... in (map x, s to ...)(1, countup(0)) => let ... in if null?(countup(0)) then false else or(1 = first(countup(0)), member(1,rest(countup(0)))) => let ... in if null?(cons(0,countup(1+0))) then false else or(1 = first(countup(0)), member(1,rest(countup(0)))) => let ... in if false then false else or(1 = first(countup(0)), member(1,rest(countup(0)))) => let ... in or(1 = first(countup(0)), member(1,rest(countup(0)))) => let ... in (map x,y to ...)(1 = first(countup(0)), member(1,rest(countup(0)))) => let ... in if 1 = first(countup(0)) then true else member(1,rest(countup(0)))) => let ... in if 1 = first(cons(0, countup(1+0))) then true else member(1,rest(countup(0)))) => let ... in if 1 = 0 then true else member(1,rest(countup(0)))) => let ... in if false then true else member(1,rest(countup(0)))) => let ... in member(1,rest(countup(0)))) => let ... in (map x, s to ...)(1,rest(countup(0)))) => let ... in if null?(rest(countup(0))) then false else or(1 = first(rest(countup(0))), member(1,rest(rest(countup(0))))) => let ... in if null?(rest(cons(0,countup(1+0)))) then false else or(1 = first(rest(countup(0))), member(1,rest(rest(countup(0))))) => let ... in if null?(countup(1+0))) then false else or(1 = first(rest(countup(0))), member(1,rest(rest(countup(0))))) => let ... in if null?(countup(1))) then false else or(1 = first(rest(countup(0))), member(1,rest(rest(countup(0))))) => let ... in if null?(cons(1,countup(1+1))) then false else or(1 = first(rest(countup(0))), member(1,rest(rest(countup(0))))) => let ... in if false then false else or(1 = first(rest(countup(0))), member(1,rest(rest(countup(0))))) => let ... in or(1 = first(rest(countup(0))), member(1,rest(rest(countup(0))))) => let ... in (map x,y to ...)(1 = first(rest(countup(0))), member(1,rest(rest(countup(0))))) => let ... in if 1 = first(rest(countup(0))) then true else member(1,rest(rest(countup(0)))) => let ... in if 1 = first(rest(cons(0,countup(1+0)))) then true else member(1,rest(rest(countup(0)))) => let ... in if 1 = first(countup(1+0)) then true else member(1,rest(rest(countup(0)))) => let ... in if 1 = first(cons(1+0,countup(1+0)) then true else member(1,rest(rest(countup(0)))) => let ... in if 1 = 1+0 then true else member(1,rest(rest(countup(0)))) => let ... in if 1 = 1 then true else member(1,rest(rest(countup(0)))) => let ... in if true then true else member(1,rest(rest(countup(0)))) => let ... in true Done.