From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Sun, 27 May 2012 22:04:59 +0000 (+0100)
Subject: strategy: traversal wip proofs
X-Git-Url: https://www.chiark.greenend.org.uk/ucgi/~ian/git?a=commitdiff_plain;h=0c3db5a204f508f8a8a59c74ea8a9bf56d3ab59e;p=topbloke-formulae.git

strategy: traversal wip proofs
---

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