X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=merge.tex;h=7a48a25cf994a282b5c1d74d019af0f45aafb7d2;hp=5dc99ee548760ebeb80f908a8d1dd959416bd928;hb=dbc2fa88cece12d33ca5788ad5d359f77676a802;hpb=23862a524934c97cc30445f0250c943df589c729 diff --git a/merge.tex b/merge.tex index 5dc99ee..7a48a25 100644 --- a/merge.tex +++ b/merge.tex @@ -111,20 +111,29 @@ $\qed$ \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 -\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$. +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$.) -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$. @@ -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$ -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$. -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$. -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$:} -$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$, -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$, -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$.