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