-\newcommand{\true}{t}
-\newcommand{\false}{f}
-
-\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 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 these sets are distinct. Hence:
-
-\item[ $ \patchof{ C } $ ]
-Either $\p$ s.t. $ C \in \p $, or $\bot$.
-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 \haspatch \p $ ]
-$\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
-~ Informally, $C$ has the contents of $\p$.
-
-\item[ $ C \nothaspatch \p $ ]
-$\displaystyle \bigforall_{D \in \py} D \not\isin C $.
-~ Informally, $C$ has none of the contents of $\p$.
-
-Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
-patch is applied to a non-Topbloke branch and then bubbles back to
-the Topbloke patch itself, we hope that git's merge algorithm will
-DTRT or that the user will no longer care about the Topbloke patch.
-
-\item[ $\displaystyle \merge{C}{L}{M}{R} $ ]
-The contents of a git merge result:
-
-$\displaystyle D \isin C \equiv
- \begin{cases}
- (D \isin L \land D \isin R) \lor D = C : & \true \\
- (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
- \text{otherwise} : & D \not\isin M
- \end{cases}
-$
-
-\end{basedescript}
-\newpage
-\section{Invariants}
-
-We maintain these each time we construct a new commit. \\
-\[ \eqn{No Replay:}{
- C \has D \implies C \ge D
-}\]
-\[\eqn{Unique Base:}{
- \bigforall_{C \in \py} \pendsof{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 Acyclic:}{
- \bigforall_{B \in \pn} D \isin B \implies D \notin \py
-}\]
-\[\eqn{Coherence:}{
- \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
-}\]
-\[\eqn{Foreign Inclusion:}{
- \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
-}\]
-
-\section{Some lemmas}
-
-\[ \eqn{Exclusive Tip Contents:}{
- \bigforall_{C \in \py}
- \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
- \Bigr]
-}\]
-Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
-
-\proof{
-Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
-So by Base Acyclic $D \isin B \implies D \notin \py$.
-}
-\[ \corrolary{
- \bigforall_{C \in \py} D \isin C \equiv
- \begin{cases}
- D \in \py : & D \le C \\
- D \not\in \py : & D \isin \baseof{C}
- \end{cases}
-}\]
-
-\[ \eqn{Tip Self Inpatch:}{
- \bigforall_{C \in \py} C \haspatch \p
-}\]
-Ie, tip commits contain their own patch.
-
-\proof{
-Apply Exclusive Tip Contents to some $D \in \py$:
-$ \bigforall_{C \in \py}\bigforall_{D \in \py}
- D \isin C \equiv D \le C $
-}