chiark / gitweb /
split into multiple source files
[topbloke-formulae.git] / create-tip.tex
1 \section{Create Tip}
2
3 Given a Topbloke base $B$ for a patch $\pq$,
4 create a tip branch initial commit B.
5 \gathbegin
6  C \hasparents \{ B \}
7 \gathnext
8  \patchof{B} = \pqy
9 \gathnext
10  D \isin C \equiv D \isin B \lor D = C
11 \end{gather}
12
13 \subsection{Conditions}
14
15 \[ \eqn{ Ingredients }{
16  \patchof{B} = \pqn
17 }\]
18 \[ \eqn{ No Sneak }{
19  \pendsof{B}{\pqy} = \{ \}
20 }\]
21
22 \subsection{No Replay}
23
24 Ingredients Prevent Replay applies.  $\qed$
25
26 \subsection{Unique Base}
27
28 Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$.  $\qed$
29
30 \subsection{Tip Contents}
31
32 Consider some arbitrary commit $D$.  If $D = C$, trivially satisfied.
33
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$.
37
38
39 $\qed$
40
41 \subsection{Base Acyclic}
42
43 Not applicable.
44
45 \subsection{Coherence and Patch Inclusion}
46
47 $$
48 \begin{cases}
49   \p = \pq    \lor B \haspatch \p : & C \haspatch \p \\
50   \p \neq \pq \land B \nothaspatch \p : & C \nothaspatch \p
51 \end{cases}
52 $$
53
54 \proofstarts
55 ~ Consider some $D \in \py$.
56
57 \subsubsection{For $\p = \pq$:}
58
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 \haspatch \pq$.
61
62 \subsubsection{For $\p \neq \pq$:}
63
64 $D \neq C$.  So $D \isin C \equiv D \isin B$,
65 and $D \le C \equiv D \le B$.
66
67 $\qed$
68
69 \subsection{Foreign Inclusion}
70
71 Simple Foreign Inclusion applies.  $\qed$
72
73 \subsection{Foreign Contents}
74
75 Not applicable.
76