X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=blobdiff_plain;f=merge.tex;h=881dd249cce6b73a0a97e83b6173383af844c3df;hb=35d8920c70badf3ea6556ad6cf53ea96ef6aec0c;hp=9daaa00450ae562db1d3af581b856e08de0e4af0;hpb=547f81711b274591ce075b8df2c3e41c6394eb93;p=topbloke-formulae.git

diff --git a/merge.tex b/merge.tex
index 9daaa00..881dd24 100644
--- a/merge.tex
+++ b/merge.tex
@@ -1,4 +1,5 @@
 \section{Merge}
+\label{commit-merge}
 
 Merge commits $L$ and $R$ using merge base $M$:
 \gathbegin
@@ -27,6 +28,16 @@ satisfied; in particular, provided that $L \ge \baseof{R}$.
       \text{otherwise} : & \false
    \end{cases}
 }\]
+\[ \eqn{ Base Merge }{
+ L \in \pn \implies
+  \big[
+   R \in \pn
+     \lor
+   R \in \foreign
+     \lor
+   R \in \pqy
+  \big]
+}\]
 \[ \eqn{ Merge Acyclic }{
     L \in \pn
    \implies
@@ -314,3 +325,24 @@ $\qed$
 Only relevant if $\isforeign{L}$, in which case
 $\isforeign{C}$ and by Foreign Merges $\isforeign{R}$,
 so Totally Foreign Contents applies.  $\qed$
+
+\subsection{Bases' Children}
+
+If $L \in \py, R \in \py$: not applicable for either $D=L$ or $D=R$.
+
+If $L \in \py, R \in \pn$: not applicable for $L$, OK for $R$.
+
+Other possibilities for $L \in \py$ are excluded by Tip Merge.
+
+If $L \in \pn, R \in \pn$: satisfied for both $L$ and $R$.
+
+If $L \in \pn, R \in \foreign$: satisfied for $L$, not applicable for
+$R$.
+
+If $L \in \pn, R \in \pqy$: satisfied for $L$, not applicable for
+$R$.
+
+Other possibilities for $L \in \pn$ are excluded by Base Merge.
+
+If $L \in \foreign$: not applicable for $L$; nor for $R$, by Foreign Merges.
+