diff --git a/4a1s/MFES/PL - Aula 5.md b/4a1s/MFES/PL - Aula 5.md
index ba43366..db1eb5a 100644
--- a/4a1s/MFES/PL - Aula 5.md	
+++ b/4a1s/MFES/PL - Aula 5.md	
@@ -44,7 +44,7 @@ pred Invs {
   	all x, y: Node | (x.prox = y) implies x.key.hash = y.key.hash
   	//ALTERNATIVELY
   	//no node links to nodes associated with a different hash
-  	all x, y: Node | x.key.hash != y.key.hash implies (x.prox != y and y.prox != x)
+  	//all x, y: Node | x.key.hash != y.key.hash implies (x.prox != y and y.prox != x)
 
 
   	//a node with the same hash as two others in the same hash cannot be prox of them two
@@ -52,7 +52,17 @@ pred Invs {
 
 
 
-
+    //heads are unique to a single bucket
+  	all x: Bucket | lone x.head
+  
+  	//nodes must be prox to another node or be the head of a bucket
+   	all x: Node | (x in Bucket.head) or (x in Node.prox)
+  
+  	//diffenrent buckets must have different heads
+	all x, y: Bucket, z : Node | x != y and x.head = z implies y.head!=z
+  
+  	//keys must have a hash
+  	all x: Key | some y: Hash | x.hash = y