**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

Wed Jul 12 14:10:43 PDT 2000