chiark / gitweb /
traversal: wip prove Recreate Base Beginning OK, currently need to prove Tip Correct...
[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
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 Create Acyclic
35 $D \not\in \pqy$.  $\qed$
36
37 \subsection{Coherence and Patch Inclusion}
38
39 Consider some $D \in \py$.
40 $B \not\in \py$ so $D \neq B$.  So $D \isin B \equiv D \isin L$
41 and $D \le B \equiv D \le L$.
42
43 Thus $L \haspatch \p \equiv B \haspatch P$
44 and $L \nothaspatch \p \equiv B \nothaspatch P$.
45
46 $\qed$
47
48 \subsection{Unique Tips:}
49
50 Single Parent Unique Tips applies.  $\qed$
51
52 \subsection{Foreign Inclusion}
53
54 Simple Foreign Inclusion applies. $\qed$
55
56 \subsection{Foreign Contents}
57
58 Not applicable.
59