wip create tip

diff --git a/article.tex b/article.tex
index bb050ae6273ad9cba01131a4131c4b4ba75e1622..cc67c04a3b9c7cc2fdbb93f8c573d90f4bdae764 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -567,13 +567,28 @@ Not applicable.
 
 \subsection{Coherence and Patch Inclusion}
 
 
 \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 = \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}
 xxx up to here
 
 \section{Anticommit}