chiark / gitweb /
index 5dc99ee..7a48a25 100644 (file)
--- a/merge.tex
+++ b/merge.tex
@@ -111,20 +111,29 @@ $\qed$

\subsection{Coherence and Patch Inclusion}

\subsection{Coherence and Patch Inclusion}

-Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
-This involves considering $D \in \py$.
+$$+\begin{cases} + L \nothaspatch \p \land R \nothaspatch \p : & C \nothaspatch \p \\ + L \haspatch \p \land R \haspatch \p : & C \haspatch \p \\ + \text{otherwise} \land M \haspatch \p : & C \nothaspatch \p \\ + \text{otherwise} \land M \nothaspatch \p : & C \haspatch \p +\end{cases} +$$
+\proofstarts
+~ Consider $D \in \py$.

\subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
$D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L \subsubsection{For$L \nothaspatch \p, R \nothaspatch \p$:}$D \not\isin L \land D \not\isin R$.$C \not\in \py$(otherwise$L
-\in \py$ie$\neg[ L \nothaspatch \p ]$by Tip Own Contents for$L$). +\in \py$ ie $L \haspatch \p$ by Tip Own Contents for $L$).
So $D \neq C$.
Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
So $D \neq C$.
Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
+OK.

\subsubsection{For $L \haspatch \p, R \haspatch \p$:}
$D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
(Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)

\subsubsection{For $L \haspatch \p, R \haspatch \p$:}
$D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
(Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)

-Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
+Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \zhaspatch \p$.

For $D \neq C$: $D \le C \equiv D \le L \lor D \le R \equiv D \isin L \lor D \isin R$.

For $D \neq C$: $D \le C \equiv D \le L \lor D \le R \equiv D \isin L \lor D \isin R$.
@@ -132,41 +141,40 @@ For $D \neq C$: $D \le C \equiv D \le L \lor D \le R Consider$D \neq C, D \isin X \land D \isin Y$: By$\merge$,$D \isin C$. Also$D \le X$Consider$D \neq C, D \isin X \land D \isin Y$: By$\merge$,$D \isin C$. Also$D \le X$-so$D \le C$. OK for$C \haspatch \p$. +so$D \le C$. OK for$C \zhaspatch \p$. Consider$D \neq C, D \not\isin X \land D \not\isin Y$: By$\merge$,$D \not\isin C$. And$D \not\le X \land D \not\le Y$so$D \not\le C$. Consider$D \neq C, D \not\isin X \land D \not\isin Y$: By$\merge$,$D \not\isin C$. And$D \not\le X \land D \not\le Y$so$D \not\le C$. -OK for$C \haspatch \p$. +OK for$C \zhaspatch \p$. Remaining case, wlog, is$D \not\isin X \land D \isin Y$.$D \not\le X$so$D \not\le M$so$D \not\isin M$. Thus by$\merge$,$D \isin C$. And$D \le Y$so$D \le C$. Remaining case, wlog, is$D \not\isin X \land D \isin Y$.$D \not\le X$so$D \not\le M$so$D \not\isin M$. Thus by$\merge$,$D \isin C$. And$D \le Y$so$D \le C$. -OK for$C \haspatch \p$. +OK for$C \zhaspatch \p$. -So indeed$L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$. +So, in all cases,$C \zhaspatch \p$. +And by$L \haspatch \p$,$\exists_{F \in \py} F \le L$+and this$F \le C$so indeed$C \haspatch \p$. \subsubsection{For (wlog)$X \not\haspatch \p, Y \haspatch \p$:} \subsubsection{For (wlog)$X \not\haspatch \p, Y \haspatch \p$:} -$M \haspatch \p \implies C \nothaspatch \p$. -$M \nothaspatch \p \implies C \haspatch \p$. - -\proofstarts - One of the Merge Ends conditions applies. Recall that we are considering$D \in \py$.$D \isin Y \equiv D \le Y$.$D \not\isin X$. We will show for each of various cases that if$M \haspatch \p$,$D \not\isin C$, One of the Merge Ends conditions applies. Recall that we are considering$D \in \py$.$D \isin Y \equiv D \le Y$.$D \not\isin X$. We will show for each of various cases that if$M \haspatch \p$,$D \not\isin C$, -whereas if$M \nothaspatch \p$,$D \isin C \equiv \land D \le C$. +whereas if$M \nothaspatch \p$,$D \isin C \equiv D \le C$. +And by$Y \haspatch \p$,$\exists_{F \in \py} F \le Y$and this +$F \le C$so this suffices. Consider$D = C$: Thus$C \in \py, L \in \py$. By Tip Own Contents,$\neg[ L \nothaspatch \p ]$so$L \neq X$, therefore we must have$L=Y$,$R=X$. By Tip Merge$M = \baseof{L}$so$M \in \pn$so by Base Acyclic$M \nothaspatch \p$. By$\merge$,$D \isin C$, Consider$D = C$: Thus$C \in \py, L \in \py$. By Tip Own Contents,$\neg[ L \nothaspatch \p ]$so$L \neq X$, therefore we must have$L=Y$,$R=X$. By Tip Merge$M = \baseof{L}$so$M \in \pn$so by Base Acyclic$M \nothaspatch \p$. By$\merge$,$D \isin C$, -and$D \le C$, consistent with$C \haspatch \p$. OK. +and$D \le C$. OK. Consider$D \neq C, M \nothaspatch \p, D \isin Y$:$D \le Y$so$D \le C$. Consider$D \neq C, M \nothaspatch \p, D \isin Y$:$D \le Y$so$D \le C\$.