-\[ \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''$.
-}
-\[ \eqn{Calculation Of Ends:}{
- \bigforall_{C \hasparents \set A}
- \pendsof{C}{\set P} =
- \left\{ E \Big|
- \Bigl[ \Largeexists_{A \in \set A}
- E \in \pendsof{A}{\set P} \Bigr] \land
- \Bigl[ \Largenexists_{B \in \set A}
- E \neq B \land E \le B \Bigr]
- \right\}
-}\]
-XXX proof TBD.
-
-\subsection{No Replay for Merge Results}
-
-If we are constructing $C$, with,
-\gathbegin
- \mergeof{C}{L}{M}{R}
-\gathnext
- L \le C
-\gathnext
- R \le C
-\end{gather}
-No Replay is preserved. \proofstarts
-
-\subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
-
-\subsubsection{For $D \isin L \land D \isin R$:}
-$D \isin C$. And $D \isin L \implies D \le L \implies D \le C$. OK.
-
-\subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
-$D \not\isin C$. OK.
-
-\subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
- \land D \not\isin M$:}
-$D \isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
-R$ so $D \le C$. OK.
-
-\subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
- \land D \isin M$:}
-$D \not\isin C$. OK.
-
-$\qed$
-
-\section{Commit annotation}
-
-We annotate each Topbloke commit $C$ with:
-\gathbegin
- \patchof{C}
-\gathnext
- \baseof{C}, \text{ if } C \in \py
-\gathnext
- \bigforall_{\pa{Q}}
- \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
-\gathnext
- \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 and patch inclusion}
-
-Need to consider $D \in \py$
-
-\subsubsection{For $A \haspatch P, D = C$:}
-
-Ancestors of $C$:
-$ D \le C $.
-
-Contents of $C$:
-$ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
-
-\subsubsection{For $A \haspatch P, D \neq C$:}
-Ancestors: $ D \le C \equiv D \le A $.
-
-Contents: $ D \isin C \equiv D \isin A \lor f $
-so $ D \isin C \equiv D \isin A $.
-
-So:
-\[ A \haspatch P \implies C \haspatch P \]
-
-\subsubsection{For $A \nothaspatch P$:}
-
-Firstly, $C \not\in \py$ since if it were, $A \in \py$.
-Thus $D \neq C$.
-
-Now by contents of $A$, $D \notin A$, so $D \notin C$.
-
-So:
-\[ A \nothaspatch P \implies C \nothaspatch P \]
-$\qed$
-
-\subsection{Foreign inclusion:}
-
-If $D = C$, trivial. For $D \neq C$:
-$D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
-
-\section{Anticommit}
-
-Given $L, R^+, R^-$ where
-$R^+ \in \pry, R^- = \baseof{R^+}$.
-Construct $C$ which has $\pr$ removed.
-Used for removing a branch dependency.
-\gathbegin
- C \hasparents \{ L \}
-\gathnext
- \patchof{C} = \patchof{L}
-\gathnext
- \mergeof{C}{L}{R^+}{R^-}
-\end{gather}
-
-\subsection{Conditions}