-\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 in non-Topbloke-controlled branches; these are considered
-normal, forward, commits. For merges and Topbloke-generated
-anticommits, 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 these sets are distinct. Hence:
-
-\item[ $ \patchof{ C } $ ]
-Either $\p$ s.t. $ C \in \p $, or $\bot$.
-A function from commits to sets $\p$.
-
-\item[ $ \pancs{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[ $ \pends{C}{\set P} $ ]
-$ \{ E \; | \; E \in \pancs{C}{\set P}
- \land \mathop{\not\exists}_{A \in \pancs{C}{\set P}}
- A \neq E \land E \le A \} $
-i.e. all $\le$-maximal commits in $\pancs{C}{\set P}$.
-
-\item[ $ \baseof{C} $ ]
-$ \pends{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
-A partial function from commits to commits.
-See ``unique base'', below.
-
-\item[ $ C \haspatch \p $ ]
-$ \bigforall_{D \in \py} D \isin C \equiv D \le C $.
-Informally, $C$ has the contents of $\p$.
-
-\item[ $\displaystyle C \nothaspatch \p $ ]
-$\displaystyle \bigforall_{D \in \py} D \not\isin C $.
-~ Informally, $C$ has none of the contents of $\p$.
-
-\end{basedescript}
-
-\section{Invariants}
-
-\[ \eqn{No replay:}{
- C \has D \implies C \ge D
-}\]
-\[\eqn{Unique base:}{
- \bigforall_{C \in \py} \pends{C}{\pn} = \{ B \}
-}\]
-\[\eqn{Tip contents:}{
- \bigforall_{C \in \py} D \isin C \equiv
- { D \isin \baseof{C} \lor \atop
- (D \in \py \land D \le C) }
-}\]
-\[\eqn{Base non-circ:}{
- \bigforall_{B \in \pn} D \isin B \implies D \notin \py
-}\]
-
-\section{Test more symbols}
-
-$ C \haspatch \p $
-
-$ C \nothaspatch \p $
-
-$ \p \patchisin C $
-
-$ \p \notpatchisin C $
-
-$ \{ B \} \areparents C $