diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json
index d379108..73007b8 100644
--- a/.obsidian/workspace.json
+++ b/.obsidian/workspace.json
@@ -18,8 +18,21 @@
                 "source": false
               }
             }
+          },
+          {
+            "id": "6a363953132aebe7",
+            "type": "leaf",
+            "state": {
+              "type": "markdown",
+              "state": {
+                "file": "4a1s/MFES/PL - Aula 5.md",
+                "mode": "source",
+                "source": false
+              }
+            }
           }
-        ]
+        ],
+        "currentTab": 1
       }
     ],
     "direction": "vertical"
@@ -85,7 +98,7 @@
             "state": {
               "type": "backlink",
               "state": {
-                "file": "4a1s/MFES/PL - Aula 4.md",
+                "file": "4a1s/MFES/PL - Aula 5.md",
                 "collapseAll": false,
                 "extraContext": false,
                 "sortOrder": "alphabetical",
@@ -102,7 +115,7 @@
             "state": {
               "type": "outgoing-link",
               "state": {
-                "file": "4a1s/MFES/PL - Aula 4.md",
+                "file": "4a1s/MFES/PL - Aula 5.md",
                 "linksCollapsed": false,
                 "unlinkedCollapsed": true
               }
@@ -125,7 +138,7 @@
             "state": {
               "type": "outline",
               "state": {
-                "file": "4a1s/MFES/PL - Aula 4.md"
+                "file": "4a1s/MFES/PL - Aula 5.md"
               }
             }
           },
@@ -158,13 +171,13 @@
       "digitalgarden:Digital Garden Publication Center": false
     }
   },
-  "active": "3ca14d4a6c304083",
+  "active": "6a363953132aebe7",
   "lastOpenFiles": [
+    "4a1s/MFES/PL - Aula 4.md",
     "4a1s/MFES/PL - Aula 5.md",
     "4a1s/RAS/Notas Projeto RAS.md",
     "4a1s/CP/PL - Aula 4.md",
     "4a1s/MFES/T - Aula 2.md",
-    "4a1s/MFES/PL - Aula 4.md",
     "4a1s/CP/Projeto Fase 1.md",
     "4a1s/CP/PL - Aula 6.md",
     "My Digital Garden.md",
diff --git a/4a1s/MFES/PL - Aula 5.md b/4a1s/MFES/PL - Aula 5.md
index bb46439..768fb94 100644
--- a/4a1s/MFES/PL - Aula 5.md	
+++ b/4a1s/MFES/PL - Aula 5.md	
@@ -44,7 +44,17 @@ pred Invs {
   	
   	//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)
+  	
+  	//the head of a bucket may be empty
+  	all x: Bucket, y : Node | x.head = y or not x.head = y
   
+  	//the prox node of another node may be empty
+  	all x: Node, y : Node | x.prox = y or not x.prox = y
+
+
+  	//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
 }
 
 ```
\ No newline at end of file