\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}}
\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
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$
\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}
\patchof{L} = \pa{L} \lor \patchof{L} = \bot
}\]
\[ \eqn{ Create Acyclic }{
- L \not\haspatch \pa{Q}
+ L \not\haspatch \pq
}\]
\subsection{No Replay}
\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}
\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}
\subsection{Conditions}
\[ \eqn{ Ingredients }{
- \patchof{B} = \pan{Q}
+ \patchof{B} = \pqn
}\]
\subsection{No Replay}
\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$