=========================================================================================================================
=========================================================================================================================

is Lemma:
---------

If  X |- (D;G) good   and   X |- is good
then  (D;P;G) |- is : G'  and  X |- (D,G') good

Proof by induction on the structure of is:

empty case - G' = G

mov/sub cases - both rk and rk' updated equivalently, new G' reflects these changes




=========================================================================================================================
=========================================================================================================================

Block Addition Lemma:
----------------------

If  X;GenPsi(L,l) |- C : GenPsi(C)  and  [[X]]_l = All[D]((G,ri-><R,check,Y>),alpha o n))  
and  D; (P1 union P2); (G,ri-><R,check,Y>); alpha o n; Y; P(n+1) |- b
then X;GenPsi(L) |- C[l -> b] : GenPsi(C,l)

Proof: 
------

By inversion and reconstruction of (trans-C-t).



=========================================================================================================================
=========================================================================================================================

Block Construction Lemma:
--------------------------

If X |- (L,C,is,l) ok  
then Forall l' in (L,l) or Dom(C).
(1) GenPsi(X,L) |- C[l -> check l; is; intendjmp l'] : GenPsi(X,(Dom(C),l))
(2) if l+1 in (L,l) or Dom(C). GenPsi(X,L) |- C[l -> check l; is; intendbrz rz l'] : GenPsi(X,(Dom(C),l))


Proof:
------


Definitions:

dP1. P1 = GenPsi(L,l)							
dP2. P2 = GenPsi(Dom(C))
dP3. P3 = P1 union P2

dD1. let D1 = D,Y:kint,alpha:kseq
dD2. let D2 = D,alpha:kseq

dto1. to = P3(l+1)    

dG1. let G1 = G,ri-><R,check,Y>
dG2. let G2 = (G,ri-><R,check,Y>)[tg-><R,int,l>]
dG3. let G3 = (G,ri-><R,check,Y>)[tg-><R,int,l-Y>]
dG4. let G4 = (G,ri-><B,ok,l>)[tg-><R,int,0>]
dG5 = #15
dG6. G5[ tb -> <B,P(l'),l'> ][ tg-> <G,P(l'),l'> ][ ri -> <B,go,l'> ]
dG7 = G5[ tb -> <B,P3(l'),l'> ][ tb -> <B,P3(l+1),l+1> ][ tg -> <G,P3(l'),l'> ][ ri -> <B,goz,Ez'?l+1:l'> ]

dSt. St = E61/a1l',...,E6n/anl',  E6tg/atgl', E6tb/atbl', E6ri/aril', (alpha o l)/ahistl'


1. X;P1 |- C : P2								[ Inversion of (partial-trans-ok), a1, dP1, dP2 ]
2. <deleted>						
3. X |- is good

5. P1(l) = [[X]]_l								[ Inversion of (trans-C-t), 1, dP1 ]
6. P1(l) = All[D1]((G,ri-><R,check,Y>),alpha o l)				[ Inspection of ([[X]]), 6 ]										
7. D |- G ok  
8. Forall r' in Dom(G). G(r') =/= <R,t',E'>
9. D |- P(l+1) ok 
10. Forall k = 1 to n. G(rk) = <G,int,Ek> 					
    and G(rk') = <B,int,Ek'> and D |- Ek = Ek'

11. D2 |- G4									[ dD2, dG4, 7 ]
12. Forall k = 1 to n. G4(rk) = <G,int,Ek> 					[ dG4, 10 ]		
    and G4(rk') = <B,int,Ek'> and D |- Ek = Ek'
13. G4(ri) = <B,ok,l>								[ dG4 ]
14. X |- (D2,G4) ok								[ (GD-good), 5, 11, 12, 13 ]

15. (D2;P3;G4) |- is : G5							[ is Lemma, 14, 3 ]
16. X |- (D2,G5) good

17. D2 |- G5									[ Inversion of (GD-good), 16 ]
18. Forall xk in X. G(rk) = <G,int,Ek> and G(rk') = <B,int,Ek'> and D |-Ek=Ek'	
19. G5(ri) = <c,ok,Ei>

dl'. let l' be a label in L

26. D2 |- S : Dl'								[ dSt, 22, 25 ]
27. D2 |- G6[ ri -> <R,check,Et'>] <= St(Gl')					[ (G-subtp), (subtp-reflex), (subtp-int), dG6, 24, dSt ]

28. G5(rz) = <G,int,Ez>  and G5(rz') = <G,int,Ez'>  and D2 |- Ez = Ez'		[ 18 ]

dl1. assume l+1 in L
29. Deconstruct structure of P3(l+1) and build Sf as in 20 - 27 for l'		[ dl', 20 - 27, all code blocks have same type ]







							G7(ri) = <B,goz,Ez'?l+1:l'>			[ dG7 ]
							D2 |- l+1 = l + 1				[ ]
							G7(rz) = <G,int,Ez>				[ dG7, 28 ]
							D2 |- Ez = Ez'					[ dG7, 28 ]
							G7(rt) = <G,All[Dl'](Gl',Al'),l'>		[ dG7, 21 ]
							D2 |- l' = l'					[ ]
							D2 |- St : Dl'					[ 26 ]
							D2 |- G6[ ri -> <R,check,Et'>] <= St(Gl')	[ 27 ]
							D2 |- alpha o l o l' = S(Al')			[ 23, dS ]
							D2 |- Sf : Dl1					[ 29 ]
							D2 |- G6[ ri -> <R,check,Et'>] <= St(Gl1)	[ 29 ]
							D2 |- alpha o l o (l+1) = S(Al1)		[ 29 ]
							--------------------------------------------------------------------- (brz-t)
D2;P3;G5;alphaol;l;to |- movi...intendz : G7		D2;P3;G7;alphaol;l;to |- brz rz tg
---------------------------------------------------------------------------------------------------------------------------------------------------
D2;P3;G5;alphaol;l;to |- movi tb B l+1; intend tb; movi tb B (l+1); intend tb; movi tg G l'; intendz rz' tb; brz rz tg
--------------------------------------------------------------------------------------------------------------------------------------------------- [macro expansion ]
D2;P3;G5;alphaol;l;to |- intendzbrz rz l l'

30. if l+1 in L.      D2;P3;G5;alphaol;l;to |- intendzbrz rz l l'







									G6(ri) = <B,go,l'>				[ dG6 ]
									G6(rt) = <G,P(l'),l'>				[ dG6 ]
									D2 |- l' = l'					[ ]
									D2 |- St : Dl'					[ 26 ]
									D2 |- G6[ ri -> <R,check,Et'>] <= St(Gl')	[ 27 ]
[ (mov-t), (sequence-t), (intend-t), (sequence-t), (mov-t), 19 ]        D2 |- alpha o l o l' = S(Al')			[ 23, dS ]
-----------------------------------------------------------------    	--------------------------------------------------------------------------- (jmp-t)
D2;P3;G5;alphaol;l;to |- mov tb B l'; intend tb; mov tg G l';  G6    	D2;P3;G6;alphaol;l;to |- jmp tg
--------------------------------------------------------------------------------------------------------------------------------------------------- (sequence-t)
D2;P3;G5;alphaol;l;to |- mov tb B l'; intend tb; mov tg G l';  jmp tg
--------------------------------------------------------------------------------------------------------------------------------------------------- [macro expansion ]
D2;P3;G5;alphaol;l;to |- intendjmp l'

31. D2;P3;G5;alphaol;l;to |- intendjmp l'





32. let bend be either intendjmp l' or intendzbrz rz l l'
33. D2;P3;G5;alphaol;l;to |- bend						[ 30, 31, 32 ]
34. D2;P;G4;alphaol;l;to |- is;bend						[ (sequence-t), 15, 33 ]






								                           G3(tg) = <R,int,l-Y>			[ dG3 ]
								                           G3(ri) = <R,int,Y>			[ dG3 ]
								                           D2 |- G3/ri/rz ok			[ 7, dG3, dD2]
								                           D2 |- alpha				[ dD2 ]
								                           D2 |- l				[ dD2 ]
								                           D2;P;G4;alphaol;l;to |- is;bend	[ 34 ]
				      ------------------------------------------(sub-t)    ------------------------------------------------------------- (recovernz-t)
tg =/= ri			      D1;P3;G2;alphaol;Y;to |- sub tg tg ri : G3           D3,Y;kint;P;G3;alphaol;Y;to |- recovernz tg;is;bend 
---------------------------(movi-t)   ---------------------------------------------------------------------------------------------------------------- (sequence-t) 
D1;P3;G1 |- movi tg R l : G2          D1;P3;G2;alphaol;Y;to |- sub tg tg ri; recovernz tg; is; bend 
------------------------------------------------------------------------------------------------------------------------------------------------------ (sequence-t)
D1;P3;G1;alphaol;Y;to |- movi tg R l; sub tg tg ri; recovernz tg; is; bend 
------------------------------------------------------------------------------------------------------------------------------------------------------ [macro expansion]
D1;P3;G1;alphaol;Y;to |- check l ;is;bend 

35. D1;P3;G1;alphaol;Y;to |- check l; is; intendjmp l'		
36. if l+1 in L. D1;P3;G1;alphaol;Y;to |- check l; is; intendzbrz rz l l'	

37. P3 = (P1/l) union (P2[l -> [[X]]_l ])						[ dP3 ]

38. X;(P1/l) |- C[l -> check l; is; intendjmp l'] : P2[l -> [[X]]_l ]			[ (partial-trans-ok), 1, 37, 35 ]
39. if l+1 in L										[ (partial-trans-ok), 1, 37, 36 ]
    X;(P1/l) |- C[l -> check l; is; intendbrz rz l'] : P2[l -> [[X]]_l ]
    
40. X;GenPsi(X,L) |- C[l -> check l; is; intendjmp l'] : GenPsi(X,(Dom(C),l))	[ 38, dP1, dP2 ]
41. if l+1 in L. 									[ 39, dP1, dP2 ]
    X;GenPsi(X,L) |- C[l -> check l; is; intendbrz rz l'] : GenPsi(X,(Dom(C),l))

* Block Construction Lemma Complete





=========================================================================================================================
=========================================================================================================================


Partial Trans Lemma
---------------------

If [[X |- s]] (L,C,is,l) = (L',C',is',l')   and  X |- (L,C,is,l) good
then X |- (L',C',is',l') good  and  L = L'


Proof:  By induction on the structure of [[X |- s]] (L,C,is,l) = (L',C',is',l')
------

a2. X |- (L,C,is,l) good



CASE TRANS-ASSIGN:
~~~~~~~~~~~~~~~~~~

is' = is; movi rk G v; movi rk' B v
----------------------------------------------------------------- (trans-assign)
[[X |- xk := v ]] (L,C,is,l) = (L,C,is',l)

d1. P1 = GenPsi(L,l)								[ Inversion of (partial-trans-ok), a2 ]
d2. P2 = GenPsi(Dom(C))
1. X; P1 |- C : P2
2. X |- is good

10. xk in X									[ Inversion of (wf-assign), a1 ]
2'. X |- is; movi rk G v; movi rk' B v good					[ (is-movi-good), 2, 10 ]

12. X |- (L,C,is',l) good							[ (partial-trans-ok), d1, d2, 1, 2' ]
13. L = L
* TRANS-ASSIGN complete




CASE TRANS-SUB:
~~~~~~~~~~~~~~~~~~

is' = is; sub rk rm rn; sub rk' rm' rn'
----------------------------------------------------------------- (trans-sub)
[[X |- xk := xm - xn ]] (L,C,is,l) = (L,C,is',l)

d1. P1 = GenPsi(L,l)								[ Inversion of (partial-trans-ok), a2 ]
d2. P2 = GenPsi(Dom(C))
1. X; P1 |- C : P2
2. X |- is good

10. xk in X  and xm in X  and Xn in X						[ Inversion of (wf-assign), a1 ]
2'. X |- is; sub rk rm rn; sub rk' rm' rn' good					[ (is-sub-good), 2, 10 ]

12. X |- (L,C,is',l) good							[ (partial-trans-ok), d1, d2, 1, 2' ]
13. L = L
* TRANS-SUB complete



CASE TRANS-IF:
~~~~~~~~~~~~~~~~~~

p1. let lf = l+1									// fallthrough (false) label
p2. let lt = lf + Blks(s1)								// target (true) label
p3. let lj = lt + Blks(s2)								// join label
p4. let bl = (check l); is; intendzbrz rk lf lt
p5. [[X |- s1]] ( (L,lf), C[l -> bl], ., lt ) = (Lt', Ct', ist', lt')
p6. [[X |- s2]] ( (L,lt), C[l -> bl], ., lf ) = (Lf', Cf', isf', lf')
p7. let C' = (Ct' union Cf')[ lt' -> check lt'; ist'; intendjmp lj ][ lf' -> check lf'; isf'; intendjmp lj ]
------------------------------------------------------------------------------------------ (trans-if)
[[X |- if xk = 0 then s1 else s2 ]] ( L, C, is, l ) = (L,C',.,lj)



d1. P1 = GenPsi(L,l)								[ Inversion of (partial-trans-ok), a2 ]
d2. P2 = GenPsi(Dom(C))
1. X; P1 |- C : P2
2. X |- is good

3. X |- ( (L,lt,lf), C, is, l ) good						[ Weakening on L, a2 ]
4. X; GenPsi(X,(L,lf,lt)) |- C[ l -> bl ] : GenPsi(X,(C,l))			[ Block Construction Lemma, 3, p4 ]			
5. X |- . good									[ is-empty-good ]
6. X |- ( (L,lf), C[l -> bl], ., lt ) good					[ (partial-trans-ok), 4, 5 ]
7. X |- ( (L,lt), C[l -> bl], ., lf ) good					[ (partial-trans-ok), 4, 5 ]
8. X |- ((L,lf), Ct', ist', lt') good and {Dom(C),l,lt} subseteq {Dom(Ct'),lt'} [ I.H., p5, 6 ]
9. X |- ((L,lt), Cf', isf', lf') good and {Dom(C),l,lf} subseteq {Dom(Cf'),lf'} [ I.H., p6, 7 ]

10. X; GenPsi(L,lf,lt') |- Ct' : GenPsi(Ct')					[ Inversion of (partial-trans-ok), 8 ]
11. X |- ist' good
12. X; GenPsi(L,lt,lf') |- Cf' : GenPsi(Cf')					[ Inversion of (partial-trans-ok), 9 ]
13. X |- isf' good

14. {Dom(C),l,lt,lf} subseteq {Dom(Cf'),Dom(Ct'),lt',lf'}			[ 8, 9 ]
15. X; GenPsi(L,lt',lf') |- (Ct' union Cf') : GenPsi(Ct' union Cf')		[ Block Addition Lemma, 10, 12, 14 ]
6. X; GenPsi(L,lt',lf',lj) |- (Ct' union Cf') : GenPsi(Ct' union Cf')		[ Weakening on L, 15 ]

17. X |- ( (L,lf',lj), (Ct' union Cf'), ist', lt') good				[ (partial-trans-ok), 16, 11 ]
18. X; GenPsi(L,lf',lj) |- 							[ Block Construction Lemma, 17 ]
   (Ct' union Cf')[lt' -> check lt'; ist'; intendjmp lj] : GenPsi(Ct' union Cf', lt')
   
19. X |- ((L,lj),(Ct'unionCf')[lt'->check lt';ist';intendjmp lj],isf',lf') good	[ (partial-trans-ok, 18, 13 ]
20. X; GenPsi(L,lj) |- C' : GenPsi(C')					[ Block Construction Lemma, 19, p7 ]

21. X |- (L,C',.,lj) good							[ (partial-trans-ok), 20, 5 ]
22. {Dom(C),l} subseteq {Dom(C'),lj}						[ 8, 9 ]
* TRANS-IF complete



CASE TRANS-WHILE:
~~~~~~~~~~~~~~~~~~

p1. let lb = l + 1									// beginning label
p2. let ls = lb + 1									// body (s) label
p3. let le = ls + Blks(s)								// end label
p4. let bl = check l; is; intendjmp lb
p5. let bb = (check lb); intendzbrz rk le ls
p6. [[X |- s]] ( (L,le), C[l -> bl][lb -> bb], ., ls ) = (Ls', Cs', iss', ls')
p7. let bs = check ls'; iss'; intendjmp lb
p8. let C' = Cs'[ ls' -> bs ]
------------------------------------------------------------------------------------------ (trans-while)
[[X |- while xk =/= 0 do s ]] ( L, C, is, l ) = (L, C', . le)


d1. P1 = GenPsi(L,l)								[ Inversion of (partial-trans-ok), a2 ]
d2. P2 = GenPsi(Dom(C))
1. X; P1 |- C : P2
2. X |- is good

3. X |- ( (L,lb), C, is, l ) good						[ Weakening on L, a2 ]
4. X; GenPsi(X,(L,lb)) |- C[ l -> bl ] : GenPsi(X,(C,l))			[ Block Construction Lemma, 3, p4 ]
5. X |- ( (L,le,ls), C[l -> bl], ., lb) good					[ (partial-trans-ok), 4, (is-empty-t), Weakening on L ]
6. X; GenPsi(X,(L,le,ls)) |- C[l->bl][lb->bb] : GenPsi(X,(C,l,lb))		[ Block Construction Lemma, 5, p5 ]
7. X |- ( (L,le), C[l -> bl][lb -> bb], ., ls ) good				[ (partial-trans-ok), 6, (is-empty-t) ]
8. X |- ( (L,le), Cs', iss', ls') good   					[ I.H, 7, p6 ]
9. {Dom(C),l,lb,ls} subseteq {Dom(Cs'),ls'}

10. GenPsi(X,(L,le)) |- Cs'[ls' -> bs] : GenPsi(Cs',ls')			[ Block Construction Lemma, 8, p7 ]
11. X |- (L, C', ., le) good							[ (partial-trans-ok), 10, (is-empty-t), p8 ]
12. {Dom(C),l)} subseteq {Dom(C'),le}						[ 9 ]
* TRANS-WHILE Complete



CASE TRANS-SEQ:
~~~~~~~~~~~~~~~~~~

p1. [[X |- s1]] ( L, C, is, l ) = (L1', C1', is1', l1')
p2. [[X |- s2]] ( L1', C1', is1', l1') = (L', C', is', l')
------------------------------------------------------------------------------------------ (trans-seq)
[[X |- s1;s2 ]] ( L, C, is, l ) = (L', C', is', l')

1. X |- (L1', C1', is1', l1') good  and  {Dom(C),l} subseteq {Dom(C1'),l1'}	[ I.H., p1, a2 ]
2. X |- (L',C',is',l') good and {Dom(C1'),l1'} subseteq {Dom(C'),l'}		[ I.H., p2, 1 ]	
3. X |- (L',C',is',l')  and  {Dom(C),l} subseteq {Dom(C'),l'}			[ 1, 2 ]
* TRANS-SEQ complete

** Partial Trans Lemma Complete