From b1e89d6e339d715529ba2653335d212a27e2738d Mon Sep 17 00:00:00 2001
From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Mon, 12 Mar 2012 14:13:49 +0000
Subject: [PATCH] wip create tip

---
 article.tex | 35 ++++++++++++++++++++++++++++++++++-
 1 file changed, 34 insertions(+), 1 deletion(-)

diff --git a/article.tex b/article.tex
index 50fc96c..44942ff 100644
--- a/article.tex
+++ b/article.tex
@@ -525,7 +525,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}
 
-- 
2.30.2