From 7cd1ca9a1f69a3ead1014e6ddb3c76ac69476497 Mon Sep 17 00:00:00 2001 From: Alice Date: Mon, 23 Oct 2023 20:08:40 +0100 Subject: [PATCH] vault backup: 2023-10-23 20:08:40 --- 4a1s/MFES/PL - Aula 5.md | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/4a1s/MFES/PL - Aula 5.md b/4a1s/MFES/PL - Aula 5.md index 7e8d280..9565f97 100644 --- a/4a1s/MFES/PL - Aula 5.md +++ b/4a1s/MFES/PL - Aula 5.md @@ -44,7 +44,14 @@ pred Invs { //ALTERNATIVELY //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) - + + //a node with the same hash as two others in the same hash cannot be prox of them two + all x, y, z:Node, w : Key | (x.key = w and y.key = w and z.key = w and x.prox = z) implies y.prox!=z + + + + + //MAY BE WORNG STUFF @@ -54,7 +61,9 @@ pred Invs { //the prox node of another node may be empty all x: Node, y : Node | x.prox = y or not x.prox = y -//all x : Node | x.prox.key != x.key + //the sequence of nodes associated with the same hash should not loop + //all x : Node | x.prox.key != x.key + //WORNG STUFF