No Replay for Merge Results

diff --git a/article.tex b/article.tex
index f712ba63fc0e7fdb37b78598eb1f192d357a634b..674e5936f60fc6ae27161506b57b458b7517ccab 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -254,6 +254,34 @@ by the LHS.  And $A \le A''$.
 }\]
 XXX proof TBD.
 
 }\]
 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:}
+
+\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 \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$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
+R$ so $D \le C$.  OK.
+
+$\qed$
+

 \section{Commit annotation}
 
 We annotate each Topbloke commit $C$ with:
 \section{Commit annotation}
 
 We annotate each Topbloke commit $C$ with:


@@ -406,30 +434,9 @@ Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
    \end{cases}
 }\]
 
    \end{cases}
 }\]
 

-\subsection{No Replay}
-
-\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 \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$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
-R$ so $D \le C$.  OK.
+\subsection{Merge Results}

 
 

-$\qed$
+As above.

 
 \subsection{Unique Base}
 
 
 \subsection{Unique Base}