chiark / gitweb /
index bc3813e..bb926ea 100644 (file)
@@ -1,32 +1,32 @@
\section{Invariants}

We maintain these each time we construct a new commit. \\
-$\eqn{No Replay:}{ +\[ \eqn{No Replay}{ C \has D \implies C \ge D }$
-$\eqn{Unique Base:}{ +\[\eqn{Unique Base}{ \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \} }$
-$\eqn{Tip Contents:}{ +\[\eqn{Tip Contents}{ \bigforall_{C \in \py} D \isin C \equiv { D \isin \baseof{C} \lor \atop (D \in \py \land D \le C) } }$
-$\eqn{Base Acyclic:}{ +\[\eqn{Base Acyclic}{ \bigforall_{C \in \pn} D \isin C \implies D \notin \py }$
-$\eqn{Coherence:}{ +\[\eqn{Coherence}{ \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p }$
-$\eqn{Unique Tips:}{ - \bigforall_{C,\p} C \haspatch \p \implies \pendsof{C}{\p} = \{ T \} +\[\eqn{Unique Tips}{ + \bigforall_{C,\p} C \haspatch \p \implies \pendsof{C}{\py} = \{ T \} }$
-$\eqn{Foreign Inclusion:}{ - \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C +\[\eqn{Foreign Inclusion}{ + \bigforall_{D \in \foreign} D \isin C \equiv D \leq C }$
-$\eqn{Foreign Contents:}{ - \bigforall_{C \text{ s.t. } \patchof{C} = \bot} - D \le C \implies \patchof{D} = \bot +\[\eqn{Foreign Contents}{ + \bigforall_{C \in \foreign} + D \le C \implies \isforeign{D} }$

We also assign each new commit $C$ to zero or one of the sets $\p$, as