1 \documentclass[a4paper,leqno]{strayman}
3 \let\numberwithin=\notdef
11 \renewcommand{\ge}{\geqslant}
12 \renewcommand{\le}{\leqslant}
13 \newcommand{\nge}{\ngeqslant}
14 \newcommand{\nle}{\nleqslant}
16 \newcommand{\has}{\sqsupseteq}
17 \newcommand{\isin}{\sqsubseteq}
19 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
20 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
21 \newcommand{\haspatch}{\sqSupset}
22 \newcommand{\patchisin}{\sqSubset}
24 \newif\ifhidehack\hidehackfalse
25 \DeclareRobustCommand\hidefromedef[2]{%
26 \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
27 \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
29 \newcommand{\set}[1]{\mathbb{#1}}
30 \newcommand{\pay}[1]{\pa{#1}^+}
31 \newcommand{\pan}[1]{\pa{#1}^-}
33 \newcommand{\p}{\pa{P}}
34 \newcommand{\py}{\pay{P}}
35 \newcommand{\pn}{\pan{P}}
37 \newcommand{\pr}{\pa{R}}
38 \newcommand{\pry}{\pay{R}}
39 \newcommand{\prn}{\pan{R}}
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}}
47 \renewcommand{\implies}{\Rightarrow}
48 \renewcommand{\equiv}{\Leftrightarrow}
49 \renewcommand{\nequiv}{\nLeftrightarrow}
50 \renewcommand{\land}{\wedge}
51 \renewcommand{\lor}{\vee}
53 \newcommand{\pancs}{{\mathcal A}}
54 \newcommand{\pends}{{\mathcal E}}
56 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
57 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
59 \newcommand{\merge}{{\mathcal M}}
60 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
61 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
63 \newcommand{\patch}{{\mathcal P}}
64 \newcommand{\base}{{\mathcal B}}
66 \newcommand{\patchof}[1]{\patch ( #1 ) }
67 \newcommand{\baseof}[1]{\base ( #1 ) }
69 \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
70 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
72 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
73 \newcommand{\bigforall}{%
75 {\hbox{\huge$\forall$}}%
76 {\hbox{\Large$\forall$}}%
77 {\hbox{\normalsize$\forall$}}%
78 {\hbox{\scriptsize$\forall$}}}%
81 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
82 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
84 \newcommand{\qed}{\square}
85 \newcommand{\proofstarts}{{\it Proof:}}
86 \newcommand{\proof}[1]{\proofstarts #1 $\qed$}
88 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
89 \newcommand{\gathnext}{\\ \tag*{}}
92 \newcommand{\false}{f}
100 \desclabelstyle{\nextlinelabel}
102 \item[ $ C \hasparents \set X $ ]
103 The parents of commit $C$ are exactly the set
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 $.
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
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:
127 \item[ $ \patchof{ C } $ ]
128 Either $\p$ s.t. $ C \in \p $, or $\bot$.
129 A function from commits to patches' sets $\p$.
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$.
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}$.
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.
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$.
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$.
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.
160 \item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
161 The contents of a git merge result:
163 $\displaystyle D \isin C \equiv
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
171 Some (overlapping) alternative formulations:
173 $\displaystyle D \isin C \equiv
175 D \isin L \equiv D \isin R : & D = C \lor D \isin L \\
176 D \isin L \equiv D \isin R : & D = C \lor D \isin R \\
177 D \isin L \nequiv D \isin R : & D = C \lor D \not\isin M \\
178 D \isin M \equiv D \isin L : & D = C \lor D \isin R \\
179 D \isin M \equiv D \isin R : & D = C \lor D \isin L \\
187 We maintain these each time we construct a new commit. \\
189 C \has D \implies C \ge D
191 \[\eqn{Unique Base:}{
192 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
194 \[\eqn{Tip Contents:}{
195 \bigforall_{C \in \py} D \isin C \equiv
196 { D \isin \baseof{C} \lor \atop
197 (D \in \py \land D \le C) }
199 \[\eqn{Base Acyclic:}{
200 \bigforall_{B \in \pn} D \isin B \implies D \notin \py
203 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
205 \[\eqn{Foreign Inclusion:}{
206 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
209 \section{Some lemmas}
211 \[ \eqn{Exclusive Tip Contents:}{
212 \bigforall_{C \in \py}
213 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
216 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
219 Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
220 So by Base Acyclic $D \isin B \implies D \notin \py$.
222 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
223 \bigforall_{C \in \py} D \isin C \equiv
225 D \in \py : & D \le C \\
226 D \not\in \py : & D \isin \baseof{C}
230 \[ \eqn{Tip Self Inpatch:}{
231 \bigforall_{C \in \py} C \haspatch \p
233 Ie, tip commits contain their own patch.
236 Apply Exclusive Tip Contents to some $D \in \py$:
237 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
238 D \isin C \equiv D \le C $
241 \[ \eqn{Exact Ancestors:}{
242 \bigforall_{ C \hasparents \set{R} }
244 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
248 \[ \eqn{Transitive Ancestors:}{
249 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
250 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
254 The implication from right to left is trivial because
255 $ \pends() \subset \pancs() $.
256 For the implication from left to right:
257 by the definition of $\mathcal E$,
258 for every such $A$, either $A \in \pends()$ which implies
259 $A \le M$ by the LHS directly,
260 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
261 in which case we repeat for $A'$. Since there are finitely many
262 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
263 by the LHS. And $A \le A''$.
265 \[ \eqn{Calculation Of Ends:}{
266 \bigforall_{C \hasparents \set A}
267 \pendsof{C}{\set P} =
269 \Bigl[ \Largeexists_{A \in \set A}
270 E \in \pendsof{A}{\set P} \Bigr] \land
271 \Bigl[ \Largenexists_{B \in \set A}
272 E \neq B \land E \le B \Bigr]
277 \subsection{No Replay for Merge Results}
279 If we are constructing $C$, with,
287 No Replay is preserved. \proofstarts
289 \subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
291 \subsubsection{For $D \isin L \land D \isin R$:}
292 $D \isin C$. And $D \isin L \implies D \le L \implies D \le C$. OK.
294 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
297 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
298 \land D \not\isin M$:}
299 $D \isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
302 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
308 \section{Commit annotation}
310 We annotate each Topbloke commit $C$ with:
314 \baseof{C}, \text{ if } C \in \py
317 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
319 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
322 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
323 make it wrong to make plain commits with git because the recorded $\pends$
324 would have to be updated. The annotation is not needed because
325 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
327 \section{Simple commit}
329 A simple single-parent forward commit $C$ as made by git-commit.
331 \tag*{} C \hasparents \{ A \} \\
332 \tag*{} \patchof{C} = \patchof{A} \\
333 \tag*{} D \isin C \equiv D \isin A \lor D = C
336 \subsection{No Replay}
339 \subsection{Unique Base}
340 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
342 \subsection{Tip Contents}
343 We need to consider only $A, C \in \py$. From Tip Contents for $A$:
344 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
345 Substitute into the contents of $C$:
346 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
348 Since $D = C \implies D \in \py$,
349 and substituting in $\baseof{C}$, this gives:
350 \[ D \isin C \equiv D \isin \baseof{C} \lor
351 (D \in \py \land D \le A) \lor
352 (D = C \land D \in \py) \]
353 \[ \equiv D \isin \baseof{C} \lor
354 [ D \in \py \land ( D \le A \lor D = C ) ] \]
355 So by Exact Ancestors:
356 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
360 \subsection{Base Acyclic}
362 Need to consider only $A, C \in \pn$.
364 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
366 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
367 $A$, $D \isin C \implies D \not\in \py$. $\qed$
369 \subsection{Coherence and patch inclusion}
371 Need to consider $D \in \py$
373 \subsubsection{For $A \haspatch P, D = C$:}
379 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
381 \subsubsection{For $A \haspatch P, D \neq C$:}
382 Ancestors: $ D \le C \equiv D \le A $.
384 Contents: $ D \isin C \equiv D \isin A \lor f $
385 so $ D \isin C \equiv D \isin A $.
388 \[ A \haspatch P \implies C \haspatch P \]
390 \subsubsection{For $A \nothaspatch P$:}
392 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
395 Now by contents of $A$, $D \notin A$, so $D \notin C$.
398 \[ A \nothaspatch P \implies C \nothaspatch P \]
401 \subsection{Foreign inclusion:}
403 If $D = C$, trivial. For $D \neq C$:
404 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
408 Given $L, R^+, R^-$ where
409 $R^+ \in \pry, R^- = \baseof{R^+}$.
410 Construct $C$ which has $\pr$ removed.
411 Used for removing a branch dependency.
413 C \hasparents \{ L \}
415 \patchof{C} = \patchof{L}
417 \mergeof{C}{L}{R^+}{R^-}
420 \subsection{Conditions}
422 \[ \eqn{ Unique Tip }{
423 \pendsof{L}{\pry} = \{ R^+ \}
425 \[ \eqn{ Currently Included }{
432 \subsection{No Replay}
434 By Unique Tip, $R^+ \le L$. By definition of $\base$, $R^- \le R^+$
435 so $R^- \le L$. So $R^+ \le C$ and $R^- \le C$ and No Replay for
436 Merge Results applies. $\qed$
438 \subsection{Desired Contents}
440 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
443 \subsubsection{For $D = C$:}
445 Trivially $D \isin C$. OK.
447 \subsubsection{For $D \neq C, D \not\le L$:}
449 By No Replay $D \not\isin L$. Also $D \not\le R^-$ hence
450 $D \not\isin R^-$. Thus $D \not\isin C$. OK.
452 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
454 By Currently Included, $D \isin L$.
456 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
457 by Unique Tip, $D \le R^+ \equiv D \le L$.
460 By Base Acyclic, $D \not\isin R^-$.
462 Apply $\merge$: $D \not\isin C$. OK.
464 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
466 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
468 Apply $\merge$: $D \isin C \equiv D \isin L$. OK.
472 \subsection{Unique Base}
474 Need to consider only $C \in \py$, ie $L \in \py$.
478 xxx need to finish anticommit
482 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
484 C \hasparents \{ L, R \}
486 \patchof{C} = \patchof{L}
490 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
492 \subsection{Conditions}
494 \[ \eqn{ Tip Merge }{
497 R \in \py : & \baseof{R} \ge \baseof{L}
498 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
499 R \in \pn : & M = \baseof{L} \\
500 \text{otherwise} : & \false
503 \[ \eqn{ Merge Acyclic }{
508 \[ \eqn{ Removal Merge Ends }{
509 X \not\haspatch \p \land
513 \pendsof{Y}{\py} = \pendsof{M}{\py}
515 \[ \eqn{ Addition Merge Ends }{
516 X \not\haspatch \p \land
520 \bigforall_{E \in \pendsof{X}{\py}} E \le Y
524 \subsection{No Replay}
526 See No Replay for Merge Results.
528 \subsection{Unique Base}
530 Need to consider only $C \in \py$, ie $L \in \py$,
531 and calculate $\pendsof{C}{\pn}$. So we will consider some
532 putative ancestor $A \in \pn$ and see whether $A \le C$.
534 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
535 But $C \in py$ and $A \in \pn$ so $A \neq C$.
536 Thus $A \le C \equiv A \le L \lor A \le R$.
538 By Unique Base of L and Transitive Ancestors,
539 $A \le L \equiv A \le \baseof{L}$.
541 \subsubsection{For $R \in \py$:}
543 By Unique Base of $R$ and Transitive Ancestors,
544 $A \le R \equiv A \le \baseof{R}$.
546 But by Tip Merge condition on $\baseof{R}$,
547 $A \le \baseof{L} \implies A \le \baseof{R}$, so
548 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
549 Thus $A \le C \equiv A \le \baseof{R}$.
550 That is, $\baseof{C} = \baseof{R}$.
552 \subsubsection{For $R \in \pn$:}
554 By Tip Merge condition on $R$ and since $M \le R$,
555 $A \le \baseof{L} \implies A \le R$, so
556 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
557 Thus $A \le C \equiv A \le R$.
558 That is, $\baseof{C} = R$.
562 \subsection{Coherence and Patch Inclusion}
564 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
565 This involves considering $D \in \py$.
567 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
568 $D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
569 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch). So $D \neq C$.
570 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
572 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
573 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
574 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
576 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
578 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
579 \equiv D \isin L \lor D \isin R$.
580 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
582 Consider $D \neq C, D \isin X \land D \isin Y$:
583 By $\merge$, $D \isin C$. Also $D \le X$
584 so $D \le C$. OK for $C \haspatch \p$.
586 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
587 By $\merge$, $D \not\isin C$.
588 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
589 OK for $C \haspatch \p$.
591 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
592 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
593 Thus by $\merge$, $D \isin C$. And $D \le Y$ so $D \le C$.
594 OK for $C \haspatch \p$.
596 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
598 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
600 $C \haspatch \p \equiv M \nothaspatch \p$.
604 One of the Merge Ends conditions applies.
605 Recall that we are considering $D \in \py$.
606 $D \isin Y \equiv D \le Y$. $D \not\isin X$.
607 We will show for each of
608 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
609 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
611 Consider $D = C$: Thus $C \in \py, L \in \py$, and by Tip
612 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$. By Tip Merge,
613 $M=\baseof{L}$. So by Base Acyclic $D \not\isin M$, i.e.
614 $M \nothaspatch \p$. And indeed $D \isin C$ and $D \le C$. OK.
616 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
617 $D \le Y$ so $D \le C$.
618 $D \not\isin M$ so by $\merge$, $D \isin C$. OK.
620 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
621 $D \not\le Y$. If $D \le X$ then
622 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
623 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
624 Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK.
626 Consider $D \neq C, M \haspatch P, D \isin Y$:
627 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
628 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
629 Thus $D \isin M$. By $\merge$, $D \not\isin C$. OK.
631 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
632 By $\merge$, $D \not\isin C$. OK.
636 \subsection{Base Acyclic}
638 This applies when $C \in \pn$.
639 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
641 Consider some $D \in \py$.
643 By Base Acyclic of $L$, $D \not\isin L$. By the above, $D \not\isin
644 R$. And $D \neq C$. So $D \not\isin C$. $\qed$
646 \subsection{Tip Contents}
648 We need worry only about $C \in \py$.
649 And $\patchof{C} = \patchof{L}$
650 so $L \in \py$ so $L \haspatch \p$. We will use the Unique Base
651 of $C$, and its Coherence and Patch Inclusion, as just proved.
653 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
654 \p$ and by Coherence/Inclusion $C \haspatch \p$ . If $R \not\in \py$
655 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
656 of $\nothaspatch$, $M \nothaspatch \p$. So by Coherence/Inclusion $C
657 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
659 We will consider an arbitrary commit $D$
660 and prove the Exclusive Tip Contents form.
662 \subsubsection{For $D \in \py$:}
663 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
666 \subsubsection{For $D \not\in \py, R \not\in \py$:}
668 $D \neq C$. By Tip Contents of $L$,
669 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
670 $D \isin L \equiv D \isin M$. So by definition of $\merge$, $D \isin
671 C \equiv D \isin R$. And $R = \baseof{C}$ by Unique Base of $C$.
672 Thus $D \isin C \equiv D \isin \baseof{C}$. OK.
674 \subsubsection{For $D \not\in \py, R \in \py$:}
682 xxx the coherence is not that useful ?
686 xxx need to recheck this
688 $C \in \py$ $C \haspatch P$ so $D \isin C \equiv D \le C$. OK.
690 \subsubsection{For $L \in \py, D \not\in \py, R \in \py$:}
692 Tip Contents for $L$: $D \isin L \equiv D \isin \baseof{L}$.
694 Tip Contents for $R$: $D \isin R \equiv D \isin \baseof{R}$.
696 But by Tip Merge, $\baseof{R} \ge \baseof{L}$