CF Lemma
--------
 
If |-cf Sf  then  Sf -->* recover(Sf.h)
 

Proof: 
------

By induction on the length of b. 

Length(b) = 1:
Since |-cf Sf and b = jmp or brz, contradiction and subcase does not apply

Length(b) = 2:
Call CF Step Lemma. Since b' = jmp or brz, must be that S -->_0 recover. then use blk-evak-recover.

Inductive case:
Call CF Step Lemma. Either 
(1) S -->_0 recover -- use blk-exec-recover
(2) S -->_0 S' and |-cf S'. Use IH and then put back together with S-->_0 S' using blk-eval-sequence and blk-eval-recover.


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


CF Step Lemma
-------------
 
If |-cf (C,h,R,b)   
then either (1) (C,h,R,b) -->_0 (C,h,R',b')  and |-cf S'  
	    (2) (C,h,R,b) -->_0 recover(h)

 
Proof: By case analysis on the structure of b - 
------
 

CASE MOVI: b = movi rd v; b'
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
a1. |-cf (C,h,R,movi rd v; b')
 
1. (C,h,R,movi rd v; b') -->_0 (C, h, R[rd -> v], b')				[ (movi) ]
2. |-cf (C, h, R[rd -> v], b')							[ Progress-No-Elevation, a1, 1 ]
3. (C,h,R,movi rd v;b') -->_0 (C,h,R[rd -> v],b') and |-cf (C,h,R[rd -> v],b')	[ 1, 2 ]
* MOVI complete

 
 
CASE SUB: b = sub rd rs rs; b'
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
a1. |-cf (C,h,R,sub rd rs rs; b')
 
d1. let v' = R_col(rs1) (R_val(rs1) - R_val(rs2))
1. (C,h,R,sub rd rs rs; b') -->_0 (C, h, R[rd -> v], b)				[ (sub), d1 ]
2. |-cf (C, h, R[rd -> v], b)							[ Progress-No-Elevation, a1, 1]
3. (C,h,R,sub rd rs rs;b') -->_0 (C,h,R[rd -> v],b) and |-cf (C,h,R[rd -> v],b) [ 1, 2 ]
* SUB complete

 
 
CASE INTEND: b = intend ri rt; b'
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

a1. |-cf (C,(h,l),R, intend ri rt; b')

1. . |- Ei =/= l 								[ Inversion of (S-t), a1 ]
2. G(ri) =/= <R,check,Ei> ==> . |- Ei = l
3. .;P;G;A;Ei;P(l+1) |- intend ri rt; b'

4. G(ri) = <ci,ok,Ei>								[ Inversion of (sequence-t), 3, Inversion of (intend-t), ]
5. . |- Ei = l									[ 2, 4 ]
6. contradiction								[ 1, 5 ]
case does not apply
* INTEND complete

 
 
 
CASE INTENDZ: b = intendz rz rt; b'
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
a1. |-cf (C,(h,l),R, intendz rz rt; b')

1. . |- Ei =/= l 								[ Inversion of (S-t), a1 ]
2. G(ri) =/= <R,check,Ei> ==> . |- Ei = l
3. .;P;G;A;Ei;P(l+1) |- intendz rz rt; b'

4. G(ri) = <R,check,Eli>							[ Inversion of (sequence-t), 3, Inversion of (intendz-t), ]
5. . |- Ei = l									[ 2, 4 ]
6. contradiction								[ 1, 5 ]
case does not apply
* INTENDZ complete
 
 
 
 
CASE RECOVERNZ: b = recovernz rz; b'
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
a1. |- (C,(h,l),R,recovernz rz; b')

1. . |- Ei =/= l 								[ Inversion of (S-t), a1, Inspection of (recovernz-t, -eq-t, -neq-t) ]
2. G(ri) =/= <R,check,Ei> ==> . |- Ei = l
3. |- (h,l) : seq o Ela
4. .;P;G;seq o Ela;Ei;P(l+1) |- recovernz rz; b'

subcase on the structure of 4 (recovernz-t does not apply as D = .)


SUBCASE RECOVERNZ.A:

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

5a. . |- l = Ela 								[ Inversion of (h-append-t), 3 ]
6a. . |- Ei = l									[ Exp Eq Transitivity, pa4, 5a ]
7a. contradiction								[ 6a, 1 ]
subcase does not apply
* RECOVERNZ.A complete


SUBCASE RECOVERNZ.B:

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

5b. P |-cf R : G								[ Inversion of (S-t), a1 ]
6b. .;P |-cf R(ri) : <R,check,Ei>						[ Inversion of (R-t), 5b, pb2 ]
7b. .;P |-cf R(rz) : <R,int,Ez>							[ Inversion of (R-t), 5b, pb1 ]
8b. . |- R_val(ri) = Ei								[ Canonical Forms, 6b, (Inversion of (S-t), a1) ]
9b. . |- R_val(rz) = Ez								[ Canonical Forms, 7b, (Inversion of (S-t), a1) ]
10b. . |- R_val(rz) = Ei - Ela							[ Exp Eq Transitivity, 9b, pb3 ]
11b. R_val(rz) =/= 0								[ 10b, pb4 ]
12b. (C, (h,l), R, recovernz rz; b) -->_0 recover(h,l)				[ (recover-halt), 11b ]
* RECOVERNZ.B complete

 
 
 
 
CASE BRZ: b = brz rz rt
~~~~~~~~~~~~~~~~~~~~~~~
 
a1. |-cf (C,(h,l),R, brz rz rt)

1. . |- Ei =/= l 								[ Inversion of (S-t), a1 ]
2. G(ri) =/= <R,check,Ei> ==> . |- Ei = l
3. .;P;G;A;Ei;P(l+1) |- brz rz rt

4. G(ri) = <B,goz,Ez'?Ef':Et'>							[ Inversion of (sequence-t), 3, Inversion of (brz-t), ]
5. . |- Ei = l									[ 2, 4 ]
6. contradiction								[ 1, 5 ]
case does not apply
* BRZ complete
 
 

 
CASE JMP: b = jmp rt
~~~~~~~~~~~~~~~~~~~~

a1. |-cf (C,(h,l),R, jmp rt)

1. . |- Ei =/= l 								[ Inversion of (S-t), a1 ]
2. G(ri) =/= <R,check,Ei> ==> . |- Ei = l
3. .;P;G;A;Ei;P(l+1) |- jmp rt

4. G(ri)= <B,go,Et'>								[ Inversion of (sequence-t), 3, Inversion of (jmp-t), ]
5. . |- Ei = l									[ 2, 4 ]
6. contradiction								[ 1, 5 ]
case does not apply
* JMP complete