diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json
index e36971e..a2422c4 100644
--- a/.obsidian/workspace.json
+++ b/.obsidian/workspace.json
@@ -242,10 +242,10 @@
   },
   "active": "43416c0d533d9ab4",
   "lastOpenFiles": [
+    "Concurrent Systems/slides/class 7.pdf",
+    "Concurrent Systems/notes/7- MUTEX-free concurrency.md",
     "Concurrent Systems/notes/3a - Hardware primitives & Lamport Bakery algorithm.md",
     "Concurrent Systems/notes/8 - Enhancing Liveness Properties.md",
-    "Concurrent Systems/notes/7- MUTEX-free concurrency.md",
-    "Concurrent Systems/slides/class 7.pdf",
     "Concurrent Systems/slides/class 8.pdf",
     "Pasted image 20250325090735.png",
     "Concurrent Systems/notes/images/Pasted image 20250324091452.png",
diff --git a/Concurrent Systems/notes/7- MUTEX-free concurrency.md b/Concurrent Systems/notes/7- MUTEX-free concurrency.md
index e8238d2..5aab377 100644
--- a/Concurrent Systems/notes/7- MUTEX-free concurrency.md	
+++ b/Concurrent Systems/notes/7- MUTEX-free concurrency.md	
@@ -182,3 +182,6 @@ la conclude serve a garantire che il sequence number sia corretto. Se è stato g
 the implementation of the stack is non-blocking
 
 *Proof:*
+Let us consider an operation invocation performed by p
+- if it terminates, √
+- otherwise, TOP has changed between the first of TOP and the last Compare&set
\ No newline at end of file