\[ \eqn{ Ingredients }{
\patchof{B} = \pqn
}\]
+\[ \eqn{ No Sneak }{
+ \pendsof{B}{\pqy} = \{ \}
+}\]
\subsection{No Replay}
$\qed$
+\subsection{Base Acyclic}
+
+Not applicable.
+
+\subsection{Coherence and Patch Inclusion}
+
+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$.
+
xxx up to here
\section{Anticommit}