\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{\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$; if a Topbloke
patch is applied to a non-Topbloke branch and then bubbles back to
the Topbloke patch itself, we hope that git's merge algorithm will
DTRT or that the user will no longer care about the Topbloke patch.

\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
}\]

\section{Some lemmas}

\[ \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
}\]

\[ \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} =
       \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\}
}\]
XXX proof TBD.

\subsection{No Replay for Merge Results}

If we are constructing $C$, with,
\gathbegin
  \mergeof{C}{L}{M}{R}
\gathnext
  L \le C
\gathnext
  R \le C
\end{gather}
No Replay is preserved.  \proofstarts

\subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.

\subsubsection{For $D \isin L \land D \isin R$:}
$D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.

\subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
$D \not\isin C$.  OK.

\subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 \land D \not\isin M$:}
$D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
R$ so $D \le C$.  OK.

\subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 \land D \isin M$:}
$D \not\isin C$.  OK.

$\qed$

\section{Commit annotation}

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

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 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}

\subsection{No Replay}
Trivial.

\subsection{Unique Base}
If $A, C \in \py$ then $\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$

\section{Anticommit}

Given $L, R^+, R^-$ where
$R^+ \in \pry, R^- = \baseof{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{ Unique Tip }{
 \pendsof{L}{\pry} = \{ R^+ \}
}\]
\[ \eqn{ Currently Included }{
 L \haspatch \pry
}\]
\[ \eqn{ Not Self }{
 L \not\in \{ R^+ \}
}\]

\subsection{No Replay}

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$ and No Replay for
Merge Results 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}

Need to consider only $C \in \py$, ie $L \in \py$.

xxx tbd

xxx need to finish anticommit

\section{Merge}

Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
\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{ 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 : & R \ge \baseof{L}
              \land 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]
}\]

\subsection{No Replay}

See No Replay for Merge Results.

\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$,
$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$:}

$C \haspatch \p \equiv M \nothaspatch \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 coherence and
patch inclusion of $C$ 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 some $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$.  xxx up to here


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


%D \in \py$:}



xxx the coherence is not that useful ?

$L \haspatch \p$ by 

xxx need to recheck this

$C \in \py$ $C \haspatch P$ so $D \isin C \equiv D \le C$.  OK.

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

Tip Contents for $L$: $D \isin L \equiv D \isin \baseof{L}$.

Tip Contents for $R$: $D \isin R \equiv D \isin \baseof{R}$.

But by Tip Merge, $\baseof{R} \ge \baseof{L}$

\end{document}
