From 5c819ac7103f8910fcf52df232cf7028a747a210 Mon Sep 17 00:00:00 2001
From: Alice <alicevteixeira@gmail.com>
Date: Mon, 13 Nov 2023 12:51:23 +0000
Subject: [PATCH] vault backup: 2023-11-13 12:51:23

---
 .obsidian/workspace.json | 32 ++++++++++----------------------
 4a1s/MFES/PL - Aula 8.md | 39 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 49 insertions(+), 22 deletions(-)
 create mode 100644 4a1s/MFES/PL - Aula 8.md

diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json
index fef4e7f..5d8baaf 100644
--- a/.obsidian/workspace.json
+++ b/.obsidian/workspace.json
@@ -4,28 +4,16 @@
     "type": "split",
     "children": [
       {
-        "id": "c0bba0acc3e22afb",
+        "id": "e1841f20d0865df6",
         "type": "tabs",
         "children": [
           {
-            "id": "9853b375f7893cb9",
+            "id": "a3f61b3a67420afc",
             "type": "leaf",
             "state": {
               "type": "markdown",
               "state": {
-                "file": "4a1s/MFES/PL - Aula 4.md",
-                "mode": "source",
-                "source": false
-              }
-            }
-          },
-          {
-            "id": "47ffa0ada12cc565",
-            "type": "leaf",
-            "state": {
-              "type": "markdown",
-              "state": {
-                "file": "4a1s/MFES/PL - Aula 6.md",
+                "file": "4a1s/MFES/PL - Aula 8.md",
                 "mode": "source",
                 "source": false
               }
@@ -97,7 +85,7 @@
             "state": {
               "type": "backlink",
               "state": {
-                "file": "4a1s/MFES/PL - Aula 4.md",
+                "file": "4a1s/MFES/PL - Aula 8.md",
                 "collapseAll": false,
                 "extraContext": false,
                 "sortOrder": "alphabetical",
@@ -114,7 +102,7 @@
             "state": {
               "type": "outgoing-link",
               "state": {
-                "file": "4a1s/MFES/PL - Aula 4.md",
+                "file": "4a1s/MFES/PL - Aula 8.md",
                 "linksCollapsed": false,
                 "unlinkedCollapsed": true
               }
@@ -137,7 +125,7 @@
             "state": {
               "type": "outline",
               "state": {
-                "file": "4a1s/MFES/PL - Aula 4.md"
+                "file": "4a1s/MFES/PL - Aula 8.md"
               }
             }
           },
@@ -170,10 +158,12 @@
       "digitalgarden:Digital Garden Publication Center": false
     }
   },
-  "active": "9853b375f7893cb9",
+  "active": "a3f61b3a67420afc",
   "lastOpenFiles": [
-    "4a1s/MFES/PL - Aula 3.md",
+    "4a1s/MFES/PL - Aula 8.md",
     "4a1s/MFES/PL - Aula 4.md",
+    "4a1s/MFES/MFES - UC Details.md",
+    "4a1s/MFES/PL - Aula 3.md",
     "4a1s/MFES/PL - Aula 5.md",
     "4a1s/MFES/PL - Aula 7.md",
     "4a1s/index.md",
@@ -196,9 +186,7 @@
     "Excalidraw/doodles.excalidraw.md",
     "My Digital Garden.md",
     "4a1s/MFES/T - Aula 2.md",
-    "4a1s/MFES/PL - Aula 2.md",
     "Images/Pasted image 20231018122801.png",
-    "Excalidraw/Drawing 2023-10-25 12.16.38.excalidraw.md",
     "Images/Pasted image 20231018121319.png",
     "Images/Pasted image 20231018120412.png",
     "Images/Pasted image 20231018120219.png",
diff --git a/4a1s/MFES/PL - Aula 8.md b/4a1s/MFES/PL - Aula 8.md
new file mode 100644
index 0000000..1c5f949
--- /dev/null
+++ b/4a1s/MFES/PL - Aula 8.md	
@@ -0,0 +1,39 @@
+
+```c
+module Offices
+
+  type office = One | Two | Three
+  type person = Ana | Nuno | Pedro | Maria
+
+  predicate hasOffice (person) (office)
+
+  axiom A1 : forall p:person. exists o:office. hasOffice p o
+  axiom A2 : forall p:person, o1 o2 : office.
+    hasOffice p o1 /\ hasOffice p o2 -> o1 = o2
+  
+  axiom B : forall o1 o2 : office. hasOffice Pedro o1 /\ hasOffice Nuno o2 ->
+      o1 <> o2
+  
+  predicate alone (p:person) = forall o:office. forall p1:person.
+    (hasOffice p o) /\ hasOffice p1 o -> p = p1
+
+  axiom C : alone Ana -> alone Pedro
+  axiom D : forall p1 p2 p3: person, o:office.
+    hasOffice p1 o /\ hasOffice p2 o /\ hasOffice p3 o ->
+        p1 = p2 \/ p1 = p3 \/ p3 = p2
+
+  goal sanity_test : false (*check if the model makes sense*)
+  
+  goal g1 : hasOffice Maria One -> alone Maria
+  goal g2 : forall o1:office. (hasOffice Ana o1 /\ hasOffice Nuno o1) -> 
+      exists o2:office. hasOffice Pedro o2 /\ hasOffice Maria o2 
+
+  predicate empty (o:office) = forall p:person. not (hasOffice p o)
+  
+  lemma atMostOneEmpty : forall o1 o2: office. empty o1 /\ empty o2 ->
+      o1 = o2
+
+end 
+```
+
+