traversal: wip prove Recreate Base Beginning OK, currently need to prove Tip Correct...

[topbloke-formulae.git] / annotations.tex

diff --git a/annotations.tex b/annotations.tex
index 72b00e8cc63055f3dbcb3db1a9e5fbd6d6b6ea0a..b4e86dab19b0648af7998e233209b520e0b7011c 100644 (file)
--- a/annotations.tex
+++ b/annotations.tex
@@ -10,6 +10,8 @@ We annotate each Topbloke commit $C$ with:
    \text{ either } C \haspatch \p \text{ or } C \nothaspatch \p
 \gathnext
  \bigforall_{\py \not\ni C} \pendsof{C}{\py}
+\gathnext
+ \pendsof{C}{\foreign}
 \end{gather}
 
 $\patchof{C}$, for each kind of Topbloke-generated commit, is stated
@@ -19,7 +21,7 @@ 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 \p$ or $\nothaspatch \p$ is represented as a
-list of $\p$ for which it is known that $C \haspatch \p$;
+list of $\p$ for which $C \haspatch \p$;
 for any $\p$ not listed, $C \nothaspatch \p$.
 Whether to record $C \haspatch \p$ in a new commit
 is in stated
@@ -27,10 +29,11 @@ is in stated
 for the ingredients $I$)
 in the proof of Coherence for each kind of commit.
 
-$\pendsof{C}{\py}$ is computed, for all Topbloke-generated commits,
+$\pendsof{C}{\py}$ and $\pendsof{C}{\foreign}$
+are computed, for all Topbloke-generated commits,
 using the lemma Calculation of Ends, above.
-We do not annotate $\pendsof{C}{\pay{C}}$ for $C \in \pay{C}$.  Doing so would
+We do not annotate $\pendsof{C}{\set S}$ for $C \in \set S$.  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 in that case
-because $\forall_{\pay{C} \ni C} \; \pendsof{C}{\pay{C}} = \{C\}$.
+because $\forall_{\set S \ni C} \; \pendsof{C}{\set S} = \{C\}$.