wip anticommit; use \merge

diff --git a/article.tex b/article.tex
index 06b76126865f6c828a0fb58a3f7cbf9ae6d6c5b0..f712ba63fc0e7fdb37b78598eb1f192d357a634b 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -363,17 +363,24 @@ Used for removing a branch dependency.
 \gathnext
  \patchof{C} = \patchof{L}
 \gathnext
- D \isin C \equiv
-   \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}
+ \merge{C}{L}{R^+}{R^-}
 \end{gather}
 
-xxx want to prove $D \isin C \equiv D \not\in pry \land D \isin L$.
+\subsection{Conditions}
+
+\[ \eqn{ Unique Tip }{
+ \pendsof{L}{\pry} = \{ R^+ \}
+}\]
+\[ \eqn{ Correct Base }{
+ \baseof{R^+} = R^-
+}\]
+\[ \eqn{ Currently Included }{
+ L \haspatch \pry
+}\]
+
+
+
+xxx want to prove $D \isin C \equiv D \not\in \pry \land D \isin L$.
 
 \section{Merge}
 
@@ -383,12 +390,7 @@ Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 \gathnext
  \patchof{C} = \patchof{L}
 \gathnext
- D \isin C \equiv
-  \begin{cases}
-    (D \isin L \land D \isin R) \lor D = C : & \true \\
-    (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
-    \text{otherwise} : & D \not\isin M
-  \end{cases}
+ \merge{C}{L}{M}{R}
 \end{gather}
 
 \subsection{Conditions}