\gathnext
\mergeof{C}{L}{M}{R}
\end{gather}
+We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
\subsection{Conditions}
\text{otherwise} : & \false
\end{cases}
}\]
+\[ \eqn{ Merge Ends }{
+ X \not\haspatch \p \land
+ Y \haspatch \p \land
+ E \in \pendsof{X}{\py}
+ \implies
+ E \le Y
+}\]
\subsection{No Replay}
Need to determine $C \haspatch P$ based on $L,M,R \haspatch P$.
This involves considering $D \in \py$.
-We will use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
-
\subsubsection{For $L \nothaspatch P, R \nothaspatch P$:}
$D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
\in \py$ ie $L \haspatch P$ by Tip Self Inpatch). So $D \neq C$.
So indeed $L \haspatch P \land R \haspatch P \implies C \haspatch P$.
+\subsubsection{For (wlog) $X \not\haspatch P, Y \haspatch P$:}
+
+$C \haspatch P \equiv C \nothaspatch M$.
+
+\proofstarts
+
\end{document}