Translation Theorem
-------------------
 
If   X |- s  and  [[X |- s]] (.,.,.,1) = (.,C',is',l')   
and InitRegFile(X) = R
then |- (C'[l'-> check l'; is'; intendjmp lh][lh -> check lh; intendjmp lh],0,R,intendjmp 1)


Proof:
------

1. GenPsi(X,1) |- . : .								[ (trans-C-t), def of GenPsi() ]
2. X |- (.,.,.,1) good								[ (partial-trasn-ok), (is-empty-t) ] 
3. X |- (.,C',is',l') good							[ Partial Trans Lemma, a2, 2 ]

6. X |- (lh},C',is',l') good							[ 3, Weakening on L ]
7. GenPsi(X,{lh}) |- 								[ Block Construction Lemma, 6 ]
     C'[l' -> check l'; is'; intendjmp lh] : GenPsi(C',l')
8. X |- (.,C[l'->...],.,lh) good						[ (partial-trans-good), 7, (is-empty-good)]
9. GenPsi(X,.) |- C'[l'->...][lh->...] : GenPsi(C',l',lh)			[ Block Construction Lemma, 8 ]

dP. P = GenPsi(Dom(C'[l'-> check l'; is'; intendjmp lh][lh -> check lh; intendjmp lh])

4. X;. |- C'[l'-> check l';is';intendjmp lh][lh -> check lh;intendjmp lh] : P   [ Inversion on (partial-trans-good), 3 ]
1'. |- C'[l'-> check l';is';intendjmp lh][lh -> check lh;intendjmp lh] : P	[ Inversion on (trans-C-t), 4, (C-t), def of [[X]]_l ]


dG = { r1 -> <G,int,0>, r1' -> <B,int,0>,
       ...,
       rn -> <G,int,0>, rn' -> <B,int,0>,
       ri -> <B,ok,0>,
       tg -> <G,int,0>, tb -> <B,int,0> }
   
10. Forall r. .;P |- R(r) : G(r)					[ a3, def of InitRegFile, dG, (int-t), (rit-t), (val-t) ]
2'. P |- R : G								[ (R-t), 11 ]

3'. |- 0 : empty o 0


dG'. G' = G[tg -> <G,P(1),1>][tb -> <B,P(1),1>][ri -> <B,go,1>]
dS.  S = 0/a1',...,0/an',  1/atg, 1/atb, 1/ari, (emptyo0)/alpha

13. P(1) = [[X]]_l								[ Inversion of (trans-C-t), 1, dP ]
14. P(1) = All[D1](G1,A1)							[ Inversion of ([[X]]), 13 ]
15. D1 = a1:kint, ..., an:kint, alpha:khist, 
          ari: int, atg:kint, atbt:kint, atbf:kint, atr:kint
16. A1 = alpha o 1
17. G1 = { r1:<G,int,a1>, r1':<g,int,a1>, 
	    ..., 
	    rn:<G,int,an>, rn':<G,int,an>,
            ri:<R,check,ari>, 
            tg:<G,int,atg>, tb:<B,int,atb> }

18. G' = {  r1:<G,int,0>, r1':<B,int,0>, 					[ dG', dG ]
	    ..., 
	    rn:<G,int,0>, rn':<B,int,0>,
            ri:<B,go,1>, 
            tg:<G,P(1),1>, tb:<B,P(1),1> }

19. . |- S : D1									[ dS, 15 ]
20. . |- G'[ri-><R,check,1>] <= S(G1)						[ (G-subtp), (subtp-reflex), 17, dS, dG' ]




									G'(ri) = <B,go,1>				[ dG' ]
									G'(rt) = <G,All[D1](G1,A1),1>			[ dG' ]
									. |- 1 = 1					[ ]
									. |- S : D1					[ 19 ]
									. |- G'[ ri -> <R,check,Et'>] <= S(G1)		[ 20 ]
[ (mov-t), (sequence-t), (mov-t), (sequence-t), (intend-t), 19 ]        . |- empty o 0 o 1 = S(A1)			[ 16, dS ]
-----------------------------------------------------------------    	--------------------------------------------------------------------------- (jmp-t)
.;P;G;emptyo0;0;undef |- mov tb B 1; intend tb; mov tg G 1; G'    	.;P;G';emptyo0;0;undef |- jmp tg
--------------------------------------------------------------------------------------------------------------------------------------------------- (sequence-t)
.;P;G;emptyo0;0;undef |- mov tb B 1; intend tb; mov tg G 1; jmp tg
--------------------------------------------------------------------------------------------------------------------------------------------------- [macro expansion ]
.;P;G;emptyo0;0;undef |- intendjmp 1

6'. .;P;G;emptyo0;0;undef |- intendjmp 1

4'. . |- 0 = 0
5'. . |- 0 = 0


21. |- (C'[l'-> check l'; is'; intendjmp lh][lh -> check lh; intendjmp lh],0,R,intendjmp 1)	[ (S-t), 1', 2', 3', 4', 5', 6' ]


* Translation Theorem Complete