}\]
xxx proof tbd
-\[ \eqn{Ingredients Prohibit Replay:}{
+\[ \eqn{Ingredients Prevent Replay:}{
\left[
{C \hasparents \set A} \land
\\
\subsection{No Replay}
-Ingredients Prohibit Replay applies. $\qed$
+Ingredients Prevent Replay applies. $\qed$
\subsection{Unique Base}
If $A, C \in \py$ then by Calculation of Ends for
\gathbegin
B \hasparents \{ L \}
\gathnext
- \patchof{B} = \pan{B}
+ \patchof{B} = \pan{Q}
\gathnext
D \isin B \equiv D \isin L \lor D = B
\end{gather}
\patchof{L} = \pa{L} \lor \patchof{L} = \bot
}\]
\[ \eqn{ Non-recursion }{
- L \not\in \pa{B}
+ L \not\in \pa{Q}
}\]
\subsection{No Replay}
-Ingredients Prohibit Replay applies. $\qed$
+Ingredients Prevent Replay applies. $\qed$
\subsection{Unique Base}
If $D \neq B$, $D \isin L$. By No Replay of $D$ in $L$, $D \le L$.
Thus by Foreign Contents of $L$, $\patchof{D} = \bot$. OK.
+xxx this is wrong
+
$\qed$
\subsection{Coherence and Patch Inclusion}
\section{Create Tip}
-xxx tbd
+Given a Topbloke base $B$, create a tip branch initial commit B.
+\gathbegin
+ C \hasparents \{ B \}
+\gathnext
+ \patchof{B} = \pay{Q}
+\gathnext
+ D \isin C \equiv D \isin B \lor D = C
+\end{gather}
+
+\subsection{Conditions}
+
+\[ \eqn{ Ingredients }{
+ \patchof{B} = \pan{Q}
+}\]
+
+\subsection{No Replay}
+
+Ingredients Prevent Replay applies. $\qed$
+
+\subsection{Unique Base}
+
+Trivially, $\pendsof{C}{\pan{Q}} = \{B\}$ so $\baseof{C} = B$.
+
+\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 \pay{Q}$.
+So $D \isin C \equiv D \isin \baseof{B}$.
+
+$\qed$
+
+xxx up to here
\section{Anticommit}
By definition of $\merge$,
$D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$.
So, by Ordering of Ingredients,
-Ingredients Prohibit Replay applies. $\qed$
+Ingredients Prevent Replay applies. $\qed$
\subsection{Desired Contents}
By definition of $\merge$,
$D \isin C \implies D \isin L \lor D \isin R \lor D = C$.
So, by Ingredients,
-Ingredients Prohibit Replay applies. $\qed$
+Ingredients Prevent Replay applies. $\qed$
\subsection{Unique Base}