# Proofs for Section 3 This appendix proves the results announced in Section 3. Appendix 6 proves Lemma 2 (validity); Appendix 7 proves Lemma 4 (soundness of $\mathsf{split}$); and Appendix 8 proves Proposition 5 (soundness of $\mathsf{annotate}$). Appendices 9 to 12 are devoted to the proof of results needed for Theorem 13. We show that barrier elimination commutes with renaming and substitution (proof of Lemma 8 in Appendix 9) and that it preserves reduction (proof of Lemma 9 in Appendix 10). Using these interim results, we prove Proposition 7 (Appendix 11). Appendix 12 proves Propositions 10 and 11. Finally, Appendix 13 proves our results on replicated barriers (Section 3.5.1). # Proof of Lemma 2 (validity)

**Lemma 17**. *If $C[Q]$ is valid, $\sigma$ is a ground substitution, $C[\_]$ binds the variables in $\mathsf{dom}(\sigma)$ and no other variable above the hole, and $\mathsf{fn}(\mathsf{range}(\sigma)) \cap \mathsf{channels}(\mathsf{barriers}(Q)) = \emptyset$, then $\mathsf{barriers}(Q\sigma) = \mathsf{barriers}(Q)$ and $Q \sigma$ is valid.*

*Proof.* The process $Q\sigma$ is closed because $\mathsf{fv}(Q\sigma) \subseteq \mathsf{fv}(Q) \setminus \mathsf{dom}(\sigma) \cup \mathsf{fv}(\mathsf{range}(\sigma)) \subseteq \mathsf{fv}(C[Q]) \cup \mathsf{fv}(\mathsf{range}(\sigma)) = \emptyset$ since $C[Q]$ is closed and $\sigma$ is ground. Consider an annotated barrier in $Q$, such that $Q = C'[t[a,c,\varsigma]\textnormal{::}\,Q']$. We rename the bound variables so that the variables in $\mathsf{dom}(\sigma)$ are not bound by $C'[\_]$ and the bound names so that the names in the range of $\sigma$ are not bound by $C'[\_]$. Since $C[Q]$ is valid, we have $\mathsf{fv}(Q') \subseteq \mathsf{dom}(\varsigma)$, so $(t[a,c,\varsigma]\textnormal{::}\,Q')\sigma = t[a,c,\varsigma\sigma]\textnormal{::}\,Q'$, so $$\begin{aligned} \mathsf{barriers}((t[a,c,\varsigma]\textnormal{::}\,Q')\sigma) & =\mathsf{barriers}(t[a,c,\varsigma\sigma]\textnormal{::}\,Q')\\ & =\{t[a,c,\mathsf{ordom}(\varsigma\sigma)]\textnormal{::}\,Q'\} \cup \mathsf{barriers}(Q')\\ & =\{t[a,c,\mathsf{ordom}(\varsigma)]\textnormal{::}\,Q'\} \cup \mathsf{barriers}(Q')\\ & =\mathsf{barriers}(t[a,c,\varsigma]\textnormal{::}\,Q') \end{aligned}$$ Therefore, $\mathsf{barriers}(Q\sigma) = \mathsf{barriers}(Q)$. Hence, $\mathsf{channels}(\mathsf{barriers}(Q\sigma)) = \mathsf{channels}(\mathsf{barriers}(Q)) \subseteq \mathsf{channels}(\mathsf{barriers}(C[Q]))$ has pairwise distinct elements, and $$\begin{aligned} &\mathsf{channels}(\mathsf{barriers}(Q\sigma)) \cap \mathsf{fn\text{-}nobc}(Q\sigma)\\ &\quad \subseteq \mathsf{channels}(\mathsf{barriers}(Q)) \cap (\mathsf{fn\text{-}nobc}(Q) \cup \mathsf{fn}(\mathsf{range}(\sigma)))\\ &\quad \subseteq \mathsf{channels}(\mathsf{barriers}(C[Q])) \cap \mathsf{fn\text{-}nobc}(Q) = \emptyset\,. \end{aligned}$$ Consider an annotated barrier in $Q\sigma$, such that $Q\sigma = C'[t[a,c,\varsigma]\textnormal{::}\,Q']$. Then $Q = C''[t[a,c,\varsigma']\textnormal{::}\,Q'']$, $C'[\_]= C''[\_]\sigma$, $\varsigma = \varsigma'\sigma$, and $Q' = Q''\sigma$, after renaming the bound variables so that the variables in $\mathsf{dom}(\sigma)$ are not bound by $C''[\_]$ nor by $\varsigma'$ and the bound names so that the names in the range of $\sigma$ are not bound by $C''[\_]$. Since $C[Q]$ is valid, $\mathsf{fv}(Q'') \subseteq \mathsf{dom}(\varsigma')$, so $Q' = Q''\sigma = Q''$. We have $\mathsf{fv}(Q') = \mathsf{fv}(Q'') \subseteq \mathsf{dom}(\varsigma') = \mathsf{dom}(\varsigma)$, $C'[\_]$ does not bind $a$, $c$, and the names in $\mathsf{fn}(Q') = \mathsf{fn}(Q'')$ since $C[C''[\_]]$ does not bind $a$, $c$, and the names in $\mathsf{fn}(Q'')$ and $C'[\_]$ binds the same names as $C''[\_]$. ◻

*Proof of Lemma 2.* We prove each of the properties (denoted in italics) below: *If $P$ is a valid process, then $\mathcal{C}_{\textnormal{init}}(P)$ is valid.* Suppose that $P$ is valid. As defined in Section 3.1, we have $\mathcal{C}_{\textnormal{init}}(P) = B, E, {\mathcal P}$, where $B = \mathsf{barriers}(P)$, $E = \mathsf{channels}(B)$, and ${\mathcal P}= \{ P\}$, so a fortiori $\mathsf{barriers}({\mathcal P}) \subseteq B$, $\mathsf{channels}(B) \subseteq E$, all processes in ${\mathcal P}$ are valid, the elements of $\mathsf{channels}(B) = \mathsf{channels}(\mathsf{barriers}(P))$ are pairwise distinct, and $\mathsf{channels}(B) \cap \mathsf{fn\text{-}nobc}({\mathcal P}) = \mathsf{channels}(\mathsf{barriers}(P)) \cap \mathsf{fn\text{-}nobc}(P) = \emptyset$. Therefore, $\mathcal{C}_{\textnormal{init}}(P)$ is valid. *Validity is preserved by reduction.* We proceed by cases on the reduction rule. - Cases $\mbox{\sc (Red Nil)}$ and $\mbox{\sc (Red Par)}$ are easy. - Case $\mbox{\sc (Red Repl)}$: Since barriers never occur under replication, the transformed process $!P$ contains no barrier. Preservation of validity follows easily. - Case $\mbox{\sc (Red Res)}$: Suppose that $B,E,{\mathcal P}\cup \{\nu\,n.P\}\;\rightarrow\;B,E \cup \{n'\},{\mathcal P}\cup \{P\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}\}$ by $\mbox{\sc (Red Res)}$, for some name $n'$ such that $n'\not\in E \cup \mathsf{fn}({\mathcal P}\cup \{\nu\,n.P\})$, and $B,E,{\mathcal P}\cup \{\nu\,n.P\}$ is a valid configuration. Suppose that an annotated barrier $t[a,c,\varsigma]\textnormal{::}\,Q$ occurs in $P$, so that $P = C[t[a,c,\varsigma]\textnormal{::}\,Q]$. Since $\nu\,n.P$ is valid, $\nu\,n.C[\_]$ does not bind the names $a$, $c$, and $\mathsf{fn}(Q)$ above the hole, hence $n\notin\{a,c\}\cup\mathsf{fn}(Q)$, so $$(t[a,c,\varsigma]\textnormal{::}\,Q)\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\} = t[a,c,\varsigma\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}]\textnormal{::}\,Q\,,$$ so $$\begin{aligned} \mathsf{barriers}((t[a,c,\varsigma]\textnormal{::}\,Q)\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}) & =\mathsf{barriers}(t[a,c,\varsigma\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}]\textnormal{::}\,Q)\\ & =\{t[a,c,\mathsf{ordom}(\varsigma\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\})]\textnormal{::}\,Q\} \cup \mathsf{barriers}(Q)\\ & =\{t[a,c,\mathsf{ordom}(\varsigma)]\textnormal{::}\,Q\} \cup \mathsf{barriers}(Q)\\ & =\mathsf{barriers}(t[a,c,\varsigma]\textnormal{::}\,Q) \end{aligned}$$ Therefore, $\mathsf{barriers}(P\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}) = \mathsf{barriers}(P) = \mathsf{barriers}(\nu\,n.P)$. Hence, we have $\mathsf{barriers}({\mathcal P}\cup \{P\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}\}) = \mathsf{barriers}({\mathcal P}\cup \{\nu\,n.P\}) \subseteq B$ and $\mathsf{channels}(B) \subseteq E \subseteq E \cup \{ n'\}$. The processes in ${\mathcal P}$ are valid. Let us show that the process $P\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}$ is valid. The process $P\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}$ is closed because $\nu\,n.P$ is closed. The elements of $\mathsf{channels}(\mathsf{barriers}(P\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\})) = \mathsf{channels}(\mathsf{barriers}(\nu\,n.P))$ are pairwise distinct. We have $$\begin{aligned} &\mathsf{channels}(\mathsf{barriers}(P\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\})) \cap \mathsf{fn\text{-}nobc}(P\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\})\\ &\quad \subseteq \mathsf{channels}(\mathsf{barriers}(\nu\,n.P)) \cap (\mathsf{fn\text{-}nobc}(\nu\,n.P) \cup \{ n'\}) = \emptyset \end{aligned}$$ because $n' \notin \mathsf{channels}(\mathsf{barriers}(\nu\,n.P))$ since $$\mathsf{channels}(\mathsf{barriers}(\nu\,n.P)) \subseteq \mathsf{channels}(B) \subseteq E$$ and $n' \notin E$. Consider an annotated barrier in $P\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}$, such that $P\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\} = C[t[a,c,\varsigma]\textnormal{::}\,Q]$. Since $n' \notin \mathsf{fn}(\nu\,n.P) = \mathsf{fn}(P) \setminus\{n\}$, $\nu\,n.P = \nu\,n.(P\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}\{\textnormal{\raisebox{2pt}{\footnotesize $n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n'$}}\}) =\nu\,n.(C[t[a,c,\varsigma]\textnormal{::}\,Q]\{\textnormal{\raisebox{2pt}{\footnotesize $n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n'$}}\})$. We rename the bound names in $C[\_]$ so that they are different from $n$ and $n'$, and let $C'[\_]= C[\_]\{\textnormal{\raisebox{2pt}{\footnotesize $n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n'$}}\}$. Then $\nu\,n.P = \nu\,n.C'[t[a\{\textnormal{\raisebox{2pt}{\footnotesize $n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n'$}}\},\allowbreak c\{\textnormal{\raisebox{2pt}{\footnotesize $n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n'$}}\},\allowbreak \varsigma\{\textnormal{\raisebox{2pt}{\footnotesize $n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n'$}}\}]\textnormal{::}\,\allowbreak Q\{\textnormal{\raisebox{2pt}{\footnotesize $n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n'$}}\}]$. Since $\nu\,n.P$ is valid, we have $\mathsf{fv}(Q) = \mathsf{fv}(Q\{\textnormal{\raisebox{2pt}{\footnotesize $n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n'$}}\}) \subseteq \mathsf{dom}(\varsigma\{\textnormal{\raisebox{2pt}{\footnotesize $n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n'$}}\}) = \mathsf{dom}(\varsigma)$ and $C[\_]$ does not bind $a$, $c$, and the names in $\mathsf{fn}(Q)$ above the hole since $\nu\,n.C'[\_]$ does not bind $a\{\textnormal{\raisebox{2pt}{\footnotesize $n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n'$}}\}$, $c\{\textnormal{\raisebox{2pt}{\footnotesize $n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n'$}}\}$, and the names of $\mathsf{fn}(Q\{\textnormal{\raisebox{2pt}{\footnotesize $n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n'$}}\})$ above the hole. The elements of $\mathsf{channels}(B)$ are pairwise distinct by hypothesis, and $$\begin{aligned} &\mathsf{channels}(B) \cap \mathsf{fn\text{-}nobc}({\mathcal P}\cup \{P\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}\})\\ &\quad \subseteq \mathsf{channels}(B) \cap (\mathsf{fn\text{-}nobc}({\mathcal P}\cup \{ \nu\,n.P \}) \cup \{ n'\}) = \emptyset \end{aligned}$$ because $n' \notin \mathsf{channels}(B)$ since $\mathsf{channels}(B) \subseteq E$ and $n' \notin E$. - Case $\mbox{\sc (Red I/O)}$: Suppose that $B,E,{\mathcal P}\cup \{\overline{N}\langle M\rangle.P, N(x).Q\}\;\rightarrow\;B,E,{\mathcal P}\cup \{P,Q\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}$ by $\mbox{\sc (Red I/O)}$ and $B,E,{\mathcal P}\cup \{\overline{N}\langle M\rangle.P, N(x).Q\}$ is a valid configuration. The term $M$ is ground since $\overline{N}\langle M\rangle.P$ is closed. Moreover, $\mathsf{channels}(\mathsf{barriers}(Q)) \cap \mathsf{fn}(M) = \emptyset$ since $\mathsf{channels}(\mathsf{barriers}({\mathcal P}\cup \{\overline{N}\langle M\rangle.P, N(x).Q\})) \cap \mathsf{fn\text{-}nobc}({\mathcal P}\cup \{\overline{N}\langle M\rangle.P, N(x).Q\}) = \emptyset$. Hence, by Lemma 17, we have $\mathsf{barriers}({\mathcal P}\cup \{P,Q\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}) = \mathsf{barriers}({\mathcal P}\cup \{P,Q\}) = \mathsf{barriers}({\mathcal P}\cup \{\overline{N}\langle M\rangle.P, N(x).Q\}) \subseteq B$. We have $\mathsf{channels}(B) \subseteq E$. The processes in ${\mathcal P}$ are valid. The validity of $P$ follows easily from the validity of $\overline{N}\langle M\rangle.P$. The process $Q\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$ is valid by Lemma 17. The elements of $\mathsf{channels}(B)$ are pairwise distinct by hypothesis, and $\mathsf{channels}(B) \cap \mathsf{fn\text{-}nobc}({\mathcal P}\cup \{P,Q\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}) \subseteq \mathsf{channels}(B) \cap \mathsf{fn\text{-}nobc}({\mathcal P}\cup \{\overline{N}\langle M\rangle.P, N(x).Q\}) = \emptyset$. Therefore, $B,E,{\mathcal P}\cup \{P,Q\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}$ is valid. - Case $\mbox{\sc (Red Destr 1)}$: Suppose that $B,E,{\mathcal P}\cup \{\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q\}\;\rightarrow\;B,E,{\mathcal P}\cup \{P\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}$ by $\mbox{\sc (Red Destr 1)}$, where $D\Downarrow M$, and $B,E,{\mathcal P}\cup \{\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q\}$ is a valid configuration. The term $M$ is ground since $D$ is ground, and $\mathsf{channels}(\mathsf{barriers}(P)) \cap \mathsf{fn}(M) = \emptyset$ since $\mathsf{channels}(\mathsf{barriers}(P)) \cap \mathsf{fn}(D) = \emptyset$, since $\mathsf{channels}(\mathsf{barriers}(\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q)) \mathrel\cap\allowbreak \mathsf{fn\text{-}nobc}(\allowbreak\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q) = \emptyset$ by validity of $\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q$. Hence, by Lemma 17, we have $$\begin{aligned} \mathsf{barriers}({\mathcal P}\cup \{P\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}) & = \mathsf{barriers}({\mathcal P}\cup \{P\}) \\ & \subseteq \mathsf{barriers}({\mathcal P}\cup \{\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q\})\\ & \subseteq B\,. \end{aligned}$$ We have $\mathsf{channels}(B) \subseteq E$. The processes in ${\mathcal P}$ are valid. The process $P\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$ is valid by Lemma 17. The elements of $\mathsf{channels}(B)$ are pairwise distinct by hypothesis, and $\mathsf{channels}(B) \cap \mathsf{fn\text{-}nobc}({\mathcal P}\cup \{P\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}) \subseteq \mathsf{channels}(B) \cap \mathsf{fn\text{-}nobc}({\mathcal P}\cup \{\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q\}) = \emptyset$. Therefore, $B,E,{\mathcal P}\cup \{P\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}$ is valid. - Case $\mbox{\sc (Red Destr 2)}$: Suppose that $B,E,{\mathcal P}\cup \{\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q\}\;\rightarrow\;B,E,{\mathcal P}\cup \{Q\}$ by $\mbox{\sc (Red Destr 2)}$ and $B,E,{\mathcal P}\cup \{\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q\}$ is a valid configuration. We have $\mathsf{barriers}({\mathcal P}\cup \{Q\}) \subseteq \mathsf{barriers}({\mathcal P}\cup \{\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q\}) \subseteq B$ and $\mathsf{channels}(B) \subseteq E$. The processes in ${\mathcal P}$ are valid. The validity of $Q$ follows easily from the validity of $\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q$. The elements of $\mathsf{channels}(B)$ are pairwise distinct, and $\mathsf{channels}(B) \cap \mathsf{fn\text{-}nobc}({\mathcal P}\cup \{ Q\}) \subseteq \mathsf{channels}(B) \cap \mathsf{fn\text{-}nobc}({\mathcal P}\cup \{\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q\}) = \emptyset$. Therefore, $B,E,{\mathcal P}\cup \{Q\}$ is valid. - Case $\mbox{\sc (Red Bar')}$: Let ${\mathcal P}_1 = {\mathcal P}\cup \{t\textnormal{::}\,P_1,\allowbreak \dots,\allowbreak t\textnormal{::}\,P_m, \allowbreak t[a_{m+1},c_{m+1},\varsigma_{m+1}]\textnormal{::}\,P_{m+1}, \allowbreak \dots, \allowbreak t[a_n,\allowbreak c_n, \allowbreak \varsigma_n]\textnormal{::}P_n\}$ ${\mathcal P}_2 = {\mathcal P}\cup \{P_1,\allowbreak \dots,\allowbreak P_m,\allowbreak P_{m+1}\varsigma_{m+1},\allowbreak \dots,\allowbreak P_n\varsigma_n\}$, and suppose that $B,E,{\mathcal P}_1 \rightarrow\;B',E,{\mathcal P}_2$ by $\mbox{\sc (Red Bar')}$, where $B = \{ t^m, t[a_{m+1},c_{m+1},\mathsf{ordom}(\varsigma_{m+1})]\textnormal{::}\,P_{m+1}, \allowbreak \dots, \allowbreak t[a_n,c_n,\mathsf{ordom}(\varsigma_n)]\textnormal{::}\,P_n \} \cup B'$; for all $t'$ such that $t' \leq t$, we have $t'\notin B'$ and $t'[\_]\textnormal{::}\,\_ \notin B'$; and $B,E,{\mathcal P}_1$ is a valid configuration. The substitution $\varsigma_i$ is ground since $t[a_i,c_i,\varsigma_i]\textnormal{::}\,P_i$ is closed and $\mathsf{channels}(\mathsf{barriers}(P_i)) \cap \mathsf{fn}(\mathsf{range}(\varsigma_i)) = \emptyset$ since $\mathsf{channels}(\mathsf{barriers}(t[a_i,c_i,\varsigma_i]\textnormal{::}\,P_i)) \cap \mathsf{fn\text{-}nobc}(t[a_i,c_i,\varsigma_i]\textnormal{::}\,P_i) = \emptyset$ since $t[a_i,c_i,\varsigma_i]\textnormal{::}\,P_i$ is valid. We have $$\begin{aligned} &\mathsf{barriers}({\mathcal P}_2)\\ &\quad = \mathsf{barriers}({\mathcal P}\cup \{P_1, \dots, P_m, P_{m+1}\varsigma_{m+1}, \dots,P_n\varsigma_n\})\\ &\quad = \mathsf{barriers}({\mathcal P}\cup \{P_1, \dots, P_n\})\tag*{by Lemma~\ref{lem:valid-subst}}\\ &\quad = \mathsf{barriers}({\mathcal P}_1) \setminus \{ t^m, t[a_{m+1},c_{m+1},\mathsf{ordom}(\varsigma_{m+1})]\textnormal{::}\,P_{m+1}, \dots, t[a_n,c_n,\mathsf{ordom}(\varsigma_n)]\textnormal{::}\,P_n \}\\ &\quad \subseteq B\setminus \{ t^m, t[a_{m+1},c_{m+1},\mathsf{ordom}(\varsigma_{m+1})]\textnormal{::}\,P_{m+1}, \dots, \allowbreak t[a_n,c_n,\mathsf{ordom}(\varsigma_n)]\textnormal{::}\,P_n \}\\ &\quad = B' \end{aligned}$$ and $\mathsf{channels}(B') \subseteq \mathsf{channels}(B) \subseteq E$. The processes in ${\mathcal P}$ are valid. The validity of $P_i$ for $i \leq m$ follows easily from the validity of $t\textnormal{::}\,P_i$. The process $P_i \varsigma_i$ for $i > m$ is valid by Lemma 17. The elements of $\mathsf{channels}(B') \subseteq \mathsf{channels}(B)$ are pairwise distinct, and $\mathsf{channels}(B') \cap \mathsf{fn\text{-}nobc}({\mathcal P}_2) \subseteq \mathsf{channels}(B) \cap \mathsf{fn\text{-}nobc}({\mathcal P}_1) = \emptyset$. *Validity is preserved by application of an adversarial context.* Let $\mathcal{C}= B, E, {\mathcal P}$ be a valid configuration and $C[\_]$ be an adversarial context. We have $C[\_]= \nu\,\tilde n.(\_ \mid Q)$ with $\mathsf{fv}(Q) = \emptyset$ and $\mathsf{barriers}(Q) = \emptyset$. We suppose that the names in $E$ have been renamed so that $\mathsf{fn}(Q) \cap E = \emptyset$. Then we have $C[\mathcal{C}] = B,E \cup \{\tilde n\},{\mathcal P}\cup\{Q\}$. Let us show that $C[\mathcal{C}]$ is valid. We have $$\begin{aligned} &\mathsf{barriers}({\mathcal P}\cup\{Q\}) = \mathsf{barriers}({\mathcal P}) \subseteq B\\ &\mathsf{channels}(B) \subseteq E \subseteq E \cup \{\tilde n\} \end{aligned}$$ All processes in ${\mathcal P}$ are valid and $Q$ is valid since it is closed and contains no barriers. The elements of $\mathsf{channels}(B)$ are pairwise distinct by hypothesis, and $\mathsf{channels}(B) \cap \mathsf{fn\text{-}nobc}({\mathcal P}\cup \{Q\}) = \emptyset$ because $\mathsf{channels}(B) \cap \mathsf{fn\text{-}nobc}({\mathcal P}) = \emptyset$ and $\mathsf{channels}(B) \cap \mathsf{fn\text{-}nobc}(Q) \subseteq E \cap \mathsf{fn}(Q) = \emptyset$. Therefore, $C[\mathcal{C}]$ is valid. *Validity is preserved by application of $\mathsf{fst}$ and $\mathsf{snd}$.* We consider the case of $\mathsf{fst}$. The case of $\mathsf{snd}$ is symmetric. We first show that, if biprocess $P$ is valid, then $\mathsf{fst}(P)$ is valid. Suppose that $P$ is valid. Since $P$ is closed and $\mathsf{fv}(\mathsf{fst}(P)) \subseteq \mathsf{fv}(P)$, the process $\mathsf{fst}(P)$ is also closed. The elements of $\mathsf{channels}(\mathsf{barriers}(\mathsf{fst}(P))) = \mathsf{channels}(\mathsf{barriers}(P))$ are pairwise distinct. We have $\mathsf{channels}(\mathsf{barriers}(\mathsf{fst}(P))) \cap \mathsf{fn\text{-}nobc}(\mathsf{fst}(P)) \subseteq \mathsf{channels}(\mathsf{barriers}(P)) \cap \mathsf{fn\text{-}nobc}(P) = \emptyset$. Consider an annotated barrier in $\mathsf{fst}(P)$, such that $\mathsf{fst}(P) = C[t[a,c,\varsigma]\textnormal{::}\,Q]$. Then $P = C'[t[a,c,\varsigma']\textnormal{::}\,Q']$ such that $C[\_]= \mathsf{fst}(C'[\_])$, $\varsigma = \mathsf{fst}(\varsigma')$, and $Q = \mathsf{fst}(Q')$. We have $\mathsf{fv}(Q) \subseteq \mathsf{fv}(Q') \subseteq \mathsf{dom}(\varsigma') = \mathsf{dom}(\varsigma)$, $C'[\_]$ does not bind $a$, $c$, nor the names in $\mathsf{fn}(Q')$ above the hole, so $C[\_]$ does not bind $a$, $c$, nor the names in $\mathsf{fn}(Q) \subseteq \mathsf{fn}(Q')$ above the hole, because $C[\_]$ binds the same names as $C'[\_]$. So $\mathsf{fst}(P)$ is valid. Next, we show that, if a configuration $B, E, {\mathcal P}$ is valid, then $\mathsf{fst}(B, E, {\mathcal P}) = \mathsf{fst}(B), E, \mathsf{fst}({\mathcal P})$ is valid. Suppose that $B, E, {\mathcal P}$ is valid. We have $$\begin{aligned} &\mathsf{barriers}(\mathsf{fst}({\mathcal P})) = \mathsf{fst}(\mathsf{barriers}({\mathcal P})) \subseteq \mathsf{fst}(B)\,,\\ &\mathsf{channels}(\mathsf{fst}(B)) = \mathsf{channels}(B) \subseteq E\,, \end{aligned}$$ all processes in $\mathsf{fst}({\mathcal P})$ are valid since all processes in ${\mathcal P}$ are valid, the elements of $\mathsf{channels}(\mathsf{fst}(B)) = \mathsf{channels}(B)$ are pairwise distinct, and $$\mathsf{channels}(\mathsf{fst}(B)) \cap \mathsf{fn\text{-}nobc}(\mathsf{fst}({\mathcal P})) \subseteq \mathsf{channels}(B) \cap \mathsf{fn\text{-}nobc}({\mathcal P}) = \emptyset\,.$$ So $\mathsf{fst}(B, E, {\mathcal P})$ is valid. ◻

# Proof of Lemma 4 (soundness of $\mathsf{split}$)

*Proof of Lemma 4.* The proof proceeds by induction on $Q$. - Case $Q = M$ with $(\mathsf{fv}(M) \cup \mathsf{fn}(M)) \cap U = \emptyset$. We have $\mathsf{split}({U}, {M}) = (x, (\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}))$ where $x$ is a fresh variable, so $Q' = x$ and $\varsigma = (\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}})$. Hence $Q'\varsigma = M = Q$, $(\mathsf{fv}(\mathsf{range}(\varsigma)) \cup \mathsf{fn}(\mathsf{range}(\varsigma))) \cap U = (\mathsf{fv}(M) \cup \mathsf{fn}(M)) \cap U = \emptyset$, $\mathsf{fv}(Q') = \mathsf{dom}(\varsigma) = \{x\}$, $\mathsf{fn}(Q') = \emptyset$, and $\mathsf{dom}(\varsigma)$ consists of fresh variables. - Case $Q = u$ with $u \in U$. We have $\mathsf{split}({U}, {u}) = (u, \emptyset)$, so $Q' = u$ and $\varsigma = \emptyset$. Hence $Q'\varsigma = u = Q$, $\mathsf{fv}(\mathsf{range}(\varsigma)) \cup \mathsf{fn}(\mathsf{range}(\varsigma)) = \emptyset$, $\mathsf{dom}(\varsigma) = \emptyset$, $\mathsf{fv}(Q') \subseteq U$, and $\mathsf{fn}(Q') \subseteq U$. - Case $Q = C[Q_1, \dots, Q_n]$. The considered contexts $C[\_]$ do not have any free names or variables. We have $\mathsf{split}({U}, {C[Q_1, \dots, Q_n]}) = (C[Q'_1,\dots,Q'_n], \varsigma)$ where for all $i \leq n$, $\mathsf{split}({U \cup U_i}, {Q_i}) = (Q'_i, \varsigma_i)$, $C[\_,\dots,\_]$ binds the names and variables in $U_i$ above the $i$-th hole, and $\varsigma = \varsigma_1 + \dots + \varsigma_n$, so $Q' = C[Q'_1,\dots,Q'_n]$. Hence $Q' \varsigma = C[Q'_1\varsigma_1,\dots,Q'_n\varsigma_n]$ because $Q'_i \varsigma = Q'_i \varsigma_i$, since $\mathsf{fv}(Q'_i) \subseteq \mathsf{dom}(\varsigma_i) \cup U$ and, for all $j \neq i$, $\mathsf{dom}(\varsigma_j)$ consists of fresh variables, so it does not intersect $\mathsf{dom}(\varsigma_i) \cup U$, and $C[\_,\dots,\_]$ does not capture names nor variables because $(\mathsf{fv}(\mathsf{range}(\varsigma_i)) \cup \mathsf{fn}(\mathsf{range}(\varsigma_i))) \cap U_i = \emptyset$ and $\mathsf{dom}(\varsigma_i) \cap U_i = \emptyset$. Moreover, $(\mathsf{fv}(\mathsf{range}(\varsigma)) \cup \mathsf{fn}(\mathsf{range}(\varsigma))) \cap U \subseteq \bigcup_{i \leq n} (\mathsf{fv}(\mathsf{range}(\varsigma_i)) \cup \mathsf{fn}(\mathsf{range}(\varsigma_i))) \cap (U \cup U_i) = \emptyset$. For all $i \leq n$, $\mathsf{dom}(\varsigma_i) \subseteq \mathsf{fv}(Q'_i)\subseteq \mathsf{dom}(\varsigma_i) \cup U \cup U_i$, so $\mathsf{dom}(\varsigma_i) \subseteq \mathsf{fv}(Q'_i) \setminus U_i \subseteq \mathsf{dom}(\varsigma_i) \cup U$ since $\mathsf{dom}(\varsigma_i) \cap U_i = \emptyset$, so by taking the union over $i \leq n$, $\mathsf{dom}(\varsigma) \subseteq \mathsf{fv}(Q') \subseteq \mathsf{dom}(\varsigma) \cup U$. For all $i \leq n$, $\mathsf{fn}(Q'_i) \subseteq U \cup U_i$, so $\mathsf{fn}(Q'_i) \setminus U_i \subseteq U$, so by taking the union over $i \leq n$, $\mathsf{fn}(Q') \subseteq U$. Finally, for all $i \leq n$, $\mathsf{dom}(\varsigma_i)$ consists of fresh variables, so $\mathsf{dom}(\varsigma)$ consists of fresh variables. ◻

# Proof of Proposition 5 (soundness of $\mathsf{annotate}$)

**Proposition 18**. *Let $B, E, {\mathcal P}$ be a valid configuration, and $n$ be a name, where $n \notin \mathsf{fn}({\mathcal P})$. We have $B, E, {\mathcal P}\approx B, E \cup \{n\}, {\mathcal P}$.*

*Proof.* If $n\in E$, the result is obvious. Let us prove it when $n \notin E \cup \mathsf{fn}({\mathcal P})$. When $B, E, {\mathcal P}$ is valid, $B, E \cup \{n\}, {\mathcal P}$ is a fortiori valid. We define the relation $\mathrel{\mathcal{R}}$ by $$(B, E, {\mathcal P}) \mathrel{\mathcal{R}}(B, E \cup \{n\}, {\mathcal P})$$ for any $B$, $E$, ${\mathcal P}$, $n$ such that $n \notin E \cup \mathsf{fn}({\mathcal P})$, and $B, E, {\mathcal P}$ and $B, E \cup \{n\}, {\mathcal P}$ are valid configurations. We have that $\mathrel{\mathcal{R}}\cup \mathrel{\mathcal{R}}^{-1}$ is symmetric and satisfies the three conditions of Definition 1. For condition 2, we assume $\mathcal{C}= (B, E, {\mathcal P})\mathrel{\mathcal{R}}\mathcal{C}' = (B, E \cup \{n\}, {\mathcal P})$ and $\mathcal{C}\rightarrow \mathcal{C}_1$. In case $\mathcal{C}\rightarrow \mathcal{C}_1$ is derived by ${\ensuremath{\mbox{\sc (Red Res)}}}$, we have ${\mathcal P}= {\mathcal P}' \cup \{\nu\,n_0.P\}$ and $\mathcal{C}= (B, E, {\mathcal P}' \cup \{\nu\,n_0.P\})$ reduces into $\mathcal{C}_1 = (B,E \cup \{n_1\},{\mathcal P}\cup \{P\{\textnormal{\raisebox{2pt}{\footnotesize $n_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n_0$}}\}\})$ with $n_1\notin E \cup \mathsf{fn}({\mathcal P})$. Moreover, $\mathcal{C}' = (B, E \cup \{n\}, {\mathcal P}' \cup \{\nu\,n_0.P\})$ reduces into $\mathcal{C}'_1 = (B,E \cup \{n'_1, n\},{\mathcal P}\cup \{P\{\textnormal{\raisebox{2pt}{\footnotesize $n'_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n_0$}}\}\})$ with $n'_1\notin E \cup \{n\} \cup \mathsf{fn}({\mathcal P})$. By the convention that configurations $(B, E, {\mathcal P})$ are considered equal modulo any renaming of the names in $E, {\mathcal P}$ that leaves $\mathsf{fn}({\mathcal P})\setminus E$ unchanged, we have $\mathcal{C}'_1 = (B,E \cup \{n_1, n'\},{\mathcal P}\cup \{P\{\textnormal{\raisebox{2pt}{\footnotesize $n_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n_0$}}\}\})$ for some $n' \notin E \cup \{n_1\} \cup \mathsf{fn}({\mathcal P})$, so $\mathcal{C}_1 \mathrel{\mathcal{R}}\mathcal{C}'_1$. The other cases are left to the reader. Hence ${\mathrel{\mathcal{R}}\cup \mathrel{\mathcal{R}}^{-1}} \subseteq {\approx}$. This property implies the desired equivalence. ◻

**Proposition 19**. *For any context $C[\_]$ without replication above the hole, any process $P$, barrier $t$, names $a, c$, ordered substitution $\varsigma$ such that $C[t\textnormal{::}\,P\varsigma]$ and $C[t[a,c,\varsigma]\textnormal{::}\,P]$ are valid processes, we have $$C[t\textnormal{::}\,P\varsigma] \approx C[t[a,c,\varsigma]\textnormal{::}\,P]$$*

*Proof.* We define the relations $\mathrel{\mathcal{R}}_0$ and $\mathrel{\mathcal{R}}_1$ by $$\begin{aligned} (B, E, {\mathcal P}) &\mathrel{\mathcal{R}}_0 (B', E, {\mathcal P})\\ (B, E, \{C[t\textnormal{::}\,P\varsigma]\} \cup {\mathcal P}) &\mathrel{\mathcal{R}}_1 (B', E, \{C[t[a,c,\varsigma]\textnormal{::}\,P]\} \cup {\mathcal P}) \end{aligned}$$ where $(B, E, {\mathcal P})$, $(B', E, {\mathcal P})$, $(B, E, \{C[t\textnormal{::}\,P\varsigma]\} \cup {\mathcal P})$, and $(B', E, \{C[t[a,c,\varsigma]\textnormal{::}\,P]\} \cup {\mathcal P})$ are valid configurations and for all $t'$, $B_{|t'} = B'_{|t'}$, where $B_{|t'}$ denotes the total number of barriers of the form $t'$ or $t'[a',c',\tilde{x}]\textnormal{::}\,P'$ in $B$. We show that ${\mathrel{\mathcal{R}}} = {\mathrel{\mathcal{R}}_0 \cup \mathrel{\mathcal{R}}_1 \cup \mathrel{\mathcal{R}}_1^{-1}}$ is symmetric and satisfies the three conditions of Definition 1. Conditions 1 and 3 are obvious. To prove Condition 2, we notice that, when $(B, E, {\mathcal P}) \mathrel{\mathcal{R}}(B', E, {\mathcal P}')$, ${\ensuremath{\mbox{\sc (Red Bar')}}}$ is enabled for barrier $t'$ in $(B, E, {\mathcal P})$ if and only if it is enabled in $(B', E, {\mathcal P}')$. Indeed, ${\ensuremath{\mbox{\sc (Red Bar')}}}$ is enabled for barrier $t'$ in $(B, E, {\mathcal P})$ when $B_{|t''} = 0$ for all $t'' < t'$ and ${\mathcal P}$ contains $B_{|t'}$ processes of form $t'\textnormal{::}\,P$ or $t'[a,c,\varsigma]\textnormal{::}\,P$. (Validity ensures that $\mathsf{barriers}({\mathcal P})\subseteq B$, so for barrier $t'$, $B$ and ${\mathcal P}$ contain the same number of standard, resp. annotated, barriers and the content of annotated barriers also matches.) From this property, we prove Condition 2: - Case 1: $(B, E, {\mathcal P}) \mathrel{\mathcal{R}}_0 (B', E, {\mathcal P})$ and $(B, E, {\mathcal P}) \xrightarrow{}\mathcal{C}_1$. If this reduction is by ${\ensuremath{\mbox{\sc (Red Bar')}}}$ for barrier $t'$, then $\mathcal{C}_1 = (B_1, E, {\mathcal P}_1)$ where $B_1$ is obtained from $B$ by removing all (standard or annotated) barriers $t'$. Let $B'_1$ be obtained from $B'$ by removing all (standard or annotated) barriers $t'$. Then we have $(B', E, {\mathcal P}) \xrightarrow{}(B'_1, E, {\mathcal P}_1)$ and $(B_1, E, {\mathcal P}_1) \mathrel{\mathcal{R}}_0 (B'_1, E, {\mathcal P}_1)$. Otherwise, $\mathcal{C}_1 = (B, E_1, {\mathcal P}_1)$, $(B', E, {\mathcal P}) \xrightarrow{}(B', \allowbreak E_1, \allowbreak {\mathcal P}_1)$ by the same reduction and $(B, \allowbreak E_1, \allowbreak {\mathcal P}_1) \mathrel{\mathcal{R}}_0 (B', \allowbreak E_1, \allowbreak {\mathcal P}_1)$. - Case 2: $(B, E, \{C[t\textnormal{::}\,P\varsigma]\} \cup {\mathcal P}) \mathrel{\mathcal{R}}_1 (B', \allowbreak E, \allowbreak \{C[t[a,c,\varsigma]\textnormal{::}\,P]\} \cup {\mathcal P})$ and $(B, \allowbreak E, \allowbreak \{C[t\textnormal{::}\,P\varsigma]\} \cup {\mathcal P}) \xrightarrow{}\mathcal{C}_1$. If this reduction reduces only processes in ${\mathcal P}$, then the same reduction applies on the other side, much like in Case 1, and the reduced processes are in $\mathrel{\mathcal{R}}_1$. If this reduction reduces $C[t\textnormal{::}\,P\varsigma]$ and is not ${\ensuremath{\mbox{\sc (Red Bar')}}}$ for barrier $t$, then the same reduction also applies on the other side. If the reduction eliminates $t\textnormal{::}\,P\varsigma$ (so the reduction reduces $C[t\textnormal{::}\,P\varsigma]$ by ${\ensuremath{\mbox{\sc (Red Destr 1)}}}$ or ${\ensuremath{\mbox{\sc (Red Destr 2)}}}$), then the reduced processes are in $\mathrel{\mathcal{R}}_0$. Otherwise, the reduced processes are still in $\mathrel{\mathcal{R}}_1$, and any substitutions are applied to $\varsigma$. (By validity, $\mathsf{fv}(P) \subseteq \mathsf{dom}(\varsigma)$, so substitutions leave $P$ unchanged.) If this reduction is ${\ensuremath{\mbox{\sc (Red Bar')}}}$ for barrier $t$, then context $C[\_]$ is empty. (When $n$ barriers $t$ reduce, ${\mathcal P}_0 = \{C[t\textnormal{::}\,P\varsigma]\} \cup {\mathcal P}$ contains $n$ barriers $t$ at the top-level and $B$ contains $n$ barriers $t$. Since $\mathsf{barriers}({\mathcal P}_0)\subseteq B$ by validity, all barriers $t$ in ${\mathcal P}_0$ are at the top-level and are reduced.) The reduction transforms $t\textnormal{::}\,P\varsigma$ into $P\varsigma$. The same reduction also applies on the other side, and transforms $t[a,c,\varsigma]\textnormal{::}\,P$ into $P\varsigma$, so the reduced processes are in $\mathrel{\mathcal{R}}_0$. - Case 3: $(B', E, \{C[t[a,c,\varsigma]\textnormal{::}\,P]\} \cup {\mathcal P}) \mathrel{\mathcal{R}}_1^{-1} (B, E, \{C[t\textnormal{::}\,P\varsigma]\} \cup {\mathcal P})$ and $(B, \allowbreak E, \allowbreak \{C[t[a,c,\varsigma]\textnormal{::}\,P]\} \cup {\mathcal P}) \xrightarrow{}\mathcal{C}_1$. This case can be treated similarly to Case 2. Hence ${\mathrel{\mathcal{R}}_0 \cup \mathrel{\mathcal{R}}_1 \cup \mathrel{\mathcal{R}}_1^{-1}} \subseteq {\approx}$. Let $$\begin{aligned} &B = \mathsf{barriers}(C[t\textnormal{::}\,P\varsigma])\,,\\ &B' = \mathsf{barriers}(C[t[a,c,\varsigma]\textnormal{::}\,P])\,,\\ &E = \mathsf{channels}(B)\,\text{, and}\\ &E' = \mathsf{channels}(B') = E \cup \{a,c\}\,. \end{aligned}$$ We have $$\begin{aligned} &\mathcal{C}_{\textnormal{init}}(C[t\textnormal{::}\,P\varsigma]) = B, E, \{C[t\textnormal{::}\,P\varsigma]\}\text{ and}\\ &\mathcal{C}_{\textnormal{init}}(C[t[a,c,\varsigma]\textnormal{::}\,P]) = B', E', \{C[t[a,c,\varsigma]\textnormal{::}\,P]\}\,. \end{aligned}$$ By Lemma 2, these configurations are valid. Furthermore, since $B, E, \{C[t\textnormal{::}\,P\varsigma]\}$ is valid, $B, \allowbreak E',\allowbreak \{C[t\textnormal{::}\,P\varsigma]\}$ is a fortiori valid, and since $C[t[a,c,\varsigma]\textnormal{::}\,P]$ is valid, $$\mathsf{channels}(\mathsf{barriers}(C[t[a,c,\varsigma]\textnormal{::}\,P])) \cap \mathsf{fn\text{-}nobc}(C[t[a,c,\varsigma]\textnormal{::}\,P]) = \emptyset\,,$$ so $\{a,c\} \cap \mathsf{fn\text{-}nobc}(C[t\textnormal{::}\,P\varsigma]) = \emptyset$ and the elements of multiset $\mathsf{channels}(\mathsf{barriers}(C[t[a,c,\varsigma]\textnormal{::}\,P]))$ are pairwise distinct, so $\{a,c\} \cap \mathsf{channels}(\mathsf{barriers}(C[t\textnormal{::}\,P\varsigma])) = \emptyset$, so $\{a,c \} \cap \mathsf{fn}(C[t\textnormal{::}\,P\varsigma]) = \emptyset$. By Proposition 18, $$B, E, \{C[t\textnormal{::}\,P\varsigma]\} \approx B, E', \{C[t\textnormal{::}\,P\varsigma]\}\,.$$ By the result shown above, $$B, E', \{C[t\textnormal{::}\,P\varsigma]\} \approx B', E', \{C[t[a,c,\varsigma]\textnormal{::}\,P]\}\,,$$ so by transitivity of $\approx$, $$\mathcal{C}_{\textnormal{init}}(C[t\textnormal{::}\,P\varsigma]) \approx\mathcal{C}_{\textnormal{init}}(C[t[a,c,\varsigma]\textnormal{::}\,P])\,,$$ which proves the desired result. ◻

*Proof of Proposition 5.* Let us first show that $P'_0 = \mathsf{annotate}(P_0)$ is valid. The proof is done by induction on the number of transformation steps made from $P_0$. First, the process after 0 transformation steps, $P_0$ itself, is valid. Indeed, since $P_0$ is a closed standard biprocess, it contains no annotated barrier, hence it is valid. Moreover, if the process after $n$ transformation steps is valid, then so is the process after $n+1$ transformation steps, because the transformation performed by $\mathsf{annotate}$ preserves validity: if $C[t\textnormal{::}\,Q]$ is valid, then $C[t[a,c,\varsigma]\textnormal{::}\,Q']$ is also valid, as we show next. We can then conclude that $P'_0 = \mathsf{annotate}(P_0)$ is valid as well. Let us show that, if $C[t\textnormal{::}\,Q]$ is valid, then $C[t[a,c,\varsigma]\textnormal{::}\,Q']$ is also valid. We have $\mathsf{fv}(t[a,c,\varsigma]\textnormal{::}\,Q') = \mathsf{fv}(\mathsf{range}(\varsigma)) \cup (\mathsf{fv}(Q') \setminus \mathsf{dom}(\varsigma)) = \mathsf{fv}(Q'\varsigma) = \mathsf{fv}(Q)$ since $\mathsf{fv}(Q') = \mathsf{dom}(\varsigma)$ by Lemma 3. Therefore, if $C[t\textnormal{::}\,Q]$ is closed, then $C[t[a,c,\varsigma]\textnormal{::}\,Q']$ is also closed. Since barriers are transformed in a top-down order, the barriers in $Q$ and $Q'$ are standard, so we have $$\mathsf{channels}(\mathsf{barriers}(C[t[a,c,\varsigma]\textnormal{::}\,Q'])) = \{ a, c\} \cup \mathsf{channels}(\mathsf{barriers}(C[t\textnormal{::}\,Q]))\,.$$ Since $a$ and $c$ are distinct fresh names, the elements of $\mathsf{channels}(\mathsf{barriers}(C[t[a,c,\varsigma]\textnormal{::}\,Q']))$ are pairwise distinct, and $$\begin{split} &\mathsf{channels}(\mathsf{barriers}(C[t[a,c,\varsigma]\textnormal{::}\,Q'])) \cap \mathsf{fn\text{-}nobc}(C[t[a,c,\varsigma]\textnormal{::}\,Q']) \\ &\quad \subseteq (\{a, c\} \cup \mathsf{channels}(\mathsf{barriers}(C[t\textnormal{::}\,Q]))) \cap \mathsf{fn\text{-}nobc}(C[t\textnormal{::}\,Q]) = \emptyset\,. \end{split}$$ - For the transformed barrier, $a$ and $c$ are fresh names, so $C[\_]$ does not bind $a$ nor $c$ above the hole. Moreover, by Lemma 3, $\mathsf{fv}(Q') \subseteq \mathsf{dom}(\varsigma)$ and $C[\_]$ does not bind the names in $\mathsf{fn}(Q')$ above the hole, since $\mathsf{fn}(Q') = \emptyset$. - For the annotated barriers that already occur in $C[t\textnormal{::}\,Q]$, we have $C[t\textnormal{::}\,Q] = C'[t'[a',c',\varsigma']\textnormal{::}\,Q'']$. Since barriers are transformed in a top-down order, the barriers in $Q$ are standard, so the annotated barriers in question occur in $C[\_]$, and two cases may happen: - The transformed barrier is under $t'[a',c',\varsigma']$, inside $Q''$: $$\begin{aligned} C[t\textnormal{::}\,Q] &= C'[t'[a',c',\varsigma']\textnormal{::}\,C''[t\textnormal{::}\,Q]]\\ C[t[a,c,\varsigma]\textnormal{::}\,Q'] &= C'[t'[a',c',\varsigma']\textnormal{::}\,C''[t[a,c,\varsigma]\textnormal{::}\,Q']] \end{aligned}$$ for some context $C''[\_]$. Since $C'[t'[a',\allowbreak c',\allowbreak \varsigma']\textnormal{::}\,\allowbreak C''[t\textnormal{::}\,Q]]$ is valid, we have $\mathsf{fv}(C''[t\textnormal{::}\,Q]) \subseteq \mathsf{dom}(\varsigma')$ and $C'[\_]$ does not bind $a'$, $c'$, nor the names in $\mathsf{fn}(C''[t\textnormal{::}\,Q])$ above the hole. Furthermore, $\mathsf{fv}(t[a,c,\varsigma]\textnormal{::}\,Q') = \mathsf{fv}(Q) = \mathsf{fv}(t\textnormal{::}\,Q)$, so $\mathsf{fv}(C''[t[a,c,\varsigma]\textnormal{::}\,Q']) \subseteq \mathsf{dom}(\varsigma')$. Moreover, $$\begin{aligned} \mathsf{fn}(t[a,c,\varsigma]\textnormal{::}\,Q') &= \{a,c\} \cup \mathsf{fn}(Q'\varsigma)\\ &= \{a,c\} \cup \mathsf{fn}(Q) \\ &= \{a,c\} \cup \mathsf{fn}(t\textnormal{::}\,Q)\,, \end{aligned}$$ so $\mathsf{fn}(C''[t[a,c,\varsigma]\textnormal{::}\,Q']) = \{a,c\} \cup \mathsf{fn}(C''[t\textnormal{::}\,Q])$. Since $a$ and $c$ are fresh, they are not bound by $C'[\_]$, so $C'[\_]$ does not bind the names in $\mathsf{fn}(C''[t[a,c,\varsigma]\textnormal{::}\,Q'])$ above the hole. - The transformed barrier and the barrier $t'[a',c',\varsigma']$ are not under one another: $$\begin{aligned} C[t\textnormal{::}\,Q] &= C''[t'[a',c',\varsigma']\textnormal{::}\,Q'', t\textnormal{::}\,Q]\\ C[t[a,c,\varsigma]\textnormal{::}\,Q'] &= C''[t'[a',c',\varsigma']\textnormal{::}\,Q'', t[a,c,\varsigma]\textnormal{::}\,Q'] \end{aligned}$$ for some context $C''[\_,\_]$ with two holes. Since $C''[t'[a',c',\varsigma']\textnormal{::}\,Q'', t\textnormal{::}\,Q]$ is valid, we have $\mathsf{fv}(Q'') \subseteq \mathsf{dom}(\varsigma')$ and $C''[\_,\_]$ does not bind $a'$, $c'$, nor the names in $\mathsf{fn}(Q'')$ above its first hole. In all cases, $C[t[a,c,\varsigma]\textnormal{::}\,Q']$ is valid. From an annotated biprocess $P'_0 = \mathsf{annotate}(P_0)$, we can rebuild $P_0$ by replacing each occurrence of an annotated barrier $t[a,c,\varsigma]\textnormal{::}\,Q$ with $t\textnormal{::}\, Q\varsigma$, by Lemma 3. Therefore, we can also rebuild $\mathsf{fst}(P_0)$ from $\mathsf{fst}(P'_0)$ by replacing each occurrence of an annotated barrier $t[a,c,\varsigma]\textnormal{::}\,Q$ (in $\mathsf{fst}(P'_0)$) with $t\textnormal{::}\, Q\varsigma$. Furthermore, since validity is preserved by application of $\mathsf{fst}$ (Lemma 2), the considered processes are valid. Hence by applying several times Proposition 19 and by transitivity of $\approx$, we obtain that $\mathsf{fst}(P'_0) \approx \mathsf{fst}(P_0)$. We obtain $\mathsf{snd}(P'_0) \approx \mathsf{snd}(P_0)$ symmetrically. ◻

# Proof of Lemma 8 (barrier elimination commutes with renaming and substitution)

$$\begin{array}{r@{}l} \mathsf{bar\text{-}elim}(Q \mid R)\sigma & {}= (\mathsf{bar\text{-}elim}(Q) \mid \mathsf{bar\text{-}elim}(R)) \sigma \\ & {}= \mathsf{bar\text{-}elim}(Q)\sigma \mid \mathsf{bar\text{-}elim}(R) \sigma \\ & {}= \mathsf{bar\text{-}elim}(Q\sigma) \mid \mathsf{bar\text{-}elim}(R \sigma) \\ & {}= \mathsf{bar\text{-}elim}(Q\sigma \mid R \sigma) \\ & {}= \mathsf{bar\text{-}elim}((Q \mid R) \sigma) \\[0.55em] % \mathsf{bar\text{-}elim}(!Q)\sigma & {}= {(!\mathsf{bar\text{-}elim}(Q))\sigma} \\ & {}= {!(\mathsf{bar\text{-}elim}(Q)\sigma)} \\ & {}= {!\mathsf{bar\text{-}elim}(Q\sigma)} \\ & {}= \mathsf{bar\text{-}elim}(!(Q\sigma)) \\ & {}= \mathsf{bar\text{-}elim}((!Q)\sigma) \\[0.55em] % %%%%% % \mathsf{bar\text{-}elim}(\nu\,n.Q)\sigma & {}= (\nu\,n.\mathsf{bar\text{-}elim}(Q))\sigma \\%&&\textrm{by definition of $\compilerISymb$} \\ & {}= \nu\,n'.(\mathsf{bar\text{-}elim}(Q)\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}\sigma)\\%&&\textrm{by application of $\sigma$} \\ & {}= \nu\,n'.(\mathsf{bar\text{-}elim}(Q\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\})\sigma)\\%&&\textrm{by Lemma~\ref{lem:substIbb}} \\ & {}= \nu\,n'.\mathsf{bar\text{-}elim}(Q\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}\sigma)\\%&&\textrm{by induction hypothsis} \\ & {}= \mathsf{bar\text{-}elim}(\nu\,n'.(Q\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}\sigma))\\%&&\textrm{by definition of $\compilerISymb$} \\ & {}= \mathsf{bar\text{-}elim}((\nu\,n.Q)\sigma)\\[0.55em]%&&\textrm{by application of $\sigma$} % %%%%% % \mathsf{bar\text{-}elim}(M(x).Q)\sigma & {}= (M(x).\mathsf{bar\text{-}elim}(Q))\sigma \\% &&\textrm{by definition of $\compilerISymb$}\\ & {}= M\sigma(x').(\mathsf{bar\text{-}elim}(Q)\{\textnormal{\raisebox{2pt}{\footnotesize $x'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\sigma) \\% &&\textrm{by application of $\sigma$} \\ & {}= M\sigma(x').\mathsf{bar\text{-}elim}(Q\{\textnormal{\raisebox{2pt}{\footnotesize $x'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\sigma) \\% &&\textrm{by induction hypothsis}\\ & {}= \mathsf{bar\text{-}elim}(M\sigma(x').(Q\{\textnormal{\raisebox{2pt}{\footnotesize $x'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\sigma)) \\% &&\textrm{by definition of $\compilerISymb$}\\ & {}= \mathsf{bar\text{-}elim}((M(x).Q)\sigma) \\[0.55em]%&&\textrm{by application of $\sigma$} \\ % %%%%% % \mathsf{bar\text{-}elim}(\overline{M}\langle N\rangle.Q)\sigma & {}= (\overline{M}\langle N\rangle.\mathsf{bar\text{-}elim}(Q))\sigma \\ & {}= \overline{M}\langle N\rangle\sigma.\mathsf{bar\text{-}elim}(Q)\sigma \\ & {}= \overline{M}\langle N\rangle\sigma.\mathsf{bar\text{-}elim}(Q\sigma) \\ & {}= \mathsf{bar\text{-}elim}(\overline{M}\langle N\rangle\sigma.Q\sigma) \\ & {}= \mathsf{bar\text{-}elim}((\overline{M}\langle N\rangle.Q)\sigma) \\[0.55em] % \mathsf{bar\text{-}elim}(\textnormal{let } x=D \textnormal{ in } Q \textnormal{ else }R)\sigma & {}= (\textnormal{let } x=D \textnormal{ in } \mathsf{bar\text{-}elim}(Q) \textnormal{ else }\mathsf{bar\text{-}elim}(R))\sigma \\ % &&\textrm{by definition of $\compilerISymb$}\\ & {} = \textnormal{let } x'=D\sigma \textnormal{ in } \mathsf{bar\text{-}elim}(Q)\{\textnormal{\raisebox{2pt}{\footnotesize $x'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\sigma \textnormal{ else }\mathsf{bar\text{-}elim}(R)\sigma \\ % &&\textrm{by application of $\sigma$} \\ & {}= \textnormal{let } x'=D\sigma \textnormal{ in } \mathsf{bar\text{-}elim}(Q\{\textnormal{\raisebox{2pt}{\footnotesize $x'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\sigma) \textnormal{ else }\mathsf{bar\text{-}elim}(R\sigma) \\ % &&\textrm{by induction hypothesis}\\ & {}= \mathsf{bar\text{-}elim}(\textnormal{let } x'=D\sigma \textnormal{ in } Q\{\textnormal{\raisebox{2pt}{\footnotesize $x'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\sigma \textnormal{ else }R\sigma) \\ % &&\textrm{by definition of $\compilerISymb$}\\ & {}= \mathsf{bar\text{-}elim}((\textnormal{let } x=D \textnormal{ in } Q \textnormal{ else }R)\sigma) % &&\textrm{by application of $\sigma$} \end{array}$$ $$\begin{array}{@{}l@{}} \mathsf{bar\text{-}elim}(t[a,c,(\textnormal{\raisebox{2pt}{\footnotesize $M_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_1$}}, \dots, \textnormal{\raisebox{2pt}{\footnotesize $M_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_n$}} )]\textnormal{::}\,Q)\sigma\\ \quad= (\overline{a}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1,\dots,M_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.c(z).\textnormal{let } z_1=\pi_{1,n}(z) \textnormal{ in } \dots \textnormal{let } z_n=\pi_{n,n}(z) \textnormal{ in }\mathsf{bar\text{-}elim}(Q))\sigma \\ \quad= \overline{a}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1\sigma,\dots,M_n\sigma}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.c(z).\textnormal{let } z'_1=\pi_{1,n}(z) \textnormal{ in } \dots \textnormal{let } z'_n=\pi_{n,n}(z) \textnormal{ in }\\ \quad\qquad\mathsf{bar\text{-}elim}(Q)\{\textnormal{\raisebox{2pt}{\footnotesize $z'_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_1$}},\dots,\textnormal{\raisebox{2pt}{\footnotesize $z'_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_n$}}\}\sigma \\ \quad= \overline{a}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1\sigma,\dots,M_n\sigma}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.c(z).\textnormal{let } z'_1=\pi_{1,n}(z) \textnormal{ in } \dots \textnormal{let } z'_n=\pi_{n,n}(z) \textnormal{ in }\\ \quad\qquad\mathsf{bar\text{-}elim}(Q\{\textnormal{\raisebox{2pt}{\footnotesize $z'_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_1$}},\dots,\textnormal{\raisebox{2pt}{\footnotesize $z'_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_n$}}\}\sigma) \\ \quad= \mathsf{bar\text{-}elim}(t[a,c,(\textnormal{\raisebox{2pt}{\footnotesize $M_1\sigma$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z'_1$}}, \dots, \textnormal{\raisebox{2pt}{\footnotesize $M_n\sigma$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z'_n$}} )]\textnormal{::}\, Q\{\textnormal{\raisebox{2pt}{\footnotesize $z'_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_1$}},\dots,\textnormal{\raisebox{2pt}{\footnotesize $z'_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_n$}}\}\sigma) \\ \quad= \mathsf{bar\text{-}elim}((t[a,c,(\textnormal{\raisebox{2pt}{\footnotesize $M_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_1$}}, \dots, \textnormal{\raisebox{2pt}{\footnotesize $M_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_n$}} )]\textnormal{::}\,Q)\sigma) \end{array}$$

Derivations for the inductive case of Lemma [lem:substIIb]

*Proof of Lemma [lem:substIIb].* Let us proceed by structural induction on $P$. In the base case, we derive $\mathsf{bar\text{-}elim}(0)\sigma = 0\sigma = 0 = \mathsf{bar\text{-}elim}(0) = \mathsf{bar\text{-}elim}(0\sigma)$ by definition of $\mathsf{bar\text{-}elim}$ and application of $\sigma$. The inductive cases (Figure 7) additionally apply the induction hypothesis. In Figure 7, we assume name $n'$ is fresh in the name restriction case; variable $x'$ is fresh in the input and expression evaluation cases; variables $z, z'_1, \dots, z'_n$ are fresh in the barrier case. We rename bound names and variables to fresh names and variables respectively, to avoid any name or variable capture. ◻

# Proof of Lemma 9 (barrier elimination preserves reduction)

*Proof of Lemma 9.* Suppose configurations $\mathcal{C}$, $\mathcal{C}'$, $\mathcal{C}_1$ and $\mathcal{C}'_1$ are given above. We proceed by case analysis of our reduction rules. First, we consider Property [prop1]. ${\ensuremath{\mbox{\sc (Red Nil)}}}$ In this case, ${\mathcal P}= {\mathcal P}_1 \cup \{0\}$ and $E = E_1$. It follows that $\mathsf{bar\text{-}elim}({\mathcal P}) = \mathsf{bar\text{-}elim}({\mathcal P}_1) \cup \{0\}$, hence, $\mathcal{C}'\xrightarrow{}\mathcal{C}_1'$. ${\ensuremath{\mbox{\sc (Red Repl)}}}$ In this case, $E = E_1$ and there exist a multiset of processes ${\mathcal P}_0$ and a process $R$ such that ${\mathcal P}= {\mathcal P}_0 \cup \{!R\}$ and ${\mathcal P}_1 = {\mathcal P}_0 \cup \{R,!R\}$. It follows that $\mathsf{bar\text{-}elim}({\mathcal P}) = \mathsf{bar\text{-}elim}({\mathcal P}_0) \cup \{\mathsf{bar\text{-}elim}(!R)\}$ and $\mathsf{bar\text{-}elim}({\mathcal P}_1) = \mathsf{bar\text{-}elim}({\mathcal P}_0) \cup \{\mathsf{bar\text{-}elim}(R),\mathsf{bar\text{-}elim}(!R)\}$. Moreover, since $\mathsf{bar\text{-}elim}(!R) = {!\mathsf{bar\text{-}elim}(R)}$, we have $\mathcal{C}' \xrightarrow{}\mathcal{C}_1'$. ${\ensuremath{\mbox{\sc (Red Par)}}}$ In this case, $E = E_1$ and there exist a multiset of processes ${\mathcal P}_0$ and processes $R$ and $R'$ such that ${\mathcal P}= {\mathcal P}_0 \cup \{R \mid R'\}$ and ${\mathcal P}_1 = {\mathcal P}_0 \cup \{R,R'\}$. It follows that $\mathsf{bar\text{-}elim}({\mathcal P}) = \mathsf{bar\text{-}elim}({\mathcal P}_0) \cup \{\mathsf{bar\text{-}elim}(R) \mid \mathsf{bar\text{-}elim}(R')\}$ and $\mathsf{bar\text{-}elim}({\mathcal P}_1) = \mathsf{bar\text{-}elim}({\mathcal P}_0) \cup \{\mathsf{bar\text{-}elim}(R), \mathsf{bar\text{-}elim}(R')\}$, hence, $\mathcal{C}' \xrightarrow{}\mathcal{C}_1'$. ${\ensuremath{\mbox{\sc (Red Res)}}}$ In this case, there exist a multiset of processes ${\mathcal P}_0$, a process $R$ and names $n$ and $n'$ such that ${\mathcal P}= {\mathcal P}_0 \cup \{\nu\,n.R\}$, $E_1 = E \cup \{n'\}$ and ${\mathcal P}_1 = {\mathcal P}_0 \cup \{R\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}\}$, where $n'\not\in E \cup \mathsf{fn}({\mathcal P})$. It follows that $\mathsf{bar\text{-}elim}({\mathcal P}) = \mathsf{bar\text{-}elim}({\mathcal P}_0) \cup \{\nu\,n.\mathsf{bar\text{-}elim}(R)\}$ and $\mathsf{bar\text{-}elim}({\mathcal P}_1) = \mathsf{bar\text{-}elim}({\mathcal P}_0) \cup \{\mathsf{bar\text{-}elim}(R\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\})\}$. We have $\mathsf{bar\text{-}elim}(R\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}) = \mathsf{bar\text{-}elim}(R)\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}$ by , hence, $\mathcal{C}'\rightarrow\mathcal{C}'_1$. ${\ensuremath{\mbox{\sc (Red I/O)}}}$ In this case, $E = E_1$ and there exist a multiset of processes ${\mathcal P}_0$, processes $R$ and $R'$, terms $M$ and $N$, and a variable $x$ such that ${\mathcal P}= {\mathcal P}_0 \cup \{\overline{N}\langle M\rangle.R, \allowbreak N(x).R'\}$ and ${\mathcal P}_1 = {\mathcal P}_0 \cup \{R,R'\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}$. It follows that $\mathsf{bar\text{-}elim}({\mathcal P}) = \mathsf{bar\text{-}elim}({\mathcal P}_0) \cup \{\overline{N}\langle M\rangle.\mathsf{bar\text{-}elim}(R), \allowbreak N(x).\mathsf{bar\text{-}elim}(R')\}$ and $\mathsf{bar\text{-}elim}({\mathcal P}_1) = \mathsf{bar\text{-}elim}({\mathcal P}_0) \cup \{\mathsf{bar\text{-}elim}(R), \allowbreak \mathsf{bar\text{-}elim}(R'\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\})\}$. Moreover, we have $\mathsf{bar\text{-}elim}(\allowbreak{}R'\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}) = \mathsf{bar\text{-}elim}(R')\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$ by , hence, $\mathcal{C}'\rightarrow\mathcal{C}'_1$. ${\ensuremath{\mbox{\sc (Red Destr 1)}}}$ In this case, $E = E_1$ and there exist a multiset of processes ${\mathcal P}_0$, processes $R$ and $R'$, an expression $D$, a term $M$, and a variable $x$ such that ${\mathcal P}= {\mathcal P}_0 \cup \{\textnormal{let } x=D \textnormal{ in } R \textnormal{ else }R'\}$ and ${\mathcal P}_1 = {\mathcal P}_0 \cup \{R\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}$, where $D\Downarrow M$. It follows that $\mathsf{bar\text{-}elim}({\mathcal P}) = \mathsf{bar\text{-}elim}({\mathcal P}_0) \cup \{\textnormal{let } x=D \textnormal{ in } \mathsf{bar\text{-}elim}(R) \textnormal{ else }\mathsf{bar\text{-}elim}(R')\}$ and $\mathsf{bar\text{-}elim}({\mathcal P}_1) = \mathsf{bar\text{-}elim}({\mathcal P}_0) \cup \{\mathsf{bar\text{-}elim}(R\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\})\}$. Moreover, we have $\mathsf{bar\text{-}elim}(R\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}) = \mathsf{bar\text{-}elim}(R)\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$ by , hence, $\mathcal{C}'\rightarrow\mathcal{C}'_1$. ${\ensuremath{\mbox{\sc (Red Destr 2)}}}$ In this case, $E = E_1$ and there exist a multiset of processes ${\mathcal P}_0$, processes $R$ and $R'$, an expression $D$, and a variable $x$ such that ${\mathcal P}= {\mathcal P}_0 \cup \{\textnormal{let } x=D \textnormal{ in } R \textnormal{ else }R'\}$ and ${\mathcal P}_1 = {\mathcal P}_0 \cup \{R'\}$, where there is no $M$ such that $D\Downarrow M$. It follows that $\mathsf{bar\text{-}elim}({\mathcal P}) = \mathsf{bar\text{-}elim}({\mathcal P}_0) \cup \{\textnormal{let } x=D \textnormal{ in } \mathsf{bar\text{-}elim}(R) \textnormal{ else }\mathsf{bar\text{-}elim}(R')\}$ and $\mathsf{bar\text{-}elim}({\mathcal P}_1) = \mathsf{bar\text{-}elim}({\mathcal P}_0) \cup \{\mathsf{bar\text{-}elim}(R')\}$, hence, $\mathcal{C}' \xrightarrow{}\mathcal{C}_1'$. ${\ensuremath{\mbox{\sc (Red Bar')}}}$ By inspection of our reduction rules, the reduction $\mathcal{C}\xrightarrow{}\mathcal{C}_1$ cannot apply ${\ensuremath{\mbox{\sc (Red Bar')}}}$, since $B$ remains constant in the configurations $\mathcal{C}$ and $\mathcal{C}_1$. Secondly, we consider Property [prop2]. ${\ensuremath{\mbox{\sc (Red Nil)}}}$ In this case, $E = E_1$, $0\in\mathsf{bar\text{-}elim}({\mathcal P})$, and ${\mathcal P}'_1 = \mathsf{bar\text{-}elim}({\mathcal P}) \backslash\{0\}$. By definition of $\mathsf{bar\text{-}elim}$ (Figure 6), it follows immediately that $0\in{\mathcal P}$ and hence $\mathcal{C}\xrightarrow{}\mathcal{C}_1$, where $\mathcal{C}_1 = B,E_1,{\mathcal Q}\cup {\mathcal P}_1$ and ${\mathcal P}_1 = {\mathcal P}\backslash\{0\}$. Moreover, since $\mathsf{bar\text{-}elim}(0) = 0$, we have ${\mathcal P}'_1 = \mathsf{bar\text{-}elim}({\mathcal P}_1)$. ${\ensuremath{\mbox{\sc (Red Repl)}}}$ In this case, $E = E_1$ and there exist a multiset of processes ${\mathcal P}'_0$ and a process $R$ such that $\mathsf{bar\text{-}elim}({\mathcal P}) = {\mathcal P}'_0 \cup \{!R\}$ and ${\mathcal P}'_1 = {\mathcal P}'_0 \cup \{R,{!R}\}$. So there are ${\mathcal P}_0$ and $R_0$ such that ${\mathcal P}= {\mathcal P}_0 \cup \{R_0\}$ with ${\mathcal P}'_0 = \mathsf{bar\text{-}elim}({\mathcal P}_0)$ and $!R = \mathsf{bar\text{-}elim}(R_0)$. By definition of $\mathsf{bar\text{-}elim}$ (Figure 6), there exists a process $\hat R$ such that $\mathsf{bar\text{-}elim}(\hat R) = R$ and $R_0 = !\hat R$, so ${\mathcal P}= {\mathcal P}_0 \cup \{!\hat R\}$. Let ${\mathcal P}_1 = {\mathcal P}_0 \cup \{\hat R, {! \hat R}\}$. It follows immediately that $\mathcal{C}\xrightarrow{}\mathcal{C}_1$, where $\mathcal{C}_1 = B,E_1,{\mathcal Q}\cup {\mathcal P}_1$ and ${\mathcal P}'_1 = \mathsf{bar\text{-}elim}({\mathcal P}_1)$. ${\ensuremath{\mbox{\sc (Red Par)}}}$ In this case, $E = E_1$ and there exist a multiset of processes ${\mathcal P}'_0$ and processes $R$ and $R'$ such that $\mathsf{bar\text{-}elim}({\mathcal P}) = {\mathcal P}'_0 \cup \{R \mid R'\}$ and ${\mathcal P}'_1 = {\mathcal P}'_0 \cup \{R,R'\}$. So there are ${\mathcal P}_0$ and $R_0$ such that ${\mathcal P}= {\mathcal P}_0 \cup \{R_0\}$ with ${\mathcal P}'_0 = \mathsf{bar\text{-}elim}({\mathcal P}_0)$ and $R \mid R' = \mathsf{bar\text{-}elim}(R_0)$. By definition of $\mathsf{bar\text{-}elim}$ (Figure 6), there exist processes $\hat R$ and $\hat R'$ such that $\mathsf{bar\text{-}elim}(\hat R) = R$, $\mathsf{bar\text{-}elim}(\hat R') = R'$, and $R_0 = \hat R \mid \hat R'$, so ${\mathcal P}= {\mathcal P}_0 \cup \{\hat R \mid \hat R'\}$. Let ${\mathcal P}_1 = {\mathcal P}_0 \cup \{\hat R,\hat R'\}$. It follows immediately that ${\mathcal P}'_1 = \mathsf{bar\text{-}elim}({\mathcal P}_1)$ and $\mathcal{C}\xrightarrow{}\mathcal{C}_1$, where $\mathcal{C}_1 = B,E_1,{\mathcal Q}\cup {\mathcal P}_1$. ${\ensuremath{\mbox{\sc (Red Res)}}}$ In this case, there exist a multiset of processes ${\mathcal P}'_0$, a process $R$ and names $n$ and $n'$ such that $E_1 = E \cup \{n'\}$, $\mathsf{bar\text{-}elim}({\mathcal P}) = {\mathcal P}'_0 \cup \{\nu\,n.R\}$, and ${\mathcal P}'_1 = {\mathcal P}'_0 \cup \{R\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}\}$, where $n'\not\in E \cup \mathsf{fn}({\mathcal P}'_0 \cup \{\nu\,n.R\})$. So there are ${\mathcal P}_0$ and $R_0$ such that ${\mathcal P}= {\mathcal P}_0 \cup \{R_0\}$ with ${\mathcal P}'_0 = \mathsf{bar\text{-}elim}({\mathcal P}_0)$ and $\nu\,n.R = \mathsf{bar\text{-}elim}(R_0)$. By definition of $\mathsf{bar\text{-}elim}$ (Figure 6), there exists a process $\hat R$ such that $R = \mathsf{bar\text{-}elim}(\hat R)$ and $R_0 = \nu\,n.\hat R$, so ${\mathcal P}= {{\mathcal P}_0} \cup \{\nu\,n.\hat R\}$. Let ${\mathcal P}_1 = {\mathcal P}_0 \cup \{\hat R\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}\}$. It follows that $\mathcal{C}\xrightarrow{}\mathcal{C}_1$ and $\mathsf{bar\text{-}elim}({\mathcal P}_1) = \mathsf{bar\text{-}elim}({\mathcal P}_0) \cup \{\mathsf{bar\text{-}elim}(\hat R\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\})\}$. Moreover, we have ${\mathcal P}'_1 = \mathsf{bar\text{-}elim}({\mathcal P}_1)$ by . ${\ensuremath{\mbox{\sc (Red I/O)}}}$ In this case, $E = E_1$ and there exist a multiset of processes ${\mathcal P}'_0$, processes $R$ and $R'$, terms $M$ and $N$, and a variable $x$ such that $\mathsf{bar\text{-}elim}({\mathcal P}) = {\mathcal P}'_0 \cup \{\overline{N}\langle M\rangle.R, \allowbreak N(x).R'\}$ and ${\mathcal P}'_1 = {\mathcal P}'_0 \cup \{R,R'\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}$. So there are ${\mathcal P}_0$, $R_0$, and $R'_0$ such that ${\mathcal P}= {\mathcal P}_0 \cup \{R_0, R'_0\}$ with ${\mathcal P}'_0 = \mathsf{bar\text{-}elim}({\mathcal P}_0)$, $\overline{N}\langle M\rangle.R = \mathsf{bar\text{-}elim}(R_0)$, and $N(x).R' = \mathsf{bar\text{-}elim}(R'_0)$. By definition of $\mathsf{bar\text{-}elim}$ (Figure 6), $N(x).R' = \mathsf{bar\text{-}elim}(R'_0)$ implies $N(x).\hat R' = R'_0$ for some process $\hat R'$ such that $\mathsf{bar\text{-}elim}(\hat R') = R'$. Moreover, $\overline{N}\langle M\rangle.R = \mathsf{bar\text{-}elim}(R_0)$ implies: 1) there exists a process $\hat R$ such that $R_0 = \overline{N}\langle M\rangle.\hat R$, where $\mathsf{bar\text{-}elim}(\hat R) = R$; or 2) $N$ is a name and there exist a barrier $t$, name $c$, ordered substitution $\varsigma$, process $R''$, variable $z$, and integer $n$, such that $R_0 = t[N,c,\varsigma]\textnormal{::}\,R''$, and $R = c(z).\textnormal{let } z_1=\pi_{1,n}(z) \textnormal{ in } \cdots\ \textnormal{let } z_n=\pi_{n,n}(z) \textnormal{ in }\mathsf{bar\text{-}elim}(R'')$. In the first case, ${\mathcal P}= {\mathcal P}_0 \cup \{\overline{N}\langle M\rangle.\hat R, N(x).\hat R'\}$. Let ${\mathcal P}_1 = {\mathcal P}_0 \cup \{\hat R, \hat R'\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}$. It follows that $\mathcal{C}\xrightarrow{}\mathcal{C}_1$, where $\mathcal{C}_1 = B,E_1,{\mathcal Q}\cup {\mathcal P}_1$. Moreover, we have $\mathsf{bar\text{-}elim}(\hat R'\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}) = \mathsf{bar\text{-}elim}(\hat R')\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$ by , hence, ${\mathcal P}'_1 = \mathsf{bar\text{-}elim}({\mathcal P}_1)$. We show that the second case cannot arise. Since $N$ is a name, we have $N \in \mathsf{fn\text{-}nobc}(N(x).\hat R') = \mathsf{fn\text{-}nobc}(R'_0) \subseteq \mathsf{fn\text{-}nobc}({\mathcal Q}\cup {\mathcal P})$. Furthermore, $N \in \mathsf{channels}(\mathsf{barriers}(t[N,c,\varsigma]\textnormal{::}\,R'')) = \mathsf{channels}(\mathsf{barriers}(R_0)) \subseteq \mathsf{channels}(\mathsf{barriers}({\mathcal Q}\cup {\mathcal P}))$ and since $\mathcal{C}$ is a valid configuration, we have $\mathsf{channels}(\mathsf{barriers}({\mathcal Q}\cup {\mathcal P})) \cap \mathsf{fn\text{-}nobc}({\mathcal Q}\cup {\mathcal P}) = \emptyset$, thereby deriving a contradiction. ${\ensuremath{\mbox{\sc (Red Destr 1)}}}$ In this case, $E = E_1$ and there exist a multiset of processes ${\mathcal P}'_0$, processes $R$ and $R'$, an expression $D$, a term $M$, and a variable $x$ such that $\mathsf{bar\text{-}elim}({\mathcal P}) = {\mathcal P}'_0 \cup \{\textnormal{let } x=D \textnormal{ in } R \textnormal{ else }R'\}$ and ${\mathcal P}'_1 = {\mathcal P}'_0 \cup \{R\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}$, where $D\Downarrow M$. So there are ${\mathcal P}_0$ and $R_0$ such that ${\mathcal P}= {\mathcal P}_0 \cup \{R_0\}$ with ${\mathcal P}'_0 = \mathsf{bar\text{-}elim}({\mathcal P}_0)$ and $\textnormal{let } x=D \textnormal{ in } R \textnormal{ else }R' = \mathsf{bar\text{-}elim}(R_0)$. By definition of $\mathsf{bar\text{-}elim}$ (Figure 6), there exist processes $\hat R$ and $\hat R'$ such that $\mathsf{bar\text{-}elim}(\hat R) = R$, $\mathsf{bar\text{-}elim}(\hat R') = R'$, and $R_0 = \textnormal{let } x=D \textnormal{ in } \hat R \textnormal{ else }\hat R'$, so ${\mathcal P}= {\mathcal P}_0 \cup \{\textnormal{let } x=D \textnormal{ in } \hat R \textnormal{ else }\hat R'\}$. Let ${\mathcal P}_1 = {\mathcal P}_0 \cup \{\hat R\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}$. It follows that $\mathcal{C}\xrightarrow{}\mathcal{C}_1$, where $\mathcal{C}_1 = B,E_1,{\mathcal Q}\cup {\mathcal P}_1$. Moreover, we have $\mathsf{bar\text{-}elim}({\mathcal P}_1) = \mathsf{bar\text{-}elim}({\mathcal P}_0) \cup \{\mathsf{bar\text{-}elim}(\hat R\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\})\}$. Furthermore, we have $\mathsf{bar\text{-}elim}(\hat R\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}) = \mathsf{bar\text{-}elim}(\hat R)\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$ by , hence, ${\mathcal P}'_1 = \mathsf{bar\text{-}elim}({\mathcal P}_1)$. ${\ensuremath{\mbox{\sc (Red Destr 2)}}}$ In this case, $E = E_1$ and there exist a multiset of processes ${\mathcal P}'_0$, processes $R$ and $R'$, an expression $D$, and a variable $x$ such that $\mathsf{bar\text{-}elim}({\mathcal P}) = {\mathcal P}'_0 \cup \{\textnormal{let } x=D \textnormal{ in } R \textnormal{ else }R'\}$ and ${\mathcal P}'_1 = {\mathcal P}'_0 \cup \{R'\}$, where there is no $M$ such that $D\Downarrow M$. So there are ${\mathcal P}_0$ and $R_0$ such that ${\mathcal P}= {\mathcal P}_0 \cup \{R_0\}$ with ${\mathcal P}'_0 = \mathsf{bar\text{-}elim}({\mathcal P}_0)$ and $\textnormal{let } x=D \textnormal{ in } R \textnormal{ else }R' = \mathsf{bar\text{-}elim}(R_0)$. By definition of $\mathsf{bar\text{-}elim}$ (Figure 6), there exist processes $\hat R$ and $\hat R'$ such that $\mathsf{bar\text{-}elim}(\hat R) = R$, $\mathsf{bar\text{-}elim}(\hat R') = R'$, and $R_0 = \textnormal{let } x=D \textnormal{ in } \hat R \textnormal{ else }\hat R'$, so ${\mathcal P}= {\mathcal P}_0 \cup \{\textnormal{let } x=D \textnormal{ in } \hat R \textnormal{ else }\hat R'\}$. Let ${\mathcal P}_1 = {\mathcal P}_0 \cup \{\hat R'\}$. It follows immediately that ${\mathcal P}'_1 = \mathsf{bar\text{-}elim}({\mathcal P}_1)$ and $\mathcal{C}\xrightarrow{}\mathcal{C}_1$, where $\mathcal{C}_1 = B,E_1,{\mathcal Q}\cup {\mathcal P}_1$. ${\ensuremath{\mbox{\sc (Red Bar')}}}$ By definition of $\mathsf{bar\text{-}elim}$, configuration $\mathcal{C}'$ does not contain barriers and therefore we do not consider applications of the rule ${\ensuremath{\mbox{\sc (Red Bar')}}}$. ◻

# Proof of Proposition 7 (main proposition) We introduce some rudimentary results (), before proving the main technical result (Proposition 7). An *annotated configuration* is a configuration in which all processes are annotated.

**Lemma 20**. *Suppose $\mathcal{C}= B,E,{\mathcal P}$ is a valid annotated configuration such that $\mathsf{bar\text{-}elim}(P) = \overline{N}\langle M\rangle.Q$ for some processes $P \in {\mathcal P}$ and $Q$, and terms $M$ and $N$, where $\mathsf{fn}(N)\cap E = \emptyset$. We have $\mathcal{C}\downarrow_N$.*

*Proof.* By definition of $\mathsf{bar\text{-}elim}$, either: 1) $P = \overline{N}\langle M\rangle.R\in {\mathcal P}$ for some process $R$ such that $\mathsf{bar\text{-}elim}(R) = Q$; or 2) $P = t[N,c,\varsigma]\textnormal{::}\,R\in {\mathcal P}$ for some barrier $t$, channel name $c$, ordered substitution $\varsigma$, and process $R$. In the first case, it follows immediately that $\mathcal{C}\downarrow_N$. We show that the second case cannot arise. By definition of a valid configuration (Definition 4), $\mathsf{channels}(\mathsf{barriers}({\mathcal P})) \subseteq E$, so $N \in E$, which contradicts the assumption $\mathsf{fn}(N)\cap E = \emptyset$. ◻

We define $$\begin{aligned} &\textrm{add-lets}(Q) = \Bigl\{ \textnormal{let } z_j=\pi_{j,n}(\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1, \dots, M_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}) \textnormal{ in } \cdots \textnormal{let } z_n=\pi_{n,n}(\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1, \dots, M_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}) \textnormal{ in }Q' \\ &\quad \mathrel{\Big|} \begin{array}{l} 1 \leq j \leq n, Q = Q'\{\textnormal{\raisebox{2pt}{\footnotesize $M_j$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_j$}}, \dots, \textnormal{\raisebox{2pt}{\footnotesize $M_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_n$}}\}, M_1, \ldots, M_n \text{ ground terms}, \\ z_j, \dots, z_n \text{ pairwise distinct variables} \end{array} \Bigr\} \cup \{ Q \} \end{aligned}$$

**Lemma 21**. *Let $Q' \in \textrm{add-lets}(Q)$ and $B, E, {\mathcal P}\cup \{Q'\}$ be a valid configuration. We have $B, E, {\mathcal P}\cup \{Q'\} \xrightarrow{}^* B, E, {\mathcal P}\cup \{ Q\}$. Furthermore, if $Q' \neq Q$ and $B, E, {\mathcal P}\cup \{Q'\} \xrightarrow{}B, E, {\mathcal P}\cup \{Q''\}$ by reducing $Q'$, then $Q'' \in \textrm{add-lets}(Q)$.*

*Proof.* If $Q' = Q$, then we have obviously $B, E, {\mathcal P}\cup \{Q'\} \xrightarrow{}^* B, E, {\mathcal P}\cup \{ Q\}$, with no reduction. Otherwise, $$Q' = \textnormal{let } z_j=\pi_{j,n}(\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1, \dots, M_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}) \textnormal{ in } \cdots \textnormal{let } z_n=\pi_{n,n}(\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1, \dots, M_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}) \textnormal{ in }Q_1$$ where $Q = Q_1\{\textnormal{\raisebox{2pt}{\footnotesize $M_j$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_j$}}, \dots, \textnormal{\raisebox{2pt}{\footnotesize $M_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_n$}}\}$, $M_1, \ldots, M_n$ are ground terms, $z_j, \dots, z_n$ are pairwise distinct variables, and $1 \leq j \leq n$. Then $B, E, {\mathcal P}\cup \{Q'\} \xrightarrow{}^* B, E, {\mathcal P}\cup \{ Q\}$ by $n-j+1$ applications of ${\ensuremath{\mbox{\sc (Red Destr 1)}}}$. If $B, E, {\mathcal P}\cup \{Q'\} \xrightarrow{}B, E, {\mathcal P}\cup \{Q''\}$ by reducing $Q'$, then this reduction is obtained by one application of ${\ensuremath{\mbox{\sc (Red Destr 1)}}}$, so $$Q'' = \textnormal{let } z_{j+1}=\pi_{j+1,n}(\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1, \dots, M_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}) \textnormal{ in } \cdots \textnormal{let } z_n=\pi_{n,n}(\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1, \dots, M_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}) \textnormal{ in }Q_2$$ where $Q_2 = Q_1\{\textnormal{\raisebox{2pt}{\footnotesize $M_j$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_j$}}\}$, so $$\begin{aligned} Q & = Q_1\{\textnormal{\raisebox{2pt}{\footnotesize $M_j$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_j$}}, \dots, \textnormal{\raisebox{2pt}{\footnotesize $M_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_n$}}\}\\ & = Q_2\{\textnormal{\raisebox{2pt}{\footnotesize $M_{j+1}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{j+1}$}}, \dots, \textnormal{\raisebox{2pt}{\footnotesize $M_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_n$}}\}\,. \end{aligned}$$ If $j

**Lemma 22**. *If $B, E, {\mathcal P}\cup \{ t[a,c,\varsigma]\textnormal{::}\,Q \}$ is a valid annotated configuration, then $c \notin \mathsf{fn}({\mathcal P}\cup \{ Q\varsigma \})$.*

*Proof.* By validity, the elements of multiset $\mathsf{channels}(B)$ are pairwise distinct. Since $\mathsf{channels}(B)$ contains $$\begin{aligned} \mathsf{channels}(\mathsf{barriers}( {\mathcal P}\cup \{ t[a,c,\varsigma]\textnormal{::}\,Q \})) & = \{a,c\} \cup \mathsf{channels}(\mathsf{barriers}({\mathcal P}\cup \{ Q \}))\\ & = \{a,c\} \cup \mathsf{channels}(\mathsf{barriers}({\mathcal P}\cup \{ Q\varsigma \}))\,, \end{aligned}$$ we have $c \notin \mathsf{channels}(\mathsf{barriers}({\mathcal P}\cup \{ Q\varsigma \}))$. Moreover $\mathsf{channels}(B) \cap \mathsf{fn\text{-}nobc}({\mathcal P}\cup\{ t[a,c,\varsigma]\textnormal{::}\,Q \}) = \emptyset$ so $c \notin \mathsf{fn\text{-}nobc}({\mathcal P}\cup\{ t[a,c,\varsigma]\textnormal{::}\,Q \}) \supseteq \mathsf{fn\text{-}nobc}({\mathcal P}\cup \{ Q \})\cup \mathsf{fn}(\mathsf{range}(\varsigma)) \supseteq \mathsf{fn\text{-}nobc}({\mathcal P}\cup \{ Q\varsigma \})$. Therefore, $c\notin \mathsf{fn}({\mathcal P}\cup \{ Q\varsigma \})$. ◻

These results allow us to prove Proposition 7.

*Proof of Proposition 7.* Suppose the configurations $\mathcal{C}_0$ and $\mathcal{C}'_0$ are given in Proposition 7. We will construct a symmetric relation $\mathrel{\mathcal{R}}$ such that $\mathsf{fst}(\mathcal{C}_0)\mathrel{\mathcal{R}}\mathsf{fst}(\mathcal{C}'_0)$, $\mathsf{snd}(\mathcal{C}_0)\mathrel{\mathcal{R}}\mathsf{snd}(\mathcal{C}'_0)$, and $\mathrel{\mathcal{R}}$ satisfies the three conditions of Definition 1. #### Relation $\mathrel{\mathcal{R}}$ We first define some functions $$\begin{aligned} &\mathsf{bar\text{-}elim}_{\textrm{in}}(\overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1, \dots, M_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle,Q) = {}\\* &\quad \big\{ c(z).\textnormal{let } z_1=\pi_{1,n}(z) \textnormal{ in } \cdots \textnormal{let } z_n=\pi_{n,n}(z) \textnormal{ in }\mathsf{bar\text{-}elim}(Q')\\* &\qquad \mathrel{\big|} Q = Q'\{\textnormal{\raisebox{2pt}{\footnotesize $M_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_1$}}, \dots, \textnormal{\raisebox{2pt}{\footnotesize $M_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_n$}}\}, z, z_1, \dots, z_n \text{ pairwise distinct variables} \big\}\\ &\mathsf{bar\text{-}elim}'_{\textrm{in}}(t[a,c,\varsigma]\textnormal{::}\,Q) = {}\\* &\quad \big\{ c(z).\textnormal{let } z_1=\pi_{1,n}(z) \textnormal{ in } \cdots \textnormal{let } z_n=\pi_{n,n}(z) \textnormal{ in }\mathsf{bar\text{-}elim}(Q) \\* &\qquad \mathrel{\big|} \varsigma = (\textnormal{\raisebox{2pt}{\footnotesize $M_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_1$}} \dots, \textnormal{\raisebox{2pt}{\footnotesize $M_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_n$}}), z \text{ variable different from }z_1, \dots, z_n \big\}\\ &\mathsf{swapper}_1(\emptyset) = \{ 0 \}\\ &\mathsf{swapper}_1(B) = {}\\* &\quad\begin{array}{@{}l@{}} \big\{a_1(x_1)\mathrel. \cdots \mathrel. a_n(x_n).\overline{c_1}\langle x_{f(1)}\rangle\mathrel. \cdots \mathrel. \overline{c_n}\langle x_{f(n)}\rangle.R\\ \big| \mathrel{} \textrm{$B = \{t[a_1,c_1,\tilde{z}_1]\textnormal{::}\, Q_1,\dots,t[a_n,c_n,\tilde{z}_n]\textnormal{::}\, Q_n\} \cup B'$,}\\ \quad\textrm{where $t'>t$ for all $t'[a,c,\tilde{z}]\textnormal{::}\,Q\in B'$;}\\ \quad\textrm{function $f$ is a permutation of $\{1,\dots,n\}$ such}\\ \quad\textrm{that $Q_l/\tilde{z}_l =_{\mathsf{ch}}Q_{f(l)}/\tilde{z}_{f(l)}$ for all $1 \leq l \leq n$;}\\ \quad\textrm{$R \in \mathsf{swapper}_1(B')$; and $x_1, \dots, x_n$ are pairwise distinct variables}\big\}\\ \textrm{if $B \neq \emptyset$} \end{array} \end{aligned}$$ The sets of processes $\mathsf{bar\text{-}elim}_{\textrm{in}}(\overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1, \dots, M_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle,Q)$ and $\mathsf{bar\text{-}elim}'_{\textrm{in}}(t[a,c,\varsigma]\textnormal{::}\,Q)$ represent partially reduced compiled barriers: the output on channel $a$ has been executed but not the input on channel $c$. For $\mathsf{bar\text{-}elim}'_{\textrm{in}}(t[a,c,\varsigma]\textnormal{::}\,Q)$, this set is computed from the process $t[a,c,\varsigma]\textnormal{::}\,Q$ before reduction of the barrier. For $\mathsf{bar\text{-}elim}_{\textrm{in}}(\overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1, \dots, M_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle,Q)$, this set is computed from the process $Q$ after reduction of the barrier. In this case, we need the additional argument $\overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1, \dots, M_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle$ representing the message sent on channel $c$ to know how to compile the barrier. The function $\mathsf{swapper}_1(B)$ is similar to $\mathsf{swapper}(B)$ but produces only one component of the $\mathsf{diff}$. Let us consider the smallest relations $\mathrel{\mathcal{R}}_1$, $\mathrel{\mathcal{R}}_2$ and $\mathrel{\mathcal{R}}_3$ between configurations such that the conditions below are satisfied. 1. Suppose that $B, E, {\mathcal P}\cup {\mathcal Q}$ is a valid annotated configuration, ${\mathcal P}= \{P_1, \allowbreak \dots, \allowbreak P_m\}$, ${\mathcal Q}= \{t[a_1,c_1,\varsigma_1]\textnormal{::}\,Q_1,\allowbreak \dots,\allowbreak t[a_k,c_k,\varsigma_k]\textnormal{::}\,Q_k\}$, $\varsigma_l = (\textnormal{\raisebox{2pt}{\footnotesize $M_{l,1}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{l,1}$}},\allowbreak \dots,\allowbreak \textnormal{\raisebox{2pt}{\footnotesize $M_{l,|\varsigma_l|}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{l,|\varsigma_l|}$}})$ for all $l \leq k$, $B = \{t[a_1,c_1,\tilde{z}_1]\textnormal{::}\,Q_1,\allowbreak \dots,\allowbreak t[a_n,c_n,\tilde{z}_n]\textnormal{::}\,Q_n\} \cup B'$, $t' > t$ for all $t'[a',c',\tilde{z}']\textnormal{::}\,Q' \in B'$, $k \leq n$, and $\tilde{z}_{l} = (z_{l,1}, \dots, z_{l,|\tilde{z}_{l}|})$ for all $l \leq n$. Finally, suppose $f$ is a permutation of $\{1,\dots,n\}$ such that, for all $1\leq l \leq n$, we have $Q_l/\tilde{z}_l =_{\mathsf{ch}}Q_{f(l)}/\tilde{z}_{f(l)}$. Let ${\mathcal P}' = \{P'_1, \dots, P'_m\}$ and ${\mathcal Q}' = \{Q'_1, \dots, Q'_k\}$, where $P'_i \in \textrm{add-lets}(\mathsf{bar\text{-}elim}(P_i))$ for all $i \leq m$ and $Q'_i \in \mathsf{bar\text{-}elim}'_{\textrm{in}}(t[a_i,c_i,\varsigma_i]\textnormal{::}\,Q_i)$ for all $i \leq k$. We have $$\Big( B,E,{\mathcal P}\cup {\mathcal Q}\Big) \mathrel{\mathcal{R}}_1 \Big(\emptyset, E,{\mathcal P}' \cup {\mathcal Q}' \cup \{R\} \Big)$$ where $$\begin{split} R &{} \in \Bigl\{ a_{k+1}(x_{k+1})\mathrel.\cdots\mathrel.a_n(x_n)\mathrel. \overline{c_{1}}\langle {N_{f(1)}}\rangle\mathrel.\cdots\mathrel.\overline{c_n}\langle{N_{f(n)}}\rangle\mathrel.R' \\ &\Big|\begin{array}{l@{}} \textrm{$N_{l} = \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_{l,1},\dots,M_{l,|\varsigma_{l}|}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$ for all $l\leq k$; $N_{l} = x_l$ for all $l > k$;}\\ \textrm{$R' \in \mathsf{swapper}_1(B')$; and variables $x_{k+1},\allowbreak\dots,\allowbreak{}x_n$ are pairwise distinct} \end{array}\Bigr\} \end{split}$$ 2. Configuration $\mathcal{C}= B,E,{\mathcal P}\cup {\mathcal Q}$ is waiting to synchronise at barrier $t$ and configuration $\mathcal{C}' = \emptyset, E,{\mathcal P}' \cup {\mathcal Q}' \cup \{R\}$ represents an encoding of such a synchronisation with swapping. Multiset ${\mathcal Q}$ contains $k$ processes that are ready to synchronise at barrier $t$, while $n$ processes are needed for the synchronisation to take place. The multiset ${\mathcal P}$ may contain other processes that will synchronise at barrier $t$. In the configuration $\mathcal{C}'$, the communications that implement the barrier $t$ are partly done: the $k$ processes in ${\mathcal Q}'$, corresponding to the $k$ processes in ${\mathcal Q}$, have output messages on private channels and are awaiting input on private channels, i.e., the processes are ready to synchronise at $t$. Process $R$ has received $k$ private channel inputs and is awaiting for a further $n-k$ private inputs; once all inputs have been received, process $R$ will respond to all processes waiting to synchronise. 3. Suppose $B, E, {\mathcal P}\cup {\mathcal Q}$ is a valid annotated configuration, such that ${\mathcal P}= \{P_1, \dots, P_m\}$ and ${\mathcal Q}= \{Q_1, \dots, Q_k\}$. Let ${\mathcal P}' = \{P'_1, \ldots, P'_m\}$ and ${\mathcal Q}' = \{Q'_1, \dots, Q'_k\}$, where $P'_i \in \textrm{add-lets}(\mathsf{bar\text{-}elim}(P_i))$ for all $i \leq m$, and $Q'_i \in \mathsf{bar\text{-}elim}_{\textrm{in}}(\overline{c_i}\langle M_i\rangle,Q_i)$ for all $i \leq k$, for some pairwise distinct names $c_1, \dots, c_k$ in $E \setminus \mathsf{fn}({\mathcal P}\cup {\mathcal Q})$, and some ground tuples $M_1, \dots, M_k$. We have $$\Big( B,E,{\mathcal P}\cup {\mathcal Q}\Big) \mathrel{\mathcal{R}}_2 \Big(\emptyset, E,{\mathcal P}' \cup {\mathcal Q}' \cup \{ R\}\Big)$$ where $R \in \{\overline{c_1}\langle M_1\rangle\mathrel.\cdots\mathrel.\overline{c_k}\langle M_k\rangle\mathrel.R' \mid R' \in \mathsf{swapper}_1(B) \}$. 4. Configuration $\mathcal{C}= B,E,{\mathcal P}\cup {\mathcal Q}$ has just synchronised and configuration $\mathcal{C}' = \emptyset, E, {\mathcal P}' \cup {\mathcal Q}' \cup \{R\}$ represents an encoding of such a synchronisation with swapping. When $k > 0$, the communications that implement the last barrier upon which synchronisation happened are not fully done yet: $k$ outputs remain in $R$, and correspondingly ${\mathcal Q}'$ contains $k$ processes ready to receive these outputs. The condition $Q'_i \in \mathsf{bar\text{-}elim}_{\textrm{in}}(\overline{c_i}\langle M_i\rangle,Q_i)$ constrains $M_i$ to be a tuple of terms that occur in $Q_i$, so that $Q'_i$ reduces to $\mathsf{bar\text{-}elim}(Q_i)$ after receiving $M_i$ on channel $c_i$. 5. Suppose ${\mathcal P}= \{P_1, \ldots, P_m\}$ is a multiset of processes such that $\mathsf{barriers}({\mathcal P}) = \emptyset$, and $E$ is a set of names. Let ${\mathcal P}' = \{P'_1, \dots, P'_m\}$ be a multiset of processes, where $P'_i \in \textrm{add-lets}(P_i)$ for all $i \leq m$. We have: $$\Big(\emptyset, E, {\mathcal P}\Big) \mathrel{\mathcal{R}}_3 \Big(\emptyset, E, {\mathcal P}'\Big)$$ Let ${\mathrel{\mathcal{R}}} = {\mathrel{\mathcal{R}}_1 \cup \mathrel{\mathcal{R}}_2 \cup \mathrel{\mathcal{R}}_3 \cup \mathrel{\mathcal{R}}_1^{-1} \cup \mathrel{\mathcal{R}}_2^{-1} \cup \mathrel{\mathcal{R}}_3^{-1}}$. #### Relation $\mathrel{\mathcal{R}}$ relates $\mathsf{fst}(\mathcal{C}_0)$ with $\mathsf{fst}(\mathcal{C}'_0)$ and $\mathsf{snd}(\mathcal{C}_0)$ with $\mathsf{snd}(\mathcal{C}'_0)$ Recall that $\mathcal{C}_0 = B_0,E,\{P_0\}$ and $\mathcal{C}'_0 = \emptyset, E,\{\mathsf{bar\text{-}elim}(P_0), R_0\}$, where $B_0 = \mathsf{barriers}(P_0)$, $E = \mathsf{channels}(B_0)$, and $R_0\in\mathsf{swapper}(B_0)$. By Lemma 2, $\mathcal{C}_0 = \mathcal{C}_{\textnormal{init}}(P_0)$ is valid, so $\mathsf{fst}(\mathcal{C}_0)$ and $\mathsf{snd}(\mathcal{C}_0)$ are valid. We notice that, if $R_0 \in \mathsf{swapper}(B_0)$, then $\mathsf{fst}(R_0) \in \mathsf{swapper}_1(\mathsf{fst}(B_0))$, using the identity function for $f$, and $\mathsf{snd}(R_0) \in \mathsf{swapper}_1(\mathsf{snd}(B_0))$, using the same function $f$ as in the computation of $R_0 \in \mathsf{swapper}(B_0)$. Hence we have $\mathsf{fst}(\mathcal{C}_0)\mathrel{\mathcal{R}}_2\mathsf{fst}(\mathcal{C}'_0)$ with $B = \mathsf{fst}(B_0)$, $k = 0$, ${\mathcal P}= \{\mathsf{fst}(P_0)\}$, ${\mathcal P}' = \mathsf{bar\text{-}elim}({\mathcal P})$, ${\mathcal Q}' = {\mathcal Q}= \emptyset$, $R = \mathsf{fst}(R_0)$, and $\mathsf{snd}(\mathcal{C}_0) \mathrel{\mathcal{R}}_2 \mathsf{snd}(\mathcal{C}'_0)$ similarly using $\mathsf{snd}$ instead of $\mathsf{fst}$. #### Relation $\mathrel{\mathcal{R}}$ satisfies the conditions of Definition 1 The relation $\mathrel{\mathcal{R}}$ is symmetric and it remains to show that $\mathrel{\mathcal{R}}$ satisfies the three conditions of Definition 1. Let us first introduce the following results about our relation.

**Fact 1**. *Given configurations $\mathcal{C}= B,E,{\mathcal P}\cup {\mathcal Q}$ and $\mathcal{C}'$ such that $\mathcal{C}\mathrel{\mathcal{R}}_2 \mathcal{C}'$, we have $\mathcal{C}' \xrightarrow{}^* \emptyset, E, \mathsf{bar\text{-}elim}({\mathcal P}\cup{\mathcal Q}) \cup \{ R' \}$, where $R' \in \mathsf{swapper}_1(B)$.*

*Proof of Fact 1.* We use the notations of the definition of $\mathrel{\mathcal{R}}_2$. We transform $\mathcal{C}'$ by applying $\mbox{\sc (Red I/O)}$ $k$ times between $R$ and $Q'_i$ for $i$ from 1 to $k$. Then $R$ reduces into $R' \in \mathsf{swapper}_1(B)$ and $Q'_i$ reduces into an element of $\textrm{add-lets}(\mathsf{bar\text{-}elim}(Q_i))$. By Lemma 21, we reduce $P'_i$ into $\mathsf{bar\text{-}elim}(P_i)$ and further reduce $Q'_i$ into $\mathsf{bar\text{-}elim}(Q_i)$, so Fact 1 holds. ◻

**Fact 2**. *Given configurations $\mathcal{C}$, $\mathcal{C}'$, and $\mathcal{C}_1$ such that $\mathcal{C}\mathrel{\mathcal{R}}_1 \mathcal{C}'$ with $k = n$ and $\mathcal{C}\xrightarrow{}\mathcal{C}_1$ by $\mbox{\sc (Red Bar')}$, we have $\mathcal{C}_1 \mathrel{\mathcal{R}}_2 \mathcal{C}'$.*

Fact 2 handles the swapping of data at barriers, so it is a key step of the proof.

*Proof of Fact 2.* We use the notations of the definition of $\mathrel{\mathcal{R}}_1$. Since ${\mathcal Q}$ contains $n$ barriers, we have $\mathcal{C}\xrightarrow{}\mathcal{C}_1 = B', E, {\mathcal P}\cup \{ Q_1\varsigma_1, \dots, Q_n\varsigma_n \}$ by $\mbox{\sc (Red Bar')}$. We have $\mathcal{C}' = \emptyset, E,{\mathcal P}' \cup {\mathcal Q}' \cup \{R\}$ and since $k = n$, we have $R = \overline{c_{1}}\langle {N_{f(1)}}\rangle\mathrel.\cdots\mathrel.\overline{c_n}\langle{N_{f(n)}}\rangle\mathrel.R'$ with $N_{l} = \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_{l,1},\dots,M_{l,|\varsigma_{l}|}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$ for all $l \leq n$ and $R' \in \mathsf{swapper}_1(B')$. Moreover, ${\mathcal Q}' = \{Q'_1, \dots, Q'_n\}$ with $Q'_i \in \mathsf{bar\text{-}elim}'_{\textrm{in}}(t[a_i,c_i,\varsigma_i]\textnormal{::}\,Q_i)$ for all $i \leq n$. Since for all $1\leq l \leq n$, $Q_l/\tilde{z}_l =_{\mathsf{ch}}Q_{f(l)}/\tilde{z}_{f(l)}$, we have $$Q_{l} \{\textnormal{\raisebox{2pt}{\footnotesize $y_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{l,1}$}},\dots,\textnormal{\raisebox{2pt}{\footnotesize $y_{|\tilde{z}_{l}|}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{l,|\tilde{z}_{l}|}$}}\} =_{\mathsf{ch}} Q_{f(l)} \{\textnormal{\raisebox{2pt}{\footnotesize $y_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{f(l),1}$}},\dots,\textnormal{\raisebox{2pt}{\footnotesize $y_{|\tilde{z}_{l}|}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{f(l),|\tilde{z}_{l}|}$}}\}\,,$$ where $y_1,\dots,y_{|\tilde{z}_l|}$ are fresh variables, so we have $$Q_{l} \{\textnormal{\raisebox{2pt}{\footnotesize $y_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{l,1}$}},\dots,\textnormal{\raisebox{2pt}{\footnotesize $y_{|\tilde{z}_{l}|}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{l,|\tilde{z}_{l}|}$}}\} = Q_{f(l)} \{\textnormal{\raisebox{2pt}{\footnotesize $y_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{f(l),1}$}},\dots,\textnormal{\raisebox{2pt}{\footnotesize $y_{|\tilde{z}_{l}|}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{f(l),|\tilde{z}_{l}|}$}}\}\rho_l\,,$$ for some renaming $\rho_l$ of channels of annotated barriers. (Recall that processes are considered equal modulo renaming of bound names and variables.) The renaming $\rho_l$ maps names in $\mathsf{channels}(\mathsf{barriers}(Q_{f(l)}))$ to names in $\mathsf{channels}(\mathsf{barriers}(Q_l))$. Since the names in $\mathsf{channels}(\mathsf{barriers}({\mathcal P}\cup {\mathcal Q}))$ are pairwise distinct, for $l \neq l'$, $\mathsf{channels}(\mathsf{barriers}(Q_l)) \cap \mathsf{channels}(\mathsf{barriers}(Q_{l'})) = \emptyset$, so we can merge all functions $\rho_l$ for $1 \leq l \leq n$ into a single function $\rho$. Since furthermore $f$ is a permutation, $\rho$ is a permutation of $\mathsf{channels}(B')$ and leaves other names unchanged. Since the names in $\mathsf{channels}(\mathsf{barriers}({\mathcal P}\cup {\mathcal Q}))$ are pairwise distinct, $\rho$ leaves unchanged the names in $\mathsf{channels}(\mathsf{barriers}({\mathcal P}))$ and $a_1$, $c_1$, …, $a_n$, $c_n$. Hence, we obtain $$\mathsf{bar\text{-}elim}(Q_{i}) \{\textnormal{\raisebox{2pt}{\footnotesize $y_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{i,1}$}},\dots,\textnormal{\raisebox{2pt}{\footnotesize $y_{|\tilde{z}_{i}|}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{i,|\tilde{z}_{i}|}$}}\} = \mathsf{bar\text{-}elim}(Q_{f(i)})\{\textnormal{\raisebox{2pt}{\footnotesize $y_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{f(i),1}$}},\dots,\textnormal{\raisebox{2pt}{\footnotesize $y_{|\tilde{z}_{l}|}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{f(i),|\tilde{z}_{l}|}$}}\}\rho$$ for all $i \leq n$ by Lemma 8, so $$\mathsf{bar\text{-}elim}'_{\textrm{in}}(t[a_i,c_i,\varsigma_i]\textnormal{::}\,Q_i) = \mathsf{bar\text{-}elim}'_{\textrm{in}}(t[a_i,c_i,\varsigma_{f(i)}]\textnormal{::}\,Q_{f(i)})\rho$$ for all $i \leq n$. (Recall that processes are considered equal modulo renaming of bound variables.) So $Q'_i \in \mathsf{bar\text{-}elim}'_{\textrm{in}}(t[a_i,c_i,\varsigma_{f(i)}]\textnormal{::}\,Q_{f(i)})\rho$. Therefore, $Q'_i \in \mathsf{bar\text{-}elim}_{\textrm{in}}(\overline{c_i}\langle N_{f(i)}\rangle,\allowbreak Q_{f(i)}\varsigma_{f(i)})\rho$, so $Q'_i \rho^{-1} \in \mathsf{bar\text{-}elim}_{\textrm{in}}(\overline{c_i}\langle N_{f(i)}\rangle,Q_{f(i)}\varsigma_{f(i)})$. We define ${\mathcal Q}_1 = \{ Q_{1}\varsigma_1,\allowbreak\dots,\allowbreak Q_n\varsigma_n \} = \{ Q_{f(1)} \varsigma_{f(1)}, \dots, Q_{f(n)} \varsigma_{f(n)} \}$ since $f$ is a permutation of $\{1,\dots,n\}$, ${\mathcal Q}'_1 = \{ Q'_1\rho^{-1}, \dots, Q'_n \rho^{-1}\} = {\mathcal Q}'\rho^{-1}$, and $R_1 = R\rho^{-1} = \overline{c_{1}}\langle {N_{f(1)}}\rangle\mathrel.\cdots\mathrel.\overline{c_n}\langle{N_{f(n)}}\rangle\mathrel.R'_1$, where $R'_1 = R'\rho^{-1} \in \mathsf{swapper}_1(B'\rho^{-1})$ since $R' \in \mathsf{swapper}_1(B')$. Moreover, $B'\rho^{-1} = B'$ since $\rho^{-1}$ maps a barrier of $Q_l$ to a barrier of $Q_{f(l)}$ for all $l \leq n$ and leaves other barriers unchanged. Therefore, $R'_1 \in \mathsf{swapper}_1(B')$. Moreover, since $\mathcal{C}$ is valid, the elements of $\mathsf{channels}(B)$ are pairwise distinct so $c_1, \dots, c_n$ are pairwise distinct names. By Lemma 22, for all $i \leq n$, $c_i \notin \mathsf{fn}(\{Q_i\varsigma_i\} \cup {\mathcal P}\cup {\mathcal Q}\setminus \{t[a_i,c_i,\varsigma_i]\textnormal{::}\,Q_i\}) \supseteq \mathsf{fn}({\mathcal P}\cup {\mathcal Q}_1)$. Furthermore, $c_1, \dots, c_n$ are in $\mathsf{channels}(B)$, so they are in $E$ since $\mathcal{C}$ is valid, hence they are in $E \setminus \mathsf{fn}({\mathcal P}\cup {\mathcal Q}_1)$. We have $\mathcal{C}' = (\emptyset, E, {\mathcal P}' \cup {\mathcal Q}' \cup \{R\}) = (\emptyset, E\rho^{-1}, {\mathcal P}' \rho^{-1}\cup {\mathcal Q}'\rho^{-1} \cup \{R\rho^{-1}\})$ since configurations are considered equal modulo renaming, so $\mathcal{C}' = (\emptyset, E, {\mathcal P}' \cup {\mathcal Q}'_1 \cup \{R_1\})$. It follows that $\mathcal{C}_1 = (B', E, {\mathcal P}\cup {\mathcal Q}_1) \mathrel{\mathcal{R}}_2 \mathcal{C}' = (\emptyset, E, {\mathcal P}' \cup {\mathcal Q}'_1 \cup \{R_1\})$ using $N_{f(i)}$ for $M_i$ for all $i \leq n$. ◻

We proceed with the proof of Proposition 7 by showing that $\mathrel{\mathcal{R}}$ satisfies the three conditions of Definition 1. #### Condition 1 We show that, if $\mathcal{C}\mathrel{\mathcal{R}}' \mathcal{C}'$ and $\mathcal{C}\downarrow_N$, then $\mathcal{C}'\xrightarrow{}^*\downarrow_N$, where $\mathrel{\mathcal{R}}' \in \{{\mathrel{\mathcal{R}}_1}, {\mathrel{\mathcal{R}}_2}, {\mathrel{\mathcal{R}}_3}, \mathrel{\mathcal{R}}_1^{-1}, \mathrel{\mathcal{R}}_2^{-1}, \mathrel{\mathcal{R}}_3^{-1}\}$, by distinguishing the following cases: ${\mathrel{\mathcal{R}}'}={\mathrel{\mathcal{R}}_1}$. In this case, $\mathcal{C}= B,E,{\mathcal P}\cup {\mathcal Q}$ and $\mathcal{C}' = \emptyset, E,{\mathcal P}'\cup {\mathcal Q}' \cup\{R\}$. By inspection of ${\mathcal P}\cup {\mathcal Q}$, we have $P_i = \overline{N}\langle M\rangle.Q \in {\mathcal P}$ for some index $i$, process $Q$, and term $M$, with $\mathsf{fn}(N) \cap E = \emptyset$. It follows that $\mathsf{bar\text{-}elim}(P_i) = \overline{N}\langle M\rangle.\mathsf{bar\text{-}elim}(Q)$ and by Lemma 21, $P'_i \in \textrm{add-lets}(\mathsf{bar\text{-}elim}(P_i))$ reduces into $\mathsf{bar\text{-}elim}(P_i)$ inside $\mathcal{C}'$, hence $\mathcal{C}'\xrightarrow{}^*\downarrow_N$. ${\mathrel{\mathcal{R}}'}={\mathrel{\mathcal{R}}_2}$. In this case, $\mathcal{C}= B,E,{\mathcal P}\cup {\mathcal Q}$, where $\overline{N}\langle M\rangle.Q\in{\mathcal P}\cup {\mathcal Q}$ for some process $Q$ and term $M$, with $\mathsf{fn}(N) \cap E = \emptyset$. It follows that $\overline{N}\langle M\rangle.\mathsf{bar\text{-}elim}(Q) \in \mathsf{bar\text{-}elim}({\mathcal P}\cup{\mathcal Q})$. By Fact 1, we have $\mathcal{C}' \xrightarrow{}^* \mathcal{C}'_1 = \emptyset, E,\mathsf{bar\text{-}elim}({\mathcal P}\cup{\mathcal Q}) \cup \{ R' \}$, where $R' \in \mathsf{swapper}_1(B)$ and, moreover, $\mathcal{C}'_1\downarrow_N$, hence, $\mathcal{C}'\xrightarrow{}^*\downarrow_N$. ${\mathrel{\mathcal{R}}'}={\mathrel{\mathcal{R}}_3}$. In this case, $\mathcal{C}= \emptyset, E, {\mathcal P}$ and $\mathcal{C}' = \emptyset, E, {\mathcal P}'$, where $P_i = \overline{N}\langle M\rangle.Q\in{\mathcal P}$ for some index $i$, process $Q$ and term $M$, with $\mathsf{fn}(N) \cap E = \emptyset$. We have $P'_i \in \textrm{add-lets}(P_i)$, so by Lemma 21, $P'_i$ reduces into $P_i$ inside $\mathcal{C}'$. It follows immediately that $\mathcal{C}'\xrightarrow{}^*\downarrow_N$. ${\mathrel{\mathcal{R}}'}={\mathrel{\mathcal{R}}_1^{-1}}$. In this case, $\mathcal{C}= \emptyset,E,{\mathcal P}' \cup {\mathcal Q}' \cup\{R\}$ and $\mathcal{C}' = B, E,{\mathcal P}\cup {\mathcal Q}$. We have $\overline{N}\langle M\rangle.Q \in {\mathcal P}'\cup {\mathcal Q}' \cup \{R\}$ for some process $Q$ and term $M$, with $\mathsf{fn}(N) \cap E = \emptyset$. The process $R$ cannot be the output $\overline{N}\langle M\rangle.Q$ because if $k \neq n$, then $R$ starts with an input and if $k = n$, then $R$ starts with an output on channel $c_1 \in E$ since $\mathsf{channels}(B) \subseteq E$. Therefore, by inspection of ${\mathcal P}' \cup {\mathcal Q}' \cup\{R\}$, we have $P'_i = \overline{N}\langle M\rangle.Q = \mathsf{bar\text{-}elim}(P_i) \in {\mathcal P}'$ for some index $i$, and $\mathcal{C}'\downarrow_N$ by . ${\mathrel{\mathcal{R}}'}={\mathrel{\mathcal{R}}_2^{-1}}$. In this case $\mathcal{C}= \emptyset,E,{\mathcal P}' \cup {\mathcal Q}' \cup \{R\}$ and $\mathcal{C}' = B, E,{\mathcal P}\cup{\mathcal Q}$. We have $\overline{N}\langle M\rangle.Q \in {\mathcal P}'\cup {\mathcal Q}' \cup \{R\}$ for some process $Q$ and term $M$, with $\mathsf{fn}(N) \cap E = \emptyset$. If $k > 0$, then $R$ starts with an output on $c_1\in E\setminus\mathsf{fn}({\mathcal P}\cup {\mathcal Q})$. It follows immediately that $N\neq c_1$, since $\mathsf{fn}(N) \cap E = \emptyset$. If $k = 0$, then $R$ is either 0 or starts with an input, so in all cases, $R$ does not start with the output $\overline{N}\langle M\rangle.Q$. Therefore, by inspection of ${\mathcal P}' \cup {\mathcal Q}' \cup\{R\}$, we have $P'_i = \overline{N}\langle M\rangle.Q = \mathsf{bar\text{-}elim}(P_i) \in {\mathcal P}'$ for some index $i$, and $\mathcal{C}'\downarrow_N$ by . ${\mathrel{\mathcal{R}}'}={\mathrel{\mathcal{R}}_3^{-1}}$. In this case, $\mathcal{C}= \emptyset, E, {\mathcal P}'$ and $\mathcal{C}' = \emptyset, E, {\mathcal P}$. By inspection of ${\mathcal P}'$, it follows that $P'_i = \overline{N}\langle M\rangle.Q = P_i \in{\mathcal P}$ for some index $i$, process $Q$, and term $M$, with $\mathsf{fn}(N) \cap E = \emptyset$, and, hence, $\mathcal{C}'\downarrow_N$. #### Condition 2 We show that, if $\mathcal{C}\mathrel{\mathcal{R}}' \mathcal{C}'$ and $\mathcal{C}\xrightarrow{}\mathcal{C}_1$, then $\mathcal{C}'\xrightarrow{}^*\mathcal{C}'_1$ and $\mathcal{C}_1 \mathrel{\mathcal{R}}\mathcal{C}'_1$ for some $\mathcal{C}'_1$, where $\mathrel{\mathcal{R}}' \in \{{\mathrel{\mathcal{R}}_1}, {\mathrel{\mathcal{R}}_2}, {\mathrel{\mathcal{R}}_3}, \mathrel{\mathcal{R}}_1^{-1}, \mathrel{\mathcal{R}}_2^{-1}, \mathrel{\mathcal{R}}_3^{-1}\}$, by distinguishing the following cases: ${\mathrel{\mathcal{R}}'}={\mathrel{\mathcal{R}}_1}$. We have $\mathcal{C}= B,E,{\mathcal P}\cup {\mathcal Q}$ and $\mathcal{C}' = \emptyset, E, {\mathcal P}'\cup {\mathcal Q}' \cup\{ R\}$, with the conditions given in the definition of $\mathrel{\mathcal{R}}_1$. Let us distinguish two cases: - Case I: $\mathcal{C}\xrightarrow{}\mathcal{C}_1$ by ${\ensuremath{\mbox{\sc (Red Bar')}}}$. In this case, $\mathcal{C}= B, E, {\mathcal P}\cup {\mathcal Q}$, ${\mathcal Q}= \{t[a_1,c_1, \varsigma_1]\textnormal{::}\,Q_1,\allowbreak\dots,\allowbreak t[a_k,c_k,\varsigma_k]\textnormal{::}\,Q_k\}$, ${\mathcal P}= {\mathcal P}_1 \cup \{ t[a_{k+1},c_{k+1}, \varsigma_{k+1}]\textnormal{::}\,Q_{k+1},\allowbreak\dots,\allowbreak t[a_n,c_n,\varsigma_n]\textnormal{::}\,Q_n\}$, and $\mathcal{C}_1 =B',E,{\mathcal P}_1 \cup \{Q_{1}\varsigma_1,\dots,Q_n\varsigma_n\}$, where $B' = B \setminus \{t[a_1,c_1,\tilde{z}_1]\textnormal{::}\, Q_1,\dots,t[a_n,c_n,\tilde{z}_n]\textnormal{::}\, Q_n\}$ and $\tilde{z}_i = \mathsf{ordom}(\varsigma_i)$ for all $i \leq n$. For a suitable numbering of processes, we have $P_i = t[a_{k+i},c_{k+i}, \varsigma_{k+i}]\textnormal{::}\,Q_{k+i}$ for $i = 1, \dots, n-k$ and ${\mathcal P}_1 = \{P_{n-k+1}, \dots, P_m\}$. Since $\mathcal{C}\mathrel{\mathcal{R}}_1 \mathcal{C}'$, we have $\mathcal{C}' = \emptyset, E, {\mathcal P}' \cup {\mathcal Q}' \cup \{R\}$ where ${\mathcal P}' = \{P'_1, \dots, P'_m\}$ with $P'_i \in \textrm{add-lets}(\mathsf{bar\text{-}elim}(P_i))$ for all $i \leq m$ and ${\mathcal Q}' = \{Q'_1, \dots, Q'_k\}$ with $Q'_i \in \mathsf{bar\text{-}elim}'_{\textrm{in}}(t[a_i,c_i,\varsigma_i]\textnormal{::}\,Q_i)$ for all $i \leq k$. By Lemma 21, we can reduce the lets so that $\mathcal{C}' \xrightarrow{}^* \mathcal{C}'_2 = \emptyset, E, {\mathcal P}'_2 \cup {\mathcal Q}' \cup \{R\}$ where ${\mathcal P}'_2 = \{P''_1, \dots, P''_m\}$ with $P''_i = \mathsf{bar\text{-}elim}(P_i)$ for all $i \leq m$. Furthermore, we can reduce each $P''_i \in \mathsf{bar\text{-}elim}(t[a_{k+i},c_{k+i}, \varsigma_{k+i}]\textnormal{::}\,Q_{k+i})$ for $i = 1, \dots, n-k$ with $R$ by $\mbox{\sc (Red I/O)}$, so that $\mathcal{C}'_2 \xrightarrow{}^{n-k} \mathcal{C}'_1 = \emptyset, E, {\mathcal P}'_1 \cup {\mathcal Q}'_1 \cup \{R_1\}$, where ${\mathcal P}'_1 = \{ P''_{n-k+1}, \ldots, P''_m\}$ with $P''_i = \mathsf{bar\text{-}elim}(P_i)$ for $i = n-k+1, \dots, m$, ${\mathcal Q}'_1 = \{Q'_1, \dots, Q'_n\}$ with $Q'_i \in \mathsf{bar\text{-}elim}'_{\textrm{in}}(t[a_i,c_i,\varsigma_i]\textnormal{::}\,Q_i)$ for all $i \leq n$, and $R_1 = \overline{c_{1}}\langle {N_{f(1)}}\rangle.\cdots.\overline{c_n}\langle{N_{f(n)}}\rangle.R'$ where $N_{l} = \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_{l,1},\dots,M_{l,|\varsigma_{l}|}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$ for all $l \leq n$ and $R' \in \mathsf{swapper}_1(B')$. After these reductions, we obtain $\mathcal{C}\mathrel{\mathcal{R}}_1 \mathcal{C}'_1$ with $k = n$. By Fact 2, we have $\mathcal{C}_1 \mathrel{\mathcal{R}}_2 \mathcal{C}'_1$. Therefore, $\mathcal{C}_1 \mathrel{\mathcal{R}}\mathcal{C}'_1$ and $\mathcal{C}' \xrightarrow{}^* \mathcal{C}'_1$. - Case II: $\mathcal{C}\xrightarrow{}\mathcal{C}_1$ without application of ${\ensuremath{\mbox{\sc (Red Bar)}}}$. By inspection of our reduction rules, the reduction $\mathcal{C}\xrightarrow{}\mathcal{C}_1$ is obtained by reducing processes in ${\mathcal P}$ and $\mathcal{C}_1 = B,E_1,{\mathcal P}_1 \cup {\mathcal Q}$ for some multiset of processes ${\mathcal P}_1$ and set of names $E_1$. By Lemma 21, we can reduce the lets in ${\mathcal P}'$ so that $\mathcal{C}' \rightarrow^* \mathcal{C}'_2 = B, E_1, \mathsf{bar\text{-}elim}({\mathcal P}) \cup {\mathcal Q}' \cup \{R\}$. By Lemma 9 [prop1], $\mathcal{C}'_2\xrightarrow{}\mathcal{C}'_1$, where $\mathcal{C}'_1 = \emptyset,E_1, \mathsf{bar\text{-}elim}({\mathcal P}_1)\cup {\mathcal Q}' \cup \{ R \}$. Hence, $\mathcal{C}_1\mathrel{\mathcal{R}}_1\mathcal{C}'_1$ (with $k$, $n$, $f$ unchanged), therefore, $\mathcal{C}_1 \mathrel{\mathcal{R}}\mathcal{C}_1'$ and $\mathcal{C}' \xrightarrow{}^* \mathcal{C}'_1$. ${\mathrel{\mathcal{R}}'} = {\mathrel{\mathcal{R}}_2}$. We have $\mathcal{C}= B,E,{\mathcal P}\cup {\mathcal Q}$ and $\mathcal{C}' = \emptyset, E, {\mathcal P}' \cup {\mathcal Q}' \cup \{ R\}$, with the conditions given in the definition of $\mathrel{\mathcal{R}}_2$. By Fact 1, we have $\mathcal{C}' \xrightarrow{}^* \mathcal{C}'_2 = \emptyset, E,\mathsf{bar\text{-}elim}({\mathcal P}\cup{\mathcal Q})\cup\{ R'\}$, where $R' \in \mathsf{swapper}_1(B)$. - Case I: $B = \emptyset$. Since $\mathcal{C}$ is a valid configuration, we have $\mathsf{barriers}({\mathcal P}\cup{\mathcal Q}) \subseteq B$, so ${\mathcal P}$ and ${\mathcal Q}$ contain no barrier, therefore, ${\mathcal P}\cup {\mathcal Q}= \mathsf{bar\text{-}elim}({\mathcal P}\cup{\mathcal Q})$ by definition of $\mathsf{bar\text{-}elim}$ (Figure 6). By definition of $\mathsf{swapper}_1$, we have $R' = \{0\}$. Hence, $\mathcal{C}' \xrightarrow{}^* \mathcal{C}'_2 = \emptyset, E,{\mathcal P}\cup{\mathcal Q}\cup\{ 0\} \xrightarrow{}\mathcal{C}= \emptyset, E,{\mathcal P}\cup{\mathcal Q}$. Since $\mathcal{C}\xrightarrow{}\mathcal{C}_1$, we have $\mathcal{C}' \xrightarrow{}^* \mathcal{C}_1$. Moreover, we have $\mathcal{C}_1 \mathrel{\mathcal{R}}_3 \mathcal{C}_1$, so $\mathcal{C}_1 \mathrel{\mathcal{R}}\mathcal{C}_1$, and we conclude with $\mathcal{C}'_1 = \mathcal{C}_1$. - Case II: $B \neq \emptyset$. We have $\mathcal{C}\mathrel{\mathcal{R}}_1 \mathcal{C}'_2$ with $k = 0$ by expanding the definition of $\mathsf{swapper}_1(B)$, and we conclude by the case ${\mathrel{\mathcal{R}}'} = {\mathrel{\mathcal{R}}_1}$ above. ${\mathrel{\mathcal{R}}'} = {\mathrel{\mathcal{R}}_3}$. We have $\mathcal{C}= \emptyset,E,{\mathcal P}$ and $\mathcal{C}' = \emptyset, E,{\mathcal P}'$ with $\mathsf{barriers}({\mathcal P}) = \emptyset$ and $P'_i \in \textrm{add-lets}(P_i)$ for all $i \leq m$. By Lemma 21, we can reduce the lets in ${\mathcal P}'$ so that $\mathcal{C}' \xrightarrow{}^* \mathcal{C}= \emptyset, E,{\mathcal P}$. Since $\mathcal{C}\xrightarrow{}\mathcal{C}_1$, we have $\mathcal{C}' \xrightarrow{}^* \mathcal{C}_1$. Moreover, we have $\mathcal{C}_1 \mathrel{\mathcal{R}}_3 \mathcal{C}_1$, so $\mathcal{C}_1 \mathrel{\mathcal{R}}\mathcal{C}_1$, and we conclude with $\mathcal{C}'_1 = \mathcal{C}_1$. ${\mathrel{\mathcal{R}}'} = {\mathrel{\mathcal{R}}_1^{-1}}$. We have $\mathcal{C}= \emptyset, E,{\mathcal P}' \cup {\mathcal Q}' \cup \{R\}$ and $\mathcal{C}' = B,E,{\mathcal P}\cup {\mathcal Q}$, with the conditions given in the definition of $\mathrel{\mathcal{R}}_1$. - Case I: $k = n$. Since ${\mathcal Q}$ contains $n$ barriers, we have $\mathcal{C}' \xrightarrow{}\mathcal{C}'_2 = B', E, {\mathcal P}\cup \{ Q_1\varsigma_1, \dots, Q_n\varsigma_n \}$ by $\mbox{\sc (Red Bar')}$. By Fact 2, we have $\mathcal{C}'_2 \mathrel{\mathcal{R}}_2 \mathcal{C}$, so we conclude by the case ${\mathrel{\mathcal{R}}'} = {\mathrel{\mathcal{R}}_2^{-1}}$ (below). - Case II: $k < n$. - Case II.1: $\mathcal{C}\xrightarrow{}\mathcal{C}_1$ by reducing at least $R$. Since $R$ starts with an input on $a_{k+1}$, it can only reduce by $\mbox{\sc (Red I/O)}$ with an output on $a_{k+1}$. The processes in ${\mathcal Q}'$ start with an input, so they cannot reduce with $R$. Hence $R$ reduces with a process $P'_i \in \textrm{add-lets}(\mathsf{bar\text{-}elim}(P_i))$ in ${\mathcal P}'$. If $P'_i$ starts with a let, it cannot reduce by $\mbox{\sc (Red I/O)}$, so we have $P'_i = \mathsf{bar\text{-}elim}(P_i)$. Since $a_{k+1} \in \mathsf{channels}(B)$ and $\mathcal{C}'$ is valid, $a_{k+1} \notin \mathsf{fn\text{-}nobc}({\mathcal P}\cup {\mathcal Q})$, so $a_{k+1}$ occurs free in ${\mathcal P}\cup {\mathcal Q}$ only as channel of a barrier in ${\mathcal P}\cup {\mathcal Q}$. Since $P'_i = \mathsf{bar\text{-}elim}(P_i)$ starts with an output on $a_{k+1}$ and $\mathsf{barriers}(P_i) \subseteq B$, we have $P_i = t[a_{k+1},c_{k+1},\varsigma_{k+1}]\textnormal{::}\,Q_{k+1}$ for some $\varsigma_{k+1} = (\textnormal{\raisebox{2pt}{\footnotesize $M_{k+1,1}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{k+1,1}$}}, \allowbreak \dots, \allowbreak \textnormal{\raisebox{2pt}{\footnotesize $M_{k+1,|\varsigma_{k+1}|}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{k+1,|\varsigma_{k+1}|}$}})$. Let $N'_{k+1} = \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_{k+1,1},\dots,M_{k+1,|\varsigma_{k+1}|}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$ and for all $l \neq k+1$, $N'_l = N_l$. We have $$\begin{aligned} P'_i = {}&\overline{a_{k+1}}\langle N'_{k+1}\rangle.c_{k+1}(z). \textnormal{let } z_{k+1,1}=\pi_{1,|\varsigma_{k+1}|}(z) \textnormal{ in }\ \cdots\\ &\textnormal{let } z_{k+1,|\varsigma_{k+1}|}=\pi_{|\varsigma_{k+1}|,|\varsigma_{k+1}|}(z) \textnormal{ in } \mathsf{bar\text{-}elim}(Q_{k+1})\,. \end{aligned}$$ Let $$\begin{aligned} Q'_{k+1} &= c_{k+1}(z).\textnormal{let } z_{k+1,1}=\pi_{1,|\varsigma_{k+1}|}(z) \textnormal{ in }\cdots\\ &\phantom{{} = {}}\textnormal{let } z_{k+1,|\varsigma_{k+1}|}=\pi_{|\varsigma_{k+1}|,|\varsigma_{k+1}|}(z) \textnormal{ in } \mathsf{bar\text{-}elim}(Q_{k+1})\\ & \in \mathsf{bar\text{-}elim}'_{\textrm{in}}(t[a_{k+1},c_{k+1},\varsigma_{k+1}]\textnormal{::}\,Q_{k+1})\,. \end{aligned}$$ After reduction by $\mbox{\sc (Red I/O)}$, $P'_i$ becomes $Q'_{k+1}$ and $R$ becomes $R_1 = a_{k+2}(x_{k+2})\mathrel.\cdots\mathrel.a_n(x_n)\mathrel.\overline{c_{1}}\langle {N'_{f(1)}}\rangle\mathrel.\cdots\mathrel.\overline{c_n}\langle{N'_{f(n)}}\rangle\mathrel.R'$. Let ${\mathcal P}_1 = {\mathcal P}\setminus \{P_i\}$, ${\mathcal Q}_1 = {\mathcal Q}' \cup \{P_i\} = {\mathcal Q}' \cup \{ t[a_{k+1},c_{k+1},\varsigma_{k+1}]\textnormal{::}\,Q_{k+1} \}$, ${\mathcal P}'_1 = {\mathcal P}' \setminus \{ P'_i\}$, and ${\mathcal Q}'_1 = {\mathcal Q}' \cup \{Q'_{k+1}\}$. Then we have $\mathcal{C}= (\emptyset, E,{\mathcal P}' \cup {\mathcal Q}' \cup \{R\}) \xrightarrow{}\mathcal{C}_1 = (\emptyset, E, {\mathcal P}'_1 \cup {\mathcal Q}'_1 \cup \{R_1\})$ and $\mathcal{C}' = (B, E, {\mathcal P}_1 \cup {\mathcal Q}_1) \mathrel{\mathcal{R}}_1 \mathcal{C}_1 = (\emptyset, E, {\mathcal P}'_1 \cup {\mathcal Q}'_1 \cup \{R_1\})$ (with $m$ decreased by one, $k$ increased by one, and $f$ unchanged), so we conclude with $\mathcal{C}'_1 = \mathcal{C}'$. - Case II.2: $\mathcal{C}\xrightarrow{}\mathcal{C}_1$ by reducing at least a process in ${\mathcal Q}'$. Since we reduce $Q'_i \in {\mathcal Q}'$, which starts with an input on $c_i$, this process can only reduce by $\mbox{\sc (Red I/O)}$, with an output on $c_i$. If it reduced with $P'_j \in {\mathcal P}'$, since $P'_j \in \textrm{add-lets}(\mathsf{bar\text{-}elim}(P_j))$, we would actually have $P'_j = \mathsf{bar\text{-}elim}(P_j)$. Since $\mathcal{C}$ is valid, by Lemma 22, $c_i \notin \mathsf{fn}({\mathcal P})$, so $c_i \notin \mathsf{fn}(P'_j) = \mathsf{fn}(\mathsf{bar\text{-}elim}(P_j)) = \mathsf{fn}(P_j)$, hence $Q'_i$ cannot reduce with a process $P'_j \in {\mathcal P}'$. It also cannot reduce with $R$ or with another process in ${\mathcal Q}'$ since they start with an input. Therefore, this case cannot happen. - Case II.3: $\mathcal{C}\xrightarrow{}\mathcal{C}_1$ by reducing only processes in ${\mathcal P}'$. - Case II.3.1: a reduced process is $P'_i \neq \mathsf{bar\text{-}elim}(P_i)$. We have $P'_i \in \textrm{add-lets}(\allowbreak\mathsf{bar\text{-}elim}(\allowbreak{}P_i))$. By Lemma 21, $\mathcal{C}_1 = \emptyset, E,({\mathcal P}' \setminus \{P'_i\}) \cup \{P''_i\} \cup {\mathcal Q}' \cup \{R\}$ with $P''_i \in \textrm{add-lets}(\mathsf{bar\text{-}elim}(P_i))$, so we still have $\mathcal{C}' \mathrel{\mathcal{R}}_1 \mathcal{C}_1$, so we conclude with $\mathcal{C}'_1 = \mathcal{C}'$. - Case II.3.2: the reduced process(es) are $P'_i = \mathsf{bar\text{-}elim}(P_i)$ and possibly $P'_j = \mathsf{bar\text{-}elim}(P_j)$. Let ${\mathcal P}_{\textnormal{red}}' = \{P'_i\}$ or ${\mathcal P}_{\textnormal{red}}' = \{P'_i, P'_j\}$ be the multiset of reduced processes, such that ${\mathcal P}_{\textnormal{red}}' = \mathsf{bar\text{-}elim}({\mathcal P}_{\textnormal{red}})$, ${\mathcal P}' = {\mathcal P}_{\textnormal{stay}}' \cup {\mathcal P}_{\textnormal{red}}'$, ${\mathcal P}= {\mathcal P}_{\textnormal{stay}}\cup {\mathcal P}_{\textnormal{red}}$. We have $\mathcal{C}= (\emptyset, E, {\mathcal P}_{\textnormal{stay}}' \cup \mathsf{bar\text{-}elim}({\mathcal P}_{\textnormal{red}}) \cup {\mathcal Q}' \cup \{R\}) \xrightarrow{}\mathcal{C}_1 = (\emptyset, E_1, {\mathcal P}_{\textnormal{stay}}' \cup {\mathcal P}_{\textnormal{red1}}' \cup {\mathcal Q}' \cup \{R\})$ by reducing one or more processes in $\mathsf{bar\text{-}elim}({\mathcal P}_{\textnormal{red}})$, so by Lemma 9 [prop2], there exists ${\mathcal P}_{\textnormal{red1}}$ such that ${\mathcal P}_{\textnormal{red1}}' = \mathsf{bar\text{-}elim}({\mathcal P}_{\textnormal{red1}})$ and $\mathcal{C}' = (B, E, {\mathcal P}_{\textnormal{stay}}\cup {\mathcal P}_{\textnormal{red}}\cup {\mathcal Q}) \xrightarrow{}\mathcal{C}'_1 = (B, E, {\mathcal P}_{\textnormal{stay}}\cup {\mathcal P}_{\textnormal{red1}}\cup {\mathcal Q})$. Letting ${\mathcal P}_1 = {\mathcal P}_{\textnormal{stay}}\cup {\mathcal P}_{\textnormal{red1}}$ and ${\mathcal P}'_1 = {\mathcal P}_{\textnormal{stay}}' \cup {\mathcal P}_{\textnormal{red1}}'$, we obtain that $\mathcal{C}'_1 = (B, E, {\mathcal P}_1 \cup {\mathcal Q})\mathrel{\mathcal{R}}_1 \mathcal{C}_1 = (\emptyset, E_1, {\mathcal P}'_1 \cup {\mathcal Q}' \cup \{R\})$ (with $f$, $k$, $n$ unchanged), so $\mathcal{C}_1 \mathrel{\mathcal{R}}\mathcal{C}'_1$. ${\mathrel{\mathcal{R}}'} = {\mathrel{\mathcal{R}}_2^{-1}}$. We have $\mathcal{C}=\emptyset, E, {\mathcal P}' \cup {\mathcal Q}' \cup \{ R\}$ and $\mathcal{C}' = B,E,{\mathcal P}\cup {\mathcal Q}$, with the conditions given in the definition of $\mathrel{\mathcal{R}}_2$. We distinguish several cases. - Case I: $\mathcal{C}\xrightarrow{}\mathcal{C}_1$ by reducing at least $R$. - Case I.1: $k = 0$. In this case, ${\mathcal Q}= {\mathcal Q}' = \emptyset$. - Case I.1.1: $B = \emptyset$. Then $R = 0$, so $\mathcal{C}\xrightarrow{}\mathcal{C}_1 =\emptyset, E, {\mathcal P}'$, $\mathcal{C}' = \emptyset,E,{\mathcal P}$, and furthermore since $B = \emptyset$, we have $\mathsf{barriers}({\mathcal P}) = \emptyset$, so $P'_i \in \textrm{add-lets}(\mathsf{bar\text{-}elim}(P_i)) = \textrm{add-lets}(P_i)$, so $\mathcal{C}' \mathrel{\mathcal{R}}_3 \mathcal{C}_1$, so $\mathcal{C}_1 \mathrel{\mathcal{R}}\mathcal{C}'$. We conclude with $\mathcal{C}'_1 = \mathcal{C}'$. - Case I.1.2: $B \neq \emptyset$. Then we have $\mathcal{C}' \mathrel{\mathcal{R}}_1 \mathcal{C}$ by expanding the definition of $\mathsf{swapper}_1(B)$, we conclude by using the case ${\mathrel{\mathcal{R}}'} = {\mathrel{\mathcal{R}}_1^{-1}}$, Case II.1 ($k < n$, $\mathcal{C}\xrightarrow{}\mathcal{C}_1$ by reducing $R$, above). - Case I.2: $k > 0$. The process $R$ starts with an output on $c_1$, hence it can only reduce by $\mbox{\sc (Red I/O)}$ with an input on $c_1$. If $R$ reduced with $P'_i \in {\mathcal P}'$, since $P'_i \in \textrm{add-lets}(\mathsf{bar\text{-}elim}(P_i))$, we would actually have $P'_i = \mathsf{bar\text{-}elim}(P_i)$. By definition of $\mathrel{\mathcal{R}}_2$, $c_1 \notin \mathsf{fn}(P_i)$, so $c_1 \notin \mathsf{fn}(P'_i) = \mathsf{fn}(\mathsf{bar\text{-}elim}(P_i)) = \mathsf{fn}(P_i)$, hence $R$ cannot reduce with $P'_i \in {\mathcal P}'$. It cannot reduce with $Q'_i$ for $i > 1$ because $c_1, \dots, c_k$ are pairwise distinct. Therefore, $R$ reduces with $Q'_1$ by $\mbox{\sc (Red I/O)}$. After reduction, $R$ is transformed into $$R_1 = \overline{c_2}\langle M_2\rangle\mathrel.\cdots\mathrel.\overline{c_k}\langle M_k\rangle\mathrel.R'$$ with $R' \in \mathsf{swapper}_1(B)$, and since $Q'_1 \in \mathsf{bar\text{-}elim}_{\textrm{in}}(\overline{c_1}\langle M_1\rangle,Q_1)$, $$Q'_1 = c_1(z).\textnormal{let } z_1=\pi_{1,n}(z) \textnormal{ in } \cdots \textnormal{let } z_n=\pi_{n,n}(z) \textnormal{ in }\mathsf{bar\text{-}elim}(Q')$$ with $M_1 = \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{N_1,\dots, N_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$, $Q_1 = Q'\{\textnormal{\raisebox{2pt}{\footnotesize $N_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_1$}}, \dots, \textnormal{\raisebox{2pt}{\footnotesize $N_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_n$}}\}$, and $z, \allowbreak z_1, \allowbreak \dots, \allowbreak z_n$ pairwise distinct variables is transformed into $$\begin{aligned} P'_{m+1} &= \textnormal{let } z_1=\pi_{1,n}(M_1) \textnormal{ in } \cdots \textnormal{let } z_n=\pi_{n,n}(M_1) \textnormal{ in }\mathsf{bar\text{-}elim}(Q')\\ &\in \textrm{add-lets}(\mathsf{bar\text{-}elim}(Q_1)) \end{aligned}$$ because $\mathsf{bar\text{-}elim}(Q_1) = \mathsf{bar\text{-}elim}(Q')\{\textnormal{\raisebox{2pt}{\footnotesize $N_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_1$}}, \dots, \textnormal{\raisebox{2pt}{\footnotesize $N_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_n$}}\}$ by Lemma [lem:substIIb]. We let ${\mathcal P}_1 = {\mathcal P}\cup \{Q_1\}$, ${\mathcal Q}_1 = {\mathcal Q}\setminus \{Q_1\}$, ${\mathcal P}'_1 = {\mathcal P}' \cup \{P'_{m+1}\}$, and ${\mathcal Q}'_1 = {\mathcal Q}' \setminus \{Q'_1\}$. Then we have $\mathcal{C}= (\emptyset, E, {\mathcal P}' \cup {\mathcal Q}' \cup \{ R\}) \xrightarrow{} \mathcal{C}_1 = (\emptyset, E, {\mathcal P}'_1 \cup {\mathcal Q}'_1 \cup \{ R_1\})$ and $\mathcal{C}' = (B,E,{\mathcal P}\cup {\mathcal Q}) = (B,E,{\mathcal P}_1 \cup {\mathcal Q}_1) \mathrel{\mathcal{R}}_2 \mathcal{C}_1 = (\emptyset, E, {\mathcal P}'_1 \cup {\mathcal Q}'_1 \cup \{ R_1\})$ (with $k$ decreased by one and $m$ increased by one), so we conclude with $\mathcal{C}'_1 = \mathcal{C}'$. - Case II: $\mathcal{C}\xrightarrow{}\mathcal{C}_1$ by reducing at least a process in ${\mathcal Q}'$ and not reducing $R$. Since we reduce $Q'_i \in {\mathcal Q}'$, which starts with an input on $c_i$, this process can reduce only by $\mbox{\sc (Red I/O)}$, with an output on $c_i$. If it reduced with $P'_j \in {\mathcal P}'$, since $P'_j \in \textrm{add-lets}(\mathsf{bar\text{-}elim}(P_j))$, we would actually have $P'_j = \mathsf{bar\text{-}elim}(P_j)$. By definition of $\mathrel{\mathcal{R}}_2$, $c_i \notin \mathsf{fn}(P_j)$, so $c_i \notin \mathsf{fn}(P'_j) = \mathsf{fn}(\mathsf{bar\text{-}elim}(P_j)) = \mathsf{fn}(P_j)$, hence $Q'_i$ cannot reduce with a process $P'_j \in {\mathcal P}'$. Moreover, $Q'_i$ cannot reduce with another process in ${\mathcal Q}'$ because all these processes start with inputs. Therefore, this case is impossible. - Case III: $\mathcal{C}\xrightarrow{}\mathcal{C}_1$ by reducing only processes in ${\mathcal P}'$. This case is similar to the case ${\mathrel{\mathcal{R}}'} = {\mathrel{\mathcal{R}}_1^{-1}}$, Case II.3. ${\mathrel{\mathcal{R}}'} = {\mathrel{\mathcal{R}}_3^{-1}}$. We have $\mathcal{C}= \emptyset, E, {\mathcal P}'$ and $\mathcal{C}' = \emptyset, E, {\mathcal P}$ with $\mathsf{barriers}({\mathcal P}) = \emptyset$, ${\mathcal P}= \{P_1, \ldots, P_m\}$, ${\mathcal P}' = \{P'_1, \dots, P'_m\}$, and for all $i \leq m$, $P'_i \in \textrm{add-lets}(P_i)$. - Case I: a reduced process is $P'_i \neq P_i$. We have $P'_i \in \textrm{add-lets}(P_i)$. By Lemma 21, $\mathcal{C}_1 = \emptyset, E,({\mathcal P}' \setminus \{P'_i\}) \cup \{P''_i\}$ with $P''_i \in \textrm{add-lets}(P_i)$, so we still have $\mathcal{C}' \mathrel{\mathcal{R}}_3 \mathcal{C}_1$, so we conclude with $\mathcal{C}'_1 = \mathcal{C}'$. - Case II: the reduced process(es) are $P'_i = P_i$ and possibly $P'_j = P_j$. Let ${\mathcal P}_{\textnormal{red}}= \{P_i\}$ or ${\mathcal P}_{\textnormal{red}}= \{P_i, P_j\}$ be the multiset of reduced processes, ${\mathcal P}' = {\mathcal P}_{\textnormal{stay}}' \cup {\mathcal P}_{\textnormal{red}}$, and ${\mathcal P}= {\mathcal P}_{\textnormal{stay}}\cup {\mathcal P}_{\textnormal{red}}$. We have $\mathcal{C}= (\emptyset, E, {\mathcal P}_{\textnormal{stay}}' \cup {\mathcal P}_{\textnormal{red}}) \xrightarrow{}\mathcal{C}_1 = (\emptyset, E_1, {\mathcal P}_{\textnormal{stay}}' \cup {\mathcal P}_{\textnormal{red1}})$ by reducing one or more processes in ${\mathcal P}_{\textnormal{red}}$. Since the reduction rules are independent of the non-reduced processes, we also have $\mathcal{C}' = (\emptyset, E, {\mathcal P}_{\textnormal{stay}}\cup {\mathcal P}_{\textnormal{red}}) \xrightarrow{}\mathcal{C}'_1 = (\emptyset, E_1, {\mathcal P}_{\textnormal{stay}}\cup {\mathcal P}_{\textnormal{red1}})$ and furthermore $\mathcal{C}'_1 \mathrel{\mathcal{R}}_3 \mathcal{C}_1$, so $\mathcal{C}_1 \mathrel{\mathcal{R}}\mathcal{C}'_1$. #### Condition 3 We show that, if $\mathcal{C}\mathrel{\mathcal{R}}_i \mathcal{C}'$ and $C[\_]$ is an adversarial context, then $C[\mathcal{C}] \mathrel{\mathcal{R}}_i C[\mathcal{C}']$, for $i \in \{1, 2, 3\}$. Let $C[\_]= \nu\,\tilde n.(\_ \mid Q)$ with $\mathsf{fv}(Q) = \emptyset$ and $\mathsf{barriers}(Q) = \emptyset$. We rename $E$ in $\mathcal{C}$ and $\mathcal{C}'$ so that $E \cap \mathsf{fn}(Q) = \emptyset$. $i = 1$. We have $\mathcal{C}= B, E, {\mathcal P}\cup {\mathcal Q}$ and $\mathcal{C}' = \emptyset, E, {\mathcal P}' \cup {\mathcal Q}' \cup \{R\}$. Let ${\mathcal P}_1 = {\mathcal P}\cup \{Q\}$, ${\mathcal P}'_1 = {\mathcal P}' \cup \{Q\}$, and $E_1 = E \cup \{\tilde n\}$. Since $Q$ contains no barrier, we have $\mathsf{bar\text{-}elim}(Q) = Q$, so $Q \in \textrm{add-lets}(\mathsf{bar\text{-}elim}(Q))$, hence $C[\mathcal{C}] = (B, E_1, {\mathcal P}_1 \cup {\mathcal Q}) \mathrel{\mathcal{R}}_1 C[\mathcal{C}'] = (\emptyset, E_1, {\mathcal P}'_1 \cup {\mathcal Q}' \cup \{R\})$ (with $m$ increased by one and $k$, $n$, $f$ unchanged). $i = 2$. We have $\mathcal{C}= B, E, {\mathcal P}\cup {\mathcal Q}$ and $\mathcal{C}' = \emptyset, E, {\mathcal P}' \cup {\mathcal Q}' \cup \{R\}$. Let ${\mathcal P}_1 = {\mathcal P}\cup \{Q\}$, ${\mathcal P}'_1 = {\mathcal P}' \cup \{Q\}$, and $E_1 = E \cup \{\tilde n\}$. Since $Q$ contains no barrier, we have $\mathsf{bar\text{-}elim}(Q) = Q$, so $Q \in \textrm{add-lets}(\mathsf{bar\text{-}elim}(Q))$, hence $C[\mathcal{C}] = (B, E_1, {\mathcal P}_1 \cup {\mathcal Q}) \mathrel{\mathcal{R}}_2 C[\mathcal{C}'] = (\emptyset, E_1, {\mathcal P}'_1 \cup {\mathcal Q}' \cup \{R\})$ (with $m$ increased by one and $k$ unchanged.) $i = 3$. We have $\mathcal{C}= B, E, {\mathcal P}$ and $\mathcal{C}' = \emptyset, E, {\mathcal P}'$. Let ${\mathcal P}_1 = {\mathcal P}\cup \{Q\}$, ${\mathcal P}'_1 = {\mathcal P}' \cup \{Q\}$, and $E_1 = E \cup \{\tilde n\}$. We have $Q \in \textrm{add-lets}(Q)$, so $C[\mathcal{C}] = (B, E_1, {\mathcal P}_1) \mathrel{\mathcal{R}}_3 C[\mathcal{C}'] = (\emptyset, E_1, {\mathcal P}'_1)$ (with $m$ increased by one). #### Conclusion Since $\mathrel{\mathcal{R}}$ is symmetric and satisfies the three conditions of Definition 1, we have ${\mathrel{\mathcal{R}}} \subseteq {\approx}$. Since $\mathsf{fst}(\mathcal{C}_0)\mathrel{\mathcal{R}}\mathsf{fst}(\mathcal{C}'_0)$ and $\mathsf{snd}(\mathcal{C}_0)\mathrel{\mathcal{R}}\mathsf{snd}(\mathcal{C}'_0)$, we conclude that $\mathsf{fst}(\mathcal{C}_0)\approx\mathsf{fst}(\mathcal{C}'_0)$ and $\mathsf{snd}(\mathcal{C}_0)\approx\mathsf{snd}(\mathcal{C}'_0)$. ◻

# Proofs of Propositions 10 and 11

*Proof of Proposition 10.* We have $B, E, \{\nu\,n.P\}\cup{\mathcal P}\;\rightarrow\; B, E\cup\{n'\}, \{P\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}\}\cup{\mathcal P}$ by $\mbox{\sc (Red Res)}$, so by Lemma 2, $B, E\cup\{n'\}, \{P\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}\}\cup{\mathcal P}$ is also a valid configuration. We define the relations $\mathrel{\mathcal{R}}_0$ and $\mathrel{\mathcal{R}}_1$ by $$\begin{aligned} \mathcal{C}&\mathrel{\mathcal{R}}_0 \mathcal{C}\\ (B, E, \{\nu\,n.P\}\cup{\mathcal P}) &\mathrel{\mathcal{R}}_1 (B, E\cup\{n'\}, \{P\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}\}\cup{\mathcal P}) \end{aligned}$$ for any $\mathcal{C}$, $B$, $E$, $n$, $n'$, $P$, ${\mathcal P}$ such that $n'\not\in E \cup \mathsf{fn}(\{\nu\,n.P\}\cup{\mathcal P})$ and $\mathcal{C}$, $(B, E, \{\nu\,n.P\}\cup{\mathcal P})$, and $(B, E\cup\{n'\}, \{P\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}\}\cup{\mathcal P})$ are valid configurations. We have that $\mathrel{\mathcal{R}}_0 \cup \mathrel{\mathcal{R}}_1 \cup \mathrel{\mathcal{R}}_1^{-1}$ is symmetric and satisfies the three conditions of Definition 1. Hence ${\mathrel{\mathcal{R}}_0 \cup \mathrel{\mathcal{R}}_1 \cup \mathrel{\mathcal{R}}_1^{-1}} \subseteq {\approx}$. This property implies the desired equivalence. ◻

*Proof of Proposition 11.* We have $B, E, \{P \mid Q\} \cup {\mathcal P}\;\rightarrow\; B, E, \{P, Q\} \cup {\mathcal P}$ by $\mbox{\sc (Red Par)}$, so by Lemma 2, $B, E, \{P, Q\} \cup {\mathcal P}$ is also a valid configuration. We define the relations $\mathrel{\mathcal{R}}_0$ and $\mathrel{\mathcal{R}}_1$ by $$\begin{aligned} \mathcal{C}&\mathrel{\mathcal{R}}_0 \mathcal{C}\\ (B, E, \{P \mid Q\} \cup {\mathcal P}) &\mathrel{\mathcal{R}}_1 (B, E, \{P, Q\} \cup {\mathcal P}) \end{aligned}$$ for any $\mathcal{C}$, $B$, $E$, $P$, $Q$, ${\mathcal P}$ such that $\mathcal{C}$, $(B, E, \{P \mid Q\} \cup {\mathcal P})$, and $(B, E, \{P, Q\} \cup {\mathcal P})$ are valid configurations. We have that $\mathrel{\mathcal{R}}_0 \cup \mathrel{\mathcal{R}}_1 \cup \mathrel{\mathcal{R}}_1^{-1}$ is symmetric and satisfies the three conditions of Definition 1. Hence ${\mathrel{\mathcal{R}}_0 \cup \mathrel{\mathcal{R}}_1 \cup \mathrel{\mathcal{R}}_1^{-1}} \subseteq {\approx}$. This property implies the desired equivalence. ◻

# Proofs for Section 3.5.1 (replicated barriers)

*Proof sketch of Proposition 14.* Since barriers are forbidden under replication, the process $Q$ does not contain any barrier. We have $\mathsf{annotate}(C[!Q]) = C_1[!Q]$ and $\mathsf{annotate}(C[!^n Q]) = C_1[!^n Q]$, for some $C_1[\_]$ obtained by annotating the barriers in $C[\_]$. By induction on $C_1[\_]$, we have $\mathsf{bar\text{-}elim}(C_1[!Q]) = C_2[!Q]$ and $\mathsf{bar\text{-}elim}(C_1[!^n Q]) = C_2[!^n Q]$ for some $C_2[\_]$. Let $B = \mathsf{barriers}(C_1[!Q]) = \mathsf{barriers}(C_1[!^n Q])$ and $\{\tilde a\} = \mathsf{channels}(B)$. So $\mathsf{compiler}(C[!Q]) = \mathsf{elim\text{-}and\text{-}swap}(C_1[!Q]) = \{ C_3[!Q] \mid C_3[\_]= \nu\,\tilde a.(C_2[\_]\mid R), R \in \mathsf{swapper}(B) \}$ and $\mathsf{compiler}(C[!^n Q]) = \mathsf{elim\text{-}and\text{-}swap}(C_1[!^n Q]) = \{ C_3[!^n Q] \mid C_3[\_]= \nu\,\tilde a.(C_2[\_]\mid R), R \in \mathsf{swapper}(B) \}$. Let $C_4[\_]= \nu\,\tilde n.(\_ \mid Q')$ be an adversarial context. We have $C_4[\mathcal{C}_{\textnormal{init}}(C_3[!^n Q])] = \emptyset, \{\tilde n\}, \{C_3[!^n Q], Q'\}$ and similarly $C_4[\mathcal{C}_{\textnormal{init}}(C_3[!Q])] = \emptyset, \{\tilde n\}, \{C_3[!Q], Q'\}$. Moreover, for any context $C_3[\_]$, all traces of $\emptyset, \{\tilde n\}, \{C_3[!^n Q], Q'\}$ are matched by traces of $\emptyset, \{\tilde n\}, \{C_3[!Q], Q'\}$, by expanding the replication $!Q$ $n$ times when it appears at the root of a process in a semantic configuration. Therefore, if $\emptyset, \{\tilde n\}, \{C_3[!^n Q], Q'\} \rightarrow^* \uparrow$, then $\emptyset, \{\tilde n\}, \{C_3[! Q], Q'\} \rightarrow^* \uparrow$. Hence, if $C_3[!Q]$ satisfies diff-equivalence, then $C_3[!^n Q]$ satisfies diff-equivalence. So we conclude that, if some process in $\mathsf{compiler}(C[!Q])$ satisfies diff-equivalence, then some process in $\mathsf{compiler}(C[!^n Q])$ satisfies diff-equivalence. ◻

*Proof sketch of Proposition 15.* Let $P = C[Q]$ and $P' = C[t\textnormal{::}\,Q]$. Since annotation proceeds from top to bottom, we annotate the barriers in $C[\_]$ first, transforming $P = C[Q]$ into $C_1[Q_1]$ and $P' = C[t\textnormal{::}\,Q]$ into $C_1[t\textnormal{::}\,Q_1]$. Then we annotate $t\textnormal{::}\,Q_1$, transforming $P'$ into $C_1[t[a,c,\varsigma]\textnormal{::}\,Q'_1]$ where $Q_1 = Q_1'\varsigma$. Then we annotate the barriers in $Q_1$, respectively $Q'_1$. If $\mathsf{split}({U}, {Q}) = (Q', \varsigma')$ and $(\mathsf{fv}(\mathsf{range}(\varsigma)) \cup \mathsf{fn}(\mathsf{range}(\varsigma)) \cup \mathsf{dom}(\varsigma)) \cap U = \emptyset$, then $\mathsf{split}({U}, {Q\varsigma}) = (Q', \varsigma'\varsigma)$, by induction on $Q$. Let $Q'_1 = C'[t'\textnormal{::}\,Q_2]$. Then $Q_1 = C'\varsigma[t'\textnormal{::}\,Q_2\varsigma]$, after renaming the bound names and variables of $C'[\_]$ so that they do not occur in $\varsigma$, and we have $\mathsf{split}({\emptyset}, {Q_2}) = (Q_3, \varsigma')$, so $\mathsf{split}({\emptyset}, {Q_2\varsigma}) = (Q_3, \varsigma'\varsigma)$. Therefore, by annotating $t'\textnormal{::}\,Q_2$, $Q'_1$ becomes $Q_4' = C'[t'[a',c',\varsigma']\textnormal{::}\,Q_3]$ and $Q_1$ becomes $C'\varsigma[t'[a',c',\varsigma'\varsigma]\textnormal{::}\,Q_3] = Q_4'\varsigma$ since $\mathsf{fv}(Q_3) \subseteq \mathsf{dom}(\varsigma')$. Hence, the property that $P'$ is transformed into $C_1[t[a,c,\varsigma]\textnormal{::}\,Q_1']$ and $P$ is transformed into $C_1[Q'_1\varsigma]$ for some $C_1[\_]$, $\varsigma$, $Q_1'$, and fresh names $a$, $c$ is preserved by annotation of $Q'_1$, respectively $Q_1'\varsigma$. Therefore, $$\begin{aligned} &P'_1 =\mathsf{annotate}(P') = C_1[t[a,c,\varsigma]\textnormal{::}\,Q_1']\\ &P_1 =\mathsf{annotate}(P) = C_1[Q'_1\varsigma] \end{aligned}$$ for some $C_1[\_]$, $\varsigma$, $Q_1'$, and fresh names $a$, $c$ that do not occur in $C_1[\_]$, $\varsigma$, and $Q_1'$. Let us define $$\begin{aligned} \mathsf{add\text{-}in\text{-}let}({Q},{a,c,\varsigma}) &= c(z).\textnormal{let } z_1=\pi_{1,n}(z) \textnormal{ in }\cdots \textnormal{let } z_n=\pi_{n,n}(z) \textnormal{ in }Q\\ \mathsf{add\text{-}out\text{-}in\text{-}let}({Q},{a,c,\varsigma}) &= \overline{a}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1, \dots, M_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.\mathsf{add\text{-}in\text{-}let}({Q},{a,c,\varsigma}) \end{aligned}$$ where $\varsigma = (\textnormal{\raisebox{2pt}{\footnotesize $M_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_1$}}, \dots, \textnormal{\raisebox{2pt}{\footnotesize $M_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_n$}})$ and $z$ is a fresh variable. We have $$\begin{aligned} \mathsf{bar\text{-}elim}(C_1[t[a,c,\varsigma]\textnormal{::}\,Q_1']) &= C_2[\mathsf{add\text{-}out\text{-}in\text{-}let}({\mathsf{bar\text{-}elim}(Q_1')},{a,c,\varsigma})]\\ \mathsf{bar\text{-}elim}(C_1[Q_1'\varsigma]) &= C_2[\mathsf{bar\text{-}elim}(Q_1'\varsigma)] \end{aligned}$$ for some $C_2[\_]$ such that $a$ and $c$ do not occur in $C_2[\_]$, by induction on $C_1[\_]$. Furthermore, $C_1[\_]$ and $C_2[\_]$ do not contain replications above the hole, since barriers never occur under replication. So $$\begin{aligned} &\mathsf{bar\text{-}elim}(P_1') = C_2[\mathsf{add\text{-}out\text{-}in\text{-}let}({\mathsf{bar\text{-}elim}(Q_1')},{a,c,\varsigma})]\\ &\mathsf{bar\text{-}elim}(P_1) = C_2[\mathsf{bar\text{-}elim}(Q_1'\varsigma)] = C_2[\mathsf{bar\text{-}elim}(Q_1')\varsigma] \end{aligned}$$ by Lemma 8. Moreover, $$\mathsf{barriers}(P_1') = \{ t[a,c,\mathsf{ordom}(\varsigma)]\textnormal{::}\,Q'_1 \} \cup \mathsf{barriers}(P_1)\,.$$ So, considering permutations $f$ that leave $j$ unchanged when the $j$-th barrier is $t[a,c,\allowbreak \mathsf{ordom}(\varsigma)]\textnormal{::}\,Q'_1$, we have that $$\begin{aligned} \mathsf{swapper}(\mathsf{barriers}(P_1')) &\supseteq \{ C_{3,i}[a(x).C_{4,i}[\overline{c}\langle x\rangle.Q_{2,i}]] \mid i = 1, \dots, n \}\\ \mathsf{swapper}(\mathsf{barriers}(P_1)) &= \{ C_{3,i}[C_{4,i}[Q_{2,i}]] \mid i = 1, \dots, n \} \end{aligned}$$ for some families of contexts $C_{3,i}[\_]$ and $C_{4,i}[\_]$ and processes $Q_{2,i}$, such that $C_{3,i}[\_]$ and $C_{4,i}[\_]$ do not bind $x$ and do not contain replications, $x$ is not free in $C_{4,i}$ and $Q_{2,i}$, and $a$ and $c$ do not occur in $C_{3,i}[\_]$, $C_{4,i}[\_]$, and $Q_{2,i}$. We make a small abuse here: we write $\overline{c}\langle x\rangle.Q_{2,i}$ instead of $\overline{c}\langle\mathsf{diff}[x,x]\rangle.Q_{2,i}$. It is clear that the replacement of $\mathsf{diff}[x,x]$ with $x$ does not change the behaviour of the process. Let $\{\tilde a\} = \mathsf{channels}(\mathsf{barriers}(P_1))$. We have $\mathsf{channels}(\mathsf{barriers}(P'_1)) = \{\tilde a, a, c\}$. We finally obtain that $$\begin{aligned} &\mathsf{compiler}(P') = \mathsf{elim\text{-}and\text{-}swap}(P'_1) \supseteq \{P'_{2,i} \mid i = 1, \dots, n \}\\ &\mathsf{compiler}(P) = \mathsf{elim\text{-}and\text{-}swap}(P_1) = \{P_{2,i} \mid i = 1, \dots, n \} \end{aligned}$$ where $$\begin{aligned} &P'_{2,i} =\nu\,\tilde a, a, c.(C_2[\mathsf{add\text{-}out\text{-}in\text{-}let}({Q_2'},{a,c,\varsigma})] \mid C_{3,i}[a(x).C_{4,i}[\overline{c}\langle x\rangle.Q_{2,i}]])\\ &P_{2,i} =\nu\,\tilde a.(C_2[Q_2'\varsigma] \mid C_{3,i}[C_{4,i}[Q_{2,i}]]) \end{aligned}$$ for some $C_2[\_]$, $Q_2'$, $C_{3,i}[\_]$, $C_{4,i}[\_]$, $Q_{2,i}$, $\varsigma$, $\tilde a$, $a$, $c$, $x$, such that $C_2[\_]$ does not contain replications above the hole, $C_{3,i}[\_]$ and $C_{4,i}[\_]$ do not bind $x$ and do not contain replications, $x$ is not free in $C_{4,i}$ and $Q_{2,i}$, and $a$ and $c$ do not occur in $C_2[\_]$, $Q_2'$, $C_{3,i}[\_]$, $C_{4,i}[\_]$, $Q_{2,i}$, $\varsigma$, and $\tilde a$. Let $C_5[\_] = \nu\,n.(\_ \mid Q')$ be an adversarial context. We have $C_5[\mathcal{C}_{\textnormal{init}}(P'_{2,i})] = \emptyset, \{\tilde n\}, \{P'_{2,i}, Q'\}$ and similarly $C_5[\mathcal{C}_{\textnormal{init}}(P_{2,i})] = \emptyset, \{\tilde n\}, \{P_{2,i}, Q'\}$. We show that all traces of $\emptyset, \{\tilde n\}, \{P'_{2,i}, Q'\}$ are matched by traces of $\emptyset, \{\tilde n\}, \{P_{2,i}, Q'\}$. Formally, if $\emptyset, \{\tilde n\}, \{P'_{2,i}, Q'\} \rightarrow^* \mathcal{C}$, then one of the following cases occurs: 1. $\mathcal{C}= \emptyset, E', \{ \nu\,\tilde b'.(C_2[\mathsf{add\text{-}out\text{-}in\text{-}let}({Q_2'},{a,c,\varsigma})] \mid C_{3,i}[a(x).C_{4,i}[\overline{c}\langle x\rangle.Q_{2,i}]]) \} \cup {\mathcal P}$ $\emptyset, \{\tilde n\}, \{P_{2,i}, Q'\}\rightarrow^* \emptyset, E, \{\nu\,\tilde b.(C_2[Q_2'\varsigma] \mid C_{3,i}[C_{4,i}[Q_{2,i}]])\} \cup {\mathcal P}$ for some $E$, $E'$, $\tilde b$, $\tilde b'$, and ${\mathcal P}$ such that $\{a,c\} \cap (E \cup \{\tilde b\}) = \emptyset$, $E' \cup \{\tilde b'\} = E \cup \{\tilde b, a, c\}$, and $a$ and $c$ do not occur in ${\mathcal P}$. 2. $\mathcal{C}= \emptyset, E \cup \{a, c\}, \{ C_2[\mathsf{add\text{-}out\text{-}in\text{-}let}({Q_2'},{a,c,\varsigma})], C_3[a(x).C_4[\overline{c}\langle x\rangle.Q_2]]) \} \cup {\mathcal P}$ $\emptyset, \{\tilde n\}, \{P_{2,i}, Q'\}\rightarrow^* \emptyset, E, \{ C_2[Q_2'\varsigma], C_3[C_4[Q_2]] \} \cup {\mathcal P}$ for some $E$, $C_2[\_]$, $Q_2'$, $C_3[\_]$, $C_4[\_]$, $Q_2$, $\varsigma$, ${\mathcal P}$ such that $C_2[\_]$ does not contain replications above the hole, $C_3[\_]$ and $C_4[\_]$ do not bind $x$ and do not contain replications, $x$ is not free in $C_4[\_]$ and $Q_2$, and $a$ and $c$ do not occur in $C_2[\_]$, $Q_2'$, $C_3[\_]$, $C_4[\_]$, $Q_2$, ${\mathcal P}$, $\varsigma$, and $E$. ($C_2[\_]$, $\varsigma$, and $Q_2$ may be different from the initial ones.) 3. $\mathcal{C}= \emptyset, E \cup \{a, c\}, \{ \mathsf{add\text{-}in\text{-}let}({Q_2'},{a,c,\varsigma}), C_4[\overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1, \dots, M_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle.Q_2] \} \cup {\mathcal P}$ $\emptyset, \{\tilde n\}, \{P_{2,i}, Q'\}\rightarrow^* \emptyset, E, \{ Q_2'\varsigma, C_4[Q_2] \} \cup {\mathcal P}$ for some $E$, $Q_2'$, $C_4[\_]$, $Q_2$, $\varsigma$, $M_1$, …, $M_n$, ${\mathcal P}$ such that $\varsigma = ( \textnormal{\raisebox{2pt}{\footnotesize $M_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_1$}}, \dots, \textnormal{\raisebox{2pt}{\footnotesize $M_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_n$}} )$, $C_4[\_]$ does not contain replications, and $a$ and $c$ do not occur in $Q_2'$, $C_4[\_]$, $Q_2$, ${\mathcal P}$, $\varsigma$, and $E$. ($\varsigma$ and $Q_2$ may be different from the initial ones.) 4. $\mathcal{C}= \emptyset, E \cup \{a, c\}, \{ Q_4 \} \cup {\mathcal P}$ and $\emptyset, \{\tilde n\}, \{P_{2,i}, Q'\}\rightarrow^* \emptyset, E, \{Q_3\} \cup {\mathcal P}$ for some $E$, $Q_3$, $Q_4$, and ${\mathcal P}$ such that $Q_4 \in \textrm{add-lets}(Q_3)$. This property is proved by induction on the length of the trace $\emptyset, \{\tilde n\}, \{P'_{2,i}, Q'\} \rightarrow^* \mathcal{C}$. By inspecting all cases, we conclude that, if $\emptyset, \allowbreak \{\tilde n\}, \allowbreak \{P'_{2,i}, Q'\} \rightarrow^* \uparrow$, then $\emptyset, \{\tilde n\}, \{P_{2,i}, Q'\} \rightarrow^* \uparrow$. Hence, if $P_{2,i}$ satisfies diff-equivalence, then $P'_{2,i}$ also satisfies diff-equivalence. So, if some process in $\mathsf{compiler}(P)$ satisfies diff-equivalence, then some process in $\mathsf{compiler}(P')$ satisfies diff-equivalence. ◻

# References

n.d.

Abadi, Martín. 2000. “Security Protocols and their Properties.” In *Foundations of Secure Computation*, 39–60. NATO Science Series. IOS Press.

Abadi, Martín, and Véronique Cortier. 2006. “Deciding Knowledge in Security Protocols Under Equational Theories.” *Theoretical Computer Science* 367 (1–2): 2–32.

Abadi, Martı́n, and Bruno Blanchet. 2005. “Computer-Assisted Verification of a Protocol for Certified Email.” *Science of Computer Programming* 58 (1–2): 3–27.

Abadi, Martı́n, and Cédric Fournet. 2001. “Mobile Values, New Names, and Secure Communication.” In *POPL’01: 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, 104–15. ACM Press.

Abadi, Martı́n, and Andrew D. Gordon. 1997. “A Calculus for Cryptographic Protocols: The Spi Calculus.” In *CCS’97: 4th ACM Conference on Computer and Communications Security*, 36–47. ACM Press.

———. 1998. “A Bisimulation Method for Cryptographic Protocols.” *Nordic Journal of Computing* 5 (4): 267–303.

Adida, Ben, Olivier de Marneffe, Olivier Pereira, and Jean-Jacques Quisquater. 2009. “Electing a University President Using Open-Audit Voting: Analysis of Real-World Use of Helios.” In *EVT/WOTE’09: Electronic Voting Technology Workshop/Workshop on Trustworthy Elections*. USENIX Association.

Arapinis, Myrto, Jia Liu, Eike Ritter, and Mark Ryan. 2014. “Stateful Applied Pi Calculus.” In *POST’14: 3rd Conference on Principles of Security and Trust*, 8414:22–41. LNCS. Springer.

Arenstorf, Norbert S., and Harry F. Jordan. 1989. “Comparing barrier algorithms.” *International Journal of Parallel Computing* 12 (2): 157–70.

Backes, Michael, Cătălin Hriţcu, and Matteo Maffei. 2008. “Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-calculus.” In *CSF’08: 21st IEEE Computer Security Foundations Symposium*, 195–209. IEEE Computer Society.

Basin, David, Jannik Dreier, and Ralf Casse. 2015. “Automated Symbolic Proofs of Observational Equivalence.” In *CCS’15: 22nd ACM Conference on Computer and Communications Security*, 1144–55. ACM.

Baudet, Mathieu. 2005. “Deciding Security of Protocols Against Off-Line Guessing Attacks.” In *CCS’05: 12th ACM Conference on Computer and Communications Security*, 16–25. ACM Press.

———. 2007. “Sécurité Des Protocoles Cryptographiques : Aspects Logiques Et Calculatoires.” PhD thesis, Laboratoire Spécification et Vérification, ENS Cachan, France.

Blanchet, Bruno. 2004. “Automatic Proof of Strong Secrecy for Security Protocols.” In *S&p’04: 25th IEEE Symposium on Security and Privacy*, 86–100. IEEE Computer Society.

———. 2008. “Vérification Automatique de Protocoles Cryptographiques: Modèle Formel Et Modèle Calculatoire.” M\\emoire d'habilitation \\a diriger des recherches, Université Paris-Dauphine.

———. 2009. “Automatic Verification of Correspondences for Security Protocols.” *Journal of Computer Security* 17 (4): 363–434.

———. 2016. “Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif.” *Foundations and Trends in Privacy and Security* 1 (1–2): 1–135.

Blanchet, Bruno, Martı́n Abadi, and Cédric Fournet. 2008. “Automated verification of selected equivalences for security protocols.” *Journal of Logic and Algebraic Programming* 75 (1): 3–51.

Blanchet, Bruno, and Ben Smyth. 2016. “Automated Reasoning for Equivalences in the Applied Pi Calculus with Barriers.” In *CSF’16: 29th Computer Security Foundations Symposium*, 310–24. IEEE Computer Society.

Blanchet, Bruno, Ben Smyth, and Vincent Cheval. 2016. “ProVerif 1.96: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial.” .

Borgström, Johannes, Sébastien Briais, and Uwe Nestmann. 2004. “Symbolic Bisimulation in the Spi Calculus.” In *CONCUR’04: 15th International Conference on Concurrency Theory*, 3170:161–76. LNCS. Springer.

Borgström, Johannes, and Uwe Nestmann. 2005. “On bisimulations for the spi calculus.” *Mathematical Structures in Computer Science* 15 (3): 487–552.

Brooks, Eugene D., III. 1986. “The Butterfly Barrier.” *International Journal of Parallel Programming* 15 (4): 295–307.

Chadha, Rohit, Stefan Ciobâca, and Steve Kremer. 2012. “Automated Verification of Equivalence Properties of Cryptographic Protocols.” In *ESOP’12: 21st European Symposium on Programming*, 7211:108–27. LNCS. Springer.

Cheval, Vincent, and Bruno Blanchet. 2013. “Proving More Observational Equivalences with ProVerif.” In *POST’13: 2nd Conference on Principles of Security and Trust*, 7796:226–46. LNCS. Springer.

Cheval, Vincent, Hubert Comon-Lundh, and Stéphanie Delaune. 2011. “Trace Equivalence Decision: Negative Tests and Non-Determinism.” In *CCS’11: Proceedings of the 18th ACM Conference on Computer and Communications Security*, 321–30. ACM Press.

Chothia, Tom. 2006. “Analysing the MUTE Anonymous File-Sharing System Using the Pi-Calculus.” In *FORTE’06: 26th International Conference on Formal Techniques for Networked and Distributed Systems*, 4229:115–30. LNCS. Springer.

Chothia, Tom, Simona Orzan, Jun Pang, and Muhammad Torabi Dashti. 2007. “A Framework for Automatically Checking Anonymity with $\mu$CRL.” In *TGC’06: 2nd Symposium on Trustworthy Global Computing*, 4661:301–18. LNCS. Springer.

Chrétien, Rémy, Véronique Cortier, and Stéphanie Delaune. 2015a. “Decidability of Trace Equivalence for Protocols with Nonces.” In *CSF’15: Proceedings of the 28th IEEE Computer Security Foundations Symposium*, 170–84. IEEE Computer Society.

———. 2015b. “From Security Protocols to Pushdown Automata.” *ACM Transactions on Computational Logic* 17 (1:3).

Ciobâca, Stefan. 2011. “Verification and Composition of Security Protocols with Applications to Electronic Voting.” PhD thesis, Laboratoire Spécification et Vérification, ENS Cachan & CNRS & INRIA.

Cortier, Véronique, and Stéphanie Delaune. 2009. “A method for proving observational equivalence.” In *CSF’09: 22nd IEEE Computer Security Foundations Symposium*, 266–76. IEEE Computer Society.

Cortier, Véronique, Michaël Rusinowitch, and Eugen Zǎlinescu. 2007. “Relating Two Standard Notions of Secrecy.” *Logical Methods in Computer Science* 3 (3).

Cortier, Véronique, and Ben Smyth. 2013. “Attacking and fixing Helios: An analysis of ballot secrecy.” *Journal of Computer Security* 21 (1): 89–148.

Cremers, Cas, and Lucca Hirschi. 2017. “Improving Automated Symbolic Analysis for E-voting Protocols: A Method Based on Sufficient Conditions for Ballot Secrecy.” arXiv, Report 1709.00194.

Dahl, Morten, Stéphanie Delaune, and Graham Steel. 2010. “Formal Analysis of Privacy for Vehicular Mix-Zones.” In *ESORICS’10: 15th European Symposium on Research in Computer Security*, 6345:55–70. LNCS. Springer.

———. 2011. “Formal Analysis of Privacy for Anonymous Location Based Services.” In *TOSCA’11: Proceedings of the Workshop on Theory of Security and Applications*, 6993:98–112. LNCS. Springer.

Delaune, Stéphanie, Steve Kremer, and Olivier Pereira. 2009. “Simulation based security in the applied pi calculus.” In *FSTTCS: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science*, 4:169–80. Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik.

Delaune, Stéphanie, Steve Kremer, and Mark D. Ryan. 2009. “Verifying privacy-type properties of electronic voting protocols.” *Journal of Computer Security* 17 (4): 435–87.

———. 2010. “Symbolic Bisimulation for the Applied Pi Calculus.” *Journal of Computer Security* 18 (2): 317–77.

Delaune, Stéphanie, Mark D. Ryan, and Ben Smyth. 2008. “Automatic Verification of Privacy Properties in the Applied Pi-Calculus.” In *IFIPTM’08: 2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security*, 263:263–78. International Federation for Information Processing. Springer.

Dreier, Jannik, Charles Duménil, Steve Kremer, and Ralf Sasse. 2017. “Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols.” In *6th International Conference on Principles of Security and Trust (POST)*, edited by Matteo Maffei and Mark Ryan, 10204:117–40. LNCS. Uppsala, Sweden: Springer.

Dreier, Jannik, Pascal Lafourcade, and Yassine Lakhnech. 2011. “Vote-Independence: A Powerful Privacy Notion for Voting Protocols.” In *FPS’11: 4th Workshop on Foundations & Practice of Security*, 6888:164–80. LNCS. Springer.

Durante, Luca, Riccardo Sisto, and Adriano Valenzano. 2003. “Automatic Testing Equivalence Verification of Spi Calculus Specifications.” *ACM Transactions on Software Engineering and Methodology* 12 (2): 222–84.

Freudiger, Julien, Maxim Raya, Márk Félegyházi, Panos Papadimitratos, and Jean-Pierre Hubaux. 2007. “Mix-Zones for Location Privacy in Vehicular Networks.” In *WiN-ITS’07: 1st International Workshop on Wireless Networking for Intelligent Transportation Systems*.

Hensgen, Debra, Raphael Finkel, and Udi Manber. 1988. “Two Algorithms for Barrier Synchronization.” *International Journal of Parallel Programming* 17 (1): 1–17.

Hirschi, Lucca, David Baelde, and Stéphanie Delaune. 2016. “A Method for Verifying Privacy-Type Properties: The Unbounded Case.” In *Proceedings of the 37th IEEE Symposium on Security and Privacy (S&P’16)*, 564–81. IEEE Computer Society.

Hüttel, Hans. 2003. “Deciding Framed Bisimilarity.” *Electronic Notes in Theoretical Computer Science* 68 (6): 1–20.

Juels, Ari, Dario Catalano, and Markus Jakobsson. 2010. “Coercion-Resistant Electronic Elections.” In *Towards Trustworthy Elections: New Directions in Electronic Voting*, 6000:37–63. LNCS. Springer.

Klus, Petr, Ben Smyth, and Mark D. Ryan. 2010. “ProSwapper: Improved equivalence verifier for ProVerif.” .

Kremer, Steve, and Mark D. Ryan. 2005. “Analysis of an Electronic Voting Protocol in the Applied Pi Calculus.” In *ESOP’05: 14th European Symposium on Programming*, 3444:186–200. LNCS. Springer.

Lee, Byoungcheon, Colin Boyd, Ed Dawson, Kwangjo Kim, Jeongmo Yang, and Seungjae Yoo. 2004. “Providing Receipt-Freeness in Mixnet-Based Voting Protocols.” In *ICISC’03: 6th International Conference on Information Security and Cryptology*, 2971:245–58. LNCS. Springer.

Lubachevsky, Boris D. 1990. “Synchronization Barrier and Related Tools for Shared Memory Parallel Programming.” *International Journal of Parallel Programming* 19 (3): 225–50.

Pfitzmann, Andreas, and Marit Köhntopp. 2001. “Anonymity, Unobservability, and Pseudonymity – A Proposal for Terminology.” In *International Workshop on Design Issues in Anonymity and Unobservability*, 2009:1–9. LNCS. Springer.

Reiter, Michael K., and Aviel D. Rubin. 1998. “Crowds: Anonymity for Web Transactions.” *ACM Transactions on Information and System Security* 1 (1): 66–92.

Ryan, Mark D., and Ben Smyth. 2011. “Applied pi calculus.” In *Formal Models and Techniques for Analyzing Security Protocols*. IOS Press.

Santiago, Sonia, Santiago Escobar, Catherine Meadows, and José Meseguer. 2014. “A Formal Definition of Protocol Indistinguishability and Its Verification Using Maude-NPA.” In *STM’14: Security and Trust Management*, 8743:162–77. LNCS. Springer.

Smyth, Ben. 2007. “Automatic Verification of Privacy Properties in the Applied Pi Calculus.” In *Formal Protocol Verification Applied: Abstracts Collection*. Dagstuhl Seminar Proceedings 07421.

———. 2011. “Formal verification of cryptographic protocols with automated reasoning.” PhD thesis, School of Computer Science, University of Birmingham.

Tiu, Alwen, and Jeremy Dawson. 2010. “Automating Open Bisimulation Checking for the Spi Calculus.” In *CSF’10: 23rd IEEE Computer Security Foundations Symposium*, 307–21. IEEE Computer Society.

[^1]: Corresponding author. [^2]: Corresponding author. [^3]: Only a few rules of the operational semantics need to be adapted to equations, as in (Blanchet 2016, sec. 2.5.1); the definition of our compiler and many parts of the proofs remain unchanged. A tricky point is that, with equations, the evaluation of expressions may introduce names that do not appear in the initial expression, and these names may collide with other names. There are several ways to solve this technical issue, either by considering a representative in which these names are renamed to avoid such collisions or by restricting ourselves to the equational theories that ProVerif supports, in which the equations can be oriented to avoid such introduction of names. Adapting the proofs to equations is otherwise straightforward. [^4]: The use of distinct channels helps avoid an incompleteness issue of ProVerif. In essence, ProVerif overapproximates a private channel as a set of messages: an input on a private channel $a$ may receive any message sent on $a$ at any point, in any order. By using distinct channels for barriers, we make sure that there is a single output and a single input for each private channel, so we reduce the effect of this overapproximation to a minimum.