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:
81ac90d
)
use \p rather than just P
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Tue, 6 Mar 2012 17:46:30 +0000
(17:46 +0000)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Tue, 6 Mar 2012 17:46:30 +0000
(17:46 +0000)
article.tex
patch
|
blob
|
history
diff --git
a/article.tex
b/article.tex
index 2f512f4c96e2215b002ae886742a107753823bb2..6a5023c3ceaf24813e16dfbe0d309a2a38e22178 100644
(file)
--- a/
article.tex
+++ b/
article.tex
@@
-536,19
+536,19
@@
$\qed$
\subsection{Coherence and patch inclusion}
\subsection{Coherence and patch inclusion}
-Need to determine $C \haspatch
P$ based on $L,M,R \haspatch P
$.
+Need to determine $C \haspatch
\p$ based on $L,M,R \haspatch \p
$.
This involves considering $D \in \py$.
This involves considering $D \in \py$.
-\subsubsection{For $L \nothaspatch
P, R \nothaspatch P
$:}
+\subsubsection{For $L \nothaspatch
\p, R \nothaspatch \p
$:}
$D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
$D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
-\in \py$ ie $L \haspatch
P
$ by Tip Self Inpatch). So $D \neq C$.
-Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch
P
$.
+\in \py$ ie $L \haspatch
\p
$ by Tip Self Inpatch). So $D \neq C$.
+Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch
\p
$.
-\subsubsection{For $L \haspatch
P, R \haspatch P
$:}
+\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$.)
$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 \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$.
@@
-556,23
+556,23
@@
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 \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 \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 \haspatch
\p
$.
-So indeed $L \haspatch
P \land R \haspatch P \implies C \haspatch P
$.
+So indeed $L \haspatch
\p \land R \haspatch \p \implies C \haspatch \p
$.
-\subsubsection{For (wlog) $X \not\haspatch
P, Y \haspatch P
$:}
+\subsubsection{For (wlog) $X \not\haspatch
\p, Y \haspatch \p
$:}
-$C \haspatch
P
\equiv C \nothaspatch M$.
+$C \haspatch
\p
\equiv C \nothaspatch M$.
\proofstarts
\proofstarts