From cb4b2dd9304a4ff862894f6cbc9cc54b3963cb7f Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Thu, 8 Mar 2012 18:35:43 +0000 Subject: [PATCH] wip merge tip contents --- article.tex | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/article.tex b/article.tex index d5451ea..775bcb3 100644 --- a/article.tex +++ b/article.tex @@ -634,11 +634,27 @@ R$. And $D \neq C$. So $D \not\isin C$. $\qed$ \subsection{Tip Contents} We will consider some $D$ and prove the Exclusive Tip Contents form. -We use the Coherence of $C$ as just proved. +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. + +Firstly we prove $C \haspatch \p$: If $R \in \py$, this is true by +coherence/inclusion $C \haspatch \p$. So by definition of +$\haspatch$, $D \isin C \equiv D \le C$. OK. + +\subsubsection{For $L \in \py, D \in \py, $:} +$R \haspatch \p$ so + +\subsubsection{For $L \in \py, D \not\in \py, R \in \py$:} + + +%D \in \py$:} + + xxx the coherence is not that useful ? -\subsubsection{For $L \in \py, D \in \py$:} +$L \haspatch \p$ by xxx need to recheck this -- 2.30.2