chiark
/
gitweb
/
~ian
/
topbloke-formulae.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Foreign Contents section in a couple of places
[topbloke-formulae.git]
/
article.tex
diff --git
a/article.tex
b/article.tex
index 0428df707a2978eae6c336b40447f29b5b820385..3d8bd8179a5f26dc787fa70a4de9046f32709f6d 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,
@@
-440,6
+459,13
@@
$\qed$
If $D = C$, trivial. For $D \neq C$:
$D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
If $D = C$, trivial. For $D \neq C$:
$D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
+\subsection{Foreign Contents:}
+
+Only relevant if $\patchof{C} = \bot$. Trivial by Foreign Contents of
+$A$. $\qed$
+
+xxx fixme not trivial use Totally Foreign Contents
+
\section{Create Base}
Given $L$, create a Topbloke base branch initial commit $B$.
\section{Create Base}
Given $L$, create a Topbloke base branch initial commit $B$.
@@
-484,7
+510,7
@@
xxx unfinished
\section{Create Tip}
\section{Create Tip}
-xxx tbd
\
+xxx tbd
\section{Anticommit}
\section{Anticommit}
@@
-598,7
+624,7
@@
so $L \haspatch \p \implies C \haspatch \p$.
$\qed$
$\qed$
-\section{Foreign Inclusion}
+\s
ubs
ection{Foreign Inclusion}
Consider some $D$ s.t. $\patchof{D} = \bot$. $D \neq C$.
So by Desired Contents $D \isin C \equiv D \isin L$.
Consider some $D$ s.t. $\patchof{D} = \bot$. $D \neq C$.
So by Desired Contents $D \isin C \equiv D \isin L$.
@@
-609,6
+635,10
@@
Thus $D \isin C \equiv D \le C$.
$\qed$
$\qed$
+\subsection{Foreign Contents:}
+
+Not applicable. $\qed$
+
\section{Merge}
Merge commits $L$ and $R$ using merge base $M$:
\section{Merge}
Merge commits $L$ and $R$ using merge base $M$:
@@
-869,4
+899,11
@@
OK
$\qed$
$\qed$
+\subsection{Foreign Contents:}
+
+xxx use Totally Foreign Contents
+
+If $\patchof{C} = \bot$, by Foreign Merges
+$\patchof{L} = \patchof{R} = \bot$.
+
\end{document}
\end{document}