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:
3ac7463
)
clarify merge complex D=C
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Sun, 25 Mar 2012 20:02:02 +0000
(21:02 +0100)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Sun, 25 Mar 2012 20:02:02 +0000
(21:02 +0100)
merge.tex
patch
|
blob
|
history
diff --git
a/merge.tex
b/merge.tex
index 90f5ab2ede0ee1cbc92ccaf41374242f5cb72028..48e72702c780d17648ffe6ef5d5e5a6b1253fcce 100644
(file)
--- a/
merge.tex
+++ b/
merge.tex
@@
-172,7
+172,8
@@
$F \le C$ so this suffices.
Consider $D = C$: Thus $C \in \py, L \in \py$.
By Tip Own Contents, $L \haspatch \p$ so $L \neq X$,
therefore we must have $L=Y$, $R=X$.
Consider $D = C$: Thus $C \in \py, L \in \py$.
By Tip Own Contents, $L \haspatch \p$ so $L \neq X$,
therefore we must have $L=Y$, $R=X$.
-By Tip Merge $M = \baseof{L}$ so $M \in \pn$ so
+Conversely $R \not\in \py$
+so by Tip Merge $M = \baseof{L}$. Thus $M \in \pn$ so
by Base Acyclic $M \nothaspatch \p$. By $\merge$, $D \isin C$,
and $D \le C$. OK.
by Base Acyclic $M \nothaspatch \p$. By $\merge$, $D \isin C$,
and $D \le C$. OK.