merge: add non-cyclic Condition to Base Merge (although I think it's implied by Merge...

[topbloke-formulae.git] / pseudomerge.tex

diff --git a/pseudomerge.tex b/pseudomerge.tex
index a8ba08a6ebcaf247ac27eb89aa5f5adc658e2dba..c1a88f8c6dc170be2e451902101dcc6ebebb5970 100644 (file)
--- a/pseudomerge.tex
+++ b/pseudomerge.tex
@@ -88,9 +88,17 @@ 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$.
 
-\subsection{Foreign Contents}
+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}
 
 Not applicable.