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 )
257 \[ \eqn{Transitive Ancestors:}{
258 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
259 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
263 The implication from right to left is trivial because
264 $ \pends() \subset \pancs() $.
265 For the implication from left to right:
266 by the definition of $\mathcal E$,
267 for every such $A$, either $A \in \pends()$ which implies
268 $A \le M$ by the LHS directly,
269 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
270 in which case we repeat for $A'$. Since there are finitely many
271 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
272 by the LHS. And $A \le A''$.
275 \[ \eqn{Calculation Of Ends:}{
276 \bigforall_{C \hasparents \set A}
277 \pendsof{C}{\set P} =
281 C \not\in \p : & \displaystyle
283 \Bigl[ \Largeexists_{A \in \set A}
284 E \in \pendsof{A}{\set P} \Bigr] \land
285 \Bigl[ \Largenexists_{B \in \set A}
286 E \neq B \land E \le B \Bigr]
292 \subsection{No Replay for Merge Results}
294 If we are constructing $C$, with,
302 No Replay is preserved. \proofstarts
304 \subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
306 \subsubsection{For $D \isin L \land D \isin R$:}
307 $D \isin C$. And $D \isin L \implies D \le L \implies D \le C$. OK.
309 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
312 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
313 \land D \not\isin M$:}
314 $D \isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
317 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
323 \section{Commit annotation}
325 We annotate each Topbloke commit $C$ with:
329 \baseof{C}, \text{ if } C \in \py
332 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
334 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
337 $\patchof{C}$, for each kind of Topbloke-generated commit, is stated
338 in the summary in the section for that kind of commit.
340 Whether $\baseof{C}$ is required, and if so what the value is, is
341 stated in the proof of Unique Base for each kind of commit.
343 $C \haspatch \pa{Q}$ or $\nothaspatch \pa{Q}$ is represented as the
344 set $\{ \pa{Q} | C \haspatch \pa{Q} \}$. Whether $C \haspatch \pa{Q}$
346 (in terms of $I \haspatch \pa{Q}$ or $I \nothaspatch \pa{Q}$
347 for the ingredients $I$),
348 in the proof of Coherence for each kind of commit.
350 $\pendsof{C}{\pa{Q}^+}$ is computed, for all Topbloke-generated commits,
351 using the lemma Calculation of Ends, above.
352 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
353 make it wrong to make plain commits with git because the recorded $\pends$
354 would have to be updated. The annotation is not needed in that case
355 because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
357 \section{Simple commit}
359 A simple single-parent forward commit $C$ as made by git-commit.
361 \tag*{} C \hasparents \{ A \} \\
362 \tag*{} \patchof{C} = \patchof{A} \\
363 \tag*{} D \isin C \equiv D \isin A \lor D = C
365 This also covers Topbloke-generated commits on plain git branches:
366 Topbloke strips the metadata when exporting.
368 \subsection{No Replay}
371 \subsection{Unique Base}
372 If $A, C \in \py$ then by Calculation of Ends for
373 $C, \py, C \not\in \py$:
374 $\pendsof{C}{\pn} = \pendsof{A}{\pn}$ so
375 $\baseof{C} = \baseof{A}$. $\qed$
377 \subsection{Tip Contents}
378 We need to consider only $A, C \in \py$. From Tip Contents for $A$:
379 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
380 Substitute into the contents of $C$:
381 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
383 Since $D = C \implies D \in \py$,
384 and substituting in $\baseof{C}$, this gives:
385 \[ D \isin C \equiv D \isin \baseof{C} \lor
386 (D \in \py \land D \le A) \lor
387 (D = C \land D \in \py) \]
388 \[ \equiv D \isin \baseof{C} \lor
389 [ D \in \py \land ( D \le A \lor D = C ) ] \]
390 So by Exact Ancestors:
391 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
395 \subsection{Base Acyclic}
397 Need to consider only $A, C \in \pn$.
399 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
401 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
402 $A$, $D \isin C \implies D \not\in \py$.
406 \subsection{Coherence and patch inclusion}
408 Need to consider $D \in \py$
410 \subsubsection{For $A \haspatch P, D = C$:}
416 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
418 \subsubsection{For $A \haspatch P, D \neq C$:}
419 Ancestors: $ D \le C \equiv D \le A $.
421 Contents: $ D \isin C \equiv D \isin A \lor f $
422 so $ D \isin C \equiv D \isin A $.
425 \[ A \haspatch P \implies C \haspatch P \]
427 \subsubsection{For $A \nothaspatch P$:}
429 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
432 Now by contents of $A$, $D \notin A$, so $D \notin C$.
435 \[ A \nothaspatch P \implies C \nothaspatch P \]
438 \subsection{Foreign inclusion:}
440 If $D = C$, trivial. For $D \neq C$:
441 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
443 \section{Create Base}
445 Given $L$, create a Topbloke base branch initial commit $B$.
447 B \hasparents \{ L \}
451 D \isin B \equiv D \isin L \lor D = B
454 \subsection{Conditions}
456 \[ \eqn{ Ingredients }{
457 \patchof{L} = \pa{L} \lor \patchof{L} = \bot
459 \[ \eqn{ Non-recursion }{
463 \subsection{No Replay}
465 If $\patchof{L} = \pa{L}$, trivial by Base Acyclic for $L$.
467 If $\patchof{L} = \bot$, xxx
469 Trivial from Base Acyclic for $L$. $\qed$
471 \subsection{Unique Base}
473 Not applicable. $\qed$
475 \subsection{Tip Contents}
477 Not applicable. $\qed$
479 \subsection{Base Acyclic}
491 Given $L$ and $\pr$ as represented by $R^+, R^-$.
492 Construct $C$ which has $\pr$ removed.
493 Used for removing a branch dependency.
495 C \hasparents \{ L \}
497 \patchof{C} = \patchof{L}
499 \mergeof{C}{L}{R^+}{R^-}
502 \subsection{Conditions}
504 \[ \eqn{ Ingredients }{
505 R^+ \in \pry \land R^- = \baseof{R^+}
507 \[ \eqn{ Into Base }{
510 \[ \eqn{ Unique Tip }{
511 \pendsof{L}{\pry} = \{ R^+ \}
513 \[ \eqn{ Currently Included }{
517 \subsection{Ordering of ${L, R^+, R^-}$:}
519 By Unique Tip, $R^+ \le L$. By definition of $\base$, $R^- \le R^+$
520 so $R^- \le L$. So $R^+ \le C$ and $R^- \le C$.
523 (Note that $R^+ \not\le R^-$, i.e. the merge base
524 is a descendant, not an ancestor, of the 2nd parent.)
526 \subsection{No Replay}
528 No Replay for Merge Results applies. $\qed$
530 \subsection{Desired Contents}
532 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
535 \subsubsection{For $D = C$:}
537 Trivially $D \isin C$. OK.
539 \subsubsection{For $D \neq C, D \not\le L$:}
541 By No Replay $D \not\isin L$. Also $D \not\le R^-$ hence
542 $D \not\isin R^-$. Thus $D \not\isin C$. OK.
544 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
546 By Currently Included, $D \isin L$.
548 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
549 by Unique Tip, $D \le R^+ \equiv D \le L$.
552 By Base Acyclic, $D \not\isin R^-$.
554 Apply $\merge$: $D \not\isin C$. OK.
556 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
558 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
560 Apply $\merge$: $D \isin C \equiv D \isin L$. OK.
564 \subsection{Unique Base}
566 Into Base means that $C \in \pn$, so Unique Base is not
569 \subsection{Tip Contents}
571 Again, not applicable. $\qed$
573 \subsection{Base Acyclic}
575 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
576 And by Into Base $C \not\in \py$.
577 Now from Desired Contents, above, $D \isin C
578 \implies D \isin L \lor D = C$, which thus
579 $\implies D \not\in \py$. $\qed$.
581 \subsection{Coherence and Patch Inclusion}
583 Need to consider some $D \in \py$. By Into Base, $D \neq C$.
585 \subsubsection{For $\p = \pr$:}
586 By Desired Contents, above, $D \not\isin C$.
587 So $C \nothaspatch \pr$.
589 \subsubsection{For $\p \neq \pr$:}
590 By Desired Contents, $D \isin C \equiv D \isin L$
591 (since $D \in \py$ so $D \not\in \pry$).
593 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
594 So $L \nothaspatch \p \implies C \nothaspatch \p$.
596 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
597 so $L \haspatch \p \implies C \haspatch \p$.
601 \section{Foreign Inclusion}
603 Consider some $D$ s.t. $\patchof{D} = \bot$. $D \neq C$.
604 So by Desired Contents $D \isin C \equiv D \isin L$.
605 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
607 And $D \le C \equiv D \le L$.
608 Thus $D \isin C \equiv D \le C$.
614 Merge commits $L$ and $R$ using merge base $M$:
616 C \hasparents \{ L, R \}
618 \patchof{C} = \patchof{L}
622 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
624 \subsection{Conditions}
625 \[ \eqn{ Ingredients }{
628 \[ \eqn{ Tip Merge }{
631 R \in \py : & \baseof{R} \ge \baseof{L}
632 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
633 R \in \pn : & M = \baseof{L} \\
634 \text{otherwise} : & \false
637 \[ \eqn{ Merge Acyclic }{
642 \[ \eqn{ Removal Merge Ends }{
643 X \not\haspatch \p \land
647 \pendsof{Y}{\py} = \pendsof{M}{\py}
649 \[ \eqn{ Addition Merge Ends }{
650 X \not\haspatch \p \land
654 \bigforall_{E \in \pendsof{X}{\py}} E \le Y
658 \subsection{Non-Topbloke merges}
660 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$.
661 I.e. not only is it forbidden to merge into a Topbloke-controlled
662 branch without Topbloke's assistance, it is also forbidden to
663 merge any Topbloke-controlled branch into any plain git branch.
665 Given those conditions, Tip Merge and Merge Acyclic do not apply.
666 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
667 Merge Ends condition applies. Good.
669 \subsection{No Replay}
671 No Replay for Merge Results applies. $\qed$
673 \subsection{Unique Base}
675 Need to consider only $C \in \py$, ie $L \in \py$,
676 and calculate $\pendsof{C}{\pn}$. So we will consider some
677 putative ancestor $A \in \pn$ and see whether $A \le C$.
679 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
680 But $C \in py$ and $A \in \pn$ so $A \neq C$.
681 Thus $A \le C \equiv A \le L \lor A \le R$.
683 By Unique Base of L and Transitive Ancestors,
684 $A \le L \equiv A \le \baseof{L}$.
686 \subsubsection{For $R \in \py$:}
688 By Unique Base of $R$ and Transitive Ancestors,
689 $A \le R \equiv A \le \baseof{R}$.
691 But by Tip Merge condition on $\baseof{R}$,
692 $A \le \baseof{L} \implies A \le \baseof{R}$, so
693 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
694 Thus $A \le C \equiv A \le \baseof{R}$.
695 That is, $\baseof{C} = \baseof{R}$.
697 \subsubsection{For $R \in \pn$:}
699 By Tip Merge condition on $R$ and since $M \le R$,
700 $A \le \baseof{L} \implies A \le R$, so
701 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
702 Thus $A \le C \equiv A \le R$.
703 That is, $\baseof{C} = R$.
707 \subsection{Coherence and Patch Inclusion}
709 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
710 This involves considering $D \in \py$.
712 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
713 $D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
714 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch). So $D \neq C$.
715 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
717 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
718 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
719 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
721 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
723 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
724 \equiv D \isin L \lor D \isin R$.
725 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
727 Consider $D \neq C, D \isin X \land D \isin Y$:
728 By $\merge$, $D \isin C$. Also $D \le X$
729 so $D \le C$. OK for $C \haspatch \p$.
731 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
732 By $\merge$, $D \not\isin C$.
733 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
734 OK for $C \haspatch \p$.
736 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
737 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
738 Thus by $\merge$, $D \isin C$. And $D \le Y$ so $D \le C$.
739 OK for $C \haspatch \p$.
741 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
743 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
745 $M \haspatch \p \implies C \nothaspatch \p$.
746 $M \nothaspatch \p \implies C \haspatch \p$.
750 One of the Merge Ends conditions applies.
751 Recall that we are considering $D \in \py$.
752 $D \isin Y \equiv D \le Y$. $D \not\isin X$.
753 We will show for each of
754 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
755 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
757 Consider $D = C$: Thus $C \in \py, L \in \py$, and by Tip
758 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$. By Tip Merge,
759 $M=\baseof{L}$. So by Base Acyclic $D \not\isin M$, i.e.
760 $M \nothaspatch \p$. And indeed $D \isin C$ and $D \le C$. OK.
762 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
763 $D \le Y$ so $D \le C$.
764 $D \not\isin M$ so by $\merge$, $D \isin C$. OK.
766 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
767 $D \not\le Y$. If $D \le X$ then
768 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
769 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
770 Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK.
772 Consider $D \neq C, M \haspatch P, D \isin Y$:
773 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
774 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
775 Thus $D \isin M$. By $\merge$, $D \not\isin C$. OK.
777 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
778 By $\merge$, $D \not\isin C$. OK.
782 \subsection{Base Acyclic}
784 This applies when $C \in \pn$.
785 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
787 Consider some $D \in \py$.
789 By Base Acyclic of $L$, $D \not\isin L$. By the above, $D \not\isin
790 R$. And $D \neq C$. So $D \not\isin C$.
794 \subsection{Tip Contents}
796 We need worry only about $C \in \py$.
797 And $\patchof{C} = \patchof{L}$
798 so $L \in \py$ so $L \haspatch \p$. We will use the Unique Base
799 of $C$, and its Coherence and Patch Inclusion, as just proved.
801 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
802 \p$ and by Coherence/Inclusion $C \haspatch \p$ . If $R \not\in \py$
803 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
804 of $\nothaspatch$, $M \nothaspatch \p$. So by Coherence/Inclusion $C
805 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
807 We will consider an arbitrary commit $D$
808 and prove the Exclusive Tip Contents form.
810 \subsubsection{For $D \in \py$:}
811 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
814 \subsubsection{For $D \not\in \py, R \not\in \py$:}
816 $D \neq C$. By Tip Contents of $L$,
817 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
818 $D \isin L \equiv D \isin M$. So by definition of $\merge$, $D \isin
819 C \equiv D \isin R$. And $R = \baseof{C}$ by Unique Base of $C$.
820 Thus $D \isin C \equiv D \isin \baseof{C}$. OK.
822 \subsubsection{For $D \not\in \py, R \in \py$:}
827 $D \isin L \equiv D \isin \baseof{L}$ and
828 $D \isin R \equiv D \isin \baseof{R}$.
830 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
831 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
832 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
833 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
835 So $D \isin M \equiv D \isin L$ and by $\merge$,
836 $D \isin C \equiv D \isin R$. But from Unique Base,
837 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$. OK.
841 \subsection{Foreign Inclusion}
843 Consider some $D$ s.t. $\patchof{D} = \bot$.
844 By Foreign Inclusion of $L, M, R$:
845 $D \isin L \equiv D \le L$;
846 $D \isin M \equiv D \le M$;
847 $D \isin R \equiv D \le R$.
849 \subsubsection{For $D = C$:}
851 $D \isin C$ and $D \le C$. OK.
853 \subsubsection{For $D \neq C, D \isin M$:}
855 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
856 R$. So by $\merge$, $D \isin C$. And $D \le C$. OK.
858 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
860 By $\merge$, $D \isin C$.
861 And $D \isin X$ means $D \le X$ so $D \le C$.
864 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
866 By $\merge$, $D \not\isin C$.
867 And $D \not\le L, D \not\le R$ so $D \not\le C$.