\newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
\newcommand{\qed}{\square}
-\newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
+\newcommand{\proofstarts}{{\it Proof:}}
+\newcommand{\proof}[1]{\proofstarts #1 $\qed$}
\newcommand{\gathbegin}{\begin{gather} \tag*{}}
\newcommand{\gathnext}{\\ \tag*{}}
\subsection{No Replay for Merge Results}
-If we are constructing $C$, given
+If we are constructing $C$, with,
\gathbegin
\mergeof{C}{L}{M}{R}
\gathnext
\gathnext
R \le C
\end{gather}
-No Replay is preserved. {\it Proof:}
+No Replay is preserved. \proofstarts
\subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
\subsection{Desired Contents}
\[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
-{\it Proof.}
+\proofstarts
\subsubsection{For $D = C$:}
\gathnext
\mergeof{C}{L}{M}{R}
\end{gather}
+We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
\subsection{Conditions}
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$.