-\subsection{No Replay for Merge Results}
-
-If we are constructing $C$, with,
-\gathbegin
- \mergeof{C}{L}{M}{R}
-\gathnext
- L \le C
-\gathnext
- R \le C
-\end{gather}
-No Replay is preserved. \proofstarts
-
-\subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
-
-\subsubsection{For $D \isin L \land D \isin R$:}
-$D \isin C$. And $D \isin L \implies D \le L \implies D \le C$. OK.
-
-\subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
-$D \not\isin C$. OK.
-
-\subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
- \land D \not\isin M$:}
-$D \isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
-R$ so $D \le C$. OK.
-
-\subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
- \land D \isin M$:}
-$D \not\isin C$. OK.
+\[ \eqn{Ingredients Prevent Replay:}{
+ \left[
+ {C \hasparents \set A} \land
+ \\
+ \left(
+ D \isin C \implies
+ D = C \lor
+ \Largeexists_{A \in \set A} D \isin A
+ \right)
+ \right] \implies \left[
+ D \isin C \implies D \le C
+ \right]
+}\]
+\proof{
+ Trivial for $D = C$. Consider some $D \neq C$, $D \isin C$.
+ By the preconditions, there is some $A$ s.t. $D \in \set A$
+ and $D \isin A$. By No Replay for $A$, $D \le A$. And
+ $A \le C$ so $D \le C$.
+}