chiark / gitweb /
prove and use totally foreign contents
authorIan Jackson <ijackson@chiark.greenend.org.uk>
Sun, 11 Mar 2012 17:43:32 +0000 (17:43 +0000)
committerIan Jackson <ijackson@chiark.greenend.org.uk>
Sun, 11 Mar 2012 17:43:32 +0000 (17:43 +0000)
article.tex

index f69420f..65be01f 100644 (file)
@@ -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}