From: Ian Jackson Date: Thu, 15 Mar 2012 19:20:27 +0000 (+0000) Subject: merge ends conditions change order of precondition to put M in middle, for clarity X-Git-Tag: f0.2~22 X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=commitdiff_plain;h=8addc4c379707bd89ab14defc11914a85ee45254;p=topbloke-formulae.git merge ends conditions change order of precondition to put M in middle, for clarity --- diff --git a/article.tex b/article.tex index ab9d645..45acbb3 100644 --- a/article.tex +++ b/article.tex @@ -823,15 +823,15 @@ $L \in \pn$, $R \in \pry$, $M = \baseof{R}$. }\] \[ \eqn{ Removal Merge Ends }{ X \not\haspatch \p \land - Y \haspatch \p \land - M \haspatch \p + M \haspatch \p \land + Y \haspatch \p \implies \pendsof{Y}{\py} = \pendsof{M}{\py} }\] \[ \eqn{ Addition Merge Ends }{ X \not\haspatch \p \land - Y \haspatch \p \land - M \nothaspatch \p + M \nothaspatch \p \land + Y \haspatch \p \implies \left[ \bigforall_{E \in \pendsof{X}{\py}} E \le Y \right]