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:
1059b23
)
wip anticommit desired contents
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Tue, 6 Mar 2012 09:39:12 +0000
(09:39 +0000)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Tue, 6 Mar 2012 09:39:12 +0000
(09:39 +0000)
article.tex
patch
|
blob
|
history
diff --git
a/article.tex
b/article.tex
index 4c5f6751682c83a13e478fdb11d64496abd1bd22..b71bb326c09fcf3eb8387c075b3f7ded903087b6 100644
(file)
--- a/
article.tex
+++ b/
article.tex
@@
-408,10
+408,9
@@
Used for removing a branch dependency.
\[ \eqn{ Currently Included }{
L \haspatch \pry
}\]
\[ \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}
\subsection{No Replay}
@@
-419,6
+418,22
@@
By Unique Tip, $R^+ \le L$. By definition of $\base$, $R^- \le R^+$
so $R^- \le L$. So $R^+ \le C$ and $R^- \le C$ and No Replay for
Merge Results applies. $\qed$
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$.
\subsection{Unique Base}
Need to consider only $C \in \py$, ie $L \in \py$.