\section{Simple commit}

A simple single-parent forward commit $C$ as made by git-commit.
\begin{gather}
\tag*{} C \hasparents \{ L \} \\
\tag*{} \patchof{C} = \patchof{L} \\
\tag*{} D \isin C \equiv D \isin L \lor D = C
\end{gather}
This also covers Topbloke-generated commits on plain git branches:
Topbloke strips the metadata when exporting.

\subsection{No Replay}

Ingredients Prevent Replay applies.  $\qed$

\subsection{Unique Base}
If $L, C \in \py$ then by Calculation of Ends,
$\pendsof{C}{\pn} = \pendsof{L}{\pn}$ so
$\baseof{C} = \baseof{L}$. $\qed$

\subsection{Tip Contents}
We need to consider only $L, C \in \py$.  From Tip Contents for $L$:
\[ D \isin L \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L ) \]
Substitute into the contents of $C$:
\[ D \isin C \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L )
    \lor D = C \]
Since $D = C \implies D \in \py$,
and substituting in $\baseof{C}$, from Unique Base above, this gives:
\[ D \isin C \equiv D \isin \baseof{C} \lor
    (D \in \py \land D \le L) \lor
    (D = C \land D \in \py) \]
\[ \equiv D \isin \baseof{C} \lor
   [ D \in \py \land ( D \le L \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 $L, 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 L$, so by Base Acyclic for
$L$, $D \isin C \implies D \not\in \py$.

$\qed$

\subsection{Coherence and Patch Inclusion}

Need to consider $D \in \py$

\subsubsection{For $L \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 $L \haspatch \p, D \neq C$:}
Ancestors: $ D \le C \equiv D \le L $.

Contents: $ D \isin C \equiv D \isin L \lor f $
so $ D \isin C \equiv D \isin L $, i.e. $ C \zhaspatch P $.
By $\haspatch$ for $L$, $\exists_{F \in \py} F \le L$
and this $F$ is also $\le C$.  So $\haspatch$.

So:
\[ L \haspatch \p \implies C \haspatch \p \]

\subsubsection{For $L \nothaspatch \p$:}

Firstly, $C \not\in \py$ since if it were, $L \in \py$.
Thus $D \neq C$.

Now by contents of $L$, $D \notin L$, so $D \notin C$.

So:
\[ L \nothaspatch \p \implies C \nothaspatch \p \]
$\qed$

\subsection{Foreign Inclusion:}

Simple Foreign Inclusion applies.  $\qed$

\subsection{Foreign Contents:}

Only relevant if $\patchof{C} = \bot$, and in that case Totally
Foreign Contents applies. $\qed$

