diff --git a/4a1s/MFES/PL - Aula 4.md b/4a1s/MFES/PL - Aula 4.md index 0942345..0f4a965 100644 --- a/4a1s/MFES/PL - Aula 4.md +++ b/4a1s/MFES/PL - Aula 4.md @@ -69,24 +69,30 @@ pred inv3 { //or all x :User, y :Photo | x in sees.y implies y in x.follows.posts + Ad + + //or + all x :User, y :Photo | y in x.sees implies y in x.follows.posts + Ad + + //or + all x :User | x.sees in x.follows.posts + Ad } pred inv4 { // If a user posts an ad then all its posts should be labeled as ads. - + } pred inv5 { // Influencers are followed by everyone else. - + all x: Influencer | follows.x = User-x } pred inv6 { // Influencers post every day. - + all x: Influencer, y : Day | x.posts.date = y }