L \nothaspatch \pry
}\]
\[ \eqn{ Insertion Acyclic }{
- R^+ \nothaspatch \pqy
+ R^+ \nothaspatch \pq
}\]
\subsection{No Replay}
For $D \isin L$, Base Acyclic for L suffices. For $D \isin R^+$,
Insertion Acyclic suffices. For $D = C$, trivial. $\qed$.
+\subsection{Coherence}
+
+We consider some $D \in \py$.
+
+\subsubsection{For $\p = \pq$:}
+
xxx up to here
+$D \not\isin L$, $D \not\isin $
+
\section{Merge}
Merge commits $L$ and $R$ using merge base $M$: