pseudomerge: Bases' Children

[topbloke-formulae.git] / annotations.tex

diff --git a/annotations.tex b/annotations.tex
index 1bf2fcd5f1d504ebd7d6428d0c4490534dd64ae2..b4e86dab19b0648af7998e233209b520e0b7011c 100644 (file)
--- a/annotations.tex
+++ b/annotations.tex
@@ -4,12 +4,14 @@ We annotate each Topbloke commit $C$ with:
 \gathbegin
  \patchof{C}
 \gathnext
- \baseof{C}, \text{ if } C \in \py
+ \baseof{C}, \text{ if } C \in \pay{C}
 \gathnext
- \bigforall_{\pq}
-   \text{ either } C \haspatch \pq \text{ or } C \nothaspatch \pq
+ \bigforall_{\p}
+   \text{ either } C \haspatch \p \text{ or } C \nothaspatch \p
 \gathnext
- \bigforall_{\pqy \not\ni C} \pendsof{C}{\pqy}
+ \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
@@ -18,19 +20,20 @@ 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 \pq$ or $\nothaspatch \pq$ is represented as a
-list of $\pq$ for which it is known that $C \haspatch \pq$;
-for any $\pq$ not listed, $C \nothaspatch \pq$.
-Whether to record $C \haspatch \pq$ in a new commit
+$C \haspatch \p$ or $\nothaspatch \p$ is represented as a
+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
-(in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$
+(in terms of $I \haspatch \p$ or $I \nothaspatch \p$
 for the ingredients $I$)
 in the proof of Coherence for each kind of commit.
 
-$\pendsof{C}{\pq^+}$ 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}{\py}$ for $C \in \py$.  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_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
+because $\forall_{\set S \ni C} \; \pendsof{C}{\set S} = \{C\}$.