**************************
*  PRESERVATION THEOREM  *
**************************

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

PROOF:

By case analysis on the structure of (h,g,s,b) -> (h',g',s',b').



case E-MOV:
~~~~~~~~~~~

  g |- o ==> w
  (g,s){r<-w}(g',s')
  -------------------------------------- (e-mov)
  (h,g,s,(mov r,o; b2)) --> (h,g',s',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 ]
4'. {};H;G';S' |- b2						[ Inversion of b-ins, 4, 5 ]

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

2'. {};H |- s' : S'						[ Lemma A-U-Preservation, 8, 7, p1, p2, 1, 2, 3 ]
3'. {};H |- g' : G'									

8. |- (h,g',s',b2)						[ m-tp, 1, 2', 3', 4' ]
* E-MOV complete







case E-ADD-D:
~~~~~~~~~~~~~

  g |- r ==> d
  g |- o ==> -4*i
  (g,s){r<-d+i}(g',s')
  -------------------------------------- (e-add-d)
  (h,g,s,(add r,o; b2)) --> (h,g',s',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 ]

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

subcase on the structure of 5.

subcase E-ADD-D.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')


7a. Exists d, d'. l = d and l' = d' and d + i = d'		[ Lemma S-arithmetic-d, pa2, 2 ]
8a. {};H;G |- d+i : Single(l')					[ o-d, 7a ]
9a. g |- d+i ==> d+i						[ eo-w ]

2'. {};H |- s' : S'						[ Lemma A-U-Preservation, pa3, 8a, 9a, p3, 1, 2, 3 ]
3'. {};H |- g' : G'							

10a. |- (h,g',s',b2)						[ m-tp, 1, 2', 3', 4' ]
* E-ADD-D.a complete


subcase E-ADD-D.b:

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

7b. Exists i. g |- r ==> i					[ Canonical Forms, (o-reg, pb3), 1, 3 ]
7c. i = d							[ Lemma Deterministic-EO, 7b, p1 ]
contradiction - subcase does not apply
 * E-ADD-D.b complete






case E-ADD:
~~~~~~~~~~~
  g |- r ==> i1
  g |- o ==> i2
  (g,s){r<-i1+i2}(g',s')
  -------------------------------------- (e-add)
  (h,g,s,(add r,o; b2)) --> (h,g',s',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 ]

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


subcase on the structure of 5.

subcase E-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')

7a. Exists d. l = d 						[ Lemma S-arithmetic-d, pa2, 2 ]
8a. g |- r ==> d						[ Canonical Forms, (o-reg, pa1, 7a), 1, 3 ]
9a. i1 = d'							[ Lemma Deterministic-EO, 8a, p1 ]
contradiction - subcase does not apply
* E-ADD-D.a complete



subcase E-ADD.b:

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


7b. {};H;G |- (i1+i2) : int					[ o-int ]
8b. {};H;G |- (i1+i2) : G(r) 					[ 7b, pb3 ]
9b. {};H |- g[r <- i1+i2] : G					[ g-tp, 3, 8b ]

10b. s' = s and g' = g[r <- i1+i2]				[ Inversion on u-not-esp, p3, pb2 ]

2'. {};H |- s' : S						[ 2, 10b ]
3'. {};H |- g' : G						[ 9b, 10b ]

11b. |- (h,g',s',b2)						[ m-tp, 1, 2', 3', 4' ]
* E-ADD complete.







case E-SUB:
~~~~~~~~~~~

  g |- r ==> i1
  g |- o ==> i2
  (g,s){r<-i1-i2}(g',s')
  ------------------------------------ (e-sub)
  (h,g,s,(sub r,o; b)) --> (h,g',s',b)

as in subcase E-ADD.b
* E-SUB complete








case E-LOAD-P:				
~~~~~~~~~~~~~~

  g |- r2 ==> p
  h(p) = <w>
  (g,s){r1<-w}(g',s')
  ------------------------------------------- (e-load-p)
  (h,g,s,(load r1,[r2+0]; b2)) --> (h,g',s',b2)
  
a1. |- (h,g,s, load r1,[r2+0]; 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+0]; b2				[ Inversion of m-tp, a1 ]

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

subcase on the structure of 5.  
  
  
subcase E-LOAD-P.a:

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

7a. {};H;G |- r2 : HeapPtr(t)					[ o-reg, pa1 ]
8a. Exists p',w'. g|-r2==>p' and h(p')=<w'> and {};H;{}|-w':t   [ Canonical Forms, 7a, 1, 3 ]
9a. p' = p, w' = w						[ Lemma Deterministic-EO, p1, 8a, def of h ]
10a. {};H;G |- w : t						[ 8a, 9a, weakening on G ]
11a. g |- w ==> w						[ eo-w ]

2'. {};H |- s' : S'						[ Lemma A-U-Preservation, pa2, 9a, 10a, p3, 1, 2, 3 ]
3'. {};H |- g' : G'						

12a. |- (h,g',s',b2)						[ m-tp, 1, 2', 3', 4' ]
* E-LOAD-P.a complete


subcase E-LOAD-P.b:

  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')

7b. Exists d. l = d 						[ Lemma S-arithmetic-d, pb2, 2 ]
8b. g |- r2 ==> d						[ Canonical Forms, (o-reg, pa1, 7b), 1, 3 ]
9b. i1 = d							[ Lemma Deterministic-EO, 8b, p1 ]
contradiction - subcase does not apply
* E-LOAD-P.b complete


subcase E-LOAD-P.c: loading from an aliased location 

  G(r2) = Single(l)      
  S |- l : t
  |- (G,S){r1<-t}(G',S')
  ------------------------------------------------ (i-load-aliased)
  D;H |- (G;S){load r1,[r2+0]}(G';S')
 
7c. (l,t) in atoms(S)						[ Lemma S-lookup-atom, pc2 ]
8c. Exists p. l = p and H(p) = HeapPtr(t)			[ Lemma S-atom-in-stack, 2, 7c ]
    or Exists d,w. l = d and s(d) = w and {};H;{} |- w : t

subsubcase on 8c    

subsubcase E-LOAD-P.c1: loading from an aliased location that is really a heap location
a2c1. l = p
a3c1. H(p) = HeapPtr(t)

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

2'. {};H |- s' : S'						[ Lemma A-U-Preservation, pc3, 13c1, 14c1, p3, 1, 2, 3 ]
3'. {};H |- g' : G'						

15c1. |- (h,g',s',b2)						[ m-tp, 1, 2', 3', 4' ]
* E-LOAD-P.c1 complete

subsubcase E-LOAD-P.c2: loading from an aliased location that is really a stack location
a2c2. d,w. l = d
9c2. g |- r2 ==> d						[ Canonical Forms, (o-reg, pc1, a2c2), 1, 3 ]
10c2. d = p							[ Lemma Deterministic-EO, 9c2, p1 ]
contradiction - subcase does not apply
* E-LOAD-P.c2 complete

  
  
  
  
  

case E-LOAD-D:
~~~~~~~~~~~~~~

  g |- r2 ==> d
  s(d+i) = w
  (g,s){r1<-w}(g',s')
  ------------------------------------------- (e-load-d)
  (h,g,s,(load r1,[r2+i]; b2)) --> (h,g',s',b2)


a1. |- (h,g,s, load r1,[r2+0]; 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+0]; b2				[ Inversion of m-tp, a1 ]

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

subcase on the structure of 5.  
  
  
subcase E-LOAD-D.a:

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

7a. {};H;G |- r2 : HeapPtr(t)					[ o-reg, pa1 ]
8a. Exists p. g |- r2 ==> p  					[ Canonical Forms, 7a, 1, 3 ]
9a. p = d							[ Lemma Deterministic-EO, p1, 8a ]
contradiction - subcase does not apply
* E-LOAD-D.a complete



subcase E-LOAD-P.b:

  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')

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

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

2'. {};H |- s' : S'						[ Lemma A-U-Preservation, pc4, 11b, 12b, p3, 1, 2, 3 ]
3'. {};H |- g' : G'		

13b. |- (h,g',s',b2)						[ m-tp, 1, 2', 3', 4' ] 
* E-LOAD-P.b complete



subcase E-LOAD-D.c: loading from an aliased location 

  G(r2) = Single(l)      
  S |- l : t
  |- (G,S){r1<-t}(G',S')
  ------------------------------------------------ (i-load-aliased)
  D;H |- (G;S){load r1,[r2+0]}(G';S')
 
7c. (l,t) in atoms(S)						[ Lemma S-lookup-atom, pc2 ]
8c. Exists p. l = p and H(p) = HeapPtr(t)			[ Lemma S-atom-in-stack, 2, 7c ]
    or Exists d,w. l = d and s(d) = w and {};H;{} |- w : t

subsubcase on 8c   

subsubcase E-LOAD-D.c1: loading from an aliased location that is really a heap location
a2c1. l = p
9c1. g |- r2 ==> p						[ Canonical Forms, (o-reg, pc1, a2c1), 1, 3 ]
10c1. p = d							[ Lemma Deterministic-EO, p1, 9c1 ]
contradiction - subcase does not apply
* E-LOAD-D.c1 complete

subsubcase E-LOAD-D.c2: loading from an aliased location that is really a stack location
a2c2. d,w. l = d
a3c2. s(d) = w
a4c2. {};H;{} |- w : t

9c2. {};H;G |- w : t						[ a4c2, weakening on G ]
10c2. g |- w ==> w						[ eo-w ]

2'. {};H |- s' : S'						[ Lemma A-U-Preservation, pc3, 9c2, 10c2, p3, 1, 2, 3]
3'. {};H |- g' : G'		

11c2. |- (h,g',s',b2)						[ m-tp, 1, 2', 3', 4' ]
* E-LOAD-D.c2 complete







case E-STORE-P:
~~~~~~~~~~~~~~~

  g |- r1 ==> p
  g |- r2 ==> w'
  h(p) = <w>
  ------------------------------------------------- (e-store-p)
  (h,g,s,(store r1,[r2+0]; b2)) --> (h[p<-w'],g,s,b2)

a1. |- (h,g,s, store r1,[r2+0]; 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 |- store r1,[r2+0]; b2				[ Inversion of m-tp, a1 ]

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


subcase on the structure of 5.  


subcase E-STORE-P.a:

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

7a. {};H;G |- r1 : HeapPtr(t)					[ o-reg, pa1 ]
8a. {};H;{} |- p : HeapPtr(t)					[ Lemma EO-Type-Preservation, 7a, 3, p1 ]
9a. H(p) = HeapPtr(t)						[ Inspection of o-H-p, 8a ]

10a. {};H;G |- r2 : t						[ o-reg, pa2 ]
11a. {};H;{} |- w' : t						[ Lemma EO-Type-Preservation, 11a, 3, p2 ] 
12a. {};H;{} |- (h[p <- w'])(p) : t				[ 11a, def of h[p<-w'] ]

13a. {};H |- <(h[p <- w'])(p)> : HeapPtr(t)			[ v-hp, 12a ]
14a. Forall p' in dom(H) or dom(h). {}; H |- h(p') : H(p')	[ Inversion of h-tp, 1]
1'. |- h[p <- w'] : H						[ h-tp, 13a, 14a, 9a ]

15a. |- (h[p<-w'],g,s,b2)					[ m-tp, 1', 2, 3, 4' ]
* E-STORE-P.a complete	



subcase E-STORE-P.b:

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

7b. Exists d,d'. l = d and l' = d' and d' = d + i		[ Lemma S-arithmetic-d, pb3, 2 ]
8b. {};H;G |- r1 : Single(d)					[ o-reg, pb1, 7b ]
9b. g |- r1 ==> d						[ Canonical Forms, 8b, 1, 3 ]
10b. d = p							[ Lemma Deterministic-EO, p1, 9b ]
contradiction - subcase does not apply
* E-STORE-P.b complete



subcase E-STORE-P.c:
  
  G(r1) = Single(l)
  S |- l : t 
  G(r2) = t
  ------------------------------------- (i-store-aliased)
  D;H |- (G;S){store [r1+0],r2}(G;S)
  
7c. (l,t) in atoms(S)						[ Lemma S-lookup-atom, pc2 ]
8c. Exists p. l = p and H(p) = HeapPtr(t)			[ Lemma S-atom-in-stack, 2, 7c ]
    or Exists d,w. l = d and s(d) = w and {};H;{} |- w : t

subsubcase on 8c    

subsubcase E-STORE-P.c1: loading from an aliased location that is really a heap location
a2c1. l = p
a3c1. H(p) = HeapPtr(t)

9c. {};H;G |- r2 : t						[ o-reg, pc3 ]
10c. {};H;{} |- w' : t						[ Lemma EO-Type-Preservation, 9c, 3, p2 ] 
11c. {};H;{} |- (h[p <- w'])(p) : t				[ 10c, def of h[p<-w'] ]

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

14a. |- (h[p<-w'],g,s,b2)					[ m-tp, 1', 2, 3, 4']
* E-STORE-P.c1 complete

subsubcase E-LOAD-P.c2: loading from an aliased location that is really a stack location
a2c2. d,w. l = d
9c2. g |- r1 ==> d						[ Canonical Forms, (o-reg, pc1, a2c2), 1, 3 ]
10c2. d = p							[ Lemma Deterministic-EO, p1, 9c2 ]
contradiction - subcase does not apply
* E-STORE-P.c2 complete






case E-STORE-d:
~~~~~~~~~~~~~~~

  g |- r1 ==> d
  g |- r2 ==> w
  s' = s[d+i<-w]
  ------------------------------------------- (e-store-d)
  (h,g,s,(store r1,[r2+i]; b2)) --> (h,g,s',b2)

a1. |- (h,g,s, store r1,[r2+0]; 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 |- store r1,[r2+0]; b2				[ Inversion of m-tp, a1 ]

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

subcase on the structure of 5.  

subcase E-STORE-P.a:

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

7a. {};H;G |- r1 : HeapPtr(t)					[ o-reg, pa1 ]
8a. Exists p,w. g |- r1 ==> p 					[ Canonical Forms, 7a, 1, 3 ]
9a. p = d							[ Lemma Deterministic-EO, 8a, p1 ] 
contradiction - subcase does not apply
* E-STORE-D.a complete



subcase E-STORE-D.b:

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

7b. Exists d,d'. l = d and l' = d' and d' = d + i		[ Lemma S-arithmetic-d, pb3, 2 ]
8b. S |- d' <- t ~~> S'						[ pb4, 7b ]

9b. {};H;G |- r2 : t						[ o-reg, pb1 ]
10b  {};H;{} |- w : t						[ Lemma EO-Type-Preservation, 9b, 3, p2 ] 

2'. {};H |- s' : S'						[ Lemma S-Update-Stack, p3, 10b, 8b, 7b, 2 ]

11b. |- (h,g,s',b2)						[ m-tp, 1, 2', 3, 4' ]
* E-STORE-D.b complete



subcase E-STORE-P.c:
  
  G(r1) = Single(l)
  S |- l : t 
  G(r2) = t
  ------------------------------------- (i-store-aliased)
  D;H |- (G;S){store [r1+0],r2}(G;S)
  
7c. (l,t) in atoms(S)						[ Lemma S-lookup-atom, pc2 ]
8c. Exists p. l = p and H(p) = HeapPtr(t)			[ Lemma S-atom-in-stack, 2, 7c ]
    or Exists d,w. l = d and s(d) = w and {};H;{} |- w : t

subsubcase on 8c    

subsubcase E-STORE-D.c1: loading from an aliased location that is really a heap location
a2c1. l = p
9c1. g |- r2 ==> p						[ Canonical Forms, (o-reg, pc1, a2c1), 1, 3 ]
10c1. p = d							[ Lemma Deterministic-EO, p1, 9c1 [
contradiction - subcase does not apply
* E-LOAD-D.c1 complete

subsubcase E-LOAD-P.c2: loading from an aliased location that is really a stack location
a2c2. d,w. l = d
a3c2. s(d) = w
a4c2. {};H;{} |- w : t

9c2. S |- l <- t ~~> S						[ S-update-weak, pc2 ]
2'. {};H |- s' : S						[ Lemma S-Update-Stack, p3, a4c2, 9c2, 2 ]


10c2. |- (h,g,s',b2)						[ m-tp, 1, 2', 3, 4' ]
* E-STORE-D.b complete






case E-HEAPALLOC:
~~~~~~~~~~~~~~~~~

  g |- o ==> w
  p not in domain(h)
  h' = h,p-><w>
  (g,s){r<-p}(g',s')
  ---------------------------------------------- (e-heapalloc)
  (h,g,s,(heapalloc r = <o>;b2)) --> (h',g',s',b2)

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

let H' = H, p->HeapPtr(t)

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 r = <o>; b2				[ Inversion of m-tp, a1 ]

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

6. {};H;G |- o : t						[ Inversion of i-heapalloc, 5 ]

8. {};H;{} |- w : t						[ Lemma EO-Type-Preservation, 6, 3, p1 ]	
9. {};H |- <w> : HeapPtr(t)					[ v-hp, 8 ] 
10. {};H |- h'(p) : H'(p)					[ v-hp, 8, def of H', p3 ]
1'. |- h' : H'							[ h-tp, 1, 9, def of H', p3 ]

10. |- (G,S){r<-HeapPtr(t)}(G',S')				[ Inversion of i-heapalloc, 5 ]
11. G' = G[r <- HeapPtr(t)], S' = S				[ Inspection of a-not-esp, 10 ]
12. r != esp							[ Inversion of a-not-esp, 10 ]
13. g' = g[r<-p], s' = s					[ p4, Inspection of e-not-esp, 12 ]

2'. {};H' |- s' : S'						[ 2, 11, 13, weakening on H ]

14. {};H';{} |- p : H'(p)					[ o-p-H, def of H' ]
15. {};H';{} |- g'(r) : G'(r)					[ 14, 13, 11, def of H' ]
3'. {};H' |- g' : G'						[ 2, 11, 13, 15, weakening on H ]

16. |- (h',g',s',b2)						[ m-tp, 1', 2', 3', 4' ]
* E-HEAPALLOC complete








case E-JUMPIF0-FALSE:
~~~~~~~~~~~~~~~~~~~~~

  g |- r ==> i
  i != 0
  ---------------------------------------- (e-jumpif0-false)
  (h,g,s,(jumpif0 r,o;b2)) --> (h,g,s,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, inspection of i-jumpif0 ]
4'. {};H;G;S |- b2						[ Inversion of b-ins, 4, 5 ]

7. |- (h,g,s,b2)						[ m-tp, 1, 2, 3, 4' ]
* E-JUMPIF0-FALSE complete







case E-JUMPIF0-TRUE:
~~~~~~~~~~~~~~~~~~~~

  g |- r ==> 0
  g |- o ==> p[subst]
  h(p) = all[D'](G',S') b'
  ------------------------------------------------ (e-jumpif0-true)
  (h,g,s,(jumpif0 r,o;b2)) --> (h,g,s,b'[subst/D'])


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, Inspection of i-jumpif0 ]

6. G(r) = int							[ Inversion of i-jumpif0, 5 ]
7. {};H;G |- o : All[](G1,S1)
8. G => G1
9. S => S1	

10. Exists p', subst', D2, G3, S3.  g |- o ==> p'[subst']  	[ Canonical Forms, 7, 1, 3 ]
11. h(p') = all[D2](G3,S3) 
12. G1 = G3[subst/D2]  and S1 = S3[subst/D2] 

13. subst = subst' and p = p'					[ Lemma Deterministic-EO, p2, 10 ]
14. D' = D2, G' = G3, S' = S3					[ 11, p3, 13 ]

15. Forall p'' in dom(h) or dom(H). {}; H |- h(p'') : H(p'')	[ Inversion of h-tp, 1 ]
16. {};H |- h(p) : H(p)						[ 15, p3 ]
17. {};H |- all[D2](G3,S3) b' : All[D2](G3,S3)			[ Inspection of v-code, 16, 11, 13 ]
18. H |- all[D2](G3,S3)	b'					[ Inversion of v-code, 17 ]
19. D2;H;G3;S3 |- b'						[ Inversion of block-tp, 18 ]

20. {};H;G3[subst/D2];S3[subst/D2] |- b'[subst/D2]		[ Substitution Lemma, 19 ] 	

21. {};H;G1;S1 |- b'[subst/D']					[ 20, 12, 14 ]

22. {};H;G;S1 |- b'[subst/D']					[ Lemma RegFile-Weakening, 21, 8 ]
4'. {};H;G;S |- b'[subst/D']					[ Lemma Stack-Weakening, 22, 9 ]

23. |- (h,g,s,b'[subst/D']					[ m-tp, 1, 2, 3, 4' ]
*






case E-UNPACK:
~~~~~~~~~~~~~~

  g |- o ==> p
  (g,s){r<-p}(g',s')
  -------------------------------------------------- (e-unpack)
  (h,g,s,((L,r) = unpack(o);b2)) --> (h,g',s',b2[p/L])


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;S) (L,r) = unpack(o) (G;S)			[ Inversion of b-ins, 4, Inspection of i-jumpif0 ]

let G' = G[r<-Single(L)]
let S' = S /\ {L:t}

6. {};H;G |- o : HeapPtr(t)					[ Inversion of i-unpack, 5 ]
7. r != esp
8. L not in {}
9. L;H;G';S' |- b2

4'. {};H;G'[p/L];S'[p/L] |- b2[p/L]				[ Substitution Lemma, 9 ] 

11. g' = g[r<-p], s' = s					[ Inspection of e-not-esp, p2, 7 ]

12. Forall r'. {};H;{} |- g(r') : G(r')				[ Inversion of g-tp, 3 ]
13. {};H;{} |- p : Single(p)					[ o-p ]
14. {};H;{} |- p : (G'[p/L])(r)					[ def of G', def of G(r) ]
15. {};H;{} |- g'(r) : (G'[p/L])(r)				[ 14, 11 ]
3'. {};H |- g' : G'[p/L]					[ g-tp, 12, 15, def of G', 11 ]

17. Exists p',w. g |- o==>p' and h(p')=<w> and H(p')=HeapPtr(t) [ Canonical Forms, 6, 1, 3 ]
18. p = p'							[ Lemma Deterministic-EO, 17, p1 ]
19. Exists H'. H = {p -> HeapPtr(t)},H' 			[ def of H, 17, 18 ]
20. Exists l_t,Q. S = l_t:Q					[ def of S ]
21. {};{p -> HeapPtr(t)},H' |- s : l_t:Q			[ 2, 19, 20 ]
22. {};H |- s : (l_t : (Q /\ {p:t}))				[ s-alias, 21 ] 
2'. {};H |- s : S'[p/L]						[ 22, def of S' ]

24. |- (h,g',s',b2[p/L])					[ m-tp, 1, 2', 3', 4' ]





case E-JUMP:
~~~~~~~~~~~~

  g |- o ==> p[subst]
  h(p) = all[D](G,S) b
  --------------------------------------- (e-jump)
  (h,g,s,(jump o)) --> (h,g,s,b[subst/D])

as in case E-JUMPIF0-TRUE
* E-JUMP complete