chiark / gitweb /
pseudomerge: new Ingredients condition
[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  L \nothaspatch \pq
17 }\]
18 \[ \eqn{ Ingredients }{
19  \patchof L = \foreign \lor \patchof L = \py
20 }\]
21
22 \subsection{No Replay}
23
24 Ingredients Prevent Replay applies.  $\qed$
25
26 \subsection{Unique Base}
27
28 Not applicable.
29
30 \subsection{Tip Contents}
31
32 Not applicable.
33
34 \subsection{Base Acyclic}
35
36 Consider some $D \isin B$.  If $D = B$, $D \in \pqn$.
37 If $D \neq B$, $D \isin L$, so by Create Acyclic
38 $D \not\in \pqy$.  $\qed$
39
40 \subsection{Coherence and Patch Inclusion}
41
42 Consider some $D \in \py$.
43 $B \not\in \py$ so $D \neq B$.  So $D \isin B \equiv D \isin L$
44 and $D \le B \equiv D \le L$.
45
46 Thus $L \haspatch \p \equiv B \haspatch P$
47 and $L \nothaspatch \p \equiv B \nothaspatch P$.
48
49 $\qed$
50
51 \subsection{Unique Tips:}
52
53 Single Parent Unique Tips applies.  $\qed$
54
55 \subsection{Foreign Inclusion}
56
57 Simple Foreign Inclusion applies. $\qed$
58
59 \subsection{Foreign Contents}
60
61 Not applicable.
62
63 \subsection{Bases' Children}
64
65 Not applicable, by Ingredients.
66