diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json
index 1600c2c..edfd9a0 100644
--- a/.obsidian/workspace.json
+++ b/.obsidian/workspace.json
@@ -88,7 +88,7 @@
             "state": {
               "type": "search",
               "state": {
-                "query": "tag:#𝑆X",
+                "query": "",
                 "matchingCase": false,
                 "explainSearch": false,
                 "collapseAll": false,
@@ -109,7 +109,8 @@
               "title": "Segnalibri"
             }
           }
-        ]
+        ],
+        "currentTab": 1
       }
     ],
     "direction": "horizontal",
diff --git a/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md b/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md
index 5e3a235..20ac61d 100644
--- a/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md	
+++ b/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md	
@@ -68,13 +68,13 @@ IDEA:
 - `PROGRESS[1..n]` is an array of SWMR atomic registers used by proc’s to signal that they’re alive
 - $p_{i}$ suspects $p_j$ if pi doesn’t see any progress of $p_{j}$ after a proper time interval (to be guessed) set in its timer
 - the leader is the least suspected process, or the one with smallest/biggest ID among the least suspected ones (if there are more than one)
-	- this changes in time, but not forever
+	- this changes in time, but not forever (can be proved, but it's not covered here)
 
 Guessing the time duration for suspecting a process:
-- SUSPECT[i,j] = #times pi has suspected pj
-- For all k, take the t+1 minimum values in SUSPECT[1..n , k]
-- Sum them, to obtain Sk
-- The interval to use in the timers is the minimum Sk
+- `SUSPECT[i,j]` = # of times pi has suspected pj
+- For all k, take the t+1 minimum values in `SUSPECT[1..n , k]`
+- Sum them, to obtain $S_{k}$
+- The interval to use in the timers is the minimum $S_{k}$
 	- it can be proved that this eventually becomes ≥ $\nabla$
 
 ### From obstruction-freedom to wait-freedom