vault backup: 2025-04-30 19:28:22

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.