diff --git a/4a1s/MFES/PL - Aula 5.md b/4a1s/MFES/PL - Aula 5.md index 768fb94..41d3174 100644 --- a/4a1s/MFES/PL - Aula 5.md +++ b/4a1s/MFES/PL - Aula 5.md @@ -45,13 +45,15 @@ 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) + + + //MAY BE WORNG STUFF //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