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 xxx proof tbd
 258
 259 \[ \eqn{Transitive Ancestors:}{
 260   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
 261   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
 262 }\]
 263
 264 \proof{
 265 The implication from right to left is trivial because
 266 $ \pends() \subset \pancs() $.
 267 For the implication from left to right:
 268 by the definition of $\mathcal E$,
 269 for every such $A$, either $A \in \pends()$ which implies
 270 $A \le M$ by the LHS directly,
 271 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
 272 in which case we repeat for $A'$.  Since there are finitely many
 273 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
 274 by the LHS.  And $A \le A''$.
 275 }
 276
 277 \[ \eqn{Calculation Of Ends:}{
 278   \bigforall_{C \hasparents \set A}
 279     \pendsof{C}{\set P} =
 280       \begin{cases}
 281        C \in \p : & \{ C \}
 282       \\
 283        C \not\in \p : & \displaystyle
 284        \left\{ E \Big|
 285            \Bigl[ \Largeexists_{A \in \set A}
 286                        E \in \pendsof{A}{\set P} \Bigr] \land
 287            \Bigl[ \Largenexists_{B \in \set A}
 288                        E \neq B \land E \le B \Bigr]
 289        \right\}
 290       \end{cases}
 291 }\]
 292 xxx proof tbd
 293
 294 \subsection{No Replay for Merge Results}
 295
 296 If we are constructing $C$, with,
 297 \gathbegin
 298   \mergeof{C}{L}{M}{R}
 299 \gathnext
 300   L \le C
 301 \gathnext
 302   R \le C
 303 \end{gather}
 304 No Replay is preserved.  \proofstarts
 305
 306 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
 307
 308 \subsubsection{For $D \isin L \land D \isin R$:}
 309 $D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
 310
 311 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
 312 $D \not\isin C$.  OK.
 313
 314 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 315  \land D \not\isin M$:}
 316 $D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
 317 R$ so $D \le C$.  OK.
 318
 319 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 320  \land D \isin M$:}
 321 $D \not\isin C$.  OK.
 322
 323 $\qed$
 324
 325 \section{Commit annotation}
 326
 327 xxx need to compute annotation for every commit type
 328
 329 We annotate each Topbloke commit $C$ with:
 330 \gathbegin
 331  \patchof{C}
 332 \gathnext
 333  \baseof{C}, \text{ if } C \in \py
 334 \gathnext
 335  \bigforall_{\pa{Q}}
 336    \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
 337 \gathnext
 338  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
 339 \end{gather}
 340
 341 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
 342 make it wrong to make plain commits with git because the recorded $\pends$
 343 would have to be updated.  The annotation is not needed because
 344 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
 345
 346 \section{Simple commit}
 347
 348 A simple single-parent forward commit $C$ as made by git-commit.
 349 \begin{gather}
 350 \tag*{} C \hasparents \{ A \} \\
 351 \tag*{} \patchof{C} = \patchof{A} \\
 352 \tag*{} D \isin C \equiv D \isin A \lor D = C
 353 \end{gather}
 354 This also covers Topbloke-generated commits on plain git branches:
 355 Topbloke strips the metadata when exporting.
 356
 357 \subsection{No Replay}
 358 Trivial.
 359
 360 \subsection{Unique Base}
 361 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
 362
 363 \subsection{Tip Contents}
 364 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
 365 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
 366 Substitute into the contents of $C$:
 367 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
 368     \lor D = C \]
 369 Since $D = C \implies D \in \py$,
 370 and substituting in $\baseof{C}$, this gives:
 371 \[ D \isin C \equiv D \isin \baseof{C} \lor
 372     (D \in \py \land D \le A) \lor
 373     (D = C \land D \in \py) \]
 374 \[ \equiv D \isin \baseof{C} \lor
 375    [ D \in \py \land ( D \le A \lor D = C ) ] \]
 376 So by Exact Ancestors:
 377 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
 378 ) \]
 379 $\qed$
 380
 381 \subsection{Base Acyclic}
 382
 383 Need to consider only $A, C \in \pn$.
 384
 385 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 386
 387 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
 388 $A$, $D \isin C \implies D \not\in \py$. $\qed$
 389
 390 \subsection{Coherence and patch inclusion}
 391
 392 Need to consider $D \in \py$
 393
 394 \subsubsection{For $A \haspatch P, D = C$:}
 395
 396 Ancestors of $C$:
 397 $ D \le C $.
 398
 399 Contents of $C$:
 400 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 401
 402 \subsubsection{For $A \haspatch P, D \neq C$:}
 403 Ancestors: $ D \le C \equiv D \le A $.
 404
 405 Contents: $ D \isin C \equiv D \isin A \lor f $
 406 so $ D \isin C \equiv D \isin A $.
 407
 408 So:
 409 \[ A \haspatch P \implies C \haspatch P \]
 410
 411 \subsubsection{For $A \nothaspatch P$:}
 412
 413 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
 414 Thus $D \neq C$.
 415
 416 Now by contents of $A$, $D \notin A$, so $D \notin C$.
 417
 418 So:
 419 \[ A \nothaspatch P \implies C \nothaspatch P \]
 420 $\qed$
 421
 422 \subsection{Foreign inclusion:}
 423
 424 If $D = C$, trivial.  For $D \neq C$:
 425 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 426
 427 \section{Anticommit}
 428
 429 Given $L, R^+, R^-$ where
 430 $R^+ \in \pry, R^- = \baseof{R^+}$.
 431 Construct $C$ which has $\pr$ removed.
 432 Used for removing a branch dependency.
 433 \gathbegin
 434  C \hasparents \{ L \}
 435 \gathnext
 436  \patchof{C} = \patchof{L}
 437 \gathnext
 438  \mergeof{C}{L}{R^+}{R^-}
 439 \end{gather}
 440
 441 \subsection{Conditions}
 442
 443 \[ \eqn{ Into Base }{
 444  L \in \pn
 445 }\]
 446 \[ \eqn{ Unique Tip }{
 447  \pendsof{L}{\pry} = \{ R^+ \}
 448 }\]
 449 \[ \eqn{ Currently Included }{
 450  L \haspatch \pry
 451 }\]
 452
 453 \subsection{Ordering of ${L, R^+, R^-}$:}
 454
 455 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
 456 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$.
 457
 458 (Note that the merge base $R^+ \not\le R^-$, i.e. the merge base is
 459 later than one of the branches to be merged.)
 460
 461 \subsection{No Replay}
 462
 463 No Replay for Merge Results applies.  $\qed$
 464
 465 \subsection{Desired Contents}
 466
 467 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
 468 \proofstarts
 469
 470 \subsubsection{For $D = C$:}
 471
 472 Trivially $D \isin C$.  OK.
 473
 474 \subsubsection{For $D \neq C, D \not\le L$:}
 475
 476 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
 477 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
 478
 479 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
 480
 481 By Currently Included, $D \isin L$.
 482
 483 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
 484 by Unique Tip, $D \le R^+ \equiv D \le L$.
 485 So $D \isin R^+$.
 486
 487 By Base Acyclic, $D \not\isin R^-$.
 488
 489 Apply $\merge$: $D \not\isin C$.  OK.
 490
 491 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
 492
 493 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
 494
 495 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
 496
 497 $\qed$
 498
 499 \subsection{Unique Base}
 500
 501 Into Base means that $C \in \pn$, so Unique Base is not
 502 applicable. $\qed$
 503
 504 \subsection{Tip Contents}
 505
 506 Again, not applicable. $\qed$
 507
 508 \subsection{Base Acyclic}
 509
 510 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
 511 And by Into Base $C \not\in \py$.
 512 Now from Desired Contents, above, $D \isin C
 513 \implies D \isin L \lor D = C$, which thus
 514 $\implies D \not\in \py$.  $\qed$.
 515
 516 \subsection{Coherence and Patch Inclusion}
 517
 518 Need to consider some $D \in \py$.  By Into Base, $D \neq C$.
 519
 520 \subsubsection{For $\p = \pr$:}
 521 By Desired Contents, above, $D \not\isin C$.
 522 So $C \nothaspatch \pr$.
 523
 524 \subsubsection{For $\p \neq \pr$:}
 525 By Desired Contents, $D \isin C \equiv D \isin L$
 526 (since $D \in \py$ so $D \not\in \pry$).
 527
 528 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
 529 So $L \nothaspatch \p \implies C \nothaspatch \p$.
 530
 531 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
 532 so $L \haspatch \p \implies C \haspatch \p$.
 533
 534 \section{Foreign Inclusion}
 535
 536 Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
 537 So by Desired Contents $D \isin C \equiv D \isin L$.
 538 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
 539
 540 And $D \le C \equiv D \le L$.
 541 Thus $D \isin C \equiv D \le C$.  $\qed$
 542
 543 \section{Merge}
 544
 545 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 546 \gathbegin
 547  C \hasparents \{ L, R \}
 548 \gathnext
 549  \patchof{C} = \patchof{L}
 550 \gathnext
 551  \mergeof{C}{L}{M}{R}
 552 \end{gather}
 553 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
 554
 555 \subsection{Conditions}
 556
 557 \[ \eqn{ Tip Merge }{
 558  L \in \py \implies
 559    \begin{cases}
 560       R \in \py : & \baseof{R} \ge \baseof{L}
 561               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
 562       R \in \pn : & M = \baseof{L} \\
 563       \text{otherwise} : & \false
 564    \end{cases}
 565 }\]
 566 \[ \eqn{ Merge Acyclic }{
 567     L \in \pn
 568    \implies
 569     R \nothaspatch \p
 570 }\]
 571 \[ \eqn{ Removal Merge Ends }{
 572     X \not\haspatch \p \land
 573     Y \haspatch \p \land
 574     M \haspatch \p
 575   \implies
 576     \pendsof{Y}{\py} = \pendsof{M}{\py}
 577 }\]
 578 \[ \eqn{ Addition Merge Ends }{
 579     X \not\haspatch \p \land
 580     Y \haspatch \p \land
 581     M \nothaspatch \p
 582    \implies \left[
 583     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
 584    \right]
 585 }\]
 586
 587 \subsection{Non-Topbloke merges}
 588
 589 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$.
 590 I.e. not only is it forbidden to merge into a Topbloke-controlled
 591 branch without Topbloke's assistance, it is also forbidden to
 592 merge any Topbloke-controlled branch into any plain git branch.
 593
 594 Given those conditions, Tip Merge and Merge Acyclic do not apply.
 595 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
 596 Merge Ends condition applies.  Good.
 597
 598 \subsection{No Replay}
 599
 600 No Replay for Merge Results applies.  $\qed$
 601
 602 \subsection{Unique Base}
 603
 604 Need to consider only $C \in \py$, ie $L \in \py$,
 605 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 606 putative ancestor $A \in \pn$ and see whether $A \le C$.
 607
 608 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 609 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 610 Thus $A \le C \equiv A \le L \lor A \le R$.
 611
 612 By Unique Base of L and Transitive Ancestors,
 613 $A \le L \equiv A \le \baseof{L}$.
 614
 615 \subsubsection{For $R \in \py$:}
 616
 617 By Unique Base of $R$ and Transitive Ancestors,
 618 $A \le R \equiv A \le \baseof{R}$.
 619
 620 But by Tip Merge condition on $\baseof{R}$,
 621 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 622 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 623 Thus $A \le C \equiv A \le \baseof{R}$.
 624 That is, $\baseof{C} = \baseof{R}$.
 625
 626 \subsubsection{For $R \in \pn$:}
 627
 628 By Tip Merge condition on $R$ and since $M \le R$,
 629 $A \le \baseof{L} \implies A \le R$, so
 630 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 631 Thus $A \le C \equiv A \le R$.
 632 That is, $\baseof{C} = R$.
 633
 634 $\qed$
 635
 636 \subsection{Coherence and Patch Inclusion}
 637
 638 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
 639 This involves considering $D \in \py$.
 640
 641 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
 642 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
 643 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
 644 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
 645
 646 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
 647 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
 648 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
 649
 650 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
 651
 652 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
 653  \equiv D \isin L \lor D \isin R$.
 654 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
 655
 656 Consider $D \neq C, D \isin X \land D \isin Y$:
 657 By $\merge$, $D \isin C$.  Also $D \le X$
 658 so $D \le C$.  OK for $C \haspatch \p$.
 659
 660 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
 661 By $\merge$, $D \not\isin C$.
 662 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
 663 OK for $C \haspatch \p$.
 664
 665 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
 666 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
 667 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
 668 OK for $C \haspatch \p$.
 669
 670 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
 671
 672 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
 673
 674 $M \haspatch \p \implies C \nothaspatch \p$.
 675 $M \nothaspatch \p \implies C \haspatch \p$.
 676
 677 \proofstarts
 678
 679 One of the Merge Ends conditions applies.
 680 Recall that we are considering $D \in \py$.
 681 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
 682 We will show for each of
 683 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
 684 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
 685
 686 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
 687 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
 688 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
 689 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
 690
 691 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
 692 $D \le Y$ so $D \le C$.
 693 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
 694
 695 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
 696 $D \not\le Y$.  If $D \le X$ then
 697 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
 698 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
 699 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
 700
 701 Consider $D \neq C, M \haspatch P, D \isin Y$:
 702 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
 703 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
 704 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
 705
 706 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
 707 By $\merge$, $D \not\isin C$.  OK.
 708
 709 $\qed$
 710
 711 \subsection{Base Acyclic}
 712
 713 This applies when $C \in \pn$.
 714 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
 715
 716 Consider some $D \in \py$.
 717
 718 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
 719 R$.  And $D \neq C$.  So $D \not\isin C$.  $\qed$
 720
 721 \subsection{Tip Contents}
 722
 723 We need worry only about $C \in \py$.
 724 And $\patchof{C} = \patchof{L}$
 725 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
 726 of $C$, and its Coherence and Patch Inclusion, as just proved.
 727
 728 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
 729 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
 730 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
 731 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
 732 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
 733
 734 We will consider an arbitrary commit $D$
 735 and prove the Exclusive Tip Contents form.
 736
 737 \subsubsection{For $D \in \py$:}
 738 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
 739 \le C$.  OK.
 740
 741 \subsubsection{For $D \not\in \py, R \not\in \py$:}
 742
 743 $D \neq C$.  By Tip Contents of $L$,
 744 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
 745 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
 746 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
 747 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
 748
 749 \subsubsection{For $D \not\in \py, R \in \py$:}
 750
 751 $D \neq C$.
 752
 753 By Tip Contents
 754 $D \isin L \equiv D \isin \baseof{L}$ and
 755 $D \isin R \equiv D \isin \baseof{R}$.
 756
 757 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
 758 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
 759 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
 760 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
 761
 762 So $D \isin M \equiv D \isin L$ and by $\merge$,
 763 $D \isin C \equiv D \isin R$.  But from Unique Base,
 764 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
 765
 766 $\qed$
 767
 768 \subsection{Foreign Inclusion}
 769
 770 Consider some $D$ s.t. $\patchof{D} = \bot$.
 771 By Foreign Inclusion of $L, M, R$:
 772 $D \isin L \equiv D \le L$;
 773 $D \isin M \equiv D \le M$;
 774 $D \isin R \equiv D \le R$.
 775
 776 \subsubsection{For $D = C$:}
 777
 778 $D \isin C$ and $D \le C$.  OK.
 779
 780 \subsubsection{For $D \neq C, D \isin M$:}
 781
 782 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
 783 R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.
 784
 785 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
 786
 787 By $\merge$, $D \isin C$.
 788 And $D \isin X$ means $D \le X$ so $D \le C$.
 789 OK.
 790
 791 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
 792
 793 By $\merge$, $D \not\isin C$.
 794 And $D \not\le L, D \not\le R$ so $D \not\le C$.
 795 OK
 796
 797 $\qed$
 798
 799 \end{document}