X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=traversal.tex;h=ab1e6d4ade011651642cbc61bf8ac5ab3e3a4aae;hp=a241644e3e3ff1c2711904fc73b69c19d944793d;hb=02d646dff7177c19756094eb179a5c324e268f3b;hpb=0bee06686567e976f393e3d5d26a435d695e3b91

diff --git a/traversal.tex b/traversal.tex
index a241644..ab1e6d4 100644
--- a/traversal.tex
+++ b/traversal.tex
@@ -221,14 +221,16 @@ R = \tipcn$ and $M = \baseof{W}$.
   \condproof{Ingredients}{
    $M \le L$ is trivial.  For $M \le R$ we want
    $\tipcn \ge \baseof{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}$.
+  }
+  \condproof{Tip Merge}{ Trivial. }
+  \condproof{Merge Acyclic}{
+   By Base Acyclic, $\tipcn \nothaspatch \p$.
   }
+  \condproof{Foreign Merges}{ Not applicable. }
 
   TODO TBD