chiark / gitweb /
 author Ian Jackson Thu, 8 Mar 2012 18:46:34 +0000 (18:46 +0000) committer Ian Jackson Thu, 8 Mar 2012 18:46:34 +0000 (18:46 +0000)
 article.tex patch | blob | history

index 775bcb3..39a1287 100644 (file)
@@ -633,13 +633,22 @@ 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 need worry only about$C \in \py$. And$\patchof{C} = \patchof{L}$+xxx up to here + +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 +coherence/inclusion$C \haspatch \p$. If$R \not\in \py$then +by Tip Merge + + +We will consider some$D$and prove the Exclusive Tip Contents form. + + +So by definition of$\haspatch$,$D \isin C \equiv D \le C$. OK. \subsubsection{For$L \in \py, D \in \py, \$:}