-----------
| S -->_0 S | 	
 -----------


---------------------------------------------------- (movi)
(C, h, R, movi rd v; b) -->_0 (C, h, R[rd -> v], b)



v' = R_col(rs1) (R_val(rs1) - R_val(rs2))
--------------------------------------------------------------- (sub)
(C, h, R, sub rd, rs1, rs2; b) -->_0 (C, h, R[ rd -> v' ],  b)



---------------------------------------------------------- (intend)
(C, h, R, intend rt; b) -->_0 (C, h, R[ri -> R(rt)],  b)


R_val(rz) = 0
-------------------------------------------------------------- (intendz-set)
(C, h, R, intendz rz rt; b) -->_0 (C, h, R[ri -> R(rt)],  b)    


R_val(rz) =/= 0
------------------------------------------------- (intendz-unset)
(C, h, R, intendz rz rt; b) -->_0 (C, h, R, b)



R_val(rz) = 0
---------------------------------------------- (recovernz-ok)
(C, h, R, recovernz rz; b) -->_0 (C, h, R, b) 
 

R_val(rz) =/= 0
-------------------------------------------- (recovernz-halt)
(C, h, R, recovernz rz; b) -->_0 recover(h)


R_val(rz) =/= 0		l+1 in Dom(C)
---------------------------------------------------------------------------- (brz-untaken)
(C, (h,l), R, brz rz rt) -->_0 (C, (h,l,l+1), R[ri -> R R_val(ri)], C(l+1))  


R_val(rz) = 0   R_val(rt) in Dom(C)
----------------------------------------------------------------------------------------- (brz-taken)
(C, (h,l), R, brz rz rt) -->_0 (C, (h,l,R_val(rt)), R[ri -> R R_val(ri)], C(R_val(rt))) 


R_val(rz) = 0    R_val(rt) not in Dom(C)
----------------------------------------- (brz-hw-error)
(C, h, R, brz rz rt) -->_0 hw-error (h) 


R_val(rt) in Dom(C)
------------------------------------------------------------------------------ (jmp)
(C, h, R, jmp rt) -->_0 (C, (h,R_val(rt)), R[ri -> R R_val(ri)], C(R_val(rt)))  


R_val(rt) not in Dom(C)
--------------------------------- (jmp-hw-error)
(C, h, R, jmp rt) -->_0 hw-error(h)



 -----------
| S -->_1 S | 	
 -----------

R(r) = c n 
------------------------------------------- (zap-reg)
(C, h, R, b) -->_1 (C, h, R[r -> c n'], b)  


R(rz) =/= 0		l in Dom(C)
--------------------------------------------------------------- (zap-recover-linC)
(C, h, R, recover rz; b) -->_1 (C, (h,l), R, C(l))  

R(rz) =/= 0		
--------------------------------------------------------------- (zap-recover-lnotinC)
(C, (h,l), R, recover rz; b) -->_1 hw-error(h)