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