chiark
/
gitweb
/
~ian
/
topbloke-formulae.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
6424f58
)
wip exclusive haspatch - fix Merge Coherence (for both haspatch)
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Wed, 21 Mar 2012 21:25:27 +0000
(21:25 +0000)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Wed, 21 Mar 2012 21:25:27 +0000
(21:25 +0000)
merge.tex
patch
|
blob
|
history
diff --git
a/merge.tex
b/merge.tex
index fc5df3bbba880e392eccee6b0da74581b7f04a42..ca3304d26b0b5442f968f7f92a461f783e6ded13 100644
(file)
--- 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$.)
$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 \
z
haspatch \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,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$
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 \
z
haspatch \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 \
z
haspatch \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 \
z
haspatch \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$:}