1 \documentclass[a4paper,leqno]{strayman}
3 \let\numberwithin=\notdef
11 \renewcommand{\ge}{\geqslant}
12 \renewcommand{\le}{\leqslant}
13 \newcommand{\nge}{\ngeqslant}
14 \newcommand{\nle}{\nleqslant}
16 \newcommand{\has}{\sqsupseteq}
17 \newcommand{\isin}{\sqsubseteq}
19 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
20 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
21 \newcommand{\haspatch}{\sqSupset}
22 \newcommand{\patchisin}{\sqSubset}
24 \newif\ifhidehack\hidehackfalse
25 \DeclareRobustCommand\hidefromedef[2]{%
26 \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
27 \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
29 \newcommand{\set}[1]{\mathbb{#1}}
30 \newcommand{\pay}[1]{\pa{#1}^+}
31 \newcommand{\pan}[1]{\pa{#1}^-}
33 \newcommand{\p}{\pa{P}}
34 \newcommand{\py}{\pay{P}}
35 \newcommand{\pn}{\pan{P}}
37 \newcommand{\pr}{\pa{R}}
38 \newcommand{\pry}{\pay{R}}
39 \newcommand{\prn}{\pan{R}}
41 %\newcommand{\hasparents}{\underaccent{1}{>}}
42 %\newcommand{\hasparents}{{%
43 % \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
44 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
45 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
47 \renewcommand{\implies}{\Rightarrow}
48 \renewcommand{\equiv}{\Leftrightarrow}
49 \renewcommand{\nequiv}{\nLeftrightarrow}
50 \renewcommand{\land}{\wedge}
51 \renewcommand{\lor}{\vee}
53 \newcommand{\pancs}{{\mathcal A}}
54 \newcommand{\pends}{{\mathcal E}}
56 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
57 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
59 \newcommand{\merge}{{\mathcal M}}
60 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
61 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
63 \newcommand{\patch}{{\mathcal P}}
64 \newcommand{\base}{{\mathcal B}}
66 \newcommand{\patchof}[1]{\patch ( #1 ) }
67 \newcommand{\baseof}[1]{\base ( #1 ) }
69 \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
70 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
72 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
73 \newcommand{\bigforall}{%
75 {\hbox{\huge$\forall$}}%
76 {\hbox{\Large$\forall$}}%
77 {\hbox{\normalsize$\forall$}}%
78 {\hbox{\scriptsize$\forall$}}}%
81 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
82 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
84 \newcommand{\qed}{\square}
85 \newcommand{\proofstarts}{{\it Proof:}}
86 \newcommand{\proof}[1]{\proofstarts #1 $\qed$}
88 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
89 \newcommand{\gathnext}{\\ \tag*{}}
92 \newcommand{\false}{f}
98 xxx make all conditions be in conditions, not in (or also in) intro
100 \begin{basedescript}{
102 \desclabelstyle{\nextlinelabel}
104 \item[ $ C \hasparents \set X $ ]
105 The parents of commit $C$ are exactly the set
109 $C$ is a descendant of $D$ in the git commit
110 graph. This is a partial order, namely the transitive closure of
111 $ D \in \set X $ where $ C \hasparents \set X $.
113 \item[ $ C \has D $ ]
114 Informally, the tree at commit $C$ contains the change
115 made in commit $D$. Does not take account of deliberate reversions by
116 the user or reversion, rebasing or rewinding in
117 non-Topbloke-controlled branches. For merges and Topbloke-generated
118 anticommits or re-commits, the ``change made'' is only to be thought
119 of as any conflict resolution. This is not a partial order because it
122 \item[ $ \p, \py, \pn $ ]
123 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
124 are respectively the base and tip git branches. $\p$ may be used
125 where the context requires a set, in which case the statement
126 is to be taken as applying to both $\py$ and $\pn$.
127 None of these sets overlap. Hence:
129 \item[ $ \patchof{ C } $ ]
130 Either $\p$ s.t. $ C \in \p $, or $\bot$.
131 A function from commits to patches' sets $\p$.
133 \item[ $ \pancsof{C}{\set P} $ ]
134 $ \{ A \; | \; A \le C \land A \in \set P \} $
135 i.e. all the ancestors of $C$
136 which are in $\set P$.
138 \item[ $ \pendsof{C}{\set P} $ ]
139 $ \{ E \; | \; E \in \pancsof{C}{\set P}
140 \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
141 E \neq A \land E \le A \} $
142 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
144 \item[ $ \baseof{C} $ ]
145 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
146 A partial function from commits to commits.
147 See Unique Base, below.
149 \item[ $ C \haspatch \p $ ]
150 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
151 ~ Informally, $C$ has the contents of $\p$.
153 \item[ $ C \nothaspatch \p $ ]
154 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
155 ~ Informally, $C$ has none of the contents of $\p$.
157 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$. This
158 includes commits on plain git branches made by applying a Topbloke
160 patch is applied to a non-Topbloke branch and then bubbles back to
161 the relevant Topbloke branches, we hope that
162 if the user still cares about the Topbloke patch,
163 git's merge algorithm will DTRT when trying to re-apply the changes.
165 \item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
166 The contents of a git merge result:
168 $\displaystyle D \isin C \equiv
170 (D \isin L \land D \isin R) \lor D = C : & \true \\
171 (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
172 \text{otherwise} : & D \not\isin M
180 We maintain these each time we construct a new commit. \\
182 C \has D \implies C \ge D
184 \[\eqn{Unique Base:}{
185 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
187 \[\eqn{Tip Contents:}{
188 \bigforall_{C \in \py} D \isin C \equiv
189 { D \isin \baseof{C} \lor \atop
190 (D \in \py \land D \le C) }
192 \[\eqn{Base Acyclic:}{
193 \bigforall_{B \in \pn} D \isin B \implies D \notin \py
196 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
198 \[\eqn{Foreign Inclusion:}{
199 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
202 \section{Some lemmas}
204 \[ \eqn{Alternative (overlapping) formulations defining
205 $\mergeof{C}{L}{M}{R}$:}{
208 D \isin L \equiv D \isin R : & D = C \lor D \isin L \\
209 D \isin L \nequiv D \isin R : & D = C \lor D \not\isin M \\
210 D \isin L \equiv D \isin M : & D = C \lor D \isin R \\
211 D \isin L \nequiv D \isin M : & D = C \lor D \isin L \\
212 \text{as above with L and R exchanged}
218 Original definition is symmetrical in $L$ and $R$.
221 \[ \eqn{Exclusive Tip Contents:}{
222 \bigforall_{C \in \py}
223 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
226 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
229 Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
230 So by Base Acyclic $D \isin B \implies D \notin \py$.
232 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
233 \bigforall_{C \in \py} D \isin C \equiv
235 D \in \py : & D \le C \\
236 D \not\in \py : & D \isin \baseof{C}
240 \[ \eqn{Tip Self Inpatch:}{
241 \bigforall_{C \in \py} C \haspatch \p
243 Ie, tip commits contain their own patch.
246 Apply Exclusive Tip Contents to some $D \in \py$:
247 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
248 D \isin C \equiv D \le C $
251 \[ \eqn{Exact Ancestors:}{
252 \bigforall_{ C \hasparents \set{R} }
254 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
259 \[ \eqn{Transitive Ancestors:}{
260 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
261 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
265 The implication from right to left is trivial because
266 $ \pends() \subset \pancs() $.
267 For the implication from left to right:
268 by the definition of $\mathcal E$,
269 for every such $A$, either $A \in \pends()$ which implies
270 $A \le M$ by the LHS directly,
271 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
272 in which case we repeat for $A'$. Since there are finitely many
273 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
274 by the LHS. And $A \le A''$.
277 \[ \eqn{Calculation Of Ends:}{
278 \bigforall_{C \hasparents \set A}
279 \pendsof{C}{\set P} =
283 C \not\in \p : & \displaystyle
285 \Bigl[ \Largeexists_{A \in \set A}
286 E \in \pendsof{A}{\set P} \Bigr] \land
287 \Bigl[ \Largenexists_{B \in \set A}
288 E \neq B \land E \le B \Bigr]
294 \subsection{No Replay for Merge Results}
296 If we are constructing $C$, with,
304 No Replay is preserved. \proofstarts
306 \subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
308 \subsubsection{For $D \isin L \land D \isin R$:}
309 $D \isin C$. And $D \isin L \implies D \le L \implies D \le C$. OK.
311 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
314 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
315 \land D \not\isin M$:}
316 $D \isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
319 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
325 \section{Commit annotation}
327 xxx need to compute annotation for every commit type
329 We annotate each Topbloke commit $C$ with:
333 \baseof{C}, \text{ if } C \in \py
336 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
338 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
341 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
342 make it wrong to make plain commits with git because the recorded $\pends$
343 would have to be updated. The annotation is not needed because
344 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
346 \section{Simple commit}
348 A simple single-parent forward commit $C$ as made by git-commit.
350 \tag*{} C \hasparents \{ A \} \\
351 \tag*{} \patchof{C} = \patchof{A} \\
352 \tag*{} D \isin C \equiv D \isin A \lor D = C
354 This also covers Topbloke-generated commits on plain git branches:
355 Topbloke strips the metadata when exporting.
357 \subsection{No Replay}
360 \subsection{Unique Base}
361 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
363 \subsection{Tip Contents}
364 We need to consider only $A, C \in \py$. From Tip Contents for $A$:
365 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
366 Substitute into the contents of $C$:
367 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
369 Since $D = C \implies D \in \py$,
370 and substituting in $\baseof{C}$, this gives:
371 \[ D \isin C \equiv D \isin \baseof{C} \lor
372 (D \in \py \land D \le A) \lor
373 (D = C \land D \in \py) \]
374 \[ \equiv D \isin \baseof{C} \lor
375 [ D \in \py \land ( D \le A \lor D = C ) ] \]
376 So by Exact Ancestors:
377 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
381 \subsection{Base Acyclic}
383 Need to consider only $A, C \in \pn$.
385 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
387 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
388 $A$, $D \isin C \implies D \not\in \py$. $\qed$
390 \subsection{Coherence and patch inclusion}
392 Need to consider $D \in \py$
394 \subsubsection{For $A \haspatch P, D = C$:}
400 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
402 \subsubsection{For $A \haspatch P, D \neq C$:}
403 Ancestors: $ D \le C \equiv D \le A $.
405 Contents: $ D \isin C \equiv D \isin A \lor f $
406 so $ D \isin C \equiv D \isin A $.
409 \[ A \haspatch P \implies C \haspatch P \]
411 \subsubsection{For $A \nothaspatch P$:}
413 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
416 Now by contents of $A$, $D \notin A$, so $D \notin C$.
419 \[ A \nothaspatch P \implies C \nothaspatch P \]
422 \subsection{Foreign inclusion:}
424 If $D = C$, trivial. For $D \neq C$:
425 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
429 Given $L, R^+, R^-$ where
430 $R^+ \in \pry, R^- = \baseof{R^+}$.
431 Construct $C$ which has $\pr$ removed.
432 Used for removing a branch dependency.
434 C \hasparents \{ L \}
436 \patchof{C} = \patchof{L}
438 \mergeof{C}{L}{R^+}{R^-}
441 \subsection{Conditions}
443 \[ \eqn{ Into Base }{
446 \[ \eqn{ Unique Tip }{
447 \pendsof{L}{\pry} = \{ R^+ \}
449 \[ \eqn{ Currently Included }{
453 \subsection{Ordering of ${L, R^+, R^-}$:}
455 By Unique Tip, $R^+ \le L$. By definition of $\base$, $R^- \le R^+$
456 so $R^- \le L$. So $R^+ \le C$ and $R^- \le C$.
458 (Note that the merge base $R^+ \not\le R^-$, i.e. the merge base is
459 later than one of the branches to be merged.)
461 \subsection{No Replay}
463 No Replay for Merge Results applies. $\qed$
465 \subsection{Desired Contents}
467 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
470 \subsubsection{For $D = C$:}
472 Trivially $D \isin C$. OK.
474 \subsubsection{For $D \neq C, D \not\le L$:}
476 By No Replay $D \not\isin L$. Also $D \not\le R^-$ hence
477 $D \not\isin R^-$. Thus $D \not\isin C$. OK.
479 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
481 By Currently Included, $D \isin L$.
483 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
484 by Unique Tip, $D \le R^+ \equiv D \le L$.
487 By Base Acyclic, $D \not\isin R^-$.
489 Apply $\merge$: $D \not\isin C$. OK.
491 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
493 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
495 Apply $\merge$: $D \isin C \equiv D \isin L$. OK.
499 \subsection{Unique Base}
501 Into Base means that $C \in \pn$, so Unique Base is not
504 \subsection{Tip Contents}
506 Again, not applicable. $\qed$
508 \subsection{Base Acyclic}
510 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
511 And by Into Base $C \not\in \py$.
512 Now from Desired Contents, above, $D \isin C
513 \implies D \isin L \lor D = C$, which thus
514 $\implies D \not\in \py$. $\qed$.
516 \subsection{Coherence and Patch Inclusion}
518 Need to consider some $D \in \py$. By Into Base, $D \neq C$.
520 \subsubsection{For $\p = \pr$:}
521 By Desired Contents, above, $D \not\isin C$.
522 So $C \nothaspatch \pr$.
524 \subsubsection{For $\p \neq \pr$:}
525 By Desired Contents, $D \isin C \equiv D \isin L$
526 (since $D \in \py$ so $D \not\in \pry$).
528 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
529 So $L \nothaspatch \p \implies C \nothaspatch \p$.
531 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
532 so $L \haspatch \p \implies C \haspatch \p$.
534 \section{Foreign Inclusion}
536 Consider some $D$ s.t. $\patchof{D} = \bot$. $D \neq C$.
537 So by Desired Contents $D \isin C \equiv D \isin L$.
538 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
540 And $D \le C \equiv D \le L$.
541 Thus $D \isin C \equiv D \le C$. $\qed$
545 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
547 C \hasparents \{ L, R \}
549 \patchof{C} = \patchof{L}
553 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
555 \subsection{Conditions}
557 \[ \eqn{ Tip Merge }{
560 R \in \py : & \baseof{R} \ge \baseof{L}
561 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
562 R \in \pn : & M = \baseof{L} \\
563 \text{otherwise} : & \false
566 \[ \eqn{ Merge Acyclic }{
571 \[ \eqn{ Removal Merge Ends }{
572 X \not\haspatch \p \land
576 \pendsof{Y}{\py} = \pendsof{M}{\py}
578 \[ \eqn{ Addition Merge Ends }{
579 X \not\haspatch \p \land
583 \bigforall_{E \in \pendsof{X}{\py}} E \le Y
587 \subsection{Non-Topbloke merges}
589 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$.
590 I.e. not only is it forbidden to merge into a Topbloke-controlled
591 branch without Topbloke's assistance, it is also forbidden to
592 merge any Topbloke-controlled branch into any plain git branch.
594 Given those conditions, Tip Merge and Merge Acyclic do not apply.
595 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
596 Merge Ends condition applies. Good.
598 \subsection{No Replay}
600 No Replay for Merge Results applies. $\qed$
602 \subsection{Unique Base}
604 Need to consider only $C \in \py$, ie $L \in \py$,
605 and calculate $\pendsof{C}{\pn}$. So we will consider some
606 putative ancestor $A \in \pn$ and see whether $A \le C$.
608 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
609 But $C \in py$ and $A \in \pn$ so $A \neq C$.
610 Thus $A \le C \equiv A \le L \lor A \le R$.
612 By Unique Base of L and Transitive Ancestors,
613 $A \le L \equiv A \le \baseof{L}$.
615 \subsubsection{For $R \in \py$:}
617 By Unique Base of $R$ and Transitive Ancestors,
618 $A \le R \equiv A \le \baseof{R}$.
620 But by Tip Merge condition on $\baseof{R}$,
621 $A \le \baseof{L} \implies A \le \baseof{R}$, so
622 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
623 Thus $A \le C \equiv A \le \baseof{R}$.
624 That is, $\baseof{C} = \baseof{R}$.
626 \subsubsection{For $R \in \pn$:}
628 By Tip Merge condition on $R$ and since $M \le R$,
629 $A \le \baseof{L} \implies A \le R$, so
630 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
631 Thus $A \le C \equiv A \le R$.
632 That is, $\baseof{C} = R$.
636 \subsection{Coherence and Patch Inclusion}
638 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
639 This involves considering $D \in \py$.
641 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
642 $D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
643 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch). So $D \neq C$.
644 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
646 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
647 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
648 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
650 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
652 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
653 \equiv D \isin L \lor D \isin R$.
654 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
656 Consider $D \neq C, D \isin X \land D \isin Y$:
657 By $\merge$, $D \isin C$. Also $D \le X$
658 so $D \le C$. OK for $C \haspatch \p$.
660 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
661 By $\merge$, $D \not\isin C$.
662 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
663 OK for $C \haspatch \p$.
665 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
666 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
667 Thus by $\merge$, $D \isin C$. And $D \le Y$ so $D \le C$.
668 OK for $C \haspatch \p$.
670 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
672 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
674 $M \haspatch \p \implies C \nothaspatch \p$.
675 $M \nothaspatch \p \implies C \haspatch \p$.
679 One of the Merge Ends conditions applies.
680 Recall that we are considering $D \in \py$.
681 $D \isin Y \equiv D \le Y$. $D \not\isin X$.
682 We will show for each of
683 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
684 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
686 Consider $D = C$: Thus $C \in \py, L \in \py$, and by Tip
687 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$. By Tip Merge,
688 $M=\baseof{L}$. So by Base Acyclic $D \not\isin M$, i.e.
689 $M \nothaspatch \p$. And indeed $D \isin C$ and $D \le C$. OK.
691 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
692 $D \le Y$ so $D \le C$.
693 $D \not\isin M$ so by $\merge$, $D \isin C$. OK.
695 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
696 $D \not\le Y$. If $D \le X$ then
697 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
698 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
699 Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK.
701 Consider $D \neq C, M \haspatch P, D \isin Y$:
702 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
703 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
704 Thus $D \isin M$. By $\merge$, $D \not\isin C$. OK.
706 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
707 By $\merge$, $D \not\isin C$. OK.
711 \subsection{Base Acyclic}
713 This applies when $C \in \pn$.
714 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
716 Consider some $D \in \py$.
718 By Base Acyclic of $L$, $D \not\isin L$. By the above, $D \not\isin
719 R$. And $D \neq C$. So $D \not\isin C$. $\qed$
721 \subsection{Tip Contents}
723 We need worry only about $C \in \py$.
724 And $\patchof{C} = \patchof{L}$
725 so $L \in \py$ so $L \haspatch \p$. We will use the Unique Base
726 of $C$, and its Coherence and Patch Inclusion, as just proved.
728 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
729 \p$ and by Coherence/Inclusion $C \haspatch \p$ . If $R \not\in \py$
730 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
731 of $\nothaspatch$, $M \nothaspatch \p$. So by Coherence/Inclusion $C
732 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
734 We will consider an arbitrary commit $D$
735 and prove the Exclusive Tip Contents form.
737 \subsubsection{For $D \in \py$:}
738 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
741 \subsubsection{For $D \not\in \py, R \not\in \py$:}
743 $D \neq C$. By Tip Contents of $L$,
744 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
745 $D \isin L \equiv D \isin M$. So by definition of $\merge$, $D \isin
746 C \equiv D \isin R$. And $R = \baseof{C}$ by Unique Base of $C$.
747 Thus $D \isin C \equiv D \isin \baseof{C}$. OK.
749 \subsubsection{For $D \not\in \py, R \in \py$:}
754 $D \isin L \equiv D \isin \baseof{L}$ and
755 $D \isin R \equiv D \isin \baseof{R}$.
757 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
758 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
759 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
760 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
762 So $D \isin M \equiv D \isin L$ and by $\merge$,
763 $D \isin C \equiv D \isin R$. But from Unique Base,
764 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$. OK.
768 \subsection{Foreign Inclusion}
770 Consider some $D$ s.t. $\patchof{D} = \bot$.
771 By Foreign Inclusion of $L, M, R$:
772 $D \isin L \equiv D \le L$;
773 $D \isin M \equiv D \le M$;
774 $D \isin R \equiv D \le R$.
776 \subsubsection{For $D = C$:}
778 $D \isin C$ and $D \le C$. OK.
780 \subsubsection{For $D \neq C, D \isin M$:}
782 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
783 R$. So by $\merge$, $D \isin C$. And $D \le C$. OK.
785 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
787 By $\merge$, $D \isin C$.
788 And $D \isin X$ means $D \le X$ so $D \le C$.
791 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
793 By $\merge$, $D \not\isin C$.
794 And $D \not\le L, D \not\le R$ so $D \not\le C$.