vault backup: 2023-11-10 11:45:55

This commit is contained in:
Alice 2023-11-10 11:45:55 +00:00
parent 61f15370f5
commit b511d7f8a7
2 changed files with 7 additions and 7 deletions

View file

@ -42,12 +42,12 @@ pred insert[n : Node] {
//if hash empty -> node to head of bucket
n.key.hash not in Hash implies
(
lone b:Bucket | b.head = node implies b.head' = n
lone b:Bucket | b.head = none implies b.head' = n
)
//if hash empty -> bucket of desired hash, add to next
n.key.hash in Hash implies
(
lone b: Bucket | b.head.key.hash = n.key.hash | b.head.*prox =
lone b: Bucket | b.head.key.hash = n.key.hash | b.head.*prox = n
)
}