chiark / gitweb /
wip merge tip contents
authorIan Jackson <ijackson@chiark.greenend.org.uk>
Thu, 8 Mar 2012 17:27:25 +0000 (17:27 +0000)
committerIan Jackson <ijackson@chiark.greenend.org.uk>
Thu, 8 Mar 2012 17:27:25 +0000 (17:27 +0000)
article.tex

index 01297a8..aef968a 100644 (file)
@@ -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}