3 Given a Topbloke base $B$ for a patch $\pq$,
4 create a tip branch initial commit $C$.
10 D \isin C \equiv D \isin B \lor D = C
13 \subsection{Conditions}
15 \[ \eqn{ Ingredients }{
19 \pendsof{B}{\pqy} = \{ \}
22 \subsection{No Replay}
24 Ingredients Prevent Replay applies. $\qed$
26 \subsection{Unique Base}
28 Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$. $\qed$
30 \subsection{Tip Contents}
32 Consider some arbitrary commit $D$. If $D = C$, trivially satisfied.
34 If $D \neq C$, $D \isin C \equiv D \isin B$,
35 which by Unique Base, above, $ \equiv D \isin \baseof{B}$.
36 By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$.
41 \subsection{Base Acyclic}
45 \subsection{Coherence and Patch Inclusion}
49 \p = \pq \lor B \haspatch \p : & C \haspatch \p \\
50 \p \neq \pq \land B \nothaspatch \p : & C \nothaspatch \p
55 ~ Consider some $D \in \py$.
57 \subsubsection{For $\p = \pq$:}
59 By Base Acyclic, $D \not\isin B$. So $D \isin C \equiv D = C$.
60 By No Sneak, $D \not\le B$ so $D \le C \equiv D = C$. Thus $C \zhaspatch \pq$.
61 And we can set $F = C$ giving $F \in \pqy \land F \le C$ so $C
64 \subsubsection{For $\p \neq \pq$:}
66 $D \neq C$. So $D \isin C \equiv D \isin B$,
67 and $D \le C \equiv D \le B$.
71 \subsection{Unique Tips:}
73 Single Parent Unique Tips applies. $\qed$
75 \subsection{Foreign Inclusion}
77 Simple Foreign Inclusion applies. $\qed$
79 \subsection{Foreign Ancestry}
83 \subsection{Bases' Children}
85 Trivial, by Ingredients.