(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.