chiark / gitweb /
wip merge complex
[topbloke-formulae.git] / 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
494   \implies \left[
495   \bigforall_{E \in \pendsof{X}{\py}}
496     E \le Y
497   \right]
498 }\]
499
500 \subsection{No Replay}
501
502 See No Replay for Merge Results.
503
504 \subsection{Unique Base}
505
506 Need to consider only $C \in \py$, ie $L \in \py$,
507 and calculate $\pendsof{C}{\pn}$.  So we will consider some
508 putative ancestor $A \in \pn$ and see whether $A \le C$.
509
510 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
511 But $C \in py$ and $A \in \pn$ so $A \neq C$.  
512 Thus $A \le C \equiv A \le L \lor A \le R$.
513
514 By Unique Base of L and Transitive Ancestors,
515 $A \le L \equiv A \le \baseof{L}$.
516
517 \subsubsection{For $R \in \py$:}
518
519 By Unique Base of $R$ and Transitive Ancestors,
520 $A \le R \equiv A \le \baseof{R}$.
521
522 But by Tip Merge condition on $\baseof{R}$,
523 $A \le \baseof{L} \implies A \le \baseof{R}$, so
524 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
525 Thus $A \le C \equiv A \le \baseof{R}$.  
526 That is, $\baseof{C} = \baseof{R}$.
527
528 \subsubsection{For $R \in \pn$:}
529
530 By Tip Merge condition on $R$,
531 $A \le \baseof{L} \implies A \le R$, so
532 $A \le R \lor A \le \baseof{L} \equiv A \le R$.  
533 Thus $A \le C \equiv A \le R$.  
534 That is, $\baseof{C} = R$.
535
536 $\qed$
537
538 \subsection{Coherence and patch inclusion}
539
540 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
541 This involves considering $D \in \py$.  
542
543 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
544 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
545 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
546 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
547
548 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
549 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
550 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
551
552 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
553
554 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
555  \equiv D \isin L \lor D \isin R$.  
556 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
557
558 Consider $D \neq C, D \isin X \land D \isin Y$:
559 By $\merge$, $D \isin C$.  Also $D \le X$ 
560 so $D \le C$.  OK for $C \haspatch \p$.
561
562 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
563 By $\merge$, $D \not\isin C$.  
564 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.  
565 OK for $C \haspatch \p$.
566
567 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
568 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.  
569 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
570 OK for $C \haspatch \p$.
571
572 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
573
574 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
575
576 $C \haspatch \p \equiv M \nothaspatch \p$.
577
578 \proofstarts
579
580 Merge Ends applies.  Recall that we are considering $D \in \py$.
581 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
582 We will show for each of
583 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
584 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
585
586 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
587 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
588 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
589 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
590
591 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
592 $D \le Y$ so $D \le C$.  
593 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
594
595 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
596 $D \not\le Y$.  If $D \le X$ then
597 $D \in \pancsof{X}{\py}$, so by Merge Ends and 
598 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
599 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
600
601 \end{document}