(D \in \py \land D \le C) }
}\]
\[\eqn{Base Acyclic:}{
- \bigforall_{B \in \pn} D \isin B \implies D \notin \py
+ \bigforall_{C \in \pn} D \isin C \implies D \notin \py
}\]
\[\eqn{Coherence:}{
\bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
\bigforall_{C \text{ s.t. } \patchof{C} = \bot}
D \le C \implies \patchof{D} = \bot
}\]
+
+A commit $C$ which satisfies all of the above is said to be
+``conformant''.
+
+For each operation we will perform which generates a new commit, we
+will assume the conformance of the existing history and prove the
+conformance of the new commit.
}\]
\subsection{Tip Self Inpatch}
-Given Exclusive Tip Contents and Base Acyclic for $C$,
+Given Base Acyclic for $C$,
$$
\bigforall_{C \in \py} C \haspatch \p \land \neg[ C \nothaspatch \p ]
$$
}
\subsection{Ingredients Prevent Replay}
+Given conformant commits $A \in \set A$,
$$
\left[
{C \hasparents \set A} \land
$$
\proof{
Trivial for $D = C$. Consider some $D \neq C$, $D \isin C$.
- By the preconditions, there is some $A$ s.t. $D \in \set A$
+ By the preconditions, there is some $A$ s.t. $A \in \set A$
and $D \isin A$. By No Replay for $A$, $D \le A$. And
$A \le C$ so $D \le C$.
}
\subsection{Simple Foreign Inclusion}
+Given a conformant commit $L$,
$$
\left[
C \hasparents \{ L \}
}
\subsection{Totally Foreign Contents}
+Given conformant commits $A \in \set A$,
$$
\left[
C \hasparents \set A \land