\[\eqn{Foreign Inclusion:}{
\bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
}\]
+\[\eqn{Foreign Contents:}{
+ \bigforall_{C \text{ s.t. } \patchof{C} = \bot}
+ D \le C \implies \patchof{D} = \bot
+}\]
\section{Some lemmas}
}\]
xxx proof tbd
+\[ \eqn{Totally Foreign Contents:}{
+ \bigforall_{C \hasparents \set A}
+ \left[
+ \patchof{C} = \bot \land
+ \bigforall_{A \in \set A} \patchof{A} = \bot
+ \right]
+ \implies
+ \left[
+ D \isin C
+ \implies
+ \patchof{D} = \bot
+ \right]
+}\]
+xxx proof tbd
+
\subsection{No Replay for Merge Results}
If we are constructing $C$, with,
\section{Create Base}
-xxx tbd
+Given $L$, create a Topbloke base branch initial commit $B$.
+\gathbegin
+ B \hasparents \{ L \}
+\gathnext
+ \patchof{B} = \pa{B}
+\gathnext
+ D \isin B \equiv D \isin L \lor D = B
+\end{gather}
+
+\subsection{Conditions}
+
+\[ \eqn{ Ingredients }{
+ \patchof{L} = \pa{L} \lor \patchof{L} = \bot
+}\]
+\[ \eqn{ Non-recursion }{
+ L \not\in \pa{B}
+}\]
+
+\subsection{No Replay}
+
+If $\patchof{L} = \pa{L}$, trivial by Base Acyclic for $L$.
+
+If $\patchof{L} = \bot$, xxx
+
+Trivial from Base Acyclic for $L$. $\qed$
+
+\subsection{Unique Base}
+
+Not applicable. $\qed$
+
+\subsection{Tip Contents}
+
+Not applicable. $\qed$
+
+\subsection{Base Acyclic}
+
+xxx
+
+xxx unfinished
\section{Create Tip}
-xxx tbd\
+xxx tbd
\section{Anticommit}
$\qed$
-\section{Foreign Inclusion}
+\subsection{Foreign Inclusion}
Consider some $D$ s.t. $\patchof{D} = \bot$. $D \neq C$.
So by Desired Contents $D \isin C \equiv D \isin L$.