The problem of the relations between source language and object language arithmetic is dealt with here by assuming that the + signs in formulas (2.1) and (3.11) which define the semantics of the source and object languages represent the same operation. Theorem 1 does not depend on any properties of this operation, not even commutativity or associativity.

The proof is entirely straightforward once the necessary machinery has been created. Additional operations such as subtraction, multiplication and division could be added without essential change in the proof.

For example, to put multiplication into the system the following changes would be required.

1. Add isprod(*e*), and *p*1(e), and *p*2(*e*) to the abstract syntax of the source
language.

2. Add a term

**if **isprod(*e*) **then ** value(
value(

to Equation (2.1).

3. Add

to the hypotheses of the source language induction principle.

4. Add an instruction mul *x* and the three syntactical
functions ismul(*s*) adr(*r*), mkmul(*x*) to the abstract syntax
of the object language together with the necessary relations among them.

5. Add to the definition (3.11) of *step* a term

6. Add to the compiler a term

7. Add to the proof a case isprod(*e*) which parallels the case
issum(*e*) exactly.

The following other extensions are contemplated.

1. Variable length sums.

2. Sequences of assignment statements.

3. Conditional expressions.

4. **go to** statements in the source language.

In order to make these extensions, a complete revision of the formalism will be required.

Wed Sep 29 13:40:01 PDT 1999