From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Mon, 12 Mar 2012 14:28:13 +0000 (+0000)
Subject: introduce macros \pq \pqy \pqn
X-Git-Tag: f0.2~59
X-Git-Url: https://www.chiark.greenend.org.uk/ucgi/~ian/git?a=commitdiff_plain;h=75cfdcadb6d61aaa914e4ac7196b077812b2ad48;p=topbloke-formulae.git

introduce macros \pq \pqy \pqn
---

diff --git a/article.tex b/article.tex
index c58b1ab..69f530a 100644
--- a/article.tex
+++ b/article.tex
@@ -34,6 +34,10 @@
 \newcommand{\py}{\pay{P}}
 \newcommand{\pn}{\pan{P}}
 
+\newcommand{\pq}{\pa{Q}}
+\newcommand{\pqy}{\pay{Q}}
+\newcommand{\pqn}{\pan{Q}}
+
 \newcommand{\pr}{\pa{R}}
 \newcommand{\pry}{\pay{R}}
 \newcommand{\prn}{\pan{R}}
@@ -340,10 +344,10 @@ We annotate each Topbloke commit $C$ with:
 \gathnext
  \baseof{C}, \text{ if } C \in \py
 \gathnext
- \bigforall_{\pa{Q}} 
-   \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
+ \bigforall_{\pq}
+   \text{ either } C \haspatch \pq \text{ or } C \nothaspatch \pq
 \gathnext
- \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
+ \bigforall_{\pqy \not\ni C} \pendsof{C}{\pqy}
 \end{gather}
 
 $\patchof{C}$, for each kind of Topbloke-generated commit, is stated
@@ -352,14 +356,14 @@ 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}$
+$C \haspatch \pq$ or $\nothaspatch \pq$ is represented as the
+set $\{ \pq | C \haspatch \pq \}$.  Whether $C \haspatch \pq$
 is in stated
-(in terms of $I \haspatch \pa{Q}$ or $I \nothaspatch \pa{Q}$
+(in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$
 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,
+$\pendsof{C}{\pq^+}$ 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$
@@ -464,7 +468,7 @@ Given $L$, create a Topbloke base branch initial commit $B$.
 \gathbegin
  B \hasparents \{ L \}
 \gathnext
- \patchof{B} = \pan{Q}
+ \patchof{B} = \pqn
 \gathnext
  D \isin B \equiv D \isin L \lor D = B
 \end{gather}
@@ -475,7 +479,7 @@ Given $L$, create a Topbloke base branch initial commit $B$.
  \patchof{L} = \pa{L} \lor \patchof{L} = \bot
 }\]
 \[ \eqn{ Create Acyclic }{
- L \not\haspatch \pa{Q}
+ L \not\haspatch \pq
 }\]
 
 \subsection{No Replay}
@@ -492,9 +496,9 @@ Not applicable.
 
 \subsection{Base Acyclic}
 
-Consider some $D \isin B$.  If $D = B$, $D \in \pan{Q}$.
+Consider some $D \isin B$.  If $D = B$, $D \in \pqn$.
 If $D \neq B$, $D \isin L$, and by Create Acyclic
-$D \not\in \pay{Q}$.  $\qed$
+$D \not\in \pqy$.  $\qed$
 
 \subsection{Coherence and Patch Inclusion}
 
@@ -524,7 +528,7 @@ Given a Topbloke base $B$, create a tip branch initial commit B.
 \gathbegin
  C \hasparents \{ B \}
 \gathnext
- \patchof{B} = \pay{Q}
+ \patchof{B} = \pqy
 \gathnext
  D \isin C \equiv D \isin B \lor D = C
 \end{gather}
@@ -532,7 +536,7 @@ Given a Topbloke base $B$, create a tip branch initial commit B.
 \subsection{Conditions}
 
 \[ \eqn{ Ingredients }{
- \patchof{B} = \pan{Q}
+ \patchof{B} = \pqn
 }\]
 
 \subsection{No Replay}
@@ -541,14 +545,14 @@ Ingredients Prevent Replay applies.  $\qed$
 
 \subsection{Unique Base}
 
-Trivially, $\pendsof{C}{\pan{Q}} = \{B\}$ so $\baseof{C} = B$.
+Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$.
 
 \subsection{Tip Contents}
 
 Consider some arbitrary commit $D$.  If $D = C$, trivially satisfied.
 
 If $D \neq C$, $D \isin C \equiv D \isin B$.
-By Base Acyclic of $B$, $D \isin B \implies D \not\in \pay{Q}$.
+By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$.
 So $D \isin C \equiv D \isin \baseof{B}$.
 
 $\qed$