-\[ \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 $
-}
-
-\[ \eqn{Exact Ancestors:}{
- \bigforall_{ C \hasparents \set{R} }
- D \le C \equiv
- ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
- \lor D = C
-}\]
-
-\[ \eqn{Transitive Ancestors:}{
- \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
- \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
-}\]
-
-\proof{
-The implication from right to left is trivial because
-$ \pends() \subset \pancs() $.
-For the implication from left to right:
-by the definition of $\mathcal E$,
-for every such $A$, either $A \in \pends()$ which implies
-$A \le M$ by the LHS directly,
-or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
-in which case we repeat for $A'$. Since there are finitely many
-commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
-by the LHS. And $A \le A''$.
-}
-
-\section{Commit annotation}
-
-We annotate each Topbloke commit $C$ with:
-\begin{gather}
-\tag*{} \patchof{C} \\
-\tag*{} \baseof{C}, \text{ if } C \in \py \\
-\tag*{} \bigforall_{\pa{Q}}
- \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q} \\
-\tag*{} \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
-\end{gather}
-
-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$
-would have to be updated. The annotation is not needed because
-$\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
-
-\section{Simple commit}
-
-A simple single-parent forward commit $C$ as made by git-commit.
-\begin{gather}
-\tag*{} C \hasparents \{ A \} \\
-\tag*{} \patchof{C} = \patchof{A} \\
-\tag*{} D \isin C \equiv D \isin A \lor D = C
-\end{gather}
-
-\subsection{No Replay}
-Trivial.
-
-\subsection{Unique Base}
-If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
-
-\subsection{Tip Contents}
-We need to consider only $A, C \in \py$. From Tip Contents for $A$:
-\[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
-Substitute into the contents of $C$:
-\[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
- \lor D = C \]
-Since $D = C \implies D \in \py$,
-and substituting in $\baseof{C}$, this gives:
-\[ D \isin C \equiv D \isin \baseof{C} \lor
- (D \in \py \land D \le A) \lor
- (D = C \land D \in \py) \]
-\[ \equiv D \isin \baseof{C} \lor
- [ D \in \py \land ( D \le A \lor D = C ) ] \]
-So by Exact Ancestors:
-\[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
-) \]
-$\qed$
-
-\subsection{Base Acyclic}
-
-Need to consider only $A, C \in \pn$.
-
-For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
-
-For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
-$A$, $D \isin C \implies D \not\in \py$. $\qed$
-
-\subsection{Coherence}
-
-\subsubsection{For $A \haspatch P, D = C$:}
-\[ D \isin C \equiv \ldots \lor t \text{ so } D \haspatch C \]
-\[ D \le C \]
-OK
-
-\section{Test more symbols}
-
-$ C \haspatch \p $
-
-$ C \nothaspatch \p $
-
-$ \p \patchisin C $