vault backup: 2023-10-23 19:38:40
This commit is contained in:
parent
bbd2f7db9d
commit
95e73aa572
2 changed files with 29 additions and 6 deletions
25
.obsidian/workspace.json
vendored
25
.obsidian/workspace.json
vendored
|
@ -18,8 +18,21 @@
|
||||||
"source": false
|
"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"
|
"direction": "vertical"
|
||||||
|
@ -85,7 +98,7 @@
|
||||||
"state": {
|
"state": {
|
||||||
"type": "backlink",
|
"type": "backlink",
|
||||||
"state": {
|
"state": {
|
||||||
"file": "4a1s/MFES/PL - Aula 4.md",
|
"file": "4a1s/MFES/PL - Aula 5.md",
|
||||||
"collapseAll": false,
|
"collapseAll": false,
|
||||||
"extraContext": false,
|
"extraContext": false,
|
||||||
"sortOrder": "alphabetical",
|
"sortOrder": "alphabetical",
|
||||||
|
@ -102,7 +115,7 @@
|
||||||
"state": {
|
"state": {
|
||||||
"type": "outgoing-link",
|
"type": "outgoing-link",
|
||||||
"state": {
|
"state": {
|
||||||
"file": "4a1s/MFES/PL - Aula 4.md",
|
"file": "4a1s/MFES/PL - Aula 5.md",
|
||||||
"linksCollapsed": false,
|
"linksCollapsed": false,
|
||||||
"unlinkedCollapsed": true
|
"unlinkedCollapsed": true
|
||||||
}
|
}
|
||||||
|
@ -125,7 +138,7 @@
|
||||||
"state": {
|
"state": {
|
||||||
"type": "outline",
|
"type": "outline",
|
||||||
"state": {
|
"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
|
"digitalgarden:Digital Garden Publication Center": false
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
"active": "3ca14d4a6c304083",
|
"active": "6a363953132aebe7",
|
||||||
"lastOpenFiles": [
|
"lastOpenFiles": [
|
||||||
|
"4a1s/MFES/PL - Aula 4.md",
|
||||||
"4a1s/MFES/PL - Aula 5.md",
|
"4a1s/MFES/PL - Aula 5.md",
|
||||||
"4a1s/RAS/Notas Projeto RAS.md",
|
"4a1s/RAS/Notas Projeto RAS.md",
|
||||||
"4a1s/CP/PL - Aula 4.md",
|
"4a1s/CP/PL - Aula 4.md",
|
||||||
"4a1s/MFES/T - Aula 2.md",
|
"4a1s/MFES/T - Aula 2.md",
|
||||||
"4a1s/MFES/PL - Aula 4.md",
|
|
||||||
"4a1s/CP/Projeto Fase 1.md",
|
"4a1s/CP/Projeto Fase 1.md",
|
||||||
"4a1s/CP/PL - Aula 6.md",
|
"4a1s/CP/PL - Aula 6.md",
|
||||||
"My Digital Garden.md",
|
"My Digital Garden.md",
|
||||||
|
|
|
@ -45,6 +45,16 @@ pred Invs {
|
||||||
//no node links to nodes associated with a different hash
|
//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)
|
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
|
||||||
}
|
}
|
||||||
|
|
||||||
```
|
```
|
Loading…
Reference in a new issue