The proof is accomplished by an
induction on the expression *e* being compiled.
We prove it first for constants, then for variables, and then for sums on the
induction hypothesis that it is true for the summands. Thus there are three
cases.

I.isconst(e). We have

II.isvar(e). We have

III.issum(e). In this case, we first write

using the relation between concatenating programs and composing the functions they represent. Now we introduce some notation. Let

so that . Further let

so that = outcome(compile( , and we want to prove that

We have

and

Now

and

Next

=

Here we again use the induction hypothesis that *s*2(*e*) is compiled
correctly. In order to apply it, we need
*c*(loc( ,map), for
each variable which is proved as follows:

Now we can continue with

Finally,

This concludes the proof.

Wed Sep 29 13:40:01 PDT 1999