chiark
/
gitweb
/
~ian
/
topbloke-formulae.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
f58dec7
)
invariants: change notation in Bases' Children
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Wed, 7 Aug 2013 21:05:39 +0000
(22:05 +0100)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Wed, 7 Aug 2013 21:05:39 +0000
(22:05 +0100)
invariants.tex
patch
|
blob
|
history
diff --git
a/invariants.tex
b/invariants.tex
index 3134e5c9cde1d48718b1cfb70d883a9e624c0283..28647658cb30190e30a2f93a658757a81f8ddf59 100644
(file)
--- a/
invariants.tex
+++ b/
invariants.tex
@@
-29,9
+29,9
@@
We maintain these each time we construct a new commit. \\
D \le C \implies \isforeign{D}
}\]
\[\eqn{Bases' Children}{
- C \hasparent D \land D \in \pn
+ C \hasparent D \land D \in \p
d
n
\implies
- C \in \p
n \lor C \in \p
y
+ C \in \p
dn \lor C \in \pd
y
}\]
We also assign each new commit $C$ to zero or one of the sets $\p$, as