THEOREM[preservation]
    If C = D;U;R;G;P;L and |- C and C |- prog and (U;R;L;prog) --> (U';R';L';prog')
    then |- C' and C' |- prog' where C' = D;U';R';G;P;L'
Follows from:
(1) If |- C and C |- e:t and e --> e'
    then C |- e':t
(2) If C = D;Up;R;G;P;L and |- C,Us and C |- e:t
    and Us,Up;R;e --> U';R';e'
    then |- C',Us and C' |- e':t
    where C' = D;Up';R';G;P;L and U'=Us,Up' and R' = R R'' for some R'' and Up'
(3) If C = D;Up;R;G;P;L and |- C,Us and C |- c:t
    and Us,Up;R;c --> U';R';c'
    then |- C',Us and C' |- c':t
    where C' = D;Up';R';G;P;L and U'=Us,Up' and R' = R R'' for some R'' and Up'
(4) If C = D;Up;R;G;P;Lp and |- C,Us,Ls and C |- prog
    and Us,Up;R;Ls,Lp;prog --> U';R';L';prog'
    then |- C',Us,Ls and C' |- prog'
    where C' = D;Up';R';G;P;Lp' and U'=Us,Up' and L'=Ls,Lp' and R' = R R'' for some R'' and Up' and Lp'

Proof by induction on the typing derivation.  See below.

THEOREM[progress]
    If C = {};U;R;{};P;L and |- C and C |- prog
    then there is some U';R';L';prog' such that U;R;L;prog --> U';R';L';prog'
Follows from:
(1) If C = {};U;R;{};P;L and |- C and C |- e:t and e is not a value
    and there is no t' such that C |- t = %t'
    then there is some e' such that e --> e'
(2) If C = {};Up;R;{};P;L and |- C,Us and C |- e:t and e is not a value
    then there is some Up';R';e' such that Us,Up;R;e --> Us,Up';R';e'
(3) If C = {};Up;R;{};P;L and |- C,Us and C |- c:t and c is not a value
    then there is some Up';R';c' such that Us,Up;R;c --> Us,Up';R';c'
(4) If C = {};Up;R;{};P;Lp and |- C,Us,Ls and C |- prog
    then there is some U';R';L';prog' such that Us,Up;R;Ls,Lp;prog --> Us,Up';R';Ls,Lp';prog'

Proof by induction on the typing derivation.  See below.

LEMMA[typing inversion]
If C |- e:t than a rule other than 

  C |- e:t1
  C |- t1 = t2
  ------------
  C |- e:t2

concludes C |- e:t', where C |- t=t'

Proof by induction on C |- e:t, where any derivation not rooted at the t1=t2 rule
above is a base case.  (The only induction case is the t1=t2 rule above.)

LEMMA[type weakening]
If D |- t:k and D'=D,A:k then D' |- t:k
Proof by induction on D |- t:k

LEMMA[type equivalence weakening]
If R |- t1=t2 and R'=R,q_k->t then R' |- t1=t2
Proof by induction on R |- t1=t2

LEMMA[expression weakening]
If C = D;U;R;G;P;L
and C'=D,A:k;U;R;G;P;L or C'=D;U;R,q_k->t;G;P;L or C'=D;U;R;G,!x->t;P;L then
(1) If C |- e:t then C' |- e:t
(2) If C |- c:t then C' |- c:t
(3a) If (C);(Cb) |- ins:t then (C');(Cb) |- ins:t
(3b) If (Ca);(C) |- ins:t then (Ca);(C') |- ins:t
(4) If C |- blk then C' |- blk
(5) If C |- n->b:t then C' |- n->b:t
(6) If C' = D';U;R';G;{};L and C |- prog then C' |- prog
Proof by inductions on typing derivations.

LEMMA[single-step type confluence]

If R |- ta => tb and R |- ta => tc
then there is a td s.t. R |- tb=>td and R |- tc => td

Proof by induction on sum of sizes of derivations of R |- ta => tb and R |- ta => tc.

Label the => rules as follows:

  R |- t =1> t

  R |- tj => tj' ... R |- tk => tk'
  ---------------------------------
  R |- T[t1...tk] =2> T[t1'...tk']

  R |- (\A:k.tb) ta =3> [A<-ta]tb

  R,q_k->t |- type(q_k) =4> type(t)

  R |- (type(t1)) t2 =5> type(t1 t2)

  R |- (pf(t1)) t2 =6> pf(t1 t2)

For brevity, the cases below elide the "R |- ".

The following x,y produce syntactically legal ta =x> tb and ta =y> tc:
   x,x
   1,y
   x,1
   2,y
   x,2

CASE 1,y: ta=tb, so choose td=tc

CASE x,1: ta=tc, so choose td=tb

CASE 2,2:
   T[ta1...tak] => T[tb1...tbk]
   T[ta1...tak] => T[tc1...tck]
   By induction, tb1=>td1...tbk=>tdk and tc1=>td1...tck=>tdk
   By rule =2>:
     T[tb1...tbk] => T[td1...tdk]
     T[tc1...tck] => T[td1...tdk]

CASE x,x for x=3,4,5,6: tb=tc, so choose td=tb=tc

CASE 2,3:
(\A:k.ta') ta'' => (\A:k.tb') tb'' where ta'=>tb' and ta''=>tb''
(\A:k.ta') ta'' => [A<-ta'']ta'
Choose td = [A<-tb'']tb'


CASE 2,4:
type(qa) => type(qb) where qa => qb
R,qa->t |- type(qa) => type(t)
The only => rule for qa=>qb is qa=>qa, so qb=qa
Choose td = type(t)


CASE 2,5:
(type(ta1)) ta2 => type(ta1 ta2)
Similar to case 2,6.


CASE 2,6:

(pf(ta1)) ta2 => (pf(tb1)) tb2 where ta1=>tb1 and ta2=>tb2
(pf(ta1)) ta2 => pf(ta1 ta2)
Choose td = pf(tb1 tb2)


CASES 3,2 and 4,2 and 5,2 and 6,2: see cases 2,3 and 2,4 and 2,5 and 2,6


LEMMA[type confluence]

Define t0 =>* tn to mean t0=>t1=>t2=>t3...=>tn, where n>=0.
If R |- tb = tc then there is a td s.t. R |- tb =>* td and R |- tc =>* td

Proof by single-step type confluence using standard tiling argument.
(e.g. see Pierce, "Types and Programming Languages")


LEMMA[single-step type equivalence inversion]

If R |- S[t1...tn] => t' then t' = S[t1'...tn']
where R |- t1=>t1' ... R |- tn=>tn'

and:
  S[t1] = !t1 | s(t1) | all A:k.t1 | exists A:k.t1 | \A:k.t1 | Delay t1 | %t1
  S[t1,t2] = t1 -o t2 | t1*t2 | Reg t1 t2 | Mem t1 t2 | Code t1 t2
(S is the same as T, but excludes (if0 t1 t2 t3) and (t1 t2) and type(t1) and pf(t1), and includes %t1)

Proof by cases of definition of => (no induction).  For example:

R |- t1 => t1'
----------------------
R |- pf(t1) => pf(t1')
----------------------------------
R |- type(pf(t1)) => type(pf(t1'))
(i.e. R |- %t1 => %t1')
(no other derivation of type(pf(t1)) => type(pf(t1')) is possible)

It's important to observe that these rules are not applicable to S[t1...tn]=>t':
  R |- (\A:k.tb) ta => [A<-ta]tb
  R |- if0 0 tz ts => tz
  R |- if0 s(tm) tz ts => ts tm
  R,q_k->t |- type(q_k) => type(t)
  R |- (type(t1)) t2 => type(t1 t2)
  R |- (pf(t1)) t2 => pf(t1 t2)
For example, type(q_k) does not match any S[t1] or S[t1,t2],
since type(q_k) does not syntactically match %t=type(pf(t)) for any t.


LEMMA[type equivalence inversion]

If R |- S[t1...tn] = S'[t1'...tm'] then S = S' and n=m and R |- t1=t1' ... R |- tn=tn'

Proof:
By lemma[type confluence], then there is some t''
such that R |- S[t1...tn] =>* t'' and R |- S'[t1'...tm'] =>* t''

By induction on number of => steps
and single-step type equivalence inversion lemma:
  - If t = S[t1...tn] and R |- t =>* t'' then t'' = S[t1''...tn'']
    where R |- t1 =>* t1'' ... R |- tn =>* tn''
  - If t' = S'[t1'...tm'] and R |- t' =>* t'' then t'' = S'[t1''...tm'']
    where R |- t1' =>* t1'' ... R |- tm' =>* tm''
So S=S' and m=n.
From R |- tk =>* tk'' conclude R |- tk = tk'' (repeated transitivity)
From R |- tk' =>* tk'' conclude R |- tk' = tk'' (repeated transitivity)
Thus conclude R |- tk = tk' (symmetry, transitivity).


LEMMA[type(q) equivalence inversion]

If R |- type(q_k) = type(q_k') and q_k not in domain(R) and q_k' not in domain(R)
then q_k=q_k'
Proof:
By lemma[type confluence], then there is some t''
such that R |- type(q_k) =>* t'' and R |- type(q_k') =>* t''

Consider R |- type(q_k) =>* t''.
The rule R,q_k->t |- type(q_k) => type(t) is inapplicable, since q_k,q_k' not in domain(R)
The only applicable rule is:
R |- q_k => q_k
---------------------------
R |- type(q_k) => type(q_k)
Therefore, t'' = type(q_k)

By the same reasoning, t'' = type(q_k').  So q_k = q_k'.


LEMMA[type equivalence kinds]
If C = D;U;R;G;P;L and |- C and D |- t1:k and R |- t1=t2 then D |- t2:k
Proof by induction on R |- t1=t2.
Sample case: R,q_k->t |- type(q_k) = type(t)
  Kinding rule for q_k says D |- q_k:k.
  Kinding rule for type(...) says D |- type(q_k):k
  |- C implies forall q_k->t in R, |- t:k.
  Kinding rule for type(...) says D |- type(t):k


LEMMA[environment typing / expression kinds]
(1) If C = D;U;R;G;P;L and |- C and C |- e:t then D |- t:type
(2) Suppose C |- e:t by some typing rule with
premises ...C' |- e':t'....  Then |- C implies |- C'.

Proof by induction on C |- e:t.


LEMMA[type substitution]
If C,A:ka |- t:k and D |- ta:ka then D |- [A<-ta]t:k
Proof by induction on C,A:ka |- t:k.


LEMMA[type equivalence substitution]
If R |- t1=t2 and (forall q_k->t in R, |- t:k)
then R |- [A<-t']t1=[A<-t']t2
Proof by induction on R |- t1=t2.


LEMMA[expression type substitution]
If C = D;U;R;G;P;L and |- C and C |- ta:ka then
(1) If C,A:ka |- eb:tb
    then D;U;R;[A<-ta]G;P;L |- [A<-ta]eb:[A<-ta]tb
(2) If C,A:ka |- cb:tb
    then D;U;R;[A<-ta]G;P;L |- [A<-ta]cb:[A<-ta]tb
(3) If C,A:ka |- blk
    then D;U;R;[A<-ta]G;P;L |- [A<-ta]blk
(4) If C,A:ka |- n->b:tb
    then D;U;R;[A<-ta]G;P;L |- n->[A<-ta]b:[A<-ta]tb
(5) If C,A:ka |- prog
    then D;U;R;[A<-ta]G;P;L |- [A<-ta]prog
Proof by induction on typing derivations for eb,cb,blk,n->b,prog.


LEMMA[expression nonlinear substitution]
If |- !Ca,Cb and !Ca |- ea:ta then
(1) If Cb,!x:ta |- eb:tb
    then !Ca,Cb |- [x<-ea]eb:tb
(2) If Cb,!x:ta |- cb:tb
    then !Ca,Cb |- [x<-ea]cb:tb
(3) If Cb,!x:ta |- blk
    then !Ca,Cb |- [x<-ea]blk
(4) If Cb,!x:ta |- n->b:tb
    then !Ca,Cb |- n->[x<-ea]b:tb
(5) If Cb,!x:ta |- prog and Ca=D;U;R;G;{};L
    then !Ca,Cb |- [x<-ea]prog
Proof by induction on typing derivations for eb,cb,blk,n->b,prog.

CASE
!C,!x:ta |- x:ta
!Ca |- [x<-ea]x:ta
By weakening, !Cb,!Ca |- [x<-ea]x:ta

CASE
!Cb,!x:ta |- e:t
------------------
!Cb,!x:ta |- !e:!t
By induction, !Ca,!Cb |- [x<-ea]e:t
By rule, !Ca,!Cb |- !([x<-ea]e):!t
!([x<-ea]e) = [x<-ea](!e)

OTHER CASES SIMILAR


LEMMA[expression linear substitution]
If |- Ca,Cb and Ca |- ea:ta then
(1) If Cb,x:ta |- eb:tb
    then Ca,Cb |- [x<-ea]eb:tb
(2) If Cb,x:ta |- cb:tb
    then Ca,Cb |- [x<-ea]cb:tb
(3) If Cb,x:ta |- blk
    then Ca,Cb |- [x<-ea]blk
(4) If Cb,x:ta |- prog and Ca=D;U;R;G;{};L
    then Ca,Cb |- [x<-ea]prog
Proof by induction on typing derivations for eb,cb,blk,n->b,prog.

CASE
!Cb,x:ta |- x:ta
Ca |- [x<-ea]x:ta
By weakening, !Cb,Ca |- [x<-ea]x:ta

CASE
!Cb,!x:ta |- e:t
------------------
!Cb,!x:ta |- !e:!t
Case does not apply, because !x:ta does not match assumption x:ta.

OTHER CASES SIMILAR


LEMMA[pattern substitution]

If |- Ca,Cb
and |- pat:ta => D;G
and Ca |- ea:ta
and pat<-ea => [s]
then
(1) If Cb D;G |- eb:tb
    and Ca,Cb |- tb:type
    then Ca,Cb |- [s]eb:tb
(2) If Cb D;G |- cb:tb
    and Ca,Cb |- tb:type
    then Ca,Cb |- [s]cb:tb
(3) If Cb D;G |- blk
    then Ca,Cb |- [s]blk
(4) If Cb D;G |- n->b:tb
    and Ca,Cb |- tb:type
    then Ca,Cb |- n->[s]b:tb
(5) If Cb D;G |- prog and Ca=D;U;R;G;{};L
    then Ca,Cb |- [s]prog


By induction on pat.  Only eb cases are shown below.

CASE
pat = x
|- x:ta => {};{x:ta}
x<-ea => [x<-ea]

|- Ca,Cb
Ca |- ea:ta
Cb,x:ta |- eb:tb
By lemma[expression linear substitution], Ca,Cb |- [x<-ea]eb:tb


CASE
pat = !x
|- !x:!ta => {};{!x:ta}
!x<-!ea => [x<-ea]

Ca |- !ea:!ta
By typing inversion and type equivalence inversion:
!Ca' |- ea:ta' where !C |- ta=ta'
---------------
!Ca' |- !ea:!ta
Thus Ca=!Ca' and !Ca' |- ea:ta.

|- !Ca',Cb
!Ca' |- ea:ta
Cb,!x:ta |- eb:tb
By lemma[expression nonlinear substitution], Ca,Cb |- [x<-ea]eb:tb


CASE
pat = A,pat1
Alpha-rename so that A does not appear in Ca,Cb.

|- pat1:t' => D;G
---------------------------------
|- A,pat1:exists A:k.t' => D,A:k;G

pat1<-e1 => [s]
------------------------------------
A,pat1<-pack t,e1 as exists A:k.t'' => [A<-t][s]

Ca |- pack t,e1 as exists A:k.t'' : exists A:k.t'
By typing inversion:
  Ca |- t:k
  Ca |- e1:[A<-t]t''
  ---------------------------------
  Ca |- pack t,e1 as exists A:k.t'' : exists A:k.t''
where Ca |- exists A:k.t' = exists A:k.t''
By type equivalence inversion, Ca |- t' = t''
By type equivalence substitution, Ca |- [A<-t]t' = [A<-t]t''
So Ca |- e1:[A<-t]t'

|- pat1:t' => D;G implies |- pat1:[A<-t]t' => D;[A<-t]G (easy induction)

We know Cb D,A:k;G |- eb:tb.
Substitution implies Cb D;[A<-t]G |- [A<-t]eb:[A<-t]tb.
Since Ca,Cb |- tb:type and A does not appear in Ca,Cb, A does
not appear free in tb and [A<-t]tb = tb.

Therefore we know:
      |- Ca,Cb
  and |- pat1:[A<-t]t' => D;[A<-t]G
  and Ca |- e1:[A<-t]t'
  and Cb D;[A<-t]G |- [A<-t]eb:tb
  and Ca,Cb |- tb:type
  and pat1<-e1 => [s]
so by induction:
  then Ca,Cb |- [s][A<-t]eb:tb


CASE
pat = pat1,pat2

|- pat1:t1 => D1;G1
|- pat2:t2 => D2;G2
---------------------------------
|- pat1,pat2:t1*t2 => D1 D2;G1 G2

pat1<-e1 => [s1]
pat2<-e2 => [s2]
---------------------------
pat1,pat2<-e1,e2 => [s1][s2]

ta = t1*t2
ea = e1,e2

By typing inversion, type equivalence inversion:
  C1 |- e1:t1' where C1,C2 |- t1=t1'
  C2 |- e2:t2' where C1,C2 |- t2=t2'
  --------------------
  C1,C2 |- e1,e2:t1*t2
Thus C1 |- e1:t1 and C2 |- e2:t2 and Ca=C1,C2.
Cb D;G = Cb D1 D2;G1 G2 = (Cb D2;G2) D1;G1
By induction, C2,Cb D2;G2 |- [s1]eb:tb
By induction, C1,C2,Cb |- [s2][s1]eb:tb

OTHER CASES SIMILAR


THEOREM[preservation]
(1) If |- C and C |- e:t and e --> e'
    then C |- e':t

CASE
!C |- e:t
-----------
!C |- !e:!t
  where
e-->e'
--------
!e-->!e'

By induction, !C |- e':t
By rule, !C |- !e':!t

CASE
C |- e:t
C |- t = t'
-----------
C |- e:t'
where e-->e'
By induction, C |- e':t
By rule, C |- e':t'

CASE
C1 |- ef:ta -o tb
C2 |- ea:ta
-----------------
C1,C2 |- ef ea:tb
  where
ea --> ea'
----------------
ef ea --> ef ea'
C2 = D;U2;R;G2;P;L2
U=U1,U2
G=G1,G2
L=L1,L2
|- C2
By induction, C2 |- ea':ta
By rule, C1,C2 |- ef ea':tb

CASE
C1 |- ef:ta -o tb
C2 |- ea:ta
-----------------
C1,C2 |- ef ea:tb
  where ef=(\pat:ta'.eb) and
pat<-ea => [s]
--------------------------
(\pat:ta'.eb) ea --> [s]eb

By typing inversion and type equality inversion:
|- pat:ta' => D;G
C1 D;G |- e:tb'
C1 |- tb':type
------------------------------
C1 |- (\pat:ta'.eb):ta' -o tb' where C1 |- ta=ta' and C1 |- tb=tb'
By rule,  C2 |- ea:ta'
So we know:
      |- C1,C2
  and |- pat:ta' => D;G
  and C2 |- ea:ta'
  and C1 D;G |- e:tb'
  and C1,C2 |- tb':type
  and pat<-ea => [s]
By pattern substitution, C1,C2 |- [s]e:tb'
By rule, C1,C2 |- [s]e:tb

OTHER CASES SIMILAR

THEOREM[preservation]
(2) If C = D;Up;R;G;P;L and |- C,Us and C |- e:t
    and Us,Up;R;e --> U';R';e'
    then |- C',Us and C' |- e':t
    where C' = D;Up';R';G;P;L and U'=Us,Up' and R' = R R'' for some R'' and Up'

CASE
C |- e:t
C |- t = t'
-----------
C |- e:t'
where Us,Up;R;e --> U';R';e'
By induction, |- C',Us and C' |- e':t 
    where C' = D;Up';R';G;P;L and U'=Us,Up' and R' = R R'' for some R'' and Up'
By weakening, R' |- t = t'
By rule, C' |- e':t'

CASE
Ca |- ea:%ta
Cf |- ef:ta -o tb
------------------------
Ca,Cf |- ea >>@ ef : %tb
  where
Us,Up;R;ea --> U';R';ea'
--------------------------------------
Us,Up;R;ea >>@ ef --> U';R';ea' >>@ ef
Ca = D;Upa;R;Ga;P;La
Cf = D;Upf;R;Gf;P;Lf
Up=Upa,Upf
G=Ga,Gb
L=La,Lb
Us,Up=(Us,Upf),Upa
|- Ca,(Us,Upf)
By induction, |- Ca',(Us,Upf) and Ca' |- ea':%ta
    where Ca' = D;Upa';R';Ga;P;La and U'=(Us,Upf),Upa' and R' = R R'' for some R'' and Upa'
Let Cf' = D;Upf;R';Gf;P;Lf
By weakening, Cf' |- ef:ta -o tb
U'=Us,(Upa',Upf)
Let C' = Ca',Cf' = D;Upa',Upf;R';Ga,Gf;P;La,Lf
|- C',Us
By rule, C' |- ea' >>@ ef : %tb

CASE
Ca |- %ea:%ta
Cf |- vf:ta -o tb
-------------------------
Ca,Cf |- %ea >>@ vf : %tb
  where
(U;R; %ea >>@ vf) --> (U;R; %(vf ea))
C=Ca,Cf

By typing inversion and type equivalence inversion:
Ca |- ea:ta' where Ca |- ta=ta'
--------------
Ca |- %ea:%ta'
By rule, Ca |- ea:ta

Cf |- vf:ta -o tb
Ca |- ea:ta
-------------------
Ca,Cf |- vf ea : tb
-----------------------
Ca,Cf |- %(vf ea) : %tb

Let C'=C and R'=R and Up'=Up

CASE
!C |- delay k: %(exists A:k.Delay type(A))
  where
(U;R; delay k) --> (U,q_k;R; %pack q_k,fact as exists A:k.Delay type(A))  where q_k is fresh
!C=D;{};R;!G;P;{} and |- !C,Us
U=Us
Let C'=!C,q_k
|- C',Us

!C,q_k |- fact : Delay type(q_k)
!C,q_k |- q_k : k
------------------------------------------------------------------------------
!C,q_k |- pack q_k,fact as exists A:k.Delay type(A) : exists A:k.Delay type(A)
----------------------------------------------------------------------------------
!C,q_k |- %pack q_k,fact as exists A:k.Delay type(A) : %(exists A:k.Delay type(A))

CASE
C |- fact:Delay type(q_k)
C |- type(q_k):k
C |- t':k
----------------------------------------------------------------------------
C |- commit[type(q_k)=type(t')]e:%(!all F:k->type.F type(q_k) -o F type(t'))
  where
R |- t=type(q_k)
-----------------------------------------------------------------------------------
(U,q_k;R; commit[t=type(t')] fact) --> (U;R,q_k->t'; %!\F:k->type.\x:F type(q_k).x)
C = D;Up;R;G;P;L
U,q_k = Us,Up

By typing inversion:
  D;{q_k'};R;!G';P;{} |- fact:Delay type(q_k')
where Up={q_k'} and G=!G' and L={} and R |- Delay type(q_k) = Delay type(q_k')
By type equivalence inversion, R |- type(q_k) = type(q_k')
|- D;U,q_k;R;!G';P;{} implies q_k not in domain(R)
|- D;Us,q_k';R;!G';P;{} implies q_k' not in domain(R)
By type(q) equivalence inversion, q_k=q_k'.
Us = U

Let C'=D;{};R,q_k->t';!G';P;{}.
|- C',Us

C',F:k->type,x:F type(q_k) |- x : F type(q_k)
C' |- F type(q_k) = F type(t')
---------------------------------------------
C',F:k->type,x:F type(q_k) |- x : F type(t')
--------------------------------------------
C',F:k->type |- \x:F type(q_k).x : F type(q_k) -o F type(t')
---------------------------------------------------------------------------
C' |- \F:k->type.\x:F type(q_k).x : all F:k->type.F type(q_k) -o F type(t')
-----------------------------------------------------------------------------
C' |- !\F:k->type.\x:F type(q_k).x : !all F:k->type.F type(q_k) -o F type(t')
---------------------------------------------------------------------------------
C' |- %!\F:k->type.\x:F type(q_k).x : %(!all F:k->type.F type(q_k) -o F type(t'))

OTHER CASES SIMILAR

THEOREM[preservation]
(3) If C = D;Up;R;G;P;L and |- C,Us and C |- c:t
    and Us,Up;R;c --> U';R';c'
    then |- C',Us and C' |- c':t
    where C' = D;Up';R';G;P;L and U'=Us,Up' and R' = R R'' for some R'' and Up'
(note: case c=e handled by (2))

CASE
C |- c:%t
---------
C |- #c:t
  where
(U;R;c) --> (U';R';c')
------------------------
(U;R;#c) --> (U';R';#c')
By induction:
    then |- C' and C' |- c':%t
    where C' = D;Up';R';G;P;L and U'=Us,Up' and R' = R R'' for some R'' and Up'
By rule, C' |- #c':t

CASE
C |- %e:%t
-----------
C |- #%e:t
  where
(U;R;#%e) --> (U;R;e)
By typing inversion:
C |- e:t'
-----------
C |- %e:%t' where C |- %t=%t'
By type equivalence inversion, C |- t=t'
By rule, C |- e:t
Let C' = C


THEOREM[preservation]
(4) If C = D;Up;R;G;P;Lp and |- C,Us,Ls and C |- prog
    and Us,Up;R;Ls,Lp;prog --> U';R';L';prog'
    then |- C',Us,Ls and C' |- prog'
    where C' = D;Up';R';G;P;Lp' and U'=Us,Up' and L'=Ls,Lp' and R' = R R'' for some R'' and Up' and Lp'
(note: prog = B blk is covered by (6))

CASE
prog = (B [c]jmp m)

C1 |- c:(Code m t') * t'
------------------------
C1 |- [c]jmp m
!C1 |- n1->b1:t1' ... !C1 |- nn->bn:tn'
--------------------------------------------
D;Up;R;G;{};Lp |- B [c]jmp m

  where B = {n1->b1,...,nn->bn}
  where C1 = D;Up;R;G;{n1->t1',...,nn->tn');Lp
  where c = (code(n)[t1...tj],v) and U=Us,Up and L=Ls,Lp and:

pat<-v => [s]
------------------------------------------------------------------------
B |- U;R;L;[c]jmp m --> U;R;L;[s][Aj<-tj]...[A1<-t1]blk
-------------------------------------------------------------------------
(U;R;L;B [c]jmp m) --> U;R;L;B [s][Aj<-tj]...[A1<-t1]blk
  where bm = \A1:k1...\An:kj.\pat:t.blk

Let Up'=Up, Lp'=L, R'=R.

C1 |- (code(n)[t1...tj],v):(Code m t') * t'
By typing inversion and type equivalence inversion:
C1 |- v:t'
!C1 |- code(m)[t1...tj]:Code m [Aj<-tj]...[A1<-t1]t''
  where !C1 |- t1:k1 ... !C1 |- tj:kj
  and !C1 |- t' = [A1<-t1,...,An<-tj]t''
  and !C1 |- tm' = all A1:k1...all An:kn.Code n t''

!C1 |- m->\A1:k1...\An:kj.\pat:t.blk : tm'
By inversion:
!C1,A1:k1...An:kj |- m->\pat:t.blk : tm''
  where tm' = all A1:k1...all An:kj.tm''
By inversion:
|- pat:t => D1;G1
!C1,A1:k1...An:kj D1;G1 |- blk
where tm'' = Code m t
By substitution:
!C1 D1;[Aj<-tj]...[A1<-t1]G1 |- [Aj<-tj]...[A1<-t1]blk

tm' = all A1:k1...all An:kj.Code m t
!C1 |- tm' = all A1:k1...all An:kn.Code n t''
By type equivalence inversion, !C1 |- t = t''

!C1 |- t' = [Aj<-tj]...[A1<-t1]t''
By type equivalence substitution:
!C1 |- t' = [Aj<-tj]...[A1<-t1]t

|- pat:[Aj<-tj]...[A1<-t1]t => D1;[Aj<-tj]...[A1<-t1]G1
C1 |- v:[Aj<-tj]...[A1<-t1]t
pat<-v => [s]
!C1 D1;[Aj<-tj]...[A1<-t1]G1 |- [Aj<-tj]...[A1<-t1]blk
By pattern substitution:
C1 |- [s][Aj<-tj]...[A1<-t1]blk

D;Up;R;G;{};Lp |- B [s][Aj<-tj]...[A1<-t1]blk


CASE
prog = (B let pat = [c|e]add r1<-r2+m in blk)

Cr |- fact:Reg r1 t1
Ca,Cr |-* fact:Reg r2 t2
-------------------------------------------------------
(Ca,Cr);(Cr) |- [fact|fact]add r1<-r2+m : Reg r1 (t2+m)
-------------------------------------------------------
|- pat:Reg r1 (t2+m) => D;G
Ca D;G |- blk
----------------------------------------------
C1 |- let pat = [fact|fact]add r1<-r2+m in blk
!C1 |- n1->b1:t1 ... !C1 |- nn->bn:tn
------------------------------------------------------------------------------
D;Up;R;G;{};Lp |- {n1->b1,...,nn->bn} let pat = [fact|fact]add r1<-r2+m in blk

  where C1 = D;Up;R;G;{n1->t1,...,nn->tn);Lp
  and C1 = Ca,Cr
  and:

Us,Up;R;Ls,Lp;[fact|fact]add r1<-r2+m --> Us,Up;R;L0,r1->L(r2)+m;fact
------------------------------------------------------------------------------------------------------------
B |- Us,Up;R;Ls,Lp;let pat = [fact|fact]add r1<-r2+m in blk --> Us,Up;R;L0,r1->L(r2)+m;let pat = fact in blk
---------------------------------------------------------------------------------------------------------------
(Us,Up;R;Ls,Lp;B let pat = [fact|fact]add r1<-r2+m in blk) --> (Us,Up;R;L0,r1->L(r2)+m;B let pat = fact in blk)
  where L = L0,r1->m0 and L = Ls,Lp

By typing inversion and type equivalence inversion:
!_Cr,r1->m1 |- fact:Reg r1 t1 where R |- t1=m1 and Cr=!_Cr,r1->m1
_Car,r2->m2 |- fact:Reg r2 t2 where R |- t2=m2 and Ca,Cr=_Car,r2->m2
Lp(r1) = m1
Lp(r2) = m2
L0 = Ls,Lp0

Let Lp' = Lp0,r1->L(r2)+m and Up'=Up and R'=R
|- C',Us,Ls
Lp'(r1) = L(r2)+m = Lp(r2)+m = m2+m
Let Cr'=!_Cr,r1->m2+m
Cr' |- fact:Reg r1 (m2+m)
Cr' |- fact:Reg r1 (t2+m)
C' |- B let pat = fact in blk


OTHER CASES SIMILAR

LEMMA[canonical forms]
If C |- v:t then:
(1) If C |- t=!t' then v = !v'
(2) If C |- t=ta -o tb then v = \pat:t'.e and C |- t'=ta
(3) If C |- t=t1*t2 then v = v1,v2
(4) If C |- t=all A:k.t1 then v = \A:k.e
(5) If C |- t=exists A:k.t1 then v = pack t',v' as t'' and C |- t''=exists A:k.t1
(6) If C |- t=%t' then v = %e
(7) If C |- t=Reg t1 t2 or C |- v:Mem t1 t2 or C |- v:Delay t1 then v = fact
(8) If C |- t=Code t1 t2 then v = code(n)[t1'...tn']

Proof by induction on C |- v:t

CASE
C |- v:t'
C |- t' = t
-----------
C |- v:t
By induction, (1)...(8) hold.
(note: this is the only induction case; all other C |- v:t are base cases)

CASE
C |- e:t''
------------
C |- %e:%t''
Only case (6) applies: C |- %t''=t=%t'
Type equivalence inversion rules out other cases.
For example, C |- %t''=t=!t' violates type equivalence inversion.
So v = %e.

OTHER CASES SIMILAR

THEOREM[progress]
(1) If C = {};U;R;{};P;L and |- C and C |- e:t and e is not a value
    and there is no t' such that C |- t = %t'
    then there is some e' such that e --> e'

CASE
C |- e:t''
C |- t'' = t
-----------
C |- e:t
There is no t' such that C |- t'' = %t'
(otherwise, C |- t = t'' = %t')
By induction, there is some e' such that e --> e'

CASE
C1 |- ef:ta -o tb
C2 |- ea:ta
-----------------
C1,C2 |- ef ea:tb
Suppose ef is not a value:
  By type equivalence inversion, there is no t' s.t. C |- ta -o tb = %t'
  By induction, ef-->ef', so ef ea-->ef' ea.
Otherwise, ef is a value.
By canonical forms, ef = \pat:t'.e.
(\pat:t'.e) ea steps.

CASES delay k | commit[t=type(t)] e | e >>@ e | e >>* e
These have type %t'; (1) does not apply.
(See (2) instead.)

OTHER CASES SIMILAR

THEOREM[progress]
(2) If C = {};Up;R;{};P;L and |- C,Us and C |- e:t and e is not a value
    then there is some Up';R';e' such that Us,Up;R;e --> Us,Up';R';e'

CASE
C1 |- ef:ta -o tb
C2 |- ea:ta
-----------------
C1,C2 |- ef ea:tb
By (1), ef ea --> e'
By rule, Us,Up;R;ef ea --> Us,Up;R;e'

CASE
!C |- delay k: %(exists A:k.Delay type(A))
(Us,Up;R; delay k) --> (Us,(Up,q_k);R; %pack q_k,fact as exists A:k.Delay type(A))  where q_k is fresh

CASE
C |- e:Delay t
C |- t:k
C |- t':k
------------------------------------------------------------
C |- commit[t=type(t')]e:%(!all F:k->type.F t -o F type(t'))
Suppose e is not a value:
  By induction, U;R;e --> U';R';e',
  so U;R;commit[t=type(t')]e --> U';R';commit[t=type(t')]e'
Otherwise, e is a value.
By canonical forms, e = fact.
By typing inversion:
D;{q_k};R;!G;P;{} |- fact:Delay type(q_k)
where C = D;{q_k};R;!G;P;{} and R |- Delay t = Delay type(q_k).
By type equivalence inversion, R |- t = type(q_k).
Up = {q_k}.
Let Up' = {}.

R |- t=type(q_k)
-----------------------------------------------------------------------------------
(Us,q_k;R; commit[t=type(t')] fact) --> (Us;R,q_k->t'; %!\F:k->type.\x:F type(q_k).x)

CASE
C1 |- e1:%ta
C2 |- e2:ta -o tb
------------------------
C1,C2 |- e1 >>@ e2 : %tb
Suppose e1 is not a value:
  By induction, U;R;e1 --> U';R';e1', so U;R;e1>>@e2 --> U';R';e1'>>@e2
Otherwise, suppose e2 is not a value:
  By induction, U;R;e2 --> U';R';e2', so U;R;e1>>@e2 --> U';R';e1>>@e2'
Otherwise, e1 and e2 are values.
By canonical forms, e1=%ea.
(U;R; %ea >>@ e2) --> (U;R; %(e2 ea))
  (where e2 is a value)

OTHER CASES SIMILAR

THEOREM[progress]
(3) If C = {};Up;R;{};P;L and |- C,Us and C |- c:t and c is not a value
    then there is some Up';R';c' such that Us,Up;R;c --> Us,Up';R';c'
(note: c = e is handled by (2))

CASE
C |- c:%t
---------
C |- #c:t
Suppose c is not a value:
  By induction, U;R;c --> U';R';c', so U;R;#c --> U';R';#c'
Otherwise, c is a value.
By canonical forms, c = %e.
(U;R;#%e) --> (U;R;e)

THEOREM[progress]
(4) If C = {};Up;R;{};P;Lp and |- C,Us,Ls and C |- prog
    then there is some U';R';L';prog' such that Us,Up;R;Ls,Lp;prog --> Us,Up';R';Ls,Lp';prog'

CASE
prog = B [c]jmp m

C1 |- c:(Code m t) * t
----------------------
C1 |- [c]jmp m
!C1 |- n1->b1:t1 ... !C1 |- nn->bn:tn
-------------------------------------
D;U;R;G;{};L |- B [c]jmp m
  where C1 = D;U;R;G;{n1->t1,...,nn->tn);L
  and B = {n1->b1,...,nn->bn}
If c is not a value:
  By (3), c steps, so [c]jmp n steps by congruence.
Otherwise, c is a value.
By canonical forms, c = (code(m)[t1...tj],v) where:
  D |- t1:k1 ... D |- tj:kj
  tm = all A1:k1...all Aj:kj.Code m t'
  t = [Aj<-tj]...[A1<-t1]t'
By inversion on !C1 |- m->bm:tm :
  !C1,A1:k1,...,Aj:kj |- m->bm':Code m t'
  where bm = \A1:k1...\Aj:kj.bm'
  bm' = \pat:t'.blk

pat<-v => [s]
------------------------------------------------------------------------
B |- U;R;L;[code(n)[t1...tj],v]jmp n --> U;R;L;[s][Aj<-tj]...[A1<-t1]blk
  where bm=\A1:k1...\An:kj.\pat:t'.blk

OTHER CASES SIMILAR