chiark
/
gitweb
/
~ian
/
topbloke-formulae.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
cb50366
)
merge ends conditions change order of precondition to put M in middle, for clarity
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Thu, 15 Mar 2012 19:20:27 +0000
(19:20 +0000)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Thu, 15 Mar 2012 19:20:27 +0000
(19:20 +0000)
article.tex
patch
|
blob
|
history
diff --git
a/article.tex
b/article.tex
index ab9d645f11059e3534939ece640708ed02e0cc4a..45acbb30bf9573e9b76e72109f8a04c2cc85d126 100644
(file)
--- 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 \not
haspatch \p
+
M \not
haspatch \p \land
+
Y \
haspatch \p
\implies \left[
\bigforall_{E \in \pendsof{X}{\py}} E \le Y
\right]