X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=blobdiff_plain;f=traversal.tex;h=55a4900f790d4a08aed2ed4ae8272cdb9f0f9354;hb=0b2f9c02d4b77a5cadff5f255ba9d2eab0f39c3f;hp=407c60d7f84f19e94564928d05c35ef7e82d7659;hpb=389264b61a113301ca87b6d17fe19dafdd50e9e9;p=topbloke-formulae.git

diff --git a/traversal.tex b/traversal.tex
index 407c60d..55a4900 100644
--- a/traversal.tex
+++ b/traversal.tex
@@ -215,10 +215,21 @@ $L = W, \; R = \tipdy, \; M = \baseof{R} = \tipdn$.
 \item TODO CHOOSE/REFINE W AND S as was done during Ranking for bases
 
 \item $\alg{Merge}$ from $\tipcn$.  That is, $L = W, \;
-R = \tipcn$ and choose any suitable $M$.
+R = \tipcn$ and $M = \baseof{W}$.
 
  \commitproof{
-  $L = W$, $R = \tipcn$.
+  \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 $
+  }
+
   TODO TBD
 
   Afterwards, $\baseof{W} = \tipcn$.