{\hbox{\scriptsize$\forall$}}}%
}
+\newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
+\newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
\newcommand{\qed}{\square}
\newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
\item[ $ \pendsof{C}{\set P} $ ]
$ \{ E \; | \; E \in \pancsof{C}{\set P}
\land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
- A \neq E \land E \le A \} $
+ E \neq A \land E \le A \} $
i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
\item[ $ \baseof{C} $ ]
\subsection{No Replay}
-\subsubsection{For $D=C$:} $D \isin C, D \le C$, trivial.
+\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
+$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$
\end{document}