From 2a35782b2846fda8b2b879c14fa940e5f703afc7 Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Thu, 8 Mar 2012 16:21:23 +0000 Subject: [PATCH] wip merge complex --- article.tex | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/article.tex b/article.tex index fac5c82..be767aa 100644 --- a/article.tex +++ b/article.tex @@ -583,9 +583,19 @@ We will show for each of various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$ (which suffices by definition of $\haspatch$ and $\nothaspatch$). -Consider $D = C$. Thus $C \in \py, L \in \py$, and by Tip +Consider $D = C$: Thus $C \in \py, L \in \py$, and by Tip Self Inpatch $L \haspatch \p$, so $L=Y, R=X$. By Tip Merge, $M=\baseof{L}$. So by Base Acyclic $D \not\isin M$, i.e. $M \nothaspatch \p$. And indeed $D \isin C$ and $D \le C$. OK. +Consider $D \neq C, M \nothaspatch P, D \isin Y$: +$D \le Y$ so $D \le C$. +$D \not\isin M$ so by $\merge$, $D \isin C$. OK. + +Consider $D \neq C, M \nothaspatch P, D \not\isin Y$: +$D \not\le Y$. If $D \le X$ then +$D \in \pancsof{X}{\py}$, so by Merge Ends and +Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$. +Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK. + \end{document} -- 2.1.4