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:
7e264f9
)
new foreign contents restriction
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Sun, 11 Mar 2012 17:34:15 +0000
(17:34 +0000)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Sun, 11 Mar 2012 17:34:15 +0000
(17:34 +0000)
article.tex
patch
|
blob
|
history
diff --git
a/article.tex
b/article.tex
index 73217528caf6f8329960297c22fc687353e5fecf..7630745d41eaf60ca7369bd99e7ec29ea03cbe98 100644
(file)
--- a/
article.tex
+++ b/
article.tex
@@
-196,6
+196,10
@@
We maintain these each time we construct a new commit. \\
\[\eqn{Foreign Inclusion:}{
\bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
}\]
\[\eqn{Foreign Inclusion:}{
\bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
}\]
+\[\eqn{Foreign Contents:}{
+ \bigforall_{C \text{ s.t. } \patchof{C} = \bot}
+ D \le C \implies \patchof{D} = \bot
+}\]
\section{Some lemmas}
\section{Some lemmas}
@@
-289,6
+293,21
@@
by the LHS. And $A \le A''$.
}\]
xxx proof tbd
}\]
xxx proof tbd
+\[ \eqn{Totally Foreign Contents:}{
+ \bigforall_{C \hasparents \set A}
+ \left[
+ \patchof{C} = \bot \land
+ \bigforall_{A \in \set A} \patchof{A} = \bot
+ \right]
+ \implies
+ \left[
+ D \isin C
+ \implies
+ \patchof{D} = \bot
+ \right]
+}\]
+xxx proof tbd
+
\subsection{No Replay for Merge Results}
If we are constructing $C$, with,
\subsection{No Replay for Merge Results}
If we are constructing $C$, with,