annotation calculation

[topbloke-formulae.git] / article.tex

diff --git a/article.tex b/article.tex
index 7f55e4fea15e0ba20f05978cfe052a2f5dee1101..70d6d88200ffa76188a4e3fb553043e4094288a2 100644 (file)
--- 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}
 
@@ -444,6 +466,9 @@ Used for removing a branch dependency.
 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$.
 
+(Note that the merge base $R^+ \not\le R^-$, i.e. the merge base is
+later than one of the branches to be merged.)
+
 \subsection{No Replay}
 
 No Replay for Merge Results applies.  $\qed$
@@ -517,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$):
@@ -574,7 +608,7 @@ Merge Ends condition applies.  Good.
 
 \subsection{No Replay}
 
-See No Replay for Merge Results.
+No Replay for Merge Results applies.  $\qed$
 
 \subsection{Unique Base}