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 Some (overlapping) alternative formulations:
 175
 176 $\displaystyle D \isin C \equiv
 177   \begin{cases}
 178     D \isin L \equiv D \isin R     : & D = C \lor D \isin L \\
 179     D \isin L \equiv D \isin R     : & D = C \lor D \isin R \\
 180     D \isin L \nequiv D \isin R  : & D = C \lor D \not\isin M \\
 181     D \isin M \equiv D \isin L     : & D = C \lor D \isin R \\
 182     D \isin M \equiv D \isin R     : & D = C \lor D \isin L \\
 183   \end{cases}
 184 $
 185
 186 \end{basedescript}
 187 \newpage
 188 \section{Invariants}
 189
 190 We maintain these each time we construct a new commit. \\
 191 \[ \eqn{No Replay:}{
 192   C \has D \implies C \ge D
 193 }\]
 194 \[\eqn{Unique Base:}{
 195  \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
 196 }\]
 197 \[\eqn{Tip Contents:}{
 198   \bigforall_{C \in \py} D \isin C \equiv
 199     { D \isin \baseof{C} \lor \atop
 200       (D \in \py \land D \le C) }
 201 }\]
 202 \[\eqn{Base Acyclic:}{
 203   \bigforall_{B \in \pn} D \isin B \implies D \notin \py
 204 }\]
 205 \[\eqn{Coherence:}{
 206   \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
 207 }\]
 208 \[\eqn{Foreign Inclusion:}{
 209   \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
 210 }\]
 211
 212 \section{Some lemmas}
 213
 214 \[ \eqn{Exclusive Tip Contents:}{
 215   \bigforall_{C \in \py}
 216     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
 217       \Bigr]
 218 }\]
 219 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
 220
 221 \proof{
 222 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
 223 So by Base Acyclic $D \isin B \implies D \notin \py$.
 224 }
 225 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
 226   \bigforall_{C \in \py} D \isin C \equiv
 227   \begin{cases}
 228     D \in \py : & D \le C \\
 229     D \not\in \py : & D \isin \baseof{C}
 230   \end{cases}
 231 }\]
 232
 233 \[ \eqn{Tip Self Inpatch:}{
 234   \bigforall_{C \in \py} C \haspatch \p
 235 }\]
 236 Ie, tip commits contain their own patch.
 237
 238 \proof{
 239 Apply Exclusive Tip Contents to some $D \in \py$:
 240 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
 241   D \isin C \equiv D \le C $
 242 }
 243
 244 \[ \eqn{Exact Ancestors:}{
 245   \bigforall_{ C \hasparents \set{R} }
 246   D \le C \equiv
 247     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
 248     \lor D = C
 249 }\]
 250
 251 \[ \eqn{Transitive Ancestors:}{
 252   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
 253   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
 254 }\]
 255
 256 \proof{
 257 The implication from right to left is trivial because
 258 $ \pends() \subset \pancs() $.
 259 For the implication from left to right:
 260 by the definition of $\mathcal E$,
 261 for every such $A$, either $A \in \pends()$ which implies
 262 $A \le M$ by the LHS directly,
 263 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
 264 in which case we repeat for $A'$.  Since there are finitely many
 265 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
 266 by the LHS.  And $A \le A''$.
 267 }
 268 \[ \eqn{Calculation Of Ends:}{
 269   \bigforall_{C \hasparents \set A}
 270     \pendsof{C}{\set P} =
 271        \left\{ E \Big|
 272            \Bigl[ \Largeexists_{A \in \set A}
 273                        E \in \pendsof{A}{\set P} \Bigr] \land
 274            \Bigl[ \Largenexists_{B \in \set A}
 275                        E \neq B \land E \le B \Bigr]
 276        \right\}
 277 }\]
 278 XXX proof TBD.
 279
 280 \subsection{No Replay for Merge Results}
 281
 282 If we are constructing $C$, with,
 283 \gathbegin
 284   \mergeof{C}{L}{M}{R}
 285 \gathnext
 286   L \le C
 287 \gathnext
 288   R \le C
 289 \end{gather}
 290 No Replay is preserved.  \proofstarts
 291
 292 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
 293
 294 \subsubsection{For $D \isin L \land D \isin R$:}
 295 $D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
 296
 297 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
 298 $D \not\isin C$.  OK.
 299
 300 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 301  \land D \not\isin M$:}
 302 $D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
 303 R$ so $D \le C$.  OK.
 304
 305 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 306  \land D \isin M$:}
 307 $D \not\isin C$.  OK.
 308
 309 $\qed$
 310
 311 \section{Commit annotation}
 312
 313 We annotate each Topbloke commit $C$ with:
 314 \gathbegin
 315  \patchof{C}
 316 \gathnext
 317  \baseof{C}, \text{ if } C \in \py
 318 \gathnext
 319  \bigforall_{\pa{Q}}
 320    \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
 321 \gathnext
 322  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
 323 \end{gather}
 324
 325 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
 326 make it wrong to make plain commits with git because the recorded $\pends$
 327 would have to be updated.  The annotation is not needed because
 328 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
 329
 330 \section{Simple commit}
 331
 332 A simple single-parent forward commit $C$ as made by git-commit.
 333 \begin{gather}
 334 \tag*{} C \hasparents \{ A \} \\
 335 \tag*{} \patchof{C} = \patchof{A} \\
 336 \tag*{} D \isin C \equiv D \isin A \lor D = C
 337 \end{gather}
 338 This also covers Topbloke-generated commits on plain git branches:
 339 Topbloke strips the metadata when exporting.
 340
 341 \subsection{No Replay}
 342 Trivial.
 343
 344 \subsection{Unique Base}
 345 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
 346
 347 \subsection{Tip Contents}
 348 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
 349 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
 350 Substitute into the contents of $C$:
 351 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
 352     \lor D = C \]
 353 Since $D = C \implies D \in \py$,
 354 and substituting in $\baseof{C}$, this gives:
 355 \[ D \isin C \equiv D \isin \baseof{C} \lor
 356     (D \in \py \land D \le A) \lor
 357     (D = C \land D \in \py) \]
 358 \[ \equiv D \isin \baseof{C} \lor
 359    [ D \in \py \land ( D \le A \lor D = C ) ] \]
 360 So by Exact Ancestors:
 361 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
 362 ) \]
 363 $\qed$
 364
 365 \subsection{Base Acyclic}
 366
 367 Need to consider only $A, C \in \pn$.
 368
 369 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 370
 371 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
 372 $A$, $D \isin C \implies D \not\in \py$. $\qed$
 373
 374 \subsection{Coherence and patch inclusion}
 375
 376 Need to consider $D \in \py$
 377
 378 \subsubsection{For $A \haspatch P, D = C$:}
 379
 380 Ancestors of $C$:
 381 $ D \le C $.
 382
 383 Contents of $C$:
 384 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 385
 386 \subsubsection{For $A \haspatch P, D \neq C$:}
 387 Ancestors: $ D \le C \equiv D \le A $.
 388
 389 Contents: $ D \isin C \equiv D \isin A \lor f $
 390 so $ D \isin C \equiv D \isin A $.
 391
 392 So:
 393 \[ A \haspatch P \implies C \haspatch P \]
 394
 395 \subsubsection{For $A \nothaspatch P$:}
 396
 397 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
 398 Thus $D \neq C$.
 399
 400 Now by contents of $A$, $D \notin A$, so $D \notin C$.
 401
 402 So:
 403 \[ A \nothaspatch P \implies C \nothaspatch P \]
 404 $\qed$
 405
 406 \subsection{Foreign inclusion:}
 407
 408 If $D = C$, trivial.  For $D \neq C$:
 409 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 410
 411 \section{Anticommit}
 412
 413 Given $L, R^+, R^-$ where
 414 $R^+ \in \pry, R^- = \baseof{R^+}$.
 415 Construct $C$ which has $\pr$ removed.
 416 Used for removing a branch dependency.
 417 \gathbegin
 418  C \hasparents \{ L \}
 419 \gathnext
 420  \patchof{C} = \patchof{L}
 421 \gathnext
 422  \mergeof{C}{L}{R^+}{R^-}
 423 \end{gather}
 424
 425 \subsection{Conditions}
 426
 427 \[ \eqn{ Unique Tip }{
 428  \pendsof{L}{\pry} = \{ R^+ \}
 429 }\]
 430 \[ \eqn{ Currently Included }{
 431  L \haspatch \pry
 432 }\]
 433 \[ \eqn{ Not Self }{
 434  L \not\in \{ R^+ \}
 435 }\]
 436
 437 \subsection{No Replay}
 438
 439 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
 440 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$ and No Replay for
 441 Merge Results applies. $\qed$
 442
 443 \subsection{Desired Contents}
 444
 445 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
 446 \proofstarts
 447
 448 \subsubsection{For $D = C$:}
 449
 450 Trivially $D \isin C$.  OK.
 451
 452 \subsubsection{For $D \neq C, D \not\le L$:}
 453
 454 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
 455 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
 456
 457 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
 458
 459 By Currently Included, $D \isin L$.
 460
 461 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
 462 by Unique Tip, $D \le R^+ \equiv D \le L$.
 463 So $D \isin R^+$.
 464
 465 By Base Acyclic, $D \not\isin R^-$.
 466
 467 Apply $\merge$: $D \not\isin C$.  OK.
 468
 469 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
 470
 471 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
 472
 473 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
 474
 475 $\qed$
 476
 477 \subsection{Unique Base}
 478
 479 Need to consider only $C \in \py$, ie $L \in \py$.
 480
 481 xxx tbd
 482
 483 xxx need to finish anticommit
 484
 485 \section{Merge}
 486
 487 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 488 \gathbegin
 489  C \hasparents \{ L, R \}
 490 \gathnext
 491  \patchof{C} = \patchof{L}
 492 \gathnext
 493  \mergeof{C}{L}{M}{R}
 494 \end{gather}
 495 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
 496
 497 \subsection{Conditions}
 498
 499 \[ \eqn{ Tip Merge }{
 500  L \in \py \implies
 501    \begin{cases}
 502       R \in \py : & \baseof{R} \ge \baseof{L}
 503               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
 504       R \in \pn : & M = \baseof{L} \\
 505       \text{otherwise} : & \false
 506    \end{cases}
 507 }\]
 508 \[ \eqn{ Merge Acyclic }{
 509     L \in \pn
 510    \implies
 511     R \nothaspatch \p
 512 }\]
 513 \[ \eqn{ Removal Merge Ends }{
 514     X \not\haspatch \p \land
 515     Y \haspatch \p \land
 516     M \haspatch \p
 517   \implies
 518     \pendsof{Y}{\py} = \pendsof{M}{\py}
 519 }\]
 520 \[ \eqn{ Addition Merge Ends }{
 521     X \not\haspatch \p \land
 522     Y \haspatch \p \land
 523     M \nothaspatch \p
 524    \implies \left[
 525     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
 526    \right]
 527 }\]
 528
 529 \subsection{Non-Topbloke merges}
 530
 531 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$.
 532 I.e. not only is it forbidden to merge into a Topbloke-controlled
 533 branch without Topbloke's assistance, it is also forbidden to
 534 merge any Topbloke-controlled branch into any plain git branch.
 535
 536 Given those conditions, Tip Merge and Merge Acyclic do not apply.
 537 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
 538 Merge Ends condition applies.  Good.
 539
 540 \subsection{No Replay}
 541
 542 See No Replay for Merge Results.
 543
 544 \subsection{Unique Base}
 545
 546 Need to consider only $C \in \py$, ie $L \in \py$,
 547 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 548 putative ancestor $A \in \pn$ and see whether $A \le C$.
 549
 550 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 551 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 552 Thus $A \le C \equiv A \le L \lor A \le R$.
 553
 554 By Unique Base of L and Transitive Ancestors,
 555 $A \le L \equiv A \le \baseof{L}$.
 556
 557 \subsubsection{For $R \in \py$:}
 558
 559 By Unique Base of $R$ and Transitive Ancestors,
 560 $A \le R \equiv A \le \baseof{R}$.
 561
 562 But by Tip Merge condition on $\baseof{R}$,
 563 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 564 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 565 Thus $A \le C \equiv A \le \baseof{R}$.
 566 That is, $\baseof{C} = \baseof{R}$.
 567
 568 \subsubsection{For $R \in \pn$:}
 569
 570 By Tip Merge condition on $R$ and since $M \le R$,
 571 $A \le \baseof{L} \implies A \le R$, so
 572 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 573 Thus $A \le C \equiv A \le R$.
 574 That is, $\baseof{C} = R$.
 575
 576 $\qed$
 577
 578 \subsection{Coherence and Patch Inclusion}
 579
 580 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
 581 This involves considering $D \in \py$.
 582
 583 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
 584 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
 585 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
 586 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
 587
 588 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
 589 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
 590 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
 591
 592 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
 593
 594 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
 595  \equiv D \isin L \lor D \isin R$.
 596 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
 597
 598 Consider $D \neq C, D \isin X \land D \isin Y$:
 599 By $\merge$, $D \isin C$.  Also $D \le X$
 600 so $D \le C$.  OK for $C \haspatch \p$.
 601
 602 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
 603 By $\merge$, $D \not\isin C$.
 604 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
 605 OK for $C \haspatch \p$.
 606
 607 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
 608 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
 609 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
 610 OK for $C \haspatch \p$.
 611
 612 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
 613
 614 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
 615
 616 $C \haspatch \p \equiv M \nothaspatch \p$.
 617
 618 \proofstarts
 619
 620 One of the Merge Ends conditions applies.
 621 Recall that we are considering $D \in \py$.
 622 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
 623 We will show for each of
 624 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
 625 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
 626
 627 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
 628 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
 629 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
 630 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
 631
 632 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
 633 $D \le Y$ so $D \le C$.
 634 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
 635
 636 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
 637 $D \not\le Y$.  If $D \le X$ then
 638 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
 639 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
 640 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
 641
 642 Consider $D \neq C, M \haspatch P, D \isin Y$:
 643 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
 644 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
 645 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
 646
 647 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
 648 By $\merge$, $D \not\isin C$.  OK.
 649
 650 $\qed$
 651
 652 \subsection{Base Acyclic}
 653
 654 This applies when $C \in \pn$.
 655 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
 656
 657 Consider some $D \in \py$.
 658
 659 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
 660 R$.  And $D \neq C$.  So $D \not\isin C$.  $\qed$
 661
 662 \subsection{Tip Contents}
 663
 664 We need worry only about $C \in \py$.
 665 And $\patchof{C} = \patchof{L}$
 666 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
 667 of $C$, and its Coherence and Patch Inclusion, as just proved.
 668
 669 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
 670 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
 671 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
 672 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
 673 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
 674
 675 We will consider an arbitrary commit $D$
 676 and prove the Exclusive Tip Contents form.
 677
 678 \subsubsection{For $D \in \py$:}
 679 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
 680 \le C$.  OK.
 681
 682 \subsubsection{For $D \not\in \py, R \not\in \py$:}
 683
 684 $D \neq C$.  By Tip Contents of $L$,
 685 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
 686 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
 687 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
 688 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
 689
 690 \subsubsection{For $D \not\in \py, R \in \py$:}
 691
 692 $D \neq C$.
 693
 694 By Tip Contents
 695 $D \isin L \equiv D \isin \baseof{L}$ and
 696 $D \isin R \equiv D \isin \baseof{R}$.
 697
 698 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
 699 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
 700 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
 701 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
 702
 703 So $D \isin M \equiv D \isin L$ and by $\merge$,
 704 $D \isin C \equiv D \isin R$.  But from Unique Base,
 705 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
 706
 707 $\qed$
 708
 709 xxx up to here, need to prove other things about merges
 710
 711 \end{document}