--------
| D |- E |	      Static Expression Equality
 --------

x in Dom(D)
------------ (wf-var)
D |- x : D(x)


-------------- (wf-int)
D |- n : kint


D |- E1:kint   D |- E2:kint
--------------------------- (wf-sub)
D |- E1 - E2 : kint


D |- E1:kint   D |- E2:k   D |- E3:k
------------------------------------ (wf-ifexp)
D |- E1 ? E2 : E3 : k





 -------------
| D |- E = E  |	      Static Expression Equality
 -------------

D |- E1:kint   D |- E2: kint
Forall S.  . |- S : D  ==>  [[S(E1)]] = [[S(E2)]]
--------------------------------------------------- (E-eq)
D |- E1 = E2


D |- E1:kint   D |- E2: kint
Forall S.  . |- S : D  ==>  [[S(E1)]] =/= [[S(E2)]]
--------------------------------------------------- (E-eq)
D |- E1 =/= E2



D |- E1 = E2   D |- seq1 = seq2
----------------------------------
D |- seq1 o E1 = seq2 o E2


----------------------
D |- empty = empty




 ---------
|  [[E]]  |
 ---------
 
[[n]]  =  n
[[E1 - E2]]  =  [[E1]] - [[E2]]
[[Eb?Et:Ef]] = if [[Eb]] then [[Et]] else [[Ef]]





 --------------
| D |- S : D'  |	
 --------------

				D |- S : D'    D |- E:k    x not in (D union D')
----------- (subst-empt-t)	-----------------------------------------------  (subst-t)
D |- . : .			D |-  S,E/x  :  (D',x:k)





 -------------
| P |- n : t' |	      Integer Typing Judgment
 -------------


--------------- (int-t)		--------------- (address-t)	------------- (rit-t)
P |- n : int			P |- n : P(n)			P |- n : rit





 ---------------
| D |-  t <= t' |	Subtyping Judgment
 ---------------

D |- E1 = E2
-------------------------- (subtp-reflex)
D |- <c,b,E1> <= <c,b,E2>


D |- E1 = E2
--------------------------- (subtp-int)
D |- <c,b,E1> <= <c,int,E2>


Forall r. G1(r) <= G2(r)
------------------------------- (G-subtp)
D |- G1 <= G2





 -----------------
| D; P |-Z  v : t |	Value Typing Judgment
 -----------------



P |- n : t'     D |- E = n
--------------------------- (val-t)
D;P |-Z  c n : <c,t',E>


D |- E : kint
--------------------------- (val-zap-c-t)
D;P |-c  c n : <c,t',E>


D |- E : kint
c' = B or c' = G					<-- Note: value can be red
--------------------------- (val-zap-cf-t)
D;P |-cf  c n : <c',t',E>






 -----------------
| D;P;G |- i : G' |	   Instruction Typing Judgment
 -----------------

rd =/= ri
-------------------------------------------------- (movi-t)
(D;P;G) |- movi rd c i : G[ rd -> <c,int,i> ]


rd =/= ri
G(rs1) = <c,int,Es1>   G(rs2) = <c,int,Es2>
---------------------------------------------------- (sub-t)
D;P;G |- sub rd rs1 rs2 : G[ rd -> <c,int,Es1-Es2> ]




G(ri) = <ci,ok,Ei>    G(rt) = <B,All[Dt](Gt,At),Et> 
----------------------------------------------------- (intend-t)
D;P;G |- intend rt : G[ ri -> <B,go,Et> ] 


G(ri) = <B,go,Ei>
G(rt) = <B,All[Dt](Gt,At),Et>    
G(rz) = <B,int,Ez> 
----------------------------------------------------- (intendz-t)
D;P;G |- intendz rz rt : G[ ri -> <B,goz,Ez?Ei:Et> ]





 --------------------
| D;P;G;A;Ei;to |- b |	Block Typing Judgment		
 --------------------
// Ei is where we had intended to go, on block entry will always describe ri
// to is type of fallthru block


D;P;G |- i : G'     D;P;G';A;Ei;to |- b 
------------------------------------------------------- (sequence-t)
D; P; G; A; Ei; to |- i;b  



G(rz) = <R,int,Ez>    D,x:kint |- Ez = El - x  
G(ri) = <R,check,x>
D |- G/ri/rz wf      D |- seq wf    D |- El : kint
D;P;G[rz-><R,int,0>][ri-><B,ok,El>]; seq o El; El; to |- b
------------------------------------------------------------------ (recovernz-t)
(D,x:kint); P; G; seq o El; x; to |- recovernz rz; b



G(rz) = <R,int,Ez> 
G(ri) = <R,check,Eli>
. |- Ez = Eli - Ela
. |- Eli = Ela 				
.; P; G[ri -> <R,ok,Eli>]; seq o Ela; Eli; to |- b
------------------------------------------------- (recovernz-eq-t)
.; P; G; seq o Ela; Eli; to |- recovernz rz ; b 



G(rz) = <R,int,Ez>    
G(ri) = <R,check,Eli>
. |- Ez = Eli - Ela   
. |- Eli =/= Ela 
------------------------------------------------- (recovernz-neq-t)
.; P; G; seq o Ela; Eli; to |- recovernz rz; b 



G(ri)= <B,goz,Ez'?Ef':Et'>
D |- Ef' = Ela + 1

G(rz) = <G,int,Ez>  
D |- Ez = Ez'

G(rt) = <G,All[Dt](Gt,At),Et>
D |- Et = Et'

Exists St. D |- St : Dt
D |- G[ri -> <R,check,Et'>] <= St(Gt)
D |- seq o Ela o Et' = St(At)

Exists Sf. D |- Sf : Df
D |- G[ri -> <R,check,Ef'>] <= Sf(Gf)
D |- seq o Ela o Ef' = Sf(Af)
--------------------------------------------------------------------------- (brz-t)
(D; P; G; seq o Ela; Ei; All[Df](Gf,Af) ) |- brz rz rt  




G(ri)= <B,go,Et'>

G(rt) = <G,All[Dt](Gt,At),Et>
D |- Et = Et'

Exists S. D |- St : Dt
D |- G[ri -> <R,check,Et'>] <= St(Gt)
D |- seq o Ela o Et = St(At)
----------------------------------------- (jmp-t)
(D; P; G; seq o Ela; Ei; t) |- jmp rt





 ----------
| |- C : P |	Code Typing Judgment
 ----------


Forall n in Dom(C) union Dom(P). 
P(n) = All[D,Y:kint,alpha:kseq]((G,ri-><R,check,Y>),alpha o n)											
/\ D |- G wf  /\ Forall r' in Dom(G). G(r') =/= <R,t',E'>
/\ D |- P(n+1) wf
/\ (D,Y:kint,alpha:kseq); P; (G,ri-><R,check,Y>); alpha o n; Y; P(n+1) |- C(n)	
------------------------------------------------------------------------------- (C-t)
|- C : P





 ------------
| P |- R : G |	Register File Typing Judgment
 ------------


Forall r. P;. |-Z  R(r) : G(r)
------------------------------ (R-t)
P |-Z  R : G





 -------------
| |-  h : seq |	  Sequence Typing Judgment
 -------------


------------------------------ (h-empty-t)	
|- () : empty



|- E = n
|- h : seq
------------------------------ (h-append-t)				
|- (h,n): seq o E





 ------------------
| |-Z (C, h, R, b) |	Machine Typing Judgment
 ------------------


|- C : P
P |-Z R : G
|- (h,l) : A
Z = cf  ? . |- Ei =/= l  : |- Ei = l
G(ri) =/= <R,check,Ei> ==> . |- Ei = l
.;P;G;A;Ei;P(l+1) |- b 
------------------------------------ (S-t) 
|-Z (C,(h,l),R,b)