\[ \eqn{ Currently Included }{
L \haspatch \pry
}\]
-
-\subsection{Desired Contents}
-
-xxx need to prove $D \isin C \equiv D \not\in \pry \land D \isin L$.
+\[ \eqn{ Not Self }{
+ L \not\in \{ R^+ \}
+}\]
\subsection{No Replay}
so $R^- \le L$. So $R^+ \le C$ and $R^- \le C$ and No Replay for
Merge Results applies. $\qed$
+\subsection{Desired Contents}
+
+\[ $D \isin C \equiv [ D \not\in \pry \land D \isin L$ ] \lor D = C \]
+{\it Proof.}
+
+\subsubsection{For $D = C$:}
+
+Trivially $D \isin C$. OK.
+
+\subsubsection{For $D \not\le C$:}
+
+
+
+\subsubsection{For $D \in R^+$:}
+By Currently Included,
+
\subsection{Unique Base}
Need to consider only $C \in \py$, ie $L \in \py$.