Congruenza forte

Ora vogliamo mostrare che la bisimualzione forte è una congruenza

Dimostriamo dunque che la bisimulazione forte è sostituitiva per tutti i combinatori:

Proposizione 6..7   Sia $p_1 \: \sim \: p_2$. Allora

1. $\alpha.p_1 \: \sim \: \alpha.p_2$

2. $p_1+q \: \sim \: p_2 +q$

3. $p_1\vert q \: \sim \: p_2\vert q$

4. $p_1 \setminus L \: \sim \: p_2 \setminus L$

5. $p_1[f] \: \sim \: p_2[f]$

Dimostrazione. Per 1., possiamo facilmente dedurre le condizioni 1. e 2. della proposizione 6.3 sostituendo $\alpha.p$ e $\alpha.q$ al posto di $p$ e $q$.

La prova per 2. è simile.

Per 3., invece, si deve mostrare che $\mathcal{S}$ è una bisimulazione, dove

$$\mathcal{S} = \{ (p_1\vert q, p_2\vert q) \: : \: p_1 \: \sim \: p_2 \}$$

Supponiamo allora che $(p_1\vert q, p_2\vert q) \: \in \: \mathcal{S}$. Sia $p_1 \vert q \stackrel{\alpha}{\longrightarrow} r$. Ci sono tre casi possibili:

Caso 1

$p_1 \stackrel{\alpha}{\longrightarrow} p_1'$ e $r \equiv p_1'\vert q$
Allora, dal momento che $p_1 \: \sim \: p_2$, abbiamo che $p_2 \stackrel{\alpha}{\longrightarrow} p_2'$ con $p_1' \: \sim \: p_2'$; da questo si ha $p_2\vert q \stackrel{\alpha}{\longrightarrow} p_2'\vert q$ e $(p_1'\vert q, p_2'\vert q) \: \in \: \mathcal{S}$.

Caso 2

$q \stackrel{\alpha}{\longrightarrow} q'$ e $r \equiv p_1\vert q'$
Allora anche $p_2\vert q \stackrel{\alpha}{\longrightarrow} p_2\vert q'$ e $(p_1\vert q', p_2\vert q') \: \in \: \mathcal{S}$.

Caso 3

$\alpha = \tau, p_1 \stackrel{l}{\longrightarrow} p_1' \: \wedge \: q \stackrel{\overline{l}}{\longrightarrow} q'$ e $r \equiv p_1'\vert q_1$
Allora, dal momento che $p_1 \: \sim \: p_2$, abbiamo che $p_2 \stackrel{l}{\longrightarrow} p_2'$ con $p_1' \: \sim \: p_2'$; da questo si ha $p_2\vert q \stackrel{\tau}{\longrightarrow} p_2'\vert q'$ e $(p_1'\vert q', p_2'\vert q') \: \in \: \mathcal{S}$.

Con un argomento simmetrico, si completa la prova che $\mathcal{S}$ è una bisimulazione forte.

Le prove per 4. e 5. sono simili.

$\qedsymbol$