Progress

1. If |- S then S -->_0 S'
2. If |-Z S then S -->_0 FS


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

PART 1: If |- (C,h,R,b) then (C,h,R,b) -->_0 (C',h',R',b')

 

PROOF: By case analysis on b
				


CASE MOVI: b = movi rd v; b'
~~~~~~~~~~~~~~~~~~~~~~~~~~~~

1. (C, h, R, movi rd v; b') -->_0 (C, h, R[rd -> v], b')		[ (movi) ]
* MOVI complete



CASE SUB: b = sub rd rs rs; b'
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

d1. let v' = R_col(rs) (R_val(rs) - R_val(rt))				[ definition ]
1. (C,h,R,sub rd, rs, rt; b') -->_0 (C,h,R[ rd -> v' ], b')		[ (sub) ]
* SUB complete



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

1. (C,h,R,intend rd rs; b') -->_0 (C,h,R[rd -> R(rs)], b')		[ (intend) ]
* INTEND complete



CASE INTENDZ: b = intendz rz rt; b'
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

subcase on R_val(rz) =?= 0:

SUBCASE INTENDZ.a:
aa1. R_val(rz) = 0							[ subcase assumption ]
1a. (C,h,R,intendz rz rd rs; b') -->_0 (C,h,R[rd -> R(rs)],b')		[ (intendz-set), aa1 ]
* INTENDZ.a complete

SUBCASE INTENDZ.b:
ab1. R_val(rz) =/= 0 							[ subcase assumption ]
1b. (C,h,R, intendz rz rd rs; b') -->_0 (C,h,R,b')			[ (intendz-unset), ab1 ]
* INTENDZ.b complete




CASE RECOVERNZ: b = recovernz rz; b'
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

a1. |- (C,(h,l),R,recovernz rz; b')

1. |- C : P								[ Inversion of (S-t), a1 ]
2. P |- R : G
3. . |- (h,l) : A
4. . |- Ei = l		
5. .;P;G;A;Ei;P(l+1) |- b' 

subcase on the structure of 5 (recovernz-t doesn't apply since D = .)

SUBCASE RECOVERNZ.A:

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

6a. .;P |-Z R(rz) : <R,int,Ez>						[ Inversion of (R-t), 2, pa1 ]
7a. . |- R_val(rz) = Ez							[ Canonical Forms, 6a, 2 ]
8a. . |- Ela - Ei = 0							[ pa4 ]
9a. . |- R_val(rz) = 0 							[ Exp Eq Transitivity, 7a, pa3, 8a ]

10a. (C, (h,l), R, recovernz rz; b) -->_0 (C, (h,l), R, b) 		[ recovernz-ok, 9a ]
* 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; t |- recovernz rz; b 

6b. . |- Ela = l							[ Inversion of (h-append-t), 3 ]
7b. . |- Ela = Ei							[ Exp Eq Transitivity, 4, 6b ]
8b. subcase does not apply						[ 7b contradicts pb4 ]
* RECOVERNZ.B complete




CASE BRZ: b = brz rz rt
~~~~~~~~~~~~~~~~~~~~~~~

a1. |- (C,h,R,brz rz rt)

subcase on R_val(rz) =?= 0:

1. |- C : P
2. P |- R : G
3. .;P;G;A;Ei;P(l+1) |- brz rz rt 

subcase on R_val(rz) =?= 0

SUBCASE BRZ.a:
aa1. R_val(rz) = 0								[ subcase assumption ]

4a. G(rt) = <G,All[Dt](Gt,It,Rt),Et>						[ Inversion of (brz-t), 3 ]
5a. .;P |- R(rt) : G(rt) 							[ Inversion of (R-t), 4a ]
6a. R_val(rt) in Dom(C)								[ Canonical Forms, (4a, 5a), 1 ]

7a. (C,h,R,brz rz rt) -->_0 (C,(h,R_val(rt)),R[ri -> R R_val(ri)],C(R_val(rt)))	[ brz-taken, aa1, 6a ]
* BRZ.a complete


SUBCASE BRZ.b:
ab1. R_val(rz) =/= 0 								[ subcase assumption ]

4b. P(l+1) = All[Df](Gf,Af)							[ Inspection of (brz-t), 3 ]
5b. l+1 in Dom(P)								[ 4b, def of P ]
6b. l+1 in Dom(C)								[ Inversion of (C-t), 1, 5b ]
1b. (C,h,R,brz rz rt [ri]; b') -->_0 (C,h,R,b')					[ brz-untaken, ab1, 6b ]
* BRZ.b complete	




CASE JMP: b = jmp rt
~~~~~~~~~~~~~~~~~~~~
a1. |- (C,h,R,jmp rt)

1. |- C : P
2. P |- R : G
3. .;P;G;A;Ei;P(l+1) |- brz rz rt 
4. G(rt) = <G,All[Dt](Gt,It,Rt),Et>						[ Inversion of (jmp-t), 3 ]
5. .;P |- R(rt) : G(rt) 							[ Inversion of (R-t), 2 ]
6a. R_val(rt) in Dom(C)								[ Canonical Forms, (4, 5), 1 ]

7a. (C,h,R,jmp) -->_0 (C,(h,R_val(rt)),R[ri -> R R_val(ri)],C(R_val(rt)))	[ jmp, 6a ]
* JMP complete


** Progress Part 1 Complete.






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

PART 2: If |-Z (C,h,R,b) then (C,h,R,b) -->_0 FS

PROOF: By case analysis on b




CASES MOVI, SUB, INTEND, INTENDZ:
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

As in Progress Part 1. (Don't depend on typing info.)
* MOVI, SUB, INTEND, INTENDZ complete



CASE RECOVERNZ: b = recovernz rz; b'
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

subcase on R_val(rz) =?= 0:

SUBCASE RECOVERNZ.a:
aa1. R_val(rz) = 0							
1a. (C,h,R,recovernz rz; b') -->_0 (C,h,R,b')				[ (recovernz-ok), aa1 ]
* RECOVERNZ.a complete

SUBCASE RECOVERNZ.b:
ab1. R_val(rz) =/= 0 							
1b. (C, h, R, recovernz rz; b) -->_0 recover(h)				[ (recovernz-halt), ab1 ]
* RECOVERNZ.b complete





CASE BRZ: b = brz rz rt 
~~~~~~~~~~~~~~~~~~~~~~~~

a1. |-Z (C,h,R,brz rz rt) 

subcase on R_val(rz) and then R_val(rd) in Dom(C).

SUBCASE BRZ.a:
aa1. R_val(rz) =/= 0

1a. |- C : P									[ Inversion of (S-t), a1 ]
2a. .;P;G;A;Ei;P(l+1) |- brz rz rt 
3a. P(l+1) = All[Df](Gf,Af)							[ Inspection of (brz-t), 2a ]
4a. l+1 in Dom(P)								[ 3a, def of P ]
5a. l+1 in Dom(C)								[ Inversion of (C-t), 1a, 4a ]
6a. (C,h,R,brz rz rt [ri]; b') -->_0 (C,h,R,b')					[ brz-untaken, aa1, 5a ]
* BRZ.a complete

SUBCASE BRZ.b:
ab1. R_val(rz) = 0
ab2. R_val(rd) in Dom(C)
1b. (C,h,R,brz rz rt)-->_0(C,(h,l,R_val(rt)),R[ri -> R R_val(ri)],C(R_val(rt))) [ (brz-taken), ab1, ab2 ]
* BRZ.b complete

SUBCASE BRZ.b:
ac1. R_val(rz) = 0
ac2. R_val(rd) not in Dom(C)
1c. (C,h,R,brz rz rd; b) -->_0 hw-error(h)					[ (brz-hw-error, ac1, ac2 ]
* BRZ.c complete



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

a1. |-Z (C,h,R,brz rz rt) 

subcase on R_val(rd) in Dom(C).

SUBCASE JMP.a:
aa1. R_val(rd) in Dom(C)
1a. (C,h,R,jmp rt)-->_0(C,(h,R_val(rt)),R[ri -> R R_val(ri)],C(R_val(rt))) 	[ jmp, aa1 ]
* JMP.a complete

SUBCASE JMP.b:
ab1. R_val(rd) not in Dom(C)
1a. (C,h,R,jmp rt) -->_0 hw-error(h)						[ jmp-hw-error, ab1 ]
* JMP.b complete


** Progress Part 2 complete