\newcommand{\gathbegin}{\begin{gather} \tag*{}}
\newcommand{\gathnext}{\\ \tag*{}}
+\newcommand{\true}{t}
+\newcommand{\false}{f}
+
\begin{document}
\section{Notation}
$ D \le C $.
Contents of $C$:
-$ D \isin C \equiv \ldots \lor t \text{ so } D \haspatch C $.
+$ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
\subsubsection{For $A \haspatch P, D \neq C$:}
Ancestors: $ D \le C \equiv D \le A $.
If $D = C$, trivial. For $D \neq C$:
$D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
+\section{Merge}
+
+Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
+\gathbegin
+ C \hasparents \{ L, 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}
+\end{gather}
+
+\subsection{Conditions}
+
+\[ \eqn{ Merges Exhaustive }{
+ L \in \py => \Bigl[ R \in \py \lor R \in \pn \Bigr]
+}\]
+\[ \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]
+}\]
+
\end{document}