Lemmas




Canonical Forms Lemma
~~~~~~~~~~~~~~~~~~~~~

If  .;P |-Z c n : <c',t',E'>  and  |- C : P


then
1. if Z = cf and (c' = B or c' = G), then . |- E' : kint

2. if Z = c' then c = c' and . |- E' : kint

3. if Z =/= c' and (Z =/= cf or c' =/= B and c' =/= G) then
	c = c' and
	t' = int  ==>  . |- E' = n
	t' = rit  ==>  . |- E' = n
	t' = All[D](G,A)  ==>  n in Dom(C)  and  . |- E' = n 

	
	
	
	
Subtyping Lemma:
----------------
If D |- t <= t' and D;P |-Z v:t then D;P |-Z v:t'

Proof:
By induction on the derivation of D;P |-Z v:t.  Each case uses inversion
of the subtyping rules and transitivity of D |- E1 = E2.
	



Equal Code Labels Lemma:
------------------------

If .;P |-f c n1: <c,All[D1](G2,A2),Et>  and  . |- Et = n2
then P |- n2 : All[D1](G2,A2)

Proof: 

For some f =/= c, inversion tells us that P |- All[D1](G2,A2) : Et and . |- Et = n1. 
By transitivity, . |- n1 = n2.
By equality, P |- n2 : All[D1](G2,A2)





Exp Conditional Lemma
~~~~~~~~~~~~~~~~~~~~~
If D |- Ez = 0    then  D |- Ez?Ef:Et = Et.
If D |- Ez =/= 0  then  D |- Ez?Ef:Et = Ef.

Proof: By definition of D |- E = E and definition of [[E]]




Substitution Structure Lemma
~~~~~~~~~~~~~~~~~~~~~~~~~~~~

If D |- S : (D',x:k)  
then Exists E, S'.  S = S', E/x  and  D |- E : k  and  D |- S' : D'

Proof: By inspection of (subst-t)
 



Exp Eq Trans Lemma
-------------------------

If  D |- E1 = E2   and  D |- E2 = E3  then  D |- E1 = E3
If  D |- seq1 = seq2  and  D |- seq2 = seq3  then  D |- seq1 = seq3

Proof: By definition of D |- E1 = E2 and definition of [[E]].




Color Weakening Lemma
~~~~~~~~~~~~~~~~~~~~~

If D;P |- v : t and then D;P |-c v : t 
If D;P |-c v: t and c = B or c = G  then D;P |-cf v:t

Proof: By case analysis of D;P |- v : t



Substitution Lemma
~~~~~~~~~~~~~~~~~~
1. If D,x:k |- E': k'  and  D |- E : k  then  D |- E'[E/x] : k'
2. If D,x:k |- E1 = E2  and  D |- E : k  then D |- E1[E/x] = E2[E/x]
3. If D,x:k;P |-Z v : t  and  D |- E : k  then  D;P |-Z v : t[E/x]
4. If D,x:k;P;G;A;Et;t |- b  and  D |- E : k  then  D;P;G[E/x];A[E/x];Et[E/x];t[E/x] |- b

5. If (D1,D2) |- E':k'  and  D1 |- S : D2  then D1 |- S(E') : k'
6. If (D1,D2) |- E1 = E2  and  D1 |- S : D2  then  D1 |- E1[E/x] = E2[E/x]
7. If (D1,D2);P |-Z v : t  and  D1 |- S : D2  then D1;P |-Z v : S(t)
8. If (D1,D2);P;G;I;A;Ei;to |- b  and D1 |- S : D2  then  D1;P;S(G);S(I);S(A);S(Ei);S(to) |- b


PROOF:
1. By induction on the structure of D,x:k |- E':k'.
2. By case analysis on the structure of D,x:k |- E1 = E2 using Part 1.
3. By case analysis on the structure of D,x:k;P |-Z v : t using Parts 1 and 2.
4. By induction on the structure of D,x:k;P;G;I;A |- b using Parts 1-3. The case for recovernz-t		
   divides into two subcases depending on if Ez = 0 and uses recovernz-eq-t or recovernz-neq-t as appropriate.

5-8. By induction on the size of D, using Parts 1-4 respectively.