$\qed$
-\section{Traversal phase}
+\section{Traversal phase --- algorithm}
(In general, unless stated otherwise below, when we generate a new
commit $C$ using one of the commit kind algorith, we update
(Tip Source Merge.)
\end{enumerate}
+
+
+\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}
+