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
 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 }\]
 260
 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.
 284
 285 \subsection{No Replay for Merge Results}
 286
 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
 296
 297 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
 298
 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.
 301
 302 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
 303 $D \not\isin C$.  OK.
 304
 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.
 309
 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.
 313
 314 $\qed$
 315
 316 \section{Commit annotation}
 317
 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}
 329
 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\}$.
 334
 335 \section{Simple commit}
 336
 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.
 345
 346 \subsection{No Replay}
 347 Trivial.
 348
 349 \subsection{Unique Base}
 350 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
 351
 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$
 369
 370 \subsection{Base Acyclic}
 371
 372 Need to consider only $A, C \in \pn$.
 373
 374 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 375
 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$
 378
 379 \subsection{Coherence and patch inclusion}
 380
 381 Need to consider $D \in \py$
 382
 383 \subsubsection{For $A \haspatch P, D = C$:}
 384
 385 Ancestors of $C$:
 386 $ D \le C $.
 387
 388 Contents of $C$:
 389 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 390
 391 \subsubsection{For $A \haspatch P, D \neq C$:}
 392 Ancestors: $ D \le C \equiv D \le A $.
 393
 394 Contents: $ D \isin C \equiv D \isin A \lor f $
 395 so $ D \isin C \equiv D \isin A $.
 396
 397 So:
 398 \[ A \haspatch P \implies C \haspatch P \]
 399
 400 \subsubsection{For $A \nothaspatch P$:}
 401
 402 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
 403 Thus $D \neq C$.
 404
 405 Now by contents of $A$, $D \notin A$, so $D \notin C$.
 406
 407 So:
 408 \[ A \nothaspatch P \implies C \nothaspatch P \]
 409 $\qed$
 410
 411 \subsection{Foreign inclusion:}
 412
 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$
 415
 416 \section{Anticommit}
 417
 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}
 429
 430 \subsection{Conditions}
 431
 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 }\]
 441
 442 \subsection{Ordering of ${L, R^+, R^-}$:}
 443
 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$.
 446
 447 (Note that the merge base $R^+ \not\le R^-$, i.e. the merge base is
 448 later than one of the branches to be merged.)
 449
 450 \subsection{No Replay}
 451
 452 No Replay for Merge Results applies.  $\qed$
 453
 454 \subsection{Desired Contents}
 455
 456 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
 457 \proofstarts
 458
 459 \subsubsection{For $D = C$:}
 460
 461 Trivially $D \isin C$.  OK.
 462
 463 \subsubsection{For $D \neq C, D \not\le L$:}
 464
 465 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
 466 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
 467
 468 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
 469
 470 By Currently Included, $D \isin L$.
 471
 472 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
 473 by Unique Tip, $D \le R^+ \equiv D \le L$.
 474 So $D \isin R^+$.
 475
 476 By Base Acyclic, $D \not\isin R^-$.
 477
 478 Apply $\merge$: $D \not\isin C$.  OK.
 479
 480 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
 481
 482 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
 483
 484 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
 485
 486 $\qed$
 487
 488 \subsection{Unique Base}
 489
 490 Into Base means that $C \in \pn$, so Unique Base is not
 491 applicable. $\qed$
 492
 493 \subsection{Tip Contents}
 494
 495 Again, not applicable. $\qed$
 496
 497 \subsection{Base Acyclic}
 498
 499 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
 500 And by Into Base $C \not\in \py$.
 501 Now from Desired Contents, above, $D \isin C
 502 \implies D \isin L \lor D = C$, which thus
 503 $\implies D \not\in \py$.  $\qed$.
 504
 505 \subsection{Coherence and Patch Inclusion}
 506
 507 Need to consider some $D \in \py$.  By Into Base, $D \neq C$.
 508
 509 \subsubsection{For $\p = \pr$:}
 510 By Desired Contents, above, $D \not\isin C$.
 511 So $C \nothaspatch \pr$.
 512
 513 \subsubsection{For $\p \neq \pr$:}
 514 By Desired Contents, $D \isin C \equiv D \isin L$
 515 (since $D \in \py$ so $D \not\in \pry$).
 516
 517 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
 518 So $L \nothaspatch \p \implies C \nothaspatch \p$.
 519
 520 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
 521 so $L \haspatch \p \implies C \haspatch \p$.
 522
 523 \section{Foreign Inclusion}
 524
 525 Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
 526 So by Desired Contents $D \isin C \equiv D \isin L$.
 527 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
 528 So $D \isin C \equiv D \le L$.
 529
 530 xxx up to here
 531
 532 By Tip Contents of $R^+$, $D \isin R^+ \equiv D \isin \baseof{R^+}$
 533 i.e. $\equiv D \isin R^-$.
 534 So by $\merge$, $D \isin C \equiv D \isin L$.
 535
 536 Thus $D \isin C \equiv $
 537
 538 \section{Merge}
 539
 540 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 541 \gathbegin
 542  C \hasparents \{ L, R \}
 543 \gathnext
 544  \patchof{C} = \patchof{L}
 545 \gathnext
 546  \mergeof{C}{L}{M}{R}
 547 \end{gather}
 548 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
 549
 550 \subsection{Conditions}
 551
 552 \[ \eqn{ Tip Merge }{
 553  L \in \py \implies
 554    \begin{cases}
 555       R \in \py : & \baseof{R} \ge \baseof{L}
 556               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
 557       R \in \pn : & M = \baseof{L} \\
 558       \text{otherwise} : & \false
 559    \end{cases}
 560 }\]
 561 \[ \eqn{ Merge Acyclic }{
 562     L \in \pn
 563    \implies
 564     R \nothaspatch \p
 565 }\]
 566 \[ \eqn{ Removal Merge Ends }{
 567     X \not\haspatch \p \land
 568     Y \haspatch \p \land
 569     M \haspatch \p
 570   \implies
 571     \pendsof{Y}{\py} = \pendsof{M}{\py}
 572 }\]
 573 \[ \eqn{ Addition Merge Ends }{
 574     X \not\haspatch \p \land
 575     Y \haspatch \p \land
 576     M \nothaspatch \p
 577    \implies \left[
 578     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
 579    \right]
 580 }\]
 581
 582 \subsection{Non-Topbloke merges}
 583
 584 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$.
 585 I.e. not only is it forbidden to merge into a Topbloke-controlled
 586 branch without Topbloke's assistance, it is also forbidden to
 587 merge any Topbloke-controlled branch into any plain git branch.
 588
 589 Given those conditions, Tip Merge and Merge Acyclic do not apply.
 590 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
 591 Merge Ends condition applies.  Good.
 592
 593 \subsection{No Replay}
 594
 595 No Replay for Merge Results applies.  $\qed$
 596
 597 \subsection{Unique Base}
 598
 599 Need to consider only $C \in \py$, ie $L \in \py$,
 600 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 601 putative ancestor $A \in \pn$ and see whether $A \le C$.
 602
 603 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 604 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 605 Thus $A \le C \equiv A \le L \lor A \le R$.
 606
 607 By Unique Base of L and Transitive Ancestors,
 608 $A \le L \equiv A \le \baseof{L}$.
 609
 610 \subsubsection{For $R \in \py$:}
 611
 612 By Unique Base of $R$ and Transitive Ancestors,
 613 $A \le R \equiv A \le \baseof{R}$.
 614
 615 But by Tip Merge condition on $\baseof{R}$,
 616 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 617 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 618 Thus $A \le C \equiv A \le \baseof{R}$.
 619 That is, $\baseof{C} = \baseof{R}$.
 620
 621 \subsubsection{For $R \in \pn$:}
 622
 623 By Tip Merge condition on $R$ and since $M \le R$,
 624 $A \le \baseof{L} \implies A \le R$, so
 625 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 626 Thus $A \le C \equiv A \le R$.
 627 That is, $\baseof{C} = R$.
 628
 629 $\qed$
 630
 631 \subsection{Coherence and Patch Inclusion}
 632
 633 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
 634 This involves considering $D \in \py$.
 635
 636 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
 637 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
 638 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
 639 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
 640
 641 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
 642 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
 643 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
 644
 645 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
 646
 647 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
 648  \equiv D \isin L \lor D \isin R$.
 649 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
 650
 651 Consider $D \neq C, D \isin X \land D \isin Y$:
 652 By $\merge$, $D \isin C$.  Also $D \le X$
 653 so $D \le C$.  OK for $C \haspatch \p$.
 654
 655 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
 656 By $\merge$, $D \not\isin C$.
 657 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
 658 OK for $C \haspatch \p$.
 659
 660 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
 661 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
 662 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
 663 OK for $C \haspatch \p$.
 664
 665 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
 666
 667 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
 668
 669 $M \haspatch \p \implies C \nothaspatch \p$.
 670 $M \nothaspatch \p \implies C \haspatch \p$.
 671
 672 \proofstarts
 673
 674 One of the Merge Ends conditions applies.
 675 Recall that we are considering $D \in \py$.
 676 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
 677 We will show for each of
 678 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
 679 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
 680
 681 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
 682 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
 683 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
 684 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
 685
 686 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
 687 $D \le Y$ so $D \le C$.
 688 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
 689
 690 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
 691 $D \not\le Y$.  If $D \le X$ then
 692 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
 693 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
 694 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
 695
 696 Consider $D \neq C, M \haspatch P, D \isin Y$:
 697 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
 698 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
 699 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
 700
 701 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
 702 By $\merge$, $D \not\isin C$.  OK.
 703
 704 $\qed$
 705
 706 \subsection{Base Acyclic}
 707
 708 This applies when $C \in \pn$.
 709 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
 710
 711 Consider some $D \in \py$.
 712
 713 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
 714 R$.  And $D \neq C$.  So $D \not\isin C$.  $\qed$
 715
 716 \subsection{Tip Contents}
 717
 718 We need worry only about $C \in \py$.
 719 And $\patchof{C} = \patchof{L}$
 720 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
 721 of $C$, and its Coherence and Patch Inclusion, as just proved.
 722
 723 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
 724 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
 725 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
 726 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
 727 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
 728
 729 We will consider an arbitrary commit $D$
 730 and prove the Exclusive Tip Contents form.
 731
 732 \subsubsection{For $D \in \py$:}
 733 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
 734 \le C$.  OK.
 735
 736 \subsubsection{For $D \not\in \py, R \not\in \py$:}
 737
 738 $D \neq C$.  By Tip Contents of $L$,
 739 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
 740 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
 741 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
 742 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
 743
 744 \subsubsection{For $D \not\in \py, R \in \py$:}
 745
 746 $D \neq C$.
 747
 748 By Tip Contents
 749 $D \isin L \equiv D \isin \baseof{L}$ and
 750 $D \isin R \equiv D \isin \baseof{R}$.
 751
 752 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
 753 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
 754 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
 755 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
 756
 757 So $D \isin M \equiv D \isin L$ and by $\merge$,
 758 $D \isin C \equiv D \isin R$.  But from Unique Base,
 759 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
 760
 761 $\qed$
 762
 763 \subsection{Foreign Inclusion}
 764
 765 Consider some $D$ s.t. $\patchof{D} = \bot$.
 766 By Foreign Inclusion of $L, M, R$:
 767 $D \isin L \equiv D \le L$;
 768 $D \isin M \equiv D \le M$;
 769 $D \isin R \equiv D \le R$.
 770
 771 \subsubsection{For $D = C$:}
 772
 773 $D \isin C$ and $D \le C$.  OK.
 774
 775 \subsubsection{For $D \neq C, D \isin M$:}
 776
 777 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
 778 R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.
 779
 780 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
 781
 782 By $\merge$, $D \isin C$.
 783 And $D \isin X$ means $D \le X$ so $D \le C$.
 784 OK.
 785
 786 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
 787
 788 By $\merge$, $D \not\isin C$.
 789 And $D \not\le L, D \not\le R$ so $D \not\le C$.
 790 OK
 791
 792 $\qed$
 793
 794 \end{document}