diff --git a/4a1s/MFES/PL - Aula 5.md b/4a1s/MFES/PL - Aula 5.md
index 292bde9..ba43366 100644
--- a/4a1s/MFES/PL - Aula 5.md	
+++ b/4a1s/MFES/PL - Aula 5.md	
@@ -36,17 +36,19 @@ pred Invs {
 	// that you specification is not accepting.
 
   
-  	//no node links to itself and its children don't link to it
+  	//no node links to itself and its children don't link to it (no loops)
   	all x: Node | x not in x.^prox
-  
+
+
   	//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)
 
+
   	//a node with the same hash as two others in the same hash cannot be prox of them two
-  	all x, y, z:Node, w : Key | (x.key = w and y.key = w and z.key = w and x.prox = z) implies y.prox!=z
+  	//all x, y, z:Node, w : Key | (x.key = w and y.key = w and z.key = w and x.prox = z) implies y.prox!=z