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 : & M = \baseof{L} \\
 500       \text{otherwise} : & \false
 501    \end{cases}
 502 }\]
 503 \[ \eqn{ Merge Acyclic }{
 504     L \in \pn
 505    \implies
 506     R \nothaspatch \p
 507 }\]
 508 \[ \eqn{ Removal Merge Ends }{
 509     X \not\haspatch \p \land
 510     Y \haspatch \p \land
 511     M \haspatch \p
 512   \implies
 513     \pendsof{Y}{\py} = \pendsof{M}{\py}
 514 }\]
 515 \[ \eqn{ Addition Merge Ends }{
 516     X \not\haspatch \p \land
 517     Y \haspatch \p \land
 518     M \nothaspatch \p
 519    \implies \left[
 520     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
 521    \right]
 522 }\]
 523
 524 \subsection{No Replay}
 525
 526 See No Replay for Merge Results.
 527
 528 \subsection{Unique Base}
 529
 530 Need to consider only $C \in \py$, ie $L \in \py$,
 531 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 532 putative ancestor $A \in \pn$ and see whether $A \le C$.
 533
 534 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 535 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 536 Thus $A \le C \equiv A \le L \lor A \le R$.
 537
 538 By Unique Base of L and Transitive Ancestors,
 539 $A \le L \equiv A \le \baseof{L}$.
 540
 541 \subsubsection{For $R \in \py$:}
 542
 543 By Unique Base of $R$ and Transitive Ancestors,
 544 $A \le R \equiv A \le \baseof{R}$.
 545
 546 But by Tip Merge condition on $\baseof{R}$,
 547 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 548 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 549 Thus $A \le C \equiv A \le \baseof{R}$.
 550 That is, $\baseof{C} = \baseof{R}$.
 551
 552 \subsubsection{For $R \in \pn$:}
 553
 554 By Tip Merge condition on $R$ and since $M \le R$,
 555 $A \le \baseof{L} \implies A \le R$, so
 556 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 557 Thus $A \le C \equiv A \le R$.
 558 That is, $\baseof{C} = R$.
 559
 560 $\qed$
 561
 562 \subsection{Coherence and patch inclusion}
 563
 564 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
 565 This involves considering $D \in \py$.
 566
 567 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
 568 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
 569 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
 570 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
 571
 572 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
 573 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
 574 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
 575
 576 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
 577
 578 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
 579  \equiv D \isin L \lor D \isin R$.
 580 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
 581
 582 Consider $D \neq C, D \isin X \land D \isin Y$:
 583 By $\merge$, $D \isin C$.  Also $D \le X$
 584 so $D \le C$.  OK for $C \haspatch \p$.
 585
 586 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
 587 By $\merge$, $D \not\isin C$.
 588 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
 589 OK for $C \haspatch \p$.
 590
 591 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
 592 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
 593 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
 594 OK for $C \haspatch \p$.
 595
 596 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
 597
 598 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
 599
 600 $C \haspatch \p \equiv M \nothaspatch \p$.
 601
 602 \proofstarts
 603
 604 One of the Merge Ends conditions applies.
 605 Recall that we are considering $D \in \py$.
 606 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
 607 We will show for each of
 608 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
 609 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
 610
 611 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
 612 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
 613 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
 614 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
 615
 616 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
 617 $D \le Y$ so $D \le C$.
 618 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
 619
 620 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
 621 $D \not\le Y$.  If $D \le X$ then
 622 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
 623 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
 624 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
 625
 626 Consider $D \neq C, M \haspatch P, D \isin Y$:
 627 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
 628 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
 629 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
 630
 631 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
 632 By $\merge$, $D \not\isin C$.  OK.
 633
 634 $\qed$
 635
 636 \subsection{Base Acyclic}
 637
 638 This applies when $C \in \pn$.
 639 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
 640
 641 Consider some $D \in \py$.
 642
 643 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
 644 R$.  And $D \neq C$.  So $D \not\isin C$.  $\qed$
 645
 646 \subsection{Tip Contents}
 647
 648 We need worry only about $C \in \py$.
 649 And $\patchof{C} = \patchof{L}$
 650 so $L \in \py$ so $L \haspatch \p$.  We will use the unique base,
 651 and coherence and patch inclusion, of $C$ as just proved.
 652
 653 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
 654 \p$ and by coherence/inclusion $C \haspatch \p$ .  If $R \not\in \py$
 655 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
 656 of $\nothaspatch$, $M \nothaspatch \p$.  So by coherence/inclusion $C
 657 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
 658
 659 We will consider some $D$ and prove the Exclusive Tip Contents form.
 660
 661 \subsubsection{For $D \in \py$:}
 662 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
 663 \le C$.  OK.
 664
 665 \subsubsection{For $D \not\in \py, R \not\in \py$:}
 666
 667 $D \neq C$.  By Tip Contents of $L$,
 668 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
 669 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
 670 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
 671 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
 672
 673 \subsubsection{For $D \not\in \py, R \in \py$:}
 674
 675 xxx up to here
 676
 677 %D \in \py$:}
 678
 679
 680
 681 xxx the coherence is not that useful ?
 682
 683 $L \haspatch \p$ by
 684
 685 xxx need to recheck this
 686
 687 $C \in \py$ $C \haspatch P$ so $D \isin C \equiv D \le C$.  OK.
 688
 689 \subsubsection{For $L \in \py, D \not\in \py, R \in \py$:}
 690
 691 Tip Contents for $L$: $D \isin L \equiv D \isin \baseof{L}$.
 692
 693 Tip Contents for $R$: $D \isin R \equiv D \isin \baseof{R}$.
 694
 695 But by Tip Merge, $\baseof{R} \ge \baseof{L}$
 696
 697 \end{document}