chiark / gitweb /
 author Ian Jackson Mon, 5 Mar 2012 19:50:46 +0000 (19:50 +0000) committer Ian Jackson Mon, 5 Mar 2012 19:50:46 +0000 (19:50 +0000)
 article.tex patch | blob | history

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$