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$, given
 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
 478 \subsection{Conditions}
 479
 480 \[ \eqn{ Tip Merge }{
 481  L \in \py \implies
 482    \begin{cases}
 483       R \in \py : & \baseof{R} \ge \baseof{L}
 484               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
 485       R \in \pn : & R \ge \baseof{L}
 486               \land M = \baseof{L} \\
 487       \text{otherwise} : & \false
 488    \end{cases}
 489 }\]
 490
 491 \subsection{No Replay}
 492
 493 See No Replay for Merge Results.
 494
 495 \subsection{Unique Base}
 496
 497 Need to consider only $C \in \py$, ie $L \in \py$,
 498 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 499 putative ancestor $A \in \pn$ and see whether $A \le C$.
 500
 501 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 502 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 503 Thus $A \le C \equiv A \le L \lor A \le R$.
 504
 505 By Unique Base of L and Transitive Ancestors,
 506 $A \le L \equiv A \le \baseof{L}$.
 507
 508 \subsubsection{For $R \in \py$:}
 509
 510 By Unique Base of $R$ and Transitive Ancestors,
 511 $A \le R \equiv A \le \baseof{R}$.
 512
 513 But by Tip Merge condition on $\baseof{R}$,
 514 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 515 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 516 Thus $A \le C \equiv A \le \baseof{R}$.
 517 That is, $\baseof{C} = \baseof{R}$.
 518
 519 \subsubsection{For $R \in \pn$:}
 520
 521 By Tip Merge condition on $R$,
 522 $A \le \baseof{L} \implies A \le R$, so
 523 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 524 Thus $A \le C \equiv A \le R$.
 525 That is, $\baseof{C} = R$.
 526
 527 $\qed$
 528
 529 \subsection{Coherence and patch inclusion}
 530
 531 Need to determine $C \haspatch P$ based on $L,M,R \haspatch P$.
 532 This involves considering $D \in \py$.
 533
 534 We will use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
 535
 536 \subsubsection{For $L \nothaspatch P, R \nothaspatch P$:}
 537 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
 538 \in \py$ ie $L \haspatch P$ by Tip Self Inpatch).  So $D \neq C$.
 539 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch P$.
 540
 541 \subsubsection{For $L \haspatch P, R \haspatch P$:}
 542 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
 543 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
 544
 545 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch P$.
 546
 547 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
 548  \equiv D \isin L \lor D \isin R$.
 549 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
 550
 551 Consider $D \neq C, D \isin X \land D \isin Y$:
 552 By $\merge$, $D \isin C$.  Also $D \le X$
 553 so $D \le C$.  OK for $C \haspatch P$.
 554
 555 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
 556 By $\merge$, $D \not\isin C$.
 557 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
 558 OK for $C \haspatch P$.
 559
 560 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
 561 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
 562 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
 563 OK for $C \haspatch P$.
 564
 565 So indeed $L \haspatch P \land R \haspatch P \implies C \haspatch P$.
 566
 567 \end{document}