From 0186895a1fa260b40e49b33d826e13226bbe0931 Mon Sep 17 00:00:00 2001
From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Tue, 6 Mar 2012 14:34:10 +0000
Subject: [PATCH] anticommit desired contents

---
 article.tex | 26 ++++++++++++++++++++++----
 1 file changed, 22 insertions(+), 4 deletions(-)

diff --git a/article.tex b/article.tex
index 0e3732d..4c7f22c 100644
--- a/article.tex
+++ b/article.tex
@@ -423,19 +423,37 @@ Merge Results applies. $\qed$
 
 \subsection{Desired Contents}
 
-\[ $D \isin C \equiv [ D \not\in \pry \land D \isin L$ ] \lor D = C \]
+\[ D \isin C \equiv [ D \notin \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 \neq C, D \not\le L$:}
 
+By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
+$D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
 
+\subsubsection{For $D \neq C, D \le L, D \in \pry$:}
 
-\subsubsection{For $D \in R^+$:}
-By Currently Included, 
+By Currently Included, $D \isin L$.
+
+By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
+by Unique Tip, $D \le R^+ \equiv D \le L$.  
+So $D \isin R^+$.
+
+By Base Acyclic, $D \not\isin R^-$.
+
+Apply $\merge$: $D \not\isin C$.  OK.
+
+\subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
+
+By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
+
+Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
+
+$\qed$
 
 \subsection{Unique Base}
 
-- 
2.30.2