From 27639d3c9826ecc3e57e43d686147f4b9ccd961e Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Sun, 11 Mar 2012 08:17:50 +0000 Subject: [PATCH] wip merge tip contents --- article.tex | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/article.tex b/article.tex index 643ef44..2121fb4 100644 --- a/article.tex +++ b/article.tex @@ -644,16 +644,13 @@ 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. +\subsubsection{For $D \in \py$:} +$C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D +\le C$. OK. -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 +xxx up to here \subsubsection{For $L \in \py, D \not\in \py, R \in \py$:} -- 2.30.2