From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Tue, 6 Mar 2012 09:39:12 +0000 (+0000)
Subject: wip anticommit desired contents
X-Git-Tag: f0.2~146
X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=commitdiff_plain;ds=sidebyside;h=d69833629e848b5da6cd00bca1986ffe84abd510;p=topbloke-formulae.git

wip anticommit desired contents
---

diff --git a/article.tex b/article.tex
index 4c5f675..b71bb32 100644
--- a/article.tex
+++ b/article.tex
@@ -408,10 +408,9 @@ Used for removing a branch dependency.
 \[ \eqn{ Currently Included }{
  L \haspatch \pry
 }\]
-
-\subsection{Desired Contents}
-
-xxx need to prove $D \isin C \equiv D \not\in \pry \land D \isin L$.
+\[ \eqn{ Not Self }{
+ L \not\in \{ R^+ \}
+}\]
 
 \subsection{No Replay}
 
@@ -419,6 +418,22 @@ By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$ and No Replay for
 Merge Results applies. $\qed$
 
+\subsection{Desired Contents}
+
+\[ $D \isin C \equiv [ D \not\in \pry \land D \isin L$ ] \lor D = C \]
+{\it Proof.}
+
+\subsubsection{For $D = C$:}
+
+Trivially $D \isin C$.  OK.
+
+\subsubsection{For $D \not\le C$:}
+
+
+
+\subsubsection{For $D \in R^+$:}
+By Currently Included, 
+
 \subsection{Unique Base}
 
 Need to consider only $C \in \py$, ie $L \in \py$.