It does not matter what order we perform the reductions in, as long as we
perform all available ones eventually\cite{Reduction}.  Therefore, to prove
that our algorithm will find all possible reductions in the graph we need to
show that the only vertices that need to be tested are in the queue, or have
already been tested; we do not have to worry about what order we discover the
reductions.  To prove that our algorithm is correct, we use the following:

\newtheorem*{correct}{Loop Invariant}
\begin{correct}
All reductions currently possible in the graph are completeable from the
partial matches stored in $M$ and at least one of the vertices stored in $Q$.
\end{correct}

\newtheorem{lem}{Lemma}
\begin{lem}[Base Case]
The invariant is true prior to executing the body of the loop.
\end{lem}

\begin{proof} For our initial trip through the loop, all vertices that are
small enough to be matched with some black vertex are in the queue and $M$ is
empty, so our invariant certainly starts out true.  \end{proof}

\begin{lem}[Inductive Case]
If the lemma is true before executing an iteration the loop, it will be true afterwards as well.
\end{lem}

\begin{proof} On every loop we deal with one of two cases: the vertex was
placeable, or it was not.  If the vertex was placeable then it was either
stored in $M$, reduced via some rule removed from the graph, or reduced via
some rule but not removed and so placed back in $Q$.  In all cases, our
invariant remains true.

If we could not find a match region for the vertex, then we can safely conclude
that, unless one of its white neighbors becomes black, the vertex will never
match any reduction rule.  But if one of its neighbors becomes black, then that
neighbor will be put in the queue and the match involving our discarded vertex
is will be available for discovery via the neighbor.  Therefore it is safe to
discard the vertex under consideration if it can't currently be matched.  This
proves that our invariant remains true whether a match was discovered or not.
\end{proof}

Using these two lemmas, we can prove

\newtheorem*{thm}{Theorem}
\begin{thm}[Correctness]
The combination of the loop termination condition and our loop invariant implies that the algorithm is correct.
\end{thm}

\begin{proof} When the loop terminates, we know that $Q$ is empty.  Since our
invariant remains true, this implies that we've exhausted all possible matches
and it is safe to check the resultant graph for isomorphism against the set of
base reducts.  This, combined with Lemmas 1 and 2 which prove the correctness
of the loop invariant, proves that the algorithm correctly tests for membership
in the class defined by the given graph reduction system, and our proof is
complete!  \end{proof}