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
175 We maintain these each time we construct a new commit. \\
177 C \has D \implies C \ge D
179 \[\eqn{Unique Base:}{
180 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
182 \[\eqn{Tip Contents:}{
183 \bigforall_{C \in \py} D \isin C \equiv
184 { D \isin \baseof{C} \lor \atop
185 (D \in \py \land D \le C) }
187 \[\eqn{Base Acyclic:}{
188 \bigforall_{B \in \pn} D \isin B \implies D \notin \py
191 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
193 \[\eqn{Foreign Inclusion:}{
194 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
197 \section{Some lemmas}
199 \[ \eqn{Exclusive Tip Contents:}{
200 \bigforall_{C \in \py}
201 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
204 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
207 Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
208 So by Base Acyclic $D \isin B \implies D \notin \py$.
210 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
211 \bigforall_{C \in \py} D \isin C \equiv
213 D \in \py : & D \le C \\
214 D \not\in \py : & D \isin \baseof{C}
218 \[ \eqn{Tip Self Inpatch:}{
219 \bigforall_{C \in \py} C \haspatch \p
221 Ie, tip commits contain their own patch.
224 Apply Exclusive Tip Contents to some $D \in \py$:
225 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
226 D \isin C \equiv D \le C $
229 \[ \eqn{Exact Ancestors:}{
230 \bigforall_{ C \hasparents \set{R} }
232 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
236 \[ \eqn{Transitive Ancestors:}{
237 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
238 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
242 The implication from right to left is trivial because
243 $ \pends() \subset \pancs() $.
244 For the implication from left to right:
245 by the definition of $\mathcal E$,
246 for every such $A$, either $A \in \pends()$ which implies
247 $A \le M$ by the LHS directly,
248 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
249 in which case we repeat for $A'$. Since there are finitely many
250 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
251 by the LHS. And $A \le A''$.
253 \[ \eqn{Calculation Of Ends:}{
254 \bigforall_{C \hasparents \set A}
255 \pendsof{C}{\set P} =
257 \Bigl[ \Largeexists_{A \in \set A}
258 E \in \pendsof{A}{\set P} \Bigr] \land
259 \Bigl[ \Largenexists_{B \in \set A}
260 E \neq B \land E \le B \Bigr]
265 \subsection{No Replay for Merge Results}
267 If we are constructing $C$, with,
275 No Replay is preserved. \proofstarts
277 \subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
279 \subsubsection{For $D \isin L \land D \isin R$:}
280 $D \isin C$. And $D \isin L \implies D \le L \implies D \le C$. OK.
282 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
285 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
286 \land D \not\isin M$:}
287 $D \isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
290 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
296 \section{Commit annotation}
298 We annotate each Topbloke commit $C$ with:
302 \baseof{C}, \text{ if } C \in \py
305 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
307 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
310 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
311 make it wrong to make plain commits with git because the recorded $\pends$
312 would have to be updated. The annotation is not needed because
313 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
315 \section{Simple commit}
317 A simple single-parent forward commit $C$ as made by git-commit.
319 \tag*{} C \hasparents \{ A \} \\
320 \tag*{} \patchof{C} = \patchof{A} \\
321 \tag*{} D \isin C \equiv D \isin A \lor D = C
324 \subsection{No Replay}
327 \subsection{Unique Base}
328 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
330 \subsection{Tip Contents}
331 We need to consider only $A, C \in \py$. From Tip Contents for $A$:
332 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
333 Substitute into the contents of $C$:
334 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
336 Since $D = C \implies D \in \py$,
337 and substituting in $\baseof{C}$, this gives:
338 \[ D \isin C \equiv D \isin \baseof{C} \lor
339 (D \in \py \land D \le A) \lor
340 (D = C \land D \in \py) \]
341 \[ \equiv D \isin \baseof{C} \lor
342 [ D \in \py \land ( D \le A \lor D = C ) ] \]
343 So by Exact Ancestors:
344 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
348 \subsection{Base Acyclic}
350 Need to consider only $A, C \in \pn$.
352 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
354 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
355 $A$, $D \isin C \implies D \not\in \py$. $\qed$
357 \subsection{Coherence and patch inclusion}
359 Need to consider $D \in \py$
361 \subsubsection{For $A \haspatch P, D = C$:}
367 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
369 \subsubsection{For $A \haspatch P, D \neq C$:}
370 Ancestors: $ D \le C \equiv D \le A $.
372 Contents: $ D \isin C \equiv D \isin A \lor f $
373 so $ D \isin C \equiv D \isin A $.
376 \[ A \haspatch P \implies C \haspatch P \]
378 \subsubsection{For $A \nothaspatch P$:}
380 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
383 Now by contents of $A$, $D \notin A$, so $D \notin C$.
386 \[ A \nothaspatch P \implies C \nothaspatch P \]
389 \subsection{Foreign inclusion:}
391 If $D = C$, trivial. For $D \neq C$:
392 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
396 Given $L, R^+, R^-$ where
397 $R^+ \in \pry, R^- = \baseof{R^+}$.
398 Construct $C$ which has $\pr$ removed.
399 Used for removing a branch dependency.
401 C \hasparents \{ L \}
403 \patchof{C} = \patchof{L}
405 \mergeof{C}{L}{R^+}{R^-}
408 \subsection{Conditions}
410 \[ \eqn{ Unique Tip }{
411 \pendsof{L}{\pry} = \{ R^+ \}
413 \[ \eqn{ Currently Included }{
420 \subsection{No Replay}
422 By Unique Tip, $R^+ \le L$. By definition of $\base$, $R^- \le R^+$
423 so $R^- \le L$. So $R^+ \le C$ and $R^- \le C$ and No Replay for
424 Merge Results applies. $\qed$
426 \subsection{Desired Contents}
428 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
431 \subsubsection{For $D = C$:}
433 Trivially $D \isin C$. OK.
435 \subsubsection{For $D \neq C, D \not\le L$:}
437 By No Replay $D \not\isin L$. Also $D \not\le R^-$ hence
438 $D \not\isin R^-$. Thus $D \not\isin C$. OK.
440 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
442 By Currently Included, $D \isin L$.
444 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
445 by Unique Tip, $D \le R^+ \equiv D \le L$.
448 By Base Acyclic, $D \not\isin R^-$.
450 Apply $\merge$: $D \not\isin C$. OK.
452 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
454 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
456 Apply $\merge$: $D \isin C \equiv D \isin L$. OK.
460 \subsection{Unique Base}
462 Need to consider only $C \in \py$, ie $L \in \py$.
466 xxx need to finish anticommit
470 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
472 C \hasparents \{ L, R \}
474 \patchof{C} = \patchof{L}
478 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
480 \subsection{Conditions}
482 \[ \eqn{ Tip Merge }{
485 R \in \py : & \baseof{R} \ge \baseof{L}
486 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
487 R \in \pn : & R \ge \baseof{L}
488 \land M = \baseof{L} \\
489 \text{otherwise} : & \false
492 \[ \eqn{ Merge Acyclic }{
497 \[ \eqn{ Removal Merge Ends }{
498 X \not\haspatch \p \land
502 \pendsof{Y}{\py} = \pendsof{M}{\py}
504 \[ \eqn{ Addition Merge Ends }{
505 X \not\haspatch \p \land
509 \bigforall_{E \in \pendsof{X}{\py}} E \le Y
513 \subsection{No Replay}
515 See No Replay for Merge Results.
517 \subsection{Unique Base}
519 Need to consider only $C \in \py$, ie $L \in \py$,
520 and calculate $\pendsof{C}{\pn}$. So we will consider some
521 putative ancestor $A \in \pn$ and see whether $A \le C$.
523 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
524 But $C \in py$ and $A \in \pn$ so $A \neq C$.
525 Thus $A \le C \equiv A \le L \lor A \le R$.
527 By Unique Base of L and Transitive Ancestors,
528 $A \le L \equiv A \le \baseof{L}$.
530 \subsubsection{For $R \in \py$:}
532 By Unique Base of $R$ and Transitive Ancestors,
533 $A \le R \equiv A \le \baseof{R}$.
535 But by Tip Merge condition on $\baseof{R}$,
536 $A \le \baseof{L} \implies A \le \baseof{R}$, so
537 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
538 Thus $A \le C \equiv A \le \baseof{R}$.
539 That is, $\baseof{C} = \baseof{R}$.
541 \subsubsection{For $R \in \pn$:}
543 By Tip Merge condition on $R$,
544 $A \le \baseof{L} \implies A \le R$, so
545 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
546 Thus $A \le C \equiv A \le R$.
547 That is, $\baseof{C} = R$.
551 \subsection{Coherence and patch inclusion}
553 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
554 This involves considering $D \in \py$.
556 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
557 $D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
558 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch). So $D \neq C$.
559 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
561 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
562 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
563 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
565 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
567 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
568 \equiv D \isin L \lor D \isin R$.
569 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
571 Consider $D \neq C, D \isin X \land D \isin Y$:
572 By $\merge$, $D \isin C$. Also $D \le X$
573 so $D \le C$. OK for $C \haspatch \p$.
575 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
576 By $\merge$, $D \not\isin C$.
577 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
578 OK for $C \haspatch \p$.
580 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
581 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
582 Thus by $\merge$, $D \isin C$. And $D \le Y$ so $D \le C$.
583 OK for $C \haspatch \p$.
585 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
587 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
589 $C \haspatch \p \equiv M \nothaspatch \p$.
593 One of the Merge Ends conditions applies.
594 Recall that we are considering $D \in \py$.
595 $D \isin Y \equiv D \le Y$. $D \not\isin X$.
596 We will show for each of
597 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
598 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
600 Consider $D = C$: Thus $C \in \py, L \in \py$, and by Tip
601 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$. By Tip Merge,
602 $M=\baseof{L}$. So by Base Acyclic $D \not\isin M$, i.e.
603 $M \nothaspatch \p$. And indeed $D \isin C$ and $D \le C$. OK.
605 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
606 $D \le Y$ so $D \le C$.
607 $D \not\isin M$ so by $\merge$, $D \isin C$. OK.
609 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
610 $D \not\le Y$. If $D \le X$ then
611 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
612 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
613 Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK.
615 Consider $D \neq C, M \haspatch P, D \isin Y$:
616 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
617 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
618 Thus $D \isin M$. By $\merge$, $D \not\isin C$. OK.
620 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
621 By $\merge$, $D \not\isin C$. OK.
625 \subsection{Base Acyclic}
627 This applies when $C \in \pn$.
628 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
630 Consider some $D \in \py$.
632 By Base Acyclic of $L$, $D \not\isin L$. By the above, $D \not\isin
633 R$. And $D \neq C$. So $D \not\isin C$. $\qed$
635 \subsection{Tip Contents}
637 We need worry only about $C \in \py$.
638 And $\patchof{C} = \patchof{L}$
639 so $L \in \py$ so $L \haspatch \p$. We will use the coherence and
640 patch inclusion of $C$ as just proved.
642 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
643 \p$ and by coherence/inclusion $C \haspatch \p$ . If $R \not\in \py$
644 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
645 of $\nothaspatch$, $M \nothaspatch \p$. So by coherence/inclusion $C
646 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
648 We will consider some $D$ and prove the Exclusive Tip Contents form.
650 \subsubsection{For $D \in \py$:}
651 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
654 \subsubsection{For $D \not\in \py, R \not\in \py$:}
656 $D \neq C$. By Tip Contents of $L$,
657 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
658 $D \isin L \equiv D \isin M$. xxx up to here
661 \subsubsection{For $D \not\in \py, R \in \py$:}
668 xxx the coherence is not that useful ?
672 xxx need to recheck this
674 $C \in \py$ $C \haspatch P$ so $D \isin C \equiv D \le C$. OK.
676 \subsubsection{For $L \in \py, D \not\in \py, R \in \py$:}
678 Tip Contents for $L$: $D \isin L \equiv D \isin \baseof{L}$.
680 Tip Contents for $R$: $D \isin R \equiv D \isin \baseof{R}$.
682 But by Tip Merge, $\baseof{R} \ge \baseof{L}$