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:
400772c
)
wip merge
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Fri, 2 Mar 2012 16:34:20 +0000
(16:34 +0000)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Fri, 2 Mar 2012 16:34:20 +0000
(16:34 +0000)
article.tex
patch
|
blob
|
history
diff --git
a/article.tex
b/article.tex
index d85a022ff8fb8388f380325f4ffd4ed9e4330d5d..1f3d1647d8df7544fe1eabf8e2d8b6841b6d069b 100644
(file)
--- a/
article.tex
+++ b/
article.tex
@@
-334,15
+334,22
@@
Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
\subsection{Conditions}
\subsection{Conditions}
-\[ \eqn{ Merges Exhaustive }{
- L \in \py => \Bigl[ R \in \py \lor R \in \pn \Bigr]
-}\]
\[ \eqn{ Tip Merge }{
\[ \eqn{ Tip Merge }{
- L \in \py \land R \in \py \implies \Bigl[ \text{TBD} \Bigr]
-}\]
-\[ \eqn{ Base Merge }{
- L \in \py \land R \in \pn \implies \Bigl[ R \ge \baseof{L} \land M =
- \baseof{L} \Bigr]
+ L \in \py \implies
+ \begin{cases}
+ R \in \py : & \baseof{R} \ge \baseof{L}
+ \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
+ R \in \pn : & R \ge \baseof{L}
+ \land M = \baseof{L} \\
+ \text{otherwise} : & \false
+ \end{cases}
}\]
}\]
+\subsection{No Replay}
+
+\subsubsection{For $D=C$:} $D \isin C, D \le C$, trivial.
+
+\subsubsection{For $D \isin L \land D \isin R$:}
+$D \isin C$. And $D \isin L
+
\end{document}
\end{document}