strategy: traversal wip proofs

diff --git a/strategy.tex b/strategy.tex
index e3ba372373a06af330823732cb03bf7e3b8b727c..0f03ddb9883200fed514b821df14948994e78aca 100644 (file)
--- a/strategy.tex
+++ b/strategy.tex
@@ -229,7 +229,7 @@ this must complete eventually.
 
 $\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
@@ -366,3 +366,12 @@ $\alg{Merge}$ with $L = W, \; R = S$ and any suitable $M$.
 (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}
+