From 0c3db5a204f508f8a8a59c74ea8a9bf56d3ab59e Mon Sep 17 00:00:00 2001
From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Sun, 27 May 2012 23:04:59 +0100
Subject: [PATCH] strategy: traversal wip proofs

---
 strategy.tex | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/strategy.tex b/strategy.tex
index e3ba372..0f03ddb 100644
--- 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}
+
-- 
2.30.2