From b0829518c57769b909a278ca6a3610a057e66fdf Mon Sep 17 00:00:00 2001
From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Mon, 16 Jul 2012 05:51:02 +0100
Subject: [PATCH] strategy: traversal, Tip-Merge, from base, ingredients

---
 traversal.tex | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/traversal.tex b/traversal.tex
index 55a4900..b07cc9c 100644
--- a/traversal.tex
+++ b/traversal.tex
@@ -221,13 +221,10 @@ R = \tipcn$ and $M = \baseof{W}$.
   \condproof{Ingredients}{
    $M \le L$ is trivial.  For $M \le R$ we want
    $\tipcn \ge \baseof{W}$.
-   Well $W$
-   Now $\pendsof{\allreach}{\tipcy} =
-   \pendsof{\allreachof{\pcn}}{\tipcy}$
-   since we have created no commits $\in \pcn$ since
-   calculating $\tipcy$.
-
-   By Base Covers Reachable, $\tipcn \ge $
+   Well $W \in \set S^{\pcy}$ so $W \in \allreachof{\pcn}$
+   and $W \in \pcy$.  So $W \in \pendsof{\allreachof{\pcn}}{\pcy}$
+   so Base Covers Reachable indeed
+   $\tipcn \ge \baseof{W}$.
   }
 
   TODO TBD
-- 
2.30.2