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$.
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$.
\item[ $ \patchof{ C } $ ]
Either $\p$ s.t. $ C \in \p $, or $\bot$.
\item[ $ \patchof{ C } $ ]
Either $\p$ s.t. $ C \in \p $, or $\bot$.
\item[ $ C \nothaspatch \p $ ]
$\displaystyle \bigforall_{D \in \py} D \not\isin C $.
~ Informally, $C$ has none of 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$.
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
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
set $\{ \pq | C \haspatch \pq \}$. Whether $C \haspatch \pq$
is in stated
(in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$
set $\{ \pq | C \haspatch \pq \}$. Whether $C \haspatch \pq$
is in stated
(in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$
in the proof of Coherence for each kind of commit.
$\pendsof{C}{\pq^+}$ is computed, for all Topbloke-generated commits,
in the proof of Coherence for each kind of commit.
$\pendsof{C}{\pq^+}$ is computed, for all Topbloke-generated commits,
-If $L, C \in \py$ then by Calculation of Ends for
-$C, \py, C \not\in \py$:
+If $L, C \in \py$ then by Calculation of Ends,
\[ D \isin C \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L )
\lor D = C \]
Since $D = C \implies D \in \py$,
\[ D \isin C \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L )
\lor D = C \]
Since $D = C \implies D \in \py$,
\[ D \isin C \equiv D \isin \baseof{C} \lor
(D \in \py \land D \le L) \lor
(D = C \land D \in \py) \]
\[ D \isin C \equiv D \isin \baseof{C} \lor
(D \in \py \land D \le L) \lor
(D = C \land D \in \py) \]
-If $D \neq C$, $D \isin C \equiv D \isin B$.
+If $D \neq C$, $D \isin C \equiv D \isin B$,
+which by Unique Base, above, $ \equiv D \isin \baseof{B}$.
\subsubsection{For $\p = \pq$:}
By Base Acyclic, $D \not\isin B$. So $D \isin C \equiv D = C$.
\subsubsection{For $\p = \pq$:}
By Base Acyclic, $D \not\isin B$. So $D \isin C \equiv D = C$.
$D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$.
So, by Ordering of Ingredients,
Ingredients Prevent Replay applies. $\qed$
$D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$.
So, by Ordering of Ingredients,
Ingredients Prevent Replay applies. $\qed$
-By No Replay $D \not\isin L$. Also $D \not\le R^-$ hence
+By No Replay for $L$, $D \not\isin L$.
+Also, by Ordering of Ingredients, $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$.
$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 Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
-And by Into Base $C \not\in \py$.
+By Into Base and Base Acyclic for $L$, $D \isin L \implies D \not\in \pqy$.
+And by Into Base $C \not\in \pqy$.
Now from Desired Contents, above, $D \isin C
\implies D \isin L \lor D = C$, which thus
Now from Desired Contents, above, $D \isin C
\implies D \isin L \lor D = C$, which thus
\end{gather}
We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
\end{gather}
We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
\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
Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
\subsubsection{For $L \haspatch \p, R \haspatch \p$:}
Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
\subsubsection{For $L \haspatch \p, R \haspatch \p$:}
(which suffices by definition of $\haspatch$ and $\nothaspatch$).
Consider $D = C$: Thus $C \in \py, L \in \py$, and by Tip
(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,
+Self Inpatch for $L$, $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.
$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.