chiark / gitweb /
a todo item
[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 xxx make all conditions be in conditions, not in (or also in) intro
99
100 \begin{basedescript}{
101 \desclabelwidth{5em}
102 \desclabelstyle{\nextlinelabel}
103 }
104 \item[ $ C \hasparents \set X $ ]
105 The parents of commit $C$ are exactly the set
106 $\set X$.
107
108 \item[ $ C \ge D $ ]
109 $C$ is a descendant of $D$ in the git commit
110 graph.  This is a partial order, namely the transitive closure of 
111 $ D \in \set X $ where $ C \hasparents \set X $.
112
113 \item[ $ C \has D $ ]
114 Informally, the tree at commit $C$ contains the change
115 made in commit $D$.  Does not take account of deliberate reversions by
116 the user or reversion, rebasing or rewinding in
117 non-Topbloke-controlled branches.  For merges and Topbloke-generated
118 anticommits or re-commits, the ``change made'' is only to be thought
119 of as any conflict resolution.  This is not a partial order because it
120 is not transitive.
121
122 \item[ $ \p, \py, \pn $ ]
123 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
124 are respectively the base and tip git branches.  $\p$ may be used
125 where the context requires a set, in which case the statement
126 is to be taken as applying to both $\py$ and $\pn$.
127 None of these sets overlap.  Hence:
128
129 \item[ $ \patchof{ C } $ ]
130 Either $\p$ s.t. $ C \in \p $, or $\bot$.  
131 A function from commits to patches' sets $\p$.
132
133 \item[ $ \pancsof{C}{\set P} $ ]
134 $ \{ A \; | \; A \le C \land A \in \set P \} $ 
135 i.e. all the ancestors of $C$
136 which are in $\set P$.
137
138 \item[ $ \pendsof{C}{\set P} $ ]
139 $ \{ E \; | \; E \in \pancsof{C}{\set P}
140   \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
141   E \neq A \land E \le A \} $ 
142 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
143
144 \item[ $ \baseof{C} $ ]
145 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
146 A partial function from commits to commits.
147 See Unique Base, below.
148
149 \item[ $ C \haspatch \p $ ]
150 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
151 ~ Informally, $C$ has the contents of $\p$.
152
153 \item[ $ C \nothaspatch \p $ ]
154 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
155 ~ Informally, $C$ has none of the contents of $\p$.  
156
157 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$.  This
158 includes commits on plain git branches made by applying a Topbloke
159 patch.  If a Topbloke
160 patch is applied to a non-Topbloke branch and then bubbles back to
161 the relevant Topbloke branches, we hope that 
162 if the user still cares about the Topbloke patch,
163 git's merge algorithm will DTRT when trying to re-apply the changes.
164
165 \item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
166 The contents of a git merge result:
167
168 $\displaystyle D \isin C \equiv
169   \begin{cases}
170     (D \isin L \land D \isin R) \lor D = C : & \true \\
171     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
172     \text{otherwise} : & D \not\isin M
173   \end{cases}
174
175
176 \end{basedescript}
177 \newpage
178 \section{Invariants}
179
180 We maintain these each time we construct a new commit. \\
181 \[ \eqn{No Replay:}{
182   C \has D \implies C \ge D
183 }\]
184 \[\eqn{Unique Base:}{
185  \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
186 }\]
187 \[\eqn{Tip Contents:}{
188   \bigforall_{C \in \py} D \isin C \equiv
189     { D \isin \baseof{C} \lor \atop
190       (D \in \py \land D \le C) }
191 }\]
192 \[\eqn{Base Acyclic:}{
193   \bigforall_{B \in \pn} D \isin B \implies D \notin \py
194 }\]
195 \[\eqn{Coherence:}{
196   \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
197 }\]
198 \[\eqn{Foreign Inclusion:}{
199   \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
200 }\]
201
202 \section{Some lemmas}
203
204 \[ \eqn{Alternative (overlapping) formulations defining
205   $\mergeof{C}{L}{M}{R}$:}{
206  D \isin C \equiv
207   \begin{cases}
208     D \isin L  \equiv D \isin R  : & D = C \lor D \isin L     \\
209     D \isin L \nequiv D \isin R  : & D = C \lor D \not\isin M \\
210     D \isin L  \equiv D \isin M  : & D = C \lor D \isin R     \\
211     D \isin L \nequiv D \isin M  : & D = C \lor D \isin L     \\
212     \text{as above with L and R exchanged}
213   \end{cases}
214 }\]
215 \proof{
216   Truth table xxx
217
218   Original definition is symmetrical in $L$ and $R$.
219 }
220
221 \[ \eqn{Exclusive Tip Contents:}{
222   \bigforall_{C \in \py} 
223     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
224       \Bigr]
225 }\]
226 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
227
228 \proof{
229 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
230 So by Base Acyclic $D \isin B \implies D \notin \py$.
231 }
232 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
233   \bigforall_{C \in \py} D \isin C \equiv
234   \begin{cases}
235     D \in \py : & D \le C \\
236     D \not\in \py : & D \isin \baseof{C}
237   \end{cases}
238 }\]
239
240 \[ \eqn{Tip Self Inpatch:}{
241   \bigforall_{C \in \py} C \haspatch \p
242 }\]
243 Ie, tip commits contain their own patch.
244
245 \proof{
246 Apply Exclusive Tip Contents to some $D \in \py$:
247 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
248   D \isin C \equiv D \le C $
249 }
250
251 \[ \eqn{Exact Ancestors:}{
252   \bigforall_{ C \hasparents \set{R} }
253   D \le C \equiv
254     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
255     \lor D = C
256 }\]
257
258 \[ \eqn{Transitive Ancestors:}{
259   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
260   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
261 }\]
262
263 \proof{
264 The implication from right to left is trivial because
265 $ \pends() \subset \pancs() $.
266 For the implication from left to right: 
267 by the definition of $\mathcal E$,
268 for every such $A$, either $A \in \pends()$ which implies
269 $A \le M$ by the LHS directly,
270 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
271 in which case we repeat for $A'$.  Since there are finitely many
272 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
273 by the LHS.  And $A \le A''$.
274 }
275 \[ \eqn{Calculation Of Ends:}{
276   \bigforall_{C \hasparents \set A}
277     \pendsof{C}{\set P} =
278        \left\{ E \Big|
279            \Bigl[ \Largeexists_{A \in \set A} 
280                        E \in \pendsof{A}{\set P} \Bigr] \land
281            \Bigl[ \Largenexists_{B \in \set A} 
282                        E \neq B \land E \le B \Bigr]
283        \right\}
284 }\]
285 XXX proof TBD.
286
287 \subsection{No Replay for Merge Results}
288
289 If we are constructing $C$, with,
290 \gathbegin
291   \mergeof{C}{L}{M}{R}
292 \gathnext
293   L \le C
294 \gathnext
295   R \le C
296 \end{gather}
297 No Replay is preserved.  \proofstarts
298
299 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
300
301 \subsubsection{For $D \isin L \land D \isin R$:}
302 $D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
303
304 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
305 $D \not\isin C$.  OK.
306
307 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
308  \land D \not\isin M$:}
309 $D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
310 R$ so $D \le C$.  OK.
311
312 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
313  \land D \isin M$:}
314 $D \not\isin C$.  OK.
315
316 $\qed$
317
318 \section{Commit annotation}
319
320 We annotate each Topbloke commit $C$ with:
321 \gathbegin
322  \patchof{C}
323 \gathnext
324  \baseof{C}, \text{ if } C \in \py
325 \gathnext
326  \bigforall_{\pa{Q}} 
327    \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
328 \gathnext
329  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
330 \end{gather}
331
332 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
333 make it wrong to make plain commits with git because the recorded $\pends$
334 would have to be updated.  The annotation is not needed because
335 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
336
337 \section{Simple commit}
338
339 A simple single-parent forward commit $C$ as made by git-commit.
340 \begin{gather}
341 \tag*{} C \hasparents \{ A \} \\
342 \tag*{} \patchof{C} = \patchof{A} \\
343 \tag*{} D \isin C \equiv D \isin A \lor D = C
344 \end{gather}
345 This also covers Topbloke-generated commits on plain git branches:
346 Topbloke strips the metadata when exporting.
347
348 \subsection{No Replay}
349 Trivial.
350
351 \subsection{Unique Base}
352 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
353
354 \subsection{Tip Contents}
355 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
356 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
357 Substitute into the contents of $C$:
358 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
359     \lor D = C \]
360 Since $D = C \implies D \in \py$, 
361 and substituting in $\baseof{C}$, this gives:
362 \[ D \isin C \equiv D \isin \baseof{C} \lor
363     (D \in \py \land D \le A) \lor
364     (D = C \land D \in \py) \]
365 \[ \equiv D \isin \baseof{C} \lor
366    [ D \in \py \land ( D \le A \lor D = C ) ] \]
367 So by Exact Ancestors:
368 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
369 ) \]
370 $\qed$
371
372 \subsection{Base Acyclic}
373
374 Need to consider only $A, C \in \pn$.  
375
376 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
377
378 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
379 $A$, $D \isin C \implies D \not\in \py$. $\qed$
380
381 \subsection{Coherence and patch inclusion}
382
383 Need to consider $D \in \py$
384
385 \subsubsection{For $A \haspatch P, D = C$:}
386
387 Ancestors of $C$:
388 $ D \le C $.
389
390 Contents of $C$:
391 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
392
393 \subsubsection{For $A \haspatch P, D \neq C$:}
394 Ancestors: $ D \le C \equiv D \le A $.
395
396 Contents: $ D \isin C \equiv D \isin A \lor f $
397 so $ D \isin C \equiv D \isin A $.
398
399 So:
400 \[ A \haspatch P \implies C \haspatch P \]
401
402 \subsubsection{For $A \nothaspatch P$:}
403
404 Firstly, $C \not\in \py$ since if it were, $A \in \py$.  
405 Thus $D \neq C$.
406
407 Now by contents of $A$, $D \notin A$, so $D \notin C$.
408
409 So:
410 \[ A \nothaspatch P \implies C \nothaspatch P \]
411 $\qed$
412
413 \subsection{Foreign inclusion:}
414
415 If $D = C$, trivial.  For $D \neq C$:
416 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
417
418 \section{Anticommit}
419
420 Given $L, R^+, R^-$ where
421 $R^+ \in \pry, R^- = \baseof{R^+}$.  
422 Construct $C$ which has $\pr$ removed.
423 Used for removing a branch dependency.
424 \gathbegin
425  C \hasparents \{ L \}
426 \gathnext
427  \patchof{C} = \patchof{L}
428 \gathnext
429  \mergeof{C}{L}{R^+}{R^-}
430 \end{gather}
431
432 \subsection{Conditions}
433
434 \[ \eqn{ Into Base }{
435  L \in \pn
436 }\]
437 \[ \eqn{ Unique Tip }{
438  \pendsof{L}{\pry} = \{ R^+ \}
439 }\]
440 \[ \eqn{ Currently Included }{
441  L \haspatch \pry
442 }\]
443
444 \subsection{Ordering of ${L, R^+, R^-}$:}
445
446 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
447 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$.
448
449 (Note that the merge base $R^+ \not\le R^-$, i.e. the merge base is
450 later than one of the branches to be merged.)
451
452 \subsection{No Replay}
453
454 No Replay for Merge Results applies.  $\qed$
455
456 \subsection{Desired Contents}
457
458 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
459 \proofstarts
460
461 \subsubsection{For $D = C$:}
462
463 Trivially $D \isin C$.  OK.
464
465 \subsubsection{For $D \neq C, D \not\le L$:}
466
467 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
468 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
469
470 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
471
472 By Currently Included, $D \isin L$.
473
474 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
475 by Unique Tip, $D \le R^+ \equiv D \le L$.  
476 So $D \isin R^+$.
477
478 By Base Acyclic, $D \not\isin R^-$.
479
480 Apply $\merge$: $D \not\isin C$.  OK.
481
482 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
483
484 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
485
486 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
487
488 $\qed$
489
490 \subsection{Unique Base}
491
492 Into Base means that $C \in \pn$, so Unique Base is not
493 applicable. $\qed$
494
495 \subsection{Tip Contents}
496
497 Again, not applicable. $\qed$
498
499 \subsection{Base Acyclic}
500
501 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
502 And by Into Base $C \not\in \py$.
503 Now from Desired Contents, above, $D \isin C
504 \implies D \isin L \lor D = C$, which thus
505 $\implies D \not\in \py$.  $\qed$.
506
507 \subsection{Coherence and Patch Inclusion}
508
509 Need to consider some $D \in \py$.  By Into Base, $D \neq C$.
510
511 \subsubsection{For $\p = \pr$:}
512 By Desired Contents, above, $D \not\isin C$.
513 So $C \nothaspatch \pr$.
514
515 \subsubsection{For $\p \neq \pr$:}
516 By Desired Contents, $D \isin C \equiv D \isin L$
517 (since $D \in \py$ so $D \not\in \pry$).
518
519 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
520 So $L \nothaspatch \p \implies C \nothaspatch \p$.
521
522 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
523 so $L \haspatch \p \implies C \haspatch \p$.
524
525 \section{Foreign Inclusion}
526
527 Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
528 So by Desired Contents $D \isin C \equiv D \isin L$.
529 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
530 So $D \isin C \equiv D \le L$.
531
532 xxx up to here
533
534 By Tip Contents of $R^+$, $D \isin R^+ \equiv D \isin \baseof{R^+}$
535 i.e. $\equiv D \isin R^-$.
536 So by $\merge$, $D \isin C \equiv D \isin L$.
537
538 Thus $D \isin C \equiv $
539
540 \section{Merge}
541
542 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
543 \gathbegin
544  C \hasparents \{ L, R \}
545 \gathnext
546  \patchof{C} = \patchof{L}
547 \gathnext
548  \mergeof{C}{L}{M}{R}
549 \end{gather}
550 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
551
552 \subsection{Conditions}
553
554 \[ \eqn{ Tip Merge }{
555  L \in \py \implies
556    \begin{cases}
557       R \in \py : & \baseof{R} \ge \baseof{L}
558               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
559       R \in \pn : & M = \baseof{L} \\
560       \text{otherwise} : & \false
561    \end{cases}
562 }\]
563 \[ \eqn{ Merge Acyclic }{
564     L \in \pn
565    \implies
566     R \nothaspatch \p
567 }\]
568 \[ \eqn{ Removal Merge Ends }{
569     X \not\haspatch \p \land
570     Y \haspatch \p \land
571     M \haspatch \p
572   \implies
573     \pendsof{Y}{\py} = \pendsof{M}{\py}
574 }\]
575 \[ \eqn{ Addition Merge Ends }{
576     X \not\haspatch \p \land
577     Y \haspatch \p \land
578     M \nothaspatch \p
579    \implies \left[
580     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
581    \right]
582 }\]
583
584 \subsection{Non-Topbloke merges}
585
586 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$.
587 I.e. not only is it forbidden to merge into a Topbloke-controlled
588 branch without Topbloke's assistance, it is also forbidden to
589 merge any Topbloke-controlled branch into any plain git branch.
590
591 Given those conditions, Tip Merge and Merge Acyclic do not apply.
592 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
593 Merge Ends condition applies.  Good.
594
595 \subsection{No Replay}
596
597 No Replay for Merge Results applies.  $\qed$
598
599 \subsection{Unique Base}
600
601 Need to consider only $C \in \py$, ie $L \in \py$,
602 and calculate $\pendsof{C}{\pn}$.  So we will consider some
603 putative ancestor $A \in \pn$ and see whether $A \le C$.
604
605 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
606 But $C \in py$ and $A \in \pn$ so $A \neq C$.  
607 Thus $A \le C \equiv A \le L \lor A \le R$.
608
609 By Unique Base of L and Transitive Ancestors,
610 $A \le L \equiv A \le \baseof{L}$.
611
612 \subsubsection{For $R \in \py$:}
613
614 By Unique Base of $R$ and Transitive Ancestors,
615 $A \le R \equiv A \le \baseof{R}$.
616
617 But by Tip Merge condition on $\baseof{R}$,
618 $A \le \baseof{L} \implies A \le \baseof{R}$, so
619 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
620 Thus $A \le C \equiv A \le \baseof{R}$.  
621 That is, $\baseof{C} = \baseof{R}$.
622
623 \subsubsection{For $R \in \pn$:}
624
625 By Tip Merge condition on $R$ and since $M \le R$,
626 $A \le \baseof{L} \implies A \le R$, so
627 $A \le R \lor A \le \baseof{L} \equiv A \le R$.  
628 Thus $A \le C \equiv A \le R$.  
629 That is, $\baseof{C} = R$.
630
631 $\qed$
632
633 \subsection{Coherence and Patch Inclusion}
634
635 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
636 This involves considering $D \in \py$.  
637
638 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
639 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
640 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
641 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
642
643 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
644 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
645 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
646
647 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
648
649 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
650  \equiv D \isin L \lor D \isin R$.  
651 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
652
653 Consider $D \neq C, D \isin X \land D \isin Y$:
654 By $\merge$, $D \isin C$.  Also $D \le X$ 
655 so $D \le C$.  OK for $C \haspatch \p$.
656
657 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
658 By $\merge$, $D \not\isin C$.  
659 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.  
660 OK for $C \haspatch \p$.
661
662 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
663 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.  
664 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
665 OK for $C \haspatch \p$.
666
667 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
668
669 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
670
671 $M \haspatch \p \implies C \nothaspatch \p$.
672 $M \nothaspatch \p \implies C \haspatch \p$.
673
674 \proofstarts
675
676 One of the Merge Ends conditions applies.  
677 Recall that we are considering $D \in \py$.
678 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
679 We will show for each of
680 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
681 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
682
683 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
684 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
685 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
686 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
687
688 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
689 $D \le Y$ so $D \le C$.  
690 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
691
692 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
693 $D \not\le Y$.  If $D \le X$ then
694 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and 
695 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
696 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
697
698 Consider $D \neq C, M \haspatch P, D \isin Y$:
699 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
700 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
701 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
702
703 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
704 By $\merge$, $D \not\isin C$.  OK.
705
706 $\qed$
707
708 \subsection{Base Acyclic}
709
710 This applies when $C \in \pn$.
711 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
712
713 Consider some $D \in \py$.
714
715 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
716 R$.  And $D \neq C$.  So $D \not\isin C$.  $\qed$
717
718 \subsection{Tip Contents}
719
720 We need worry only about $C \in \py$.  
721 And $\patchof{C} = \patchof{L}$
722 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
723 of $C$, and its Coherence and Patch Inclusion, as just proved.
724
725 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
726 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
727 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
728 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
729 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
730
731 We will consider an arbitrary commit $D$
732 and prove the Exclusive Tip Contents form.
733
734 \subsubsection{For $D \in \py$:}
735 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
736 \le C$.  OK.
737
738 \subsubsection{For $D \not\in \py, R \not\in \py$:}
739
740 $D \neq C$.  By Tip Contents of $L$,
741 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
742 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
743 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
744 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
745
746 \subsubsection{For $D \not\in \py, R \in \py$:}
747
748 $D \neq C$.
749
750 By Tip Contents
751 $D \isin L \equiv D \isin \baseof{L}$ and
752 $D \isin R \equiv D \isin \baseof{R}$.
753
754 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
755 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
756 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
757 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
758
759 So $D \isin M \equiv D \isin L$ and by $\merge$,
760 $D \isin C \equiv D \isin R$.  But from Unique Base,
761 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
762
763 $\qed$
764
765 \subsection{Foreign Inclusion}
766
767 Consider some $D$ s.t. $\patchof{D} = \bot$.
768 By Foreign Inclusion of $L, M, R$:
769 $D \isin L \equiv D \le L$;
770 $D \isin M \equiv D \le M$;
771 $D \isin R \equiv D \le R$.
772
773 \subsubsection{For $D = C$:}
774
775 $D \isin C$ and $D \le C$.  OK.
776
777 \subsubsection{For $D \neq C, D \isin M$:}
778
779 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
780 R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.
781
782 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
783
784 By $\merge$, $D \isin C$.
785 And $D \isin X$ means $D \le X$ so $D \le C$.
786 OK.
787
788 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
789
790 By $\merge$, $D \not\isin C$.
791 And $D \not\le L, D \not\le R$ so $D \not\le C$.
792 OK
793
794 $\qed$
795
796 \end{document}