vault backup: 2023-10-23 20:28:40
This commit is contained in:
parent
7cd1ca9a1f
commit
ec8d5f1ba9
1 changed files with 2 additions and 2 deletions
|
@ -36,8 +36,8 @@ pred Invs {
|
|||
// that you specification is not accepting.
|
||||
|
||||
|
||||
// no node links to itself
|
||||
all x: Node | x->x not in prox
|
||||
//no node links to itself and its children don't link to it
|
||||
all x: Node | x not in x.^prox
|
||||
|
||||
//for all nodes sequentially linked, they must have the same hash
|
||||
all x, y: Node | (x.prox = y) implies x.key.hash = y.key.hash
|
||||
|
|
Loading…
Add table
Reference in a new issue