with:

$$ \forall l \in L_Q v_{kl} = v_{(n'_k)l} \wedge v'_{kl} = v_{(n'_k)l} $$

$$ \alpha_k = \alpha'_{n_k} \{ \bigcirc_{j=n_k-1}^{n'_k} \mathrm{Post}''_j \} $$

$$ \gamma_{kj}^{j \in J \cap \mathrm{Holes}(Q)} = \bigoplus_{i=n'_k}^{(n_k-1)} (\beta_{ij}^{j \in J \cap \mathrm{Holes}(Q)} \{ \bigcirc_{l=i-1}^{n'_k} \mathrm{Post}''_l \})^{\nabla} \oplus (\beta_{n_k j}^{j \in J \cap \mathrm{Holes}(Q)} \{ \bigcirc_{l=n_k-1}^{n'_k} \mathrm{Post}''_l \})^{\nabla} \oplus \\ \bigoplus_{i=n_k+1}^{n'_k+1-1} (\beta_{ij}^{j \in J \cap \mathrm{Holes}(Q)} \{ \bigcirc_{l=i-1}^{n_k+1} \mathrm{Post}''_l \odot \mathrm{Post}''_{n_k} \odot \bigcirc_{l=n_k-1}^{n'_k} \mathrm{Post}''_l \})^{\nabla} $$

$$ \mathrm{Pred}_k = \bigwedge_{i=n'_k}^{n_k-1} \mathrm{Pred}''_i \{ \bigcirc_{j=i-1}^{n'_k} \mathrm{Post}''_j \} \wedge \mathrm{Pred}''_{n_k} \{ \bigcirc_{j=n_k-1}^{n'_k} \mathrm{Post}''_j \} \wedge \\ \bigwedge_{i=n_k+1}^{n'_k+1-1} \mathrm{Pred}''_i \{ \bigcirc_{j=i-1}^{n'_k} \mathrm{Post}''_j \odot \mathrm{Post}''_{n_k} \odot \bigcirc_{j=n_k-1}^{n'_k} \mathrm{Post}''_j \} $$

$$ \mathrm{Post}_k = \bigcirc_{j=n'_{k+1}-1}^{n'_k} \mathrm{Post}''_j $$

Note that for all $k \in [1..n-1]$, $v'_{kl} = v_{(k+1)l}$, $v_{1l} = s_{1l} = s_l$, and $v'_{nl} = v_{(n_1+n_2+3)l} = u_{(n_2+1)l} = s'_l$.

By definition of $\mathrm{Post}_k$, we have $\bigcirc_{j=n'_{k}-1}^{1} \mathrm{Post}''_j = \bigcirc_{j=k-1}^{1} \mathrm{Post}_j$. Consequently, we have:

$$ \alpha'_{n_k} \{ \bigcirc_{j=n_k-1}^{1} \mathrm{Post}''_j \} = \alpha'_{n_k} \{ \bigcirc_{j=n_k-1}^{n'_k} \mathrm{Post}''_j \odot \bigcirc_{j=n'_k-1}^{1} \mathrm{Post}''_j \} = \alpha_k \{ \bigcirc_{j=n'_k-1}^{1} \mathrm{Post}''_j \} = \alpha_k \{ \bigcirc_{j=k-1}^{1} \mathrm{Post}_j \} $$

From equation B.1, we obtain the following equation (we recall that the actions $\alpha_k$ are the actions $\alpha'_p$ that are observable):

$$ \begin{align*} \mathrm{Pred}_{\beta} &\iff \gamma_{j_0} = \bigoplus_{p=1}^{p=n_1+n_2+2} (\alpha'_{p} \{ \bigcirc_{j=p-1}^{1} \mathrm{Post}_j \})^{\nabla} \\ &\iff \gamma_{j_0} = [\alpha_p \{ \bigcirc_{j=p-1}^{1} \mathrm{Post}_j \} | p \in [1..n]] \end{align*} $$

We need now to show that the set of WOT obtained above verifies the
conditions of the lemma, i.e. it is a set of WOT of the form:

$$Q \models \begin{array}{c} \gamma_{pj}^{j \in J_p}, \text{Pred}_p, \text{Post}_p \\ \vdots \\ \llap{$\llap{s_{pi}}$} \llap{$\llap{s_{pi}}$} \llap{$\llap{s_{pi}}$} \llap{$\llap{s_{pi}}$} \llap{$\llap{s_{pi}}$} \llap{$\llap{s_{pi}}$} \llap{$\llap{s_{pi}}$} \llap{$\llap{s_{pi}}$} \llap{$\llap{s_{pi}}$} \llap{$\llap{s_{pi}}$} \llap{$\llap{s_{pi}}$} \llap{$\llap{s_{pi}}$} \end{array}$$

with

$$\bigcup_{p=1}^{n} J_p = J \cap \text{Holes}(Q) \quad \text{trivial}$$

$$\gamma_j^{j \in J \cap \text{Holes}(Q)} = \bigoplus_{p=1}^{n} (\gamma_{pj}^{j \in J_p}) \{ \bigcirc_{i=p-1}^{1} \text{Post}_i \}$$

Indeed we have:

$$\gamma_j^{j \in J} = \bigoplus_{i=1}^{m_1} (\overline{\beta_{1i}} \{ \bigcirc_{j=i-1}^{1} \text{Post}_{1j} \})^{\nabla} \oplus (\overline{\beta_2} \{ \bigcirc_{j=m_1}^{1} \text{Post}_{1j} \})^{\nabla} \oplus \\ \bigoplus_{i=1}^{m_2} (\overline{\beta_{3i}} \{ \bigcirc_{j=i-1}^{1} \text{Post}_{3j} \odot \text{Post}_2 \odot \bigcirc_{j=m_1}^{1} \text{Post}_{1j} \})^{\nabla}$$

And thus, because $\beta_{pj}^{j \in J \cap \text{Holes}(Q)}$ are equal to the concatenation of $(\beta'_{1pj})^{j \in J \cap \text{Holes}(Q)}$, $(\beta'_{2j})^{j \in J \cap \text{Holes}(Q)}$, and $(\beta'_{3pj})^{j \in J \cap \text{Holes}(Q)}$ (re-indexed because we skipped some transitions), and additionally $(\beta'_{1pj})^{j \in J \cap \text{Holes}(Q)}$, $(\beta'_{2j})^{j \in J \cap \text{Holes}(Q)}$, and $(\beta'_{3pj})^{j \in J \cap \text{Holes}(Q)}$ are identical to the hole labels $\beta_{1kj}^{j \in J \cap \text{Holes}(Q)}$, $\beta_{2j}^{j \in J \cap \text{Holes}(Q)}$, and $\beta_{3kj}^{j \in J \cap \text{Holes}(Q)}$ (re-indexed) when $Q$ moves$^{17}$. We can assert a similar equality on post-conditions, i.e. between $\text{Post}''_p$ and $\text{Post}''_1$, $\text{Post}''_2$, $\text{Post}''_3$ where $\text{Post}''_p$ is the restriction of $\text{Post}_{1p}$ over $\text{vars}(Q)$ (see initial decomposition, case 1, 2, and 3 above). Overall, we have $\forall i \in L_Q. s_{(n+1)i} = s'_i \wedge s_{0i} = s_i$ (see above):

$$\begin{align*} \gamma_j^{j \in J \cap \text{Holes}(Q)} &= \bigoplus_{i=1}^{m_1} ((\overline{\beta'_{1i}}) \{ \bigcirc_{j=i-1}^{1} \text{Post}''_{1j} \})^{\nabla} \oplus (\overline{\beta'_2} \{ \bigcirc_{j=m_1}^{1} \text{Post}''_{1j} \})^{\nabla} \oplus \\ & \qquad \bigoplus_{i=1}^{m_2} (\overline{\beta'_{3i}} \{ \bigcirc_{j=i-1}^{1} \text{Post}''_{3j} \odot \text{Post}''_{2} \odot \bigcirc_{j=m_1}^{1} \text{Post}''_{1j} \})^{\nabla} \\ &= \bigoplus_{k=1}^{n} \left( \bigoplus_{i=n'_k}^{n'_k+1-1} (\beta_{ij}^{j \in J \cap \text{Holes}(Q)} \{ \bigcirc_{j=i-1}^{n'_k} \text{Post}''_{j} \bigcirc \bigcirc_{j=n'_k-1}^{1} \text{Post}''_{j} \})^{\nabla} \right) \\ &= \bigoplus_{k=1}^{n} \left( \gamma_{kj}^{j \in J \cap \text{Holes}(Q)} \{ \bigcirc_{j=k-1}^{1} \text{Post}_k \} \right) \end{align*}$$

<footnote>$^{17}$more precisely, when $Q$ moves either $\beta_{1kj}^{j \in J \cap \text{Holes}(Q)}$ is not empty and thus $(\beta'_{1pj})^{j \in J \cap \text{Holes}(Q)} = \beta_{1kj}^{j \in J \cap \text{Holes}(Q)}$, or both are empty if the holes of $Q$ perform no action.</footnote>
Next, we have:

$$Pred = Pred' \wedge \bigwedge_{p=1}^{n} \left( \left( \alpha_p \left\{ \left( \bigcirc_{i=p-1}^{1} Post_i \right) \right\} \right) = \beta_p \wedge \left( Pred_p \left\{ \left( \bigcirc_{i=p-1}^{1} Post_i \right) \right\} \right) \right)$$

Indeed we have:

$$
\begin{align*}
Pred &\iff \bigwedge_{i=1}^{m_1} Pred_{1i} \left\{ \left( \bigcirc_{j=i-1}^{1} Post_{1j} \right) \wedge Pred_{2i} \left\{ \left( \bigcirc_{j=m_1}^{1} Post_{1j} \right) \wedge Pred_{3i} \left\{ \left( \bigcirc_{j=i-1}^{1} Post_{3j} \odot Post_{2j} \wedge \bigcirc_{j=m_1}^{1} Post_{1j} \right) \right\} \right\} \\
&\iff \bigwedge_{i=1}^{m_1} \left( Pred'_{1i} \wedge Pred''_{1i} \wedge \alpha_{1i} = \beta_{1ij_0} \right) \left\{ \left( \bigcirc_{j=i-1}^{1} Post_{1j} \right) \right\} \\
&\qquad \wedge \left( Pred'_{2i} \wedge Pred''_{2i} \wedge \alpha_{2i} = \beta_{2j_0} \right) \left\{ \left( \bigcirc_{j=m_1}^{1} Post_{1j} \right) \right\} \\
&\qquad \wedge \bigwedge_{i=1}^{m_2} \left( Pred'_{3i} \wedge Pred''_{3i} \wedge \alpha_{3i} = \beta_{3j_0} \right) \left\{ \left( \bigcirc_{j=i-1}^{0} Post_{3j} \odot Post_{2j} \wedge \bigcirc_{j=m_1}^{1} Post_{1j} \right) \right\} \\
&\iff \bigwedge_{i=1}^{m_1} \left( Pred'_{1i} \left\{ \left( \bigcirc_{j=i-1}^{1} Post'_{1j} \right) \wedge Pred''_{1i} \left\{ \left( \bigcirc_{j=i-1}^{1} Post''_{1j} \right) \wedge (\alpha_{1i} = \beta_{1ij_0}) \left\{ \left( \bigcirc_{j=i-1}^{1} Post_{1j} \right) \right\} \right\} \right\} \\
&\qquad \wedge \left( Pred'_{2i} \left\{ \left( \bigcirc_{j=m_1}^{1} Post_{1j} \right) \wedge Pred''_{2i} \left\{ \left( \bigcirc_{j=m_1}^{1} Post_{1j} \right) \wedge (\alpha_{2i} = \beta_{2j_0}) \left\{ \left( \bigcirc_{j=m_1}^{1} Post_{1j} \right) \right\} \right\} \right\} \\
&\qquad \wedge \bigwedge_{i=1}^{m_2} \left( Pred'_{3i} \left\{ \left( \bigcirc_{j=i-1}^{1} Post_{3j} \odot Post_{2j} \wedge \bigcirc_{j=m_1}^{1} Post_{1j} \right) \wedge Pred''_{3i} \left\{ \left( \bigcirc_{j=i-1}^{1} Post_{3j} \odot Post_{2j} \wedge \bigcirc_{j=m_1}^{1} Post_{1j} \right) \right\} \right\} \\
&\qquad \wedge (\alpha_{3i} = \beta_{3ij_0}) \left\{ \left( \bigcirc_{j=i-1}^{1} Post_{3j} \odot Post_{2j} \wedge \bigcirc_{j=m_1}^{1} Post_{1j} \right) \right\}
\end{align*}
$$
$$
\begin{align*}
&\iff Pred' \wedge \bigwedge_{k=1}^{n} Pred_k \left\{ \left( \bigcirc_{j=k-1}^{1} Post_j \right) \right\} \wedge Pred_\beta \\
&\iff Pred' \wedge \bigwedge_{k=1}^{n} Pred_k \left\{ \left( \bigcirc_{j=k-1}^{1} Post_j \right) \right\} \wedge (\gamma_{j_0} = [\alpha_i \left\{ \left( \bigcirc_{j=i-1}^{1} Post_j \right) \right\} | i \in [1..n]])
\end{align*}
$$

which is exactly what is needed with $\gamma_{j_0} = [\beta_0..\beta_n]$.
$$
\bar{\gamma} = \bigoplus_{h=1}^{k} (\overline{\beta_{1h}} \{ \{ \bigcirc Post_{1j} \} \})^{\nabla} \oplus (\overline{\beta_{2}} \{ \{ \bigcirc Post_{1j} \} \})^{\nabla} \oplus
$$

$$
\bigoplus_{h=1}^{k'} (\overline{\beta_{3h}} \{ \{ \bigcirc Post_{3j} \odot Post_2 \bigcirc \bigcirc Post_{1j} \} \})^{\nabla}
$$

$$
Pred_Q = \bigwedge_{h=01}^{k} Pred_{1h} \{ \{ \bigcirc Post_{1j} \} \} \wedge Pred_2 \{ \{ \bigcirc Post_{1h} \} \} \wedge
$$

$$
\bigwedge_{h=1}^{k'} Pred_{3h} \{ \{ \bigcirc Post_{3j} \odot Post_2 \bigcirc \bigcirc Post_{1h} \} \}
$$

$$
Post_Q = \bigcirc_{h=k'}^{1} Post_{3h} \odot Post_2 \odot \bigcirc_{j=k}^{1} Post_{1j}
$$

1. For the first $k$ open tau transitions, by Definition 11 $P$ can necessarily make a tau open transition if the hole indexed $j_0$ makes a tau action. So by Lemma 2 we obtain $k$ open transitions in the form:

$$
P[Q]_{j_0} \models \frac{\overline{\beta_{1h}}, Pred_{1h}, Post_{1h}}{\triangleleft s_{1h} \uplus s_i^{i \in L} \triangleright \xrightarrow{\tau} \triangleleft s_{1(h+1)} \uplus s_i^{i \in L} \triangleright}
$$

2. For the possibly observable open transition. By Lemma 2 with the lemma hypotheses we obtain:

$$
P[Q]_{j_0} \models \frac{\beta_j^{(j \in J \setminus \{j_0\})} \uplus \overline{\beta_2}, Pred \wedge Pred_2 \wedge \alpha_Q = \beta_{j_0}, Post \uplus Post_2}{\triangleleft s_i^{i \in L} \uplus s_{21} \triangleright \xrightarrow{\alpha} \triangleleft s_i^{i' \in L} \uplus s_{22} \triangleright}
$$

3. We proceed in the same way as the first item for $k'$ last weak open transitions, and we obtain $k'$ open tau transitions.

Using Lemma 4, from cases (1), (2) and (3) we get:

$$
P[Q]_{j_0} \models \frac{\bar{\gamma}_c, Pred_c, Post_c}{\triangleleft s_{11} \uplus s_i^{i \in L} \triangleright \xrightarrow{\alpha'} \triangleleft s_i^{i' \in L} \uplus s_{3(k'+1)} \triangleright}
$$

where $\alpha' = \alpha\{\bigcirc Post_{1j}\}$ and $\alpha = \alpha'$ because $Post_{1j}$ acts on variables of $Q$ and $\alpha$ contains only variables of $P$.

$$
\bar{\gamma}_c = \bigoplus_{h=1}^{k} (\overline{\beta_{1h}} \{ \{ \bigcirc Post_{1i} \} \})^{\nabla} \oplus ((\beta_j^{(j \in J \setminus \{j_0\})} \uplus \overline{\beta_2}) \{ \{ \bigcirc Post_{1i} \} \})^{\nabla} \oplus
$$

$$
\bigoplus_{h=1}^{k'} (\overline{\beta_{3h}} \{ \{ \bigcirc Post_{3i} \odot Post_2 \bigcirc \bigcirc Post_{1i} \} \})^{\nabla}
$$

$$
= \bar{\gamma} \uplus (\beta_j^{\in J \setminus \{j_0\}})^{\nabla} \text{ because } Post_{1j} \text{ does not act on variables of } \beta_j.
$$
$$
\begin{align*}
Pred_c &= \bigwedge_{h=1}^{k} Pred_{1h} \{ \left\langle \bigcirc_{i=h-1}^{1} Post_{1i} \right\rangle \} \wedge (Pred \wedge Pred_2 \wedge \alpha'_Q = \beta_{j_0}) \{ \left\langle \bigcirc_{i=k}^{1} Post_{1i} \right\rangle \} \wedge \\
&\quad \bigwedge_{h=1}^{k'} Pred_{3h} \{ \left\langle \bigcirc_{i=h-1}^{1} Post_{3i} \odot (Post \uplus Post_2) \odot \bigcirc_{i=k}^{1} Post_{1i} \right\rangle \} \\
Post_c &= \left( \bigcirc_{i=k'}^{1} Post_{3i} \right) \odot (Post \uplus Post_2) \odot \bigcirc_{i=k}^{1} Post_{1i}
\end{align*}
$$

Note that we have $s_i^{i \in L_Q} = s_{11} \wedge s_{1(k+1)i} = s_{21} \wedge s_{22} = s_{31} \wedge s_{3(k'+1)i} = s_i^{i \in L_Q}$.

Note also that *Post* only acts on variables of *P* while *Post*<sub>*1i*</sub> only acts on variables of *Q*. We conclude on predicate and posts as follows<sup>18</sup>:

$$
\begin{align*}
Pred_c &= Pred_Q \wedge Pred\{\left\langle\bigcirc_{i=k}^{1} Post_{1i}\right\rangle\} \wedge (\alpha'_Q = \beta_{j_0}) \{\left\langle\bigcirc_{i=k}^{1} Post_{1i}\right\rangle\} \\
&= Pred_Q \wedge Pred \wedge \alpha_Q = \beta_{j_0}
\end{align*}
\[
Post_c = Post \uplus Post_Q
\]
$$

□

**Lemma 8 (Weak open transition composition).** Suppose that we have a weak open automaton such that the WOTs cannot observe silent actions (see Definition 11). Suppose $j_0 \in J$ and $\gamma_{j_0} = [\beta_0..\beta_n]$ and additionally:

$$
P \models \left\{
\begin{array}{c}
\gamma_j^{j \in J} \\
\bigwedge_{i \in L} s_i \\
\bigwedge_{i' \in L} s_i^{i' \in L}
\end{array}
\right\}
, Pred, Post
\quad \text{and } \forall p \in [1..n] \quad
Q \models \left\{
\begin{array}{c}
\gamma_{pj}^{j \in J_p} \\
\bigwedge_{i \in L_Q} s_i \\
\bigwedge_{i' \in L_Q} s_{i'}^{i' \in L_Q}
\end{array}
\right\}
$$

Let

$$
\begin{align*}
J_Q &= \bigcup_{p=1}^{n} J_p && \forall i \in L_Q. s_i = s_{0i} \wedge s'_i = s_{(n+1)i} \\
    && \forall j \in J_p, \gamma_j = \bigoplus_{p=1}^{n} \gamma_{pj} \{ \{ \bigcirc Post_k \} \}
\end{align*}
$$

$$
Pred' = Pred \wedge \bigwedge_{p=1}^{n} (\alpha_p = \beta_p \wedge Pred_p) \{ \{ \bigcirc Post_i \} \} \quad Post' = Post \uplus \{ \bigcirc Post_p \}
$$

Then, we have:

$$
P[Q]_{j_0} \models \left\{
\begin{array}{c}
\gamma_j^{j \in (J \setminus \{j_0\}) \uplus J_Q} \\
\bigwedge_{i \in L \uplus L_Q} s_i \\
\bigwedge_{i' \in L \uplus L_Q} s_{i'}^{i' \in L \uplus L_Q}
\end{array}
\right\}
, Pred', Post'
$$

<footnote n="18"><sup>18</sup>*Post*<sub>*1i*</sub> only has an effect on variables of *Q* and thus does not modify *Pred* or *β*<sub>*j*<sub>0</sub></sub>.</footnote>
PROOF. Suppose we have:

$$ P \models \begin{array}{c} \gamma_j^{j \in J} \\ \vdots \\ \Delta s_i^{i \in L} \triangleright \\ \qquad \alpha \\ \Delta s_i^{i' \in L} \triangleright \end{array} $$

By Lemma 4 this implies the following:

$$ \forall p \in [1..m_1]. P \models \begin{array}{c} \beta_{1pj}^{j \in J_{1p}}, \text{Pred}_{1p}, \text{Post}_{1p} \\ \Delta(s_{1pi})^{i \in L} \triangleright \xrightarrow{\tau} \Delta(s_{1(p+1)i})^{i \in L} \triangleright \end{array} $$

$$ P \models \begin{array}{c} \beta_{2j}^{j \in J_2}, \text{Pred}_2, \text{Post}_2 \\ \Delta(s_{21i})^{i \in L} \triangleright \xrightarrow{\alpha'} \Delta(s_{22i})^{i \in L} \triangleright \end{array} $$

$$ \text{and } \forall p \in [1..m_2]. P \models \begin{array}{c} \beta_{3pj}^{j \in J_{3p}}, \text{Pred}_{3p}, \text{Post}_{3p} \\ \Delta(s_{3pi})^{i \in L} \triangleright \xrightarrow{\tau} \Delta(s_{3(p+1)i})^{i \in L} \triangleright \end{array} $$

where:

$$ \forall i \in L. \quad s_i = s_{11i} \wedge s_{1(m_1+1)i} = s_{21i} \wedge s_{22i} = s_{31i} \wedge s_{3(m_2+1)i} = s_i' $$

$$ \alpha = \alpha' \{ \bigcirc_{j=m_1}^{1} \text{Post}_{1j} \} $$

$$ \gamma_j^{j \in J} = \bigoplus_{i=1}^{m_1} (\beta_{1ij}^{j \in J_{1p}} \{ \bigcirc_{k=i-1}^{1} \text{Post}_{1k} \})^{\nabla} \oplus (\beta_{2j}^{j \in J_2} \{ \bigcirc_{k=m_1}^{10} \text{Post}_{1k} \})^{\nabla} \oplus $$

$$ \bigoplus_{i=1}^{m_2} (\beta_{3ij}^{j \in J_{3p}} \{ \bigcirc_{k=i-1}^{1} \text{Post}_{3k} \odot \text{Post}_{2} \bigcirc \bigcirc_{k=m_1}^{1} \text{Post}_{1k} \})^{\nabla} $$

$$ \text{Pred} = \bigwedge_{p=1}^{m_1} (\text{Pred}_{1p} \{ \bigcirc_{j=p-1}^{1} \text{Post}_{1j} \}) \wedge \text{Pred}_{2} \{ \bigcirc_{p=m_1}^{1} \text{Post}_{1p} \} \wedge $$

$$ \bigwedge_{p=1}^{m_2} \text{Pred}_{3p} \{ \bigcirc_{j=p-1}^{1} \text{Post}_{3j} \odot \text{Post}_{2} \odot \bigcirc_{p=m_1}^{1} \text{Post}_{1p} \} $$

$$ \text{Post} = \bigcirc_{p=m_2}^{1} \text{Post}_{3p} \odot \text{Post}_{2} \odot \bigcirc_{j=m_1}^{1} \text{Post}_{1j} $$

Note that, for $l \in \{1,3\}$ if $\beta_{lpj_0} = \tau$, then, because of Definition 11, $P$ necessarily makes a $\tau$ open transition and remains in the same state, e.g. $s_{1pi} = s_{1(p+1)i}$. Thus without loss of generality, we can bypass such an open transition and obtain another decomposition of the WOT without the open transition that requires $\beta_{lpj_0} = \tau$. We can thus suppose that for all $p$ and $l$ we have $\beta_{lpj_0} \neq \tau$ or $j_0 \notin J_{1p}$. To avoid a special case, we suppose that the hole $j_0$ moves during the OT $\alpha'$, i.e. $\beta_{2j_0} = \beta_m$ for some $m$. Additionally, $\beta_m \neq \tau$, else we would have $\alpha = \alpha' = \tau$ and the $\alpha'$ OT could be also removed from the reduction, leading to a particular and simpler case.

We introduce $n_i^{i \in [1..m-1]}$, and $(n_i')^{i \in [m+1..n]}$ the indices of the steps in which the hole $j_0$ moves in the 3 sets of OTs above ($\beta_m$ is the action that matches the hole $j_0$ in the OT $\alpha'$), in other words, we have for all $i$, $\beta_{1n_i j_0}$ a visible action,
as additionally:

$$
\begin{align*}
\gamma_{j0} &= [\beta_0..\beta_n] \\
&= \bigoplus_{\substack{i=1 \\ j_0 \in J_{1i}}}^{m_1} (\beta_{1ij_0} \{ \langle \bullet \otimes \text{Post}_{1k} \rangle \}^\nabla) \oplus (\beta_{2j_0} \{ \langle \bullet \otimes \text{Post}_{1k} \rangle \}^\nabla) \oplus \\
&\qquad \bigoplus_{\substack{i=0 \\ j_0 \in J_{3i}}}^{m_2} (\beta_{3ij_0} \{ \langle \bullet \otimes \text{Post}_{3k} \odot \text{Post}_{2k} \rangle \}^\nabla) \oplus \\
&\qquad (\beta_{4j_0} \{ \langle \bullet \otimes \text{Post}_{4k} \rangle \}^\nabla)
\end{align*}
$$

We have, by definition of $n_i$ and $n'_i$:

$$
\forall i \in [1..m-1], \beta_{1n_{i}j_{0}} \{ \bigcirc_{k=n_{i}-1}^{1} \text{Post}_{1k} \} = \beta_{i}, \quad \beta_{2j_{0}} \{ \bigcirc_{k=m_{1}}^{1} \text{Post}_{1k} \} = \beta_{m}, \text{ and}
$$

$$
\forall i \in [m+1..n], \beta_{3n'_{i}j_{0}} \{ \bigcirc_{k=n'_{i}-1}^{1} \text{Post}_{3k} \odot \text{Post}_{2k} \bigcirc \bigcirc_{k=m_{1}}^{1} \text{Post}_{1k} \} = \beta_{i}
$$

Now, we compose OTs for each of the case above (depending on the OT of P):

1. For the first $\tau$ OTs, i.e. $p \in [1..m_1]$. We have:
Either there is $i$ such that $p = n_i$, and thus $\beta_i$ and $\beta_{1pj_0}$ are defined. In this case by Lemma 7, we have:

$$
P[Q]_{j_0} \models \overline{\gamma'_{1p}, \mathrm{Pred}'_{1p}, \mathrm{Post}'_{1p}}
$$

with

$$
\bar{\gamma}_{1p} = \gamma_{ij}^{j \in J_i} \cup (\beta_{1pj}^{j \in J_{1p} \setminus \{j_0\}})^{\nabla} \quad \mathrm{Pred}'_{1p} = \mathrm{Pred}_{1p} \wedge (\beta_{1pj_0} = \alpha_i \wedge \mathrm{Pred}_i)
$$

$$
\mathrm{Post}'_{1p} = \mathrm{Post}_{1p} \uplus \mathrm{Post}_i
$$

Or $j_0 \notin \text{dom}(\beta_{1p})$ and $Q$ does not move in the composed reduction. In this case there is no $i$ such that $p = n_i$, but there is $i$ such that $p \in]n_i..n_{i+1}[$, and

$$
P[Q]_{j_0} \models \overline{\beta_{1p}, \mathrm{Pred}_{1p}, \mathrm{Post}_{1p}}
$$

and thus we also have a weak OT by Definition 13 (rule (WT2)):

$$
P[Q]_{j_0} \models \overline{\gamma'_{1p}, \mathrm{Pred}'_{1p}, \mathrm{Post}'_{1p}}
$$

with $\overline{\gamma'_{1p}} = (\overline{\beta_{1p}})^{\nabla}$, $\mathrm{Pred}'_{1p} = \mathrm{Pred}_{1p}$, $\mathrm{Post}'_{1p} = \mathrm{Post}_{1p}$
2. Similarly, for the middle OT with label $\alpha$:

$$ P[Q]_{j_0} \models \frac{\overline{\gamma'_2, Pred'_2, Post'_2}}{\Delta(s_{21j})^{j \in L} \uplus (s_{mj})^{j \in L_Q} \triangleright \alpha' \Rightarrow \Delta(s_{22j})^{j \in L} \uplus (s_{(m+1)j})^{j \in L_Q} \triangleright} $$

with

$$ \overline{\gamma'_2} = \gamma_{mj}^{j \in J_m} \uplus (\beta_{2j}^{j \in J_2} \setminus \{j_0\})^{\nabla} $$

$$ Pred'_2 = Pred_2 \wedge (\beta_{2j_0} = \alpha_m \wedge Pred_m) $$

$$ Post'_2 = Post_2 \uplus Post_m $$

3. For the last $\tau$ OTs, i.e. $p \in [1..m_2]$. We have similarly to the first case: Either there is $i$ such that $p = n'_i$, and thus $\beta_i$ and $\beta_{1pj_0}$ are defined. In this case by Lemma 7, we have:

$$ P[Q]_{j_0} \models \frac{\overline{\gamma'_{3p}, Pred'_{3p}, Post'_{3p}}}{\Delta s_{3pj}^{j \in L} \uplus s_{ij}^{j \in L_Q} \triangleright \tau \Rightarrow \Delta s_{3(p+1)j}^{j \in L} \uplus s_{(i+1)j}^{j \in L_Q} \triangleright} $$

with

$$ \overline{\gamma'_{3p}} = \gamma_{ij}^{j \in J_i} \uplus (\beta_{3pj}^{j \in J_{3p}} \setminus \{j_0\})^{\nabla} $$

$$ Pred'_{3p} = Pred_{3p} \wedge (\beta_{3pj_0} = \alpha_i \wedge Pred_i) $$

$$ Post'_{3p} = Post_{3p} \uplus Post_i $$

Or $j_0 \notin \text{dom}(\beta_{3p})$ and $Q$ does not move in the composed reduction. In this case there is no $i$ such that $p = n'_i$, but there is $i$ such that $p \in ]n'_i..n'_{i+1}[$, and

$$ P[Q]_{j_0} \models \frac{\overline{\beta_{3p}, Pred_{3p}, Post_{3p}}}{\Delta s_{3pj}^{j \in L} \uplus s_{ij}^{j \in L_Q} \triangleright \tau \Rightarrow \Delta s_{3(p+1)j}^{j \in L} \uplus s_{ij}^{j \in L_Q} \triangleright} $$

and thus we also have a weak OT by definition 13 (rule **WT2**):

$$ P[Q]_{j_0} \models \frac{\overline{\gamma'_{3p}, Pred'_{3p}, Post'_{3p}}}{\Delta s_{3pj}^{j \in L} \uplus s_{ij}^{j \in L_Q} \triangleright \alpha'' \Rightarrow \Delta s_{3(p+1)j}^{j \in L} \uplus s_{ij}^{j \in L_Q} \triangleright} $$

with $\overline{\gamma'_{3p}} = \overline{\beta_{3p}}$, $Pred'_{3p} = Pred_{3p}$, $Post'_{3p} = Post_{3p}$

By definition of weak open transition (Definition 13, rule **WT3**), we obtain:

$$ P[Q]_{j_0} \models \frac{\overline{\gamma', Pred'', Post''}}{\Delta s_{10j}^{j \in L} \uplus s_{0j}^{j \in L_Q} \triangleright \alpha'' \Rightarrow \Delta s_{3(m_2+1)j}^{j \in L} \uplus s_{(n+1)j}^{j \in L_Q} \triangleright} $$
where

$$ \alpha'' = \alpha' \{ \bigcirc_{j=m_1}^{1} \mathrm{Post}'_{1j} \} $$

$$ \bar{\gamma}' = \bigoplus_{i=1}^{m_1} \bar{\gamma}'_{1i} \{ \bigcirc_{k=i-1}^{1} \mathrm{Post}'_{1k} \} \oplus \bar{\gamma}'_2 \{ \bigcirc_{k=m_1}^{1} \mathrm{Post}'_{1k} \} \oplus $$

$$ \bigoplus_{i=1}^{m_2} \bar{\gamma}'_{3i} \{ \bigcirc_{k=i-1}^{1} \mathrm{Post}'_{3k} \odot \mathrm{Post}'_{2} \odot \bigcirc_{k=n}^{1} \mathrm{Post}'_{1k} \} $$

$$ \mathrm{Pred}'' = \bigwedge_{i=1}^{m_1} \mathrm{Pred}'_{1i} \{ \bigcirc_{j=i-1}^{1} \mathrm{Post}'_{1j} \} \wedge \mathrm{Pred}'_2 \{ \bigcirc_{j=m_1}^{1} \mathrm{Post}'_{1j} \} \wedge $$

$$ \bigwedge_{i=1}^{m_2} \mathrm{Pred}'_{3i} \{ \bigcirc_{j=i-1}^{1} \mathrm{Post}'_{3j} \odot \mathrm{Post}'_{2} \odot \bigcirc_{j=m_2}^{1} \mathrm{Post}'_{1j} \} $$

$$ \mathrm{Post}'' = \bigcirc_{j=m_2}^{1} \mathrm{Post}'_{3j} \odot \mathrm{Post}'_{2} \odot \bigcirc_{j=m_1}^{1} \mathrm{Post}'_{1j} $$

However it must be noticed that in steps 1 and 3, we have two kinds of WOTs with different signatures (depending on whether $Q$ moves or not). It is still possible to glue them together in a global rule with two more terms for $Pred$ and $Post$ terms. This global merge is possible because the post-conditions of $P$ only act on variables of $P$ and those of $Q$ on variables of $Q$ (for example $Post_i$ has no effect on $Pred_{1p}$ and thus does not need to be taken into account when dealing with WOTs where $Q$ does not move).

We now compare each element of the obtained WOT with the conclusion of the lemma:

$$ \alpha'' = \alpha' \{ \bigcirc_{j=m_1}^{1} \mathrm{Post}'_{1j} \} $$

$$ = \alpha' \{ \bigcirc_{j=m_1}^{1} \mathrm{Post}_{1j} \} \quad \alpha' \text{ only contains variables of } P \text{ untouched by } \mathrm{Post}_i $$

$$ = \alpha $$

For $\bar{\gamma}'$ we distinguish elements in the holes of $P$ and of $Q$.

First suppose $j \in J \setminus \{j_0\}$ we have $\gamma'_j = \gamma_j$ because $\mathrm{Post}'_{ij}$ has no effect on variables of $P$ and on $\beta_{1pj}$, consequently we have:

$$ \gamma'_j = \bigoplus_{i=1}^{m_1} (\beta_{1ij} \{ \bigcirc_{k=i-1}^{1} \mathrm{Post}_{1k} \})^{\nabla} \oplus (\beta_{2j} \{ \bigcirc_{k=m_1}^{1} \mathrm{Post}_{1k} \})^{\nabla} \oplus $$

$$ \bigoplus_{i=1}^{m_2} (\beta_{3ij} \{ \bigcirc_{k=i-1}^{1} \mathrm{Post}_{3k} \odot \mathrm{Post}_{2} \odot \bigcirc_{k=m_1}^{1} \mathrm{Post}_{1k} \})^{\nabla} $$
Second, when $j \in J_t$ for some $t$, $\gamma'_j$ is the concatenation of elements of $\gamma'_{1ij}$, $\gamma'_{2j}$, $\gamma'_{3ij}$ that are not empty. By construction the concatenation of these elements is $\gamma_{tj}$, for $t \in [0..n]$. $Post_{ik}$ has no effect on $\gamma_{tj}$ but $Post_k$ has. We obtain:

$$
\begin{align*}
\gamma'_j &= \bigoplus_{i=1}^{m_1} \gamma'_{1ij} \{ \{ \bigcirc^{1} Post'_{1k} \} \} \oplus \gamma'_{2j} \{ \{ \bigcirc^{1} Post'_{1k} \} \} \oplus \\
&\qquad \bigoplus_{i=1}^{m_2} \gamma'_{3ij} \{ \{ \bigcirc^{1} Post'_{3k} \odot Post'_{2} \odot \bigcirc^{1} Post'_{1k} \} \} \\
&= \bigoplus_{t=1}^{n} \gamma_{tj} \{ \{ \bigcirc^{1} Post_k \} \}
\end{align*}
$$

Concerning predicates, we also separate predicates on P from predicates on Q, and from the equality on the action filling the hole:

$$
\begin{align*}
Pred'' &= \left( \bigwedge_{i=1}^{m_1} Pred'_{1i} \{ \{ \bigcirc^{1} Post'_{1j} \} \} \wedge Pred'_{2} \{ \{ \bigcirc^{1} Post'_{1j} \} \} \right. \\
&\qquad \left. \wedge \bigwedge_{i=1}^{m_3} Pred'_{3i} \{ \{ \bigcirc^{1} Post'_{3j} \odot Post'_{2} \odot \bigcirc^{1} Post'_{1j} \} \} \right) \\
&= \left( \bigwedge_{p=1}^{m_1} Pred_{1p} \{ \{ \bigcirc^{1} Post_{1j} \} \} \wedge Pred_{2} \{ \{ \bigcirc^{1} Post_{1p} \} \} \wedge \bigwedge_{p=1}^{m_2} Pred_{3p} \{ \{ \bigcirc^{1} Post_{3j} \otimes Post_{2} \otimes \bigcirc^{1} Post_{1p} \} \} \right. \\
&\qquad \left. \wedge \bigwedge_{t=1}^{n} Pred_t \{ \bigcirc^{1} Post_i \wedge \left( \bigwedge_{i=1}^{m_1} (\beta_{1n_i j_0} = \alpha_i) \{ \{ \bigcirc^{1} Post'_{1j} \} \wedge (\beta_{2j_0} = \alpha_m) \{ \{ \bigcirc^{1} Post'_{1j} \} \} \right. \right. \\
&\qquad \left. \left. \wedge \bigwedge_{i=m+1}^{n} (\beta_{3n'_i j_0} = \alpha_i) \{ \{ \bigcirc^{1} Post'_{3j} \odot Post'_{2} \odot \bigcirc^{1} Post'_{1j} \} \} \right) \right) \\
&= \left( \bigwedge_{p=1}^{m_1} Pred_{1p} \{ \{ \bigcirc^{1} Post_{1j} \} \} \wedge Pred_{2} \{ \{ \bigcirc^{1} Post_{1p} \} \} \wedge \bigwedge_{p=1}^{m_2} Pred_{3p} \{ \{ \bigcirc^{1} Post_{3j} \otimes Post_{2} \otimes \bigcirc^{1} Post_{1p} \} \} \right) \\
&\qquad \left. \wedge \bigwedge_{t=1}^{n} Pred_t \{ \bigcirc^{1} Post_i \wedge \left( \bigwedge_{i=1}^{m_1} (\beta_i = \alpha_i) \{ \{ \bigcirc^{1} Post_j \} \wedge (\beta_m = \alpha_m) \{ \{ \bigcirc^{1} Post_j \} \} \right. \right. \\
&\qquad \left. \left. \wedge \bigwedge_{i=m+1}^{n} (\beta_i = \alpha_i) \{ \{ \bigcirc^{m} Post_j \odot Post_m \odot \bigcirc^{1} Post_j \} \} \right) \right)
\end{align*}
\qquad = Pred
$$
Finally, concerning post-conditions:

$$
\begin{align*}
Post'' &= \bigcirc_{j=m_2}^{1} Post'_{3j} \odot Post'_{2} \odot \bigcirc_{j=m_1}^{1} Post'_{1j} \\
&= \left( \bigcirc_{j=m_2}^{1} Post'_{3j} \odot Post'_{2} \odot \bigcirc_{j=m_1}^{1} Post'_{1j} \right) \uplus \bigcirc_{j=n}^{1} Post_j \\
&= Post \uplus \bigcirc_{j=n}^{1} Post_j
\end{align*}
$$

This allows us to conclude concerning the lemma. □

**Theorem 7. Congruence.** Consider an open pNet: $P = \langle P_i^{i \in I}, \text{Sort}_j^{j \in J}, \overline{SV} \rangle$. Let $j_0 \in J$ be a hole. Let $Q$ and $Q'$ be two weak FH-bisimilar pNets such that $\text{Sort}(Q) = \text{Sort}(Q') = \text{Sort}_{j_0}$. Then $P[Q]_{j_0}$ and $P[Q']_{j_0}$ are weak FH-bisimilar.

PROOF. Consider $Q$ weak FH-bisimilar to $Q'$. It means that there exists an FH-bisimulation $\mathcal{R}_{Q,Q'}$ relating the two pNets $Q$ and $Q'$. We define a relation $\mathcal{R}$ relating states of $P[Q]_{j_0}$ with states of $P[Q']_{j_0}$:

$$
\mathcal{R} = \{(\langle S_P \uplus S_Q \rangle, \langle S_P \uplus S_{Q'} \rangle, \langle \text{Pred}_{Q,Q'} \rangle) | (S_Q, S_{Q'}, \text{Pred}_{Q,Q'}) \in \mathcal{R}_{Q,Q'}\}
$$

To prove weak FH-bisimilarity of $P[Q]_{j_0}$ and $P[Q']_{j_0}$, we consider an open transition $\text{OT}$ of $P[Q]_{j_0}$, and an equivalent state of $P[Q']_{j_0}$, and we try to find a family of WOT of $P[Q']_{j_0}$ that simulates $\text{OT}$. Consider an OT of $P[Q]_{j_0}$ it is of the form (notations introduced to prepare the decomposition):

$$
P[Q]_{j_0} \models \frac{\beta_j^{j \in (J_P \uplus J_Q)}, \text{Pred}_P \wedge \text{Pred}_Q, \text{Post}_P \uplus \text{Post}_Q}{\langle S_P \uplus S_Q \rangle \stackrel{\alpha}{\longrightarrow} \langle S'_P \uplus S'_Q \rangle}
$$

By the decomposition lemma for OTs (Lemma 1), we obtain the 2 following
OTs (equality side-conditions have been unlined for clarity):

$$
P \models \frac{\beta_j^{j \in J_P} \uplus (j_0 \to \alpha_Q), \text{Pred}_P, \text{Post}_Q}{\langle S_P \rangle \stackrel{\alpha}{\longrightarrow} \langle S'_P \rangle} \quad \text{and} \quad Q \models \frac{\beta_j^{j \in J_Q}, \text{Pred}_Q, \text{Post}_Q}{\langle S_Q \rangle \stackrel{\alpha_Q}{\longrightarrow} \langle S'_Q \rangle}
$$

By definition of $\mathcal{R}$ we have $(S_Q, S_{Q'} | \text{Pred}_{Q,Q'}) \in \mathcal{R}_{Q,Q'}$. And thus, by definition of weak FH-bisimulation, there exists a family of weak open transitions $WOT_x$:

$$
\frac{\gamma_{jx}^{j \in J_Q}, \mathrm{Pred}_{Q'x}, \mathrm{Post}_{Q'x}}{\langle S_{Q'} \rangle \stackrel{\alpha_x}{\Longrightarrow} \langle S'_{Q'} x \rangle}
$$

where

$$
\forall x. (S'_{Q}, S'_{Q'x} | \text{Pred}_{Q,Q'x}) \in \mathcal{R}_{Q,Q'}
$$
and

$$ \mathrm{Pred}_{Q,Q'} \wedge \mathrm{Pred}_{Q} \implies \left( \bigvee_{x \in X} (\forall j \in J_Q . (\beta_j)^\nabla = \gamma_{jx}) \Rightarrow (\mathrm{Pred}_{Q_x} \wedge \alpha_Q = \alpha_x \wedge \mathrm{Pred}_{Q,Q'_x} \{\mathrm{Post}_{Q'_x} \uplus \mathrm{Post}_Q\}) \right) $$

Composing the OT of P with the WOTs of $Q'$ by Lemma 7 we obtain:

$$ P[Q']_{j_0} \models \frac{(\beta_j^{j \in J_P})^{\nabla} \uplus \gamma_{jx}^{j \in J_Q}, \mathrm{Pred}_P \wedge \mathrm{Pred}_{Q'_x}, \mathrm{Post}_P \uplus \mathrm{Post}_{Q'_x}}{\langle \mathrm{S}_P \uplus \mathrm{S}_{Q'} \rangle^{\alpha} \Rightarrow \langle \mathrm{S}'_P \uplus \mathrm{S}'_{Q'_x} \rangle} $$

with $\bigvee_{x \in X} (\forall j \in J_Q . (\beta_j)^\nabla = \gamma_{jx} \implies \alpha_Q = \alpha_x)$ that ensures that the open transitions can be recomposed when the OT fires.

Side conditions necessary to prove weak-FH bisimulations are:

$$ \forall x. (S'_P \uplus S'_Q, S'_P \uplus S'_{Q'_x} | \mathrm{Pred}_{Q,Q'_x}) \in \mathcal{R} $$

which is true, and

$$ \mathrm{Pred}_{Q,Q'} \wedge \mathrm{Pred}_P \wedge \mathrm{Pred}_Q \implies \left( \bigvee_{x \in X} (\forall j \in J_Q . (\beta_j)^\nabla = \gamma_{jx} \wedge \forall j \in J_P . (\beta_j)^\nabla = (\beta_j)^\nabla) \Rightarrow (\mathrm{Pred}_P \wedge \mathrm{Pred}_{Q'_x} \wedge \alpha = \alpha \wedge \mathrm{Pred}_{Q,Q'_x} \{\mathrm{Post}_P \uplus \mathrm{Post}_{Q'_x} \uplus \mathrm{Post}_Q\}) \right) $$

We conclude by observing that $\mathrm{Post}_P$ has no effect on variables of $Q$ and $Q'$, and thus on $\mathrm{Pred}_{Q,Q'_x}$. $\square$

**Theorem 8.** *Context equivalence.* Consider two FH-bisimilar open pNets: $P = \langle P_i^{i \in I}, \mathrm{Sort}_i^{j \in J}, \overline{\mathrm{SV}} \rangle$ and $P' = \langle P_i'^{i \in I}, \mathrm{Sort}_i^{j \in J}, \overline{\mathrm{SV}}' \rangle$ (recall they must have the same holes to be bisimilar). Let $j_0 \in J$ be a hole, and $Q$ be a pNet such that $\mathrm{Sort}(Q) = \mathrm{Sort}_{j_0}$. Then $P[Q]_{j_0}$ and $P'[Q]_{j_0}$ are FH-bisimilar.

**PROOF.** Consider $P$ weak FH-bisimilar to $P'$. There exists an FH-bisimulation $\mathcal{R}_{P,P'}$ relating $P$ and $P'$. We define a relation $\mathcal{R}$ relating states of $P[Q]_{j_0}$ with states of $P'[Q]_{j_0}$:

$$ \mathcal{R} = \{(\langle \mathrm{S}_P \uplus \mathrm{S}_{Q'} \rangle, \langle \mathrm{S}_{P'} \uplus \mathrm{S}_{Q'} \rangle, \mathrm{Pred}_{P,P'}) | (S_P, S_{P'}, \mathrm{Pred}_{P,P'}) \in \mathcal{R}_{P,P'}\} $$

To prove weak FH-bisimilarity of $P[Q]_{j_0}$ and $P'[Q]_{j_0}$, we consider an open transition OT of $P[Q]_{j_0}$, and an equivalent state of $P'[Q]_{j_0}$, and we try to find a family of WOT of $P'[Q]_{j_0}$ that simulates OT. Consider an OT of $P[Q]_{j_0}$ it is of the form (notations introduced to prepare the decomposition):

$$ P[Q]_{j_0} \models \frac{\beta_j^{j \in (J_P \uplus J_Q)}, \mathrm{Pred}_P \wedge \mathrm{Pred}_{Q'} \wedge \mathrm{Pred}, \mathrm{Post}_P \uplus \mathrm{Post}_Q}{\langle \mathrm{S}_P \uplus \mathrm{S}_{Q'} \rangle^{\alpha} \Rightarrow \langle \mathrm{S}'_P \uplus \mathrm{S}'_{Q'} \rangle} $$
By the decomposition lemma for OTs (Lemma 1), we obtain the 2 following OTs (equality side-conditions have been unlined for clarity):

$$P \models \frac{\beta_j^{j \in J_P} \uplus (j_0 \to \alpha_Q), Pred_P, Post_Q}{\triangleleft S_P \triangleright \xrightarrow{\alpha} \triangleleft S'_{P'} \triangleright}$$

and

$$Q \models \frac{\beta_j^{j \in J_Q}, Pred_Q, Post_Q}{\triangleleft S_Q \triangleright \xrightarrow{\alpha_Q} \triangleleft S'_{Q'} \triangleright}$$

$$\text{With } Pred \iff \alpha_Q = \beta_{j_0}$$

By definition of $\mathcal{R}$ we have $(S_P, S_{P'}, Pred_{P,P'}) \in \mathcal{R}_{P,P'}$. And thus, by definition of weak FH-bisimulation, there exists a family of weak open transitions $WOT_x$:

$$\frac{\gamma_{jx}^{j \in J_P \uplus \{j_0\}}, Pred_{P'x}, Post_{P'x}}{\triangleleft S_{P'} \triangleright \xrightarrow{\alpha_x} \triangleleft S'_{P'x} \triangleright}$$

where

$$\forall x. (S'_{P}, S'_{P'x}, Pred_{P,P'x}) \in \mathcal{R}_{P,P'}$$

and

$$Pred_{P,P'} \wedge Pred_P \implies \left( \bigvee_{x \in X} (\forall j \in J_P. (\beta_j)^\nabla = \gamma_{jx} \wedge (\alpha_Q)^\nabla = \gamma_{j_0}) \Rightarrow (Pred_{P_x} \wedge \alpha = \alpha_x \wedge Pred_{P,P'_x} \{Post_{P'_x} \uplus Post_P\}) \right)$$

We here need a special case of Lemma 8 where the inner pNet $Q$ does a simple OT. This is just a particular case of the theorem but where notations get simplified because the inner pNet does a single transition. This way we can compose the WOTs of $P'$ with the OT of $Q$ and obtain, with $\gamma_{j_0} = [\beta]$:

$$P'[Q]_{j_0} \models \frac{(\beta_j^{j \in J_Q})^\nabla \uplus \gamma_{jx}^{j \in J_P}, Pred_{P'x} \wedge Pred_Q \wedge \alpha_Q = \beta, Post_{P'x} \uplus Post_Q}{\triangleleft S_{P'} \uplus S_Q \triangleright \xrightarrow{\alpha_x} \triangleleft S'_{P'x} \uplus S'_Q \triangleright}$$

Side conditions necessary to prove weak FH-bisimulations are:

$$\forall x. (S'_{P} \uplus S'_{Q}, S'_{P'x} \uplus S'_{Q}, Pred_{P,P'x}) \in \mathcal{R}$$

which is true, and

$$Pred_{P,P'} \wedge Pred_P \wedge Pred_Q \wedge Pred \implies \left( \bigvee_{x \in X} (\forall j \in J_P. (\beta_j)^\nabla = \gamma_{jx} \wedge \forall j \in J_Q. (\beta_j)^\nabla = (\beta_j)^\nabla) \Rightarrow (Pred_{P'x} \wedge Pred_Q \wedge \alpha_Q = \beta \wedge \alpha_x = \alpha \wedge Pred_{P,P'_x} \{Post_{P'_x} \uplus Post_P \uplus Post_Q\}) \right)$$

We conclude by observing that $Post_Q$ has no effect on variables of $P$ and $P'$, and thus on $Pred_{P,P'_x}$ and $Pred$ leading to the conclusion about $\alpha_Q = \beta$. $\square$
## Appendix C. Full details of the Simple Protocol Example

The first piece of code is the textual definition of the *SimpleProtocolSpec* pNet, that was drawn in Figure 2, page 14. This code should be intuitive enough to read, with the following language conventions, that brings some user-friendly features, mapped by the editor into pure pNet constructs.

* Constants of any type (including Action) must be declared as "const". They are used either as functions with argument, as typically `in(msg)`, or constants without argument, typically as `tau()`.

* Variables can be declared as global variables of a pLTS (e.g. `m_msg` in `PerfectBuffer`), or a pNet Node in the case of synchronisation vector variables (e.g. `p_a`), or as input variables in a pLTS, as `?msg` in `PerfectBuffer`.

* The variables in the guards of synchronisation vectors (e.g. in SV1) do not need to be explicitly quantified: by convention, all variables in a guard that do not appear inside the vector actions will be recognised as bound by a *forall* quantifier inside the guard.

* The tools will check that everything is correctly declared, that variables are used properly and do not conflict between different objects, that vectors have coherent length, etc.

```pnet
SimpleProtocolSpec:
    import "Data_Alg.algp"
root SimpleProtocolSpec
const in, out:Action
const p_send, q_recv: Action
const tau:Action

pLTS PerfectBuffer
initial b0
vars ?m:Data
vars b_message:Data b_ec: Nat

state b0
transition in(m) -> b1 {b_message:=m, b_ec:=0}

state b1
transition out(b_message, b_ec) -> b0
transition synchro(tau()) -> b1 {b_ec:=b_ec+1}

pNet SimpleProtocolSpec
holes P,Q
subnets P,PerfectBuffer,Q
vars p_a,q_b:Action m:Data ec: Nat

vector SV0 <p_send(m), in(m), _->synchro(in(m))
vector SV1 <p_a,_, _->p_a [p_a != p_send(x)]
vector SV2 <_, out(m,ec), q_recv(m,ec) _->synchro(out(m,ec))
vector SV3 <_, q_b>->q_a [q_b != q_recv(x,y)]
```
The corresponding generated Open Automaton was given in Figure 4, page 21.

Next is the code for the *SimpleProtocolImpl* pNet:

```c
SimpleProtocolImpl:
    import "Data_Alg.algp"
    root SimpleProtocolImpl
const in,out:Action
const tau,p_send,q_recv,m_recv,m_send,m_error: Action
const s_recv,s_send,s_ACK,s_error,r_recv,r_ACK,r_send: Action

pLTS Sender
    initial s0
    vars ?m:Data
    vars s_message:Data s_ec: Nat
state s0
    transition s_recv(m) -> s1 {s_message:=m, s_ec:=0}
state s1
    transition s_send(s_message, s_ec) -> s2
state s2
    transition s_ACK() -> s0
    transition s_error() -> s1 {s_ec:=s_ec+1}

pLTS Medium
    initial m0
    vars ?m:Data ?ec: Nat
    vars m_message:Data m_ec: Nat
state m0
    transition m_recv(m,ec) -> m1 {m_message:=m, m_ec:=ec}
state m1
    transition m_send(m_message, m_ec) -> m0
    transition synchro(tau()) -> m2
state m2
    transition m_error() -> m0

pLTS Receiver
    initial r0
    vars ?m:Data ?ec: Nat
    vars r_message:Data r_ec: Nat
state r0
    transition r_recv(m,ec) -> r1 {r_message:=m, r_ec:=ec}
state r1
    transition r_send(r_message, r_ec) -> r2
state r2
    transition r_ACK() -> r0

pNet SimpleProtocol
    subnets Sender,Medium,Receiver
    vars m:Data c: Nat
vector SV0 <s_recv(m),_, _->in(m)
vector SV1 <s_send(m,ec),m_recv(m,ec), _->synchro(tau())
vector SV2 <_,m_send(m,ec),r_recv(m,ec)>->synchro(tau())
vector SV3 <s_ACK(),_,r_ACK()>->synchro(tau())
vector SV4 <s_error(),m_error(), _->synchro(tau())
vector SV5 <_,_,r_send(m,ec)>->out(m,ec)

pNet SimpleProtocolImpl
    holes P,Q
    subnets P,SimpleProtocol,Q
    vars p_a,q_a:Action m:Data c: Nat
vector SV0 <p_send(m),in(m), _->synchro(in(m))
vector SV1 <p_a,_, _->p_a [p_a != p_send(x)]
vector SV2 <_,out(m,ec),q_recv(m,ec)>->synchro(out(m,ec))
vector SV3 <_,_,q_b>_->q_b [q_b != q_recv(x,y)]
```
<figure><img src="image_17.png" /><figcaption>Figure C.11: Weak Open Automaton for SimpleProtocolImpl</figcaption></figure>

In Figure C.11 we recall the weak open automaton of SimpleProtocolImpl. This drawing is based on the observation that states 202 and 000 are only linked by a "pure $\tau$" transition, and have exactly the same possible behaviours. In this configuration we can guarantee that they are weak bisimilar, and we have merged their (incoming and outgoing) transitions in the figure. We denote this equivalence class of states as $\{000, 202\}$.

Full details of the weak transitions is listed here:

In the first 3 weak transitions, $S$ denotes the set of all global states.

$$W_{\tau} = \frac{\{\}, True, ()}{S \overset{\tau}{\Rightarrow} S}$$

$$WI_1 = \frac{\{P \to p-a\}, [\forall x.p-a \neq p-send(x)], ()}{S \underset{p-a}{\stackrel{\rightleftharpoons}{\Rightarrow}} S}$$

$$WI_2 = \frac{\{Q \to q-b\}, [\forall x,y.q-b \neq q-recv(x,y)], ()}{S \underset{q-b}{\stackrel{\rightleftharpoons}{\Rightarrow}} S}$$

All the following transitions are parameterised by an integer $n \in \mathbb{N}$, meaning they stand for the corresponding (infinite) set of weak OTs. In some cases, this set is further restricted (see e.g. $WI_{7b}(n)$), in which cases we have added an explicit quantifier.

$$WI_3(n) = \frac{\{P \to p-send(m)\}, True, (s_msg \leftarrow m, s_ec \leftarrow n)}{\{000, 202\} \stackrel{\text{in(m)}}{\rightleftharpoons} 100}$$

$$WI_{3a}(n) = \frac{\{P \to p-send(m)\}, True, (m_msg \leftarrow m, m_ec \leftarrow n, s_ec \leftarrow n)}{\{000, 202\} \stackrel{\text{in(m)}}{\rightleftharpoons} 210}$$

$$WI_{3b}(n) = \frac{\{P \to p-send(m)\}, True, (s_ec \leftarrow n)}{\{000, 202\} \stackrel{\text{in(m)}}{\rightleftharpoons} 220}$$
$$WI_{3c}(n) = \frac{\{P \to p\text{-send}(m)\}, True, (r\_msg \leftarrow m, r\_ec \leftarrow n)}{\{000, 202\} \overset{\text{in}(m)}{\rightleftharpoons} 201}$$

$$WI_{4}(n) = \frac{\{\}, True, (m\_msg \leftarrow s\_msg, m\_ec \leftarrow s\_ec + n, s\_ec \leftarrow s\_ec + n)}{100 \xrightarrow{\tau} 210}$$

$$WI_{4a}(n) = \frac{\{\}, True, (s\_ec \leftarrow s\_ec + n)}{100 \xrightarrow{\tau} 220}$$

$$WI_{5}(n) = \frac{\{\}, True, (s\_ec \leftarrow s\_ec + n)}{210 \xrightarrow{\tau} 220}$$

$$WI_{5a}(n) = \frac{\{\}, True, (s\_ec \leftarrow s\_ec + 1 + n)}{210 \xrightarrow{\tau} 100}$$

$$WI_{6}(n) = \frac{\{\}, True, (s\_ec \leftarrow s\_ec + 1 + n)}{220 \xrightarrow{\tau} 100}$$

$$WI_{6a}(n) = \frac{\{\}, True, (m\_msg \leftarrow s\_msg, m\_ec \leftarrow s\_ec + 1 + n, s\_ec \leftarrow s\_ec + 1 + n)}{220 \xrightarrow{\tau} 210}$$

Because

$$\begin{aligned}
Post_{6a} &= post_{4} \odot post_{456}^{*} \odot post_{6} \\
&= ((m\_msg \leftarrow s\_msg, m\_ec \leftarrow s\_ec) \odot (s\_ec \leftarrow s\_ec + n)) \odot (s\_ec \leftarrow s\_ec + 1) \\
&= (m\_msg \leftarrow s\_msg, m\_ec \leftarrow (s\_ec + 1) + n, s\_ec \leftarrow (s\_ec + 1) + n)
\end{aligned}$$

$$WI_{456*}(n) = \frac{\{\}, True, (s\_ec \leftarrow s\_ec + n)}{100 \xrightarrow{\tau} 100}$$

$$WI_{564*}(n) = \frac{\{\}, True, (m\_msg \leftarrow s\_msg, s\_ec \leftarrow s\_ec + 1 + n, m\_ec \leftarrow s\_ec + 1 + n)}{210 \xrightarrow{\tau} 210}$$

$$WI_{645*}(n) = \frac{\{\}, True, (s\_ec \leftarrow s\_ec + 1 + n)}{220 \xrightarrow{\tau} 220}$$

$$WI_{7}(n) = \frac{\{\}, True, (r\_msg \leftarrow s\_msg, r\_ec \leftarrow s\_ec + n)}{210 \xrightarrow{\tau} 201}$$

$$WI_{7a}(n) = \frac{\{\}, True, (r\_msg \leftarrow s\_msg, r\_ec \leftarrow m\_ec + n)}{220 \xrightarrow{\tau} 201}$$

$$\forall n \ge 1. WI_{7b}(n) = \frac{\{\}, True, (r\_msg \leftarrow m\_msg, r\_ec \leftarrow s\_ec + n)}{100 \xrightarrow{\tau} 201}$$

$$WI_{8} = \frac{\{Q \to q\text{-recv}(r1\_msg, r1\_ec)\}, True, ()}{201 \xrightarrow{\text{out}(r1\_msg, r1\_ec)} \{202, 000\}}$$

$$\forall n \ge 1. WI_{8a}(n) = \frac{\{Q \to q\text{-recv}(m\_msg, m\_ec + n)\}, True, ()}{210 \xrightarrow{\text{out}(m\_msg, m\_ec + n)} \{202, 000\}}$$

$$\forall n \ge 1. WI_{8b}(n) = \frac{\{Q \to q\text{-recv}(s\_msg, s\_ec + n)\}, True, ()}{220 \xrightarrow{\text{out}(s\_msg, s\_ec + n)} \{202, 000\}}$$
$$ \forall n \geq 1. WI_{8c}(n) = \frac{\{Q \to q-recv(s\_msg, s\_ec + n)\}, True, ()}{100 \underset{\text{out}(s\_msg, s\_ec+n)}{\longrightarrow} \{202, 000\}} $$

Then for all $\tau$ transitions above we have a similar WOT that include a non-$\tau$ move from an external action of $P$ or $Q$, like for example:

$$ \{P \to p-a\}, [\forall x.p-a \neq p-send(x)], $$

$$ WI_4 P(n) = \frac{(m\_msg \leftarrow s\_msg, m\_ec \leftarrow s\_ec + n, s\_ec \leftarrow s\_ec + n)}{100 \underset{p \to a}{\longrightarrow} 210} $$

$$ \{Q \to q-b\}, [\forall x,y.q-b \neq q-recv(x,y)], $$

$$ (m\_msg \leftarrow s\_msg, m\_ec \leftarrow s\_ec + n, s\_ec \leftarrow s\_ec + n) $$

$$ \text{and } WI_4 Q(n) = \frac{}{100 \underset{q \to b}{\longrightarrow} 210} $$

but also e.g.:

$$ WI_{456*} P(n) = \frac{\{P \to p-a\}, [\forall x.p-a \neq p-send(x)], (s\_msg \leftarrow s\_msg, s\_ec \leftarrow s\_ec + n)}{100 \underset{p \to a}{\longrightarrow} 100} $$

The following table give a summary of WOTs, when sharing their names as much as possible.

<table><thead><tr><th>WOT name</th><th>Pairs of source states and target states</th><th># WOTs</th></tr></thead><tbody><tr><td>WI<sub>1</sub> WI<sub>2</sub> WI<sub>τ</sub></td><td>{(s, s)|s∈States of WOA}∪{(202,000)}</td><td>21</td></tr><tr><td>WI<sub>3</sub>(n)</td><td>{(202,100),(000,100)}</td><td>2</td></tr><tr><td>WI<sub>3a</sub>(n)</td><td>{(202,210),(000,210)}</td><td>2</td></tr><tr><td>WI<sub>3b</sub>(n)</td><td>{(202,220),(000,220)}</td><td>2</td></tr><tr><td>WI<sub>3c</sub>(n)</td><td>{(202,201),(000,201)}</td><td>2</td></tr><tr><td>WI<sub>4</sub>(n) WI<sub>4</sub>(n) WI<sub>4</sub>(n) WI<sub>4</sub>(n)</td><td>{(100,210)}</td><td>3</td></tr><tr><td>WI<sub>4a</sub>(n) WI<sub>4a</sub>(n) WI<sub>4a</sub>(n) WI<sub>4a</sub>(n)</td><td>{(100,220)}</td><td>3</td></tr><tr><td>WI<sub>456*</sub>(n) WI<sub>456*</sub>(n) WI<sub>456*</sub>(n) WI<sub>456*</sub>(n)</td><td>{(100,100)}</td><td>3</td></tr><tr><td>WI<sub>5</sub>(n) WI<sub>5</sub>(n) WI<sub>5</sub>(n) WI<sub>5</sub>(n)</td><td>{(210,220)}</td><td>3</td></tr><tr><td>WI<sub>5a</sub>(n) WI<sub>5a</sub>(n) WI<sub>5a</sub>(n) WI<sub>5a</sub>(n)</td><td>{(210,100)}</td><td>3</td></tr><tr><td>WI<sub>564*</sub>(n) WI<sub>564*</sub>(n) WI<sub>564*</sub>(n) WI<sub>564*</sub>(n)</td><td>{(210,210)}</td><td>3</td></tr><tr><td>WI<sub>6</sub>(n) WI<sub>6</sub>(n) WI<sub>6</sub>(n) WI<sub>6</sub>(n)</td><td>{(220,100)}</td><td>3</td></tr><tr><td>WI<sub>6a</sub>(n) WI<sub>6a</sub>(n) WI<sub>6a</sub>(n) WI<sub>6a</sub>(n)</td><td>{(220,210)}</td><td>3</td></tr><tr><td>WI<sub>645*</sub>(n) WI<sub>645*</sub>(n) WI<sub>645*</sub>(n) WI<sub>645*</sub>(n)</td><td>{(220,220)}</td><td>3</td></tr><tr><td>WI<sub>7</sub>(n) WI<sub>7</sub>(n) WI<sub>7</sub>(n) WI<sub>7</sub>(n)</td><td>{(210,201)}</td><td>3</td></tr><tr><td>WI<sub>7a</sub>(n) WI<sub>7a</sub>(n) WI<sub>7a</sub>(n) WI<sub>7a</sub>(n)</td><td>{(220,201)}</td><td>3</td></tr><tr><td>WI<sub>7b</sub>(n) WI<sub>7b</sub>(n) WI<sub>7b</sub>(n) WI<sub>7b</sub>(n)</td><td>{(100,201)}</td><td>3</td></tr><tr><td>WI<sub>8</sub>(n)</td><td>{(201,202),(201,000)}</td><td>2</td></tr><tr><td>WI<sub>8a</sub>(n)</td><td>{(201,202),(201,000)}</td><td>2</td></tr><tr><td>WI<sub>8b</sub>(n)</td><td>{(220,202),(220,000)}</td><td>2</td></tr><tr><td>WI<sub>8c</sub>(n)</td><td>{(100,202),(100,000)}</td><td>2</td></tr></tbody></table>

That makes a total of 73 WOTs in the open automaton for *SimpleProtocolImpl*.
Appendix C.1. Details of the FH-bisimulation checking

We recall here the relation $\mathcal{R}$ that is the candidate for our weak FH-bisimulation relation:

<table><thead><tr><th>SimpleProtocolSpec<br>states</th><th>SimpleProtocolImpl<br>states</th><th>Predicate</th></tr></thead><tbody><tr><td>b0</td><td>000</td><td>True</td></tr><tr><td>b0</td><td>202</td><td>True</td></tr><tr><td>b1</td><td>100</td><td>b_msg = s_msg &amp; b_ec = s_ec</td></tr><tr><td>b1</td><td>210</td><td>b_msg = m_msg &amp; b_ec = m_ec</td></tr><tr><td>b1</td><td>220</td><td>b_msg = s_msg &amp; b_ec = s_ec</td></tr><tr><td>b1</td><td>201</td><td>b_message = r_message &amp; b_ec = r_ec</td></tr></tbody></table>

Consider the first triple `<b0, 000, True>`, we have to prove the following 6 properties, in which `OT << WOT` means that the (strong) open transition `OT` is covered, in the sense of Definition 14, by the weak transition `WOT` (it could be a set, but this will not be used here):

SS₁ << WI₁      SI₁ << WS₁
SS₂ << WI₂      SI₂ << WS₂
SS₃ << WI₃      SI₃ << WS₃

Note that if we were using the alternative weak FH-bisimulation relation from Appendix B.1, Lemma 4, that is checking strong FH-bisimulation between the corresponding weak automaton, we would have a more transitions coverage to examine, as we have 4 weak transitions for `b0` in the `SimpleProtocolSpec` weak automaton, and 7 WOTs (including 4 parameterised WOTs) from 000 in the `SimpleProtocolImpl` automaton.

Preliminary remarks:

* Both pNets trivially verify the “non-observability” condition: the only vectors having $\tau$ as an action of a sub-net are of the form “$< -, \tau, - \to \tau$”.

* We must take care of variable name conflicts: in our example, the variables of the 2 systems already have different names, but the action parameters occurring in the transitions (m, msg, ec) are the same, that is not correct. Recall that we disambiguate the reference to the variable `m` into `m1` for `SimpleProtocolSpec` and `m2` for `SimpleProtocolImpl`.

In our running example in page 34, we have shown the proof for one of the transitions of `(b0, 202, True)`, namely that `SS₃` is covered by `WI₃(0)`. We give here another example with `SS₁ << WI₁`, from the first triple `(b0, 000, True)`. It includes less trivial predicates in the OTs:

$$SS_1 = \{ \mathbf{P} \to \mathbf{p}-\mathbf{a}1 \}, [ \forall \mathbf{m}1. \mathbf{p}-\mathbf{a}1 \neq \mathbf{p}-\mathbf{send}(\mathbf{m}1) ], () \\ \mathbf{b}0 \xrightarrow{\mathbf{p}-\mathbf{a}1} \mathbf{b}0$$
$$WI_1 = \frac{\{P \to P \text{ - a2}\}, [\forall m2 \text{ . } P \text{ - a2} \neq \text{ p - send (m2)}], ()} {000 \overset{P \text{ - a2}}{\rightleftharpoons} 000}$$

Let us check formally the conditions:

* Their sets of active (non-silent) holes is the same: $J' = J_x = \{P\}$.

* Triple (b0, 000, True) is in $\mathcal{R}$.

* The verification condition

$$\forall fv_{OT}. \{Pred \land Pred_{OT} \implies \bigvee_{x \in X} [\exists fv_{OT_x}. (\forall j \in J_x. (\beta_j)^\nabla = \gamma_{jx} \land Pred_{OT_x} \land \alpha = \alpha_x \land Pred_{s',t_x} \{Post_{OT} \uplus Post_{OT_x}\})] \}$$

Gives us:

$$\forall \mathbf{p}-\mathbf{a}1. \{ \mathbf{True} \land \forall \mathbf{m}1. \mathbf{p}-\mathbf{a}1 \neq \mathbf{p}-\mathbf{send}(\mathbf{m}1) \\ \implies \exists \mathbf{p}-\mathbf{a}2. (\mathbf{p}-\mathbf{a}1 = \mathbf{p}-\mathbf{a}2 \land \forall \mathbf{m}2. \mathbf{p}-\mathbf{a}2 \neq \mathbf{p}-\mathbf{send}(\mathbf{m}2) \land \mathbf{p}-\mathbf{a}1 = \mathbf{p}-\mathbf{a}2 \land \mathbf{True} \}$$

That is trivially true, choosing $\mathbf{p}-\mathbf{a}2=\mathbf{p}-\mathbf{a}1$ for each given $\mathbf{p}-\mathbf{a}1$.

All others pairs from this set are just as easily proven true.