From 6b14ca6a279b611027dae5f53f21324e7559d1b9 Mon Sep 17 00:00:00 2001
From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Mon, 12 Mar 2012 14:38:24 +0000
Subject: [PATCH] wip create tip

---
 article.tex | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/article.tex b/article.tex
index bb050ae..cc67c04 100644
--- a/article.tex
+++ b/article.tex
@@ -567,13 +567,28 @@ Not applicable.
 
 \subsection{Coherence and Patch Inclusion}
 
-Consider some $D \in \py$.
+$$
+\begin{cases}
+  \p = \pq    \lor B \haspatch \p : & C \haspatch \p \\
+  \p \neq \pq \land B \nothaspatch \p : & C \nothaspatch \p
+\end{cases}
+$$
+
+\proofstarts
+~ Consider some $D \in \py$.
 
 \subsubsection{For $\p = \pq$:}
 
 By Base Acyclic, $D \not\isin B$.  So $D \isin C \equiv D = C$.
 By No Sneak, $D \le B \equiv D = C$.  Thus $C \haspatch \pq$.
 
+\subsubsection{For $\p \neq \pq$:}
+
+$D \neq C$.  So $D \isin C \equiv D \isin B$,
+and $D \le C \equiv D \le B$.
+
+$\qed$
+
 xxx up to here
 
 \section{Anticommit}
-- 
2.30.2