chiark / gitweb /
 author Ian Jackson Tue, 6 Mar 2012 14:34:10 +0000 (14:34 +0000) committer Ian Jackson Tue, 6 Mar 2012 14:34:10 +0000 (14:34 +0000)
 article.tex patch | blob | history

index 0e3732d..4c7f22c 100644 (file)
@@ -423,19 +423,37 @@ Merge Results applies. $\qed$

\subsection{Desired Contents}

-$D \isin C \equiv [ D \not\in \pry \land D \isin L ] \lor D = C$
+$D \isin C \equiv [ D \notin \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 \neq C, D \not\le L$:}

+By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
+$D \not\isin R^-$.  Thus $D \not\isin C$.  OK.

+\subsubsection{For $D \neq C, D \le L, D \in \pry$:}

-\subsubsection{For $D \in R^+$:}
-By Currently Included,
+By Currently Included, $D \isin L$.
+
+By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
+by Unique Tip, $D \le R^+ \equiv D \le L$.
+So $D \isin R^+$.
+
+By Base Acyclic, $D \not\isin R^-$.
+
+Apply $\merge$: $D \not\isin C$.  OK.
+
+\subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
+
+By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
+
+Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
+
+$\qed$

\subsection{Unique Base}