+\subsection{Conditions}
+
+\[ \eqn{ Tip Merge }{
+ L \in \py \implies
+ \begin{cases}
+ R \in \py : & \baseof{R} \ge \baseof{L}
+ \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
+ R \in \pn : & R \ge \baseof{L}
+ \land M = \baseof{L} \\
+ \text{otherwise} : & \false
+ \end{cases}
+}\]
+
+\subsection{No Replay}
+
+\subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
+
+\subsubsection{For $D \isin L \land D \isin R$:}
+$D \isin C$. And $D \isin L \implies D \le L \implies D \le C$. OK.
+
+\subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
+$D \not\isin C$. OK.
+
+\subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
+$D \not\isin C$. OK.
+
+\subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
+ \land D \not\isin M$:}
+$D \isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
+R$ so $D \le C$. OK.
+
+\subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
+ \land D \isin M$:}
+$D \not\isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
+R$ so $D \le C$. OK.
+
+$\qed$