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:
d2c96fc
)
merge ends condition - change condition to one that is equivalent but looks stronger...
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Thu, 8 Mar 2012 16:56:57 +0000
(16:56 +0000)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Thu, 8 Mar 2012 16:56:57 +0000
(16:56 +0000)
article.tex
patch
|
blob
|
history
diff --git
a/article.tex
b/article.tex
index dd4538988cdb51cc42c6dee6ab12edaf486126db..1feeb4834899e942a4d300f7d48df120e58426ec 100644
(file)
--- a/
article.tex
+++ b/
article.tex
@@
-493,8
+493,8
@@
We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
Y \haspatch \p
\implies
\begin{cases}
Y \haspatch \p
\implies
\begin{cases}
- M \haspatch \p : & \
displaystyle
-
\bigforall_{E \in \pendsof{Y}{\py}} E \le M
\\
+ M \haspatch \p : & \
pendsof{Y}{\py} = \pendsof{M}{\py}
+ \\
M \nothaspatch \p : & \displaystyle
\bigforall_{E \in \pendsof{X}{\py}} E \le Y
\end{cases}
M \nothaspatch \p : & \displaystyle
\bigforall_{E \in \pendsof{X}{\py}} E \le Y
\end{cases}
@@
-603,7
+603,7
@@
Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK.
Consider $D \neq C, M \haspatch P, D \isin Y$:
$D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Merge Ends
Consider $D \neq C, M \haspatch P, D \isin Y$:
$D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Merge Ends
-and Transitive Ancestors $D \le M$.
+and Transitive Ancestors $D \
in \pancsof{M}{\py}$ so $D \
le M$.
Thus $D \isin M$. By $\merge$, $D \not\isin C$. OK.
Consider $D \neq C, M \haspatch P, D \not\isin Y$:
Thus $D \isin M$. By $\merge$, $D \not\isin C$. OK.
Consider $D \neq C, M \haspatch P, D \not\isin Y$: