new macro \statement (for \[\eqn{...}{...}\] - many possible call sites)

[topbloke-formulae.git] / trav-proofs.tex

\section{Traversal phase --- proofs}

For each operation called for by the traversal algorithms, we prove
that the commit generation preconditions are met.

\subsection{Tip Base Merge}