\section{Create Tip}
Given a Topbloke base $B$ for a patch $\pq$,
-create a tip branch initial commit B.
+create a tip branch initial commit $C$.
\gathbegin
C \hasparents \{ B \}
\gathnext
- \patchof{B} = \pqy
+ \patchof{C} = \pqy
\gathnext
D \isin C \equiv D \isin B \lor D = C
\end{gather}
\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 \haspatch \pq$.
+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$:}
$\qed$
+\subsection{Unique Tips:}
+
+Single Parent Unique Tips applies. $\qed$
+
\subsection{Foreign Inclusion}
Simple Foreign Inclusion applies. $\qed$