improve "no replay for merge results" (correct conditions, remove some duplicate...

diff --git a/article.tex b/article.tex
index b97350feb3e49447324ba7a794cdaf5b5ebe6425..1f7a59bd4018b2ed9aba33b8a46989dd24cb33c4 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -259,8 +259,15 @@ XXX proof TBD.
 
 \subsection{No Replay for Merge Results}
 
 
 \subsection{No Replay for Merge Results}
 

-If we are constructing $C$ such that $\merge{C}{L}{M}{R}$, No Replay
-is preserved.  {\it Proof:}
+If we are constructing $C$, given
+\gathbegin
+  \merge{C}{L}{M}{R}
+\gathnext
+  L \le C
+\gathnext
+  R \le C
+\end{gather}
+No Replay is preserved.  {\it Proof:}

 
 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
 
 
 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
 


@@ -270,9 +277,6 @@ $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 \not\isin L \land D \not\isin R$:}
 $D \not\isin 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
 \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


@@ -280,8 +284,7 @@ R$ so $D \le C$.  OK.
 
 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
  \land D \isin M$:}
 
 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
  \land D \isin M$:}

-$D \not\isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
-R$ so $D \le C$.  OK.
+$D \not\isin C$.  OK.

 
 $\qed$
 
 
 $\qed$