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

Notation:
  S = l:Q
  Q = P | Empty | t::S | Q /\ {l:t}
  O = P | Empty | t::S

  atoms(l:P) = {}
  atoms(l:Empty) = {}
  atoms(l:t::S) = atoms(S),(l,t)
  atoms(l:Q /\ {lt:t}) = atoms(l:Q),(lt,t)

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

LEMMA [S-IMP2-YIELD]

    if S =>> S' yielding LMap
  then LMap = atoms(S)

Proof by induction on S =>> S'.

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

LEMMA [S-IMP-DUPLICATE-ALIAS]:  l:(Q /\ {lt:t}) => l:((Q /\ {lt:t}) /\ {lt:t})

  l:(Q /\ {lt:t}) => l:(Q /\ {lt:t})
  l:(Q /\ {lt:t}) => l:(Q /\ {lt:t})
  ---------------------------------------------- (S-imp-merge-alias)
  l:(Q /\ {lt:t}) => l:((Q /\ {lt:t}) /\ {lt:t})

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

LEMMA [S-IMP-SWAP-ALIAS]:  l:((Q /\ {l1:t1}) /\ {l2:t2}) => l:((Q /\ {l2:t2}) /\ {l1:t1})

  l:(Q /\ {l1:t1})              => l:Q
  ------------------------------------------------- (S-imp-alias)
  l:((Q /\ {l1:t1}) /\ {l2:t2}) => l:(Q /\ {l2:t2})
  l:((Q /\ {l1:t1}) /\ {l2:t2}) => l:(Q /\ {l1:t1})
  -------------------------------------------------------------- (S-imp-merge-alias)
  l:((Q /\ {l1:t1}) /\ {l2:t2}) => l:((Q /\ {l2:t2}) /\ {l1:t1})

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

LEMMA [S-IMP2-IMP]:
    if S =>> l:Q yielding LMap
  then S => l:Q
   and forall (l',t') in LMap, S => l:(Q /\ {l':t'})

Proof by induction on S =>> l:Q yielding LMap

CASES
  l:P =>> l:P yielding {}  (S-imp2-P)
  l:Empty =>> l:Empty yielding {}  (S-imp2-empty)

  By rule S => S  (S-imp-eq)

CASE
  S1 =>> l2:Q2 yielding LMap
  ------------------------------------------ (S-imp2-concat)
  l:t::S1 =>> l:t::l2:Q2 yielding LMap,(l,t)

  By induction, S1 => l2:Q2
    and forall (l',t') in LMap, S1 => l2:(Q2 /\ {l':t'})

  By rule, l:t::S1 => l:t::l2:Q2  (S-imp-concat)

  For each (l',t') in LMap:
         S1 =>       l2:(Q2 /\ {l':t'})
    ------------------------------------ (S-imp-concat)
    l:t::S1 => l:(t::l2:(Q2 /\ {l':t'}))
               l:(t::l2:(Q2 /\ {l':t'})) => l:((t::l2:Q2) /\ {l':t'}) (S-imp-expand-alias)
    ----------------------------------------------------------------- (S-imp-trans)
    l:t::S1                              => l:((t::l2:Q2) /\ {l':t'})

  For (l,t):
         S1 =>       l2:Q2
    ----------------------- (S-imp-concat)
    l:t::S1 => l:(t::l2:Q2)
               l:(t::l2:Q2) => l:((t::l2:Q2) /\ {l:t}) (S-imp-add-alias)
    -------------------------------------------------- (S-imp-trans)
    l:t::S1                 => l:((t::l2:Q2) /\ {l:t})

CASE
  l':Q =>> l':O yielding LMap
  -------------------------------------------- (S-imp2-alias-left)
  l':(Q /\ {l:t}) =>> l':O yielding LMap,(l,t)

  By induction, l':Q => l':O
   and forall (l'',t'') in LMap, l':Q => l':(O /\ {l'':t''})

  l':(Q /\ {l:t}) => l':Q         (s-imp-drop-alias)
                     l':Q => l':O
  ------------------------------- (s-imp-trans)
  l':(Q /\ {l:t})         => l':O

  For each (l'',t'') in LMap:
    l':(Q /\ {l:t}) => l':Q                        (s-imp-drop-alias)
                       l':Q => l':(O /\ {l'':t''})
    ---------------------------------------------- (s-imp-trans)
    l':(Q /\ {l:t})         => l':(O /\ {l'':t''})

  For (l,t):
    l':Q                    => l':O
    ------------------------------------------ (s-imp-alias)
    l':(Q /\ {l:t})         => l':(O /\ {l:t})

CASE
  S =>> l':Q' yielding LMap,(l,t)
  ------------------------------------------ (S-imp2-alias-right)
  S =>> l':(Q' /\ {l:t}) yielding LMap,(l,t)

  By induction, S => l':Q'
   and forall (l'',t'') in (LMap,(l,t)), S => l':(Q' /\ {l'':t''})

  Since (l,t) is in (LMap,(l,t)), S => l':(Q' /\ {l:t})

  For each (l'',t'') in LMap:
    S => l':(Q' /\ {l:t})
    S => l':(Q' /\ {l'':t''})
    ------------------------------------ (S-imp-merge-alias)
    S => l':((Q' /\ {l:t}) /\ {l'':t''})

  For (l,t):
    S => l':(Q' /\ {l:t})
    S => l':(Q' /\ {l:t})
    -------------------------------- (S-imp-merge-alias)
    S => l':((Q' /\ {l:t}) /\ {l:t})

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

LEMMA [S-IMP2-LMAP-EQ]:
    if S =>> S1 yielding LMap1
   and S =>> S2 yielding LMap2
  then LMap1 = LMap2

By S-IMP2-YIELD, atoms(S) = LMap1.
By S-IMP2-YIELD, atoms(S) = LMap2.

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

LEMMA [S-IMP2-ALIAS-LEFT-Q]:
    if l':Q =>> l':Q' yielding LMap
  then l':(Q /\ {l:t}) =>> l':Q' yielding LMap,(l,t)
(i.e. the following rule is admissible:
  l':Q =>> l':Q' yielding LMap
  --------------------------------------------- [S-IMP2-ALIAS-LEFT-Q]
  l':(Q /\ {l:t}) =>> l':Q' yielding LMap,(l,t)
)

Proof by induction on Q'

CASE Q' = O

  l':Q =>> l':O yielding LMap
  -------------------------------------------- (s-imp2-alias-left)
  l':(Q /\ {l:t}) =>> l':O yielding LMap,(l,t)

CASE Q' = Q'' /\ {l'':t''}

  We know:
    l':Q =>> l':(Q'' /\ {l'':t''}) yielding LMap
  This can only be generated by the following rule:
    l':Q =>> l':Q'' yielding LMap'',(l'',t'')
    -------------------------------------------------------- (s-imp2-alias-right)
    l':Q =>> l':(Q'' /\ {l'':t''}) yielding LMap'',(l'',t'')
  where LMap = LMap'',(l'',t'')

  By induction:
    l':Q =>> l':Q'' yielding LMap'',(l'',t'')
    ---------------------------------------------------------- (induction)
    l':(Q /\ {l:t}) =>> l':Q'' yielding LMap'',(l'',t''),(l,t)

  By rule:
    l':(Q /\ {l:t}) =>> l':Q'' yielding LMap'',(l,t),(l'',t'')
    ------------------------------------------------------------------------- (s-imp2-alias-right)
    l':(Q /\ {l:t}) =>> l':(Q'' /\ {l'':t''}) yielding LMap'',(l,t),(l'',t'')
  So:
    l':(Q /\ {l:t}) =>> l':Q' yielding LMap,(l,t)

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

LEMMA [S-IMP2-EQ]: S =>> S yielding LMap, for some LMap

Proof by induction on S.

CASE S = l:P or S = l:Empty
  S =>> S yielding {}  (s-imp2-P, s-imp2-empty)

CASE S = l:t::S'
  By induction, S' =>> S' yielding LMap'
  By rule:
    S' =>> S' yielding LMap'
    ---------------------------------------- (s-imp2-concat)
    l:t::S' =>> l:t::S' yielding LMap',(l,t)

CASE S = l':(Q /\ {l:t})
  By induction, l':Q =>> l':Q yielding LMap'

  l':Q =>> l':Q yielding LMap
  -------------------------------------------- [S-IMP2-ALIAS-LEFT-Q]
  l':(Q /\ {l:t}) =>> l':Q yielding LMap,(l,t)
  ------------------------------------------------------- (s-imp2-alias-right)
  l':(Q /\ {l:t}) =>> l':(Q /\ {l:t}) yielding LMap,(l,t)

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

LEMMA [S-IMP2-LABEL-EQ]
    if l1:Q1 =>> l2:Q2 yielding LMap
  then l1 = l2

Proof by induction on derivation of l1:Q1 =>> l2:Q2.

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

LEMMA [S-IMP2-TRANS]:
    if S1 =>> S2 yielding LMap1
   and S2 =>> S3 yielding LMap2
  then S1 =>> S3 yielding LMap1 U LMap2

Proof by induction on sum of sizes of derivations of:
       S1 =>> S2 yielding LMap1
   and S2 =>> S3 yielding LMap2

There are 5 cases for the root of each derivation; call these 1,2,3,4,5.
There are 25 total potential cases (not all of which are legal); call
these 11,12,13,14,15,21,22,...,54,55.

CASES 15 25 35 45 55
    S2 =>> l3:Q3 yielding LMap,(l,t)
    ------------------------------------------- (s-imp2-alias-right)
    S2 =>> l3:(Q3 /\ {l:t}) yielding LMap,(l,t)
  where LMap2 = LMap,(l,t)

  By induction, S1 =>> l3:Q3 yielding LMap1 U (LMap,(l,t))
    S1 =>> l3:Q3 yielding LMap1 U (LMap,(l,t))
    ----------------------------------------------------- (s-imp2-alias-right)
    S1 =>> l3:(Q3 /\ {l:t}) yielding LMap1 U (LMap,(l,t))

CASES 41 42 43 44
    l':Q1 =>> l':O2 yielding LMap
    ---------------------------------------------- (s-imp2-alias-left)
    l':(Q1 /\ {l:t}) =>> l':O2 yielding LMap,(l,t)
  where S1 = l':(Q1 /\ {l:t}) and S2 = l':O2 and LMap1 = LMap,(l,t)

  By induction, l':Q1 =>> S3 yielding LMap U LMap2
    l':Q1 =>> S3 yielding LMap U LMap2
    ----------------------------------------------------- [S-IMP2-ALIAS-LEFT-Q, S-IMP2-LABEL-EQ]
    l':(Q1 /\ {l:t}) =>> S3 yielding (LMap U LMap2),(l,t)

CASE 54
    S1 =>> l':Q2 yielding LMap1',(l,t)
    --------------------------------------------- (s-imp2-alias-right)
    S1 =>> l':(Q2 /\ {l:t}) yielding LMap1',(l,t)

    l':Q2 =>> l':O3 yielding LMap2'
    ------------------------------------------------ (s-imp2-alias-left)
    l':(Q2 /\ {l:t}) =>> l':O3 yielding LMap2',(l,t)

  By induction, S1 =>> l':O3 yielding (LMap1',(l,t)) U LMap2'
  LMap1 U LMap2 = (LMap1',(l,t)) U (LMap2',(l,t)) = (LMap1',(l,t)) U LMap2'

CASE 11: S1 = l:P and S2 = l:P and S3 = l:P (easy case)

CASE 22: S1 = l:Empty and S2 = l:Empty and S3 = l:Empty (easy case)

CASE 33
    S1' =>> S2' yielding LMap1'
    ------------------------------------------- (s-imp2-concat)
    l:t::S1' =>> l:t::S2' yielding LMap1',(l,t)

    S2' =>> S3' yielding LMap2'
    ------------------------------------------- (s-imp2-concat)
    l:t::S2' =>> l:t::S3' yielding LMap2',(l,t)

  By induction, S1' =>> S3' yielding LMap1' U LMap2'

    S1' =>> S3' yielding LMap1' U LMap2'
    ------------------------------------------------------ (s-imp2-concat)
    l:t::S1' =>> l:t::S3' yielding (LMap1' U LMap2'),(l,t)

CASES 12 21 13 31 23 32: impossible

CASES 51 52 53: impossible

CASES 14 24 34: impossible

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

LEMMA [S-IMP-IMP2]:
    if S => S'
  then S =>> S' yielding LMap, for some LMap

Proof by induction on S => S'

CASE
  S => S  (s-imp-eq)

  By lemma [S-IMP2-EQ], S =>> S yielding LMap

CASE 
  S1 => S2
  S2 => S3
  -------- (s-imp-trans)
  S1 => S3

  By induction, S1 =>> S2 yielding LMap1
  By induction, S2 =>> S3 yielding LMap2
  By lemma [S-IMP2-TRANS], S1 =>> S3 yielding LMap1 U LMap2

CASE
  S => S'
  --------------------- (s-imp-concat)
  l:(t::S) => l:(t::S')

  By induction, S =>> S' yielding LMap

  S =>> S' yielding LMap
  --------------------------------------- (s-imp2-concat)
  l:t::S =>> l:t::S' yielding LMap,(l,t)

CASE
  l':Q => l':Q'
  ----------------------------------- (s-imp-alias)
  l':(Q /\ {l:t}) => l':(Q' /\ {l:t})

  By induction, l:Q =>> l:Q' yielding LMap

  l':Q =>> l':Q' yielding LMap
  -------------------------------------------- [S-IMP2-ALIAS-LEFT-Q]
  l':(Q /\ {l:t}) =>> l':Q' yielding LMap,(l,t)
  -------------------------------------------------------- (s-imp2-alias-right)
  l':(Q /\ {l:t}) =>> l':(Q' /\ {l:t}) yielding LMap,(l,t)

CASE
  l:(t::S) => l:(t::S /\ {l:t})  (s-imp-add-alias)

  S =>> S yielding LMap  (by lemma[S-IMP2-EQ])
  ----------------------------------------- (s-imp2-concat)
  l:(t::S) =>> l:(t::S) yielding LMap,(l,t)
  -------------------------------------------------- (s-imp2-alias-right)
  l:(t::S) =>> l:(t::S /\ {l:t}) yielding LMap,(l,t)

CASE
  l:(t1::lq:(Q /\ {l2:t2})) => l:((t1::lq:Q) /\ {l2:t2})  (s-imp-expand-alias)

  lq:Q =>> lq:Q yielding LMap (by lemma)
  ------------------------------------------------ [S-IMP2-ALIAS-LEFT-Q]
  lq:(Q /\ {l2:t2}) =>> lq:Q yielding LMap,(l2:t2)
  ----------------------------------------------------------------------- (s-imp2-concat)
  l:(t1::lq:(Q /\ {l2:t2})) =>> l:(t1::lq:Q) yielding LMap,(l2:t2),(l:t1)
  ------------------------------------------------------------------------------------ (s-imp2-alias-right)
  l:(t1::lq:(Q /\ {l2:t2})) =>> l:((t1::lq:Q) /\ {l2:t2}) yielding LMap,(l2:t2),(l:t1)

CASE
  l:(Q /\ {lt:t}) => l:Q  (s-imp-drop-alias)

  l:Q =>> l:Q yielding LMap (by lemma)
  -------------------------------------------- [S-IMP2-ALIAS-LEFT-Q]
  l:(Q /\ {lt:t}) =>> l:Q yielding LMap,(lt:t)

CASE
  S => l:(Q /\ {l1:t1})
  S => l:(Q /\ {l2:t2})
  ---------------------------------- (s-imp-merge-alias)
  S => l:((Q /\ {l1:t1}) /\ {l2:t2})

  By induction:
    S =>> l:(Q /\ {l1:t1}) yielding LMap1
    S =>> l:(Q /\ {l2:t2}) yielding LMap2
  By lemma [S-IMP2-LMAP-EQ], LMap1 = LMap2, so:
    S =>> l:(Q /\ {l1:t1}) yielding LMap2

  Only one rule can conclude S =>> l:(Q /\ {l2:t2}) yielding LMap2:
    S =>> l:Q yielding LMap2'
    ---------------------------------------------- (s-imp2-alias-right)
    S =>> l:(Q /\ {l2:t2}) yielding LMap2',(l2:t2)
  where LMap2 = LMap2',(l2:t2)

  S =>> l:(Q /\ {l1:t1}) yielding LMap2',(l2:t2)
  ----------------------------------------------------------- (s-imp2-alias-right)
  S =>> l:((Q /\ {l1:t1}) /\ {l2:t2}) yielding LMap2',(l2:t2)

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

LEMMA [S-IMP-LABEL-EQ]
    if l1:Q1 => l2:Q2
  then l1 = l2

Proof by S-IMP-IMP2 and S-IMP2-LABEL-EQ

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

LEMMA [S-SIZE-LABEL]
    if D;H |- s : l:Q
  then l = size(s)

Proof by induction on D;H |- s : l:Q

CASE
  D;H |- empty : (base:Empty)   (s-base)
  base = size(empty)

CASE
  D;H,{p->HeapPtr(t)} |- s : (l:Q)
  -------------------------------------------(s-alias)
  D;H,{p->HeapPtr(t)} |- s : (l:(Q /\ {p:t}))

  By induction, l = size(s)

CASE
  D;H |- s : l:Q
  D;H;{} |- w : t
  ---------------------------- (s-concat)
  D;H |- w::s : next(l):t::l:Q

  By induction, l = size(s), so next(l) = size(w::s)

CASE
  D;H |- s : l:Q
  l:Q => l':Q'
  ---------------- (s-imp)
  D;H |- s : l':Q'

  By induction, l = size(s).
  By S-IMP-LABEL-EQ, l' = l.

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

LEMMA [S-IMP-ATOMS-SUBSET]
    if S => S'
  then atoms(S') subsetof atoms(S)

Proof by induction on S => S'.

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

LEMMA [S-ATOM-IN-STACK]
    if {};H |- s : S
   and (l,t) in atoms(S)
  then either:
    1) there exists p so that:
         l = p
         H(p) = HeapPtr(t)
   or
    2) there exists d and w so that:
         l = d
         s(d) = w
         {};H;{} |- w : t

CASE
    D;H |- empty : (base:Empty)   (s-base)
  impossible case: atoms(Empty) = {}

CASE
    {};H,{p1->HeapPtr(t1)} |- s : (l1:Q1)
    --------------------------------------------------(s-alias)
    {};H,{p1->HeapPtr(t1)} |- s : (l1:(Q1 /\ {p1:t1}))

  (l,t) in atoms(l1:(Q1 /\ {p1:t1}))
  (l,t) in atoms(l1:Q1) U {(p1,t1)}

  If (l,t) = (p1,t1), then l = p1 and (H,{p1->HeapPtr(t1)})(p1) = HeapPtr(t)

  Otherwise, (l,t) in atoms(l1:Q1), so conclusion follows by induction.

CASE
    {};H |- s : l1:Q1
    {};H;{} |- w1 : t1
    ---------------------------------- (s-concat)
    {};H |- w1::s : next(l1):t1::l1:Q1

  (l,t) in atoms(next(l1):t1::l1:Q1)
  (l,t) in atoms(l1:Q1) U {(next(l1),t1)}

  If (l,t) = (next(l1),t1) then
    l = next(l1)
    {};H;{} |- w1 : t1
    By S-SIZE-LABEL, size(w1::s) = next(l1)
    By s-lookup-top, (w1::s)(next(l1)) = w1

  Otherwise, (l,t) in atoms(l1:Q1), so by induction, either:
    1) l = p and H(p) = HeapPtr(t)
    2) l = d and s(d) = w and {};H;{} |- w : t
      By s-lookup, (w1::s)(d) = w

CASE
    {};H |- s : S
    S => S'
    -------------- (s-imp)
    {};H |- s : S'

  (l,t) in atoms(S')
  By S-IMP-ATOMS-SUBSET, (l,t) in atoms(S)
  Conclusion follows by induction.

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

LEMMA [S-ALIAS-IN-STACK]
    if {};H |- s : S
   and S => l':(Q /\ {l:t})
  then either:
    1) there exists d so that:
         l = p
         H(p) = HeapPtr(t)
   or
    2) forall G, there exists d and w so that:
         l = d
         s(d) = w
         {};H;{} |- w : t

(l,t) in atoms(l':(Q /\ {l:t}))
By S-IMP-ATOMS-SUBSET, (l,t) in atoms(S).
Conclusion follows by S-ATOM-IN-STACK.

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

LEMMA [S-LOOKUP-ATOM]
    if S |- l : t
  then (l,t) in atoms(S)

By inverting S-lookup, S => l':(Q /\ {l:t})
(l,t) in atoms(l':(Q /\ {l:t}))
By S-IMP-ATOMS-SUBSET, (l,t) in atoms(S).

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

LEMMA [S-UPDATE-ATOM]
    if S |- l <- t' ~~> S'
  then Exists t. (l,t) in atoms(S)

Proof by cases on S |- l <- t' ~~> S'

CASE (S-update-weak)
  S |- l : t'
  By S-LOOKUP-ATOM, (l,t') in atoms(S).

CASE (S-update-strong)
  S => T @ (l:t::S')
  (l,t) in atoms(T @ (l:t::S'))
  By S-IMP-ATOMS-SUBSET, (l,t) in atoms(S).

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

LEMMA [S-NO-ATOMS-BEYOND-SIZE]
    if D;H |- s : S
  then (next^(n+1)(size(s)),t) not in atoms(S)

Proof by induction on D;H |- s : S

CASE
    D;H |- empty : (base:Empty)   (s-base)
  atoms(empty) = {}

CASE
    D;H,{p->HeapPtr(t)} |- s : (l:Q)
    -------------------------------------------(s-alias)
    D;H,{p->HeapPtr(t)} |- s : (l:(Q /\ {p:t}))

  By induction, (next^(n+1)(size(s)),t) not in atoms(l:Q)
  Since p and next^(n+1)(size(s)) are syntactically distinct,
    (next^(n+1)(size(s)),t) not in atoms(l:(Q /\ {p:t}))

CASE
    D;H |- s : l:Q
    D;H |- w : t'
    ----------------------------- (s-concat)
    D;H |- w::s : next(l):t'::l:Q
  By induction (choosing n appropriately),
    (next^(n+2)(size(s)),t) not in atoms(l:Q)
  So
    (next^(n+1)(size(w::s)),t) not in atoms(l:Q)
  By S-SIZE-LABEL, next(l) = size(w::s)
  So next(l) != next^(n+1)(size(w::s))
  So (next^(n+1)(size(w::s)),t) not in atoms(l:Q) U {(next(l),t')}
  So (next^(n+1)(size(w::s)),t) not in atoms(next(l):t'::l:Q)

CASE
    D;H |- s : S
    S => S'
    ------------- (s-imp)
    D;H |- s : S'
  By induction, (next^(n+1)(size(s)),t) not in atoms(S)
  By S-IMP-ATOMS-SUBSET, (next^(n+1)(size(s)),t) not in atoms(S')

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

LEMMA [S-UPDATE-ATOM-IN-STACK]
    if s' = s[d<-w']
   and D;H;{} |- w' : t
   and (d,t) in atoms(S)
   and D;H |- s : S
  then D;H |- s' : S

Proof by induction on D;H |- s : S.

CASE
    D;H |- empty : (base:Empty)   (s-base)

  impossible case: s' = empty[d<-w'] cannot hold

CASE
    D;H,{p->HeapPtr(t')} |- s : (l':Q')
    -----------------------------------------------(s-alias)
    D;H,{p->HeapPtr(t')} |- s : (l':(Q' /\ {p:t'}))

  (d,t) in atoms(l':(Q' /\ {p:t'}))
  (d,t) in atoms(l':Q') U {(p,t')}
  Since d and p are syntactically distinct, (d,t) in atoms(l':Q')
  By induction, D;H,{p->HeapPtr(t')} |- s' : (l':Q')
  By s-alias,   D;H,{p->HeapPtr(t')} |- s' : (l':(Q' /\ {p:t'}))

CASE
    D;H |- s'' : l:Q
    D;H;{} |- w'' : t''
    ----------------------------------- (s-concat)
    D;H |- w''::s'' : next(l):t''::l:Q

  If size(w''::s'') = d, then:
    w'::s'' = (w''::s'')[size(w''::s'')<-w'] (s-assign-top)
    So s' = w'::s''
    By S-NO-ATOMS-BEYOND-SIZE, (next(size(s'')),t) not in atoms(l:Q)
    So (d,t) not in atoms(l:Q)
    Since (d,t) in atoms(next(l):t''::l:Q) = atoms(l:Q) U {(next(l),t'')}, we know t = t''
    So D;H;{} |- w' : t''
    By s-concat, D;H |- w'::s'' : next(l):t''::l:Q

  Otherwise:
      s''' = s''[d<-w']
      -----------------------------       (s-assign)
      w''::s''' = (w''::s'')[d<-w']
    where s' = w''::s'''
    By induction, D;H |- s''' : l:Q
    By s-concat, D;H |- w''::s''' : next(l):t''::l:Q

CASE
    D;H |- s : S
    S => S'
    -------------- (s-imp)
    D;H |- s : S'

  (d,t) in atoms(S')
  By S-IMP-ATOMS-SUBSET, (d,t) in atoms(S).
  By induction, D;H |- s' : S
  By s-imp, D;H |- s' : S'

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

LEMMA [S-UPDATE-IN-STACK]
    if s' = s[d<-w']
   and D;H;{} |- w' : t
   and S => l:(Q /\ {d:t})
   and D;H |- s : S
  then D;H |- s' : S

(d,t) in atoms(l:(Q /\ {d:t}))
By S-IMP-ATOMS-SUBSET, (d,t) in atoms(S).
Conclusion follows by S-UPDATE-ATOM-IN-STACK.

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

LEMMA [S-UPDATE-STACK-STRONG]
    if s' = s[d<-w']
   and D;H;{} |- w' : t'
   and S => T @ (d:t::S')
   and D;H |- s : S
  then D;H |- s' : T @ (d:t'::S')

Proof by induction on {};H |- s : S

CASE
    D;H |- empty : (base:Empty)   (s-base)

  S = base:Empty
  So base:Empty => T @ (d:t::S')
  By S-IMP-IMP2, base:Empty =>> T @ (d:t::S') yielding LMap
  No s-imp2 rule can prove this, so this case is impossible

CASE
    D;H,{p->HeapPtr(t)} |- s : (l:Q)
    -------------------------------------------(s-alias)
    D;H,{p->HeapPtr(t)} |- s : (l:(Q /\ {p:t}))

  S = l:(Q /\ {p:t})
  So l:(Q /\ {p:t}) => T @ (d:t::S')
  By S-IMP-IMP2, l:(Q /\ {p:t}) =>> T @ (d:t::S') yielding LMap
  Only S-imp2-alias-left can prove this, so l:Q =>> T @ (d:t::S') yielding LMap'
  By S-IMP2-IMP, l:Q => T @ (d:t::S')
  Conclusion follows by induction

CASE
    D;H |- s : l:Q
    D;H;{} |- w : tq
    ----------------------------- (s-concat)
    D;H |- w::s : next(l):tq::l:Q

  S = next(l):tq::l:Q

  If T = () then
    next(l):tq::l:Q => d:t::S'
    By S-IMP-IMP2, next(l):tq::l:Q =>> d:t::S' yielding LMap
    Only S-imp2-concat can prove this, so t = tq and d = next(l) and l:Q = S'
    D;H |- w::s : d:t::S'
    By S-SIZE-LABEL, d = size(w::s)
    Therefore w'::s = (w::s)[d<-w']

    D;H |- s : S'
    By s-concat, D;H |- w'::s : d:t'::S'

  Otherwise T = (t'');T'
    next(l):tq::l:Q => (t'');T' @ d:t::S'
    By S-IMP-IMP2, next(l):tq::l:Q =>> (t'');T' @ d:t::S' yielding LMap
    Only S-imp2-concat can prove this, so t'' = tq and l:Q =>> T' @ d:t::S' yielding LMap'
    By S-IMP2-IMP, l:Q => T' @ d:t::S'
    By s-imp, D;H |- s : T' @ d:t::S'
    By S-NO-ATOMS-BEYOND-SIZE, (next^(n+1)(size(s)),tn) not in atoms(T' @ d:t::S')
    So next^(n+1)(size(s)) != d
    So size(w::s) != d
    We know s' = (w::s)[d<-w']
    Since size(w::s) != d, only s-assign can prove s' = (w::s)[d<-w']
    Therefore, for some w'', s'' = s[d<-w']
    By s-assign, w::s'' = (w::s)[d<-w']
    By induction, D;H |- s'' : T' @ (d:t'::S')
    By s-concat, D;H |- w::s'' : (tq);T' @ (d:t'::S')
    So D;H |- (w::s)[d<-w'] : (t'');T' @ (d:t'::S')

CASE
    D;H |- s : S''
    S'' => S
    -------------- (s-imp)
    D;H |- s : S

  By s-imp-trans, S'' => T @ (d:t::S')
  Conclusion follows by induction

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

LEMMA [S-UPDATE-STACK]
    if s' = s[d<-w']
   and D;H;{} |- w' : t
   and S |- d <- t ~~> S'
   and D;H |- s : S
  then D;H |- s' : S'

Proof by cases on S |- d <- t ~~> S'

CASE
    S |- d : t
    -------------------- (S-update-weak)
    S |- d <- t ~~> S
  S' = S
  Only S-lookup can prove S |- d : t, so S => l:(Q /\ {d:t})
  By S-UPDATE-IN-STACK, D;H |- s' : S

CASE
    S => T @ (d:t::S')
    ------------------------------- (S-update-strong)
    S |- d <- t' ~~> T @ (d:t'::S')
  By S-UPDATE-STACK-STRONG, D;H |- s' : T @ (d:t'::S')

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

LEMMA [S-CONCAT-d]
    if S => T @ (l':Q')
   and D;H |- s : S
  then Exists d. l' = d

Proof by induction on D;H |- s : S

CASE
    D;H |- empty : (base:Empty)   (s-base)
  S = base:Empty
  base:Empty => T @ (l':Q')
  By S-IMP-IMP2, base:Empty =>> T @ (l':Q') yielding LMap
  Only S-imp2-empty can prove this, so T @ (l':Q') = base:Empty
  So l' = base

CASE
    D;H,{p->HeapPtr(t)} |- s : (l:Q)
    -------------------------------------------(s-alias)
    D;H,{p->HeapPtr(t)} |- s : (l:(Q /\ {p:t}))
  S = l:(Q /\ {p:t})
  l:(Q /\ {p:t}) => T @ (l':Q')

  If T = () then
    l:(Q /\ {p:t}) => l':Q'
    By s-imp, D;H,{p->HeapPtr(t)} |- s : l':Q'
    By S-SIZE-LABEL, l' = size(s)

  Otherwise, T = (t'');T'
    l:(Q /\ {p:t}) => l'':t''::(T' @ (l':Q'))
    By S-IMP-IMP2, l:(Q /\ {p:t}) =>> l'':t''::(T' @ (l':Q')) yielding LMap
    Only s-imp2-alias-left can prove this, so
      l:Q =>> l'':t''::(T' @ (l':Q')) yielding LMap'
    Conclusion follows by induction

CASE
    D;H |- s : l:Q
    D;H;{} |- w : t
    ---------------------------- (s-concat)
    D;H |- w::s : next(l):t::l:Q

  If T = () then
    next(l):t::l:Q => l':Q'
    By s-imp, D;H |- w::s : l':Q'
    By S-SIZE-LABEL, l' = size(w::s)

  Otherwise, T = (t'');T'
    next(l):t::l:Q => l'':t''::(T' @ (l':Q'))
    By S-IMP-IMP2, next(l):t::l:Q =>> l'':t''::(T' @ (l':Q')) yielding LMap
    Only S-imp2-concat can prove this, so l:Q =>> T' @ (l':Q') yielding LMap'
    Conclusion follows by induction

CASE
    D;H |- s : S'
    S' => S
    ------------- (s-imp)
    D;H |- s : S

  By S-imp-trans, S' => T @ (l':Q')
  Conclusion follows by induction

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

LEMMA [S-ARITHMETIC-d]
    if S |- l + i = l'
   and D;H |- s : S
  then Exists d, d'. l = d and l' = d' and d + i = d'

Proof by cases on S |- l + i = l'

judgment: S |- l + i = l'

CASE
    S => T @ (l:Q)
    ----------------------  (S-offset-next)
    S |- l + n = next^n(l)

  By S-CONCAT-d, Exists d. l = d
  l' = next^n(l) = next^n(d) = d'
  d + n = next^n(d) = d'

CASE
    S => T @ (l':Q)
    ------------------------  (S-offset-prev)
    S |- next^n(l') - n = l'

  By S-CONCAT-d, Exists d'. l' = d'
  l = next^n(l') = next^n(d') = d
  d + (-n) = next^n(d') + (-n) = d'

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

LEMMA [S-RESIZE-d]
    if |- Resize(l',S) = S'
   and D;H |- s : S
  then Exists d. l' = d

Proof by cases on |- Resize(l',S) = S'

CASE
    S => T @ (l':Q')
    ----------------------- (S-shrink)
    |- Resize(l',S) = l':Q'

  Conclusion follows by S-CONCAT-d

CASE 
    |- Resize(next^n(l),l:Q) = (Nonsense_n;...;Nonsense_1) @ (l:Q)  (S-grow)
  where S = l:Q and l' = next^n(l)

  D;H |- s : (l:Q)
  By S-SIZE-LABEL, l = size(s)
  Therefore l' = next^n(size(s))

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

LEMMA [s-LOOKUP-UPDATE]
    if s(d) = w
  then Exists s'. s' = s[d<-w']

Proof by induction on s(d) = w

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

LEMMA [S-s-RESIZE-SHRINK]
    if D;H |- s : S
   and S => T @ (d':Q')
  then D;H |- resize(d',s) : d':Q'
   and Exists n. size(s) = d' + n

Proof by induction on D;H |- s : S

CASE T = ()
  S => d':Q'
  By s-imp, D;H |- s : (d':Q')
  By S-SIZE-LABEL, d' = size(s)
  resize(d',s) = resize(size(s),s) = s
  D;H |- resize(d',s) : S
  By s-imp, D;H |- resize(d',s) : (d':Q')

CASE T = (t'');T' and
    D;H |- empty : (base:Empty)   (s-base)

  S = base:Empty
  base:Empty => (t'');T' @ (d':Q')
  By S-IMP-IMP2, base:Empty =>> (t'');T' @ (d':Q') yielding LMap
  This case reaches a contradiction; no rule can prove
    base:Empty =>> (t'');T' @ (d':Q') yielding LMap

CASE T = (t'');T' and
    D;H,{p->HeapPtr(t)} |- s : (l:Q)
    -------------------------------------------(s-alias)
    D;H,{p->HeapPtr(t)} |- s : (l:(Q /\ {p:t}))

  S = l:(Q /\ {p:t})
  l:(Q /\ {p:t}) => (t'');T' @ (d':Q')
  By S-IMP-IMP2, l:(Q /\ {p:t}) =>> (t'');T' @ (d':Q') yielding LMap
  Only s-imp2-alias-left can prove this, so
    l:Q =>> (t'');T' @ (d':Q') yielding LMap'
  Conclusion follows by induction

CASE T = (t'');T' and
    D;H |- s : l:Q
    D;H;{} |- w : t
    ---------------------------- (s-concat)
    D;H |- w::s : next(l):t::l:Q

  S = next(l):t::l:Q
  next(l):t::l:Q => (t'');T' @ (d':Q')
  By S-IMP-IMP2, next(l):t::l:Q =>> (t'');T' @ (d':Q') yielding LMap
  Only S-imp2-concat can prove this, so l:Q =>> T' @ (d':Q') yielding LMap'
  By induction, D;H |- resize(d',s) : d':Q' and Exists n. size(s) = d' + n
  size(w::s) = d' + (n + 1)
  resize(d',w::s) = resize(d',s)
  D;H |- resize(d',w::s) : d':Q'

CASE
    D;H |- s : S'
    S' => S
    ------------- (s-imp)
    D;H |- s : S

  By s-imp-trans, S' => T @ (d':Q')
  Conclusion follows by induction

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

LEMMA [S-s-RESIZE]
    if D;H |- s : S
   and |- Resize(d',S) = S'
  then D;H |- resize(d',s) : S'

Proof by cases on |- Resize(d',S) = S'

CASE
    S => T @ (d':Q')
    ----------------------- (S-shrink)
    |- Resize(d',S) = d':Q'

  Conclusion follows from S-s-RESIZE-SHRINK

CASE
    |- Resize(next^n(d),d:Q) = (Nonsense_n;...;Nonsense_1) @ (d:Q)  (S-grow)
  where S = d:Q and d' = next^n(d)

  D;H |- s : (d:Q)
  By S-SIZE-LABEL, d = size(s)

  Knowing D;H |- s : (d:Q)
    prove D;H |- resize(next^n(d),s) : (Nonsense_n;...;Nonsense_1) @ (d:Q)
  Proof by induction on n

  CASE 0
    resize(d,s) = resize(size(s),s) = s
    D;H |- resize(d,s) : (d:Q)

  CASE n + 1
    By induction, D;H |- resize(next^n(d),s) : (Nonsense_n;...;Nonsense_1) @ (d:Q)
    resize(next^(n+1)(d),s) = nonsense::resize(next^n(d),s)
    D;H;{} |- nonsense : Nonsense  (o-ns)
    By s-concat, D;H |- resize(next^(n+1)(d),s) : (Nonsense_(n+1);...;Nonsense_1) @ (d:Q)

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