From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Fri, 27 Apr 2012 12:31:59 +0000 (+0100)
Subject: strategy: wip
X-Git-Url: https://www.chiark.greenend.org.uk/ucgi/~ian/git?a=commitdiff_plain;h=727ac7504bdc6df349acce9934892cd372ffe086;p=topbloke-formulae.git

strategy: wip
---

diff --git a/strategy.tex b/strategy.tex
index 532b24e..d170919 100644
--- a/strategy.tex
+++ b/strategy.tex
@@ -123,7 +123,25 @@ it is, are we fast forward to $E_i$
 --- formally, $\grefu = \text{max}(\grefc, E_i)$ ---
 and drop $E_i$ from the planned ordering.
 
-\subsection{Merge Contributors for UP TO HERE}
+\subsection{Merge Contributors for $\pcy$}
+
+Merge $\pcn$ into $\grefc$.  That is, merge with
+$L = \grefc, R = \greffa{\pcn}, M = \baseof{\grefc}$.
+to construct $\grefu$.
+
+Merge conditions: Ingredients satisfied by construction.
+Tip Merge satisfied by construction.  Merge Acyclic follows
+from Perfect Contents and $\hasdep$ being acyclic.
+
+Removal Merge Ends: For $\p = \pc$, $M \nothaspatch \p$.
+For $p \neq \pc$, by Tip Contents,
+$M \haspatch \p \equiv L \haspatch \p$, so we need only
+worry about $X = R, Y = L$; ie $L \haspatch \p$,
+$M = \baseof{L} \haspatch \p$.
+By Tip Contents for $L$, $D \le L \equiv D \le M$.  $\qed$
+
+OK
+UP TO HERE
 
 with $M=M_j, L=T_{\pc,j-1}, R=E_j$,
 and calculate what the resulting desired direct dependencies file