\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
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.
+