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{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
  69 \newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }
  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 All these sets are distinct.  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 \[ \corrolary{
 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 Ends }{
 492     X \not\haspatch \p \land
 493     Y \haspatch \p \land
 494     E \in \pendsof{X}{\py}
 495   \implies
 496     E \le Y
 497 }\]
 498
 499 \subsection{No Replay}
 500
 501 See No Replay for Merge Results.
 502
 503 \subsection{Unique Base}
 504
 505 Need to consider only $C \in \py$, ie $L \in \py$,
 506 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 507 putative ancestor $A \in \pn$ and see whether $A \le C$.
 508
 509 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 510 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 511 Thus $A \le C \equiv A \le L \lor A \le R$.
 512
 513 By Unique Base of L and Transitive Ancestors,
 514 $A \le L \equiv A \le \baseof{L}$.
 515
 516 \subsubsection{For $R \in \py$:}
 517
 518 By Unique Base of $R$ and Transitive Ancestors,
 519 $A \le R \equiv A \le \baseof{R}$.
 520
 521 But by Tip Merge condition on $\baseof{R}$,
 522 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 523 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 524 Thus $A \le C \equiv A \le \baseof{R}$.
 525 That is, $\baseof{C} = \baseof{R}$.
 526
 527 \subsubsection{For $R \in \pn$:}
 528
 529 By Tip Merge condition on $R$,
 530 $A \le \baseof{L} \implies A \le R$, so
 531 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 532 Thus $A \le C \equiv A \le R$.
 533 That is, $\baseof{C} = R$.
 534
 535 $\qed$
 536
 537 \subsection{Coherence and patch inclusion}
 538
 539 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
 540 This involves considering $D \in \py$.
 541
 542 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
 543 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
 544 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
 545 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
 546
 547 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
 548 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
 549 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
 550
 551 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
 552
 553 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
 554  \equiv D \isin L \lor D \isin R$.
 555 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
 556
 557 Consider $D \neq C, D \isin X \land D \isin Y$:
 558 By $\merge$, $D \isin C$.  Also $D \le X$
 559 so $D \le C$.  OK for $C \haspatch \p$.
 560
 561 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
 562 By $\merge$, $D \not\isin C$.
 563 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
 564 OK for $C \haspatch \p$.
 565
 566 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
 567 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
 568 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
 569 OK for $C \haspatch \p$.
 570
 571 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
 572
 573 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
 574
 575 $C \haspatch \p \equiv C \nothaspatch M$.
 576
 577 \proofstarts
 578
 579 \end{document}