chiark
/
gitweb
/
~ian
/
topbloke-formulae.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
notation: define \commitmergeof in terms of \stmtmergeof
[topbloke-formulae.git]
/
invariants.tex
diff --git
a/invariants.tex
b/invariants.tex
index 0cac868d3e6b8aaf7de01d375a4a28c8b229d77c..bb926ea1f71460e1db981d110bf06078ab818a78 100644
(file)
--- a/
invariants.tex
+++ b/
invariants.tex
@@
-22,11
+22,11
@@
We maintain these each time we construct a new commit. \\
\bigforall_{C,\p} C \haspatch \p \implies \pendsof{C}{\py} = \{ T \}
}\]
\[\eqn{Foreign Inclusion}{
\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
+ \bigforall_{D \
in \foreign
} 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
+ \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
}\]
We also assign each new commit $C$ to zero or one of the sets $\p$, as