diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json
index 8d8779b..2ecb80d 100644
--- a/.obsidian/workspace.json
+++ b/.obsidian/workspace.json
@@ -193,6 +193,7 @@
   },
   "active": "ec8d1a91f1f0cc7e",
   "lastOpenFiles": [
+    "Pasted image 20250430171336.png",
     "Concurrent Systems/slides/class 13.pdf",
     "Concurrent Systems/notes/13 - Weak Bisimilarity.md",
     "Concurrent Systems/notes/14.md",
diff --git a/Concurrent Systems/notes/13 - Weak Bisimilarity.md b/Concurrent Systems/notes/13 - Weak Bisimilarity.md
index 7927510..601dd1d 100644
--- a/Concurrent Systems/notes/13 - Weak Bisimilarity.md	
+++ b/Concurrent Systems/notes/13 - Weak Bisimilarity.md	
@@ -111,7 +111,9 @@ Every component can be in three states:
 - C (extracted, waiting to externally communicate its value and start the process again): $$A_{i}=a_{i}.B_{i} \quad B_{i}=\tau.C_{i}+\bar{a}_{(i \space mod \space n)+1}.A_{i} \quad C_{i}=\bar{p}_{i}.B_{i}$$
 In pratica ogni volta o estrae di nuovo "se stesso" oppure "abilita" il componente successivo.
 
-Implementation: $$Impl \triangleq (B_{1}|A_{2}|\dots|An)$$
+Implementation: $$Impl \triangleq (B_{1}|A_{2}|\dots|An)\setminus_{\{ a_{1}\dots an \}}$$
 basically we need to have an initially habilitated process, which can be any (the first one in our case).
 
-This will generate the LTS:
\ No newline at end of file
+This will generate the LTS:
+![500](../../Pasted%20image%2020250430171336.png)
+
diff --git a/Pasted image 20250430171336.png b/Pasted image 20250430171336.png
new file mode 100644
index 0000000..0114988
Binary files /dev/null and b/Pasted image 20250430171336.png differ