A.8 Lemma

---

A.8 Lemma

If

   if t1 then t2 else t3 →* v, 

then either t₁ →* true and t₂ →* v or t₁ →* false and t₃ →* v. Moreover, the evaluation sequences for t₁ and t₂ or t₃ are strictly shorter than the given evaluation sequence. (And similarly for the other term constructors.)

Proof: By induction on the length of the given evaluation sequence. Since a condition is not a value, there must be at least one step of evaluation. Proceed by case analysis on the final rule used in this step (note that it must be one of the If rules).

Case E-IF:

By the induction hypothesis, either and t₂ →* v or and t₃ →* v. Adding the initial step to the derivation of or yields the desired result. It is easy to check that the resulting evaluation sequences are shorter than the original.

Case E-IFTRUE:

if true then t₂ else t₂ → t₂ →* v

Immediate.

Case E-IFFALSE:

if false then t₂ else t₂ →t₃ →* v

Immediate.

---