1 \section{Simple commit}
3 A simple single-parent forward commit $C$ as made by git-commit.
5 \tag*{} C \hasparents \{ L \} \\
6 \tag*{} \patchof{C} = \patchof{L} \\
7 \tag*{} D \isin C \equiv D \isin L \lor D = C
9 This also covers Topbloke-generated commits on plain git branches:
10 Topbloke strips the metadata when exporting.
12 \subsection{No Replay}
14 Ingredients Prevent Replay applies. $\qed$
16 \subsection{Unique Base}
17 If $L, C \in \py$ then by Calculation of Ends,
18 $\pendsof{C}{\pn} = \pendsof{L}{\pn}$ so
19 $\baseof{C} = \baseof{L}$. $\qed$
21 \subsection{Tip Contents}
22 We need to consider only $L, C \in \py$. From Tip Contents for $L$:
23 \[ D \isin L \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L ) \]
24 Substitute into the contents of $C$:
25 \[ D \isin C \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L )
27 Since $D = C \implies D \in \py$,
28 and substituting in $\baseof{C}$, from Unique Base above, this gives:
29 \[ D \isin C \equiv D \isin \baseof{C} \lor
30 (D \in \py \land D \le L) \lor
31 (D = C \land D \in \py) \]
32 \[ \equiv D \isin \baseof{C} \lor
33 [ D \in \py \land ( D \le L \lor D = C ) ] \]
34 So by Exact Ancestors:
35 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
39 \subsection{Base Acyclic}
41 Need to consider only $L, C \in \pn$.
43 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
45 For $D \neq C$: $D \isin C \equiv D \isin L$, so by Base Acyclic for
46 $L$, $D \isin C \implies D \not\in \py$.
50 \subsection{Coherence and patch inclusion}
52 Need to consider $D \in \py$
54 \subsubsection{For $L \haspatch P, D = C$:}
60 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
62 \subsubsection{For $L \haspatch P, D \neq C$:}
63 Ancestors: $ D \le C \equiv D \le L $.
65 Contents: $ D \isin C \equiv D \isin L \lor f $
66 so $ D \isin C \equiv D \isin L $.
69 \[ L \haspatch P \implies C \haspatch P \]
71 \subsubsection{For $L \nothaspatch P$:}
73 Firstly, $C \not\in \py$ since if it were, $L \in \py$.
76 Now by contents of $L$, $D \notin L$, so $D \notin C$.
79 \[ L \nothaspatch P \implies C \nothaspatch P \]
82 \subsection{Foreign Inclusion:}
84 Simple Foreign Inclusion applies. $\qed$
86 \subsection{Foreign Contents:}
88 Only relevant if $\patchof{C} = \bot$, and in that case Totally
89 Foreign Contents applies. $\qed$