X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=invariants.tex;h=bb926ea1f71460e1db981d110bf06078ab818a78;hp=20d6e7644f76148d3c9790b31b55a47e8489fa35;hb=9ad96b436e0c1ddc5c4fb5074c588644e88c0bae;hpb=891ae7626916bde1eb7dfa38762bbb4d94b85211 diff --git a/invariants.tex b/invariants.tex index 20d6e76..bb926ea 100644 --- a/invariants.tex +++ b/invariants.tex @@ -1,29 +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{Foreign Inclusion:}{ - \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C +\[\eqn{Unique Tips}{ + \bigforall_{C,\p} C \haspatch \p \implies \pendsof{C}{\py} = \{ T \} }$ -$\eqn{Foreign Contents:}{ - \bigforall_{C \text{ s.t. } \patchof{C} = \bot} - D \le C \implies \patchof{D} = \bot +\[\eqn{Foreign Inclusion}{ + \bigforall_{D \in \foreign} D \isin C \equiv D \leq C +}$ +$\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