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

LEMMA [S-IMP2-DECIDABLE]

    given S1 and S2, it is decidable whether there exists an LMap
      such that S1 =>> S2 yielding LMap

Proof: define
  size(l:P) = 1
  size(l:Empty) = 1
  size(l:t::S) = 1 + size(S)
  size(l:Q /\ {l':t}) = 1 + size(l:Q)

Each S-imp2-* rule with conclusion "S1 =>> S2 yielding LMap" has either:
  - no premise
  - one premise of the form "S1' =>> S2' yielding LMap'" where
    size(S1') + size(S2') < size(S1) + size(S2)
Therefore any derivation of "S1 =>> S2 yielding LMap" has height at most:
  size(S1) + size(S2)

Furthermore, only one derivation is possible, since the S-imp2-* rules for
"S1 =>> S2 yielding LMap" are directed by the syntax of S1 and S2.

Finally, only one LMap is possible.  This LMap is determined by
starting at the leaf of the derivation, where LMap = {}, and working towards
the root.

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

LEMMA [S-IMP-DECIDABLE] given S1 and S2, it is decidable whether S1 => S2

Follows from S-IMP2-DECIDABLE, S-IMP2-IMP, and S-IMP-IMP2.

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

LEMMA [S-SLOOKUP] S => T @ (l:Q) iff exists Q' s.t. l:Q' => l:Q and (T,Q') in slookup(l,S)
where we define the total computable function slookup(l,S):

    slookup(l,S) = shead(l,S) U stail(l,S)

    shead(l,l:Q) = {((),Q)}
    shead(l,l':Q) = {} where l ! = l'

    stail(l,l':P) = {}
    stail(l,l':Empty) = {}
    stail(l,l':t::l'':Q'') = {((t);T,Q) | (T,Q) in slookup(l,l'':Q'') and l' = next(l'')}
    stail(l,l':(Q /\ {lt:t})) = slookup(l,l':Q)

  Proof that S => T @ (l:Q) implies exists Q' s.t. l:Q' => l:Q and (T,Q') in slookup(l,S)
    Special case: proof for T = ():
      S => l:Q
      By S-IMP-LABEL-EQ, S = l:Q' for some Q', so l:Q' => l:Q
      shead(l,l:Q') = {((),Q')},
        so ((),Q') in slookup(l,l:Q')
        so (T,Q') in slookup(l,S)
    Proof for all T:
      By S-IMP-IMP2, S =>> l:Q yielding LMap.
      Then do proof by induction on S =>> l:Q yielding LMap.
      (The T = () base cases follow from the the special case proof above)

      CASE: T = (t);T' and
          S =>> T' @ (l:Q) yielding LMap
          ----------------------------------------------- (S-imp2-concat)
          l':t::S =>> (t);T' @ (l:Q) yielding LMap,(l',t)
        By induction, there is some Q' s.t. l:Q' => l:Q and (T',Q') in slookup(l,S)
        let S = l'':Q''
        slookup(l,l':t::S) subsetof stail(l,l':t::S) = {((t);T,Q) | (T,Q) in slookup(l,S) and l' = next(l'')}
        By definition of @, there is some n and Q'' such that:
              T' @ (l:Q) =                  next^n(l):Q''
          (t);T' @ (l:Q) = next^(n+1)(l):t::next^n(l):Q''
        By S-IMP2-LABEL-EQ, l'' = next^(n) and l' = next^(n+1)(l)
        so l' = next(l'')
        so ((t);T',Q') in slookup(l,l':t::S)

      CASE:
          l':Qs =>> l':O yielding LMap
          ----------------------------------------------- (S-imp2-alias-left)
          l':(Qs /\ {lt:t}) =>> l':O yielding LMap,(lt,t)
        By induction, there is some Q' s.t. l:Q' => l:Q and (T,Q') in slookup(l,l':Qs)
        Therefore (T,Q') in slookup(l,l':(Qs /\ {lt:t}))

      CASE:
          S =>> l':Q yielding LMap,(lt,t)
          ------------------------------------------- (S-imp2-alias-right)
          S =>> l':(Q /\ {lt:t}) yielding LMap,(lt,t)
        Since l':(Q /\ {lt:t}) does not have the form (t);T' @ S',
          we conclude T = (), and the proof follows from the special case

  Proof that S => T @ (l:Q) implied by exists Q' s.t. l:Q' => l:Q and (T,Q') in slookup(l,S)
    By induction on S.
    Subproof: if l:Q' => l:Q and (T,Q') in shead(l,S) then S => T @ (l:Q)
      If shead(l,S) contains (T,Q'), then S = l:Q' and T = (), so S => T @ (l:Q)
    Subproof: if l:Q' => l:Q and (T,Q') in stail(l,S) then S => T @ (l:Q)
      Case S = l':t::l'':Q'':
        (T,Q') in stail(l,l':t::l'':Q'') implies T = (t);T'
          where (T',Q') in slookup(l,l'':Q'')
          and l' = next(l'')
        By induction, l'':Q'' => T' @ (l:Q)
        By S-IMP-LABEL-EQ, T' @ (l:Q) = l'':Qt for some Qt
        By S-imp-concat, l':t::l'':Q'' => l':t::l'':Qt
        l':t::l'':Qt = next(l''):t::l'':Qt = (t);T' @ (l:Q)
      Case S = l':(Q' /\ {lt:t}):
        (T,Q') in stail(l,l':(Q' /\ {lt:t})) implies (T,Q') in stail(l,l':Q')
        By induction, l':Q' => T @ (l:Q)
        By S-imp-drop-alias, l':(Q' /\ {lt:t}) => T @ (l:Q)

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

LEMMA [S-ATOMS-ALIAS] (l,t) in atoms(S) iff exists l',Q. S => l':(Q /\ {l:t})
(note that atoms(S) is a total computable function)

  Proof that (l,t) in atoms(S) implies exists l',Q. S => l':(Q /\ {l:t})
    By S-IMP2-EQ, S =>> S yielding LMap, for some LMap
    By S-IMP2-YIELD, S =>> S yielding atoms(S)
    Let S = l':Q
    Since (l,t) in atoms(S), by S-imp2-alias-right, S => l':(Q /\ {l:t}) yielding LMap

  Proof that (l,t) in atoms(S) implied by exists l',Q. S => l':(Q /\ {l:t})
    S => l':(Q /\ {l:t})
    By S-IMP-IMP2, for some LMap, S =>> l':(Q /\ {l:t}) yielding LMap
    By S-IMP2-YIELD, S =>> l':(Q /\ {l:t}) yielding atoms(S)
    Only S-imp2-alias-right can conclude S =>> l':(Q /\ {l:t}) yielding atoms(S),
      so (l,t) in atoms(S)

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

LEMMA [S-OFFSET-DECIDABLE]

    given S and l and i, there is an algorithm that decides whether
      there exists l' such that
        S |- l + i = l'
      and, if so, produces l'

Proof:
  Decidability of S => T @ (l:Q) follows from S-SLOOKUP
  Only one l' is possible by S-offset-next and S-offset-prev
    (note that if i = 0, l + 0 = l and l - 0 = l yield same answer)

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

LEMMA [S-RESIZE-DECIDABLE]

    given S and l, there is an algorithm to produce a finite set A
      such that |- Resize(l,S) = S' iff exists S''. S'' in A and S'' => S'

Proof:
  Let A = A1 U A2
  where A1 = {l:Q' | (T,Q') in slookup(l,S)}
    By S-SLOOKUP, S => T @ (l:Q) iff exists Q' s.t. l:Q' => l:Q and (T,Q') in slookup(l,S)
    so exists T. S => T @ (l:Q) iff exists S'' in A1 s.t. S'' => l:Q
  where A2 = {(Nonsense_n;...;Nonsense_1) @ (l':Q) | S = l':Q and l = next^n(l')}

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

LEMMA [S-LOOKUP-DECIDABLE]

    given S and l, there is an algorithm to produce a finite set A
      such that S |- l : t iff t in A

Proof:
  Let A = {t | (l,t) in atoms(S)}
  Proof follows from S-ATOMS-ALIAS

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

LEMMA [S-UPDATE-DECIDABLE]

    given S, l, and t', there is an algorithm to produce a finite set A
      such that S |- l <- t' ~~> S' iff exists S''. S'' in A and S'' => S'

Proof:
  Let A = A1 U A2
  where A1 = {S | (l,t') in atoms(S)}
    (see S-LOOKUP-DECIDABLE)
  where A2 = {T @ (l:t'::St) | (T,Q') in slookup(l,S) and Q' = t::St}
    Subproof: S => T @ (l:t::S') implies exists S''. S'' in A2 and S'' => T @ (l:t'::S')
      By S-SLOOKUP, S => T @ (l:t::S') implies exists Q' s.t. l:Q' => l:t::S' and (T,Q') in slookup(l,S)
      By S-IMP-IMP2, l:Q' =>> l:t::S' yielding LMap
      Let Q' = O' /\ {l1:t1} /\ ... /\ {ln:tn}
      By induction on S, (T,Q') in slookup(l,S) implies (T,O') in slookup(l,S)
      Only S-imp2-concat followed by zero or more S-imp2-alias-left can conclude l:Q' =>> l:t::S' yielding LMap,
        so by S-IMP2-IMP and S-imp-drop-alias, exists St s.t. O' = t::St and St => S'
      Let S'' = T @ (l:t'::St)
      T @ (l:t'::St) => T @ (l:t'::S')
    Subproof: S => T @ (l:t::S') implied by exists S''. S'' in A2 and S'' => T @ (l:t'::S')
      S'' = T'' @ (l:t'::St'') where (T'',Q') in slookup(l,S) and Q' = t::St''
      T'' @ (l:t':St'') => T @ (l:t'::S')
      By S-IMP-IMP2, T'' @ (l:t':St'') =>> T @ (l:t'::S') yielding LMap
      S-imp2-concat can prove this, so T'' = T and St'' =>> S' yielding LMap'
      l:t::St'' => l:t::S' (by S-IMP2-IMP, s-imp-concat)
      l:Q' => l:t::S'
      (T,Q') in slookup(l,S)
      By S-SLOOKUP, S => T @ (l:t::S')

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

LEMMA [G-IMP-DECIDABLE] given G and G', G => G' is decidable
LEMMA [WF-l-DECIDABLE] given D and l, D |- l is decidable

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

LEMMA [WF-t-DECIDABLE] given D and t, D |- t is decidable
LEMMA [WF-G-DECIDABLE] given D and G, D |- G is decidable
LEMMA [WF-S-DECIDABLE] given D and S, D |- S is decidable

Proof by mutual induction on t and G and S

CASE
    D |- l
    D |- t
    D |- lq:Q
    forall lq',t',Q', if lq:Q => lq':(Q' /\ {l:t'}) then t = t'
    ----------------------------------------------------------- (wf-S-alias)
    D |- lq:(Q /\ {l:t})
  By induction, D |- lq:Q is decidable
  By S-ATOMS-ALIAS, (l,t') in atoms(lq:Q) iff exists lq',Q'. lq:Q => lq':(Q' /\ {l:t'})
  For each (l,t') in atoms(lq:Q), check that t = t'

CASE
    D |- l
    D |- t
    D |- S
    forall lq',l',t',Q', if S => lq':(Q' /\ {l':t'}) then l != l'
    ------------------------------------------------------------- (wf-S-concat)
    D |- l:(t::S)
  By induction, D |- S is decidable
  By S-ATOMS-ALIAS, (l',t') in atoms(S) iff exists lq',Q'. S => lq':(Q' /\ {l':t'})
  For each (l',t') in atoms(S), check that l != l'

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

LEMMA [a-DECIDABLE] given G and S and r and t, there is an algorithm to compute a finite set A
  such that |- (G,S){r<-t}(G',S') iff exists S''. (G',S'') in A and S'' => S'

Proof follows from S-RESIZE-DECIDABLE

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

LEMMA [v-DECIDABLE] given D and H and v, there is an algorithm to compute a finite set A
  such that D;H |- v:t iff t in A
LEMMA [o-DECIDABLE] given D and H and G and o, there is an algorithm to compute a finite set A
  such that D;H;G |- o:t iff t in A
LEMMA [i-DECIDABLE] given D and H and G and S and ins, there is an algorithm to compute a finite set A
  such that D;H |- (G,S){ins}(G',S') iff exists S''. (G',S'') in A and S'' => S'
LEMMA [b-DECIDABLE] given D and H and G and S and b, D;H;G;S |- b is decidable
THEOREM [block-DECIDABLE] given H and block, H |- block is decidable

Proof by mutual induction on v and o and ins and b and block

CASE:
    D;H |- (G;S){ins}(G';S')
    D;H;G';S' |- b
    ------------------------ (b-ins)
    D;H;G;S |- ins; b
  By induction, we can compute a finite set A such that
    D;H |- (G,S){ins}(G',S') iff exists S''. (G',S'') in A and S'' => S'
  So
    D;H;G;S |- ins; b iff exists S',G'. D;H;G';S' |- b and exists S''. (G',S'') in A and S'' => S'
  So
    D;H;G;S |- ins; b iff exists G',S''. (G',S'') in A and exists S'. D;H;G';S' |- b and S'' => S'
  By Stack-weakening, exists S'. D;H;G';S' |- b and S'' => S' implies D;H;G';S'' |- b
  By choosing S' = S'' and using s-imp-eq, D;H;G';S'' |- b implies exists S'. D;H;G';S' |- b and S'' => S'
  So
    D;H;G;S |- ins; b iff exists G',S''. (G',S'') in A and D;H;G';S'' |- b
  Decidability of D;H;G';S'' |- b follows by induction

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