**********************
*  PROGRESS THEOREM  *
**********************

If  |- (h,g,s,b)  then  (h,g,s,b) -> (h',g',s',b')


PROOF:

By case analysis on the structure of b.

(Shorthands: a1 for "assumption 1", p1 for "case premise 1", pa1 for "subcase a, premise 1")





CASE MOV: b = mov r,o ; b2
~~~~~~~~~~~~~~~~~~~~~~~~~~~

a1. |- (h, g, s, mov r,o; b2 )					[ assumption ]

1. |-  h : H   							[ Inversion of m-tp, a1 ]
2. {};H |- s : S						[ Inversion of m-tp, a1 ]
3. {};H |- g : G						[ Inversion of m-tp, a1 ]
4. {};H;G;S |- mov r,o; b2					[ Inversion of m-tp, a1 ]

5. {};H |- (G;S) mov r, o (G';S')				[ Inversion of b-ins, 4, inspection of i-mov ]
6. {};H;G |- o : t						[ Inversion of i-mov, 5 ]
7. {};H |- (G;S) {r <- t} (G';S')				[ Inversion of i-mov, 5 ]

8. Exists w. g |- o ==> w					[ Canonical Forms, 6, 1, 3 ]
9. Exists g',s'. (g,s) {r <- w} (g', s')			[ Lemma A-U-Progress, 7, 6, 8, 1, 2, 3 ]
10. (h, g, s, mov r,o; b2 ) --> (h, g', s', b2)			[ e-mov, 8, 9 ]
* MOV complete





CASE ADD: b = add r, o; b2                                                                               
~~~~~~~~~~~~~~~~~~~~~~~~~~~

a1. |- (h,g,s, add r, o; b2)					[ assumption ]

1. |-  h : H   							[ Inversion of m-tp, a1 ]
2. {};H |- s : S						[ Inversion of m-tp, a1 ]
3. {};H |- g : G						[ Inversion of m-tp, a1 ]
4. {};H;G;S |- add r,o; b2					[ Inversion of m-tp, a1 ]

6. {};H |- (G;S) add r o (G';S')				[ Inversion of b-ins, 4 ]

subcase on the structure of 6

subcase ADD.a:

  G(r) = Single(l)
  S |- l + i = l'
  (G;S) {r <- Single(l')} (G';S')
  -------------------------------- (i-add-l)
  {};H |- (G;S){add r,-4*i}(G';S')

6b. {};H;G |- r : Single(l)					[ o-reg, pa2 ]
7b. Exists d, d'. l = d and l' = d' and d + i = d'		[ S-arithmetic-d, pa2, 2 ]
8b. {};H;G |- r : Single(d)					[ 6b, 7b ]
9b. Exists d. g |- r ==> d 					[ Canonical Forms, 8b, 1, 3 ] 

10b. g |- -4*i ==> -4*i 					[ eo-w ]

11b. {};H;G |- d+i : Single(l')					[ o-d, 7b ] 
12b. g |- d+i ==> d+i						[ eo-w ]
13b. Exists g',s'. (g,s) {r1 <- d+i} (g',s')			[ Lemma A-U-Progress, pa3, 11b, 12b, 1, 2, 3 ]

14b. (h,g,s,add r,o;b2) --> (h,g',s', b2)			[ e-add-d, 9b, 10b, 13b ]
* ADD.a complete

subcase ADD.b:

  {};H;G |- o : int
  r ! = esp
  G(r) = int
  -------------------------- (i-add)
  {};H |- (G;S){add r,o}(G;S)

6c. {};H;G |- r : int						[ o-reg, pc3]
7c. Exists i1. g |- r ==> i1					[ Canonical Forms, 6c, 1, 3 ]
8c. Exists i2. g |- o ==> i2					[ Canonical Forms, pc1, 1, 3 ]
9c. (g,s) {r <- i1+i2} (g[r <- i1+i2],s)			[ u-not-esp, pc2 ]
10c. (h,g,s,add r,o;b2) --> (h,g[r <- i1+i2],s, b2)		[ e-add, 7c, 8c, 9c ]
* ADD.b complete






CASE SUB: b = add r, o; b2
~~~~~~~~~~~~~~~~~~~~~~~~~~

as in case ADD.b (i-sub instead of i-add, e-sub instead of e-add)
* SUB complete





CASE LOAD: b = load r1, [r2+i]; b2
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

a1. |- (h,g,s, load r1, [r2+i]; b2)				[ assumption ]

1. |-  h : H   							[ Inversion of m-tp, a1 ]
2. {};H |- s : S						[ Inversion of m-tp, a1 ]
3. {};H |- g : G						[ Inversion of m-tp, a1 ]
4. {};H;G;S |- load r1, [r2+i]; b2				[ Inversion of m-tp, a1 ]

5. {};H |- (G;S) load r1, [r2+i] (G';S')			[ Inversion of b-ins, 4 ]
subcase on the structure of 5


subcase LOAD.a: loading from a heap pointer

  G(r2) = HeapPtr(t)
  |- (G,S){r1<-t}(G',S')
  ------------------------------------ (i-load-p)
  {};H |- (G;S){load r1,[r2+0]}(G';S')

6a. {};H;G |- r2 : HeapPtr(t)						[ o-reg, pa1 ]
7a. Exists p,w. g |- r2 ==> p  and  h(p) = <w>  and H(p) = HeapPtr(t)	[ Canonical Forms, 6a, 1, 3]

8a. Forall p' in dom(H) or dom(h). {}; H |- h(p') : H(p')		[ Inversion of h-tp, 1 ]
9a. {};H |- <w> : HeapPtr(t)						[ 8a, 7a ]
10a. {};H;G |- w : t							[ Inversion of v-hp, 9a, weakening with G ]
11a. g |- w ==> w							[ eo-w ]
12a. Exists g', s'. (g,s) {r1 <- w} (g',s')				[ Lemma A-U-Progress, pa2, 10a, 11a, 1, 2, 3 ]

13a. (h,g,s,load r1, [r2+0];b2) --> (h,g',s', b2)			[ e-load-p, 7a, 7a, 12a ]
* LOAD.a complete


subcase LOAD.b: loading from a known stack location

  G(r2) = Single(l)
  S |- l + i = l'
  S |- l' : t
  |- (G,S){r1<-t}(G',S')
  -------------------------------------- (i-load-concat)
  {};H |- (G;S){load r1,[r2+4*i]}(G';S')

6b. Exists d,d'. l = d and l' = d' and d' = d + i		[ Lemma S-arithmetic-d, pb2, 2 ] 			
7b. {};H;G |- r2 : Single(d)					[ o-reg, pb1, 6b ]
8b. g |- r2 ==> d						[ Canonical Forms, 7b, 1, 3 ]

9b. (l',t) in atoms(S)						[ Lemma S-lookup-atom, pb3 ]
10b. Exists w. s(d') = w  and  {};H;{} |- w : t			[ Lemma S-atom-in-stack, 2, 9b, 6b ]

11b. g |- w ==> w						[ eo-w ]

16b. Exists s', g'. (g,s) {r1 <- w} (g',s')			[ Lemma A-U-Progress, pb4, 10b, 11b, 1, 2, 3 ]
17b. (h,g,s,(load r1,[r2+i]; b2)) --> (h,g',s',b2)		[ e-load-d, 8b, (10b,6b), 16b ]
* LOAD.b complete


subcase LOAD.c: loading from an aliased stack location...

  G(r2) = Single(l)      
  S |- l : t
  |- (G,S){r1<-t}(G',S')
  ------------------------------------------------ (i-load-aliased)
  {};H |- (G;S){load r1,[r2+0]}(G';S')


6c. (l,t) in atoms(S)						[ Lemma S-lookup-atom, pc2 ]
7c. Exists p. l = p and H(p) = HeapPtr(t)			[ Lemma S-atom-in-stack, 2, 6c ]
    or Exists d,w. l = d and s(d) = w and {};H;{} |- w : t
subsubcase on 7c.


subsubcase LOAD.c1: loading from an aliased stack location that is really a heap location

a2c1. Exist p. l = p
a3c1. H(p) = HeapPtr(t)

8c1. {};H;G |- r2 : Single(p)					[ o-reg, pc1, a2c1 ]
9c1. g |- r2 ==> p						[ Canonical Forms, 8c1, 1, 3 ] 

10c1. Forall p' in dom(H) or dom(h). {}; H |- h(p') : H(p')	[ Inversion of h-tp, 1]  
11c1. {}; H |- h(p) : HeapPtr(t)				[ 10c1, a3c1 ]
12c1. h(p) = <w>						[ Inspection of v-hp, 11c1 ]
13c1. D;H;{} |- w : t						[ Inversion of v-hp, 11c1 ]
14c1. g |- w ==> w						[ eo-w ]

15c1. Exists g',s'. (g,s) {r1 <- w} (g',s')			[ Lemma A-U-Progress, pc3, 14c1, 9c1, 1, 2, 3 ]
16c1. (h,g,s,(load r1,[r2+0]; b2)) --> (h,g',s',b2)		[ e-load-p, 9c1, 12c1, 15c1 ]
* LOAD.c1 complete


subsubcase LOAD.c2: loading from an aliased stack location that is really a stack location

a2c2. Exists d,w. l = d
a3c2. s(d) = w
a4c2. {};H;{} |- w : t

8c2. {};H;G |- r2 : Single(d)					[ o-reg, pc1, a2c2 ]
9c2. g |- r2 ==> d						[ Canonical Forms, 8c2, 1, 3 ]

10c2. g |- w ==> w						[ eo-w ]
11c2. Exists g',s'. (g,s) {r1 <-w} (g',s')			[ Lemma A-U-Progress, pc3, a4c4, 10c2, 1, 2, 3 ]
12c2. (h,g,s,(load r1,[r2+0]; b2)) --> (h,g',s',b2)		[ e-load-l, 9c2, ac22, 11c2 ]
* LOAD.c2 complete







CASE STORE: b = store [r1+i], r2; b2
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

a1. |- (h,g,s, store [r1+i], r2; b2)				[ assumption ]

1. |-  h : H   							[ Inversion of m-tp, a1 ]
2. {};H |- s : S						[ Inversion of m-tp, a1 ]
3. {};H |- g : G						[ Inversion of m-tp, a1 ]
4. {};H;G;S |- load r1, [r2+i]; b2				[ Inversion of m-tp, a1 ]

5. {};H |- (G;S) store [r1+i], r2 (G';S')			[ Inversion of b-ins, 4 ]

subcase on the structure of 5


subcase STORE.a: storing to a heap pointer

  G(r1) = HeapPtr(t')
  G(r2) = t
  ---------------------------------- (i-store-p)
  {};H |- (G;S){store [r1+0],r2}(G;S)

6a. {};H;G |- r1 : HeapPtr(t')					[ o-reg, pa1 ]
7a. Exists p,w.  g |- r1 ==> p  and  h(p) = <w>  and H(p) = t	[ Canonical Forms, 6a, 1, 3 ]

8a. {};H;G |- r2 : t						[ o-reg, pa2 ]
9a. Exists w'. g |- r2 ==> w'					[ Canonical Forms, 8a, 1, 3 ]

10a. (h,g,s,(store r1,[r2+0]; b2)) --> (h[p<-w'],g,s,b)		[ e-load-p, 8a, 9a, 8a ]
* STORE.a complete


subcase STORE.b: storing to a known stack pointer

  G(r1) = Single(l)
  G(r2) = t
  S |- l + i = l'
  S |- l' <- t ~~> S'
  ---------------------------------------- (i-store-strong)
  {};H |- (G;S){store [r1+(-4*i)],r2}(G;S')

6b. Exists d,d'. l = d and l' = d' and d' = d + i		[ Lemma S-arithmetic-d, pb3, 2 ]
7b. {};H;G |- r1 : Single(d)					[ o-reg, pb1, 6b ]
8b. g |- r1 ==> d						[ Canonical Forms, 7b, 1, 3 ]

9b. {};H;G |- r2: t						[ o-reg, pb2 ]
10b. Exists w. g |- r2 ==> w					[ Canonical Forms, 9b, 1, 3 ]

10b. Exists t'. (l',t') in atoms(S)				[ Lemma S-update-atom, pb4 ]
11b. Exists w'. s(d') = w'  and  {};H;{} |- w' : t		[ Lemma S-atom-in-stack, 2, 9b, 6b ]
12b. Exists s'. s' = s[d' <- w]					[ Lemma S-lookup-update, 10b ]

12b. (h,g,s,(store [r1+i],r2; b2)) --> (h,g,s',b)		[ e-store-d, 8b, 10b, (12b, 6b) ]
* STORE.b complete


subcase STORE.c: storing to an aliased stack pointer

  G(r1) = Single(l)
  S |- l : t 
  G(r2) = t
  ------------------------------------- (i-store-weak)
  {};H |- (G;S){store [r1+0],r2}(G;S)

6c. {};H;G |- r2: t						[ o-reg, pc3 ]
7c. Exists w. g |- r2 ==> w					[ Canonical Forms, 6c, 1, 3 ]

8c. (l,t) in atoms(S)						[ Lemma S-lookup-atom, pc2 ]
9c. Exists p. l = p and H(p) = HeapPtr(t)			[ Lemma S-atom-in-stack, 2, 8c ]
    or Exists d,w. l = d and s(d) = w and {};H;{} |- w : t
subsubcase on 9c.

subsubcase STORE.c1: storing to an aliased stack location that is really a heap pointer
a2c1. Exist p. l = p
a3c1. H(p) = HeapPtr(t)

8c1. {};H;G |- r1 : Single(p)					[ o-reg, pc1, a2c1 ]
9c1. g |- r1 ==> p						[ Canonical Forms, 8c1, 1, 3 ]

10c1. Forall p' in dom(H) or dom(h). {}; H |- h(p') : H(p')	[ Inversion of h-tp, 1]
11c1. {}; H |- h(p) : HeapPtr(t)				[ 10c1, a3c1 ]
12c1. Exists w'. h(p) = <w'>					[ Inspection of v-hp, 11c1 ]

11a. (h,g,s,(store [r1+i],r2; b2)) --> (h[p<-w],g,s,b)		[ e-load-p, 9c1, 7c, 12c1 ]
* STORE.c1 complete

subsubcase STORE.c2: storing to an aliased stack location that is really a stack location
a2c2. Exists d,w'. l = d
a3c2. s(d) = w'
a4c2. {};H;{} |- w' : t

8c2. {};H;G |- r1 : Single(d)					[ o-reg, pc1, a2c2 ]
9c2. g |- r1 ==> d						[ Canonical Forms, 8c2, 1, 3 ]

10c2. Exists s'. s' = s[d <- w]					[ Lemma S-lookup-update, a3c2 ]

11c2. (h,g,s,(store [r1+i],r2; b2)) --> (h,g,s',b)		[ e-store-d, 9c2, 7c, 10c2 ]
* STORE.c2 complete







CASE HEAPALLOC: b = heapalloc r1 <o>; b2
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

a1. |- (h,g,s, heapalloc r1 <o>; b2)				[ assumption ]

1. |-  h : H   							[ Inversion of m-tp, a1 ]
2. {};H |- s : S						[ Inversion of m-tp, a1 ]
3. {};H |- g : G						[ Inversion of m-tp, a1 ]
4. {};H;G;S |- heapalloc r1 <o>; b2				[ Inversion of m-tp, a1 ]

5. {};H |- (G;S) heapalloc r1 <o> (G';S')			[ Inversion of b-ins, 4 ]

6. {};H;G |- o : t						[ Inversion of i-heapalloc, 6 ]
7. |- (G,S){r<-HeapPtr(t)}(G',S')				[ Inversion of i-heapalloc, 6 ]

8. Exists w. g |- o ==> w					[ Canonical Forms, 6, 1, 3 ]
10. r != esp							[ Inversion of a-not-esp, 7 ]
11. let p be fresh						
12. (g,s) {r <- p} (g[r<-p], s)					[ e-not-esp, 10 ]

12. (h,g,s,(heapalloc r = <o>;b2)) --> ((h,p-><w>),g[r<-p],s,b2)[ e-heapalloc, 9, 11, 12]
* HEAPALLOC complete






CASE UNPACK: b = (L,r) = unpack(o); b2
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

a1. |- (h,g,s, (L,r) = unpack(o); b2)				[ assumption ]

1. |-  h : H   							[ Inversion of m-tp, a1 ]
2. {};H |- s : S						[ Inversion of m-tp, a1 ]
3. {};H |- g : G						[ Inversion of m-tp, a1 ]
4. {};H;G;S |- (L,r) = unpack(o); b2				[ Inversion of m-tp, a1 ]

5. {};H;G |- o : HeapPtr(t)					[ Inversion of i-unpack, 6]
6. r != esp							[ Inversion of i-unpack, 6]

8. Exists p,w.  g |- o ==> p  and  h(p) = <w> 			[ Canonical Forms, 5, 1, 3 ]
9. (g,s) { r <- p } (g[r<-p],s)					[ e-not-esp, 6 ]

12. (h,g,s,((L,r) = unpack(o);b2)) --> (h,g[r<-p],s,b2[p/L])	[ e-unpack, 8, 9 ]
* UNPACK complete






CASE JUMPIF0: b = jumpif0 r, o; b2
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

a1. |- (h,g,s, jumpif0 r, o; b2)				[ assumption ]

1. |-  h : H   							[ Inversion of m-tp, a1 ]
2. {};H |- s : S						[ Inversion of m-tp, a1 ]
3. {};H |- g : G						[ Inversion of m-tp, a1 ]
4. {};H;G;S |- jumpif0 r, o; b2					[ Inversion of m-tp, a1 ]

5. {};H |- (G;S) jumpif0 r, o (G';S')				[ Inversion of b-ins, 4 ]
6. G(r) = int							[ Inversion of i-jumpif0, 6 ]
7. {};H;G |- o : All[](G',S')					[ Inversion of i-jumpif0, 6 ]

8. {};H;G |- r : int						[ o-reg, 7 ]
9. Exists i. g |- r ==> i					[ Canonical Forms, 8, 1, 3 ]

subcase on the value of i.


subcase JUMPIF0.a: i is not 0
a2a. i != 0

10a. (h,g,s,(jumpif0 r,o;b2)) --> (h,g,s,b2)			[ e-jumpif0-false, 12, a2a ]
* JUMPIF0.a complete


subcase JUMPIF0.b: i is 0
a2b. i = 0

10b. g |- r ==> 0						[ 9, a2b ]
11b. Exists p, subst. g |- o ==> p[subst]  and h(p) = block	[ Canonical Forms, 7, 1, 3 ] 
12b. h(p) = all[D'](G',S') b'					[ 11b, def of block ]

13b. (h,g,s,(jumpif0 r,o;b2)) --> (h,g,s,b'[subst/D'])		[ e-jumpif0-true, 10b, 11b, 12b ]
* JUMPIF0.b complete






CASE JUMP: b = jump o
~~~~~~~~~~~~~~~~~~~~~~

a1. |- (h,g,s, jump o)						[ ssumption ]

1. |-  h : H   							[ Inversion of m-tp, a1 ]
2. {};H |- s : S						[ Inversion of m-tp, a1 ]
3. {};H |- g : G						[ Inversion of m-tp, a1 ]
4. {};H;G;S |- jump o						[ Inversion of m-tp, a1 ]

5. {};H;G |- o : All[](G',S')					[ Inversion of b-jump, 4 ]
6. Exists p, subst. g |- o ==> p[subst]  and h(p) = block	[ Canonical Forms, 5, 1, 3 ]
7. h(p) = all[D'](G',S') b'					[ 6, def of block ]

11. (h,g,s,(jump o)) --> (h,g,s,b'[subst/D])			[ e-jump, 6, 7 ]
* JUMP complete




**** End Proof of Progress