split into multiple source files

[topbloke-formulae.git] / simple.tex

diff --git a/simple.tex b/simple.tex
new file mode 100644 (file)
index 0000000..28dc6e5
--- /dev/null
+++ b/simple.tex
@@ -0,0 +1,90 @@
+\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 $.
+
+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$
+