chiark / gitweb /
wip create tip
authorIan Jackson <ijackson@chiark.greenend.org.uk>
Mon, 12 Mar 2012 14:38:24 +0000 (14:38 +0000)
committerIan Jackson <ijackson@chiark.greenend.org.uk>
Mon, 12 Mar 2012 14:38:24 +0000 (14:38 +0000)
article.tex

index bb050ae..cc67c04 100644 (file)
@@ -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}