chiark / gitweb /
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}
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{\land}{\wedge}
50 \renewcommand{\lor}{\vee}
52 \newcommand{\pancs}{{\mathcal A}}
53 \newcommand{\pends}{{\mathcal E}}
55 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
56 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
58 \newcommand{\merge}{{\mathcal M}}
59 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
60 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
62 \newcommand{\patch}{{\mathcal P}}
63 \newcommand{\base}{{\mathcal B}}
65 \newcommand{\patchof}[1]{\patch ( #1 ) }
66 \newcommand{\baseof}[1]{\base ( #1 ) }
68 \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
69 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
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 }
80 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
81 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
83 \newcommand{\qed}{\square}
84 \newcommand{\proofstarts}{{\it Proof:}}
85 \newcommand{\proof}[1]{\proofstarts #1 $\qed$}
87 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
88 \newcommand{\gathnext}{\\ \tag*{}}
90 \newcommand{\true}{t}
91 \newcommand{\false}{f}
93 \begin{document}
95 \section{Notation}
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$.
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$.
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.
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 None of these sets overlap.  Hence:
126 \item[ $\patchof{ C }$ ]
127 Either $\p$ s.t. $C \in \p$, or $\bot$.
128 A function from commits to patches' sets $\p$.
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$.
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}$.
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.
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$.
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$.
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.
159 \item[ $\displaystyle \mergeof{C}{L}{M}{R}$ ]
160 The contents of a git merge result:
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 170 \end{basedescript} 171 \newpage 172 \section{Invariants} 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 }$ 196 \section{Some lemmas} 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. 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 $\eqntag{{\it Corollary - equivalent to Tip Contents}}{ 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 }$ 217 $\eqn{Tip Self Inpatch:}{ 218 \bigforall_{C \in \py} C \haspatch \p 219 }$ 220 Ie, tip commits contain their own patch. 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 } 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 }$ 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 }$ 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. 264 \subsection{No Replay for Merge Results} 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 276 \subsubsection{For$D=C$:}$D \isin C, D \le C$. OK. 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. 281 \subsubsection{For$D \neq C \land D \not\isin L \land D \not\isin R$:} 282$D \not\isin C$. OK. 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. 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. 293$\qed$295 \section{Commit annotation} 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} 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\}$. 314 \section{Simple commit} 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} 323 \subsection{No Replay} 324 Trivial. 326 \subsection{Unique Base} 327 If$A, C \in \py$then$\baseof{C} = \baseof{A}$.$\qed$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$347 \subsection{Base Acyclic} 349 Need to consider only$A, C \in \pn$. 351 For$D = C$:$D \in \pn$so$D \not\in \py$. OK. 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$356 \subsection{Coherence and patch inclusion} 358 Need to consider$D \in \py$360 \subsubsection{For$A \haspatch P, D = C$:} 362 Ancestors of$C$: 363$ D \le C $. 365 Contents of$C$: 366$ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $. 368 \subsubsection{For$A \haspatch P, D \neq C$:} 369 Ancestors:$ D \le C \equiv D \le A $. 371 Contents:$ D \isin C \equiv D \isin A \lor f $372 so$ D \isin C \equiv D \isin A $. 374 So: 375 $A \haspatch P \implies C \haspatch P$ 377 \subsubsection{For$A \nothaspatch P$:} 379 Firstly,$C \not\in \py$since if it were,$A \in \py$. 380 Thus$D \neq C$. 382 Now by contents of$A$,$D \notin A$, so$D \notin C$. 384 So: 385 $A \nothaspatch P \implies C \nothaspatch P$ 386$\qed$388 \subsection{Foreign inclusion:} 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$393 \section{Anticommit} 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} 407 \subsection{Conditions} 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 }$ 419 \subsection{No Replay} 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$425 \subsection{Desired Contents} 427 $D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C$ 428 \proofstarts 430 \subsubsection{For$D = C$:} 432 Trivially$D \isin C$. OK. 434 \subsubsection{For$D \neq C, D \not\le L$:} 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. 439 \subsubsection{For$D \neq C, D \le L, D \in \pry$:} 441 By Currently Included,$D \isin L$. 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^+$. 447 By Base Acyclic,$D \not\isin R^-$. 449 Apply$\merge$:$D \not\isin C$. OK. 451 \subsubsection{For$D \neq C, D \le L, D \notin \pry$:} 453 By Tip Contents for$R^+$,$D \isin R^+ \equiv D \isin R^-$. 455 Apply$\merge$:$D \isin C \equiv D \isin L$. OK. 457$\qed$459 \subsection{Unique Base} 461 Need to consider only$C \in \py$, ie$L \in \py$. 463 xxx tbd 465 xxx need to finish anticommit 467 \section{Merge} 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\}$. 479 \subsection{Conditions} 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 Acyclic }{ 492 L \in \pn 493 \implies 494 R \nothaspatch \p 495 }$ 496 $\eqn{ Removal Merge Ends }{ 497 X \not\haspatch \p \land 498 Y \haspatch \p \land 499 M \haspatch \p 500 \implies 501 \pendsof{Y}{\py} = \pendsof{M}{\py} 502 }$ 503 $\eqn{ Addition Merge Ends }{ 504 X \not\haspatch \p \land 505 Y \haspatch \p \land 506 M \nothaspatch \p 507 \implies \left[ 508 \bigforall_{E \in \pendsof{X}{\py}} E \le Y 509 \right] 510 }$ 512 \subsection{No Replay} 514 See No Replay for Merge Results. 516 \subsection{Unique Base} 518 Need to consider only$C \in \py$, ie$L \in \py$, 519 and calculate$\pendsof{C}{\pn}$. So we will consider some 520 putative ancestor$A \in \pn$and see whether$A \le C$. 522 By Exact Ancestors for C,$A \le C \equiv A \le L \lor A \le R \lor A = C$. 523 But$C \in py$and$A \in \pn$so$A \neq C$. 524 Thus$A \le C \equiv A \le L \lor A \le R$. 526 By Unique Base of L and Transitive Ancestors, 527$A \le L \equiv A \le \baseof{L}$. 529 \subsubsection{For$R \in \py$:} 531 By Unique Base of$R$and Transitive Ancestors, 532$A \le R \equiv A \le \baseof{R}$. 534 But by Tip Merge condition on$\baseof{R}$, 535$A \le \baseof{L} \implies A \le \baseof{R}$, so 536$A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$. 537 Thus$A \le C \equiv A \le \baseof{R}$. 538 That is,$\baseof{C} = \baseof{R}$. 540 \subsubsection{For$R \in \pn$:} 542 By Tip Merge condition on$R$, 543$A \le \baseof{L} \implies A \le R$, so 544$A \le R \lor A \le \baseof{L} \equiv A \le R$. 545 Thus$A \le C \equiv A \le R$. 546 That is,$\baseof{C} = R$. 548$\qed$550 \subsection{Coherence and patch inclusion} 552 Need to determine$C \haspatch \p$based on$L,M,R \haspatch \p$. 553 This involves considering$D \in \py$. 555 \subsubsection{For$L \nothaspatch \p, R \nothaspatch \p$:} 556$D \not\isin L \land D \not\isin R$.$C \not\in \py$(otherwise$L
557 \in \py$ie$L \haspatch \p$by Tip Self Inpatch). So$D \neq C$. 558 Applying$\merge$gives$D \not\isin C$i.e.$C \nothaspatch \p$. 560 \subsubsection{For$L \haspatch \p, R \haspatch \p$:} 561$D \isin L \equiv D \le L$and$D \isin R \equiv D \le R$. 562 (Likewise$D \isin X \equiv D \le X$and$D \isin Y \equiv D \le Y$.) 564 Consider$D = C$:$D \isin C$,$D \le C$, OK for$C \haspatch \p$. 566 For$D \neq C$:$D \le C \equiv D \le L \lor D \le R
567  \equiv D \isin L \lor D \isin R$. 568 (Likewise$D \le C \equiv D \le X \lor D \le Y$.) 570 Consider$D \neq C, D \isin X \land D \isin Y$: 571 By$\merge$,$D \isin C$. Also$D \le X$572 so$D \le C$. OK for$C \haspatch \p$. 574 Consider$D \neq C, D \not\isin X \land D \not\isin Y$: 575 By$\merge$,$D \not\isin C$. 576 And$D \not\le X \land D \not\le Y$so$D \not\le C$. 577 OK for$C \haspatch \p$. 579 Remaining case, wlog, is$D \not\isin X \land D \isin Y$. 580$D \not\le X$so$D \not\le M$so$D \not\isin M$. 581 Thus by$\merge$,$D \isin C$. And$D \le Y$so$D \le C$. 582 OK for$C \haspatch \p$. 584 So indeed$L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$. 586 \subsubsection{For (wlog)$X \not\haspatch \p, Y \haspatch \p$:} 588$C \haspatch \p \equiv M \nothaspatch \p$. 590 \proofstarts 592 One of the Merge Ends conditions applies. 593 Recall that we are considering$D \in \py$. 594$D \isin Y \equiv D \le Y$.$D \not\isin X$. 595 We will show for each of 596 various cases that$D \isin C \equiv M \nothaspatch \p \land D \le C$597 (which suffices by definition of$\haspatch$and$\nothaspatch$). 599 Consider$D = C$: Thus$C \in \py, L \in \py$, and by Tip 600 Self Inpatch$L \haspatch \p$, so$L=Y, R=X$. By Tip Merge, 601$M=\baseof{L}$. So by Base Acyclic$D \not\isin M$, i.e. 602$M \nothaspatch \p$. And indeed$D \isin C$and$D \le C$. OK. 604 Consider$D \neq C, M \nothaspatch P, D \isin Y$: 605$D \le Y$so$D \le C$. 606$D \not\isin M$so by$\merge$,$D \isin C$. OK. 608 Consider$D \neq C, M \nothaspatch P, D \not\isin Y$: 609$D \not\le Y$. If$D \le X$then 610$D \in \pancsof{X}{\py}$, so by Addition Merge Ends and 611 Transitive Ancestors$D \le Y$--- a contradiction, so$D \not\le X$. 612 Thus$D \not\le C$. By$\merge$,$D \not\isin C$. OK. 614 Consider$D \neq C, M \haspatch P, D \isin Y$: 615$D \le Y$so$D \in \pancsof{Y}{\py}$so by Removal Merge Ends 616 and Transitive Ancestors$D \in \pancsof{M}{\py}$so$D \le M$. 617 Thus$D \isin M$. By$\merge$,$D \not\isin C$. OK. 619 Consider$D \neq C, M \haspatch P, D \not\isin Y$: 620 By$\merge$,$D \not\isin C$. OK. 622$\qed$624 \subsection{Base Acyclic} 626 This applies when$C \in \pn$. 627$C \in \pn$when$L \in \pn$so by Merge Acyclic,$R \nothaspatch \p$. 629 Consider some$D \in \py$. 631 By Base Acyclic of$L$,$D \not\isin L$. By the above,$D \not\isin
632 R$. And$D \neq C$. So$D \not\isin C$.$\qed$634 \subsection{Tip Contents} 636 We need worry only about$C \in \py$. 637 And$\patchof{C} = \patchof{L}$638 so$L \in \py$so$L \haspatch \p$. We will use the coherence and 639 patch inclusion of$C$as just proved. 641 Firstly we prove$C \haspatch \p$: If$R \in \py$, then$R \haspatch
642 \p$and by coherence/inclusion$C \haspatch \p$. If$R \not\in \py$643 then by Tip Merge$M = \baseof{L}$so by Base Acyclic and definition 644 of$\nothaspatch$,$M \nothaspatch \p$. So by coherence/inclusion$C
645 \haspatch \p$(whether$R \haspatch \p$or$\nothaspatch$). 647 We will consider some$D$and prove the Exclusive Tip Contents form. 649 \subsubsection{For$D \in \py$:} 650$C \haspatch \p$so by definition of$\haspatch$,$D \isin C \equiv D
651 \le C$. OK. 653 xxx up to here 655 \subsubsection{For$L \in \py, D \not\in \py, R \in \py$:} 658 %D \in \py$:}
662 xxx the coherence is not that useful ?
664 $L \haspatch \p$ by
666 xxx need to recheck this
668 $C \in \py$ $C \haspatch P$ so $D \isin C \equiv D \le C$.  OK.
670 \subsubsection{For $L \in \py, D \not\in \py, R \in \py$:}
672 Tip Contents for $L$: $D \isin L \equiv D \isin \baseof{L}$.
674 Tip Contents for $R$: $D \isin R \equiv D \isin \baseof{R}$.
676 But by Tip Merge, $\baseof{R} \ge \baseof{L}$
678 \end{document}