This is a correctness proof of the algorithm adopted by the SIL StackNesting
utility in late 2025. It is a text file rather than Markdown because the
notation it uses is quite unfriendly to Markdown.

Repeating the text from the in-file comment:

We use a straightforward, single-pass algorithm:

  enum AllocationStatus {
    case allocated
    case pendingDeallocation
    case undeallocatable
  }
  struct State {
    var stack = [(StackAllocationInst, AllocationStatus)]()
  }
  F.searchBlocksForJointPostDominance(initialState: State()) {
    (block, state) in
    for inst in block.instructions {
      if inst.isStackAllocation {
        state.stack.push((inst, .allocated))
      } else if inst.isStackDeallocation {
        let allocation = inst.stackAllocation
        if state.stack.top == (A, .allocated) {
          _ = state.stack.pop()
          let builder = SILBuilder(insertAfter: I)
          while !state.stack.isEmpty &&
                state.stack.top!.1 == .pendingDeallocation {
            builder.createStackDeallocation(for: state.stack.pop().0)
          }
        } else {
          I.remove()
          let curStatus = state.findStatus(A)
          assert(curStatus != .pendingDeallocation)
          if curStatus == .allocated) {
            state.setStatus(A, .pendingDeallocation)
          }
        }
      }
    }
  }

The expectation is that searchBlocksForJointPostDominance performs a
depth-first search, passing a state that reflects the current simple path
from the entry block that is being explored. However, there's a twist to this
from a standard DFS; see below.

For the most part, the value in `state` at the end of processing a block is
the initial value of `state` at the start of processing its successor as
visited by the DFS, but this also has a twist; see below.

The state consists of (1) an active stack of allocations which haven't yet
been deallocated on this path and (2) an active status for each allocation.

It has five invariants:

1. Allocations on the stack dominate all allocations above them.
2. Every allocation on the stack dominates the current point
   being considered.
3. The top of the stack never has pending status.
4. If a stack item has undeallocatable status, every item
   below it also has undeallocatable status.
5. If an allocation has pending status, there is an allocation
   above it on the stack which has allocated status.

The twist about the search order and state relates to the non-coherence of
SIL's joint post-dominance requirement for stack allocations. Specifically,
SIL permits the current state of the stack to vary on different edges into a
dead-end region; this just means it is not permitted to pop any of those
deallocations from the stack. (More allocations can be pushed and popped, but
the existing ones become untouchable.) StackNesting therefore permits its
input to be non-coherent: whether an allocation has been deallocated is
allowed to vary across the entries to a dead-end region.

To handle this, the search delays considering edges into a dead-end region
until it has seen the last such edge. Furthermore, the initial state of the
destination block is set to a conservative merger of the final states of all
of the predecessors: if two states differ in any way, the contents of the
stack are pared back to the common prefix, and all allocations are placed in
the undeallocatable state.

Bear in mind that a depth-first search of a CFG corresponds to the selection
of a spanning tree T of that CFG, so when this proof talks about states under
a particular spanning tree, it really means "while performing a depth-first
search". The twist doesn't change that: from the DFS perspective, it just
delays the visitation of the successor block until later.

The twist *does* create a significantly stronger invariant in the algorithm,
however, because it reestablishes the property that the allocations currently
on the stack always dominate the current point. Without the twist, this can
be lost when the search explores a dead-end path.

(An earlier version of this algorithm simply allowed the DFS to continue into
dead-end blocks normally. It turns out that, when doing so, it's still
impossible to emit a deallocation at a point the allocation does not
dominate, because there is an invariant that every allocation with pending
status is beneath an allocation with allocated status that it dominates.
But that version of the algorithm could not always properly establish nesting
for deallocations in dead-end blocks, so it needed to be fixed by the
addition of MERGE operations.)

Induction principles
--------------------

This proof contains several proofs by structural induction over paths in an
implicit spanning tree T:

   \forall P: point -> pred .
     P(entry point) /\
     (\forall x: point . \forall p: path .
        (\exists p': path .
           p in T /\
           p ends at x /\
           p = (p'..., c) /\
           (\forall x': point . p' visits x' => P(x')))
         => P(x))
     => \forall x: point . P(x)

or over the SCC tree:

   \forall P: point -> pred .
     (\forall x: point .
       (\forall y: point . SCC(y) is a proper ancestor of SCC(x) => P(y))
       => P(x))
     => \forall x: point . P(x)

These induction principles only actually work for reachable points --- they
are ultimately derived by inducting on the definition of reachability --- but
that's fine because we only care about the properties of reachable points.

Spanning tree path induction is useful because the state at a point is defined
inductively over the path to that point in some spanning tree T.
(Remember that the choice of a spanning tree T reflects the arbitrary
decision of which path the DFS takes to a block, which is ultimately proven
not to matter to the algorithm by the [tree-invariance] theorem.)

SCC tree induction is useful because certain properties are easier to build up
that way, especially properties that are affected by the "twist" for dead-end
regions.

Theory and notation
-------------------

The CFG is generally thought of as a directed graph of blocks, with
control-flow edges between them. However, in this proof, we deal mostly with
the point-graph, the directed graph of points (the gaps before and after
instructions). The edges in the point-graph are the instructions and control
flow edges of the function.

In this proof, we will consistently use "edge" to mean a control-flow edge
between blocks, and we will use "component" to refer to the things that act
as edges in the point-graph.

<I is the CFG point prior to an instruction I.
I> is the CFG point after an instruction I.
If I is immediately followed by J, then I> and <J are the same point. In the
point-graph, an instruction I acts as an edge from <I to I>.

<B is the start point of block B, which is the same point as <I,
  where I is the first instruction in the block.
B> is the ending point of block B, which is the same point as I>,
  where I is the last instruction in the block.
The entry point is the start point of the entry block.

X -> Y is a control flow edge from its source block X to its destination block
Y. In the point-graph, it acts as an edge from X> to <Y.

<K and K> are the CFG points before and after a component K. If K is an
instruction I, then <K = <I and K> = I>. If K is a control flow edge X -> Y,
then <K = X> and K> = <Y, which is probably a little confusing, sorry.

A path through the CFG (sometimes called a walk in other sources: we are not
assuming non-repetition) is a sequence of CFG points joined by components
(either instructions or control-flow edges). A path consisting of a single
point is called the empty path at that point. A simple path is a path that
does not visit the same point twice.

If the text talks about the path to some point in a spanning tree, without
clarifing the start point of the path, the path is implicitly from the
entry point.

A path is written as the sequence of the instructions and control-flow edges
that it passes through. There is an implicit requirement that the end point
of each part of this notation be the start point of the next, which must
be satisfied when concatenating paths.

As an example:
  (P..., I, A -> B)
The path follows the subpath P (which must end at <I), then passes through I,
then passes through the control flow edge from block A (which I must be the
last instruction of) to B.

A point X is said to be live if there exists a path from X to an exit of the
function. A block B is said to be live if its start point is live. An SCC
is live if all of its blocks are live. If a point/block/SCC is not live, it
is dead-end.

The entry SCC is the SCC containing the entry block.

An edge is an internal edge of an SCC if its source and destination blocks are
both in that SCC. An edge is an entry edge of an SCC if its destination block
is in that SCC but its source block is not. All edges are either internal
edges or entry edges of some SCC.

A path is life-preserving if it does not pass through any entry edges
into dead-end regions. (Note that it can begin in a dead-end region;
it just can't enter a different one.)

A component is said to be in an SCC C if it is an instruction that's in
a block in that SCC or if it's an internal edge whose source and destination
blocks are in that SCC. Entry edges are not in any SCC.

The start blocks of an SCC are:
- for the entry SCC, the singleton set containing the entry block;
- for any other SCC, the set of all blocks that are the destination block
  of some entry edge into the SCC.
The start points of an SCC are the set of the start points of the
start blocks of that SCC.

Points, blocks, and SCCs only ever refer to entities reachable from the entry
point, as if unreachable blocks simply didn't exist in the CFG. The algorithm
implicitly ignores unreachable code, and so shall we. (The implementation
does still has to account for them, since they're allowed to exist in SIL.)

MAP(S, F) applies F to the elements of S in order. It is a monoid morphism and
therefore respects concatenation, i.e.
  MAP((), F) = ()
  MAP((A..., B...), F) = (MAP(A, F)..., MAP(B, F)...)

FLAT_MAP(S, F) applies F to the elements of S in order and concatenates the
resulting sequences. It is a monoid morphism and therefore respects
concatenation, i.e.
  FLAT_MAP((), F) = ()
  FLAT_MAP((A..., B...), F) = (FLAT_MAP(A, F)..., FLAT_MAP(B, F)...)

EDGE_FLAT_MAP(S, F) applies F to the joining elements of S in order. For
example, on a CFG, it applies F to the components that the path passes
through. It is a monoid morphism and therefore respects concatenation, i.e.
  EDGE_FLAT_MAP((), F) = ()
  EDGE_FLAT_MAP((A..., B...), F) = (EDGE_FLAT_MAP(A, F)..., EDGE_FLAT_MAP(B, F)...)

All of the theorems below are implicitly quantified over an arbitrary spanning
tree T unless they're marked (tree-independent).

Formal definition of the algorithm
----------------------------------

The following definitions formalize the state changes of the algorithm:

Definition [state].
  A algorithm state is a sequence of pairs of allocation instructions
  and status. A status is one of "allocated", "pending", or
  "undeallocatable".

  An allocation A is said to be present (or contained by, or included in)
  a state S if there is an element of S with A as its first element.

  An allocation A is said that have status X in S if there is an element
  of S with A as its first element and X as its second.

  A state is well-formed if no allocations repeat in it and if the
  allocations having undeallocatable status form a prefix of the sequence.

  There are four state operations. It is a precondition for all of them
  that the initial state S is well-formed.

  STATE_PUSH(S, A) := (S..., (A, allocated))
    It is a precondition that A is not already present in S.
  STATE_POP(S, A) := PREFIX(S, I)
    where I is the smallest index such that all elements at I and later in S,
    except for the last, have pending status. It is a precondition that
    the final element of S is (A, allocated).
  STATE_PEND(S, A) := SET_STATUS(S, I, pending)
    where I is the smallest index such that the allocation at index I of S
    is A. It is a precondition A is not the final element of S and that
    S gives A allocated status.
  STATE_MERGE(S, PSS) := CONSERVATIVE_MERGE(PSS)
    It is a precondition that S is an element of PSS.

  SET_STATUS(S', I, X) produces a sequence S where LENGTH(S') = LENGTH(S),
    where S[J][0] = S'[J][0], and where either
      S[J][1] = X           (if I = J)
      S[J][1] = S'[J][1]    (if I != J)
    It is a precondition that I < LENGTH(S').

  CONSERVATIVE_MERGE(PSS) produces a sequence S where
    - LENGTH(S) is the maximum L such that
      - for all S1 in PSS, L <= LENGTH(S1)
      - for all S1 and S2 in PSS, and for all I' < L, S1[I'][0] = S2[I'][0]
    - S[I][0] = S'[I][0], where S' may be any element of PSS
    - S[I][1] = undeallocatable
  The second rule is well-founded because I < LENGTH(S) and therefore
  S1[I][0] = S2[I][0] for all S1 and S2 in PSS.

  The empty stack is the state at the entry point:

  STATE_EMPTY := ()

Definition [operation, operation sequence, state at a point,
            predecessor state set].
  All of these definitions are sensitive to a specific spanning tree T
  because of the rules around entry edges into dead-end regions. In this
  section, we will make the T parameter explicit, but most places in the
  proof will leave it off.

  An operation sequence is a non-empty sequence of states joined by
  operations, e.g.
    [ () ]
    [ (), PUSH@A, ((A, allocated)) ]
    [ (), PUSH@A, ((A, allocated)), POP@D, () ]

  Like paths, we will usually not be explicit about states, because
  they can be imputed from context and the operations; instead, we will
  just write the operations, like so:
    (PUSH@A)

  When we need to be explicit about states, we will write the sequence in
  square brackets [ ... ] rather than parentheses ( ... ).

  Concatenation on operation sequences requires the end state of the first
  sequence to match the start state of the second; it then just concatenates
  the underlying sequences after discarding the start state from the second
  sequence. Concatenation is associative, and the empty sequence (at the
  right state) is both a left-identity and a right-identity; we will not
  prove these properties.

  The operations are:
  - PUSH@A, where A is an allocation
  - POP@D, where D is a deallocation
  - PEND@D, where D is a deallocation
  - MERGE@(X -> Y), where X -> Y is a conservative entry edge in T

  An operation O changes state S' to state S (under T) if
    S = OPERATION_APPLY(S', O, T)
  where
    OPERATION_APPLY(S', PUSH@A, T) := STATE_PUSH(S', A)
    OPERATION_APPLY(S', POP@D, T) := STATE_POP(S', ALLOCATION(D))
    OPERATION_APPLY(S', PEND@D, T) := STATE_PEND(S', ALLOCATION(D))
    OPERATION_APPLY(S', MERGE@(X -> Y), T) := STATE_MERGE(S', PSS(SCC(Y), T))
  Here ALLOCATION(D) is the allocation of a deallocation and SCC(Y) is the
  SCC containing the block Y.

  An operation O is said to be well-formed for a transition from S1 to S2
  (under T) if
  - S1 and S2 are well-formed states,
  - O satisfies its component restriction (under T),
  - S1 satisfies the preconditions of the corresponding state operation, and
  - O changes S1 to S2 (under T).

  An operation sequence OS is well-formed (under T) if
  - each state in OS is well-formed and
  - each operation triple [ S1, O, S2 ] in OS is well-formed (under T),
    defined as O being well-formed for the transition from S1 to S2 (under T).

  Given an initial path P in T, the tree-driven operation sequence
  OS(P, T) is defined as OS_PATH(STATE_EMPTY, P, T).

  Given a path P, the path-driven operation sequence OS_PATH(S, P, T)
  corresponding to P (under T) and start with state S is derived
  inductively:

    OS_PATH(S, (), T) := [ S ]
    OS_PATH(S, (P..., C), T) :=
      (OS_PATH(S, P', T)..., OPERATION(S', SC, T)...)
      where S' is the end state of OS_PATH(S, P', T).

  OPERATION(S, C, T) is defined as follows:

  - If C is an allocation A, then
      OPERATION(S, C, T) := [ S, PUSH@A, STATE_PUSH(S, A) ]
  - If C is a deallocation D of an allocation A, and A has allocated
    status and is at the top of the stack in S, then
      OPERATION(S, C, T) := [ S, POP@D, STATE_POP(S, A) ]
  - If C is a deallocation D of an allocation A, and A has allocated
    status and is not at the top of the stack in S, then
      OPERATION(S, C, T) := [ S, PEND@D, STATE_PEND(S, A) ]
  - If C is a conservative entry edge X -> Y into R, then
      OPERATION(S, C, T) := [ S, MERGE@(X -> Y), STATE_MERGE(S, PSS(R, T)) ]
  - Otherwise
      OPERATION(S, C, T) := [ S ]

  Note that the path must pass through an instruction or edge, not just reach
  it, in order for the operation sequence to include the corresponding
  operation.

  The state at a point X (under T) is the end state of the operation
  sequence corresponding to the path to X in T.

  The start state of a block B (under T) is the state at <B (under T).
  The end state of a block B (under T) is the state at B> (under T).

  The start state of a path P (under T) is the state at the start
  point of P (under T).
  The end state of a path P (under T) is the state at the end point of P
  (under T).

  The predecessor state set PSS(C, T) of an SCC C is the set of end
  states (under T) of all blocks B that are not in C but have an edge to a
  block in C.

  An edge is a conservative entry edge (under T) if it is an entry edge
  into a dead-end region R where PSS(R, T) is not singleton.

  A path is deallocatability-preserving (under T) if it does not pass through
  any conservative entry edges (under T).

  That OS(P, T) produces a well-formed operation sequence and satisfies the
  preconditions on the state operations is proven by
  [correctness-operation-sequence].

  Note that OPERATION does not create an operation for every deallocation.
  - If the allocation has allocated status, OPERATION always creates an
    operation.
  - If the allocation is not in S, or if it has pending status, OPERATION
    silently ignores it. These cases are proven impossible by
    [correctness-deallocation-preconditions].
  - If the allocation has undeallocatable status, OPERATION silently
    ignores it (in terms of state changes). This is okay because it can
    only happen in dead-end regions, and since the algorithm will also
    just delete the deallocation at these points.

Formal definitions
------------------

Axiom [block-single-entry].
  If an initial path visits a point in block B, then it has a suffix that
  starts at <B and does not pass through an edge.

Axiom [block-single-exit].
  For every point X in block B, there exists a path from <B to X
  that does not pass through an edge.

Axiom [block-straight-line].
  If a path does not pass through an edge, it is a simple path, and it
  is the unique such path from its start point to its end point.

Proofs of general utility
-------------------------

Definition [SCC ancestry].
  These are all basic definitions and theorems in the theory of SCCs and are
  presented without proof.

  A is an ancestor of B if there is a path from some block in A to some block
  in B. A is a proper ancestor of B if A is an ancestor of B and A != B.
  A is a descendent of B if B is an ancestor of A. A is a proper descendent
  of B if B is a propert ancestor of A.

  A cannot be both a proper ancestor of B and a descendent of B.
  A cannot be both an ancestor of B and a proper descendent of B.

  If A is an ancestor of B, there is a path from the start point of any
  block in A to any point in B. If A is a proper ancestor of B, there is a
  path from any point in A to any point in B.

  If A is a proper ancestor of B, there is no path from any point in B to any
  point in A.

  If X -> Y is an entry edge into the SCC of Y, the SCC of X is a proper
  ancestor of the SCC of Y.

  If P is a path to a point in a proper ancestor of A, then all points on P
  are in SCCs that are proper ancestors of A.

  If P is a path between two points in the same SCC, then all points on P
  and components passed through by P are in that SCC.
End.

Definition [SCC entry prefix, entry suffix, entry path, entry point].
  If P is a path that visits an SCC C,
  - the SCC entry point of P for C is the first point on P that is in C,
  - the SCC entry prefix of P for C is the shortest prefix of P that ends at
    a point in C, and
  - the SCC entry suffix of P for C is the longest suffix of P that begins at
    a point in C.

  P is an SCC entry path for C if it is an initial path that ends at a point
  in C, but only the point at the end index of P is in C.

  X is an SCC entry point of C if there exists an initial path P that visits
  C such that X is the SCC entry point of P.
End.

Lemma [scc-non-entry-path]. (tree-independent)
  If an initial path P to the start point of a block B is not an SCC entry
  path for the SCC C containing B, then
    P = (P_I..., M -> B)
  where M -> B is an internal edge of C.
Pf.
  Because P is not an SCC entry path for C, there exists a point on P that
  is in C besides the end point. P is therefore not the empty path, and can
  be partitioned before its last component:
    P = (P_I..., K)
  P_I passes through a point in C; let it be partitioned at such a point:
    P_I = (P_II..., P_IF...)
  Then (P_IF..., K) is a path from a point in C to a point in C, and
  so every component it passes through must be in C, including K. The end
  point of P is the start point of the block B, so K must be an edge to B:
    P = (P_I..., M -> B)
  and because M -> B is in C, it must be an internal edge of C.
Qed.

Lemma [scc-entry-point].
  If P is a path that visits an SCC C, P_I is the SCC entry prefix of P for C,
  and P_F is the entry suffix of P for C, then
    P = (P_I..., P_F...)

  Furthermore, the entry point of P for C is the same as the end point of P_I
  and the start point of P_F.
Pf.
  P_I is a prefix of P, so it ends at some position X in P.
  P_F is a suffix of P, so it ends at some position Y in P.
  The points at X and Y are in C by definition.

  If X < Y, then the suffix of P start from X would be longer than P_F;
  since it would also start from a point in C, this would contradict the
  assumption that P_F is the longest such suffix of P.

  If Y < X, then the prefix of P ending at Y would be shorter than P_I; since
  it would also end at a point in C, this would contradict the assumption
  that P_I is the shortest such prefix of P.

  Therefore Y = X, and concatenating a prefix and a suffix of a sequence taken
  at the same position always produces the original sequence.

  The point of P at X is the entry point of P for C: if there were an earlier
  point in P that was in C, then the prefix of P ending at the index of that
  point would be shorter than P_I; since it would end at a point in C, that
  would contradict the assumption that P_I is the shortest such prefix of P.
Qed.

Lemma [scc-entry-prefix-ancestry].
  If P_I is the SCC entry prefix of some path P for C, then
  - if P_I is an initial path, it is an entry path of C;
  - P_I does not pass through any components of descendent SCCs of C;
  - P_I visits only points in ancestor SCCs of C; and
  - if P_I is not the empty path, it ends with an entry edge into C
    and the points of P_I at all indexes except the end index are in proper
    ancestor SCCs of C.
Pf.
  Let X be the end point of P_I. By definition, X is in C.

  Let X' be a point visited by P_I, and let C' be the SCC containing X'. Then
  the suffix of P_I start at X' is a path from a point in C' to a point in
  C, which makes C' an ancestor SCC of C by definition.

  P_I does not pass through any component K of a descendent SCC C' of C:
    Suppose it did; let
      P_I = (PK_I..., K, PK_F...)
    PK_F is a path from K> (a point in C') to X (a point in C), so C' must
    be an ancestor SCC of C'; since it is both an ancestor and a descendent
    of C, C' = C. Then since <K is also a point in C, and it is at an earlier
    index of P than X, a prefix of P_I ending at <K would be a shorter prefix
    of P that ends at a point in C, which would contradict the assumption
    that P_I is the SCC entry prefix of P for C. So P_I cannot pass through
    any such component.

  If P_I is not the empty path:
    P_I ends by passing through some component K. As previously argued,
    K cannot be in C, but since K> is in C, K must be an entry edge M -> N
    into C. The SCC containing M is a proper ancestor of C. Let X be a point
    on P_I prior to this edge. Then the subpath of P_I from X to M> is a path
    to a point in a proper ancestor SCC of C, which means X is in a proper
    ancestor SCC of C.

  If P_I is an initial path:
    As previously argued, the end point of P_I is in C.

    If P_I is the empty path, then there are no indexes in P except the final
    index, so it is vacuously true that only the point at the end index of P
    is in C.

    If P_I is not the empty path, then as previously argued, all points of P_I
    at indexes other than the end index are in proper ancestors of C, and
    therefore not in C.

    Therefore, in all cases, P_I is an entry path of C.
Qed.

Lemma [scc-entry-suffix-ancestry]. (tree-independent)
  If P_F is the SCC entry suffix of some path P for C, then P_F visits only
  points in descendent SCCs of C. Furthermore, if P ends at a point in C,
  P_F visits only points in C.
Pf.
  The start point of P_F is in C. Let X be a point visited by P_F; then
  the prefix of P_F ending at X is a path from a point in C to a point in the
  SCC containing X, which makes the SCC containing X a descendent SCC of C
  by definition.

  If P ends at a point in C:
    Let X be a point visited by P_F. Then the suffix of P_F start at X
    is a path from X to a point in C, which makes the SCC containing X
    an ancestor SCC of C as well. Since it is both a descendent and an
    ancestor of C, it must be C.
Qed.

Lemma [scc-entry-suffix-suffix]. (tree-independent)
  If a path P has a partition like so
    P = (P_I..., M -> N, P_F...)
  where M -> N is an entry edge, and P_F' is the SCC entry suffix of P for
  the SCC containing the end point of P, then P_F' is a suffix of P_F.
Pf.
  Let C be the SCC containing the end point of P. By definition, P_F' is
  the longest suffix of P that begins at a point in C. By the given
  partition of P, all indexes in P correspond to points in either P_I or P_F.

  Suppose that P_F' begins at an index into the P_I subpath of P, and let
  P_I' be the suffix of P_I from that index. But then the start point of
  P_I' is in C, so there exists a path P_FI from the end point of P to the
  start point of P_I'. (P_I..., M -> N, P_F..., P_FI...) is a cycle
  that begins and ends at a point in C, so all points on it must be in C.
  In particular, M> and <N must both in the C, which contradicts the
  assumption that M -> N is an entry edge.

  Therefore P_F' must begin at an index into the P_F subpath of P, and so
  P_F' is a suffix of P_F.
Qed.

Lemma [scc-entry-path-existence]. (tree-independent)
  For every SCC C and spanning tree T, there exists (possibly non-uniquely) an
  SCC entry path of C.
Pf.
  (Recall that we universally assume reachability.)

  Let X' be a point in C, and let P' be the path to X' in T. Then let P be the
  SCC entry prefix of P' for C. P is an initial path because is a prefix of an
  initial path. Therefore by [scc-entry-prefix-ancestry], P is an SCC entry
  path of C.
Qed.

Lemma [scc-entry-path-ancestry]. (tree-independent)
  If P is an SCC entry path of C,
  - P is the SCC entry prefix of P for C,
  - P visits only points in ancestor SCCs of C; and
  - if P is not the empty path, it ends with an entry edge into C
    and the points of P at all indexes except the end index are in proper
    ancestor SCCs of C.
Pf.
  Let P' be the SCC entry prefix of P for C. By definition, only the point at
  the final index of P is in C, so P' is a prefix of P that must contain the
  final index of P, which means P = P'.

  Since P is the SCC entry prefix of P for C, the other properties are true
  by [scc-entry-prefix-ancestry].
Qed.

Lemma [scc-entry-edge-partition]. (tree-independent)
  If a path P contains an edge X -> Y that is an entry edge into SCC C,
  then
    P = (P_I.., X -> Y, P_F...)
  where (P_I..., X -> Y) is the SCC entry prefix of P for C and P_F is the
  SCC entry suffix of P for C. All points visited by P_I are in proper
  ancestors of C.
Pf.
  Let P be split around the edge as specified:
    P = (P_I..., X -> Y, P_F...)

  Let CX be the SCC containing X. Because X -> Y is an entry edge into C, CX
  is a proper ancestor of C; since X> is a point in CX, all points on P_I are
  in proper ancestors of C. Therefore the first index of P that is for a
  point in C must be the index following the X -> Y edge, making
    (P_I..., X -> Y)
  the SCC entry prefix of P for C and P_F the SCC entry suffix of P for C.
Qed.

Lemma [scc-entry-path-partition]. (tree-independent)
  If an initial path P visits an SCC C, and C is not the entry SCC, then
  there uniquely exist M, N, P_I, and P_F such that
    P = (P_I..., M -> N, P_F...)
  such that (P_I..., M -> N) is the SCC entry prefix of P for C, P_F is the
  SCC entry suffix of P for C, M -> N is an entry edge into C, and all points
  visited by P_I are in proper ancestors of C.
Pf.
  Let P_I' be the SCC entry prefix of P for C, and let P_F be the SCC entry
  suffix of P for C. By [scc-entry-point],
    P = (P_I'..., P_F...)

  P_I' must be an initial path because P_I is. P_I' therefore cannot be the
  empty path because otherwise the final point of P_I' would be both the
  entry point and in C, and C is not the entry SCC by assumption. Therefore
  [scc-entry-prefix-ancestry] tells us that P_I' can be further split:
    P_I' = (P_I..., M -> N)
  where M -> N is an entry edge into C and P_I contains only points in
  proper ancestors of C.

  By substitution,
    P = (P_I..., M -> N, P_F...)
  and P_I, M -> N, and P_F satisfy all the requirements of the lemma.
Qed.

Lemma [acyclic-scc-entry-point]. (tree-independent)
  If X is a point in an acyclic SCC C, the entry point for C of all initial
  paths to X is the start point of the block containing X.
Pf.
  Let an initial path P to X be given, and let P be partitioned by its
  entry point for C:
    P = (P_I..., P_F...)
  The entry point of P for C is the start point of P_F, which must be the
  start point of some block in C. But an acyclic SCC contains only a single
  block, and so this must be the block containing X.
Qed.

Lemma [no-cyclic-scc-deallocation]. (tree-independent)
  A cyclic SCC C cannot contain a deallocation D for an allocation A that is
  not in C.
Pf.
  Let C, D, and A be given, and let P be a path to D>. The entry block is
  never a cyclic SCC, so P must pass through exactly one entry edge of C:
    P = (P_EX..., X -> Y, P_YD...)
  such that X is not in C and Y is in C. Then P_YD lies entirely within C.
  Because C is a cyclic SCC, there must exist a path P_DY from D> to <Y which
  also lies entirely within C. Then
    (P_EX..., X -> Y, P_YD..., P_DY..., P_YD...)
  is a (non-simple) path that passes through two deallocations of A. This path
  cannot pass through A between the deallocations because that portion of the
  path lies entirely within C, and A is not in C. This violates the joint
  post-dominance rule of deallocation.
Qed.

Lemma [no-scc-self-path-deallocation]. (tree-independent)
  A path P from <X to <Y, where X and Y are two blocks in the same SCC, can
  never pass through a deallocation of an allocation from a different SCC.
Pf.
  If the SCC is not cyclic, then X and Y must be the same
  block, and the only possible such path is empty and therefore
  does not pass through anything. Otherwise, it is cyclic and
  [no-cyclic-scc-deallocation] applies.
Qed.

Lemma [no-scc-self-path-history]. (tree-independent)
  If P is a path from <X to <Y, where X and Y are two blocks in the same SCC
  C, and A is an allocation from a different SCC, then AH(A, P) = ().
Pf.
  P passes through only components of C, so it cannot pass through A,
  which is not in C by assumption. By [no-scc-self-path-deallocation],
  P also cannot pass through a deallocation of A. Therefore AH(A, P) = ().
Qed.

Lemma [implied-dominance]. (tree-independent)
  For all points X, Y, and Z, if X dominates Z, and there is a path
  P_YZ from Y to Z that does not pass through X, then X dominates Y.
Pf.
  Let X, Y, Z, and P be given. Let P_Y be an arbitrary path from
  the entry point to Y; then PZ := (P_Y..., P_YZ...) is a path from
  the entry point to Z. X dominates Z, so all paths from the entry
  point to Z pass through X, and that includes P_Z. The P_YZ subpath
  of P_Z does not pass through X, so the P_Y subpath must. But that
  means that all paths to Y pass through X, so X dominates Y.
Qed.

Lemma [same-block-dominance]. (tree-independent)
  If a simple initial path to X passes through an instruction I in the
  same block as X, then I dominates X.
Pf.
  Let an arbitrary initial path P' to X be given. Let B be the block
  containing X.

  By [block-single-entry], P and P' have suffixes that start at <B and do
  not pass through an edge.
    P = (PI..., PF...)
    P' = (PI'..., PF'...)

  PF must pass through A:
    P passes through A, so either PI or PF passes through A.
    If PI passes through A, it can be partitioned around that:
      PI = (PAI..., A, PAF...)
    and then since PAI visits <A, a point in B, it has a suffix that starts
    at <B by [block-single-entry]:
      PAI = (PAII..., PAIF...)
    Then altogether, P looks like this:
      P = (PAII..., PAIF..., A, PAF..., PF...)
    and since both PAIF and PF start at <B, and they are separated by at
    least one concrete component on P, P must visit <B twice, which
    contradicts the assumption that it is a simple path. So PI cannot
    pass through A, and so PF must.

  By [block-straight-line], PF = PF', so P' also passes through A.
  Since P' was an arbitrary initial path to X, all such paths pass
  through A, and so A dominates X.
Qed.

Lemma [live-ancestry]. (tree-independent)
  If P is a path from X to Y, and Y is a live point, then X is a live
  point, and P is a life-preserving path.
Pf.
  Since Y is a live point, there exists a path PYF from Y to a function exit.
  Then (P..., PYF...) is a path from X to a function exit, so by definition,
  X is a live point.

  Suppose that P passed through an entry edge M -> N into a dead-end region;
  then there exist PI and PF such that
    P = (PI..., M -> N, PF...)
  But then (PF..., PYF...) is a path from <N to a function exit, contradicting
  the assumption that N is in a dead-end region. So P cannot pass through
  such an edge.
Qed.

Lemma [dead-end-region-ancestry]. (tree-independent)
  If P is a path from X to Y, and X is in a dead-end region, then
  Y is in a dead-end region.
Pf.
  Suppose that Y was in a live SCC; then Y is a live point, and so by
  [live-ancestry], X is also a live point, which contradicts the assumption
  that X is in a dead-end region. Therefore Y is in a dead-end region.
Qed.

Lemma [dead-end-region-path]. (tree-independent)
  If P is a life-preserving path, then the start point of P is in a
  dead-end region R if and only if the end point of P is in R.
Pf.
  Let X and Y be the start and end points of P.

  If Y is in a dead-end region R', then X is in R':
    Every point on P is in R', which we can prove by reverse structural
    induction on P. Let P' be a suffix of P.

    In the base case, P' is the empty path, and its start point, Y, is in R'
    by assumption.

    In the inductive case, P' := (K, P''...), and all points on P'' are in
    R' by the induction hypothesis. This includes K>.

    If K is a instruction, then <K is in the same block, and therefore the
    same SCC, as K>, which means the start point of P' is in R'.

    If K is an edge M -> N, then <N is in R', which is a dead-end region. K
    cannot be an entry edge into a dead-end region because of the assumption
    that P is life-preserving. So it must be an internal edge, which means M>
    is in the same region as <N, which is R'. Therefore the start point of
    P' is in R'.

    In all cases, the start point of P' is in R, and by induction, the
    start point of P is in R, and so X is in R.

  If X is in R:
    Y must be in a dead-end region R' by [dead-end-region-ancestry],
    so X is in R' by the helper lemma above. But we assumed that X is in R,
    so R = R', which means Y is in R.

  If Y is in R:
    X is in R by the helper lemma above.
Qed.

States and operations
---------------------

Lemma [push-cases].
  If PUSH@A' is well-formed for the transition from S' to S, then for all
  allocations A, exactly one of the following is true:
  #top:    A = A', S gives A allocated status, the last element of S is
           (A, allocated), and S' does not contain A, or
  #prefix: A != A', and S gives A status U if and only if S' gives A status U.
Pf.
  Because PUSH@A' is well-formed for the transition from S' to S,
    S = STATUS_PUSH(S', A') = (S'..., (A', allocated))
  and A' is not contained in S'.

  Let an allocation A be given.

  If A = A':
    (A, allocated) is the last element of S, which means by definition that
    S gives A allocated status. A is not contained in S because A' is not.
    Therefore #top is true. #prefix is not true because A = A'.

  If A != A', then:
    If A has status U in S':
      (A, U) must be an element of S'. S' is a prefix of S, so (A, U)
      must also be an element of S. Therefore A has status U in S.
    If A has status U in S:
      (A, U) must be an element of S, and S = (S'..., (A', allocated)),
      so either (A, U) is an element of S' or (A, U) = (A', allocated).
      But A != A', so the latter is impossible, and therefore (A, U)
      is an element of S', which means S' gives A status U.
    Therefore #prefix is true. #top is not true because A = A'.
Qed.

Lemma [push-preserves-preceding].
  If PUSH@A is well-formed for the transition from S' to S, then
  if S' gives A' some status U, S gives A' some status U.
Pf.
  By [push-cases], one of the following is true for A':
  If #top:
    S' does not contain A, so this is a contradiction.
  If #prefix:
    Under the conditions of this case, since S' gives A status U, S gives A
    status U.
Qed.

Lemma [push-allocated].
  If PUSH@A is well-formed for the transition from S' to S, then
  S gives A allocated status.
Pf.
  By [push-cases], one of the following is true for A:
  If #top:
    Under the conditions of this case, S gives A allocated status.
  If #prefix:
    Under the conditions of this case, A != A, which is a contradiction.
Qed.

Lemma [pop-cases].
  If POP@D is well-formed for the transition from S' to S, and A' is the
  allocation deallocated by D, then
  - S is a prefix of S'.
  - (A', allocated) is the final element of S', and therefore A has allocated
    status in S'.
  - For all allocations A, if S gives A status U, S' gives A status U.
  - For all allocations A, exactly one of the following is true:
    #absent: A != A', and neither S' nor S contains A;
    #top:    A = A', S' gives A allocated status, and S does not contain A;
    #popped: A != A', S' gives A pending status, the allocations in S' at all
             indexes following A other than the final index have pending
             status, and S does not contain A; or
    #prefix: A != A', S' and S both contain A and give it the same status, and
             if S' gives A pending status, there exists an index I' following A
             other than the final index of S' such that the allocation at that
             index has allocated status in S', and I' < LENGTH(S).
Pf.
  Because POP@D is well-formed for the transition from S' to S, S' does not
  repeat allocations, the undeallocatable allocations of S' are a prefix,
  the final element of S' is (A', allocated), and
    S = STATUS_POP(S', A') = PREFIX(S', I)
  where I is the smallest index such that all elements at I and later in S',
  except for the last, have pending status.

  Let an allocation A be given such that S gives A status U; then
  (A,U) is an element of S, which is a prefix of S', and so (A,U) is
  an element of S', and so S' gives A status U.

  A' is at index LENGTH(S') - 1 in S'. Because S' does not repeat
  allocations, A' is not at any other index in S'.

  Let an allocation A be given.

  If A = A':
    If A were in S, i.e. if A were in PREFIX(S', I), then I would have
    to be LENGTH(S') because A cannot be at any other index of S' except
    LENGTH(S') - 1. But then I' := LENGTH(S') - 1 would be a smaller
    index where all elements at indexes >= I' but != LENGTH(S') - 1 have
    pending status (because there are no such elements). So S does not
    contain A. Therefore #top is true. None of the others is true because
    A = A'.

  If A != A', and S' does not contain A:
    S is a prefix of S', so S also cannot contain A. Therefore [absent]
    is true. #top is not true because A != A'. #popped and #prefix are
    not true because S' does not contain A.

  If A != A', S' contains A, and the index IA of A in S' is >= I:
    By the construction of I, for all indexes J >= I, either
    J = LENGTH(S') - 1 or the status of the allocation at index J of S' is
    pending. IA >= I, so this is true of all indexes >= IA. IA cannot be
    LENGTH(S') - 1, because the allocation there is A', and we already
    know that A != A'; so the status of A (the allocation at index IA of S')
    is pending. If S contained A, it would have to be at some index J;
    since S is a prefix of S', it would be at index J of S', but that would
    mean that A repeats in S'; therefore S does not contain A.

    Therefore #popped is true. #absent is not true because S' contains A.
    #top is not true because A != A'. #prefix is not true because S
    does not contain A.

  If A != A', S' contains A, and the index IA of A in S' is < I:
    S = PREFIX(S', I), so an identical entry for A exists in S, which
    means S both contains A and gives A the same status as S'.

    Suppose that A has pending status in S':
      By assumption, I is the least index such that all elements at I
      and later in S', except for the last, having pending status.
      There must exist an index > IA but != LENGTH(S') - 1 that does not
      have pending status, or else IA would be a smaller such index.
      Let I' be the least such index. I' < I by the conditions on I,
      and so I' < LENGTH(S) = LENGTH(PREFIX(S', I)) = I. The element
      at I' does not have pending status in S', and it does not have
      undeallocatable status in S' because the undeallocatable allocations
      are a prefix of S' but A, the element at AI, which is less than I'
      by assumption, has pending status, not undeallocatable. Therefore
      the element at I' in S' has allocated status.

    Therefore #prefix is true. #absent is not true because S' contains A.
    #top is not true because A != A'. #popped is not true because
    the element at index I', which is >= IA and != LENGTH(S') - 1, has
    allocated status.
Qed.

Lemma [pop-preserves-prefix].
  If POP@D is well-formed for a transition from S' to S, and S gives
  some allocation A a status U, then S' gives A status U.
Pf.
  By [pop-cases], exactly one of the following is true for A:
  #absent: S does not contain A, which is a contradiction.
  #top:    S does not contain A, which is a contradiction.
  #popped: S does not contain A, which is a contradiction.
  #prefix: S' give A the same status as S does.
Qed.

Lemma [pend-cases].
  If PEND@D is well-formed for a transition from S' to S, and A' is the
  allocation deallocated by D, then for all allocations A, then
  - S contains A if and only if S' contains A; and
  - exactly one of the following is true:
    #changed: A = A', A is not the final allocation of either S' or S,
              S' gives A allocated status, and S gives A pending status.
    #kept:    A != A', and S' and S give A the same status U.
    #absent:  A != A', and neither S' nor S contain A.
Pf.
  Because O is part of a well-formed operation sequence, S' does not
  repeat allocations, the undeallocatable allocations of S' are a prefix,
  A' is not the final allocation of S', S' gives A' allocated status, and
    S = STATUS_PEND(S', A') = SET_STATUS(S', I, pending)
  where I is the smallest index such that the allocation at index I of S'
  is A'.

  Let an allocation A be given.

  If S' contains A, then let AI be the index of A in S'; SET_STATUS does
  not change the allocation sequence, so AI is also the index of A in
  SET_STATUS(S', I, pending), so S contain A.

  If S contains A, then let AI be the index of A in SET_STATUS(S', I, pending); SET_STATUS does not change the allocation sequence, so AI is also the index
  of A in in S', so S' contains A.

  If A = A':
    By substitution, S' gives A allocated status, and A is not the final
    allocation of S'. The sequence of allocations in the same in S' and
    SET_STATUS(S', _, _), so A is also not the final allocation of S.
    I is the smallest index of A in S', and it is unique because S' does
    not repeat allocations; so the allocation at index I of
    SET_STATUS(S', I, pending) is also A, and its status is pending
    by the definition of SET_STATUS, and so S gives A pending status.
    Therefore #changed is true. #kept and #absent are not true
    because A = A'.

  If A != A':
    If S' contains A:
      Let AI be the index of A in S'; S'[AI][0] = A. Let U = S'[AI][1].
      By definition, since AI is index of A in S', S' gives A the status U.

      By the axioms of SET_STATUS,
        SET_STATUS(S', I, pending)[AI][0] = S'[AI][0]
      so S contains A.

      AI != I because the allocation at index I in S' is A', and A != A'
      by assumption in this case. So by the axioms of SET_STATUS,
        SET_STATUS(S', I, pending)[AI][1] = S'[AI][1] = U
      So S gives A status U.

      Therefore #kept is true. #changed is not true because
      A != A', and #absent is not true because S' contains A.

    If S' does not contain A:
      Suppose S contained A; then let AI be the index of A in S, such that
      S[AI][0] = A. But by the axioms of SET_STATUS,
        SET_STATUS(S', I, pending)[AI][0] = S'[AI][0]
      so if S[AI][0] = A, then S'[AI][0] = A, which contradicts the assumption
      that S' does not contain A. So S does not contain A.

      Therefore #absent is true. #changed is not true because A != A'.
      #kept is not true because S' does not contain A.
Qed.

Lemma [pend-preserves-allocation-set].
  If PEND@D is well-formed for a transition from S' to S, then
  S contains some allocation A if and only if S' contains A.
Pf.
  By [pend-cases], exactly one of the following is true for A:
  #changed:   S' gives A allocated status and S gives A pending status,
              so both S' and S contain A.
  #kept:      S' and S both give A the same status U, so both contain A.
  #absent:    Neither S' nor S contain A.
Qed.

Lemma [conservative-merge-index].
  If S = CONSERVATIVE_MERGE(PSS(R)), and I < LENGTH(S), and S' is the end
  state of a block with an entry edge into R, then S[I][0] = S[I'][0].
Pf.
  By the axioms of CONSERVATIVE_MERGE, there exists a state S'' in PSS(R)
  such that S[I][0] = S''[I][0].

  By the axioms of CONSERVATIVE_MERGE, LENGTH(S) is a number such that,
  for all I' < LENGTH(S), for all S1 and S2 in PSS(R), S1[I'][0] = S2[I'][0].
  I < LENGTH(S), and S' and S'' are in PSS(R), so S'[I][0] = S''[I][0].
  By transitivity, S[I][0] = S'[I][0].
Qed.

Lemma [conservative-merge-predecessors].
  If CONSERVATIVE_MERGE(PSS(R)) contains an allocation A, then for all
  blocks B that have an entry edge into R, the state at B> contains A.
Pf.
  Let S = CONSERVATIVE_MERGE(PSS(R)). Let I be the index of A in S;
  that is, S[I][0] = A.

  Let an arbitrary block B that has an entry edge into R be given,
  and let S' be the state at B>. Then by [conservative-merge-index],
  S'[I][0] = S[I][0] = A. Therefore S' contains A. Since the choice of
  B was arbitrary, this is true for all such blocks.
Qed.

Lemma [merge-preserves-allocation-set-prefix].
  If MERGE@(X -> Y) is well-formed for a transition from S' to S,
  then if S contains some allocation A, and B is a block with an
  entry edge into the SCC containing Y, the state at B> contains A.

  In particular, the state at M> contains A.
Pf.
  Let R be the SCC containing Y. By the well-formedness rules
    S = STATE_MERGE(S', PSS(R)) = CONSERVATIVE_MERGE(PSS(R))
  So since S contains A, by [conservative-merge-predecessors],
  B> contains A.

  M is a block with an entry edge into R (namely, X -> Y), so by
  the previous conclusion, M> contains A.
Qed.

Allocation history
------------------

Definition [allocation history].
  The allocation history AH(A,P) of an allocation A on a path P is the
  sequence of allocations and deallocations of A that P passes through,
  in order:
    AH(A, P) = EDGE_FLAT_MAP(P, AH_ELEMENT(A))
  where
    AH_ELEMENT(A)(A)) = (A)             (if the equality holds)
    AH_ELEMENT(A)(D)) = (D)             (if D is a deallocation of A)
    AH_ELEMENT(A)(K)) = ()              (otherwise)

  A simplified allocation history is a string over the set {a,b}.
  If H is an allocation history, then AH_SIMPLIFY(H) produces a
  simplified allocation history corresponding to H, defined as:
    AH_SIMPLIFY(H) = MAP(H, AH_SIMPLIFY_ELEMENT)
  where
    AH_SIMPLIFY_ELEMENT(A) = a          (if A is an allocation)
    AH_SIMPLIFY_ELEMENT(D) = d          (if D is a deallocation)

  An allocation pattern is a regular expression over the terminals {a,d}.

  An allocation pattern R is said to match a history H if AH_SIMPLIFY(H) is in
  the language of R. (This implies a *complete* match.)

  Then the joint post-dominance axioms can be directly restated as follows:
    For all allocations A and initial paths P,
    - /d.*/ may not match AH(A,P),
    - /.*aa.*/ may not match AH(A,P),
    - /.*dd.*/ may not match AH(A,P), and
    - /.*a/ may not match AH(A,P) if P is also a terminating path.

  This is equivalent to saying that /(ad)*a?/ must match AH(A,P), and more
  specifically /(ad)*/ must match AH(A,P) if AH(A,P) is terminating.

  An allocation pattern R1 is a refinement of an allocation pattern R2 if
  the language of R1 is a subset of the language of R2.

  A singleton allocation pattern is an allocation pattern that matches exactly
  one simplified allocation history.

  The instruction-final prefix of a path P is PREFIX(P, I), where I is
  LENGTH(P) if P does not end in a edge and LENGTH(P) - 1 if it does.

  A path P is an instruction-simple path if its instruction-final
  prefix is a simple path.
End.

Lemma [history-concatenation]. (tree-independent)
  AH(A, (P1..., P2...)) = (AH(A, P1)..., AH(A, P2)...)
Pf.
  AH(A, (P1..., P2...)) = EDGE_FLAT_MAP((P1..., P2...), AH_ELEMENT(A))
                        = (EDGE_FLAT_MAP(P1, AH_ELEMENT(A))...,
                           EDGE_FLAT_MAP(P2, AH_ELEMENT(A))...)
                        = (AH(A, P1)..., AH(A, P2)...)
Qed.

Lemma [simplified-history-concatenation]. (tree-independent)
  AH_SIMPLIFY((H1..., H2...)) = (AH_SIMPLIFY(H1)..., AH_SIMPLIFY(H2)...)
Pf.
  AH_SIMPLIFY((H1..., H2...)) = MAP((H1..., H2...), AH_SIMPLIFY_ELEMENT)
                              = (MAP(H1, AH_SIMPLIFY_ELEMENT)...,
                                 MAP(H2, AH_SIMPLIFY_ELEMENT)...)
                              = (AH_SIMPLIFY(H1...), AH_SIMPLIFY(H2...))
Qed.

Lemma [history-pattern-concatenation]. (tree-independent)
  If R1 matches AH(A, P1) and R2 matches AH(A, P2), then the concatenation
  expression /(R1)(R2)/ matches AH(A, (P1..., P2...)).
Pf.
  Let S1 = AH_SIMPLIFY(AH(A, P1)) and let S2 = AH_SIMPLIFY(AH(A, P1)).

  By the definition of matching, S1 is in the language of R1 and S2 is in the
  language of R2.

  In the theory of regular expressions, the concatenation /(R1)(R2)/
  is defined as the expression whose language is the set
    { X where \exists X1,X2 . X = (X1..., X2...) /\
                              X1 is in the language of R1 /\
                              X2 is in the language of R2 }
  Then (S1..., S2...) is in that set.

  By [history-concatenation] and then [simplified-history-concatenation],
    AH_SIMPLIFY(AH(A, (P1..., P2...))) = AH_SIMPLIFY((AH(A, P1)..., AH(A, P2)...))
                                       = (AH_SIMPLIFY(AH(A, P1))...,
                                          AH_SIMPLIFY(AH(A, P2))...)
                                       = (S1..., S2...)
  So AH_SIMPLIFY(AH(A, (P1..., P2...))) is in the language of /(R1)(R2)/,
  and by definition that means /(R1)(R2)/ matches AH(A, (P1..., P2...)).
Qed.

Lemma [history-pattern-prefix-removal]. (tree-independent)
  If S1 is a simplified allocation history, and R is an allocation pattern,
  then there exists an allocation pattern R2 such that, for all simplified
  allocation histories S2, R matches (S1..., S2...) if and only if R2 accepts S2.
Pf.
  Let
    D = (Q, {a,d}, δ, q0, F)
  be a DFA corresponding to R. Let q1 = δ*(q0, S1). Then define
    D2 := (Q, {a,d}, δ, q1, F)
  and let R2 be a regular expression corresponding to D2.

  Suppose that R matches (S1..., S2...); by construction, D accepts
  (S1..., S2...). By the definition of DFA acceptance,
    δ*(q0, (S1..., S2...))
  is therefore some state q in F. But it is a well-known property of DFAs that
    δ*(q0, (S1..., S2...)) = δ*(δ*(q0, S1), S2)
  and substituting the definition of q1 gives
    δ*(q0, (S1..., S2...)) = δ*(q1, S2)
  which means that D2 accepts S2, and therefore R2 matches S2.

  Suppose that R2 matches S2; by construction, D2 accepts S2, and by definition
    δ*(q1, S2)
  is some state q in F. By substitution
    δ*(δ*(q0, S1), S2) = q
  and thus
    δ*(q0, (S1..., S2...)) = q
  and therefore D accepts (and R matches) (S1..., S2...).
Qed.

Lemma [history-prefix-removal]. (tree-independent)
  If R matches AH(A, (P1..., P2...)), and a singleton pattern R1 (with uniquely-
  matched history H1) matches AH(A, P1), and R2 is constructed such that the
  language of /(R1)(R2)/ is
    { S where (R matches S /\ S has a prefix H1) }
  then R2 matches AH(A, P2).
Pf.
  (Note that this would not be reliably true if R1 if were not a singleton
  pattern.)

  We are given that R1 matches AH(A, P1), which means that
  AH_SIMPLIFY(AH(A, P1)) is in the language of R1. Since R1 is a singleton
  allocation pattern, AH_SIMPLIFY(AH(A, P1)) = H1, the uniquely matched
  history of R1.

  Let S := AH_SIMPLIFY(AH(A, (P1..., P2...)))
  By [history-concatenation] and [simplified-history-concatenation]
    S = AH_SIMPLIFY((AH(A, P1)..., AH(A, P2)...))
      = (AH_SIMPLIFY(AH(A, P1))..., AH_SIMPLIFY(AH(A, P2))...)
      = (H1..., AH_SIMPLIFY(AH(A, P2))...)

  We are given that R matches AH(A, (P1..., P2...)) (as an allocation history),
  and therefore R matches S (as a simplified allocation history).
  Then by the construction of R2, S is in the language of /(R1)(R2)/.

  By the definition of matching a concatenation pattern, there must exist
  strings X1 and X2 such that S = (X1..., X2...) where R1 matches X1 and
  R2 matches X2. But R1 is a singleton pattern that only matches H1, so
  X1 must be H1. Since we have both
    S = (H1..., X2...) and
    S = (H1..., AH_SIMPLIFY(AH(A, P2))...)
  we must also have
    X2 = AH_SIMPLIFY(AH(A, P2))
  which means that R2 matches AH(A, P2).
Qed.

Lemma [history-path-narrowing]. (tree-independent)
  If P = (P', X -> Y), then AH(A, P) = AH(A, P').
  If P = (X -> Y, P'), then AH(A, P) = AH(A, P').
Pf.
  In the first case, by substitution and [history-concatenation],
    AH(A, P) = AH(A, (P', X -> Y)) = (AH(A, P')..., AH(A, (X -> Y))...)
  but AH(A, (X -> Y)) = () because an edge is neither an allocation nor
  a deallocation, so this concatenation simplifies to
    AH(A, P) = AH(A, P')

  In the second case, by substitution and [history-concatenation],
    AH(A, P) = AH(A, (X -> Y, P1)) = (AH(A, (X -> Y))..., AH(A, P')...)
  but AH(A, (X -> Y)) = () because an edge is neither an allocation nor
  a deallocation, so this concatenation simplifies to
    AH(A, P) = AH(A, P')
Qed.

Lemma [history-instruction-simple]. (tree-independent)
  If P is an instruction-simple path, R matches AH(A, P) if and only if
  R matches AH(A, P'), where P' is the instruction-final prefix of P.
Pf.
  If P does not end in an edge: P = P', so this is trivially true.
  If P does end in an edge:
    P = (P'..., X -> Y), so by [history-concatenation],
    AH(A, P) = AH(A, (P'..., X -> Y))
             = (AH(A, P')..., AH(X -> Y)...)
             = AH(A, P')
Qed.

Lemma [history-proper-ancestor]. (tree-independent)
  If P is a path to a point in a proper ancestor SCC of some SCC C, and
  A is an allocation in C, then // matches AH(A, P).
Pf.
  Let P_I be an initial path to the start point of P, and let
    P' = (P_I..., P...)
  P' passes only through components in proper ancestor SCCs of C, so
  it does not pass through A, and so its subpath P does not pass through
  A. If P' passed through a deallocation D of A, then since it is an
  initial path, it would also have to pass through A by the dominance
  axioms, which contradicts the previous conclusion; therefore P' does
  not pass through a deallocation of A, and so its subpath P does not
  either. Therefore P does not pass through either an allocation or a
  deallocation of A, which is to say that AH(A, P) = () and therefore
  // matches AH(A, P).
Qed.

Lemma [cyclic-scc-history]. (tree-independent)
  Let P be a reachable cyclic path. Then for all allocations A,
  /((ad)*|(da)*)/ must match AH(A, P).
Pf.
  Since P is reachable, there exists a path P_E from the entry
  point to the start point of P. Then
    P'  := (P_E..., P...)
    P'' := (P_E..., P..., P...)
  are both well-formed initial paths. Now let an allocation A be
  given.

  AH(A, P') must match /(ad)*a?/ by the axioms. This constrains
  AH(A, P) to match some suffix of that pattern, which (per standard
  regular expression theory) means it must match a pattern that can
  be expressed as the choice between patterns produced by taking
  a suffix at each of the sequence positions in the pattern. This
  produces /((ad)*a?|d(ad)*a?|a?|)/, which can be simplified to
  /((ad)*a?|d(ad)*a?)/ because /a?/ and // are subsets of /(ad)*a?/.

  But AH(A, P'') must also match /(ad)*a?/ by the axioms. Since P''
  contains P twice sequentially, P cannot start and end with the
  same kind of instruction, or else P'' will have that sequence.
  We can restrict the pattern by "unrolling" each non-empty choice
  to make it start and end with a terminal, adding back options
  that this excluded:

  First, forcing a terminal at the beginning of each clause:
    /(ad)*a?/    => /ad(ad)*a?/  (adding back /a?/)
    /a?/         => /a/          (adding back //)
    //           => //
    /d(ad)*a?/   => /d(ad)*a?/
  Next, forcing a terminal at the ending of each clause:
    /ad(ad)*a?/  => /ad(ad)*a/   (adding back /ad(ad)*/)
    /ad(ad)*/    => /ad(ad)*ad/  (adding back /ad/)
    /ad/         => /ad/
    /a/          => /a/
    //           => //
    /d(ad)*a?/   => /d(ad)*a/    (adding back /d(ad)*/)
    /d(ad)*/     => /d(ad)*ad/   (adding back /d/)
    /d/          => /d/

  Now we can exclude choices that begin and end with the same terminal.
    /ad(ad)*a/   => excluded
    /ad(ad)*ad/  => included
    /ad/         => included
    /a/          => excluded
    //           => included
    /d(ad)*a/    => included
    /d(ad)*ad/   => excluded
    /d/          => excluded

  And then reassemble the choice:
    /(ad(ad)*ad|ad||d(ad)*a)/
  which is equivalent to /((ad)*|(da)*)/.
Qed.

Lemma [history-reverse-concatenation]. (tree-independent)
  If /(R1)(R2)/ matches AH(A, P), then there exist P1 and P2 such that
    P = (P1..., P2...)
  where R1 matches AH(A, P1) and R2 matches AH(A, P2).
Pf.
  AH_SIMPLIFY(AH(A, P)) is in the language of /(R1)(R2)/.
  By the definition of the language of a concatenation regular expression,
  there exist simplified allocation histories S1 and S2 where
    AH_SIMPLIFY(AH(A, P)) = (S1..., S2...)
  such that R1 matches S1 and R2 matches S2.

  Let
    H1 := PREFIX(AH(A, P), LENGTH(S1))
    H2 := SUFFIX(AH(A, P), LENGTH(S1))
  Then
    H := (H1..., H2...)
       = (PREFIX(AH(A, P), LENGTH(S1))...,
          SUFFIX(AH(A, P), LENGTH(S1))...)
       = AH(A, P)

  AH_SIMPLIFY is a MAP operation, which preserves length.
    LENGTH(H1) = LENGTH(PREFIX(AH(A, P), LENGTH(S1)))
               = LENGTH(S1)
    LENGTH(H2) = LENGTH(SUFFIX(AH(A, P), LENGTH(S1)))
               = LENGTH(AH(A, P)) - LENGTH(S1)
               = LENGTH(AH_SIMPLIFY(AH(A, P))) - LENGTH(S1)
               = LENGTH((S1..., S2...)) - LENGTH(S1)
               = LENGTH(S1) + LENGTH(S2) - LENGTH(S1)
               = LENGTH(S2)
  So S1 = AH_SIMPLIFY(H1) and S2 = AH_SIMPLIFY(H2).
  By substitution and the definition of matching an allocation history,
  R1 matches H1 and R2 matches H2.

  AH(A,_) is a PATH_FLAT_MAP, so for all P1 and P2,
    AH(A,(P1..., P2...)) = (AH(A,P1)..., AH(A,P2)...)
  So since AH(A,P) = (H1..., H2...), there must be paths P1 and P2
  such that P = (P1, P2), AH(A, P1) = H1, and AH(A, P2) = H2.
  Then by substitution, R1 matches AH(A, P1) and R2 matches AH(A, P2).
Qed.

Lemma [history-reverse-partition]. (tree-independent)
  Let R2 = /a/ or /d/. Then if /(R1)(R2)(R3)/ matches AH(A, P), then
  there exist P_I and P_F such that
    P = (P_I..., K, P_F...)
  and where R1 matches AH(A, P_I), R3 matches AH(A, P_F), and
  K is either A (if R2 = /a/) or a deallocation of A (if R2 = /d/).
Pf.
  By [history-reverse-concatenation], there exist P1 and P2' such that
    P = (P1..., P2'...)
  and where R1 matches P1 and /(R2)(R3)/ matches P2'. Applying it again,
  there exist P2 and P3 such that
    P2' = (P2..., P3...)
  and where R2 matches P2 and /R3/ matches P3.

  If R2 = /a/, then AH(A, P2) must be (A); let K = A.
  If R2 = /d/, then AH(A, P2) must be (D) for some deallocation D of A;
  let K = D.
  K is on P2, so there exist PK1 and PK2 such that
    P2 = (PK1..., K, PK3...)
  Then by substitution
    P = (P1..., P2'...)
      = (P1..., P2..., P3...)
      = (P1..., PK1..., K, PK3..., P3...)
  So let P_I = (P1..., PK1...) and P_F = (PK3..., P3...); then
    P = (P_I..., K, P_F...)

  By substitution
    AH(A, P2) = AH(A, (PK1..., K, PK3...))
              = (AH(A, PK1)..., AH(A, (K))..., AH(A, PK3)...)
  But we know that AH(A, P2) = AH(A, (K)), so AH(A, PK1) = ()
  and AH(A, PK3) = ().

  Therefore
    AH(A, A_I) = AH(A, (P1..., PK1...))
               = (AH(A, P1)..., AH(A, PK1)...)
               = (AH(A, P1)..., ()...)
               = AH(A, P1)
  and therefore R1 matches AH(A, A_I).

  Similarly
    AH(A, A_F) = AH(A, (PK3..., P3...))
               = (AH(A, PK3)..., AH(A, P3)...)
               = (()..., AH(A, P3)...)
               = AH(A, P3)
  and therefore R3 matches AH(A, A_F).
Qed.

Proof of the algorithm
----------------------

Lemma [operation-sequence-concatenation-path]. (tree-independent)
  If PXY is the path in T from X to Y, PYZ is the path in T from Y to Z,
  SX is the state at X under T, and SY is the end state of
  OS_PATH(SX, PXY, T), then
    OS_PATH(SX, (PXY..., PYZ...), T) = (OS_PATH(SX, PXY, T)...,
                                        OS_PATH(SY, PYZ, T)...)
Pf.
  By induction on PYZ.

  For the base case, PYZ is an empty path. By the definiton of OS_PATH
    OS_PATH(SY, PYZ, T) = [ SY ]
  Then consider
    (OS_PATH(SX, PXY, T)..., OS_PATH(SY, PYZ, T)...)
  Since SY is the end state of OS_PATH(SX, PXY, T), this concatenation is
  proper and simplifies to OS_PATH(SX, PXY, T). Meanwhile, by substitution
    OS_PATH(SX, (PXY..., PYZ...), T) = OS_PATH(SX, (PXY..., ()...), T)
                                     = OS_PATH(SX, PXY, T)
  So the equality holds by transitivity.

  For the inductive case, PYZ = (PYZ'..., K), and by the induction hypothesis
    OS_PATH(SX, (PXY..., PYZ'...), T) = (OS_PATH(SX, PXY, T)...,
                                         OS_PATH(SY, PYZ', T)...)
  Let SZ be the end state of OS_PATH(SX, (PXY..., PYZ'...), T). By this
  equality, and the properties of operation sequence concatenation, SZ is also
  the end state of OS_PATH(SY, PYZ', T).

  OS_PATH(SY, PYZ, T)
    = OS_PATH(SY, (PYZ'..., K), T)                (by substitution)
    = (OS_PATH(SX, PYZ', T)...,                   (by the OS_PATH definition)
       OPERATION(SZ, K, T)...)

  OS_PATH(SX, (PXY..., PYZ...), T)
    = OS_PATH(SX, (PXY..., PYZ'..., K), T)        (by substitution)
    = OS_PATH(SX, ((PXY..., PYZ'...)..., K), T)   (by associativity)
    = (OS_PATH(SX, (PXY..., PYZ'...), T)...,      (by the OS_PATH definition)
       OPERATION(SZ, K, T)...)
    = ((OS_PATH(SX, PXY, T)...,                   (by the I.H.)
        OS_PATH(SY, PYZ', T)...)...,
       OPERATION(SZ, K, T)...)
    = (OS_PATH(SX, PXY, T)...,                    (by associativity)
       (OS_PATH(SY, PYZ', T)...,
        OPERATION(SZ, K, T)...)...)
    = (OS_PATH(SX, PXY, T)...,                    (by the equation above)
       OS_PATH(SY, PYZ, T)...)
Qed.

Lemma [entry-state]. (tree-independent)
  For all spanning trees T, the state at the entry point under T is
  STATE_EMPTY.

  STATE_EMPTY is a well-formed state.
Pf.
  Let a spanning tree T be given, and let P be the path to the entry point
  in T. This is necessarily the empty path. By definition
    OS(P, T) = OS_PATH(STATE_EMPTY, P, T)
  Applying the definition of OS_PATH
    OS(P, T) = [ STATE_EMPTY ]
  So the end point of OS(P, T) is STATE_EMPTY, which is to say, the state
  at the entry point under T is STATE_EMPTY.

  STATE_EMPTY is well-formed because it contains no allocations, so no
  allocations can repeat in it and the allocations having undeallocatable
  status trivially form a prefix of the state.
Qed.

Lemma [operation-sequence-path-helper]. (tree-independent)
  If SX is the state at X under T, and PXY is the path in T from X to Y,
  then the end state of OS_PATH(SX, PXY, T) is SY, the state at Y under T.
Pf.
  By the definition of state at a point, SX and SY are the end states of
  OS(PX, T) and OS(PY, T), where PX and PY are the paths to X and Y in T.
  Because T is a tree, it must be true that
    PY = (PX..., PXY...)
  Expanding the definition of OS:
    OS(PX, T) = OS_PATH(STATE_EMPTY, PX, T)
    OS(PY, T) = OS_PATH(STATE_EMPTY, PY, T)
  So SX is the end state of OS_PATH(STATE_EMPTY, PX, T).

  By [entry-state], EMPTY_STATE is the state at the entry under point under T.
  Therefore
    OS(PY, T) = OS_PATH(STATE_EMPTY, PY, T)
              = (OS_PATH(STATE_EMPTY, PX, T)....
                 OS_PATH(SX, PXY, T)...)
                                 (by [operation-sequence-concatenation-path])
  So SY, the end state of OS(PY, T), must also be the end state of
  OS_PATH(SX, PXY, T).
Qed.

Lemma [operation-sequence-concatenation]. (tree-independent)
  If PXY is the path in T from X to Y, PYZ is the path in T from Y to Z,
  SX is the state at X under T, and SY is the state at Y under T, then
    OS_PATH(SX, (PXY..., PYZ...), T) =
      (OS_PATH(SX, PXY, T)..., OS_PATH(SY, PYZ, T)...)

  And in particular,
    OS((PXY..., PYZ...), T) = (OS(PXY, T)..., OS_PATH(SY, PYZ, T)...)
Pf.
  By [operation-sequence-path-helper], SY is the end state of
  OS_PATH(SX, PXY, T). Then by [operation-sequence-concatenation-path],
    OS_PATH(SX, (PXY..., PYZ...), T) =
      (OS_PATH(SX, PXY, T)..., OS_PATH(SY, PYZ, T)...)

  OS((PXY..., PYZ...), T)
    = OS_PATH(STATE_EMPTY, (PXY..., PYZ...), T)         (by the OS definition)
    = (OS_PATH(STATE_EMPTY, PXY, T)...,
       OS_PATH(SY, PYZ, T)...)                          (by the above)
    = (OS(PXY, T)..., OS_PATH(SY, PYZ, T)...)           (by the OS definition)
Qed.

Lemma [correctness-operation-sequence-helper]. (tree-independent)
  For all spanning trees T1, if
  - P is a simple path in T1 from X to Y,
  - SX and SY are the states at X and Y under T1,
  - SX is well-formed, and
  - if SX contains some allocation A, then the path to X in T passes
    through A,
  then
  - OS_PATH(SX, P, T1) is well-formed under T1.
  - If SY contains some allocation A, but SX does not, then P passes
    through A.
  - If P is a life-preserving path, then for all spanning trees T2,
    if SX is also the state at X under T2, then
      OS_PATH(SX, P, T1) = OS_PATH(SX, P, T2).
Pf.
  By induction on P.

  If P is the empty path, then:
    By the definition of OS_PATH
      OS_PATH(SX, (), T1) = [ SX ]

    [ SX ] is a well-formed operation sequence under T1:
      The only state in [ SX ] is SX, and SX is well-formed by assumption.
      There are no operations in [ SX ], so all such operations are vacuously
      well-formed under T for the transition from their preceding state to
      their following state.

    If SY contains some allocation A, but SX does not, then P passes through A:
      Let A be given. By assumption, the end state of [ SX ] contains A; but
      the end state of [ SX ] is just SX, so this means SX contains A. This
      contradicts the assumption that SX does not contain A. So this holds
      (vacuously) for all allocations A.

    If P is a life-preserving path...:
      It is also true by the definition of OS_PATH that
        OS_PATH(SX, (), T2) = [ SX ]
      so OS_PATH(SX, (), T1) = [ SX ] = OS_PATH(SX, (), T2).

  Otherwise, P = (P'..., K), and Y = K>. Let SK be the end state of
  OS_PATH(SX, P', T1). Then by the definition of OS_PATH,
    OS_PATH(SX, P, T1) = (OS_PATH(SX, P', T1)..., OPERATION(SK, K, T1)...)

  Lemma [helper-induction-well-formed].
    If OPERATION(SK, K, T1) = [ SK, O, SY ], and SY is well-formed,
    and O is well-formed for the transition from SK to SY under T1,
    then OS_PATH(SX, P, T1) is well-formed under T1.
  Pf.
    By the induction hypothesis, OS_PATH(SX, P', T1) is well-formed under T1,
    and its end state is SK by construction. Then the concatenation in
      OS_PATH(SX, P, T1) = (OS_PATH(SX, P', T1)..., OPERATION(SK, K, T1)...)
    is proper, and this simplifies to
      OS_PATH(SX, P, T1) = [ OS_PATH(SX, P', T1)..., O, SY ]

    Then the states in OS_PATH(SX, P, T1) are the states in OS_PATH(SX, P', T1),
    plus SY; the former are all well-formed because OS_PATH(SX, P', T1) is
    well-formed, and the latter is well-formed by assumption.

    Similarly, the operation triples in OS_PATH(SX, P, T1) are the triples
    in OS_PATH(SX, P', T1), plus [ SX, O, SY ]; the former are all well-formed
    under T1 because OS_PATH(SX, P', T1) is well-formed under T1, and
    the latter is well-formed under T1 because O is well-formed for the
    transition from SX to SY under T1 by assumption.
  Qed.

  Lemma [helper-induction-allocation-present].
    If SK contains some allocation A, but SX does not, then P passes through A:
  Pf.
    By the induction hypothesis, P' passes through A, so P also passes through
    A because P' is a subpath of P.
  Qed.

  Lemma [helper-induction-life-preserving].
    If P is a life-preserving path, and T2 is a spanning tree, and SX is the
    state at X under T2, and
      OPERATION(SK, K, T1) = OPERATION(SK, K, T2)
    then
      OS_PATH(SX, P, T1) = OS_PATH(SX, P, T2).
  Pf.
    Let T2 be given, and suppose that SX is also the state at X under T2.
    By the definition of OS_PATH
      OS_PATH(SX, P, T2) = (OS_PATH(SX, P', T2)..., OPERATION(SK2, K, T2)...)
    where SK2 is the end state of OS_PATH(SX, P', T2).

    P' is a life-preserving path because it is a subpath of P and therefore
    cannot pass through any components that P does not pass through. So by the
    induction hypothesis, OS_PATH(SX, P', T1) = OS_PATH(SX, P', T2). In
    particular, SK2 = SK.

    Therefore we can substitute:
      OS_PATH(SX, P, T2) = (OS_PATH(SX, P', T2)..., OPERATION(SK2, K, T2)...)
                         = (OS_PATH(SX, P', T1)..., OPERATION(SK2, K, T2)...)
                         = (OS_PATH(SX, P', T1)..., OPERATION(SK, K, T2)...)
                         = (OS_PATH(SX, P', T1)..., OPERATION(SK, K, T1)...)
                         = OS_PATH(SX, P, T1)
  Qed.

  By the induction hypothesis, OS_PATH(SX, P', T1) is well-formed under T1,
  and SK is a state on OS_PATH(SX, P', T1), so SK is well-formed under T1.

  Now we can expand the definition of OPERATION(SK, K, T1).

  If K is an allocation A:
    Then the definition in this case gives
      OPERATION(SK, K, T1) = [ SK, PUSH@A, STATE_PUSH(SK, A) ]
    Therefore SY = STATE_PUSH(SK, A).

    STATE_PUSH(SK, A) has a precondition that SK must not contain A.
    Let PX be the path to X in T, and let
      PK' = (PX..., P'...)
      PK = (PX..., P'..., K)
    Suppose that SK contains A. Then PK' must pass through A:
      Either SX contains A or not. If SX contains A, then by assumption,
      PX passes through A, and so PK' passes through A because PX is a
      subpath of PK'. If SX does not contain A, then by the induction
      hypothesis, P' passes through A, and so PK' passes though A because
      P' is a subpath of PK'.
    PK is a concatenation of paths that are all in the same tree T, so it
    must also be a simple path. But PK' is a subpath of PK, and because
    PK' passes though K, it visits K> by definition; and (K) also visits
    K>, and not at index 0; so the concatenation of K' and (K), i.e. PK,
    must visit K> twice, which is a contradiction. Therefore SK does not
    contain A.

    SY is a well-formed state:
      By the definition of STATE_PUSH
        SY = (SK..., (A, allocated))

      SY[I][0] = SY[J][0] => I = J:
        If either I or J is LENGTH(SK), the allocation there in SY is A;
        by the precondition we just proved, there is no index I' in SK such
        that SY[I'][0] = A, so the other index must also be LENGTH(SK).
        Otherwise both I and J are < LENGTH(SK), so SY[I][0] = SK[I][0] and
        SY[J][0] = SK[J][0], so if SY[I][0] = SY[J][0] then SK[I][0] = SK[J][0]
        and thus I = J because SK is well-formed.

      SY[I][1] = undeallocatable /\ SY[J][1] != undeallocatable => I < J:
        I must be < LENGTH(SK) because the status there is allocated.
        If J = LENGTH(SK) then I < J. Otherwise SY[I][1] = SK[I][1]
        and SY[J][1] = SK[J][1], so this holds because SK is well-formed.

    PUSH@A changes SK to SY under T:
      OPERATION_APPLY(SK, PUSH@A) = STATE_PUSH(SK, A)
                                  = SY

    PUSH@A is well-formed for the transition from SK to SY in T1:
      PUSH@A satisfies its component restriction because A is an allocation.
      All of the other requirements have just been proven.

    So OS_PATH(SX, P, T1) is well-formed by [helper-induction-well-formed].

    If SY contains some allocation A', but SX does not, then P passes through A':
      Suppose that SY contains A' but SX does not. Then applying [push-cases]
      to A', one of the following is true:
      If #top: A' = A = K. P passes through K by assumption, so P passes
        through A.
      If #prefix: Since SY contains A, SK contains A, and P passes through
        A by [helper-induction-allocation-present].

    If P is a life-preserving path...:
      Let T2 be given, and suppose that SX is the state at X under T2. Then
        OPERATION(SK, K, T2) = [ SK, PUSH@A, STATE_PUSH(SK, A) ]
      because K is an allocation and there are no earlier cases of OPERATION.

      Therefore OPERATION(SK, K, T2) = OPERATION(SK, K, T1), so this
      conclusion holds by [helper-induction-life-preserving].

  If K is a deallocation D of an allocation A, and A has allocated
  status and is at the top of the stack in SK:
    Then the definition in this case gives
      OPERATION(SK, K, T1) = [ SK, POP@D, STATE_POP(SK, A) ]
    Therefore SY = STATE_POP(SK, A).

    STATE_POP(SK, A) has a precondition that the last element of SK is
    (A, allocated). This comes directly from the conditions on this case.

    SY is a well-formed state:
      SY = STATE_POP(SK, A) = PREFIX(SK, L) for some L whose exact value is
      unimportant here.

      SY[I][0] = SY[J][0] => I = J:
        By the axioms of PREFIX, SY[I][0] = SK[I][0] and SY[J][0] = SK[J][0],
        so this holds because SK is well-formed.

      SY[I][1] = undeallocatable /\ SY[J][1] != undeallocatable => I < J:
        By the axioms of PREFIX, SY[I][1] = SK[I][1] and SY[J][1] = SK[J][1],
        so this holds because SK is well-formed.

    POP@D changes SK to SY:
      OPERATION_APPLY(SK, POP@D) = STATE_POP(SK, DEALLOCATION(D))
                                 = STATE_POP(SK, A)
                                 = SY

    POP@D is well-formed for the transition from SK to SY in T1:
      POP@D satisfies its component restriction because D is a deallocation.
      All of the other requirements have just been proven.

    So OS_PATH(SX, P, T1) is well-formed by [helper-induction-well-formed].

    If SY contains some allocation A', but SX does not, then P passes through A':
      Suppose that SY contains an allocation A' but SX does not. Then applying
      [pop-preserves-prefix] to A', SK contains A'. Then P passes through A'
      by [helper-induction-allocation-present].

    If P is a life-preserving path...:
      Let T2 be given, and suppose that SX is the state at X under T2. Then
        OPERATION(SK, K, T2) = [ SK, POP@D, STATE_POP(SK, A) ]
      because the first case of OPERATION does not apply because K is not an
      allocation, and K is a deallocation D of A.

      Therefore OPERATION(SK, K, T2) = OPERATION(SK, K, T1), so this
      conclusion holds by [helper-induction-life-preserving].

  If K is a deallocation D of an allocation A, and A has allocated
  status and is not at the top of the stack in SK:
    Then the definition in this case gives
      OPERATION(SK, K, T1) = [ SK, PEND@D, STATE_PEND(SK, A) ]
    Therefore SY = STATE_PEND(SK, A).

    STATE_PEND(SK, A) has a precondition that SK has an element (A, allocatd)
    that is not the last element. This comes directly from the conditions on
    this case.

    SY is a well-formed state:
      SY = SET_STATUS(SK, AI, pending), where AI is the index of A in SK.
      Because (A, allocated) must be in SK, there is such an index AI, and so
      AI < LENGTH(SK), satisfying the precondition of SET_STATUS.

      SY[I][0] = SY[J][0] => I = J:
        SY[I][0] = SK[I][0] and SY[I][0] = SK[I][0] by the axioms of
        SET_STATUS, so this holds because SK is well-formed.

      SY[I][1] = undeallocatable /\ SY[J][1] != undeallocatable => I < J:
        If I = AI, then SY[I][1] = pending, which is a contradiction.
        So I != AI and SY[I][1] = SK[I][1] = undeallocatable.
        If J = AI, then SY[J][1] = pending and SY[J][1] = allocated;
          then since SK is well-formed, I < J.
        If J != AI, then SY[J][1] = SK[J][1]; then since SK is well-formed,
          I < J.

    PEND@D changes SK to SY:
      OPERATION_APPLY(SK, PEND@D) = STATE_PEND(SK, DEALLOCATION(D))
                                  = STATE_PEND(SK, A)
                                  = SY

    PEND@D is well-formed for the transition from SK to SY in T1:
      PEND@D satisfies its component restriction because D is a deallocation.
      All of the other requirements have just been proven.

    So OS_PATH(SX, P, T1) is well-formed by [helper-induction-well-formed].

    If SY contains some allocation A', but SX does not, then P passes through A':
      Suppose that SY contains an allocation A' but SX does not. Then applying
      [pend-preserves-allocation-set] to A', SK contains A'. Then P passes
      through A' by [helper-induction-allocation-present].

    If P is a life-preserving path...:
      Let T2 be given, and suppose that SX is the state at X under T2. Then
        OPERATION(SK, K, T2) = [ SK, POP@D, STATE_PEND(SK, A) ]
      because the first case of OPERATION does not apply because K is not an
      allocation, the second case of OPERATION does not apply because A
      is not at the end of SK, and K is a deallocation D of A.

      Therefore OPERATION(SK, K, T2) = OPERATION(SK, K, T1), so this
      conclusion holds by [helper-induction-life-preserving].

  If K is a conservative entry edge M -> N into a dead-end region R:
    Then the definition in this case gives
      OPERATION(SK, K, T1) = [ SK, MERGE@(M -> N), STATE_MERGE(SK, PSS(R, T1)) ]
    Therefore SY = STATE_MERGE(SK, PSS(R, T1)).

    STATE_MERGE(SK, PSS(R, T1)) has a precondition that SK is in PSS(R, T1).
    PSS(R, T1) is the set of all end states under T1 of all blocks that have
    entry edges into R. M has an entry edge into R, namely M -> N. P' is the
    path from X to M> in T1, and SX is the state at X under T1, so SK,
    the end state of OS_PATH(SX, P', T1), is the state at M> under T1 by
    [operation-sequence-path-helper]. Therefore SK is in PSS(R, T1).

    SY is a well-formed state:
      SY = CONSERVATIVE_MERGE(PSS(R, T1)). SK is a member of PSS(R, T1) by
      the precondition.

      SY[I][0] = SY[J][0] => I = J:
        By [conservative-merge-index], SY[I][0] = SK[I][0] and
        SY[J][0] = SK[J][0]. So this holds because SK is well-formed.

      SY[I][1] = undeallocatable /\ SY[J][1] != undeallocatable => I < J:
        By the axioms of CONSERVATIVE_MERGE, there is no J where
        SY[J][1] != undeallocatable, so this is vacuously true.

    MERGE@(M -> N) changes SK to SY:
      OPERATION_APPLY(SK, MERGE@(M -> N)) = STATE_MERGE(SK, PSS(SCC(N), T1))
                                          = STATE_MERGE(S', PSS(R, T1))
                                          = SY

    MERGE@(M -> N) is well-formed for the transition from SK to SY in T1:
      PEND@(M -> N) satisfies its component restriction because M -> N is a
      conservative entry edge. All of the other requirements have just been
      proven.

    So OS_PATH(SX, P, T1) is well-formed by [helper-induction-well-formed].

    If SY contains some allocation A', but SX does not, then P passes through A':
      Suppose that SY contains an allocation A', and let I be the index of A'
      in SY. SK is in SY by the precondition proven above.
      SY = CONSERVATIVE_MERGE(PSS(R, T1)), so by [conservative-merge-index],
      SY[I][0] = A', so SK[I][0] = A'. Therefore SK contains A, so by
      [helper-induction-allocation-present], P passes through A'.

    If P is a life-preserving path...:
      P passes through M -> N, an entry edge into a dead-end region, which
      contradicts the assumption that P is a life-preserving path.

  Otherwise:
    The definition in this case gives
      OPERATION(SK, K) = [ SK ]
    So SY = SK and OS_PATH(SX, P, T1) = OS_PATH(SX, P', T1).

    OS_PATH(SX, P, T1) is therefore well-formed by the induction hypothesis.

    If SY contains some allocation A', but SX does not, then P passes through A':
      Suppose that SY contains an allocation A', but SX does not. SY = SK,
      so SK contains A'; therefore P passes through A' by
      [helper-induction-allocation-present].

    If P is a life-preserving path...:
      Let T2 be given, and suppose that SX is the state at X under T2. Then
        OPERATION(SK, K, T2) = [ SK ]
      because the first three cases of OPERATION do not apply because K is
      not an allocation or deallocation, and the fourth case of OPERATION
      does not apply because, if K were any kind of entry edge into a dead-end
      region (conservative or not), then since P passes through K, the
      assumption that P is a life-preserving path would be contradicted.

      Therefore OPERATION(SK, K, T2) = OPERATION(SK, K, T1), so this
      conclusion holds by [helper-induction-life-preserving].

  So the conclusions hold for P no matter what case of OPERATION applies. By
  induction, they holds for all paths in T.
Qed.

Theorem [correctness-operation-sequence].
  If P is an initial path in T, OS(P) is well-formed.
Pf.
  The start point of P is the entry point, so by [entry-state], the state at
  the start point of P is STATE_EMPTY, and STATE_EMPTY is well-formed.

  Let OSP = OS_PATH(STATE_EMPTY, P). OSP is well-formed under T by
  [correctness-operation-sequence-path], and by definition OS(P) = OSP.
Qed.

Theorem [correctness-state].
  The state at any point is a well-formed state.
Pf.
  Let an arbitrary point X be given, and let P be the path to X in T.
  By definition, the state SX at X is the end state of OS(P).
  By [correctness-operation-sequence], OS(P) is a well-formed operation
  sequence, which means all states in it are well-formed, including
  the end state SX. So the state at X is a well-formed state.
Qed.

Lemma [present-implies-visit-path].
  If P is a path in T, and the state at the start point of P does not
  contain an allocation A, and the state at the end point of P does,
  then P passes through A.
Pf.
  Let S be the state at the start point of P. By [correctness-state],
  S is well-formed. Then by [correctness-operation-sequence-path],
  P passes through A.
Qed.

Lemma [present-implies-visit].
  If the state S at X contains an allocation A, the path P to X in T
  passes through A.
Pf.
  The start point of P is the entry point, so by [entry-state], the state at
  the start point of P is STATE_EMPTY, and STATE_EMPTY is well-formed.

  By definition, the state at X is the end point of OS(P).
  Let OSP = OS_PATH(STATE_EMPTY, P); by definition, OS(P) = OSP, so
  S must be the end state of OSP. Then P passes through A by
  [correctness-operation-sequence-path],
Qed.

Lemma [operation-sequence-path].
  If P is a path in T, then let S be the state at the start point of P.
  OS_PATH(S, P) is a well-formed operation sequence, and the end state of
  OS_PATH(S, P) is the state of the end point of P.
Pf.
  Let X be the end point of P, and let P_EX be the path to X in T;
  because T is a spanning tree, P must be a suffix of P_EX. Then by
  [operation-sequence-concatenation],
    OS(P_EX) = (OS(P_I)..., OS_PATH(S, P)...)

  OS_PATH(S, P) is therefore a suffix of OS(P_EX). Since OS(P_EX) is
  well-formed by [correctness-operation-sequence], OS_PATH(S, P) is as well.
  Since the state at X is by definition the end state of OS(P_EX), and the
  end states of OS(P_EX) and OS_PATH(S, P) are the same, the end state of
  OS_PATH(S, P) is the same as the state at X.
Qed.

Lemma [operation-sequence-component].
  For all point-graph components K in T, if S' is the state at <K and
  S is the state at K>, then OPERATION(S', K) is a well-formed operation
  sequence whose initial state is S' and whose final state is S; it
  contains at most one operation.
Pf.
  Let P be the path to K> in T. T is a spanning tree, so necessarily,
    P = (P_K..., K)
  By the definition of the state at a point, the state at K> is the end
  state of OS(P).

  By the definition of OS and OS_PATH
    OS(P) = OS_PATH(STATE_EMPTY, P)
          = OS_PATH(STATE_EMPTY, (P_K..., K))
          = (OS_PATH(STATE_EMPTY, P_K)..., OPERATION(S'', K)...)
  where S'' is the end state of OS_PATH(STATE_EMPTY, P_K), which by
  definition is the state of the end point of P_K, i.e. <K. Therefore
  S'' = S'. This must be the start state of OPERATION(S'', K) by the
  properness of the concatenation.

  By the path equality above, the end state of OPERATION(S', K) must be
  the same as the end state of OS(P), i.e. to S.

  By [correctness-operation-sequence], OS(P) is a well-formed operation
  sequence, so its subpath OPERATION(S', K) is also a well-formed
  operation sequence. By inspection of OPERATION, OPERATION(S', K) is
  either empty or a single operation.
Qed.

Lemma [operation-sequence-instruction].
  For all instructions I, if S' is the state at <I and S is the state
  at I>, then OPERATION(S', I) is either the empty operation sequence
  (in which case S' = S) or a single operation that changes S' to S.
Pf.
  All instructions are in T, so this follows immediately from
  [operation-sequence-component].
Qed.

Lemma [operation-cases-component].
  For all components K in T, let S' be the state at <K and S be the
  state at K>. Then one of the following is true:

  #push  PUSH@K is well-formed for the transition from S' to S;
  #pop   POP@K is well-formed for the transition from S' to S;
  #pend  PEND@K is well-formed for the transition from S' to S;
  #merge MERGE@K is well-formed for the transition from S' to S; or
  #other S = S', K is not an allocation, K is not a conservative entry edge,
         and either (K is not a deallocation of an allocation A, or
         A does not have allocated status in S').
Pf.
  By [operation-sequence-component], OPERATION(S', K) is well-formed,
  its start state is S', and its end state is S.

  Applying the definition of OPERATION:

  If K is an allocation:
    By definition
      OPERATION(S', K) = [ S', PUSH@K, STATE_PUSH(S', K) ]
    Because this is a well-formed operation sequence, PUSH@K is well-formed
    for the transition from S' to S.
    So this satisfies the requirements of the #push case.

  If K is a deallocation of an allocation A, and A has allocated status
  and is at the top of the stack in S':
    By definition
      OPERATION(S', K) := [ S', POP@K, STATE_POP(S', A) ]
    Because this is a well-formed operation sequence, POP@K is well-formed
    for the transition from S' to S.
    So this satisfies the requirements of the #pop case.

  If K is a deallocation of an allocation A, and A has allocated status
  and is no at the top of the stack in S':
    By definition
      OPERATION(S', K) := [ S', PEND@K, STATE_PEND(S', A) ]
    Because this is a well-formed operation sequence, PEND@K is well-formed
    for the transition from S' to S.
    So this satisfies the requirements of the #pend case.

  If K is a conservative entry edge into a dead-end region R:
    By definition
      OPERATION(S', K) := [ S', MERGE@K, STATE_MERGE(S', PSS(R)) ]
    Because this is a well-formed operation sequence, MERGE@K is well-formed
    for the transition from S' to S.
    So this satisfies the requirements of the #merge case.

  Otherwise:
    By definition
      OPERATION(S', C) := [ S' ]
    S is the same as the end state, so S = S'.
    Because OPERATION did not use the first case, K cannot be an allocation.
    Because OPERATION did not use the fourth case, K is not a conservative
    entry edge.

    Let
      PredA := K is not a deallocation of A
      PredB := A is not the top of the stack in S'
      PredC := S' does not give A allocated status
    Because OPERATION did not use the second case,
      PredA \/ PredB \/ PredC
    Because OPERATION did not use the third case,
      PredA \/ !PredB \/ PredC
    Together, these simplify to PredA \/ PredC.

    So this satisfies the requirements of the #other case.
Qed.

Lemma [operation-allocation].
  If A is an allocation, then PUSH@A is well-formed for the transition
  from the state at <A to the state at A>.
Pf.
  By [operation-cases-component], one of five cases applies:
  If #push:  The lemma holds by the conditions of this case.
  If #pop:   A is not a deallocation, so this a contradiction.
  If #pend:  A is not a deallocation, so this a contradiction.
  If #merge: A is not an edge, so this a contradiction.
  If #other: A is an allocation, so this is a contradiction.
Qed.

Lemma [allocation-state].
  If A is an allocation, then the state at A> gives A allocated status.
Pf.
  Let SA' and SA be the state at <A and A>, respectively.
  By [operation-allocation], PUSH@A is well-formed for the transition
  from SA' to SA. By [push-allocated], SA gives A allocated status.
Qed.

Lemma [operation-cases-edge].
  For all edges M -> N in T, let SM be the state at M> and SN be the
  state at <N. Then one of the following is true:
  #merge: MERGE@(M -> N) is well-formed for a transition from SM to SN; or
  #other: M -> N is not a conservative entry edge, and SM = SN.
Pf.
  By [operation-cases-component], one of five cases applies:
  If #push:  M -> N is not an allocation, so this is a contradiction.
  If #pop:   M -> N is not a deallocation, so this is a contradiction.
  If #pend:  M -> N is not a deallocation, so this is a contradiction.
  If #merge: All of the conditions of this lemma's #merge case hold.
  If #other: All of the conditions of this lemma's #other case hold.
Qed.

Lemma [operation-non-dead-entry-edge].
  If M -> N is an edge in T that is not an entry edge into a dead-end
  region, then the state SM at M> is the same as the state SN at <N.
Pf.
  By [operation-cases-edge], one of two cases applies:
  If #merge: Since MERGE@(M -> N) is well-formed for a transition from
    SM to SN, M -> N is a conservative entry edge; but this contradicts
    the assumption that it is not an entry edge into a dead-end region.
  If #other: In this case, SM = SN.
Qed.

Lemma [operation-cases-dead-entry-edge].
  If M -> N is a entry edge in T into a dead-end region R, and SM
  is the state at M> and SN is the state at <N, then SM is in PSS(R),
  and exactly one of the following is true:
  #merge: MERGE@(M -> N) is well-formed for a transition from SM to SN,
          M -> N is a conservative entry edge, PSS(R) is not singleton,
          and SN = CONSERVATIVE_MERGE(PSS(R)); or
  #other: M -> N is not a conservative entry edge, PSS(R) = { SN },
          and SM = SN.
Pf.
  By [operation-cases-edge], there are two cases:

  If #merge:
    Under this case, MERGE@(M -> N) is well-formed for the transition from
    SM to SN. So M -> N is a conservative entry edge and
      SN = CONSERVATIVE_MERGE(PSS(R)).
    PSS(R) contains SM by the well-formedness conditions.
    By the definition of a conservative entry edge, PSS(R) is not singleton.
    So this lemma's #merge case holds. #other does not hold because
    M -> N is a conservative entry edge.

  If #other:
    Under this case, M -> N is not a conservative entry edge and SM = SN.
    Since M -> N satisfies all the other conditions of being a conservative
    entry edge, PSS(R) must be singleton. M -> N is an entry edge into R,
    so SM, as the state at M>, in in PSS(R) by definition. Since PSS(R) is
    a singleton set containing SM, PSS(R) = { SN }.
    So this lemma's #other case holds. #merge does not hold because
    M -> N is not a conservative entry edge.
Qed.

Lemma [dead-end-entry-preserves-allocation-set-prefix].
  If M -> N is a entry edge in T into a dead-end region R, and B is an
  arbitrary block with an entry edge into R, then if A is
  in the state at <N, then A is in the state at B>.
Pf.
  Let SM be the state at M>, let SN be the state at <N, and let SB be the
  state at B>.

  By [operation-cases-edge], one of two cases must hold for M -> N:

  If #merge:
    Under this case, MERGE@(M -> N) is well-formed for the transition from
    SM to SN. By [merge-preserves-allocation-set-prefix], SB contains A.

  If #other:
    Under this case, PSS(R) = { SN }. By definition, PSS(R) is the set of
    all end states of blocks with entry edges into C; B is such a block,
    so SB is in PSS(R), which means that SB = SN. Since SN contains A,
    SB contains A.
Qed.

Lemma [absence-is-permanent].
  If a path P in T passes through an allocation A, and there is a point X
  following A on P where the state at X does not include A, then the state at
  the end of P must also not include A.
Pf.
  The only operation that can add an allocation that is not present in the
  preceding state is PUSH, so if the state at the end of P contains A, there
  must be a PUSH that adds A in the suffix of P that begins at X. This PUSH
  in OS(P) must correspond to visiting A itself in P, but by assumption, P
  already passes through A prior to reaching X. This would mean that P visits
  A twice, but P is a path in the spanning tree T and must be simple.
Qed.

Lemma [allocation-index].
  Let SA be the state at A>, for some allocation A. If the state S at some
  point X contains A, then:
  - LENGTH(S) >= LENGTH(SA),
  - for all I < LENGTH(SA), S[I][0] = SA[I][0], and
  - SA[LENGTH(SA) - 1][0] = S[LENGTH(SA) - 1][0] = A.
Pf.
  By structural induction on the path P to X in T.

  In the base case, P is the empty path at the entry point. The
  state at X is the empty stack, which does not contain A, so the
  implication holds vacuously.

  In the inductive case,
    P = (P'..., K)
  for some component K.

  By the inductive hypothesis, if S' contains A,
  - LENGTH(S') >= LENGTH(SA)
  - for all J < LENGTH(SA), S'[J][0] = SA[J][0], and, in particular,
  - SA[LENGTH(SA) - 1][0] = S'[LENGTH(SA) - 1][0] = A
  We must prove each of these for S instead of S'.

  Let S' be the state at <K. By [operation-sequence-component],
  OPERATION(S', K) is a well-formed operation sequence whose start state
  is S' and whose end state is S, and it contains at most one operation.

  If OPERATION(S', K) is the empty operation sequence, then S' = S,
  so all of the implications hold by the inductive hypothesis.

  Otherwise, there is an operation O that changes S' to S; we can
  proceed by cases on O.

  If O = PUSH@K:
    K is an allocation, and S = STATE_PUSH(S', K) = (S'..., (K, allocated)).
    LENGTH(S) = LENGTH(S') + 1, and therefore LENGTH(S) > LENGTH(S').

    If S contains A, let AI be index of A in S, such that S[AI][0] = A.
    Either AI < LENGTH(S') or AI = LENGTH(S').
    If AI = LENGTH(S'):
      S[AI][0] = (S'..., (K, allocated))[LENGTH(S')][0]
               = (K, allocated)[0]
               = K
      But S[AI][0] = A by assumption, so K = A. But this means the end
      point of P is A>, so S = SA. The first two implications then hold
      trivially. For the third,
        S[LENGTH(SA) - 1][0] = S[LENGTH(S) - 1][0]
                             = S[LENGTH(S')][0]
                             = (S'..., (K, allocated))[LENGTH(S')][0]
                             = (K, allocated)[0]
                             = K
                             = A

    If AI < LENGTH(S'):
      S[AI][0] = (S'..., (K, allocated))[AI][0]
               = S'[AI][0]
      Therefore S' contains A.

      LENGTH(S') >= LENGTH(SA) by the I.H., and since LENGTH(S) > LENGTH(SA),
      LENGTH(S) >= LENGTH(SA).

      Let an index J < LENGTH(SA) be given.
        S[J][0] = (S'..., (K, allocated))[J][0]
      Since J < LENGTH(SA), and LENGTH(SA) <= LENGTH(S') by the I.H., this
      can be simplified:
        S[J][0] = S'[J][0]
                = SA[J][0]    (by the I.H.)

      Finally,
        S[LENGTH(SA) - 1] = (S'..., (K, allocated))[LENGTH(SA) - 1][0]
      Since LENGTH(SA) - 1 < LENGTH(SA), and LENGTH(SA) <= LENGTH(S'),
        S[LENGTH(SA) - 1][0] = S'[LENGTH(SA) - 1][0]
      By the I.H. this is known to be A.

  If O = POP@K:
    K is an deallocation D of some allocation A, and
      S = STATE_POP(S', A) = PREFIX(S', L)
    for some index L whose exactly value isn't important here.

    If S contains A, let AI be the index of A in S, such that S[AI][0] = A.
      S[AI][0] = PREFIX(S', L)[AI][0]
               = S'[AI][0]
    So S'[AI][0] = A, and therefore S' contains A.
    Then by the I.H., S'[LENGTH(SA) - 1][0] = A, and since S' is a well-formed
    state, A cannot be repeated in it; this means AI = LENGTH(SA) - 1.

    LENGTH(S) = L. L > AI, and AI = LENGTH(SA) - 1, so L > LENGTH(SA) - 1.
    Therefore L >= LENGTH(SA), and so LENGTH(S) >= LENGTH(SA).

    Let an index J < LENGTH(SA) be given.
      S[J][0] = PREFIX(S', L)[J][0]
              = S'[J][0]
              = SA[J][0]    (by the I.H.)

    Finally,
      S[LENGTH(SA) - 1][0] = PREFIX(S', L)[LENGTH(SA) - 1][0]
                           = S'[LENGTH(SA) - 1][0]
                           = A    (by the I.H.)

  If O = PEND@K:
    K is an deallocation D of some allocation A, and
      S = STATE_PEND(S', A) = SET_STATUS(S', I, pending)
    for some index I whose value isn't important here.

    If S contains A, let AI be the index of A in S, such that S[AI][0] = A.
    Then by the axioms of SET_STATUS,
      S[AI][0] = SET_STATUS(S', I, pending)[AI][0]
               = S'[AI][0]
    So S'[AI][0] = A, and therefore S' contains A.

    LENGTH(S) = LENGTH(SET_STATUS(S', I, pending))
              = LENGTH(S')     (by the axioms of SET_STATUS)
              >= LENGTH(SA)    (by the I.H.)

    Let an index J < LENGTH(SA) be given.
      S[J][0] = SET_STATUS(S', I, pending)[J][0]
              = S'[J][0]    (by the axioms of SET_STATUS)
              = SA[J][0]    (by the I.H.)

    Finally,
      S[LENGTH(SA) - 1][0] = SET_STATUS(S', I, pending)[LENGTH(SA) - 1][0]
                           = S'[LENGTH(SA) - 1][0]   (by the axioms)
                           = A                       (by the I.H.)

  If O = MERGE@K:
    K is an entry edge X -> Y into some dead-end region R, and
      S = STATE_MERGE(S', PSS(R)) = CONSERVATIVE_MERGE(PSS(R))

    If S contains A, let AI be the index of A in S, such that S[AI][0] = A.

    S' is an element of PSS(R), so
      S[AI][0] = CONSERVATIVE_MERGE(PSS(R))[AI][0]
               = S'[AI][0]     (by the axioms of CONSERVATIVE_MERGE)
    So S'[AI][0] = A, and therefore S' contains A.
    Then by the I.H., S'[LENGTH(SA) - 1][0] = A, and since S' is a well-formed
    state, A cannot be repeated in it; this means AI = LENGTH(SA) - 1.

    LENGTH(S) = L. L > AI, and AI = LENGTH(SA) - 1, so L > LENGTH(SA) - 1.
    Therefore L >= LENGTH(SA), and so LENGTH(S) >= LENGTH(SA).

    Let an index J < LENGTH(SA) be given.
      S[J][0] = PREFIX(S', L)[J][0]
              = S'[J][0]
              = SA[J][0]    (by the I.H.)

    Finally,
      S[LENGTH(SA) - 1][0] = PREFIX(S', L)[LENGTH(SA) - 1][0]
                           = S'[LENGTH(SA) - 1][0]
                           = A    (by the I.H.)

  So by induction, the lemma holds for all points X.
Qed.

Lemma [deallocatability-preserving-path].
  If a path P is the path in T from X to Y, and P is
  deallocatability-preserving, then the prefix of undeallocatable allocations
  in the state SX of the X is the same as the prefix of deallocatable
  allocations in the state SY of Y.
Pf.
  By induction on P.

  In the base case, X = Y and so SX = SY, so the prefix of deallocatable
  allocations is the same.

  In the inductive case, P = (P'..., K). Let Y' be the end point of P',
  and let SY' be the state at Y'. By [operation-sequence-component],
  OPERATION(SY', K) is either the empty operation sequence or a single
  operation O that changes SY' to SY. If it is the empty sequence, then
  SY = SY' and so SY has the same prefix of undeallocatable instructions
  as SX. Otherwise, we proceed by cases:

  If O = PUSH@K:
    Then by construction
      SY = STATE_PUSH(SY', K) = (SY'..., (K, allocated))
    So SY still haas the same prefix of undeallocatable instructions as SY'
    and therefore as SX.
  If O = POP@K:
    Then by construction
      SY = STATE_POP(SY', K) = PREFIX(SY', I)
    for some I such that all allocations at index >= I have a status of
    either pending or allocated. So SY still haas the same prefix of
    undeallocatable instructions as SY' and therefore as SX.
  If O = PEND@K:
    Then by construction
      SY = STATE_PEND(SY', K) = SET_STATUS(SY', I, pending)
    for some I whose status is allocated in SY'. So SY still haas the same
    prefix of undeallocatable instructions as SY' and therefore as SX.
  If O = MERGE@(M -> N):
    Then M -> N is a conservative entry edge, but this contradicts our
    assumption that P does not pass through such an edge.

  Therefore the lemma holds for all paths P in T.
Qed.

Lemma [deallocatability-preserving-path-invariance].
  If a path P in T is deallocatability-preserving, then the state SX at
  the start point of P gives an allocation A undeallocatable status if
  and only if the state SY at the end point of P gives A undeallocatable
  status.
Pf.
  Let U be the prefix U of undeallocatable allocations in SX.
  By [deallocatability-preserving-path], U is the same as the prefix of
  undeallocatable allocations in SY.

  If SX gives A undeallocatable status, then SX has an element
  (A, undeallocatable), which must be in U by the well-formedness of SX,
  so SY also has such an element, so SY gives A undeallocatable status.

  If SY gives A undeallocatable status, then SY has an element
  (A, undeallocatable), which must be in U by the well-formedness of SY,
  so SX also has such an element, so SX gives A undeallocatable status.
Qed.

Lemma [scc-undeallocatable-invariance].
  The state at a point X gives an allocation A undeallocatable status if
  and only if the state at the entry point of the path to X in T for the SCC
  containing X gives A undeallocatable status.
Pf.
  Let P be the path to X in T, and let P_F be the SCC entry suffix of P for
  the SCC C containing X. Then P_F is a path entirely within C, so it passes
  through no entry edges at all, so it is deallocatability-preserving.
  Then the lemma holds by [deallocatability-preserving-path-invariance].
Qed.

Lemma [undeallocatable-implies-dead-end].
  If the state at a point X gives an allocation A undeallocatable status,
  then there exists a conservative entry edge M -> N into a dead-end region R
  such that
    P = (P_I..., M -> N, P_F...)
  where P is the path to X in T, and where P_F is a deallocability-preserving
  path. Furthermore, X is in a dead-end region.
Pf.
  Let U be the prefix of undeallocatable allocations in the state at X.
  U contains A by assumption.

  If P did not pass through a conservative entry edge, then by
  [deallocatability-preserving-path], the prefix of undeallocatable
  allocations in the state at the start point of P would have to also be U.
  But P is an initial path, so its start point is the entry point, so the
  state there is the empty stack. U is not empty because it contains A, so U
  cannot be a prefix of the empty stack.

  Therefore P does pass through a conservative entry edge; let M -> N be
  the last such edge that P passes through, such that
    P = (P_I..., M -> N, P_F...)

  P_F therefore does not pass through a conservative entry edge, so it is a
  deallocatability-preserving path.

  M -> N is an entry edge into a dead-end region, so <N is a point in a
  dead-end region. By [dead-end-path-ancestry], the end point of P_F, which
  is X, must be in a dead-end region.
Qed.

Lemma [undeallocatable-dead-end-entry].
  If the state at X gives some allocation A undeallocatable status,
  let P be the path to X in T, and let C be the SCC containing X. Then
    P = (P_I..., M -> N, P_F...)
  where M -> N is an entry edge into C, C is a dead-end-region, and
  the state at <N gives A undeallocatable status.
Pf.
  By [undeallocatable-implies-dead-end], C is a dead-end region, and
    P = (P_I'..., M' -> N', P_F'...)
  where M' -> N' is a conservative entry edge and P_F' is a
  deallocatability-preserving path.

  P is a path to a point in C that passes through an edge, so C is not the
  entry SCC. Therefore P must pass through an entry edge into C, although
  this is not necessarily M' -> N'. So by [scc-entry-edge-partition], let
    P = (P_I.., M -> N, P_F...)
  where M -> N is an entry edge into C and P_F is the SCC entry suffix
  of P for C.

  P_F is a suffix of P_F' by [scc-entry-suffix-suffix], so P_F is also a
  deallocatability-preserving path. Since the state at X (the end point of
  P_F) gives A undeallocatable status, the state at <N (the start point of
  P_F) must also give A undeallocatable status by
  [deallocatability-preserving-path.]
Qed.

Lemma [life-preserving-paths-undeallocatable-coherence].
  If P1 and P2 are life-preserving paths from X1 and X2 to the same point Y,
  and the state at X1 gives A undeallocatable status, the state at X2
  gives A undeallocatable status.
Pf.
  P1 and P2 do not pass through any conservative entry edges because they are
  life-preserving paths and so do not pass through any entry edges into
  dead-end regions at all. So by [deallocatability-preserving-path], the
  states at X1 and X2 have the same prefix of undeallocatable allocations as
  the state at Y, and so they have the same prefix as each other as well. So
  if X1 gives A undeallocatable status, then A is in that prefix, and X2 also
  gives A undeallocatable status.
Qed.

Lemma [undeallocatable-is-permanent].
  If an path P in T passes through an allocation A, and there is a point X
  following A on P where the state at X gives A undeallocatable status, then
  the state at the end of P must either not include A or give it
  undeallocatable status.
Pf.
  POP and PEND do not affect allocations that have undeallocatable status, and
  MERGE can only either leave it in undeallocatable status or remove it from
  the the state completely. So the only way that the state at the end of P
  can include A with a status other than deallocatable is if there is a PUSH
  that adds it; but as above, this must correspond to P passing through A for
  a second time on a simple path, which is impossible.
Qed.

Lemma [pending-is-permanent].
  If a path P in T passes through an allocation A, and there
  is a point X following A on P where the state at X gives A
  pending status, then the state at the end of P must either
  not include A, give it pending status, or give it undeallocatable
  status.
Pf.
  If the state at the end of P includes A and does not give it
  pending or undeallocatable status, it must give it allocated
  status. The only operation that can do this when the allocation
  is absent or has a non-allocated status in the preceding state
  is PUSH, and as above, this would require P visiting A twice
  and is impossible.
Qed.

Lemma [deallocation-is-permanent].
  If a path P in T passes through a deallocation D of allocation A, then the
  state at the end of P either does not include A or gives it a status other
  than allocated.
Pf.
  Let P and A be given which satisfy the conditions, and let D be a
  deallocation of D that P passes through. A dominates D, so A must appear
  earlier on P than D.

  If A is present and has allocated status in the state at <D, then D will
  correspond either to a POP or PEND operation. The state at D> will
  therefore either omit A or give it pending status. Otherwise, the state at
  <D must either omit A or give it either pending or undeallocatable status.
  By [absence-is-permanent], [undeallocatable-is-permanent], and
  [pending-is-permanent], the state at the end of the path must either not
  include A or give it a status other than permanent.

Lemma [allocated-implies-allocation-path].
  Let P be a path in T from point X to point Y. If the state SX
  at X does not contain X, and the state SY at Y gives A allocated status,
  then /a/ matches AH(A, P).
Pf.
  By [operation-sequence-path], OS_PATH(SX, P) is a well-formed operation
  sequence with SY as its final state.

  Since SY contains A, and SY is the final state of OS_PATH(SX, P), there
  must exist a least index K such that the state SK at index K in
  OS_PATH(SX, P) contains A. This cannot be the start index of
  OS_PATH(SX, P) because the state there does not contain A by assumption;
  therefore, there is some operation O preceding position K in
  OS_PATH(SX, P). The state SK' at index K - 1 in OS_PATH(SX, P) does not
  contain A (or the assumption that K is the least such index), and because
  OS_PATH(SX, P) is a well-formed path, O must change SK' to SK. The only
  operation that can add an allocation A to a state is PUSH@A, so
  O = PUSH@A. A is therefore on P.

  A path in T is a simple path, so P cannot pass through A twice.

  If P passed through a deallocation of A, it would have to be after it
  passed through A because A dominates all of its deallocations. Then the
  state at the end of P could not include A and give it allocated status
  because[deallocation-is-permanent]. So P does not pass through a
  deallocation of A.

  Since P passes through A a single time and does not pass through a
  deallocation of A, /a/ matches AH(A, P).
Qed.

Lemma [allocated-implies-allocation].
  If the state S at some point X gives an allocation A allocated status,
  then /a/ matches AH(A,P), where P is the path P to X in T.
Pf.
  Let P be the given to X in T. The state at the entry point
  does not contain A because it is the empty sequence, so by
  [allocated-implies-allocation-path], /a/ matches AH(A,P).
Qed.

Lemma [missing-implies-invariance].
  Let P be a path in T that does not pass through any edges into
  dead-end regions, and suppose that // matches AH(A, P) for some allocation
  A. Let SX and SY be the states at the start point and end point of P,
  respectively.

  If SX does not include A, SY does not include A.
  If SX gives A allocated status, SY gives A allocated status.
Pf.
  Let SX and SY be the states at the start and end points of P,
  respectively. By [operation-sequence-path], OS_PATH(SX, P) is a well-
  formed path whose end state is SY. Let OSP := OS_PATH(SX, P); by
  induction on OSP.

  If OSP is the empty path, then SX = SY, so both implications hold trivially.

  Otherwise, OSP = (OSP'..., O). Let SY' be the end state of OSP';
  then because OSP is well-formed, O changes SY' to SY.

  If O = PUSH@I:
    // matches AH(A, P), so I cannot be A; therefore SY' gives A status U if
    and only if SY gives A status U by by [push-cases].

  If O = POP@I:
    I is the deallocation of some allocation A'. By [pop-cases], one of the
    following four cases is true for A.

    If #absent:
      Neither SY nor SY' include A by the rules of this case.
      Suppose SX does not include A; then SY does not include A, because it
        doesn't regardless.
      Suppose SX gives A allocated status; then SY' must give A allocated status
        by the inductive hypothesis, but this is a contradiction.

    If #top:
      A' = A by the rules of this case, but // matches AH(A,P), so no
      deallocation of A can be on P; this is a contradiction.

    If #popped:
      SY' gives A pending status by the rules of this case.
      Suppose SX does not include A; then SY' does not include A by the
        induction hypothesis, so this is a contradiction.
      Suppose SX gives A allocated status; then SY' gives A allocated status
        by the induction hypothesis, so this is a contradiction.

    If #prefix:
      SY' and SY both contain A and give it the same status by the rules of
      this case.
      Suppose SX does not include A; then SY' does not include A by the
        induction hypothesis, so this is a contradiction.
      Suppose SX gives A allocated status; then SY' gives A allocated status
        by the induction hypothesis, so SY gives A allocated status.

  If O = PEND@I:
    I is the deallocation of some allocation A'. By [pend-cases], one of
    three cases is true:

    If #changed:
      A' = A by the rules of this case, but // matches AH(A,P), so no
      deallocation of A can be on P; this is a contradiction.

    If #kept:
      Under this case, SY' and SY both contain A and give it the same status.
      Suppose SX does not include A; then SY' does not include A by the
        induction hypothesis; but this is a contradiction because SY
        does gives A some status in this case.
      Suppose SX gives A allocated status; then SY' gives A allocated status
        by the induction hypothesis; so SY gives A allocated status.

    If #absent:
      Under this case, neitiher SY' nor SY contains A.
      Suppose SX does not include A; then SY' does not include A by the
        induction hypothesis, which is consistent with this case; then SY
        does not contain A by the conditions of this case.
      Suppose SX gives A allocated status; then SY' gives A allocated status
        by the induction hypothesis; but this is a contradiction because
        SY' does not contain A in this case.

  If O = MERGE@(M -> N):
    M -> N must be an edge into a dead-end block, but no such edges exists
    on P by assumption, so this a contradiction.

  Then by induction, the two implications hold for any path P that satisfies
  the conditions.
Qed.

Lemma [allocation-implies-allocated].
  Let P be a path in T that does not pass through any edges into dead-end
  regions such that /a/ matches AH(A, P) for some allocation. Then the
  state at the start point of P does not contain A, and the state at
  the end point of P gives A allocated status.
Pf.
  By [history-reverse-partition]
    P = (P_I..., A, P_F...)
  where // matches AH(A, P_I) and AH(A, P_F).

  Let XI be the start point of P, and let P_EI be the path to XI in T.
  If the state at XI contained A, then by [present-implies-visit], P_EI
  would pass through A; but then (P_EI..., P...) would pass through A
  twice, but all paths in T are simple because it is a spanning tree.

  So the state at XI does not contain A. Therefore the state SA' at <A
  does not contain A by [missing-implies-invariance]. OPERATION(SA', A)
  is (PUSH@A) by definition, and by [operation-sequence-instruction]
  its start state is SA' and its end state is the state SA at A>.
  Therefore
    SA = STATUS_PUSH(SA', A) = (SA'..., (A, allocated))
  and so SA gives A allocated status. Therefore the state at the end
  point of P_F gives A allocated status by [missing-implies-invariance],
  and by construction this is also the state at the end point of P.
Qed.

Lemma [pending-implies-deallocation].
  If the state S at some point X gives an allocation A pending
  status, then the path P to X in T passes through a deallocation
  of A which corresponds to a PEND operation on the operation
  sequence for that path. Furthermore, /ad/ matches AH(A,P).
Pf.
  By definition, S is the final state in OS(P). The empty stack does not give
  A pending status, so there is an earliest operation O in OS(P) such that
  the following state of O gives A pending status. Only PEND@D can make such
  a state change. D must be a deallocation of A, and by construction P passes
  through D.

  P must pass through A prior to D because of dominance. P cannot pass through
  A multiple times because it is a simple path. P cannot pass through
  multiple deallocations of A because that would violate joint
  post-dominance. Therefore /ad/ matches AH(A,P).
Qed.

Lemma [pop-implies-deallocated].
  Let O == POP@D be part of the operation sequence corresponding
  to some path P in T. If O removes an allocation A from its
  preceding state, then P passes through a deallocation of A.
Pf.
  To be removed by a POP operation, either A must be the top of the stack or A
  has pending status.

  If A has pending status, let PD be the subpath of P to <D. By
  [pending-implies-deallocation], P passes through a deallocation of A; since
  PD is subpath of P, P also passes through this deallocation.

  If A is the top of the stack, then D must itself be a deallocation of A, and
  by construction P passes through D.
Qed.

Lemma [merge-restricting-predecessor].
  If MERGE@(X -> Y) is well-formed for a transition from S' to S, then if S'
  contains some allocation A, and S does not, there exists a block B with an
  entry edge into the SCC containing Y such that the state at <B does
  not contain A.
Pf.
  Let R be the SCC containing Y. By the well-formedness rules
    S = STATE_MERGE(S', PSS(R)) = CONSERVATIVE_MERGE(PSS(R))

  Let SA be the state at A>. Let I be the index of A in S'. By
  [allocation-index], I = LENGTH(SA) - 1, and LENGTH(A) >= I.

  If I < LENGTH(S), then by S[I][0] = S'[1][0] by
  [conservative-merge-index], which contradicts the assumption that S does
  not contain A; therefore I >= LENGTH(S).

  By the axioms of CONSERVATIVE_MERGE, LENGTH(S) is the maximum L such that
  - for all S1 in PSS(R), L <= LENGTH(S1)
  - for all S1 and S2 in PSS(R), and for all I' < L, S1[I'][0] = S2[I'][0]

  So since I >= LENGTH(S), at least one of those must be false. Consider
  each in turn:

  If there exists an S1 in PSS(R) such that I >= LENGTH(S1):
    By the definition of PSS(R), S1 must be the end state of some block B
    with an entry edge into R.

    Suppose that S1 contains A. By [allocation-index],
    LENGTH(SA) <= LENGTH(S1). But I = LENGTH(SA) - 1, so I < LENGTH(S1).
    This contradicts the assumption that I >= LENGTH(S1). So S1 does not
    contain A.

    Therefore B satisfies the conditions of the lemma.

  If there exist S1 and S2 in PSS(R) such that, for some I' < LENGTH(S),
  S1[I'][0] != S2[I'][0]:

    Suppose that S1 and S2 both contain A. By [allocation-index], for all
    I'' < LENGTH(SA), S1[I''][0] = SA[I''][0] and S2[I''][0] = SA[I''][0].
    But I' < LENGTH(S), and LENGTH(S) <= I, and I = LENGTH(SA) - 1,
    and LENGTH(SA) - 1 < LENGTH(SA); transitively, then, I' < LENGTH(SA).
    That means that S1[I'][0] = SA[I'][0] = S2[I'][0], but that contradicts
    the assumption in this case that S1[I'][0] != S2[I'][0].

    Therefore at least one of S1 or S2 does not contain A. Whichever it is, it
    is in PSS(R) because there exists a block B of which it is the end state;
    let B be such a block. Then the end state of B does not contain A.
Qed.

Lemma [dead-end-entry-coherence].
  If X and Y are points in the same dead-end region R, then the states at
  the SCC entry points for R of the paths to X and Y in T are the same,
  and this state is either
  - the STATE_EMPTY, if R is the entry SCC;
  - the singleton element of PSS(R), if PSS(R) is a singleton; or
  - CONSERVATIVE_MERGE(PSS(R)).
Pf.
  Let PX and PY be the SCC entry prefixes of the paths to X and Y in T,
  and let SX and SY be the states at their end points.

  If R is the entry SCC, then those end points are the same point, the
  entry point. Then by [entry-state], SX = STATE_EMPTY = SY.

  Otherwise, PX and PY are non-empty, so by [scc-entry-prefix-ancestry]
    PX = (PX'..., MX -> NX)
    PY = (PY'..., MY -> NY)
  where MX -> NX and MY -> NY are entry edges into R. Let SX' and SY'
  be the states at MX> and MY>.

  Applying [operation-cases-dead-entry-edge] to MX -> NX, either
  SX' = SX and PSS(R) = { SX' }, or SX = CONSERVATIVE_MERGE(PSS(R))
  and PSS(R) is not singleton.

  Applying [operation-cases-dead-entry-edge] to MY -> NY, either
  SY' = SY and PSS(R) = { SY' }, or SY = CONSERVATIVE_MERGE(PSS(R))
  and PSS(R) is not singleton.

  If SX' = SX and PSS(R) = { SX' }:
    Then PSS(R) is singleton, so we must also have SY' = SY and
    PSS(R) = { SY' }. Therefore SX' = SY', and by subsitution, SX = SY.

  If SX = CONSERVATIVE_MERGE(PSS(R)) and PSS(R) is not singleton:
    Then we must also have SY = CONSERVATIVE_MERGE(PSS(R)), and by
    substitution, SX = SY.
Qed.

Lemma [absent-implies-missing-or-deallocation].
  If the state S at some point X does not include an allocation A, then either
  there exists an initial path to X that does not pass through A or there
  exists an initial path to X that passes through both A and a deallocation
  of A.
Pf.
  By structural induction on the SCC tree.

  Let a point X be given such that the lemma holds for all points in proper
  ancestor SCCs of the SCC C that contains X.

  Let PX be the path to X in T. If PX does not pass through A, then PX
  is an initial path to X that does not pass through A, satisfying the
  requirements of the lemma. Otherwise, partition PX at A>:
    PX = (PA..., PF...)
  PA is an initial path to A> in T; because T is a tree, PA is unique,
  which is to say, PA is *the* path to A> in T.

  Let SA', SA, and SX be the states at <A, A>, and X, respectively.

  By [allocation-state], SA gives A allocated status.

  By definition, SX is the end state of OS(PX). By
  [operation-sequence-concatenation]
    OS(PX) = OS((PA..., PF...))
           = (OS(PA)..., OS_PATH(SA, PF)...)
  By [correctness-operation-sequence], OS(PX) is well-formed. Therefore
  its subpath OS_PATH(SA, PF) is a well-formed operation sequence whose
  start state is SA and end state is SX.

  SA contains A, and by assumption, SX does not. Let I be the index of the
  first state in OS_PATH(SA, PF) that does not give A allocated status. I
  cannot be 0, because SA does give A allocated status. Let SM the state at
  index I - 1 in OS_PATH(SA, PF), and let SN be the state at index I in
  OS_PATH(SA, PF). Then we can parititon OS_PATH(SA, PF) at I - 1 and I:
    OS_PATH(SA, PF) = (OSP1..., O, OSP2...)

  Since [ SM, O, SN ] is a triple in OS_PATH(SA, PF), then by the definition
  of a well-formed operation sequence, the operation O must be well-formed for
  the transition from SM to SN. Remember that SM gives A allocated status
  and SN does not.

  Now we can consider the cases for O.

  If O = PUSH@K:
    By [push-preserves-preceding], since SM gives A allocated status, SN must
    give A allocated status. This is a contradiction.

  If O = POP@K:
    Applying [pop-cases] to A, one of the following is true:
    If #absent: In this case, SM does not contain A, a contradiction.
    If #top:    In this case, K is a deallocation of some allocation A',
                and A = A'. Therefore PF passes through a deallocation of A,
                and so PX is a path that passes through both A and a
                deallocation of A.
    If #popped: In this case, SM gives A pending status, a contradiction.
    If #prefix: In this case, since SM gives A allocated status, SN also
                gives A allocated status, a contradiction.

  If O = PEND@K:
    Applying [pend-cases] to A, one of the following is true:
    If #changed: In this case, K is a deallocation of some allocation A',
                 and A = A'. Therefore PF passes through a deallocation of A,
                 and so PX is a path that passes through both A and a
                 deallocation of A.
    If #kept:    In this case, since SM gives A allocated status, SN gives A
                 allocated status, a contradiction.
    If #absent:  In this case, SM does not contain A, a contradiction.

  If O = MERGE@K:
    In this case, K is an conservative entry edge into some region R.
    By [merge-restricting-predecessor], there exists a block B with an
    entry edge into R such that the state at B> does not contain A.
    By the definition of entry edge, the SCC containing B must be a
    proper ancestor of R.

    PF passes through K, so we can partition it around K:
      PF = (PFI..., K, PFF...)

    (PFI...) is a path from A> to B>, so the SCC containing A is an ancestor
    of the SCC containing B, which is a proper ancstor of R; therefore the
    SCC containing A is a proper ancestor of R.

    PFF is a path from K> (a point in R) to X (a point in C), which means R is
    an ancestor of C. Transitively, the SCC containing B is a proper ancestor
    of C. By the induction hypothesis, one of two cases is true:

    If there exists an initial path PB to B> that does not pass through A:
      Then define
        P' = (PB..., K, PFF...)
      P' is an initial path to X. The PB subpath does not pass through A
      by assumption. The (K) subpath does not pass through A because it is
      just a single edge. The PFF subpath does not pass through A because
      its start point is in R, so it cannot pass through any components in
      proper ancestors of R. Therefore P' does not pass through A, so P'
      satisfies the requirements of the lemma.

    If there exists an initial pah PB to B> that passes through both A
    and a deallocation of A:
      Then define
        P' = (PB..., K, PFF...)
      P' is an initial path to X, and because its PB subpath passes through
      A and a deallocation of A, P' must as well. So P' satisifes the
      requirements of the lemma.

  By induction, the lemma holds for all points.
Qed.

Theorem [deallocation-preconditions].
  In the state S at the point before a deallocation D of an allocation A, A is
  on the stack and does not have pending status.
Pf.
  Let P be the path to <D in T. P must pass through A because allocations must
  dominate their deallocations. P is a simple path because T is a spanning
  tree, so P can pass through A at most once.

  Suppose that S does not include A. Then by
  [absent-implies-missing-or-deallocation], there is a path P' to <D which
  either does not pass through A or passes through both A and a deallocation
  of A. In the latter case,(P'..., D) is a path from the entry point that
  includes A and two successive deallocations of A, which violates the rules
  of joint post-dominance. In the former case,(P'..., D) is a path from the
  entry point that includes a deallocation of A but not A, which violates the
  rules of dominance. So S must include A.

  Suppose that S gives A pending status. Then by
  [pending-implies-deallocation], there is a deallocation of A on P. But
  then (P..., D) is a path from the entry point that includes A and two
  successive deallocations of A, which violates the rules of joint
  post-dominance. So S cannot give A pending status.
Qed.

Lemma [stack-order].
  If the state at X has allocation B above allocation A,
  then the path to X in T passes through A before it
  passes through B.
Pf.
  By induction on the path P to X in T.
  In the base case, P is empty and the lemma is trivially true.

  In the inductive case, either
    P = (P'..., M -> N) or
    P = (P'..., I)
  Let S' be the state at X', the end point of P', and let
  S be the state at X.

  Let two allocations A and B be given such that B is above A in S.
  If A and B are both in S' and in the same order, then the induction
  hypothesis tells us that P' passes through A before it passes
  through B; this must also be true of P since P' is a subpath of P,
  so the lemma holds.

  If S = S', A and B must be in S' and in the same order, so the
  lemma holds. Otherwise, the last component of P must correspond
  to an operation O that changes the state from S' to S:

  If O is PUSH@I: The stack in S is exactly the stack in S'
    with I on top. A != I because there are no allocations above
    I in S. If B != I, then A and B must in the part of S unchanged
    by O, so they are both in S' and in the same order, and the lemma
    holds. Otherwise, B = I. A must be in S', so by
    [present-implies-visit], P' passes through A. P passes through B
    because B = I, and it does it this after P', so the lemma holds.

  If O is POP@I: The stack in S is a prefix of the stack in S',
    so A and B must be in S' and in the same order, so the lemma holds.

  If O is PEND@I: The stack in S is the same as the stack in S';
    only the statuses are different. So A and B must be in S' and
    in the same order, so the lemma holds.

  If O is MERGE@(M -> N): The stack in S is a prefix of the stack
    in S', so A and B must be in S' and in the same order, so the
    lemma holds.

  In all cases, the lemma holds. By induction it holds for all points.
Qed.

Definition [undeallocatable allocations set].
  The undeallocatable allocations set UDA(S) of a state S is the set of
  allocations having undeallocatable status in S.
End.

Lemma [no-merge-implies-no-deallocatable-change].
  If P is a path in T, SI and SF are the states at the start and end points
  of P, and OS_PATH(SI, P) does not contain any MERGE operations, then
  UDA(SI) = UDA(SF).
Pf.
  Let OSF = OS_PATH(SI, P). By [operation-sequence-path], OSF is a well-formed
  operation sequence, and SF is the state at the end point of P. By induction
  on OSF.

  In the base case, OSF is the empty operation sequence, so SI = SF
  and thus by substitution UDA(SI) = UDA(SF).

  In the inductive case, OSF = (OSF'..., O). Let SF' be the end state of OSF'.
  By the induction hypothesis, UDA(SI) = UDA(SF'). OSF is a well-formed
  operation sequence, so O must change SF' to SF. Consider the possible cases
  of O.

  If O = PUSH@A:
    By definition:
      SF = STATE_PUSH(SF', A)
         = (SF'..., (A, allocated))
    Therefore
      UDA(SF) = UDA((SF'..., (A, allocated)))
              = UNION(UDA(SF'), UDA(((A, allocated))))
              = UNION(UDA(SF'), {})
              = UDA(SF')
              = UDA(SI)

  If O = POP@D:
    D is a deallocation of A. By definition:
      SF = STATE_POP(SF', A)
         = PREFIX(SF', I)
    This could in theory remove allocations that undeallocated status,
    except that I is chosen such that all allocations in the suffix of SF'
    start at I have pending or allocated status. Therefore
    UDA(SF) = UDA(SF') = UDA(SI).

  If O = PEND@D:
    D is a deallocation of A. By definition:
      SF = STATE_PEND(SF', A)
         = SET_STATUS(SF', I, pending)
    SET_STATUS changes only the status of A, and A has allocated status in SF'
    and pending status in SF. Therefore UDA(SF) = UDA(SF') = UDA(SI).

  If O=MERGE@(X -> Y):
    By assumption, there are no MERGE operations on OSF.

  Therefore UDA(SF) = UDA(SI) in all cases, and by induction, the lemma holds
  for all paths in T.
Qed.

Lemma [stack-order-consistency].
  For all points X and Y, if the states at X and Y contain two different
  allocations A and B, they contain them in the same order.
Pf.
  Suppose A is below B in the state at X, but B is below A
  in the state at Y. Let PX be the path to X in T, and let
  PY be the path to Y in T. Then by [stack-order],
    PX = (PX1..., A, PX2..., B, PX3...)
    PY = (PY1..., B, PY2..., A, PY3...)
  But then (A, PX2..., B, PY2..., A) would be a cyclic path
  in T, which is an acylic graph.
Qed.

Lemma [state-differences-excess].
  If SX and SY are well-formed states, and LENGTH(SX) > LENGTH(SY),
  then SY does not contain the allocation that is at LENGTH(SY) in SX.
Pf.
  Let A be the allocation at LENGTH(SY) in SX, and let SA be the state
  at A>. By [allocation-index], since SX contains A,
    SX[LENGTH(SA) - 1] = A.
  SX is a well-formed state and so cannot repeat allocations, so
  LENGTH(SY) = LENGTH(SA) - 1, and thus LENGTH(SY) < LENGTH(SA).

  Suppose SY contains A; then by [allocation-index], LENGTH(SY) >= LENGTH(SA).
  But this is a contradiction, so SY cannot contain A.
Qed.

Lemma [state-differences-allocation-mismatch].
  If SX and SY are well-formed states of the same length, and there exists
  an index I such that SX[I][0] != SY[I][0], then SY does not contain
  the allocation that is at I in SX.
Pf.
  Let A be the allocation at I in SX, and let SA be the state at A>.
  By [allocation-index], since SX contains A,
    SX[LENGTH(SA) - 1][0] = A.
  SX is a well-formed state and so cannot repeat allocations, so
  I = LENGTH(SA) - 1.

  Suppose SY contains A; then by [allocation-index],
    SY[LENGTH(SA) - 1][0] = A
  But by substitution, this means SY[I][0] = A, and so SY[I][0] = SX[I][0],
  which contradicts the assumption of the lemma. Therefore SY cannot contain A.
Qed.

Lemma [state-differences].
  Let SX be the state at some point X and SY be the state at some point Y.
  Then either
  1. For some allocation A, SX gives A status U but SY does not.
  2. For some allocation A, SY gives A status U but SX does not.
  3. SX = SY.
Pf.
  By [correctness-state], SX and SY are well-formed states.

  Exhaustively, either LENGTH(SX) = LENGTH(SY), LENGTH(SX) < LENGTH(SY),
  or LENGTH(SX) > LENGTH(SY).

  If LENGTH(SX) > LENGTH(SY):
    Let A be the allocation at LENGTH(SY) in SX; SX gives A some status U.
    By [state-difference-excess], SY does not contain A, so SY cannot give
    A the status U.

  If LENGTH(SX) < LENGTH(SY):
    Let A be the allocation at LENGTH(SX) in SY; SY gives A some status U.
    By [state-difference-excess], SX does not contain A, so SX cannot give
    A the status U.

  If LENGTH(SX) = LENGTH(SY):
    If SX != SY:
      There exists a first index I such that SX[I] != SY[I].
      If SX[I][0] = SY[I][0]:
        It must be the case that SX[I][1] != SY[I][1], which is to say,
        that SX and SY give the allocation SX[I][0] different statuses,
        so SX gives SX[I][0] the status SX[I][1] and SY does not.
      If SX[I][0] != SY[I][0]:
        By [state-differences-allocation-mismatch], SY does not contain
        the state at SX[I][0], so SX gives it the status SX[I][1] and
        SY does not.
    If SX = SY:
      Then the states do not differ.
Qed.

Lemma [state-differences-specific].
  Let SX be the state at some point X and SY be the state at some point Y.
  Then either
  1. For some allocation A, SX gives A undeallocatable status but SY does not.
  2. For some allocation A, SY gives A undeallocatable status but SX does not.
  3. For some allocation A, SX gives A allocated status but SY either does not
     contain A or gives it pending status.
  4. For some allocation A, SY gives A allocated status but SX either does not
     contain A or gives it pending status.
  5. For some allocation A, SX gives A pending status but SY does not contain A.
  6. For some allocation A, SY gives A pending status but SX does not contain A.
  7. SX = SY.
Pf.
  By [state-differences], one of three things must be true.
  If there exists A where SX gives A status U but SY does not:
    If U = undeallocatable: We have case (1).
    If U = allocated:
      If SY gives A undeallocatable status: We have case (2).
      If SY does not give A undeallocatable status: We have case (3).
    If U = pending:
      If SY gives A undeallocatable status: We have case (2).
      If SY gives A allocated status: We have case (4).
      If SY gives A pending status: Contradiction.
      If SY does not contain A: We have case (5).
  If there exists A where SY gives A status U but SX does not:
    If U = undeallocatable: We have case (2).
    If U = allocated:
      If SX gives A undeallocatable status: We have case (1).
      If SX does not give A undeallocatable status: We have case (4).
    If U = pending:
      If SX gives A undeallocatable status: We have case (1).
      If SX gives A allocated status: We have case (3).
      If SX gives A pending status: Contradiction.
      If SX does not contain A: We have case (6).
  If SX = SY:
    We have case (7).
Qed.

Lemma [presence-implies-presence].
  If the state at X contains A, then the path P to X in T passes through A,
  and the state at all points in the suffix of P beginning at A> contains A.
Pf.
  P passes through A by [present-implies-visit]. Let PF be the suffix of P
  beginning at A>:
    P = (PA..., A, PF...)
  Let a point Y on PF given. Y follows A on P.

  Suppose that the state at Y did not include A. Then by [absence-is-permanent],
  the state at the end point of P must not contain A. But the end point of P
  is X, and the state at X contains A by assumption. Therefore this is a
  contradiction, and the state at Y must include A.
Qed.

Lemma [dominance-implies-precedes].
  For all points X, if the state SX at X contains allocations A and B, and A
  dominates B, then AI < BI, where AI and BI are the indices of A and B in S.
Pf.
  Let P be the path to X in T. By [present-implies-visit], P passes through B;
  then let P be partitioned around B:
    P = (PB..., B, PBX...)
  P is an initial path, so PB is an initial path. Since A dominates B, and
  PB is an initial path to <B, PB passes through A; then let PB be partitioned
  around A:
    PB = (PA..., A, PAB...)
  Thus:
    P = (PA..., A, PAB..., B, PBX...)

  Let SA and SB be the states at A> and B>.

  By [allocation-index] for SX and A, AI = LENGTH(SA) - 1.
  By [allocation-index] for SX and B, BI = LENGTH(SB) - 1, and BI is also
  the index of B in SB.

  B> is on the suffix of P beginning at A>, so by [presence-implies-presence],
  SB contains A. Then by [allocation-index] for SB and A,
  LENGTH(SA) <= LENGTH(SB), and the index of A in SB is LENGTH(SA) - 1. This
  means that LENGTH(SA) - 1 <= LENGTH(SB) - 1, and therefore AI <= BI. But
  AI != BI because then SX would have to contain both A and B at that index.
  Therefore AI < BI.
Qed.

Theorem [correctness-invariant-3].
  For all points X, if the state S at X is not the empty stack,
  the top of the stack at S does not have pending status.
Pf.
  No well-formed operation sequence ever leaves the top of
  the stack having pending status. We prove this by structural
  induction on the sequence.

  In the base case, the end state of the sequence is the empty
  stack, which contains no allocations.

  Let an OS := (OS'..., O) be given, and assume the induction
  hypothesis is true for OS'; therefore the end state of OS'
  does not give the top of the stack (if any) pending status.
  Now consider O:
  - If O is PUSH, the end state of OS gives the top allocation
    allocated status.
  - If O is POP, the end state of OS removes the top allocation
    and then iteratively removes all allocations in the pending
    status; the top allocation in the end state of OS can never
    have pending status, or it would have been popped as well.
  - If O is PEND, then the status of the top allocation in the
    end state of OS is the same as it was in the end state of
    OS', which by the induction hypothesis was not pending.
  - If O is MERGE, then the end state of OS gives every
    allocation remaining on the stack undeallocatable status,
    so the top allocation (if any) cannot have pending status.

  Therefore this is true for all well-formed operation
  sequences, and since S is by definition the end-state of a
  well-formed operation sequence, S does not give the top of
  the allocation stack pending status.
Qed.

Theorem [correctness-invariant-4].
  For all points X, if the state S at X contains an allocation A having
  undeallocatable status, every allocation below A on the stack at S also has
  undeallocatable status.
Pf.
  By [correctness-state], S is a well-formed state, from which this follows
  immediately.
Qed.

Lemma [simple-path-dominance-transition]. (tree-independent)
  For all simple paths P and points X, Y, and Z, if X precedes
  Y on P, Y precedes Z on P, and X does not dominate Y, then
  X also does not dominate Z.
Pf.
  Let P, X, Y, and Z be given that satisfy the conditions.
  Let P_YZ be the subpath of P from Y to Z. Because P is a simple
  path and X occurs earlier on it, X cannot occur on P_YZ.
  As X does not dominate Y, there must be a path P_EY from the
  entry point to Y that does not pass through X. Then the path
  (P_EY..., P_YZ...) is a path from the entry point to Z that
  does not pass through X, meaning X does not dominate Z.
Qed.

Lemma [nested-allocations-are-dominated].
  If a path P in T passes through an allocation A, then
  for all points X on P dominated by A, all of the allocations
  on the stack in the state at X are dominated by A.
Pf.
  Let A, P, and X be given. If an allocation B is on the stack
  in the state at X, B must precede X in P. Meanwhile, if B
  is above A on the stack at X, then PUSH@B must appear after
  PUSH@A in OS(P), so P must pass through B after it passes
  through A. A must therefore dominate B, or else A would not
  dominate X by [simple-path-dominance-transition], which
  contradicts our assumptions.
Qed.

Theorem [correctness-invariant-5].
  For all points X, for every allocation A in the state S at X,
  if A has pending status in S, then S also contains an
  allocation B dominated by A which S gives allocated status.
Pf.
  Let T and X be given, and let P be the path to X in T.

  By induction on P. In the base case, P is the empty path,
  so S is the empty stack. Since it contains no allocations,
  it satisfies the theorem trivially.

  Now suppose that P is either (PI..., I) or (PI..., X -> Y).
  Let SI be the state at the end point of PI; the inductive
  hypothesis tells us that the theorem holds for SI.
  If S = SI, then the theorem also holds for S. Otherwise,
  the final component of P must correspond to an operation O
  which changes the state from SI to S. We proceed by cases:

  O is PUSH@A: S is exactly SI, but with A pushed onto the stack
    and having allocated status. So let an allocation A' in S
    be given. If A' = A, then A' does not have pending status in
    S. Otherwise, SI must also have A' with pending status,
    and so there is a B in SI dominated by A that has allocated
    status. B must still exist in S with the same status.

  O is MERGE@(X -> Y): All the allocations in S must have
    undeallocatable status, so the theorem holds trivially.

  O is PEND@D: Let A be the allocation deallocated by D.
    A dominates D, so P must pass through A. Therefore, by
    [nested-allocations-are-dominated], all of the allocations
    above A on the stack in the state at <D (i.e. SI) are
    dominated by A. Furthermore, the allocation AT at the top of
    the stack in SI must have allocated status:
    - AT does not have pending status in SI by
      [correctness-invariant-3].
    - AT does not have undeallocatable status in SI by
      [correctness-invariant-4], since A has allocated status
      in SI and is beneath B on the stack.
    AT != A because the allocation whose status is changed by
    PEND cannot be the top of the stack. Therefore the status
    of AT is not changed by O, so it still has allocated status
    in S.

    Now let an allocation A' in S be given.

    If A' = A: AT satisfies the conditions for the theorem.

    If A' != A: the status of A' is not changed by O, so if
    A' has pending status in S, it must have pending status
    in SI. Then by the inductive hypothesis, let B be an
    allocation in SI dominated by A' that has allocated
    status in SI. If B != A, then the status of B is not
    changed in S, so B still satisfies the conditions of
    the theorem. Otherwise, B = A, so we now know that A'
    dominates A, and since dominance is transitive, A' must
    dominate AT. Since AT has allocated status in S, it
    satisfies the conditions of the theorem.

  O is POP@D: Let A be the allocation deallocated by D.
    O removes A from S, as well as some number of other
    allocations that all have pending status in SI.

    Let A' be an allocation in S that has pending status
    in S. O does not give any allocations pending status,
    so A' must also have pending status in SI. By the
    inductive hypothesis, let B be an allocation in SI
    dominated by A' which has allocated status in SI.
    Because B has allocated status in SI, it cannot be
    one of the additional allocations removed by O.

    If B != A, then B still exists in S and has allocated
    status, and so it satisfies the condition.

    If B = A, then B must dominate <D since D is a
    deallocation of A. Since A' dominates B and
    dominance is transitive, A' dominates <D.
    Therefore A' dominates every allocation above it on
    the stack in SI by [nested-allocations-are-dominated].
    Because A' has pending status in SI, and O did not
    remove A from S, there must be an allocation AT above
    A' in the stack in SI which not have pending status
    and therefore blocked POP from removing A'. AT cannot
    have undeallocatable status in SI by
    [correctness-invariant-4] because A' is below it on the
    the stack and has allocated status in SI. O does not
    change the status of any allocations it leaves on the
    stack, so AT must still be in S and have allocated status.
    Since AT is dominated by A', it satisfies the conditions
    of the theorem.

  Therefore by induction the theorem holds for all points X.
Qed.

Lemma [live-undeallocatable].
  If X is a point that is not in a dead-end region, then the operation
  sequence for the path to X in T does not include any MERGE operations,
  and there are no allocations that have undeallocatable status in the
  state at X.
Pf.
  A MERGE operation can only correspond to an entry edge into a dead-end
  region, so if there is a MERGE operation on OS(P), there is an edge X -> Y
  on P such that Y is in a dead-end region. But then the suffix of P
  beginning at <Y, concatenated with a path from X to a function exit
  (which must exist because X is not in a dead-end region), is a path from a
  block supposedly in a dead-end region to a function exit, which is a
  contradiction.

  OS(P) = OS_PATH(STATE_EMPTY, P), and STATE_EMPTY is the state at the entry
  point. Let SX be the state at X; then UDA(SX) = UDA(STATE_EMPTY) by
  [no-merge-implies-no-deallocatable-change], and since UDA(STATE_EMPTY)
  is the empty set, there are no allocations that undeallocatable status
  in SX.
Qed.


Coherence
---------

In this section, we are building up to a proof that states are always
consistent within the depth-first search. That is, if the depth-first
search *doesn't* take an edge because it's already enqueued the destination
block, the current state is the same as what the destination block is
ultimately processed with.

Note that this is different from proving that the search order doesn't matter;
that is proven later, in the Tree Invariance section.

This coherence property does not generally hold for depth-first searches that
track that they've passed through certain instructions. The property holds
for this algorithm specifically because it *stops* tracking allocations when
it processes deallocations, and only because deallocations jointly
post-dominate their allocations. Furthermore, because deallocation is not a
coherent joint post-dominance relationship, the algorithm must adopt its
twist around entry edges into dead-end blocks. In fact, the main function of
the twist is to establish the coherence property that the non-coherent joint
post-dominance relationship of allocations and deallocations otherwise lacks.


Definition [coherent point, coherence-prone path].
  A point X is deallocatability-assuring for a set of allocations AS if,
  for all allocations A in AS, for all spanning trees T, the state at X
  under T does not give A undeallocatable status.

  A point X is a coherent point for a set of allocations AS if is
  deallocatability-ensuring for AS and if, for all initial paths P to X,
  there exists a continuation of P' (a path of which P is a prefix) such
  that, for all allocations A in AS, /(ad)*/ matches AH(A, P').

  A path P is a coherence-prone path for a set of allocations AS if the end
  point of P is a coherent point for AS, P is a life-preserving path, and //
  matches AH(A, P) for all allocations A in AS.
End.

Lemma [coherent-point-allocated-coherence-helper]. (tree-independent)
  If P is an initial path to a coherent point Y for a set of allocations
  AS, and /a/ matches AH(A, P) for some allocation A in AS, then there does not
  exist any initial path P' to Y for which either // or a refinement of /.*d/
  matches AH(A, P').
Pf.
  P is an initial path to a coherent point for AS, so there exists a
  continuation
    PC := (P..., PF...)
  such that /(ad)*/ matches AH(A, P).

  By substitution and [history-concatenation] we have:
    AH(A, P_) = AH(A, PC)
              = AH(A, (P..., PF...))
              = (AH(A, P)..., AH(A, PF)...)

  By assumption, /a/ must match AH(A, P), so /d(ad)*/ must match AH(A, PF) by
  [history-pattern-prefix-removal].

  Let P' be an arbitrary initial path to Y. Then
    PC' := (P'..., PF...)
  is an initial path.

  If // matches AH(A, P'), then by [history-pattern-concatenation],
  /d(ad)*/ matches A(PC'). Since PC' is an initial path, this violates
  the dominance axiom.

  If a refinement of /.*d/ matches AH(A, P'), then /.*d/ matches AH(A, P'),
  and so, by [history-pattern-concatenation], /.*dd(ad)*/ matches A(PC');
  but this is a refinement of /.*dd.*/, and since PC' is an initial path,
  this violates the joint post-dominance axioms.
Qed.

Lemma [coherence-prone-paths-allocated-coherence]. (tree-independent)
  If P1 and P2 are coherence-prone paths from X1 and X2 to the same point Y
  for some set of allocations AS, then for all spanning trees T1 and T2,
  for all allocations A in AS, if the state at X1 under T1 gives A allocated
  status, the state at X2 under T2 gives A allocated status.
Pf.
  Let PX1 be the path to X1 in T1, and let PX2 be the path to X2 in T2.
  Then define
    PEX1 := (PX1..., P1...)
    PEX2 := (PX2..., P2...)
  PEX1 and PEX2 are initial paths to Y.

  Let an allocation A in AS be given such that the state at X1 under T1 gives
  A allocated status.

  By [history-concatenation], the definition of AH, and the assumptions
  about P1,
    AH(A, PEX1) = AH(A, (PX1..., P1))
                = (AH(A, PX1)..., AH(A, P1)...)
                = (AH(A, PX1)..., ()...)
                = AH(A, PX1)
  And similarly for P2,
    AH(A, PEX2) = AH(A, (PX2..., P2))
                = (AH(A, PX2)..., AH(A, P2)...)
                = (AH(A, PX2)..., ()...)
                = AH(A, PX2)

  By [allocated-implies-allocation], /a/ matches AH(A, PX1), and
  therefore /a/ matches AH(A, PEX1).

  Exhaustively, the state at X2 under T2 must either not include A or give it
  allocated, pending, or undeallocatable status.

  If the state at X2 under T2 does not include A:
    By [absent-implies-missing-or-deallocated], there exists an initial
    path PX2' to X2 for which either // or /ad/ matches AH(A, PX2').
    Then let PEX2' := (PX2'..., P2...). We have:
      AH(A, PEX2') = AH(A, (PX2'..., P2))
                   = (AH(A, PX2')..., AH(A, P2)...)
                   = (AH(A, PX2')..., ()...)
                   = AH(A, PX2')
    So either // or /ad/ matches AH(A, PEX2').
    Either case is impossible by [coherent-point-allocated-coherence-helper].

  If the state at X2 under T2 gives A pending status:
    By [pending-implies-deallocation], /ad/ matches AH(A, PX2),
    and so /ad/ matches AH(A, PEX2). This is also impossible by
    [coherent-point-allocated-coherence-helper].

  If the state at X2 under T2 gives A undeallocatable status:
    Then by [deallocatibility-preserving-path], the state at Y gives
    A undeallocatable status, which contradicts the assumption that Y is a
    deallocatability-assuring point for AS.

  So the state at X2 under T2 must give A allocated status.
Qed.

Lemma [coherence-prone-paths-pending-coherence]. (tree-independent)
  If P1 and P2 are coherence-prone paths from X1 and X2 to the same point Y
  for some set of allocations AS, then for all spanning trees T1 and T2, for
  all allocations A in AS, if the state at X1 under T1 gives A pending
  status, the state at X2 under T2 gives A pending status.
Pf.
  Let S1 be the state at X1 under T1, and let S2 be the state at X2 under T2.

  Let an allocation A in AS be given such that S1 gives A pending status. Then
  by [correctness-invariant-5], there is an allocation B dominated by A that
  S1 gives allocated status. S2 must therefore also give B allocated status
  by [coherence-prone-paths-allocated-coherence].

  S1 contains both A and B; let IA and IB be the index of A and B in S1.
  Let SB be the state at B>. Since S1 contains B, by [allocation-index],
    SB[LENGTH(SB) - 1][0] = S1[LENGTH(SB) - 1][0] = B
  Since S1[IB][0] = B by construction, and S1 is a well-formed state that
  cannot repeat allocations, it must be true that IB = LENGTH(SB) - 1. Since
  A dominates B, IA < IB by [dominance-implies-precedes]. But this means that
  IA < LENGTH(SB), so by [allocation-index]
    SB[IA][0] = S1[IA][0] = A
  But S2 also contains B, so by [allocation-index]
    SB[IA][0] = S2[IA][0] = A
  Therefore S2 contains A.

  Exhaustively, S2 must either give A allocated, pending, or undeallocatable
  status.

  If S2 gives A allocated status:
    S1 must give A allocated status by
    [coherence-prone-paths-allocated-coherence], but this contradicts the
    assumption that S1 gives A pending status.

  If S2 gives A undeallocatable status:
    Then by [deallocatibility-preserving-path], the state at Y gives
    A undeallocatable status, which contradicts the assumption that Y is a
    deallocatability-assuring point for AS.

  Therefore S2 must give A pending status.
Qed.

Lemma [coherence-prone-paths-coherence]. (tree-independent)
  If P1 and P2 are coherence-prone paths from X1 and X2 to the same point Y
  for some set of allocations AS, then for all spanning trees T1 and T2, for
  all allocations A in AS, if the state at X1 under T1 gives A status U, the
  state at X1 under T2 gives A status U.
Pf.
  Exhaustively, the state at X1 must give A allocated, pending, or
  undeallocatable status.

  If the state at X1 gives A allocated status, then so does the state at X2,
  by [coherence-prone-paths-allocated-coherence].

  If the state at X1 gives A pending status, then so does the state at X2,
  by [coherence-prone-paths-pending-coherence].

  If the state at X1 gives A undeallocatable status, then by
  [deallocatability-preserving-path], the state at Y gives A undeallocatable
  status, which contradicts the assumption that Y is a deallocatability-
  assuring point for AS.
Qed.

Lemma [live-point-is-coherent]. (tree-independent)
  If X is a point in a live SCC, then X is a coherent point for all
  allocation sets AS.
Pf.
  Let AS be an arbitrary set of allocations.

  X is a deallocatability-assuring point for AS:
    Let an allocation A in AS be given, and let a spanning tree T be given.
    Because X is a point in a live SCC, the state at X cannot give A
    undeallocatable status by [live-undeallocatable].

  Because X is a point in a live SCC, there exists a path P_F from X
  to a function exit. Let an arbitrary initial path P_I to X be given.
  Then (P_I..., P_F...) is a terminating initial path, so by the joint
  post-dominance axioms, /(ad)*/ matches AH(A, P) for all allocations A
  (whether they're in AS or not).
Qed.

Lemma [live-coherence-helper].
  If P is a path to a point in a live SCC, and // matches AH(A, P) for
  all allocations A in some set AS, then P is a coherence-prone path for AS.
Pf.
  The end point of P is a point in a live SCC, so by
  [live-point-is-coherent], it is a coherent point for AS.

  By [live-ancestry], P is a life-preserving path.

  Therefore (X -> Y) satisfies the conditions of a coherence-prone path
  for AS.
Qed.

Lemma [live-scc-coherence].
  If an SCC C is not a dead-end region, then the end states
  of all blocks with entry edges into C must be the same.
Pf.
  Let two entry edges X1 -> Y1 and X2 -> Y2 into C be given. Because these
  are entry edges, X1> and X2> are in proper ancestor SCCs of C.

  Let P1I and P2I be the paths to X1> in X2> in T, and let S1 and S2 be the
  states at X1> and X2>. Let AS be the set of all allocations that either P1I
  or P2I passes through.

  All allocations in AS are in proper ancestor SCCs of C:
    Let A in AS be given. Either A is on P1I or A is on P2I. In either case,
    the suffix of that path start at A> is a path to a point in a proper
    ancestor SCC of C, and so A> must be in a proper ancestor SCC of C.

  Y1 and Y2 are blocks in the same strongly-connected component, so
  let P_Y2Y1 be a path from <Y1 to <Y2. Then let
    P1 := (X1 -> Y1)
    P2 := (X2 -> Y2, P_Y2Y1...)

  For all allocations A in AS, AH(A, P1) = () by the definition of AH.
  Therefore P1 is a coherence-prone path for AS by [live-coherence-helper];
  it goes from X1> to <Y1.

  For all allocations A in AS,
    AH(A, P2) = AH(A, (X2 -> Y2, P_Y2Y1...))
  By [history-concatenation]:
              = (AH(A, (X2 -> Y2))..., AH(A, P_Y2Y1)...)
  Applying the definiton of AH to the first component gives:
    AH(A, (X2 -> Y2)) = ()
  Applying [no-scc-self-path-history] to the second component gives:
    AH(A, P_Y2Y1) = ()
  Substituting and simplifying:
    AH(A, P2) = (()..., ()...)
              = ()
  So P2 is also a coherence-prone path for AS by [live-coherence-helper]; it
  goes from X2> to <Y1.

  By [state-differences], one of three things must be true.

  If S1 gives some allocation A a status U and S2 does not:
    Since S1 contains A, by [present-implies-visit], P1I must pass through A.
    Therefore A is in AS. So by [coherence-prone-paths-coherence], S2 must
    give A the status U; so this is a contradiction.

  If S2 gives some allocation A a status U and S1 does not:
    Since S2 contains A, by [present-implies-visit], P2I must pass through A.
    Therefore A is in AS. So by [coherence-prone-paths-coherence], S1 must
    give A the status U; so this is a contradiction.

  If S1 = S2:
    The states at X1> and X2> are the same.

  Therefore the end states of all blocks with entry edges into C are the same.
Qed.

Lemma [live-block-coherence].
  If block B is live, then the end states of all blocks with edges to B must
  be the same.
Pf.
  Let B be given, alone with two edges X1 -> B and X2 -> B, and let
  S1 and S2 be the states at X1> and X2>.

  Let AS be the set of all allocations. By the definition of AH,
  AH(A, (X1 -> B)) = AH(A, (X2 -> B)) = () for any allocation A.
  Then by [live-coherence-helper], (X1 -> B) and (X2 -> B) are
  coherence-prone paths for AS.

  By [state-differences], one of three things must be true.

  If S1 gives some allocation A a status U and S2 does not:
    By [coherence-prone-paths-coherence], S2 must give A the status U; so this
    is a contradiction.

  If S2 gives some allocation A a status U and S1 does not:
    By [coherence-prone-paths-coherence], S1 must give A the status U; so this
    is a contradiction.

  If S1 = S2:
    The states at X1> and X2> are the same.

  Therefore the end states of all blocks with entry edges to B are the same.
Qed.

Lemma [scc-entry-point-coherence].
  For every SCC C, there is a unique state ENTRY(C) (under T) such
  that, for all initial paths P in T that visit C, the state at the entry
  point of P for C is ENTRY(C).

  In tree-independent proofs, this is spelled ENTRY(C, T).
Pf.
  Let X and Y be two points such that the paths PX and PY in T to X and Y,
  respectively, both visit C.

  If C is the entry SCC, then the entry point of both PX and PY for C is the
  entry point of the function. The state at the entry point of the
  function is always the empty stack.

  Otherwise, C is not the entry SCC, so by [scc-entry-path-partition],
  PX and PY can be partitioned at their entry edge to C:
    PX = (PX_I..., MX -> NX, PX_F...)
    PY = (PY_I..., MY -> NY, PY_F...)
  where MX -> NX and MY -> NY are entry edges into C, and where PX_F and PY_F
  are the entry suffixes of PX and PY for C, respectively. The start
  points of PX_F and PY_F are the entry points of PX and PY for C by
  [scc-entry-point].

  Let SNX be the state at <NX and SNY be the state at <NY. Note that
  (PX_I..., MX -> NX) is the path to <NX in T, and (PY_I..., MY -> NY)
  is the path to <NY in T.

  If C is a dead-end region, then by [dead-end-entry-coherence], SNX = SNY.

  If C is not a dead-end region, then let SMX and SMY be the states at MX> and
  MY>, respectively. By [live-scc-coherence], SMX = SMY.
  Since MX -> NX and MY -> NY are not edges into a dead-end region, neither
  edge corresponds to a MERGE operation, so by the state derivation rules,
  SMX = SNX and SMY = SNY. By the transitivity of equality, SNX = SNY.

  In all cases, then, given two arbitrary paths in T that visit C, the
  start points of the entry suffixes of those paths for C have the
  same state under T. Therefore ENTRY(C) is well-defined.
Qed.

Lemma [acyclic-scc-entry-state].
  If a block B is in an acyclic SCC C, the state at <B is ENTRY(C).
Pf.
  Let P be the path to <B in T. Since C is acyclic, the entry point of P
  for C is <B by [acyclic-scc-entry-point]. By [scc-entry-point-coherence],
  the state at <B is ENTRY(C).
Qed.

Lemma [scc-entry-operation-sequence].
  Let P be the entry suffix of the path in T to some point X for the SCC C
  containing X. Then
  - P visits only points in C,
  - OS_PATH(ENTRY(C), P) is a well-formed operation sequence,
  - the end state of OS_PATH(ENTRY(C), P) is the state at X, and
  - OS_PATH(ENTRY(C), P) does not contain any MERGE operations.
Pf.
  By [scc-entry-point-coherence] and [scc-entry-point], the state at the
  start point of P is ENTRY(C). By [operation-sequence-path], OS_PATH
  (ENTRY(C), P) is a well-formed operation sequence, and the end state of
  OS_PATH(ENTRY(C), P) is the state at X.

  P ends at a point in C, so by [scc-entry-suffix-ancestry], all of the points
  on P are in C.

  Because all of the points on P at in a single SCC, P passes through no
  entry edges (whether to a dead-end region or not), and so no component
  of P can correspond to a MERGE operation.
Qed.

Lemma [scc-entry-path-end-state].
  If P is an entry path of C in T, then the state at the end point of P is
  ENTRY(C).
Pf.
  P visits a point in C, so by [scc-entry-point],
    P = (P_I..., P_F...)
  where P_I is the SCC entry prefix of P for C and P_F is the SCC entry
  suffix of P for C. By [scc-entry-path-ancestry], P = P_I, so P_F must be
  the empty path at the end point of P.

  By [scc-entry-point-coherence], the state at the entry point of P for C
  (which is the start point of P_F) is ENTRY(C).
Qed.

Lemma [scc-entry-state-allocations].
  For every SCC C, ENTRY(C) contains only allocations from proper ancestor
  SCCs of C.
Pf.
  Choose P to be an entry path of C in T, by [scc-entry-path-existence].
  Let X be the end point of X. By [scc-entry-path-end-state], the state
  at X is ENTRY(C).

  Let A be an allocation in ENTRY(C); then P passes through A by
  [present-implies-visit]. P is therefore non-empty, so by
  [entry-path-ancestry], the points at all indexes of P except the final
  index are in proper ancestor SCCs of C. Since P passes through A, the point
  <A must be in a non-final index of P, and therefore it is a propery
  ancestor SCC of C, and therefore A is in a proper ancestor SCC of C.
Qed.

Lemma [scc-external-allocation].
  If the state at some point X in an SCC C contains an allocation A from
  an SCC other than C, then ENTRY(C) contains A.
Pf.
  Let P be the path to X in T. By [present-implies-visit], P passes through A,
  which is not in C, so C cannot be the entry SCC. Then by
  [scc-entry-path-partition]
    P = (P_I, M -> N, P_F)
  where <N is the entry point of P for C and P_F is the entry suffix
  of P for C.

  Since P is an initial path in T that visits C, the state at <N
  is ENTRY(C) by [scc-entry-point-coherence]. If ENTRY(C) did not
  contain A, then by [present-implies-visit-path], P_F would have to
  pass through A. But P_F starts and ends at points in C, so it can
  only pass through components of C, and A is not in C by assumption.
  Therefore ENTRY(C) must contain A.
Qed.

Lemma [scc-undeallocatable-invariance].
  If S is the state at a point X in SCC C, UDA(S) = UDA(ENTRY(C)).
Pf.
  Let P be the path to X in T, and let P_F be the SCC entry suffix of P for C.
  By [scc-entry-point-coherence] and [scc-entry-point], the state at the
  start point of P_F is ENTRY(C).

  By [scc-entry-operation-sequence], OS_PATH(ENTRY(C), P_F) is a well-formed
  operation sequence that does not contain a MERGE operation and has S
  as its end state. By [no-merge-implies-no-deallocatable-change],
    UDA(ENTRY(C)) = UDA(S).
Qed.

Lemma [cyclic-scc-input-invariance].
  Let SX be the state at a point X in a cyclic SCC C. Then there exists
  a sequence SUF such that
    SX = (ENTRY(C)..., SUF...)
  where for all allocations A in SUF, A is in C and has a status of
  either allocated or pending.
Pf.
  Let P be the path to X in T, and let PX be the SCC entry suffix of P for C.
  Let XC be the start point of PX. By [scc-entry-point-coherence], the
  state at XC is ENTRY(C).

  By [scc-entry-operation-sequence]
    OSPX = OS_PATH(ENTRY(C), PX)
  is a well-formed operation sequence, and the end state of OSPX is SX.
  Furthermore, PX visits only points in C, and therefore only passes through
  components of C, and so the operations on OSPX must correspond to
  components of C.

  We prove the lemma for SX by inducting on the operation sequence OSPX
  that derives it from ENTRY(C).

  In the base case, OSPX is the empty operation sequence at the state
  ENTRY(C). Then let
    SUF := ()
  By definition, SX = ENTRY(C) = (ENTRY(C)..., SUF...). SUF is the empty
  sequence and so the lemma holds vacuously.

  In the inductive case,
    OSPX = (OSPX'..., O)
  where O corresponds to some component K, which must be a component of C
  because all operations in OSPX correspond to components of C.

  Let SX' be the preceding state of O in OSPX. Because OSPX is a well-formed
  operation sequence, O must change SX' to SX.

  By the inductive hypothesis, there exists a sequence SUF' such that
    SX' = (ENTRY(C)..., SUF'...)
  and where all the allocations in SUF' are in C and have a status of either
  allocated or pending.

  Note that K cannot be a deallocation of an allocation A in ENTRY(C), because
  by [scc-entry-state-allocations], A would have to be from a proper ancestor
  SCC of C, and by [no-cyclic-scc-deallocation], C cannot contain a
  deallocation of an allocation that is not in C.

  We proceed by cases on O.

  If O is PUSH@K:
    K is an allocation A. By definition and substitution,
      SX = STATE_PUSH(SX', A)
         = (SX'..., (A, allocated))
         = (ENTRY(C)..., SUF'..., (A, allocated))
    Then let
      SUF := (SUF'..., (A, allocated))
    Let be an allocation A' in SUF be given. Either A' = A or A' is in SUF'.
    If A' = A, then A is a component of C and has allocated status.
    If A' is in SUF', then A' is a component of C and has allocated or pending
    status by the induction hypothesis.

  If O is PEND@K:
    K is a deallocation of some allocation A. By definition and substitution,
      SX = STATE_PEND(SX', A)
         = SET_STATUS(SX', A, pending)
         = SET_STATUS((ENTRY(C)..., SUF'...), A, pending)

    K is a component of C, so, as previously argued, it cannot be a
    deallocation of an allocation in ENTRY(C). Therefore we can simplify
    the SX equation further:
      SX = (ENTRY(C)..., SET_STATUS(SUF', A, pending)...)
    Then let
      SUF := SET_STATUS(SUF', A, pending)

    Let an allocation A' in SUF be given; then for some index I,
    SUF[I][0] = A'. By the axioms of SET_STATUS, SUF'[I][0] = A', so by
    the induction hypothesis, A' is a component of C. If A' = A, then
    SUF gives A' pending status; otherwise, SUF gives A' the same status
    that SUF' does, and by the induction hypothesis, SUF' gives A' either
    pending or allocated status.

  If O is POP@K:
    K is a deallocation of some allocation A. By definition and substitution,
      SX = STATE_POP(SX', A)
         = PREFIX(SX', I)
         = PREFIX((ENTRY(C)..., SUF'...), I)
    where I is defined to be the smallest index such that the status in SX' at
    index I' is pending for all indexes I' such that
      I <= I' < LENGTH(SX') - 1
    Therefore, if the status in SX' at index I' is not pending, either I > I'
    or I' = LENGTH(SX') - 1.

    By [correctness-invariant-3], the state at CX (which is ENTRY(C)) must
    either be the empty stack or a stack whose top does not have pending
    status. This means that either LENGTH(ENTRY(C)) = 0 or the status in
    ENTRY(C) at index LENGTH(ENTRY(C)) - 1 is not pending.

    If LENGTH(ENTRY(C)) = 0:
      then I >= LENGTH(ENTRY(C)) trivially.
    If the status in ENTRY(C) at index LENGTH(ENTRY(C)) - 1 is not pending:
      By the earlier reasoning about STATE_POP, either
        I > LENGTH(ENTRY(C)) - 1 or
        LENGTH(ENTRY(C)) - 1 = LENGTH(SX') - 1.
      If I > LENGTH(ENTRY(C)) - 1:
         then I >= LENGTH(ENTRY(C)).
      If LENGTH(ENTRY(C)) - 1 = LENGTH(SX') - 1:
        Then we have
          LENGTH(ENTRY(C)) = LENGTH(SX')
                           = LENGTH((ENTRY(C)..., SUF'...))
        which means that SUF' must be the empty sequence. But K must be a
        deallocation of the allocation at the top of the stack in SX', which
        is to say, at the end of SX'; so if SUF' is the empty sequence, K
        must be a dallocation of the last allocation in ENTRY(C), and as
        previously argued this is impossible.

    Therefore in all possible cases, I >= LENGTH(ENTRY(C)), so we can further
    simplify the SX equation:
      SX = (ENTRY(C)..., PREFIX(SUF', I - LENGTH(ENTRY(C)))...)

    Then let
      SUF := PREFIX(SUF', I - LENGTH(ENTRY(C)))

    Let an allocation A' in SUF be given; let I be the index of A' in SUF.
    By the axioms of prefix, SUF[I][0] = SUF'[I][0]; therefore A' is in SUF'
    and must be in C by the induction hypothesis. Furthermore,
    SUF[I][0] = SUF'[I][0], and by the induction hypothesis, SUF'[I][0] must
    be either allocated or pending, so SUF[I][0] must be as well.

  If O is MERGE@K:
    This is impossible, because K is a component of C, which means it cannot
    be an entry edge of any kind.

  Therefore in all possible cases of O, there exists a sequence SUF such that
    SX = (ENTRY(C)..., SUF...)
  and where SUF only contains allocations in C and gives them allocated or
  pending status. This proves the inductive case.

  Then by induction the lemma holds regardless of the value of OSPX.
Qed.

Lemma [cyclic-scc-external-allocation].
  If S is the state at some point in a cyclic SCC C, and A is an allocation
  in an SCC other than C, then S gives A some status if and only if
  ENTRY(C) gives A the same status.
Pf.
  By [cyclic-scc-input-invariance], there exists a sequence SUF such that
    SX = (ENTRY(C)..., SUF...)
  where SUF contains only allocations in C. Since A is not in C, SUF
  does not contain A, so only the elements of ENTRY(C) matter for whether
  SX contains A and, if so, what status it gives A.
Qed.

Lemma [cyclic-scc-external-allocation-coherence].
  If X and Y are points in a cyclic SCC C, and A is an allocation in an
  SCC other than C, and the state at X gives A some status U, then
  the state at Y gives A the same status.
Pf.
  By [cyclic-scc-external-allocation], since the state at X gives A the
  status U, ENTRY(C) gives A the status U.
  By [cyclic-scc-external-allocation], since ENTRY(C) gives A the status U,
  the state at Y gives A the status U.
Qed.

Lemma [cyclic-point-undeallocatable].
  If X is a point in a cyclic SCC C, and A is an allocation in a descendent
  SCC of C, the state SX at X cannot give A undeallocatable status.
Pf.
  By [cyclic-scc-input-invariance], there exists a sequence SUF such that
    SX = (ENTRY(C)..., SUF...)
  where SUF contains only allocations in C and gives them only allocated
  or pending status. By [scc-entry-state-allocations], ENTRY(C) contains
  only allocations from proper ancestors of C and therefore cannot contain
  A. Thus, if A is in SX, it must be in SUF, and therefore A can only have
  pending or allocated status.
Qed.

Lemma [cyclic-point-is-coherent]. (tree-independent)
  If X is a point in a cyclic SCC C, then X is a coherent point for the set
  AS of all allocations in descendent SCCs of C.
Pf.
  X is a deallocatability-assuring point for AS:
    Let an allocation A in AS be given, and let a spanning tree T be given.
    Because X is a point in a cyclic SCC, the state at X cannot give A
    undeallocatable status by [cyclic-point-undeallocatable].

  Let an arbitrary initial path P to X be given. By [scc-entry-point],
    P = (P_I..., P_X...)
  where P_X is the SCC entry suffix of P for C. The start point of P_X
  is an SCC entry point for C.

  Since C is cyclic, there exists a path P_XI from X back to the start
  point of P_X. Define
    P_L := (P_X..., P_XI...)
  P_L is a cycle entirely within C, and it starts from an entry point of C.

  Define
    P_C  := (P_I..., P_X..., P_XI...)
  P_C is a continuation of P. By the associativity of concatenation,
    P_C = (P_I..., (P_X..., P_XI...)...)
        = (P_I..., P_L...)
  Now also define
    P_C' := (P_I..., P_L..., P_L...)
  This is well-formed because P_L begins and ends at the start point of P_X.
  P_C and P_C' are both initial paths.

  Let an arbitrary allocation A be given from AS; by assumption, it is in
  a descendent SCC of C. By [history-concatenation]
    AH(A, P_C) = AH(A, (P_I..., P_L...))
               = (AH(A, P_I)..., AH(A, P_L)...)
    AH(A, P_C') = AH(A, (P_I..., P_L..., P_L...))
                = (AH(A, P_I)..., AH(A, P_L)..., AH(A, P_L)...)

  P_I is the entry prefix of P for C, so by [scc-entry-prefix-ancestry] it
  cannot pass through any component of a descendent SCC of C, and therefore
  it does not pass through A. It is an initial path, so it also cannot pass
  through a deallocation of A, because then by the dominance axiom it would
  also have to pass through A. So AH(A, P_I) = (). Therefore we have:
    AH(A, P_C) = AH(A, P_L)
    AH(A, P_C') = (AH(A, P_L)..., AH(A, P_L)...)

  Because P_C is an initial path, /(ad)*a?/ must match AH(A, P_C) and
  therefore AH(A, P_L). It is not directly required to end in a deallocation
  by the joint post-dominance axioms because it is not terminal. But
  AH(A, P_L) cannot end with an allocation: if it did, it would be non-empty,
  and so AH(A, P_L) would also have to start with an A, and that means
  AH(A, P_C') would pass through A twice without passing through an
  intervening deallocation of A. In pattern terms, if /(ad)*a/ matches
  AH(A, P_L), then /(ad)*a(ad)*a/ matches AH(A, P_C'); this is
  equivalent to /(ad)*aa(da)*/, which is a refinement of /.*aa.*/, which
  violates the joint post-dominance axioms.

  So /(ad)*/ matches AH(A, P_L), and therefore also AH(A, P_C). Therefore
  P_C is a continuation of P which satisfies the requirements.
Qed.

Lemma [scc-strong-entry-point-coherence].
  If X -> Y is an entry edge into an SCC C, then the state at <Y is ENTRY(C).

  (Note that [scc-entry-point-coherence] requires X -> Y to be in T.)
Pf.
  Let PY be the path to <Y in T. If PY is an entry path of C, then
  by [scc-entry-path-end-state], the state at <Y is ENTRY(C). Otherwise
    PY = (PYI..., Z -> Y)
  where Z -> Y is an internal edge of C by [scc-non-entry-path]. Because
  C contains an internal edge, it is cyclic.

  Let SY be the state at <Y. By [cyclic-scc-input-invariance], there exists
  a state suffix SUF where
    SY = (ENTRY(C)..., SUF...)
  and where all allocations in SUF are in C and have either allocated or
  pending status.

  Suppose there is an allocation A in SUF. Then there exists an allocation
  A' in SUF that has allocated status:
    A either has allocated or pending status. If A has allocated status, then
    let A' = A. Otherwise, A has pending status, so there is an allocation
    A'' in SY which is dominated by A that has allocated status by
    [correctness-invariant-5]; by [dominance-implies-precedes], the index of A''
    in SX is greater than the index of A in SX, and therefore A'' is in SUF;
    then let A' = A''.

  By [allocated-implies-allocation], /a/ matches AH(A', PY).
  <Y is in a cyclic SCC, and A' is an allocation in C, so there exists a
  continuation of PY such that /(ad)*/ matches AH(A', PY) by
  [cyclic-point-is-coherent]:
    PY' = (PY..., PYF...)
  By [history-prefix-removal], /d(ad)*/ matches AH(A', PYF).

  Let PX be the path to X> in T, and define
    PXY = (PX..., Z -> Y)
  Then PXY is an initial path to <Y. Z -> Y is an entry edge into C, so
  Z> is a point in a proper ancestor SCC of C, so by [history-proper-ancestor],
  // matches AH(A', PX), and therefore (because Z -> Y is just an edge)
  // matches AH(A', PXY).

  Define
    PXYF := (PXY..., PYF...)
  PXYF is an initial path, and so /(ad)*a?/ matches AH(A', PXYF) by the
  post-dominance axioms. But by [history-concatenation]
    AH(A', PXYF) = (AH(A', PXY)..., AH(A', PYF)...)
                 = AH(A', PYF)
  And since AH(A', PYF) starts with a deallocation of A', there is a
  contradiction.

  Therefore there cannot be any allocation A in SUF, so SUF is the empty
  sequence, and therefore SY = ENTRY(C).
Qed.

Lemma [cyclic-edge-coherence].
  If X -> Y is an internal edge of an SCC C, then the state at X>
  is the same as the state at <Y.
Pf.
  Because C has an internal edge, it must be a cyclic SCC. By
  [cyclic-point-is-coherent], Y is a coherent point for the set SA of all
  allocations in C.

  The empty path at Y> is a coherence-prone path for SA because it ends
  at a coherent point for SA, trivially does not pass through any entry
  edges into dead-end regions, and trivially does not pass through any
  allocations or deallocations for SA. It goes from Y> to Y>.

  (X -> Y) is a coherence-prone path for SA because it ends at a coherent
  point for SA, does not pass through any entry edges into dead-end regions
  (because X -> Y is an internal edge), and trivially does not pass through
  any allocations or deallocations for SA. It goes from <X to Y>.

  Let SX be the state at X> and SY be the state at <Y. By [state-differences],
  one of three things must be true:

  If SX gives some allocation A a status U but SY does not:
    If A is in AS, then by [coherence-prone-paths-coherence], SY must give
    A status U, which is a contradiction.

    If A is not in AS, then by [cyclic-scc-external-allocation-coherence],
    SY must give A status U, which is a contradiction.

  If SY gives some allocation A a status U but SX does not:
    If A is in AS, then by [coherence-prone-paths-coherence], SX must give
    A status U, which is a contradiction.

    If A is not in AS, then by [cyclic-scc-external-allocation-coherence],
    SX must give A status U, which is a contradiction.

  If SX = SY:
    Then the states are the same.
Qed.

Theorem [edge-coherence].
  If there is an edge X -> Y that is not an entry edge into a dead-end
  region, then the state at X> is the same as the state at <Y.
Pf.
  If X -> Y is an internal edge of a SCC, then this is true by
  [cyclic-edge-coherence].

  Otherwise, X -> Y is an entry edge. Let P be the path to <Y in T. Y cannot
  be the entry block because there is an edge to it, so P cannot be empty; let
    P = (PX'..., X' -> Y)
  The SCC containing Y cannot be a dead-end region by assumption, so Y must
  be a live block.

  Let SX be the state at X>, SX' be the state at X'>, and SY be the state at
  <Y. By [live-block-coherence], SX = SX'. By [operation-cases-edge], there
  are two cases.

  If X' -> Y is a conservative entry edge:
    Y is a live block, so this is a contradiction.

  If X' -> Y is not a conservative entry edge:
    SX' = SY by the conditions of this case. By transitivity, SX = SY.
Qed.

Dominance
---------

In this section, we are building up to a proof of invariant #2, that the
allocations on the current stack always dominate the point that the algorithm
is working on. Depth-first searches are not dominance-tree walks, and if
there are cycles in the CFG, a DFS can easily cross an edge to a block that
is not dominated by earlier blocks.

Fortunately, joint post-dominance means we cannot still have non-dominating
allocations with allocated status on the stack when crossing such edges, at
least when entering live regions: either there's a path where we don't
deallocate them before exiting the function, or there's some path from the
entry point that can reach that deallocation without ever passing through the
allocation.

Unfortunately, that doesn't save us directly when it comes to dead-end
regions. It would still be true that the algorithm wouldn't try to insert
deallocations for non-dominated allocations --- there's always a "guard"
allocation with allocated status on the stack which is dominated by any
pending allocations that we'd want to emit. But the twist we do with entry
edges into dead-end regions has the property of forcing coherence on those
edges in a way that re-establishes the stronger dominance property.

It's possible that this can be proven directly from coherence; if there
is, I didn't figure it out.


Definition [closed-under-dominance].
  A set of allocations AS is closed under dominance if, for all allocations
  A and B, if A is in AS, and A dominates B, then B is in AS.
End.

Lemma [coherent-point-allocated-dominance].
  If the state at X gives an allocation A allocated status, and X is a
  coherent point for a set of allocations including A, then A dominates X.
Pf.
  Let P be the path to X in T. Since X is a coherent point for a set of
  allocations that includes A, by definition there exists a continuation
  of P:
    P_C := (P..., P_F...)
  such that /(ad)*/ matches AH(A, P_C). By [history-concatenation],
    AH(A, P_C) = (AH(A, P)..., AH(A, P_F)...)
  /a/ matches AH(A, P) by [allocated-implies-allocation], so by
  [history-prefix-removal], /d(ad))*/ matches AH(A, P_F).

  Let an arbitrary initial path P' to X be given, and define:
    P_C' := (P'..., P_F...)

  AH(A, P') must pass through A or else P_C', an initial path, will pass
  through a deallocation of A without first passing through A, a violation
  of the dominance axioms. Therefore A dominates X.
Qed.

Lemma [coherent-point-dominance].
  If the state at X contains an allocation A, and X is a coherent point for a
  set of allocations AS that includes A and is closed under dominance, then A
  dominates X.
Pf.
  By induction on the SCC tree.

  Let X be a point in an SCC C.

  Lemma [ih-apply].
    If a point X' is in a proper ancestor SCC of C, and the state at X'
    contains A, then A dominates X':
  Pf.
    Since X' is in a proper ancestor SCC of C, there is a path P_XX from
    X' to X. Then, given an arbitrary initial path P' to X', the
    path P := (P'..., P_XX...) is an initial path to X. Because X
    is a coherent point for AS, there exists a continuation P_C of P
    such that /(ad)*/ matches AH(A', P_C) for all allocations A' in AS.
    P_C is also a continuation of P', so X' is a coherent point for AS.

    Then by the inductive hypothesis, if the state at X' contains A,
    A dominates X'.
  Qed.

  Exhaustively, the state at X either gives A allocated, pending, or
  deallocated status.

  If the state at X gives A allocated status:
    A dominates X by [coherent-point-allocated-dominance].

  If the state at X gives A pending status:
    By [correctness-invariant-5], there is an allocation B dominated by A that
    the state at X gives allocated status. Therefore B dominates X by
    [coherent-point-allocated-dominance], and since A dominates B,
    A dominates X by the transitivity of dominance.

  If the state at X gives A undeallocatable status:
    Let P be the path to path to X in T. By [undeallocatable-dead-end-entry],
      P = (P_I..., M -> N, P_F...)
    where M -> N is an entry edge into C, C is a dead-end region, and
    the state SN at <N gives A undeallocatable status.

    Now let an arbitrary initial path P' to X be given. By
    [scc-entry-path-partition]
      P' = (P_I', M' -> N', P_F')
    where M' -> N' is an entry edge into C. M' is therefore a block with an
    entry edge into C, so the state at M'> must contain A by
    [dead-end-entry-preserves-allocation-set-prefix]. M' is a proper ancestor
    of C, again because it has an entry edge into C, so by [ih-apply],
    A dominates M'>, which is to say, all initial paths to M'> must pass
    through A. P_I' is an initial path of M'>, so it must pass through A.
    Therefore P' does as well.

    Since the choice of initial path to X was arbitrary, this is true for
    all such paths, and so A dominates X.

  Therefore, regardless of exactly which status the state at X gives A,
  A dominates X.
Qed.

Lemma [scc-descendent-allocations-set-is-closed-under-dominance].
  The set AS of allocations in descendent SCCs of some SCC C is
  closed under dominance.
Pf.
  Let A and B be allocations, and suppose that A is in AS. By definition, A is
  a descendent SCC of C. Let P_B be an initial path to B; since B is
  dominated by A, A is on P_B. Let P_AB be a suffix from of P_B starting at
  A>. Then P_AB is a path from A> to <B, so B must be in a descendent SCC of
  the SCC containing A, which is itself a descendent SCC of C. Therefore B is
  an allocation in a descendent SCC of C and must be in AS.
Qed.

Theorem [correctness-invariant-2].
  If the state at X contains an allocation A, then A dominates X.
Pf.
  By induction on the SCC tree.

  Let X be a point in an SCC C. C is either a live SCC or a dead-end region.

  If C is a live SCC:
    Let AS be the set of all allocations. By [live-point-is-coherent], X is a
    coherent point for AS. A is trivially in AS, and AS is trivially closed
    under dominance. Then by [coherent-point-dominance], A dominates X.

  If C is a dead-end region:
    A is either in a descendent SCC of C or in a proper ancestor of C.

    If A is in a descendent SCC of C:
      A must actually be in C:
        By [present-implies-visit], the path to X in T passes through A.
        So the suffix of that path starting from A> is a path from a point
        in the SCC containing A to a point in C, o the SCC containing A
        is an ancestor of C; since it is also a descendent by assumption,
        it must be C.

      C is either a cyclic SCC or not.

      If C is a cyclic SCC:
        Let AS be the set of allocations in descendent SCCs of C.
        By [cyclic-point-is-coherent], X is a coherent point for AS.
        A is in AS by definition. AS is closed under dominance by
        [scc-descendent-allocations-set-is-closed-under-dominance].
        Therefore by [coherent-point-dominance], A dominates X.

      If C is not a cyclic SCC:
        An acyclic SCC can only contain one block, and both X and C
        must be in that block. Then by [same-block-dominance], A
        dominates X.

    If A is in a proper ancestor SCC of C:
      Since there exists a proper ancestor SCC of C, C is not the entry SCC.

      Let P be the path to X in T. P can be partitioned at its entry edge
      into C by [scc-entry-path-partition]:
        P = (P_I..., M -> N, P_F...)
      M -> N is an entry edge into R. It is in T because P is a path in T.

      Since the state at X contains A, and A is a proper ancestor SCC of C,
      ENTRY(C) contains A by [scc-external-allocation]. P is an initial
      path in T, and <N is the entry point of P for C, so the state at <N is
      ENTRY(C) by [scc-entry-point-coherence]. Therefore the state at <N
      contains A.

      Now let an arbitrary initial path P' to X be given. P' can also be
      partitioned at its entry edge into C by [scc-entry-path-partition]:
        P' = (P_I'..., M' -> N', P_F'...)

      M' -> N' is an entry edge into C, so M' is a block with such an edge.

      By applying [operation-cases-dead-entry-edge] to M -> N (the entry edge
      in T taken from P above) and M' (the predecessor block from the
      arbitrary path to X), we can conclude that the state at M'> contains A.

      M'> is a point in a proper ancestor SCC of C, so by the induction
      hypothesis, A dominates M'>. By the definition of dominance, any initial
      path to M'> must pass through A. P_I' is such a path, and so it passes
      through A; but then so must P'. Since P' was an arbitrary initial path
      to X, all initial paths to X must pass through A. Then by definition,
      A dominates X.
Qed.

Theorem [correctness-invariant-1].
  For all points X, if the state at X contains allocations A and B, then A
  dominates B if and only if A is below B on the stack.
Pf.
  If SX[I][0] dominates SX[J][0], I < J:
    By [dominance-implies-precedes].

  If I < J, then SX[I][0] dominates SX[J][0]:
    By [stack-order], the path PX to X in T passes through A before it passes
    through B, so
      PX = (PA..., A, PAB..., B, PBX...)
    By [presence-implies-presence], since the state at X contains A, the
    state at <B also contains A. So by [correctness-invariant-2], A
    dominates B.
Qed.

Tree Invariance
---------------

In this section, we are building up to a proof that the search order doesn't
actually matter: the stack will be the same at a particular point in the
function, no matter how we we reached that point. What this looks like in
formal terms is that we prove that the states are the same regardless of
the choice of tree.

This largely builds on the earlier concepts of coherence, as the central
lemmas actually work independently of spanning trees. It's quite possible
that more of the coherence proofs could be directly generalized to work with
arbitrary spanning trees, the way that [coherence-prone-paths-coherence] has
been, making most of the following proof redundant. Many parts of this proof
still reflect the order in which results were proven. Coherence-prone paths
weren't constrained to be life-preserving until coherence had to be proven in
cyclic dead-end regions, and coherent points weren't constrained to be
deallocatability-assuring until invariance had to be proven across trees.
(Undeallocatable status can't change along a coherence-prone path within
a single tree because the entry states of a SCC are always the same.)


Lemma [life-preserving-path-invariance]. (tree-independent)
  For any two spanning trees T1 and T2, if P is a life-preserving path from X
  to Y, and P is in both T1 and T2, and the state at X is the same under T1
  and T2, then the state at Y is the same under T1 and T2.
Pf.
  Let SX be the state at X in both T1 and T2, and let SY1 and SY2 be the
  states at Y in T1 and T2 respectively. By [operation-sequence-path],
  SY1 is the end state of the path OS_PATH(S, P, T1), and SY2 is the end
  state of the path OS_PATH(S, P, T2). But
    OS_PATH(S, P, T1 = OS_PATH(S, P, T2)
  by [correctness-operation-sequence-helper], and therefore SY1 = SY2.
Qed.

Lemma [block-invariance]. (tree-independent)
  Given two spanning trees T1 and T2 and a point X, if the state at the start
  point of the block containing X is the same under T1 and T2, then the
  state at X is the same under T1 and T2.
Pf.
  Let B be the block containing X, and let SB be the state at <B in both T1
  and T2. Let P1 and P2 be the paths from <B to X in T1 and T2; because
  these are simple paths between points in the same block, P1 = P2. Then
  the states at X under T1 and T2 are the same by
  [life-preserving-path-invariance].
Qed.

Lemma [predecessor-invariance-implies-pss-invariance]. (tree-independent)
  If, for all points X in proper ancestor SCCs of some SCC C, the state
  at X under T1 is the same as the state at X under T2, then
    PSS(C, T1) = PSS(C, T2).
Pf.
  Let a state S in PSS(C, T1) be given; by the definition of PSS, there is
  a block B such that the state at B> under T1 is S. By the induction
  hypothesis, the state at B> under T2 is also S, so S is in PSS(C, T2).

  Let a state S in PSS(C, T2) be given; by the definition of PSS, there is
  a block B such that the state at B> under T1 is S. By the induction
  hypothesis, the state at B> under T1 is also S, so S is in PSS(C, T1).

  Therefore PSS(C, T1) = PSS(C, T2).
Qed.

Lemma [predecessor-invariance-implies-entry-state-invariance]. (tree-independent)
  If, for all points X in proper ancestor SCCs of some SCC C, the state
  at X under T1 is the same as the state at X under T2, then
    ENTRY(C, T1) = ENTRY(C, T2)
Pf.
  If C is the entry SCC, then ENTRY(C, T1) = STATE_EMPTY = ENTRY(C, T1).

  Otherwise, let X be a point in C, and let P be the path to X in T1. By
  [scc-entry-path-partition]
    P = (PI..., M -> N, PF...)
  where M -> N is an entry edge into C.

  Let SN1 and SN2 be the states at <N under T1 and T2. By
  [scc-strong-entry-point-coherence], SN1 = ENTRY(C, T1) and
  SN2 = ENTRY(C, T2).

  If C is not a dead-end region:
    Let SM1 and SM2 be the states at M> under T1 and T2. SM1 = SN1 and
    SM2 = SN2 by [edge-coherence]. M> is a point in a proper ancestor SCC of
    C, so by the invariance assumption, SM1 = SM2. Therefore
      ENTRY(C, T1) = SN1 = SM1 = SM2 = SN2 = ENTRY(C, T2).

  If C is a dead-end region:
    Let PSS1 = PSS(C, T1), and let PSS2 = PSS(C, T2). PSS1 = PSS2 by
    By [predecessor-invariance-implies-pss-invariance].

    Applying [dead-end-entry-coherence] to SN1, one of three cases must apply.

    If C is the entry SCC:
      This contradicts the "otherwise" above.

    If PSS1 is singleton:
      Then SN1 is the single element of PSS1. But PSS1 = PSS2, so PSS2 is also
      singleton. Applying [dead-end-entry-coherence] to SN2, and discarding
      contradicted cases, SN2 must be the single element of PSS2. Since
      PSS1 = PSS2, the single element of PSS1 is the same as the single
      element of PSS2, so SN1 = SN2, so ENTRY(C, T1) = ENTRY(C, T2).

    If PSS1 is not singleton:
      Then SN1 = CONSERVATIVE_MERGE(PSS1). But PSS1 = PSS2, so PSS2 is also
      not singleton. Applying [dead-end-entry-coherence] to SN2 and discarding
      contradicted cases, SN2 = CONSERVATIVE_MERGE(PSS2). Since PSS1 = PSS2,
      CONSERVATIVE_MERGE(PSS1) = CONSERVATIVE_MERGE(PSS2), so SN1 = SN2, so
      ENTRY(C, T1) = ENTRY(C, T2).
Qed.

Lemma [cyclic-point-invariance-helper]. (tree-independent)
  Given two spanning trees T1 and T2, if Y is a point in a cyclic SCC C, and
  ENTRY(C, T1) = ENTRY(C, T2), then for all allocations A, if the state at Y
  under T1 gives A some status U, then the state at Y under T2 gives A the
  status U.
Pf.
  Let P1 and P2 be the entry suffixes for C of the paths to Y in T1 and T2.
  Let X1 and X2 be the start points of P1 and P2.

  Let SX be the state at X1 under T1, and let SX2 be the state at X2 under T2.
  By [scc-entry-point-coherence], SX = ENTRY(C, T1) and SX2 = ENTRY(C, T2).
  By the assumption of the lemma, ENTRY(C, T1) = ENTRY(C, T2), so transitively
  SX = SX2.

  Let SY1 and SY2 be the states at Y under T1 and T2. By
  [cyclic-scc-input-invariance],
    SY1 = (SX..., SUF1...)
    SY2 = (SX2..., SUF2...) = (SX..., SUF2...)
  where SUF1 and SUF2 contain only allocations from C and give them either
  allocated or pending status. By [scc-entry-state-allocations], SX contains
  only allocations from proper ancestors of C.

  Now let an allocation A be given such that SY1 gives A the status U. Let
  AI be the index of A in SY1, such that SY1[AI][0] = A and SY1[AI][1] = U.

  If A is not in C:
    AI must be < LENGTH(SX):
      If AI >= LENGTH(SX), then SY1[AI][0] = SUF1[AI - LENGTH(SX)][0] = A;
      but SUF1 only contains allocations from C, and A is not in C.
    Therefore SY1[AI][0] = SX[AI][0] = A, and SY1[AI][1] = SX[AI][0] = U.
    But then SY2[AI][0] = SX[AI][0] = A, and SY2[AI][1] = SX[AI][0] = U,
    so SY2 gives A the status U.

  If A is in C:
    Let AS be the set of allocations in descendent SCCs of C. By
    [cyclic-point-is-coherent], Y is a coherent point for AS. A is in
    AS because it is in C, which is a descendent SCC of itself.

    The empty path at Y is a coherence-prone path for AS: its end point
    is a coherent point for AS, and it is trivially a life-preserving path
    for which // matches AH(A, P) for all allocations A in AS.

    Then by [coherence-prone-paths-coherence], SY2 gives A the status U.
Qed.

Lemma [cyclic-point-invariance]. (tree-independent)
  Given two spanning trees T1 and T2, if Y is a point in a cyclic SCC C, and
  ENTRY(C, T1) = ENTRY(C, T2), then the state at Y under T1 is the same
  as the state at Y under T2.
Pf.
  Let SY1 and SY2 be the states at Y under T1 and T2. By [state-differences],
  SY1 and SY2 must differ in one of two ways, or else they are the same.

  If SY1 gives an allocation A the status U, and SY2 does not:
    By [cyclic-point-invariance-helper], SY2 must give A the status U,
    so this is a contradiction.

  If SY2 gives an allocation A the status U, and SY1 does not:
    By [cyclic-point-invariance-helper], SY1 must give A the status U,
    so this is a contradiction.

  Therefore SY1 = SY2.
Qed.

Theorem [tree-invariance]. (tree-independent)
  Given two spanning trees T1 and T2, for all points X, the state at X under
  T1 is the same as the state at X under T2.
Pf.
  By induction on the SCC tree.

  Let a point X be given in an SCC C such that, for all points X' in proper
  ancestor SCCs of C, the state at X' under T1 is the same as the state at X'
  under T2. Let SX1 and SX2 be the states at X under T1 and T2.

  By [predecessor-invariance-implies-entry-state-invariance],
  ENTRY(C, T1) = ENTRY(C, T2).

  If C is not a cyclic SCC, then let B be the block containing X.
  By [acyclic-scc-entry-point], the state at <B under T1 is ENTRY(C, T1),
  and the state at <B under T2 is ENTRY(C, T2), which are equal. Therefore,
  SX1 = SX2 by [block-invariance].

  Otherwise, C is a cyclic SCC. SX1 = SX2 by [cyclic-point-invariance].
Qed.


Mutations
---------

This section proves the correctness of the actual removals and insertions
performed by the algorithm. Or, well, it will.


Theorem.
  The algorithm preserves the joint post-dominance of
  allocations and deallocations.
Pf.
  FIXME