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}
100 \desclabelstyle{\nextlinelabel}
102 \item[ $ C \hasparents \set X $ ]
103 The parents of commit $C$ are exactly the set
107 $C$ is a descendant of $D$ in the git commit
108 graph. This is a partial order, namely the transitive closure of
109 $ D \in \set X $ where $ C \hasparents \set X $.
111 \item[ $ C \has D $ ]
112 Informally, the tree at commit $C$ contains the change
113 made in commit $D$. Does not take account of deliberate reversions by
114 the user or reversion, rebasing or rewinding in
115 non-Topbloke-controlled branches. For merges and Topbloke-generated
116 anticommits or re-commits, the ``change made'' is only to be thought
117 of as any conflict resolution. This is not a partial order because it
120 \item[ $ \p, \py, \pn $ ]
121 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
122 are respectively the base and tip git branches. $\p$ may be used
123 where the context requires a set, in which case the statement
124 is to be taken as applying to both $\py$ and $\pn$.
125 None of these sets overlap. Hence:
127 \item[ $ \patchof{ C } $ ]
128 Either $\p$ s.t. $ C \in \p $, or $\bot$.
129 A function from commits to patches' sets $\p$.
131 \item[ $ \pancsof{C}{\set P} $ ]
132 $ \{ A \; | \; A \le C \land A \in \set P \} $
133 i.e. all the ancestors of $C$
134 which are in $\set P$.
136 \item[ $ \pendsof{C}{\set P} $ ]
137 $ \{ E \; | \; E \in \pancsof{C}{\set P}
138 \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
139 E \neq A \land E \le A \} $
140 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
142 \item[ $ \baseof{C} $ ]
143 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
144 A partial function from commits to commits.
145 See Unique Base, below.
147 \item[ $ C \haspatch \p $ ]
148 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
149 ~ Informally, $C$ has the contents of $\p$.
151 \item[ $ C \nothaspatch \p $ ]
152 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
153 ~ Informally, $C$ has none of the contents of $\p$.
155 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$. This
156 includes commits on plain git branches made by applying a Topbloke
158 patch is applied to a non-Topbloke branch and then bubbles back to
159 the relevant Topbloke branches, we hope that
160 if the user still cares about the Topbloke patch,
161 git's merge algorithm will DTRT when trying to re-apply the changes.
163 \item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
164 The contents of a git merge result:
166 $\displaystyle D \isin C \equiv
168 (D \isin L \land D \isin R) \lor D = C : & \true \\
169 (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
170 \text{otherwise} : & D \not\isin M
178 We maintain these each time we construct a new commit. \\
180 C \has D \implies C \ge D
182 \[\eqn{Unique Base:}{
183 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
185 \[\eqn{Tip Contents:}{
186 \bigforall_{C \in \py} D \isin C \equiv
187 { D \isin \baseof{C} \lor \atop
188 (D \in \py \land D \le C) }
190 \[\eqn{Base Acyclic:}{
191 \bigforall_{B \in \pn} D \isin B \implies D \notin \py
194 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
196 \[\eqn{Foreign Inclusion:}{
197 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
200 \section{Some lemmas}
202 \[ \eqn{Alternative (overlapping) formulations defining
203 $\mergeof{C}{L}{M}{R}$:}{
206 D \isin L \equiv D \isin R : & D = C \lor D \isin L \\
207 D \isin L \nequiv D \isin R : & D = C \lor D \not\isin M \\
208 D \isin L \equiv D \isin M : & D = C \lor D \isin R \\
209 D \isin L \nequiv D \isin M : & D = C \lor D \isin L \\
210 \text{as above with L and R exchanged}
216 Original definition is symmetrical in $L$ and $R$.
219 \[ \eqn{Exclusive Tip Contents:}{
220 \bigforall_{C \in \py}
221 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
224 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
227 Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
228 So by Base Acyclic $D \isin B \implies D \notin \py$.
230 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
231 \bigforall_{C \in \py} D \isin C \equiv
233 D \in \py : & D \le C \\
234 D \not\in \py : & D \isin \baseof{C}
238 \[ \eqn{Tip Self Inpatch:}{
239 \bigforall_{C \in \py} C \haspatch \p
241 Ie, tip commits contain their own patch.
244 Apply Exclusive Tip Contents to some $D \in \py$:
245 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
246 D \isin C \equiv D \le C $
249 \[ \eqn{Exact Ancestors:}{
250 \bigforall_{ C \hasparents \set{R} }
252 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
256 \[ \eqn{Transitive Ancestors:}{
257 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
258 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
262 The implication from right to left is trivial because
263 $ \pends() \subset \pancs() $.
264 For the implication from left to right:
265 by the definition of $\mathcal E$,
266 for every such $A$, either $A \in \pends()$ which implies
267 $A \le M$ by the LHS directly,
268 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
269 in which case we repeat for $A'$. Since there are finitely many
270 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
271 by the LHS. And $A \le A''$.
273 \[ \eqn{Calculation Of Ends:}{
274 \bigforall_{C \hasparents \set A}
275 \pendsof{C}{\set P} =
277 \Bigl[ \Largeexists_{A \in \set A}
278 E \in \pendsof{A}{\set P} \Bigr] \land
279 \Bigl[ \Largenexists_{B \in \set A}
280 E \neq B \land E \le B \Bigr]
285 \subsection{No Replay for Merge Results}
287 If we are constructing $C$, with,
295 No Replay is preserved. \proofstarts
297 \subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
299 \subsubsection{For $D \isin L \land D \isin R$:}
300 $D \isin C$. And $D \isin L \implies D \le L \implies D \le C$. OK.
302 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
305 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
306 \land D \not\isin M$:}
307 $D \isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
310 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
316 \section{Commit annotation}
318 We annotate each Topbloke commit $C$ with:
322 \baseof{C}, \text{ if } C \in \py
325 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
327 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
330 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
331 make it wrong to make plain commits with git because the recorded $\pends$
332 would have to be updated. The annotation is not needed because
333 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
335 \section{Simple commit}
337 A simple single-parent forward commit $C$ as made by git-commit.
339 \tag*{} C \hasparents \{ A \} \\
340 \tag*{} \patchof{C} = \patchof{A} \\
341 \tag*{} D \isin C \equiv D \isin A \lor D = C
343 This also covers Topbloke-generated commits on plain git branches:
344 Topbloke strips the metadata when exporting.
346 \subsection{No Replay}
349 \subsection{Unique Base}
350 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
352 \subsection{Tip Contents}
353 We need to consider only $A, C \in \py$. From Tip Contents for $A$:
354 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
355 Substitute into the contents of $C$:
356 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
358 Since $D = C \implies D \in \py$,
359 and substituting in $\baseof{C}$, this gives:
360 \[ D \isin C \equiv D \isin \baseof{C} \lor
361 (D \in \py \land D \le A) \lor
362 (D = C \land D \in \py) \]
363 \[ \equiv D \isin \baseof{C} \lor
364 [ D \in \py \land ( D \le A \lor D = C ) ] \]
365 So by Exact Ancestors:
366 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
370 \subsection{Base Acyclic}
372 Need to consider only $A, C \in \pn$.
374 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
376 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
377 $A$, $D \isin C \implies D \not\in \py$. $\qed$
379 \subsection{Coherence and patch inclusion}
381 Need to consider $D \in \py$
383 \subsubsection{For $A \haspatch P, D = C$:}
389 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
391 \subsubsection{For $A \haspatch P, D \neq C$:}
392 Ancestors: $ D \le C \equiv D \le A $.
394 Contents: $ D \isin C \equiv D \isin A \lor f $
395 so $ D \isin C \equiv D \isin A $.
398 \[ A \haspatch P \implies C \haspatch P \]
400 \subsubsection{For $A \nothaspatch P$:}
402 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
405 Now by contents of $A$, $D \notin A$, so $D \notin C$.
408 \[ A \nothaspatch P \implies C \nothaspatch P \]
411 \subsection{Foreign inclusion:}
413 If $D = C$, trivial. For $D \neq C$:
414 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
418 Given $L, R^+, R^-$ where
419 $R^+ \in \pry, R^- = \baseof{R^+}$.
420 Construct $C$ which has $\pr$ removed.
421 Used for removing a branch dependency.
423 C \hasparents \{ L \}
425 \patchof{C} = \patchof{L}
427 \mergeof{C}{L}{R^+}{R^-}
430 \subsection{Conditions}
432 \[ \eqn{ Into Base }{
435 \[ \eqn{ Unique Tip }{
436 \pendsof{L}{\pry} = \{ R^+ \}
438 \[ \eqn{ Currently Included }{
442 \subsection{Ordering of ${L, R^+, R^-}$:}
444 By Unique Tip, $R^+ \le L$. By definition of $\base$, $R^- \le R^+$
445 so $R^- \le L$. So $R^+ \le C$ and $R^- \le C$.
447 (Note that the merge base $R^+ \not\le R^-$, i.e. the merge base is
448 later than one of the branches to be merged.)
450 \subsection{No Replay}
452 No Replay for Merge Results applies. $\qed$
454 \subsection{Desired Contents}
456 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
459 \subsubsection{For $D = C$:}
461 Trivially $D \isin C$. OK.
463 \subsubsection{For $D \neq C, D \not\le L$:}
465 By No Replay $D \not\isin L$. Also $D \not\le R^-$ hence
466 $D \not\isin R^-$. Thus $D \not\isin C$. OK.
468 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
470 By Currently Included, $D \isin L$.
472 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
473 by Unique Tip, $D \le R^+ \equiv D \le L$.
476 By Base Acyclic, $D \not\isin R^-$.
478 Apply $\merge$: $D \not\isin C$. OK.
480 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
482 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
484 Apply $\merge$: $D \isin C \equiv D \isin L$. OK.
488 \subsection{Unique Base}
490 Into Base means that $C \in \pn$, so Unique Base is not
493 \subsection{Tip Contents}
495 Again, not applicable. $\qed$
497 \subsection{Base Acyclic}
499 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
500 And by Into Base $C \not\in \py$.
501 Now from Desired Contents, above, $D \isin C
502 \implies D \isin L \lor D = C$, which thus
503 $\implies D \not\in \py$. $\qed$.
505 \subsection{Coherence and Patch Inclusion}
507 Need to consider some $D \in \py$. By Into Base, $D \neq C$.
509 \subsubsection{For $\p = \pr$:}
510 By Desired Contents, above, $D \not\isin C$.
511 So $C \nothaspatch \pr$.
513 \subsubsection{For $\p \neq \pr$:}
514 By Desired Contents, $D \isin C \equiv D \isin L$
515 (since $D \in \py$ so $D \not\in \pry$).
517 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
518 So $L \nothaspatch \p \implies C \nothaspatch \p$.
520 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
521 so $L \haspatch \p \implies C \haspatch \p$.
525 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
527 C \hasparents \{ L, R \}
529 \patchof{C} = \patchof{L}
533 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
535 \subsection{Conditions}
537 \[ \eqn{ Tip Merge }{
540 R \in \py : & \baseof{R} \ge \baseof{L}
541 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
542 R \in \pn : & M = \baseof{L} \\
543 \text{otherwise} : & \false
546 \[ \eqn{ Merge Acyclic }{
551 \[ \eqn{ Removal Merge Ends }{
552 X \not\haspatch \p \land
556 \pendsof{Y}{\py} = \pendsof{M}{\py}
558 \[ \eqn{ Addition Merge Ends }{
559 X \not\haspatch \p \land
563 \bigforall_{E \in \pendsof{X}{\py}} E \le Y
567 \subsection{Non-Topbloke merges}
569 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$.
570 I.e. not only is it forbidden to merge into a Topbloke-controlled
571 branch without Topbloke's assistance, it is also forbidden to
572 merge any Topbloke-controlled branch into any plain git branch.
574 Given those conditions, Tip Merge and Merge Acyclic do not apply.
575 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
576 Merge Ends condition applies. Good.
578 \subsection{No Replay}
580 See No Replay for Merge Results.
582 \subsection{Unique Base}
584 Need to consider only $C \in \py$, ie $L \in \py$,
585 and calculate $\pendsof{C}{\pn}$. So we will consider some
586 putative ancestor $A \in \pn$ and see whether $A \le C$.
588 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
589 But $C \in py$ and $A \in \pn$ so $A \neq C$.
590 Thus $A \le C \equiv A \le L \lor A \le R$.
592 By Unique Base of L and Transitive Ancestors,
593 $A \le L \equiv A \le \baseof{L}$.
595 \subsubsection{For $R \in \py$:}
597 By Unique Base of $R$ and Transitive Ancestors,
598 $A \le R \equiv A \le \baseof{R}$.
600 But by Tip Merge condition on $\baseof{R}$,
601 $A \le \baseof{L} \implies A \le \baseof{R}$, so
602 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
603 Thus $A \le C \equiv A \le \baseof{R}$.
604 That is, $\baseof{C} = \baseof{R}$.
606 \subsubsection{For $R \in \pn$:}
608 By Tip Merge condition on $R$ and since $M \le R$,
609 $A \le \baseof{L} \implies A \le R$, so
610 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
611 Thus $A \le C \equiv A \le R$.
612 That is, $\baseof{C} = R$.
616 \subsection{Coherence and Patch Inclusion}
618 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
619 This involves considering $D \in \py$.
621 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
622 $D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
623 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch). So $D \neq C$.
624 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
626 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
627 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
628 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
630 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
632 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
633 \equiv D \isin L \lor D \isin R$.
634 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
636 Consider $D \neq C, D \isin X \land D \isin Y$:
637 By $\merge$, $D \isin C$. Also $D \le X$
638 so $D \le C$. OK for $C \haspatch \p$.
640 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
641 By $\merge$, $D \not\isin C$.
642 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
643 OK for $C \haspatch \p$.
645 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
646 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
647 Thus by $\merge$, $D \isin C$. And $D \le Y$ so $D \le C$.
648 OK for $C \haspatch \p$.
650 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
652 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
654 $M \haspatch \p \implies C \nothaspatch \p$.
655 $M \nothaspatch \p \implies C \haspatch \p$.
659 One of the Merge Ends conditions applies.
660 Recall that we are considering $D \in \py$.
661 $D \isin Y \equiv D \le Y$. $D \not\isin X$.
662 We will show for each of
663 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
664 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
666 Consider $D = C$: Thus $C \in \py, L \in \py$, and by Tip
667 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$. By Tip Merge,
668 $M=\baseof{L}$. So by Base Acyclic $D \not\isin M$, i.e.
669 $M \nothaspatch \p$. And indeed $D \isin C$ and $D \le C$. OK.
671 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
672 $D \le Y$ so $D \le C$.
673 $D \not\isin M$ so by $\merge$, $D \isin C$. OK.
675 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
676 $D \not\le Y$. If $D \le X$ then
677 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
678 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
679 Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK.
681 Consider $D \neq C, M \haspatch P, D \isin Y$:
682 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
683 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
684 Thus $D \isin M$. By $\merge$, $D \not\isin C$. OK.
686 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
687 By $\merge$, $D \not\isin C$. OK.
691 \subsection{Base Acyclic}
693 This applies when $C \in \pn$.
694 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
696 Consider some $D \in \py$.
698 By Base Acyclic of $L$, $D \not\isin L$. By the above, $D \not\isin
699 R$. And $D \neq C$. So $D \not\isin C$. $\qed$
701 \subsection{Tip Contents}
703 We need worry only about $C \in \py$.
704 And $\patchof{C} = \patchof{L}$
705 so $L \in \py$ so $L \haspatch \p$. We will use the Unique Base
706 of $C$, and its Coherence and Patch Inclusion, as just proved.
708 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
709 \p$ and by Coherence/Inclusion $C \haspatch \p$ . If $R \not\in \py$
710 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
711 of $\nothaspatch$, $M \nothaspatch \p$. So by Coherence/Inclusion $C
712 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
714 We will consider an arbitrary commit $D$
715 and prove the Exclusive Tip Contents form.
717 \subsubsection{For $D \in \py$:}
718 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
721 \subsubsection{For $D \not\in \py, R \not\in \py$:}
723 $D \neq C$. By Tip Contents of $L$,
724 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
725 $D \isin L \equiv D \isin M$. So by definition of $\merge$, $D \isin
726 C \equiv D \isin R$. And $R = \baseof{C}$ by Unique Base of $C$.
727 Thus $D \isin C \equiv D \isin \baseof{C}$. OK.
729 \subsubsection{For $D \not\in \py, R \in \py$:}
734 $D \isin L \equiv D \isin \baseof{L}$ and
735 $D \isin R \equiv D \isin \baseof{R}$.
737 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
738 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
739 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
740 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
742 So $D \isin M \equiv D \isin L$ and by $\merge$,
743 $D \isin C \equiv D \isin R$. But from Unique Base,
744 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$. OK.
748 \subsection{Foreign Inclusion}
750 Consider some $D$ s.t. $\patchof{D} = \bot$.
751 By Foreign Inclusion of $L, M, R$:
752 $D \isin L \equiv D \le L$;
753 $D \isin M \equiv D \le M$;
754 $D \isin R \equiv D \le R$.
756 \subsubsection{For $D = C$:}
758 $D \isin C$ and $D \le C$. OK.
760 \subsubsection{For $D \neq C, D \isin M$:}
762 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
763 R$. So by $\merge$, $D \isin C$. And $D \le C$. OK.
765 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
767 By $\merge$, $D \isin C$.
768 And $D \isin X$ means $D \le X$ so $D \le C$.
771 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
773 By $\merge$, $D \not\isin C$.
774 And $D \not\le L, D \not\le R$ so $D \not\le C$.