create base fix base acyclic and condition

[topbloke-formulae.git] / article.tex

diff --git a/article.tex b/article.tex
index c3c658ce30a417fe861c3a52abd8762ba72d1142..85e09e1c470a695becbf92bfa58fcaad0dc000e8 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -475,7 +475,7 @@ Given $L$, create a Topbloke base branch initial commit $B$.
  \patchof{L} = \pa{L} \lor \patchof{L} = \bot
 }\]
 \[ \eqn{ Non-recursion }{
- L \not\in \pa{Q}
+ L \not\haspatch \pa{Q}
 }\]
 
 \subsection{No Replay}
@@ -492,12 +492,9 @@ Not applicable.
 
 \subsection{Base Acyclic}
 
-Consider some $D \isin B$.  If $D = B$, $D \in \pn$, OK.
-
-If $D \neq B$, $D \isin L$.  By No Replay of $D$ in $L$, $D \le L$.
-Thus by Foreign Contents of $L$, $\patchof{D} = \bot$.  OK.
-
-$\qed$
+Consider some $D \isin B$.  If $D = B$, $D \in \pan{Q}$.
+If $D \neq B$, $D \isin L$, and by Non-recursion
+$D \not\in \pay{Q}$.  $\qed$
 
 \subsection{Coherence and Patch Inclusion}
 
@@ -523,7 +520,40 @@ Not applicable.
 
 \section{Create Tip}
 
-xxx tbd
+Given a Topbloke base $B$, create a tip branch initial commit B.
+\gathbegin
+ C \hasparents \{ B \}
+\gathnext
+ \patchof{B} = \pay{Q}
+\gathnext
+ D \isin C \equiv D \isin B \lor D = C
+\end{gather}
+
+\subsection{Conditions}
+
+\[ \eqn{ Ingredients }{
+ \patchof{B} = \pan{Q}
+}\]
+
+\subsection{No Replay}
+
+Ingredients Prevent Replay applies.  $\qed$
+
+\subsection{Unique Base}
+
+Trivially, $\pendsof{C}{\pan{Q}} = \{B\}$ so $\baseof{C} = B$.
+
+\subsection{Tip Contents}
+
+Consider some arbitrary commit $D$.  If $D = C$, trivially satisfied.
+
+If $D \neq C$, $D \isin C \equiv D \isin B$.
+By Base Acyclic of $B$, $D \isin B \implies D \not\in \pay{Q}$.
+So $D \isin C \equiv D \isin \baseof{B}$.
+
+$\qed$
+
+xxx up to here
 
 \section{Anticommit}