\item[ $ C \haspatch \p $ ]
$\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
-~ Informally, $C$ has the contents of $\p$.
+~ Informally, $C$ has all the reachable contents of $\p$.
\item[ $ C \nothaspatch \p $ ]
$\displaystyle \bigforall_{D \in \py} D \not\isin C $.
$
\end{basedescript}
-\newpage
+
\section{Invariants}
We maintain these each time we construct a new commit. \\
Not applicable.
-\section{Dependency Removal}
+\section{Anticommit}
Given $L$ which contains $\pr$ as represented by $R^+, R^-$.
-Construct $C$ which has $\pr$ removed by applying a single
-commit which is the anticommit of $\pr$.
+Construct $C$ which has $\pr$ removed.
Used for removing a branch dependency.
\gathbegin
C \hasparents \{ L \}
\end{gather}
We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
+This can also be used for dependency re-insertion, by setting
+$L \in \pn$, $R \in \pry$, $M = \baseof{R}$.
+
\subsection{Conditions}
\[ \eqn{ Ingredients }{
M \le L, M \le R
}\]
\[ \eqn{ Removal Merge Ends }{
X \not\haspatch \p \land
- Y \haspatch \p \land
- M \haspatch \p
+ M \haspatch \p \land
+ Y \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
+ M \nothaspatch \p \land
+ Y \haspatch \p
\implies \left[
\bigforall_{E \in \pendsof{X}{\py}} E \le Y
\right]