diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json
index 8690022..0732644 100644
--- a/.obsidian/workspace.json
+++ b/.obsidian/workspace.json
@@ -213,9 +213,10 @@
   },
   "active": "56150e6df7869900",
   "lastOpenFiles": [
-    "Pasted image 20250428083727.png",
     "Concurrent Systems/slides/class 13.pdf",
     "Concurrent Systems/notes/13 - Weak Bisimilarity.md",
+    "Pasted image 20250428084340.png",
+    "Pasted image 20250428083727.png",
     "Concurrent Systems/notes/12 - Calculus of communicating system.md",
     "Concurrent Systems/slides/class 12.pdf",
     "Concurrent Systems/notes/12b - CCS cose varie.md",
@@ -231,8 +232,6 @@
     "Concurrent Systems/notes/images/Pasted image 20250414082824.png",
     "Concurrent Systems/notes/images/Pasted image 20250414152300.png",
     "Concurrent Systems/notes/images/Pasted image 20250414152247.png",
-    "Concurrent Systems/notes/images/Pasted image 20250414152234.png",
-    "Concurrent Systems/notes/images/Pasted image 20250414152221.png",
     "HCIW/notes/3 - Beacons.md",
     "HCIW/slides/Zooming interfaces.pdf",
     "HCIW/slides/Gestural interaction.pdf",
diff --git a/Concurrent Systems/notes/13 - Weak Bisimilarity.md b/Concurrent Systems/notes/13 - Weak Bisimilarity.md
index 6a9bac0..b875d53 100644
--- a/Concurrent Systems/notes/13 - Weak Bisimilarity.md	
+++ b/Concurrent Systems/notes/13 - Weak Bisimilarity.md	
@@ -36,6 +36,18 @@ $\approx$ is a
 
 *Proof:*
 take the symmetric closure of the following relations, that can be easily shown to be weak simulations:
-1. $S = \{ P,\tau.P \}\cup Id$
-2. $S=\{ M+N+\tau.N,M+\tau.N \}\cup Id$
-3. $S=\\{ (M+\alpha.P+) \}$
\ No newline at end of file
+1. $S = \{ (P,\tau.P )\}\cup Id$
+2. $S=\{ (M+N+\tau.N,M+\tau.N )\}\cup Id$
+3. $S=\{ ((M+\alpha.P+\alpha.(N+\tau.P), M+\alpha.(N+\tau.P)) \} \cup Id$
+
+#### Weak bisimilarity abstracts from any $\tau$
+![](../../Pasted%20image%2020250428084340.png)
+
+**There exists no weak bisimulation S that contains (P, Q).**
+*Proof:*
+By contr. suppose that a bisimulation exists
+Since Q −τ→ b.0, there must exist a P’ such that P ⇒ P and (P,b.0) ∈ S The only P that satisfies P ⇒ P’ is P itself
+hence it should be (P,b.0) ∈ S
+
+Contradiction: P can perform a whereas b.0 cannot !!
+Similarly, P/R and Q/R are NOT weakly bisimilar
\ No newline at end of file
diff --git a/Pasted image 20250428084340.png b/Pasted image 20250428084340.png
new file mode 100644
index 0000000..6e370fa
Binary files /dev/null and b/Pasted image 20250428084340.png differ