From 54ca78a0be26d58013c39e1921ea1f75d09f9fab Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Wed, 30 Apr 2025 19:23:22 +0200 Subject: [PATCH] vault backup: 2025-04-30 19:23:22 --- .../notes/14 Checking bisimilarity, an inference system.md | 4 ++++ 1 file changed, 4 insertions(+) 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 8bab1b9..92a8db2 100644 --- a/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md +++ b/Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md @@ -43,6 +43,10 @@ $P$ is in standard form if and only if $P \triangleq \sum_{i}\alpha_{i}P_{i}$ an **Base case:** $P \triangleq 0$. It suffices to consider $P' \triangleq 0$ and conclude reflexivity. **Inductive step:** we have to consider three cases. +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) ![](images/Pasted%20image%2020250429084921.png) ![](images/Pasted%20image%2020250429084950.png)