| < Free Open Study > |
|
If t ⇓ v then t →* v.
Proof: By induction on the derivation of t ⇓ v, with a case analysis on the final rule used.
Case B-VALUE: | t = v |
Immediate.
Case B-IFTRUE: | t = if t1 then t2 else t3 t1 ⇓ true t2 ⇓ v |
By the induction hypothesis, t1 →* true. By Lemma A.6,
if t1 then t2 else t3 →* if true then t2 else t3.
By E-IFTRUE, if true then t2 else t3 → t2. By the induction hypothesis, t2 →* v. The result then follows by the transitivity of →*.
The other cases are similar.
| < Free Open Study > |
|