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:
ff4ffb2
)
pseudomerge: Fix Foreign Inclusion
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Sat, 10 Aug 2013 14:53:50 +0000
(15:53 +0100)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Sat, 10 Aug 2013 14:53:50 +0000
(15:53 +0100)
pseudomerge.tex
patch
|
blob
|
history
diff --git
a/pseudomerge.tex
b/pseudomerge.tex
index 27b2e528525bef39cd8a2bfe8556389cac0ff5c7..c1a88f8c6dc170be2e451902101dcc6ebebb5970 100644
(file)
--- a/
pseudomerge.tex
+++ b/
pseudomerge.tex
@@
-88,7
+88,15
@@
Explicitly dealt with by our Unique Tips condition.
\subsection{Foreign Inclusion}
-True by Foreign Identical, and Foreign Inclusion of $L$.
+We need to consider $D \in \foreign$.
+
+For $D = C$: $D \has C$, $D \le C$; OK.
+
+For $D \neq C$: $D \has C \equiv D \has L$ by construction.
+$D \has L \equiv D \le L$ by Foreign Inclusion of $L$.
+$D \neq C$ so this $D \le L \equiv D \le C$.
+
+$\qed$
\subsection{Foreign Ancestry}