vault backup: 2025-04-29 09:23:47

.obsidian/workspace.json

@@ -213,6 +213,9 @@
   },
   "active": "ec8d1a91f1f0cc7e",
   "lastOpenFiles": [
+    "Pasted image 20250429092305.png",
+    "Pasted image 20250429092055.png",
+    "Pasted image 20250429091959.png",
     "Concurrent Systems/slides/class 14.pdf",
     "Concurrent Systems/notes/14.md",
     "Pasted image 20250429091029.png",
@@ -223,8 +226,6 @@
     "Pasted image 20250429083535.png",
     "Pasted image 20250429083455.png",
     "Pasted image 20250429083129.png",
-    "Pasted image 20250429082905.png",
-    "Pasted image 20250429082812.png",
     "Concurrent Systems/notes/13 - Weak Bisimilarity.md",
     "Concurrent Systems/slides/class 13.pdf",
     "Concurrent Systems/notes/12 - Calculus of communicating system.md",

Concurrent Systems/notes/14.md

@@ -53,4 +53,11 @@ exercise: prove the weak bisimilarity
 
 Let us consider the parallel of processes M and R, by using the axiom for parallel, we have $$\vdash M|R=put.(\overline{go}|R)+go.(M|\overline{rcv})$$
 By using the same axiom to the parallel of the three processes, we obtain
-$$\vdash S|(M|R)=send.(\overline{put}|(M|R))+put.(\overline{go})$$
+$$\vdash S|(M|R)=send.(\overline{put}|(M|R))+put.(\overline{go}|R|S)+go.(\overline{rcv}|S|M)$$
+By restricting *put* and *go*, and by using the second axiom for restriction, we have that:
+![](../../Pasted%20image%2020250429091959.png)
+
+We now apply the third axiom for restriction to the three summands:
+![](../../Pasted%20image%2020250429092055.png)
+![](../../Pasted%20image%2020250429092305.png)
+