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,l to if null?(l) then false else or(x = first(l), member(x, rest(l))); zeroes := cons(0, zeros); in member (1, zeros) => let ... in (map x, l to ...)(1, cons(0, zeroes)) [*] => let ... in if null?(cons(0,zeroes)) then false else or(1 = first(cons(0,zeroes)), member(1,rest(cons(0,zeroes)))) => let ... in if false then false else or(1 = first(cons(0,zeroes)), member(1,rest(cons(0,zeroes)))) => let ... in or(1 = first(cons(0,zeroes)), member(1,rest(cons(0,zeroes)))) => let ... in (map x,y to ...)(1 = first(cons(0,zeroes)), member(1,rest(cons(0,zeroes)))) => let ... in (map x,y to ...)(1 = 0, member(1,rest(cons(0,zeroes)))) => let ... in (map x,y to ...)(false, (map x,l to ...)(1,rest(cons(0,zeroes)))) => let ... in (map x,y to ...)(false, (map x,l to ...)(1,zeroes)) => let ... in (map x,y to ...)(false, (map x,l to ...)(1,cons(0,zeroes))) which is let ... in (map x,y to ...)(false, [**]) where [*] above is let ... in [**] We have generated exactly the same reduction subproblem (reducing the phrase [**} as we had in [*] above. Hence this computation diverges.