Let us now assume that $val_x$ does not satisfy $[[\Gamma]]_\phi$. In particular there exists a clause of $[[\Gamma]]_\phi$, say the $i^{th}$ clause with $i = \sum_{k=1}^m \pi_k 2^{k-1}$, which is falsified by $val_x$. In particular, if the three variable of this clause are called $x_1, x_2, x_3$ with respective negation bits $b_1, b_2, b_3$, the following formula is evaluated to false (i.e. 0):

$$ \bigvee_{i=1}^{3} (b_j = val_x(x_j)) $$

Therefore, by choosing the sequence $\pi_1, \dots, \pi_m$ to instanciate the initial Choose($p_1, \dots, p_m$) of CheckSat($x$), we obtain the following sequence of transitions, which concludes the proof:

$$ \text{CheckSat}(x) \stackrel{\epsilon}{\Rightarrow} \bar{c}\langle h(0, s) \rangle \cdot \bar{c}\langle h(1, s) \rangle \quad \blacksquare $$

We finally gathered all the ingredients needed to prove the main lemma:

**PROPOSITION 5.23 (correctness of the reduction).** For any equivalence relation $\approx \in \{\approx_s, \approx_t, \approx_b\}$, $[[\Gamma]]_\phi$ is satisfiable iff $A \not\approx B$.

**PROOF.** We prove the result by double implication.

⇒ Let us consider a valuation satisfying $\phi$ and let $t$ be a message such that $val_t$ is equal to this valuation. Then since the trace $B \stackrel{c(t).\bar{c}\langle ax_1 \rangle .\bar{c}\langle ax_2 \rangle}{\rightleftharpoons} (\emptyset, \Phi_0)$ cannot be matched in $A$ by Lemma D.15, we obtain $B \not\subseteq_t A$. Hence, since trace equivalence is the coarsest of the considered equivalence relations, we obtain the desired result.

⇔ By contraposition, let us suppose that $\phi$ is unsatisfiable, and let us prove that $A \approx_b B$ (which implies all other equivalences). Let us consider $\mathcal{R}$ the smallest reflexive symmetric relation on extended processes such that:

1. $A \mathcal{R} B$

2. $A'(x) \mathcal{R} B'(x)$ for all message $x$, where $A = c(x).A'(x)$ and $B = c(x).B'(x)$

3. $P_i \mathcal{R} P'_i$, where:

$$ P_i = (\{\bar{c}\langle t_{i+1} \rangle \dots \bar{c}\langle t_p \rangle\}, \{ax_1 \mapsto t_1, \dots, ax_i \mapsto t_i\}) $$

$$ P'_i = (\{\bar{c}\langle t'_{i+1} \rangle \dots \bar{c}\langle t'_p \rangle\}, \{ax_1 \mapsto t'_1, \dots, ax_i \mapsto t'_i\}) $$

and where $\{ax_1 \mapsto t_1, \dots, ax_p \mapsto t_p\} \sim \{ax_1 \mapsto t'_1, \dots, ax_p \mapsto t'_p\}$

It easily follows from Lemma D.15,5.21,5.22 that $\mathcal{R}$ is a bisimulation up to $\rightsquigarrow$, hence the conclusion.