Mathematics for Computer Science

6.4. Arithmetic Expressions 187

Theorem 6.4.4.For all expressionse;f 2 Aexp andn 2 Z,

eval.subst.f;e/;n/Deval.e;eval.f;n//: (6.21)

Proof. The proof is by structural induction one.^1

Base cases:

 Case[x]

The left hand side of equation (6.21) equals eval.f;n/by this base case in

Definition 6.4.3 of the substitution function, and the right hand side also

equals eval.f;n/by this base case in Definition 6.4.2 of eval.

 Case[k].

The left hand side of equation (6.21) equalskby this base case in Defini-

tions 6.4.3 and 6.4.2 of the substitution and evaluation functions. Likewise,

the right hand side equalskby two applications of this base case in the Def-

inition 6.4.2 of eval.

Constructor cases:

 Case[[e 1 +e 2 ]]

By the structural induction hypothesis (6.21), we may assume that for all

f 2 Aexp andn 2 Z,

eval.subst.f;ei/;n/Deval.ei;eval.f;n// (6.22)

foriD1;2. We wish to prove that

eval.subst.f;[e 1 +e 2 ]/;n/Deval.[e 1 +e 2 ];eval.f;n// (6.23)

The left hand side of (6.23) equals

eval.[subst.f;e 1 /+subst.f;e 2 /];n/

by Definition 6.4.3.6.16 of substitution into a sum expression. But this equals

eval.subst.f;e 1 /;n/Ceval.subst.f;e 2 /;n/

(^1) This is an example of why it’s useful to notify the reader what the induction variable is—in this
case it isn’tn.