chiark / gitweb /
merge conditions into conditions
[topbloke-formulae.git] / article.tex
1 \documentclass[a4paper,leqno]{strayman}
2 \errorcontextlines=50
3 \let\numberwithin=\notdef
4 \usepackage{amsmath}
5 \usepackage{mathabx}
6 \usepackage{txfonts}
7 \usepackage{amsfonts}
8 \usepackage{mdwlist}
9 %\usepackage{accents}
10
11 \renewcommand{\ge}{\geqslant}
12 \renewcommand{\le}{\leqslant}
13 \newcommand{\nge}{\ngeqslant}
14 \newcommand{\nle}{\nleqslant}
15
16 \newcommand{\has}{\sqsupseteq}
17 \newcommand{\isin}{\sqsubseteq}
18
19 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
20 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
21 \newcommand{\haspatch}{\sqSupset}
22 \newcommand{\patchisin}{\sqSubset}
23
24         \newif\ifhidehack\hidehackfalse
25         \DeclareRobustCommand\hidefromedef[2]{%
26           \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
27         \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
28
29 \newcommand{\set}[1]{\mathbb{#1}}
30 \newcommand{\pay}[1]{\pa{#1}^+}
31 \newcommand{\pan}[1]{\pa{#1}^-}
32
33 \newcommand{\p}{\pa{P}}
34 \newcommand{\py}{\pay{P}}
35 \newcommand{\pn}{\pan{P}}
36
37 \newcommand{\pr}{\pa{R}}
38 \newcommand{\pry}{\pay{R}}
39 \newcommand{\prn}{\pan{R}}
40
41 %\newcommand{\hasparents}{\underaccent{1}{>}}
42 %\newcommand{\hasparents}{{%
43 %  \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
44 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
45 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
46
47 \renewcommand{\implies}{\Rightarrow}
48 \renewcommand{\equiv}{\Leftrightarrow}
49 \renewcommand{\nequiv}{\nLeftrightarrow}
50 \renewcommand{\land}{\wedge}
51 \renewcommand{\lor}{\vee}
52
53 \newcommand{\pancs}{{\mathcal A}}
54 \newcommand{\pends}{{\mathcal E}}
55
56 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
57 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
58
59 \newcommand{\merge}{{\mathcal M}}
60 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
61 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
62
63 \newcommand{\patch}{{\mathcal P}}
64 \newcommand{\base}{{\mathcal B}}
65
66 \newcommand{\patchof}[1]{\patch ( #1 ) }
67 \newcommand{\baseof}[1]{\base ( #1 ) }
68
69 \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
70 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
71
72 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
73 \newcommand{\bigforall}{%
74   \mathop{\mathchoice%
75     {\hbox{\huge$\forall$}}%
76     {\hbox{\Large$\forall$}}%
77     {\hbox{\normalsize$\forall$}}%
78     {\hbox{\scriptsize$\forall$}}}%
79 }
80
81 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
82 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
83
84 \newcommand{\qed}{\square}
85 \newcommand{\proofstarts}{{\it Proof:}}
86 \newcommand{\proof}[1]{\proofstarts #1 $\qed$}
87
88 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
89 \newcommand{\gathnext}{\\ \tag*{}}
90
91 \newcommand{\true}{t}
92 \newcommand{\false}{f}
93
94 \begin{document}
95
96 \section{Notation}
97
98 \begin{basedescript}{
99 \desclabelwidth{5em}
100 \desclabelstyle{\nextlinelabel}
101 }
102 \item[ $ C \hasparents \set X $ ]
103 The parents of commit $C$ are exactly the set
104 $\set X$.
105
106 \item[ $ C \ge D $ ]
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 $.
110
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
118 is not transitive.
119
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:
126
127 \item[ $ \patchof{ C } $ ]
128 Either $\p$ s.t. $ C \in \p $, or $\bot$.  
129 A function from commits to patches' sets $\p$.
130
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$.
135
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}$.
141
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.
146
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$.
150
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$.  
154
155 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$.  This
156 includes commits on plain git branches made by applying a Topbloke
157 patch.  If a Topbloke
158 patch is applied to a non-Topbloke branch and then bubbles back to
159 the relevant Topbloke branches, we hope that 
160 if the user still cares about the Topbloke patch,
161 git's merge algorithm will DTRT when trying to re-apply the changes.
162
163 \item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
164 The contents of a git merge result:
165
166 $\displaystyle D \isin C \equiv
167   \begin{cases}
168     (D \isin L \land D \isin R) \lor D = C : & \true \\
169     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
170     \text{otherwise} : & D \not\isin M
171   \end{cases}
172
173
174 \end{basedescript}
175 \newpage
176 \section{Invariants}
177
178 We maintain these each time we construct a new commit. \\
179 \[ \eqn{No Replay:}{
180   C \has D \implies C \ge D
181 }\]
182 \[\eqn{Unique Base:}{
183  \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
184 }\]
185 \[\eqn{Tip Contents:}{
186   \bigforall_{C \in \py} D \isin C \equiv
187     { D \isin \baseof{C} \lor \atop
188       (D \in \py \land D \le C) }
189 }\]
190 \[\eqn{Base Acyclic:}{
191   \bigforall_{B \in \pn} D \isin B \implies D \notin \py
192 }\]
193 \[\eqn{Coherence:}{
194   \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
195 }\]
196 \[\eqn{Foreign Inclusion:}{
197   \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
198 }\]
199
200 \section{Some lemmas}
201
202 \[ \eqn{Alternative (overlapping) formulations defining
203   $\mergeof{C}{L}{M}{R}$:}{
204  D \isin C \equiv
205   \begin{cases}
206     D \isin L  \equiv D \isin R  : & D = C \lor D \isin L     \\
207     D \isin L \nequiv D \isin R  : & D = C \lor D \not\isin M \\
208     D \isin L  \equiv D \isin M  : & D = C \lor D \isin R     \\
209     D \isin L \nequiv D \isin M  : & D = C \lor D \isin L     \\
210     \text{as above with L and R exchanged}
211   \end{cases}
212 }\]
213 \proof{
214   Truth table xxx
215
216   Original definition is symmetrical in $L$ and $R$.
217 }
218
219 \[ \eqn{Exclusive Tip Contents:}{
220   \bigforall_{C \in \py} 
221     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
222       \Bigr]
223 }\]
224 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
225
226 \proof{
227 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
228 So by Base Acyclic $D \isin B \implies D \notin \py$.
229 }
230 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
231   \bigforall_{C \in \py} D \isin C \equiv
232   \begin{cases}
233     D \in \py : & D \le C \\
234     D \not\in \py : & D \isin \baseof{C}
235   \end{cases}
236 }\]
237
238 \[ \eqn{Tip Self Inpatch:}{
239   \bigforall_{C \in \py} C \haspatch \p
240 }\]
241 Ie, tip commits contain their own patch.
242
243 \proof{
244 Apply Exclusive Tip Contents to some $D \in \py$:
245 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
246   D \isin C \equiv D \le C $
247 }
248
249 \[ \eqn{Exact Ancestors:}{
250   \bigforall_{ C \hasparents \set{R} }
251   D \le C \equiv
252     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
253     \lor D = C
254 }\]
255 xxx proof tbd
256
257 \[ \eqn{Transitive Ancestors:}{
258   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
259   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
260 }\]
261
262 \proof{
263 The implication from right to left is trivial because
264 $ \pends() \subset \pancs() $.
265 For the implication from left to right: 
266 by the definition of $\mathcal E$,
267 for every such $A$, either $A \in \pends()$ which implies
268 $A \le M$ by the LHS directly,
269 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
270 in which case we repeat for $A'$.  Since there are finitely many
271 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
272 by the LHS.  And $A \le A''$.
273 }
274
275 \[ \eqn{Calculation Of Ends:}{
276   \bigforall_{C \hasparents \set A}
277     \pendsof{C}{\set P} =
278       \begin{cases}
279        C \in \p : & \{ C \}
280       \\
281        C \not\in \p : & \displaystyle
282        \left\{ E \Big|
283            \Bigl[ \Largeexists_{A \in \set A} 
284                        E \in \pendsof{A}{\set P} \Bigr] \land
285            \Bigl[ \Largenexists_{B \in \set A} 
286                        E \neq B \land E \le B \Bigr]
287        \right\}
288       \end{cases}
289 }\]
290 xxx proof tbd
291
292 \subsection{No Replay for Merge Results}
293
294 If we are constructing $C$, with,
295 \gathbegin
296   \mergeof{C}{L}{M}{R}
297 \gathnext
298   L \le C
299 \gathnext
300   R \le C
301 \end{gather}
302 No Replay is preserved.  \proofstarts
303
304 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
305
306 \subsubsection{For $D \isin L \land D \isin R$:}
307 $D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
308
309 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
310 $D \not\isin C$.  OK.
311
312 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
313  \land D \not\isin M$:}
314 $D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
315 R$ so $D \le C$.  OK.
316
317 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
318  \land D \isin M$:}
319 $D \not\isin C$.  OK.
320
321 $\qed$
322
323 \section{Commit annotation}
324
325 We annotate each Topbloke commit $C$ with:
326 \gathbegin
327  \patchof{C}
328 \gathnext
329  \baseof{C}, \text{ if } C \in \py
330 \gathnext
331  \bigforall_{\pa{Q}} 
332    \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
333 \gathnext
334  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
335 \end{gather}
336
337 $\patchof{C}$, for each kind of Topbloke-generated commit, is stated
338 in the summary in the section for that kind of commit.
339
340 Whether $\baseof{C}$ is required, and if so what the value is, is
341 stated in the proof of Unique Base for each kind of commit.
342
343 $C \haspatch \pa{Q}$ or $\nothaspatch \pa{Q}$ is represented as the
344 set $\{ \pa{Q} | C \haspatch \pa{Q} \}$.  Whether $C \haspatch \pa{Q}$
345 is in stated
346 (in terms of $I \haspatch \pa{Q}$ or $I \nothaspatch \pa{Q}$
347 for the ingredients $I$),
348 in the proof of Coherence for each kind of commit.
349
350 $\pendsof{C}{\pa{Q}^+}$ is computed, for all Topbloke-generated commits,
351 using the lemma Calculation of Ends, above.
352 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
353 make it wrong to make plain commits with git because the recorded $\pends$
354 would have to be updated.  The annotation is not needed in that case
355 because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
356
357 \section{Simple commit}
358
359 A simple single-parent forward commit $C$ as made by git-commit.
360 \begin{gather}
361 \tag*{} C \hasparents \{ A \} \\
362 \tag*{} \patchof{C} = \patchof{A} \\
363 \tag*{} D \isin C \equiv D \isin A \lor D = C
364 \end{gather}
365 This also covers Topbloke-generated commits on plain git branches:
366 Topbloke strips the metadata when exporting.
367
368 \subsection{No Replay}
369 Trivial.
370
371 \subsection{Unique Base}
372 If $A, C \in \py$ then by Calculation of Ends for
373 $C, \py, C \not\in \py$:
374 $\pendsof{C}{\pn} = \pendsof{A}{\pn}$ so
375 $\baseof{C} = \baseof{A}$. $\qed$
376
377 \subsection{Tip Contents}
378 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
379 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
380 Substitute into the contents of $C$:
381 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
382     \lor D = C \]
383 Since $D = C \implies D \in \py$, 
384 and substituting in $\baseof{C}$, this gives:
385 \[ D \isin C \equiv D \isin \baseof{C} \lor
386     (D \in \py \land D \le A) \lor
387     (D = C \land D \in \py) \]
388 \[ \equiv D \isin \baseof{C} \lor
389    [ D \in \py \land ( D \le A \lor D = C ) ] \]
390 So by Exact Ancestors:
391 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
392 ) \]
393 $\qed$
394
395 \subsection{Base Acyclic}
396
397 Need to consider only $A, C \in \pn$.  
398
399 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
400
401 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
402 $A$, $D \isin C \implies D \not\in \py$.
403
404 $\qed$
405
406 \subsection{Coherence and patch inclusion}
407
408 Need to consider $D \in \py$
409
410 \subsubsection{For $A \haspatch P, D = C$:}
411
412 Ancestors of $C$:
413 $ D \le C $.
414
415 Contents of $C$:
416 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
417
418 \subsubsection{For $A \haspatch P, D \neq C$:}
419 Ancestors: $ D \le C \equiv D \le A $.
420
421 Contents: $ D \isin C \equiv D \isin A \lor f $
422 so $ D \isin C \equiv D \isin A $.
423
424 So:
425 \[ A \haspatch P \implies C \haspatch P \]
426
427 \subsubsection{For $A \nothaspatch P$:}
428
429 Firstly, $C \not\in \py$ since if it were, $A \in \py$.  
430 Thus $D \neq C$.
431
432 Now by contents of $A$, $D \notin A$, so $D \notin C$.
433
434 So:
435 \[ A \nothaspatch P \implies C \nothaspatch P \]
436 $\qed$
437
438 \subsection{Foreign inclusion:}
439
440 If $D = C$, trivial.  For $D \neq C$:
441 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
442
443 \section{Create Base}
444
445 xxx tbd
446
447 \section{Create Tip}
448
449 xxx tbd\
450
451 \section{Anticommit}
452
453 Given $L$ and $\pr$ as represented by $R^+, R^-$.
454 Construct $C$ which has $\pr$ removed.
455 Used for removing a branch dependency.
456 \gathbegin
457  C \hasparents \{ L \}
458 \gathnext
459  \patchof{C} = \patchof{L}
460 \gathnext
461  \mergeof{C}{L}{R^+}{R^-}
462 \end{gather}
463
464 \subsection{Conditions}
465
466 \[ \eqn{ Ingredients }{
467 R^+ \in \pry \land R^- = \baseof{R^+}
468 }\]
469 \[ \eqn{ Into Base }{
470  L \in \pn
471 }\]
472 \[ \eqn{ Unique Tip }{
473  \pendsof{L}{\pry} = \{ R^+ \}
474 }\]
475 \[ \eqn{ Currently Included }{
476  L \haspatch \pry
477 }\]
478
479 \subsection{Ordering of ${L, R^+, R^-}$:}
480
481 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
482 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$.
483 $\qed$
484
485 (Note that $R^+ \not\le R^-$, i.e. the merge base
486 is a descendant, not an ancestor, of the 2nd parent.)
487
488 \subsection{No Replay}
489
490 No Replay for Merge Results applies.  $\qed$
491
492 \subsection{Desired Contents}
493
494 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
495 \proofstarts
496
497 \subsubsection{For $D = C$:}
498
499 Trivially $D \isin C$.  OK.
500
501 \subsubsection{For $D \neq C, D \not\le L$:}
502
503 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
504 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
505
506 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
507
508 By Currently Included, $D \isin L$.
509
510 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
511 by Unique Tip, $D \le R^+ \equiv D \le L$.  
512 So $D \isin R^+$.
513
514 By Base Acyclic, $D \not\isin R^-$.
515
516 Apply $\merge$: $D \not\isin C$.  OK.
517
518 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
519
520 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
521
522 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
523
524 $\qed$
525
526 \subsection{Unique Base}
527
528 Into Base means that $C \in \pn$, so Unique Base is not
529 applicable. $\qed$
530
531 \subsection{Tip Contents}
532
533 Again, not applicable. $\qed$
534
535 \subsection{Base Acyclic}
536
537 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
538 And by Into Base $C \not\in \py$.
539 Now from Desired Contents, above, $D \isin C
540 \implies D \isin L \lor D = C$, which thus
541 $\implies D \not\in \py$.  $\qed$.
542
543 \subsection{Coherence and Patch Inclusion}
544
545 Need to consider some $D \in \py$.  By Into Base, $D \neq C$.
546
547 \subsubsection{For $\p = \pr$:}
548 By Desired Contents, above, $D \not\isin C$.
549 So $C \nothaspatch \pr$.
550
551 \subsubsection{For $\p \neq \pr$:}
552 By Desired Contents, $D \isin C \equiv D \isin L$
553 (since $D \in \py$ so $D \not\in \pry$).
554
555 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
556 So $L \nothaspatch \p \implies C \nothaspatch \p$.
557
558 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
559 so $L \haspatch \p \implies C \haspatch \p$.
560
561 $\qed$
562
563 \section{Foreign Inclusion}
564
565 Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
566 So by Desired Contents $D \isin C \equiv D \isin L$.
567 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
568
569 And $D \le C \equiv D \le L$.
570 Thus $D \isin C \equiv D \le C$.
571
572 $\qed$
573
574 \section{Merge}
575
576 Merge commits $L$ and $R$ using merge base $M$:
577 \gathbegin
578  C \hasparents \{ L, R \}
579 \gathnext
580  \patchof{C} = \patchof{L}
581 \gathnext
582  \mergeof{C}{L}{M}{R}
583 \end{gather}
584 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
585
586 \subsection{Conditions}
587 \[ \eqn{ Ingredients }{
588  M \le L, M \le R
589 }\]
590 \[ \eqn{ Tip Merge }{
591  L \in \py \implies
592    \begin{cases}
593       R \in \py : & \baseof{R} \ge \baseof{L}
594               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
595       R \in \pn : & M = \baseof{L} \\
596       \text{otherwise} : & \false
597    \end{cases}
598 }\]
599 \[ \eqn{ Merge Acyclic }{
600     L \in \pn
601    \implies
602     R \nothaspatch \p
603 }\]
604 \[ \eqn{ Removal Merge Ends }{
605     X \not\haspatch \p \land
606     Y \haspatch \p \land
607     M \haspatch \p
608   \implies
609     \pendsof{Y}{\py} = \pendsof{M}{\py}
610 }\]
611 \[ \eqn{ Addition Merge Ends }{
612     X \not\haspatch \p \land
613     Y \haspatch \p \land
614     M \nothaspatch \p
615    \implies \left[
616     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
617    \right]
618 }\]
619
620 \subsection{Non-Topbloke merges}
621
622 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$.
623 I.e. not only is it forbidden to merge into a Topbloke-controlled
624 branch without Topbloke's assistance, it is also forbidden to
625 merge any Topbloke-controlled branch into any plain git branch.
626
627 Given those conditions, Tip Merge and Merge Acyclic do not apply.
628 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
629 Merge Ends condition applies.  Good.
630
631 \subsection{No Replay}
632
633 No Replay for Merge Results applies.  $\qed$
634
635 \subsection{Unique Base}
636
637 Need to consider only $C \in \py$, ie $L \in \py$,
638 and calculate $\pendsof{C}{\pn}$.  So we will consider some
639 putative ancestor $A \in \pn$ and see whether $A \le C$.
640
641 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
642 But $C \in py$ and $A \in \pn$ so $A \neq C$.  
643 Thus $A \le C \equiv A \le L \lor A \le R$.
644
645 By Unique Base of L and Transitive Ancestors,
646 $A \le L \equiv A \le \baseof{L}$.
647
648 \subsubsection{For $R \in \py$:}
649
650 By Unique Base of $R$ and Transitive Ancestors,
651 $A \le R \equiv A \le \baseof{R}$.
652
653 But by Tip Merge condition on $\baseof{R}$,
654 $A \le \baseof{L} \implies A \le \baseof{R}$, so
655 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
656 Thus $A \le C \equiv A \le \baseof{R}$.  
657 That is, $\baseof{C} = \baseof{R}$.
658
659 \subsubsection{For $R \in \pn$:}
660
661 By Tip Merge condition on $R$ and since $M \le R$,
662 $A \le \baseof{L} \implies A \le R$, so
663 $A \le R \lor A \le \baseof{L} \equiv A \le R$.  
664 Thus $A \le C \equiv A \le R$.  
665 That is, $\baseof{C} = R$.
666
667 $\qed$
668
669 \subsection{Coherence and Patch Inclusion}
670
671 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
672 This involves considering $D \in \py$.  
673
674 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
675 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
676 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
677 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
678
679 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
680 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
681 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
682
683 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
684
685 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
686  \equiv D \isin L \lor D \isin R$.  
687 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
688
689 Consider $D \neq C, D \isin X \land D \isin Y$:
690 By $\merge$, $D \isin C$.  Also $D \le X$ 
691 so $D \le C$.  OK for $C \haspatch \p$.
692
693 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
694 By $\merge$, $D \not\isin C$.  
695 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.  
696 OK for $C \haspatch \p$.
697
698 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
699 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.  
700 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
701 OK for $C \haspatch \p$.
702
703 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
704
705 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
706
707 $M \haspatch \p \implies C \nothaspatch \p$.
708 $M \nothaspatch \p \implies C \haspatch \p$.
709
710 \proofstarts
711
712 One of the Merge Ends conditions applies.  
713 Recall that we are considering $D \in \py$.
714 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
715 We will show for each of
716 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
717 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
718
719 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
720 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
721 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
722 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
723
724 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
725 $D \le Y$ so $D \le C$.  
726 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
727
728 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
729 $D \not\le Y$.  If $D \le X$ then
730 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and 
731 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
732 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
733
734 Consider $D \neq C, M \haspatch P, D \isin Y$:
735 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
736 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
737 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
738
739 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
740 By $\merge$, $D \not\isin C$.  OK.
741
742 $\qed$
743
744 \subsection{Base Acyclic}
745
746 This applies when $C \in \pn$.
747 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
748
749 Consider some $D \in \py$.
750
751 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
752 R$.  And $D \neq C$.  So $D \not\isin C$.
753
754 $\qed$
755
756 \subsection{Tip Contents}
757
758 We need worry only about $C \in \py$.  
759 And $\patchof{C} = \patchof{L}$
760 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
761 of $C$, and its Coherence and Patch Inclusion, as just proved.
762
763 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
764 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
765 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
766 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
767 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
768
769 We will consider an arbitrary commit $D$
770 and prove the Exclusive Tip Contents form.
771
772 \subsubsection{For $D \in \py$:}
773 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
774 \le C$.  OK.
775
776 \subsubsection{For $D \not\in \py, R \not\in \py$:}
777
778 $D \neq C$.  By Tip Contents of $L$,
779 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
780 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
781 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
782 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
783
784 \subsubsection{For $D \not\in \py, R \in \py$:}
785
786 $D \neq C$.
787
788 By Tip Contents
789 $D \isin L \equiv D \isin \baseof{L}$ and
790 $D \isin R \equiv D \isin \baseof{R}$.
791
792 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
793 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
794 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
795 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
796
797 So $D \isin M \equiv D \isin L$ and by $\merge$,
798 $D \isin C \equiv D \isin R$.  But from Unique Base,
799 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
800
801 $\qed$
802
803 \subsection{Foreign Inclusion}
804
805 Consider some $D$ s.t. $\patchof{D} = \bot$.
806 By Foreign Inclusion of $L, M, R$:
807 $D \isin L \equiv D \le L$;
808 $D \isin M \equiv D \le M$;
809 $D \isin R \equiv D \le R$.
810
811 \subsubsection{For $D = C$:}
812
813 $D \isin C$ and $D \le C$.  OK.
814
815 \subsubsection{For $D \neq C, D \isin M$:}
816
817 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
818 R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.
819
820 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
821
822 By $\merge$, $D \isin C$.
823 And $D \isin X$ means $D \le X$ so $D \le C$.
824 OK.
825
826 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
827
828 By $\merge$, $D \not\isin C$.
829 And $D \not\le L, D \not\le R$ so $D \not\le C$.
830 OK
831
832 $\qed$
833
834 \end{document}