chiark / gitweb /
 author Ian Jackson Sun, 11 Mar 2012 17:43:32 +0000 (17:43 +0000) committer Ian Jackson Sun, 11 Mar 2012 17:43:32 +0000 (17:43 +0000)
 article.tex patch | blob | history

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}