chiark / gitweb /
improve "no replay for merge results" (correct conditions, remove some duplicate...
authorIan Jackson <ijackson@chiark.greenend.org.uk>
Mon, 5 Mar 2012 19:50:46 +0000 (19:50 +0000)
committerIan Jackson <ijackson@chiark.greenend.org.uk>
Mon, 5 Mar 2012 19:50:46 +0000 (19:50 +0000)
article.tex

index b97350f..1f7a59b 100644 (file)
@@ -259,8 +259,15 @@ XXX proof TBD.
 
 \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.
 
@@ -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 \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$:}
-$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$