\end{cases}
$
-Some (overlapping) alternative formulations:
-
-$\displaystyle D \isin C \equiv
- \begin{cases}
- D \isin L \equiv D \isin R : & D = C \lor D \isin L \\
- D \isin L \equiv D \isin R : & D = C \lor D \isin R \\
- D \isin L \nequiv D \isin R : & D = C \lor D \not\isin M \\
- D \isin M \equiv D \isin L : & D = C \lor D \isin R \\
- D \isin M \equiv D \isin R : & D = C \lor D \isin L \\
- \end{cases}
-$
-
\end{basedescript}
\newpage
\section{Invariants}
\section{Some lemmas}
+\[ \eqn{Alternative (overlapping) formulations defining
+ $\mergeof{C}{L}{M}{R}$:}{
+ D \isin C \equiv
+ \begin{cases}
+ D \isin L \equiv D \isin R : & D = C \lor D \isin L \\
+ D \isin L \nequiv D \isin R : & D = C \lor D \not\isin M \\
+ D \isin L \equiv D \isin M : & D = C \lor D \isin R \\
+ D \isin L \nequiv D \isin M : & D = C \lor D \isin L \\
+ \text{as above with L and R exchanged}
+ \end{cases}
+}\]
+\proof{
+ Truth table xxx
+
+ Original definition is symmetrical in $L$ and $R$.
+}
+
\[ \eqn{Exclusive Tip Contents:}{
\bigforall_{C \in \py}
\neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )