From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Wed, 21 Mar 2012 21:25:27 +0000 (+0000)
Subject: wip exclusive haspatch - fix Merge Coherence (for both haspatch)
X-Git-Tag: f0.3~21
X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=commitdiff_plain;ds=sidebyside;h=ec16deb7967d93aa02befa015c339a8e8f30ae07;p=topbloke-formulae.git

wip exclusive haspatch - fix Merge Coherence (for both haspatch)
---

diff --git a/merge.tex b/merge.tex
index fc5df3b..ca3304d 100644
--- a/merge.tex
+++ b/merge.tex
@@ -124,7 +124,7 @@ Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \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,19 +132,21 @@ 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$:}