From f8dce57b7b88b1ecac72b81f3d3511630b5c7d8d Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Sun, 11 Mar 2012 09:02:57 +0000 Subject: [PATCH] wip merge tip contents --- article.tex | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/article.tex b/article.tex index 71e0960..3da2db9 100644 --- a/article.tex +++ b/article.tex @@ -648,8 +648,8 @@ R$. And $D \neq C$. So $D \not\isin C$. $\qed$ We need worry only about $C \in \py$. And $\patchof{C} = \patchof{L}$ -so $L \in \py$ so $L \haspatch \p$. We will use the coherence and -patch inclusion of $C$ as just proved. +so $L \in \py$ so $L \haspatch \p$. We will use the unique base, +and coherence and patch inclusion, of $C$ as just proved. Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch \p$ and by coherence/inclusion $C \haspatch \p$ . If $R \not\in \py$ @@ -667,11 +667,13 @@ $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D $D \neq C$. By Tip Contents of $L$, $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition, -$D \isin L \equiv D \isin M$. xxx up to here - +$D \isin L \equiv D \isin M$. So by definition of $\merge$, $D \isin +C \equiv D \isin R$. And $R = \baseof{C}$ by Unique Base of $C$. +Thus $D \isin C \equiv D \isin \baseof{C}$. OK. \subsubsection{For $D \not\in \py, R \in \py$:} +xxx up to here %D \in \py$:} -- 2.30.2