THEOREM[preservation] If C = D;G;P;L and |- C and C |- prog and (L;prog) --> (L';prog') then |- C' and C' |- prog' where C' = D;G;P;L' Follows from: (1) If |- C and C |- e:t and e --> e' then C |- e':t (2) If C = D;G;P;L and |- C and C |- c:t and c --> c' then C |- c':t (3) If C = D;G;P;Lp and |- C,Ls and C |- prog and Ls,Lp;prog --> L';prog' then |- C',Ls and C' |- prog' where C' = D;G;P;Lp' and L'=Ls,Lp' for some Lp' Proof by induction on the typing derivation. See below. THEOREM[progress] If C = {};{};P;L and |- C and C |- prog then there is some L';prog' such that L;prog --> L';prog' Follows from: (1) If C = {};{};P;L and |- C and C |- e:t and e is not a value then there is some e' such that e --> e' (2) If C = {};{};P;L and |- C and C |- c:t and c is not a value then there is some c' such that c --> c' (3) If C = {};{};P;Lp and |- C,Ls and C |- prog then there is some L';prog' such that Ls,Lp;prog --> 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[expression weakening] If C = D;G;P;L and C'=D,A:k;G;P;L or C'=D;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';G;{};L and C |- prog then C' |- prog Proof by inductions on typing derivations. LEMMA[single-step type confluence] If |- ta => tb and |- ta => tc then there is a td s.t. |- tb=>td and |- tc => td Proof by induction on sum of sizes of derivations of |- ta => tb and |- ta => tc. Label the => rules as follows: |- t =1> t |- tj => tj' ... |- tk => tk' ------------------------------ |- T[t1...tk] =2> T[t1'...tk'] |- (\A:k.tb) ta =3> [A<-ta]tb |- rec t =4> %(t (rec t)) |- (%t1) t2 =5> %(t1 t2) For brevity, the cases below elide the "|- ". 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: rec ta' => rec tb' where ta' => tb' rec ta' => %(ta' (rec ta')) choose td = %(tb' (rec tb')) CASE 2,5: (%ta1) ta2 => (%tb1) tb2 where ta1=>tb1 and ta2=>tb2 (%ta1) ta2 => %(ta1 ta2) Choose td = %(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 |- tb = tc then there is a td s.t. |- tb =>* td and |- 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 |- S[t1...tn] => t' then t' = S[t1'...tn'] where |- t1=>t1' ... |- tn=>tn' and: S[t1] = !t1 | s(t1) | all A:k.t1 | exists A:k.t1 | \A:k.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 (elim t1 t2 t3) and (t1 t2) and (rec t), and includes %t1) Proof by cases of definition of => (no induction). For example: |- t1 => t1' -------------- |- %t1 => %t1' (no other derivation of %t1 => %t1' is possible) It's important to observe that these rules are not applicable to S[t1...tn]=>t': |- (\A:k.tb) ta => [A<-ta]tb |- elim 0 tz ts => tz |- elim s(tm) tz ts => ts tm (elim tm tz ts) |- rec t => %(t (rec t)) |- (%t1) t2 => %(t1 t2) For example, (rec t) does not match any S[t1] or S[t1,t2]. LEMMA[type equivalence inversion] If |- S[t1...tn] = S'[t1'...tm'] then S = S' and n=m and |- t1=t1' ... |- tn=tn' Proof: By lemma[type confluence], then there is some t'' such that |- S[t1...tn] =>* t'' and |- S'[t1'...tm'] =>* t'' By induction on number of => steps and single-step type equivalence inversion lemma: - If t = S[t1...tn] and |- t =>* t'' then t'' = S[t1''...tn''] where |- t1 =>* t1'' ... |- tn =>* tn'' - If t' = S'[t1'...tm'] and |- t' =>* t'' then t'' = S'[t1''...tm''] where |- t1' =>* t1'' ... |- tm' =>* tm'' So S=S' and m=n. From |- tk =>* tk'' conclude |- tk = tk'' (repeated transitivity) From |- tk' =>* tk'' conclude |- tk' = tk'' (repeated transitivity) Thus conclude |- tk = tk' (symmetry, transitivity). LEMMA[type equivalence kinds] If C = D;G;P;L and |- C and |- t1=t2 then (D |- t1:k if and only if D |- t2:k) Proof by induction on |- t1=t2. Sample case: |- rec t = %(t (rec t)) Consider "D |- t1:k implies D |- t2:k" Only one possible kinding derivation for rec t: D |- t:k->k ------------ D |- rec t:k Given t:k->k, conclude: D |- t:k->k ------------ D |- t:k->k D |- rec t:k ----------------------------- D |- t (rec t):k -------------------------- D |- %(t (rec t)):k The "D |- t2:k implies D |- t1:k" direction is similar. LEMMA[environment typing / expression kinds] (1) If C = D;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 |- t1=t2 then |- [A<-t']t1=[A<-t']t2 Proof by induction on |- t1=t2. LEMMA[expression type substitution] If C = D;G;P;L and |- C and C |- ta:ka then (1) If C,A:ka |- eb:tb then D;[A<-ta]G;P;L |- [A<-ta]eb:[A<-ta]tb (2) If C,A:ka |- cb:tb then D;[A<-ta]G;P;L |- [A<-ta]cb:[A<-ta]tb (3) If C,A:ka |- blk then D;[A<-ta]G;P;L |- [A<-ta]blk (4) If C,A:ka |- n->b:tb then D;[A<-ta]G;P;L |- n->[A<-ta]b:[A<-ta]tb (5) If C,A:ka |- prog then D;[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;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;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;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;G2;P;L2 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 |- ta' -o 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 |- ta' -o tb':type (which implies C1,C2 |- tb':type) and pat<-ea => [s] By pattern substitution, C1,C2 |- [s]e:tb' By rule, C1,C2 |- [s]e:tb CASE Cf |- ef:%(ta -o tb) Ca |- ea:%ta ------------------------ Cf,Ca |- ef %<< ea : %tb where ea --> ea' ------------------------ ef %<< ea --> ef %<< ea' Cf = D;Gf;P;Lf Ca = D;Ga;P;La G=Ga,Gb L=La,Lb |- Ca By induction, and Ca |- ea':%ta By rule, C |- ef %<< ea' : %tb CASE Cf |- %ef:%(ta -o tb) Ca |- %ea:%ta ------------------------- Cf,Ca |- %ef %<< %ea : %tb where %ef %<< %ea --> %(ef ea) C=Cf,Ca By typing inversion and type equivalence inversion: Ca |- ea:ta' where Ca |- ta=ta' -------------- Ca |- %ea:%ta' By rule, Ca |- ea:ta By typing inversion and type equivalence inversion: Cf |- ef:tab' where Cf |- %(ta -o tb)=tab' -------------- Cf |- %ef:%tab' By rule, Ca |- ef:ta -o tb Cf |- ef:ta -o tb Ca |- ea:ta ------------------- Ca,Cf |- ef ea : tb ----------------------- Ca,Cf |- %(ef ea) : %tb OTHER CASES SIMILAR THEOREM[preservation] (2) If C = D;G;P;L and |- C and C |- c:t and c --> c' then C |- c':t (note: case c=e handled by (1)) CASE C |- c:%t --------- C |- #c:t where c --> c' ---------- #c --> #c' By induction: C |- c':%t By rule, C |- #c':t CASE C |- %e:%t ----------- C |- #%e:t where #%e --> 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 THEOREM[preservation] (3) If C = D;G;P;Lp and |- C,Ls and C |- prog and Ls,Lp;prog --> L';prog' then |- C',Ls and C' |- prog' where C' = D;G;P;Lp' and L'=Ls,Lp' for some 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;G;{};Lp |- B [c]jmp m where B = {n1->b1,...,nn->bn} where C1 = D;G;{n1->t1',...,nn->tn');Lp where c = (code(n)[t1...tj],v) and L=Ls,Lp and: pat<-v => [s] ------------------------------------------------------------------------ B |- L;[c]jmp m --> L;[s][Aj<-tj]...[A1<-t1]blk ------------------------------------------------------------------------- (L;B [c]jmp m) --> L;B [s][Aj<-tj]...[A1<-t1]blk where bm = \A1:k1...\An:kj.\pat:t.blk Let Lp'=L. 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;G;{};Lp |- B [s][Aj<-tj]...[A1<-t1]blk CASE prog = (B let pat = [c1|c2]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;G;{};Lp |- {n1->b1,...,nn->bn} let pat = [fact|fact]add r1<-r2+m in blk where C1 = D;G;{n1->t1,...,nn->tn);Lp and C1 = Ca,Cr and: Ls,Lp;[fact|fact]add r1<-r2+m --> L0,r1->L(r2)+m;fact ------------------------------------------------------------------------------------------------------------ B |- Ls,Lp;let pat = [fact|fact]add r1<-r2+m in blk --> L0,r1->L(r2)+m;let pat = fact in blk --------------------------------------------------------------------------------------------------------------- (Ls,Lp;B let pat = [fact|fact]add r1<-r2+m in blk) --> (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 |- t1=m1 and Cr=!_Cr,r1->m1 _Car,r2->m2 |- fact:Reg r2 t2 where |- t2=m2 and Ca,Cr=_Car,r2->m2 Lp(r1) = m1 Lp(r2) = m2 L0 = Ls,Lp0 Let Lp' = Lp0,r1->L(r2)+m |- C',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 |- t=Mem t1 t2 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 = {};{};P;L and |- C and C |- e:t and e is not a value then there is some e' such that e --> e' CASE C |- e:t'' C |- t'' = t ----------- C |- e: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 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. CASE C1 |- e1:%(ta -o tb) C2 |- e2:%ta ------------------------ C1,C2 |- e1 %<< e2 : %tb Suppose e1 is not a value: By induction, e1 --> e1', so e1%< e1'%< e2', so e1%< e1%< %(ef ea) OTHER CASES SIMILAR THEOREM[progress] (2) If C = {};{};P;L and |- C and C |- c:t and c is not a value then there is some c' such that c --> c' (note: c = e is handled by (2)) CASE C |- c:%t --------- C |- #c:t Suppose c is not a value: By induction, c --> c', so #c --> #c' Otherwise, c is a value. By canonical forms, c = %e. #%e --> e THEOREM[progress] (3) If C = {};{};P;Lp and |- C,Ls and C |- prog then there is some L';prog' such that Ls,Lp;prog --> 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;G;{};L |- B [c]jmp m where C1 = D;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 |- L;[code(n)[t1...tj],v]jmp n --> L;[s][Aj<-tj]...[A1<-t1]blk where bm=\A1:k1...\An:kj.\pat:t'.blk OTHER CASES SIMILAR