chiark / gitweb /
 author Ian Jackson Wed, 21 Mar 2012 21:25:27 +0000 (21:25 +0000) committer Ian Jackson Wed, 21 Mar 2012 21:25:27 +0000 (21:25 +0000)
 merge.tex patch | blob | history

index fc5df3b..ca3304d 100644 (file)
--- a/merge.tex
+++ b/merge.tex
@@ -124,7 +124,7 @@ Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
$D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
(Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)

-Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
+Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \zhaspatch \p$.

For $D \neq C$: $D \le C \equiv D \le L \lor D \le R \equiv D \isin L \lor D \isin R$.
@@ -132,19 +132,21 @@ For $D \neq C$: $D \le C \equiv D \le L \lor D \le R Consider$D \neq C, D \isin X \land D \isin Y$: By$\merge$,$D \isin C$. Also$D \le X$-so$D \le C$. OK for$C \haspatch \p$. +so$D \le C$. OK for$C \zhaspatch \p$. Consider$D \neq C, D \not\isin X \land D \not\isin Y$: By$\merge$,$D \not\isin C$. And$D \not\le X \land D \not\le Y$so$D \not\le C$. -OK for$C \haspatch \p$. +OK for$C \zhaspatch \p$. Remaining case, wlog, is$D \not\isin X \land D \isin Y$.$D \not\le X$so$D \not\le M$so$D \not\isin M$. Thus by$\merge$,$D \isin C$. And$D \le Y$so$D \le C$. -OK for$C \haspatch \p$. +OK for$C \zhaspatch \p$. -So indeed$L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$. +So, in all cases,$C \zhaspatch \p$. +And by$L \haspatch \p$,$\exists_{F \in \py} F \le L$+and this$F \le C$so indeed$C \haspatch \p$. \subsubsection{For (wlog)$X \not\haspatch \p, Y \haspatch \p\$:}