\section{Anticommit}

Given $L$ which contains $\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 \pln
}\]
\[ \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 $\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 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$.

By Tip Own Contents for $R^+$, $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 for $R^-$, $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 \pln$, so Unique Base is not
applicable.

\subsection{Tip Contents}

Again, not applicable.

\subsection{Base Acyclic}

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

\subsection{Coherence and Patch Inclusion}

$$
\begin{cases}
  \p = \pr                            : & C \nothaspatch \p  \\
  \p \neq \pr \land L \nothaspatch \p : & C \nothaspatch \p  \\
  \p \neq \pr \land L \haspatch    \p : & C \haspatch    \p
\end{cases}
$$
\proofstarts
~ 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$.
OK.

\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$.
OK.

Whereas, if $L \haspatch \p$, $D \isin L \equiv D \le L$,
so $C \zhaspatch \p$;
and $\exists_{F \in \py} F \le L$ and this $F \le C$.
Thus $C \haspatch \p$.
OK.

$\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.

