\documentclass[a4paper,leqno]{strayman}
\let\numberwithin=\notdef
\usepackage{amsmath}
\usepackage{mathabx}
\usepackage{txfonts}
\usepackage{amsfonts}
\usepackage{mdwlist}
%\usepackage{accents}

\renewcommand{\ge}{\geqslant}
\renewcommand{\le}{\leqslant}

\newcommand{\has}{\sqsupseteq}
\newcommand{\isin}{\sqsubseteq}

\newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
\newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
\newcommand{\haspatch}{\sqSupset}
\newcommand{\patchisin}{\sqSubset}

\newcommand{\set}[1]{\mathbb #1}
\newcommand{\pa}[1]{\varmathbb #1}
\newcommand{\pay}[1]{\pa{#1}^+}
\newcommand{\pan}[1]{\pa{#1}^-}

\newcommand{\p}{\pa{P}}
\newcommand{\py}{\pay{P}}
\newcommand{\pn}{\pan{P}}

%\newcommand{\hasparents}{\underaccent{1}{>}}
%\newcommand{\hasparents}{{%
%  \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
\newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
\newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}

\renewcommand{\implies}{\Rightarrow}
\renewcommand{\equiv}{\Leftrightarrow}
\renewcommand{\land}{\wedge}
\renewcommand{\lor}{\vee}

\newcommand{\pancs}[2]{{\mathcal A} ( #1 , #2 ) }
\newcommand{\pends}[2]{{\mathcal E} ( #1 , #2 ) }

\newcommand{\patchof}[1]{{\mathcal P} ( #1 ) }
\newcommand{\baseof}[1]{{\mathcal B} ( #1 ) }

\newcommand{\eqn}[2]{ #2 \tag*{\mbox{#1}} }

\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}

\begin{document}

\section{Notation}

\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 $

\end{document}
