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)));
        zeros := cons(0, zeros);
   in member(1, zeros)

=> let ... in (map x,s to ...)(1, zeros)
=> let ... in if null?(zeros) then false
              else or(1 = first(zeros), member(1,rest(zeros)))
=> let ... in if null?(cons(0,zeros)) then false
              else or(1 = first(zeros), member(1,rest(zeros)))
=> let ... in if false then false
              else or(1 = first(zeros), member(1,rest(zeros)))
=> let ... in or(1 = first(zeros), member(1,rest(zeros)))
=> let ... in (map x,y to ...)(1 = first(zeros), member(1,rest(zeros)))
=> let ... in if 1 = first(zeros) then true else member(1,rest(zeros))
=> let ... in if 1 = first(cons(0,zeros)) then true else member(1,rest(zeros))
=> let ... in if 1 = 0 then true else member(1,rest(zeros))
=> let ... in if false then true else member(1,rest(zeros))
=> let ... in member(1,rest(zeros))

which is semantically equivalent to exactly where we started (because
zeros = rest(zeros), yet no closer to an answer implying the
evaluation diverges.  Note that subsequent computation will generate steps

=> let ... in member(1,rest( ... (rest(zeros))...)

where the second ellipsis is filled in by progressively longer stacks
of applications of rest.