&\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;d{\boldsymbol{[}}\tau.(\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{4}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{d}}.\end{array}$

Finally, by Proposition 7 we get:

$\mathrm{GSP}_{6}(s_{1}[v]\mbox{; }s_{2}\mbox{ did not
gossip})\>\mathrel{{}_{1-p}\\!\\!\sqsupseteq}\>\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;d{\boldsymbol{[}}\tau.(\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{4}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{d}}$ (13)

Let us consider now the symmetric case.

#### (b) Node $s_{2}$ transmits while $s_{1}$ does not.

This case can be arranged by switching the roles of the nodes $s_{1}$ and
$s_{2}$ in Equation 12:

$\begin{array}[]{rl}&\mathrm{GSP}_{6}(\mbox{$s_{1}$ did not gossip; $s_{2}$
sends in $1$ or $2$ rounds})\\\\[2.0pt]
\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&s_{1}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\tau.(\sigma.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;d{\boldsymbol{[}}\tau.(\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{4}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{d}}\end{array}$ (14)

Finally, let us consider the last case.

#### (c) Both nodes $s_{1}$ and $s_{2}$ transmit.

If both senders decide to transmit in the same time instant then there will be
a collision and the transmitted message will never reach the destination. If
this happens then the network $\mathrm{GSP}_{6}$ cannot simulate a network in
which the message has reached the destination node $d$. On the other hand, if
$s_{1}$ broadcasts with a delay of one time unit, and $s_{2}$ with a delay of
two time units, then there will be no collisions and the message may
eventually reach the destination.

Thus, by an application of:  (i) Proposition 14(4) to timeout node $d$ in the
absence of a sender;  (ii) Corollary 23 to broadcast the message of $s_{1}$ to
$d$, together with Proposition 14(2) to work underneath $\sigma$ prefixes;
(iii) Proposition 14(3) to timeout node $d$, as after one round there are no
senders around;  (iv) the straightforward equation
$d{\boldsymbol{[}}{\mathsf{sndu}\langle
v\rangle}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\mathrel{{}_{0}\\!\\!\sqsupseteq}d{\boldsymbol{[}}{\sigma.{\mathsf{snd}\langle
v\rangle}_{1}}{\boldsymbol{]}}^{\nu_{d}}$, together with Proposition 14(2) to
work underneath $\sigma$ prefixes;  (v) Proposition 14(5) to model that the
message broadcast by $s_{2}$ gets lost, together with Proposition 14(2) to
work underneath $\sigma$ prefixes;  (vi) Proposition 14(1) to remove $\sigma$
prefixes in $s_{1}$ and $s_{2}$;  it follows that:

$\begin{array}[]{rl}&\mathrm{GSP}_{6}(\mbox{$s_{1}$ sends in $1$ round;
$s_{2}$ sends in $2$ rounds})\\\\[1.0pt]
\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&s_{1}{\boldsymbol{[}}\sigma.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{1}}}\>\;\big{|}\>\;s_{2}{\boldsymbol{[}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{2}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\end{array}$
$\begin{array}[]{rl}\mathrel{{}_{0}\\!\\!\sqsupseteq}&s_{1}{\boldsymbol{[}}\sigma.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{1}}}\>\;\big{|}\>\;s_{2}{\boldsymbol{[}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{2}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\sigma.\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{0}\\!\\!\sqsupseteq}&s_{1}{\boldsymbol{[}}\sigma.\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\>\;\big{|}\>\;s_{2}{\boldsymbol{[}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{2}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\sigma.\mathsf{resndu}\langle
v\rangle_{1,1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{0}\\!\\!\sqsupseteq}&s_{1}{\boldsymbol{[}}\sigma.\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\>\;\big{|}\>\;s_{2}{\boldsymbol{[}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{2}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\sigma.\sigma.{\mathsf{sndu}\langle
v\rangle}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{0}\\!\\!\sqsupseteq}&s_{1}{\boldsymbol{[}}\sigma.\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\>\;\big{|}\>\;s_{2}{\boldsymbol{[}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{2}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\sigma.\sigma.\sigma.{\mathsf{snd}\langle
v\rangle}_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{0}\\!\\!\sqsupseteq}&s_{1}{\boldsymbol{[}}\sigma.\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{1}}}\>\;\big{|}\>\;s_{2}{\boldsymbol{[}}\sigma^{2}.\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{2}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}.\end{array}$

By transitivity (Proposition 7) we derive:

$\mathrm{GSP}_{6}(\mbox{$s_{1}$ sends in $1$ round; $s_{2}$ sends in $2$
rounds})\;\mathrel{{}_{0}\\!\\!\sqsupseteq}\;\,\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}$ (15)

As nodes $s_{1}$ and $s_{2}$ have the same neighbours, the symmetric case,
when $s_{1}$ broadcasts with a delay of two rounds and $s_{2}$ with a delay of
one round, can be captured by switching the roles of $s_{1}$ and $s_{2}$ in
Equation 15:

$\begin{array}[]{rl}&\mathrm{GSP}_{6}(\mbox{$s_{1}$ sends in $2$ rounds ;
$s_{2}$ sends in $1$ round})\\\\[2.0pt]
\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&s_{1}{\boldsymbol{[}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{1}}}\>\;\big{|}\>\;s_{2}{\boldsymbol{[}}\sigma.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{2}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}|d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}.\end{array}$ (16)

Next, we compose the previous estimations to evaluate the tolerance when both
senders transmit with a probabilistic delay. Please, notice that the following
law holds for any network $N$ ($1$ is the maximum distance):

$s_{1}{\boldsymbol{[}}\sigma^{h}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{1}}}\>\;\big{|}\>\;s_{2}{\boldsymbol{[}}\sigma^{h}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{2}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\>\mathrel{{}_{1}\\!\\!\sqsupseteq}\>N$

In the rest of this section, we will use the following instances of the law
above:

$\begin{array}[]{c}s_{1}{\boldsymbol{[}}\sigma.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{1}}}\>\big{|}\>s_{2}{\boldsymbol{[}}\sigma.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{2}}}\>\big{|}\>d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\;\mathrel{{}_{1}\\!\\!\sqsupseteq}\;\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\big{|}\>d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\end{array}$ (17)

$\begin{array}[]{c}s_{1}{\boldsymbol{[}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{1}}}\big{|}\,s_{2}{\boldsymbol{[}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{2}}}\big{|}\,d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\,\mathrel{{}_{1}\\!\\!\sqsupseteq}\,\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\,\big{|}\,d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\end{array}$ (18)

Thus, in the case when $s_{1}$ broadcasts with a delay of one round and
$s_{2}$ with a probabilistic delay of one or two rounds, by applying, in
sequence:  (i) Theorem 18 in which the network $M$ is structural congruent to
$s_{1}{\boldsymbol{[}}\sigma.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{1}}}|d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}$,
and the node $m$ is instantiated as $s_{2}$, to compose the paths deriving
from Equation 15 and Equation 17;  (ii) the straightforward law
$d{\boldsymbol{[}}\tau.(\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{d}}\mathrel{{}_{0}\\!\\!\sqsupseteq}d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}$;  we derive:

$\begin{array}[]{rl}&\mathrm{GSP}_{6}(\mbox{$s_{1}$ sends in $1$ round;
$s_{2}$ sends in $1$ or $2$ rounds})\\\\[2.0pt]
\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&s_{1}{\boldsymbol{[}}\sigma.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{1}}}\>\;\big{|}\>\;s_{2}{\boldsymbol{[}}\tau.(\sigma.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{s_{2}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{\frac{1}{2}}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\tau.(\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}.\end{array}$

By transitivity (Proposition 7) we obtain

$\begin{array}[]{c}\mathrm{GSP}_{6}(\mbox{\small$s_{1}$ sends in $1$ rnd;
$s_{2}$ sends in $1$ or $2$
rnds})\>\mathrel{{}_{\frac{1}{2}}\\!\\!\sqsupseteq}\>\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}|d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}\end{array}$ (19)

Analogously, in the case when $s_{1}$ broadcasts with a delay of two rounds
and $s_{2}$ with a probabilistic delay of one or two rounds, we can apply in
sequence:  (i) Theorem 18 in which the network $M$ is structural congruent to
$s_{1}{\boldsymbol{[}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{1}}}|d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}$
and the node $m$ is instantiated as $s_{2}$, to compose the paths deriving
from Equation 16 and Equation 18;  (ii) the straightforward law
$d{\boldsymbol{[}}\tau.(\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{d}}\mathrel{{}_{0}\\!\\!\sqsupseteq}d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}$;  we derive:

$\begin{array}[]{rl}&\mathrm{GSP}_{6}(\mbox{$s_{1}$ sends in $2$ rounds;
$s_{2}$ sends in $1$ or $2$ rounds})\\\
\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&s_{1}{\boldsymbol{[}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{s_{1}}}\;\big{|}\;s_{2}{\boldsymbol{[}}\tau.(\sigma.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{s_{2}}}\;\big{|}\;d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{\frac{1}{2}}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\tau.(\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}.\end{array}$

By transitivity (Proposition 7) we obtain

$\mathrm{GSP}_{6}(\mbox{\small$s_{1}$ sends in $2$ rnds; $s_{2}$ sends in $1$
or $2$
rnds})\>\mathrel{{}_{\frac{1}{2}}\\!\\!\sqsupseteq}\;\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}$ (20)

Thus, to estimate the tolerance when both $s_{1}$ and $s_{2}$ broadcast with a
probabilistic delay of one or two steps, we can apply in sequence:  (i)
Theorem 18 in which the network $M$ is structural congruent to
$s_{2}{\boldsymbol{[}}\tau.(\sigma.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{s_{2}}}|d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}$
and the node $m$ is instantiated as $s_{1}$, to compose the paths deriving
from Equation 19 and Equation 20;  (ii) the straightforward law
$d{\boldsymbol{[}}\tau.(\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{d}}\mathrel{{}_{0}\\!\\!\sqsupseteq}d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}$;  to obtain:

$\begin{array}[]{rl}&\mathrm{GSP}_{6}(\mbox{both $s_{1}$ and $s_{2}$ send in
$1$ or $2$ rounds})\\\\[2.0pt]
\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\tau.(\sigma.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{\frac{1}{2}}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\tau.(\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}.\end{array}$

By transitivity (Proposition 7) we obtain

$\mathrm{GSP}_{6}(\mbox{\small both $s_{1}$ and $s_{2}$ send in $1$ or $2$
rounds})\>\mathrel{{}_{\frac{1}{2}}\\!\\!\sqsupseteq}\;\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\;\big{|}\;d{\boldsymbol{[}}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}{\boldsymbol{]}}^{\nu_{d}}$ (21)

By exploiting the three cases _(a), (b), (c)_ analysed above, we can calculate
now the tolerance $r$ of
$\mathrm{GSP}_{6}\,\mathrel{{}_{r}\\!\\!\sqsupseteq}\,\mathrm{DONE}_{6}$.
First, to estimate the tolerance when $s_{2}$ transmits (with a probabilistic
delay of one or two steps) independently whether $s_{1}$ transmits or not, we
can apply:  (i) Theorem 18 in which the network $M$ is structural congruent to
$s_{2}{\boldsymbol{[}}\tau.(\sigma.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{s_{2}}}|d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}$
and the node $m$ is instantiated as $s_{1}$, to compose the paths deriving
from Equation 14 and Equation 21;  (ii) Proposition 11(3)  (iii) both
additivity and commutativity properties of $\oplus$;  to obtain:

$\begin{array}[]{rl}&\mathrm{GSP}_{6}(\mbox{$s_{1}[v]$; $s_{2}$ sends in $1$
or $2$ rounds})\\\\[2.0pt]
\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&s_{1}{\boldsymbol{[}}\mathsf{sndu}\langle
v\rangle_{p,2}{\boldsymbol{]}}^{\nu_{s_{1}}}\>\;\big{|}\>\;s_{2}{\boldsymbol{[}}\tau.(\sigma.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{2}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{s_{2}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{\frac{p}{2}}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\tau.\big{(}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\oplus_{p}\tau.(\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{4}.\mathsf{snd}\langle
v\rangle_{1})\big{)}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\tau.\big{(}p{\colon}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\>\oplus\>{\frac{1}{2}}(1-p){\colon}\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\>\oplus\>{\frac{1}{2}}(1-p){\colon}\sigma^{4}.\mathsf{snd}\langle
v\rangle_{1}\big{)}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\tau.(\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\left(\frac{1}{2}+\frac{p}{2}\right)}\sigma^{4}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{d}}.\end{array}$

By transitivity (Proposition 7) we obtain

$\mathrm{GSP}_{6}(\mbox{\small$s_{1}[v]$; $s_{2}$ sends in $1$ or $2$
rnds})\>\mathrel{{}_{\frac{p}{2}}\\!\\!\sqsupseteq}\>\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}|d{\boldsymbol{[}}\tau.(\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\oplus_{q}\sigma^{4}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{d}}$ (22)

with $q=\left(\frac{1}{2}+\frac{p}{2}\right)$. Finally, in order to estimate
the behaviour of the whole network $\mathrm{GSP}_{6}$ we can apply in
sequence:  (i) Theorem 18 in which the network $M$ is structural congruent to
$s_{1}{\boldsymbol{[}}\mathsf{sndu}\langle
v\rangle_{p,2}{\boldsymbol{]}}^{\nu_{s_{1}}}|d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}$
and the node $m$ is instantiated as $s_{2}$, to compose the paths deriving
from Equation 13 and Equation 22;  (ii) Proposition 11(3) together with the
additivity and commutativity properties of $\oplus$;  to obtain:

$\begin{array}[]{rl}&\mathrm{GSP}_{6}\\\\[2.0pt]
\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{sndu}\langle
v\rangle_{p,2}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\mathsf{fwdu}_{1,1}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{r}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\tau.\big{(}\tau.(\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\oplus_{q}\sigma^{4}.\mathsf{snd}\langle
v\rangle_{1})\oplus_{p}\tau.(\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\oplus_{\frac{1}{2}}\sigma^{4}.\mathsf{snd}\langle
v\rangle_{1})\big{)}{\boldsymbol{]}}^{\nu_{d}}\\\\[3.0pt]
\mathrel{{}_{0}\\!\\!\sqsupseteq}&\prod_{i=1}^{2}s_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{s_{i}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\tau.(\sigma^{3}.\mathsf{snd}\langle
v\rangle_{1}\,\oplus_{q^{\prime}}\,\sigma^{4}.\mathsf{snd}\langle
v\rangle_{1}){\boldsymbol{]}}^{\nu_{d}}\\\\[2.0pt]
\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}&\mathrm{DONE}_{6}.\end{array}$

with $q^{\prime}=p\cdot q+(1-p)\cdot\frac{1}{2}=\frac{1}{2}{+}\frac{p^{2}}{2}$
and $r=p\cdot\frac{p}{2}+(1-p)(1-p)=1-(2p-\frac{3}{2}p^{2})$. By transitivity
(Proposition 7) we can finally derive

$\mathrm{GSP}_{6}\;\mathrel{{}_{r}\\!\\!\sqsupseteq}\;\,\mathrm{DONE}_{6}.$

Hence, the network $\mathrm{GSP_{6}}$ succeeds in delivering the message to
the destination node with (at least) probability $2p-\frac{3}{2}p^{2}$.

Summarising, in the previous sections we have seen that in the absence of
collisions the success probability of $\mathrm{GSP}_{1}$ is (at least)
$2p-p^{2}$. Whereas when collisions are taken into account, the network
$\mathrm{GSP}_{4}$ succeeds in propagating the message with (at least)
probability $2p-2p^{2}$, where $2p-2p^{2}<2p-p^{2}$, for any $p>0$. Since
$2p-2p^{2}<2p-\frac{3}{2}p^{2}<2p-p^{2}$, for any $p>0$, this small example
shows that the introduction of random delays may mitigate the effect of
collisions.

##  6\. Conclusions, related and future work

We have proposed a compositional analysis technique to formally study
probabilistic gossip protocols expressed in a simple probabilistic timed
process calculus for wireless networks. The calculus is equipped with a notion
of _weak simulation quasimetric_ which is used to define a _weak simulation
with tolerance_ , _i.e._ , a _compositional_ simulation theory to express that
a probabilistic system may be simulated by another one with a given tolerance
measuring the distance between the two systems. Basically, weak simulation
quasimetric is the asymmetric counterpart of _weak bisimulation metric_
[DJGP02], and the quantitative analogous of _weak simulation preorder_
[BKHH02, BHK04]. Based on our simulation quasimetric, we have developed an
_algebraic theory_ to estimate the performance of _gossip wireless networks_
in terms of the probability to successfully propagate messages up to the
desired destination. In our study we have considered gossip networks, with and
without _communication collisions_ , and _randomised gossip networks_ adopting
a uniform probability distribution to decide whether broadcasting a message.

A nice survey of formal verification techniques for the analysis of gossip
protocols appears in Bakhashi et al.’s paper [BBFH07]. Probabilistic model-
checking has been used by Fehnker and Gao [FG06] to study the influence of
different modelling choices on message propagation in flooding and gossip
protocols, and by Kwiatkowska et al. [KNP08] to investigate the expected
rounds of gossiping required to form a connected network and how the expected
path length between nodes evolves over the execution of the protocol. However,
the analysis of gossip protocols in large-scale networks remains beyond the
capabilities of current probabilistic model-checking tools. For this reason,
Bakhashi et al. [BCFH09] have suggested to apply mean-field analysis for a
formal evaluation of gossip protocols. Intuitively, the stochastic process
representing the modelled system converges to a deterministic process if the
number of nodes goes to infinity, providing an approximation for large numbers
of nodes. Finally, Bakhashi et al. [BGFvS09] have developed and validated an
analytical model, based on epidemic techniques, for a shuffle protocol, a
protocol to disseminate data items to a collection of wireless devices, in a
decentralised fashion.

A preliminary version of the current paper has appeared in [LMT17b]. However,
in that paper neither communication collisions nor randomised gossip protocols
are taken into account. The current paper is the ideal continuation of Lanotte
and Merro’s work [LM11]. In that paper, the authors developed a notion of
_simulation up to probability_ to measure the closeness rather than the
distance between two probabilistic systems. Then, as in here, simulation up to
probability has been used to provide an algebraic theory to evaluate the
performance of gossip networks. Despite the similarity of the two simulation
theories, the simulation up to probability has a number of limitations that
have motivated the current work:  (i) the simulation up to probability is not
transitive, while simulation quasimetrics are transitive by definition;  (ii)
in order to work with a transitive relation, paper [LM11] introduces an
auxiliary rooted simulation which is much stronger than the main definition;
(iii) that rooted simulation (and hence the simulation up to probability) is
not suitable to compose estimates originating from paths with different
lengths (as we do here by means of Theorem 18), and, more generally, to deal
with more transmissions;  (iv) paper [LM11] does not consider randomised
gossip protocols.

Our simulation quasimetric has been inspired by [DGJP04, DJGP02, vBW05,
DCPP06], where the notion of behavioural distance between two probabilistic
systems is formalised in terms of the notion of bisimulation metric.
Bisimulation metric works fine for systems being approximately equivalent.
Recent applications of weak bisimulation metrics can be found in [LMT18a,
LMT18b]. However, when the simulation game works only in one direction, as in
the gossip protocols analysed in the current paper, an asymmetric notion of
simulation pseudometric is required.

The compositionality criteria proposed in the literature for bisimulation
metrics require that operators satisfy different forms of _uniform continuity_
property [GT13, GT14, GLT15, GT15, LMT17a]. We proved that simulation
quasimetric matches one of the most restrictive, namely _non-expansiveness_
[DJGP02, DGJP04] (also known as 1-non-extensiveness [BBLM13]).

Finally, several process calculi for wireless systems have been proposed in
the last years [LS10, NH06, God07, SRS10, GFM10, FvGH+12, BHJ+15]. Among
these, Merro et al. [MBS11, CHM15] have proposed two different calculi
modelling time-consuming communication to formally represent and study
communication collisions in a wireless setting. Song and Godskesen [SG10] have
proposed the first probabilistic untimed calculus for wireless systems, where
connections are established with a given probability. pTCWS is a probabilistic
variant of the calculus proposed by Macedonio and Merro [MM14] that takes
inspiration from Deng et al.’s probabilistic CSP [DvGHM08].

As future work, we intend to study gossip protocols in the presence of lossy
channels. We then plan to apply our metric-based simulation theory in the
context of other probabilistic protocols, such as those for _probabilistic
anonymity_ [Cha88] and _probabilistic non-repudiation_ [MR99].

## Acknowledgments

The authors would like to thank the anonymous reviewers for their insightful
reviews.

## References

  * [BBFH07] R. Bakhshi, F. Bonnet, W. Fokkink, and B. R. Haverkort.  Formal analysis techniques for gossiping protocols.  Operating Systems Review, 41(5):28–36, 2007.
  * [BBLM13] G. Bacci, G. Bacci, K. G. Larsen, and R. Mardare.  Computing behavioral distances, compositionally.  In MFCS, volume 8087 of LNCS, pages 74–85. Springer, 2013\.
  * [BCFH09] R. Bakhshi, L. Cloth, W. Fokkink, and B. R. Haverkort.  Mean-Field Analysis for the Evaluation of Gossip Protocols.  In QEST, pages 247–256. IEEE Computer Society, 2009.
  * [BGFvS09] R. Bakhshi, D. Gavidia, W. Fokkink, and M. van Steen.  An analytical model of information dissemination for a gossip-based protocol.  Computer Networks, 53(13):2288–2303, 2009.
  * [BHJ+15] J. Borgström, S. Huang, M. Johansson, P. Raabjerg, B. Victor, J. A. Pohjola, and J. Parrow.  Broadcast psi-calculi with an application to wireless protocols.  Software and System Modeling, 14(1):201–216, 2015.
  * [BHK04] C. Baier, H. Hermanns, and J. P. Katoen.  Probabilistic weak simulation is decidable in polynomial time.  Information Processing Letters, 89(3):123–130, 2004.
  * [BKHH02] C. Baier, J. P. Katoen, H. Hermanns, and B. R. Haverkort.  Simulation for Continuous-Time Markov Chains.  In CONCUR, volume 2421 of LNCS, pages 338–354. Springer, 2002.
  * [Cha88] D. Chaum.  The dining cryptographers problem: Unconditional sender and recipient untraceability.  Journal of Cryptology, 1:65–75, 1988.
  * [CHM15] A. Cerone, M. Hennessy, and M. Merro.  Modelling mac-layer communications in wireless systems.  Logical Methods in Computer Science, 11(1:18), 2015.
  * [dAFS09] L. de Alfaro, M. Faella, and M. Stoelinga.  Linear and branching system metrics.  IEEE Transactions on Software Engineering, 35(2):258–273, 2009\.
  * [DCPP06] Y. Deng, T. Chothia, C. Palamidessi, and J. Pang.  Metrics for Action-labelled Quantitative Transition Systems.  In QAPL, volume 153(2) of ENTCS, pages 79–96, 2006.
  * [DD09] Y. Deng and W. Du.  The Kantorovich Metric in Computer Science: A Brief Survey.  In QAPL, volume 253(3) of ENTCS, pages 73–82, 2009.
  * [DD11] Y. Deng and W. Du.  Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation.  Technical Report CMU-CS-11-110, CMU, March 2011.
  * [Den15] Y. Deng.  Semantics of Probabilistic Processes: An Operational Approach.  Springer, 2015.
  * [DGJP04] J. Desharnais, J. Gupta, R. Jagadeesan, and P. Panangaden.  Metrics for Labelled Markov Processes.  Theoretical Computer Science, 318(3):323–354, 2004.
  * [DJGP02] J. Desharnais, R. Jagadeesan, V. Gupta, and P. Panangaden.  The metric analogue of weak bisimulation for probabilistic processes.  In LICS, pages 413–422. IEEE Computer Society, 2002.
  * [DvGHM08] Y. Deng, R. J. van Glabbeek, M. Hennessy, and C. Morgan.  Characterising testing preorders for finite probabilistic processes.  Logical Methods in Computer Science, 4(4), 2008.
  * [FG06] A. Fehnker and P. Gao.  Formal Verification and Simulation for Performance Analysis for Probabilistic Broadcast Protocols.  In ADHOC-NOW, volume 4104 of LNCS, pages 128–141. Springer, 2006.
  * [FvGH+12] A. Fehnker, R. J. van Glabbeek, P. Höfner, A. McIver, M. Portmann, and W. L. Tan.  A process algebra for wireless mesh networks.  In ESOP, volume 7211 of LNCS, pages 295–315. Springer, 2012\.
  * [GFM10] F. Ghassemi, W. Fokkink, and A. Movaghar.  Equational reasoning on mobile ad hoc networks.  Fundamenta Informaticae, 105(4):375–415, 2010.
  * [GJS90] A. Giacalone, C. Jou, and S. A. Smolka.  Algebraic reasoning for probabilistic concurrent systems.  In Proceedings of IFIP Work, Conf. on Programming, Concepts and Methods, pages 443–458, 1990.
  * [GLT15] D. Gebler, K. G. Larsen, and S. Tini.  Compositional Metric Reasoning with Probabilistic Process calculi.  In FoSSaCS, volume 9034 of LNCS, pages 230–245. Springer, 2015.
  * [GLT16] D. Gebler, K. G. Larsen, and S. Tini.  Compositional Bisimulation Metric Reasoning with Probabilistic Process Calculi.  Logical Methods in Computer Science, 12(4), 2016.
  * [God07] J. C. Godskesen.  A Calculus for Mobile Ad Hoc Networks.  In COORDINATION, volume 4467 of LNCS, pages 132–150. Springer, 2007.
  * [GT13] D. Gebler and S. Tini.  Compositionality of approximate bisimulation for probabilistic systems.  In EXPRESS/SOS, volume 120 of EPTCS, pages 32–46, 2013.
  * [GT14] D. Gebler and S. Tini.  Fixed-point Characterization of Compositionality Properties of Probabilistic Processes Combinators.  In EXPRESS/SOS, volume 160 of EPTCS, pages 63–78, 2014\.
  * [GT15] D. Gebler and S. Tini.  SOS Specifications of Probabilistic Systems by Uniformly Continuous Operators.  In CONCUR, volume 42 of LIPIcs, pages 155–168. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
  * [GT18] D. Gebler and S. Tini.  SOS specifications for uniformly continuous operators.  Journal of Computer and System Sciences, 92:113–151, 2018.
  * [HR95] M. Hennessy and T. Regan.  A Process Algebra for Timed Systems.  Information and Computation, 117(2):221–239, 1995.
  * [JLY01] B. Jonsson, K. G. Larsen, and W. Yi.  Probabilistic Extensions of Process Algebras.  In Handbook of Process Algebra, pages 685–710. Elsevier, 2001.
  * [KNP08] M. Z. Kwiatkowska, G. Norman, and D. Parker.  Analysis of a gossip protocol in PRISM.  SIGMETRICS Performance Evaluation Review, 36(3):17–22, 2008.
  * [KvS07] A. M. Kermarrec and M. van Steen.  Gossiping in distributed systems.  Operating Systems Review, 41(5):2–7, 2007.
  * [LM11] R. Lanotte and M. Merro.  Semantic analysis of gossip protocols for wireless sensor networks.  In CONCUR, volume 6901 of LNCS, pages 156–170. Springer, 2011.
  * [LMT17a] R. Lanotte, M. Merro, and S. Tini.  Compositional weak metrics for group key update.  In MFCS, volume 83 of LIPIcs, pages 72:1–72:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017.
  * [LMT17b] R. Lanotte, M. Merro, and S. Tini.  Weak simulation quasimetric in a gossip scenario.  In FORTE, volume 10321 of LNCS, pages 139–155. Springer, 2017.
  * [LMT18a] R. Lanotte, M. Merro, and S. Tini.  A Probabilistic Calculus of Cyber-Physical Systems.  Information and Computation, 2018.
  * [LMT18b] R. Lanotte, M. Merro, and S. Tini.  Towards a formal notion of impact metric for cyber-physical attacks.  In iFM, volume 11023 of LNCS. Springer, 2018.
  * [LS91] K. G. Larsen and A. Skou.  Bisimulation through Probabilistic Testing.  Information and Computation, 94(1):1–28, 1991.
  * [LS10] I. Lanese and D. Sangiorgi.  An Operational Semantics for a Calculus for Wireless Systems.  Theoretical Computer Science, 411:1928–1948, 2010.
  * [MBS11] M. Merro, F. Ballardin, and E. Sibilio.  A timed calculus for wireless systems.  Theoretical Computer Science, 412(47):6585–6611, 2011.
  * [Mil89] R. Milner.  Communication and Concurrency.  Prentice Hall, 1989.
  * [MM14] D. Macedonio and M. Merro.  A semantic analysis of key management protocols for wireless sensor networks.  Science of Computer Programming, 81:53–78, 2014.
  * [MR99] O. Markowitch and Y. Roggeman.  Probabilistic non-repudiation without trusted third party.  In SCN, LNCS, pages 1–12. Springer, 1999.
  * [MZS09] S. Misra, I. Zhang, and C. Subhas.  Guide to Wireless Ad Hoc Networks.  Springer Science & Business Media, 2009.
  * [NCO04] S. Nair and R. Cardell-Oliver.  Formal specification and analysis of performance variation in sensor network diffusion protocols.  In MSWiM, pages 170–173. ACM, 2004.
  * [NH06] S. Nanz and C. Hankin.  A Framework for Security Analysis of Mobile Wireless Networks.  Theoretical Computer Science, 367(1-2):203–227, 2006.
  * [NS92] X. Nicollin and J. Sifakis.  An Overview and Synthesis on Timed Process Algebras.  In CAV, volume 575 of LNCS, pages 376–398. Springer, 1992\.
  * [Seg95] R. Segala.  Modeling and Verification of Randomized Distributed Real-Time Systems.  PhD thesis, Laboratory for Computer Science, Massachusetts Institute of Technology, 1995.
  * [SG10] L. Song and J.C. Godskesen.  Probabilistic mobility models for mobile and wireless networks.  In IFIP TCS, volume 323 of IFIP, pages 86–100. Springer, 2010\.
  * [SL95] R. Segala and N. Lynch.  Probabilistic simulations for probabilistic processes.  Nordic Journal of Computing, 2:250–273, 1995.
  * [SRS10] A. Singh, C. R. Ramakrishnan, and S. A. Smolka.  A process calculus for Mobile Ad Hoc Networks.  Science of Computer Programming, 75(6):440–469, 2010.
  * [vBW05] F. van Breugel and J. Worrell.  A behavioural pseudometric for probabilistic transition systems.  Theoretical Computer Science, 331(1):115–142, 2005.
  * [Vil08] C. Villani.  Optimal transport, old and new.  Springer, 2008.

##  Appendix A Proofs

###  A.1. Proofs of results in Section 2

_Proof of Proposition 5_. Let ${\mathcal{R}}$ denote the relation
${\mathcal{R}}=\\{(M,N)\,:\,d(M,N)=0\\}$. We have to prove that, given any
pair of related networks $M\,{\mathcal{R}}\,N$, whenever
$M\xrightarrow{\,{\alpha}\,}\Delta$ there are a transition $N\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Theta$ and a matching
$\omega\in\Omega(\Delta,\Theta)$ with $\omega(M^{\prime},N^{\prime})>0$ only
if $M^{\prime}\,{\mathcal{R}}\,N^{\prime}$. By definition of ${\mathcal{R}}$,
relation $M\,{\mathcal{R}}\,N$ implies $d(M,N)=0$. Being $d$ a weak simulation
quasimetric, $d(M,N)=0$ implies that whenever
$M\xrightarrow{\,{\alpha}\,}\Delta$ there are a transition $N\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Theta$ with
$\operatorname{\mathbf{K}}(d)(\Delta,\Theta+(1-\mid\\!\\!{\Theta}\\!\\!\mid)\overline{\mathsf{Dead}})\leq
d(M,N)=0$. From
$\operatorname{\mathbf{K}}(d)(\Delta,\Theta+(1-\mid\\!\\!{\Theta}\\!\\!\mid)\overline{\mathsf{Dead}})\leq
0$ we infer that $\mid\\!\\!{\Theta}\\!\\!\mid=1$, thus giving
$\operatorname{\mathbf{K}}(d)(\Delta,\Theta)=0$. Let
$\omega\in\Omega(\Delta,\Theta)$ be one of the optimal matchings realising
$\operatorname{\mathbf{K}}(d)(\Delta,\Theta)$. From
$\operatorname{\mathbf{K}}(d)(\Delta,\Theta)=0$ we infer that
$\omega(M^{\prime},N^{\prime})>0$ only if $d(M^{\prime},N^{\prime})=0$.
Namely, $\omega(M^{\prime},N^{\prime})>0$ only if
$M^{\prime}\,{\mathcal{R}}\,N^{\prime}$, which complete the proof. ∎

To prove Theorem 6 we need two preliminary results. First we show that the
pseudoquasimetric property is preserved by function
$\operatorname{\mathbf{K}}$, namely $\operatorname{\mathbf{K}}(d)$ is a
pseudoquasimetric whenever $d$ is a pseudoquasimetric.

######  Proposition 24.

If $d\colon\texttt{pTCWS}{}\times\texttt{pTCWS}{}\to[0,1]$ is a $1$-bounded
pseudoquasimetric, then $\operatorname{\mathbf{K}}(d)$ is a $1$-bounded
pseudoquasimetric.

######  Proof A.1.

To show $\operatorname{\mathbf{K}}(d)(\Delta,\Delta)=0$ it is enough to take
the matching $\omega\in\Omega(\Delta,\Delta)$ defined by
$\omega(M,M)=\Delta(M)$, for all $M\in\texttt{pTCWS}{}$, and $\omega(M,N)=0$,
for all $M,N\in\texttt{pTCWS}{}$ with $M\neq N$. In fact, we obtain
$\operatorname{\mathbf{K}}(d)(\Delta,\Delta)=0$ by
$\operatorname{\mathbf{K}}(d)(\Delta,\Delta)\leq\sum_{M,N\in\texttt{pTCWS}}\omega(M,N)\cdot
d(M,N)=\sum_{M\in\texttt{pTCWS}}\Delta(M)\cdot d(M,M)=0$, because $d(M,M)=0$.

To show the triangular property
$\operatorname{\mathbf{K}}(d)(\Delta_{1},\Delta_{2})\leq\operatorname{\mathbf{K}}(d)(\Delta_{1},\Delta_{3})+\operatorname{\mathbf{K}}(d)(\Delta_{3},\Delta_{2})$,
we take the function
$\omega\colon\texttt{pTCWS}{}\times\texttt{pTCWS}{}\to[0,1]$ defined for all
networks $M_{1},M_{2}\in\texttt{pTCWS}{}$ as
$\omega(M_{1},M_{2})=\sum_{M_{3}\in\texttt{pTCWS}{}\mid\Delta_{3}(M_{3})\neq
0}\frac{\omega_{1}(M_{1},M_{3})\cdot\omega_{2}(M_{3},M_{2})}{\Delta_{3}(M_{3})}$,
with $\omega_{1}\in\Omega(\Delta_{1},\Delta_{3})$ one of the optimal matchings
realising $\operatorname{\mathbf{K}}(d)(\Delta_{1},\Delta_{3})$, and
$\omega_{2}\in\Omega(\Delta_{3},\Delta_{2})$ one of the optimal matchings
realising $\operatorname{\mathbf{K}}(d)(\Delta_{3},\Delta_{2})$. Then, we
prove that:  (i) $\omega$is a matching in $\Omega(\Delta_{1},\Delta_{2})$, and
(ii) $\sum_{M_{1},M_{2}\in\texttt{pTCWS}{}}\omega(M_{1},M_{2})\cdot
d(M_{1},M_{2})\leq\operatorname{\mathbf{K}}(d)(\Delta_{1},\Delta_{3})+\operatorname{\mathbf{K}}(d)(\Delta_{3},\Delta_{2})$,
which immediately implies
$\operatorname{\mathbf{K}}(d)(\Delta_{1},\Delta_{2})\leq\operatorname{\mathbf{K}}(d)(\Delta_{1},\Delta_{3})+\operatorname{\mathbf{K}}(d)(\Delta_{3},\Delta_{2})$.
To show (i) we prove that the left marginal of $\omega$ is $\Delta_{1}$ by
$\begin{array}[]{rl}&\sum_{M_{2}\in\texttt{pTCWS}{}}\omega(M_{1},M_{2})\\\\[3.0pt]
=&\sum_{M_{2}\in\texttt{pTCWS}{}}\sum_{M_{3}\in\texttt{pTCWS}{}\mid\Delta_{3}(M_{3})\neq
0}\frac{\omega_{1}(M_{1},M_{3})\cdot\omega_{2}(M_{3},M_{2})}{\Delta_{3}(M_{3})}\\\\[3.0pt]
=&\sum_{M_{3}\in\texttt{pTCWS}{}\mid\Delta_{3}(M_{3})\neq
0}\frac{\omega_{1}(M_{1},M_{3})\cdot\Delta_{3}(M_{3})}{\Delta_{3}(M_{3})}\\\\[3.0pt]
=&\sum_{M_{3}\in\texttt{pTCWS}{}\mid\Delta_{3}(M_{3})\neq
0}\omega_{1}(M_{1},M_{3})\\\\[3.0pt] =&\Delta_{1}(M_{1})\end{array}$

with the second step by $\omega_{2}\in\Omega(\Delta_{3},\Delta_{2})$ and the
last step by $\omega_{1}\in\Omega(\Delta_{1},\Delta_{3})$. The proof that the
right marginal of $\omega$ is $\Delta_{2}$ is analogous. Then, we show (ii) by
$\begin{array}[]{rlr}&\sum_{M_{1},M_{2}\in\texttt{pTCWS}{}}\omega(M_{1},M_{2})\cdot
d(M_{1},M_{2})\\\\[3.0pt]
=&\sum_{M_{1},M_{2}\in\texttt{pTCWS}{}}\sum_{M_{3}\in\texttt{pTCWS}{}\mid\Delta_{3}(M_{3})\neq
0}\frac{\omega_{1}(M_{1},M_{3})\cdot\omega_{2}(M_{3},M_{2})}{\Delta_{3}(M_{3})}\cdot
d(M_{1},M_{2})\\\\[3.0pt]
\leq&\sum_{M_{1},M_{2}\in\texttt{pTCWS}{},M_{3}\in\texttt{pTCWS}{}\mid\Delta_{3}(M_{3})\neq
0}\frac{\omega_{1}(M_{1},M_{3})\cdot\omega_{2}(M_{3},M_{2})}{\Delta_{3}(M_{3})}\cdot
d(M_{1},M_{3})\;+\\\\[3.0pt]
&\sum_{M_{1},M_{2}\in\texttt{pTCWS}{},M_{3}\in\texttt{pTCWS}{}\mid\Delta_{3}(M_{3})\neq
0}\frac{\omega_{1}(M_{1},M_{3})\cdot\omega_{2}(M_{3},M_{2})}{\Delta_{3}(M_{3})}\cdot
d(M_{3},M_{2})\\\\[4.0pt]
=&\sum_{M_{1},M_{3}\in\texttt{pTCWS}{}}\frac{\omega_{1}(M_{1},M_{3})\cdot\Delta_{3}(M_{3})}{\Delta_{3}(M_{3})}\cdot
d(M_{1},M_{3})\;+\\\\[3.0pt]
&\sum_{M_{2},M_{3}\in\texttt{pTCWS}{}}\frac{\Delta_{3}(M_{3})\cdot\omega_{2}(M_{3},M_{2})}{\Delta_{3}(M_{3})}\cdot
d(M_{3},M_{2})\\\\[3.0pt]
=&\sum_{M_{1},M_{3}\in\texttt{pTCWS}{}}\omega_{1}(M_{1},M_{3})\cdot
d(M_{1},M_{3})\;+\sum_{M_{2},M_{3}\in\texttt{pTCWS}{}}\omega_{2}(M_{3},M_{2})\cdot
d(M_{3},M_{2})\\\\[3.0pt]
=&\operatorname{\mathbf{K}}(d)(\Delta_{1},\Delta_{3})+\operatorname{\mathbf{K}}(d)(\Delta_{3},\Delta_{2})\end{array}$
where the inequality follows from the triangular property of $d$ and the third
last equality follows by $\omega_{2}\in\Omega(\Delta_{3},\Delta_{2})$ and
$\omega_{1}\in\Omega(\Delta_{1},\Delta_{2})$.

Now we prove that if $d(M,N)<1$ for any weak simulation quasimetric $d$, then
$N$ is able to simulate transitions of the form $M\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Delta$, besides those of the form
$M\xrightarrow{\,{\alpha}\,}\Delta$.

######  Lemma 25.

Assume any weak simulation quasimetric $d$ and two networks
$M,N\in\texttt{pTCWS}{}$ with $d(M,N)<1$. If $M\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Delta$ then there is a weak
transition $N\ext@arrow 0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Theta$ such
that
$\operatorname{\mathbf{K}}(d)(\Delta+(1-\mid\\!\\!{\Delta}\\!\\!\mid)\overline{\mathsf{Dead}},\Theta+(1-\mid\\!\\!{\Theta}\\!\\!\mid)\overline{\mathsf{Dead}})\leq
d(M,N)$.

######  Proof A.2.

We proceed by induction on the length $n$ of $M\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Delta$.

_Base case $n=1$_. We have two cases: The first is $\alpha=\tau$ and
$\Delta=\overline{M}$, the second is $M\xrightarrow{\,{\alpha}\,}\Delta$. In
the first case, by definition of
$\mathrel{\;\raisebox{0.0pt}{$\stackrel{{\scriptstyle\,\widehat{\tau}}}{{\makebox[13.22226pt]{\mbox{}\leavevmode\xleaders\hbox{$\mkern-2.6mu\Relbar\mkern-2.6mu$}\hfill\mbox{}}}}$}\Rightarrow}$
we have $N\ext@arrow 0359\Rightarrowfill@{}{\,{\widehat{\tau}}\,}\overline{N}$
and the thesis holds for the distribution $\Theta=\overline{N}$ by
$\operatorname{\mathbf{K}}(d)(\overline{M}+(1-\mid\\!\\!{\overline{M}}\\!\\!\mid)\overline{\mathsf{Dead}}),\overline{N}+(1-\mid\\!\\!{\overline{N}}\\!\\!\mid)\overline{\mathsf{Dead}})=\operatorname{\mathbf{K}}(d)(\overline{M},\overline{N})=d(M,N)$.
In the second case, the thesis follows directly by the definition of weak
simulation quasimetric.

_Inductive step $n>1$_. The derivation $M\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Delta$ is obtained by $M\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\beta}_{1}}\,}\Delta^{\prime}$ and
$\Delta^{\prime}\xrightarrow{\,{\hat{\beta}_{2}}\,}\Delta$, for some
distribution $\Delta^{\prime}\in{\mathcal{D}}(\texttt{pTCWS}{})$. The length
of the derivation $M\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\beta}_{1}}\,}\Delta^{\prime}$ is $n-1$ and
hence, by the inductive hypothesis, there is a weak transition $N\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\beta}_{1}}\,}\Theta^{\prime}$ such that
$\operatorname{\mathbf{K}}(d)(\Delta^{\prime}+(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid)\overline{\mathsf{Dead}},\Theta^{\prime}+(1-\mid\\!\\!{\Theta^{\prime}}\\!\\!\mid)\overline{\mathsf{Dead}})\leq
d(M,N)$. The sub-distributions $\Delta^{\prime}$ and $\Theta^{\prime}$ are of
the form $\Delta^{\prime}=\sum_{i\in I}p_{i}M_{i}$ and
$\Theta^{\prime}=\sum_{j\in J}q_{j}N_{j}$, for suitable networks $M_{i}$ and
$N_{j}$. We have two sub-cases: The first is $\beta_{1}=\tau$ and
$\beta_{2}=\alpha$, the other $\beta_{1}=\alpha$ and $\beta_{2}=\tau$.

We consider the case $\beta_{1}=\tau$ and $\beta_{2}=\alpha$, the other is
analogous. In this case we have
$\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid=\mid\\!\\!{\Theta^{\prime}}\\!\\!\mid=1$
and $\operatorname{\mathbf{K}}(d)(\Delta^{\prime},\Theta^{\prime})\leq
d(M,N)$. The transition
$\Delta^{\prime}\xrightarrow{\,{\hat{\beta}_{2}}\,}\Delta$ is derived from a
$\beta_{2}$-transition by some of the networks $M_{i}$, namely $I$ is
partitioned into sets $I_{1}$ and $I_{2}$ such that:  (i) for all $i\in I_{1}$
we have $M_{i}\xrightarrow{\,{\beta_{2}}\,}\Delta_{i}$ for suitable
distributions $\Delta_{i}$,  (ii) for each $i\in I_{2}$ we have
$M_{i}\not\\!\\!\xrightarrow{\,{\beta_{2}}\,}$,  (iii) $\Delta=\sum_{i\in
I_{1}}p_{i}\Delta_{i}$,  (iv) $1-|\Delta|=\sum_{i\in I_{2}}p_{i}$.
Analogously, $J$ is partitioned into sets $J_{1}$ and $J_{2}$ such that for
all $j\in J_{1}$ we have $N_{j}\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\beta}_{2}}\,}\Theta_{j}$ for suitable
distributions $\Theta_{j}$ and for each $j\in J_{2}$ we have
$N_{j}\not\\!\\!\ext@arrow 0359\Rightarrowfill@{}{\,{\hat{\beta}_{2}}\,}$.
This gives $\Theta^{\prime}\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\beta}_{2}}\,}\Theta$ with $\Theta=\sum_{j\in
J_{1}}q_{j}\Theta_{j}$. Since we had $N\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\beta}_{1}}\,}\Theta^{\prime}$, we can conclude
$N\ext@arrow 0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Theta$. In the
following we will prove that the transitions $N_{j}\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\beta}_{2}}\,}\Theta_{j}$ can be chosen so that
$\operatorname{\mathbf{K}}(d)(\Delta+(1-\mid\\!\\!{\Delta}\\!\\!\mid)\overline{\mathsf{Dead}},\Theta+(1-\mid\\!\\!{\Theta}\\!\\!\mid)\overline{\mathsf{Dead}})\leq
d(M,N)$, which will conclude the proof.

Let $\omega$ be one of the optimal matchings realising
$\operatorname{\mathbf{K}}(d)(\Delta^{\prime},\Theta^{\prime})$. Since
$p_{i}=\sum_{j\in J}\omega(M_{i},N_{j})$ for all $i\in I$ and, then,
$q_{j}=\sum_{i\in I}\omega(M_{i},N_{j})$ for all $j\in J$, we can rewrite the
distributions $\Delta^{\prime}=\sum_{i\in I}p_{i}M_{i}$ and
$\Theta^{\prime}=\sum_{j\in J}q_{j}N_{j}$ as $\Delta^{\prime}=\sum_{i\in
I,j\in J}\omega(M_{i},N_{j})M_{i}$ and $\Theta^{\prime}=\sum_{i\in I,j\in
J}\omega(M_{i},N_{j})N_{j}$. For all $i\in I_{1}$ and $j\in J$, define
$\Delta_{i,j}=\Delta_{i}$. Since $\Delta=\sum_{i\in I_{1}}p_{i}\Delta_{i}$, we
can rewrite $\Delta$ as $\Delta=\sum_{i\in I_{1},j\in
J}\omega(M_{i},N_{j})\Delta_{i,j}$. Analogously, for each $j\in J_{1}$ and
$i\in I$ we note that the transition $q_{j}\overline{N_{j}}\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\beta}_{2}}\,}\Theta_{j}$ can always be split
into $\sum_{i\in I}\omega(M_{i},N_{j})\overline{N_{j}}\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\beta}_{2}}\,}\sum_{i\in
I}\omega(M_{i},N_{j})\Theta_{i,j}$ for suitable distributions $\Theta_{i,j}$
so that for all $j\in J_{1}$ we can rewrite $\Theta_{j}$ as
$\Theta_{j}=\sum_{i\in I}\omega(M_{i},N_{j})\Theta_{i,j}$, and we can rewrite
$\Theta$ as $\Theta=\sum_{i\in I,j\in J_{1}}\omega(M_{i},N_{j})\Theta_{i,j}$.
Then we note that for all $i\in I_{1}$ and $j\in J_{1}$ with
$d(M_{i},N_{j})<1$, the transition $N_{j}\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\beta}_{2}}\,}\Theta_{i,j}$ can be chosen so
that
$\operatorname{\mathbf{K}}(d)(\Delta_{i,j},\Theta_{i,j}+(1-\mid\\!\\!{\Theta_{i,j}}\\!\\!\mid)\overline{\mathsf{Dead}})\leq
d(M_{i},N_{j})$. For all $i\in I_{1}$ and $j\in J_{1}$ with
$d(M_{i},N_{j})<1$, let $\omega_{i,j}$ be one of the optimal matchings
realising
$\operatorname{\mathbf{K}}(d)(\Delta_{i,j},\Theta_{i,j}+(1-\mid\\!\\!{\Theta_{i,j}}\\!\\!\mid)\overline{\mathsf{Dead}})$.

Define $\omega^{\prime}\colon\texttt{pTCWS}{}\times\texttt{pTCWS}{}\to[0,1]$
as the function such that $\omega^{\prime}(M^{\prime},N^{\prime})$ is the
summation of the following values:

  1. (1)

$\sum_{i\in I_{1},j\in
J_{1}}\omega(M_{i},N_{j})\cdot\omega_{i,j}(M^{\prime},N^{\prime})$

  2. (2)

$\sum_{i\in I_{1},j\in
J_{2}}\omega(M_{i},N_{j})\cdot\Delta_{i,j}(M^{\prime})\cdot\overline{\mathsf{Dead}}(N^{\prime})$

  3. (3)

$\sum_{i\in I_{2},j\in
J_{1}}\omega(M_{i},N_{j})\cdot\left(\overline{\mathsf{Dead}}(M^{\prime})\cdot\Theta_{i,j}(N^{\prime})+(1-\mid\\!\\!{\Theta_{i,j}}\\!\\!\mid)\cdot\overline{\mathsf{Dead}}(M^{\prime})\cdot\overline{\mathsf{Dead}}(N^{\prime})\right)$

  4. (4)

$\sum_{i\in I_{2},j\in
J_{2}}\omega(M_{i},N_{j})\cdot\overline{\mathsf{Dead}}(M^{\prime})\cdot\overline{\mathsf{Dead}}(N^{\prime})$.

To infer the proof obligation
$\operatorname{\mathbf{K}}(d)(\Delta+(1-\mid\\!\\!{\Delta}\\!\\!\mid)\overline{\mathsf{Dead}},\Theta+(1-\mid\\!\\!{\Theta}\\!\\!\mid)\overline{\mathsf{Dead}})\leq
d(M,N)$ it is now enough to show that:

  1. (a)

the function $\omega^{\prime}$ is a matching in
$\Omega(\Delta+(1-\mid\\!\\!{\Delta}\\!\\!\mid)\overline{\mathsf{Dead}},\Theta+(1-\mid\\!\\!{\Theta}\\!\\!\mid)\overline{\mathsf{Dead}})$,
and

  2. (b)

$\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}{}}\omega^{\prime}(M^{\prime},N^{\prime})\cdot
d(M^{\prime},N^{\prime})\leq d(M,N)$.

To show (a) we prove that the left marginal of $\omega^{\prime}$ is
$\Delta+(1-\mid\\!\\!{\Delta}\\!\\!\mid)\overline{\mathsf{Dead}}$. The proof
that the right marginal is
$\Theta+(1-\mid\\!\\!{\Theta}\\!\\!\mid)\overline{\mathsf{Dead}})$ is
analogous. For any network $M^{\prime}\in\texttt{pTCWS}{}$ we have that
$\sum_{N^{\prime}\in\texttt{pTCWS}}\omega^{\prime}(M^{\prime},N^{\prime})$ is
the summation of the following values:

  1. (1)

$\sum_{N^{\prime}\in\texttt{pTCWS}}\sum_{i\in I_{1},j\in
J_{1}}\omega(M_{i},N_{j})\cdot\omega_{i,j}(M^{\prime},N^{\prime})=\sum_{i\in
I_{1},j\in J_{1}}\omega(M_{i},N_{j})\cdot\Delta_{i,j}(M^{\prime})$

  2. (2)

$\sum_{N^{\prime}\in\texttt{pTCWS}}\sum_{i\in I_{1},j\in
J_{2}}\omega(M_{i},N_{j})\cdot\Delta_{i,j}(M^{\prime})\cdot\overline{\mathsf{Dead}}(N^{\prime})=\sum_{i\in
I_{1},j\in J_{2}}\omega(M_{i},N_{j})\cdot\Delta_{i,j}(M^{\prime})$

  3. (3)

$\sum_{N^{\prime}\in\texttt{pTCWS}}\sum_{i\in I_{2},j\in
J_{1}}\omega(M_{i},N_{j})\left(\overline{\mathsf{Dead}}(M^{\prime})\Theta_{i,j}(N^{\prime})+(1-\mid\\!\\!{\Theta_{i,j}}\\!\\!\mid)\overline{\mathsf{Dead}}(M^{\prime})\overline{\mathsf{Dead}}(N^{\prime})\right)\\\
=\sum_{i\in I_{2},j\in
J_{1}}\omega(M_{i},N_{j})\cdot\overline{\mathsf{Dead}}(M^{\prime})$

  4. (4)

$\sum_{N^{\prime}\in\texttt{pTCWS}}\sum_{i\in I_{2},j\in
J_{2}}\omega(M_{i},N_{j})\overline{\mathsf{Dead}}(M^{\prime})\overline{\mathsf{Dead}}(N^{\prime})=\sum_{i\in
I_{2},j\in J_{2}}\omega(M_{i},N_{j})\overline{\mathsf{Dead}}(M^{\prime})$

with the first equality by
$\omega_{i,j}\in\Omega(\Delta_{i,j},\Theta_{i,j}+(1-\mid\\!\\!{\Theta_{i,j}}\\!\\!\mid)$,
the second by
$\sum_{N^{\prime}\in\texttt{pTCWS}{}}\overline{\mathsf{Dead}}(N^{\prime})=1$,
the third by
$\sum_{N^{\prime}\in\texttt{pTCWS}{}}\Theta_{i,j}(N^{\prime})=\mid\\!\\!{\Theta_{i,j}}\\!\\!\mid$
and
$\sum_{N^{\prime}\in\texttt{pTCWS}{}}\overline{\mathsf{Dead}}(N^{\prime})=1$,
and the last by
$\sum_{N^{\prime}\in\texttt{pTCWS}{}}\overline{\mathsf{Dead}}(N^{\prime})=1$.

The summation of the first two items gives $\sum_{i\in I_{1},j\in
J}\omega(M_{i},N_{j})\cdot\Delta_{i,j}(M^{\prime})$, which is
$\Delta(M^{\prime})$ by the definition of $\Delta$, and the summation of the
last two items gives $\sum_{i\in I_{2},j\in
J}\omega(M_{i},N_{j})\cdot\overline{\mathsf{Dead}}(M^{\prime})$, which is
$(1-\mid\\!\\!{\Delta}\\!\\!\mid)\overline{\mathsf{Dead}}(M^{\prime})$.
Overall, the summation of all items gives
$\Delta(M^{\prime})+(1-\mid\\!\\!{\Delta}\\!\\!\mid)\overline{\mathsf{Dead}}(M^{\prime})$,
namely
$(\Delta+(1-\mid\\!\\!{\Delta}\\!\\!\mid)\overline{\mathsf{Dead}})(M^{\prime})$.

To prove (b), by the definition of $\omega^{\prime}$ we have that
$\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}}\omega^{\prime}(M^{\prime},N^{\prime})\cdot
d(M^{\prime},N^{\prime})$ is the summation of the following values:

  1. (1)

$\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}}\sum_{i\in I_{1},j\in
J_{1}}\omega(M_{i},N_{j})\cdot\omega_{i,j}(M^{\prime},N^{\prime})\cdot
d(M^{\prime},N^{\prime})$

  2. (2)

$\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}}\sum_{i\in I_{1},j\in
J_{2}}\omega(M_{i},N_{j})\cdot\Delta_{i,j}(M^{\prime})\cdot\overline{\mathsf{Dead}}(N^{\prime})\cdot
d(M^{\prime},N^{\prime})\\\ =\sum_{M^{\prime}\in\texttt{pTCWS}}\sum_{i\in
I_{1},j\in J_{2}}\omega(M_{i},N_{j})\cdot\Delta_{i,j}(M^{\prime})\cdot
d(M^{\prime},\mathsf{Dead})\\\
\leq\sum_{M^{\prime}\in\texttt{pTCWS}}\sum_{i\in I_{1},j\in
J_{2}}\omega(M_{i},N_{j})\cdot\Delta_{i,j}(M^{\prime})$

  3. (3)

$\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}}\sum_{i\in I_{2},j\in
J_{1}}\omega(M_{i},N_{j})\cdot(\overline{\mathsf{Dead}}(M^{\prime})\cdot\Theta_{i,j}(N^{\prime})+(1-\mid\\!\\!{\Theta_{i,j}}\\!\\!\mid)\cdot\overline{\mathsf{Dead}}(M^{\prime})\cdot\overline{\mathsf{Dead}}(N^{\prime}))\cdot
d(M^{\prime},N^{\prime})=0$

  4. (4)

$\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}}\sum_{i\in I_{2},j\in
J_{2}}\omega(M_{i},N_{j})\cdot\overline{\mathsf{Dead}}(M^{\prime})\cdot\overline{\mathsf{Dead}}(N^{\prime})\cdot
d(M^{\prime},N^{\prime})=0$.

where in the second item the equality follows from
$\overline{\mathsf{Dead}}(\mathsf{Dead})=1$ and
$\overline{\mathsf{Dead}}(N^{\prime})=0$ for all $N^{\prime}\neq\mathsf{Dead}$
and the inequality from $d(M^{\prime},\mathsf{Dead})\leq 1$, and in the third
and fourth item the equality follows by the fact the only network with
$\overline{\mathsf{Dead}}(M^{\prime})>0$ is $\mathsf{Dead}$, for which we have
$d(\mathsf{Dead}^{\prime},N^{\prime})=0$ for all
$N^{\prime}\in\texttt{pTCWS}{}$.

By the definition of $\omega_{i,j}$ the first item is $\sum_{i\in I_{1},j\in
J_{1}}\omega(M_{i},N_{j})\cdot\operatorname{\mathbf{K}}(d)(\Delta_{i,j},\Theta_{i,j})$.
If $d(M_{i},N_{j})<1$, we argued above that the distribution $\Theta_{i,j}$
satisfies $\operatorname{\mathbf{K}}(d)(\Delta_{i,j},\Theta_{i,j})\leq
d(M_{i},N_{j})$. If $d(M_{i},N_{j})=1$, then
$\operatorname{\mathbf{K}}(d)(\Delta_{i,j},\Theta_{i,j})\leq d(M_{i},N_{j})$
is immediate. Henceforth we are sure that in all cases the first item is less
or equal $\sum_{i\in I_{1},j\in J_{1}}\omega(M_{i},N_{j})\cdot
d(M_{i},N_{j})$. The second item is clearly less or equal than $\sum_{i\in
I_{1},j\in J_{2}}\omega(M_{i},N_{j})$. Summarising, we have

$\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}}\omega^{\prime}(M^{\prime},N^{\prime})\cdot
d(M^{\prime},N^{\prime})\leq\sum_{i\in I_{1},j\in
J_{1}}\omega(M_{i},N_{j})\cdot d(M_{i},N_{j})+\sum_{i\in I_{1},j\in
J_{2}}\omega(M_{i},N_{j}).$

Then, since $\operatorname{\mathbf{K}}(d)(\Delta^{\prime},\Theta^{\prime})$ is
the summation of the following values:

  * •

$\sum_{i\in I_{1},j\in J_{1}}\omega(M_{i},N_{j})\cdot d(M_{i},N_{j})$

  * •

$\sum_{i\in I_{1},j\in J_{2}}\omega(M_{i},N_{j})\cdot
d(M_{i},N_{j})=\sum_{i\in I_{1},j\in J_{2}}\omega(M_{i},N_{j})$ (since
$M_{i}\xrightarrow{\,{\beta_{2}}\,}$ and $N_{j}\mathrel{{\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\beta_{2}}}\,}}\makebox[0.0pt][r]{$\not$\hskip
8.61108pt}}{\\!}$ give $d(M_{i},N_{j})=1$)

  * •

$\sum_{i\in I_{2},j\in J_{1}}\omega(M_{i},N_{j})\cdot d(M_{i},N_{j})$

  * •

$\sum_{i\in I_{2},j\in J_{2}}\omega(M_{i},N_{j})\cdot d(M_{i},N_{j})$.

it is immediate that $\sum_{i\in I_{1},j\in J_{1}}\omega(M_{i},N_{j})\cdot
d(M_{i},N_{j})+\sum_{i\in I_{1},j\in
J_{2}}\omega(M_{i},N_{j})\leq\operatorname{\mathbf{K}}(d)(\Delta^{\prime},\Theta^{\prime})$.
Since we had
$\operatorname{\mathbf{K}}(d)(\Delta^{\prime},\Theta^{\prime})\leq d(M,N)$ we
can conclude that
$\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}}\omega^{\prime}(M^{\prime},N^{\prime})\cdot
d(M^{\prime},N^{\prime})\leq d(M,N)$, as required.

We are now ready to prove Theorem 6.

_Proof of Theorem 6._ Let $D$ be the set of all weak simulation quasimetrics.
Define the function $\operatorname{{\bf
d}}\colon\texttt{pTCWS}{}\times\texttt{pTCWS}{}\to[0,1]$ by

$\operatorname{{\bf d}}(M,N)=\inf\left\\{\sum_{i=1}^{n}\inf_{d\in
D}d(O_{i},O_{i+1})\mid
n\in\mathbb{N}^{+},O_{1}=M,O_{n+1}=N,O_{i}\in\texttt{pTCWS}{}\right\\}$

for all $M,N\in\texttt{pTCWS}{}$. It is immediate that for all $d\in D$ we
have $\operatorname{{\bf d}}(M,N)\leq d(M,N)$ for all
$M,N\in\texttt{pTCWS}{}$. Therefore, to derive the thesis it is enough to show
to $\operatorname{{\bf d}}$ is a weak simulation quasimetric. We start with
showing that $\operatorname{{\bf d}}$ is a pseudoquasimetric. The property
$\operatorname{{\bf d}}(M,M)=0$ follows directly by $\operatorname{{\bf
d}}(M,M)\leq d(M,M)$ and $d(M,M)=0$ for all $d\in D$. Then we show the
triangular inequality $\operatorname{{\bf d}}(M,N)\leq\operatorname{{\bf
d}}(M,O)+\operatorname{{\bf d}}(O,N)$ by
$\begin{array}[]{rl}&\operatorname{{\bf d}}(M,N)\\\\[3.0pt]
=&\inf\\{\sum_{i=1}^{n}\inf_{d\in D}d(O_{i},O_{i+1})\mid
n\in\mathbb{N}^{+},O_{1}=M,O_{n+1}=N,O_{i}\in\texttt{pTCWS}{}\\}\\\\[3.0pt]
\leq&\inf\\{\sum_{i=1}^{n}\inf_{d\in D}d(O_{i},O_{i+1})\mid
n\in\mathbb{N}^{+},O_{1}=M,O_{n+1}=N,O_{i}\in\texttt{pTCWS}{}\\}\end{array}$
$\begin{array}[]{rl}=&\inf\\{\sum_{i=1}^{n}\inf_{d\in D}d(O_{i},O_{i+1})\mid
n\in\mathbb{N}^{+},O_{1}=M,O_{n+1}=O,O{\in}\\{O_{2},..,O_{n}\\},O_{i}\in\texttt{pTCWS}{}\\}\\\\[3.0pt]
&+\\\\[3.0pt] &\inf\\{\sum_{i=1}^{n}\inf_{d\in D}d(O_{i},O_{i+1})\mid
n\in\mathbb{N}^{+},O_{1}=O,O{\in}\\{O_{2},..,O_{n}\\},O_{n+1}=N,O_{i}\in\texttt{pTCWS}{}\\}\\\\[3.0pt]
=&\operatorname{{\bf d}}(M,O)+\operatorname{{\bf d}}(O,N).\end{array}$
We conclude that the pseudometric property of $\operatorname{{\bf d}}$ is
given. It remains to prove that whenever $\operatorname{{\bf d}}(M,N)<1$ and
$M\xrightarrow{\,{\alpha}\,}\Delta$ there is a transition $N\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Theta$ with
$\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Delta,\Theta+(1-\mid\\!\\!{\Theta}\\!\\!\mid)\overline{\mathsf{Dead}})\leq\operatorname{{\bf
d}}(M,N)$. By the finite branching property, it is enough to prove that, fixed
$O_{1}=M$ and $O_{n+1}=N$ and given arbitrary networks
$O_{2},\ldots,O_{n}\in\texttt{pTCWS}{}$ and arbitrary weak simulation
quasimetrics $d_{1},\ldots,d_{n}\in D$ such that
$\sum_{i=1}^{n}d_{i}(O_{i},O_{i+1})\leq 1$, then
$M\xrightarrow{\,{\alpha}\,}\Delta$ implies that there is a transition
$N\ext@arrow 0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Theta$ with
$\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Delta,\Theta+(1-\mid\\!\\!{\Theta}\\!\\!\mid)\overline{\mathsf{Dead}})\leq\sum_{i=1}^{n}d_{i}(O_{i},O_{i+1})$.
Assume such a $M\xrightarrow{\,{\alpha}\,}\Delta$, and let
$\Delta_{1}=\Delta$. For $i=1,\ldots,n$ we get $O_{i}\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Delta_{i}$ with
$\operatorname{\mathbf{K}}(d_{i})(\Delta_{i}+(1-\mid\\!\\!{\Delta_{i}}\\!\\!\mid)\overline{\mathsf{Dead}},\Delta_{i+1}+(1-\mid\\!\\!{\Delta_{i+1}}\\!\\!\mid)\overline{\mathsf{Dead}})\leq
d_{i}(O_{i},O_{i+1})$, by exploiting Lemma 25 in cases $i=2,\ldots,n$. This
allows us to infer
$\begin{array}[]{rlr}&\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Delta_{1},\Delta_{n+1}+(1-\mid\\!\\!{\Delta_{n+1}}\\!\\!\mid)\overline{\mathsf{Dead}})\\\\[3.0pt]
\leq&\sum_{i=1}^{n}\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Delta_{i}+(1-\mid\\!\\!{\Delta_{i}}\\!\\!\mid)\overline{\mathsf{Dead}},\Delta_{i+1}+(1-\mid\\!\\!{\Delta_{i+1}}\\!\\!\mid)\overline{\mathsf{Dead}})\\\\[3.0pt]
\leq&\sum_{i=1}^{n}\operatorname{\mathbf{K}}(d_{i})(\Delta_{i}+(1-\mid\\!\\!{\Delta_{i}}\\!\\!\mid)\overline{\mathsf{Dead}},\Delta_{i+1}+(1-\mid\\!\\!{\Delta_{i+1}}\\!\\!\mid)\overline{\mathsf{Dead}})\\\\[3.0pt]
\leq&\sum_{i=1}^{n}d_{i}(O_{i},O_{i+1})\end{array}$
thus confirming that $\Delta_{n+1}$ is the distribution $\Theta$ we were
looking for, where the first step follows by the triangular inequality for
$\operatorname{\mathbf{K}}(\operatorname{{\bf d}})$, which is a
pseudoquasimetric by Proposition 24 and the fact that we have already proved
that $\operatorname{{\bf d}}$ is a pseudoquasimetric, and the second step
follows by the monotonicity of $\operatorname{\mathbf{K}}$ and the fact that
we have proved that $\operatorname{{\bf d}}(M^{\prime},N^{\prime})\leq
d_{i}(M^{\prime},N^{\prime})$ for all
$M^{\prime},N^{\prime}\in\texttt{pTCWS}{}$. ∎

_Proof of Proposition 8_. We have to prove that any transition
$N\xrightarrow{\,{\alpha}\,}\Theta$ is simulated by a suitable weak transition
$M\ext@arrow 0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Theta^{\prime}$ with
$\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Theta,\Theta^{\prime}+(1-\mid\\!\\!{\Theta^{\prime}}\\!\\!\mid)\overline{\mathsf{Dead}})\leq
q$. Assume an arbitrary transition $N\xrightarrow{\,{\alpha}\,}\Theta$. From
$N\xrightarrow{\,{\alpha}\,}\Theta$ and the hypothesis $M\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}(1-q)\overline{N}+q\Delta$, we get
$M\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}(1-q)\Theta+q\Delta^{\prime}$, for a
suitable sub-distribution $\Delta^{\prime}$ such that $\Delta\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Delta^{\prime}$. To conclude we
have to prove that $\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Theta,(1-q)\Theta+q\Delta^{\prime}+q(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid)\overline{\mathsf{Dead}})\leq
q$, namely $(1-q)\Theta+q\Delta^{\prime}$ is the sub-distribution
$\Theta^{\prime}$ we were looking for. Let
$\omega\colon\texttt{pTCWS}{}\times\texttt{pTCWS}{}\to[0,1]$ be the function
defined by

  * •

$\omega(M^{\prime},M^{\prime})=(1-q)\cdot\Theta(M^{\prime})+q\cdot\Theta(M^{\prime})\cdot\Delta^{\prime}(M^{\prime})+q\cdot(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid)\cdot\Theta(M^{\prime})\cdot\overline{\mathsf{Dead}}(M^{\prime})$,
and

  * •

$\omega(M^{\prime},N^{\prime})=q\cdot\Theta(M^{\prime})\cdot\Delta^{\prime}(N^{\prime})+q\cdot(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid)\cdot\Theta(M^{\prime})\cdot\overline{\mathsf{Dead}}(N^{\prime})$,
for $M^{\prime}\neq N^{\prime}$.

We have to prove that:

  1. (1)

$\omega\in\Omega(\Theta,(1-q)\Theta+q\Delta^{\prime}+q(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid)\overline{\mathsf{Dead}}))$,
and

  2. (2)

$\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}}\omega(M^{\prime},N^{\prime})\cdot\operatorname{{\bf
d}}(M^{\prime},N^{\prime})\leq q$.

To prove (1) we show that the left marginal of $\omega$ is $\Theta$ by
$\begin{array}[]{rl}&\sum_{N^{\prime}\in\texttt{pTCWS}}\omega(M^{\prime},N^{\prime})\\\\[2.0pt]
=&\omega(M^{\prime},M^{\prime})+\sum_{N^{\prime}\neq
M^{\prime}}\omega(M^{\prime},N^{\prime})\\\\[2.0pt]
=&(1-q)\cdot\Theta(M^{\prime})+q\cdot\Theta(M^{\prime})\cdot\Delta^{\prime}(M^{\prime})+q\cdot(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid)\cdot\Theta(M^{\prime})\cdot\overline{\mathsf{Dead}}(M^{\prime})\>+\\\
&\sum_{N^{\prime}\neq
M^{\prime}}q\cdot\Theta(M^{\prime})\cdot\Delta^{\prime}(N^{\prime})+q\cdot(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid)\cdot\Theta(M^{\prime})\cdot\overline{\mathsf{Dead}}(N^{\prime})\\\\[2.0pt]
=&(1-q)\cdot\Theta(M^{\prime})+\sum_{N^{\prime}\in\texttt{pTCWS}{}}q\cdot\Theta(M^{\prime})\cdot\Delta^{\prime}(N^{\prime})\>+\\\
&\sum_{N^{\prime}\in\texttt{pTCWS}{}}q\cdot(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid)\cdot\Theta(M^{\prime})\cdot\overline{\mathsf{Dead}}(N^{\prime})\end{array}$
$\begin{array}[]{rl}=&(1-q)\cdot\Theta(M^{\prime})+q\cdot\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid\cdot\Theta(M^{\prime})+q\cdot(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid)\cdot\Theta(M^{\prime})\\\\[2.0pt]
=&\Theta(M^{\prime})\end{array}$
the proof that the right marginal is
$(1-q)\Theta+q\Delta^{\prime}+q(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid)\overline{\mathsf{Dead}}$
being analogous. We get (2) by
$\begin{array}[]{rl}&\sum_{M^{\prime},N^{\prime}}\omega(M^{\prime},N^{\prime})\cdot\operatorname{{\bf
d}}(M^{\prime},N^{\prime})\\\\[2.0pt]
=&\sum_{M^{\prime},M^{\prime}}\omega(M^{\prime},M^{\prime})\cdot\operatorname{{\bf
d}}(M^{\prime},M^{\prime})+\sum_{M^{\prime}\neq
N^{\prime}}\omega(M^{\prime},N^{\prime})\cdot\operatorname{{\bf
d}}(M^{\prime},N^{\prime})\\\\[2.0pt] =&\sum_{M^{\prime}\neq
N^{\prime}}\omega(M^{\prime},N^{\prime})\cdot\operatorname{{\bf
d}}(M^{\prime},N^{\prime})\\\\[2.0pt] =&\sum_{M^{\prime}\neq
N^{\prime}}(q\cdot\Theta(M^{\prime})\cdot\Delta^{\prime}(N^{\prime})+q\cdot(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid)\cdot\Theta(M^{\prime})\cdot\overline{\mathsf{Dead}}(N^{\prime}))\cdot\operatorname{{\bf
d}}(M^{\prime},N^{\prime})\\\\[2.0pt]
\leq&q\cdot\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid+q\cdot(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid)\\\\[2.0pt]
\leq&q\end{array}$
with the second equality by $\operatorname{{\bf d}}(M^{\prime},M^{\prime})=0$
and the first inequality by $\operatorname{{\bf d}}(M^{\prime},N^{\prime})\leq
1$, the fact that $\sum_{M^{\prime}\in\texttt{pTCWS}{}}\Theta(M^{\prime})=1$
and
$\sum_{N^{\prime}\in\texttt{pTCWS}{}}\overline{\mathsf{Dead}}(N^{\prime})=1$.
∎

_Proof of Proposition 9._ Assume a transition
$M\xrightarrow{\,{\alpha}\,}\Theta$. By $M\mathrel{\sqsubseteq_{p}}N$ there is
a transition $N\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Theta^{\prime}$ with
$\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Theta,\Theta^{\prime}+(1-\mid\\!\\!{\Theta^{\prime}}\\!\\!\mid)\overline{\mathsf{Dead}})\leq
p$. By the hypothesis $O\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}(1-q)\overline{N}+q\Delta$ we get
$O\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}(1-q)\Theta^{\prime}+q\Delta^{\prime}$,
for a suitable distribution $\Delta^{\prime}$ such that $\Delta\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Delta^{\prime}$. To conclude the
proof we should show that

$\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Theta,(1-q)\Theta^{\prime}+q\Delta^{\prime}+((1-q)(1-\mid\\!\\!{\Theta^{\prime}}\\!\\!\mid)+q(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid))\overline{\mathsf{Dead}})\leq
p(1-q)+q.$

Let us consider
$\omega\in\Omega(\Theta,\Theta^{\prime}+(1-\mid\\!\\!{\Theta^{\prime}}\\!\\!\mid)\overline{\mathsf{Dead}})$
as one of the optimal matching realising
$\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Theta,\Theta^{\prime}+(1-\mid\\!\\!{\Theta^{\prime}}\\!\\!\mid)\overline{\mathsf{Dead}})$.
Define the function
$\omega^{\prime}\colon\texttt{pTCWS}{}\times\texttt{pTCWS}{}\to[0,1]$ by

$\omega^{\prime}(M^{\prime},N^{\prime})=(1-q)\cdot\omega(M^{\prime},N^{\prime})+q\cdot\Theta(M^{\prime})\cdot\Delta^{\prime}(N^{\prime})+q\cdot(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid)\cdot\Theta(M^{\prime})\cdot\overline{\mathsf{Dead}}(N^{\prime})$

for all $M^{\prime},N^{\prime}\in\texttt{pTCWS}{}$. We have to prove that

  1. (1)

$\omega^{\prime}\in\Omega(\Theta,(1-q)\cdot\Theta^{\prime}+q\Delta^{\prime}+((1-q)(1-\mid\\!\\!{\Theta^{\prime}}\\!\\!\mid)+q(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid))\overline{\mathsf{Dead}})$,
and

  2. (2)

$\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}}\omega^{\prime}(M^{\prime},N^{\prime})\cdot\operatorname{{\bf
d}}(M^{\prime},N^{\prime})\leq p(1-q)+q$.

To prove (1) we show that the left marginal of $\omega^{\prime}$ is $\Theta$
by
$\begin{array}[]{rl}&\sum_{N^{\prime}\in\texttt{pTCWS}}\omega^{\prime}(M^{\prime},N^{\prime})\\\\[2.0pt]
=&(1-q)\cdot\sum_{N^{\prime}\in\texttt{pTCWS}}\omega(M^{\prime},N^{\prime})+q\cdot\sum_{N^{\prime}\in\texttt{pTCWS}}\Theta(M^{\prime})\cdot\Delta^{\prime}(N^{\prime})+\\\
&q\cdot\sum_{N^{\prime}\in\texttt{pTCWS}{}}(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid)\cdot\Theta(M^{\prime})\cdot\overline{\mathsf{Dead}}(N^{\prime})\\\\[2.0pt]
=&(1-q)\cdot\Theta(M^{\prime})+q\cdot\Theta(M^{\prime})\cdot|\Delta^{\prime}|+q\cdot\Theta(M^{\prime})\cdot(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid)\\\\[2.0pt]
=&\Theta(M^{\prime})\end{array}$
with the second equality by the fact that $\omega$ is a matching in
$\Omega(\Theta,\Theta^{\prime}+(1-\mid\\!\\!{\Theta^{\prime}}\\!\\!\mid)\overline{\mathsf{Dead}}))$
and by the equalities
$\sum_{N^{\prime}\in\texttt{pTCWS}{}}\Delta^{\prime}(N^{\prime})=\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid$
and
$\sum_{N^{\prime}\in\texttt{pTCWS}{}}\overline{\mathsf{Dead}}(N^{\prime})=1$.
The proof that the right marginal is
$(1-q)\Theta^{\prime}+q\Delta^{\prime}+((1-q)(1-\mid\\!\\!{\Theta^{\prime}}\\!\\!\mid)+q(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid))\overline{\mathsf{Dead}}$
is analogous. We get (2) by the following chain of inequalities:

$\begin{array}[]{rl}&\sum_{M^{\prime},N^{\prime}}\omega^{\prime}(M^{\prime},N^{\prime})\cdot\operatorname{{\bf
d}}(M^{\prime},N^{\prime})\\\\[2.0pt]
=&(1{-}q)\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}}\omega(M^{\prime},N^{\prime})\cdot\operatorname{{\bf
d}}(M^{\prime},N^{\prime})+q\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}}\Theta(M^{\prime})\cdot\Delta^{\prime}(N^{\prime})\cdot\operatorname{{\bf
d}}(M^{\prime},N^{\prime})\\\
+&q\cdot\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}{}}(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid)\cdot\Theta(M^{\prime})\cdot\overline{\mathsf{Dead}}(N^{\prime})\cdot\operatorname{{\bf
d}}(M^{\prime},N^{\prime})\\\\[2.0pt]
\leq&(1-q)\cdot\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Theta,\Theta^{\prime}+(1-\mid\\!\\!{\Theta^{\prime}}\\!\\!\mid)\overline{\mathsf{Dead}})+q\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid+q(1-\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid)\\\\[2.0pt]
\leq&p(1-q)+q\end{array}$

with the first inequality deriving by the fact that $\omega$ is a matching
realising

$\displaystyle\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Theta,\Theta^{\prime}+(1-\mid\\!\\!{\Theta^{\prime}}\\!\\!\mid)\overline{\mathsf{Dead}}),\operatorname{{\bf
d}}(M^{\prime},N^{\prime})\leq 1$

and the equalities

$\displaystyle\sum_{M^{\prime}\in\texttt{pTCWS}{}}\Theta(M^{\prime})=1,\qquad\sum_{N^{\prime}\in\texttt{pTCWS}{}}\Delta^{\prime}(N^{\prime})=\mid\\!\\!{\Delta^{\prime}}\\!\\!\mid,\quad\text{
and
}\sum_{N^{\prime}\in\texttt{pTCWS}{}}\overline{\mathsf{Dead}}(N^{\prime})=1.$
∎

_Proof of Proposition 10._ Assume a transition
$M\xrightarrow{\,{\alpha}\,}\Theta$. By $M\mathrel{\sqsubseteq_{p}}N$ there is
a transition $N\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Theta^{\prime}$ with
$\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Theta,\Theta^{\prime}+(1-\mid\\!\\!{\Theta^{\prime}}\\!\\!\mid)\overline{\mathsf{Dead}})\leq
p$. By the hypothesis that $N$ can perform only the transition
$N\xrightarrow{\,{\sigma}\,}\overline{N^{\prime}}$ for a network $N^{\prime}$
such that
$N^{\prime}\mathrel{{\xrightarrow{\,{\tau}\,}}\makebox[0.0pt][r]{$\not$\hskip
8.61108pt}}{\\!}$, we are sure that $\alpha=\sigma$ and
$\Theta^{\prime}=\overline{N^{\prime}}$. By the hypothesis
$O\xrightarrow{\,{\sigma}\,}O^{\prime}\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}(1-q)\overline{N^{\prime}}+q\Delta$ we
get $O\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}(1-q)\Theta^{\prime}+q\Delta^{\prime}$,
for a suitable distribution $\Delta^{\prime}$ such that $\Delta\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Delta^{\prime}$. To conclude, it
remains to prove $\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Theta,(1-q)\Theta^{\prime}+q\Delta^{\prime}+((1-q)(1-\mid\\!\\!{\Theta^{\prime}}\\!\\!\mid)+q(1-|\Delta^{\prime}|))\overline{\mathsf{Dead}})\leq
p(1-q)+q$, which follows as in the proof of Lemma 9. ∎

To prove Theorem 12 we give the following preliminary result.

######  Lemma 26.

$M\mathrel{\sqsubseteq_{p}}N$ entails $M|O\mathrel{\sqsubseteq_{p}}N|O$ and
$O|M\mathrel{\sqsubseteq_{p}}O|N$.

######  Proof A.3.

We show that $M\mathrel{\sqsubseteq_{p}}N$ entails
$M|O\mathrel{\sqsubseteq_{p}}N|O$, the property
$O|M\mathrel{\sqsubseteq_{p}}O|N$ can be derived analogously. It is enough to
prove that $\operatorname{{\bf d}}(M,N)=p$ entails $\operatorname{{\bf
d}}(M|O,N|O)\leq p$. Let us define the function
$d^{\prime}\colon\texttt{pTCWS}{}\times\texttt{pTCWS}{}\to[0,1]$ by
$d^{\prime}(M\mid O,N\mid O)=\operatorname{{\bf d}}(M,N)$ for all
$M,N,O\in\texttt{pTCWS}{}$. To prove the thesis it is enough to show that
$d^{\prime}$ is a weak simulation quasimetric. In fact, since
$\operatorname{{\bf d}}$ is the minimal weak simulation quasimetric, this
implies $\operatorname{{\bf d}}\sqsubseteq d^{\prime}$, thus giving
$\operatorname{{\bf d}}(M\mid O,N\mid O)\leq d^{\prime}(M\mid O,N\mid
O)=\operatorname{{\bf d}}(M,N)$. Hence we need to show that $d^{\prime}(M\mid
O,N\mid O)<1$ and $M\mid O\xrightarrow{\,{\alpha}\,}\Delta$ implies that there
is a transition $N\mid O\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Theta$ with
$\operatorname{\mathbf{K}}(d^{\prime})(\Delta,\Theta+(1-\mid\\!\\!{\Theta}\\!\\!\mid)\overline{\mathsf{Dead}})\leq
d^{\prime}(M\mid O,N\mid O)$. We distinguish three cases.

  * •

$M\mid O\xrightarrow{\,{\alpha}\,}\Delta$ follows by
$M\xrightarrow{\,{\alpha}\,}\Delta^{\prime}$ and
$\Delta=\Delta^{\prime}\mid\overline{O}$ by applying rule (TauPar)

  * •

$M\mid O\xrightarrow{\,{\alpha}\,}\Delta$ follows by
$O\xrightarrow{\,{\alpha}\,}\Delta^{\prime}$ and
$\Delta=\overline{M}\mid\Delta^{\prime}$ by applying rule (TauPar)

  * •

$M\mid O\xrightarrow{\,{\alpha}\,}\Delta$ follows by
$M\xrightarrow{\,{\alpha_{1}}\,}\Delta_{1}$ and
$O\xrightarrow{\,{\alpha_{2}}\,}\Delta_{2}$ and
$\Delta=\Delta_{1}\mid\Delta_{2}$ by applying one of the rules (RcvPar),
(Bcast), ($\sigma$-Par).

We consider the first case, the others are analogous. Since $M\mid
O\xrightarrow{\,{\alpha}\,}\Delta$ is obtained by applying rule (TauPar), we
have $\alpha=\tau$. By $d^{\prime}(M\mid O,N\mid O)<1$ we get
$\operatorname{{\bf d}}(M,N)<1$, which, together with
$M\xrightarrow{\,{\alpha}\,}\Delta^{\prime}$ gives $N\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Theta^{\prime}$, with
$\mid\\!\\!{\Theta^{\prime}}\\!\\!\mid=1$ following by $\alpha=\tau$, and
$\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Delta^{\prime},\Theta^{\prime})\leq\operatorname{{\bf d}}(M,N)$. By
applying the rule (TauPar) possibly several times we can derive $N\mid
O\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Theta^{\prime}\mid\overline{O}$. We
have now to show that
$\operatorname{\mathbf{K}}(d^{\prime})(\Delta^{\prime}\mid\overline{O},\Theta^{\prime}\mid\overline{O})\leq
d^{\prime}(M\mid O,N\mid O)$, namely that $\Theta^{\prime}\mid\overline{O}$ is
the distribution $\Theta$ we were looking for. To this end, we take one of the
optimal matchings $\omega\in\Omega(\Delta^{\prime},\Theta^{\prime})$ realising
$\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Delta^{\prime},\Theta^{\prime})$ and we define
$\omega^{\prime}\colon\texttt{pTCWS}{}\times\texttt{pTCWS}{}\to[0,1]$ by
$\omega^{\prime}(M^{\prime}\mid O,N^{\prime}\mid
O)=\omega(M^{\prime},N^{\prime})$ and
$\omega^{\prime}(M^{\prime\prime},N^{\prime\prime})=0$ whenever
$M^{\prime\prime}$ is not of the form $M^{\prime}\mid O$ or $N^{\prime\prime}$
is not of the form $N^{\prime}\mid O$. Thus, we prove:

  1. (1)

$\omega^{\prime}$ is a matching in
$\Omega(\Delta^{\prime}\mid\overline{O},\Theta^{\prime}\mid\overline{O})$, and

  2. (2)

$\sum_{M^{\prime\prime},N^{\prime\prime}\in\texttt{pTCWS}{}}d^{\prime}(M^{\prime\prime},N^{\prime\prime})\cdot\omega^{\prime}(M^{\prime\prime},N^{\prime\prime})\leq
d^{\prime}(M^{\prime}\mid O,N^{\prime}\mid O)$.

To show (1) we prove that the left marginal of $\omega^{\prime}$ is
$\Delta^{\prime}\mid\overline{O}$ by
$\begin{array}[]{rl}&\sum_{N^{\prime\prime}\in\texttt{pTCWS}{}}\omega^{\prime}(M^{\prime}\mid
O,N^{\prime\prime})\\\\[2.0pt]
=&\sum_{N^{\prime}\in\texttt{pTCWS}{}}\omega^{\prime}(M^{\prime}\mid
O,N^{\prime}\mid O)\\\\[2.0pt]
=&\sum_{N^{\prime}\in\texttt{pTCWS}{}}\omega(M^{\prime},N^{\prime})\\\\[2.0pt]
=&\Delta^{\prime}(M^{\prime})\\\\[2.0pt]
=&(\Delta^{\prime}\mid\overline{O})(M^{\prime}\mid O)\end{array}\\\ $ with the
second last equality by $\omega\in\Omega(\Delta^{\prime},\Theta^{\prime})$.
The proof that the right marginal of $\omega^{\prime}$ is
$\Theta^{\prime}\mid\overline{O^{\prime}}$ can be proved analogously. Then,
(2) follows by
$\begin{array}[]{rl}&\sum_{M^{\prime\prime},N^{\prime\prime}\in\texttt{pTCWS}{}}d^{\prime}(M^{\prime\prime},N^{\prime\prime})\cdot\omega^{\prime}(M^{\prime\prime},N^{\prime\prime})\\\\[2.0pt]
=&\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}{}}d^{\prime}(M^{\prime}\mid
O,N^{\prime}\mid O)\cdot\omega(M^{\prime},N^{\prime})\end{array}$
$\begin{array}[]{rl}=&\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}{}}\operatorname{{\bf
d}}(M^{\prime},N^{\prime})\cdot\omega(M^{\prime},N^{\prime})\\\\[2.0pt]
=&\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Delta^{\prime},\Theta^{\prime})\\\\[2.0pt] \leq&\operatorname{{\bf
d}}(M^{\prime},N^{\prime})\\\\[2.0pt] =&d^{\prime}(M^{\prime}\mid
O^{\prime},N^{\prime}\mid O^{\prime}).\end{array}\\\ $ with the second last
equality by the fact that $\omega$ is an optimal matching in
$\Omega(\Delta^{\prime},\Theta^{\prime})$.

_Proof of Theorem 12._ By Lemma 26 and transitivity (Proposition 7). ∎

_Proof of Proposition 13._ Assume that $M\xrightarrow{\,{\alpha}\,}\Delta$. By
the hypothesis
$M\sqsubseteq_{s_{i}}n{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\nu}|N$ we have
$n{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\nu}|N\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\Delta_{i}$ with
$\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Delta,\Delta_{i}+(1-\mid\\!\\!{\Delta_{i}}\\!\\!\mid)\overline{\mathsf{Dead}})\leq
s_{i}$. Hence we have $n{\boldsymbol{[}}\tau.\bigoplus_{i\in
I}p_{i}{:}P_{i}{\boldsymbol{]}}^{\nu}\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\alpha}}\,}\sum_{i\in I}p_{i}\Delta_{i}$. It
remains to show the inequality $\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Delta,\sum_{i\in I}p_{i}\Delta_{i}+(1-\mid\\!\\!{\sum_{i\in
I}p_{i}\Delta_{i}}\\!\\!\mid)\overline{\mathsf{Dead}})\leq\sum_{i\in
I}p_{i}s_{i}$. Assume that $\omega_{i}$ is one of the optimal matchings
realising $\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Delta,\Delta_{i}+(1-\mid\\!\\!{\Delta_{i}}\\!\\!\mid)\overline{\mathsf{Dead}})$.
Define the function $\omega\colon\texttt{pTCWS}{}\times\texttt{pTCWS}\to[0,1]$
by $\omega(M^{\prime},N^{\prime})=\sum_{i\in
I}p_{i}\omega_{i}(M^{\prime},N^{\prime})$ for all networks
$M^{\prime},N^{\prime}\in\texttt{pTCWS}{}$. To conclude that
$\operatorname{\mathbf{K}}(\operatorname{{\bf d}})(\Delta,\sum_{i\in
I}p_{i}\Delta_{i}+(1-\mid\\!\\!{\sum_{i\in
I}p_{i}\Delta_{i}}\\!\\!\mid)\overline{\mathsf{Dead}})\leq\sum_{i\in
I}p_{i}s_{i}$, we show that:

  1. (1)

$\omega$ is a matching in $\Omega(\Delta,\sum_{i\in
I}p_{i}\Delta_{i}+(1-\mid\\!\\!{\sum_{i\in
I}p_{i}\Delta_{i}}\\!\\!\mid)\overline{\mathsf{Dead}})$ and

  2. (2)

$\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}{}}\omega(M^{\prime},N^{\prime})\cdot
d(M^{\prime},N^{\prime})\leq\sum_{i\in I}p_{i}s_{i}$.

Let us start with (1). The proof that the left marginal of $\omega$ is
$\Delta$ is immediate. We show that the right marginal of $\omega$ is the
distribution $\sum_{i\in I}p_{i}\Delta_{i}+(1-\mid\\!\\!{\sum_{i\in
I}p_{i}\Delta_{i}}\\!\\!\mid)\overline{\mathsf{Dead}}$ by
$\begin{array}[]{rl}&\sum_{M^{\prime}\in\texttt{pTCWS}{}}\omega(M^{\prime},N^{\prime})\\\\[2.0pt]
=&\sum_{M^{\prime}\in\texttt{pTCWS}{}}\sum_{i\in
I}p_{i}\cdot\omega_{i}(M^{\prime},N^{\prime})\\\\[3.0pt] =&\sum_{i\in
I}p_{i}\sum_{M^{\prime}\in\texttt{pTCWS}{}}\omega_{i}(M^{\prime},N^{\prime})\\\\[3.0pt]
=&\sum_{i\in
I}p_{i}\cdot(\Delta_{i}+(1-\mid\\!\\!{\Delta_{i}}\\!\\!\mid)\overline{\mathsf{Dead}})(N^{\prime})\\\\[3.0pt]
=&(\sum_{i\in I}p_{i}\Delta_{i}+(1-\mid\\!\\!{\sum_{i\in
I}p_{i}\Delta_{i}}\\!\\!\mid)\overline{\mathsf{Dead}})(N^{\prime})\end{array}$
for each $N^{\prime}\in\texttt{pTCWS}{}$, with the second last equality by
$\omega_{i}\in\Omega(\Delta,\Delta_{i}+(1-\mid\\!\\!{\Delta_{i}}\\!\\!\mid)\overline{\mathsf{Dead}})$.
Consider now (2). We have
$\begin{array}[]{rl}&\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}{}}\omega(M^{\prime},N^{\prime})\cdot
d(M^{\prime},N^{\prime})\\\\[4.0pt]
=&\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}{}}\sum_{i\in
I}p_{i}\cdot\omega_{i}(M^{\prime},N^{\prime})\cdot
d(M^{\prime},N^{\prime})\\\\[4.0pt] =&\sum_{i\in
I}p_{i}\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}{}}\omega_{i}(M^{\prime},N^{\prime})\cdot
d(M^{\prime},N^{\prime})\\\ =&\sum_{i\in
I}p_{i}\cdot\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Delta,\Delta_{i}+(1-\mid\\!\\!{\Delta_{i}}\\!\\!\mid)\overline{\mathsf{Dead}})\\\\[4.0pt]
\leq&\sum_{i\in I}p_{i}\cdot s_{i}\end{array}$
with the last equality by the definition of $\omega_{i}$. This concludes the
proof. ∎

_Proof of Proposition 14._

  1. (1)

We proceed by induction over $k$. The base case $k=0$ is immediate. Consider
the inductive step $k+1$. We prove that any transition by
$n{\boldsymbol{[}}\sigma^{k+1}.\mathsf{nil}{\boldsymbol{]}}^{\mu}$ can be
simulated by $n{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\mu}$, the
symmetric case is analogous. The only transition by
$n{\boldsymbol{[}}\sigma^{k+1}.\mathsf{nil}{\boldsymbol{]}}^{\mu}$ is the
transition
$n{\boldsymbol{[}}\sigma^{k+1}.\mathsf{nil}{\boldsymbol{]}}^{\mu}\xrightarrow{\,{\sigma}\,}\overline{n{\boldsymbol{[}}\sigma^{k}.\mathsf{nil}{\boldsymbol{]}}^{\mu}}$
derived by rule (Sleep). By an application of rule ($\sigma$-nil) we get
$n{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\mu}\xrightarrow{\,{\sigma}\,}\overline{n{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\mu}}$.
We have $\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\overline{n{\boldsymbol{[}}\sigma^{k}.\mathsf{nil}{\boldsymbol{]}}^{\mu}},\overline{n{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\mu}})=\operatorname{{\bf
d}}(n{\boldsymbol{[}}\sigma^{k}.\mathsf{nil}{\boldsymbol{]}}^{\mu},n{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\mu})=0$,
where the last equality follows by the inductive hypothesis.

  2. (2)

By the fact that the only transitions that can be made by the two networks
$\prod_{i\in
I}m_{i}{\boldsymbol{[}}\sigma.P_{i}{\boldsymbol{]}}^{\nu_{m_{i}}}$ and
$\prod_{j\in
J}n_{j}{\boldsymbol{[}}\sigma.Q_{j}{\boldsymbol{]}}^{\mu_{n_{j}}}$ are
$\prod_{i\in
I}m_{i}{\boldsymbol{[}}\sigma.P_{i}{\boldsymbol{]}}^{\nu_{m_{i}}}\xrightarrow{\,{\sigma}\,}\overline{\prod_{i\in
I}m_{i}{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\nu_{m_{i}}}}$ and $\prod_{j\in
J}n_{j}{\boldsymbol{[}}\sigma.Q_{j}{\boldsymbol{]}}^{\mu_{n_{j}}}\xrightarrow{\,{\sigma}\,}\overline{\prod_{j\in
J}n_{j}{\boldsymbol{[}}Q_{j}{\boldsymbol{]}}^{\mu_{n_{j}}}}$ (see rules
(Sleep) and ($\sigma$-Par)).

  3. (3)

The hypothesis that nodes in $\mu$ do not send in the current time interval
imply that the only transition by $n{\boldsymbol{[}}\lfloor?(x){C}\rfloor
D{\boldsymbol{]}}^{\mu}$ is $n{\boldsymbol{[}}\lfloor?(x){C}\rfloor
D{\boldsymbol{]}}^{\mu}\xrightarrow{\,{\sigma}\,}\llbracket
n{\boldsymbol{[}}D{\boldsymbol{]}}^{\mu}\rrbracket$. On the other hand, the
only transition by $n{\boldsymbol{[}}\sigma.D{\boldsymbol{]}}^{\mu}$ is
$n{\boldsymbol{[}}\sigma.D{\boldsymbol{]}}^{\mu}\xrightarrow{\,{\sigma}\,}\llbracket
n{\boldsymbol{[}}D{\boldsymbol{]}}^{\nu}\rrbracket$. The thesis immediately
follows.

  4. (4)

This is an immediate corollary of item 3.

  5. (5)

By Proposition 8, it is enough to prove that

$m{\boldsymbol{[}}\tau.(!\langle
v\rangle\oplus_{p}\mathsf{nil}){\boldsymbol{]}}^{\nu}\>\;\big{|}\>\;\prod_{i\in
I}n_{i}{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\nu_{i}}\>\;\ext@arrow
0359\Rightarrowfill@{}{\,{\tau}\,}\>\;\overline{m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}\>\;\big{|}\>\;\prod_{i\in
I}n_{i}{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\nu_{i}}}$ (23)

By rule (Tau) we get

$m{\boldsymbol{[}}\tau.(!\langle
v\rangle\oplus_{p}\mathsf{nil}){\boldsymbol{]}}^{\nu}\>\;\xrightarrow{\,{\tau}\,}\>\;p\overline{m{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu}}+(1-p)\overline{m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}}.$

Hence, to prove Equation 23 it suffices to show that

$m{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu}\>\;big|\>\;\prod_{i\in
I}n_{i}{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\nu_{i}}\>\;\ext@arrow
0359\Rightarrowfill@{}{\,{\tau}\,}\>\;\overline{m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}\>\;\big{|}\>\;\prod_{i\in
I}n_{i}{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\nu_{i}}}$ (24)

To this end, first of all we note that, since for all $i\in I$
$P_{i}\neq\lfloor?(x){C}\rfloor D$, by rule (RcvEnb) we have that

$n_{i}{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\nu_{i}}\>\;\xrightarrow{\,{m?v}\,}\>\;\overline{n_{i}{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\nu_{i}}}$

and, then, by rule (RcvPar) we get $\prod_{i\in
I}n_{i}{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\nu_{i}}\xrightarrow{\,{m?v}\,}\prod_{i\in
I}\overline{n_{i}{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\nu_{i}}}$. By an
application of rule (Snd) we have $m{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu}\xrightarrow{\,{m!v{\triangleright}\nu}\,}\overline{m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu}}$.
Finally, we can apply rule (Bcast) to the last two transitions, and, since
$\nu=\bigcup_{i\in I}n_{i}$, by applying rule (Shh) we get the proof
obligation Equation 24. ∎

###  A.2. Proofs of results in Section 3

First we describe how we prove Theorem 15. Let $O$ denote the network
$O\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;N|\prod_{i\in
I}m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}|\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}$. We will prove that for some
distribution $\Delta$ there is a transition $M\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}(1-\prod_{i\in
I}(1-p_{i}))\cdot\overline{O}+\prod_{i\in I}(1-p_{i})\cdot\Delta$, then the
thesis follows by Proposition 8. The proof that $M\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}(1-\prod_{i\in
I}(1-p_{i}))\cdot\overline{O}+\prod_{i\in I}(1-p_{i})\cdot\Delta$ is divided
in two parts. First we prove that with probability $(1-\prod_{i\in
I}(1-p_{i}))$ the network $M$ can reach through a sequence of
$\tau$-transitions a network $O_{I_{1},I_{2},I_{3}}$ of the form
$O_{I_{1},I_{2},I_{3}}=N\big{|}\prod_{i\in I_{1}}m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}\big{|}\prod_{i\in
I_{2}}m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}\big{|}$
$\prod_{i\in I_{3}}m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}\big{|}\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}$, for $I_{1}\cup I_{2}\cup
I_{3}$ some partition of $I$. In particular, one of the $\tau$-transitions in
this sequence is derived via rule (ShhSnd) as a consequence of the broadcast
of the message by one of the senders. Then we prove that
$O_{I_{1},I_{2},I_{3}}\ext@arrow
0359\Rightarrowfill@{}{\,{\tau}\,}\overline{O}$. The first part of the proof
is given directly in the proof of Theorem 15, whereas
$O_{I_{1},I_{2},I_{3}}\ext@arrow
0359\Rightarrowfill@{}{\,{\tau}\,}\overline{O}$ is proved in the following
Lemma.

######  Lemma 27.

Assume the hypothesis of Theorem 15. Let $O$ denote the network

$\begin{array}[]{c}O\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;N\>\;\big{|}\>\;\prod_{i\in
I}m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}\end{array}$

and $O_{I_{1},I_{2},I_{3}}$ denote the network

$\begin{array}[]{c}N\;\big{|}\;\prod_{i\in I_{1}}m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}\;\big{|}\;\prod_{i\in
I_{2}}m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}\;\big{|}\;\prod_{i\in
I_{3}}m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}\;\big{|}\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}\end{array}$

for $I_{1}\cup I_{2}\cup I_{3}$ any partition of $I$. Then, we have
$O_{I_{1},I_{2},I_{3}}\ext@arrow
0359\Rightarrowfill@{}{\,{\tau}\,}\overline{O}$.

######  Proof A.4.

We reason by induction over $\mid\\!\\!{I_{1}\cup I_{3}}\\!\\!\mid$. The base
case $\mid\\!\\!{I_{1}\cup I_{3}}\\!\\!\mid=0$ is immediate, since $I_{2}=I$
and $O_{I_{1},I_{2},I_{3}}$ is the network $O$. Consider the inductive step
$\mid\\!\\!{I_{1}\cup I_{3}}\\!\\!\mid=n+1$. We distinguish two sub-cases,
depending whether $I_{3}$ is empty or not.

Case $I_{3}\neq\emptyset$. In this case the network $O_{I_{1},I_{2},I_{3}}$
can perform a $\tau$-step originated by a sender $m_{k}$ with $k\in I_{3}$.
Formally, by rule (Tau) we get

$\begin{array}[]{c}m_{k}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{k}}{\boldsymbol{]}}^{\nu_{m_{k}}}\xrightarrow{\,{\tau}\,}p_{k}\cdot\overline{m_{k}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{k}}}}+(1-p_{k})\cdot\overline{m_{k}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{k}}}}\end{array}$

and, then, by an application of rule (TauPar) we get

$\begin{array}[]{rcl}O_{I_{1},I_{2},I_{3}}&\xrightarrow{\,{\tau}\,}&\overline{N}\>\;\big{|}\>\;\prod_{i\in
I_{1}}\overline{m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}}\>\;\big{|}\>\;\prod_{i\in
I_{2}}\overline{m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}}\>\;\big{|}\;q\prod_{i\in
I_{3}\setminus{\\{k\\}}}\overline{m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}}\>\;\big{|}\\\\[4.0pt]
&&(p_{k}\cdot\overline{m_{k}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{k}}}}+(1-p_{k})\cdot\overline{m_{k}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{k}}}})\>\;\big{|}\>\;\prod_{j\in
J}\overline{n_{j}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}}\end{array}$

namely

$\begin{array}[]{c}O_{I_{1},I_{2},I_{3}}\>\;\xrightarrow{\,{\tau}\,}\>\;p_{k}\cdot\overline{O_{I_{1}\cup\\{k\\},I_{2},I_{3}\setminus\\{k\\}}}+(1-p_{k})\cdot\overline{O_{I_{1},I_{2}\cup\\{k\\},I_{3}\setminus\\{k\\}}}\end{array}$
(25)

Consider first the network $O_{I_{1}\cup\\{k\\},I_{2},I_{3}\setminus\\{k\\}}$
in Equation 25. A $\tau$-transition by network
$O_{I_{1}\cup\\{k\\},I_{2},I_{3}\setminus\\{k\\}}$ models the broadcasting of
$v$ by $m_{k}$ that is not received by any other node. In detail, by rule
(Snd) we get

$\begin{array}[]{c}m_{k}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{k}}}\xrightarrow{\,{m_{k}!v{\triangleright}\nu_{m_{k}}}\,}\overline{m_{k}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{k}}}}\,.\end{array}$

Then, by an application of rule (RcvEnb) we infer

$\begin{array}[]{c}N\xrightarrow{\,{m_{k}?v}\,}\overline{N}\end{array}$

which can be applied since by the hypothesis we know that no node in $N$ is
able to receive, by the same (RcvEnb) we get

$m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}\xrightarrow{\,{m_{k}?v}\,}\overline{m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}}$

for all $i\in I_{1}$,

$m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}\xrightarrow{\,{m_{k}?v}\,}\overline{m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}}$

for all $i\in I_{2}$, and

$m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}\xrightarrow{\,{m_{k}?v}\,}\overline{m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}}$

for all $i\in I_{3}\setminus\\{k\\}$, then again by rule (RcvEnb) we infer

$n_{j}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}\xrightarrow{\,{m_{k}?v}\,}\overline{n_{j}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}}$

for all $j\in J$, thus allowing us to apply rules (RcvPar) and (Bcast) and
obtain

$O_{I_{1}\cup\\{k\\},I_{2},I_{3}\setminus\\{k\\}}\xrightarrow{\,{m_{k}!v{\triangleright}\nu_{m_{k}}\setminus{\mathsf{nds}}(M)}\,}\overline{O_{I_{1},I_{2}\cup\\{k\\},I_{3}\setminus\\{k\\}}}$

from which we get

$\begin{array}[]{c}O_{I_{1}\cup\\{k\\},I_{2},I_{3}\setminus\\{k\\}}\xrightarrow{\,{\tau}\,}\overline{O_{I_{1},I_{2}\cup\\{k\\},I_{3}\setminus\\{k\\}}}\end{array}$
(26)

by rule (ShhSnd), which can be applied since by the hypothesis we know that
$\nu_{m_{k}}\subseteq{\mathsf{nds}}(M)$. Now, since $\mid\\!\\!{I_{1}\cup
I_{3}\setminus\\{k\\}}\\!\\!\mid=n$ we can apply the inductive hypothesis thus
obtaining $O_{I_{1},I_{2}\cup\\{k\\},I_{3}\setminus\\{k\\}}\ext@arrow
0359\Rightarrowfill@{}{\,{\tau}\,}\overline{O}$. Finally, by Equation 26 and
$O_{I_{1},I_{2}\cup\\{k\\},I_{3}\setminus\\{k\\}}\ext@arrow
0359\Rightarrowfill@{}{\,{\tau}\,}\overline{O}$ we get

$\begin{array}[]{c}O_{I_{1}\cup\\{k\\},I_{2},I_{3}\setminus\\{k\\}}\ext@arrow
0359\Rightarrowfill@{}{\,{\tau}\,}\overline{O}\end{array}$ (27)

Consider now the network $O_{I_{1},I_{2}\cup\\{k\\},I_{3}\setminus\\{k\\}}$ in
Equation 25. Since $\mid\\!\\!{I_{1}\cup I_{3}\setminus\\{k\\}}\\!\\!\mid=n$
we can apply the inductive hypothesis thus giving
$O_{I_{1},I_{2}\cup\\{k\\},I_{3}\setminus\\{k\\}}\ext@arrow
0359\Rightarrowfill@{}{\,{\tau}\,}\overline{O}$, which, together with Equation
25 and Equation 27, gives the thesis.

Case $I_{3}=\emptyset$. Since $\mid\\!\\!{I_{1}\cup I_{3}}\\!\\!\mid=n+1$, we
are sure that $I_{1}\neq\emptyset$. For some $k\in I_{1}$, we can reason as
above to infer that from a broadcasting transition by some $m_{k}$ with $k\in
I_{1}$ we get
$O_{I_{1},I_{2},I_{3}}\xrightarrow{\,{\tau}\,}\overline{O_{I_{1}\setminus\\{k\\},I_{2}\cup\\{k\\},I_{3}}}$,
then by the inductive hypothesis we derive
$O_{I_{1}\setminus\\{k\\},I_{2}\cup\\{k\\},I_{3}}\ext@arrow
0359\Rightarrowfill@{}{\,{\tau}\,}\overline{O}$, and, finally, from these two
transitions we conclude $O_{I_{1},I_{2},I_{3}}\ext@arrow
0359\Rightarrowfill@{}{\,{\tau}\,}\overline{O}$.

We are now ready to prove Theorem 15.

_Proof of Theorem 15._ As in the proof of Lemma 27, we use $O$ to denote the
network

$\begin{array}[]{c}O\;\stackrel{{\scriptstyle\operatorname{def}}}{{=}}\;N\>\;\big{|}\>\;\prod_{i\in
I}m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}\enspace.\end{array}$

We prove that $M\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}(1-\prod_{i\in
I}(1-p_{i}))\overline{O}+\prod_{i\in I}(1-p_{i})\Delta$, for some distribution
$\Delta$, then the thesis follows by Proposition 8.

By rule (Tau) we derive the following transition step for any sender $m_{i}$
with $i\in I$:

$m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}\xrightarrow{\,{\tau}\,}p_{i}\cdot\overline{m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}}+(1-p_{i})\cdot\overline{m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}}.$

The network $M$ can start by performing $k\leq\mid\\!\\!{I}\\!\\!\mid$
transitions labelled $\tau$, where each of these transitions comes from rule
(Tau) applied as above (namely is the initial $\tau$-step by some sender) and
(TauPar). Therefore, we can partition $I$ as $I=I^{\prime}\cup
I^{\prime\prime}$ such that

$\begin{array}[]{c}M\xrightarrow{\,{\tau}\,}\ldots\xrightarrow{\,{\tau}\,}\Theta\end{array}$

with

$\Theta\\!=\\!\overline{N}|\prod_{i\in
I^{\prime}}(p_{i}\overline{m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}}+(1{-}p_{i})\overline{m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}})|\prod_{i\in
I^{\prime\prime}}\overline{m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}}|\prod_{j\in
J}\overline{n_{j}{\boldsymbol{[}}\mathsf{fwd}_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}}$
(28)

and now we distinguish two cases.

The first case is that all senders $m_{i}$ with $i\in I$ reach the state
$m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}$ through
their initial $\tau$ transition, namely in the Equation 28 we have that
$I^{\prime}=I$, $I^{\prime\prime}=\emptyset$ and the network in the support of
$\Theta$ that is reached by $M$ is $N|\prod_{i\in
I}m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}|\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{fwd}_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}$.
Formally,

$\begin{array}[]{c}M\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}q\cdot(\overline{N}\>\;\big{|}\>\;\prod_{i\in
I}\overline{m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}}\>\;\big{|}\>\;\prod_{j\in
J}\overline{n_{j}{\boldsymbol{[}}\mathsf{fwd}_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}})\end{array}$
(29)

for $q=\prod_{i\in I}(1-p_{i})$. The network $N|\prod_{i\in
I}m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}|\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{fwd}_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}$ is
then unable to simulate $O$.

The second case is that at least one of the senders $m_{i}$ decides to
transmit and reaches the state $m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}$ through the $\tau$ transition, namely
there is a partition of $I^{\prime}=I_{1}^{\prime}\cup I_{2}^{\prime}$ such
that the state in the support of distribution $\Theta$ that is reached by $M$
has the form $N\big{|}\prod_{i\in I_{1}^{\prime}}m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}\big{|}\prod_{i\in
I_{2}^{\prime}}m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}\big{|}\prod_{i\in
I^{\prime\prime}}m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}\big{|}\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{fwd}_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}$
with $I^{\prime}_{1}\neq\emptyset$. Formally,

$M\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}q^{\prime}\cdot\Big{(}\overline{N}|\\!\prod_{i\in
I_{1}^{\prime}}\overline{m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}}|\\!\prod_{i\in
I_{2}^{\prime}}\overline{m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}}|\\!\prod_{i\in
I^{\prime\prime}}\overline{m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}}|\\!\prod_{j\in
J}\overline{n_{j}{\boldsymbol{[}}\mathsf{fwd}_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}}\Big{)}$
(30)

with $q^{\prime}=\prod_{i\in I^{\prime}_{1}}p_{i}\cdot\prod_{i\in
I^{\prime}_{2}}(1-p_{i})$. In this case, each of the nodes $m_{i}$ with $i\in
I^{\prime}_{1}$ can then broadcasts $v$. Indeed, by applying the rule (Snd) we
get $m_{h}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{h}}}\xrightarrow{\,{m_{h}!v{\triangleright}\nu_{m_{h}}}\,}\overline{m_{h}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{h}}}}$,
for some $h\in I^{\prime}_{1}$. Since by the hypothesis we know that all nodes
in $\nu_{m_{h}}\cap{\mathsf{nds}}(N)$ cannot receive in the current round,
and, analogously, all nodes $n_{i}$ with $i\in
I\setminus\\{h\\}=(I^{\prime}_{1}\cup I^{\prime}_{2}\cup
I^{\prime\prime})\setminus\\{h\\}$ cannot receive, by applying rule (RcvEnb)
we infer: (a) $N\xrightarrow{\,{m_{h}?v}\,}\overline{N}$, (b)
$m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}\xrightarrow{\,{m_{h}?v}\,}\overline{m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}}$, (c)
$m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}\xrightarrow{\,{m_{h}?v}\,}\overline{m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}}$.
Moreover, for all $j\in J$, by rule (Rcv) we infer

$n_{j}{\boldsymbol{[}}\mathsf{fwd}_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}\xrightarrow{\,{m_{h}?v}\,}\overline{n_{j}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}}$

thus implying that we can apply rules (RecPar) and (Bcast) and obtain

${\scriptsize\begin{array}[]{c}\displaystyle N\>\;\big{|}\>\;\prod_{i\in
I_{1}^{\prime}}m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}\>\;\big{|}\>\;\prod_{i\in
I_{2}^{\prime}}m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}\>\;\big{|}\>\;\prod_{i\in
I^{\prime\prime}}m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{fwd}_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}\\\\[8.0pt]
\xrightarrow{\,{m_{h}!v{\triangleright}\nu_{m_{h}}\setminus{\mathsf{nds}}(M)}\,}\\\\[8.0pt]
\displaystyle\overline{N}\>\;\big{|}\>\;\overline{m_{h}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{h}}}}\>\;\big{|}\prod_{i\in
I_{1}^{\prime}\setminus\\{h\\}}\overline{m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}}\>\;\big{|}\prod_{i\in
I_{2}^{\prime}}\overline{m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}}\>\;\big{|}\prod_{i\in
I^{\prime\prime}}\overline{m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}}\>\;\big{|}\prod_{j\in
J}\overline{n_{j}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}}\,.\end{array}}$

Since by the hypothesis we have $\nu_{m_{h}}\subseteq{\mathsf{nds}}(M)$, we
can apply rule (ShhSnd) to infer

${\scriptsize\begin{array}[]{c}\displaystyle N\>\;\big{|}\>\;\prod_{i\in
I_{1}^{\prime}}m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}\>\;\big{|}\>\;\prod_{i\in
I_{2}^{\prime}}m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}\>\;\big{|}\>\;\prod_{i\in
I^{\prime\prime}}m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{fwd}_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}\\\\[1.0pt]
\xrightarrow{\,{\tau}\,}\\\\[4.0pt]
\displaystyle\overline{N}\;\big{|}\;\overline{m_{h}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{h}}}}\;\big{|}\prod_{i\in
I_{1}^{\prime}\setminus\\{h\\}}\overline{m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}}\;\;\big{|}\prod_{i\in
I_{2}^{\prime}}\overline{m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}}\;\;\big{|}\prod_{i\in
I^{\prime\prime}}\overline{m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}}\;\;\big{|}\prod_{j\in
J}\overline{n_{j}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}}\end{array}}$ (31)

Let $O^{\prime}$ denote the only network in the support of the distribution in
Equation 31, i.e. $N\big{|}\prod_{i\in
I_{1}^{\prime}\setminus\\{h\\}}m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}\big{|}\prod_{i\in
I_{2}^{\prime}\cup\\{h\\}}m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}\big{|}\prod_{i\in
I^{\prime\prime}}m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}\big{|}\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{resnd}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}$. We observe that by adopting
the notation in Lemma 27, $O^{\prime}$ is in the form $O_{I_{1},I_{2},I_{3}}$
with $I_{1}=I^{\prime}_{1}\setminus\\{h\\}$,
$I_{2}=I^{\prime}_{2}\cup\\{h\\}$, $I_{3}=I^{\prime\prime}$. By Lemma 27 we
have $O^{\prime}\ext@arrow 0359\Rightarrowfill@{}{\,{\tau}\,}\overline{O}$.
This transition together with Equation 30 and Equation 31 gives $M\ext@arrow
0359\Rightarrowfill@{}{\,{{\tau}}\,}q^{\prime}\overline{O}$, where we remind
that $q^{\prime}=\prod_{i\in I^{\prime}_{1}}p_{i}\cdot\prod_{i\in
I^{\prime}_{2}}(1-p_{i})$. This transition is derived for any partition
$I^{\prime}_{1}\cup I^{\prime}_{2}\cup I^{\prime\prime}$ of $I$ with
$I^{\prime}_{1}\neq\emptyset$. Hence $M\ext@arrow
0359\Rightarrowfill@{}{\,{{\tau}}\,}(1-q)\overline{O}$, with $q$ the
probability value in Equation 29, which gives the thesis. ∎

_Proof of Theorem 16_. Let us denote with $M_{0}$, $M_{1}$ and $M_{2}$ the
following networks:

  * •

$M_{0}\>=\>N\>\;\big{|}\>\;m{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\lfloor?(x_{j}){P_{j}}\rfloor
Q_{j}{\boldsymbol{]}}^{\nu_{n_{j}}}$

  * •

$M_{1}\>=\>N\>\;\big{|}\>\;m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}{\\{^{v}\\!/\\!_{x_{j}}\\}}P_{j}{\boldsymbol{]}}^{\nu_{n_{j}}}$

  * •

$M_{2}\>=\>N\>\;\big{|}\>\;m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\lfloor?(x_{j}){P_{j}}\rfloor
Q_{j}{\boldsymbol{]}}^{\nu_{n_{j}}}$.

We recall that $\mathsf{snd}\langle v\rangle_{p}=\tau.(!\langle
v\rangle\oplus_{p}\mathsf{nil})$. Therefore we infer the thesis from
Proposition 13 if we show that $M\mathrel{\sqsubseteq_{s_{1}}}M_{0}$ and
$M\mathrel{\sqsubseteq_{s_{2}}}M_{2}$. The relation
$M\mathrel{\sqsubseteq_{s_{2}}}M_{2}$ holds by the hypothesis, hence we have
to prove $M\mathrel{\sqsubseteq_{s_{1}}}M_{0}$. To this purpose, it suffices
to prove $M_{1}\mathrel{\sqsubseteq_{0}}M_{0}$. In fact,
$M_{1}\mathrel{\sqsubseteq_{0}}M_{0}$ and the hypothesis
$M\mathrel{\sqsubseteq_{s_{1}}}M_{1}$ give, by transitivity (Proposition 7),
$M\mathrel{\sqsubseteq_{s_{1}}}M_{0}$. Finally, to prove
$M_{1}\mathrel{\sqsubseteq_{0}}M_{0}$, by Proposition 8 it is enough to prove
that $M_{0}\xrightarrow{\,{\tau}\,}\overline{M_{1}}$.

We show now that this transition can be derived. By rule (Snd) we get
$m{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m}}\xrightarrow{\,{m!v{\triangleright}\nu_{m}}\,}\overline{m{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m}}}$.
By an application of rule (Rcv) we get

$n_{j}{\boldsymbol{[}}\lfloor?(x_{j}){P_{j}}\rfloor
Q_{j}{\boldsymbol{]}}^{\nu_{n_{j}}}\>\;\xrightarrow{\,{m?v}\,}\>\;\overline{n_{j}{\boldsymbol{[}}{\\{^{v}\\!/\\!_{x_{j}}\\}}P_{j}{\boldsymbol{]}}^{\nu_{n_{j}}}}$

for all $j\in J$, where (Rcv) can be applied since we have $m\in\nu_{n_{j}}$
for all $j\in J$, which follows by the hypothesis $\\{n_{j}\mid j\in
J\\}\subseteq\nu_{m}$ and well-formedness. By rule (RcvEnb) we get
$N\xrightarrow{\,{m?v}\,}\overline{N}$, where (RcvEnb) can be applied since by
the hypothesis we know that all nodes in $\nu_{m}\cap{\mathsf{nds}}(N)$ are
not able to receive in the current instant of time. Summarising, we can apply
rule (Bcast) to obtain
$M_{0}\xrightarrow{\,{m!v{\triangleright}\nu_{m}\setminus{\mathsf{nds}}(M)}\,}\overline{M_{1}}$.
Then, since by the hypothesis we have $\nu_{m}\subseteq{\mathsf{nds}}(M)$, to
conclude the proof, we can apply rule (ShhSnd) to derive the transition
$M_{0}\xrightarrow{\,{\tau}\,}\overline{M_{1}}$. ∎

_Proof of Theorem 18._ Let us denote with $M_{0}$ and $M_{i}$, for $i\in I$,
the following networks:

  * •

$M_{0}\>=\>\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{j}}}\>\;\big{|}\>\;d{\boldsymbol{[}}\tau.\bigoplus_{i\in
I}p_{i}{:}P_{i}{\boldsymbol{]}}^{\nu_{d}}$

  * •

$M_{i}\>=\>\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{n_{j}}}\>\;\big{|}\>\;d{\boldsymbol{[}}P_{i}{\boldsymbol{]}}^{\nu_{d}}$.

The only admissible transition for the network $M_{0}$ is
$M_{0}\xrightarrow{\,{\tau}\,}\Delta=\sum_{i\in I}p_{i}\cdot\overline{M_{i}}$,
derived by rules (Tau) and (TauPar). By rules (Tau) and (TauPar), we can
derive the transition $M\mid m{\boldsymbol{[}}\tau.\bigoplus_{i\in
I}p_{i}{:}Q_{i}{\boldsymbol{]}}^{\nu_{m}}\xrightarrow{\,{\tau}\,}\Theta=\sum_{i\in
I}p_{i}\cdot\overline{M\mid
m{\boldsymbol{[}}Q_{i}{\boldsymbol{]}}^{\nu_{m}}}$. Since
$\mid\\!\\!{\Theta}\\!\\!\mid=1$, it is enough to prove that
$\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Delta,\Theta)\leq\sum_{i\in I}p_{i}s_{i}$. Define
$\omega\colon\texttt{pTCWS}{}\times\texttt{pTCWS}\to[0,1]$ by
$\omega(M_{i},M\;\big{|}\;m{\boldsymbol{[}}Q_{i}{\boldsymbol{]}}^{\nu_{m}})=p_{i}$,
for any $i\in I$, and $\omega(M^{\prime},N^{\prime})=0$ for all other pairs
$(M^{\prime},N^{\prime})$. To conclude
$\operatorname{\mathbf{K}}(\operatorname{{\bf
d}})(\Delta,\Theta)\leq\sum_{i\in I}p_{i}s_{i}$, it is enough to show that:

  1. (1)

the function $\omega$ is a matching in $\Omega(\Delta,\Theta)$ and

  2. (2)

$\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}{}}\omega(M^{\prime},N^{\prime})\cdot\operatorname{{\bf
d}}(M^{\prime},N^{\prime})\leq\sum_{i\in I}p_{i}s_{i}$.

The case (1) is immediate. Consider now (2). We have that
$\sum_{M^{\prime},N^{\prime}\in\texttt{pTCWS}{}}\omega(M^{\prime},N^{\prime})\cdot\operatorname{{\bf
d}}(M^{\prime},N^{\prime})=\sum_{i\in I}p_{i}\operatorname{{\bf
d}}(M_{i},M\;\big{|}\;m{\boldsymbol{[}}Q_{i}{\boldsymbol{]}}^{\nu_{m}})\leq\sum_{i\in
I}p_{i}s_{i}$ with the inequality by the hypothesis
$M_{i}\mathrel{\sqsubseteq_{s_{i}}}M\mid
n{\boldsymbol{[}}Q_{i}{\boldsymbol{]}}^{\nu_{n}}$. ∎

###  A.3. Proofs of results in Section 4

_Proof of Theorem 19._ Let $O\,=\,N\>\;\big{|}\>\;\prod_{i\in
I}m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{resndc}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}$. We prove that

$\begin{array}[]{c}M\ext@arrow
0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}(\sum_{i\in I}p_{i}\prod_{j\in
I{\setminus}\\{i\\}}(1-p_{j}))\overline{O}+(1-\sum_{i\in I}p_{i}\prod_{j\in
I{\setminus}\\{i\\}}(1-p_{j}))\Delta\end{array}$ (32)

for some distribution $\Delta$, then the proof follows by Proposition 8. By
rule (Tau) we get the following transition step for any sender $m_{i}$ with
$i\in I$:

$m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}\xrightarrow{\,{\tau}\,}p_{i}\cdot\overline{m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}}+(1-p_{i})\cdot\overline{m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}}.$

The network $M$ can start by performing $|\\!I\\!|$ transitions labelled
$\tau$, where each of these transitions comes from rule (Tau) applied as above
(namely is the initial $\tau$-step by some sender) and (TauPar). Therefore, we
have

$M\xrightarrow{\,{\tau}\,}\ldots\xrightarrow{\,{\tau}\,}\Theta$

with $\Theta=\overline{N}\;\big{|}\;\prod_{i\in
I}\big{(}p_{i}\cdot\overline{m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}}+(1-p_{i})\cdot\overline{m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}}\big{)}\;\big{|}\;\prod_{j\in
J}\overline{n_{j}{\boldsymbol{[}}\mathsf{fwd}_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}}$.
In detail, all elements in the support of $\Theta$ have the form

$\begin{array}[]{c}M_{I^{\prime},I^{\prime\prime}}=N\>\;\big{|}\>\;\prod_{i\in
I^{\prime}}m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}\>\;\big{|}\>\;\prod_{i\in
I^{\prime\prime}}m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}\>\;\big{|}\>\;\prod_{j\in
J}n_{j}{\boldsymbol{[}}\mathsf{fwd}_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}\end{array}$

for a suitable partition $I^{\prime}\cup I^{\prime\prime}=I$, and we have

$M\ext@arrow 0359\Rightarrowfill@{}{\,{\hat{\tau}}\,}\big{(}\prod_{i\in
I^{\prime}}p_{i}\prod_{j\in I^{\prime\prime}}(1-p_{j})\big{)}\cdot
M_{I^{\prime},I^{\prime\prime}}.$

Consider any $M_{I^{\prime},I^{\prime\prime}}$. If $I^{\prime}=\emptyset$ then
$M_{I^{\prime},I^{\prime\prime}}$ cannot simulate $N$ since no forwarder
process in node $n_{j}$ can receive any message. If $I^{\prime}\neq\emptyset$,
each of the $m_{i}$ with $i\in I^{\prime}$ can then broadcasts $v$. Indeed, by
applying the rule (Snd) we get

$m_{h}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{h}}}\>\;\xrightarrow{\,{m_{h}!v{\triangleright}\nu_{m_{h}}}\,}\>\;\overline{m_{h}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{h}}}}$

for some $h\in I^{\prime}$. Since by the hypothesis we know that all nodes in
$\nu_{m_{h}}\cap{\mathsf{nds}}(M^{\prime})$ cannot receive in the current
round, and, analogously, all nodes $n_{i}$ with $i\in
I\setminus\\{h\\}=(I^{\prime}\cup I^{\prime\prime})\setminus\\{h\\}$ cannot
receive, by applying rule (RcvEnb) we infer:  (i)
$N\xrightarrow{\,{m_{h}?v}\,}\overline{N}$;  (ii)
$m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}\xrightarrow{\,{m_{h}?v}\,}\overline{m_{i}{\boldsymbol{[}}\mathsf{snd}\langle
v\rangle_{p_{i}}{\boldsymbol{]}}^{\nu_{m_{i}}}}$;  (iii)
$m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}\xrightarrow{\,{m_{h}?v}\,}\overline{m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}}$.
Moreover, for all $j\in J$, by rule (Rcv) we infer:

$n_{j}{\boldsymbol{[}}\mathsf{fwd}_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}\>\;\xrightarrow{\,{m_{h}?v}\,}\>\;\overline{n_{j}{\boldsymbol{[}}\mathsf{resndc}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}}$

thus implying that we can apply rules (RcvPar) and (Bcast) and obtain

$\begin{array}[]{c}M_{I^{\prime},I^{\prime\prime}}\xrightarrow{\,{\alpha}\,}\overline{N}\>\;\big{|}\>\;\prod_{i\in
I^{\prime}\setminus\\{h\\}}\overline{m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}}\>\;\big{|}\>\;\prod_{i\in
I^{\prime\prime}\cup\\{h\\}}\overline{m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}}\>\;\big{|}\>\;\prod_{j\in
J}\overline{n_{j}{\boldsymbol{[}}\mathsf{resndc}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}}\end{array}$

with $\alpha=m_{h}!v{\triangleright}\nu_{m_{h}}\setminus{\mathsf{nds}}(M)$.
Since by the hypothesis we have $\nu_{m_{h}}\subseteq{\mathsf{nds}}(M)$, we
can apply rule (ShhSnd) to infer

$\begin{array}[]{c}M_{I^{\prime},I^{\prime\prime}}\xrightarrow{\,{\tau}\,}\overline{N}\>\;\big{|}\>\;\prod_{i\in
I^{\prime}\setminus\\{h\\}}\overline{m_{i}{\boldsymbol{[}}!\langle
v\rangle{\boldsymbol{]}}^{\nu_{m_{i}}}}\>\;\big{|}\>\;\prod_{i\in
I^{\prime\prime}\cup\\{h\\}}\overline{m_{i}{\boldsymbol{[}}\mathsf{nil}{\boldsymbol{]}}^{\nu_{m_{i}}}}\>\;\big{|}\>\;\prod_{j\in
J}\overline{n_{j}{\boldsymbol{[}}\mathsf{resndc}\langle
v\rangle_{q_{j}}{\boldsymbol{]}}^{\nu_{n_{j}}}}\enspace.\end{array}$

Now we note that if $I^{\prime}\setminus\\{h\\}=\emptyset$ then the target of
this transition is the network $O$ and we can derive

$\begin{array}[]{c}M\>\;\ext@arrow
0359\Rightarrowfill@{}{\,{{\tau}}\,}\>\;p_{i}\prod_{j\in
I\setminus\\{i\\}}(1-p_{j})\overline{O}\end{array}$ (33)

Otherwise, if $I^{\prime}\setminus\\{h\\}\neq\emptyset$ then the network
$M_{I^{\prime},I^{\prime\prime}}$ cannot simulate $O$ since the nodes
$\mathsf{resndc}\langle v\rangle_{q_{j}}$ fail in the present round since they
receive from some sender $m_{i}$ with $i\in I^{\prime}\setminus\\{h\\}$.
Overall, we have Equation 33 for all $i\in I$, from which the proof obligation
in Equation 32 follows. ∎