From f23c0520b23cead59ff2dae3d2b0cdef81de07d9 Mon Sep 17 00:00:00 2001 From: Alice Date: Fri, 10 Nov 2023 12:32:06 +0000 Subject: [PATCH] vault backup: 2023-11-10 12:32:05 --- 4a1s/MFES/PL - Aula 7.md | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/4a1s/MFES/PL - Aula 7.md b/4a1s/MFES/PL - Aula 7.md index ffde529..29f10f6 100644 --- a/4a1s/MFES/PL - Aula 7.md +++ b/4a1s/MFES/PL - Aula 7.md @@ -58,13 +58,10 @@ pred insert[n : Node] { pred insert[n : Node] { //nodes always in the head or linked to prox //always n in ( Bucket.head + Bucket.head.prox) - always{ - n in Bucket.head + always n.key.hash not in Hash { + } - historically n.key.hash not in Hash - lone b:Bucket | b.head = none implies b.head' = n - }