These functions are taken from [McC62] with slight changes.

We work with a state vector . It will be the situation *s* in
our application, but we use here in order to emphasize the
mathematical notion. There are two functions.

denotes the contents of the variable *var* in the state
.

denotes the new state obtained by assigning the
value *value* to the variable *var* in the state and leaving
all the other variables with the values they have in the state .

We have the axioms

These axioms capture the notion that an assignment of a value produces a new state in which just that variable has its value changed. These functions are just what we need when we introduce frames.

Thu Jan 30 13:14:14 PDT 1997