From a2f21df285ac3c9f388cf8dbe3125f6b559c47cd Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Sun, 11 Mar 2012 08:12:49 +0000 Subject: [PATCH] wip merge tip contents --- article.tex | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/article.tex b/article.tex index 39a1287..643ef44 100644 --- a/article.tex +++ b/article.tex @@ -633,17 +633,18 @@ R$. And $D \neq C$. So $D \not\isin C$. $\qed$ \subsection{Tip Contents} -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$. If $R \not\in \py$ then -by Tip Merge +Firstly we prove $C \haspatch \p$: If $R \in \py$, then $R \haspatch +\p$ and by coherence/inclusion $C \haspatch \p$ . If $R \not\in \py$ +then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition +of $\nothaspatch$, $M \nothaspatch \p$. So by coherence/inclusion $C +\haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$). +xxx up to here We will consider some $D$ and prove the Exclusive Tip Contents form. -- 2.30.2