[topbloke-formulae.git] / article.tex

\documentclass[a4paper,leqno]{strayman}
\errorcontextlines=50
\let\numberwithin=\notdef
\usepackage{amsmath}
\usepackage{mathabx}
\usepackage{txfonts}
\usepackage{amsfonts}
\usepackage{mdwlist}
%\usepackage{accents}

\renewcommand{\ge}{\geqslant}
\renewcommand{\le}{\leqslant}
\newcommand{\nge}{\ngeqslant}
\newcommand{\nle}{\nleqslant}

\newcommand{\has}{\sqsupseteq}
\newcommand{\isin}{\sqsubseteq}

\newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
\newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
\newcommand{\haspatch}{\sqSupset}
\newcommand{\patchisin}{\sqSubset}

        \newif\ifhidehack\hidehackfalse
        \DeclareRobustCommand\hidefromedef[2]{%
          \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
        \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}

\newcommand{\set}[1]{\mathbb{#1}}
\newcommand{\pay}[1]{\pa{#1}^+}
\newcommand{\pan}[1]{\pa{#1}^-}

\newcommand{\p}{\pa{P}}
\newcommand{\py}{\pay{P}}
\newcommand{\pn}{\pan{P}}

\newcommand{\pq}{\pa{Q}}
\newcommand{\pqy}{\pay{Q}}
\newcommand{\pqn}{\pan{Q}}

\newcommand{\pr}{\pa{R}}
\newcommand{\pry}{\pay{R}}
\newcommand{\prn}{\pan{R}}

%\newcommand{\hasparents}{\underaccent{1}{>}}
%\newcommand{\hasparents}{{%
%  \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
\newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
\newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}

\renewcommand{\implies}{\Rightarrow}
\renewcommand{\equiv}{\Leftrightarrow}
\renewcommand{\nequiv}{\nLeftrightarrow}
\renewcommand{\land}{\wedge}
\renewcommand{\lor}{\vee}

\newcommand{\pancs}{{\mathcal A}}
\newcommand{\pends}{{\mathcal E}}

\newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
\newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }

\newcommand{\merge}{{\mathcal M}}
\newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
%\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}

\newcommand{\patch}{{\mathcal P}}
\newcommand{\base}{{\mathcal B}}

\newcommand{\patchof}[1]{\patch ( #1 ) }
\newcommand{\baseof}[1]{\base ( #1 ) }

\newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
\newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }

%\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
\newcommand{\bigforall}{%
  \mathop{\mathchoice%
    {\hbox{\huge$\forall$}}%
    {\hbox{\Large$\forall$}}%
    {\hbox{\normalsize$\forall$}}%
    {\hbox{\scriptsize$\forall$}}}%
}

\newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
\newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}

\newcommand{\qed}{\square}
\newcommand{\proofstarts}{{\it Proof:}}
\newcommand{\proof}[1]{\proofstarts #1 $\qed$}

\newcommand{\gathbegin}{\begin{gather} \tag*{}}
\newcommand{\gathnext}{\\ \tag*{}}

\newcommand{\true}{t}
\newcommand{\false}{f}

\begin{document}

\section{Notation}

\begin{basedescript}{
\desclabelwidth{5em}
\desclabelstyle{\nextlinelabel}
}
\item[ $ C \hasparents \set X $ ]
The parents of commit $C$ are exactly the set
$\set X$.

\item[ $ C \ge D $ ]
$C$ is a descendant of $D$ in the git commit
graph.  This is a partial order, namely the transitive closure of 
$ D \in \set X $ where $ C \hasparents \set X $.

\item[ $ C \has D $ ]
Informally, the tree at commit $C$ contains the change
made in commit $D$.  Does not take account of deliberate reversions by
the user or reversion, rebasing or rewinding in
non-Topbloke-controlled branches.  For merges and Topbloke-generated
anticommits or re-commits, the ``change made'' is only to be thought
of as any conflict resolution.  This is not a partial order because it
is not transitive.

\item[ $ \p, \py, \pn $ ]
A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
are respectively the base and tip git branches.  $\p$ may be used
where the context requires a set, in which case the statement
is to be taken as applying to both $\py$ and $\pn$.
None of these sets overlap.  Hence:

\item[ $ \patchof{ C } $ ]
Either $\p$ s.t. $ C \in \p $, or $\bot$.  
A function from commits to patches' sets $\p$.

\item[ $ \pancsof{C}{\set P} $ ]
$ \{ A \; | \; A \le C \land A \in \set P \} $ 
i.e. all the ancestors of $C$
which are in $\set P$.

\item[ $ \pendsof{C}{\set P} $ ]
$ \{ E \; | \; E \in \pancsof{C}{\set P}
  \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
  E \neq A \land E \le A \} $ 
i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.

\item[ $ \baseof{C} $ ]
$ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
A partial function from commits to commits.
See Unique Base, below.

\item[ $ C \haspatch \p $ ]
$\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
~ Informally, $C$ has the contents of $\p$.

\item[ $ C \nothaspatch \p $ ]
$\displaystyle \bigforall_{D \in \py} D \not\isin C $.
~ Informally, $C$ has none of the contents of $\p$.  

Non-Topbloke commits are $\nothaspatch \p$ for all $\p$.  This
includes commits on plain git branches made by applying a Topbloke
patch.  If a Topbloke
patch is applied to a non-Topbloke branch and then bubbles back to
the relevant Topbloke branches, we hope that 
if the user still cares about the Topbloke patch,
git's merge algorithm will DTRT when trying to re-apply the changes.

\item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
The contents of a git merge result:

$\displaystyle D \isin C \equiv
  \begin{cases}
    (D \isin L \land D \isin R) \lor D = C : & \true \\
    (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
    \text{otherwise} : & D \not\isin M
  \end{cases}
$ 

\end{basedescript}
\newpage
\section{Invariants}

We maintain these each time we construct a new commit. \\
\[ \eqn{No Replay:}{
  C \has D \implies C \ge D
}\]
\[\eqn{Unique Base:}{
 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
}\]
\[\eqn{Tip Contents:}{
  \bigforall_{C \in \py} D \isin C \equiv
    { D \isin \baseof{C} \lor \atop
      (D \in \py \land D \le C) }
}\]
\[\eqn{Base Acyclic:}{
  \bigforall_{B \in \pn} D \isin B \implies D \notin \py
}\]
\[\eqn{Coherence:}{
  \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
}\]
\[\eqn{Foreign Inclusion:}{
  \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
}\]
\[\eqn{Foreign Contents:}{
  \bigforall_{C \text{ s.t. } \patchof{C} = \bot}
    D \le C \implies \patchof{D} = \bot
}\]

\section{Some lemmas}

\[ \eqn{Alternative (overlapping) formulations defining
  $\mergeof{C}{L}{M}{R}$:}{
 D \isin C \equiv
  \begin{cases}
    D \isin L  \equiv D \isin R  : & D = C \lor D \isin L     \\
    D \isin L \nequiv D \isin R  : & D = C \lor D \not\isin M \\
    D \isin L  \equiv D \isin M  : & D = C \lor D \isin R     \\
    D \isin L \nequiv D \isin M  : & D = C \lor D \isin L     \\
    \text{as above with L and R exchanged}
  \end{cases}
}\]
\proof{
  Truth table xxx

  Original definition is symmetrical in $L$ and $R$.
}

\[ \eqn{Exclusive Tip Contents:}{
  \bigforall_{C \in \py} 
    \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
      \Bigr]
}\]
Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.

\proof{
Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
So by Base Acyclic $D \isin B \implies D \notin \py$.
}
\[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
  \bigforall_{C \in \py} D \isin C \equiv
  \begin{cases}
    D \in \py : & D \le C \\
    D \not\in \py : & D \isin \baseof{C}
  \end{cases}
}\]

\[ \eqn{Tip Self Inpatch:}{
  \bigforall_{C \in \py} C \haspatch \p
}\]
Ie, tip commits contain their own patch.

\proof{
Apply Exclusive Tip Contents to some $D \in \py$:
$ \bigforall_{C \in \py}\bigforall_{D \in \py}
  D \isin C \equiv D \le C $
}

\[ \eqn{Exact Ancestors:}{
  \bigforall_{ C \hasparents \set{R} }
  D \le C \equiv
    ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
    \lor D = C
}\]
xxx proof tbd

\[ \eqn{Transitive Ancestors:}{
  \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
  \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
}\]

\proof{
The implication from right to left is trivial because
$ \pends() \subset \pancs() $.
For the implication from left to right: 
by the definition of $\mathcal E$,
for every such $A$, either $A \in \pends()$ which implies
$A \le M$ by the LHS directly,
or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
in which case we repeat for $A'$.  Since there are finitely many
commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
by the LHS.  And $A \le A''$.
}

\[ \eqn{Calculation Of Ends:}{
  \bigforall_{C \hasparents \set A}
    \pendsof{C}{\set P} =
      \begin{cases}
       C \in \p : & \{ C \}
      \\
       C \not\in \p : & \displaystyle
       \left\{ E \Big|
           \Bigl[ \Largeexists_{A \in \set A} 
                       E \in \pendsof{A}{\set P} \Bigr] \land
           \Bigl[ \Largenexists_{B \in \set A} 
                       E \neq B \land E \le B \Bigr]
       \right\}
      \end{cases}
}\]
xxx proof tbd

\[ \eqn{Ingredients Prevent Replay:}{
  \left[
    {C \hasparents \set A} \land
   \\
    \left(
      D \isin C \implies
       D = C \lor
       \Largeexists_{A \in \set A} D \isin A
    \right)
  \right] \implies \left[
    D \isin C \implies D \le C
  \right]
}\]
\proof{
  Trivial for $D = C$.  Consider some $D \neq C$, $D \isin C$.
  By the preconditions, there is some $A$ s.t. $D \in \set A$
  and $D \isin A$.  By No Replay for $A$, $D \le A$.  And
  $A \le C$ so $D \le C$.
}

\[ \eqn{Totally Foreign Contents:}{
  \bigforall_{C \hasparents \set A}
   \left[
    \patchof{C} = \bot \land
      \bigforall_{A \in \set A} \patchof{A} = \bot
   \right]
  \implies
   \left[
    D \le C
   \implies
    \patchof{D} = \bot
   \right]
}\]
\proof{
Consider some $D \le C$.  If $D = C$, $\patchof{D} = \bot$ trivially.
If $D \neq C$ then $D \le A$ where $A \in \set A$.  By Foreign
Contents of $A$, $\patchof{D} = \bot$.
}

\section{Commit annotation}

We annotate each Topbloke commit $C$ with:
\gathbegin
 \patchof{C}
\gathnext
 \baseof{C}, \text{ if } C \in \py
\gathnext
 \bigforall_{\pq}
   \text{ either } C \haspatch \pq \text{ or } C \nothaspatch \pq
\gathnext
 \bigforall_{\pqy \not\ni C} \pendsof{C}{\pqy}
\end{gather}

$\patchof{C}$, for each kind of Topbloke-generated commit, is stated
in the summary in the section for that kind of commit.

Whether $\baseof{C}$ is required, and if so what the value is, is
stated in the proof of Unique Base for each kind of commit.

$C \haspatch \pq$ or $\nothaspatch \pq$ is represented as the
set $\{ \pq | C \haspatch \pq \}$.  Whether $C \haspatch \pq$
is in stated
(in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$
for the ingredients $I$),
in the proof of Coherence for each kind of commit.

$\pendsof{C}{\pq^+}$ is computed, for all Topbloke-generated commits,
using the lemma Calculation of Ends, above.
We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
make it wrong to make plain commits with git because the recorded $\pends$
would have to be updated.  The annotation is not needed in that case
because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.

\section{Simple commit}

A simple single-parent forward commit $C$ as made by git-commit.
\begin{gather}
\tag*{} C \hasparents \{ A \} \\
\tag*{} \patchof{C} = \patchof{A} \\
\tag*{} D \isin C \equiv D \isin A \lor D = C
\end{gather}
This also covers Topbloke-generated commits on plain git branches:
Topbloke strips the metadata when exporting.

\subsection{No Replay}

Ingredients Prevent Replay applies.  $\qed$

\subsection{Unique Base}
If $A, C \in \py$ then by Calculation of Ends for
$C, \py, C \not\in \py$:
$\pendsof{C}{\pn} = \pendsof{A}{\pn}$ so
$\baseof{C} = \baseof{A}$. $\qed$

\subsection{Tip Contents}
We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
\[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
Substitute into the contents of $C$:
\[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
    \lor D = C \]
Since $D = C \implies D \in \py$, 
and substituting in $\baseof{C}$, this gives:
\[ D \isin C \equiv D \isin \baseof{C} \lor
    (D \in \py \land D \le A) \lor
    (D = C \land D \in \py) \]
\[ \equiv D \isin \baseof{C} \lor
   [ D \in \py \land ( D \le A \lor D = C ) ] \]
So by Exact Ancestors:
\[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
) \]
$\qed$

\subsection{Base Acyclic}

Need to consider only $A, C \in \pn$.  

For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.

For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
$A$, $D \isin C \implies D \not\in \py$.

$\qed$

\subsection{Coherence and patch inclusion}

Need to consider $D \in \py$

\subsubsection{For $A \haspatch P, D = C$:}

Ancestors of $C$:
$ D \le C $.

Contents of $C$:
$ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.

\subsubsection{For $A \haspatch P, D \neq C$:}
Ancestors: $ D \le C \equiv D \le A $.

Contents: $ D \isin C \equiv D \isin A \lor f $
so $ D \isin C \equiv D \isin A $.

So:
\[ A \haspatch P \implies C \haspatch P \]

\subsubsection{For $A \nothaspatch P$:}

Firstly, $C \not\in \py$ since if it were, $A \in \py$.  
Thus $D \neq C$.

Now by contents of $A$, $D \notin A$, so $D \notin C$.

So:
\[ A \nothaspatch P \implies C \nothaspatch P \]
$\qed$

\subsection{Foreign inclusion:}

If $D = C$, trivial.  For $D \neq C$:
$D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$

\subsection{Foreign Contents:}

Only relevant if $\patchof{C} = \bot$, and in that case Totally
Foreign Contents applies. $\qed$

\section{Create Base}

Given $L$, create a Topbloke base branch initial commit $B$.
\gathbegin
 B \hasparents \{ L \}
\gathnext
 \patchof{B} = \pqn
\gathnext
 D \isin B \equiv D \isin L \lor D = B
\end{gather}

\subsection{Conditions}

\[ \eqn{ Ingredients }{
 \patchof{L} = \pa{L} \lor \patchof{L} = \bot
}\]
\[ \eqn{ Create Acyclic }{
 L \not\haspatch \pq
}\]

\subsection{No Replay}

Ingredients Prevent Replay applies.  $\qed$

\subsection{Unique Base}

Not applicable.

\subsection{Tip Contents}

Not applicable.

\subsection{Base Acyclic}

Consider some $D \isin B$.  If $D = B$, $D \in \pqn$.
If $D \neq B$, $D \isin L$, and by Create Acyclic
$D \not\in \pqy$.  $\qed$

\subsection{Coherence and Patch Inclusion}

Consider some $D \in \p$.
$B \not\in \py$ so $D \neq B$.  So $D \isin B \equiv D \isin L$
and $D \le B \equiv D \le L$.

Thus $L \haspatch \p \implies B \haspatch P$
and $L \nothaspatch \p \implies B \nothaspatch P$.

$\qed$.

\subsection{Foreign Inclusion}

Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq B$
so $D \isin B \equiv D \isin L$.
By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
And by Exact Ancestors $D \le L \equiv D \le B$.
So $D \isin B \equiv D \le B$.  $\qed$

\subsection{Foreign Contents}

Not applicable.

\section{Create Tip}

Given a Topbloke base $B$, create a tip branch initial commit B.
\gathbegin
 C \hasparents \{ B \}
\gathnext
 \patchof{B} = \pqy
\gathnext
 D \isin C \equiv D \isin B \lor D = C
\end{gather}

\subsection{Conditions}

\[ \eqn{ Ingredients }{
 \patchof{B} = \pqn
}\]
\[ \eqn{ No Sneak }{
 \pendsof{B}{\pqy} = \{ \}
}\]

\subsection{No Replay}

Ingredients Prevent Replay applies.  $\qed$

\subsection{Unique Base}

Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$.  $\qed$

\subsection{Tip Contents}

Consider some arbitrary commit $D$.  If $D = C$, trivially satisfied.

If $D \neq C$, $D \isin C \equiv D \isin B$.
By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$.
So $D \isin C \equiv D \isin \baseof{B}$.

$\qed$

\subsection{Base Acyclic}

Not applicable.

\subsection{Coherence and Patch Inclusion}

$$
\begin{cases}
  \p = \pq    \lor B \haspatch \p : & C \haspatch \p \\
  \p \neq \pq \land B \nothaspatch \p : & C \nothaspatch \p
\end{cases}
$$

\proofstarts
~ Consider some $D \in \py$.

\subsubsection{For $\p = \pq$:}

By Base Acyclic, $D \not\isin B$.  So $D \isin C \equiv D = C$.
By No Sneak, $D \le B \equiv D = C$.  Thus $C \haspatch \pq$.

\subsubsection{For $\p \neq \pq$:}

$D \neq C$.  So $D \isin C \equiv D \isin B$,
and $D \le C \equiv D \le B$.

$\qed$

xxx up to here

\section{Anticommit}

Given $L$ and $\pr$ as represented by $R^+, R^-$.
Construct $C$ which has $\pr$ removed.
Used for removing a branch dependency.
\gathbegin
 C \hasparents \{ L \}
\gathnext
 \patchof{C} = \patchof{L}
\gathnext
 \mergeof{C}{L}{R^+}{R^-}
\end{gather}

\subsection{Conditions}

\[ \eqn{ Ingredients }{
R^+ \in \pry \land R^- = \baseof{R^+}
}\]
\[ \eqn{ Into Base }{
 L \in \pn
}\]
\[ \eqn{ Unique Tip }{
 \pendsof{L}{\pry} = \{ R^+ \}
}\]
\[ \eqn{ Currently Included }{
 L \haspatch \pry
}\]

\subsection{Ordering of Ingredients:}

By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$.
$\qed$

(Note that $R^+ \not\le R^-$, i.e. the merge base
is a descendant, not an ancestor, of the 2nd parent.)

\subsection{No Replay}

By definition of $\merge$,
$D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$.
So, by Ordering of Ingredients,
Ingredients Prevent Replay applies.  $\qed$

\subsection{Desired Contents}

\[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
\proofstarts

\subsubsection{For $D = C$:}

Trivially $D \isin C$.  OK.

\subsubsection{For $D \neq C, D \not\le L$:}

By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
$D \not\isin R^-$.  Thus $D \not\isin C$.  OK.

\subsubsection{For $D \neq C, D \le L, D \in \pry$:}

By Currently Included, $D \isin L$.

By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
by Unique Tip, $D \le R^+ \equiv D \le L$.  
So $D \isin R^+$.

By Base Acyclic, $D \not\isin R^-$.

Apply $\merge$: $D \not\isin C$.  OK.

\subsubsection{For $D \neq C, D \le L, D \notin \pry$:}

By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.

Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.

$\qed$

\subsection{Unique Base}

Into Base means that $C \in \pn$, so Unique Base is not
applicable. $\qed$

\subsection{Tip Contents}

Again, not applicable. $\qed$

\subsection{Base Acyclic}

By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
And by Into Base $C \not\in \py$.
Now from Desired Contents, above, $D \isin C
\implies D \isin L \lor D = C$, which thus
$\implies D \not\in \py$.  $\qed$.

\subsection{Coherence and Patch Inclusion}

Need to consider some $D \in \py$.  By Into Base, $D \neq C$.

\subsubsection{For $\p = \pr$:}
By Desired Contents, above, $D \not\isin C$.
So $C \nothaspatch \pr$.

\subsubsection{For $\p \neq \pr$:}
By Desired Contents, $D \isin C \equiv D \isin L$
(since $D \in \py$ so $D \not\in \pry$).

If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
So $L \nothaspatch \p \implies C \nothaspatch \p$.

Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
so $L \haspatch \p \implies C \haspatch \p$.

$\qed$

\subsection{Foreign Inclusion}

Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
So by Desired Contents $D \isin C \equiv D \isin L$.
By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.

And $D \le C \equiv D \le L$.
Thus $D \isin C \equiv D \le C$.

$\qed$

\subsection{Foreign Contents}

Not applicable.

\section{Merge}

Merge commits $L$ and $R$ using merge base $M$:
\gathbegin
 C \hasparents \{ L, R \}
\gathnext
 \patchof{C} = \patchof{L}
\gathnext
 \mergeof{C}{L}{M}{R}
\end{gather}
We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.

\subsection{Conditions}
\[ \eqn{ Ingredients }{
 M \le L, M \le R
}\]
\[ \eqn{ Tip Merge }{
 L \in \py \implies
   \begin{cases}
      R \in \py : & \baseof{R} \ge \baseof{L}
              \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
      R \in \pn : & M = \baseof{L} \\
      \text{otherwise} : & \false
   \end{cases}
}\]
\[ \eqn{ Merge Acyclic }{
    L \in \pn
   \implies
    R \nothaspatch \p
}\]
\[ \eqn{ Removal Merge Ends }{
    X \not\haspatch \p \land
    Y \haspatch \p \land
    M \haspatch \p
  \implies
    \pendsof{Y}{\py} = \pendsof{M}{\py}
}\]
\[ \eqn{ Addition Merge Ends }{
    X \not\haspatch \p \land
    Y \haspatch \p \land
    M \nothaspatch \p
   \implies \left[
    \bigforall_{E \in \pendsof{X}{\py}} E \le Y
   \right]
}\]
\[ \eqn{ Foreign Merges }{
    \patchof{L} = \bot \equiv \patchof{R} = \bot
}\]

\subsection{Non-Topbloke merges}

We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$
(Foreign Merges, above).
I.e. not only is it forbidden to merge into a Topbloke-controlled
branch without Topbloke's assistance, it is also forbidden to
merge any Topbloke-controlled branch into any plain git branch.

Given those conditions, Tip Merge and Merge Acyclic do not apply.
And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
Merge Ends condition applies.

So a plain git merge of non-Topbloke branches meets the conditions and
is therefore consistent with our scheme.

\subsection{No Replay}

By definition of $\merge$,
$D \isin C \implies D \isin L \lor D \isin R \lor D = C$.
So, by Ingredients,
Ingredients Prevent Replay applies.  $\qed$

\subsection{Unique Base}

Need to consider only $C \in \py$, ie $L \in \py$,
and calculate $\pendsof{C}{\pn}$.  So we will consider some
putative ancestor $A \in \pn$ and see whether $A \le C$.

By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
But $C \in py$ and $A \in \pn$ so $A \neq C$.  
Thus $A \le C \equiv A \le L \lor A \le R$.

By Unique Base of L and Transitive Ancestors,
$A \le L \equiv A \le \baseof{L}$.

\subsubsection{For $R \in \py$:}

By Unique Base of $R$ and Transitive Ancestors,
$A \le R \equiv A \le \baseof{R}$.

But by Tip Merge condition on $\baseof{R}$,
$A \le \baseof{L} \implies A \le \baseof{R}$, so
$A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
Thus $A \le C \equiv A \le \baseof{R}$.  
That is, $\baseof{C} = \baseof{R}$.

\subsubsection{For $R \in \pn$:}

By Tip Merge condition on $R$ and since $M \le R$,
$A \le \baseof{L} \implies A \le R$, so
$A \le R \lor A \le \baseof{L} \equiv A \le R$.  
Thus $A \le C \equiv A \le R$.  
That is, $\baseof{C} = R$.

$\qed$

\subsection{Coherence and Patch Inclusion}

Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
This involves considering $D \in \py$.  

\subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
$D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
\in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.

\subsubsection{For $L \haspatch \p, R \haspatch \p$:}
$D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
(Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)

Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.

For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
 \equiv D \isin L \lor D \isin R$.  
(Likewise $D \le C \equiv D \le X \lor D \le Y$.)

Consider $D \neq C, D \isin X \land D \isin Y$:
By $\merge$, $D \isin C$.  Also $D \le X$ 
so $D \le C$.  OK for $C \haspatch \p$.

Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
By $\merge$, $D \not\isin C$.  
And $D \not\le X \land D \not\le Y$ so $D \not\le C$.  
OK for $C \haspatch \p$.

Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
$D \not\le X$ so $D \not\le M$ so $D \not\isin M$.  
Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
OK for $C \haspatch \p$.

So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.

\subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}

$M \haspatch \p \implies C \nothaspatch \p$.
$M \nothaspatch \p \implies C \haspatch \p$.

\proofstarts

One of the Merge Ends conditions applies.  
Recall that we are considering $D \in \py$.
$D \isin Y \equiv D \le Y$.  $D \not\isin X$.
We will show for each of
various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
(which suffices by definition of $\haspatch$ and $\nothaspatch$).

Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
$M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
$M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.

Consider $D \neq C, M \nothaspatch P, D \isin Y$:
$D \le Y$ so $D \le C$.  
$D \not\isin M$ so by $\merge$, $D \isin C$.  OK.

Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
$D \not\le Y$.  If $D \le X$ then
$D \in \pancsof{X}{\py}$, so by Addition Merge Ends and 
Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.

Consider $D \neq C, M \haspatch P, D \isin Y$:
$D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.

Consider $D \neq C, M \haspatch P, D \not\isin Y$:
By $\merge$, $D \not\isin C$.  OK.

$\qed$

\subsection{Base Acyclic}

This applies when $C \in \pn$.
$C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.

Consider some $D \in \py$.

By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
R$.  And $D \neq C$.  So $D \not\isin C$.

$\qed$

\subsection{Tip Contents}

We need worry only about $C \in \py$.  
And $\patchof{C} = \patchof{L}$
so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
of $C$, and its Coherence and Patch Inclusion, as just proved.

Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
\p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
\haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).

We will consider an arbitrary commit $D$
and prove the Exclusive Tip Contents form.

\subsubsection{For $D \in \py$:}
$C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
\le C$.  OK.

\subsubsection{For $D \not\in \py, R \not\in \py$:}

$D \neq C$.  By Tip Contents of $L$,
$D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
$D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.

\subsubsection{For $D \not\in \py, R \in \py$:}

$D \neq C$.

By Tip Contents
$D \isin L \equiv D \isin \baseof{L}$ and
$D \isin R \equiv D \isin \baseof{R}$.

If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
$\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
$D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.

So $D \isin M \equiv D \isin L$ and by $\merge$,
$D \isin C \equiv D \isin R$.  But from Unique Base,
$\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.

$\qed$

\subsection{Foreign Inclusion}

Consider some $D$ s.t. $\patchof{D} = \bot$.
By Foreign Inclusion of $L, M, R$:
$D \isin L \equiv D \le L$;
$D \isin M \equiv D \le M$;
$D \isin R \equiv D \le R$.

\subsubsection{For $D = C$:}

$D \isin C$ and $D \le C$.  OK.

\subsubsection{For $D \neq C, D \isin M$:}

Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.

\subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}

By $\merge$, $D \isin C$.
And $D \isin X$ means $D \le X$ so $D \le C$.
OK.

\subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}

By $\merge$, $D \not\isin C$.
And $D \not\le L, D \not\le R$ so $D \not\le C$.
OK

$\qed$

\subsection{Foreign Contents}

Only relevant if $\patchof{L} = \bot$, in which case
$\patchof{C} = \bot$ and by Foreign Merges $\patchof{R} = \bot$,
so Totally Foreign Contents applies.  $\qed$

\end{document}