diff --git a/4a1s/MFES/PL - Aula 4.md b/4a1s/MFES/PL - Aula 4.md
index 92be624..7d3f925 100644
--- a/4a1s/MFES/PL - Aula 4.md	
+++ b/4a1s/MFES/PL - Aula 4.md	
@@ -29,27 +29,31 @@ pred inv1 {
 	all x,y : User, z: Photo | x->z in posts and y->z in posts implies x=y
 	
 	// or (equivalent to 2nd formula)
-	all x,y : User, z: Photo | x in posts z and y in posts z implies x=y
+	all x,y : User, z: Photo | x in posts: z and y in posts: z implies x=y
 	
 	// or (equivalent to 1st and 2nd formula)
-	all y: Photo | some posts y
-	all y: Photo | lone posts y
+	all y: Photo | some posts: y
+	all y: Photo | lone posts: y
 	
 	// or (equivalent to 1st and 2nd formula)
-	all y:Photo | one posts y
+	all y:Photo | one posts: y
 }
  
 
 pred inv2 {
 	// Users cannot follow themselves.
 	all x: User | x->x not in follows
+	
+	//or
+	all x: User | x not in x:follows
 }
 
 
 pred inv3 {
 	// Users can see ads posted by everyone, 
 	// but only see non ads posted by followed users.
-	
+	all x : User, y :Photo | x->y sees implies (y in Ad) or 
+	(all z:User | z->y in posts implies x->z in follows)
 }