article.tex

   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}
  10
  11 \renewcommand{\ge}{\geqslant}
  12 \renewcommand{\le}{\leqslant}
  13 \newcommand{\nge}{\ngeqslant}
  14 \newcommand{\nle}{\nleqslant}
  15
  16 \newcommand{\has}{\sqsupseteq}
  17 \newcommand{\isin}{\sqsubseteq}
  18
  19 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
  20 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
  21 \newcommand{\haspatch}{\sqSupset}
  22 \newcommand{\patchisin}{\sqSubset}
  23
  24         \newif\ifhidehack\hidehackfalse
  25         \DeclareRobustCommand\hidefromedef[2]{%
  26           \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
  27         \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
  28
  29 \newcommand{\set}[1]{\mathbb{#1}}
  30 \newcommand{\pay}[1]{\pa{#1}^+}
  31 \newcommand{\pan}[1]{\pa{#1}^-}
  32
  33 \newcommand{\p}{\pa{P}}
  34 \newcommand{\py}{\pay{P}}
  35 \newcommand{\pn}{\pan{P}}
  36
  37 \newcommand{\pr}{\pa{R}}
  38 \newcommand{\pry}{\pay{R}}
  39 \newcommand{\prn}{\pan{R}}
  40
  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}}
  46
  47 \renewcommand{\implies}{\Rightarrow}
  48 \renewcommand{\equiv}{\Leftrightarrow}
  49 \renewcommand{\nequiv}{\nLeftrightarrow}
  50 \renewcommand{\land}{\wedge}
  51 \renewcommand{\lor}{\vee}
  52
  53 \newcommand{\pancs}{{\mathcal A}}
  54 \newcommand{\pends}{{\mathcal E}}
  55
  56 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
  57 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
  58
  59 \newcommand{\merge}{{\mathcal M}}
  60 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
  61 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
  62
  63 \newcommand{\patch}{{\mathcal P}}
  64 \newcommand{\base}{{\mathcal B}}
  65
  66 \newcommand{\patchof}[1]{\patch ( #1 ) }
  67 \newcommand{\baseof}[1]{\base ( #1 ) }
  68
  69 \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
  70 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
  71
  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 }
  80
  81 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
  82 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
  83
  84 \newcommand{\qed}{\square}
  85 \newcommand{\proofstarts}{{\it Proof:}}
  86 \newcommand{\proof}[1]{\proofstarts #1 $\qed$}
  87
  88 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
  89 \newcommand{\gathnext}{\\ \tag*{}}
  90
  91 \newcommand{\true}{t}
  92 \newcommand{\false}{f}
  93
  94 \begin{document}
  95
  96 \section{Notation}
  97
  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$.
 105
 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 $.
 110
 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.
 119
 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:
 126
 127 \item[ $ \patchof{ C } $ ]
 128 Either $\p$ s.t. $ C \in \p $, or $\bot$.
 129 A function from commits to patches' sets $\p$.
 130
 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$.
 135
 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}$.
 141
 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.
 146
 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$.
 150
 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$.
 154
 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.
 162
 163 \item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
 164 The contents of a git merge result:
 165
 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 $
 173
 174 \end{basedescript}
 175 \newpage
 176 \section{Invariants}
 177
 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 }\]
 199
 200 \section{Some lemmas}
 201
 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
 215
 216   Original definition is symmetrical in $L$ and $R$.
 217 }
 218
 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.
 225
 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 }\]
 237
 238 \[ \eqn{Tip Self Inpatch:}{
 239   \bigforall_{C \in \py} C \haspatch \p
 240 }\]
 241 Ie, tip commits contain their own patch.
 242
 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 }
 248
 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 }\]
 255 xxx proof tbd
 256
 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]
 260 }\]
 261
 262 \proof{
 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''$.
 273 }
 274
 275 \[ \eqn{Calculation Of Ends:}{
 276   \bigforall_{C \hasparents \set A}
 277     \pendsof{C}{\set P} =
 278       \begin{cases}
 279        C \in \p : & \{ C \}
 280       \\
 281        C \not\in \p : & \displaystyle
 282        \left\{ E \Big|
 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]
 287        \right\}
 288       \end{cases}
 289 }\]
 290 xxx proof tbd
 291
 292 \subsection{No Replay for Merge Results}
 293
 294 If we are constructing $C$, with,
 295 \gathbegin
 296   \mergeof{C}{L}{M}{R}
 297 \gathnext
 298   L \le C
 299 \gathnext
 300   R \le C
 301 \end{gather}
 302 No Replay is preserved.  \proofstarts
 303
 304 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
 305
 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.
 308
 309 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
 310 $D \not\isin C$.  OK.
 311
 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
 315 R$ so $D \le C$.  OK.
 316
 317 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 318  \land D \isin M$:}
 319 $D \not\isin C$.  OK.
 320
 321 $\qed$
 322
 323 \section{Commit annotation}
 324
 325 We annotate each Topbloke commit $C$ with:
 326 \gathbegin
 327  \patchof{C}
 328 \gathnext
 329  \baseof{C}, \text{ if } C \in \py
 330 \gathnext
 331  \bigforall_{\pa{Q}}
 332    \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
 333 \gathnext
 334  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
 335 \end{gather}
 336
 337 $\patchof{C}$, for each kind of Topbloke-generated commit, is stated
 338 in the summary in the section for that kind of commit.
 339
 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.
 342
 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}$
 345 is in stated
 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.
 349
 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\}$.
 356
 357 \section{Simple commit}
 358
 359 A simple single-parent forward commit $C$ as made by git-commit.
 360 \begin{gather}
 361 \tag*{} C \hasparents \{ A \} \\
 362 \tag*{} \patchof{C} = \patchof{A} \\
 363 \tag*{} D \isin C \equiv D \isin A \lor D = C
 364 \end{gather}
 365 This also covers Topbloke-generated commits on plain git branches:
 366 Topbloke strips the metadata when exporting.
 367
 368 \subsection{No Replay}
 369 Trivial.
 370
 371 \subsection{Unique Base}
 372 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
 373
 374 \subsection{Tip Contents}
 375 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
 376 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
 377 Substitute into the contents of $C$:
 378 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
 379     \lor D = C \]
 380 Since $D = C \implies D \in \py$,
 381 and substituting in $\baseof{C}$, this gives:
 382 \[ D \isin C \equiv D \isin \baseof{C} \lor
 383     (D \in \py \land D \le A) \lor
 384     (D = C \land D \in \py) \]
 385 \[ \equiv D \isin \baseof{C} \lor
 386    [ D \in \py \land ( D \le A \lor D = C ) ] \]
 387 So by Exact Ancestors:
 388 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
 389 ) \]
 390 $\qed$
 391
 392 \subsection{Base Acyclic}
 393
 394 Need to consider only $A, C \in \pn$.
 395
 396 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 397
 398 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
 399 $A$, $D \isin C \implies D \not\in \py$. $\qed$
 400
 401 \subsection{Coherence and patch inclusion}
 402
 403 Need to consider $D \in \py$
 404
 405 \subsubsection{For $A \haspatch P, D = C$:}
 406
 407 Ancestors of $C$:
 408 $ D \le C $.
 409
 410 Contents of $C$:
 411 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 412
 413 \subsubsection{For $A \haspatch P, D \neq C$:}
 414 Ancestors: $ D \le C \equiv D \le A $.
 415
 416 Contents: $ D \isin C \equiv D \isin A \lor f $
 417 so $ D \isin C \equiv D \isin A $.
 418
 419 So:
 420 \[ A \haspatch P \implies C \haspatch P \]
 421
 422 \subsubsection{For $A \nothaspatch P$:}
 423
 424 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
 425 Thus $D \neq C$.
 426
 427 Now by contents of $A$, $D \notin A$, so $D \notin C$.
 428
 429 So:
 430 \[ A \nothaspatch P \implies C \nothaspatch P \]
 431 $\qed$
 432
 433 \subsection{Foreign inclusion:}
 434
 435 If $D = C$, trivial.  For $D \neq C$:
 436 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 437
 438 \section{Anticommit}
 439
 440 Given $L, R^+, R^-$ where
 441 $R^+ \in \pry, R^- = \baseof{R^+}$.
 442 Construct $C$ which has $\pr$ removed.
 443 Used for removing a branch dependency.
 444 \gathbegin
 445  C \hasparents \{ L \}
 446 \gathnext
 447  \patchof{C} = \patchof{L}
 448 \gathnext
 449  \mergeof{C}{L}{R^+}{R^-}
 450 \end{gather}
 451
 452 \subsection{Conditions}
 453
 454 \[ \eqn{ Into Base }{
 455  L \in \pn
 456 }\]
 457 \[ \eqn{ Unique Tip }{
 458  \pendsof{L}{\pry} = \{ R^+ \}
 459 }\]
 460 \[ \eqn{ Currently Included }{
 461  L \haspatch \pry
 462 }\]
 463
 464 \subsection{Ordering of ${L, R^+, R^-}$:}
 465
 466 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
 467 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$.
 468
 469 (Note that the merge base $R^+ \not\le R^-$, i.e. the merge base is
 470 later than one of the branches to be merged.)
 471
 472 \subsection{No Replay}
 473
 474 No Replay for Merge Results applies.  $\qed$
 475
 476 \subsection{Desired Contents}
 477
 478 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
 479 \proofstarts
 480
 481 \subsubsection{For $D = C$:}
 482
 483 Trivially $D \isin C$.  OK.
 484
 485 \subsubsection{For $D \neq C, D \not\le L$:}
 486
 487 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
 488 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
 489
 490 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
 491
 492 By Currently Included, $D \isin L$.
 493
 494 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
 495 by Unique Tip, $D \le R^+ \equiv D \le L$.
 496 So $D \isin R^+$.
 497
 498 By Base Acyclic, $D \not\isin R^-$.
 499
 500 Apply $\merge$: $D \not\isin C$.  OK.
 501
 502 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
 503
 504 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
 505
 506 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
 507
 508 $\qed$
 509
 510 \subsection{Unique Base}
 511
 512 Into Base means that $C \in \pn$, so Unique Base is not
 513 applicable. $\qed$
 514
 515 \subsection{Tip Contents}
 516
 517 Again, not applicable. $\qed$
 518
 519 \subsection{Base Acyclic}
 520
 521 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
 522 And by Into Base $C \not\in \py$.
 523 Now from Desired Contents, above, $D \isin C
 524 \implies D \isin L \lor D = C$, which thus
 525 $\implies D \not\in \py$.  $\qed$.
 526
 527 \subsection{Coherence and Patch Inclusion}
 528
 529 Need to consider some $D \in \py$.  By Into Base, $D \neq C$.
 530
 531 \subsubsection{For $\p = \pr$:}
 532 By Desired Contents, above, $D \not\isin C$.
 533 So $C \nothaspatch \pr$.
 534
 535 \subsubsection{For $\p \neq \pr$:}
 536 By Desired Contents, $D \isin C \equiv D \isin L$
 537 (since $D \in \py$ so $D \not\in \pry$).
 538
 539 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
 540 So $L \nothaspatch \p \implies C \nothaspatch \p$.
 541
 542 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
 543 so $L \haspatch \p \implies C \haspatch \p$.
 544
 545 \section{Foreign Inclusion}
 546
 547 Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
 548 So by Desired Contents $D \isin C \equiv D \isin L$.
 549 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
 550
 551 And $D \le C \equiv D \le L$.
 552 Thus $D \isin C \equiv D \le C$.  $\qed$
 553
 554 \section{Merge}
 555
 556 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 557 \gathbegin
 558  C \hasparents \{ L, R \}
 559 \gathnext
 560  \patchof{C} = \patchof{L}
 561 \gathnext
 562  \mergeof{C}{L}{M}{R}
 563 \end{gather}
 564 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
 565
 566 \subsection{Conditions}
 567
 568 \[ \eqn{ Tip Merge }{
 569  L \in \py \implies
 570    \begin{cases}
 571       R \in \py : & \baseof{R} \ge \baseof{L}
 572               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
 573       R \in \pn : & M = \baseof{L} \\
 574       \text{otherwise} : & \false
 575    \end{cases}
 576 }\]
 577 \[ \eqn{ Merge Acyclic }{
 578     L \in \pn
 579    \implies
 580     R \nothaspatch \p
 581 }\]
 582 \[ \eqn{ Removal Merge Ends }{
 583     X \not\haspatch \p \land
 584     Y \haspatch \p \land
 585     M \haspatch \p
 586   \implies
 587     \pendsof{Y}{\py} = \pendsof{M}{\py}
 588 }\]
 589 \[ \eqn{ Addition Merge Ends }{
 590     X \not\haspatch \p \land
 591     Y \haspatch \p \land
 592     M \nothaspatch \p
 593    \implies \left[
 594     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
 595    \right]
 596 }\]
 597
 598 \subsection{Non-Topbloke merges}
 599
 600 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$.
 601 I.e. not only is it forbidden to merge into a Topbloke-controlled
 602 branch without Topbloke's assistance, it is also forbidden to
 603 merge any Topbloke-controlled branch into any plain git branch.
 604
 605 Given those conditions, Tip Merge and Merge Acyclic do not apply.
 606 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
 607 Merge Ends condition applies.  Good.
 608
 609 \subsection{No Replay}
 610
 611 No Replay for Merge Results applies.  $\qed$
 612
 613 \subsection{Unique Base}
 614
 615 Need to consider only $C \in \py$, ie $L \in \py$,
 616 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 617 putative ancestor $A \in \pn$ and see whether $A \le C$.
 618
 619 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 620 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 621 Thus $A \le C \equiv A \le L \lor A \le R$.
 622
 623 By Unique Base of L and Transitive Ancestors,
 624 $A \le L \equiv A \le \baseof{L}$.
 625
 626 \subsubsection{For $R \in \py$:}
 627
 628 By Unique Base of $R$ and Transitive Ancestors,
 629 $A \le R \equiv A \le \baseof{R}$.
 630
 631 But by Tip Merge condition on $\baseof{R}$,
 632 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 633 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 634 Thus $A \le C \equiv A \le \baseof{R}$.
 635 That is, $\baseof{C} = \baseof{R}$.
 636
 637 \subsubsection{For $R \in \pn$:}
 638
 639 By Tip Merge condition on $R$ and since $M \le R$,
 640 $A \le \baseof{L} \implies A \le R$, so
 641 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 642 Thus $A \le C \equiv A \le R$.
 643 That is, $\baseof{C} = R$.
 644
 645 $\qed$
 646
 647 \subsection{Coherence and Patch Inclusion}
 648
 649 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
 650 This involves considering $D \in \py$.
 651
 652 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
 653 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
 654 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
 655 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
 656
 657 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
 658 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
 659 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
 660
 661 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
 662
 663 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
 664  \equiv D \isin L \lor D \isin R$.
 665 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
 666
 667 Consider $D \neq C, D \isin X \land D \isin Y$:
 668 By $\merge$, $D \isin C$.  Also $D \le X$
 669 so $D \le C$.  OK for $C \haspatch \p$.
 670
 671 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
 672 By $\merge$, $D \not\isin C$.
 673 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
 674 OK for $C \haspatch \p$.
 675
 676 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
 677 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
 678 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
 679 OK for $C \haspatch \p$.
 680
 681 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
 682
 683 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
 684
 685 $M \haspatch \p \implies C \nothaspatch \p$.
 686 $M \nothaspatch \p \implies C \haspatch \p$.
 687
 688 \proofstarts
 689
 690 One of the Merge Ends conditions applies.
 691 Recall that we are considering $D \in \py$.
 692 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
 693 We will show for each of
 694 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
 695 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
 696
 697 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
 698 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
 699 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
 700 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
 701
 702 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
 703 $D \le Y$ so $D \le C$.
 704 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
 705
 706 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
 707 $D \not\le Y$.  If $D \le X$ then
 708 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
 709 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
 710 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
 711
 712 Consider $D \neq C, M \haspatch P, D \isin Y$:
 713 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
 714 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
 715 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
 716
 717 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
 718 By $\merge$, $D \not\isin C$.  OK.
 719
 720 $\qed$
 721
 722 \subsection{Base Acyclic}
 723
 724 This applies when $C \in \pn$.
 725 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
 726
 727 Consider some $D \in \py$.
 728
 729 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
 730 R$.  And $D \neq C$.  So $D \not\isin C$.  $\qed$
 731
 732 \subsection{Tip Contents}
 733
 734 We need worry only about $C \in \py$.
 735 And $\patchof{C} = \patchof{L}$
 736 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
 737 of $C$, and its Coherence and Patch Inclusion, as just proved.
 738
 739 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
 740 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
 741 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
 742 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
 743 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
 744
 745 We will consider an arbitrary commit $D$
 746 and prove the Exclusive Tip Contents form.
 747
 748 \subsubsection{For $D \in \py$:}
 749 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
 750 \le C$.  OK.
 751
 752 \subsubsection{For $D \not\in \py, R \not\in \py$:}
 753
 754 $D \neq C$.  By Tip Contents of $L$,
 755 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
 756 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
 757 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
 758 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
 759
 760 \subsubsection{For $D \not\in \py, R \in \py$:}
 761
 762 $D \neq C$.
 763
 764 By Tip Contents
 765 $D \isin L \equiv D \isin \baseof{L}$ and
 766 $D \isin R \equiv D \isin \baseof{R}$.
 767
 768 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
 769 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
 770 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
 771 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
 772
 773 So $D \isin M \equiv D \isin L$ and by $\merge$,
 774 $D \isin C \equiv D \isin R$.  But from Unique Base,
 775 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
 776
 777 $\qed$
 778
 779 \subsection{Foreign Inclusion}
 780
 781 Consider some $D$ s.t. $\patchof{D} = \bot$.
 782 By Foreign Inclusion of $L, M, R$:
 783 $D \isin L \equiv D \le L$;
 784 $D \isin M \equiv D \le M$;
 785 $D \isin R \equiv D \le R$.
 786
 787 \subsubsection{For $D = C$:}
 788
 789 $D \isin C$ and $D \le C$.  OK.
 790
 791 \subsubsection{For $D \neq C, D \isin M$:}
 792
 793 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
 794 R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.
 795
 796 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
 797
 798 By $\merge$, $D \isin C$.
 799 And $D \isin X$ means $D \le X$ so $D \le C$.
 800 OK.
 801
 802 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
 803
 804 By $\merge$, $D \not\isin C$.
 805 And $D \not\le L, D \not\le R$ so $D \not\le C$.
 806 OK
 807
 808 $\qed$
 809
 810 \end{document}