relation of ACCS. This is out of the scope of our discussion, and we point the in-
terested reader to Lemma 1.4.15 of [87], and to the list of problems presented on
the web-page of THE CONCURRENT CALCULI FORMALISATION BENCHMARK.<fnref n="14" />
We give a corollary that is useful to prove Lemma 55.

**Corollary 5.** For every $p, q \in \mathbf{ACCS}$, and $\alpha \in \mathbf{Act}_{\tau}$. $p \equiv q$ implies that $p \xrightarrow{\alpha} \cdot \equiv r$ if and only if $q \xrightarrow{\alpha} \cdot \equiv r$.

*Proof.* Since $q \equiv p \xrightarrow{\alpha} p' \equiv r$ Lemma 54 implies $q \xrightarrow{\alpha} \cdot \equiv p'$, thus $q \xrightarrow{\alpha} \cdot \equiv r$ by transitivity of $\equiv$. The other implication follows from the same argument and the symmetry of $\equiv$.

A consequence of Lemma 53 is that the LTS $\langle \mathbf{ACCS}_{\equiv}, \rightarrow_{\equiv}, \mathbf{Act}_{\tau} \rangle$ enjoys the axioms in Figure 2, and thus it is FDB. [90, Theorem 4.3] proves it reasoning modulo bisimilarity, while we reason modulo structural equivalence.

**Lemma 55.** For every $p \in \mathbf{ACCS}$, and $a \in \mathcal{N}$ the following properties are true,

- for every $\alpha \in \mathbf{Act}_{\tau}$. $p \xrightarrow{\bar{a}} \alpha \xrightarrow{\alpha} p_3$ implies $p \xrightarrow{\bar{a}} \alpha \xrightarrow{\bar{a}} \cdot \equiv p_3$;

- for every $\alpha \in \mathbf{Act}_{\tau}$. $\alpha \notin \{\tau, \bar{a}\}$. $p \xrightarrow{\bar{a}} p'$ and $p \xrightarrow{\alpha} p''$ imply that $p'' \xrightarrow{\bar{a}} q$ and $p' \xrightarrow{\alpha} q$ for some $q$;

- $p \xrightarrow{\bar{a}} p'$ and $p \xrightarrow{\bar{a}} p''$ imply $p' \equiv p''$;

- $p \xrightarrow{\bar{a}} p'$ and $p \xrightarrow{\alpha} q$ implies $p \xrightarrow{\tau} \cdot \equiv q$;

- $p \xrightarrow{\bar{a}} p'$ and $p \xrightarrow{\tau} p''$ imply that $p' \xrightarrow{\tau} q$ and $p'' \xrightarrow{\bar{a}} q$; or that $p' \xrightarrow{\tau} p''$.

- for every $p'$ if there exists a $\hat{p}$ such that $p \xrightarrow{\bar{a}} \hat{p}$ and $p' \xrightarrow{\bar{a}} \hat{p}$ then $p \equiv p'$

*Proof.* To show FEEDBACK we begin via Lemma 53 which proves $p \equiv p' \parallel \bar{a}$. We derive $p' \parallel \bar{a} \xrightarrow{\tau} q'$ and apply Corollary 5 to obtain $p \xrightarrow{\tau} \cdot \equiv q$.

We prove OUTPUT-TAU. The hypothesis and Lemma 53 imply that $p \equiv p' \parallel \underline{a}$. Since $p \xrightarrow{\tau} p''$ it must be the case that $p' \xrightarrow{\tau} \hat{p}$ for some $\hat{p}$, and $p'' = \hat{p} \parallel \underline{a}$. Let $q = \hat{p}$. We have that $p'' \xrightarrow{a} \hat{p} \parallel 0 \equiv q$.

Processes that enjoy OUTPUT-TAU are called non-preemptive in [40, Definition 10].

Each time a process $p$ reduces to a stable process $p'$, it does so by consuming at least part of the mailbox, for instance a multiset of outputs $N$, thereby arriving in a state $q$ whose inputs cannot interact with what remains of the mailbox, i.e. $M \setminus N$, where $M$ is the original mailbox.

**Lemma 56.** For every $M \in \mathbf{MO}$, $p, p' \in \mathbf{ACCS}$, if $p \parallel \underline{\Pi M} \stackrel{\epsilon}{\implies} p' \xrightarrow{\tau} \underline{\tau}$ then there exist an $N \subseteq M$ and some $q \in \mathbf{ACCS}$ such that $p \stackrel{\underline{N}}{\implies} q \xrightarrow{\underline{\tau}} \underline{\tau}$, $O(q) \subseteq O(p')$, and $\overline{I(q)} \#(M \setminus N)$.

<footnote n="14">¹⁴ https://concurrentbenchmark.github.io/</footnote>
*Proof.* By induction on the derivation of $p \parallel \Pi M \stackrel{\epsilon}{\implies} p'$. In the base case this is due to [WT-REFL], which ensures that

$$p \parallel \Pi M = p',$$

from which we obtain $p \parallel \Pi M \xrightarrow{\tau} p'$. This ensures that $\overline{I(p)} \# M$. We pick as $q$ and $N$ respectively $p \parallel \Pi M$ and $\emptyset$ as $p \parallel \Pi M \stackrel{\emptyset}{\implies} p \parallel \Pi M$ by reflexivity, and $O(p \parallel \Pi M) = O(p')$.

In the inductive case the derivation ends with an application of [WT-TAU] and

$$\frac{p \parallel \Pi M \xrightarrow{\tau} p' \qquad \overline{p' \stackrel{\epsilon}{\implies} p'}}{p \parallel \Pi M \stackrel{\epsilon}{\implies} p'} \qquad \vdots$$

We continue by case analysis on the rule used to infer the transition $p \parallel \Pi M \xrightarrow{\tau} p'$. As by definition $\Pi M \xrightarrow{\tau} p'$, the rule is either [PAR-L], i.e. a $\tau$-transition performed by $p$, or [COM], i.e. an interaction between $p$ and $\Pi M$.

*Rule [PAR-L]:* In this case $p \xrightarrow{\tau} p''$ for some $p''$, thus $p'' \parallel \Pi M \stackrel{\epsilon}{\implies} p'$ and the result follows from the inductive hypothesis.

*Rule [COM]:* The hypothesis of the rule ensure that $p \xrightarrow{a} p''$ and $\Pi M \xrightarrow{\bar{a}} p'$, and as the process $\Pi M$ does not perform any input, it must be the case that $a \in \mathcal{N}$, that $\bar{a} \in M$, and that $q \equiv \Pi(M \setminus \{\bar{a}\})$.<fnref n="15" /> Note that $p' \equiv p'' \parallel \Pi(M \setminus \{\bar{a}\})$.

The inductive hypothesis ensures that for some $N' \subseteq M \setminus \{\bar{a}\}$ and some $q_3 \in \text{ACCS}$ we have

(a) $p' \stackrel{N'}{\implies} q_3 \xrightarrow{\tau},$

(b) $O(q_3) \subseteq O(p')$, and

(c) $\overline{I(q_3)} \# (M \setminus \{\bar{a}\}) \setminus N'$

We conclude by letting $q = q_3$, and $N = \{\bar{a}\} \uplus N'$. The trace $p \xrightarrow{a} p' \stackrel{N'}{\implies} q_3$ proves that $p \stackrel{\{\bar{a}\} \uplus N'}{\implies} q_3$, moreover we already know that $q_3$ is stable. The set inclusion $O(q_3) \subseteq O(p')$ follows from b, and lastly $\overline{I(q)} \# (M \setminus (\{\bar{a}\} \uplus N'))$ is a consequence of $\overline{I(q_3)} \# (M \setminus \{\bar{a}\}) \setminus N'$ and of $(M \setminus \{\bar{a}\}) \setminus N' = (\overline{I(\{\bar{a}\})} \uplus N')$.

We define the predicate *GOOD*,

GOOD(1)

GOOD($p \parallel q$) if GOOD($p$) or GOOD($q$)

GOOD($p + q$) if GOOD($p$) or GOOD($q$)

This predicate is preserved by structural congruence.

<footnote n="15">¹⁵ In terms of LTS with mailboxes, $p' = (M \setminus \{\bar{a}\})$.</footnote>
**Lemma 57.** For every $p, q \in \mathbf{ACCS}$. $p \equiv q$ and $\mathbf{GOOD}(p)$ imply $\mathbf{GOOD}(q)$.

**Lemma 58.** For every $p, q \in \mathbf{ACCS}$. $p \equiv q$ and $p \downarrow_i$ imply $q \downarrow_i$.

**Lemma 59.** For every $p, q \in \mathbf{ACCS}$ and $s \in \mathbf{Act}^*$, we have that $p \equiv q$ and $\mathbf{FW}(p) \downarrow s$ imply $\mathbf{FW}(q) \downarrow s$.

**Lemma 60.** For every $p, r, r' \in \mathbf{ACCS}$. $r \equiv r'$ and $p \mathbf{MUST}_i r$ then $p \mathbf{MUST}_i r'$.

**Lemma 61.** For every $p, q, r \in \mathbf{ACCS}$. $p \equiv q$ and $p \mathbf{MUST}_i r$ then $q \mathbf{MUST}_i r$.

A typical technique to reason on the LTS of concurrent processes, and so also of client-server systems, is trace zipping: if $p \stackrel{s}{\Rightarrow} p'$ and $q \stackrel{\bar{s}}{\Rightarrow} q'$, an induction on $s$ ensures that $p \parallel q \implies p' \parallel q'$. Zipping together different LTS is slightly more delicate: we can zip weak transitions $\stackrel{s}{\Rightarrow}_{\mathbf{fw}}$ together with the co-transitions $\stackrel{\bar{s}}{\Rightarrow}$, but possibly moving inside equivalence classes of $\equiv$ instead of performing actual transitions in $\to$.

**Lemma 62 (Zipping).** For every $p, q \in \mathbf{ACCS}$

1. for every $\mu \in \mathbf{Act}$. if $p \xrightarrow{\mu} \mathbf{fw}$ $p'$ and $q \xrightarrow{\bar{\mu}} q'$ then $p \parallel q \xrightarrow{\tau} p' \parallel q'$ or $p \parallel q \equiv p' \parallel q'$;

2. for every $s \in \mathbf{Act}^*$. if $p \stackrel{s}{\Rightarrow}_{\mathbf{fw}} p'$ and $q \stackrel{\bar{s}}{\Rightarrow} q'$ then $p \parallel q \stackrel{\varepsilon}{\Rightarrow} \equiv p' \parallel q'$.

Obviously, for every $p, q \in A$ and output $a \in \mathcal{N}$ we have

$$p \xrightarrow{\tau} \mathbf{fw} q \text{ if and only if } p \xrightarrow{\tau} q \qquad (12)$$

$$p \stackrel{\varepsilon}{\Rightarrow}_{\mathbf{fw}} q \text{ if and only if } p \stackrel{\varepsilon}{\Rightarrow} q \qquad (13)$$

$$p \xrightarrow{\bar{a}} \mathbf{fw} q \text{ if and only if } p \xrightarrow{\bar{a}} q \qquad (14)$$

together with the expected properties of finiteness, the first one amounting to the finiteness of the global mailbox in any state:

$$| \{ \bar{a} \in \bar{\mathcal{N}} \mid p \xrightarrow{\bar{a}}_{\mathbf{fw}} \} | \in \mathbb{N} \qquad (15)$$

$$\text{For every } \mu \in \mathbf{Act}. \quad |\{q \mid p \xrightarrow{\mu} \mathbf{fw} q\}| \in \mathbb{N} \qquad (16)$$

$$| \{ q \in A \mid p \xrightarrow{\tau} \mathbf{fw} q \} | \in \mathbb{N} \qquad (17)$$

## H.2 Client generators and their properties

This subsection is devoted to the study of the semantic properties of the clients produced by the function $g$. In general these are the properties sufficient to obtain our completeness result.

**Lemma 63.** For every $p \in \mathbf{ACCS}$ and $s \in \mathbf{Act}^*$, if $p \xrightarrow{\tau} q$ then $g(p, s) \xrightarrow{\tau} q$.
$$
\begin{align*}
g(\varepsilon, r) &= r \\
g(a.s, r) &= \bar{a} \parallel g(s, r) \\
g(\bar{a}.s, r) &= a.g(s, r) + \tau. 1
\end{align*}
$$

$$
c(s) = g(s, \tau. 1) \tag{18}
$$

$$
ta(s, L) = g(s, h(L)) \text{ where } h(L) = \Pi\{\mu.1 \mid \mu \in L\} \quad (19)
$$

**Fig. 16.** Functions to generate clients.

*Proof.* By induction on the sequence *s*. In the base case *s* = *ε*. The test generated by *g* is *p*, which reduces by hypothesis, and so does *g*(*ε*, *p*). In the inductive case *s* = *α*.s₂, and we proceed by case-analysis on *α*. If *α* is an output then *g*(*α*.s₂,*p*) = *α*.(*g*(*s₂*,*p*)) + *τ*.1 which reduces to 1 using the transition rule [SUM-R]. If *μ* is an input then *g*(*α*.s₂,*p*) = *α* || *g*(*s₂*,*p*) which reduces using the transition rule [PAR-R] and the inductive hypothesis, which ensures that *g*(*s₂*,*p*) reduces.

**Lemma 64.** For every *p* and *s*, if $\neg\text{GOOD}(p)$ then for every *s*, $\neg\text{GOOD}(g(s, p))$.

*Proof.* The argument is essentially the same of Lemma 63

**Lemma 65.** For every $s \in \text{Act}^*$, if $g(s, q) \xrightarrow{\mu} o$ then either

(a) $q \xrightarrow{\mu} q'$, $s \in \mathcal{N}^*$, and $o = \Pi \bar{s} \parallel q'$, or

(b) $s = s_1 \bar{\mu} s_2$ for some $s_1 \in \mathcal{N}^*$ and $s_2 \in \text{Act}^*$, and $o = \Pi \bar{s_1} \parallel g(s_2, q)$, and

(i) $\mu \in \mathcal{N}$ implies $g(s, q) \equiv \Pi \bar{s_1} \parallel (\tau.1 + \mu.g(s_2, q)),$

(ii) $\mu \in \overline{\mathcal{N}}$ implies $g(s, q) \equiv \Pi \bar{s_1} \parallel \mu \parallel (\tau.1 + \mu.g(s_2, q))$.

*Proof.* The proof is by induction on *s*.

In the case, $s = \varepsilon$, and hence by definition $g(s,q) = q$. The hypotheses
$g(s,q) \xrightarrow{\mu} o$ implies $q \xrightarrow{\mu} o$, and $o \equiv \mathbf{0} \parallel o \equiv \Pi\varepsilon \parallel o$.

In the inductive case, $s = \nu.s'$. We have two cases, depending on whether $\nu$
is an output action or an input action.

Suppose $\nu$ is an output. In this case $g(s,q) = \tau.1 + \bar{\nu}.g(s',q)$. The hypothesis $g(s,q) \xrightarrow{\mu} o$ ensures that $\bar{\nu} = \mu$, thus $\mu$ is an input action. By letting $s_1 = \varepsilon$ and $s_2 = s'$ we obtain the required

$$
g(s, q) = \tau.1 + \mu.g(s_2, q) \equiv \Pi \bar{s_1} \parallel (\tau.1 + \mu.g(s_2, q))
$$

and $o \equiv \Pi \bar{s}_1 \parallel g(s_2, q)$.

Now suppose that $\nu$ is an input action. By definition

$$
g(s, q) = \bar{v} \parallel g(s', q) \tag{20}
$$

and the inductive hypothesis ensures that either
(1) $q \xrightarrow{\mu} q', s' \in \mathcal{N}^*$, and $o' = \Pi \overline{s'} \parallel q'$, or

(2) $s' = s'_1 \cdot \overline{\mu} \cdot s'_2$, for some $s'_1 \in \mathcal{N}^*$ and $s_2 \in \mathbf{Act}^*$, and

$$o' \equiv \Pi \overline{s'_1} \parallel g(s'_2, q) \qquad (21)$$

and

$$\mu \in \mathcal{N} \text{ implies } g(s', q) \equiv \Pi \overline{s'_1} \parallel (\tau.1 + \mu.g(s'_2, q)) \qquad (22)$$

$$\mu \in \overline{\mathcal{N}} \text{ implies } g(s', q) \equiv \Pi \overline{s'_1} \parallel \mu \parallel (\tau.1 + \mu.g(s'_2, q)) \qquad (23)$$

The action $\mu$ is either an input or an output, and we organise the proof accordingly.

Suppose $\mu$ is an input. Since $\overline{\nu}$ is an output, the transition $g(s, q) \xrightarrow{\mu} o$ must be due to a transition $g(s', q) \xrightarrow{\mu} o'$, thus Equation (20) implies

$$o = \overline{\nu} \parallel o' \qquad (24)$$

In case 1, then $s' \in \mathcal{N}^*$ and $\nu \in \mathcal{N}$ ensure $s \in \mathcal{N}^*$ and the equality $o \equiv \Pi \overline{s} \parallel q'$ follows from $o' = \Pi \overline{s'} \parallel q'$ and Equation (24).

In case 2, let $s_1 = \nu.s'_1$, $s_2 = s'_2$. Since $\nu$ is an input we have $s_1 \in \mathcal{N}^*$. The equalities $s = \nu.s'$ and $s' = s'_1 \cdot \overline{\mu} \cdot s'_2$ imply that $s = s_1 \overline{\mu} s_2$. The required $o \equiv \Pi \overline{s_1} \parallel g(s'_2, q)$ follows from $o' \equiv \Pi \overline{s'_1} \parallel g(s'_2, q)$ and Equation (24).

Now we proceed as follows,

$$
\begin{align*}
g(s, q) &= \overline{\nu} \parallel g(s', q) && \text{By Equation (20)} \\
&\equiv \overline{\nu} \parallel (\Pi \overline{s'_1} \parallel (\tau.1 + \mu.g(s'_2, q))) && \text{By Equation (22)} \\
&\equiv (\overline{\nu} \parallel \Pi \overline{s'_1}) \parallel (\tau.1 + \mu.g(s'_2, q)) && \text{Associativity} \\
&\equiv \Pi \overline{s_1} \parallel (\tau.1 + \mu.g(s'_2, q)) && \text{Because } s_1 = \nu.s'_1 \\
&\equiv \Pi \overline{s_1} \parallel (\tau.1 + \mu.g(s_2, q)) && \text{Because } s_2 = s'_2
\end{align*}
$$

Now suppose that $\mu$ is an output. Then either $\overline{\nu} = \mu$ or $\overline{\nu} \neq \mu$.

In the first case we let $s_1 = \varepsilon$ and $s_2 = s'$. Equation (20) and $\overline{\nu} = \mu$ imply $g(s, q) = \mu \parallel g(s_2, q)$ from which we obtain the required $g(s, q) \equiv \Pi \overline{s_1} \parallel \mu \parallel g(s_2, q)$, and $o \equiv \Pi \overline{s_1} \parallel g(s_2, q)$.

If $\overline{\nu} \neq \mu$ then Equation (20) ensures that the transition $g(s, q) \xrightarrow{\mu} o$ must be due to $g(s', q) \xrightarrow{\mu} o'$ and Equation (24) holds. We use the inductive hypothesis.
If 1 is true, we proceed as already discussed. In case 2 holds, let $s_1 = \nu.s'_1$, we have that $s_1 \in \mathcal{N}^*$. Let $s_2 = s'_2$, now we have that

$$
\begin{align*}
g(s, q) &= \overline{\nu} \parallel g(s', q) && \text{By Equation (20)} \\
&\equiv \overline{\nu} \parallel (\Pi \overline{s'_1} \parallel \mu \parallel g(s'_2, q)) && \text{By Equation (23)} \\
&\equiv (\overline{\nu} \parallel \Pi \overline{s'_1}) \parallel \mu \parallel g(s'_2, q) && \text{Associativity} \\
&= \Pi \overline{s_1} \parallel \mu \parallel g(s'_2, q) && \text{Because } s_1 = \nu.s'_1 \\
&= \Pi \overline{s_1} \parallel \mu \parallel g(s_2, q) && \text{Because } s_2 = s'_2
\end{align*}
$$

**Lemma 66.** For every $s \in \mathbf{Act}^*$, if $g(s, q) \xrightarrow{\mu} p$ then either:

(a) there exists $q'$ such that $q \xrightarrow{\mu} q'$, $s \in \mathcal{N}^*$ with $p \equiv \Pi \bar{s} \parallel q'$, or

(b) $s = s_1 \cdot \bar{\mu} \cdot s_2$ for some $s_1 \in \mathcal{N}^*$ and $s_2 \in \mathbf{Act}^*$ with $p \equiv g(s_1 \cdot s_2, q)$.

*Proof.* The proof is by induction over the sequence s.

In the base case $s = \varepsilon$ and we have $g(\varepsilon, q) = q$. We show part (a) and choose $q' = p$. We have $g(\varepsilon, q) = q \xrightarrow{\mu} p$, $p \equiv \Pi \bar{\varepsilon} \parallel q'$ and $\varepsilon \in \mathcal{N}^*$ as required.

In the inductive case $s = \nu.s'$. We proceed by case-analysis on $\nu$. If $\nu$ is an input, then $g(\nu.s', q) = \bar{\nu} \parallel g(s', q)$. The hypothesis $g(\nu.s', q) \xrightarrow{\mu} p$ implies that either:

(i) $\bar{\nu} \xrightarrow{\mu} 0$ with $p = 0 \parallel g(s', q)$ and $\bar{\nu} = \mu$, or

(ii) $g(s', q) \xrightarrow{\mu} \hat{p}$ with $p = \bar{\nu} \parallel \hat{p}$.

In the first case we show part (b). We choose $s_1 = \varepsilon$, $s_2 = s'$. We have $s = \mu.s' = \bar{\nu}.s'$, $p = 0 \parallel g(s', q) \equiv g(\varepsilon.s', q)$ and $\varepsilon \in \mathcal{N}^*$ as required.

In the second case the inductive hypothesis tells us that either:

(H-a) there exists $q'$ such that $q \xrightarrow{\mu} q'$, $s' \in \mathcal{N}^*$ with $\hat{p} \equiv \Pi \bar{s}' \parallel q'$, or

(H-b) $s = s_1 \cdot \bar{\mu} \cdot s_2$ for some $s_1 \in \mathcal{N}^*$ and $s_2 \in \mathbf{Act}^*$ with $\hat{p} \equiv g(s_1 \cdot s_2, q)$.

part (a) or part (b) is true.

If part (a) is true then $s' \in \mathcal{N}^*$ and there exists $q''$ such that $q \xrightarrow{\mu} q''$ with $\hat{p} \equiv \Pi \bar{s}' \parallel q''$. We prove part (a). We choose $q' = q''$ and $s = \nu.s'$. We have $p \equiv \bar{\nu} \parallel \hat{p} \equiv \bar{\nu} \parallel \Pi \bar{s}' \parallel q'' \equiv \Pi \nu.s'$ and $\nu.s' \in \mathcal{N}^*$ as required.

If part (b) is true then $s' = s'_1 \cdot \bar{\mu} \cdot s'_2$ for some $s'_1 \in \mathcal{N}^*$ and $s'_2 \in \mathbf{Act}^*$ with $\hat{p} \equiv g(s'_1 \cdot s'_2, q)$. We prove part (a). We choose $s_1 = \nu.s'_1$ and $s_2 = s'_2$. We have $p \equiv \bar{\nu} \parallel \hat{p} \equiv \bar{\nu} \parallel g(s'_1 \cdot s'_2, q) \equiv g(\nu.s'_1 \cdot s'_2, q)$ as required.

If $\nu$ is an output, then $g(\nu.s', q) = \bar{\nu}.(g(s', q)) + \tau \cdot 1$. We prove part (b) and choose $s_1 = \varepsilon$, $s_2 = s'$. The hypothesis $g(\nu.s', q) \xrightarrow{\mu} p$ implies that $\mu = \bar{\nu}$ and $p \equiv g(s', q) \equiv g(\varepsilon.s', q)$ as required.

**Lemma 67.** For every $s \in \mathbf{Act}^*$, if $g(s, q) \xrightarrow{\tau} 0$ then either

(a) GOOD(o), or
(b) $s \in \mathcal{N}^*$, $q \xrightarrow{\tau} q'$, and $o = \Pi \bar{s} \parallel q'$, or

(c) $s \in \mathcal{N}^*$, $q \xrightarrow{\nu} q'$, and $s = s_1 \cdot \nu \cdot s_2$, and $o \equiv \Pi \overline{s_1 \cdot s_2} \parallel q'$, or

(d) $o \equiv g(s_1 \cdot s_2 \cdot s_3, q)$ where $s = s_1 \cdot \mu \cdot s_2 \cdot \bar{\mu} \cdot s_3$ with $s_1 \cdot \mu \cdot s_2 \in \mathcal{N}^*$.

*Proof.* By induction on the structure of $s$.

In the base case $s = \varepsilon$. We prove b. Trivially $s \in \mathcal{N}^*$, and by definition $g(\varepsilon, q) = q$, the hypothesis implies therefore that $q \xrightarrow{\tau} o$. The $q'$ we are after is $o$ itself, for $o \equiv 0 \parallel o = \Pi \bar{s} \parallel o$.

In the inductive case $s = \nu \cdot s'$. We proceed by case analysis on whether $\nu \in \overline{\mathcal{N}}$ or $\nu \in \mathcal{N}$.

If $\nu$ is an output, by definition $g(s, q) = \tau \cdot 1 + \bar{\nu} \cdot \text{gens}'q$. Since $\bar{\nu} \cdot g(s', q) \xrightarrow{\tau} o$, the silent move $g(s, q) \xrightarrow{\tau} o$ is due to rule [SUM-L], thus $o = 1 + \bar{\nu} \cdot g(s', q)$, and thus GOOD($o$). We have proven a.

Suppose now that $\nu$ is an input, by definition

$$g(s, q) = \bar{\nu} \parallel g(s', q) \qquad (25)$$

The silent move $g(s, q) \xrightarrow{\tau} o$ must have been derived via the rule [COM], or the rule [PAR-R].

If [COM] was employed we know that

$$\frac{\bar{\nu} \xrightarrow{\underline{\underline{\bar{\nu}}}} 0 \quad \vdots \quad \overline{g(s', q) \xrightarrow{\nu} o'}}{\bar{\nu} \parallel g(s', q) \xrightarrow{\tau} 0 \parallel o'}$$

and thus $o \equiv o'$. Since $\nu$ is an input and $g(s', q) \xrightarrow{\nu} o'$, Lemma 65 ensures that either

(1) $q \xrightarrow{\nu} q'$, $s' \in \mathcal{N}^*$, and $o' = \Pi \bar{s}' \parallel q'$, or

(2) $s' = s'_1 \cdot \bar{\nu} \cdot s'_2$ for some $s'_1 \in \mathcal{N}^*$ and $s'_2 \in \text{Act}^*$, and

$$o' \equiv \overline{\Pi s'_1} \parallel g(s'_2, q) \qquad (26)$$

$$g(s, q) \equiv \overline{\Pi s'_1} \parallel (\tau \cdot 1 + \nu \cdot g(s'_2, q)) \qquad (27)$$

In case 1 we prove part (c). Since $\nu$ is an input, $s' \in \mathcal{N}^*$ ensures that $s \in \mathcal{N}^*$. By letting $s_1 = \varepsilon$ and $s_2 = s'$ we obtain $s = s_1 \cdot \nu \cdot s_2$. We have to explain why $o \equiv \overline{\Pi s_1 \cdot s_2} \parallel q'$. This follows from the definitions of $s_1$ and $s_2$, from $o \equiv 0 \parallel o'$ and from $o' \equiv \overline{\Pi s'} \parallel q'$.

In case 2 we prove part (d). Let $s_1 = \varepsilon$, $s_2 = s'_1$ and $s_3 = s'_2$.

$s' = \nu s'_1 \cdot \bar{\nu} \cdot s'_2$ By inductive hypothesis

$\nu \cdot s' = \nu \cdot s'_1 \cdot \bar{\nu} \cdot s'_2$

$s = \nu \cdot s'_1 \cdot \bar{\nu} \cdot s'_2$ Because $s = \nu \cdot s'$

$s = s_1 \cdot \nu \cdot s_2 \cdot \bar{\nu} \cdot s_3$

By definition
and $s_1 \cdot \nu \cdot s_2 \in \mathcal{N}^*$ as required. Moreover $o' = \underline{\Pi s'_1} \parallel g(s'_2, q) = \underline{\Pi \bar{s}_2} \parallel g(s_3, q) = g(s_2 \cdot s_3, q) = g(s_1 \cdot s_2 \cdot s_3, q)$ as required. This concludes the argument due to an application of [COM].

If [PAR-R] was employed we know that

$$ \frac{\vdots}{\bar{\nu} \parallel g(s', q) \xrightarrow{\tau} \bar{\nu} \parallel o'} $$

thus $g(s', q) \xrightarrow{\tau} o'$ and

$$ o = \underline{\bar{\nu}} \parallel o' \qquad (28) $$

Since $s'$ is smaller than $s$, thanks to $g(s', q) \xrightarrow{\tau} o'$ we apply the inductive hypothesis to obtain either

(i) GOOD($o'$), or

(ii) $s' \in \mathcal{N}^*$, $q \xrightarrow{\tau} q'$, and $o' = \underline{\Pi \bar{s}'} \parallel q'$, or

(iii) $s' \in \mathcal{N}^*$, $q \xrightarrow{\mu} q'$, and $s' = s'_1 \cdot \mu \cdot s'_2$, or

(iv) $o' \equiv g(s'_1 \cdot s'_2 \cdot s'_3, q)$ where $s' = s'_1 \cdot \mu \cdot s'_2 \cdot \bar{\mu} \cdot s'_3$ with $s'_1 \cdot \mu \cdot s'_2 \in \mathcal{N}^*$,

If i then Equation (28) implies a. If ii then $s = \nu \cdot s'$ and the assumption that $\nu$ is input imply that $s \in \mathcal{N}^*$. Equation (28) and $o' = \underline{\Pi \bar{s}'} \parallel q'$ imply that $o = \underline{\Pi \bar{s}} \parallel q'$. We have proven b. If ii we prove b, because $s' \in \mathcal{N}^*$ ensures $s \in \mathcal{N}^*$ and $s' = s'_1 \cdot \mu \cdot s'_2$ let use prove $s = s_1 \cdot \nu \cdot s_2$ by letting $s_1 = \nu \cdot s'_1$ and $s_2 = s'_2$.

If iv we prove d. We have $o' \equiv g(s'_1 \cdot s'_2 \cdot s'_3, q)$ and $s' = s'_1 \cdot \lambda \cdot s'_2 \cdot \bar{\lambda} \cdot s'_3$ with $s'_1 \cdot \lambda \cdot s'_2 \in \mathcal{N}^*$.

Let $s_1 = \nu \cdot s'_1$, $s_2 = s'_2$ and $s_3 = s'_3$. Since $s'_1 \cdot \mu \cdot s'_2 \in \mathcal{N}^*$, we have $s_1 \cdot \mu \cdot s_2 \in \mathcal{N}^*$. We also have

$s' = s'_1 \cdot \mu \cdot s'_2 \cdot \bar{\mu} \cdot s'_3$ By inductive hypothesis

$$ \nu \cdot s' = \nu \cdot s'_1 \cdot \mu \cdot s'_2 \cdot \bar{\mu} \cdot s'_3 $$

$$ s = \nu \cdot s'_1 \cdot \mu \cdot s'_2 \cdot \bar{\mu} \cdot s'_3 $$

Because $s = \nu \cdot s'$

$$ s = s_1 \cdot \mu \cdot s_2 \cdot \bar{\mu} \cdot s_3 $$

By definition

It remains to prove that $o \equiv g(s_1 \cdot s_2 \cdot s_3, q)$. This is a consequence of Equation (28), of $o' \equiv g(s'_1 \cdot s'_2 \cdot s'_3, q)$, and of the definitions of $s_1$, $s_2$, and $s_3$.

**Lemma 68.** For every $s \in \text{Act}^*$, and process $q$ such that or $q \xrightarrow{\tau} q'$ implies GOOD($q'$), and for every $\mu \in \mathcal{N} \cdot q \xrightarrow{\mu} q'$ implies GOOD($q'$), if $g(s, q) = o_0 \xrightarrow{\tau} o_1 \xrightarrow{\tau} o_2 \xrightarrow{\tau} \dots o_n \xrightarrow{\tau} \text{and } n > 0$ then GOOD($o_i$) for some $i \in [1, n]$.

*Proof.* Lemma 67 implies that one of the following is true,

(a) GOOD($o_1$), or

(b) $s \in \mathcal{N}^*$, $q \xrightarrow{\tau} q'$, and $o_1 = \underline{\Pi \bar{s}} \parallel q'$, or
(c) $s \in \mathcal{N}^*$, $q \xrightarrow{\mu} q'$, and $s = s_1 \cdot \mu \cdot s_2$, and $o_1 \equiv \Pi \boxed{s_1 \cdot s_2} \parallel q'$, or

(d) $o_1 \equiv g(s_1 \cdot s_2 \cdot s_3, q)$ where $s = s_1 \cdot \mu \cdot s_2 \cdot \bar{\mu} \cdot s_3$ with $s_1 \cdot \mu \cdot s_2 \in \mathcal{N}$.

If a we are done. If b or c then GOOD($q'$), and thus GOOD($o_1$).

In the base case $len(s) = 0$, thus d is false. It follows that GOOD($o_1$).

In the inductive case $s = \nu \cdot s'$. We have to discuss only the case in which d is true. The inductive hypothesis ensures that

For every $s' \in \bigcup_{i=0}^{len(s)-1}$, if $g(s', q) \xrightarrow{\tau} o'_1 \xrightarrow{\tau} o'_2 \xrightarrow{\tau} \dots o'_m \xrightarrow{\tau} \text{ and } m > 0$ then
GOOD($o'_j$) for some $j$.

Note that $o_1 \xrightarrow{\tau}$ so the reduction sequence $o_1 \implies o_n$ cannot be empty, thus $m > 0$. This and $len(s_1 s_2 s_3) < len(s)$ let us apply the inductive hypothesis to state that

$g(s_1 \cdot s_2 \cdot s_3, q) \xrightarrow{\tau} o'_1 \xrightarrow{\tau} o'_2 \xrightarrow{\tau} \dots o'_m \xrightarrow{\tau} \text{ implies } o'_j \text{ for some } j$.

We conclude the argument via Lemma 54 and because $\equiv$ preserves success.

**Lemma 69.** For every $s \in \mathbf{Act}^*$ and process $q$, if $g(s, q) \xrightarrow{\tau} \text{ then}$

1. $s \in \mathcal{N}^*$,

2. $q \xrightarrow{\tau} \emptyset$,

3. $I(q) \cap \bar{s} = \emptyset$,

4. $R(g(s, q)) = \bar{s} \cup R(q)$.

*Proof.* By induction on $s$. In the base case $\varepsilon \in \mathcal{N}^*$, and $g(\varepsilon, q) = q$, thus $q \xrightarrow{\tau} \emptyset$. The last two points follow from this equality and from $\varepsilon$ containing no actions.

In the inductive case $s = \mu \cdot s'$. The hypothesis $g(\mu \cdot s', q) \xrightarrow{\tau} \text{ and the definition}$
of $g$ imply that $g(\mu \cdot s', q) = \bar{\mu} \parallel g(s', q)$, thus $\mu \in \mathcal{N}$. The inductive hypothesis
ensures that

1. $s' \in \mathcal{N}^*$,

2. $q \xrightarrow{\tau} \emptyset$,

3. for every $I(q) \cap \bar{s}' = \emptyset$,

4. for every $R(g(s', q)) = \bar{s}' \cup R(q)$

Since $\bar{\mu} \parallel g(s', q) \xrightarrow{\tau} \text{ rule [COM] cannot be applied, thus } q \xrightarrow{\mu} \emptyset$, and so $I(q) \cap \bar{s} = \emptyset$. From $R(g(s', q)) = \bar{s}' \cup R(q)$ we obtain $R(g(s, q)) = \bar{s} \cup R(q)$.

**Lemma 70.** For every $\mu \in \mathbf{Act}$, $s$ and $p$, $g(\mu \cdot s, p) \xrightarrow{\bar{\mu}} g(s, p)$.

*Proof.* We proceed by case-analysis on $\mu$. If $\mu$ is an input then $g(\mu \cdot s, p) = \bar{\mu} \parallel g(s, p)$. We have $\bar{\mu} \parallel g(s, p) \xrightarrow{\bar{\mu}} 0 \parallel g(s, p) \equiv g(s, p)$ as required. If $\mu$ is an output then $g(\mu \cdot s, p) = \bar{\mu} \cdot g(s, p) + \tau \cdot 1$. We have $\bar{\mu} \cdot g(s, p) + \tau \cdot 1 \xrightarrow{\bar{\mu}} g(s, p)$ as required.

**Lemma 71.** For every $s \in \mathbf{Act}^*$, and $q \in \mathbf{ACCS}$. $c(s) \xrightarrow{\tau}_{fw} q$ either
(a) GOOD($q$), or

(b) there exist $b, s_1, s_2$ and $s_3$ with $s_1.b.s_2 \in \mathcal{N}^*$ such that $s = s_1.b.s_2.b.s_3$ and $q \equiv c(s_1.s_2.s_3)$.

*Proof.* The proof is by induction on $s$.

In the base case $s = \varepsilon$, $c(\varepsilon) = \tau.1$ and then $q = 1$. We prove a with GOOD(1).

In the inductive case $s = \mu.s'$. We proceed by case-analysis over $\mu$.

If $\mu$ is an input then $c(\mu.s') = \bar{\mu} \parallel c(s')$. We continue by case-analysis over the reduction $\bar{\mu} \parallel c(s') \xrightarrow{\tau} q$. It is either due to:

(i) a communication between $\bar{\mu}$ and $c(s')$ such that $\bar{\mu} \xrightarrow{\bar{\mu}} 0$ and $c(s') \xrightarrow{\mu} q'$ with $q = 0 \parallel q'$, or

(ii) a reduction of $c(s')$ such that $c(s') \xrightarrow{\tau} q'$ with $q = \bar{\mu} \parallel q'$.

If i is true then Lemma 66 tells us that there exist $s'_1$ and $s'_2$ such that $s' = s'_1 \cdot \bar{\mu} \cdot s'_2$ and $q' \equiv c(s'_1.s'_2)$ with $s'_1 \in \mathcal{N}^*$. We prove (b). We choose $b = \mu, s_1 = \varepsilon, s_2 = s'_1, s_3 = s'_2$. We show the first requirement by $s = \mu.s' = \mu.s'_1 \cdot \bar{\mu} \cdot s'_2 = \varepsilon \cdot \mu.s'_1 \cdot \bar{\mu} \cdot s'_2 = s_1.b.s_2.b.s_3$. The second requirement is $q = 0 \parallel q' \equiv c(s'_1.s'_2) = c(\varepsilon.s'_1.s'_2) = c(s_1.s_2.s_3)$.

We now consider the case (ii). The inductive hypothesis tells us that either:

1. GOOD($q'$), or

2. there exist $\iota, s'_1, s'_2$ and $s'_3$ with $s'_1 \cdot \iota \cdot s'_2 \in \mathcal{N}^*$ such that $s' = s'_1 \cdot \iota \cdot s'_2 \cdot \bar{\iota} \cdot s'_3$ and $q' \equiv c(s'_1.s'_2.s'_3)$.

If (1) is true then we prove a with $q = \bar{\mu} \parallel q'$ and $\bar{\mu} \parallel q'$ and GOOD($q'$). If (2) is true then we prove (b). We choose $b = \iota, s_1 = \mu.s'_1, s_2 = s'_2, s_3 = s'_3$. We show the first requirement with $s = \mu.s' = \mu.s'_1 \cdot \iota \cdot s'_2 \cdot \bar{\iota} \cdot s'_3 = s_1.b.s_2.b.s_3$. The second requirement is $q = \bar{\mu} \parallel q' \equiv \bar{\mu} \parallel c(s'_1.s'_2.s'_3) = c(\mu.s'_1.s'_2.s'_3) = c(s_1.s_2.s_3)$.

If $\mu$ is an output then $c(\mu.s') = \bar{\mu}.(cs') + \tau.1$. The hypothesis $c(\mu.s') \xrightarrow{\tau} q$ implies $q = 1$. We prove (a) with GOOD(1).

## I Counter-example to existing completeness result

In this section we recall the definition of the alternative preorder $\ll_{ch}$ by [38], and show that it is not complete with respect to $\preceq_{MUST}$, i.e. $\preceq_{MUST} \not\subseteq \ll_{ch}$. We start with some auxiliary definitions.

The predicate $\rightsquigarrow^I$ is defined by the following two rules:

- $p \rightsquigarrow^I p$ if $p \xrightarrow{\tau} I$ and $I(p) \cap I = \emptyset$,

- $p \xrightarrow{I \uplus \{a\}} p''$ if $p \stackrel{a}{\Rightarrow} p'$ and $p' \rightsquigarrow^I p'$

The *generalised acceptance set* of a process $p$ after a trace $s$ with respect to a multiset of input actions $I$ is defined by

$$ \mathcal{G}A(p, s, I) = \{O(p'') \mid p \stackrel{s}{\Rightarrow_{fw}} p' \rightsquigarrow^I p''\} $$
The set of input multisets of a process $p$ after a trace $s$ is defined by

$$IM(p, s) = \{ \{a_1, \dots, a_n\} \mid a_i \in \mathcal{N}, p \underset{fw}{\stackrel{s}{\Rightarrow}} \stackrel{a_1}{\Rightarrow} \dots \stackrel{a_n}{\Rightarrow} \}$$

The convergence predicate over traces performed by forwarders is denoted $\Downarrow_a$, and defined as $\Downarrow$, but over the LTS given in Example 4.

The preorder $\ll_{ch}$ is now defined as follows:

**Definition 17 (Alternative preorder $\ll_{ch}$ [38]).** Let $p \ll_{ch} q$ if for every $s \in \text{Act}^*$. $p \Downarrow_a s$ implies

1. $q \Downarrow_a s$,

2. for every $R \in \mathcal{A}(q, s)$ and every $I \in IM(p, s)$ such that $I \cap R = \emptyset$ there exists some $O \in \mathcal{G}\mathcal{A}(p, s, I)$ such that $O \setminus \bar{I} \subseteq R$.

We illustrate the three auxiliary definitions using the process $\text{Pierre} = b.(\tau.\Omega + c.\bar{d})$ introduced in Example 3. We may infer that

$$\text{Pierre} \stackrel{\{b,c\}}{\rightsquigarrow} \bar{d} \qquad (29)$$

thanks to the following derivation tree

$$\begin{array}{r@{\quad}l}
\begin{array}{c}
\begin{tikzpicture}[baseline=(current bounding box.center), scale=0.4, every node/.style={scale=0.4}]
\node[circle, fill, inner sep=1pt] (top) at (0,0) {};
\node[circle, fill, inner sep=1pt] (bottom) at (0,0) {};
\draw[->] (top) -- (bottom);
\node[above=0.1cm of top] (top) {$\bar{d}$};
\node[below=0.1cm of bottom] (bottom) {$\bar{d}$};
\node[left=0.5cm of top] (left) {$\tau \to$};
\node[right=0.5cm of top] (right) {$\emptyset \to \emptyset$};
\node[above=0.1cm of left] (left) {$\bar{d}$};
\node[below=0.1cm of right] (right) {$\bar{d}$};
\end{tikzpicture}
& \text{and } I(\bar{d}) \cap \emptyset = \emptyset \\
\hline
\begin{tikzpicture}[baseline=(current bounding box.center), scale=0.4, every node/.style={scale=0.4}]
\node[circle, fill, inner sep=1pt] (top) at (0,0) {};
\node[circle, fill, inner sep=1pt] (bottom) at (0,0) {};
\draw[->] (top) -- (bottom);
\node[above=0.1cm of top] (top) {$\bar{d}$};
\node[below=0.1cm of bottom] (bottom) {$\bar{d}$};
\node[left=0.5cm of top] (left) {$\tau \to$};
\node[right=0.5cm of top] (right) {$\emptyset \to \emptyset$};
\node[above=0.1cm of left] (left) {$\bar{d}$};
\node[below=0.1cm of right] (right) {$\bar{d}$};
\end{tikzpicture}
\end{array}
& \qquad \tau.\Omega + c.\bar{d} \stackrel{c}{\Rightarrow} \bar{d} \\
\hline
\begin{tikzpicture}[baseline=(current bounding box.center), scale=0.4, every node/.style={scale=0.4}]
\node[circle, fill, inner sep=1pt] (top) at (0,0) {};
\node[circle, fill, inner sep=1pt] (bottom) at (0,0) {};
\draw[->] (top) -- (bottom);
\node[above=0.1cm of top] (top) {$\tau.\Omega + c.\bar{d} \stackrel{\{b,c\}}{\rightsquigarrow} \bar{d}$};
\node[below=0.1cm of bottom] (bottom) {$\tau.\Omega + c.\bar{d} \stackrel{\{b,c\}}{\rightsquigarrow} \bar{d}$};
\node[above=0.1cm of top] (top) {$\bar{d}$};
\node[below=0.1cm of bottom] (bottom) {$\bar{d}$};
\node[left=0.5cm of top] (left) {$\tau \to$};
\node[right=0.5cm of top] (right) {$\emptyset \to \emptyset$};
\node[above=0.1cm of left] (left) {$\bar{d}$};
\node[below=0.1cm of right] (right) {$\bar{d}$};
\end{tikzpicture}
& \qquad \text{Pierre} \stackrel{b}{\Rightarrow} \tau.\Omega + c.\bar{d} \\
\hline
\begin{tikzpicture}[baseline=(current bounding box.center), scale=0.4, every node/.style={scale=0.4}]
\node[circle, fill, inner sep=1pt] (top) at (0,0) {};
\node[circle, fill, inner sep=1pt] (bottom) at (0,0) {};
\draw[->] (top) -- (bottom);
\node[above=0.1cm of top] (top) {$\bar{d}$};
\node[below=0.1cm of bottom] (bottom) {$\bar{d}$};
\node[left=0.5cm of top] (left) {$\tau \to$};
\node[right=0.5cm of top] (right) {$\emptyset \to \emptyset$};
\node[above=0.1cm of left] (left) {$\bar{d}$};
\node[below=0.1cm of right] (right) {$\bar{d}$};
\end{tikzpicture}
& \qquad \text{Pierre} \stackrel{\{b,c\}}{\rightsquigarrow} \bar{d}
\end{array}$$

Let us now consider the generalised acceptance set of Pierre after the trace $\varepsilon$ with respect to the multiset $\{\{b, c\}\}$. We prove that

$$\mathcal{G}\mathcal{A}(\text{Pierre}, \varepsilon, \{\{b, c\}\}) = \{\{\bar{d}\}\} \qquad (30)$$

By definition $\mathcal{G}\mathcal{A}(\text{Pierre}, \varepsilon, \{\{b, c\}\}) = \{O(p'') \mid \text{Pierre} \stackrel{\varepsilon}{\Rightarrow}_{fw} p' \stackrel{\{b,c\}}{\rightsquigarrow} p''\}$. Since Pierre $\stackrel{\tau}{\to}$, we have

$$\mathcal{G}\mathcal{A}(\text{Pierre}, \varepsilon, \{\{b, c\}\}) = \{O(p'') \mid \text{Pierre} \stackrel{\{b,c\}}{\rightsquigarrow} p''\} \qquad (31)$$

Then, thanks to Equation (29) we get $O(\bar{d}) = \{\bar{d}\} \in \mathcal{G}\mathcal{A}(\text{Pierre}, \varepsilon, \{\{b, c\}\})$. We show now that $\{\bar{d}\}$ is the only element of this acceptance set. By (31) above, it is enough to show that Pierre $\stackrel{\{b,c\}}{\rightsquigarrow} p''$ implies $p'' = \bar{d}$. Observe that

1. $I(\text{Pierre}) \cap \{\{b, c\}\} \neq \emptyset$,

2. Pierre $\stackrel{a}{\Rightarrow}$ $p'$ implies $a = b$, and

3. There are two different states $p'$ such that Pierre $\stackrel{b}{\Rightarrow} p'$, but the only one that can do the input $c$ is $p' = \tau.\Omega + c.\bar{d}$.
This implies that the only way to infer Pierre $\underset{\sim}{\stackrel{\{b,c\}}{\rightleftharpoons}}$ p'' is via the derivation tree
that proves Equation (29) above. Thus $p'' = \bar{d}$.

**Counterexample 18** The alternative preorder $\ll_{ch}$ is not complete for $\preceq_{MUST}$,
namely $p \preceq_{MUST} q$ does not imply $p \ll_{ch} q$.

Proof. The cornerstone of the proof is the process Pierre = b.(τ.Ω + c.⟨d⟩) dis-
cussed above. In Example 3 we have shown that Pierre $\preceq_{MUST}$ 0. Here we show
that Pierre $\ll_{ch}$ 0, because the pair (Pierre, 0) does not satisfy Condition 2 of
Definition 17.

Since Pierre $\xrightarrow{\tau}$, we know that Pierre $\downarrow$, and thus by definition Pierre $\downarrow_a \varepsilon$.
We also have by definition $\mathcal{A}(0, \varepsilon) = \{\emptyset\}$, and $\mathrm{IM}(\mathrm{Pierre}, \varepsilon) = \{\emptyset, \{\!\!\{b\!\!\}\}, \{\!\!\{b, c\!\!\}\}\}$.

Let us check Condition 2 of Definition 17 for $p = \text{Pierre}$ and $q = 0$. Since there is a unique $R \in \mathcal{A}(0, \varepsilon)$, which is $\emptyset$, and $I \cap \emptyset = \emptyset$ for any $I$, we only have to check that for every $I \in \mathrm{IM}(\mathrm{Pierre}, \varepsilon)$ there exists some $O \in \mathcal{G}\mathcal{A}(\mathrm{Pierre}, \varepsilon, I)$ such that $O \setminus \bar{I} \subseteq \emptyset$.

Let $I = \{\!\!\{b, c\!\!\}\}$. By Equation (30) it must be $O = \{\bar{d}\}$. Since $\{\bar{d}\} \setminus \bar{I} = \{\bar{d}\} \setminus \{\!\!\{b, c\!\!\}\} = \{\bar{d}\} \not\subseteq \emptyset$, the condition is not satisfied. Thus Pierre $\ll_{ch}$ 0.

J Highlights of the Coq mechanisation

J.1 Preliminaries

We begin this section recalling the definition of MUST, which is given in Defi-
nition 2. It is noteworthy that the mechanised definition, i.e. must Extensional,
depends on the typeclass Sts (Figure J.1), and not the type class Lts. This lays
bare what stated in Section 1: to define MUST a reduction semantics (i.e. a state
transition system), and a predicate GOOD over clients suffice.

**State Transition Systems** The typeclass for state transition systems (Sts) is defined as follows, where *A* is the set of states of the Sts. It included a notion of stability which is axiomatized and decidable.

1.  **Class Sts (A: Type) := {**
2.     sts_step: A → A → Prop;
3.     sts_state_eqdec: EqDecision A;
4.     sts_step_decidable: RelDecision sts_step;
5.6.     sts_stable: A → Prop;
7.     sts_stable_decidable p : Decision (sts_stable p);
8.     sts_stable_spec1 p : ¬ sts_stable p -> { q | sts_step p q };
9.     sts_stable_spec2 p : { q | sts_step p q } → ¬ sts_stable p;
10.}.**
**Maximal computations** A computation is maximal if it is infinite or if its last state is stable. Given a state s, the type max_exec_from s contains all the maximal traces that start from s. Note the use of a coinductive type to allow for infinite executions.

1 Context `{Sts A}`.

2

3 CoInductive max_exec_from: A -> Type :=

4 | MExStop s (Hstable: sts_stable s) : max_exec_from s

5 | MExStep s s' (Hstep: sts_step s s') (η: max_exec_from s') :

6 max_exec_from s.

## J.2 The must-preorder

**Client satisfaction** The predicate GOOD is defined as any predicate over the states of an LTS that satisfies certain properties: it is preserved by structural congruence, by outputs in both directions (if $p \stackrel{\bar{a}}{\to} p'$ then $\mathrm{GOOD}(p) \Leftrightarrow \mathrm{GOOD}(p')$).

It is defined as a typeclass indexed over the type of states and labels, because we expect a practitioner to reason on a single canonical notion of "good" at a time.

1

2 Class Good (A L : Type) `{Lts A L, ! LtsEq A L}` := {

3 good : A -> Prop;

4 good_preserved_by_eq p q : good p -> p == q -> good q;

5 good_preserved_by_lts_output p q a :

6 p --> [ActOut a] q -> good p -> good q;

7 good_preserved_by_lts_output_converse p q a :

8 p --> [ActOut a] q -> good q -> good p

9 }.

10

**Must testing** Definition 2: We write $p_{\text{MUST}} r$ if every maximal computation of $p \triangleright r$ is successful.

Given an integer $n$ and a maximal execution $\eta$, the function `mex_take_from` $n$ applied to $\eta$ returns `None` if $\eta$ is shorter than $n$ and Some $p$, where $p$ is a finite execution corresponding to the first $n$ steps of $\eta$.

Then, we define the extensional version of $p_{\text{MUST}} e$ by stating that, for all maximal executions $\eta$ starting from $(p, e)$, there exists an integer $n$ such that the $n$-th element of $\eta$ is good. The $n$th element is obtained by taking the last element of the finite prefix of length $n$ computed using the function above.

1 Context `{good : B -> Prop}`.

2

3 Fixpoint mex_take_from (n: nat) {x} (η: max_exec_from x) :

4 option (finexec_from x) :=

5 match n with
```coq
6 | O => Some $ FExSingl x
7 | S n => match η with
8 | MExStop x Hstable => None
9 | MExStep x x' Hstep η' =>
10      let p' := mex_take_from n η' in
11      (λ p', FExStep x x' (bool_decide_pack _ Hstep) p') <$$> p'
12 end
13 end.
14
15 Definition must_extensional (p : A) (e : B) : Prop :=
16   ∀forall η : max_exec_from (p, e), exists n fex,
17   mex_take_from n η = Some fex /\ good (fex_from_last fex).2.
```

The preorder Definition 3 is mechanised in a straightforward way:

1 Definition pre_extensional (p : A) (q : R) : Prop :=
2   ∀forall (r : B), must_extensional p r -> must_extensional q r.
3
4 Notation "p ⊑_e q" := (pre_extensional p q).
```

## J.3 Behavioural characterizations

**Labeled Transition Systems** An LTS is a typeclass indexed by the type of states and the type of labels. The type of labels must be equipped with decidable equality and be countable, as enforced by the Label typeclass. An action `a`: Act L is either an internal action `τ` or an external action: an input or an output of a label in L.

```coq
1 Class Label (L: Type) := {
2   label_eqdec: EqDecision L;
3   label_countable: Countable L;
4 }.
5
6 Inductive Act (A: Type) := ActExt (μ: ExtAct A) | τ.
7
8 Class Lts (A L : Type) `~{Label L} := {
9   lts_step: A -> Act L -> A -> Prop;
10  lts_state_eqdec: EqDecision A;
11
12  lts_step_decidable a α b : Decision (lts_step a α b);
13
14  lts outputs : A -> gset L;
15  lts outputs_spec1 p1 x p2 :
16    lts step p1 (ActExt (ActOut x)) p2 -> x ∈ lts outputs p1;
17  lts outputs_spec2 p1 x :
18    x ∈ lts outputs p1 -> {p2 | lts step p1 (ActExt (ActOut x)) p2};
19
20  lts_stable: A -> Act L -> Prop;
21  lts_stable_decidable p α : Decision (lts_stable p α);
```
22 `lts_stable_spec1 p α : ¬ lts_stable p α → { q | lts_step p α q } ;`
23 `lts_stable_spec2 p α : { q | lts_step p α q } → ¬ lts_stable p α ;`
24 `}`.

25

26 `Notation "p → q" := (lts_step p τ q).`

27 `Notation "p → { α } q" := (lts_step p α q).`

28 `Notation "p → [ α ] q" := (lts_step p (ActExt µ) q).`

An LTS *L* is cast into an STS by taking only the *τ*-transitions, as formalised by the following instance, which says that *A* can be equipped with an STS structure when, together with some labels *L*, *A* is equipped with a LTS structure.

1 Program Instance sts_of LTS `~{Label L} (M: Lts A L): Sts A :=`
2 {|
3 sts_step p q := sts_step p τ q;
4 sts_stable s := lts_stable s τ;
5 |}.

1

2

3

4

5

**Weak transitions** Let $\Rightarrow \subseteq A \times Act^* \times A$ denote the least relation such that:

[wt-refl] $p \stackrel{e}{\Rightarrow} p'$,

[wt-tau] $p \stackrel{s}{\Rightarrow} q$ if $p \xrightarrow{\tau} p'$, and $p' \stackrel{s}{\Rightarrow} q$

[wt-mu] $p \stackrel{\mu.s}{\Rightarrow} q$ if $p \xrightarrow{\mu} p'$ and $p' \stackrel{s}{\Rightarrow} q$.

1 Definition trace L := list (ExtAct L).

2

3 Inductive wt : A -> trace L -> A -> Prop :=

4 | wtNil p : wt p [] p

5 | wt_tau s p q t (l : p → q) (w : wt q s t) : wt p s t

6 | wt_act µ s p q t (l : p → [µ] q) (w : wt q s t) : wt p (µ :: s) t.

7

8 Notation "p ⇒⇒⇒ [s] q" := (wt p s q).

**Product of LTS** The characteristic function of the transition relation of the LTS resulting from the parallel composition of two LTS. States of the parallel product of $L_1$ and $L_2$ are pairs $(a, b) \in L_1 \times L_2$. The first two cases correspond to unsynchronized steps from either LTS, and the third case corresponds to the LTS taking steps with dual actions. The predicate `act_match l1 l2` states that the two actions are visible and are dual of each other.

1 Inductive parallel_step `~{M1: Lts A L, M2: Lts B L} :`

2 A * B → Act L → A * B → Prop :=

3 | ParLeft l a1 a2 b: a1 -[l]→ a2 → parallel_step (a1, b) l (a2, b)

4 | ParRight l a b1 b2: b1 -[l]→ b2 → parallel_step (a, b1) l (a, b2)

5 | ParSync l1 l2 a1 a2 b1 b2:

6 act_match l1 l2 → a1 -[l1]→ a2 → b1 -[l2]→ b2 →

7 parallel_step (a1, b1) τ (a2, b2)

8
<figure><img src="image_17.png" /><figcaption>Fig. 17. Typeclasses to formalise LTSs.</figcaption></figure>

## J.4 Typeclasses for LTS

Our basic typeclasses are Lts ≥ LtsEq ≥ LtsOba, where LtsOba is a super-class of both LtsObaFB and LtsObaFW. The class LtsObaFB represents output-buffered agents with feedback, while LtsObaFW represents output-buffered agents with forwarding.

Class LtsOba (A L : Type) `~{Lts A L, !LtsEq A L} :=
MkOBA {
  lts_oba_output_commutativity {p q r a α} :
    p → [ActOut a] q → q → {α} r →
    ∃ t, p → {α} t ∧ t →≡ [ActOut a] r ;
  lts_oba_output_confluence {p q1 q2 a µ} :
    µ ≠ ActOut a → p → [ActOut a] q1 → p → [µ] q2 →
    ∃ r, q1 → [µ] r ∧ q2 →≡ [ActOut a] r ;
  lts_oba_output_tau {p q1 q2 a} :
    p → [ActOut a] q1 → p → q2 →
    (∃ t, q1 → t ∧ q2 →≡ [ActOut a] t) ∨ q1 →≡ [ActIn a] q2 ;
  lts_oba_output_deter {p1 p2 p3 a} :
    p1 → [ActOut a] p2 → p1 → [ActOut a] p3 → p2 ≡ p3 ;
  lts_oba_output_deter_inv {p1 p2 q1 q2} a :
    p1 → [ActOut a] q1 → p2 → [ActOut a] q2 → q1 ≡ q2 → p1 ≡ p2;
  (* Multiset of outputs *)
  lts_oba mo p : gmultiset L;
  lts_oba mo_spec1 p a : a ∈ lts_oba mo p <-> a ∈ ltsOutputs p;
  lts_oba mo_spec2 p a q :
    p → [ActOut a] q -> lts_oba mo p = {[+ a +]} ∪ lts_oba mo q;
}.

Class LtsObaFB (A L : Type) `~{LtsOba A L} :=
MkLtsObaFB {
  lts_obaFB feedback {p1 p2 p3 a} :
    p1 → [ActOut a] p2 → p2 → [ActIn a] p3 → p1 →≡ p3
}.

Class LtsObaFW (A L : Type) `~{LtsOba A L} :=
MkLtsObaFW {
31 lts_obapla forward p1 a :
32   ∃ p2, p1 → [ActIn a] p2 ∧ p2 →≡ [ActOut a] p1;
33 lts_obapla feedback {p1 p2 p3 a} :
34   p1 → [ActOut a] p2 → p2 → [ActIn a] p3 → p1 →≡ p3 ∨ p1 ≡ p3;
35 }.

**Termination** We write *p* ↓ and say that *p* converges if every sequence of τ-transitions performed by *p* is finite. This is expressed extensionally by the property that all maximal computations starting from *p* contain a *stable* process, meaning that it is finite.

1 Definition terminate (p : A) : Prop :=
2forall η : max_exec_from p, exists n fex,
3mex take_from n η = Some fex /\ lts_stable (fex_from_last fex) τ.

**Convergence along a trace** To define the behavioural characterisation of the preorder, we first define ⇝ ⊆ A × Act* as the least relation such that,

[env-epsilon] $p \Downarrow \epsilon$ if $p \downarrow$,

[env-mu] $p \Downarrow \mu.s$ if $p \downarrow$ and for each $p'$, $p \stackrel{\mu}{\implies} p'$ implies $p' \Downarrow s$.

This corresponds to the following inductive predicate in Coq:

1 Inductive cnv : A -> trace L -> Prop :=
2 | cnv_ext-nil p : terminate p -> cnv p []
3 | cnv_ext_act p µ s :
4     terminate p -> (forall q, p =⇒ {µ} q -> cnv q s) -> cnv p (µ :: s).

6 Notation "p ⇓ s" := (cnv p s).

## J.5 Forwarders

We define a mailbox *MO* as a multiset of names.

1 Definition mb (L : Type) ` {Label L} := gmultiset L.

Definition 6 and Figure 6 *Lifting of a transition relation to transitions of forwarders*.

1 Inductive ltspla step {A L : Type} ` {Lts A L} :
2 A * mb L -> Act L -> A * mb L -> Prop :=
3 | ltspla p q m α :
4 lts step p α q -> ltspla step (p ▷ m) α (q ▷ m)
5 | ltspla out_mb m p a :
6 ltspla step (p ▷ {[+ a +]} ⊎ m) (ActExt $ ActOut a) (p ▷ m)
7 | ltspla inp_mb m p a :
8 ltspla step (p ▷ m) (ActExt $ ActIn a) (p ▷ {[+ a +]} ⊎ m)
9 | ltspla com m p a q :
10 lts step p (ActExt $ ActIn a) q ->
11 ltspla step (p ▷ {[+ a +]} ⊎ m) τ (q ▷ m).
Definition 14 and Definition 15 For any LTS $\mathcal{L}$, two states of FW($\mathcal{L}$) are equivalent, denoted $p \vdash M \models q \vdash N$, if strip($p$) $\simeq$ strip($q$) and $M \uplus \mbox{mbox}(p) = N \uplus \mbox{mbox}(q)$.

1 Inductive strip `{Lts A L} : A -> gmultiset L -> A -> Prop :=

2 | stripNil p : p $\rightsquigarrow$ {} p

3 | strip_step p1 p2 p3 a m :

4 p1 $\to$ [ActOut a] p2 $\to$ p2 $\rightsquigarrow$ {m} p3 $\to$ p1 $\rightsquigarrow$ {{[+ a +]}} $\uplus$ m} p3

5

6 where "p $\rightsquigarrow$ { m } q" := (strip p m q).

7

8 Definition fw_eq `{LtsOba A L} (p : A * mb L) (q : A * mb L) :=

9forall (p' q' : A),

10 p.1 $\rightsquigarrow$ {lts_oba mo p.1} p' ->

11 q.1 $\rightsquigarrow$ {lts_oba mo q.1} q' ->

12 p' $\simeq$ q' /\ lts_oba mo p.1 $\uplus$ p.2 = lts_oba mo q.1 $\uplus$ q.2.

13

14 Infix "$\doteq$" := fw_eq (at level 70).

Lemma 16 For every $\mathcal{L}_A$ and every $p \vdash M, q \vdash N \in A \times MO$, and every $\alpha \in L$, if $p \vdash M (\doteq \alpha \vdash_{fw} q) \vdash N$ then $p \vdash M (\stackrel{\alpha}{\longrightarrow}_{fw} \doteq) q' \vdash N'$.

1 Lemma ltsNW `{LtsOBA FB A L} p q t mp mq mt $\alpha$ :

2 p $\vdash$ mp $\doteq$ t $\vdash$ mt $\to$ (t $\vdash$ mt) $\to$ {\alpha} (q $\vdash$ mq) $\to$ p $\vdash$ mp $\to$ $\doteq$ {\alpha} q $\vdash$ mq.

Lemma 2. For every LTS $\mathcal{L} \in \mathcal{FDB}$, $FW(\mathcal{L}) \in \mathcal{FWD}$.

1 Program Instance LtsMBOaFW `{LtsOBA FB A L} : LtsOBAFW (A * mb L) L.

Lemma 3 For every $\mathcal{L}_A, \mathcal{L}_B \in \mathcal{FDB}, p \in A, r \in B, p \text{MUST}_i r$ if and only if $FW(p) \text{MUST}_i r$.

1 Lemma must_iff_mustFW

2 {@LtsOBA FB A L IL LA LOA V, @LtsOBA FB B L IL LB LOB W,

3 !FiniteLts A L, !Good B L good }

4 (p : A) (e : B) : must p e $\leftrightarrow$ must (p, {} e).

## J.6 The Acceptance Set Characterisation

The behavioural characterisation with acceptance sets (Definition 5) is formalised as follows. Note that `lts outputs`, used in the second part of the definition, is part of the definition of an `Lts`, and produces the finite set of outputs that a process can immediately produce.

1 Definition bhv_pre_cond1 `{Lts A L, Lts B L} (p : A) (q : B) :=

2 `forall s, p $\downarrow$ s $\to$ q $\downarrow$ s.

3

4 Notation "p $\prec_1$ q" := (bhv_pre_cond1 p q) (at level 70).

5

6 Definition bhv_pre_cond2 `{Lts A L, Lts B L} (p : A) (q : B) :=

7 `forall s q', p $\downarrow$ s $\to$ q $\implies$ [s] q' $\to$ q' $\leftrightarrow$ ->
∃ p', p =⇒ [s] p' ∧ p' ↦ /\ lts outputs p' ⊑ lts outputs q'.

8

10

Notation "p ≲ 2 q" := (bhv_pre_cond2 p q) (at level 70).

11

12

Definition bhv_pre `@{Lts A L HL, @{Lts B L HL}` (p : A) (q : B) :=
p ≲ 1 q /\ p ≲ 2 q.

14

15

Notation "p ≲ q" := (bhv_pre p q) (at level 70).

Given an LTS that satisfies the right conditions, MUST-equivalence coincides
with the behavioural characterisation above on the LTS of forwarders (Theo-
rem 1).

1

Section correctness.

2

Context `@{Lts0baFB A L, Lts0baFB R L, Lts0baFB B L}`.

3

Context `@{!FiniteLts A L, !FiniteLts B L, !FiniteLts R L, !Good B L}`.

4

(* The LTS can express the tests required for completeness *)

5

Context `@{!gen_specoj conv genoj conv, !gen_specj acc genj acc}`.

6

7

Theorem equivalence\_bhv\_acc\_ctx (p : A) (q : R) :

8

p ⊑_e q <-> (p, Ø) ≲ (q, Ø).

9

End correctness.

J.7 The Must Set characterisation

The behavioural characterisation with must sets (Definition 13) is formalised as
follows.

1

Definition MUST `@{Lts A L}` (p : A) (G : gset (ExtAct L)) :=
forall p', p =⇒ p' -> exists µ p0, µ ∈ G /\ p' =⇒ {µ} p0.

3

4

Definition MUST\_s `@{FiniteLts A L}` (ps : gset A) (G : gset (ExtAct L)) :=
forall p, p ∈ ps -> MUST p G.

5

6

Definition AFTER `@{FiniteLts A L}` (p : A) (s : trace L) (hcnv : p ⇓ s) :=
wt\_set p s hcnv.

9

10

Definition bhv_pre_ms_cond2
`@{FiniteLts A L HL LtsA, FiniteLts B L HL LtsB}` (p : A) (q : B) :=
forall s h1 h2 G, MUST\_s (AFTER p s h1) G -> MUST\_s (AFTER q s h2) G.

11

12

13

14

Notation "p ≲ 2 q" := (bhv_pre_ms_cond2 p q) (at level 70).

15

16

Definition bhv_pre_ms `@{FiniteLts A L HL LtsA, FiniteLts B L HL LtsB}`
(p : A) (q : B) := p ≲ 1 q /\ p ≲ 2 q.

17

18

Notation "p ≲ q" := (bhv_pre_ms p q).

19

Lemma 8 Let $\mathcal{L}_A$, $\mathcal{L}_B \in \mathbf{FDB}$. For every $p \in A$ and $q \in B$ such that $\mathrm{FW}(p) \preceq_{\mathrm{cnv}} \mathrm{FW}(q)$, we have that $\mathrm{FW}(p) \preceq_M \mathrm{FW}(q)$ if and only if $\mathrm{FW}(p) \preceq_{\mathrm{acc}} \mathrm{FW}(q)$.
1 Context `^{{@LtsObaFB A L LL LtsA LtsEqA LtsObaA}}`.

2 Context `^{{@LtsObaFB B L LL LtsR LtsEqR LtsObaR}}`.

3

4 Lemma `equivalence_bhv_ACC_MST2` (`p`: `A`), (`q`: `B`):

5 (`p`, `Ø`) ≁₁ (`q`, `Ø`) -> (`p`, `Ø`) ≁₂ (`q`, `Ø`) <-> (`p`, `Ø`) ≁₂ (`q`, `Ø`).

Given an LTS that satisfies the right conditions, MUST-equivalence coincides with the behavioural characterisation above on the LTS of forwarders (Theorem 3).

1 Section correctness.

2 Context `^{{LtsObaFB A L, LtsObaFB R L, LtsObaFB B L}}`.

3 Context `^{{!FiniteLts A L, !FiniteLts B L, !FiniteLts R L, !Good B L}}`.

4 (* The LTS can express the tests required for completeness. *)

5 Context `^{{!gen_specoj conv genoj conv, !gen_specj acc genj acc}}`.

6

7 Theorem `equivalence_bhv_MST_ctx` (`p`: `A`), (`q`: `R`):

8 `p` ⊑<e> `q` <-> (`p`, `Ø`) ≁<e> (`q`, `Ø`).

9 End correctness.

## J.8 From extensional to intensional definitions

Proposition 2 *Given a countably branching STS $\langle S, \rightarrow \rangle$, and a decidable predicate $Q$ on $S$, for all $s \in S$, $\text{ext}_Q(s)$ implies $\text{int}_Q(s)$.*

1 Context `^{{Hsts: Sts A, @CountableSts A Hsts}}`.

2 Context `^{{@Bar A Hsts}}`.

3

4 Theorem `extensional_implies_intensional x`:

5 `extensionalpred x -> intensionalpred x`.

Corollary 2 *For every $p \in A$,*

1. $p \downarrow$ if and only if $p \downarrow_i$,

2. for every $r$ we have that $p$ MUST $r$ if and only if $p$ MUST$_i$ $r$.

1 Context `^{{Label L}}`.

2 Context `^{{!Lts A L, !FiniteLts A L}}`.

3

4 Lemma `terminateExtensional_IfTerminate` (`p`: `A`):

5 `terminateExtensional p <-> terminate p`.

6

7 Inductive `must_sts ^{Sts (A * B), good : B -> Prop} (p : A) (e : B) :`

8 `Prop :=`

9 | `m_sts_now`: `good e -> must_sts p e`

10 | `m_sts_step`

11 (nh : ¬ good e)

12 (nst : ¬ sts_stable (p, e))

13 (l : `forall p' e'`, sts_step (p, e) (p', e') -> `must_sts p' e'`)

14 : `must_sts p e`
Lemma must_extensionsal_iff_must_sts
  ``{good : B -> Prop, good_decidable : `forall` (e : B), Decision (good e)}``
  ``{Lts A L, !Lts B L, !LtsEq B L, !Good B L good,``
  ``!FiniteLts A L, !FiniteLts B L} (p : A) (e : B) :
  must_extensionsal p e <-> must_sts p e.
15
16
17
18
19
20
21

Equivalence between the inductive definitions of MUST defined using Sts and MUST defined using Lts.

Inductive must ``{Lts A L, !Lts B L, !LtsEq B L, !Good B L good}``
(p : A) (e : B) : Prop ::=
| m_now : good e -> must p e
| m_step
  (nh : ¬ good e)
  (ex : ∃ t, parallel_step (p, e) τ t)
  (pt : `forall` p', p → p' -> must p' e)
  (et : `forall` e', e → e' -> must p e')
  (com : `forall` p' e' µ, e → [µ] e' -> p → [co µ] p' -> must p' e')
: must p e
1
2
3
4
5
6
7
8
9
10
11
12
13
14

Lemma must_sts_iff_must ``{Lts A L, !Lts B L, !LtsEq B L, !Good B L good}``
(p : A) (e : B) : must_sts p e <-> must p e.
13
14

## J.9 Completeness

Properties of the functions that generate clients (Table 1).

Class gen_spec {A L : Type} ``{Lts A L, !LtsEq A L, !Good A L good}``
(gen : list (ExtAct L) -> A) := {
  gen_spec_ungood : `forall` s, ¬ good (gen s) ;
  gen_spec_mu_lts_co µ s : gen (µ :: s) →≈[co µ] gen s;
  gen_spec_out_lts_tau_ex a s : ∃ e', gen (ActOut a :: s) → e';
  gen_spec_out_lts_tau good a s e : gen (ActOut a :: s) → e -> good e;
  gen_spec_out_lts_mu_uniq {e a µ s} :
    gen (ActOut a :: s) → [µ] e -> e = gen s /\ µ = ActIn a;
}.
1
2
3
4
5
6
7
8
9
10
11
12
13
14

Class gen_specojn {A L : Type} ``{Lts A L, ! LtsEq A L, !Good A L good}``
(genojn : list (ExtAct L) -> A) := {
  genojn_spec_gen_spec : gen_spec genojn ;
  gen_specojn Nil_stable mu µ : genojn [] → [µ] ;
  gen_specojnNil_lts tau ex : ∃ e', genojn [] → e';
  gen_specojnNil_lts tau good e : genojn [] → e -> good e;
}.
10
11
12
13
14
15
16
17
18
19
20

Class gen_spec_acc {A : Type} ``{Lts A L, ! LtsEq A L, !Good A L good}``
(gen_acc : gset L -> list (ExtAct L) -> A) := {
15
16
17
18
19
20
21 gen_ACC_Spec_gen_spec 0 : gen_spec (gen_ACC 0);
22 gen_spec_ACC-nil_stable_tau 0 : gen_ACC 0 [] ↦;
23 gen_spec_ACC-nil_stable_out 0 a : gen_ACC 0 [] ↦ [ActOut a];
24 gen_spec_ACC-nilmu inv 0 a e : gen_ACC 0 [ ] → [ActIn a] e -> a ∈ 0;
25 gen_spec_ACC-nil_mem LTS_inp 0 a :
26 a ∈ 0 -> ∃ r, gen_ACC 0 [] → [ActIn a] r;
27 gen_spec_ACC-nil LTS_inp good μ e' 0 :
28 gen_ACC 0 [] → [μ] e' -> good e';
29 }.

Proposition 3 *For every* $\mathcal{L}_A \in \text{FWD}$, $p \in A$, and $s \in \text{Act}^*$ we have that $p \text{ MUST}_i \text{ tc}(s)$ if and only if $p \downarrow s$.

1 Lemma must_iff_cnv
2 `@{LtsObaFW A L IL LA LOA V, @LtsObaFB B L IL LB LOB W,
3 !Good B L good, !gen_specoj conv genoj conv} (p : A) s :
4 must p (genoj conv s) <-> p s.
5 Proof. split; [eapply cnv_if_must | eapply must_if_cnv]; eauto. Qed.

Lemma 14 Let $\mathcal{L}_A \in \text{FWD}$ and $\mathcal{L}_B \in \text{FDB}$. For every $p_1, p_2 \in A$, every $r_1, r_2 \in B$ and name $a \in \mathcal{N}$ such that $p_1 \xrightarrow{\bar{a}} p_2$ and $r_1 \xrightarrow{\bar{a}} r_2$, if $p_1 \text{ MUST}_i r_2$ then $p_2 \text{ MUST}_i r_1$.

1 Lemma must_output_swap_l FW
2 `@{LtsObaFW A L IL LA LOA V, @LtsObaFB B L IL LB LOB W, !Good B L good}`
3 (p1 p2 : A) (e1 e2 : B) (a : L) :
4 p1 -> [ActOut a] p2 -> e1 -> [ActOut a] e2 -> must p1 e2 -> must p2 e1.

Lemma 18. Let $\mathcal{L}_A \in \text{FWD}$. For every $p \in A$, $s \in \text{Act}^*$, and every $L, E \subseteq \mathcal{N}$, if $\overline{L} \in \mathcal{A}_{\text{fw}}(p, s)$ then $p \text{ MU} \nmid \text{ST}_i \text{ ta}(s, E \setminus L)$.

1 Lemma not_must_gen_aWithoutchin output
2 `@{LtsObaFW A L IL LA LOA V, @LtsObaFB B L IL LB LOB W,
3 !Good B L good, !gen_specj acc genj acc} (q q' : A) s 0 :
4 q = [s] q' -> q' -> ! must q (genj acc (0 \ ltsj outputs q') s).

Lemma 19 Let $\mathcal{L}_A \in \text{FWD}$. For every $p \in A$, $s \in \text{Act}^*$, and every finite set $O \subseteq \mathcal{N}$, if $p \downarrow s$ then either

(i) $p_{\text{MUST}_i} \text{ ta}(s, \bigcup \overline{\mathcal{A}_{\text{fw}}(p, s) \setminus O})$, or

(ii) there exists $\tilde{O} \in \mathcal{A}_{\text{fw}}(p, s)$ such that $\tilde{O} \subseteq O$.

1 Lemma must_gen_a_with_s
2 `@{LtsObaFW A L IL LA LOA V, @LtsObaFB B L IL LB LOB W,
3 !FiniteLts A L, !Good B L good, !gen_specj acc genj acc}`
4 s (p : A) (hcnv : p s) 0 :
5 (exists p', p = [s] p' /\ lts_stable p' \tau /\ ltsOutputs p'subseteq 0)
6 \ must p (genj acc (oas ps hcnv \ 0) s).

Lemma 20. For every $\mathcal{L}_A$, $\mathcal{L}_B \in \text{FWD}$ and servers $p \in A$, $q \in B$, if $p \preceq_{\text{MUST}} q$ then $p \preceq \text{AS} q$.
1 Lemma completeness FW

2 `^{{@LtsObaFW A L IL LA LOA V, @LtsObaFB B L IL LB LOB W,`
3 `@LtsObaFW C L IL LC LOC VC, !FiniteLts A L, !FiniteLts C L,`
4 `!FiniteLts B L. !Good B L good,`
5 `!gen_specoj conv genj conv, !gen_specj acc genj acc}}`
6 `(p : A) (q : C) : p v q -> p `<` q.

Proposition 4. For every $\mathcal{L}_A, \mathcal{L}_B \in \text{FDB}$ and servers $p \in A, q \in B$, if $p \subseteq_{\text{MUST}} q$ then $\text{FW}(p) \preceq_{\text{AS}} \text{FW}(q)$.

1 Lemma completeness

2 `^{{@LtsObaFB A L IL LA LOA V, @LtsObaFB B L IL LB LOB W,`
3 `@LtsObaFB C L IL LC LOC VC,`
4 `!FiniteLts A L, !FiniteLts B L, !FiniteLts C L, !Good C L good,`
5 `!gen_specj conv genj conv, !gen_specj acc genj acc}}`
6 `(p : A) (q : B) : p v q -> p > Ø `<` q > Ø`.

## J.10 Soundness

Figure 7. Rules to define inductively the predicate MUST<sub>aux</sub>.

1 Inductive mustx

2 `^{{Lts A L, !FiniteLts A L, !Lts B L, !LtsEq B L, !Good B L good}}`
3 `(ps : gset A) (e : B) : Prop :=`
4 `| mx_now (hh : good e) : mustx ps e`
5 `| mx_step`
6 `(nh : : good e)`
7 `(ex : `forall` (p : A), p ∈ ps -> ∃ t, parallelj step (p, e) τ t)`
8 `(pt : `forall` ps`,`
9 `| lts_j tauj setj fromj psetj spec1 ps ps' -> ps' ≠ Ø ->`
10 `| mustx ps' e)`
11 `(et : `forall` (e' : B), e -> e' -> mustx ps e')`
12 `(com : `forall` (e' : B) µ (ps' : gset A),`
13 `| ltsj step e (ActExt µ) e' ->`
14 `| wtj setj fromj psetj spec1 ps [co µ] ps' -> ps' ≠ Ø ->`
15 `| mustx ps' e)`
16 `: mustx ps e.`

Lemma 7 For every LTS $\mathcal{L}_A, \mathcal{L}_B$ and every $X \in \mathcal{P}^+(A)$, we have that $X$ MUST<sub>aux</sub> $r$ if and only if for every $p \in X$. $p$ MUST<sub>i</sub> $r$.

1 Lemma mustj setj iffj mustj forj all

2 `^{{Lts A L, !FiniteLts A L, !Lts B L, !LtsEq B L, !Good B L good}}`
3 `(X : gset A) (e : B) : X ≠ Ø ->`
4 `(forall p, p ∈ X -> must p e) <-> mustx X e.`

Lifting of the predicates `<` and `<=` to sets of servers.

1 Definition bhvj prej cond1j x `^{{FiniteLts P L, FiniteLts Q L}}`

2 `(ps : gset P) (q : Q) := `forall` s, `(forall p, p ∈ ps -> p `↓` s) -> q `↓` s`.
3

4

Notation "ps ≪_x1 q" := (bhv_pre_cond1__x ps q) (at level 70).

5

6

7

8

9

10

11

12

13

15

16

17

Definition bhv_pre_cond2__x

``{@FiniteLts P L HL LtsP, @FiniteLts Q L HL LtsQ}`

(ps . gset P) (q : Q) :=

forall s q', q = ⇒ [s] q' -> q' ↦ ->

(forall p, p ∈ ps -> p ⇓ s) ->

exists p, p ∈ ps /\ exists p',

p = ⇒ [s] p' /\ p' ↦ /\ lts outputs p' ⊆ lts outputs q'.

Notation "ps ≪_x2 q" := (bhv_pre_cond2__x ps q) (at level 70).

Notation "ps ≪_x q" := (bhv_pre_cond1__x ps q /\ bhv_pre_cond2__x ps q)

(at level 70).

Lemma 35. For every LTS $\mathcal{L}_A$, $\mathcal{L}_B$ and servers $p \in A$, $q \in B$, $p \preceq_{AS} q$ if and only if $\{p\} \preceq_{AS}^{\text{set}} q$.

1

Lemma alt_set_singleton_iff

2

3

``{@FiniteLts P L HL LtsP, @FiniteLts Q L HL LtsQ}`

(p : P) (q : Q) : p ≪ q <-> {[ p ]] ≪_x q.

Lemma 36. Let $\mathcal{L}_A$, $\mathcal{L}_B \in \text{FWD}$. For every set $X \in \mathcal{P}^+(A)$, and $q \in B$, such that $X \preceq_{\text{cnv}}^{\text{set}} q$ then

1. $q \xrightarrow{\tau} q'$ implies $X \preceq_{\text{cnv}}^{\text{set}} q'$,

2. $X \downarrow_i, X \xrightarrow{\mu} X'$ and $q \xrightarrow{\mu} q'$ imply $X' \preceq_{\text{cnv}}^{\text{set}} q'$.

Lemma 37 Let $\mathcal{L}_A$, $\mathcal{L}_B \in \text{FWD}$. For every $X, X' \in \mathcal{P}^+(A)$ and $q \in B$, such that $X \preceq_{\text{acc}}^{\text{set}} q$, then

1. $q \xrightarrow{\tau} q'$ implies $X \preceq_{\text{acc}}^{\text{set}} q'$,

2. for every $\mu \in \text{Act}$, if $X \downarrow_i$, then for every $q \xrightarrow{\mu} q'$ and set $X \xrightarrow{\mu} X'$ we have $X' \preceq_{\text{acc}}^{\text{set}} q'$.

1

Lemma bhvx_preserved_by_tau

2

3

``{@FiniteLts P L HL LtsP, @FiniteLts Q L HL LtsQ}`

(ps : gset P) (q q' : Q) : q \to q' -> ps \preceq_x q -> ps \preceq_x q'.

4

5

Lemma bhvx_preserved_by mu

6

7

8

9

10

``{@FiniteLts P L HL LtsP, @FiniteLts Q L HL LtsQ}`

(ps0 : gset P) (q : Q) µ ps1 q'

(htp :forall p, p ∈ ps0 -> terminate p) :

q \to [\mu] q' -> wt_set_from_pset_spec ps0 [\mu] ps1 ->

ps0 \preceq_x q -> ps1 \preceq_x q'.

Lemma Let $\mathcal{L}_A$, $\mathcal{L}_B \in \text{FWD}$ and $\mathcal{L}_C \in \text{FDB}$. For every $X \in \mathcal{P}^+(A)$ and $q \in B$ such that $X \preceq_{\text{AS}}^{\text{set}} q$, for every $r \in C$ if $\neg \text{GOOD}(r)$ and $X \text{ MUST}_{\text{aux}} r$ then $q \nvdash r \xrightarrow{\tau}$.
1 Lemma stability_nbhvleqtwo

2 `^{{@LtsObaFW P L Lbl LtsP LtsEqP LtsObaP,`

3 `@LtsObaFW Q L Lbl LtsQ LtsEqQ LtsObaQ,`

4 `!FiniteLts P L, !FiniteLts Q L, !Lts B L, !LtsEq B L, !Good B L good}`

5 `(X : gset P) (q : Q) e :`

6 `¬ good e -> mustx X e -> X ≪_x 2 q -> exists t, (q, e) →{τ} t.`

Lemma Let $\mathcal{L}_A, \mathcal{L}_B \in \text{FWD}$. For every $X \in \mathcal{P}^+(A)$ and $q, q' \in B$, such that $X \preceq_{\text{AS}}^s q$, then for every $\mu \in \text{Act}$, if $X \Downarrow \mu$ and $q \xrightarrow{\mu} q'$ then $X \xrightarrow{\mu} \bar{X}$.

1 Lemma bhvx mu ex `^{{@FiniteLts P L HL LtsP, @FiniteLts Q L HL LtsQ}}`

2 `(ps : gset P) (q q' : Q) µ`

3 `: ps ≪_x q -> (forall p, p \in ps -> p \Downarrow [µ]) ->`

4 `q → [µ] q' -> exists p', wt_set_from_pset_spec1 ps [µ] {[p']}]`

Lemma For every $\mathcal{L}_A \in \text{FWD}$, $\mathcal{L}_B \in \text{FDB}$, every set of processes $X \in \mathcal{P}^+(A)$, every $r \in B$, and every $\mu \in \text{Act}$, if $X \text{ MUST}_{\text{aux}} r$, $\neg \text{GOOD}(r)$ and $r \xrightarrow{\mu} \bar{X}$ then $X \Downarrow \bar{\mu}$.

1 Lemma ungood acnv mu `^{LtsOba A L, !FiniteLts A L, !Lts B L, !LtsEq B L,`

2 `!Good B L good} ps e e' : mustx ps e ->`

3 `forall µ p, p \in ps -> e -> [co µ] e' -> ¬ good e -> p \Downarrow [µ].`

Lemma 38. Let $\mathcal{L}_A, \mathcal{L}_B \in \text{FWD}$ and $\mathcal{L}_C \in \text{FDB}$. For every set of processes $X \in \mathcal{P}^+(A)$, server $q \in B$ and client $r \in C$, if $X \text{ MUST}_{\text{aux}} r$ and $X \preceq_{\text{AS}}^s q$ then $q \text{ MUST}_i r$.

1 Lemma soundnessx `^{`

2 `@LtsObaFW A L Lbl LtsA LtsEqA LtsObaA,`

3 `@LtsObaFW C L Lbl LtsC LtsEqC LtsObaC,`

4 `@LtsObaFB B L Lbl LtsB LtsEqB LtsObaB,`

5 `!FiniteLts A L, !FiniteLts C L, !FiniteLts B L, !Good B L good}`

6 `(ps : gset A) (e : B) : mustx ps e ->`

7 `forall (q : C), ps ≪_x q -> must q e.`

Proposition 5. For every $\mathcal{L}_A, \mathcal{L}_B \in \text{FDB}$ and servers $p \in A, q \in B$, if $\text{FW}(p) \preceq_{\text{AS}}^s \text{FW}(q)$ then $p \sqsubseteq_{\text{MUST}}^s q$.

1 Lemma soundness

2 `^{{@LtsObaFB A L IL LA LOA V, @LtsObaFB C L IL LC LOC T,`

3 `@LtsObaFB B L IL LB LOB W,`

4 `!FiniteLts A L, !FiniteLts C L, !FiniteLts B L, !Good B L good }`

5 `(p : A) (q : C) : p ▷ ∅ ≪ q ▷ ∅ -> p ⊑ q.`

**Corollary 6.** Let $\mathcal{L}_A, \mathcal{L}_B \in \text{FDB}$. For every $p \in A$ and $q \in B$, we have that $p \sqsubseteq_{\text{MUST}}^s q$ if and only if $p \leq_{\text{fail}} q$.

1

2 Section failure.

3
Definition Failure `@FiniteLts A L` (p : A)
(s : trace L) (G : gset (ExtAct L)) :=
p ⇓ s -> exists p', p =⇒ [s] p' /\
forall µ, µ ∈ G -> ¬ exists p0, p' =⇒ {µ} p0.

Definition fail_pre_ms_cond2
`@FiniteLts A L HL LtsA, @FiniteLts B L HL LtsB`
(p : A) (q : B) := `forall s G, Failure q s G -> Failure p s G.`

Definition fail_pre_ms
`@FiniteLts A L HL LtsA, @FiniteLts B L HL LtsB` (p : A) (q : B) :=
p ≺1 q /\ `fail_pre_ms_cond2 p q.`

Context `@LL : Label L`.
Context `@LtsA : !Lts A L, !FiniteLts A L`.
Context `@LtsR : !Lts R L, !FiniteLts R L`.

Context `@LtsObaFB A L LL LtsA LtsEqA LtsObaA`.
Context `@LtsObaFB R L LL LtsR LtsEqR LtsObaR`.

Theorem equivalence_pre_failure_must_set (p : A) (q : R) :
(p ▷ ∅) ≲ (q ▷ ∅) <-> (p ▷ ∅) ≪ (q ▷ ∅).

End failure.

## J.11 Coinductive definition

The coinductive preorder is defined in Coq using a coinductive predicate as
follows:

CoInductive copre `@FiniteLts A L HL LtsP, @FiniteLts B L HL LtsQ`
(ps : gset A) (q : B) : Prop := {
  c_tau q' : q --> q' -> copre ps q'
; c_now : (forall p, p ∈ ps -> p ↓i) -> q ↛ ->
  exists p p', p ∈ ps /\ p =⇒ p' /\ p' ↛ /\ ltsOutputs p' ⊆ ltsOutputs q
; c_step : (forall µ q' ps', (forall p, p ∈ ps -> p ⇓ [µ])) ->
  q =⇒ [µ] q' -> wt_set_from_pset_spec ps [µ] ps' -> copre ps' q'
; c_cnv : (forall p, p ∈ ps -> p ↓i) -> q ↓i
}.

The soundness and completeness of the preorder is expressed in Theorem 2,
which is formalised as follows in our development.

Theorem eqx `@FiniteLts A L HL LtsP, @FiniteLts B L HL LtsQ` (X : gset A) (q : B) :
X ≺x q <-> X ≤ q.

## J.12 The preorder on traces in normal forms

A trace in normal form is simply a list of pairs of multisets, representing inputs
and outputs:
1 Definition ntrace L `~{Label L} : Type := list (gmultiset L * gmultiset L).

Given such a trace in normal form, we can linearize it to a trace by choosing an arbitrary order for the elements of the multisets. This is achieved using the **elements** that maps a multiset to a list that contains its elements in an arbitrary order.

1 Fixpoint linearize `~{Label L} (nt : ntrace L) : trace L :=
2 match nt with
3 | [] => []
4 | (mi, mo) : : nt' =>
5 let inputs := map ActIn (elements mi) in
6 let outputs := map ActOut (elements mo) in
7 inputs ++ outputs ++ linearize nt'
8 end.

Using this operation, we can define the preorder as follows:

1 Definition bhv_lin_pre_cond1 `~{Lts P L, Lts Q L} (p : P) (q : Q) :=
2forall s, p ⇓ linearize s -> q ⇓ linearize s.

3 Notation "p ≲₁ q" := (bhv_lin_pre_cond1 p q) (at level 70).

5 Definition bhv_lin_pre_cond2 `~{@Lts P L HL, @Lts Q L HL} (p : P) (q : Q) :=
6forall nt q',
7p ⇓ linearize nt -> q = ⇒ [linearize nt] q' -> q' ↦ ->
8∃ p', p = ⇒ [linearize nt] p' ∧ p' ↦ /\ lts outputs p' ⊆ lts outputs q'.

11 Notation "p ≲₂ q" := (bhv_lin_pre_cond2 p q) (at level 70).

13 Definition bhv_lin_pre `~{@Lts P L HL, @Lts Q L HL} (p : P) (q : Q) := p ≲₁ q /\ p ≲₂ q.

15 Notation "p ≲ q" := (bhv_lin_pre p q) (at level 70).

Finally, the theorem stating that this preorder characterises the MUST-preorder is formulated as follows in our development:

1 Lemma asyn_iff_bhv

2 `~{@LtsObaFW P L IL LA LOA V, @LtsObaFW Q L IL LB LOB W,`

3 !FiniteLts Q L, !FiniteLts Q L} :

4 `forall (p : P) (q : Q), p ≲ q <-> p ≰ q.`
K Mapping of results from the paper to the Coq code

<table><thead><tr><th>Paper</th><th>Coq File</th><th>Coq name</th></tr></thead><tbody><tr><td>Figure 2</td><td>TransitionSystems.v</td><td>Class LtsOba</td></tr><tr><td>Figure 3</td><td>TransitionSystems.v</td><td>Class Sts, ExtAct, Act, Label, Lts</td></tr><tr><td>Definition 2</td><td>Equivalence.v</td><td>must_extensional</td></tr><tr><td>Definition 3</td><td>Equivalence.v</td><td>pre_extensional</td></tr><tr><td>Equation (5)</td><td>ACCSInstance.v</td><td>proc</td></tr><tr><td>Figure 5</td><td>TransitionSystems.v</td><td>LtsEq</td></tr><tr><td>Definition 2</td><td>MustEx.v</td><td>must_extensional</td></tr><tr><td>Definition 4</td><td>TransitionSystems.v</td><td>max_exec_from</td></tr><tr><td>p s p'</td><td>TransitionSystems.v</td><td>wt</td></tr><tr><td>p ↓</td><td>Equivalence.v</td><td>terminate_extensionsal</td></tr><tr><td>p ↓ s</td><td>TransitionSystems.v</td><td>cnv</td></tr><tr><td>Lemma 22</td><td>TransitionSystems.v</td><td>cnv_iff_prefix_terminate</td></tr><tr><td>Lemma 23</td><td>TransitionSystems.v</td><td>stable_tau_preserved_by_wt_output, stable_tau_input_preserved_by_wt_output</td></tr><tr><td>Lemma 21</td><td>Must.v</td><td>ungood_preserved_by_wt_output</td></tr><tr><td>Equation (7)</td><td>TransitionSystems.v</td><td>Class LtsObaFW</td></tr><tr><td>Definition 5</td><td>Must.v</td><td>bhv_pre</td></tr><tr><td>Figure 6</td><td>TransitionSystems.v</td><td>ltsStep</td></tr><tr><td>Definition 6</td><td>TransitionSystems.v</td><td>MbLts</td></tr><tr><td>Definition 14</td><td>TransitionSystems.v</td><td>strip</td></tr><tr><td>Definition 15</td><td>TransitionSystems.v</td><td>fw_eq</td></tr><tr><td>Lemma 16</td><td>TransitionSystems.v</td><td>ltsFWeqSpec</td></tr><tr><td>Lemma 2</td><td>TransitionSystems.v</td><td>Instance LtsMBObaFW</td></tr><tr><td>Lemma 3</td><td>Lift.v</td><td>must_iff_mustFW</td></tr><tr><td>Lemma 3</td><td>Lift.v</td><td>liftFWctx_pre</td></tr><tr><td>Theorem 1</td><td>Equivalence.v</td><td>equivalenceBhvaccctx</td></tr><tr><td>Definition 13</td><td>Must.v</td><td>bhv_pre_ms</td></tr><tr><td>Lemma 8</td><td>Must.v</td><td>equivalenceBhvaccmst</td></tr><tr><td>Theorem 3</td><td>Must.v</td><td>equivalenceBhv_mst_ctx</td></tr><tr><td>Lemma 1</td><td>ACCSInstance.v</td><td>ACCSLtsObaFB</td></tr><tr><td>Corollary 1</td><td>ACCSInstance.v</td><td>bhv_iff_ctx_ACCS</td></tr><tr><td>Proposition 2</td><td>Bar.v</td><td>extensionalimpliesintensional</td></tr><tr><td>p ↓<sub>i</sub></td><td>TransitionSystems.v</td><td>terminate</td></tr><tr><td>p MUST<sub>i</sub> q</td><td>Must.v</td><td>must sts</td></tr><tr><td>Corollary 2</td><td>Equivalence.v</td><td>terminate_extensionsal_iff_terminate</td></tr><tr><td>Table 1</td><td>Completeness.v</td><td>Class gen spec, gen spec conv, gen spec acc</td></tr><tr><td>Proposition 3</td><td>Completeness.v</td><td>must_iff_cnv</td></tr><tr><td>Lemma 14</td><td>Lift.v</td><td>must_output_swap_l FW</td></tr><tr><td>Lemma 18</td><td>Completeness.v</td><td>not_must_gen_aWithoutRequired_output</td></tr><tr><td>Lemma 19</td><td>Completeness.v</td><td>must_gen_a_with_s</td></tr><tr><td>Lemma 20</td><td>Completeness.v</td><td>completeness FW</td></tr><tr><td>Proposition 4</td><td>Completeness.v</td><td>completeness</td></tr><tr><td>Lemma 7</td><td>Soundness.v</td><td>must_set_iff_must_for_all</td></tr><tr><td>Figure 7</td><td>Soundness.v</td><td>mustx</td></tr><tr><td>X &le; set<sub>cnv</sub> q and X &le; set<sub>acc</sub> q</td><td>Soundness.v</td><td>bhv_pre_cond1<sub>x</sub> and bhv_pre_cond2<sub>x</sub></td></tr><tr><td>Lemma 35</td><td>Soundness.v</td><td>must_set_iff_must</td></tr><tr><td>Lemma 36, Lemma 37</td><td>Soundness.v</td><td>bhvx_preserved_by_tau, bhvx_preserved_by mu</td></tr><tr><td>Lemma 38</td><td>Soundness.v</td><td>soundnessx</td></tr><tr><td>Proposition 5</td><td>Soundness.v</td><td>soundness</td></tr><tr><td>Corollary 4</td><td>Normalisation.v</td><td>asyn_iff_bhv</td></tr><tr><td>Theorem 2</td><td>Coin.v</td><td>eq_ctx</td></tr></tbody></table>