diff --git a/4a1s/MFES/PL - Aula 5.md b/4a1s/MFES/PL - Aula 5.md
index 41d3174..7e8d280 100644
--- a/4a1s/MFES/PL - Aula 5.md	
+++ b/4a1s/MFES/PL - Aula 5.md	
@@ -41,7 +41,7 @@ pred Invs {
   
   	//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
-  	
+  	//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)
   	
@@ -54,9 +54,15 @@ pred Invs {
   	//the prox node of another node may be empty
   	all x: Node, y : Node | x.prox = y or not x.prox = y
 
+//all x : Node | x.prox.key != x.key
+
+
   	//WORNG STUFF
   	//buckets may only have one head exclusive to it
   	all x, y : Bucket| all z : Node | x.head = z implies y.head != z
+  	
+  	//all buckets have a unique hash
+  	all x, y: Bucket | (x.head != none and y.head != none) implies x.head.key.hash != y.head.key.hash 
 }
 
 ```
\ No newline at end of file