From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Thu, 8 Mar 2012 17:27:25 +0000 (+0000)
Subject: wip merge tip contents
X-Git-Tag: f0.2~122
X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=commitdiff_plain;h=60388f89942c560e84aff0e5a5d26075cc81d4e7

wip merge tip contents
---

diff --git a/article.tex b/article.tex
index 01297a8..aef968a 100644
--- a/article.tex
+++ b/article.tex
@@ -616,4 +616,25 @@ By $\merge$, $D \not\isin C$.  OK.
 
 $\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.
+
+xxx the coherence is not that useful ?
+
+\subsubsection{For $L \in \py, D \in \py$:}
+
+xxx need to recheck this
+
+$C \in \py$ $C \haspatch P$ so $D \isin C \equiv D \le C$.  OK.
+
+\subsubsection{For $L \in \py, D \not\in \py, R \in \py$:}
+
+Tip Contents for $L$: $D \isin L \equiv D \isin \baseof{L}$.
+
+Tip Contents for $R$: $D \isin R \equiv D \isin \baseof{R}$.
+
+But by Tip Merge, $\baseof{R} \ge \baseof{L}$
+
 \end{document}