chiark / gitweb /
1 \documentclass[a4paper,leqno]{strayman}
2 \errorcontextlines=50
3 \let\numberwithin=\notdef
4 \usepackage{amsmath}
5 \usepackage{mathabx}
6 \usepackage{txfonts}
7 \usepackage{amsfonts}
8 \usepackage{mdwlist}
9 %\usepackage{accents}
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}{%
74   \mathop{\mathchoice%
75     {\hbox{\huge$\forall$}}%
76     {\hbox{\Large$\forall$}}%
77     {\hbox{\normalsize$\forall$}}%
78     {\hbox{\scriptsize$\forall$}}}%
79 }
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*{}}
91 \newcommand{\true}{t}
92 \newcommand{\false}{f}
94 \begin{document}
96 \section{Notation}
98 \begin{basedescript}{
99 \desclabelwidth{5em}
100 \desclabelstyle{\nextlinelabel}
101 }
102 \item[ $C \hasparents \set X$ ]
103 The parents of commit $C$ are exactly the set
104 $\set X$.
106 \item[ $C \ge D$ ]
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
118 is not transitive.
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
157 patch.  If 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 167 \begin{cases} 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 171 \end{cases} 172 174 \end{basedescript} 175 \newpage 176 \section{Invariants} 178 We maintain these each time we construct a new commit. \\ 179 $\eqn{No Replay:}{ 180 C \has D \implies C \ge D 181 }$ 182 $\eqn{Unique Base:}{ 183 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \} 184 }$ 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) } 189 }$ 190 $\eqn{Base Acyclic:}{ 191 \bigforall_{B \in \pn} D \isin B \implies D \notin \py 192 }$ 193 $\eqn{Coherence:}{ 194 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p 195 }$ 196 $\eqn{Foreign Inclusion:}{ 197 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C 198 }$ 200 \section{Some lemmas} 202 $\eqn{Alternative (overlapping) formulations defining 203 \mergeof{C}{L}{M}{R}:}{ 204 D \isin C \equiv 205 \begin{cases} 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} 211 \end{cases} 212 }$ 213 \proof{ 214 Truth table xxx 216 Original definition is symmetrical in$L$and$R$. 217 } 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 ) 222 \Bigr] 223 }$ 224 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive. 226 \proof{ 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$. 229 } 230 $\eqntag{{\it Corollary - equivalent to Tip Contents}}{ 231 \bigforall_{C \in \py} D \isin C \equiv 232 \begin{cases} 233 D \in \py : & D \le C \\ 234 D \not\in \py : & D \isin \baseof{C} 235 \end{cases} 236 }$ 238 $\eqn{Tip Self Inpatch:}{ 239 \bigforall_{C \in \py} C \haspatch \p 240 }$ 241 Ie, tip commits contain their own patch. 243 \proof{ 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 $247 } 249 $\eqn{Exact Ancestors:}{ 250 \bigforall_{ C \hasparents \set{R} } 251 D \le C \equiv 252 ( \mathop{\hbox{\huge{\vee}}}_{R \in \set R} D \le R ) 253 \lor D = C 254 }$ 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] 259 }$ 261 \proof{ 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''$. 272 } 273 $\eqn{Calculation Of Ends:}{ 274 \bigforall_{C \hasparents \set A} 275 \pendsof{C}{\set P} = 276 \left\{ E \Big| 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] 281 \right\} 282 }$ 283 XXX proof TBD. 285 \subsection{No Replay for Merge Results} 287 If we are constructing$C$, with, 288 \gathbegin 289 \mergeof{C}{L}{M}{R} 290 \gathnext 291 L \le C 292 \gathnext 293 R \le C 294 \end{gather} 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$:} 303$D \not\isin C$. OK. 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
308 R$so$D \le C$. OK. 310 \subsubsection{For$D \neq C \land (D \isin L \equiv D \not\isin R)
311  \land D \isin M$:} 312$D \not\isin C$. OK. 314$\qed$316 \section{Commit annotation} 318 We annotate each Topbloke commit$C$with: 319 \gathbegin 320 \patchof{C} 321 \gathnext 322 \baseof{C}, \text{ if } C \in \py 323 \gathnext 324 \bigforall_{\pa{Q}} 325 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q} 326 \gathnext 327 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}} 328 \end{gather} 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. 338 \begin{gather} 339 \tag*{} C \hasparents \{ A \} \\ 340 \tag*{} \patchof{C} = \patchof{A} \\ 341 \tag*{} D \isin C \equiv D \isin A \lor D = C 342 \end{gather} 343 This also covers Topbloke-generated commits on plain git branches: 344 Topbloke strips the metadata when exporting. 346 \subsection{No Replay} 347 Trivial. 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 ) 357 \lor D = C$ 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 367 )$ 368$\qed$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$:} 385 Ancestors of$C$: 386$ D \le C $. 388 Contents of$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 $. 397 So: 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$. 403 Thus$D \neq C$. 405 Now by contents of$A$,$D \notin A$, so$D \notin C$. 407 So: 408 $A \nothaspatch P \implies C \nothaspatch P$ 409$\qed$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$416 \section{Anticommit} 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. 422 \gathbegin 423 C \hasparents \{ L \} 424 \gathnext 425 \patchof{C} = \patchof{L} 426 \gathnext 427 \mergeof{C}{L}{R^+}{R^-} 428 \end{gather} 430 \subsection{Conditions} 432 $\eqn{ Into Base }{ 433 L \in \pn 434 }$ 435 $\eqn{ Unique Tip }{ 436 \pendsof{L}{\pry} = \{ R^+ \} 437 }$ 438 $\eqn{ Currently Included }{ 439 L \haspatch \pry 440 }$ 442 \subsection{No Replay} 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$and No Replay for 446 Merge Results applies.$\qed$448 \subsection{Desired Contents} 450 $D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C$ 451 \proofstarts 453 \subsubsection{For$D = C$:} 455 Trivially$D \isin C$. OK. 457 \subsubsection{For$D \neq C, D \not\le L$:} 459 By No Replay$D \not\isin L$. Also$D \not\le R^-$hence 460$D \not\isin R^-$. Thus$D \not\isin C$. OK. 462 \subsubsection{For$D \neq C, D \le L, D \in \pry$:} 464 By Currently Included,$D \isin L$. 466 By Tip Self Inpatch,$D \isin R^+ \equiv D \le R^+$, but by 467 by Unique Tip,$D \le R^+ \equiv D \le L$. 468 So$D \isin R^+$. 470 By Base Acyclic,$D \not\isin R^-$. 472 Apply$\merge$:$D \not\isin C$. OK. 474 \subsubsection{For$D \neq C, D \le L, D \notin \pry$:} 476 By Tip Contents for$R^+$,$D \isin R^+ \equiv D \isin R^-$. 478 Apply$\merge$:$D \isin C \equiv D \isin L$. OK. 480$\qed$482 \subsection{Unique Base} 484 Into Base means that$C \in \pn$, so Unique Base is not 485 applicable.$\qed$487 \subsection{Tip Contents} 489 Again, not applicable.$\qed$491 \subsection{Base Acyclic} 493 By Base Acyclic for$L$,$D \isin L \implies D \not\in \py$. 494 And by Into Base$C \not\in \py$. 495 Now from Desired Contents, above,$D \isin C
496 \implies D \isin L \lor D = C$, which thus 497$\implies D \not\in \py$.$\qed$. 499 \section{Merge} 501 Merge commits$L$and$R$using merge base$M$($M < L, M < R$): 502 \gathbegin 503 C \hasparents \{ L, R \} 504 \gathnext 505 \patchof{C} = \patchof{L} 506 \gathnext 507 \mergeof{C}{L}{M}{R} 508 \end{gather} 509 We will occasionally use$X,Y$s.t.$\{X,Y\} = \{L,R\}$. 511 \subsection{Conditions} 513 $\eqn{ Tip Merge }{ 514 L \in \py \implies 515 \begin{cases} 516 R \in \py : & \baseof{R} \ge \baseof{L} 517 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\ 518 R \in \pn : & M = \baseof{L} \\ 519 \text{otherwise} : & \false 520 \end{cases} 521 }$ 522 $\eqn{ Merge Acyclic }{ 523 L \in \pn 524 \implies 525 R \nothaspatch \p 526 }$ 527 $\eqn{ Removal Merge Ends }{ 528 X \not\haspatch \p \land 529 Y \haspatch \p \land 530 M \haspatch \p 531 \implies 532 \pendsof{Y}{\py} = \pendsof{M}{\py} 533 }$ 534 $\eqn{ Addition Merge Ends }{ 535 X \not\haspatch \p \land 536 Y \haspatch \p \land 537 M \nothaspatch \p 538 \implies \left[ 539 \bigforall_{E \in \pendsof{X}{\py}} E \le Y 540 \right] 541 }$ 543 \subsection{Non-Topbloke merges} 545 We require both$\patchof{L} = \bot$and$\patchof{R} = \bot$. 546 I.e. not only is it forbidden to merge into a Topbloke-controlled 547 branch without Topbloke's assistance, it is also forbidden to 548 merge any Topbloke-controlled branch into any plain git branch. 550 Given those conditions, Tip Merge and Merge Acyclic do not apply. 551 And$Y \not\in \py$so$\neg [ Y \haspatch \p ]$so neither 552 Merge Ends condition applies. Good. 554 \subsection{No Replay} 556 See No Replay for Merge Results. 558 \subsection{Unique Base} 560 Need to consider only$C \in \py$, ie$L \in \py$, 561 and calculate$\pendsof{C}{\pn}$. So we will consider some 562 putative ancestor$A \in \pn$and see whether$A \le C$. 564 By Exact Ancestors for C,$A \le C \equiv A \le L \lor A \le R \lor A = C$. 565 But$C \in py$and$A \in \pn$so$A \neq C$. 566 Thus$A \le C \equiv A \le L \lor A \le R$. 568 By Unique Base of L and Transitive Ancestors, 569$A \le L \equiv A \le \baseof{L}$. 571 \subsubsection{For$R \in \py$:} 573 By Unique Base of$R$and Transitive Ancestors, 574$A \le R \equiv A \le \baseof{R}$. 576 But by Tip Merge condition on$\baseof{R}$, 577$A \le \baseof{L} \implies A \le \baseof{R}$, so 578$A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$. 579 Thus$A \le C \equiv A \le \baseof{R}$. 580 That is,$\baseof{C} = \baseof{R}$. 582 \subsubsection{For$R \in \pn$:} 584 By Tip Merge condition on$R$and since$M \le R$, 585$A \le \baseof{L} \implies A \le R$, so 586$A \le R \lor A \le \baseof{L} \equiv A \le R$. 587 Thus$A \le C \equiv A \le R$. 588 That is,$\baseof{C} = R$. 590$\qed$592 \subsection{Coherence and Patch Inclusion} 594 Need to determine$C \haspatch \p$based on$L,M,R \haspatch \p$. 595 This involves considering$D \in \py$. 597 \subsubsection{For$L \nothaspatch \p, R \nothaspatch \p$:} 598$D \not\isin L \land D \not\isin R$.$C \not\in \py$(otherwise$L
599 \in \py$ie$L \haspatch \p$by Tip Self Inpatch). So$D \neq C$. 600 Applying$\merge$gives$D \not\isin C$i.e.$C \nothaspatch \p$. 602 \subsubsection{For$L \haspatch \p, R \haspatch \p$:} 603$D \isin L \equiv D \le L$and$D \isin R \equiv D \le R$. 604 (Likewise$D \isin X \equiv D \le X$and$D \isin Y \equiv D \le Y$.) 606 Consider$D = C$:$D \isin C$,$D \le C$, OK for$C \haspatch \p$. 608 For$D \neq C$:$D \le C \equiv D \le L \lor D \le R
609  \equiv D \isin L \lor D \isin R$. 610 (Likewise$D \le C \equiv D \le X \lor D \le Y$.) 612 Consider$D \neq C, D \isin X \land D \isin Y$: 613 By$\merge$,$D \isin C$. Also$D \le X$614 so$D \le C$. OK for$C \haspatch \p$. 616 Consider$D \neq C, D \not\isin X \land D \not\isin Y$: 617 By$\merge$,$D \not\isin C$. 618 And$D \not\le X \land D \not\le Y$so$D \not\le C$. 619 OK for$C \haspatch \p$. 621 Remaining case, wlog, is$D \not\isin X \land D \isin Y$. 622$D \not\le X$so$D \not\le M$so$D \not\isin M$. 623 Thus by$\merge$,$D \isin C$. And$D \le Y$so$D \le C$. 624 OK for$C \haspatch \p$. 626 So indeed$L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$. 628 \subsubsection{For (wlog)$X \not\haspatch \p, Y \haspatch \p$:} 630$C \haspatch \p \equiv M \nothaspatch \p$. 632 \proofstarts 634 One of the Merge Ends conditions applies. 635 Recall that we are considering$D \in \py$. 636$D \isin Y \equiv D \le Y$.$D \not\isin X$. 637 We will show for each of 638 various cases that$D \isin C \equiv M \nothaspatch \p \land D \le C$639 (which suffices by definition of$\haspatch$and$\nothaspatch$). 641 Consider$D = C$: Thus$C \in \py, L \in \py$, and by Tip 642 Self Inpatch$L \haspatch \p$, so$L=Y, R=X$. By Tip Merge, 643$M=\baseof{L}$. So by Base Acyclic$D \not\isin M$, i.e. 644$M \nothaspatch \p$. And indeed$D \isin C$and$D \le C$. OK. 646 Consider$D \neq C, M \nothaspatch P, D \isin Y$: 647$D \le Y$so$D \le C$. 648$D \not\isin M$so by$\merge$,$D \isin C$. OK. 650 Consider$D \neq C, M \nothaspatch P, D \not\isin Y$: 651$D \not\le Y$. If$D \le X$then 652$D \in \pancsof{X}{\py}$, so by Addition Merge Ends and 653 Transitive Ancestors$D \le Y$--- a contradiction, so$D \not\le X$. 654 Thus$D \not\le C$. By$\merge$,$D \not\isin C$. OK. 656 Consider$D \neq C, M \haspatch P, D \isin Y$: 657$D \le Y$so$D \in \pancsof{Y}{\py}$so by Removal Merge Ends 658 and Transitive Ancestors$D \in \pancsof{M}{\py}$so$D \le M$. 659 Thus$D \isin M$. By$\merge$,$D \not\isin C$. OK. 661 Consider$D \neq C, M \haspatch P, D \not\isin Y$: 662 By$\merge$,$D \not\isin C$. OK. 664$\qed$666 \subsection{Base Acyclic} 668 This applies when$C \in \pn$. 669$C \in \pn$when$L \in \pn$so by Merge Acyclic,$R \nothaspatch \p$. 671 Consider some$D \in \py$. 673 By Base Acyclic of$L$,$D \not\isin L$. By the above,$D \not\isin
674 R$. And$D \neq C$. So$D \not\isin C$.$\qed$676 \subsection{Tip Contents} 678 We need worry only about$C \in \py$. 679 And$\patchof{C} = \patchof{L}$680 so$L \in \py$so$L \haspatch \p$. We will use the Unique Base 681 of$C$, and its Coherence and Patch Inclusion, as just proved. 683 Firstly we show$C \haspatch \p$: If$R \in \py$, then$R \haspatch
684 \p$and by Coherence/Inclusion$C \haspatch \p$. If$R \not\in \py$685 then by Tip Merge$M = \baseof{L}$so by Base Acyclic and definition 686 of$\nothaspatch$,$M \nothaspatch \p$. So by Coherence/Inclusion$C
687 \haspatch \p$(whether$R \haspatch \p$or$\nothaspatch$). 689 We will consider an arbitrary commit$D$690 and prove the Exclusive Tip Contents form. 692 \subsubsection{For$D \in \py$:} 693$C \haspatch \p$so by definition of$\haspatch$,$D \isin C \equiv D
694 \le C$. OK. 696 \subsubsection{For$D \not\in \py, R \not\in \py$:} 698$D \neq C$. By Tip Contents of$L$, 699$D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition, 700$D \isin L \equiv D \isin M$. So by definition of$\merge$,$D \isin
701 C \equiv D \isin R$. And$R = \baseof{C}$by Unique Base of$C$. 702 Thus$D \isin C \equiv D \isin \baseof{C}$. OK. 704 \subsubsection{For$D \not\in \py, R \in \py$:} 706$D \neq C$. 708 By Tip Contents 709$D \isin L \equiv D \isin \baseof{L}$and 710$D \isin R \equiv D \isin \baseof{R}$. 712 If$\baseof{L} = M$, trivially$D \isin M \equiv D \isin \baseof{L}.$713 Whereas if$\baseof{L} = \baseof{M}$, by definition of$\base$, 714$\patchof{M} = \patchof{L} = \py$, so by Tip Contents of$M$, 715$D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$. 717 So$D \isin M \equiv D \isin L$and by$\merge$, 718$D \isin C \equiv D \isin R$. But from Unique Base, 719$\baseof{C} = R$so$D \isin C \equiv D \isin \baseof{C}$. OK. 721$\qed$723 \subsection{Foreign Inclusion} 725 Consider some$D$s.t.$\patchof{D} = \bot$. 726 By Foreign Inclusion of$L, M, R$: 727$D \isin L \equiv D \le L$; 728$D \isin M \equiv D \le M$; 729$D \isin R \equiv D \le R$. 731 \subsubsection{For$D = C$:} 733$D \isin C$and$D \le C$. OK. 735 \subsubsection{For$D \neq C, D \isin M$:} 737 Thus$D \le M$so$D \le L$and$D \le R$so$D \isin L$and$D \isin
738 R$. So by$\merge$,$D \isin C$. And$D \le C$. OK. 740 \subsubsection{For$D \neq C, D \not\isin M, D \isin X$:} 742 By$\merge$,$D \isin C$. 743 And$D \isin X$means$D \le X$so$D \le C$. 744 OK. 746 \subsubsection{For$D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:} 748 By$\merge$,$D \not\isin C$. 749 And$D \not\le L, D \not\le R$so$D \not\le C$. 750 OK 752$\qed\$
754 \end{document}