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