Remark

Suppose that D = and R is a sequence of a declaration-free rule and a declaration rule with atomic declaration ``Var v ranges over U '' followed by a declaration-free body . Further suppose that U is empty in a state S appropriate for R and thus Updates(D, , S) = . Then Updates(D, R, S) equals Updates(D, , S) which may be not empty. Contrary to the situation in 4.1.2, the empty range does not give inconsistency here. One cannot choose an element from the empty set, but one can execute a for every v in the empty set: just do not execute anything.