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))); zeroes := cons(0, zeros); in member(1, zeros) => let ... in (map x,s to ...)(1, zeroes) => let ... in if null?(zeroes) then false else or(1 = first(zeroes), member(1,rest(zeroes))) => let ... in if false then false else or(1 = first(zeroes), member(1,rest(zeroes))) => let ... in or(1 = first(zeroes), member(1,rest(zeroes))) => let ... in (map x,y to ...)(1 = first(zeroes), member(1,rest(zeroes))) => let ... in if 1 = first(zeroes) then true else member(1,rest(zeroes)) => let ... in if 1 = first(cons(0,zeroes)) then true else member(1,rest(zeroes)) => let ... in if 1 = 0 then true else member(1,rest(zeroes)) => let ... in if false then true else member(1,rest(zeroes)) => let ... in member(1,rest(zeroes)) which is exactly where we started, implying the evaluation diverges