\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}

