Proof: We use the first property of our assignment functions to derive that, in our new world, .
is a shorthand for the result of equating a term in the frame, , to the term .
We use the second property of our assignment function a to derive that . This follows as is in the frame, and is true in our current world, so we have that its value persists. We also show that in the same way.
We now use the effect axiom to derive that
Finally the definition of , which is in the core theory gives us
Proof: We use the first property of our assignment functions to derive that in our new world, as above.
We use the second property of our assignment functions to derive that and as we did previously.
We now use the frame axiom 18 to derive that
using the given fact that and . Finally the definition of gives us