marcorealacci/master-degree-notes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

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

Browse source
This commit is contained in:
Marco Realacci 2025-04-30 19:23:22 +02:00
parent 8acc318d2c
commit 54ca78a0be
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
Concurrent Systems/notes/14 Checking bisimilarity, an inference system.md
View file

@ -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. **Base case:** $P \triangleq 0$. It suffices to consider $P' \triangleq 0$ and conclude reflexivity.
**Inductive step:** we have to consider three cases. **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%2020250429084358.png)
![](images/Pasted%20image%2020250429084921.png) ![](images/Pasted%20image%2020250429084921.png)
![](images/Pasted%20image%2020250429084950.png) ![](images/Pasted%20image%2020250429084950.png)