vault backup: 2023-11-10 12:32:05

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
-  
 
 }