chiark
/
gitweb
/
~ian
/
topbloke-formulae.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
60aa55b
)
anticommit desired contents
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Tue, 6 Mar 2012 14:34:10 +0000
(14:34 +0000)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Tue, 6 Mar 2012 14:34:10 +0000
(14:34 +0000)
article.tex
patch
|
blob
|
history
diff --git
a/article.tex
b/article.tex
index 0e3732d7c5f0ec97f17143a477aea7a1c6eb5d90..4c7f22cbc50446b5a2997c39107e60932727085c 100644
(file)
--- a/
article.tex
+++ b/
article.tex
@@
-423,19
+423,37
@@
Merge Results applies. $\qed$
\subsection{Desired Contents}
\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.
{\it Proof.}
\subsubsection{For $D = C$:}
Trivially $D \isin C$. OK.
-\subsubsection{For $D \n
ot\le C
$:}
+\subsubsection{For $D \n
eq 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}
\subsection{Unique Base}