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 \usepackage{fancyhdr}
  12 \pagestyle{fancy}
  13 \lhead[\rightmark]{}
  14
  15 \let\stdsection\section
  16 \renewcommand\section{\newpage\stdsection}
  17
  18 \renewcommand{\ge}{\geqslant}
  19 \renewcommand{\le}{\leqslant}
  20 \newcommand{\nge}{\ngeqslant}
  21 \newcommand{\nle}{\nleqslant}
  22
  23 \newcommand{\has}{\sqsupseteq}
  24 \newcommand{\isin}{\sqsubseteq}
  25
  26 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
  27 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
  28 \newcommand{\haspatch}{\sqSupset}
  29 \newcommand{\patchisin}{\sqSubset}
  30
  31         \newif\ifhidehack\hidehackfalse
  32         \DeclareRobustCommand\hidefromedef[2]{%
  33           \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
  34         \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
  35
  36 \newcommand{\set}[1]{\mathbb{#1}}
  37 \newcommand{\pay}[1]{\pa{#1}^+}
  38 \newcommand{\pan}[1]{\pa{#1}^-}
  39
  40 \newcommand{\p}{\pa{P}}
  41 \newcommand{\py}{\pay{P}}
  42 \newcommand{\pn}{\pan{P}}
  43
  44 \newcommand{\pq}{\pa{Q}}
  45 \newcommand{\pqy}{\pay{Q}}
  46 \newcommand{\pqn}{\pan{Q}}
  47
  48 \newcommand{\pr}{\pa{R}}
  49 \newcommand{\pry}{\pay{R}}
  50 \newcommand{\prn}{\pan{R}}
  51
  52 %\newcommand{\hasparents}{\underaccent{1}{>}}
  53 %\newcommand{\hasparents}{{%
  54 %  \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
  55 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
  56 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
  57
  58 \renewcommand{\implies}{\Rightarrow}
  59 \renewcommand{\equiv}{\Leftrightarrow}
  60 \renewcommand{\nequiv}{\nLeftrightarrow}
  61 \renewcommand{\land}{\wedge}
  62 \renewcommand{\lor}{\vee}
  63
  64 \newcommand{\pancs}{{\mathcal A}}
  65 \newcommand{\pends}{{\mathcal E}}
  66
  67 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
  68 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
  69
  70 \newcommand{\merge}{{\mathcal M}}
  71 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
  72 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
  73
  74 \newcommand{\patch}{{\mathcal P}}
  75 \newcommand{\base}{{\mathcal B}}
  76
  77 \newcommand{\patchof}[1]{\patch ( #1 ) }
  78 \newcommand{\baseof}[1]{\base ( #1 ) }
  79
  80 \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
  81 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
  82
  83 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
  84 \newcommand{\bigforall}{%
  85   \mathop{\mathchoice%
  86     {\hbox{\huge$\forall$}}%
  87     {\hbox{\Large$\forall$}}%
  88     {\hbox{\normalsize$\forall$}}%
  89     {\hbox{\scriptsize$\forall$}}}%
  90 }
  91
  92 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
  93 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
  94
  95 \newcommand{\qed}{\square}
  96 \newcommand{\proofstarts}{{\it Proof:}}
  97 \newcommand{\proof}[1]{\proofstarts #1 $\qed$}
  98
  99 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
 100 \newcommand{\gathnext}{\\ \tag*{}}
 101
 102 \newcommand{\true}{t}
 103 \newcommand{\false}{f}
 104
 105 \begin{document}
 106
 107 \section{Notation}
 108
 109 \begin{basedescript}{
 110 \desclabelwidth{5em}
 111 \desclabelstyle{\nextlinelabel}
 112 }
 113 \item[ $ C \hasparents \set X $ ]
 114 The parents of commit $C$ are exactly the set
 115 $\set X$.
 116
 117 \item[ $ C \ge D $ ]
 118 $C$ is a descendant of $D$ in the git commit
 119 graph.  This is a partial order, namely the transitive closure of
 120 $ D \in \set X $ where $ C \hasparents \set X $.
 121
 122 \item[ $ C \has D $ ]
 123 Informally, the tree at commit $C$ contains the change
 124 made in commit $D$.  Does not take account of deliberate reversions by
 125 the user or reversion, rebasing or rewinding in
 126 non-Topbloke-controlled branches.  For merges and Topbloke-generated
 127 anticommits or re-commits, the ``change made'' is only to be thought
 128 of as any conflict resolution.  This is not a partial order because it
 129 is not transitive.
 130
 131 \item[ $ \p, \py, \pn $ ]
 132 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
 133 are respectively the base and tip git branches.  $\p$ may be used
 134 where the context requires a set, in which case the statement
 135 is to be taken as applying to both $\py$ and $\pn$.
 136 All of these sets are disjoint.  Hence:
 137
 138 \item[ $ \patchof{ C } $ ]
 139 Either $\p$ s.t. $ C \in \p $, or $\bot$.
 140 A function from commits to patches' sets $\p$.
 141
 142 \item[ $ \pancsof{C}{\set P} $ ]
 143 $ \{ A \; | \; A \le C \land A \in \set P \} $
 144 i.e. all the ancestors of $C$
 145 which are in $\set P$.
 146
 147 \item[ $ \pendsof{C}{\set P} $ ]
 148 $ \{ E \; | \; E \in \pancsof{C}{\set P}
 149   \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
 150   E \neq A \land E \le A \} $
 151 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
 152
 153 \item[ $ \baseof{C} $ ]
 154 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
 155 A partial function from commits to commits.
 156 See Unique Base, below.
 157
 158 \item[ $ C \haspatch \p $ ]
 159 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
 160 ~ Informally, $C$ has the contents of $\p$.
 161
 162 \item[ $ C \nothaspatch \p $ ]
 163 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
 164 ~ Informally, $C$ has none of the contents of $\p$.
 165
 166 Commits on Non-Topbloke branches are $\nothaspatch \p$ for all $\p$.  This
 167 includes commits on plain git branches made by applying a Topbloke
 168 patch.  If a Topbloke
 169 patch is applied to a non-Topbloke branch and then bubbles back to
 170 the relevant Topbloke branches, we hope that
 171 if the user still cares about the Topbloke patch,
 172 git's merge algorithm will DTRT when trying to re-apply the changes.
 173
 174 \item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
 175 The contents of a git merge result:
 176
 177 $\displaystyle D \isin C \equiv
 178   \begin{cases}
 179     (D \isin L \land D \isin R) \lor D = C : & \true \\
 180     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
 181     \text{otherwise} : & D \not\isin M
 182   \end{cases}
 183 $
 184
 185 \end{basedescript}
 186 \newpage
 187 \section{Invariants}
 188
 189 We maintain these each time we construct a new commit. \\
 190 \[ \eqn{No Replay:}{
 191   C \has D \implies C \ge D
 192 }\]
 193 \[\eqn{Unique Base:}{
 194  \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
 195 }\]
 196 \[\eqn{Tip Contents:}{
 197   \bigforall_{C \in \py} D \isin C \equiv
 198     { D \isin \baseof{C} \lor \atop
 199       (D \in \py \land D \le C) }
 200 }\]
 201 \[\eqn{Base Acyclic:}{
 202   \bigforall_{B \in \pn} D \isin B \implies D \notin \py
 203 }\]
 204 \[\eqn{Coherence:}{
 205   \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
 206 }\]
 207 \[\eqn{Foreign Inclusion:}{
 208   \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
 209 }\]
 210 \[\eqn{Foreign Contents:}{
 211   \bigforall_{C \text{ s.t. } \patchof{C} = \bot}
 212     D \le C \implies \patchof{D} = \bot
 213 }\]
 214
 215 \section{Some lemmas}
 216
 217 \subsection{Alternative (overlapping) formulations of $\mergeof{C}{L}{M}{R}$}
 218 $$
 219  D \isin C \equiv
 220   \begin{cases}
 221     D \isin L  \equiv D \isin R  : & D = C \lor D \isin L     \\
 222     D \isin L \nequiv D \isin R  : & D = C \lor D \not\isin M \\
 223     D \isin L  \equiv D \isin M  : & D = C \lor D \isin R     \\
 224     D \isin L \nequiv D \isin M  : & D = C \lor D \isin L     \\
 225     \text{as above with L and R exchanged}
 226   \end{cases}
 227 $$
 228 \proof{ ~ Truth table (ordered by original definition): \\
 229   \begin{tabular}{cccc|c|cc}
 230      $D = C$ &
 231           $\isin L$ &
 232                $\isin M$ &
 233                     $\isin R$ & $\isin C$ &
 234                                       $L$ vs. $R$ & $L$ vs. $M$
 235   \\\hline
 236      y &  ? &  ? &  ?      &      y   & ?         & ?            \\
 237      n &  y &  y &  y      &      y   & $\equiv$  & $\equiv$     \\
 238      n &  y &  n &  y      &      y   & $\equiv$  & $\nequiv$    \\
 239      n &  n &  y &  n      &      n   & $\equiv$  & $\nequiv$    \\
 240      n &  n &  n &  n      &      n   & $\equiv$  & $\equiv$     \\
 241      n &  y &  y &  n      &      n   & $\nequiv$ & $\equiv$     \\
 242      n &  n &  y &  y      &      n   & $\nequiv$ & $\nequiv$    \\
 243      n &  y &  n &  n      &      y   & $\nequiv$ & $\nequiv$    \\
 244      n &  n &  n &  y      &      y   & $\nequiv$ & $\equiv$     \\
 245   \end{tabular} \\
 246   And original definition is symmetrical in $L$ and $R$.
 247 }
 248
 249 \subsection{Exclusive Tip Contents}
 250 Given Base Acyclic for $C$,
 251 $$
 252   \bigforall_{C \in \py}
 253     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
 254       \Bigr]
 255 $$
 256 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
 257
 258 \proof{
 259 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
 260 So by Base Acyclic $D \isin B \implies D \notin \py$.
 261 }
 262 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
 263   \bigforall_{C \in \py} D \isin C \equiv
 264   \begin{cases}
 265     D \in \py : & D \le C \\
 266     D \not\in \py : & D \isin \baseof{C}
 267   \end{cases}
 268 }\]
 269
 270 \subsection{Tip Self Inpatch}
 271 Given Exclusive Tip Contents and Base Acyclic for $C$,
 272 $$
 273   \bigforall_{C \in \py} C \haspatch \p
 274 $$
 275 Ie, tip commits contain their own patch.
 276
 277 \proof{
 278 Apply Exclusive Tip Contents to some $D \in \py$:
 279 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
 280   D \isin C \equiv D \le C $
 281 }
 282
 283 \subsection{Exact Ancestors}
 284 $$
 285   \bigforall_{ C \hasparents \set{R} }
 286   \left[
 287   D \le C \equiv
 288     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
 289     \lor D = C
 290   \right]
 291 $$
 292 \proof{ ~ Trivial.}
 293
 294 \subsection{Transitive Ancestors}
 295 $$
 296   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
 297   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
 298 $$
 299
 300 \proof{
 301 The implication from right to left is trivial because
 302 $ \pends() \subset \pancs() $.
 303 For the implication from left to right:
 304 by the definition of $\mathcal E$,
 305 for every such $A$, either $A \in \pends()$ which implies
 306 $A \le M$ by the LHS directly,
 307 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
 308 in which case we repeat for $A'$.  Since there are finitely many
 309 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
 310 by the LHS.  And $A \le A''$.
 311 }
 312
 313 \subsection{Calculation of Ends}
 314 $$
 315   \bigforall_{C \hasparents \set A}
 316     \pendsof{C}{\set P} =
 317       \begin{cases}
 318        C \in \p : & \{ C \}
 319       \\
 320        C \not\in \p : & \displaystyle
 321        \left\{ E \Big|
 322            \Bigl[ \Largeexists_{A \in \set A}
 323                        E \in \pendsof{A}{\set P} \Bigr] \land
 324            \Bigl[ \Largenexists_{B \in \set A, F \in \pendsof{B}{\p}}
 325                        E \neq F \land E \le F \Bigr]
 326        \right\}
 327       \end{cases}
 328 $$
 329 \proof{
 330 Trivial for $C \in \set P$.  For $C \not\in \set P$,
 331 $\pancsof{C}{\set P} = \bigcup_{A \in \set A} \pancsof{A}{\set P}$.
 332 So $\pendsof{C}{\set P} \subset \bigcup_{E in \set E} \pendsof{E}{\set P}$.
 333 Consider some $E \in \pendsof{A}{\set P}$.  If $\exists_{B,F}$ as
 334 specified, then either $F$ is going to be in our result and
 335 disqualifies $E$, or there is some other $F'$ (or, eventually,
 336 an $F''$) which disqualifies $F$.
 337 Otherwise, $E$ meets all the conditions for $\pends$.
 338 }
 339
 340 \subsection{Ingredients Prevent Replay}
 341 $$
 342   \left[
 343     {C \hasparents \set A} \land
 344    \\
 345     \bigforall_{D}
 346     \left(
 347        D \isin C \implies
 348        D = C \lor
 349        \Largeexists_{A \in \set A} D \isin A
 350     \right)
 351   \right] \implies \left[ \bigforall_{D}
 352     D \isin C \implies D \le C
 353   \right]
 354 $$
 355 \proof{
 356   Trivial for $D = C$.  Consider some $D \neq C$, $D \isin C$.
 357   By the preconditions, there is some $A$ s.t. $D \in \set A$
 358   and $D \isin A$.  By No Replay for $A$, $D \le A$.  And
 359   $A \le C$ so $D \le C$.
 360 }
 361
 362 \subsection{Simple Foreign Inclusion}
 363 $$
 364   \left[
 365     C \hasparents \{ L \}
 366    \land
 367     \bigforall_{D} D \isin C \equiv D \isin L \lor D = C
 368   \right]
 369  \implies
 370   \left[
 371    \bigforall_{D \text{ s.t. } \patchof{D} = \bot}
 372      D \isin C \equiv D \le C
 373   \right]
 374 $$
 375 \proof{
 376 Consider some $D$ s.t. $\patchof{D} = \bot$.
 377 If $D = C$, trivially true.  For $D \neq C$,
 378 by Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
 379 And by Exact Ancestors $D \le L \equiv D \le C$.
 380 So $D \isin C \equiv D \le C$.
 381 }
 382
 383 \subsection{Totally Foreign Contents}
 384 $$
 385    \left[
 386     C \hasparents \set A \land
 387     \patchof{C} = \bot \land
 388       \bigforall_{A \in \set A} \patchof{A} = \bot
 389    \right]
 390   \implies
 391    \left[
 392   \bigforall_{D}
 393     D \le C
 394    \implies
 395     \patchof{D} = \bot
 396    \right]
 397 $$
 398 \proof{
 399 Consider some $D \le C$.  If $D = C$, $\patchof{D} = \bot$ trivially.
 400 If $D \neq C$ then $D \le A$ where $A \in \set A$.  By Foreign
 401 Contents of $A$, $\patchof{D} = \bot$.
 402 }
 403
 404 \section{Commit annotation}
 405
 406 We annotate each Topbloke commit $C$ with:
 407 \gathbegin
 408  \patchof{C}
 409 \gathnext
 410  \baseof{C}, \text{ if } C \in \py
 411 \gathnext
 412  \bigforall_{\pq}
 413    \text{ either } C \haspatch \pq \text{ or } C \nothaspatch \pq
 414 \gathnext
 415  \bigforall_{\pqy \not\ni C} \pendsof{C}{\pqy}
 416 \end{gather}
 417
 418 $\patchof{C}$, for each kind of Topbloke-generated commit, is stated
 419 in the summary in the section for that kind of commit.
 420
 421 Whether $\baseof{C}$ is required, and if so what the value is, is
 422 stated in the proof of Unique Base for each kind of commit.
 423
 424 $C \haspatch \pq$ or $\nothaspatch \pq$ is represented as the
 425 set $\{ \pq | C \haspatch \pq \}$.  Whether $C \haspatch \pq$
 426 is in stated
 427 (in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$
 428 for the ingredients $I$)
 429 in the proof of Coherence for each kind of commit.
 430
 431 $\pendsof{C}{\pq^+}$ is computed, for all Topbloke-generated commits,
 432 using the lemma Calculation of Ends, above.
 433 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
 434 make it wrong to make plain commits with git because the recorded $\pends$
 435 would have to be updated.  The annotation is not needed in that case
 436 because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
 437
 438 \section{Simple commit}
 439
 440 A simple single-parent forward commit $C$ as made by git-commit.
 441 \begin{gather}
 442 \tag*{} C \hasparents \{ L \} \\
 443 \tag*{} \patchof{C} = \patchof{L} \\
 444 \tag*{} D \isin C \equiv D \isin L \lor D = C
 445 \end{gather}
 446 This also covers Topbloke-generated commits on plain git branches:
 447 Topbloke strips the metadata when exporting.
 448
 449 \subsection{No Replay}
 450
 451 Ingredients Prevent Replay applies.  $\qed$
 452
 453 \subsection{Unique Base}
 454 If $L, C \in \py$ then by Calculation of Ends,
 455 $\pendsof{C}{\pn} = \pendsof{L}{\pn}$ so
 456 $\baseof{C} = \baseof{L}$. $\qed$
 457
 458 \subsection{Tip Contents}
 459 We need to consider only $L, C \in \py$.  From Tip Contents for $L$:
 460 \[ D \isin L \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L ) \]
 461 Substitute into the contents of $C$:
 462 \[ D \isin C \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L )
 463     \lor D = C \]
 464 Since $D = C \implies D \in \py$,
 465 and substituting in $\baseof{C}$, from Unique Base above, this gives:
 466 \[ D \isin C \equiv D \isin \baseof{C} \lor
 467     (D \in \py \land D \le L) \lor
 468     (D = C \land D \in \py) \]
 469 \[ \equiv D \isin \baseof{C} \lor
 470    [ D \in \py \land ( D \le L \lor D = C ) ] \]
 471 So by Exact Ancestors:
 472 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
 473 ) \]
 474 $\qed$
 475
 476 \subsection{Base Acyclic}
 477
 478 Need to consider only $L, C \in \pn$.
 479
 480 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 481
 482 For $D \neq C$: $D \isin C \equiv D \isin L$, so by Base Acyclic for
 483 $L$, $D \isin C \implies D \not\in \py$.
 484
 485 $\qed$
 486
 487 \subsection{Coherence and patch inclusion}
 488
 489 Need to consider $D \in \py$
 490
 491 \subsubsection{For $L \haspatch P, D = C$:}
 492
 493 Ancestors of $C$:
 494 $ D \le C $.
 495
 496 Contents of $C$:
 497 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 498
 499 \subsubsection{For $L \haspatch P, D \neq C$:}
 500 Ancestors: $ D \le C \equiv D \le L $.
 501
 502 Contents: $ D \isin C \equiv D \isin L \lor f $
 503 so $ D \isin C \equiv D \isin L $.
 504
 505 So:
 506 \[ L \haspatch P \implies C \haspatch P \]
 507
 508 \subsubsection{For $L \nothaspatch P$:}
 509
 510 Firstly, $C \not\in \py$ since if it were, $L \in \py$.
 511 Thus $D \neq C$.
 512
 513 Now by contents of $L$, $D \notin L$, so $D \notin C$.
 514
 515 So:
 516 \[ L \nothaspatch P \implies C \nothaspatch P \]
 517 $\qed$
 518
 519 \subsection{Foreign Inclusion:}
 520
 521 Simple Foreign Inclusion applies.  $\qed$
 522
 523 \subsection{Foreign Contents:}
 524
 525 Only relevant if $\patchof{C} = \bot$, and in that case Totally
 526 Foreign Contents applies. $\qed$
 527
 528 \section{Create Base}
 529
 530 Given a starting point $L$ and a proposed patch $\pq$,
 531 create a Topbloke base branch initial commit $B$.
 532 \gathbegin
 533  B \hasparents \{ L \}
 534 \gathnext
 535  \patchof{B} = \pqn
 536 \gathnext
 537  D \isin B \equiv D \isin L \lor D = B
 538 \end{gather}
 539
 540 \subsection{Conditions}
 541
 542 \[ \eqn{ Create Acyclic }{
 543  \pendsof{L}{\pqy} = \{ \}
 544 }\]
 545
 546 \subsection{No Replay}
 547
 548 Ingredients Prevent Replay applies.  $\qed$
 549
 550 \subsection{Unique Base}
 551
 552 Not applicable.
 553
 554 \subsection{Tip Contents}
 555
 556 Not applicable.
 557
 558 \subsection{Base Acyclic}
 559
 560 Consider some $D \isin B$.  If $D = B$, $D \in \pqn$.
 561 If $D \neq B$, $D \isin L$, so by No Replay $D \le L$
 562 and by Create Acyclic
 563 $D \not\in \pqy$.  $\qed$
 564
 565 \subsection{Coherence and Patch Inclusion}
 566
 567 Consider some $D \in \py$.
 568 $B \not\in \py$ so $D \neq B$.  So $D \isin B \equiv D \isin L$
 569 and $D \le B \equiv D \le L$.
 570
 571 Thus $L \haspatch \p \implies B \haspatch P$
 572 and $L \nothaspatch \p \implies B \nothaspatch P$.
 573
 574 $\qed$.
 575
 576 \subsection{Foreign Inclusion}
 577
 578 Simple Foreign Inclusion applies. $\qed$
 579
 580 \subsection{Foreign Contents}
 581
 582 Not applicable.
 583
 584 \section{Create Tip}
 585
 586 Given a Topbloke base $B$ for a patch $\pq$,
 587 create a tip branch initial commit B.
 588 \gathbegin
 589  C \hasparents \{ B \}
 590 \gathnext
 591  \patchof{B} = \pqy
 592 \gathnext
 593  D \isin C \equiv D \isin B \lor D = C
 594 \end{gather}
 595
 596 \subsection{Conditions}
 597
 598 \[ \eqn{ Ingredients }{
 599  \patchof{B} = \pqn
 600 }\]
 601 \[ \eqn{ No Sneak }{
 602  \pendsof{B}{\pqy} = \{ \}
 603 }\]
 604
 605 \subsection{No Replay}
 606
 607 Ingredients Prevent Replay applies.  $\qed$
 608
 609 \subsection{Unique Base}
 610
 611 Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$.  $\qed$
 612
 613 \subsection{Tip Contents}
 614
 615 Consider some arbitrary commit $D$.  If $D = C$, trivially satisfied.
 616
 617 If $D \neq C$, $D \isin C \equiv D \isin B$,
 618 which by Unique Base, above, $ \equiv D \isin \baseof{B}$.
 619 By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$.
 620
 621
 622 $\qed$
 623
 624 \subsection{Base Acyclic}
 625
 626 Not applicable.
 627
 628 \subsection{Coherence and Patch Inclusion}
 629
 630 $$
 631 \begin{cases}
 632   \p = \pq    \lor B \haspatch \p : & C \haspatch \p \\
 633   \p \neq \pq \land B \nothaspatch \p : & C \nothaspatch \p
 634 \end{cases}
 635 $$
 636
 637 \proofstarts
 638 ~ Consider some $D \in \py$.
 639
 640 \subsubsection{For $\p = \pq$:}
 641
 642 By Base Acyclic, $D \not\isin B$.  So $D \isin C \equiv D = C$.
 643 By No Sneak, $D \not\le B$ so $D \le C \equiv D = C$.  Thus $C \haspatch \pq$.
 644
 645 \subsubsection{For $\p \neq \pq$:}
 646
 647 $D \neq C$.  So $D \isin C \equiv D \isin B$,
 648 and $D \le C \equiv D \le B$.
 649
 650 $\qed$
 651
 652 \subsection{Foreign Inclusion}
 653
 654 Simple Foreign Inclusion applies.  $\qed$
 655
 656 \subsection{Foreign Contents}
 657
 658 Not applicable.
 659
 660 \section{Dependency Removal}
 661
 662 Given $L$ which contains $\pr$ as represented by $R^+, R^-$.
 663 Construct $C$ which has $\pr$ removed by applying a single
 664 commit which is the anticommit of $\pr$.
 665 Used for removing a branch dependency.
 666 \gathbegin
 667  C \hasparents \{ L \}
 668 \gathnext
 669  \patchof{C} = \patchof{L}
 670 \gathnext
 671  \mergeof{C}{L}{R^+}{R^-}
 672 \end{gather}
 673
 674 \subsection{Conditions}
 675
 676 \[ \eqn{ Ingredients }{
 677 R^+ \in \pry \land R^- = \baseof{R^+}
 678 }\]
 679 \[ \eqn{ Into Base }{
 680  L \in \pqn
 681 }\]
 682 \[ \eqn{ Unique Tip }{
 683  \pendsof{L}{\pry} = \{ R^+ \}
 684 }\]
 685 \[ \eqn{ Currently Included }{
 686  L \haspatch \pry
 687 }\]
 688
 689 \subsection{Ordering of Ingredients:}
 690
 691 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
 692 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$.
 693 $\qed$
 694
 695 (Note that $R^+ \not\le R^-$, i.e. the merge base
 696 is a descendant, not an ancestor, of the 2nd parent.)
 697
 698 \subsection{No Replay}
 699
 700 By $\merge$,
 701 $D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$.
 702 So, by Ordering of Ingredients,
 703 Ingredients Prevent Replay applies.  $\qed$
 704
 705 \subsection{Desired Contents}
 706
 707 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
 708 \proofstarts
 709
 710 \subsubsection{For $D = C$:}
 711
 712 Trivially $D \isin C$.  OK.
 713
 714 \subsubsection{For $D \neq C, D \not\le L$:}
 715
 716 By No Replay for $L$, $D \not\isin L$.
 717 Also, by Ordering of Ingredients, $D \not\le R^-$ hence
 718 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
 719
 720 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
 721
 722 By Currently Included, $D \isin L$.
 723
 724 By Tip Self Inpatch for $R^+$, $D \isin R^+ \equiv D \le R^+$, but by
 725 by Unique Tip, $D \le R^+ \equiv D \le L$.
 726 So $D \isin R^+$.
 727
 728 By Base Acyclic for $R^-$, $D \not\isin R^-$.
 729
 730 Apply $\merge$: $D \not\isin C$.  OK.
 731
 732 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
 733
 734 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
 735
 736 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
 737
 738 $\qed$
 739
 740 \subsection{Unique Base}
 741
 742 Into Base means that $C \in \pqn$, so Unique Base is not
 743 applicable. $\qed$
 744
 745 \subsection{Tip Contents}
 746
 747 Again, not applicable. $\qed$
 748
 749 \subsection{Base Acyclic}
 750
 751 By Into Base and Base Acyclic for $L$, $D \isin L \implies D \not\in \pqy$.
 752 And by Into Base $C \not\in \pqy$.
 753 Now from Desired Contents, above, $D \isin C
 754 \implies D \isin L \lor D = C$, which thus
 755 $\implies D \not\in \pqy$.  $\qed$.
 756
 757 \subsection{Coherence and Patch Inclusion}
 758
 759 Need to consider some $D \in \py$.  By Into Base, $D \neq C$.
 760
 761 \subsubsection{For $\p = \pr$:}
 762 By Desired Contents, above, $D \not\isin C$.
 763 So $C \nothaspatch \pr$.
 764
 765 \subsubsection{For $\p \neq \pr$:}
 766 By Desired Contents, $D \isin C \equiv D \isin L$
 767 (since $D \in \py$ so $D \not\in \pry$).
 768
 769 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
 770 So $L \nothaspatch \p \implies C \nothaspatch \p$.
 771
 772 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
 773 so $L \haspatch \p \implies C \haspatch \p$.
 774
 775 $\qed$
 776
 777 \subsection{Foreign Inclusion}
 778
 779 Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
 780 So by Desired Contents $D \isin C \equiv D \isin L$.
 781 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
 782
 783 And $D \le C \equiv D \le L$.
 784 Thus $D \isin C \equiv D \le C$.
 785
 786 $\qed$
 787
 788 \subsection{Foreign Contents}
 789
 790 Not applicable.
 791
 792 \section{Dependency Insertion}
 793
 794 Given $L$ construct $C$ which additionally
 795 contains $\pr$ as represented by $R^+$ and $R^-$.
 796 This may even be used for reintroducing a previous-removed branch
 797 dependency.
 798 \gathbegin
 799  C \hasparents \{ L, R^+ \}
 800 \gathnext
 801  \patchof{C} = \patchof{L}
 802 \gathnext
 803  \mergeof{C}{L}{R^-}{R^+}
 804 \end{gather}
 805
 806 \subsection{Conditions}
 807
 808 \[ \eqn{ Ingredients }{
 809  R^- = \baseof{R^+}
 810 }\]
 811 \[ \eqn{ Into Base }{
 812  L \in \pqn
 813 }\]
 814 \[ \eqn{ Currently Excluded }{
 815  L \nothaspatch \pr
 816 }\]
 817 \[ \eqn{ Inserted's Ends }{
 818  E \in \pendsof{L}{\pry} \implies E \le R^+
 819 }\]
 820 \[ \eqn{ Others' Ends }{
 821  \bigforall_{\p \patchisin \L}
 822  E \in \pendsof{R^+}{\py} \implies E \le L
 823 }\]
 824 \[ \eqn{ Insertion Acyclic }{
 825  R^+ \nothaspatch \pq
 826 }\]
 827
 828 \subsection{No Replay}
 829
 830 By $\merge$,
 831 $D \isin C \implies D \isin L \lor D \isin R^+ \lor D = C$.
 832 So Ingredients Prevent Replay applies. $\qed$
 833
 834 \subsection{Unique Base}
 835
 836 Not applicable.
 837
 838 \subsection{Tip Contents}
 839
 840 Not applicable.
 841
 842 \subsection{Base Acyclic}
 843
 844 Consider some $D \isin C$.  We will show that $D \not\in \pqy$.
 845 By $\merge$, $D \isin L \lor D \isin R^+ \lor D = C$.
 846
 847 For $D \isin L$, Base Acyclic for L suffices.  For $D \isin R^+$,
 848 Insertion Acyclic suffices.  For $D = C$, trivial.  $\qed$.
 849
 850 \subsection{Coherence and Patch Inclusion}
 851
 852 $$
 853 \begin{cases}
 854   \p = \pr    \lor L \haspatch \p : & C \haspatch \p \\
 855   \p \neq \pr \land L \nothaspatch \p : & C \nothaspatch \p
 856 \end{cases}
 857 $$
 858
 859 \proofstarts
 860 ~ Consider some $D \in \py$.
 861 $D \neq C$ so $D \le C \equiv D \le L \lor D \le R^+$.
 862
 863 \subsubsection{For $\p = \pr$:}
 864
 865 $D \not\isin L$ by Currently Excluded.
 866 $D \not\isin R^-$ by Base Acyclic.
 867 So by $\merge$, $D \isin C \equiv D \isin R^+$,
 868 which by Tip Self Inpatch of $R^+$, $\equiv D \le R^+$.
 869
 870 And by definition of $\pancs$,
 871 $D \le L \equiv D \in \pancsof{L}{R^+}$.
 872 Applying Transitive Ancestors to Inserted's Ends gives
 873 $A \in \pancsof{L}{R^+} \implies A \le R^+$.
 874 So $D \le L \implies D \le R^+$.
 875 Thus $D \le C \equiv D \le R^+$.
 876
 877 So $D \isin C \equiv D \le C$, i.e. $C \haspatch \pr$.
 878 OK.
 879
 880 \subsubsection{For $\p \neq \pr$:}
 881
 882 By Exclusive Tip Contents for $R^+$ ($D \not\in \pry$ case)
 883 $D \isin R^+ \equiv D \isin R^-$.
 884 So by $\merge$, $D \isin C \equiv D \isin L$.
 885
 886 If $L \nothaspatch \p$, $D \not\isin L$ so $C \nothaspatch \p$.  OK.
 887
 888 If $L \haspatch \p$, Others' Ends applies; by Transitive
 889 Ancestors, $A \in \pancsof{R^+}{\py} \implies A \le L$.
 890 So $D \le R^+ \implies D \le L$,
 891 since $D \le R^+ \equiv D \in \pancsof{R^+}{\py}$.
 892 Thus $D \le C \equiv D \le L$.
 893 And by $\haspatch$, $D \le L \equiv D \isin L$ so
 894 $D \isin C \equiv D \le C$.  Thus $C \haspatch \p$.
 895 OK.
 896
 897 $\qed$
 898
 899 \subsection{Foreign Inclusion}
 900
 901 Consider some $D$ s.t. $\patchof{D} = \bot$.
 902
 903 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
 904 So by $\merge$, $D \isin C \equiv D \isin L$.
 905
 906 xxx up to here, need new condition
 907
 908 $D \neq C$.
 909
 910
 911
 912 \section{Merge}
 913
 914 Merge commits $L$ and $R$ using merge base $M$:
 915 \gathbegin
 916  C \hasparents \{ L, R \}
 917 \gathnext
 918  \patchof{C} = \patchof{L}
 919 \gathnext
 920  \mergeof{C}{L}{M}{R}
 921 \end{gather}
 922 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
 923
 924 \subsection{Conditions}
 925 \[ \eqn{ Ingredients }{
 926  M \le L, M \le R
 927 }\]
 928 \[ \eqn{ Tip Merge }{
 929  L \in \py \implies
 930    \begin{cases}
 931       R \in \py : & \baseof{R} \ge \baseof{L}
 932               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
 933       R \in \pn : & M = \baseof{L} \\
 934       \text{otherwise} : & \false
 935    \end{cases}
 936 }\]
 937 \[ \eqn{ Merge Acyclic }{
 938     L \in \pn
 939    \implies
 940     R \nothaspatch \p
 941 }\]
 942 \[ \eqn{ Removal Merge Ends }{
 943     X \not\haspatch \p \land
 944     Y \haspatch \p \land
 945     M \haspatch \p
 946   \implies
 947     \pendsof{Y}{\py} = \pendsof{M}{\py}
 948 }\]
 949 \[ \eqn{ Addition Merge Ends }{
 950     X \not\haspatch \p \land
 951     Y \haspatch \p \land
 952     M \nothaspatch \p
 953    \implies \left[
 954     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
 955    \right]
 956 }\]
 957 \[ \eqn{ Foreign Merges }{
 958     \patchof{L} = \bot \equiv \patchof{R} = \bot
 959 }\]
 960
 961 \subsection{Non-Topbloke merges}
 962
 963 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$
 964 (Foreign Merges, above).
 965 I.e. not only is it forbidden to merge into a Topbloke-controlled
 966 branch without Topbloke's assistance, it is also forbidden to
 967 merge any Topbloke-controlled branch into any plain git branch.
 968
 969 Given those conditions, Tip Merge and Merge Acyclic do not apply.
 970 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
 971 Merge Ends condition applies.
 972
 973 So a plain git merge of non-Topbloke branches meets the conditions and
 974 is therefore consistent with our model.
 975
 976 \subsection{No Replay}
 977
 978 By definition of $\merge$,
 979 $D \isin C \implies D \isin L \lor D \isin R \lor D = C$.
 980 So, by Ingredients,
 981 Ingredients Prevent Replay applies.  $\qed$
 982
 983 \subsection{Unique Base}
 984
 985 Need to consider only $C \in \py$, ie $L \in \py$,
 986 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 987 putative ancestor $A \in \pn$ and see whether $A \le C$.
 988
 989 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 990 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 991 Thus $A \le C \equiv A \le L \lor A \le R$.
 992
 993 By Unique Base of L and Transitive Ancestors,
 994 $A \le L \equiv A \le \baseof{L}$.
 995
 996 \subsubsection{For $R \in \py$:}
 997
 998 By Unique Base of $R$ and Transitive Ancestors,
 999 $A \le R \equiv A \le \baseof{R}$.
1000
1001 But by Tip Merge condition on $\baseof{R}$,
1002 $A \le \baseof{L} \implies A \le \baseof{R}$, so
1003 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
1004 Thus $A \le C \equiv A \le \baseof{R}$.
1005 That is, $\baseof{C} = \baseof{R}$.
1006
1007 \subsubsection{For $R \in \pn$:}
1008
1009 By Tip Merge condition on $R$ and since $M \le R$,
1010 $A \le \baseof{L} \implies A \le R$, so
1011 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
1012 Thus $A \le C \equiv A \le R$.
1013 That is, $\baseof{C} = R$.
1014
1015 $\qed$
1016
1017 \subsection{Coherence and Patch Inclusion}
1018
1019 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
1020 This involves considering $D \in \py$.
1021
1022 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
1023 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
1024 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch for $L$).  So $D \neq C$.
1025 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
1026
1027 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
1028 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
1029 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
1030
1031 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
1032
1033 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
1034  \equiv D \isin L \lor D \isin R$.
1035 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
1036
1037 Consider $D \neq C, D \isin X \land D \isin Y$:
1038 By $\merge$, $D \isin C$.  Also $D \le X$
1039 so $D \le C$.  OK for $C \haspatch \p$.
1040
1041 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
1042 By $\merge$, $D \not\isin C$.
1043 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
1044 OK for $C \haspatch \p$.
1045
1046 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
1047 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
1048 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
1049 OK for $C \haspatch \p$.
1050
1051 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
1052
1053 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
1054
1055 $M \haspatch \p \implies C \nothaspatch \p$.
1056 $M \nothaspatch \p \implies C \haspatch \p$.
1057
1058 \proofstarts
1059
1060 One of the Merge Ends conditions applies.
1061 Recall that we are considering $D \in \py$.
1062 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
1063 We will show for each of
1064 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
1065 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
1066
1067 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
1068 Self Inpatch for $L$, $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
1069 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
1070 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
1071
1072 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
1073 $D \le Y$ so $D \le C$.
1074 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
1075
1076 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
1077 $D \not\le Y$.  If $D \le X$ then
1078 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
1079 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
1080 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
1081
1082 Consider $D \neq C, M \haspatch P, D \isin Y$:
1083 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
1084 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
1085 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
1086
1087 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
1088 By $\merge$, $D \not\isin C$.  OK.
1089
1090 $\qed$
1091
1092 \subsection{Base Acyclic}
1093
1094 This applies when $C \in \pn$.
1095 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
1096
1097 Consider some $D \in \py$.
1098
1099 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
1100 R$.  And $D \neq C$.  So $D \not\isin C$.
1101
1102 $\qed$
1103
1104 \subsection{Tip Contents}
1105
1106 We need worry only about $C \in \py$.
1107 And $\patchof{C} = \patchof{L}$
1108 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
1109 of $C$, and its Coherence and Patch Inclusion, as just proved.
1110
1111 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
1112 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
1113 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
1114 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
1115 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
1116
1117 We will consider an arbitrary commit $D$
1118 and prove the Exclusive Tip Contents form.
1119
1120 \subsubsection{For $D \in \py$:}
1121 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
1122 \le C$.  OK.
1123
1124 \subsubsection{For $D \not\in \py, R \not\in \py$:}
1125
1126 $D \neq C$.  By Tip Contents of $L$,
1127 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
1128 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
1129 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
1130 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
1131
1132 \subsubsection{For $D \not\in \py, R \in \py$:}
1133
1134 $D \neq C$.
1135
1136 By Tip Contents
1137 $D \isin L \equiv D \isin \baseof{L}$ and
1138 $D \isin R \equiv D \isin \baseof{R}$.
1139
1140 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
1141 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
1142 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
1143 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
1144
1145 So $D \isin M \equiv D \isin L$ and by $\merge$,
1146 $D \isin C \equiv D \isin R$.  But from Unique Base,
1147 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
1148
1149 $\qed$
1150
1151 \subsection{Foreign Inclusion}
1152
1153 Consider some $D$ s.t. $\patchof{D} = \bot$.
1154 By Foreign Inclusion of $L, M, R$:
1155 $D \isin L \equiv D \le L$;
1156 $D \isin M \equiv D \le M$;
1157 $D \isin R \equiv D \le R$.
1158
1159 \subsubsection{For $D = C$:}
1160
1161 $D \isin C$ and $D \le C$.  OK.
1162
1163 \subsubsection{For $D \neq C, D \isin M$:}
1164
1165 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
1166 R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.
1167
1168 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
1169
1170 By $\merge$, $D \isin C$.
1171 And $D \isin X$ means $D \le X$ so $D \le C$.
1172 OK.
1173
1174 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
1175
1176 By $\merge$, $D \not\isin C$.
1177 And $D \not\le L, D \not\le R$ so $D \not\le C$.
1178 OK
1179
1180 $\qed$
1181
1182 \subsection{Foreign Contents}
1183
1184 Only relevant if $\patchof{L} = \bot$, in which case
1185 $\patchof{C} = \bot$ and by Foreign Merges $\patchof{R} = \bot$,
1186 so Totally Foreign Contents applies.  $\qed$
1187
1188 \end{document}