From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Sun, 11 Mar 2012 15:51:52 +0000 (+0000)
Subject: annotation calculation
X-Git-Tag: f0.2~88
X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=commitdiff_plain;h=bfa0996c930a2507501eec79b4a89333d35d47aa

annotation calculation
---

diff --git a/article.tex b/article.tex
index b4f7beb..70d6d88 100644
--- a/article.tex
+++ b/article.tex
@@ -95,8 +95,6 @@
 
 \section{Notation}
 
-xxx make all conditions be in conditions, not in (or also in) intro
-
 \begin{basedescript}{
 \desclabelwidth{5em}
 \desclabelstyle{\nextlinelabel}
@@ -324,8 +322,6 @@ $\qed$
 
 \section{Commit annotation}
 
-xxx need to compute annotation for every commit type
-
 We annotate each Topbloke commit $C$ with:
 \gathbegin
  \patchof{C}
@@ -338,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}