From 350ef45e0a88629579a4e8e9f08cddc8074fd438 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Wed, 30 Apr 2025 19:38:22 +0200 Subject: [PATCH] vault backup: 2025-04-30 19:38:22 --- .../14 Checking bisimilarity, an inference system.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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 1671b8d..95f71e1 100644 --- a/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md +++ b/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md @@ -52,10 +52,10 @@ $P$ is in standard form if and only if $P \triangleq \sum_{i}\alpha_{i}P_{i}$ an 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. + Now we replace $P_1$ with $P_{1}'$ and obtain: $$=\alpha_{1}.P_{1}' + \sum_{i \in I\setminus \{ 1 \}}\alpha_{i}P_{i}$$ + imagine doing this until you pulled everything out... Standard form! + +3. ![](images/Pasted%20image%2020250429085319.png)