From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Sun, 18 Mar 2012 11:00:01 +0000 (+0000)
Subject: merge coherence complex - remove unneeded ref to def of haspatch
X-Git-Tag: f0.3~44
X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=commitdiff_plain;h=bc5b48777942f1a3504812ef1822febf4c354984

merge coherence complex - remove unneeded ref to def of haspatch
---

diff --git a/merge.tex b/merge.tex
index 5dc99ee..fc5df3b 100644
--- a/merge.tex
+++ b/merge.tex
@@ -166,7 +166,7 @@ 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$.