chiark / gitweb /
merge fixes/clarifications - clarify tip contents R \not\in \py
[topbloke-formulae.git] / create-base.tex
1 \section{Create Base}
2
3 Given a starting point $L$ and a proposed patch $\pq$,
4 create a Topbloke base branch initial commit $B$.
5 \gathbegin
6  B \hasparents \{ L \}
7 \gathnext
8  \patchof{B} = \pqn
9 \gathnext
10  D \isin B \equiv D \isin L \lor D = B
11 \end{gather}
12
13 \subsection{Conditions}
14
15 \[ \eqn{ Create Acyclic }{
16  \pendsof{L}{\pqy} = \{ \}
17 }\]
18
19 \subsection{No Replay}
20
21 Ingredients Prevent Replay applies.  $\qed$
22
23 \subsection{Unique Base}
24
25 Not applicable.
26
27 \subsection{Tip Contents}
28
29 Not applicable.
30
31 \subsection{Base Acyclic}
32
33 Consider some $D \isin B$.  If $D = B$, $D \in \pqn$.
34 If $D \neq B$, $D \isin L$, so by No Replay $D \le L$
35 and by Create Acyclic
36 $D \not\in \pqy$.  $\qed$
37
38 \subsection{Coherence and Patch Inclusion}
39
40 Consider some $D \in \py$.
41 $B \not\in \py$ so $D \neq B$.  So $D \isin B \equiv D \isin L$
42 and $D \le B \equiv D \le L$.
43
44 Thus $L \haspatch \p \implies B \haspatch P$
45 and $L \nothaspatch \p \implies B \nothaspatch P$.
46
47 $\qed$.
48
49 \subsection{Foreign Inclusion}
50
51 Simple Foreign Inclusion applies. $\qed$
52
53 \subsection{Foreign Contents}
54
55 Not applicable.
56