diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json
index 8db5437..0c778c3 100644
--- a/.obsidian/workspace.json
+++ b/.obsidian/workspace.json
@@ -192,6 +192,7 @@
   },
   "active": "ec8d1a91f1f0cc7e",
   "lastOpenFiles": [
+    "Pasted image 20250430192526.png",
     "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",
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 92a8db2..3e5770a 100644
--- a/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md	
+++ b/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md	
@@ -13,7 +13,7 @@ just what we've seen so far, literally.
  quite obvious.
 
 ![350](images/Pasted%20image%2020250429082905.png)
-basically we can let the left or the right process evolve, leaving the other unchanged, or they can synchronize.
+basically we can let the left or the right process evolve, leaving the other unchanged, or they can synchronize. So we remove the parallel by just adding all the possible cases.
 
 ![350](images/Pasted%20image%2020250429083129.png)
 - if a process does not perform any action, a restriction won't do anything
@@ -45,9 +45,11 @@ $P$ is in standard form if and only if $P \triangleq \sum_{i}\alpha_{i}P_{i}$ an
 
 1. $P \triangleq P_{1}|P_{2}$. By induction, we have that $\exists P_{1}',P_{2}'$ in standard form such that $\vdash P_{1}=P_{1}'$ and $P_{2}=P_{2}'$.
 
-	By context closure, $\vdash P_{1}|P_{2}=P_{1}'|P_{2}$ and $\vdash P_{1}'|P_{2}=P_{1}'|P_{2}'$
-
-![](images/Pasted%20image%2020250429084358.png)
+	By context closure, $\vdash P_{1}|P_{2}=P_{1}'|P_{2}$ and $\vdash P_{1}'|P_{2}=P_{1}'|P_{2}'$. Now we apply the axioms for parallel, until we remove all the occurrences of "|":
+	![](../../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}$
 ![](images/Pasted%20image%2020250429084921.png)
 ![](images/Pasted%20image%2020250429084950.png)
 replacing one by one every continuation with its standard form, obtaining standard form.
diff --git a/Pasted image 20250430192526.png b/Pasted image 20250430192526.png
new file mode 100644
index 0000000..cc0ac5a
Binary files /dev/null and b/Pasted image 20250430192526.png differ