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=1ca4af73574a7343d367fed94ebc945d105dc7a3;hb=dbc2fa88cece12d33ca5788ad5d359f77676a802;hpb=410132e37a1f6e95cbfa9792d63b50b9390e59e4;ds=sidebyside

diff --git a/merge.tex b/merge.tex
index 1ca4af7..7a48a25 100644
--- a/merge.tex
+++ b/merge.tex
@@ -111,14 +111,23 @@ $\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 $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$.
@@ -150,18 +159,13 @@ 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.