X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=blobdiff_plain;f=merge.tex;h=fc5df3bbba880e392eccee6b0da74581b7f04a42;hb=bc5b48777942f1a3504812ef1822febf4c354984;hp=d9415bcb88e5c7fbd8d0a244763f079c1348695d;hpb=d3b82154c687961e6c53e88d3eca0729f632c347;p=topbloke-formulae.git

diff --git a/merge.tex b/merge.tex
index d9415bc..fc5df3b 100644
--- a/merge.tex
+++ b/merge.tex
@@ -157,15 +157,16 @@ One of the Merge Ends conditions applies.
 Recall that we are considering $D \in \py$.
 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
 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$).
+various cases that
+if $M \haspatch \p$, $D \not\isin C$,
+whereas if $M \nothaspatch \p$, $D \isin C \equiv \land D \le C$.
 
 Consider $D = C$:  Thus $C \in \py, L \in \py$.
 By Tip Own Contents, $\neg[ L \nothaspatch \p ]$ so $L \neq X$,
 therefore we must have $L=Y$, $R=X$.
 By Tip Merge $M = \baseof{L}$ so $M \in \pn$ so
 by Base Acyclic $M \nothaspatch \p$.  By $\merge$, $D \isin C$,
-and $D \le C$, consistent with $C \haspatch \p$.  OK.
+and $D \le C$.  OK.
 
 Consider $D \neq C, M \nothaspatch \p, D \isin Y$:
 $D \le Y$ so $D \le C$.