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}}
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}}
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
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
if the user still cares about the Topbloke patch,
git's merge algorithm will DTRT when trying to re-apply the changes.
if the user still cares about the Topbloke patch,
git's merge algorithm will DTRT when trying to re-apply the changes.
by the definition of $\mathcal E$,
for every such $A$, either $A \in \pends()$ which implies
$A \le M$ by the LHS directly,
by the definition of $\mathcal E$,
for every such $A$, either $A \in \pends()$ which implies
$A \le M$ by the LHS directly,
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 \]
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 \]
and substituting in $\baseof{C}$, this gives:
\[ D \isin C \equiv D \isin \baseof{C} \lor
(D \in \py \land D \le A) \lor
and substituting in $\baseof{C}$, this gives:
\[ D \isin C \equiv D \isin \baseof{C} \lor
(D \in \py \land D \le A) \lor
By Currently Included, $D \isin L$.
By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
By Currently Included, $D \isin L$.
By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
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$.
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$.
Thus $A \le C \equiv A \le L \lor A \le R$.
By Unique Base of L and Transitive Ancestors,
Thus $A \le C \equiv A \le L \lor A \le R$.
By Unique Base of L and Transitive Ancestors,
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}$.
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}$.
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
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
\subsection{Coherence and Patch Inclusion}
Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
\subsection{Coherence and Patch Inclusion}
Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
\subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
$D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
\subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
$D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
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
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
(Likewise $D \le C \equiv D \le X \lor D \le Y$.)
Consider $D \neq C, D \isin X \land D \isin Y$:
(Likewise $D \le C \equiv D \le X \lor D \le Y$.)
Consider $D \neq C, D \isin X \land D \isin Y$:
so $D \le C$. OK for $C \haspatch \p$.
Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
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$.
+By $\merge$, $D \not\isin C$.
+And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
$M \nothaspatch \p$. And indeed $D \isin C$ and $D \le C$. OK.
Consider $D \neq C, M \nothaspatch P, D \isin Y$:
$M \nothaspatch \p$. And indeed $D \isin C$ and $D \le C$. OK.
Consider $D \neq C, M \nothaspatch P, D \isin Y$:
$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 \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
Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK.
Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK.
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.
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.