The abstract analytic syntax of the source expressions is given by the table:
which asserts that the expressions comprise constants, variables and binary sums, that the predicates isconst, isvar, and issum enable one to classify each expression and that each sum e has summands s1(e) and s2(e).
The semantics is given by the formula
where val(e) gives the numerical value of an expression e representing
a constant, 
gives the value of the variable e in the state
vector 
and + is some binary operation. (It is natural to regard +
as an operation that resembles addition of real numbers, but our
results do not depend on this).
For our present purposes we do not have to give a synthetic syntax for the source language expressions since both the interpreter and the compiler use only the analytic syntax. However, we shall need the following induction principle for expressions:
Suppose 
is a predicate applicable to expressions, and suppose that
for all expressions e we have
Then we may conclude that 
is true for all expressions e.