From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Sun, 11 Mar 2012 17:43:32 +0000 (+0000)
Subject: prove and use totally foreign contents
X-Git-Tag: f0.2~74
X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=commitdiff_plain;h=e7cc038625f9a268e3fa32853f5227d44e374449;p=topbloke-formulae.git

prove and use totally foreign contents
---

diff --git a/article.tex b/article.tex
index f69420f..65be01f 100644
--- a/article.tex
+++ b/article.tex
@@ -301,12 +301,16 @@ xxx proof tbd
    \right]
   \implies
    \left[
-    D \isin C
+    D \le C
    \implies
     \patchof{D} = \bot
    \right]
 }\]
-xxx proof tbd
+\proof{
+Consider some $D \le C$.  If $D = C$, $\patchof{D} = \bot$ trivially.
+If $D \neq C$ then $D \le A$ where $A \in \set A$.  By Foreign
+Contents of $A$, $\patchof{D} = \bot$.
+}
 
 \subsection{No Replay for Merge Results}
 
@@ -461,10 +465,8 @@ $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 
 \subsection{Foreign Contents:}
 
-Only relevant if $\patchof{C} = \bot$.  Trivial by Foreign Contents of
-$A$.  $\qed$
-
-xxx fixme not trivial use Totally Foreign Contents
+Only relevant if $\patchof{C} = \bot$, and in that case Totally
+Foreign Contents applies. $\qed$
 
 \section{Create Base}
 
@@ -908,9 +910,8 @@ $\qed$
 
 \subsection{Foreign Contents}
 
-xxx use Totally Foreign Contents
-
-If $\patchof{C} = \bot$, by Foreign Merges
-$\patchof{L} = \patchof{R} = \bot$.
+Only relevant if $\patchof{L} = \bot$, in which case
+$\patchof{C} = \bot$ and by Foreign Merges $\patchof{R} = \bot$,
+so Totally Foreign Contents applies.  $\qed$
 
 \end{document}