A.7 Proposition

 < Free Open Study > 



A.7 Proposition

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 > 



Types and Programming Languages
Types and Programming Languages
ISBN: 0262162091
EAN: 2147483647
Year: 2002
Pages: 262

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net