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 xxx make all conditions be in conditions, not in (or also in) intro
100 \begin{basedescript}{
101 \desclabelwidth{5em}
102 \desclabelstyle{\nextlinelabel}
103 }
104 \item[ $C \hasparents \set X$ ]
105 The parents of commit $C$ are exactly the set
106 $\set X$.
108 \item[ $C \ge D$ ]
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
120 is not transitive.
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
159 patch.  If 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 169 \begin{cases} 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 173 \end{cases} 174 176 \end{basedescript} 177 \newpage 178 \section{Invariants} 180 We maintain these each time we construct a new commit. \\ 181 $\eqn{No Replay:}{ 182 C \has D \implies C \ge D 183 }$ 184 $\eqn{Unique Base:}{ 185 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \} 186 }$ 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) } 191 }$ 192 $\eqn{Base Acyclic:}{ 193 \bigforall_{B \in \pn} D \isin B \implies D \notin \py 194 }$ 195 $\eqn{Coherence:}{ 196 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p 197 }$ 198 $\eqn{Foreign Inclusion:}{ 199 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C 200 }$ 202 \section{Some lemmas} 204 $\eqn{Alternative (overlapping) formulations defining 205 \mergeof{C}{L}{M}{R}:}{ 206 D \isin C \equiv 207 \begin{cases} 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} 213 \end{cases} 214 }$ 215 \proof{ 216 Truth table xxx 218 Original definition is symmetrical in$L$and$R$. 219 } 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 ) 224 \Bigr] 225 }$ 226 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive. 228 \proof{ 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$. 231 } 232 $\eqntag{{\it Corollary - equivalent to Tip Contents}}{ 233 \bigforall_{C \in \py} D \isin C \equiv 234 \begin{cases} 235 D \in \py : & D \le C \\ 236 D \not\in \py : & D \isin \baseof{C} 237 \end{cases} 238 }$ 240 $\eqn{Tip Self Inpatch:}{ 241 \bigforall_{C \in \py} C \haspatch \p 242 }$ 243 Ie, tip commits contain their own patch. 245 \proof{ 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 $249 } 251 $\eqn{Exact Ancestors:}{ 252 \bigforall_{ C \hasparents \set{R} } 253 D \le C \equiv 254 ( \mathop{\hbox{\huge{\vee}}}_{R \in \set R} D \le R ) 255 \lor D = C 256 }$ 258 $\eqn{Transitive Ancestors:}{ 259 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv 260 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right] 261 }$ 263 \proof{ 264 The implication from right to left is trivial because 265$ \pends() \subset \pancs() $. 266 For the implication from left to right: 267 by the definition of$\mathcal E$, 268 for every such$A$, either$A \in \pends()$which implies 269$A \le M$by the LHS directly, 270 or$\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $271 in which case we repeat for$A'$. Since there are finitely many 272 commits, this terminates with$A'' \in \pends()$, ie$A'' \le M$273 by the LHS. And$A \le A''$. 274 } 275 $\eqn{Calculation Of Ends:}{ 276 \bigforall_{C \hasparents \set A} 277 \pendsof{C}{\set P} = 278 \left\{ E \Big| 279 \Bigl[ \Largeexists_{A \in \set A} 280 E \in \pendsof{A}{\set P} \Bigr] \land 281 \Bigl[ \Largenexists_{B \in \set A} 282 E \neq B \land E \le B \Bigr] 283 \right\} 284 }$ 285 XXX proof TBD. 287 \subsection{No Replay for Merge Results} 289 If we are constructing$C$, with, 290 \gathbegin 291 \mergeof{C}{L}{M}{R} 292 \gathnext 293 L \le C 294 \gathnext 295 R \le C 296 \end{gather} 297 No Replay is preserved. \proofstarts 299 \subsubsection{For$D=C$:}$D \isin C, D \le C$. OK. 301 \subsubsection{For$D \isin L \land D \isin R$:} 302$D \isin C$. And$D \isin L \implies D \le L \implies D \le C$. OK. 304 \subsubsection{For$D \neq C \land D \not\isin L \land D \not\isin R$:} 305$D \not\isin C$. OK. 307 \subsubsection{For$D \neq C \land (D \isin L \equiv D \not\isin R)
308  \land D \not\isin M$:} 309$D \isin C$. Also$D \isin L \lor D \isin R$so$D \le L \lor D \le
310 R$so$D \le C$. OK. 312 \subsubsection{For$D \neq C \land (D \isin L \equiv D \not\isin R)
313  \land D \isin M$:} 314$D \not\isin C$. OK. 316$\qed$318 \section{Commit annotation} 320 We annotate each Topbloke commit$C$with: 321 \gathbegin 322 \patchof{C} 323 \gathnext 324 \baseof{C}, \text{ if } C \in \py 325 \gathnext 326 \bigforall_{\pa{Q}} 327 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q} 328 \gathnext 329 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}} 330 \end{gather} 332 We do not annotate$\pendsof{C}{\py}$for$C \in \py$. Doing so would 333 make it wrong to make plain commits with git because the recorded$\pends$334 would have to be updated. The annotation is not needed because 335$\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$. 337 \section{Simple commit} 339 A simple single-parent forward commit$C$as made by git-commit. 340 \begin{gather} 341 \tag*{} C \hasparents \{ A \} \\ 342 \tag*{} \patchof{C} = \patchof{A} \\ 343 \tag*{} D \isin C \equiv D \isin A \lor D = C 344 \end{gather} 345 This also covers Topbloke-generated commits on plain git branches: 346 Topbloke strips the metadata when exporting. 348 \subsection{No Replay} 349 Trivial. 351 \subsection{Unique Base} 352 If$A, C \in \py$then$\baseof{C} = \baseof{A}$.$\qed$354 \subsection{Tip Contents} 355 We need to consider only$A, C \in \py$. From Tip Contents for$A$: 356 $D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )$ 357 Substitute into the contents of$C$: 358 $D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) 359 \lor D = C$ 360 Since$D = C \implies D \in \py$, 361 and substituting in$\baseof{C}$, this gives: 362 $D \isin C \equiv D \isin \baseof{C} \lor 363 (D \in \py \land D \le A) \lor 364 (D = C \land D \in \py)$ 365 $\equiv D \isin \baseof{C} \lor 366 [ D \in \py \land ( D \le A \lor D = C ) ]$ 367 So by Exact Ancestors: 368 $D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C 369 )$ 370$\qed$372 \subsection{Base Acyclic} 374 Need to consider only$A, C \in \pn$. 376 For$D = C$:$D \in \pn$so$D \not\in \py$. OK. 378 For$D \neq C$:$D \isin C \equiv D \isin A$, so by Base Acyclic for 379$A$,$D \isin C \implies D \not\in \py$.$\qed$381 \subsection{Coherence and patch inclusion} 383 Need to consider$D \in \py$385 \subsubsection{For$A \haspatch P, D = C$:} 387 Ancestors of$C$: 388$ D \le C $. 390 Contents of$C$: 391$ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $. 393 \subsubsection{For$A \haspatch P, D \neq C$:} 394 Ancestors:$ D \le C \equiv D \le A $. 396 Contents:$ D \isin C \equiv D \isin A \lor f $397 so$ D \isin C \equiv D \isin A $. 399 So: 400 $A \haspatch P \implies C \haspatch P$ 402 \subsubsection{For$A \nothaspatch P$:} 404 Firstly,$C \not\in \py$since if it were,$A \in \py$. 405 Thus$D \neq C$. 407 Now by contents of$A$,$D \notin A$, so$D \notin C$. 409 So: 410 $A \nothaspatch P \implies C \nothaspatch P$ 411$\qed$413 \subsection{Foreign inclusion:} 415 If$D = C$, trivial. For$D \neq C$: 416$D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.$\qed$418 \section{Anticommit} 420 Given$L, R^+, R^-$where 421$R^+ \in \pry, R^- = \baseof{R^+}$. 422 Construct$C$which has$\pr$removed. 423 Used for removing a branch dependency. 424 \gathbegin 425 C \hasparents \{ L \} 426 \gathnext 427 \patchof{C} = \patchof{L} 428 \gathnext 429 \mergeof{C}{L}{R^+}{R^-} 430 \end{gather} 432 \subsection{Conditions} 434 $\eqn{ Into Base }{ 435 L \in \pn 436 }$ 437 $\eqn{ Unique Tip }{ 438 \pendsof{L}{\pry} = \{ R^+ \} 439 }$ 440 $\eqn{ Currently Included }{ 441 L \haspatch \pry 442 }$ 444 \subsection{Ordering of${L, R^+, R^-}$:} 446 By Unique Tip,$R^+ \le L$. By definition of$\base$,$R^- \le R^+$447 so$R^- \le L$. So$R^+ \le C$and$R^- \le C$. 449 (Note that the merge base$R^+ \not\le R^-$, i.e. the merge base is 450 later than one of the branches to be merged.) 452 \subsection{No Replay} 454 No Replay for Merge Results applies.$\qed$456 \subsection{Desired Contents} 458 $D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C$ 459 \proofstarts 461 \subsubsection{For$D = C$:} 463 Trivially$D \isin C$. OK. 465 \subsubsection{For$D \neq C, D \not\le L$:} 467 By No Replay$D \not\isin L$. Also$D \not\le R^-$hence 468$D \not\isin R^-$. Thus$D \not\isin C$. OK. 470 \subsubsection{For$D \neq C, D \le L, D \in \pry$:} 472 By Currently Included,$D \isin L$. 474 By Tip Self Inpatch,$D \isin R^+ \equiv D \le R^+$, but by 475 by Unique Tip,$D \le R^+ \equiv D \le L$. 476 So$D \isin R^+$. 478 By Base Acyclic,$D \not\isin R^-$. 480 Apply$\merge$:$D \not\isin C$. OK. 482 \subsubsection{For$D \neq C, D \le L, D \notin \pry$:} 484 By Tip Contents for$R^+$,$D \isin R^+ \equiv D \isin R^-$. 486 Apply$\merge$:$D \isin C \equiv D \isin L$. OK. 488$\qed$490 \subsection{Unique Base} 492 Into Base means that$C \in \pn$, so Unique Base is not 493 applicable.$\qed$495 \subsection{Tip Contents} 497 Again, not applicable.$\qed$499 \subsection{Base Acyclic} 501 By Base Acyclic for$L$,$D \isin L \implies D \not\in \py$. 502 And by Into Base$C \not\in \py$. 503 Now from Desired Contents, above,$D \isin C
504 \implies D \isin L \lor D = C$, which thus 505$\implies D \not\in \py$.$\qed$. 507 \subsection{Coherence and Patch Inclusion} 509 Need to consider some$D \in \py$. By Into Base,$D \neq C$. 511 \subsubsection{For$\p = \pr$:} 512 By Desired Contents, above,$D \not\isin C$. 513 So$C \nothaspatch \pr$. 515 \subsubsection{For$\p \neq \pr$:} 516 By Desired Contents,$D \isin C \equiv D \isin L$517 (since$D \in \py$so$D \not\in \pry$). 519 If$L \nothaspatch \p$,$D \not\isin L$so$D \not\isin C$. 520 So$L \nothaspatch \p \implies C \nothaspatch \p$. 522 Whereas if$L \haspatch \p$,$D \isin L \equiv D \le L$. 523 so$L \haspatch \p \implies C \haspatch \p$. 525 \section{Foreign Inclusion} 527 Consider some$D$s.t.$\patchof{D} = \bot$.$D \neq C$. 528 So by Desired Contents$D \isin C \equiv D \isin L$. 529 By Foreign Inclusion of$D$in$L$,$D \isin L \equiv D \le L$. 531 And$D \le C \equiv D \le L$. 532 Thus$D \isin C \equiv D \le C$.$\qed$534 \section{Merge} 536 Merge commits$L$and$R$using merge base$M$($M < L, M < R$): 537 \gathbegin 538 C \hasparents \{ L, R \} 539 \gathnext 540 \patchof{C} = \patchof{L} 541 \gathnext 542 \mergeof{C}{L}{M}{R} 543 \end{gather} 544 We will occasionally use$X,Y$s.t.$\{X,Y\} = \{L,R\}$. 546 \subsection{Conditions} 548 $\eqn{ Tip Merge }{ 549 L \in \py \implies 550 \begin{cases} 551 R \in \py : & \baseof{R} \ge \baseof{L} 552 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\ 553 R \in \pn : & M = \baseof{L} \\ 554 \text{otherwise} : & \false 555 \end{cases} 556 }$ 557 $\eqn{ Merge Acyclic }{ 558 L \in \pn 559 \implies 560 R \nothaspatch \p 561 }$ 562 $\eqn{ Removal Merge Ends }{ 563 X \not\haspatch \p \land 564 Y \haspatch \p \land 565 M \haspatch \p 566 \implies 567 \pendsof{Y}{\py} = \pendsof{M}{\py} 568 }$ 569 $\eqn{ Addition Merge Ends }{ 570 X \not\haspatch \p \land 571 Y \haspatch \p \land 572 M \nothaspatch \p 573 \implies \left[ 574 \bigforall_{E \in \pendsof{X}{\py}} E \le Y 575 \right] 576 }$ 578 \subsection{Non-Topbloke merges} 580 We require both$\patchof{L} = \bot$and$\patchof{R} = \bot$. 581 I.e. not only is it forbidden to merge into a Topbloke-controlled 582 branch without Topbloke's assistance, it is also forbidden to 583 merge any Topbloke-controlled branch into any plain git branch. 585 Given those conditions, Tip Merge and Merge Acyclic do not apply. 586 And$Y \not\in \py$so$\neg [ Y \haspatch \p ]$so neither 587 Merge Ends condition applies. Good. 589 \subsection{No Replay} 591 No Replay for Merge Results applies.$\qed$593 \subsection{Unique Base} 595 Need to consider only$C \in \py$, ie$L \in \py$, 596 and calculate$\pendsof{C}{\pn}$. So we will consider some 597 putative ancestor$A \in \pn$and see whether$A \le C$. 599 By Exact Ancestors for C,$A \le C \equiv A \le L \lor A \le R \lor A = C$. 600 But$C \in py$and$A \in \pn$so$A \neq C$. 601 Thus$A \le C \equiv A \le L \lor A \le R$. 603 By Unique Base of L and Transitive Ancestors, 604$A \le L \equiv A \le \baseof{L}$. 606 \subsubsection{For$R \in \py$:} 608 By Unique Base of$R$and Transitive Ancestors, 609$A \le R \equiv A \le \baseof{R}$. 611 But by Tip Merge condition on$\baseof{R}$, 612$A \le \baseof{L} \implies A \le \baseof{R}$, so 613$A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$. 614 Thus$A \le C \equiv A \le \baseof{R}$. 615 That is,$\baseof{C} = \baseof{R}$. 617 \subsubsection{For$R \in \pn$:} 619 By Tip Merge condition on$R$and since$M \le R$, 620$A \le \baseof{L} \implies A \le R$, so 621$A \le R \lor A \le \baseof{L} \equiv A \le R$. 622 Thus$A \le C \equiv A \le R$. 623 That is,$\baseof{C} = R$. 625$\qed$627 \subsection{Coherence and Patch Inclusion} 629 Need to determine$C \haspatch \p$based on$L,M,R \haspatch \p$. 630 This involves considering$D \in \py$. 632 \subsubsection{For$L \nothaspatch \p, R \nothaspatch \p$:} 633$D \not\isin L \land D \not\isin R$.$C \not\in \py$(otherwise$L
634 \in \py$ie$L \haspatch \p$by Tip Self Inpatch). So$D \neq C$. 635 Applying$\merge$gives$D \not\isin C$i.e.$C \nothaspatch \p$. 637 \subsubsection{For$L \haspatch \p, R \haspatch \p$:} 638$D \isin L \equiv D \le L$and$D \isin R \equiv D \le R$. 639 (Likewise$D \isin X \equiv D \le X$and$D \isin Y \equiv D \le Y$.) 641 Consider$D = C$:$D \isin C$,$D \le C$, OK for$C \haspatch \p$. 643 For$D \neq C$:$D \le C \equiv D \le L \lor D \le R
644  \equiv D \isin L \lor D \isin R$. 645 (Likewise$D \le C \equiv D \le X \lor D \le Y$.) 647 Consider$D \neq C, D \isin X \land D \isin Y$: 648 By$\merge$,$D \isin C$. Also$D \le X$649 so$D \le C$. OK for$C \haspatch \p$. 651 Consider$D \neq C, D \not\isin X \land D \not\isin Y$: 652 By$\merge$,$D \not\isin C$. 653 And$D \not\le X \land D \not\le Y$so$D \not\le C$. 654 OK for$C \haspatch \p$. 656 Remaining case, wlog, is$D \not\isin X \land D \isin Y$. 657$D \not\le X$so$D \not\le M$so$D \not\isin M$. 658 Thus by$\merge$,$D \isin C$. And$D \le Y$so$D \le C$. 659 OK for$C \haspatch \p$. 661 So indeed$L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$. 663 \subsubsection{For (wlog)$X \not\haspatch \p, Y \haspatch \p$:} 665$M \haspatch \p \implies C \nothaspatch \p$. 666$M \nothaspatch \p \implies C \haspatch \p$. 668 \proofstarts 670 One of the Merge Ends conditions applies. 671 Recall that we are considering$D \in \py$. 672$D \isin Y \equiv D \le Y$.$D \not\isin X$. 673 We will show for each of 674 various cases that$D \isin C \equiv M \nothaspatch \p \land D \le C$675 (which suffices by definition of$\haspatch$and$\nothaspatch$). 677 Consider$D = C$: Thus$C \in \py, L \in \py$, and by Tip 678 Self Inpatch$L \haspatch \p$, so$L=Y, R=X$. By Tip Merge, 679$M=\baseof{L}$. So by Base Acyclic$D \not\isin M$, i.e. 680$M \nothaspatch \p$. And indeed$D \isin C$and$D \le C$. OK. 682 Consider$D \neq C, M \nothaspatch P, D \isin Y$: 683$D \le Y$so$D \le C$. 684$D \not\isin M$so by$\merge$,$D \isin C$. OK. 686 Consider$D \neq C, M \nothaspatch P, D \not\isin Y$: 687$D \not\le Y$. If$D \le X$then 688$D \in \pancsof{X}{\py}$, so by Addition Merge Ends and 689 Transitive Ancestors$D \le Y$--- a contradiction, so$D \not\le X$. 690 Thus$D \not\le C$. By$\merge$,$D \not\isin C$. OK. 692 Consider$D \neq C, M \haspatch P, D \isin Y$: 693$D \le Y$so$D \in \pancsof{Y}{\py}$so by Removal Merge Ends 694 and Transitive Ancestors$D \in \pancsof{M}{\py}$so$D \le M$. 695 Thus$D \isin M$. By$\merge$,$D \not\isin C$. OK. 697 Consider$D \neq C, M \haspatch P, D \not\isin Y$: 698 By$\merge$,$D \not\isin C$. OK. 700$\qed$702 \subsection{Base Acyclic} 704 This applies when$C \in \pn$. 705$C \in \pn$when$L \in \pn$so by Merge Acyclic,$R \nothaspatch \p$. 707 Consider some$D \in \py$. 709 By Base Acyclic of$L$,$D \not\isin L$. By the above,$D \not\isin
710 R$. And$D \neq C$. So$D \not\isin C$.$\qed$712 \subsection{Tip Contents} 714 We need worry only about$C \in \py$. 715 And$\patchof{C} = \patchof{L}$716 so$L \in \py$so$L \haspatch \p$. We will use the Unique Base 717 of$C$, and its Coherence and Patch Inclusion, as just proved. 719 Firstly we show$C \haspatch \p$: If$R \in \py$, then$R \haspatch
720 \p$and by Coherence/Inclusion$C \haspatch \p$. If$R \not\in \py$721 then by Tip Merge$M = \baseof{L}$so by Base Acyclic and definition 722 of$\nothaspatch$,$M \nothaspatch \p$. So by Coherence/Inclusion$C
723 \haspatch \p$(whether$R \haspatch \p$or$\nothaspatch$). 725 We will consider an arbitrary commit$D$726 and prove the Exclusive Tip Contents form. 728 \subsubsection{For$D \in \py$:} 729$C \haspatch \p$so by definition of$\haspatch$,$D \isin C \equiv D
730 \le C$. OK. 732 \subsubsection{For$D \not\in \py, R \not\in \py$:} 734$D \neq C$. By Tip Contents of$L$, 735$D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition, 736$D \isin L \equiv D \isin M$. So by definition of$\merge$,$D \isin
737 C \equiv D \isin R$. And$R = \baseof{C}$by Unique Base of$C$. 738 Thus$D \isin C \equiv D \isin \baseof{C}$. OK. 740 \subsubsection{For$D \not\in \py, R \in \py$:} 742$D \neq C$. 744 By Tip Contents 745$D \isin L \equiv D \isin \baseof{L}$and 746$D \isin R \equiv D \isin \baseof{R}$. 748 If$\baseof{L} = M$, trivially$D \isin M \equiv D \isin \baseof{L}.$749 Whereas if$\baseof{L} = \baseof{M}$, by definition of$\base$, 750$\patchof{M} = \patchof{L} = \py$, so by Tip Contents of$M$, 751$D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$. 753 So$D \isin M \equiv D \isin L$and by$\merge$, 754$D \isin C \equiv D \isin R$. But from Unique Base, 755$\baseof{C} = R$so$D \isin C \equiv D \isin \baseof{C}$. OK. 757$\qed$759 \subsection{Foreign Inclusion} 761 Consider some$D$s.t.$\patchof{D} = \bot$. 762 By Foreign Inclusion of$L, M, R$: 763$D \isin L \equiv D \le L$; 764$D \isin M \equiv D \le M$; 765$D \isin R \equiv D \le R$. 767 \subsubsection{For$D = C$:} 769$D \isin C$and$D \le C$. OK. 771 \subsubsection{For$D \neq C, D \isin M$:} 773 Thus$D \le M$so$D \le L$and$D \le R$so$D \isin L$and$D \isin
774 R$. So by$\merge$,$D \isin C$. And$D \le C$. OK. 776 \subsubsection{For$D \neq C, D \not\isin M, D \isin X$:} 778 By$\merge$,$D \isin C$. 779 And$D \isin X$means$D \le X$so$D \le C$. 780 OK. 782 \subsubsection{For$D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:} 784 By$\merge$,$D \not\isin C$. 785 And$D \not\le L, D \not\le R$so$D \not\le C$. 786 OK 788$\qed\$
790 \end{document}