From d216fbf5aaacd97ca22c9fc11c953c4b93e72172 Mon Sep 17 00:00:00 2001
From: Marco Realacci <marco@marcorealacci.me>
Date: Tue, 15 Apr 2025 08:50:18 +0200
Subject: [PATCH] vault backup: 2025-04-15 08:50:18

---
 Concurrent Systems/notes/13 - CCS cose varie.md | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/Concurrent Systems/notes/13 - CCS cose varie.md b/Concurrent Systems/notes/13 - CCS cose varie.md
index de7f6f7..bddaeac 100644
--- a/Concurrent Systems/notes/13 - CCS cose varie.md	
+++ b/Concurrent Systems/notes/13 - CCS cose varie.md	
@@ -29,3 +29,16 @@ Which challenges can (a.P)\a have?
 ## Idempotency of Sum
 **Proposition:** $α.P+α.P+M ∼ α.P+M$
 *Proof:*
+$$S = \{ (α.P+α.P+M , α.P+M) \}$$
+Is it a bisimulation?
+NO: the problem is that, for example:
+- α.P+α.P+M –α–> P
+- α.P+M –α–> P
+- BUT (P,P) in general does NOT belong to S!
+
+So we can try with $$S = \{ (α.P+α.P+M , α.P+M) \} ∪ \{(P,P)\}$$
+But it is not yet a bisimulation. 
+P –β–> P’ (challenge and reply), but we don't have (P', P') in S.
+
+So let's try with: $$S = \{ (α.P+α.P+M , α.P+M) \} ∪ Id$$
+Let's go!
\ No newline at end of file