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.
