{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}}}{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\
{\upharpoonright^{\texttt{c}}}{{\sf r}}\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{\mathtt{end}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}$}}\end{array}\end{array}$
(b) Rules for coinductive projection, Definition 3.4

Figure 3. Projection rules

###### Definition 3.4.

The inductive _projection of a global type onto a participant ${\sf r}$_
(project in Projection/IProject.v) is a partial function
${\small{\\_}{\upharpoonright}{{\sf
r}}:\texttt{g\\_ty}\nrightarrow\texttt{l\\_ty}}$ defined by recursion on
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{\sf
G}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$ whenever
one of the clauses in Figure 3(a) applies and the recursive call is defined;
the coinductive _projection of a global tree onto a participant ${\sf r}$_
(definitions Project and IProj in Projection/CProject.v) is a relation
${\small\\_\ {\upharpoonright^{\texttt{c}}}{{\sf r}}\ \\_:\texttt{rel}\ \
{\texttt{g\\_ty}^{\texttt{c}}}\ \ {\texttt{l\\_ty}^{\texttt{c}}}}$
coinductively defined in Figure 3(b).

In rules [co-proj-end] and [co-proj-cont] we have added explicit conditions on
participants. By factoring in the predicate part_of, Definition 3.4 ensures
(1) that the projection of a global tree on a participant outside the protocol
is
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{\mathtt{end}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$ (rule
[co-proj-end]) and (2) that this discipline is preserved in the continuations
(rule [co-proj-cont]). We see that the clauses for projecting of types and
trees follow the same intuition: projecting a global object onto a sending
(resp. receiving) role gives a sending (resp. receiving) local object,
provided that the local continuations are also projections of the
corresponding global continuations. As expected, the tree projection takes
care explicitly of asynchronicity (rules [co-proj-send-2] and [co-proj-
recv-2]). This is an adaptation to our coinductive setting of the definition
in (Deniélou and Yoshida, 2013, Appendix A.1). Below we give an example to
clarify the meaning of [proj-cont].

###### Example 3.5 (Projection).

About rule [proj-cont], we observe that the type

$\small\begin{array}[]{lll}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{\sf
G}}\color[rgb]{.5,0,.5}{}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{{\sf
Alice}}\to{{\sf
Bob}}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\\{\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}&\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\ell_{1}(\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{nat}}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{{\sf
Bob}}\to{{\sf
Carol}}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\ell(\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{nat}}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}).\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mathtt{end}}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5},\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}&\\\
&\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\ell_{2}(\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{nat}}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}).\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{{\sf
Alice}}\to{{\sf
Carol}}:}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\allowbreak\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\ell(\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{nat}}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}).\allowbreak\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mathtt{end}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}}&\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\\}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}\end{array}$

is not projectable onto Carol, since, after skipping the first interaction
between Alice and Bob, it would not be clear whether Carol should expect a
message from Alice or from Bob. If we take instead

$\small\begin{array}[]{lll}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{\sf
G}}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{{\sf
Alice}}\to{{\sf
Bob}}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\\{\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}&\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\ell_{1}(\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{nat}}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}).\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{{\sf
Bob}}\to{{\sf
Carol}}:}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\ell(\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{nat}}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}).\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mathtt{end}}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5},\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}&\\\
&\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\ell_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{(\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{bool}}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5})}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{.\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{{\sf
Bob}}\to{{\sf
Carol}}:}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\ell(\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{nat}}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}).\definecolor{currbkp}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\mathtt{end}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}\color[rgb]{.5,0,.5}}&\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\\}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\text{},\par\end{array}$

the projection
${\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{\sf
G}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{\upharpoonright}{{{\sf
Carol}}}$ is well defined as the local type
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\sf
L}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{?[{{{\sf
Bob}}}];}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\allowbreak\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\ell(\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{nat}}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}).\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{end}}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$.
Following common practice, we use an option type to encode projection as a
partial function in Coq.

Coinductive projection is more permissive than its inductive counterpart,
since it removes the technical issues related to formally dealing with
(equi)recursion, thus allowing for a smoother development in Coq (Appendix A.3
and (Ghilezan et al., 2019, Definition 3.6 and Remark 3.14)).

If, when reasoning about semantics, coinductive trees are more convenient
objects to work with, we still want to rely on session types for imposing a
typing discipline on the communication. The followng theorem allows us to do
so.

###### Theorem 3.6 (Unravelling preserves projections).

(ic_proj in Projection/Correctness.v.) Given a global type
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{\sf
G}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$, such
that $\texttt{guarded}\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{\sf
G}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$ and
$\texttt{closed}\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{\sf
G}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$, if  (a)
there exists a local type
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\sf
L}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$ such
that
${\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{\sf
G}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{\upharpoonright}{{\sf
r}}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\sf
L}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\ $,  (b)
there exists a global tree
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
such that
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{{\sf
G}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\;\Re\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and,  (c) there exists a local tree
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{{\sf
L^{c}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$ such
that
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\sf
L}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\;\Re\;\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{{\sf
L^{c}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
then
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\
{\upharpoonright^{\texttt{c}}}{{\sf r}}\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{{\sf
L^{c}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$.

This first central result closes the first metatheory square (M.1) of the
diagram in Figure 2. For a sketch of its proof see Appendix A, Theorem A.20.

###  3.3. Projection Environments for Asynchronous Communication

In this subsection, we introduce key concepts for building an asynchronous
operational semantics for MPST. In (Deniélou and Yoshida, 2013) a precise
correspondence is drawn between communicating finite-state automata and MPST.
We do not formalise an explicit syntax for automata, but develop labelled
transition systems for global and local trees with automata in mind.

Consider the following scenario: ${\sf p}$ sends a message to ${\sf q}$ with
label
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{\ell}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and payload of sort S and continues on
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{{\sf
L^{c}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$, and
dually ${\sf q}$ receives from ${\sf p}$ the message, with same label and
payload, and then continues on
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{\definecolor{currbkp}{rgb}{0.33203125,0.41796875,0.18359375}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{{\sf
L^{c}}}\color[rgb]{0.33203125,0.41796875,0.18359375}{}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$.
For ${\sf q}$ to receive the message, it is necessary that ${\sf p}$ has first
sent it. To model this asynchronous behaviour, we use FIFO queues: in the
designated queue $Q({\sf p},{\sf q})$ (empty at first) we enqueue the message
sent from ${\sf p}$, until the message is received by ${\sf q}$ and removed
from the queue. We use one queue for each ordered pair of participants $({\sf
p},{\sf q})$ to store in-transit messages sent from ${\sf p}$ to ${\sf q}$,
and we collect such queues in _queue environments_.

###### Definition 3.7 (Queue environments).

We call _queue environment_ (notation qenv in Local/Semantics.v) any finitely
supported function that maps a pair of participants into a finite sequence
(_queue_) of pairs of labels and sorts.

We define the operations of enqueuing and dequeuing on queue environments:

$\small\begin{array}[]{lll}\texttt{enq}\ Q\ ({\sf p},{\sf q})\
(\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})&=&Q[({\sf
p},{\sf q})\mapsfrom Q({\sf p},{\sf
q})@(\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})]\\\
\texttt{deq}\ Q\ ({\sf p},{\sf q})&=&\texttt{if}\ Q({\sf p},{\sf
q})=(\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})\\#s\\\
&&\texttt{then}\
((\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}),Q[({\sf
p},{\sf q})\mapsfrom s])\ \ \ \texttt{else}\ \texttt{None}\end{array}$

We use $\\#$ as the “cons” constructor for lists and $@$ as the “append”
operation; $f[x\mapsfrom y]$ denotes the updating of a function $f$ in $x$
with $y$, namely $f[x\mapsfrom y]\ x^{\prime}=f\ x^{\prime}$ for all $x\neq
x^{\prime}$ and $f[x\mapsfrom y]\ x=y$. We use option types for partial
functions, with None as the standard returned value where the function is
undefined. In case the sequence $Q({\sf p},{\sf q})$ is empty deq will not
perform any operation on it, but return None; in case the sequence is not
empty it will return both its head and its tail (as a pair). We denote the
empty queue environment by $\epsilon$, namely $\epsilon\ ({\sf p},{\sf
q})=\texttt{None}$ for all $({\sf p},{\sf q})$.

Global trees can represent stages of the execution, where a participant has
already sent a message, but it has not yet been received. We adapt the “queue
projection” from (Deniélou and Yoshida, 2013, Appendix A.1) to our coinductive
setting, to associate global trees to the queue contents of a system.

###### Definition 3.8 (Queue projection).

(Definition qProject in Projection/QProject.v) _Projection on queue
environments of a global tree_ (_queue projection_ for short) is the relation
${\small{\\_}{\upharpoonright^{\texttt{q}}}{\\_}\ :\ \texttt{rel}\ \
{\texttt{g\\_ty}^{\texttt{c}}}\ \ {\texttt{qenv}}}$ coinductively specified
by:

$\small\begin{array}[]{ll}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\DefTirNameOld{\footnotesize[{q-proj-
send}]}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\ooalign{$\dfrac{\forall
i\in
I.{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}{}_{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{i}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}}{\upharpoonright^{\texttt{q}}}{Q}\
\ \ \ \ \ \ \ Q({\sf p},{\sf
q})=\texttt{None}}{\phantom{{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\to{\sf
q}:\\{\ell_{i}({\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}}_{i}).\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{\upharpoonright^{\texttt{q}}}{Q}}}$\cr\raisebox{-2.0pt}{$\dfrac{\phantom{\forall
i\in
I.{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}{}_{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{i}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}}{\upharpoonright^{\texttt{q}}}{Q}\
\ \ \ \ \ \ \ Q({\sf p},{\sf
q})=\texttt{None}}}{{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\to{\sf
q}:\\{\ell_{i}({\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}}_{i}).\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{\upharpoonright^{\texttt{q}}}{Q}}$}}&\ooalign{$\dfrac{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\DefTirNameOld{\footnotesize[{q-proj-
end}]}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{\phantom{{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{\mathtt{end}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{\upharpoonright^{\texttt{q}}}{\epsilon}}}$\cr\raisebox{-2.0pt}{$\dfrac{\phantom{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\DefTirNameOld{\footnotesize[{q-proj-
end}]}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}}{{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{\mathtt{end}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{\upharpoonright^{\texttt{q}}}{\epsilon}}$}}\\\\[11.38109pt]
\lx@intercol\hfil\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\DefTirNameOld{\footnotesize[{q-proj-
recv}]}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\
\ooalign{$\dfrac{{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}{}_{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{j}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}}{\upharpoonright^{\texttt{q}}}{Q}\
\ \ \ \ \ \ \ \texttt{deq}\ Q^{\prime}({\sf p},{\sf
q})=((\ell_{j},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}{}_{j}),Q)}{\phantom{{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\mathrel{\leavevmode\hbox to8.99pt{\vbox
to12.94pt{\pgfpicture\makeatletter\hbox{\hskip 4.49426pt\lower-7.86853pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.15678pt}{-1.24393pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\hbox{{$\scriptstyle\ell_{j}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}}{}{{}}{}{{}} {}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}
}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}} {} }{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{3.89427pt}{-5.26855pt}\pgfsys@lineto{0.29427pt}{-5.26855pt}\pgfsys@lineto{-0.55931pt}{-5.96855pt}\pgfsys@lineto{-2.26648pt}{-4.56856pt}\pgfsys@lineto{-4.29427pt}{-5.26855pt}\pgfsys@lineto{-4.29427pt}{-5.26855pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.09427pt}{-5.26855pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}{\sf
q}:\\{\ell_{i}({\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}}_{i}).\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{\upharpoonright^{\texttt{q}}}{Q^{\prime}}}}$\cr\raisebox{-2.0pt}{$\dfrac{\phantom{{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}{}_{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{j}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}}{\upharpoonright^{\texttt{q}}}{Q}\
\ \ \ \ \ \ \ \texttt{deq}\ Q^{\prime}({\sf p},{\sf
q})=((\ell_{j},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}{}_{j}),Q)}}{{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\mathrel{\leavevmode\hbox to8.99pt{\vbox
to12.94pt{\pgfpicture\makeatletter\hbox{\hskip 4.49426pt\lower-7.86853pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.15678pt}{-1.24393pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\hbox{{$\scriptstyle\ell_{j}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}}{}{{}}{}{{}} {}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}
}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}} {} }{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{3.89427pt}{-5.26855pt}\pgfsys@lineto{0.29427pt}{-5.26855pt}\pgfsys@lineto{-0.55931pt}{-5.96855pt}\pgfsys@lineto{-2.26648pt}{-4.56856pt}\pgfsys@lineto{-4.29427pt}{-5.26855pt}\pgfsys@lineto{-4.29427pt}{-5.26855pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.09427pt}{-5.26855pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}{\sf
q}:\\{\ell_{i}({\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}}_{i}).\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{\upharpoonright^{\texttt{q}}}{Q^{\prime}}}$}}\hfil\lx@intercol\end{array}$

See Appendix A.4 for more details.

Analogously to queue environments, we consider all the local types of the
protocol at once.

###### Definition 3.9 (Local environments).

We call _local environment_ , or simply _environment_ , any finitely supported
function
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
that maps participants into local types.

We are interested in those environments that are defined on the participants
of a global protocol
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and that map each participant ${\sf p}$ to the projection of
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
onto such ${\sf p}$.

###### Definition 3.10 (Environment projection).

(Definition
eProject in Projection/CProject.v.) We say that
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
is an environment projection for
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
notation
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\upharpoonright\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
if it holds that $\forall{\sf p}.\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\
{\upharpoonright^{\texttt{c}}}{{\sf p}}\
(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E\
{\sf p}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})$.

We define the semantics on a set of local types together with queue
environments. We therefore consider the projection of a global tree both on
local environments and on queue environments, together in one shot.

###### Definition 3.11 (One-shot projection).

(Definition
Projection in Projection.v) We say that the pair of a local environment and of
a queue environment
$(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q)$
is a (one-shot) projection for the global tree
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$,
notation
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\upharpoonright\\!\upharpoonright(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q)$
if it holds that:
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\upharpoonright\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\quad\text{and}\quad{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{\upharpoonright^{\texttt{q}}}{Q}$.

###### Example 3.12.

Let us consider the global tree:
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\mathrel{\leavevmode\hbox to8.02pt{\vbox
to11.97pt{\pgfpicture\makeatletter\hbox{\hskip 4.01111pt\lower-7.38329pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.45834pt}{-2.43054pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\hbox{{$\scriptstyle\ell$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}}{}{{}}{}{{}} {}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}
}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}} {} }{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{3.41112pt}{-4.78331pt}\pgfsys@lineto{-0.18889pt}{-4.78331pt}\pgfsys@lineto{-1.04247pt}{-5.4833pt}\pgfsys@lineto{-2.74963pt}{-4.08331pt}\pgfsys@lineto{-3.81111pt}{-4.78331pt}\pgfsys@lineto{-3.81111pt}{-4.78331pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.61111pt}{-4.78331pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}{\sf
q}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\allowbreak\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{\ell(\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
q}\to{\sf
p}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{\ell(\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
q}\to{\sf
p}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\allowbreak\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{\ell(\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}).\dots}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
. Participant ${\sf p}$ has sent a message to ${\sf q}$, ${\sf q}$ will
receive it next (but has not yet) and then the protocol continues indefinitely
with ${\sf q}$ sending a message to ${\sf p}$ after the other. We define
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
such that: $\ \
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E\
{\sf
p}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{?^{\sf
c}[{{\sf
q}}];}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{\ell(\definecolor{currbkp}{rgb}{0.33203125,0.41796875,0.18359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{?^{\sf
c}[{{\sf
q}}];}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{\ell(\definecolor{currbkp}{rgb}{0.33203125,0.41796875,0.18359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}).\dots}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\
\ $ and $\ \
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E\
{\sf
q}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{?^{\sf
c}[{{\sf
p}}];}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{\ell(\definecolor{currbkp}{rgb}{0.33203125,0.41796875,0.18359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{!^{\sf
c}[{{\sf
p}}];}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{\ell(\definecolor{currbkp}{rgb}{0.33203125,0.41796875,0.18359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\allowbreak\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{!^{\sf
c}[{{\sf
p}}];}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{\ell(\definecolor{currbkp}{rgb}{0.33203125,0.41796875,0.18359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}).\dots}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\
$ . We then define $Q$ such that: $\ \ Q({\sf p},{\sf
q})=[(\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})]\
\ $ and $\ \ Q({\sf q},{\sf p})=\texttt{None}$. It is easy to verify that
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\upharpoonright\\!\upharpoonright(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q)$;
observe that the only “message” enqueued in $Q$ is
$(\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})$,
since this is the only one sent, but not yet received (at this stage of the
execution).

###  3.4. Labelled Transition Relations for Tree Types

At the core of the _trace semantics_ for session types lies a labelled
transition system (LTS) defined on trees, with regard to _actions_. The basic
_actions_ (datatype act in Common/Actions.v) of our asynchronous communication
are objects, ranged over by $a$, of the shape either: $!{\sf p}{\sf
q}(\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})$:
send $!$ action, from participant ${\sf p}$ to participant ${\sf q}$, of label
$\ell$ and payload type S, or $?{\sf q}{\sf
p}(\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})$:
receive $?$ action, from participant ${\sf p}$ at participant ${\sf q}$, of
label $\ell$ and payload type S. We define the _subject_ of an action $a$
(definition subject in Common/Actions.v), $\texttt{subj}\ {a}$, as ${\sf p}$
if $a=!{\sf p}{\sf
q}(\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})$
and as ${\sf q}$ if $a=?{\sf q}{\sf
p}(\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})$.333The
representation of actions is directly taken from (Deniélou and Yoshida, 2013),
however we have swapped the order of ${\sf p}$ and ${\sf q}$ in the receive
action, so that the subject of an action always occurs in first position.
Given an action, our types (represented as trees) can perform a reduction
step.

###### Definition 3.13 (LTS for global trees).

(step in Global/Semantics.v) The _labelled transition relation for global
trees_ (_global reduction_ or _global step_ for short) is, for each action
$a$, the relation $\\_\ \xrightarrow{a}\ \\_\ :\ \texttt{rel}\ \
{\texttt{g\\_ty}^{\texttt{c}}}\ \ {\texttt{g\\_ty}^{\texttt{c}}}$ inductively
specified by the following clauses:

$\small\begin{array}[]{c}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\DefTirNameOld{\footnotesize[{g-step-
send}]}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\dfrac{a=!{\sf
p}{\sf
q}(\ell_{j},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}{}_{j})}{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\to{\sf
q}:\\{\ell_{i}({\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}}_{i}).\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\xrightarrow{a}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\mathrel{\leavevmode\hbox to8.99pt{\vbox
to12.94pt{\pgfpicture\makeatletter\hbox{\hskip 4.49426pt\lower-7.86853pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.15678pt}{-1.24393pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\hbox{{$\scriptstyle\ell_{j}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}}{}{{}}{}{{}} {}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}
}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}} {} }{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{3.89427pt}{-5.26855pt}\pgfsys@lineto{0.29427pt}{-5.26855pt}\pgfsys@lineto{-0.55931pt}{-5.96855pt}\pgfsys@lineto{-2.26648pt}{-4.56856pt}\pgfsys@lineto{-4.29427pt}{-5.26855pt}\pgfsys@lineto{-4.29427pt}{-5.26855pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.09427pt}{-5.26855pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}{\sf
q}:\\{\ell_{i}({\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}}_{i}).\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}\\\\[14.22636pt]
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\DefTirNameOld{\footnotesize[{g-step-
recv}]}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\dfrac{a=?{\sf
q}{\sf
p}(\ell_{j},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}{}_{j})}{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\mathrel{\leavevmode\hbox to8.99pt{\vbox
to12.94pt{\pgfpicture\makeatletter\hbox{\hskip 4.49426pt\lower-7.86853pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.15678pt}{-1.24393pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\hbox{{$\scriptstyle\ell_{j}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}}{}{{}}{}{{}} {}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}
}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}} {} }{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{3.89427pt}{-5.26855pt}\pgfsys@lineto{0.29427pt}{-5.26855pt}\pgfsys@lineto{-0.55931pt}{-5.96855pt}\pgfsys@lineto{-2.26648pt}{-4.56856pt}\pgfsys@lineto{-4.29427pt}{-5.26855pt}\pgfsys@lineto{-4.29427pt}{-5.26855pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.09427pt}{-5.26855pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}{\sf
q}:\\{\ell_{i}({\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}}_{i}).\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\xrightarrow{a}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}{}_{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{j}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}}\\\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\DefTirNameOld{\footnotesize[{g-step-
str1}]}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\dfrac{\texttt{subj}\
{a}\neq{\sf p}\quad\texttt{subj}\ {a}\neq{\sf q}\quad\forall i\in
I.\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}{}_{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{i}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}\xrightarrow{a}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}}_{i}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\to{\sf
q}:\\{\ell_{i}({\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}}_{i}).\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\xrightarrow{a}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\to{\sf
q}:\\{\ell_{i}({\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}}_{i}).\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}^{\prime}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}\\\\[5.69054pt]
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\DefTirNameOld{\footnotesize[{g-step-
str2}]}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\dfrac{\texttt{subj}\
{a}\neq{\sf
q}\quad\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}{}_{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{j}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}\xrightarrow{a}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}}_{j}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\quad\forall
i\in
I\backslash\\{j\\}.\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}{}_{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{i}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}}^{\prime}_{i}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\mathrel{\leavevmode\hbox to8.99pt{\vbox
to12.94pt{\pgfpicture\makeatletter\hbox{\hskip 4.49426pt\lower-7.86853pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.15678pt}{-1.24393pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\hbox{{$\scriptstyle\ell_{j}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}}{}{{}}{}{{}} {}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}
}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}} {} }{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{3.89427pt}{-5.26855pt}\pgfsys@lineto{0.29427pt}{-5.26855pt}\pgfsys@lineto{-0.55931pt}{-5.96855pt}\pgfsys@lineto{-2.26648pt}{-4.56856pt}\pgfsys@lineto{-4.29427pt}{-5.26855pt}\pgfsys@lineto{-4.29427pt}{-5.26855pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.09427pt}{-5.26855pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}{\sf
q}:\\{\ell_{i}({\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}}_{i}).\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\xrightarrow{a}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\mathrel{\leavevmode\hbox to8.99pt{\vbox
to12.94pt{\pgfpicture\makeatletter\hbox{\hskip 4.49426pt\lower-7.86853pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.15678pt}{-1.24393pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\hbox{{$\scriptstyle\ell_{j}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}}{}{{}}{}{{}} {}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}
}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}} {} }{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{3.89427pt}{-5.26855pt}\pgfsys@lineto{0.29427pt}{-5.26855pt}\pgfsys@lineto{-0.55931pt}{-5.96855pt}\pgfsys@lineto{-2.26648pt}{-4.56856pt}\pgfsys@lineto{-4.29427pt}{-5.26855pt}\pgfsys@lineto{-4.29427pt}{-5.26855pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.09427pt}{-5.26855pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}{\sf
q}:\\{\ell_{i}({\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}}_{i}).\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}^{\prime}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}\end{array}$

The step relation describes a labelled transition system for global trees with
the following intuition: [g-step-send] _sending base case_ : with the sending
action $!{\sf p}{\sf
q}(\ell_{j},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}{}_{j})$,
a message with label $\ell_{j}$ and payload type
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}{}_{j}$
is sent by ${\sf p}$, but not yet received by ${\sf q}$; [g-step-recv]
_receiving base case_ : with the receiving action $?{\sf q}{\sf
p}(\ell_{j},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}{}_{j})$,
a message with label $\ell_{j}$ and payload type
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}{}_{j}$,
previously sent by ${\sf p}$, is now received by ${\sf q}$; in [g-step-str1],
a step is allowed to be performed under a sending constructor
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\to{\sf
q}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$: each
time that the subject of that action is different from ${\sf p}$ and from
${\sf q}$ and each continuation steps; [g-step-str2] with an action $a$ a step
is allowed to be performed under a receiving constructor: each time that the
subject of that action is different from ${\sf q}$ (${\sf p}$ has already sent
the message and the label $\ell_{j}$ has already been selected), the
continuation corresponding to $\ell_{j}$ steps and others stay as the same.

This semantics allows for some degree of non-determinism. For instance,
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\to{\sf
q}:\\{\ell_{i}({\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}}_{i}).\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$ could
perform a step according to both rules [g-step-send] and [g-step-str1]
(depending on the subject of the action).

Below we define a transition system for environments of local trees, together
with environments of queues.

###### Definition 3.14 (LTS for environments).

(l_step in
Local/Semantics.v) The _labelled transition relation for environments_ (_local
reduction_ or _local step_ for short) is, for each $a$, the relation $\\_\
\xrightarrow{a}\ \\_\ :\ \texttt{rel}\ \ {(\texttt{renv}*\texttt{qenv})}\ \
{(\texttt{renv}*\texttt{qenv})}$ inductively specified by the following
clauses:

$\small\begin{array}[]{c}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\DefTirNameOld{\footnotesize[{l-step-
send}]}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\
\dfrac{a=!{\sf p}{\sf
q}(\ell_{j},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}{}_{j})\quad\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E\
{\sf
p}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{!^{\sf
c}[{{\sf
q}}];\\{\ell_{i}({\definecolor{currbkp}{rgb}{0.33203125,0.41796875,0.18359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}}_{i}).\definecolor{currbkp}{rgb}{0.33203125,0.41796875,0.18359375}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{{\sf
L^{c}}}\color[rgb]{0.33203125,0.41796875,0.18359375}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q)\xrightarrow{a}(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E[{\sf
p}\mapsfrom\definecolor{currbkp}{rgb}{0.33203125,0.41796875,0.18359375}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{{\sf
L^{c}}}\color[rgb]{0.33203125,0.41796875,0.18359375}{}_{j}]}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\texttt{enq}\
Q\ ({\sf p},{\sf q})\
(\ell_{j},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}{}_{j}))}\\\\[14.22636pt]
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\DefTirNameOld{\footnotesize[{l-step-
recv}]}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\
\dfrac{\begin{array}[]{l}a=?{\sf q}{\sf
p}(\ell_{j},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}{}_{j})\\\
\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E\
{\sf
q}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}=\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{?^{\sf
c}[{{\sf
p}}];\\{\ell_{i}({\definecolor{currbkp}{rgb}{0.33203125,0.41796875,0.18359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}}_{i}).\definecolor{currbkp}{rgb}{0.33203125,0.41796875,0.18359375}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{{\sf
L^{c}}}\color[rgb]{0.33203125,0.41796875,0.18359375}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\quad
Q({\sf p},{\sf
q})=(\ell_{j},\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}{}_{j})\\#s\end{array}}{(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q)\xrightarrow{a}(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E[{\sf
q}\mapsfrom\definecolor{currbkp}{rgb}{0.33203125,0.41796875,0.18359375}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{{\sf
L^{c}}}\color[rgb]{0.33203125,0.41796875,0.18359375}{}_{j}]}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q[({\sf
p},{\sf q})\mapsfrom s])}\end{array}$

${\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\to{\sf
q}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{(\ell,\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}$${\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\mathrel{\leavevmode\hbox to7.3pt{\vbox
to11.05pt{\pgfpicture\makeatletter\hbox{\hskip 3.64998pt\lower-4.73746pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.3125pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\hbox{$${$\scriptstyle\ell$}$$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}}{}{{}}{}{{}} {}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}
}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{3.04999pt}{-2.13748pt}\pgfsys@lineto{-0.55002pt}{-2.13748pt}\pgfsys@lineto{-1.4036pt}{-2.83748pt}\pgfsys@lineto{-3.44998pt}{-2.13748pt}\pgfsys@lineto{-3.44998pt}{-2.13748pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.24998pt}{-2.13748pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}{\sf
q}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{(\ell,\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}$${\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}$${\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{!^{\sf
c}[{{\sf
q}}];}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{(\ell,\definecolor{currbkp}{rgb}{0.33203125,0.41796875,0.18359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{{\sf
L^{c}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}$${\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{{\sf
L^{c}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}$$\scriptstyle{!{\sf
p}{\sf
q}(\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(g.1)}$$\scriptstyle{\upharpoonright_{{\sf
p}}}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(p.1)}$$\scriptstyle{?{\sf
q}{\sf
p}(\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(g.2)}$$\scriptstyle{\upharpoonright_{{\sf
p}}}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(p.2)}$$\scriptstyle{\upharpoonright_{{\sf
p}}}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(p.3)}$$\scriptstyle{!{\sf
p}{\sf
q}(\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(l.1)}$
(a) ${\sf p}$ sends

${\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\to{\sf
q}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{(\ell,\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}$${\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\mathrel{\leavevmode\hbox to7.3pt{\vbox
to11.05pt{\pgfpicture\makeatletter\hbox{\hskip 3.64998pt\lower-4.73746pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.3125pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\hbox{$${$\scriptstyle\ell$}$$} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}}{}{{}}{}{{}} {}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}
}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{3.04999pt}{-2.13748pt}\pgfsys@lineto{-0.55002pt}{-2.13748pt}\pgfsys@lineto{-1.4036pt}{-2.83748pt}\pgfsys@lineto{-3.44998pt}{-2.13748pt}\pgfsys@lineto{-3.44998pt}{-2.13748pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.24998pt}{-2.13748pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}{\sf
q}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{(\ell,\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}$${\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}$${\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{?^{\sf
c}[{{\sf
p}}];}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{(\ell,\definecolor{currbkp}{rgb}{0.33203125,0.41796875,0.18359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{\definecolor{currbkp}{rgb}{0.33203125,0.41796875,0.18359375}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{{\sf
L^{c}}}\color[rgb]{0.33203125,0.41796875,0.18359375}{}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}$${\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{\definecolor{currbkp}{rgb}{0.33203125,0.41796875,0.18359375}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{{\sf
L^{c}}}\color[rgb]{0.33203125,0.41796875,0.18359375}{}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}$$\scriptstyle{!{\sf
p}{\sf
q}(\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(g.1)}$$\scriptstyle{\upharpoonright_{{\sf
q}}}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(q.1)}$$\scriptstyle{?{\sf
q}{\sf
p}(\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(g.2)}$$\scriptstyle{\upharpoonright_{{\sf
q}}}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(q.2)}$$\scriptstyle{\upharpoonright_{{\sf
q}}}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(q.3)}$$\scriptstyle{?{\sf
q}{\sf
p}(\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})}$$\scriptstyle{\definecolor[named]{.}{rgb}{1,0,0}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(l.2)}$
(b) ${\sf q}$ receives

Figure 4. Basic send/receive steps for global and local trees

###### Example 3.15 (Basic steps for global and local trees).

Figure 4(a) shows the transitions for a global tree, regulating the sending of
a message from ${\sf p}$ to ${\sf q}$, and the local transition for its
projection on ${\sf p}$. The asynchronicity of our system is witnessed by the
two different steps:
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{(g.1)}$,
for the sending action $!{\sf p}{\sf
q}(\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})$,
and
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{(g.2)}$,
for the receiving one $?{\sf q}{\sf
p}(\ell,\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0})$.
Projecting
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\to{\sf
q}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{(\ell,\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
on ${\sf p}$ (arrow
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{(g.1)}$)
gives us a local tree that performs a sending step
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{(l.1)}$
corresponding to
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{(g.1)}$,
and projection is preserved (arrow
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{(p.2)}$).
However this does not happen for the receiving step
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{(g.2)}$:
here the projections on ${\sf p}$ of
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
p}\mathrel{\leavevmode\hbox to8.02pt{\vbox
to11.97pt{\pgfpicture\makeatletter\hbox{\hskip 4.01111pt\lower-7.38329pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.45834pt}{-2.43054pt}\pgfsys@invoke{
}\hbox{{\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}\pgfsys@color@rgb@stroke{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0.00390625}{0.47265625}{0.43359375}\pgfsys@invoke{
}\hbox{{$\scriptstyle\ell$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}}{}{{}}{}{{}} {}{} {}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}
}{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {} }{{{{}{}{{}}
}}{{}} {} }{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}}{{}}}
{}{}{}{}{{}}\pgfsys@moveto{3.41112pt}{-4.78331pt}\pgfsys@lineto{-0.18889pt}{-4.78331pt}\pgfsys@lineto{-1.04247pt}{-5.4833pt}\pgfsys@lineto{-2.74963pt}{-4.08331pt}\pgfsys@lineto{-3.81111pt}{-4.78331pt}\pgfsys@lineto{-3.81111pt}{-4.78331pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.61111pt}{-4.78331pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{}{}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}{\sf
q}:}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{(\ell,\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}).}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
along
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{(p.2)}$ and
of
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
along
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{(p.3)}$ are
the same. Dually if we consider the projection on the receiving participant
${\sf q}$, Figure 4(b). Here the projections along
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{(q.1)}$ and
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{(q.2)}$,
corresponding to the global tree performing a sending action, result in the
same local tree. We have instead a local step
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{(l.2)}$
preserving the local projections on ${\sf q}$ along
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{(q.2)}$ and
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{(q.3)}$ for
the receiving action along
$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{(g.2)}$.

Figure 4 confirms our intuition: when the global tree performs one step,
_there is one local tree_ (namely, one projection of the global tree) such
that it performs a corresponding step. We have indeed defined semantics for
collections of local trees, as opposed to single local trees. The formal
relation of the small-step reductions with respect to projection is
established with soundness and completeness results (see Appendix A for proof
outlines).

###### Theorem 3.16 (Step Soundness).

(Theorem Project_step in TraceEquiv.v) If
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\xrightarrow{a}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\upharpoonright\\!\upharpoonright(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q)$,
there exist
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
and $Q^{\prime}$ such that
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\upharpoonright\\!\upharpoonright(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q^{\prime})$
and
$(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q)\xrightarrow{a}(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q^{\prime})$.

###### Theorem 3.17 (Step Completeness).

(Theorem
Project_lstep in TraceEquiv.v) If
$(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q)\xrightarrow{a}(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q^{\prime})$
and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\upharpoonright\\!\upharpoonright(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q)$,
there exist
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$
such that
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\upharpoonright\\!\upharpoonright(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q^{\prime})$
and
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\xrightarrow{a}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}$.

###  3.5. Trace Semantics and Trace Equivalence

We finally show trace equivalence for global and local types with our Coq
development of semantics for coinductive trees.

###### Definition 3.18 (Traces).

(Codatatype trace in Action.v), ranged over by $t$, are terms generated
_coinductively_ by $\ \ t\ \ \ ::=\
[]\;\mathbin{\mathbf{|\\!\\!|}}\;{a}\\#{t}\ \ $ where $a$ is any action, as
defined in § 3.4444For traces, we use the same notation as for lists, however
we bear in mind that this definiton is coinductive: it generates possibly
infinite streams..

We associate traces to the execution of global trees and local environments.

###### Definition 3.19 (Admissible traces for a global tree).

We say that a trace is admissible for a global tree if the coinductive
relation $\texttt{tr}^{\texttt{g}}\;{\\_}\;{\\_}$ (definition g_lts in
Global/Semantics.v) holds:

$\dfrac{}{\phantom{\texttt{tr}^{\texttt{g}}\;{[]}\;{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{\mathtt{end}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}}}$
---
$\dfrac{\phantom{}}{\texttt{tr}^{\texttt{g}}\;{[]}\;{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{\mathtt{end}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}}$
$\dfrac{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\xrightarrow{a}{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}\quad\texttt{tr}^{\texttt{g}}\;{t}\;{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}}{\phantom{\texttt{tr}^{\texttt{g}}\;{{a}\\#{t}}\;{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}}}$
---
$\dfrac{\phantom{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\xrightarrow{a}{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}\quad\texttt{tr}^{\texttt{g}}\;{t}\;{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{\definecolor{currbkp}{rgb}{0.00390625,0.47265625,0.43359375}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0.00390625,0.47265625,0.43359375}{}^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}}}{\texttt{tr}^{\texttt{g}}\;{{a}\\#{t}}\;{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}}$

###### Definition 3.20 (Admissible traces for environments).

We say that a trace is admissible for a pair of a local environment and a
queue environment if the coinductive relation
$\texttt{tr}^{\texttt{l}}\;{\\_}\;{\\_}$ (definition l_lts in
Local/Semantics.v) holds:

$\dfrac{\forall{\sf
p}.\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\
{\sf
p}=\texttt{None}}{\phantom{\texttt{tr}^{\texttt{l}}\;{[]}\;{(}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\epsilon)}}$
---
$\dfrac{\phantom{\forall{\sf
p}.\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\
{\sf
p}=\texttt{None}}}{\texttt{tr}^{\texttt{l}}\;{[]}\;{(}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},\epsilon)}$
$\dfrac{(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q)\xrightarrow{a}(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q^{\prime})\quad\texttt{tr}^{\texttt{l}}\;{t}\;{(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q^{\prime})}}{\phantom{\texttt{tr}^{\texttt{l}}\;{{a}\\#{t}}\;{(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q)}}}$
---
$\dfrac{\phantom{(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q)\xrightarrow{a}(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q^{\prime})\quad\texttt{tr}^{\texttt{l}}\;{t}\;{(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E^{\prime}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q^{\prime})}}}{\texttt{tr}^{\texttt{l}}\;{{a}\\#{t}}\;{(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q)}}$

Observe that generally more than one execution trace are admissible for a
global tree or for an environment555 About non-determinism in our semantics,
see Remark A.30, Appendix A..

We can now state the _trace equivalence_ theorem, our final result for
multiparty session types. We sketch an outline of the proof in Appendix A,
Theorem A.38.

###### Theorem 3.21 (Trace equivalence).

(Theorem
TraceEquivalence in TraceEquiv.v.)
If
$\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf
c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\upharpoonright\\!\upharpoonright(\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q)$,
then $\
\texttt{tr}^{\texttt{g}}\;{t}\;{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.00390625,0.47265625,0.43359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.00390625,0.47265625,0.43359375}{{\sf
G}^{\sf c}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}\
$ if and only if $\
\texttt{tr}^{\texttt{l}}\;{t}\;{(}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.33203125,0.41796875,0.18359375}\definecolor[named]{pgfstrokecolor}{rgb}{0.33203125,0.41796875,0.18359375}{E}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0},Q)\
$.

Trace equivalence for global and local types (trees) concludes our
formalisation of the metatheory of multiparty session types: squares (M.1) and
(M.2) of the diagramin Figure 2. In the next section we specify a language for
communicating systems inside Coq and extend extend the trace equivalence
result to well-typed processes.

##  4\. A Certified Process Language

This section defines Zooid, an embedded domain specific language in Coq for
specifying certified multiparty processes. Zooid combines shallow and deep
embedding: on one hand process actions are deeply embedded, represented as an
inductive type; on the other, the exchanged values, and computations applied
to them are a shallow embedding expressed as Gallina terms. The core process
calculus of Zooid is session-typed, where the typing derivation is described
as a Coq inductive predicate. The constructs of Zooid are _smart constructors_
that build both a process, and a proof that this is well-typed with respect to
a given local type. Each process is single threaded and the concurrent
semantics occurs due to the asynchronous nature of the channels.

###  4.1. Core Processes

$\begin{array}[]{l}\begin{array}[]{c}\begin{array}[]{@{}l@{}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\DefTirNameOld{\footnotesize[{p-ty-
end}]\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}}\\\
\dfrac{}{\Gamma\vdash_{\text{{lt}}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}{\texttt{finish}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}:\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathtt{end}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}\end{array}\
\begin{array}[]{@{}l@{}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\DefTirNameOld{\footnotesize[{p-ty-
jump}]\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}}\\\
\dfrac{}{\Gamma\vdash_{\text{{lt}}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}{\texttt{jump}\;\definecolor{currbkp}{rgb}{0.5,0.0,0.0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}:\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}\end{array}\
\begin{array}[]{@{}l@{}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\DefTirNameOld{\footnotesize[{p-ty-
loop}]\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}}\\\
\dfrac{\Gamma\vdash\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.78,0.08,0.52}\definecolor[named]{pgfstrokecolor}{rgb}{0.78,0.08,0.52}{e}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}:\texttt{Proc}\quad\Gamma\vdash_{\text{{lt}}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.78,0.08,0.52}\definecolor[named]{pgfstrokecolor}{rgb}{0.78,0.08,0.52}{e}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}:\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\sf
L}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{\Gamma\vdash_{\text{{lt}}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}{\texttt{loop}\;\definecolor{currbkp}{rgb}{0.5,0.0,0.0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\;\\{\definecolor{currbkp}{rgb}{0.5,0.0,0.0}\color[rgb]{0.78,0.08,0.52}\definecolor[named]{pgfstrokecolor}{rgb}{0.78,0.08,0.52}{e}\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\\}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}:\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mu\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}.\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\sf
L}}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}\end{array}\\\
\begin{array}[]{@{}l@{}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\DefTirNameOld{\footnotesize[{p-ty-
read}]\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}}\\\
\dfrac{\Gamma\vdash\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\texttt{act}_{r}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}:\texttt{unit}\to\llbracket\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\rrbracket\quad\Gamma,x:\llbracket\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\rrbracket\vdash_{\text{{lt}}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.78,0.08,0.52}\definecolor[named]{pgfstrokecolor}{rgb}{0.78,0.08,0.52}{e}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}:\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\sf
L}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{\Gamma\vdash_{\text{{lt}}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}{\texttt{read}\;{\definecolor{currbkp}{rgb}{0.5,0.0,0.0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\texttt{act}_{r}}\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}}\;(x.{\definecolor{currbkp}{rgb}{0.5,0.0,0.0}\color[rgb]{0.78,0.08,0.52}\definecolor[named]{pgfstrokecolor}{rgb}{0.78,0.08,0.52}{e}\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}})}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}:\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\sf
L}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}\end{array}\end{array}\\\\[5.69054pt]
\begin{array}[]{cc}\begin{array}[]{@{}l@{}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\DefTirNameOld{\footnotesize[{p-ty-
write}]\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}}\\\
\dfrac{\Gamma\vdash\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\texttt{act}_{w}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}:\llbracket\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\rrbracket\to\texttt{unit}\quad\Gamma\vdash{\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.78,0.08,0.52}\definecolor[named]{pgfstrokecolor}{rgb}{0.78,0.08,0.52}{e}\color[rgb]{0,0,0}{}_{v}}:\llbracket\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\rrbracket\quad\Gamma\vdash_{\text{{lt}}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.78,0.08,0.52}\definecolor[named]{pgfstrokecolor}{rgb}{0.78,0.08,0.52}{e}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}:\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\sf
L}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}{\Gamma\vdash_{\text{{lt}}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}{\texttt{write}\;{\definecolor{currbkp}{rgb}{0.5,0.0,0.0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\texttt{act}_{w}}\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}}\;{\definecolor{currbkp}{rgb}{0.5,0.0,0.0}\color[rgb]{0.78,0.08,0.52}\definecolor[named]{pgfstrokecolor}{rgb}{0.78,0.08,0.52}{e}\color[rgb]{0.5,0.0,0.0}{}_{v}}\;{\definecolor{currbkp}{rgb}{0.5,0.0,0.0}\color[rgb]{0.78,0.08,0.52}\definecolor[named]{pgfstrokecolor}{rgb}{0.78,0.08,0.52}{e}\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}:\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\sf
L}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}\end{array}\\\
\begin{array}[]{@{}l@{}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\DefTirNameOld{\footnotesize[{p-ty-
send}]\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}}\\\
\dfrac{\Gamma\vdash\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.78,0.08,0.52}\definecolor[named]{pgfstrokecolor}{rgb}{0.78,0.08,0.52}{e}\color[rgb]{0,0,0}{}_{1}:\llbracket\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,0}{}_{j}\rrbracket\quad\Gamma\vdash\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.78,0.08,0.52}\definecolor[named]{pgfstrokecolor}{rgb}{0.78,0.08,0.52}{e}\color[rgb]{0,0,0}{}_{2}:\texttt{Proc}\quad\Gamma\vdash_{\text{{lt}}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.78,0.08,0.52}\definecolor[named]{pgfstrokecolor}{rgb}{0.78,0.08,0.52}{e}\color[rgb]{0,0,0}{}_{2}:\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\sf
L}}\color[rgb]{0,0,0}{}_{j}\quad j\in
I}{\Gamma\vdash_{\text{{lt}}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}{\texttt{send}\;{\sf
p}\;(\ell_{j},\definecolor{currbkp}{rgb}{0.5,0.0,0.0}\color[rgb]{0.78,0.08,0.52}\definecolor[named]{pgfstrokecolor}{rgb}{0.78,0.08,0.52}{e}\color[rgb]{0.5,0.0,0.0}{}_{1}).\;\definecolor{currbkp}{rgb}{0.5,0.0,0.0}\color[rgb]{0.78,0.08,0.52}\definecolor[named]{pgfstrokecolor}{rgb}{0.78,0.08,0.52}{e}\color[rgb]{0.5,0.0,0.0}{}_{2}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}:\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{![{{\sf
p}}];\\{\ell_{i}({\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{\texttt{S}}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}}_{i}).\definecolor{currbkp}{rgb}{0,0,1}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{{\sf
L}}\color[rgb]{0,0,1}{}_{i}\\}_{i\in
I}}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}}\end{array}\\\
\begin{array}[]{@{}l@{}}\definecolor{currbkp}{rgb}{0,0,0}\color[rgb]{0.28125,0.23828125,0.546875}\definecolor[named]{pgfstrokecolor}{rgb}{0.28125,0.23828125,0.546875}{\DefTirNameOld{\footnotesize[{p-ty-
recv}]\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\color[rgb]{0,0,0}}}\\\
\dfrac{\forall i\in