------------
| Sf sim_c S |
 ------------



------------------- (sim-val)
c' n   sim_c  c' n


--------------------------- (sim-val-zap)
c n  sim_c  c n'


Forall r. Rf(r) sim_sc R(r)
--------------------------- (sim-R)
Rf sim_c R


|-  (C,h,R, b)
|-c (C,h,Rf,b)
Rf sim_c R
--------------------------- (sim-S)
(C,h,Rf,b) sim_c (C,h,R,b) 




 ------------
| S -->^l S' | Block Transition - transitition between blocks
 ------------
 

(C,h,R,b) -->_0 (C,(h,l),R',b')
------------------------------- (trans-eval)
(C,h,R,b) -->^l (C,(h,l),R',b')




 -------------
| S -->*_k MS | Block Evaluation -- evaluate to last instruction in current block adding k faults
 -------------  (when k is left off, assume 0)
 

(C,h,R,b) -->_0 recover
-------------------------- (blk-eval-recover)
(C,h,R,b) -->*_0 recover


--------------------------------------- (blk-eval-jmp)
(C,h,R,jmp rt) -->*_k  (C,h,R,jmp rt)


------------------------------------------- (blk-eval-brz)
C,h,R,brz rz rt) -->*_k  (C,h,R,brz rz rt)


 
(C,h,R,b) -->_k1 (C,h,R',b')    (C,h,R',b') -->*_k2 MS
----------------------------------------------------------------- (blk-eval-sequence)
(C,h,R,b) -->*_(k1+k2) MS







 ------------
| S -->^h MS | Program Execution -- evaluate a program through a sequence of blocks
 ------------  (when k is left off, assume 0)
 

S -->*_k MS
------------------------- (prog-exec-blk)
S -->^()_k MS
 

S -->^h_k S'   S' -->_0 hw-error
-------------------------------------- (prog-exec-seq-hw-error)
S -->^h_k hw-error 
 

S -->^h S''  S'' -->^l S'''  S''' -->*_k MS
-------------------------------------------- (prog-exec-seq-trans-blk)
S -->^(h,l)_k MS