vault backup: 2025-04-14 16:45:00

This commit is contained in:
Marco Realacci 2025-04-14 16:45:00 +02:00
parent 38494820ec
commit 3b2ae57b43

View file

@ -90,33 +90,23 @@ Sure Marco! Let's go step-by-step through the **CCS process transition example**
---
## 📘 Definitions
#### Example
##### 📘 Definitions
We start with the following **process definitions**:
- A≜a.AA \triangleq a.A'
- $A \triangleq a.A'$
- $A' \triangleq \bar{b}.A$
- $B \triangleq b.B'$
- $B' \triangleq \bar{c}.B$
- A≜bˉ.AA' \triangleq \bar{b}.A
- B≜b.BB \triangleq b.B'
- B≜cˉ.BB' \triangleq \bar{c}.B
Our **initial process** is:
ABA \mid B
---
## ▶️ Step 1: Transition from A
Our **initial process** is: $A \mid B$
##### ▶️ Step 1: Transition from A
From the definition:
- A≜a.AA \triangleq a.A'
So we can do:
A→aAA \xrightarrow{a} A'
- $A \triangleq a.A'$
- So we can do: $A \xrightarrow{a} A'$ (A consumes )
Using the **parallel rule** for the left-hand side: