would require a deep rethinking, especially for the definition of narrowing. Hence we plan to
use the alternative notion of delegation proposed in [81] for a session calculus without channels,
called “internal delegation”. Note that delegation remains essentially a synchronous mechanism,
even in the asynchronous setting: indeed, unlike ordinary outputs that become non-blocking, del-
egation remains blocking for the principal, who has to wait until the deputy returns the delegation
to be able to proceed. As a matter of fact, this is quite reasonable: not only does it prevent the is-
sue of “power vacancy” that would arise if the role of the principal disappeared from the network
for some time, but it also seems natural to assume that the principal delegates a task only when it
has the guarantee that the deputy will accept it.

**Acknowledgments** We are indebted to Francesco Dagnino for suggesting a simplification in the definition of balancing for asynchronous types. We also wish to thank the anonymous referees for their helpful comments. In particular, they helped us to clarify several definitions, and to expand both the comparison with the literature and the discussion on future work.

References

[1] Takeuchi K, Honda K, Kubo M. An interaction-based language and its typing system. In: Hankin C (ed.), PARLE, volume 817 of LNCS. Springer, 1994 pp. 122–138. doi:10.1007/BFb0053567.

[2] Honda K, Vasconcelos VT, Kubo M. Language primitives and type discipline for structured communication-based programming. In: Hankin C (ed.), ESOP, volume 1381 of LNCS. Springer, 1998 pp. 122–138. doi:10.1007/BFb0053567.

[3] Honda K, Yoshida N, Carbone M. Multiparty asynchronous session types. In: Necula GC, Wadler P (eds.), POPL. ACM Press, 2008 pp. 273–284. doi:10.1145/1328897.1328472.

[4] Honda K, Yoshida N, Carbone M. Multiparty asynchronous session types. Journal of ACM, 2016. 63(1):9:1–9:67. doi:10.1145/2827695.

[5] Ancona D, Bono V, Bravetti M, Campos J, Castagna G, Deniélou P, Gay SJ, Gesbert N, Giachino E, Hu R, Johnsen EB, Martins F, Mascardi V, Montesi F, Neykova R, Ng N, Padovani L, Vasconcelos VT, Yoshida N. Behavioral types in programming languages. *Foundations and Trends in Programming Languages*, 2016. 3(2-3):95–230. doi:10.1561/2500000031.

[6] Deniélou P, Yoshida N. Multiparty session types meet communicating automata. In: Seidl H (ed.), ESOP, volume 7211 of LNCS. Springer, 2012 pp. 194–213. doi:10.1007/978-3-642-28869-2\_10.

[7] Lange J, Tuosto E, Yoshida N. From communicating machines to graphical choreographies. In: Rajamani SK, Walker D (eds.), POPL. ACM Press, 2015 pp. 221–232. doi:10.1145/2676726.2676964.

[8] Tuosto E, Guanciale R. Semantics of global view of choreographies. *Journal of Logic and Algebraic Methods in Programming*, 2018. 95:17–40. doi:10.1016/j.jlamp.2017.11.002.

[9] Caires L, Pfenning F. Session types as intuitionistic linear propositions. In: Gastin P, Laroussinie F (eds.), CONCUR, volume 6269 of LNCS. Springer, 2010 pp. 222–236. doi: 10.1007/978-3-642-15375-4\_16.
[10] Toninho B, Caires L, Pfenning F. Dependent session types via intuitionistic linear type theory. In: Schneider-Kamp P, Hanus M (eds.), PPDP. ACM Press, 2011 pp. 161–172. doi:10.1145/2003476.2003499.

[11] Wadler P. Propositions as sessions. *Journal of Functional Programming*, 2014. **24**(2-3):384–418. doi:10.1017/S095679681400001X.

[12] Pérez JA, Caires L, Pfenning F, Toninho B. Linear logical relations and observational equivalences for session-based concurrency. *Information and Computation*, 2014. **239**:254–302. doi:10.1016/j.ic.2014.08.001.

[13] Caires L, Pfenning F, Toninho B. Linear logic propositions as session types. *Mathematical Structures in Computer Science*, 2016. **26**(3):367–423. doi:10.1017/S0960129514000218.

[14] Castellani I, Dezani-Ciancaglini M, Giannini P. Event structure semantics for multiparty sessions. *Journal of Logic and Algebraic Methods in Programming*, 2023. **131**:100844. doi:10.1016/j.jlamp.2022.100844.

[15] Winskel G. An introduction to event structures. In: de Bakker JW, de Roever WP, Rozenberg G (eds.), REX: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of LNCS. Springer, 1988 pp. 364–397. doi:10.1007/BFb0013026.

[16] Dezani-Ciancaglini M, Ghilezan S, Jaksic S, Pantovic J, Yoshida N. Precise subtyping for synchronous multiparty sessions. In: Gay S, Alglave J (eds.), PLACES, volume 203 of EPTCS. Open Publishing Association, 2015 pp. 29–44. doi:10.4204/EPTCS.203.3.

[17] Boudol G, Castellani I. Permutation of transitions: an event structure semantics for CCS and SCCS. In: de Bakker JW, de Roever WP, Rozenberg G (eds.), REX: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of LNCS. Springer, 1988 pp. 411–427. doi:10.1007/BFb0013028.

[18] Boudol G, Castellani I. Flow models of distributed computations: three equivalent semantics for CCS. *Information and Computation*, 1994. **114**(2):247–314. doi:10.1006/inco.1994.1088.

[19] Winskel G. Events in computation. Ph.D. thesis, University of Edinburgh, 1980.

[20] Nielsen M, Plotkin G, Winskel G. Petri nets, event structures and domains, part I. *Theoretical Computer Science*, 1981. **13**(1):85–108. doi:10.1016/0304-3975(81)90112-2.

[21] Mostrous D, Yoshida N, Honda K. Global principal typing in partially commutative asynchronous sessions. In: Castagna G (ed.), ESOP, volume 5502 of LNCS. Springer, 2009 pp. 316–332. doi:10.1007/978-3-642-00590-9_23.

[22] Bravetti M, Carbone M, Zavattaro G. Undecidability of asynchronous session subtyping. *Information and Computation*, 2017. **256**:300–320. doi:10.1016/j.ic.2017.07.010.

[23] Lange J, Yoshida N. On the undecidability of asynchronous session subtyping. In: Esparza J, Murawski AS (eds.), FOSSACS, volume 10203 of LNCS. 2017 pp. 441–457. doi:10.1007/978-3-662-54458-7_26.

[24] Courcelle B. Fundamental properties of infinite trees. *Theoretical Computer Science*, 1983. **25**:95–169. doi:10.1016/0304-3975(83)90059-2.

[25] Scalas A, Yoshida N. Less is more: multiparty session types revisited. *Proceedings of the ACM on Programming Languages*, 2019. 3(POPL):30:1–30:29. doi:10.1145/3290343.

[26] Dagnino F, Giannini P, Dezani-Ciancaglini M. Deconfined Global Types for Asynchronous Sessions. In: Damiani F, Dardha O (eds.), COORDINATION, volume 12717 of LNCS. Springer, 2021 pp. 41–60. doi:10.1007/978-3-030-78142-2_3.
[27] Pierce BC. Types and Programming Languages. MIT Press, 2002. ISBN 978-0-262-16209-8.

[28] Deniélou PM, Yoshida N. Dynamic multirole session types. In: Thomas Ball MS (ed.), POPL. ACM Press, 2011 pp. 435–446. doi:10.1145/1926385.1926435.

[29] Coppo M, Dezani-Ciancaglini M, Yoshida N, Padovani L. Global progress for dynamically interleaved multiparty sessions. *Mathematical Structures in Computer Science*, 2016. 26(2):238–302. doi:10.1017/S0960129514000188.

[30] Gay S, Hole M. Subtyping for session types in the pi calculus. *Acta Informatica*, 2005. 42(2/3):191–225. doi:10.1007/s00236-005-0177-z.

[31] Demangeon R, Honda K. Full abstraction in a subtyped pi-calculus with linear types. In: Katoen J, König B (eds.), CONCUR, volume 6901 of LNCS. Springer, 2011 pp. 280–296. doi:10.1007/978-3-642-23217-6\_19.

[32] Gay S. Subtyping supports safe session substitution. In: Lindley S, McBride C, Trinder PW, Sannella D (eds.), A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, volume 9600 of LNCS. Springer, 2016 pp. 95–108. doi:10.1007/978-3-319-30936-1\_5.

[33] Barbanera F, Dezani-Ciancaglini M, Lanese I, Tuosto E. Composition and decomposition of multiparty sessions. *Journal of Logic and Algebraic Methods Program.*, 2021. 119:100620. doi:10.1016/j.jlamp.2020.100620.

[34] Hüttel H, Lanese I, Vasconcelos VT, Caires L, Carbone M, Deniélou PM, Mostrous D, Padovani L, Ravara A, Tuosto E, Vieira HT, Zavattaro G. Foundations of session types and behavioural contracts. *ACM Computing Surveys*, 2016. 49(1):3:1–3:36. doi:10.1145/2873052.

[35] Boudol G, Castellani I. Flow models of distributed computations: event structures and nets. Research Report 1482, INRIA, 1991. URL https://inria.hal.science/inria-00075080/document.

[36] Castellani I, Dezani-Ciancaglini M, Giannini P. Event Structure Semantics for Multiparty Sessions. In: Boreale M, Corradini F, Loreti M, Pugliese R (eds.), Models, Languages, and Tools for Concurrent and Distributed Programming - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday, volume 11665 of LNCS. Springer, 2019 pp. 340–363. doi:10.1007/978-3-030-21485-2\_19.

[37] Milner R. The polyadic pi-calculus (Abstract). In: Cleaveland R (ed.), CONCUR, volume 630 of LNCS. Springer, 1992 p. 1. doi:10.1007/BFb0084778.

[38] Pierce BC, Sangiorgi D. Typing and subtyping for mobile processes. *Mathematical Structures in Computer Science*, 1996. 6(5):376–385. doi:10.1017/S096012950007002X.

[39] Kobayashi N. Type-based information flow analysis for the pi-calculus. *Acta Informatica*, 2005. 42(4-5):291–347. doi:10.1007/s00236-005-0179-x.

[40] Kobayashi N. A type system for lock-free processes. *Information and Computation*, 2002. 177(2):122–159. doi:10.1016/S0890-5401(02)93171-8.

[41] Kobayashi N. A new type system for deadlock-free processes. In: Baier C, Hermanns H (eds.), CONCUR, volume 4137 of LNCS. Springer, 2006 pp. 233–247. doi:10.1007/11817949\_16.

[42] Dardha O, Giachino E, Sangiorgi D. Session types revisited. In: Schreye DD, Janssens G, King A (eds.), PPDP. ACM, 2012 pp. 139–150. doi:10.1145/2370776.2370794.
[43] Padovani L. Type reconstruction for the linear π-calculus with composite regular types. *Logical Methods in Computer Science*, 2015. **11**(4). doi:10.2168/LMCS-11(4:13)2015.

[44] Severi P, Dezani-Ciancaglini M. Observational equivalence for multiparty sessions. *Fundamenta Informaticae*, 2019. **167**:267–305. doi:10.3233/FI-2019-1863.

[45] Bravetti M, Carbone M, Zavattaro G. On the boundary between decidability and undecidability of asynchronous session subtyping. *Theoretical Computer Science*, 2018. **722**:19–51. doi:10.1016/j.tcs.2018.02.010.

[46] Bravetti M, Carbone M, Lange J, Yoshida N, Zavattaro G. A Sound Algorithm for Asynchronous Session Subtyping and its Implementation. *Logical Methods in Computer Science*, 2021. **17**(1):20:1–20:35. doi:10.23638/LMCS-17(1:20)2021.

[47] Ghilezan S, Pantović J, Prokić I, Scalaş A, Yoshida N. Precise subtyping for asynchronous multiparty sessions. *Proceedings of the ACM on Programming Languages*, 2021. 5(POPL):1–28. doi:10.1145/3434297.

[48] Dagnino F, Giannini P, Dezani-Ciancaglini M. Deconfined Global Types for Asynchronous Sessions. *Logical Methods in Computer Science*, 2023. **19**(1). doi:10.46298/lmcs-19(1:3)2023.

[49] Winskel G. Event structure semantics for CCS and related languages. In: Nielsen M, Schmidt EM (eds.), ICALP, volume 140 of LNCS. Springer, 1982 pp. 561–576. doi:10.1007/BFb0012800.

[50] Boudol G, Castellani I. On the semantics of concurrency: partial orders and transition systems. In: Ehrig H, Kowalski RA, Levi G, Montanari U (eds.), TAPSOFT, volume 249 of LNCS. Springer, 1987 pp. 123–137. doi:10.1007/3-540-17660-8\_52.

[51] Degano P, De Nicola R, Montanari U. On the consistency of truly concurrent operational and denotational semantics. In: Chandra AK (ed.), LICS. IEEE Computer Society Press Press, 1988 pp. 133–141. doi:10.1109/LICS.1988.5112.

[52] Degano P, De Nicola R, Montanari U. A partial ordering semantics for CCS. *Theoretical Computer Science*, 1990. **75**(3):223–262. doi:10.1016/0304-3975(90)90095-Y.

[53] van Glabbeek RJ, Goltz U. Well-behaved flow event structures for parallel composition and action refinement. *Theoretical Computer Science*, 2004. **311**(1-3):463–478. doi:10.1016/j.tcs.2003.10.031.

[54] Brookes S, Hoare CA, Roscoe AW. A theory of communicating sequential processes. *Journal of ACM*, 1984. **31**(3):560–599. doi:10.1145/828.833.

[55] Olderog E. TCSP: theory of communicating sequential processes. In: Brauer W, Reisig W, Rozenberg G (eds.), Advances in Petri Nets, volume 255 of LNCS. Springer, 1986 pp. 441–465. doi:10.1007/3-540-17906-2\_34.

[56] Loogen R, Goltz U. Modelling nondeterministic concurrent processes with event structures. *Fundamenta Informaticae*, 1991. **14**(1):39–74. doi:10.3233/FI-1991-14103.

[57] Baier C, Majster-Cederbaum ME. The connection between an event structure semantics and an operational semantics for TCSP. *Acta Informatica*, 1994. **31**(1):81–104. doi:10.1007/BF01178923.

[58] Langerak R. Bundle event structures: a non-interleaving semantics for LOTOS. In: Diaz M, Groz R (eds.), FORTE, volume C-10 of IFIP Transactions. North-Holland. ISBN 0-444-89282-6, 1992 pp. 331–346.
[59] Katoen J. Quantitative and qualitative extensions of event structures. Ph.D. thesis, University of Twente, 1996.

[60] Crafa S, Varacca D, Yoshida N. Compositional event structure semantics for the internal π-Calculus. In: Caires L, Vasconcelos VT (eds.), CONCUR, volume 4703 of LNCS. Springer, 2007 pp. 317–332. doi:10.1007/978-3-540-74407-8\_22.

[61] Varacca D, Yoshida N. Typed event structures and the linear π-calculus. Theoretical Computer Science, 2010. 411(19):1949–1973. doi:10.1016/j.tcs.2010.01.024.

[62] Crafa S, Varacca D, Yoshida N. Event structure semantics of parallel extrusion in the π-calculus. In: Birkedal L (ed.), FOSSACS, volume 7213 of LNCS. Springer, 2012 pp. 225–239. doi:10.1007/978-3-642-28729-9\_15.

[63] Cristescu I. Operational and denotational semantics for the reversible π-calculus. Ph.D. thesis, University Paris Diderot - Paris 7, 2015.

[64] Cristescu I, Krivine J, Varacca D. Rigid families for CCS and the π-calculus. In: Leucker M, Rueda C, Valencia FD (eds.), ICTAC, volume 9399 of LNCS. Springer, 2015 pp. 223–240. doi:10.1007/978-3-319-25150-9\_14.

[65] Cristescu I, Krivine J, Varacca D. Rigid families for the reversible π-calculus. In: Devitt SJ, Lanese I (eds.), Reversible Computation, volume 9720 of LNCS. Springer, 2016 pp. 3–19. doi:10.1007/978-3-319-40578-0\_1.

[66] de' Liguoro U, Melgratti HC, Tuosto E. Towards refinable choreographies. In: Lange J, Mavridou A, Safina L, Scalas A (eds.), ICE, volume 324 of EPTCS. Open Publishing Association, 2020 pp. 61–77. doi:10.4204/EPTCS.324.6.

[67] Rideau S, Winskel G. Concurrent strategies. In: Grohe M (ed.), LICS. IEEE Computer Society, 2011 pp. 409–418. doi:10.1109/LICS.2011.13.

[68] Sakayori K, Tsukada T. A truly concurrent game model of the asynchronous π-calculus. In: Esparza J, Murawski AS (eds.), FOSSACS, volume 10203 of LNCS. 2017 pp. 389–406. doi:10.1007/978-3-662-54458-7\_23.

[69] Castellan S, Yoshida N. Causality in linear logic - full completeness and injectivity (unit-free multiplicative-additive fragment). In: Bojanczyk M, Simpson A (eds.), FOSSACS, volume 11425 of LNCS. Springer, 2019 pp. 150–168. doi:10.1007/978-3-030-17127-8\_9.

[70] Castellani I, Giannini P. Towards a Semantic Characterisation of Global Type Well-formedness. In: Costa D, Hu R (eds.), PLACES, volume 401 of EPTCS. Open Publishing Association, 2024 pp. 11–21. doi:10.4204/EPTCS.401.2.

[71] Tiezzi F, Yoshida N. Towards reversible sessions. In: Donaldson AF, Vasconcelos VT (eds.), PLACES, volume 155 of EPTCS. Open Publishing Association, 2014 pp. 17–24. doi:10.4204/EPTCS.155.3.

[72] Tiezzi F, Yoshida N. Reversing single sessions. In: Devitt SJ, Lanese I (eds.), RC, volume 9720 of LNCS. Springer, 2016 pp. 52–69. doi:10.1007/978-3-319-40578-0\_4.

[73] Mezzina CA, Pérez JA. Causally consistent reversible choreographies: a monitors-as-memories approach. In: Vanhoof W, Pientka B (eds.), PPDP. ACM Press, 2017 pp. 127–138. doi:10.1145/3131851.3131864.

[74] Mezzina CA, Pérez JA. Reversibility in session-based concurrency: A fresh look. Journal of Logic and Algebraic Methods in Programming, 2017. 90:2–30. doi:10.1016/j.jlamp.2017.03.003.
[75] Neykova R, Yoshida N. Let it recover: multiparty protocol-induced recovery. In: Wu P, Hack S (eds.), CC. ACM Press, 2017 pp. 98–108. doi:10.1145/3033019.

[76] Castellani I, Dezani-Ciancaglini M, Giannini P. Reversible sessions with flexible choices. *Acta Informatica*, 2019. **56**(7):553–583. doi:10.1007/s00236-019-00332-y.

[77] Phillips IC, Ulidowski I. Reversibility and asymmetric conflict in event structures. *Journal of Logical and Algebraic Methods in Programming*, 2015. **84**(6):781–805. doi:10.1016/j.jlamp.2015.07.004.

[78] Graversen E, Phillips I, Yoshida N. Towards a categorical representation of reversible event structures. In: Vasconcelos VT, Haller P (eds.), PLACES, volume 246 of *EPTCS*. Open Publishing Association, 2017 pp. 49–60. doi:10.4204/EPTCS.246.9.

[79] Graversen E, Phillips I, Yoshida N. Event structure semantics of (controlled) reversible CCS. In: Kari J, Ulidowski I (eds.), Reversible Computation, volume 11106 of *LNCS*. Springer, 2018 pp. 122–102. doi:10.1007/978-3-319-99498-7_7.

[80] Graversen E. Event structure semantics of reversible process calculi. Ph.D. thesis, Imperial College London, 2021.

[81] Castellani I, Dezani-Ciancaglini M, Giannini P, Horne R. Global types with internal delegation. *Theoretical Computer Science*, 2020. **807**:128–153. doi:10.1016/j.tcs.2019.09.027.
A. Appendix

This Appendix contains the proofs of Lemmas 3.6, 3.10, 3.11, 3.13, 3.14, 8.5, 8.14, 8.15, 8.16, 8.17, 8.18, 8.21, 8.22, 8.23 and the auxiliary Lemmas A.1, A.2 , A.3.

**Lemma 3.6** If G is bounded, then G $\uparrow$ r is a partial function for all r.

**Proof:** We redefine the projection $\downarrow_r$ as the largest relation between global types and processes such that $(G, P) \in \downarrow_r$ implies:

i) if $r \notin \text{play}(G)$, then $P = 0$;

ii) if $G = \coprod_{i \in I} \text{rq!l}_i; G_i$, then $P = \bigoplus_{i \in I} \text{q!l}_i; P_i$ and $(G_i, P_i) \in \downarrow_r$ for all $i \in I$;

iii) if $G = \text{pr!l}$; $G'$, then $(G', P) \in \downarrow_r$;

iv) if $G = \coprod_{i \in I} \text{pr!l}_i; G_i$ and $|I| > 1$, then $P = \vec{\pi}; \sum_{i \in I} \mathbf{p}?l_i; P_i$ and $(G_i, \vec{\pi}; \mathbf{p}?l_i; P_i) \in \downarrow_r$ for all $i \in I$;

v) if $G = \coprod_{i \in I} \mathbf{pq!l}_i; G_i$ and $r \notin \{\mathbf{p}, \mathbf{q}\}$ and $r \in \text{play}(G_i)$, then $(G_i, P) \in \downarrow_r$ for all $i \in I$;

vi) if $G = \text{pr}?l$; $G'$, then $P = \mathbf{p}?l$; $P'$ and $(G', P') \in \downarrow_r$;

vii) if $G = \mathbf{pq}?l$; $G'$ and $r \neq \mathbf{q}$ and $r \in \text{play}(G')$, then $(G', P) \in \downarrow_r$.

We define equality $\mathcal{E}$ of processes to be the largest symmetric binary relation $\mathcal{R}$ on processes such that $(P, Q) \in \mathcal{R}$ implies:

(a) if $P = \bigoplus_{i \in I} \mathbf{p!l}_i; P_i$, then $Q = \bigoplus_{i \in I} \mathbf{p!l}_i; Q_i$ and $(P_i, Q_i) \in \mathcal{R}$ for all $i \in I$;

(b) if $P = \sum_{i \in I} \mathbf{p}?l_i; P_i$, then $Q = \sum_{i \in I} \mathbf{p}?l_i; Q_i$ and $(P_i, Q_i) \in \mathcal{R}$ for all $i \in I$.

It is then enough to show that the relation $\mathcal{R}_r = \{(P, Q) \mid \exists G. (G, P) \in \downarrow_r \text{ and } (G, Q) \in \downarrow_r\}$ satisfies Clauses (a) and (b) (with $\mathcal{R}$ replaced by $\mathcal{R}_r$), since this will imply $\mathcal{R}_r \subseteq \mathcal{E}$. Note first that $(0, 0) \in \mathcal{R}_r$ because $(\text{End}, 0) \in \downarrow_r$, and that $(0, 0) \in \mathcal{E}$ because Clauses (a) and (b) are vacuously satisfied by the pair $(0, 0)$, which must therefore belong to $\mathcal{E}$.

The proof is by induction on $d = \text{depth}(G, r)$. We only consider Clause (b), the proof for Clause (a) being similar and simpler. So, assume $(P, Q) \in \mathcal{R}_r$ and $P = \sum_{i \in I} \mathbf{p}?l_i; P_i$.

Case $d = 1$. In this case $G = \text{pr}?l$; $G'$ and $P = \mathbf{p}?l$; $P'$ and $(G', P') \in \downarrow_r$. From $(G, Q) \in \downarrow_r$ we get $Q = \mathbf{p}?l$; $Q'$ and $(G', Q') \in \downarrow_r$. Hence $Q$ has the required form and $(P', Q') \in \mathcal{R}_r$.

Case $d > 1$. By definition of $\downarrow_r$, there are five possible subcases.

1. Case $G = \text{pr!l}$; $G'$ and $(G', P) \in \downarrow_r$. From $(G, Q) \in \downarrow_r$ we get $(G', Q) \in \downarrow_r$. Then $(P, Q) \in \mathcal{R}_r$.

2. Case $G = \coprod_{i \in I} \text{pr!l}_i; G_i$ and $(G_i, \mathbf{p}?l_i; P_i) \in \downarrow_r$ for all $i \in I$ and $|I| > 1$. From $(G, Q) \in \downarrow_r$ we get $Q = \vec{\pi}; \sum_{i \in I} \mathbf{p}?l_i; Q_i$ and $(G_i, \vec{\pi}; \mathbf{p}?l_i; Q_i) \in \downarrow_r$ for all $i \in I$.
Since $(\mathbf{p}?l_i; P_i, \vec{\pi}; \mathbf{p}?l_i; Q_i) \in \mathcal{R}_r$ for all $i \in I$, by induction Clause (b) is satisfied. Thus $\vec{\pi} = \epsilon$ and $(P_i, Q_i) \in \mathcal{R}_r$ for all $i \in I$.
3. Case $G = \coprod_{j \in J} qr!l'_j; G_j$ with $q \neq p$ and $P = pq!l; \vec{\pi}; \sum_{j \in J} q?l'_j; P'_j$ and
   $(G_j, pq!l; \vec{\pi}; q?l'_j; P'_j) \in \downarrow_r$ for all $j \in J$. From $(G, Q) \in \downarrow_r$ we get $Q = \vec{\pi}'; \sum_{j \in J} q?l'_j; Q'_j$
   and $(G_j, \vec{\pi}'; q?l'_j; Q'_j) \in \downarrow_r$ for all $j \in J$. Since $(pq!l; \vec{\pi}; q?l'_j; P'_j, \vec{\pi}'; q?l'_j; Q'_j) \in \mathcal{R}_r$ for
   all $j \in J$, by induction Clause (b) is satisfied.
   Thus $\vec{\pi} = pq!l; \vec{\pi}$ and $(\vec{\pi}; q?l'_j; P'_j, \vec{\pi}; q?l'_j; Q'_j) \in \mathcal{R}_r$ for all $j \in J$.

4. Case $G = \coprod_{j \in J} qs!l'_j; G_j$ and $r \neq s$ and $r \in \text{play}(G_j)$ and $(G_j, P) \in \downarrow_r$ for $j \in J$. From $(G, Q) \in \downarrow_r$ we get $(G_j, Q) \in \downarrow_r$ for all $j \in J$. Then $(P, Q) \in \mathcal{R}_r$.

5. Case $G = qs!l; G'$ and $r \in \text{play}(G')$. Then $(G', P) \in \downarrow_r$. From $(G, Q) \in \downarrow_r$ we get $(G', Q) \in \downarrow_r$. Then $(P, Q) \in \mathcal{R}_r$.

**Lemma 3.10** If $G \parallel \mathcal{M} \xrightarrow{\beta} G'$ \quad $\mathcal{M}'$ is a top transition and $G \parallel \mathcal{M}$ is well formed, then $G' \parallel \mathcal{M}'$ is well formed too.

**Proof:** If the transition is derived using Rule [EXT-OUT], then $G = \coprod_{i \in I} pq!l_i; G_i$ and for some $k \in I$ we have $G' = G_k$ and $\mathcal{M}' \equiv \mathcal{M} \cdot \langle p, l_k, q \rangle$. We show that $G_k \parallel \mathcal{M} \cdot \langle p, l_k, q \rangle$ is well formed. Since $G \upharpoonright p$ is defined for all $p$, by definition of projection also $G_k \upharpoonright p$ is defined for all $p$. Since $G$ is bounded and $G_k$ is a subtree of $G$, also $G_k$ is bounded. Finally, $\vdash^b G \parallel \mathcal{M}$ implies $\vdash^b G_k \parallel \mathcal{M} \cdot \langle p, l_k, q \rangle$ by inversion on Rule [OUT] of Figure 3.

If the transition is derived using Rule [EXT-IN], then $G = pq?l; G'$ and the proof is similar and simpler.

**Lemma 3.11** Let $G \parallel \mathcal{M}$ be well formed.

1. If $G \upharpoonright p = \bigoplus_{i \in I} q!l_i; P_i$, then $G \parallel \mathcal{M} \xrightarrow{pq!l_i} G_i \parallel \mathcal{M} \cdot \langle p, l_i, q \rangle$ and $G_i \upharpoonright p = P_i$ for all $i \in I$.

2. If $G \upharpoonright q = \sum_{i \in I} p?l_i; P_i$ and $\mathcal{M} \equiv \langle p, l, q \rangle \cdot \mathcal{M}'$ for some $l$, then $I = \{k\}$ and $l = l_k$ and $G \parallel \mathcal{M} \xrightarrow{pq?l_k} G' \parallel \mathcal{M}'$ and $G' \upharpoonright q = P_k$.

**Proof:** (1) The proof is by induction on $d = \text{depth}(G, p)$.

*Case* $d = 1$. By definition of projection (see Figure 2), $G \upharpoonright p = \bigoplus_{i \in I} q!l_i; P_i$ implies $G = \coprod_{i \in I} pq!l_i; G_i$ with $G_i \upharpoonright p = P_i$ for all $i \in I$. Then by Rule [EXT-OUT] we may conclude $G \parallel \mathcal{M} \xrightarrow{pq!l_i} G_i \parallel \mathcal{M} \cdot \langle p, l_i, q \rangle$ for all $i \in I$.

*Case* $d > 1$. In this case either i) $G = \coprod_{j \in J} rs!l'_j; G_j$ with $r \neq p$ or ii) $G = rs?l; G$ with $s \neq p$. i) There are three subcases.

If $s = p$ and $|J| = 1$, say $J = \{1\}$, then $G = rp!l'_1; G_1$. By definition of projection and by assumption $G \upharpoonright p = G_1 \upharpoonright p = \bigoplus_{i \in I} q!l_i; P_i$. By Lemma 3.5(1) $\text{depth}(G, p) > \text{depth}(G_1, p)$. By Lemma 3.10 $G_1 \parallel \mathcal{M} \cdot \langle r, l'_1, p \rangle$ is well formed. Then by induction

$$G_1 \parallel \mathcal{M} \cdot \langle r, l'_1, p \rangle \xrightarrow{pq!l_i} G'_i \parallel \mathcal{M} \cdot \langle r, l'_1, p \rangle \cdot \langle p, l_i, q \rangle$$
and $G'_i \upharpoonright p = P_i$ for all $i \in I$. Since $M \cdot \langle r, \ell'_1, p \rangle \cdot \langle p, \ell_i, q \rangle \equiv M \cdot \langle p, \ell_i, q \rangle \cdot \langle r, \ell'_1, p \rangle$, by Rule [ICOMM-OUT] we get $G \parallel M \xrightarrow{pq!\ell_i} rp!\ell'_1; G'_i \parallel M \cdot \langle p, \ell_i, q \rangle$ for all $i \in I$. By definition of projection ($rp!\ell'_1; G'_i \upharpoonright p = G'_i \upharpoonright p$ and so ($rp!\ell'_1; G'_i \upharpoonright p = P_i$ for all $i \in I$.

If $s = p$ and $|J| > 1$, by definition of projection and the assumption that $G \upharpoonright p$ is a choice of output actions on $q$ we have that $G \upharpoonright p = q!\ell; P$ with $P = \bar{\pi}; \Sigma_{j \in J} r?\ell'_j; Q_j$ and $G_j \upharpoonright p = q!\ell; \bar{\pi}; r?\ell'_j; Q_j$ for all $j \in J$. By Lemma 3.5(1) depth($G, p$) > depth($G_j, p$) for all $j \in J$. By Lemma 3.10 $G_j \parallel M \cdot \langle r, \ell'_j, s \rangle$ is well formed. This implies $G_j \parallel M \cdot \langle r, \ell'_j, s \rangle \xrightarrow{pq!\ell} G'_j \parallel M \cdot \langle r, \ell'_j, s \rangle \cdot \langle p, \ell, q \rangle$ and $G'_j \upharpoonright p = \bar{\pi}; r?\ell'_j; Q_j$ for all $j \in J$ by induction. Since $M \cdot \langle r, \ell'_j, s \rangle \cdot \langle p, \ell, q \rangle \equiv M \cdot \langle p, \ell, q \rangle \cdot \langle r, \ell'_j, s \rangle$, by Rule [ICOMM-OUT] we get

$G \parallel M \xrightarrow{pq!\ell} \boxtimes_{j \in J} rp!\ell'_j; G'_j \parallel M \cdot \langle p, \ell, q \rangle$. Lastly ($\boxtimes_{j \in J} rp!\ell'_j; G'_j \upharpoonright p = \bar{\pi}; \Sigma_{j \in J} r?\ell'_j; Q_j$ since $G'_j \upharpoonright p = \bar{\pi}; r?\ell'_j; Q_j$. We may then conclude that ($\boxtimes_{j \in J} rp!\ell'_j; G'_j \upharpoonright p = P$.

If $s \neq p$, then by definition of projection $G \upharpoonright p = G_j \upharpoonright p$ for all $j \in J$. By Lemma 3.5(1) depth($G, p$) > depth($G_j, p$) for all $j \in J$. Then by induction $G_j \parallel M \xrightarrow{pq!\ell_i} G_{i,j} \parallel M \cdot \langle p, \ell_i, q \rangle$ and $G_{i,j} \upharpoonright p = P_i$ for all $i \in I$ and all $j \in J$. By Rule [ICOMM-OUT]

$$G \parallel M \xrightarrow{pq!\ell_i} \boxtimes_{j \in J} rs!\ell'_j; G_{i,j} \parallel M \cdot \langle p, \ell_i, q \rangle$$

for all $i \in I$. By definition of projection ($\boxtimes_{j \in J} rs!\ell'_j; G_{i,j} \upharpoonright p = G_{i,j} \upharpoonright p = P_i$ for all $i \in I$.

ii) The proof of this case is similar and simpler than the proof of Case i). It uses Lemmas 3.5(2) and 3.10 and Rule [ICOMM-IN], instead of Lemmas 3.5(1) and 3.10 and Rule [ICOMM-OUT]. Note that, in order to apply Rule [ICOMM-IN], we need $M \equiv \langle r, \ell, s \rangle \cdot M'$. This derives from balancing of $rs?\ell; G' \parallel M$ using Rule [IN] of Figure 3.

(2) The proof is by induction on $d = \text{depth}(G, q)$.

Case $d = 1$. By definition of projection and the hypothesis $G \upharpoonright q = \Sigma_{i \in I} p?\ell_i; P_i$, it must be $G = pq?\ell; G'$ and $|I| = 1$, say $I = \{k\}$, and $\ell = \ell_k$ and $G' \upharpoonright q = P_k$. Then by Rule [EXT-IN] we deduce $G \parallel \langle p, \ell_k, q \rangle \cdot M' \xrightarrow{pq?\ell_k} G' \parallel M'$.

Case $d > 1$. In this case either i) $G = \boxtimes_{j \in J} rs!\ell'_j; G_j$ with $r \neq q$ or ii) $G = rs?\ell; G'$ with $s \neq q$. i) There are two subcases, depending on whether $s = q$ or $s \neq q$. The most interesting case is the first one, namely $G = \boxtimes_{j \in J} rq!\ell'_j; G_j$. By definition of projection $G \upharpoonright q = \bar{\pi}; \Sigma_{j \in J} r?\ell'_j; Q_j$, where $G_j \upharpoonright q = \bar{\pi}; r?\ell'_j; Q_j$. By assumption $G \upharpoonright q = \Sigma_{i \in I} p?\ell_i; P_i$, thus it must be either $\bar{\pi} = \epsilon$ or $|I| = 1$, say $I = \{k\}$, and $\bar{\pi} = p?\ell_k; \bar{\pi}^r$.

If $\bar{\pi} = \epsilon$, we have that $r = p$ and $J = I$ and $\ell'_i = \ell_i$ and $Q_i = P_i$ for all $i \in I$. This means that $G = \boxtimes_{i \in I} pq!\ell_i; G_i$ and $G_i \upharpoonright q = p?\ell_i; P_i$. Let $M_i \equiv \langle p, \ell, q \rangle \cdot M'_i$, where $M'_i = M' \cdot \langle p, \ell_i, q \rangle$. By Lemma 3.10 $M_i$ is well formed for all $i \in I$. By induction hypothesis, $G_i \parallel M_i \xrightarrow{pq?\ell} G'_i \parallel M'_i$ and $\ell = \ell_i$ and $G'_i \upharpoonright q = P_i$ for all $i \in I$. This implies that $|I| = 1$, say $I = \{k\}$. Then $G = pq!\ell; G_k$ and by Rule [ICOMM-OUT] we deduce $G \parallel M \xrightarrow{pq?\ell} G' \parallel M'$, where $G' = pq!\ell; G'_k$. Whence by definition of projection $G \upharpoonright q = G_k \upharpoonright q = p?\ell_k; P_k$ and $G' \upharpoonright q = G'_k \upharpoonright q = P_k$.

If $\bar{\pi} = p?\ell_k; \bar{\pi}^r$, then $G \upharpoonright q = p?\ell_k; P_k$, where $P_k = \bar{\pi}^r; \Sigma_{j \in J} r?\ell'_j; Q_j$. Let $M_j \equiv \langle p, \ell, q \rangle \cdot M'_j$, where $M'_j = M' \cdot \langle r, \ell'_j, q \rangle$. For all $j \in J$, $G_j \parallel M_j$ is well formed by Lemma 3.10 and depth($G, q$) > depth($G_j, q$) by Lemma 3.5(1). By induction hypothesis we get $\ell = \ell_k$ and $G_j \parallel M_j \xrightarrow{pq?\ell} G'_j \parallel M'_j$ for all $j \in J$. Let $G' = \boxtimes_{j \in J} rq!\ell'_j; G'_j$. Then $G \parallel M \xrightarrow{pq?\ell} G' \parallel M'$ by Rule [ICOMM-OUT] and $G' \upharpoonright q = \bar{\pi}^r; \Sigma_{j \in J} r?\ell'_j; Q_j = P_k$.

ii) The proof of this case is similar and simpler than the proof of Case i). It uses Lemmas 3.5(2)
and 3.10 and Rule [ICOMM-IN], instead of Lemmas 3.5(1) and 3.10 and Rule [ICOMM-OUT].
Note that, in order to apply Rule [ICOMM-IN], we need $\mathcal{M} \equiv \langle r, \ell, s \rangle \cdot \mathcal{M}'$. This derives from
balancing of $rs?\ell$; $G' \parallel \mathcal{M}$ using Rule [IN] of Figure 3.

**Lemma 3.13** Let $G \parallel \mathcal{M}$ be well formed.

1. If $G \parallel \mathcal{M} \xrightarrow{pq!\ell} G' \parallel \mathcal{M}'$, then $\mathcal{M}' \equiv \mathcal{M} \cdot \langle p, \ell, q \rangle$ and $G \upharpoonright p = \bigoplus_{i \in I} q!\ell_i; P_i$ and $\ell = \ell_k$ and $G' \upharpoonright p = P_k$ for some $k \in I$ and $G \upharpoonright r \le G' \upharpoonright r$ for all $r \neq p$.

2. If $G \parallel \mathcal{M} \xrightarrow{pq?\ell} G' \parallel \mathcal{M}'$, then $\mathcal{M} \equiv \langle p, \ell, q \rangle \cdot \mathcal{M}'$ and $G \upharpoonright q = pq?\ell; G' \upharpoonright q$ and $G \upharpoonright r \le G' \upharpoonright r$ for all $r \neq q$.

**Proof:** (1) By induction on the inference of the transition $G \parallel \mathcal{M} \xrightarrow{pq!\ell} G' \parallel \mathcal{M}'$.

*Base Case.* The applied rule must be Rule [*EXT-OUT*], so $G = \bigoplus_{i \in I} pq!\ell_i; G_i$ and $\ell = \ell_k$ and $G' = G_k$ for some $k \in I$, and

$$ \bigoplus_{i \in I} pq!\ell_i; G_i \parallel \mathcal{M} \xrightarrow{pq!\ell_k} G_k \parallel \mathcal{M} \cdot \langle p, \ell_k, q \rangle $$

By definition of projection $G \upharpoonright p = \bigoplus_{i \in I} q!\ell_i; G_i \upharpoonright p$ and $G' \upharpoonright p = G_k \upharpoonright p$. Again by definition of projection, if $r \notin \{p, q\}$ or $r = q$ and $|I| = 1$, we have $G \upharpoonright r = G_1 \upharpoonright r$ and so $G \upharpoonright r = G' \upharpoonright r$. If $r = q$ and $|I| > 1$, then $G \upharpoonright q = \bar{\pi}'; \sum_{i \in I} p?\ell_i; Q_i$, where $G_i \upharpoonright q = \bar{\pi}'; p?\ell_i; Q_i$ for all $i \in I$ and so $G \upharpoonright q \le G_k \upharpoonright q$.

*Inductive Cases.* If the applied rule is [ICOMM-OUT], then $G = \bigoplus_{j \in J} st!\ell'_j; G_j$ and $G' = \bigoplus_{j \in J} st!\ell'_j; G'_j$ and

$$ \frac{G_j \parallel \mathcal{M} \cdot \langle s, \ell'_j, t \rangle \xrightarrow{pq!\ell} G'_j \parallel \mathcal{M}' \cdot \langle s, \ell'_j, t \rangle \quad j \in J \quad p \neq s}{\bigoplus_{j \in J} st!\ell'_j; G_j \parallel \mathcal{M} \xrightarrow{pq!\ell} \bigoplus_{j \in J} st!\ell'_j; G'_j \parallel \mathcal{M}'} $$

By Lemma 3.10 $G_j \parallel \mathcal{M} \cdot \langle s, \ell'_j, t \rangle$ is well formed. By induction hypothesis $\mathcal{M}' \cdot \langle s, \ell'_j, t \rangle \equiv \mathcal{M} \cdot \langle s, \ell'_j, t \rangle \cdot \langle p, \ell, q \rangle$, which implies $\mathcal{M}' \equiv \mathcal{M} \cdot \langle p, \ell, q \rangle$. If $p \neq t$, by definition of projection $G \upharpoonright p = G_1 \upharpoonright p$ and $G_j \upharpoonright p = G_1 \upharpoonright p$ for all $j \in J$. Similarly $G' \upharpoonright p = G'_1 \upharpoonright p$ and $G'_j \upharpoonright p = G'_1 \upharpoonright p$ for all $j \in J$. By induction hypothesis $G_1 \upharpoonright p = \bigoplus_{i \in I} q!\ell_i; P_i$ and $\ell = \ell_k$ and $G'_1 \upharpoonright p = P_k$ for some $k \in I$. This implies $G \upharpoonright p = \bigoplus_{i \in I} q!\ell_i; P_i$ and $G' \upharpoonright p = P_k$.

If $p = t$ and $|J| = 1$ the proof is as in the previous case by definition of projection.

If $p = t$ and $|J| > 1$, then the definition of projection gives $G \upharpoonright p = \bar{\pi}'; \sum_{j \in J} s?\ell'_j; Q_j$ and $G_j \upharpoonright p = \bar{\pi}'; s?\ell'_j; Q_j$ and $G' \upharpoonright p = \bar{\pi}'; \sum_{j \in J} s?\ell'_j; Q'_j$ and $G'_j \upharpoonright p = \bar{\pi}'; s?\ell'_j; Q'_j$ for all $j \in J$. By induction hypothesis $\bar{\pi} = q!\ell; \bar{\pi}',$ which implies $G \upharpoonright p = q!\ell; G' \upharpoonright p$.

For $r \notin \{p, s, t\}$ by definition of projection $G \upharpoonright r = G_1 \upharpoonright r$ and $G_j \upharpoonright r = G_1 \upharpoonright r$ for all $j \in J$. Similarly $G' \upharpoonright r = G'_1 \upharpoonright r$ and $G'_j \upharpoonright r = G'_1 \upharpoonright r$ for all $j \in J$. By induction hypothesis $G_1 \upharpoonright r \le G'_1 \upharpoonright r$, which implies $G \upharpoonright r \le G' \upharpoonright r$.

For participant $s$ we have $G \upharpoonright s = \bigoplus_{j \in J} t!\ell'_j; G_j \upharpoonright s \le \bigoplus_{j \in J} t!\ell'_j; G'_j \upharpoonright s = G' \upharpoonright s$.

For participant $t \neq p$ if $|J| = 1$ the proof is the same as for $r \notin \{p, s, t\}$. If $|J| > 1$, then we have $G \upharpoonright t = \bar{\pi}'; \sum_{j \in J} s?\ell'_j; R_j$, where $G_j \upharpoonright t = \bar{\pi}'; s?\ell'_j; R_j$ and $G' \upharpoonright t = \bar{\pi}'; \sum_{j \in J} s?\ell'_j; R'_j$, where $G'_j \upharpoonright t = \bar{\pi}'; s?\ell'_j; R'_j$. From $G_j \upharpoonright t \le G'_j \upharpoonright t$ for all $j \in J$ we get $\bar{\pi}' = \bar{\pi}$ and $R_j \le R'_j$ for all $j \in J$. This implies $G \upharpoonright t \le G' \upharpoonright t$.

If the applied rule is [ICOMM-IN] the proof is similar and simpler.
(2) The proof is similar to the proof of (1). The most interesting case is the application of Rule [ICOMM-OUT]

$$
\frac{G_j \parallel \mathcal{M} \cdot \langle s, \ell'_j, t \rangle \xrightarrow{\text{pq}?\ell} G'_j \parallel \mathcal{M}' \cdot \langle s, \ell'_j, t \rangle \quad j \in J \quad q \neq s}{\boxplus_{j \in J} \text{st}! \ell'_j; G_j \parallel \mathcal{M} \xrightarrow{\text{pq}?\ell} \boxplus_{j \in J} \text{st}! \ell'_j; G'_j \parallel \mathcal{M}'}
$$

By Lemma 3.10 $G_j \parallel \mathcal{M} \cdot \langle s, \ell'_j, t \rangle$ is well formed. By induction hypothesis $\mathcal{M} \cdot \langle s, \ell'_j, t \rangle \equiv \langle p, \ell, q \rangle \cdot \mathcal{M}' \cdot \langle s, \ell'_j, t \rangle$, which implies $\mathcal{M} = \langle p, \ell, q \rangle \cdot \mathcal{M}'$. If $q \neq t$, by definition of projection $G \upharpoonright q = G_1 \upharpoonright q$ and $G_j \upharpoonright q = G_1 \upharpoonright q$ for all $j \in J$. Similarly $G' \upharpoonright q = G'_1 \upharpoonright q$ and $G'_j \upharpoonright q = G'_j \upharpoonright q$ for all $j \in J$. By induction hypothesis $G_1 \upharpoonright q = pq?\ell; G'_1 \upharpoonright q$. This implies $G \upharpoonright q = pq?\ell; G' \upharpoonright p$. If $q = t$ and $|J| = 1$ the proof is as in the previous case by definition of projection.

If $q = t$ and $|J| > 1$, then the definition of projection gives $G \upharpoonright q = \bar{\pi}'; \sum_{j \in J} s?\ell'_j; Q_j$ and
$G_j \upharpoonright q = \bar{\pi}'; s?\ell'_j; Q_j$ and $G' \upharpoonright q = \bar{\pi}'; \sum_{j \in J} s?\ell'_j; Q'_j$ and $G'_j \upharpoonright q = \bar{\pi}'; s?\ell'_j; Q'_j$ for all $j \in J$. By
induction hypothesis $\bar{\pi} = p?\ell; \bar{\pi}'$, which implies $G \upharpoonright q = p?q\ell; G' \upharpoonright p$.

The proof of $G \upharpoonright r \leq G' \upharpoonright r$ for all $r \neq q$ is as in Case (1).

**Lemma 3.14** If $f \vdash^b G \parallel \mathcal{M}$ and $G \parallel \mathcal{M} \xrightarrow{\beta} G' \parallel \mathcal{M}'$, then $f \vdash^b G' \parallel \mathcal{M}'$.

**Proof:** By induction on the inference of the transition $G \parallel \mathcal{M} \xrightarrow{\beta} G' \parallel \mathcal{M}'$ of Figure 5.

*Base Cases.* Immediate from Lemma 3.10.

Inductive Cases. Let $G \parallel \mathcal{M} \xrightarrow{\beta} G' \parallel \mathcal{M}'$ with Rule [ICOMM-OUT]. Then we get $G = \boxplus_{i \in I} pq!\ell_i; G_i$ and $G' = \boxplus_{i \in I} pq!\ell_i; G'_i$ and $G_i \parallel \mathcal{M} \cdot \langle p, \ell_i, q \rangle \xrightarrow{\beta} G'_i \parallel \mathcal{M}' \cdot \langle p, \ell_i, q \rangle$ for all $i \in I$. From Rule [OUT] of Figure 3, we get $\vdash^b G_i \parallel \mathcal{M} \cdot \langle p, \ell_i, q \rangle$ for all $i \in I$. By induction hypotheses for all $i \in I$ we can derive $\vdash^b G'_i \parallel \mathcal{M} \cdot \langle p, \ell_i, q \rangle$. Therefore using Rule [OUT] we conclude $\vdash^b G' \parallel \mathcal{M}'$.

Similarly for Rule [ICOMM-IN].

**Lemma 8.5** 1. If $\rho \prec \omega \rho'$ and $\beta \diamond \rho$ and $\beta \diamond \rho'$ and $\beta \triangleright \omega$ are defined, then $\beta \diamond \rho \prec \beta \triangleright \omega \beta \diamond \rho'$.

2. If $\rho \prec \omega \rho'$ and $\beta \triangleright \omega$ is defined, then $\beta \diamond \rho \prec \beta \triangleright \omega \beta \diamond \rho'$.

3. If $\rho \# \rho'$ and both $\beta \diamond \rho$ and $\beta \diamond \rho'$ are defined, then $\beta \diamond \rho \# \beta \diamond \rho'$.

4. If $\rho \# \rho'$, then $\beta \diamond \rho \# \beta \diamond \rho'$.

**Proof:** (1) If $\rho \prec \omega \rho'$, then

• either $\rho = p :: \eta$ and $\rho' = p :: \eta'$ and $\eta < \eta'$,

* or $\rho = p :: \zeta \cdot q!\ell$ and $\rho' = q :: \zeta' \cdot p?\ell$ and $(\omega @ p \cdot \zeta) \vdash q \preceq \vdash \approx (\omega @ q \cdot \zeta'') \vdash p$
  for some $\zeta''$ and $\chi$ such that $(\zeta' \cdot p?\ell) \vdash p \preceq (\zeta'' \cdot p?\ell \cdot \chi) \vdash p$.
In the first case, from the fact that $\beta \diamond \rho$ and $\beta \diamond \rho'$ are defined and Definition 8.1(1) we get
$\beta \diamond \rho = p :: \eta_1$ and $\beta \diamond \rho' = p :: \eta'_1$, where $\eta = \beta @ p \cdot \eta_1$ and $\eta' = \beta @ p \cdot \eta'_1$. Since $\eta_1 < \eta'_1$
we conclude $\beta \diamond \rho \prec \beta \diamond \omega \prec \beta \diamond \rho'$.

In the second case, let $\omega' = \beta \triangleright \omega$.

If $\text{play}(\beta) \not\subset \{p,q\}$, then $\beta @ p = \beta @ q = \epsilon$ and $\beta \diamond \rho = \rho$ and $\beta \diamond \rho' = \rho'$. Moreover, by Definition 8.3(1) $(\omega' @ p) \upharpoonright q = (\omega @ p) \upharpoonright q$ and $(\omega' @ q) \upharpoonright p = (\omega @ q) \upharpoonright p$. Therefore $(\omega @ p \cdot \zeta) \upharpoonright q \lesssim \upharpoonright \approx (\omega @ q \cdot \zeta'') \upharpoonright p$ implies $(\omega' @ p \cdot \zeta) \upharpoonright q \lesssim \upharpoonright \approx (\omega' @ q \cdot \zeta'') \upharpoonright p$ which proves that $\beta \diamond \rho \prec \omega' \beta \diamond \rho'$.

If $\text{play}(\beta) = \{p\}$, then either $\beta = \text{pr!}\ell'$ or $\beta = \text{rp?}\ell'$.

If $\beta = \text{pr!}\ell'$, then $\beta @ p = r!\ell'$ and $\beta @ q = \epsilon$. By Definition 8.1(1), since $\beta \diamond \rho$ is defined we have $\zeta = r!\ell' \cdot \zeta_1$. Then $\beta \diamond \rho = p :: \zeta_1 \cdot q!\ell$ and $\beta \diamond \rho' = \rho'$. Moreover, by Definition 8.3(1) $\omega' @ p = (\omega @ p) \cdot r!\ell'$ and $\omega' @ q = \omega @ q$. Therefore $\omega @ p \cdot \zeta = \omega @ p \cdot r!\ell' \cdot \zeta_1 = \omega' @ p \cdot \zeta_1$ and $\omega @ q \cdot \zeta'' = \omega' @ q \cdot \zeta''$. Then, from the fact that $(\omega @ p \cdot \zeta) \upharpoonright q \lesssim \upharpoonright \approx (\omega @ q \cdot \zeta'') \upharpoonright p$ it follows that $(\omega' @ p \cdot \zeta_1) \upharpoonright q \lesssim \upharpoonright \approx (\omega' @ q \cdot \zeta'') \upharpoonright p$.

If $\beta = \text{rp?}\ell'$, then $\beta @ p = r?\ell'$ and $\beta @ q = \epsilon$. By Definition 8.1(1), since $\beta \diamond \rho$ is defined we have $\zeta = r?\ell' \cdot \zeta_1$. Then $\beta \diamond \rho = p :: \zeta_1 \cdot q!\ell$ and $\beta \diamond \rho' = \rho'$. We now distinguish two subcases, according to whether $r = q$ or $r \neq q$.

If $r = q$, then by Definition 8.3(1) $\omega @ p = \omega' @ p$ and $\omega @ q = p!\ell' \cdot (\omega' @ q)$. Therefore we get $\omega @ p \cdot \zeta = (\omega' @ p) \cdot q?\ell' \cdot \zeta_1$ and $\omega @ q \cdot \zeta'' = p!\ell' \cdot \omega' @ q \cdot \zeta''$. Then, from the fact that $(\omega @ p \cdot \zeta) \upharpoonright q \lesssim \upharpoonright \approx (\omega @ q \cdot \zeta'') \upharpoonright p$ and $(\omega' @ p) \upharpoonright q$ cannot contain inputs, it follows that $(\omega' @ p) \upharpoonright q \cdot \zeta_1 \upharpoonright q \lesssim \upharpoonright \approx (\omega' @ q \cdot \zeta'') \upharpoonright p$.

If $r \neq q$, then by Definition 8.3(1) $\omega @ p = \omega' @ p$ and $\omega @ q = \omega' @ q$. In this case we get $(\omega @ p \cdot \zeta) \upharpoonright q = (\omega' @ p \cdot r?\ell' \cdot \zeta_1) \upharpoonright q = (\omega' @ p \cdot \zeta_1) \upharpoonright q$ and $\omega @ q \cdot \zeta'' = \omega' @ q \cdot \zeta''$. Then, from $(\omega @ p \cdot \zeta) \upharpoonright q \lesssim \upharpoonright \approx (\omega @ q \cdot \zeta'') \upharpoonright p$ it follows that $(\omega' @ p \cdot \zeta_1) \upharpoonright q \lesssim \upharpoonright \approx (\omega' @ q \cdot \zeta'') \upharpoonright p$.
If $\text{play}(\beta) = \{q\}$ the proof is similar.

(2) The proof is similar to that of Fact (1).

(3) Let $\rho = p :: \eta$ and $\rho' = p :: \eta' \text{ and } \eta \# \eta'$. From $\beta \diamond \rho$ and $\beta \diamond \rho'$ defined we get $\eta = \beta @ p \cdot \eta_1$ and $\eta' = \beta @ p \cdot \eta'_1$ and $\beta \diamond \rho = p :: \eta_1$ and $\beta \diamond \rho' = p :: \eta'_1$ by Definition 8.1(1).
Since $\eta \# \eta'$ implies $\eta_1 \# \eta'_1$ we conclude $\beta \diamond \rho \# \beta \diamond \rho'$.

In the following we use the notation $\overline{pq}?\ell$ defined by $\overline{pq}?\ell = pq!\ell$.

**Lemma 8.14** Let $\text{play}(\beta_1) \cap \text{play}(\beta_2) = \emptyset$.

1. If both $\beta_2 \triangleright \omega$ and $\beta_2 \triangleright (\beta_1 \triangleright \omega)$ are defined, then $\beta_1 \triangleright (\beta_2 \triangleright \omega) \cong \beta_2 \triangleright (\beta_1 \triangleright \omega)$.

2. If both $\beta_1 \triangleright \omega$ and $\beta_2 \triangleright \omega$ are defined, then $\beta_1 \triangleright (\beta_2 \triangleright \omega)$ is defined and $\beta_1 \triangleright (\beta_2 \triangleright \omega) \cong \beta_2 \triangleright (\beta_1 \triangleright \omega)$.

**Proof:** (1) Since $\omega_2 = \beta_2 \triangleright \omega$ is defined, by Definition 8.3(1) $\omega \cong \beta_2 \cdot \omega_2$ when $\beta_2$ is an input. Since $\beta_2 \triangleright (\beta_1 \triangleright \omega)$ is defined, $\omega_1 = \beta_1 \triangleright \omega$ is defined and by Definition 8.3 $\omega \cong \omega_1 \cdot \beta_1$ when $\beta_1$ is an output and $\omega \cong \beta_2 \cdot \omega_0 \cdot \beta_1$ for some $\omega_0$ such that $\omega_1 \cong \beta_2 \cdot \omega_0$ and $\omega_2 \cong \omega_0 \cdot \beta_1$, when $\beta_1$ is an output and $\beta_2$ is an input. Using Definition 8.3 we compute:
$$ \beta_1 \triangleright (\beta_2 \triangleright \omega) \cong \beta_2 \triangleright (\beta_1 \triangleright \omega) \cong \begin{cases} \omega_1 \cdot \beta_2 & \text{if both } \beta_1 \text{ and } \beta_2 \text{ are outputs} \\ \frac{\omega_0}{\beta_1} \cdot \omega \cdot \beta_2 & \text{if } \beta_1 \text{ is an output and } \beta_2 \text{ is an input} \\ \frac{\omega_1}{\beta_1} \cdot \omega_2 & \text{if both } \beta_1 \text{ and } \beta_2 \text{ are inputs} \end{cases} $$

(2) Since $\omega_i = \beta_i \triangleright \omega$ is defined for $i \in \{1, 2\}$, by Definition 8.3(2) $\omega \cong \omega_i \cdot \beta_i$ when $\beta_i$ is an output. Then from $\text{play}(\beta_1) \cap \text{play}(\beta_2) = \emptyset$ we get $\omega \cong \omega' \cdot \beta_1 \cdot \beta_2 \cong \omega' \cdot \beta_2 \cdot \beta_1$ for some $\omega'$ when both $\beta_1$ and $\beta_2$ are outputs. Using Definition 8.3(2) we compute:

$$ \beta_1 \triangleright (\beta_2 \triangleright \omega) \cong \beta_2 \triangleright (\beta_1 \triangleright \omega) \cong \begin{cases} \frac{\omega'}{\beta_1} \cdot \omega_j & \text{if both } \beta_1 \text{ and } \beta_2 \text{ are outputs} \\ \frac{\omega_1}{\beta_1} \cdot \omega_2 & \text{if both } \beta_1 \text{ and } \beta_2 \text{ are inputs} \end{cases} $$

**Lemma A.1.** 1. If $\beta \bullet [\omega, \beta \frown \omega \tau] \sim$ is defined, then $\omega \cdot \beta \cdot \tau$ is well formed and
$$ \beta \bullet [\omega, \beta \frown \omega \tau] \sim = [\beta \triangleright \omega, \tau] \sim $$

2. If $\beta \circ [\omega, \tau] \sim$ is defined, then $(\beta \triangleright \omega) \cdot \beta \cdot \tau$ is well formed and
$$ \beta \circ [\omega, \tau] \sim = [\beta \triangleright \omega, \beta \frown (\beta \triangleright \omega) \tau] \sim $$

**Lemma 8.15** 1. If $\beta \bullet \delta$ is defined, then $\beta \circ (\beta \bullet \delta) = \delta$.

2. If $\beta \circ \delta$ is defined, then $\beta \bullet (\beta \circ \delta) = \delta$.

3. If both $\beta_2 \bullet \delta$, $\beta_2 \bullet (\beta_1 \circ \delta)$ are defined, and $\text{play}(\beta_1) \cap \text{play}(\beta_2) = \emptyset$, then $\beta_1 \circ (\beta_2 \bullet \delta) = \beta_2 \bullet (\beta_1 \circ \delta)$.

4. If both $\beta_1 \circ \delta$, $\beta_2 \circ \delta$ are defined, and $\text{play}(\beta_1) \cap \text{play}(\beta_2) = \emptyset$, then $\beta_1 \circ (\beta_2 \circ \delta)$ is defined and $\beta_1 \circ (\beta_2 \circ \delta) = \beta_2 \circ (\beta_1 \circ \delta)$.

**Proof:** Statements (1) and (2) immediately follow from Lemma A.1. In the proofs of the remaining statements we convene that "$\beta$ is required in $\tau_1 \cdot \beta \cdot \tau_2$" is short for "the shown occurrence of $\beta$ is required in $\tau_1 \cdot \beta \cdot \tau_2$" and similarly for "$\beta$ matches an output in $\tau_1 \cdot \beta \cdot \tau_2$".

(3) Let $\delta = [\omega, \tau] \sim$. Since both $\beta_2 \bullet \delta$ and $\beta_2 \bullet (\beta_1 \circ \delta)$ are defined, by Lemma A.1 both $\beta_2 \triangleright \omega$ and $\beta_2 \triangleright (\beta_1 \triangleright \omega)$ must be defined. Then, by Lemma 8.14(1) $\beta_2 \triangleright (\beta_1 \triangleright \omega) \cong \beta_1 \triangleright (\beta_2 \triangleright \omega)$. So we set $\omega' = \beta_1 \triangleright (\beta_2 \triangleright \omega)$. Let $\omega_1 = \beta_1 \triangleright \omega$. By Definition 8.13(2) we get

$$ \delta_1 = \beta_1 \circ \delta = \begin{cases} [\omega_1, \beta_1 \cdot \tau] & \text{if } \beta_1 \cdot \tau \text{ is } \omega_1\text{-pointed} \\ [\omega_1, \tau] & \text{otherwise} \end{cases} $$

Let $\omega_2 = \beta_2 \triangleright \omega$. By Definition 8.13(1) we get

$$ \delta_2 = \beta_2 \bullet \delta = \begin{cases} [\omega_2, \tau'] & \text{if } \tau \approx_{\omega} \beta_2 \cdot \tau' \\ [\omega_2, \tau] & \text{if } \text{play}(\beta_2) \cap \text{play}(\tau) = \emptyset \end{cases} $$

The remainder of this proof is split into two cases, according to the shape of $\delta_2$.

Case $\delta_2 = [\omega_2, \tau] \sim$. Then $\text{play}(\beta_2) \cap \text{play}(\tau) = \emptyset$. By Definition 8.13(2) we get

$$ \beta_1 \circ \delta_2 = \begin{cases} [\omega', \beta_1 \cdot \tau] & \text{if } \beta_1 \cdot \tau \text{ is } \omega'\text{-pointed} \\ [\omega', \tau] & \text{otherwise} \end{cases} $$

Since $\text{play}(\beta_2) \cap \text{play}(\beta_1 \cdot \tau) = \emptyset$, by Definition 8.13(1) we get
$$
\beta_2 \bullet \delta_1 = \begin{cases} [\omega', \beta_1 \cdot \tau] \sim & \text{if } \beta_1 \cdot \tau \text{ is } \omega_1\text{-pointed} \\ [\omega', \tau] \sim & \text{otherwise} \end{cases}
$$

We have to show that

(**)$\beta_1 \cdot \tau$ is $\omega'$-pointed iff $\beta_1 \cdot \tau$ is $\omega_1$-pointed

If $\beta_1$ is an input, it must be required in $\tau$ for both $\omega'$-pointedness and $\omega_1$-pointedness, so this case is obvious.

Let $\beta_1 = \text{pq!l}$.

If $\beta_2$ is an output, then $\omega' \cong \omega_1 \cdot \beta_2$ by Definition 8.3(1). Since $\beta_2 \neq \text{pq!l}'$ for all $l'$, an input in $\tau$ matches $\beta_1$ in $\omega_1 \cdot \beta_2 \cdot \beta_1 \cdot \tau$ iff it matches $\beta_1$ in $\omega_1 \cdot \beta_1 \cdot \tau$.

If $\beta_2$ is an input, then $\omega_1 \cong \beta_2 \cdot \omega'$ by Definition 8.3(1). If $\beta_2 \neq \text{pq?l}'$ for all $l'$, then an input in $\tau$ matches $\beta_1$ in $\omega' \cdot \beta_1 \cdot \tau$ iff it matches $\beta_1$ in $\beta_2 \cdot \omega' \cdot \beta_1 \cdot \tau$. Let $\beta_2 = \text{pq?l}'$ for some $l'$. Since $\text{play}(\beta_2) \cap \text{play}(\tau) \neq \emptyset$, there is no input $\beta_0$ in $\tau$ such that $\beta_0$ matches $\beta_1$ in $\omega' \cdot \beta_1 \cdot \tau$ or in $\beta_2 \cdot \omega' \cdot \beta_1 \cdot \tau$. This concludes the proof of (**).

Case $\delta_2 = [\omega_2, \tau']$. Then $\tau \approx_{\omega} \beta_2 \cdot \tau'$. By Definition 8.13(2) we get

$$
\beta_1 \circ \delta_2 = \begin{cases} [\omega', \beta_1 \cdot \tau'] \sim & \text{if } \beta_1 \cdot \tau' \text{ is } \omega'\text{-pointed} \\ [\omega', \tau'] \sim & \text{otherwise} \end{cases}
$$

and, since $\delta = [\omega, \beta_2 \cdot \tau']$, by the same definition we get

$$
\beta_1 \circ \delta = \begin{cases} [\omega_1, \beta_1 \cdot \beta_2 \cdot \tau'] \sim & \text{if } \beta_1 \cdot \beta_2 \cdot \tau' \text{ is } \omega_1\text{-pointed} \\ [\omega_1, \beta_2 \cdot \tau'] \sim & \text{otherwise} \end{cases}
$$

We first show that $\beta_2 \cdot \beta_1 \cdot \tau' \approx_{\omega_1} \beta_1 \cdot \beta_2 \cdot \tau'$. Since $\beta_1 \circ \delta$ is defined, the trace $\omega_1 \cdot \beta_1 \cdot \beta_2 \cdot \tau'$ is well formed by Lemma A.1(2). So $\beta_1$ cannot be a matching input for $\beta_2$. To show that $\beta_2$ cannot be a matching input for $\beta_1$ observe that, if it were, then $\beta_1 = \bar{\beta}_2$. Since $\beta_2 \bullet (\beta_1 \circ \delta)$ is defined we have that $\omega_1 \equiv \bar{\beta}_2 \cdot \omega'$ by Definition 8.3(1). Therefore $\beta_2$ cannot be a matching input for $\beta_1$ in $\bar{\beta}_2 \cdot \omega' \cdot \beta_1 \cdot \beta_2 \cdot \tau'$, since it is the matching input of the first $\bar{\beta}_2$. From this and $\text{play}(\beta_1) \cap \text{play}(\beta_2) = \emptyset$ we get that $\beta_2 \cdot \beta_1 \cdot \tau' \approx_{\omega_1} \beta_1 \cdot \beta_2 \cdot \tau'$. Therefore

$$
\beta_1 \circ \delta = \begin{cases} [\omega_1, \beta_2 \cdot \beta_1 \cdot \tau'] \sim & \text{if } \beta_1 \cdot \beta_2 \cdot \tau' \text{ is } \omega_1\text{-pointed} \\ [\omega_1, \beta_2 \cdot \tau'] \sim & \text{otherwise} \end{cases}
$$

and by Definition 8.13(1)

$$
\beta_2 \bullet \delta_1 = \begin{cases} [\omega', \beta_1 \cdot \tau'] \sim & \text{if } \beta_1 \cdot \beta_2 \cdot \tau' \text{ is } \omega_1\text{-pointed} \\ [\omega', \tau'] \sim & \text{otherwise} \end{cases}
$$

We have to show that

(***) $\beta_1 \cdot \tau'$ is $\omega'$-pointed iff $\beta_1 \cdot \beta_2 \cdot \tau'$ is $\omega_1$-pointed

Note that $\beta_1$ is required in $\tau'$ iff it is required in $\beta_2 \cdot \tau'$ since $\text{play}(\beta_2) \cap \text{play}(\beta_1) = \emptyset$. Therefore the result is immediate when $\beta_1$ is an input.

Let $\beta_1$ be an output.

If $\beta_2$ is an output, then $\omega' \cong \omega_1 \cdot \beta_2$ by Definition 8.3(1). Suppose that $\beta_1 \cdot \tau'$ is $\omega'$-pointed, where $\tau' = \tau'_0 \cdot \beta_0 \cdot \tau_0''$ and $\beta_0$ matches $\beta_1$ in $\omega_1 \cdot \beta_2 \cdot \beta_1 \cdot \tau'_0 \cdot \beta_0 \cdot \tau_0''$. Then, since $\beta_2 \cdot \beta_1 \cdot \tau' \approx_{\omega_1} \beta_1 \cdot \beta_2 \cdot \tau'$, we have that $\beta_0$ matches $\beta_1$ in $\omega_1 \cdot \beta_1 \cdot \beta_2 \cdot \tau'_0 \cdot \beta_0 \cdot \tau_0''$, then $\beta_0$ matches $\beta_1$ in $\omega_1 \cdot \beta_2 \cdot \beta_1 \cdot \tau'_0 \cdot \beta_0 \cdot \tau_0''$. If $\beta_2$ is an input, then $\omega_1 \cong \beta_2 \cdot \omega'$ by Definition 8.3(1). Suppose that $\beta_1 \cdot \tau'$ is $\omega'$-pointed, where $\tau' = \tau'_0 \cdot \beta_0 \cdot \tau_0''$ and $\beta_0$ matches $\beta_1$ in $\omega' \cdot \beta_1 \cdot \tau'_0 \cdot \beta_0 \cdot \tau_0''$. Then $\beta_0$ matches $\beta_1$ in $\bar{\beta}_2 \cdot \omega' \cdot \beta_1 \cdot \beta_2 \cdot \tau'_0 \cdot \beta_0 \cdot \tau_0''$, since $\beta_2$ is the first input in the trace and it matches $\bar{\beta}_2$. In a similar
way we can prove that, if an input $\beta_0$ matches $\beta_1$ in $\overline{\beta_2} \cdot \omega' \cdot \beta_1 \cdot \beta_2 \cdot \tau_0' \cdot \beta_0 \cdot \tau_0''$, then $\beta_0$ matches $\beta_1$ in $\omega' \cdot \beta_1 \cdot \tau_0' \cdot \beta_0 \cdot \tau_0''$. Therefore (*** ) holds.

(4) Let $\delta = [\omega, \tau]$. Since $\beta_i \circ \delta$ is defined for $i \in \{1, 2\}$, by Lemma A.1(2) $\omega_i = \beta_i \triangleright \omega$ is defined for $i \in \{1, 2\}$. Then by Lemma 8.14(2) $\beta_1 \triangleright (\beta_2 \triangleright \omega) \cong \beta_2 \triangleright (\beta_1 \triangleright \omega)$. Let $\omega' = \beta_1 \triangleright (\beta_2 \triangleright \omega)$. Using Lemma A.1(2) we get for $i \in \{1, 2\}$

$$ \delta_i = \beta_i \circ [\omega, \tau] \sim = [\omega_i, \beta_i [\omega_i \tau] \sim $$

Using again Lemma A.1(2) we get

$$ \beta_2 \circ \delta_1 = \beta_2 \circ [\omega_1, \beta_1 [\omega_1 \tau] \sim] = [\omega', \beta_2 [\omega' (\beta_1 [\omega_1 \tau]) \sim] $$

Similarly

$$ \beta_1 \circ \delta_2 = \beta_1 \circ [\omega_2, \beta_2 [\omega_2 \tau] \sim] = [\omega', \beta_1 [\omega' (\beta_2 [\omega_2 \tau]) \sim] $$

We want to prove that

$$ (*) \quad \beta_1 [\omega' (\beta_2 [\omega_2 \tau]) \approx_{\omega'} \beta_2 [\omega' (\beta_1 [\omega_1 \tau])] $$

In the proof of (*) we will use the following facts, where $h, k = 1, 2$ and $h \neq k$:

(a) $\beta_h \cdot \beta_k \cdot \tau \approx_{\omega'} \beta_k \cdot \beta_h \cdot \tau$;

(b) if $\beta_h \cdot \tau$ is $\omega'$-pointed and $\beta_k \cdot \tau$ is not $\omega_k$-pointed, then $\beta_h \cdot \tau$ is $\omega_h$-pointed;

(c) if $\beta_h \cdot \tau$ is $\omega_h$-pointed and $\beta_k \cdot \tau$ is not $\omega_k$-pointed, then $\beta_h \cdot \tau$ is $\omega'$-pointed;

(d) $\beta_h \cdot \beta_k \cdot \tau$ is $\omega'$-pointed iff $\beta_h \cdot \tau$ is $\omega_h$-pointed and $\beta_k \cdot \tau$ is $\omega_k$-pointed.

Fact a. We show that $\beta_h \cdot \beta_k \cdot \tau \omega'$-swaps to $\beta_k \cdot \beta_h \cdot \tau$. By hypothesis $\text{play}(\beta_h) \cap \text{play}(\beta_k) = \emptyset$, so it is enough to show that $\beta_k$ does not match $\beta_h$ in the trace $\omega' \cdot \beta_h \cdot \beta_k \cdot \tau = (\beta_h \triangleright (\beta_k \triangleright \omega)) \cdot \beta_h \cdot \beta_k \cdot \tau$.

Suppose that $\beta_h$ is an output and $\beta_k$ is an input such that $\overline{\beta_k} = \beta_h$. Since $\delta_h = \beta_h \circ \delta$ is defined and $\beta_h$ is an output, it must be $\omega \cong \omega_h \cdot \beta_h$. Then, since $\delta_k = \beta_k \circ \delta$ is defined and $\beta_k$ is an input and $\overline{\beta_k} = \beta_h$, we get $\beta_k \triangleright \omega = \overline{\beta_k} \cdot \omega \cong \overline{\beta_k} \cdot \omega_h \cdot \beta_h \cong \beta_h \cdot \omega_h \cdot \beta_h$. Then $\omega' = \beta_h \triangleright (\beta_k \triangleright \omega) \cong \beta_h \cdot \omega_h$. Clearly, $\beta_k$ matches the initial output $\beta_h$ in the trace $\omega' \cdot \beta_h \cdot \beta_k \cdot \tau$, since $\beta_k$ is the first input in the trace and the initial $\beta_h$ is the first complementary output in the trace. Therefore $\beta_k$ does not match its adjacent output $\beta_h$.

Fact b. If $\beta_h$ is required in $\beta_h \cdot \tau$ - a condition that is always true when $\beta_h$ is an input and $\beta_h \cdot \tau$ is $\omega'$-pointed - then $\beta_h \cdot \tau$ is $\omega_0$-pointed for all $\omega_0$.

We may then assume that $\beta_h$ is an output that is not required in $\beta_h \cdot \tau$.

If $\beta_k$ is an output, then $\omega_h \cong \omega' \cdot \beta_k$. If an input matches $\beta_h$ in $\omega' \cdot \beta_h \cdot \tau$, then the same input matches $\beta_h$ in $\omega_h \cdot \beta_h \cdot \tau$, since $\text{play}(\beta_h) \cap \text{play}(\beta_k) = \emptyset$.

If $\beta_k$ is an input, then $\omega' \cong \overline{\beta_k} \cdot \omega_h$. Suppose $\beta_h = \text{pq!l}$ and $\beta_k = \text{rs?l}$. Observe that it must be $q \neq s$, because otherwise no input pq?l could occur in $\tau$, since $\beta_k \cdot \tau$ is not $\omega_k$-pointed, contradicting the hypotheses that $\beta_h \cdot \tau$ is $\omega'$-pointed and $\beta_h$ is not required in $\beta_h \cdot \tau$. Then the presence of $\overline{\beta_k} = \text{rs!l}$ cannot affect the multiplicity of pq! or pq? in any trace. Therefore, if an input matches $\beta_h$ in $\omega' \cdot \beta_h \cdot \tau$, then the same input matches $\beta_h$ in $\omega_h \cdot \beta_h \cdot \tau$.

Fact c. Again, we may assume that $\beta_h$ is an output that is not required in $\beta_h \cdot \tau$.

If $\beta_k$ is an output, then $\omega_h \cong \omega' \cdot \beta_k$. If an input matches $\beta_h$ in $\omega_h \cdot \beta_h \cdot \tau$, then the same input matches $\beta_h$ in $\omega' \cdot \beta_h \cdot \tau$, since $\text{play}(\beta_h) \cap \text{play}(\beta_k) = \emptyset$.

If $\beta_k$ is an input, then $\omega' \cong \overline{\beta_k} \cdot \omega_h$. Let $\beta_h = \text{pq!l}$ and $\beta_k = \text{rs?l}$. Again, it must be $q \neq s$, because otherwise no input pq?l could occur in $\tau$, since $\beta_k \cdot \tau$ is not $\omega_k$-pointed, contradicting the hypotheses that $\beta_h \cdot \tau$ is $\omega_h$-pointed and $\beta_h$ is not required in $\beta_h \cdot \tau$. Therefore, if an input matches $\beta_h$ in $\omega_h \cdot \beta_h \cdot \tau$, then the same input matches $\beta_h$ in $\omega' \cdot \beta_h \cdot \tau$.
Fact d. From play($\beta_h$) ∩ play($\beta_k$) = ∅ it follows that $\beta_h$ is required in $\beta_h \cdot \beta_k \cdot \tau$ iff $\beta_h$ is required in $\beta_h \cdot \tau$, and similarly for $\beta_k$. Let us then assume that $\beta_h$ and $\beta_k$ are not both required in $\beta_h \cdot \beta_k \cdot \tau$, i.e., that at least one of them is an output not required in $\beta_h \cdot \beta_k \cdot \tau$.

If both $\beta_h$ and $\beta_k$ are outputs, then $\omega_h \cong \omega' \cdot \beta_k$. Then an input matches $\beta_h$ in $\omega' \cdot \beta_h \cdot \beta_k \cdot \tau$ iff the same input matches $\beta_h$ in $\omega_h \cdot \beta_h \cdot \tau$, since $\beta_h \cdot \beta_k \cdot \tau \approx_{\omega'} \beta_k \cdot \beta_h \cdot \tau$ by Fact a.

Let $\beta_h = pq!l$ and $\beta_k = rs?l'$, where $\beta_h$ is not required in $\beta_h \cdot \beta_k \cdot \tau$. Then $\omega' \cong \overline{\beta_k} \cdot \omega_h$. Therefore an input matches $\beta_h$ in $\omega' \cdot \beta_h \cdot \beta_k \cdot \tau$ iff the same input matches $\beta_h$ in $\omega_h \cdot \beta_h \cdot \tau$, since $\beta_h \cdot \beta_k \cdot \tau \approx_{\omega'} \beta_k \cdot \beta_h \cdot \tau$ by Fact a.

We proceed now to prove (*). We distinguish three cases, according to whether:

i) each $\beta_i \cdot \tau$ is $\omega_i$-pointed, for $i = 1, 2$;

ii) no $\beta_i \cdot \tau$ is $\omega_i$-pointed, for $i = 1, 2$;

iii) $\beta_h \cdot \tau$ is $\omega_h$-pointed and $\beta_k \cdot \tau$ is not $\omega_k$-pointed, for $h, k = 1, 2$ and $h \neq k$.

Case i. Suppose each $\beta_i \cdot \tau$ is $\omega_i$-pointed, for $i = 1, 2$. Then $\beta_1 \frown_{\omega'} (\beta_2 \frown_{\omega_2} \tau) \approx_{\omega'} \beta_1 \frown_{\omega'} \beta_2 \cdot \tau$ and $\beta_2 \frown_{\omega'} (\beta_1 \frown_{\omega_1} \tau) \approx_{\omega'} \beta_2 \frown_{\omega'} \beta_1 \cdot \tau$. By Fact d both $\beta_1 \cdot \beta_2 \cdot \tau$ and $\beta_2 \cdot \beta_1 \cdot \tau$ are $\omega'$-pointed. Then $\beta_1 \frown_{\omega'} \beta_2 \cdot \tau \approx_{\omega'} \beta_1 \cdot \beta_2 \cdot \tau$ and $\beta_2 \frown_{\omega'} \beta_1 \cdot \tau \approx_{\omega'} \beta_2 \cdot \beta_1 \cdot \tau$. By Fact a $\beta_1 \cdot \beta_2 \cdot \tau \approx_{\omega'} \beta_2 \cdot \beta_1 \cdot \tau$.

Case ii. Suppose no $\beta_i \cdot \tau$ is $\omega_i$-pointed, for $i = 1, 2$. Then $\beta_1 \frown_{\omega'} (\beta_2 \frown_{\omega_2} \tau) \approx_{\omega'} \beta_1 \frown_{\omega'} \tau$ and $\beta_2 \frown_{\omega'} (\beta_1 \frown_{\omega_1} \tau) \approx_{\omega'} \beta_2 \frown_{\omega'} \tau$. By Fact b, no $\beta_i \cdot \tau$ can be $\omega'$-pointed, for $i \in \{1, 2\}$. Hence $\beta_1 \frown_{\omega'} \tau \approx_{\omega'} \beta_2 \frown_{\omega'} \tau$.

Case iii. Suppose $\beta_h \cdot \tau$ is $\omega_h$-pointed and $\beta_k \cdot \tau$ is not $\omega_k$-pointed, for $h, k = 1, 2$ and $h \neq k$. Then $\beta_h \frown_{\omega'} (\beta_k \frown_{\omega_k} \tau) \approx_{\omega'} \beta_h \frown_{\omega'} \tau$ and $\beta_k \frown_{\omega'} (\beta_h \frown_{\omega_h} \tau) \approx_{\omega'} \beta_k \frown_{\omega'} \beta_h \cdot \tau$. By Fact c $\beta_h \cdot \tau$ is $\omega'$-pointed. Hence $\beta_h \frown_{\omega'} \tau \approx_{\omega'} \beta_h \cdot \tau$. By Fact d $\beta_k \cdot \beta_h \cdot \tau$ is not $\omega'$-pointed. Therefore $\beta_k \frown_{\omega'} \beta_h \cdot \tau \approx_{\omega'} \beta_h \cdot \tau$.

**Lemma A.2.** 1. Let $\beta \triangleright \omega$ be defined and $\omega' = \beta \triangleright \omega$. Let $\tau, \tau'$ be such that $\tau'$ is $(\omega \cdot \beta \cdot \tau)$-pointed. Then

$$ (\beta \cdot \tau) \frown_{\omega} \tau' = \beta \frown_{\omega} (\tau \frown_{\omega'} \tau') $$

2. Let $\beta \triangleright \omega$ be defined and $\omega' = \beta \triangleright \omega$. Let $\tau, \tau'$ be such that $\tau'$ is $(\omega' \cdot \beta \cdot \tau)$-pointed. Then

$$ (\beta \cdot \tau) \frown_{\omega'} \tau' = \beta \frown_{\omega'} (\tau \frown_{\omega} \tau') $$

**Proof:** (1) We show $(\beta \cdot \tau) \frown_{\omega} \tau' = \beta \frown_{\omega} (\tau \frown_{\omega'} \tau')$ by induction on $\tau$.

Case $\tau = \epsilon$. In this case both the LHS and RHS reduce to $\beta \frown_{\omega} \tau'$, for whatever $\omega$.

Case $\tau = \tau'' \cdot \beta'$. By Definition 7.13 we obtain for the LHS:

$$ (\beta \cdot \tau'' \cdot \beta') \frown_{\omega} \tau' = \begin{cases} (\beta \cdot \tau'') \frown_{\omega} (\beta' \cdot \tau') & \text{if } \beta' \cdot \tau' \text{ is } (\omega \cdot \beta \cdot \tau'')\text{-pointed} \\ (\beta \cdot \tau'') \frown_{\omega} \tau' & \text{otherwise} \end{cases} $$

By Definition 7.13 (applied to the internal filtering) we obtain for the RHS:

$$ \beta \frown_{\omega} ((\tau'' \cdot \beta') \frown_{\omega'} \tau') = \begin{cases} \beta \frown_{\omega} (\tau'' \frown_{\omega'} (\beta' \cdot \tau')) & \text{if } \beta' \cdot \tau' \text{ is } (\omega' \cdot \tau'')\text{-pointed} \\ \beta \frown_{\omega} (\tau'' \frown_{\omega'} \tau') & \text{otherwise} \end{cases} $$

We distinguish two cases, according to whether $\beta$ is an input or an output.

Suppose first that $\beta$ is an output. Then $\omega' = \omega \cdot \beta$. The side condition, i.e. the requirement that $\beta' \cdot \tau'$ be $(\omega' \cdot \tau'')$-pointed, is the same in both cases. We may then immediately conclude that LHS = RHS using the induction hypothesis.
Suppose now that $\beta$ is an input. Then $\omega = \bar{\beta} \cdot \omega'$. Observe that, since $(\omega' \cdot \tau'')$ is obtained from $(\omega \cdot \beta \cdot \tau'') = (\bar{\beta} \cdot \omega' \cdot \beta \cdot \tau'')$ by erasing a pair of matching communications, $(\beta' \cdot \tau')$ is $(\omega' \cdot \tau'')$-pointed if and only if $(\beta' \cdot \tau')$ is $(\omega \cdot \beta \cdot \tau'')$-pointed. Then we may again conclude by induction.
(2) follows from (1) since $\beta \triangleright (\beta \triangleright \omega) = \omega$.

**Lemma A.3.** 1. If $\tau \neq \epsilon$ and $\beta \triangleright \omega$ is defined, then $\beta \bullet \text{ev}(\omega, \beta \cdot \tau) = \text{ev}(\beta \triangleright \omega, \tau)$.
2. If $\beta \triangleright \omega$ is defined, then $\beta \circ \text{ev}(\omega, \tau) = \text{ev}(\beta \triangleright \omega, \beta \cdot \tau)$.

**Proof:** Definition 7.14 and Lemmas A.1 and A.2 with $\tau' = \epsilon$ imply (1) and (2) since:

$$
\begin{align*}
(1) \quad \beta \bullet \text{ev}(\omega, \beta \cdot \tau) &= \beta \bullet [\omega, (\beta \cdot \tau)[_{\omega} \epsilon]_{\sim} \quad \text{by Definition 7.14} \\
&= \beta \bullet [\omega, \beta[_{\omega} (\tau[_{\omega'} \epsilon)]_{\sim} \quad \text{by Lemma A.2(1)} \\
&= [\omega', \tau[_{\omega'} \epsilon]_{\sim} \quad \text{by Lemma A.1(1)} \\
\text{ev}(\omega', \tau) &= [\omega', \tau[_{\omega'} \epsilon]_{\sim} \quad \text{by Definition 7.14} \\
& \qquad \text{where } \omega' = \beta \triangleright \omega \\
(2) \quad \beta \circ \text{ev}(\omega, \tau) &= \beta \circ [\omega, \tau[_{\omega} \epsilon]_{\sim} \quad \text{by Definition 7.14} \\
&= [\omega', \beta[_{\omega'} (\tau[_{\omega} \epsilon)]_{\sim} \quad \text{by Lemma A.1(2)} \\
&= [\omega', (\beta \cdot \tau)[_{\omega'} \epsilon]_{\sim} \quad \text{by Lemma A.2(2)} \\
\text{ev}(\omega', \beta \cdot \tau) &= [\omega', (\beta \cdot \tau)[_{\omega'} \epsilon]_{\sim} \quad \text{by Definition 7.14} \\
& \qquad \text{where } \omega' = \beta \triangleright \omega
\end{align*}
$$

**Lemma 8.16** 1. If $\delta_1 < \delta_2$ and both $\beta \circ \delta_1, \beta \circ \delta_2$ are defined, then $\beta \circ \delta_1 < \beta \circ \delta_2$.

2. If $\delta_1 < \delta_2$ and $\beta \circ \delta_1$ is defined, then $\beta \circ \delta_1 < \beta \circ \delta_2$.

3. If $\delta_1 \# \delta_2$ and both $\beta \circ \delta_1, \beta \circ \delta_2$ are defined, then $\beta \circ \delta_1 \# \beta \circ \delta_2$.

**Proof:** (1) Let $\delta_1 = [\omega, \tau]_{\sim}$ and $\delta_2 = [\omega, \tau \cdot \tau']_{\sim}$. If $\beta \circ \delta_1 = [\omega', \tau]_{\sim}$ and $\beta \circ \delta_2 = [\omega', \tau \cdot \tau']_{\sim}$ for some $\omega'$, then $\beta \circ \delta_1 < \beta \circ \delta_2$.

Let $\beta$ be an output. If $\tau \approx_{\omega} \beta \cdot \tau_1$ with $\tau_1 \neq \epsilon$, then $\beta \circ \delta_1 = [\omega \cdot \beta, \tau_1]_{\sim}$ and $\beta \circ \delta_2 = [\omega \cdot \beta, \tau_1 \cdot \tau']_{\sim}$. Therefore $\beta \circ \delta_1 < \beta \circ \delta_2$. Let play($\beta$) $\not\subseteq$ play($\tau$) and $\tau \cdot \tau' \approx_{\omega} \beta \cdot \tau_2$ with $\tau_2 \neq \epsilon$. This implies $\beta \cdot \tau_2 \approx_{\omega} \beta \cdot \tau \cdot \tau'_2$ for some $\tau'_2$. It follows that $\tau_2 \approx_{\omega, \beta} \tau \cdot \tau'_2$. Then we get $\beta \circ \delta_1 = [\omega \cdot \beta, \tau]_{\sim}$ and $\beta \circ \delta_2 = [\omega \cdot \beta, \tau_2]_{\sim} = [\omega \cdot \beta, \tau \cdot \tau'_2]_{\sim}$, which imply $\beta \circ \delta_1 < \beta \circ \delta_2$.
Let $\beta$ be an input. The proof is similar.

(2) Since $\delta_1 < \delta_2$ and $\beta \circ \delta_1$ is defined, then also $\beta \circ \delta_2$ is defined. Let $\delta_1 = [\omega, \tau]_{\sim}$ and $\delta_2 = [\omega, \tau \cdot \tau']_{\sim}$. If $\beta \circ \delta_1 = [\omega', \tau]_{\sim}$ and $\beta \circ \delta_2 = [\omega', \tau \cdot \tau']_{\sim}$ for some $\omega'$, then $\beta \circ \delta_1 < \beta \circ \delta_2$. Let $\beta$ be an output. Then $\omega \cong \omega' \cdot \beta$. If $\beta \circ \delta_1 = [\omega', \beta \cdot \tau]_{\sim}$, then it must be $\beta \circ \delta_2 = [\omega', \beta \cdot \tau \cdot \tau']_{\sim}$. Thus $\beta \circ \delta_1 < \beta \circ \delta_2$. The only other case is $\beta \circ \delta_1 = [\omega', \tau]_{\sim}$ and $\beta \circ \delta_2 = [\omega', \beta \cdot \tau \cdot \tau']_{\sim}$. Since $\beta \circ \delta_1 = [\omega', \tau]_{\sim}$, the trace $\beta \cdot \tau$ is not $\omega'$-pointed, so play($\beta$) $\not\subseteq$ play($\tau$) and $\tau$ does not contain the matching input of $\beta$. Therefore $\beta \cdot \tau \cdot \tau' \approx_{\omega'} \tau \cdot \beta \cdot \tau'$ and $\beta \circ \delta_2 = [\omega', \beta \cdot \tau \cdot \tau']_{\sim} = [\omega', \tau \cdot \beta \cdot \tau']_{\sim}$, so $\beta \circ \delta_1 < \beta \circ \delta_2$.

Let $\beta$ be an input. If $\beta \circ \delta_1 = [\bar{\beta} \cdot \omega, \beta \cdot \tau]_{\sim}$, then it must be $\beta \circ \delta_2 = [\bar{\beta} \cdot \omega, \beta \cdot \tau \cdot \tau']_{\sim}$. We get $\beta \circ \delta_1 < \beta \circ \delta_2$. The only other case is $\beta \circ \delta_1 = [\bar{\beta} \cdot \omega, \tau]_{\sim}$ and $\beta \circ \delta_2 = [\bar{\beta} \cdot \omega, \beta \cdot \tau \cdot \tau']_{\sim}$. If
$\beta \circ \delta_1 = [\bar{\beta} \cdot \omega, \tau]_{\sim}$, then play$(\beta) \not\subseteq$ play$(\tau)$. Therefore $\beta \cdot \tau \cdot \tau' \approx_{\bar{\beta} \cdot \omega} \tau \cdot \beta \cdot \tau'$ and $\beta \circ \delta_2 = [\bar{\beta} \cdot \omega, \beta \cdot \tau \cdot \tau']_{\sim} = [\bar{\beta} \cdot \omega, \tau \cdot \beta \cdot \tau']_{\sim}$, so $\beta \circ \delta_1 < \beta \circ \delta_2$.

(3) Let $\delta_1 = [\omega, \tau]_{\sim}$ and $\delta_2 = [\omega, \tau']_{\sim}$ and $\tau \@ p \# \tau' \@ p$. We select some interesting cases. Note first that $\tau \@ p \# \tau' \@ p$ implies $p \in \text{play}(\tau) \cap \text{play}(\tau')$.

If $\beta$ is an output, then $\omega \cong \omega' \cdot \beta$. If both $\beta \cdot \tau$ and $\beta \cdot \tau'$ are $\omega'$-pointed or not $\omega'$-pointed, then the result is immediate. If $\beta \cdot \tau$ is $\omega'$-pointed while $\beta \cdot \tau'$ is not $\omega'$-pointed, then play$(\beta) \not\subseteq$ play$(\tau')$. This implies $p \notin$ play$(\beta)$. Similarly, if $\beta$ is an input and play$(\beta) \subseteq$ play$(\tau)$ while play$(\beta) \not\subseteq$ play$(\tau')$, then $p \notin$ play$(\beta)$. In both cases we get $(\beta \cdot \tau) \@ p = \tau \@ p$ and $(\beta \cdot \tau') \@ p = \tau' \@ p$, so we conclude $\beta \circ \delta_1 \# \beta \circ \delta_2$.

**Lemma 8.17** 1. If $\delta \in \mathcal{T}\mathcal{E}(\boxplus_{i \in I} pq!l_i; G_i \parallel \mathcal{M})$ and $pq!l_k \bullet \delta$ is defined, then $pq!l_k \bullet \delta \in \mathcal{T}\mathcal{E}(G_k \parallel \mathcal{M} \cdot \langle p, l_k, q \rangle)$, where $k \in I$.

2. If $\delta \in \mathcal{T}\mathcal{E}(pq?l; G \parallel \langle p, l, q \rangle \cdot \mathcal{M})$ and $pq?l \bullet \delta$ is defined, then $pq?l \bullet \delta \in \mathcal{T}\mathcal{E}(G \parallel \mathcal{M})$.

3. If $\delta \in \mathcal{T}\mathcal{E}(G \parallel \mathcal{M} \cdot \langle p, l, q \rangle)$, then $pq!l \circ \delta \in \mathcal{T}\mathcal{E}(\boxplus_{i \in I} pq!l_i; G_i \parallel \mathcal{M})$, where $l = l_k$ and $G = G_k$ for some $k \in I$.

4. If $\delta \in \mathcal{T}\mathcal{E}(G \parallel \mathcal{M})$, then $pq?l \circ \delta \in \mathcal{T}\mathcal{E}(pq?l; G \parallel \langle p, l, q \rangle \cdot \mathcal{M})$.

**Proof:** (1) By Definition 7.17(1), if $\delta \in \mathcal{T}\mathcal{E}(\boxplus_{i \in I} pq!l_i; G_i \parallel \mathcal{M})$, then $\delta = \text{ev}(\omega, \tau)$, where $\omega = \text{otr}(\mathcal{M})$ and $\tau \in \text{Tr}^+(\boxplus_{i \in I} pq!l_i; G_i)$, which gives $\tau \approx_{\omega} pq!l_h \cdot \tau_h$ with $\tau_h \in \text{Tr}^+(G_h)$ for some $h \in I$. By hypothesis $pq!l_k \bullet \delta$ is defined, which implies $\tau \approx_{\omega} pq!l_k \cdot \tau_k$ and $\tau_k \neq \epsilon$. Then Lemma A.3(1) gives $pq!l_k \bullet \delta = \text{ev}(\omega \cdot pq!l_k, \tau_k)$. We conclude that
$$pq!l_k \bullet \delta \in \mathcal{T}\mathcal{E}(G_k \parallel \mathcal{M} \cdot \langle p, l_k, q \rangle)$$

(2) Similar to the proof of (1).

(3) By Definition 7.17(1), if $\delta \in \mathcal{T}\mathcal{E}(G \parallel \mathcal{M} \cdot \langle p, l, q \rangle)$, then $\delta = \text{ev}(\omega \cdot pq!l, \tau)$, where $\omega = \text{otr}(\mathcal{M})$ and $\tau \in \text{Tr}^+(G)$. By Lemma A.3(2) $pq!l \circ \delta = \text{ev}(\omega, pq!l \cdot \tau)$. Then, again by Definition 7.17(1), $pq!l \circ \delta \in \mathcal{T}\mathcal{E}(\boxplus_{i \in I} pq!l_i; G_i \parallel \mathcal{M})$, where $l = l_k$ and $G = G_k$ for some $k \in I$, since $pq!l_k \cdot \tau \in \text{Tr}^+(\boxplus_{i \in I} pq!l_i; G_i)$.

(4) Similar to the proof of (3).

**Lemma 8.18** Let $G \parallel \mathcal{M} \xrightarrow{\beta} G' \parallel \mathcal{M}'$. Then otr$(\mathcal{M}) \cong \beta \triangleright \text{otr}(\mathcal{M}')$ and

1. if $\delta \in \mathcal{T}\mathcal{E}(G \parallel \mathcal{M})$ and $\beta \cdot \delta$ is defined, then $\beta \cdot \delta \in \mathcal{T}\mathcal{E}(G' \parallel \mathcal{M}')$;

2. if $\delta \in \mathcal{T}\mathcal{E}(G' \parallel \mathcal{M}')$, then $\beta \circ \delta \in \mathcal{T}\mathcal{E}(G \parallel \mathcal{M})$.

**Proof:** Lemma 8.4 and Session Fidelity (Theorem 3.19) imply otr$(\mathcal{M}) \cong \beta \triangleright \text{otr}(\mathcal{M}')$.

(1) By induction on the inference of the transition $G \parallel \mathcal{M} \xrightarrow{\beta} G' \parallel \mathcal{M}'$, see Figure 5.

*Base Cases.* If the applied rule is [EXT-OUT], then $G = \boxplus_{i \in I} pq!l_i; G_i$ and $\beta = pq!l_k$ and $G' = G_k$ and $\mathcal{M}' \equiv \mathcal{M} \cdot \langle p, l_k, q \rangle$ for some $k \in I$. By assumption $\beta \cdot \delta$ is defined. By Lemma 8.17(1) $\beta \cdot \delta \in \mathcal{T}\mathcal{E}(G' \parallel \mathcal{M}')$.
If the applied rule is [EXT-IN], then $G = \text{pq?l}; G'$ and $\beta = \text{pq?l}$ and $M \equiv \langle p, \ell, q \rangle \cdot M'$. By assumption $\beta \bullet \delta$ is defined. By Lemma 8.17(2) $\beta \bullet \delta \in \mathcal{T}\mathcal{E}(G' \parallel M')$.

**Inductive Cases.** If the last applied rule is [ICOMM-OUT], then $G = \coprod_{i \in I} \text{pq!l}_i; G_i$ and $G' = \coprod_{i \in I} \text{pq!l}_i; G'_i$ and $G_i \parallel M \cdot \langle p, \ell_i, q \rangle \xrightarrow{\beta} G'_i \parallel M' \cdot \langle p, \ell_i, q \rangle$ for all $i \in I$ and $p \notin \text{play}(\beta)$. By Definition 7.17(1) $\delta \in \mathcal{T}\mathcal{E}(G \parallel M)$ implies $\delta = \text{ev}(\omega, \tau)$, where $\omega = \text{otr}(M)$ and $\tau \in \text{Tr}^+(G)$. Then $\tau = \text{pq!l}_k \cdot \tau'$ and $\delta = [\omega, \tau_0]_{\sim}$ with $\tau_0 = (\text{pq!l}_k \cdot \tau') \frown \epsilon$ for some $k \in I$ by Definition 7.14. We get either $\tau_0 \approx_{\omega} \text{pq!l}_k \cdot \tau'_0$ or $p \notin \text{play}(\tau_0)$ by Definition 7.13. Then $\text{pq!l}_k \cdot \delta$ is defined unless $\tau_0 \approx_{\omega} \text{pq!l}_k \cdot \tau'_0$ and $\tau'_0 = \epsilon$ by Definition 8.13(1). We consider the two cases. Case $\tau_0 \approx_{\omega} \text{pq!l}_k \cdot \tau'_0$ and $\tau'_0 = \epsilon$. We get $\beta \bullet \delta = [\beta \bullet \omega, \text{pq!l}_k]_{\sim}$ since $\text{play}(\beta) \cap \text{play}(\text{pq!l}_k) = \emptyset$, which implies $\beta \bullet \delta \in \mathcal{T}\mathcal{E}(G' \parallel M')$ by Definition 7.17(1).

Case $\tau_0 \approx_{\omega} \text{pq!l}_k \cdot \tau'_0$ and $\tau'_0 \neq \epsilon$ or $p \notin \text{play}(\tau_0)$. Let $\delta' = \text{pq!l}_k \cdot \delta$. By Lemma 8.17(1) $\delta' \in \mathcal{T}\mathcal{E}(G_k \parallel M \cdot \langle p, \ell_k, q \rangle)$. By assumption $\beta \bullet \delta$ is defined. We first show that $\beta \bullet \delta'$ is defined. Since $\beta \bullet \delta$ and $\text{pq!l}_k \cdot \delta$ are defined, by Definition 8.13(1) we have four cases:

(a) $\tau_0 \approx_{\omega} \beta \cdot \tau_1$ for some $\tau_1$ and $\tau_0 \approx_{\omega} \text{pq!l}_k \cdot \tau'_0$;

(b) $\tau_0 \approx_{\omega} \beta \cdot \tau_1$ and $p \notin \text{play}(\tau_0)$;

(c) $\text{play}(\beta) \cap \text{play}(\tau_0) = \emptyset$ and $\tau_0 \approx_{\omega} \text{pq!l}_k \cdot \tau'_0$;

(d) $\text{play}(\beta) \cap \text{play}(\tau_0) = \emptyset$ and $p \notin \text{play}(\tau_0)$.

Let $\omega' = \text{pq!l}_k \bullet \omega = \omega \cdot \text{pq!l}_k$ and $\omega'' = \beta \bullet \omega'$.

In Case a we have $\tau_0 \approx_{\omega} \beta \cdot \text{pq!l}_k \cdot \tau'_1 \approx_{\omega} \text{pq!l}_k \cdot \beta \cdot \tau'_1$ for some $\tau'_1$. Let $\tau_2 = \beta \cdot \tau'_1$. Then $\delta = [\omega, \text{pq!l}_k \cdot \tau_2]_{\sim}$ and therefore $\delta' = [\omega', \tau_2]_{\sim} = [\omega', \beta \cdot \tau'_1]_{\sim}$. Hence $\beta \bullet \delta' = [\omega'', \tau'_1]_{\sim}$.

In Case b we have $\delta = [\omega, \beta \cdot \tau_1]_{\sim}$ and $p \notin \text{play}(\beta \cdot \tau_1)$. Therefore $\delta' = [\omega', \beta \cdot \tau_1]_{\sim}$. Hence $\beta \bullet \delta' = [\omega'', \tau_1]_{\sim}$.

In Case c we have $\delta' = [\omega', \tau'_0]_{\sim}$ and $\beta \bullet \delta' = [\omega'', \tau'_0]_{\sim}$ since $\text{play}(\beta) \cap \text{play}(\tau_0) = \emptyset$ implies $\text{play}(\beta) \cap \text{play}(\tau'_0) = \emptyset$.

In Case d we have $\delta' = [\omega', \tau_0]_{\sim}$ and $\beta \bullet \delta' = [\omega'', \tau_0]_{\sim}$.

So in all cases we conclude that $\beta \bullet \delta'$ is defined.

By induction $\beta \bullet \delta' \in \mathcal{T}\mathcal{E}(G'_k \parallel M' \cdot \langle p, \ell, q \rangle)$. By Lemma 8.17(3) $\text{pq!l}_k \circ (\beta \bullet \delta') \in \mathcal{T}\mathcal{E}(G' \parallel M')$. Since $\delta'$ is defined, Lemma 8.15(1) implies $\text{pq!l}_k \circ \delta' = \delta$. Since $\beta \bullet \delta'$ and $\beta \circ (\text{pq!l}_k \circ \delta')$ are defined and $p \notin \text{play}(\beta)$, by Lemma 8.15(3) we get $\text{pq!l}_k \circ (\beta \bullet \delta') = \beta \circ (\text{pq!l}_k \circ \delta') = \beta \bullet \delta$. We conclude that $\beta \bullet \delta \in \mathcal{T}\mathcal{E}(G' \parallel M')$.

If the last applied rule is [ICOMM-IN] the proof is similar.

(2) By induction on the inference of the transition $G \parallel M \xrightarrow{\beta} G' \parallel M'$, see Figure 5.

**Base Cases.** If the applied rule is [EXT-OUT], then $G = \coprod_{i \in I} \text{pq!l}_i; G_i$ and $\beta = \text{pq!l}_k$ and $G' = G_k$ and $M' \equiv M \cdot \langle p, \ell_k, q \rangle$ for some $k \in I$. By Lemma 8.17(3) $\beta \circ \delta \in \mathcal{T}\mathcal{E}(G \parallel M)$.
If the applied rule is [EXT-IN], then $G = \text{pq?l}; G'$ and $\beta = \text{pq?l}$ and $M \equiv \langle p, \ell, q \rangle \cdot M'$. By Lemma 8.17(4) $\beta \circ \delta \in \mathcal{T}\mathcal{E}(G \parallel M)$.

**Inductive Cases.** If the last applied rule is [ICOMM-OUT], then $G = \coprod_{i \in I} \text{pq!l}_i; G_i$ and $G' = \coprod_{i \in I} \text{pq!l}_i; G'_i$ and $G_i \parallel M \cdot \langle p, \ell_i, q \rangle \xrightarrow{\beta} G'_i \parallel M' \cdot \langle p, \ell_i, q \rangle$ for all $i \in I$ and $p \notin \text{play}(\beta)$. By Definition 7.17(1) $\delta \in \mathcal{T}\mathcal{E}(G' \parallel M')$ implies $\delta = \text{ev}(\omega, \tau)$, where $\omega = \text{otr}(M')$ and $\tau \in \text{Tr}^+(G')$. Then $\tau = \text{pq!l}_k \cdot \tau'$ and $\delta = [\omega, \tau_0]_{\sim}$ with $\tau_0 = (\text{pq!l}_k \cdot \tau') \frown \epsilon$ for some $k \in I$ by Definition 7.14. We get either $\tau_0 \approx_{\omega} \text{pq!l}_k \cdot \tau'_0$ or $p \notin \text{play}(\tau_0)$ by Definition 7.13. Then $\text{pq!l}_k \cdot \delta$ is defined unless $\tau_0 \approx_{\omega} \text{pq!l}_k \cdot \tau'_0$ and $\tau'_0 = \epsilon$ by Definition 8.13(1). We consider the two cases.
Case $\tau_0 \approx_{\omega} \text{pq!}\ell_k \cdot \tau'_0$ and $\tau'_0 = \epsilon$. We get $\beta \circ \delta = [\beta \triangleright \omega, \text{pq!}\ell_k]_{\sim}$ since $p \notin \text{play}(\beta)$, which implies $\beta \circ \delta \in \mathcal{T}\mathcal{E}(G \parallel \mathcal{M})$ by Definition 7.17(1).

Case $\tau_0 \approx_{\omega} \text{pq!}\ell_k \cdot \tau'_0$ and $\tau'_0 \neq \epsilon$ or $p \notin \text{play}(\tau_0)$. Let $\delta' = \text{pq!}\ell_k \bullet \delta$. By Lemma 8.17(1) $\delta' \in \mathcal{T}\mathcal{E}(G'_k \parallel M' \cdot \langle p, \ell_k, q \rangle)$. By induction $\beta \circ \delta' \in \mathcal{T}\mathcal{E}(G_k \parallel M \cdot \langle p, \ell_k, q \rangle)$. Since $\delta'$ is defined, Lemma 8.15(1) implies $\text{pq!}\ell_k \circ \delta' = \delta$. Since $\beta \circ \delta'$ and $\text{pq!}\ell_k \circ \delta'$ are defined, by Lemma 8.15(4) and $p \notin \text{play}(\beta)$ we get $\text{pq!}\ell_k \circ (\beta \circ \delta') = \beta \circ (\text{pq!}\ell_k \circ \delta') = \beta \circ \delta$. By Lemma 8.17(3) $\text{pq!}\ell_k \circ (\beta \circ \delta') \in \mathcal{T}\mathcal{E}(G \parallel \mathcal{M})$. We conclude that $\beta \circ \delta \in \mathcal{T}\mathcal{E}(G \parallel \mathcal{M})$.
If the last applied rule is [ICOMM-IN] the proof is similar.

**Lemma 8.21** Let $\tau \neq \epsilon$ be $\omega$-well formed and $\text{tec}(\omega, \tau) = \delta_1; \dots; \delta_n$.

1. If $1 \le k, l \le n$, then $\neg(\delta_k \# \delta_l)$;

2. $\tau[i] = i/\omega(\delta_i)$ for all $i, 1 \le i \le n$.

**Proof:** (1) Let $\delta_i = [\omega, \tau_i]_{\sim}$ for all $i, 1 \le i \le n$. By Definitions 8.19 and 7.14 $\tau_i = \tau[1 \dots i]_{[\omega \ \epsilon]}$. By Definition 7.13 if $\tau_i @ p \neq \epsilon$, then there are $k_i \le i$ and $\tau'_i$ such that $\text{play}(\tau[k_i]) = \{p\}$, $p \notin \text{play}(\tau'_i)$ and $\tau_i = \tau[1 \dots k_i - 1]_{[\omega \ \tau[k_i] \cdot \tau'_i]}$. By the same definition all $\tau[j]$ with $j \le k_i$ and $\text{play}(\tau[j]) = \{p\}$ occur in $\tau_i$, in the same order as in $\tau$. Theferore $\tau_i @ p$ is a prefix of $\tau @ p$ for all $p$ and all $i, 1 \le i \le n$. This implies that $\tau_h @ p$ cannot be in conflict with $\tau_l @ p$ for any $p$ and any $h, l, 1 \le h, l \le n$.

(2) Immediate from Definitions 8.19, 7.14 and Lemma 7.15.

**Lemma 8.22** If $G \parallel \mathcal{M} \xrightarrow{\tau} G' \parallel \mathcal{M}'$ and $\omega = \text{otr}(\mathcal{M})$, then $\tau$ is $\omega$-well formed.

**Proof:** The proof is by induction on $\tau$.

Case $\tau = \beta$. If $\beta = \text{pq!}\ell$, then the result is immediate.

If $\beta = \text{pq?}\ell$, then from $G \parallel \mathcal{M} \xrightarrow{\beta} G' \parallel \mathcal{M}'$ we get $\mathcal{M} \equiv \langle p, \ell, q \rangle \cdot \mathcal{M}'$ by Lemma 3.13(2), which implies $\omega \cong \text{pq!}\ell \cdot \omega'$. Then the trace $\omega \cdot \beta = \text{pq!}\ell \cdot \omega' \cdot \text{pq?}\ell$ is well formed, since $\text{pq?}\ell$ is the first input of $q$ from $p$ and $\text{pq!}\ell$ is the first output of $p$ to $q$, and therefore $1 \propto \omega \cdot \beta |\omega| + 1$. Hence $\beta$ is $\omega$-well formed.

Case $\tau = \beta \cdot \tau'$ with $\tau' \neq \epsilon$. Let $G \parallel \mathcal{M} \xrightarrow{\beta} G'' \parallel \mathcal{M}'' \xrightarrow{\tau'} G' \parallel \mathcal{M}'$ and $\omega' = \text{otr}(\mathcal{M}'')$. By induction $\tau'$ is $\omega$'-well formed. If $\beta = \text{pq!}\ell$, then from $G \parallel \mathcal{M} \xrightarrow{\beta} G'' \parallel \mathcal{M}''$ we get $\mathcal{M}'' = \mathcal{M} \cdot \langle p, \ell, q \rangle$ by Lemma 3.13(1). Therefore $\text{otr}(\mathcal{M}'') = \omega \cdot \beta = \omega'$. Since $\tau'$ is $(\omega \cdot \beta)$-well formed, i.e. $\omega \cdot \beta \cdot \tau'$ is well formed, we may conclude that $\tau = \beta \cdot \tau'$ is $\omega$-well formed. If $\beta = \text{pq?}\ell$, as in the base case we get $\mathcal{M} \equiv \langle p, \ell, q \rangle \cdot \mathcal{M}''$ by Lemma 3.13(2), and thus $\omega = \text{pq!}\ell \cdot \omega'$. We know that $\tau'$ is $\omega$'-well formed, i.e. $\omega' \cdot \tau'$ is well formed. Therefore we have that $\text{pq!}\ell \cdot \omega' \cdot \text{pq?}\ell \cdot \tau'$ is well formed, since $1 \propto \omega \cdot \tau |\omega| + 1$, and we may conclude that $\tau$ is $\omega$-well formed.

**Lemma 8.23** 1. Let $\tau = \beta \cdot \tau'$ and $\omega' = \beta \triangleright \omega$. If $\text{tec}(\omega, \tau) = \delta_1; \dots; \delta_n$ and $\text{tec}(\omega', \tau') = \delta'_2; \dots; \delta'_n$, then $\beta \bullet \delta_i = \delta'_i$ for all $i, 2 \le i \le n$.
2. Let $\tau = \beta \cdot \tau'$ and $\omega = \beta \triangleright \omega'$. If $tec(\omega, \tau) = \delta_1; \dots; \delta_n$ and $tec(\omega', \tau') = \delta'_2; \dots; \delta'_n$, then $\beta \circ \delta'_i = \delta_i$ for all $i, 2 \le i \le n$.

**Proof:** The proof is by induction on $\tau$.

(1) By Definition 8.19 $\delta_i = ev(\omega, \beta \cdot \tau'[1 \dots i])$ and $\delta'_i = ev(\omega', \tau'[1 \dots i])$ for all $i, 2 \le i \le n$. Then by Lemma A.3(1) $\beta \circ \delta'_i = \delta_i$ for all $i, 2 \le i \le n$.

(2) By Point (1) and Lemma A.3(2).

## Glossary of symbols

*symbol meaning*

*$\beta$* input/output communication $pq!\ell, pq?\ell$

*$\delta$* type event

*$\epsilon$* empty trace

*$\zeta$* sequence of input/output actions

*$\eta$* process event (nonempty sequence of input/output actions)

*$\vartheta$* sequence of undirected actions $!\ell, ?\ell$

*$\pi$* input/output action $p!\ell, p?\ell$

*$\rho$* network event

*$\tau$* trace (sequence of input/output communications)

*$\chi$* sequence of output actions

*$\omega$* sequence of output communications