\stdsection{Notation}
Throughout, any free variables are implicitly universally quantified
at the outermost level.
\begin{basedescript}{
\desclabelwidth{5em}
\desclabelstyle{\nextlinelabel}
}
\item[ $ C \hasparents \set X $ ]
The parents of commit $C$ are exactly the set
$\set X$.
\item[ $ C \ge D $ ]
$C$ is a descendant of $D$ in the git commit
graph. This is a partial order, namely the transitive closure of
$ D \in \set X $ where $ C \hasparents \set X $.
\item[ $ C \has D $ ]
Informally, the tree at commit $C$ contains the change
made in commit $D$. Does not take account of deliberate reversions by
the user or reversion, rebasing or rewinding in
non-Topbloke-controlled branches. For merges and Topbloke-generated
anticommits or re-commits, the ``change made'' is only to be thought
of as any conflict resolution. This is not a partial order because it
is not transitive.
\item[ $ \p, \py, \pn $ ]
A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
are respectively the base and tip git branches. $\p$ may be used
where the context requires a set, in which case the statement
is to be taken as applying to both $\py$ and $\pn$.
All of these sets will be disjoint by construction
(see Invariants, below). Hence:
\item[ $\foreign$ ]
The set of all commits which are not part of a Topbloke branch. We
call these foreign commits.
\item[ $\set A$, $\set P$, $\ldots$ ]
Arbitrary sets of commits. Maybe $\set P = \p$ i.e.\ some $\py$ or $\pn$, but
maybe not.
\item[ $ \patchof{ C } $ ]
Either $\p$ s.t. $ C \in \p $, or $\foreign$.
A function from commits to patches' sets $\p$.
\item[ $ \pancsof{C}{\set P} $ ]
$ \{ A \; | \; A \le C \land A \in \set P \} $
i.e. all the ancestors of $C$
which are in $\set P$.
\item[ $ \pendsof{C}{\set P} $ ]
$ \{ E \; | \; E \in \pancsof{C}{\set P}
\land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
E \neq A \land E \le A \} $
i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
\item[ $ \baseof{C} $ ]
$ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
A partial function from commits to commits.
See Unique Base, below.
\item[ $ C \nothaspatch \p $ ]
$\displaystyle \bigforall_{D \in \py} D \not\isin C $.
~ Informally, $C$ has none of the contents of $\p$.
\item[ $ C \zhaspatch \p $ ]
$\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
~ Informally, $C$ has all the reachable contents of $\p$.
\item[ $ C \haspatch \p $ ]
$\displaystyle C \zhaspatch \p \land \exists_{F \in \py} F \le C $.
~ Informally, $C$ nontrivially has all the reachable contents of $\p$.
Note that $\zhaspatch$ and $\nothaspatch$ are neither
mutually exclusive nor exhaustive.
$\haspatch$ and $\nothaspatch$ are mutually exclusive but not
necessarily exhaustive.
Commits on Non-Topbloke branches are $\nothaspatch \p$ for all $\p$. This
includes commits on plain git branches made by applying a Topbloke
patch. If a Topbloke
patch is applied to a non-Topbloke branch and then bubbles back to
the relevant Topbloke branches, we hope that
if the user still cares about the Topbloke patch,
git's merge algorithm will DTRT when trying to re-apply the changes.
\item[ $\displaystyle \stmtmergeof{L}{M}{R} $ ]
The proper results of a merge. Formally,
where $L$, $M$ and $R$ are statements:
$$
\stmtmergeof{L}{M}{R}
\equiv
\begin{cases}
(L \land R) : & \true \\
(\neg L \land \neg R) : & \false \\
\text{otherwise} : & \neg M
\end{cases}
$$
May also be used where $L$, $M$ and $R$ are sets, in which case
$$
\setmergeof{L}{M}{R}
=
\left\{
\;
D \; \middle| \;
\setmergeof{ D \in L }{ D \in M }{ D \in R }
\;
\right\}
$$
\item[ $\displaystyle \commitmergeof{C}{L}{M}{R} $ ]
$C$ has exactly the contents of a git merge result:
$\displaystyle D \isin C \equiv
\begin{cases}
D = C : & \true \\
D \neq C : & \stmtmergeof{ D \isin L }{ D \isin M }{ D \isin R }
\end{cases}
$
We will refer to this as \commitmergename.
\end{basedescript}