From: Ian Jackson Date: Fri, 27 Apr 2012 11:51:52 +0000 (+0100) Subject: invariants: remove some slightly ugly colons X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=commitdiff_plain;h=d95cd22b31c6d38e4dd4b3132300dd3ad8df0f1a invariants: remove some slightly ugly colons --- diff --git a/invariants.tex b/invariants.tex index bd77d69..0cac868 100644 --- a/invariants.tex +++ b/invariants.tex @@ -1,30 +1,30 @@ \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:}{ +\[\eqn{Unique Tips}{ \bigforall_{C,\p} C \haspatch \p \implies \pendsof{C}{\py} = \{ T \} }\] -\[\eqn{Foreign Inclusion:}{ +\[\eqn{Foreign Inclusion}{ \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C }\] -\[\eqn{Foreign Contents:}{ +\[\eqn{Foreign Contents}{ \bigforall_{C \text{ s.t. } \patchof{C} = \bot} D \le C \implies \patchof{D} = \bot }\]