X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=blobdiff_plain;f=article.tex;h=70d6d88200ffa76188a4e3fb553043e4094288a2;hb=bfa0996c930a2507501eec79b4a89333d35d47aa;hp=b7df641e68703266c1729e1c3abf32680e35f805;hpb=c132ec1004fa71f8ea8467b659d3f5996089f1dc;p=topbloke-formulae.git

diff --git a/article.tex b/article.tex
index b7df641..70d6d88 100644
--- a/article.tex
+++ b/article.tex
@@ -252,6 +252,7 @@ $ \bigforall_{C \in \py}\bigforall_{D \in \py}
     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
     \lor D = C
 }\]
+xxx proof tbd
 
 \[ \eqn{Transitive Ancestors:}{
   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
@@ -270,17 +271,23 @@ in which case we repeat for $A'$.  Since there are finitely many
 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
 by the LHS.  And $A \le A''$.
 }
+
 \[ \eqn{Calculation Of Ends:}{
   \bigforall_{C \hasparents \set A}
     \pendsof{C}{\set P} =
+      \begin{cases}
+       C \in \p : & \{ C \}
+      \\
+       C \not\in \p : & \displaystyle
        \left\{ E \Big|
            \Bigl[ \Largeexists_{A \in \set A} 
                        E \in \pendsof{A}{\set P} \Bigr] \land
            \Bigl[ \Largenexists_{B \in \set A} 
                        E \neq B \land E \le B \Bigr]
        \right\}
+      \end{cases}
 }\]
-XXX proof TBD.
+xxx proof tbd
 
 \subsection{No Replay for Merge Results}
 
@@ -327,10 +334,25 @@ We annotate each Topbloke commit $C$ with:
  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
 \end{gather}
 
+$\patchof{C}$, for each kind of Topbloke-generated commit, is stated
+in the summary in the section for that kind of commit.
+
+Whether $\baseof{C}$ is required, and if so what the value is, is
+stated in the proof of Unique Base for each kind of commit.
+
+$C \haspatch \pa{Q}$ or $\nothaspatch \pa{Q}$ is represented as the
+set $\{ \pa{Q} | C \haspatch \pa{Q} \}$.  Whether $C \haspatch \pa{Q}$
+is in stated
+(in terms of $I \haspatch \pa{Q}$ or $I \nothaspatch \pa{Q}$
+for the ingredients $I$),
+in the proof of Coherence for each kind of commit.
+
+$\pendsof{C}{\pa{Q}^+}$ is computed, for all Topbloke-generated commits,
+using the lemma Calculation of Ends, above.
 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
 make it wrong to make plain commits with git because the recorded $\pends$
-would have to be updated.  The annotation is not needed because
-$\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
+would have to be updated.  The annotation is not needed in that case
+because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
 
 \section{Simple commit}
 
@@ -520,6 +542,15 @@ So $L \nothaspatch \p \implies C \nothaspatch \p$.
 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
 so $L \haspatch \p \implies C \haspatch \p$.
 
+\section{Foreign Inclusion}
+
+Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
+So by Desired Contents $D \isin C \equiv D \isin L$.
+By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
+
+And $D \le C \equiv D \le L$.
+Thus $D \isin C \equiv D \le C$.  $\qed$
+
 \section{Merge}
 
 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):