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 Ancestry}
  60
  61 Not applicable.
  62
  63 \subsection{Bases' Children}
  64
  65 Not applicable, by Ingredients.
  66 $\qed$