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{\land}{\wedge}
  50 \renewcommand{\lor}{\vee}
  51
  52 \newcommand{\pancs}{{\mathcal A}}
  53 \newcommand{\pends}{{\mathcal E}}
  54
  55 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
  56 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
  57
  58 \newcommand{\merge}{{\mathcal M}}
  59 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
  60 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
  61
  62 \newcommand{\patch}{{\mathcal P}}
  63 \newcommand{\base}{{\mathcal B}}
  64
  65 \newcommand{\patchof}[1]{\patch ( #1 ) }
  66 \newcommand{\baseof}[1]{\base ( #1 ) }
  67
  68 \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
  69 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
  70
  71 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
  72 \newcommand{\bigforall}{%
  73   \mathop{\mathchoice%
  74     {\hbox{\huge$\forall$}}%
  75     {\hbox{\Large$\forall$}}%
  76     {\hbox{\normalsize$\forall$}}%
  77     {\hbox{\scriptsize$\forall$}}}%
  78 }
  79
  80 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
  81 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
  82
  83 \newcommand{\qed}{\square}
  84 \newcommand{\proofstarts}{{\it Proof:}}
  85 \newcommand{\proof}[1]{\proofstarts #1 $\qed$}
  86
  87 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
  88 \newcommand{\gathnext}{\\ \tag*{}}
  89
  90 \newcommand{\true}{t}
  91 \newcommand{\false}{f}
  92
  93 \begin{document}
  94
  95 \section{Notation}
  96
  97 \begin{basedescript}{
  98 \desclabelwidth{5em}
  99 \desclabelstyle{\nextlinelabel}
 100 }
 101 \item[ $ C \hasparents \set X $ ]
 102 The parents of commit $C$ are exactly the set
 103 $\set X$.
 104
 105 \item[ $ C \ge D $ ]
 106 $C$ is a descendant of $D$ in the git commit
 107 graph.  This is a partial order, namely the transitive closure of
 108 $ D \in \set X $ where $ C \hasparents \set X $.
 109
 110 \item[ $ C \has D $ ]
 111 Informally, the tree at commit $C$ contains the change
 112 made in commit $D$.  Does not take account of deliberate reversions by
 113 the user or reversion, rebasing or rewinding in
 114 non-Topbloke-controlled branches.  For merges and Topbloke-generated
 115 anticommits or re-commits, the ``change made'' is only to be thought
 116 of as any conflict resolution.  This is not a partial order because it
 117 is not transitive.
 118
 119 \item[ $ \p, \py, \pn $ ]
 120 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
 121 are respectively the base and tip git branches.  $\p$ may be used
 122 where the context requires a set, in which case the statement
 123 is to be taken as applying to both $\py$ and $\pn$.
 124 None of these sets overlap.  Hence:
 125
 126 \item[ $ \patchof{ C } $ ]
 127 Either $\p$ s.t. $ C \in \p $, or $\bot$.
 128 A function from commits to patches' sets $\p$.
 129
 130 \item[ $ \pancsof{C}{\set P} $ ]
 131 $ \{ A \; | \; A \le C \land A \in \set P \} $
 132 i.e. all the ancestors of $C$
 133 which are in $\set P$.
 134
 135 \item[ $ \pendsof{C}{\set P} $ ]
 136 $ \{ E \; | \; E \in \pancsof{C}{\set P}
 137   \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
 138   E \neq A \land E \le A \} $
 139 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
 140
 141 \item[ $ \baseof{C} $ ]
 142 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
 143 A partial function from commits to commits.
 144 See Unique Base, below.
 145
 146 \item[ $ C \haspatch \p $ ]
 147 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
 148 ~ Informally, $C$ has the contents of $\p$.
 149
 150 \item[ $ C \nothaspatch \p $ ]
 151 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
 152 ~ Informally, $C$ has none of the contents of $\p$.
 153
 154 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
 155 patch is applied to a non-Topbloke branch and then bubbles back to
 156 the Topbloke patch itself, we hope that git's merge algorithm will
 157 DTRT or that the user will no longer care about the Topbloke patch.
 158
 159 \item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
 160 The contents of a git merge result:
 161
 162 $\displaystyle D \isin C \equiv
 163   \begin{cases}
 164     (D \isin L \land D \isin R) \lor D = C : & \true \\
 165     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
 166     \text{otherwise} : & D \not\isin M
 167   \end{cases}
 168 $
 169
 170 \end{basedescript}
 171 \newpage
 172 \section{Invariants}
 173
 174 We maintain these each time we construct a new commit. \\
 175 \[ \eqn{No Replay:}{
 176   C \has D \implies C \ge D
 177 }\]
 178 \[\eqn{Unique Base:}{
 179  \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
 180 }\]
 181 \[\eqn{Tip Contents:}{
 182   \bigforall_{C \in \py} D \isin C \equiv
 183     { D \isin \baseof{C} \lor \atop
 184       (D \in \py \land D \le C) }
 185 }\]
 186 \[\eqn{Base Acyclic:}{
 187   \bigforall_{B \in \pn} D \isin B \implies D \notin \py
 188 }\]
 189 \[\eqn{Coherence:}{
 190   \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
 191 }\]
 192 \[\eqn{Foreign Inclusion:}{
 193   \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
 194 }\]
 195
 196 \section{Some lemmas}
 197
 198 \[ \eqn{Exclusive Tip Contents:}{
 199   \bigforall_{C \in \py}
 200     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
 201       \Bigr]
 202 }\]
 203 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
 204
 205 \proof{
 206 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
 207 So by Base Acyclic $D \isin B \implies D \notin \py$.
 208 }
 209 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
 210   \bigforall_{C \in \py} D \isin C \equiv
 211   \begin{cases}
 212     D \in \py : & D \le C \\
 213     D \not\in \py : & D \isin \baseof{C}
 214   \end{cases}
 215 }\]
 216
 217 \[ \eqn{Tip Self Inpatch:}{
 218   \bigforall_{C \in \py} C \haspatch \p
 219 }\]
 220 Ie, tip commits contain their own patch.
 221
 222 \proof{
 223 Apply Exclusive Tip Contents to some $D \in \py$:
 224 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
 225   D \isin C \equiv D \le C $
 226 }
 227
 228 \[ \eqn{Exact Ancestors:}{
 229   \bigforall_{ C \hasparents \set{R} }
 230   D \le C \equiv
 231     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
 232     \lor D = C
 233 }\]
 234
 235 \[ \eqn{Transitive Ancestors:}{
 236   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
 237   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
 238 }\]
 239
 240 \proof{
 241 The implication from right to left is trivial because
 242 $ \pends() \subset \pancs() $.
 243 For the implication from left to right:
 244 by the definition of $\mathcal E$,
 245 for every such $A$, either $A \in \pends()$ which implies
 246 $A \le M$ by the LHS directly,
 247 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
 248 in which case we repeat for $A'$.  Since there are finitely many
 249 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
 250 by the LHS.  And $A \le A''$.
 251 }
 252 \[ \eqn{Calculation Of Ends:}{
 253   \bigforall_{C \hasparents \set A}
 254     \pendsof{C}{\set P} =
 255        \left\{ E \Big|
 256            \Bigl[ \Largeexists_{A \in \set A}
 257                        E \in \pendsof{A}{\set P} \Bigr] \land
 258            \Bigl[ \Largenexists_{B \in \set A}
 259                        E \neq B \land E \le B \Bigr]
 260        \right\}
 261 }\]
 262 XXX proof TBD.
 263
 264 \subsection{No Replay for Merge Results}
 265
 266 If we are constructing $C$, with,
 267 \gathbegin
 268   \mergeof{C}{L}{M}{R}
 269 \gathnext
 270   L \le C
 271 \gathnext
 272   R \le C
 273 \end{gather}
 274 No Replay is preserved.  \proofstarts
 275
 276 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
 277
 278 \subsubsection{For $D \isin L \land D \isin R$:}
 279 $D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
 280
 281 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
 282 $D \not\isin C$.  OK.
 283
 284 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 285  \land D \not\isin M$:}
 286 $D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
 287 R$ so $D \le C$.  OK.
 288
 289 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 290  \land D \isin M$:}
 291 $D \not\isin C$.  OK.
 292
 293 $\qed$
 294
 295 \section{Commit annotation}
 296
 297 We annotate each Topbloke commit $C$ with:
 298 \gathbegin
 299  \patchof{C}
 300 \gathnext
 301  \baseof{C}, \text{ if } C \in \py
 302 \gathnext
 303  \bigforall_{\pa{Q}}
 304    \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
 305 \gathnext
 306  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
 307 \end{gather}
 308
 309 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
 310 make it wrong to make plain commits with git because the recorded $\pends$
 311 would have to be updated.  The annotation is not needed because
 312 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
 313
 314 \section{Simple commit}
 315
 316 A simple single-parent forward commit $C$ as made by git-commit.
 317 \begin{gather}
 318 \tag*{} C \hasparents \{ A \} \\
 319 \tag*{} \patchof{C} = \patchof{A} \\
 320 \tag*{} D \isin C \equiv D \isin A \lor D = C
 321 \end{gather}
 322
 323 \subsection{No Replay}
 324 Trivial.
 325
 326 \subsection{Unique Base}
 327 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
 328
 329 \subsection{Tip Contents}
 330 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
 331 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
 332 Substitute into the contents of $C$:
 333 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
 334     \lor D = C \]
 335 Since $D = C \implies D \in \py$,
 336 and substituting in $\baseof{C}$, this gives:
 337 \[ D \isin C \equiv D \isin \baseof{C} \lor
 338     (D \in \py \land D \le A) \lor
 339     (D = C \land D \in \py) \]
 340 \[ \equiv D \isin \baseof{C} \lor
 341    [ D \in \py \land ( D \le A \lor D = C ) ] \]
 342 So by Exact Ancestors:
 343 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
 344 ) \]
 345 $\qed$
 346
 347 \subsection{Base Acyclic}
 348
 349 Need to consider only $A, C \in \pn$.
 350
 351 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 352
 353 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
 354 $A$, $D \isin C \implies D \not\in \py$. $\qed$
 355
 356 \subsection{Coherence and patch inclusion}
 357
 358 Need to consider $D \in \py$
 359
 360 \subsubsection{For $A \haspatch P, D = C$:}
 361
 362 Ancestors of $C$:
 363 $ D \le C $.
 364
 365 Contents of $C$:
 366 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 367
 368 \subsubsection{For $A \haspatch P, D \neq C$:}
 369 Ancestors: $ D \le C \equiv D \le A $.
 370
 371 Contents: $ D \isin C \equiv D \isin A \lor f $
 372 so $ D \isin C \equiv D \isin A $.
 373
 374 So:
 375 \[ A \haspatch P \implies C \haspatch P \]
 376
 377 \subsubsection{For $A \nothaspatch P$:}
 378
 379 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
 380 Thus $D \neq C$.
 381
 382 Now by contents of $A$, $D \notin A$, so $D \notin C$.
 383
 384 So:
 385 \[ A \nothaspatch P \implies C \nothaspatch P \]
 386 $\qed$
 387
 388 \subsection{Foreign inclusion:}
 389
 390 If $D = C$, trivial.  For $D \neq C$:
 391 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 392
 393 \section{Anticommit}
 394
 395 Given $L, R^+, R^-$ where
 396 $R^+ \in \pry, R^- = \baseof{R^+}$.
 397 Construct $C$ which has $\pr$ removed.
 398 Used for removing a branch dependency.
 399 \gathbegin
 400  C \hasparents \{ L \}
 401 \gathnext
 402  \patchof{C} = \patchof{L}
 403 \gathnext
 404  \mergeof{C}{L}{R^+}{R^-}
 405 \end{gather}
 406
 407 \subsection{Conditions}
 408
 409 \[ \eqn{ Unique Tip }{
 410  \pendsof{L}{\pry} = \{ R^+ \}
 411 }\]
 412 \[ \eqn{ Currently Included }{
 413  L \haspatch \pry
 414 }\]
 415 \[ \eqn{ Not Self }{
 416  L \not\in \{ R^+ \}
 417 }\]
 418
 419 \subsection{No Replay}
 420
 421 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
 422 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$ and No Replay for
 423 Merge Results applies. $\qed$
 424
 425 \subsection{Desired Contents}
 426
 427 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
 428 \proofstarts
 429
 430 \subsubsection{For $D = C$:}
 431
 432 Trivially $D \isin C$.  OK.
 433
 434 \subsubsection{For $D \neq C, D \not\le L$:}
 435
 436 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
 437 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
 438
 439 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
 440
 441 By Currently Included, $D \isin L$.
 442
 443 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
 444 by Unique Tip, $D \le R^+ \equiv D \le L$.
 445 So $D \isin R^+$.
 446
 447 By Base Acyclic, $D \not\isin R^-$.
 448
 449 Apply $\merge$: $D \not\isin C$.  OK.
 450
 451 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
 452
 453 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
 454
 455 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
 456
 457 $\qed$
 458
 459 \subsection{Unique Base}
 460
 461 Need to consider only $C \in \py$, ie $L \in \py$.
 462
 463 xxx tbd
 464
 465 xxx need to finish anticommit
 466
 467 \section{Merge}
 468
 469 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 470 \gathbegin
 471  C \hasparents \{ L, R \}
 472 \gathnext
 473  \patchof{C} = \patchof{L}
 474 \gathnext
 475  \mergeof{C}{L}{M}{R}
 476 \end{gather}
 477 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
 478
 479 \subsection{Conditions}
 480
 481 \[ \eqn{ Tip Merge }{
 482  L \in \py \implies
 483    \begin{cases}
 484       R \in \py : & \baseof{R} \ge \baseof{L}
 485               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
 486       R \in \pn : & R \ge \baseof{L}
 487               \land M = \baseof{L} \\
 488       \text{otherwise} : & \false
 489    \end{cases}
 490 }\]
 491 \[ \eqn{ Merge Acyclic }{
 492     L \in \pn
 493    \implies
 494     R \nothaspatch \p
 495 }\]
 496 \[ \eqn{ Removal Merge Ends }{
 497     X \not\haspatch \p \land
 498     Y \haspatch \p \land
 499     M \haspatch \p
 500   \implies
 501     \pendsof{Y}{\py} = \pendsof{M}{\py}
 502 }\]
 503 \[ \eqn{ Addition Merge Ends }{
 504     X \not\haspatch \p \land
 505     Y \haspatch \p \land
 506     M \nothaspatch \p
 507    \implies \left[
 508     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
 509    \right]
 510 }\]
 511
 512 \subsection{No Replay}
 513
 514 See No Replay for Merge Results.
 515
 516 \subsection{Unique Base}
 517
 518 Need to consider only $C \in \py$, ie $L \in \py$,
 519 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 520 putative ancestor $A \in \pn$ and see whether $A \le C$.
 521
 522 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 523 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 524 Thus $A \le C \equiv A \le L \lor A \le R$.
 525
 526 By Unique Base of L and Transitive Ancestors,
 527 $A \le L \equiv A \le \baseof{L}$.
 528
 529 \subsubsection{For $R \in \py$:}
 530
 531 By Unique Base of $R$ and Transitive Ancestors,
 532 $A \le R \equiv A \le \baseof{R}$.
 533
 534 But by Tip Merge condition on $\baseof{R}$,
 535 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 536 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 537 Thus $A \le C \equiv A \le \baseof{R}$.
 538 That is, $\baseof{C} = \baseof{R}$.
 539
 540 \subsubsection{For $R \in \pn$:}
 541
 542 By Tip Merge condition on $R$,
 543 $A \le \baseof{L} \implies A \le R$, so
 544 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 545 Thus $A \le C \equiv A \le R$.
 546 That is, $\baseof{C} = R$.
 547
 548 $\qed$
 549
 550 \subsection{Coherence and patch inclusion}
 551
 552 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
 553 This involves considering $D \in \py$.
 554
 555 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
 556 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
 557 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
 558 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
 559
 560 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
 561 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
 562 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
 563
 564 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
 565
 566 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
 567  \equiv D \isin L \lor D \isin R$.
 568 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
 569
 570 Consider $D \neq C, D \isin X \land D \isin Y$:
 571 By $\merge$, $D \isin C$.  Also $D \le X$
 572 so $D \le C$.  OK for $C \haspatch \p$.
 573
 574 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
 575 By $\merge$, $D \not\isin C$.
 576 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
 577 OK for $C \haspatch \p$.
 578
 579 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
 580 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
 581 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
 582 OK for $C \haspatch \p$.
 583
 584 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
 585
 586 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
 587
 588 $C \haspatch \p \equiv M \nothaspatch \p$.
 589
 590 \proofstarts
 591
 592 One of the Merge Ends conditions applies.
 593 Recall that we are considering $D \in \py$.
 594 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
 595 We will show for each of
 596 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
 597 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
 598
 599 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
 600 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
 601 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
 602 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
 603
 604 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
 605 $D \le Y$ so $D \le C$.
 606 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
 607
 608 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
 609 $D \not\le Y$.  If $D \le X$ then
 610 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
 611 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
 612 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
 613
 614 Consider $D \neq C, M \haspatch P, D \isin Y$:
 615 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
 616 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
 617 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
 618
 619 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
 620 By $\merge$, $D \not\isin C$.  OK.
 621
 622 $\qed$
 623
 624 \subsection{Base Acyclic}
 625
 626 This applies when $C \in \pn$.
 627 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
 628
 629 Consider some $D \in \py$.
 630
 631 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
 632 R$.  And $D \neq C$.  So $D \not\isin C$.  $\qed$
 633
 634 \subsection{Tip Contents}
 635
 636 We will consider some $D$ and prove the Exclusive Tip Contents form.
 637 We need worry only about $C \in \py$.  And $\patchof{C} = \patchof{L}$
 638 so $L \in \py$ so $L \haspatch \p$.  We will use the coherence and
 639 patch inclusion of $C$ as just proved.
 640
 641 Firstly we prove $C \haspatch \p$: If $R \in \py$, this is true by
 642 coherence/inclusion $C \haspatch \p$.  So by definition of
 643 $\haspatch$, $D \isin C \equiv D \le C$.  OK.
 644
 645 \subsubsection{For $L \in \py, D \in \py, $:}
 646 $R \haspatch \p$ so
 647
 648 \subsubsection{For $L \in \py, D \not\in \py, R \in \py$:}
 649
 650
 651 %D \in \py$:}
 652
 653
 654
 655 xxx the coherence is not that useful ?
 656
 657 $L \haspatch \p$ by
 658
 659 xxx need to recheck this
 660
 661 $C \in \py$ $C \haspatch P$ so $D \isin C \equiv D \le C$.  OK.
 662
 663 \subsubsection{For $L \in \py, D \not\in \py, R \in \py$:}
 664
 665 Tip Contents for $L$: $D \isin L \equiv D \isin \baseof{L}$.
 666
 667 Tip Contents for $R$: $D \isin R \equiv D \isin \baseof{R}$.
 668
 669 But by Tip Merge, $\baseof{R} \ge \baseof{L}$
 670
 671 \end{document}