-Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
-This involves considering $D \in \py$.
+$$
+\begin{cases}
+ L \nothaspatch \p \land R \nothaspatch \p : & C \nothaspatch \p \\
+ L \haspatch \p \land R \haspatch \p : & C \haspatch \p \\
+ \text{otherwise} \land M \haspatch \p : & C \nothaspatch \p \\
+ \text{otherwise} \land M \nothaspatch \p : & C \haspatch \p
+\end{cases}
+$$
+\proofstarts
+~ Consider $D \in \py$.
\subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
$D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
\subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
$D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
\subsubsection{For $L \haspatch \p, R \haspatch \p$:}
$D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
(Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
\subsubsection{For $L \haspatch \p, R \haspatch \p$:}
$D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
(Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
Consider $D \neq C, D \isin X \land D \isin Y$:
By $\merge$, $D \isin C$. Also $D \le X$
Consider $D \neq C, D \isin X \land D \isin Y$:
By $\merge$, $D \isin C$. Also $D \le X$
Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
By $\merge$, $D \not\isin C$.
And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
By $\merge$, $D \not\isin C$.
And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
$D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
Thus by $\merge$, $D \isin C$. And $D \le Y$ so $D \le C$.
Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
$D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
Thus by $\merge$, $D \isin C$. And $D \le Y$ so $D \le C$.
-So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
+So, in all cases, $C \zhaspatch \p$.
+And by $L \haspatch \p$, $\exists_{F \in \py} F \le L$
+and this $F \le C$ so indeed $C \haspatch \p$.
One of the Merge Ends conditions applies.
Recall that we are considering $D \in \py$.
$D \isin Y \equiv D \le Y$. $D \not\isin X$.
We will show for each of
various cases that
if $M \haspatch \p$, $D \not\isin C$,
One of the Merge Ends conditions applies.
Recall that we are considering $D \in \py$.
$D \isin Y \equiv D \le Y$. $D \not\isin X$.
We will show for each of
various cases that
if $M \haspatch \p$, $D \not\isin C$,
-whereas if $M \nothaspatch \p$, $D \isin C \equiv \land D \le C$.
+whereas if $M \nothaspatch \p$, $D \isin C \equiv D \le C$.
+And by $Y \haspatch \p$, $\exists_{F \in \py} F \le Y$ and this
+$F \le C$ so this suffices.