diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json
index 0c778c3..43d8d7c 100644
--- a/.obsidian/workspace.json
+++ b/.obsidian/workspace.json
@@ -192,10 +192,10 @@
   },
   "active": "ec8d1a91f1f0cc7e",
   "lastOpenFiles": [
-    "Pasted image 20250430192526.png",
+    "Concurrent Systems/notes/12b - CCS cose varie.md",
     "Concurrent Systems/notes/13 - Weak Bisimilarity.md",
     "Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md",
-    "Concurrent Systems/notes/12b - CCS cose varie.md",
+    "Pasted image 20250430192526.png",
     "Concurrent Systems/notes/12 - Calculus of communicating system.md",
     "Concurrent Systems/notes/11 - LTSs and Bisimulation.md",
     "Concurrent Systems/notes/10 - Implementing Consensus.md",
@@ -210,7 +210,6 @@
     "Concurrent Systems/notes/images/Pasted image 20250429092055.png",
     "Concurrent Systems/notes/images/Pasted image 20250429091959.png",
     "Concurrent Systems/notes/images/Pasted image 20250429091029.png",
-    "Concurrent Systems/notes/images/Pasted image 20250429085319.png",
     "Concurrent Systems/slides/class 12.pdf",
     "HCIW/slides/HCI in the car.pdf",
     "Concurrent Systems/slides/class 11.pdf",
diff --git a/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md b/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md
index 3e5770a..1671b8d 100644
--- a/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md	
+++ b/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md	
@@ -49,7 +49,10 @@ $P$ is in standard form if and only if $P \triangleq \sum_{i}\alpha_{i}P_{i}$ an
 	![](../../Pasted%20image%2020250430192526.png)
 	and eventually we find $P'$ which is literally the standard form of $P_{1}|P_{2}$.
 	
-2. $P \triangleq \sum_{i \in I}\alpha_{i}P_{i}$. By induction $\forall P_{i} \exists P_{i}$
+2. $P \triangleq \sum_{i \in I}\alpha_{i}P_{i}$. By induction $\forall P_{i} \exists P_{i}'$ in a standard form s.t. $\vdash P_{1}=P_{1}'$
+	Let's now consider a context: $\alpha_{1}.☐ + \sum_{i \in I}\alpha_{i}P_{i}$
+	Now we fill the context with $P_1$ and remove 1 from the set I (basically we pull it out from the summation): $$\alpha_{1}.P_{1} + \sum_{i \in I\setminus \{ 1 \}}\alpha_{i}P_{i}$$
+	Now we replace $P_1$ with $P_{1}'$
 ![](images/Pasted%20image%2020250429084921.png)
 ![](images/Pasted%20image%2020250429084950.png)
 replacing one by one every continuation with its standard form, obtaining standard form.