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
 339 \subsection{No Replay}
 340 Trivial.
 341
 342 \subsection{Unique Base}
 343 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
 344
 345 \subsection{Tip Contents}
 346 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
 347 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
 348 Substitute into the contents of $C$:
 349 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
 350     \lor D = C \]
 351 Since $D = C \implies D \in \py$,
 352 and substituting in $\baseof{C}$, this gives:
 353 \[ D \isin C \equiv D \isin \baseof{C} \lor
 354     (D \in \py \land D \le A) \lor
 355     (D = C \land D \in \py) \]
 356 \[ \equiv D \isin \baseof{C} \lor
 357    [ D \in \py \land ( D \le A \lor D = C ) ] \]
 358 So by Exact Ancestors:
 359 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
 360 ) \]
 361 $\qed$
 362
 363 \subsection{Base Acyclic}
 364
 365 Need to consider only $A, C \in \pn$.
 366
 367 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 368
 369 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
 370 $A$, $D \isin C \implies D \not\in \py$. $\qed$
 371
 372 \subsection{Coherence and patch inclusion}
 373
 374 Need to consider $D \in \py$
 375
 376 \subsubsection{For $A \haspatch P, D = C$:}
 377
 378 Ancestors of $C$:
 379 $ D \le C $.
 380
 381 Contents of $C$:
 382 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 383
 384 \subsubsection{For $A \haspatch P, D \neq C$:}
 385 Ancestors: $ D \le C \equiv D \le A $.
 386
 387 Contents: $ D \isin C \equiv D \isin A \lor f $
 388 so $ D \isin C \equiv D \isin A $.
 389
 390 So:
 391 \[ A \haspatch P \implies C \haspatch P \]
 392
 393 \subsubsection{For $A \nothaspatch P$:}
 394
 395 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
 396 Thus $D \neq C$.
 397
 398 Now by contents of $A$, $D \notin A$, so $D \notin C$.
 399
 400 So:
 401 \[ A \nothaspatch P \implies C \nothaspatch P \]
 402 $\qed$
 403
 404 \subsection{Foreign inclusion:}
 405
 406 If $D = C$, trivial.  For $D \neq C$:
 407 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 408
 409 \section{Anticommit}
 410
 411 Given $L, R^+, R^-$ where
 412 $R^+ \in \pry, R^- = \baseof{R^+}$.
 413 Construct $C$ which has $\pr$ removed.
 414 Used for removing a branch dependency.
 415 \gathbegin
 416  C \hasparents \{ L \}
 417 \gathnext
 418  \patchof{C} = \patchof{L}
 419 \gathnext
 420  \mergeof{C}{L}{R^+}{R^-}
 421 \end{gather}
 422
 423 \subsection{Conditions}
 424
 425 \[ \eqn{ Unique Tip }{
 426  \pendsof{L}{\pry} = \{ R^+ \}
 427 }\]
 428 \[ \eqn{ Currently Included }{
 429  L \haspatch \pry
 430 }\]
 431 \[ \eqn{ Not Self }{
 432  L \not\in \{ R^+ \}
 433 }\]
 434
 435 \subsection{No Replay}
 436
 437 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
 438 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$ and No Replay for
 439 Merge Results applies. $\qed$
 440
 441 \subsection{Desired Contents}
 442
 443 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
 444 \proofstarts
 445
 446 \subsubsection{For $D = C$:}
 447
 448 Trivially $D \isin C$.  OK.
 449
 450 \subsubsection{For $D \neq C, D \not\le L$:}
 451
 452 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
 453 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
 454
 455 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
 456
 457 By Currently Included, $D \isin L$.
 458
 459 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
 460 by Unique Tip, $D \le R^+ \equiv D \le L$.
 461 So $D \isin R^+$.
 462
 463 By Base Acyclic, $D \not\isin R^-$.
 464
 465 Apply $\merge$: $D \not\isin C$.  OK.
 466
 467 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
 468
 469 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
 470
 471 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
 472
 473 $\qed$
 474
 475 \subsection{Unique Base}
 476
 477 Need to consider only $C \in \py$, ie $L \in \py$.
 478
 479 xxx tbd
 480
 481 xxx need to finish anticommit
 482
 483 \section{Merge}
 484
 485 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 486 \gathbegin
 487  C \hasparents \{ L, R \}
 488 \gathnext
 489  \patchof{C} = \patchof{L}
 490 \gathnext
 491  \mergeof{C}{L}{M}{R}
 492 \end{gather}
 493 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
 494
 495 \subsection{Conditions}
 496
 497 \[ \eqn{ Tip Merge }{
 498  L \in \py \implies
 499    \begin{cases}
 500       R \in \py : & \baseof{R} \ge \baseof{L}
 501               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
 502       R \in \pn : & M = \baseof{L} \\
 503       \text{otherwise} : & \false
 504    \end{cases}
 505 }\]
 506 \[ \eqn{ Merge Acyclic }{
 507     L \in \pn
 508    \implies
 509     R \nothaspatch \p
 510 }\]
 511 \[ \eqn{ Removal Merge Ends }{
 512     X \not\haspatch \p \land
 513     Y \haspatch \p \land
 514     M \haspatch \p
 515   \implies
 516     \pendsof{Y}{\py} = \pendsof{M}{\py}
 517 }\]
 518 \[ \eqn{ Addition Merge Ends }{
 519     X \not\haspatch \p \land
 520     Y \haspatch \p \land
 521     M \nothaspatch \p
 522    \implies \left[
 523     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
 524    \right]
 525 }\]
 526
 527 \subsection{No Replay}
 528
 529 See No Replay for Merge Results.
 530
 531 \subsection{Unique Base}
 532
 533 Need to consider only $C \in \py$, ie $L \in \py$,
 534 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 535 putative ancestor $A \in \pn$ and see whether $A \le C$.
 536
 537 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 538 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 539 Thus $A \le C \equiv A \le L \lor A \le R$.
 540
 541 By Unique Base of L and Transitive Ancestors,
 542 $A \le L \equiv A \le \baseof{L}$.
 543
 544 \subsubsection{For $R \in \py$:}
 545
 546 By Unique Base of $R$ and Transitive Ancestors,
 547 $A \le R \equiv A \le \baseof{R}$.
 548
 549 But by Tip Merge condition on $\baseof{R}$,
 550 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 551 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 552 Thus $A \le C \equiv A \le \baseof{R}$.
 553 That is, $\baseof{C} = \baseof{R}$.
 554
 555 \subsubsection{For $R \in \pn$:}
 556
 557 By Tip Merge condition on $R$ and since $M \le R$,
 558 $A \le \baseof{L} \implies A \le R$, so
 559 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 560 Thus $A \le C \equiv A \le R$.
 561 That is, $\baseof{C} = R$.
 562
 563 $\qed$
 564
 565 \subsection{Coherence and Patch Inclusion}
 566
 567 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
 568 This involves considering $D \in \py$.
 569
 570 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
 571 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
 572 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
 573 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
 574
 575 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
 576 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
 577 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
 578
 579 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
 580
 581 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
 582  \equiv D \isin L \lor D \isin R$.
 583 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
 584
 585 Consider $D \neq C, D \isin X \land D \isin Y$:
 586 By $\merge$, $D \isin C$.  Also $D \le X$
 587 so $D \le C$.  OK for $C \haspatch \p$.
 588
 589 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
 590 By $\merge$, $D \not\isin C$.
 591 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
 592 OK for $C \haspatch \p$.
 593
 594 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
 595 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
 596 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
 597 OK for $C \haspatch \p$.
 598
 599 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
 600
 601 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
 602
 603 $C \haspatch \p \equiv M \nothaspatch \p$.
 604
 605 \proofstarts
 606
 607 One of the Merge Ends conditions applies.
 608 Recall that we are considering $D \in \py$.
 609 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
 610 We will show for each of
 611 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
 612 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
 613
 614 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
 615 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
 616 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
 617 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
 618
 619 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
 620 $D \le Y$ so $D \le C$.
 621 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
 622
 623 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
 624 $D \not\le Y$.  If $D \le X$ then
 625 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
 626 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
 627 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
 628
 629 Consider $D \neq C, M \haspatch P, D \isin Y$:
 630 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
 631 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
 632 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
 633
 634 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
 635 By $\merge$, $D \not\isin C$.  OK.
 636
 637 $\qed$
 638
 639 \subsection{Base Acyclic}
 640
 641 This applies when $C \in \pn$.
 642 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
 643
 644 Consider some $D \in \py$.
 645
 646 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
 647 R$.  And $D \neq C$.  So $D \not\isin C$.  $\qed$
 648
 649 \subsection{Tip Contents}
 650
 651 We need worry only about $C \in \py$.
 652 And $\patchof{C} = \patchof{L}$
 653 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
 654 of $C$, and its Coherence and Patch Inclusion, as just proved.
 655
 656 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
 657 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
 658 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
 659 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
 660 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
 661
 662 We will consider an arbitrary commit $D$
 663 and prove the Exclusive Tip Contents form.
 664
 665 \subsubsection{For $D \in \py$:}
 666 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
 667 \le C$.  OK.
 668
 669 \subsubsection{For $D \not\in \py, R \not\in \py$:}
 670
 671 $D \neq C$.  By Tip Contents of $L$,
 672 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
 673 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
 674 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
 675 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
 676
 677 \subsubsection{For $D \not\in \py, R \in \py$:}
 678
 679 $D \neq C$.
 680
 681 By Tip Contents
 682 $D \isin L \equiv D \isin \baseof{L}$ and
 683 $D \isin R \equiv D \isin \baseof{R}$.
 684
 685 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
 686 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
 687 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
 688 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
 689
 690 So $D \isin M \equiv D \isin L$ and by $\merge$,
 691 $D \isin C \equiv D \isin R$.  But from Unique Base,
 692 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
 693
 694 $\qed$
 695
 696 xxx up to here, need to prove other things about merges
 697
 698 \end{document}