\section{Create Tip}

Given a Topbloke base $B$ for a patch $\pq$,
create a tip branch initial commit $C$.
\gathbegin
 C \hasparents \{ B \}
\gathnext
 \patchof{C} = \pqy
\gathnext
 D \isin C \equiv D \isin B \lor D = C
\end{gather}

\subsection{Conditions}

\[ \eqn{ Ingredients }{
 \patchof{B} = \pqn
}\]
\[ \eqn{ No Sneak }{
 \pendsof{B}{\pqy} = \{ \}
}\]

\subsection{No Replay}

Ingredients Prevent Replay applies.  $\qed$

\subsection{Unique Base}

Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$.  $\qed$

\subsection{Tip Contents}

Consider some arbitrary commit $D$.  If $D = C$, trivially satisfied.

If $D \neq C$, $D \isin C \equiv D \isin B$,
which by Unique Base, above, $ \equiv D \isin \baseof{B}$.
By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$.


$\qed$

\subsection{Base Acyclic}

Not applicable.

\subsection{Coherence and Patch Inclusion}

$$
\begin{cases}
  \p = \pq    \lor B \haspatch \p : & C \haspatch \p \\
  \p \neq \pq \land B \nothaspatch \p : & C \nothaspatch \p
\end{cases}
$$

\proofstarts
~ Consider some $D \in \py$.

\subsubsection{For $\p = \pq$:}

By Base Acyclic, $D \not\isin B$.  So $D \isin C \equiv D = C$.
By No Sneak, $D \not\le B$ so $D \le C \equiv D = C$.  Thus $C \zhaspatch \pq$.
And we can set $F = C$ giving $F \in \pqy \land F \le C$ so $C
\haspatch \pq$.

\subsubsection{For $\p \neq \pq$:}

$D \neq C$.  So $D \isin C \equiv D \isin B$,
and $D \le C \equiv D \le B$.

$\qed$

\subsection{Foreign Inclusion}

Simple Foreign Inclusion applies.  $\qed$

\subsection{Foreign Contents}

Not applicable.

