From 07b138fe374f642fd9cdf619bbf64a932b4d3f6b Mon Sep 17 00:00:00 2001 From: Alice Date: Mon, 6 Nov 2023 23:08:39 +0000 Subject: [PATCH] vault backup: 2023-11-06 23:08:39 --- .obsidian/appearance.json | 3 --- .obsidian/workspace.json | 10 +++++----- 4a1s/MFES/PL - Aula 7.md | 15 ++++++++++++--- 3 files changed, 17 insertions(+), 11 deletions(-) diff --git a/.obsidian/appearance.json b/.obsidian/appearance.json index c8c365d..e69de29 100644 --- a/.obsidian/appearance.json +++ b/.obsidian/appearance.json @@ -1,3 +0,0 @@ -{ - "accentColor": "" -} \ No newline at end of file diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 0e7ba20..a337822 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -13,7 +13,7 @@ "state": { "type": "markdown", "state": { - "file": "4a1s/MFES/PL - Aula 6.md", + "file": "4a1s/MFES/PL - Aula 7.md", "mode": "source", "source": false } @@ -85,7 +85,7 @@ "state": { "type": "backlink", "state": { - "file": "4a1s/MFES/PL - Aula 6.md", + "file": "4a1s/MFES/PL - Aula 7.md", "collapseAll": false, "extraContext": false, "sortOrder": "alphabetical", @@ -102,7 +102,7 @@ "state": { "type": "outgoing-link", "state": { - "file": "4a1s/MFES/PL - Aula 6.md", + "file": "4a1s/MFES/PL - Aula 7.md", "linksCollapsed": false, "unlinkedCollapsed": true } @@ -125,7 +125,7 @@ "state": { "type": "outline", "state": { - "file": "4a1s/MFES/PL - Aula 6.md" + "file": "4a1s/MFES/PL - Aula 7.md" } } }, @@ -160,8 +160,8 @@ }, "active": "3ca14d4a6c304083", "lastOpenFiles": [ - "4a1s/MFES/PL - Aula 7.md", "4a1s/MFES/PL - Aula 6.md", + "4a1s/MFES/PL - Aula 7.md", "4a1s/DAA/PL - Aula 1.md", "Excalidraw/Drawing 2023-10-04 12.19.18.excalidraw.md", "Excalidraw/doodles.excalidraw.md", diff --git a/4a1s/MFES/PL - Aula 7.md b/4a1s/MFES/PL - Aula 7.md index 405aead..c399e19 100644 --- a/4a1s/MFES/PL - Aula 7.md +++ b/4a1s/MFES/PL - Aula 7.md @@ -37,11 +37,20 @@ sig Hash {} // respective commands to check how many // points you have. + pred insert[n : Node] { - some k: Hash - //if hash empty -> node to head of bucket - //else + //if hash empty -> node to head of bucket + n.key.hash not in Hash implies + ( + lone b:Bucket | b.head = node implies b.head' = n + ) + //if hash empty -> bucket of desired hash, add to next + n.key.hash in Hash implies + ( + lone b: Bucket | b.head.key.hash = n.key.hash | b.head.*prox = + ) } + ```