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 p1(e), and p2(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.