properties ensure that may session always progress, and, in the case of non-
synchronisation, a session can always safely recover.

Our system is expressive enough to capture non-trivial communication protocols
that operate in an unreliable setting. We used the UBSC to describe a basic
implementation of the Paxos consensus algorithm, the standard protocol for
achieving consensus in an asynchronous unreliable setting. Firstly, our
framework subsumes the underlying operation assumptions of the Paxos protocol.
The computation for reaching consensus takes place within a single session,
therefore the communication interaction of a Paxos agent is described as a
single session type. The session typing system ensures that a Paxos agent
interaction follows the Paxos session protocol. The only burden left to the
programmer, to achieve a correct Paxos implementation, is to implement the
Paxos algorithmic logic at each step of the session interaction.

Despite the expressive power of our framework, the syntax of the session types
follows the syntax of standard binary session types. This fact implies a
session type framework that does not increase the complexity needed to
describe protocols, as it is often done in systems that extend session types,
but moves the burden of checking for communication correctness into the type
system.

### Future Work

Our system is open for further extensions in the future. A first direction is
to capture more complicated patterns beyond the unreliable broadcast
communication and the gather communication pattern. We would also like to
investigate more elaborate autonomous recovery mechanisms, e.g. to explicitly
define time-out and interrupt routines.

Another interesting direction is the extension of the system with locations
and mobility, cf. [14], as this would allow the use of session types in a
highly dynamic and complex setting. Location and node mobility is an important
feature which allows for new nodes to be introduced, disabled, or migrate
between locations within a network. Locality and/or mobility might also imply
semantics that take into account broadcast/communication range. The feature of
communication range further strengthens the need for the existence of
autonomous recovery mechanisms.

An important direction for future research is to develop a more robust session
type system, based on multiparty session types, where network agents can
interact with multiple roles inside a session. The research direction on a
multiparty session type framework in the context of unreliable broadcast
communication can follow principles from the work on parametrised multiparty
session types [23], where a session type system is developed for describing
interaction among an arbitrary number of agents.

### Acknowledgements

Kouzapas and Gay are supported by the UK EPSRC project EP/K034413/1 “From Data
Types to Session Types: A Basis for Concurrency and Distribution”. Voinea is
supported by an EPSRC PhD studentship. This research was supported by a Short-
Term Scientific Mission grant from COST Action IC1201 (Behavioural Types for
Reliable Large-Scale Software Systems).

## References

  * [1] Adameit, M., Peters, K., Nestmann, U.: Session types for link failures. In: Bouajjani, A., Silva, A. (eds.) Formal Techniques for Distributed Objects, Components, and Systems. pp. 1–16. Springer International Publishing, Cham (2017)
  * [2] Ancona, D., Bono, V., Bravetti, M., Campos, J., Castagna, G., Deniélou, P.M., Gay, S.J., Gesbert, N., Giachino, E., Hu, R., Johnsen, E.B., Martins, F., Mascardi, V., Montesi, F., Neykova, R., Ng, N., Padovani, L., Vasconcelos, V.T., Yoshida, N.: Behavioral types in programming languages. Foundations and Trends® in Programming Languages 3, 95–230 (2016)
  * [3] Bernardi, G., Dardha, O., Gay, S.J., Kouzapas, D.: On duality relations for session types. In: Maffei, M., Tuosto, E. (eds.) Trustworthy Global Computing. pp. 51–66. Springer Berlin Heidelberg, Berlin, Heidelberg (2014)
  * [4] Borgström, J., Huang, S., Johansson, M., Raabjerg, P., Victor, B., Pohjola, J.Å., Parrow, J.: Broadcast psi-calculi with an application to wireless protocols. In: SEFM 2011. pp. 74–89 (2011)
  * [5] Capecchi, S., Giachino, E., Yoshida, N.: Global escape in multiparty sessions. Mathematical Structures in Computer Science 26 (2 2016)
  * [6] Carbone, M., Honda, K., Yoshida, N.: Structured interactional exceptions in session types. In: CONCUR. LNCS, vol. 5201, pp. 402–417. Springer (2008)
  * [7] Castagna, G., Dezani-Ciancaglini, M., Padovani, L.: On global types and multi-party session. Logical Methods in Computer Science 8(1) (2012)
  * [8] Chandra, T.D., Griesemer, R., Redstone, J.: Paxos made live: an engineering perspective. In: Proceedings of the twenty-sixth annual ACM symposium on Principles of distributed computing. pp. 398–407. ACM (2007)
  * [9] Coppo, M., Dezani-Ciancaglini, M., Yoshida, N., Padovani, L.: Global progress for dynamically interleaved multiparty sessions. Mathematical Structures in Computer Science 26(2), 238–302 (2016)
  * [10] Deniélou, P., Yoshida, N., Bejleri, A., Hu, R.: Parameterised multiparty session types. Logical Methods in Computer Science 8(4) (2012)
  * [11] Dunkels, A., Österlind, F., He, Z.: An adaptive communication architecture for wireless sensor networks. In: Proceedings of Embedded Networked Sensor Systems. pp. 335–349. SenSys ’07, ACM (2007)
  * [12] Gay, S.J., Ravara, A. (eds.): Behavioural Types: from Theory to Tools. River Publishers (2017)
  * [13] Gay, S.J., Vasconcelos, V.T.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19–50 (2010), https://doi.org/10.1017/S0956796809990268
  * [14] Hennessy, M., Riely, J.: Resource access control in systems of mobile agents. Information and Computation 173(1), 82 – 120 (2002)
  * [15] Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: ESOP. pp. 122–138. Springer-Verlag (1998)
  * [16] Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL. pp. 273–284 (2008)
  * [17] Hu, R., Kouzapas, D., Pernet, O., Yoshida, N., Honda, K.: Type-safe eventful sessions in java. In: ECOOP. pp. 329–353 (2010)
  * [18] Kouzapas, D.: A Study of Bisimulation Theory for Session Types. Ph.D. thesis, Imperial College London (2012)
  * [19] Kouzapas, D., Gutkovas, R., Gay, S.J.: Session types for broadcasting. In: PLACES. pp. 25–31 (2014)
  * [20] Kouzapas, D., Yoshida, N., Hu, R., Honda, K.: On asynchronous eventful session semantics. Mathematical Structures in Computer Science 26(2), 303–364 (2016), https://doi.org/10.1017/S096012951400019X
  * [21] Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. 16(2), 133–169 (1998)
  * [22] Lamport, L., et al.: Paxos made simple. ACM Sigact News 32(4), 18–25 (2001)
  * [23] Ng, N., Yoshida, N.: Pabble: parameterised scribble. Service Oriented Computing and Applications 9(3-4), 269–284 (2015)
  * [24] Yoshida, N., Vasconcelos, V.T.: Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication. Electronic Notes in Theoretical Computer Science 171(4), 73 – 93 (2007)

##  Appendix A Proofs

###  A.1. Congruence invariance proof

######  Lemma 8 (Congruence Invariance).

  * •

If $P\equiv P^{\prime}$, then $\Gamma;\Delta\mathrel{\vdash}P$ if, and only
if, $\Gamma;\Delta\mathrel{\vdash}P^{\prime}$.

  * •

If $N\equiv N^{\prime}$, then $\Gamma;\Delta\mathrel{\vdash}N$ if, and only
if, $\Gamma;\Delta\mathrel{\vdash}N^{\prime}$.

######  Proof A.1.

By induction on the structural congruence definition.

######  Lemma 9 (Substitution).

  * •

Whenever $\Gamma\mathrel{\vdash}e:\beta$ and
$\Gamma,x:\beta;\Delta\mathrel{\vdash}P$, then
$\Gamma;\Delta\mathrel{\vdash}P\\{{e}/{x}\\}$.

  * •

Whenever $\Gamma;\Delta,x:T\mathrel{\vdash}P$, then
$\Gamma;\Delta,s:T\mathrel{\vdash}P\\{{s}/{x}\\}$.

######  Proof A.2.

By induction on the definition of processes.

###  A.2. Typing Preservation proof

Now we are ready to prove the typing preservation property of our system.

######  Proof A.3 (Proof of Theorem 3).

By induction on the depth of derivation of
$N\mathrel{\longrightarrow}N^{\prime}$.

  * •

Rule [Conn]

Assume

$\begin{array}[]{l}\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}s\text{
fresh}\end{array}}{\begin{array}[]{l}[\,a_{!}(\breve{x}).P\,|\,B\,]\,\,|\,\,\prod_{i\in
I}[\,a_{?}(x).Q_{i}\,|\,B_{i}\,]\\\
\qquad\mathrel{\longrightarrow}(\nu\,s)([\,P\\{{\breve{s}}/{\breve{x}}\\}\,|\,B\,|\,\breve{s}[0,\varepsilon]\,]\,|\\!|\,\prod_{i\in
I}[\,Q_{i}\\{{s}/{x}\\}\,|\,B_{i}\,|\,s[0,\varepsilon]\,])\end{array}}}\end{array}\end{array}$

and

$\Gamma;\Delta\mathrel{\vdash}[\,a_{!}(\breve{x}).P\,|\,B\,]\,|\\!|\,\prod_{i\in
I}[\,a_{?}(x).Q_{i}\,|\,B_{i}\,]$

with $\Delta$ well-formed. From the latter typing judgement we get the
derivation

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{0},\Delta_{1}\mathrel{\vdash}[\,a_{!}(\breve{x}).P\,|\,B\,]\\\
\Gamma;\Delta_{0},\Delta_{2}\mathrel{\vdash}\prod_{i\in
I}[\,a_{?}(x).Q_{i}\,|\,B_{i}\,]\\\ \text{$\Delta_{0}$ only
$s$-endpoints}\quad\Delta=\Delta_{0},\Delta_{1},\Delta_{2}\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}[\,a_{!}(\breve{x}).P\,|\,B\,]\,|\\!|\,\prod_{i\in
I}[\,a_{?}(x).Q_{i}\,|\,B_{i}\,]\end{array}}}\
\footnotesize\textsc{{[TPar]}}\end{array}$

We continue the above derivation for node $[\,a_{!}(\breve{x}).P\,|\,B\,]$

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\begin{array}[]{ll}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{1}^{\prime\prime},\breve{x}:\overline{T}\mathrel{\vdash}P\quad\Gamma\mathrel{\vdash}a:T\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{1}^{\prime\prime}\mathrel{\vdash}a_{!}(\breve{x}).P\end{array}}}\
\footnotesize\textsc{{[TReq]}}\end{array}\\\
\Gamma;\Theta\mathrel{\vdash}B\quad\Delta_{1}^{\prime}=\Delta_{1}^{\prime\prime}\circ\Theta\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{1}^{\prime}\mathrel{\vdash}[\,a_{!}(s).P\,|\,B\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}&\Delta_{1}^{\prime}\mathrel{\hookrightarrow}\Delta_{0},\Delta_{1}\end{array}\\\\[34.1433pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{1}\mathrel{\vdash}[\,a_{!}(s).P\,|\,B\,]\end{array}}}\
\footnotesize\textsc{{[TSynch]}}\end{array}}$

For every node $[\,a_{?}(x).Q_{i}\,|\,B_{i}\,]$ we can derive

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\begin{array}[]{ll}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{i}^{\prime\prime},x:T\mathrel{\vdash}Q_{i}\quad\Gamma\mathrel{\vdash}a:T\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{i}^{\prime\prime}\mathrel{\vdash}a_{?}(x).Q_{i}\end{array}}}\
\footnotesize\textsc{{[TAcc]}}\end{array}\\\
\Gamma;\Theta_{i}\mathrel{\vdash}B_{i}\quad\Delta_{i}^{\prime}=\Delta_{i}^{\prime\prime}\circ\Theta_{i}\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{i}^{\prime}\mathrel{\vdash}[\,a_{?}(x).Q_{i}\,|\,B_{i}\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}&\Delta_{i}^{\prime}\mathrel{\hookrightarrow}\Delta_{0},\Delta_{i}\end{array}\\\\[34.1433pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{i}\mathrel{\vdash}[\,a_{?}(x).Q_{i}\,|\,B_{i}\,]\end{array}}}\
\footnotesize\textsc{{[TSynch]}}\end{array}}$

and also with multiple applications of the [TPar] rule we get

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\\{\Gamma;\Delta_{0},\Delta_{i}\mathrel{\vdash}[\,a_{?}(x).Q_{i}\,|\,B_{i}\,]\\}_{i\in
I}\quad\Delta_{2}=\bigcup_{i\in
I}\Delta_{i}\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{2}\mathrel{\vdash}\prod_{i\in
I}[\,a_{?}(x).Q_{i}\,|\,B_{i}\,]\end{array}}}\
\footnotesize\textsc{{[TPar]}}\end{array}$

We can then combine the information from the latter transition to derive the
type for the result of the reduction
$(\nu\,s)([\,P\\{{\breve{s}}/{\breve{x}}\\}\,|\,B\,|\,\breve{s}[0,\varepsilon]\,]\,|\\!|\,\prod_{i\in
I}[\,Q_{i}\\{{s}/{x}\\}\,|\,B_{i}\,|\,s[0,\varepsilon]\,])$. We first type
network node
$[\,P\\{{\breve{s}}/{\breve{x}}\\}\,|\,B\,|\,\breve{s}[0,\varepsilon]\,]$:

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\breve{s}:(0,\varepsilon)\mathrel{\vdash}\breve{s}[0,\varepsilon]\quad\footnotesize\textsc{{[SEmp]}}\\\
\Gamma;\Theta\mathrel{\vdash}B\text{ (from former
derivation)}\end{array}}{\begin{array}[]{l}\Gamma;\Theta,\breve{s}:(0,\varepsilon)\mathrel{\vdash}B\,|\,\breve{s}[\varepsilon,\varepsilon]\end{array}}}\
\footnotesize\textsc{{[BPar]}}\end{array}}\\\\[25.60747pt]
\begin{array}[]{l}\text{Substitution Lemma~{}\ref{lem:substitution} and former
derivation}\\\
\Gamma;\Delta_{1}^{\prime\prime},\breve{x}:\overline{T}\mathrel{\vdash}P\text{
imply
}\Gamma;\Delta_{1}^{\prime\prime},\breve{s}:\overline{T}\mathrel{\vdash}P\\{{\breve{s}}/{\breve{x}}\\}\end{array}\\\\[11.38109pt]
\Delta_{1}^{\prime\prime},\breve{s}:\overline{T}\circ\Theta,\breve{s}:(0,\varepsilon)=\Delta_{1}^{\prime},\breve{s}:(0,\overline{T})\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{1}^{\prime},\breve{s}:(0,\overline{T})\mathrel{\vdash}[\,P\\{{\breve{s}}/{\breve{x}}\\}\,|\,B\,|\,\breve{s}[0,\varepsilon]\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}\\\\[62.59605pt]
\begin{array}[]{l}\text{Linear context synchronisation
(Definition~{}\ref{def:synchr}) and former result }\\\
\Delta_{1}^{\prime}\mathrel{\hookrightarrow}\Delta_{0},\Delta_{1}\text{ imply
}\Delta_{1}^{\prime},s:0,\breve{s}:\overline{T}\mathrel{\hookrightarrow}\Delta_{0},\Delta_{1},\breve{s}:(0,\overline{T})\end{array}\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{1},\breve{s}:(0,\overline{T})\mathrel{\vdash}[\,P\\{{\breve{s}}/{\breve{x}}\\}\,|\,B\,|\,\breve{s}[0,\varepsilon]\,]\end{array}}}\
\footnotesize\textsc{{[TSynch]}}\end{array}}$

Similarly we type every network node
$[\,Q_{i}\\{{s}/{x}\\}\,|\,B_{i}\,|\,s[0,\varepsilon]\,]$

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;s:(0,\varepsilon)\mathrel{\vdash}s[0,\varepsilon]\quad\footnotesize\textsc{{[SEmp]}}\\\
\Gamma;\Theta\mathrel{\vdash}B_{i}\text{ (from former
derivation)}\end{array}}{\begin{array}[]{l}\Gamma;\Theta,s:(0,\varepsilon)\mathrel{\vdash}B_{i}\,|\,s[\varepsilon,\varepsilon]\end{array}}}\
\footnotesize\textsc{{[BPar]}}\end{array}}\\\\[25.60747pt]
\begin{array}[]{l}\text{Substitution Lemma~{}\ref{lem:substitution} and former
derivation}\\\ \Gamma;\Delta_{i}^{\prime\prime},x:T\mathrel{\vdash}Q_{i}\text{
imply
}\Gamma;\Delta_{i}^{\prime\prime},s:T\mathrel{\vdash}Q_{i}\\{{s}/{x}\\}\end{array}\\\\[11.38109pt]
\Delta_{i}^{\prime\prime},s:T\circ\Theta,s:(0,\varepsilon)=\Delta_{i}^{\prime}s:(0,T)\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{i}^{\prime},s:(0,T)\mathrel{\vdash}[\,Q_{i}\\{{s}/{x}\\}\,|\,B_{i}\,|\,s[0,\varepsilon]\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}\\\\[62.59605pt]
\begin{array}[]{l}\text{Linear context synchronisation
(Definition~{}\ref{def:synchr}) and former result }\\\
\Delta_{i}^{\prime}\mathrel{\hookrightarrow}\Delta_{0},\Delta_{1}\text{ imply
}\Delta_{i}^{\prime},s:(0,T)\mathrel{\hookrightarrow}\Delta_{0},\Delta_{i},s:(0,T)\end{array}\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{i},s:(0,T)\mathrel{\vdash}[\,Q_{i}\\{{s}/{x}\\}\,|\,B_{i}\,|\,s[0,\varepsilon]\,]\end{array}}}\
\footnotesize\textsc{{[TSynch]}}\end{array}}$

We can now have a multiple application of the [TPar] rule to type network

$\prod_{i\in I}[\,Q_{i}\\{{s}/{x}\\}\,|\,B_{i}\,|\,s[0,\varepsilon]\,]$

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{0},\Delta_{i},s:(0,T)\mathrel{\vdash}[\,Q_{i}\\{{s}/{x}\\}\,|\,B_{i}\,|\,s[0,\varepsilon]\,]\\\
\text{ from former result }\Delta_{2}=\bigcup_{i\in
I}\Delta_{i}\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{2},s:(0,T)\mathrel{\vdash}\prod_{i\in
I}[\,Q_{i}\\{{s}/{x}\\}\,|\,B_{i}\,|\,s[0,\varepsilon]\,]\end{array}}}\
\footnotesize\textsc{{[TPar]}}\end{array}$

We then use typing rule [TPar] followed by rule [TSRes] to type the result of
the reduction
$(\nu\,s)([\,P\\{{\breve{s}}/{\breve{x}}\\}\,|\,B\,|\,\breve{s}[0,\varepsilon]\,]\,|\\!|\,\prod_{i\in
I}[\,Q_{i}\\{{s}/{x}\\}\,|\,B_{i}\,|\,s[0,\varepsilon]\,])$:

$\boxed{\begin{array}[]{l}\footnotesize\textsc{{[TSRes]}}\\\
{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}\footnotesize\textsc{{[TPar]}}\\\
{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{0},\Delta_{1},\breve{s}:(0,\overline{T})\mathrel{\vdash}[\,P\\{{\breve{s}}/{\breve{x}}\\}\,|\,B\,|\,\breve{s}[0,\varepsilon]\,]\\\
\Gamma;\Delta_{0},\Delta_{2},s:(0,T)\mathrel{\vdash}\prod_{i\in
I}[\,Q_{i}\\{{s}/{x}\\}\,|\,B_{i}\,|\,s[0,\varepsilon]\,]\end{array}}{\begin{array}[]{l}\Gamma;\Delta,\breve{s}:(0,\overline{T}),s:(0,T)\mathrel{\vdash}[\,P\\{{\breve{s}}/{\breve{x}}\\}\,|\,B\,|\,\breve{s}[0,\varepsilon]\,]\,|\\!|\,\prod_{i\in
I}[\,Q_{i}\\{{s}/{x}\\}\,|\,B_{i}\,|\,s[0,\varepsilon]\,]\end{array}}}\end{array}}\\\\[34.1433pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}(\nu\,s)([\,P\\{{\breve{s}}/{\breve{x}}\\}\,|\,B\,|\,\breve{s}[0,\varepsilon]\,]\,|\\!|\,\prod_{i\in
I}[\,Q_{i}\\{{s}/{x}\\}\,|\,B_{i}\,|\,s[0,\varepsilon]\,])\end{array}}}\end{array}}$

The last result together with the trivial result
$\Delta\mathrel{\shortrightarrow}\Delta$ concludes the case.

  * •

Rule [Bcast]

Assume

$[\,\breve{s}{}_{!}\langle
e\rangle.P\,|\,B\,|\,\breve{s}[c,\varepsilon]\,]\,|\\!|\,\prod_{i\in
I}[\,P_{i}\,|\,B_{i}\,|\,s[c,\tilde{m}_{i}]\,]\mathrel{\longrightarrow}[\,P\,|\,B\,|\,s[c+1,\varepsilon]\,]\,|\\!|\,\prod_{i\in
I}[\,P_{i}\,|\,B_{i}\,|\,s[c+1,\tilde{m}_{i}\cdot e]\,]$

and

$\Gamma;\Delta\mathrel{\vdash}[\,\breve{s}{}_{!}\langle
e\rangle.P\,|\,B\,|\,\breve{s}[c,\varepsilon]\,]\,|\\!|\,\prod_{i\in
I}[\,P_{i}\,|\,B_{i}\,|\,s[c,\tilde{m}_{i}]\,]$

with $\Delta$ well-formed. We proceed with the typing derivation of the latter
typing judgement.

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\begin{array}[]{l}\text{well-
formed $\Delta$ implies
}\Delta=\Delta_{0},\Delta_{1},\breve{s}:(c,{}_{!}\beta.\overline{T}),\Delta_{2},s:(c,{}_{?}\beta.T)\\\
\text{with $\Delta_{0}$ only $s$-endpoints}\end{array}\\\
\Gamma;\Delta_{0},\Delta_{1},\breve{s}:(c,{}_{!}\beta.\overline{T})\mathrel{\vdash}[\,\breve{s}{}_{!}\langle
e\rangle.P\,|\,B\,|\,\breve{s}[c,\varepsilon]\,]\\\
\Gamma;\Delta_{0},\Delta_{2},s:{}_{?}\beta.T\mathrel{\vdash}\prod_{i\in
I}[\,P_{i}\,|\,B_{i}\,|\,s[c,\tilde{m}_{i}]\,]\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}[\,\breve{s}{}_{!}\langle
e\rangle.P\,|\,B\,|\,\breve{s}[c,\varepsilon]\,]\,|\\!|\,\prod_{i\in
I}[\,P_{i}\,|\,B_{i}\,|\,s[c,\tilde{m}_{i}]\,]\end{array}}}\
\footnotesize\textsc{{[TPar]}}\end{array}$

We continue the above derivation for network node $[\,\breve{s}{}_{!}\langle
e\rangle.P\,|\,B\,|\,\breve{s}[c,\varepsilon]\,]$:

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\breve{s}:(c,\varepsilon)\mathrel{\vdash}\breve{s}[c,\varepsilon]\quad\footnotesize\textsc{{[SEmp]}}\quad\Gamma;\Theta\mathrel{\vdash}B\end{array}}{\begin{array}[]{l}\Gamma;\Theta,\breve{s}:(c,\varepsilon)\mathrel{\vdash}B\,|\,\breve{s}[c,\varepsilon]\end{array}}}\
\footnotesize\textsc{{[BPar]}}\end{array}}\\\\[17.07164pt]
\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{1}^{\prime\prime},\breve{s}:\overline{T}\mathrel{\vdash}P\quad\Gamma\mathrel{\vdash}e:\beta\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{1}^{\prime\prime},\breve{s}:{}_{!}\beta.\overline{T}\mathrel{\vdash}\breve{s}{}_{!}\langle
e\rangle.P\end{array}}}\
\footnotesize\textsc{{[TSnd]}}\end{array}\\\\[11.38109pt]
\Delta_{1}^{\prime},\breve{s}:(c,{}_{!}\beta.\overline{T})=\Delta_{1}^{\prime\prime},\breve{s}:{}_{!}\beta.\overline{T}\circ\Theta,\breve{s}:(c,\varepsilon)\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{1}^{\prime},\breve{s}:(c,{}_{!}\beta.\overline{T})\mathrel{\vdash}[\,\breve{s}{}_{!}\langle
e\rangle.P\,|\,B\,|\,\breve{s}[c,\varepsilon]\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}\\\\[56.9055pt]
\Delta_{1}^{\prime},\breve{s}:(c,{}_{!}\beta.\overline{T})\mathrel{\hookrightarrow}\Delta_{0},\Delta_{1},\breve{s}:(c,{}_{!}\beta.\overline{T})\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{1},\breve{s}:(c,{}_{!}\beta.\overline{T})\mathrel{\vdash}[\,\breve{s}{}_{!}\langle
e\rangle.P\,|\,B\,|\,\breve{s}[c,\varepsilon]\,]\end{array}}}\
\footnotesize\textsc{{[TSynch]}}\end{array}}$

We then derive the typing for network nodes
$[\,P_{i}\,|\,B_{i}\,|\,s[c,\tilde{m}_{i}]\,]$

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}\footnotesize\textsc{{[TNode]}}\\\
{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;s:(c,M)\mathrel{\vdash}s[c,\tilde{m}_{i}]\quad\footnotesize\textsc{{[SExp]}}\quad\Gamma;\Theta_{i}\mathrel{\vdash}B_{i}\end{array}}{\begin{array}[]{l}\Gamma;\Theta_{i},s:(c,M)\mathrel{\vdash}B_{i}\,|\,s[c,\tilde{m}_{i}]\end{array}}}\
\footnotesize\textsc{{[BPar]}}\end{array}}\\\\[17.07164pt]
\Gamma;\Delta_{i}^{\prime\prime},s:T^{\prime}\mathrel{\vdash}P_{i}\quad\Delta_{i}^{\prime},s:(c,{}_{?}\beta.T)=\Delta_{1}^{\prime\prime},s:T^{\prime}\circ\Theta,s:(c,M)\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{i}^{\prime},s:(c,{}_{?}\beta.T)\mathrel{\vdash}[\,P_{i}\,|\,B_{i}\,|\,s[c,\tilde{m}_{i}]\,]\end{array}}}\end{array}}\\\\[45.5244pt]
\Delta_{i}^{\prime},s:(c,{}_{?}\beta.T)\mathrel{\hookrightarrow}\Delta_{0},\Delta_{i},s:(c,{}_{?}\beta.T)\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{i},s:(c,{}_{?}\beta.T)\mathrel{\vdash}[\,P_{i}\,|\,B_{i}\,|\,s[c,\tilde{m}_{i}]\,]\end{array}}}\
\footnotesize\textsc{{[TSynch]}}\end{array}}$

We can now have multiple applications of rule [TPar] to get:

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{0},\Delta_{i},s:(c,{}_{?}\beta.T)\mathrel{\vdash}[\,P_{i}\,|\,B_{i}\,|\,s[c,\tilde{m}_{i}]\,]\quad\Delta_{2}=\bigcup_{i\in
I}\Delta_{i}\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{2},s:(c,{}_{?}\beta.T)\mathrel{\vdash}\prod_{i\in
I}[\,P_{i}\,|\,B_{i}\,|\,s[c,\tilde{m}_{i}]\,]\end{array}}}\
\footnotesize\textsc{{[TPar]}}\end{array}$

Using the above information we can type the result of the reduction,
$[\,P\,|\,B\,|\,s[c+1,\varepsilon]\,]\,|\\!|\,\prod_{i\in
I}[\,P_{i}\,|\,B_{i}\,|\,s[c+1,\tilde{m}_{i}\cdot e]\,]$. We begin with the
typing derivation for network node $[\,P\,|\,B\,|\,s[c+1,\varepsilon]\,]$:

$\boxed{\begin{array}[]{l}\footnotesize\textsc{{[TSynch]}}\\\
{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\breve{s}:(c+1,\varepsilon)\mathrel{\vdash}\breve{s}[c+1,\varepsilon]\quad\footnotesize\textsc{{[SEmp]}}\quad\Gamma;\Theta\mathrel{\vdash}B\end{array}}{\begin{array}[]{l}\Gamma;\Theta,\breve{s}:(c+1,\varepsilon)\mathrel{\vdash}B\,|\,\breve{s}[c+1,\varepsilon]\end{array}}}\
\footnotesize\textsc{{[BPar]}}\end{array}}\\\\[14.22636pt] \text{from former
derivation
}\Gamma;\Delta_{1}^{\prime\prime},\breve{s}:\overline{T}\mathrel{\vdash}P\\\\[2.84526pt]
\Delta_{1}^{\prime},\breve{s}:(c+1,\overline{T})=\Delta_{1}^{\prime\prime},\breve{s}:\overline{T}\circ\Theta,\breve{s}:(c+1,\varepsilon)\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{1}^{\prime},\breve{s}:(c+1,\overline{T})\mathrel{\vdash}[\,P\,|\,B\,|\,\breve{s}[c,\varepsilon]\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}\\\\[51.21495pt]
\begin{array}[]{l}\text{Linear context synchronisation
(Definition~{}\ref{def:synchr}) and former result}\\\
\Delta_{1}^{\prime},\breve{s}:(c,{}_{!}\beta.\overline{T})\mathrel{\hookrightarrow}\Delta_{0},\Delta_{1},\breve{s}:(c,{}_{!}\beta.\overline{T})\text{
implies}\\\
\Delta_{1}^{\prime},\breve{s}:(c+1,\overline{T})\mathrel{\hookrightarrow}\Delta_{0},\Delta_{1},\breve{s}:(c+1,\overline{T})\end{array}\\\\[19.91692pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{1},\breve{s}:(c+1,\overline{T})\mathrel{\vdash}[\,P\,|\,B\,|\,\breve{s}[c+1,\varepsilon]\,]\end{array}}}\end{array}}$

We derive the typing judgement for network node $\prod_{i\in
I}[\,P_{i}\,|\,B_{i}\,|\,s[c+1,\tilde{m}_{i}\cdot e]\,]$:

$\boxed{\begin{array}[]{l}\footnotesize\textsc{{[TSynch]}}\\\
{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}\footnotesize\textsc{{[BPar]}}\\\
{\textstyle\frac{\begin{array}[]{c}\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\begin{array}[]{l}\text{from
former judgement }\\\ \Gamma;s:(c,M)\mathrel{\vdash}s[c,\tilde{m}_{i}\cdot
e]\end{array}\end{array}}{\begin{array}[]{l}\Gamma;s:(c+1,M.{}_{!}\beta)\mathrel{\vdash}s[c+1,\tilde{m}_{i}\cdot
e]\end{array}}}\
\footnotesize\textsc{{[SExp]}}\end{array}\quad\Gamma;\Theta_{i}\mathrel{\vdash}B_{i}\end{array}}{\begin{array}[]{l}\Gamma;\Theta_{i},s:(c+1,M.{}_{!}\beta)\mathrel{\vdash}B_{i}\,|\,s[c+1,\tilde{m}_{i}\cdot
e]\end{array}}}\end{array}}\\\\[28.45274pt]
\Gamma;\Delta_{i}^{\prime\prime},s:T^{\prime}\mathrel{\vdash}P_{i}\\\
\begin{array}[]{l}\text{Operator $\circ$
(Definition~{}\ref{def:combine_context}) and former result}\\\
\Delta_{i}^{\prime},s:(c,{}_{?}\beta.T)=\Delta_{1}^{\prime\prime},s:T^{\prime}\circ\Theta,s:(c,M)\text{
imply}\\\
\Delta_{i}^{\prime},s:(c+1,T)=\Delta_{1}^{\prime\prime},s:T^{\prime}\circ\Theta,s:(c+1,M.{}_{!}\beta)\end{array}\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{i}^{\prime},s:(c+1,T)\mathrel{\vdash}[\,P_{i}\,|\,B_{i}\,|\,s[c+1,\tilde{m}_{i}\cdot
e]\,]\end{array}}}\ \footnotesize\textsc{{[TNode]}}\end{array}}\\\\[56.9055pt]
\Delta_{i}^{\prime},s:(c+1,T)\mathrel{\hookrightarrow}\Delta_{0},\Delta_{i},s:(c+1,T)\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{i},s:(c+1,T)\mathrel{\vdash}[\,P_{i}\,|\,B_{i}\,|\,s[c+1,\tilde{m}_{i}\cdot
e]\,]\end{array}}}\end{array}}$

We can now have multiple applications of rule [TPar] to get:

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{0},\Delta_{i},s:(c+1,T)\mathrel{\vdash}[\,P_{i}\,|\,B_{i}\,|\,s[c+1,\tilde{m}_{i}\cdot
e]\,]\quad\Delta_{2}=\bigcup_{i\in
I}\Delta_{i}\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{2},s:(c+1,T)\mathrel{\vdash}\prod_{i\in
I}[\,P_{i}\,|\,B_{i}\,|\,s[c+1,\tilde{m}_{i}\cdot e]\,]\end{array}}}\
\footnotesize\textsc{{[TPar]}}\end{array}$

The final rule needed to be applied is [TPar] to get:

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{0},\Delta_{1},\breve{s}:(c+1,\overline{T})\mathrel{\vdash}[\,P\,|\,B\,|\,\breve{s}[c+1,\varepsilon]\,]\\\
\Gamma;\Delta_{0},\Delta_{2},s:(c+1,T)\mathrel{\vdash}\prod_{i\in
I}[\,P_{i}\,|\,B_{i}\,|\,s[c+1,\tilde{m}_{i}\cdot
e]\,]\end{array}}{\begin{array}[]{l}\begin{array}[]{lcl}\Gamma;\Delta_{0},\Delta_{1},\breve{s}:(c+1,\overline{T}),\Delta_{2},s:(c+1,T)\mathrel{\vdash}&&[\,P\,|\,B\,|\,\breve{s}[c+1,\varepsilon]\,]\\\
&\,|\\!|&\prod_{i\in I}[\,P_{i}\,|\,B_{i}\,|\,s[c+1,\tilde{m}_{i}\cdot
e]\,]\end{array}\end{array}}}\ \footnotesize\textsc{{[TPar]}}\end{array}$

The case concludes because
$\Delta=\Delta_{0},\Delta_{1},\breve{s}:(c,{}_{!}\beta.\overline{T}),\Delta_{2},s:{}_{?}\beta.T$
and
$\Delta\mathrel{\shortrightarrow}\Delta_{0},\Delta_{1},\breve{s}:(c+1,\overline{T}),\Delta_{2},s:(c+1,T)$
as required.

  * •

Rule [Ucast]

Assume

$\begin{array}[]{l}\footnotesize\textsc{{[Ucast]}}\\\
{\textstyle\frac{\begin{array}[]{c}c_{1}\geq
c_{2}\end{array}}{\begin{array}[]{l}[\,s{}_{!}\langle
e\rangle.P_{1}\,|\,B_{1}\,|\,s[c_{1},\varepsilon]\,]\,|\\!|\,[\,P_{2}\,|\,B_{2}\,|\,\breve{s}[c_{2},\tilde{h}]\,]\\\
\qquad\qquad\mathrel{\longrightarrow}[\,P_{1}\,|\,B_{1}\,|\,s[c_{1}+1,\varepsilon]\,]\,|\\!|\,[\,P_{2}\,|\,\breve{s}[c_{2},\tilde{h}\cdot(c_{1},e)]\,]\end{array}}}\end{array}$

and

$\Gamma;\Delta\mathrel{\vdash}[\,s{}_{!}\langle
e\rangle.P_{1}\,|\,B_{1}\,|\,s[c_{1},\varepsilon]\,]\,|\\!|\,[\,P_{2}\,|\,B_{2}\,|\,\breve{s}[c_{2},\tilde{h}]\,]$

We provide the derivation for the latter typing judgement.

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\begin{array}[]{l}\text{well-
formed $\Delta$ implies
}\Delta=\Delta_{0},\Delta_{1},s:(c_{3},T),\Delta_{2},\breve{s}:(c_{3},\overline{T})\\\
\text{with $\Delta_{0}$ only $s$-endpoints and}\end{array}\\\
\Gamma;\Delta_{0},\Delta_{1},s:(c_{3},T)\mathrel{\vdash}[\,s{}_{!}\langle
e\rangle.P_{1}\,|\,B_{1}\,|\,s[c_{1},\varepsilon]\,]\\\
\Gamma;\Delta_{0},\Delta_{0},\breve{s}:(c_{3},\overline{T})\mathrel{\vdash}[\,P_{2}\,|\,B_{2}\,|\,\breve{s}[c_{2},\tilde{h}]\,]\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}[\,s{}_{!}\langle
e\rangle.P_{1}\,|\,B_{1}\,|\,s[c_{1},\varepsilon]\,]\,|\\!|\,[\,P_{2}\,|\,B_{2}\,|\,\breve{s}[c_{2},\tilde{h}]\,]\end{array}}}\
\footnotesize\textsc{{[TPar]}}\end{array}}$

We continue with the typing derivation for network node: $[\,s{}_{!}\langle
e\rangle.P_{1}\,|\,B_{1}\,|\,s[c_{1},\varepsilon]\,]$

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;s:(c_{1},\varepsilon)\mathrel{\vdash}s[c_{1},\varepsilon]\
\footnotesize\textsc{{[SEmp]}}\quad\Gamma;\Theta_{1}\mathrel{\vdash}B_{1}\end{array}}{\begin{array}[]{l}\Gamma;\Theta_{1},s:(c_{1},\varepsilon)\mathrel{\vdash}B_{1}\,|\,s[c_{1},\varepsilon]\end{array}}}\
\footnotesize\textsc{{[BPar]}}\end{array}}\\\\[17.07164pt]
\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{1}^{\prime\prime},s:T_{1}\mathrel{\vdash}P_{1}\quad\Gamma\mathrel{\vdash}e:\beta\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{1}^{\prime\prime},s:{}_{!}\beta.T_{1}\mathrel{\vdash}\breve{s}{}_{!}\langle
e\rangle.P_{1}\end{array}}}\
\footnotesize\textsc{{[TSnd]}}\end{array}\\\\[11.38109pt]
\Delta_{1}^{\prime},s:(c_{1},{}_{!}\beta.T_{1})=\Delta_{1}^{\prime\prime},s:{}_{!}\beta.T_{1}\circ\Theta_{1},s:(c_{1},\varepsilon)\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{1}^{\prime},s:(c_{1},{}_{!}\beta.T_{1})\mathrel{\vdash}[\,s{}_{!}\langle
e\rangle.P_{1}\,|\,B_{1}\,|\,s[c_{1},\varepsilon]\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}\\\\[56.9055pt]
\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Delta_{1}^{\prime}\mathrel{\hookrightarrow}\Delta_{0},\Delta_{1}\quad
c_{3}\geq
c_{1}\quad{}_{!}\beta.T_{1}\mathrel{\shortrightarrow}^{c_{3}-c_{1}}T\end{array}}{\begin{array}[]{l}\Delta_{1}^{\prime},s:(c_{1},{}_{!}\beta.T_{1})\mathrel{\hookrightarrow}\Delta_{0},\Delta_{1},s:(c_{3},T)\end{array}}}\end{array}\\\\[11.38109pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{1},s:(c_{3},T)\mathrel{\vdash}[\,s{}_{!}\langle
e\rangle.P_{1}\,|\,B_{1}\,|\,s[c_{1},\varepsilon]\,]\end{array}}}\
\footnotesize\textsc{{[TSynch]}}\end{array}}$

We also continue the derivation of network node
$[\,P_{2}\,|\,B_{2}\,|\,\breve{s}[c_{2},\tilde{h}]\,]$:

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\dots\end{array}}{\begin{array}[]{l}\Gamma;\breve{s}:(c_{3},M)\mathrel{\vdash}\breve{s}[c_{2},\tilde{h}]\end{array}}}\
\footnotesize\textsc{{[LExp]}}\end{array}\\\ c_{3}\geq
c_{1}\quad\Gamma;\Theta_{2}\mathrel{\vdash}B_{2}\end{array}}{\begin{array}[]{l}\Gamma;\Theta_{2},\breve{s}:(c_{3},M)\mathrel{\vdash}B_{2}\,|\,\breve{s}[c_{2},\tilde{h}]\end{array}}}\
\footnotesize\textsc{{[BPar]}}\end{array}}\\\\[34.1433pt]
\Gamma;\Delta_{2}^{\prime\prime},\breve{s}:T_{2}\mathrel{\vdash}P_{2}\quad\Delta_{2}^{\prime},\breve{s}:(c_{3},\overline{T})=\Delta_{2}^{\prime\prime},\breve{s}:T_{2}\circ\Theta_{2},\breve{s}:(c_{3},M)\end{array}}{\begin{array}[]{l}\Delta_{2}^{\prime},\breve{s}:(c_{3},\overline{T})\mathrel{\vdash}[\,P_{2}\,|\,B_{2}\,|\,\breve{s}[c_{2},\tilde{h}]\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}\\\\[62.59605pt]
\Delta_{2}^{\prime},\breve{s}:(c_{3},\overline{T})\mathrel{\hookrightarrow}\Delta_{0},\Delta_{2},\breve{s}:(c_{3},\overline{T})\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Delta_{0},\Delta_{2},\breve{s}:(c_{3},\overline{T})\mathrel{\vdash}[\,P_{2}\,|\,B_{2}\,|\,\breve{s}[c_{2},\tilde{h}]\,]\end{array}}}\
\footnotesize\textsc{{[TSynch]}}\end{array}}$

Using the above information we can type the result of the reduction,
$[\,P_{1}\,|\,B_{1}\,|\,s[c_{1}+1,\varepsilon]\,]\,|\\!|\,[\,P_{2}\,|\,\breve{s}[c_{2},\tilde{h}\cdot(c_{1},e)]\,]$.
We begin with the typing derivation for network node
$[\,P_{1}\,|\,B_{1}\,|\,s[c_{1}+1,\varepsilon]\,]$:

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}\footnotesize\textsc{{[TNode]}}\\\
{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;s:(c_{1}+1,\varepsilon)\mathrel{\vdash}s[c_{1}+1,\varepsilon]\
\footnotesize\textsc{{[SEmp]}}\quad\Gamma;\Theta_{1}\mathrel{\vdash}B_{1}\end{array}}{\begin{array}[]{l}\Gamma;\Theta_{1},s:(c_{1}+1,\varepsilon)\mathrel{\vdash}B_{1}\,|\,s[c_{1}+1,\varepsilon]\end{array}}}\
\footnotesize\textsc{{[BPar]}}\end{array}}\\\\[17.07164pt]
\Gamma;\Delta_{1}^{\prime\prime},s:T_{1}\mathrel{\vdash}P_{1}\quad\Delta_{1}^{\prime},s:(c_{1}+1,T_{1})=\Delta_{1}^{\prime\prime},s:T\circ\Theta_{1},s:(c_{1}+1,\varepsilon)\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{1}^{\prime},s:(c_{1}+1,T_{1})\mathrel{\vdash}[\,P_{1}\,|\,B_{1}\,|\,s[c_{1}+1,\varepsilon]\,]\end{array}}}\end{array}}\\\\[48.36967pt]
\begin{array}[]{l}\text{results
}\Delta_{1}^{\prime},s:(c_{1},{}_{!}\beta.T_{1})\mathrel{\hookrightarrow}\Delta_{0},\Delta_{1},s:(c_{3},T)\text{
and $c_{3}\geq c_{1}$ imply}\\\
\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Delta_{1}^{\prime}\mathrel{\hookrightarrow}\Delta_{0},\Delta_{1}\quad
c_{4}=c_{3}\vee c_{4}=c_{3}+1\quad
T_{1}\mathrel{\shortrightarrow}^{c_{4}-c_{1}+1}T^{\prime}\end{array}}{\begin{array}[]{l}\Delta_{1}^{\prime},s:(c_{1}+1,T_{1})\mathrel{\hookrightarrow}\Delta_{0},\Delta_{1},s:(c_{4},T^{\prime})\end{array}}}\end{array}\end{array}\\\\[19.91692pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{1},s:(c_{4},T^{\prime})\mathrel{\vdash}[\,P_{1}\,|\,B_{1}\,|\,s[c_{1}+1,\varepsilon]\,]\end{array}}}\
\footnotesize\textsc{{[TSynch]}}\end{array}}$

We continue with the typing derivation for network node
$[\,P_{2}\,|\,\breve{s}[c_{2},\tilde{h}\cdot(c_{1},e)]\,]$:

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}\footnotesize\textsc{{[TNode]}}\\\
{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}\footnotesize\textsc{{[BPar]}}\\\
{\textstyle\frac{\begin{array}[]{c}\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\breve{s}:(c_{3},M)\mathrel{\vdash}\breve{s}[c_{2},\tilde{h}]\\\
c_{4}=c_{3}\vee
c_{4}=c_{3}+1\end{array}}{\begin{array}[]{l}\Gamma;\breve{s}:(c_{4},M.{}_{!}\beta)\mathrel{\vdash}\breve{s}[c_{2},\tilde{h}\cdot(c_{1},e)]\end{array}}}\
\footnotesize\textsc{{[LExp]}}\end{array}\quad\Gamma;\Theta_{2}\mathrel{\vdash}B_{2}\end{array}}{\begin{array}[]{l}\Gamma;\Theta_{2},\breve{s}:(c_{4},M.{}_{!}\beta)\mathrel{\vdash}B_{2}\,|\,\breve{s}[c_{2},\tilde{h}\cdot(c_{1},e)]\end{array}}}\end{array}}\\\\[39.83385pt]
\Gamma;\Delta_{2}^{\prime\prime},\breve{s}:T_{2}\mathrel{\vdash}P_{2}\quad\Delta_{2}^{\prime},\breve{s}:(c_{4},\overline{T}^{\prime})=\Delta_{2}^{\prime\prime},\breve{s}:T_{2}\circ\Theta_{2},\breve{s}:(c_{4},M.{}_{!}\beta)\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Delta_{2}^{\prime},\breve{s}:(c_{4},\overline{T}^{\prime})\mathrel{\vdash}[\,P_{2}\,|\,B_{2}\,|\,\breve{s}[c_{2},\tilde{h}]\,]\end{array}}}\end{array}}\\\\[73.97716pt]
\Delta_{2}^{\prime},\breve{s}:(c_{4},\overline{T}^{\prime})\mathrel{\hookrightarrow}\Delta_{0},\Delta_{2},\breve{s}:(c_{4},\overline{T}^{\prime})\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Delta_{0},\Delta_{2},\breve{s}:(c_{4},\overline{T}^{\prime})\mathrel{\vdash}[\,P_{2}\,|\,B_{2}\,|\,\breve{s}[c_{2},\tilde{h}]\,]\end{array}}}\
\footnotesize\textsc{{[TSynch]}}\end{array}}$

We apply rule [TPar] to get

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{0},\Delta_{1},s:(c_{4},T^{\prime})\mathrel{\vdash}[\,P_{1}\,|\,B_{1}\,|\,s[c_{1}+1,\varepsilon]\,]\\\
\Delta_{0},\Delta_{2},\breve{s}:(c_{4},\overline{T^{\prime}})\mathrel{\vdash}[\,P_{2}\,|\,B_{2}\,|\,\breve{s}[c_{2},\tilde{h}]\,]\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{1},s:(c_{4},T^{\prime}),\Delta_{2},\breve{s}:(c_{4},\overline{T}^{\prime})\mathrel{\vdash}[\,P_{1}\,|\,B_{1}\,|\,s[c_{1}+1,\varepsilon]\,]\,|\\!|\,[\,P_{2}\,|\,B_{2}\,|\,\breve{s}[c_{2},\tilde{h}]\,]\end{array}}}\
\footnotesize\textsc{{[TPar]}}\end{array}$

From here there are two cases: If $c_{4}=c_{3}$ then $T^{\prime}=T$ and the
result follows from the fact that
$\Delta_{0},\Delta_{1},s:(c_{4},T^{\prime}),\Delta_{2},\breve{s}:(c_{4},\overline{T^{\prime}})=\Delta_{0},\Delta_{1},s:(c_{3},T),\Delta_{2},\breve{s}:(c_{3},\overline{T})$.
If $c_{4}=c_{3}+1$ then $T\mathrel{\shortrightarrow}^{1}T^{\prime}$ and the
results follows the fact that
$\Delta_{0},\Delta_{1},s:(c_{3},T),\Delta_{2},\breve{s}:(c_{3},\overline{T})\mathrel{\shortrightarrow}^{1}\Delta_{0},s:(c_{4},T^{\prime}),\Delta_{2},\breve{s}:(c_{4},\overline{T^{\prime}})$

  * •

Rule [Rcv]

Assume

$[\,{s}{}_{?}(x)\langle
e^{\prime}\rangle.P\,|\,B\,|\,s[c,e\cdot\tilde{m}]\,]\mathrel{\longrightarrow}[\,P\\{{e}/{x}\\}\,|\,B\,|\,s[c,\tilde{m}]\,]$

with

$\Gamma;\Delta\mathrel{\vdash}[\,{s}{}_{?}(x)\langle
e^{\prime}\rangle.P\,|\,B\,|\,s[c,e\cdot\tilde{m}]\,]$

and $\Delta$ well-formed. We give the derivation for the latter typing
judgement

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;s:(c,M)\mathrel{\vdash}B\,|\,s[c,\tilde{m}]\end{array}}{\begin{array}[]{l}\Gamma;s:(c,{}_{!}\beta.M)\mathrel{\vdash}B\,|\,s[c,e\cdot\tilde{m}]\end{array}}}\
\footnotesize\textsc{{[SExp]}}\end{array}\quad\Gamma;\Theta\mathrel{\vdash}B\\\\[11.38109pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Theta,s:(c,{}_{!}\beta.M)\mathrel{\vdash}B\,|\,s[c,e\cdot\tilde{m}]\end{array}}}\
\footnotesize\textsc{{[BPar]}}\end{array}}\\\\[28.45274pt]
\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma\mathrel{\vdash}e^{\prime}:\beta\quad\Gamma,x:\beta;\Delta^{\prime},s:T^{\prime}\mathrel{\vdash}P\end{array}}{\begin{array}[]{l}\Gamma;\Delta^{\prime},s:{}_{?}\beta.T^{\prime}\mathrel{\vdash}{s}{}_{?}(x)\langle
e^{\prime}\rangle.P\end{array}}}\
\footnotesize\textsc{{[TRcv]}}\end{array}}\\\\[17.07164pt]
\begin{array}[]{rcl}\Delta=\Delta^{\prime},s:(c,T)&=&\Delta^{\prime},s:{}_{?}\beta.T^{\prime}\circ\Theta,(c,{}_{!}\beta.M)\\\
&=&\Delta,s:T^{\prime}\circ\Theta,s:(c,M)\end{array}\\\\[11.38109pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}[\,{s}{}_{?}(x)\langle
e^{\prime}\rangle.P\,|\,B\,|\,s[c,e\cdot\tilde{m}]\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}$

The above result allows us to produce the typing derivation for the result of
the reduction, $[\,P\\{{e}/{x}\\}\,|\,B\,|\,s[c,\tilde{m}]\,]$:

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;s:(c,M)\mathrel{\vdash}B\,|\,s[c,\tilde{m}]\quad\Gamma;\Theta\mathrel{\vdash}B\end{array}}{\begin{array}[]{l}\Gamma;\Theta,s:(c,M)\mathrel{\vdash}B\,|\,s[c,\tilde{m}]\end{array}}}\
\footnotesize\textsc{{[BPar]}}\end{array}}\\\\[17.07164pt]
\Gamma;\Delta^{\prime},s:T^{\prime}\mathrel{\vdash}P\quad\Delta=\Delta^{\prime},s:(c,T)=\Delta,s:T^{\prime}\circ\Theta,s:(c,M)\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}[\,P\\{{e}/{x}\\}\,|\,B\,|\,s[c,\tilde{m}]\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}$

as required.

  * •

Rule [Gthr].

Assume

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\tilde{h}^{\prime}=\mathsf{B}(\tilde{h},c+1)\quad
e=\mathsf{V}(\tilde{h},c+1)\end{array}}{\begin{array}[]{l}[\,{\breve{s}}{}_{?}(x).P\,|\,B\,|\,\breve{s}[c,\tilde{h}]\,]\mathrel{\longrightarrow}[\,P\\{{e}/{x}\\}\,|\,B\,|\,\breve{s}[c+1,\tilde{h}^{\prime}]\,]\end{array}}}\
\footnotesize\textsc{{[Gthr]}}\end{array}$

with

$\Gamma;\Delta\mathrel{\vdash}[\,{\breve{s}}{}_{?}(x).P\,|\,B\,|\,\breve{s}[c,\tilde{h}]\,]$

and $\Delta$ well-formed. We produce the derivation of the latter typing
judgement: We first type the session buffer $\breve{s}[c,\tilde{h}]$:

$\begin{array}[]{ll}\left.\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\breve{s}:(c,\varepsilon)\mathrel{\vdash}\breve{s}[c,\varepsilon]\
\footnotesize\textsc{{[SEmp]}}\\\
\varepsilon=\mathsf{B}(\tilde{h}_{1},c+1)\quad\Gamma\mathrel{\vdash}V(\tilde{h}_{1},c+1):\beta\end{array}}{\begin{array}[]{l}\Gamma;\breve{s}:(c+1,{}_{!}\beta)\mathrel{\vdash}\breve{s}[c,\tilde{h}_{1}]\end{array}}}\
\footnotesize\textsc{{[LExp]}}\end{array}}\\\ \vdots\\\
\Gamma;\breve{s}:(c^{\prime}-1,{}_{!}\beta.M)\mathrel{\vdash}\breve{s}[c,\tilde{h}_{c^{\prime}-c}]\\\
\tilde{h}=\mathsf{B}(\tilde{h}_{c^{\prime}-c},c^{\prime})\quad\Gamma\mathrel{\vdash}V(\tilde{h},c^{\prime}):\beta^{\prime}\end{array}}{\begin{array}[]{l}\Gamma;\breve{s}:(c^{\prime},{}_{!}\beta.M.{}_{!}\beta^{\prime})\mathrel{\vdash}\breve{s}[c,\tilde{h}]\end{array}}}\
\footnotesize\textsc{{[LExp]}}\end{array}}\end{array}\right\\}&\begin{array}[]{l}c^{\prime}-c\\\
\text{applications}\\\ \text{of rule
$\footnotesize\textsc{{[LExp]}}$}\end{array}\end{array}$

We now produce the typing derivation for term
$[\,{\breve{s}}{}_{?}(x).P\,|\,B\,|\,\breve{s}[c,\tilde{h}]\,]$:

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\breve{s}:(c^{\prime},{}_{!}\beta.M.{}_{!}\beta^{\prime})\mathrel{\vdash}\breve{s}[c,\tilde{h}]\quad\Gamma;\Theta\mathrel{\vdash}B\end{array}}{\begin{array}[]{l}\Gamma;\Theta,\breve{s}:(c^{\prime},{}_{!}\beta.M.{}_{!}\beta^{\prime})\mathrel{\vdash}B\,|\,\breve{s}[c,\tilde{h}]\end{array}}}\
\footnotesize\textsc{{[BPar]}}\end{array}}\\\\[17.07164pt]
\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma,x:\beta;\Delta^{\prime},\breve{s}:T^{\prime}\mathrel{\vdash}P\end{array}}{\begin{array}[]{l}\Gamma;\Delta^{\prime},\breve{s}:{}_{?}\beta.T^{\prime}\mathrel{\vdash}{\breve{s}}{}_{?}(x).P\end{array}}}\
\footnotesize\textsc{{[TRcv]}}\end{array}\\\\[11.38109pt]
\begin{array}[]{rcl}\Delta=\Delta^{\prime},\breve{s}:(c^{\prime},T)&=&\Delta^{\prime},\breve{s}:{}_{?}\beta.T^{\prime}\circ\Theta,\breve{s}:(c^{\prime},{}_{!}\beta.M.{}_{!}\beta^{\prime})\\\
&=&\Delta^{\prime},\breve{s}:T^{\prime}\circ\Theta,\breve{s}:(c^{\prime},M.{}_{!}\beta^{\prime})\end{array}\\\\[11.38109pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}[\,{\breve{s}}{}_{?}(x).P\,|\,B\,|\,\breve{s}[c,\tilde{h}]\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}$

We use the above information to produce the typing derivation for the result
of the reduction. We first produce the typing derivation for session buffer
$\breve{s}[c+1,\tilde{h}^{\prime}]$

$\begin{array}[]{ll}\left.\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\breve{s}:(c+1,\varepsilon)\mathrel{\vdash}\breve{s}[c+1,\varepsilon]\
\footnotesize\textsc{{[SEmp]}}\\\\[11.38109pt]
\varepsilon=\mathsf{B}(\tilde{h}_{2}^{\prime},c+2)\quad\Gamma\mathrel{\vdash}V(\tilde{h}_{2}^{\prime},c+2):\beta^{\prime\prime}\end{array}}{\begin{array}[]{l}\Gamma;\breve{s}:(c+2,{}_{!}\beta^{\prime\prime})\mathrel{\vdash}\breve{s}[c+1,\tilde{h}_{2}^{\prime}]\end{array}}}\
\footnotesize\textsc{{[LExp]}}\end{array}}\\\ \vdots\\\
\Gamma;\breve{s}(c^{\prime}-1,M)\mathrel{\vdash}\breve{s}[c+1,\tilde{h}_{c^{\prime}-c+1}^{\prime}]\\\
\tilde{h}^{\prime}=\mathsf{B}(\tilde{h}_{c^{\prime}-c+1}^{\prime},c^{\prime})\quad\Gamma\mathrel{\vdash}V(\tilde{h}^{\prime},c^{\prime}):\beta^{\prime}\end{array}}{\begin{array}[]{l}\Gamma;\breve{s}:(c^{\prime},M.{}_{!}\beta^{\prime})\mathrel{\vdash}\breve{s}[c+1,\tilde{h}^{\prime}]\end{array}}}\
\footnotesize\textsc{{[LExp]}}\end{array}}\end{array}\right\\}&\begin{array}[]{l}c^{\prime}-c+1\\\
\text{applications}\\\ \text{of rule
$\footnotesize\textsc{{[LExp]}}$}\end{array}\end{array}$

Finally we give the typing derivation for network node:
$[\,P\\{{e}/{x}\\}\,|\,B\,|\,\breve{s}[c+1,\tilde{h}^{\prime}]\,]$

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}\footnotesize\textsc{{[BPar]}}\\\
{\textstyle\frac{\begin{array}[]{c}\Gamma;\breve{s}:(c^{\prime},M.{}_{!}\beta^{\prime})\mathrel{\vdash}\breve{s}[c+1,\tilde{h}^{\prime}]\quad\quad\Gamma;\Theta\mathrel{\vdash}B\end{array}}{\begin{array}[]{l}\Gamma;\Theta,\breve{s}:(c^{\prime},M.{}_{!}\beta^{\prime})\mathrel{\vdash}B\,|\,\breve{s}[c^{\prime},\tilde{h}^{\prime}]\end{array}}}\end{array}}\\\\[22.76219pt]
\begin{array}[]{l}\text{From Substitution Lemma~{}\ref{lem:substitution} }\\\
\Gamma,x:\beta;\Delta^{\prime},\breve{s}:T^{\prime}\mathrel{\vdash}P\text{
implies
}\Gamma;\Delta^{\prime},\breve{s}:T^{\prime}\mathrel{\vdash}P\\{{e}/{x}\\}\end{array}\\\\[11.38109pt]
\Gamma;\emptyset\mathrel{\vdash}R\quad\Delta=\Delta^{\prime},\breve{s}:(c^{\prime},T)=\Delta^{\prime},\breve{s}:T^{\prime}\circ\Theta,\breve{s}:(c^{\prime},M.{}_{!}\beta^{\prime})\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}[\,{\breve{s}}{}_{?}(x).P\,|\,B\,|\,\breve{s}[c,\tilde{h}]\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}$

The result follows the fact that $\Delta\mathrel{\shortrightarrow}\Delta$.

  * •

Rule [Sel]. The proof is similar to the proof for rule [Bcast].

  * •

Rule [Bra]. The proof is similar to the proof for rule [Rcv].

  * •

Rule [Loss]

Assume

$[\,s{}_{!}\langle
e\rangle.P\,|\,B\,|\,s[c,\varepsilon]\,]\mathrel{\longrightarrow}[\,P\,|\,B\,|\,s[c+1,\varepsilon]\,]$

with

$\Gamma;\Delta\mathrel{\vdash}[\,s{}_{!}\langle
e\rangle.P\,|\,B\,|\,s[c,\varepsilon]\,]$

and $\Delta$ well-formed. We provide the derivation of the latter typing
judgement:

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;s:(c,\varepsilon)\mathrel{\vdash}s[c,\varepsilon]\
\footnotesize\textsc{{[SEmp]}}\quad\Gamma;\Theta\mathrel{\vdash}B\end{array}}{\begin{array}[]{l}\Gamma;\Theta,s:(c,\varepsilon)\mathrel{\vdash}B\,|\,s[c,\varepsilon]\end{array}}}\
\footnotesize\textsc{{[BPar]}}\end{array}}\\\\[17.07164pt]
\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta^{\prime},s:T\mathrel{\vdash}P\quad\Gamma\mathrel{\vdash}e:\beta\end{array}}{\begin{array}[]{l}\Gamma;\Delta^{\prime},s:{}_{!}\beta.\mathrel{\vdash}s{}_{!}\langle
e\rangle.P\end{array}}}\
\footnotesize\textsc{{[TSnd]}}\end{array}}\\\\[17.07164pt]
\Delta=\Delta^{\prime},s:(c,{}_{!}\beta.T)=\Delta^{\prime},s:{}_{!}\beta.T\circ\Theta,s:(c,\varepsilon)\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}[\,s{}_{!}\langle
e\rangle.P\,|\,B\,|\,s[c,\varepsilon]\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}$

The above result allows us to produce the typing derivation for the result of
the reduction, $[\,P\,|\,B\,|\,s[c+1,\varepsilon]\,]$

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;s:(c+1,\varepsilon)\mathrel{\vdash}s[c+1,\varepsilon]\
\footnotesize\textsc{{[SEmp]}}\quad\Gamma;\Theta\mathrel{\vdash}B\end{array}}{\begin{array}[]{l}\Gamma;\Theta,s:(c+1,\varepsilon)\mathrel{\vdash}B\,|\,s[c+1,\varepsilon]\end{array}}}\
\footnotesize\textsc{{[BPar]}}\end{array}}\\\\[17.07164pt]
\Gamma;\Delta^{\prime},s:T\mathrel{\vdash}P\quad\Delta^{\prime},s:(c+1,T)=\Delta^{\prime},s:T\circ\Theta,s:(c+1,\varepsilon)\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta^{\prime},s:(c+1,T)\mathrel{\vdash}[\,P\,|\,B\,|\,s[c+1,\varepsilon]\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}\\\\[39.83385pt]
\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Delta^{\prime}\mathrel{\hookrightarrow}\Delta^{\prime}\quad{}_{!}\beta.T\mathrel{\shortrightarrow}_{o}^{c+1-c}T\end{array}}{\begin{array}[]{l}\Delta^{\prime},s:(c+1,T)\mathrel{\hookrightarrow}\Delta^{\prime},s:(c,{}_{!}\beta.T)\end{array}}}\end{array}\quad\Delta=\Delta^{\prime},s:(c,{}_{!}\beta.T)\\\\[11.38109pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}[\,P\,|\,B\,|\,s[c+1,\varepsilon]\,]\end{array}}}\
\footnotesize\textsc{{[TSynch]}}\end{array}}$

as required.

  * •

Rule [Rec]

Assume

$[\,{s}{}_{?}(x)\langle
e\rangle.P\,|\,B\,|\,s[c,\varepsilon]\,]\mathrel{\longrightarrow}[\,P\\{{e}/{x}\\}\,|\,B\,|\,s[c+1,\varepsilon]\,]\
\footnotesize\textsc{{[Rec]}}$

with

$\Gamma;\Delta\mathrel{\vdash}[\,{s}{}_{?}(x)\langle
e\rangle.P\,|\,B\,|\,s[c,\varepsilon]\,]$

and $\Delta$ well-formed. We give the derivation for the latter typing
judgement

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;s:(c,\varepsilon)\mathrel{\vdash}s[c,\varepsilon]\
\footnotesize\textsc{{[SEmp]}}\quad\Gamma;\Theta\mathrel{\vdash}B\end{array}}{\begin{array}[]{l}\Gamma;\Theta,s:(c,\varepsilon)\mathrel{\vdash}B\,|\,s[c,\varepsilon]\end{array}}}\
\footnotesize\textsc{{[BPar]}}\end{array}}\\\\[17.07164pt]
\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma\mathrel{\vdash}e:\beta\quad\Gamma,x:\beta;\Delta^{\prime},s:T\mathrel{\vdash}P\end{array}}{\begin{array}[]{l}\Gamma;\Delta^{\prime},s:{}_{?}\beta.T\mathrel{\vdash}{s}{}_{?}(x)\langle
e\rangle.P\end{array}}}\
\footnotesize\textsc{{[TRcv]}}\end{array}}\\\\[17.07164pt]
\Delta=\Delta^{\prime},s:(c,{}_{?}\beta.T)=\Delta^{\prime},s:{}_{?}\beta.T\circ\Theta,(c,\varepsilon)\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}[\,{s}{}_{?}(x)\langle
e^{\prime}\rangle.P\,|\,B\,|\,s[c,e\cdot\tilde{m}]\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}$

The above result allows us to produce the typing derivation for the result of
the reduction, $[\,P\\{{e}/{x}\\}\,|\,B\,|\,s[c+1,\varepsilon]\,]$

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;s:(c+1,\varepsilon)\mathrel{\vdash}s[c+1,\varepsilon]\quad\Gamma;\Theta\mathrel{\vdash}B\end{array}}{\begin{array}[]{l}\Gamma;\Theta,s:(c+1,\varepsilon)\mathrel{\vdash}B\,|\,s[c,\tilde{m}]\end{array}}}\
\footnotesize\textsc{{[BPar]}}\end{array}}\\\\[17.07164pt]
\Gamma;\Delta^{\prime},s:T\mathrel{\vdash}P\\{{e}/{x}\\}\quad\Delta^{\prime},s:(c+1,T)=\Delta,s:T\circ\Theta,s:(c+1,\varepsilon)\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta^{\prime},s:(c+1,T)\mathrel{\vdash}[\,P\\{{e}/{x}\\}\,|\,B\,|\,s[c,\tilde{m}]\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}\\\\[39.83385pt]
\Delta^{\prime},s:(c+1,T)\mathrel{\hookrightarrow}\Delta^{\prime},s:(c,{}_{?}\beta.T)\quad\Delta=\Delta^{\prime},s:(c,{}_{?}\beta.T)\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}[\,P\\{{e}/{x}\\}\,|\,B\,|\,s[c,\tilde{m}]\,]\end{array}}}\
\footnotesize\textsc{{[TSynch]}}\end{array}}$

as required.

  * •

Rule [BRec]

Assume

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\mathrm{fs}(B)=\mathrm{fs}(R)\end{array}}{\begin{array}[]{l}[\,s\,{\triangleright}\,\\{\ell_{i}:P_{i},\mathtt{df}:R\\}_{i\in
I}\,|\,B\,|\,B^{\prime}\,|\,s[c,\varepsilon]\,]\mathrel{\longrightarrow}[\,R\,|\,B\,]\end{array}}}\end{array}\
\footnotesize\textsc{{[BRec]}}$

with

$\Gamma;\Delta\mathrel{\vdash}[\,s\,{\triangleright}\,\\{\ell_{i}:P_{i},\mathtt{df}:R\\}_{i\in
I}\,|\,B\,|\,B^{\prime}\,|\,s[c,\varepsilon]\,]$

and $\Delta$ well-formed. The last result follows typing derivation:

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;s:(c,\varepsilon)\mathrel{\vdash}s[c,\varepsilon]\
\footnotesize\textsc{{[SEmp]}}\\\
\Gamma;\Theta_{1}\mathrel{\vdash}B^{\prime}\quad\Gamma;\Theta_{2}\mathrel{\vdash}B\quad\Theta=\Theta_{1},\Theta_{2}\end{array}}{\begin{array}[]{l}\Gamma;\Theta,s:(c,\varepsilon)\mathrel{\vdash}B\,|\,B^{\prime}\,|\,s[c,\varepsilon]\end{array}}}\
\footnotesize\textsc{{[BPar]}}\end{array}}\\\\[22.76219pt]
\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\forall i\in
I,\Gamma;\Delta_{1},\Delta_{2},s:T_{i}\mathrel{\vdash}P_{i}\\\ \text{only
$s$-endpoints in
}\Delta_{1}\quad\Gamma;\Delta_{2}\mathrel{\vdash}R\quad\Delta^{\prime}=\Delta_{1},\Delta_{2}\end{array}}{\begin{array}[]{l}\Gamma;\Delta^{\prime},s:\&\\{l_{i}\mathrel{:}T_{i}\\}_{i\in
I}\mathrel{\vdash}s\,{\triangleright}\,\\{\ell_{i}:P_{i},\mathtt{df}:R\\}_{i\in
I}\end{array}}}\ \footnotesize\textsc{{[TBr]}}\end{array}}\\\\[22.76219pt]
\Delta=\Delta^{\prime},s:\&\\{l_{i}\mathrel{:}T_{i}\\}_{i\in
I}\circ\Theta,s:(c,\varepsilon)\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}[\,s\,{\triangleright}\,\\{\ell_{i}:P_{i},\mathtt{df}:R\\}_{i\in
I}\,|\,B\,|\,B^{\prime}\,|\,s[c,\varepsilon]\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}$

We can now provide the typing derivation for the result of the reduction
$[\,R\,|\,B\,]$

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{2}\mathrel{\vdash}R\quad\Gamma;\Theta_{2}\mathrel{\vdash}B\quad\mathrm{fs}(R)=\mathrm{fs}(B)\text{
implies
}\Delta^{\prime\prime}=\Delta_{2}\circ\Theta_{2}\end{array}}{\begin{array}[]{l}\Gamma;\Delta^{\prime\prime}\mathrel{\vdash}[\,R\,|\,B\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}$

Because $\Delta_{1}$ includes only $s$-enpoints, we can use
$\mathrel{\shortrightarrow}$ to drop them:

$\displaystyle\Delta$ $\displaystyle=$
$\displaystyle\Delta_{1},\Delta_{2},s:\&\\{l_{i}\mathrel{:}T_{i}\\}_{i\in
I}\circ\Theta_{1},\Theta_{2},s:(c,\varepsilon)$ $\displaystyle=$
$\displaystyle(\Delta_{1}\circ\Theta_{1}),(\Delta_{2}\circ\Theta_{2}),s:(c,\&\\{l_{i}\mathrel{:}T_{i}\\}_{i\in
I})$ $\displaystyle\mathrel{\shortrightarrow}$
$\displaystyle(\Delta_{2}\circ\Theta_{2})$ $\displaystyle=$
$\displaystyle\Delta^{\prime\prime}$

as required

  * •

Rule [True]

Assume

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Vdash\varphi\quad\mathrm{fs}(P_{1})=\mathrm{fs}(B)\end{array}}{\begin{array}[]{l}[\,\mathsf{if}\,\varphi\,\mathsf{then}\,P_{1}\,\mathsf{else}\,P_{2}\,|\,B\,|\,B^{\prime}\,]\mathrel{\longrightarrow}[\,P_{1}\,|\,B\,]\end{array}}}\
\footnotesize\textsc{{[True]}}\end{array}$

with

$\Gamma;\Delta\mathrel{\vdash}[\,\mathsf{if}\,\varphi\,\mathsf{then}\,P_{1}\,\mathsf{else}\,P_{2}\,|\,B\,|\,B^{\prime}\,]$

and $\Delta$ well-type. The derivation for the latter typing judgement is

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Theta_{1}\mathrel{\vdash}B\quad\Gamma;\Theta_{2}\mathrel{\vdash}B^{\prime}\end{array}}{\begin{array}[]{l}\Gamma;\Theta_{1},\Theta_{2}\mathrel{\vdash}B\,|\,B^{\prime}\end{array}}}\
\footnotesize\textsc{{[BPar]}}\end{array}}\\\\[17.07164pt]
\boxed{\begin{array}[]{l}\footnotesize\textsc{{[TCond]}}\\\
{\textstyle\frac{\begin{array}[]{c}\Gamma\mathrel{\vdash}\varphi:\mathsf{bool}\quad\Gamma;\Delta_{0},\Delta_{1}\mathrel{\vdash}P_{1}\quad\Gamma;\Delta_{0},\Delta_{2}\mathrel{\vdash}P_{2}\\\
i,j\in\\{1,2\\}\land
i\not=j\implies\mathrm{dom}(\Delta_{i})=\mathrm{fs}(P_{i})-\mathrm{fs}(P_{j})\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{1},\Delta_{2}\mathrel{\vdash}\mathsf{if}\,\varphi\,\mathsf{then}\,P_{1}\,\mathsf{else}\,P_{2}\end{array}}}\end{array}}\\\\[28.45274pt]
\Gamma;\emptyset\mathrel{\vdash}R\quad\Delta=\Delta_{0},\Delta_{1},\Delta_{2}\circ\Theta_{1},\Theta_{2}\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}[\,\mathsf{if}\,\varphi\,\mathsf{then}\,P_{1}\,\mathsf{else}\,P_{2}\,|\,B\,|\,B^{\prime}\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}$

We use the above information to type the result of the reduction
$[\,P_{1}\,|\,B\,]$:

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{0},\Delta_{1}\mathrel{\vdash}P_{1}\quad\Gamma;\emptyset\mathrel{\vdash}R\quad\Gamma;\Theta_{1}\mathrel{\vdash}B\quad\Delta^{\prime}=\Delta_{0},\Delta_{1}\circ\Theta_{1}\end{array}}{\begin{array}[]{l}\Gamma;\Delta^{\prime}\mathrel{\vdash}[\,P_{1}\,|\,B\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}$

The reduction condition requires that $\mathrm{fs}(B)=\mathrm{fs}(P_{1})$.
From the last equation and the fact that
$\mathrm{fs}(B)=\mathrm{dom}(\Theta_{1})$ we have that
$\mathrm{fs}(P_{1})=\mathrm{dom}(\Theta_{1})$. Also
$\mathrm{fs}(P_{1})=\mathrm{dom}(\Delta_{0},\Delta_{1})$. From the latter two
equalities we can conclude that $\Delta_{0},\Delta_{1}\circ\Theta_{1}$ is
defined and $\mathrm{fs}(P_{1})=\mathrm{dom}(\Delta^{\prime})$. Moreover,
$\mathrm{fs}(P_{1})\cup\mathrm{fs}(P_{2})=\Delta$. Therefore,
$\Delta^{\prime}\subseteq\Delta$ as required.

  * •

Rule [False]. The proof the same with the proof of case [True].

  * •

Rule (Sum).

Assume

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}[\,P_{1}\,|\,B\,]\,|\\!|\,N\mathrel{\longrightarrow}[\,P^{\prime}\,|\,B^{\prime}\,]\,|\\!|\,N^{\prime}\end{array}}{\begin{array}[]{l}[\,P_{1}+P_{2}\,|\,B\,]\,|\\!|\,N\mathrel{\longrightarrow}[\,P^{\prime}\,|\,B^{\prime}\,]\,|\\!|\,N^{\prime}\end{array}}}\
\footnotesize\textsc{{[NDet]}}\end{array}$

with

$\Gamma;\Delta\mathrel{\vdash}[\,P_{1}+P_{2}\,|\,B\,]\,|\\!|\,N$

and $\Delta$ well-formed.

We produce the derivation for the latter typing judgement.

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}\footnotesize\textsc{{[TSum]}}\\\
{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{1}^{\prime\prime}\mathrel{\vdash}P_{1}\quad\Gamma;\Delta_{1}^{\prime\prime}\mathrel{\vdash}P_{2}\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{1}^{\prime\prime}\mathrel{\vdash}P_{1}+P_{2}\end{array}}}\end{array}}\\\\[8.53581pt]
\Gamma;\Theta\mathrel{\vdash}B\quad\Delta_{1}^{\prime}=\Delta_{1}^{\prime\prime}\circ\Theta\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{1}^{\prime}\mathrel{\vdash}[\,P_{1}+P_{2}\,|\,B\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}\quad\Delta_{1}^{\prime}\mathrel{\hookrightarrow}\Delta_{0},\Delta_{1}\\\\[45.5244pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{1}\mathrel{\vdash}[\,P_{1}+P_{2}\,|\,B\,]\end{array}}}\
\footnotesize\textsc{{[TSynch]}}\end{array}}\\\\[56.9055pt]
\Gamma;\Delta_{0},\Delta_{2}\mathrel{\vdash}N\quad\Delta_{0}\text{ only
$s$-endpoints}\quad\Delta=\Delta_{0},\Delta_{1},\Delta_{2}\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}[\,P_{1}+P_{2}\,|\,B\,]\,|\\!|\,N\end{array}}}\
\footnotesize\textsc{{[TPar]}}\end{array}}$

We can now produce the typing derivation for the left hand side network of the
premise $[\,P_{1}\,|\,B\,]\,|\\!|\,N$:

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}\footnotesize\textsc{{[TNode]}}\\\
{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{1}^{\prime\prime}\mathrel{\vdash}P_{1}\quad\Gamma;\Theta\mathrel{\vdash}B\quad\Delta_{1}^{\prime}=\Delta_{1}^{\prime\prime}\circ\Theta\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{1}^{\prime}\mathrel{\vdash}[\,P_{1}\,|\,B\,]\end{array}}}\end{array}}\quad\Delta_{1}^{\prime}\mathrel{\hookrightarrow}\Delta_{0},\Delta_{1}\\\\[22.76219pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{1}\mathrel{\vdash}[\,P_{1}\,|\,B\,]\end{array}}}\
\footnotesize\textsc{{[TSynch]}}\end{array}}\\\\[39.83385pt]
\Gamma;\Delta_{0},\Delta_{2}\mathrel{\vdash}N\quad\Delta_{0}\text{ only
$s$-endpoints}\quad\Delta=\Delta_{0},\Delta_{1},\Delta_{2}\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}[\,P_{1}\,|\,B\,]\,|\\!|\,N\end{array}}}\
\footnotesize\textsc{{[TPar]}}\end{array}}$

The latter two derivations have the same typing contexts. The result is then
immediate from the induction hypothesis; from the fact that type preservation
holds on the premise of the reduction, we have that

$\Gamma;\Delta^{\prime}\mathrel{\vdash}[\,P^{\prime}\,|\,B^{\prime}\,]\,|\\!|\,N^{\prime}$

and $\Delta\mathrel{\shortrightarrow}\Delta^{\prime}$. The latter results is
what needed to conclude type preservation for the reduction.

  * •

Rule [Def].

Assume

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}[\,P\,|\,B\,]\,|\\!|\,N\mathrel{\longrightarrow}[\,P^{\prime}\,|\,B^{\prime}\,]\,|\\!|\,N^{\prime}\end{array}}{\begin{array}[]{l}[\,\mathsf{def}\
\\{D_{i}(\tilde{x}_{i})\stackrel{{\scriptstyle\mathsf{def}}}{{=}}P_{i}\\}_{i\in
I}\ \mathsf{in}\ P\,|\,B\,]\,|\\!|\,N\mathrel{\longrightarrow}[\,\mathsf{def}\
\\{D_{i}(\tilde{x}_{i})\stackrel{{\scriptstyle\mathsf{def}}}{{=}}P_{i}\\}_{i\in
I}\ \mathsf{in}\ P^{\prime}\,|\,B^{\prime}\,]\,|\\!|\,N^{\prime}\end{array}}}\
\footnotesize\textsc{{[Def]}}\end{array}$

with

$\Gamma;\Delta\mathrel{\vdash}[\,\mathsf{def}\
\\{D_{i}(\tilde{x}_{i})\stackrel{{\scriptstyle\mathsf{def}}}{{=}}P_{i}\\}_{i\in
I}\ \mathsf{in}\ P\,|\,B\,]\,|\\!|\,N$

and $\Delta$ well-formed.

We produce the typing derivation of the latter judgement. We begin with the
typing derivation for network node $[\,\mathsf{def}\
\\{D_{i}(\tilde{x}_{i})\stackrel{{\scriptstyle\mathsf{def}}}{{=}}P_{i}\\}_{i\in
I}\ \mathsf{in}\ P\,|\,B\,]$:

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\begin{array}[]{l}\footnotesize\textsc{{[TRec]}}\\\
{\textstyle\frac{\begin{array}[]{c}\forall i\in
I,D_{i}(\tilde{x}_{i}):(\Gamma_{i},\Delta_{i})\in\Gamma\land\Gamma,\Gamma_{i};\Delta_{i}\mathrel{\vdash}P_{i}\quad\Gamma;\Delta_{1}^{\prime\prime}\mathrel{\vdash}P\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{1}^{\prime\prime}\mathrel{\vdash}\mathsf{def}\
\\{D_{i}(\tilde{x}_{i})\stackrel{{\scriptstyle\mathsf{def}}}{{=}}P_{i}\\}_{i\in
I}\ \mathsf{in}\ P\end{array}}}\end{array}\\\
\Gamma;\Theta\mathrel{\vdash}B\quad\Delta_{1}^{\prime}=\Delta_{1}^{\prime\prime}\circ\Theta\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{1}^{\prime}\mathrel{\vdash}[\,\mathsf{def}\
\\{D_{i}(\tilde{x}_{i})\stackrel{{\scriptstyle\mathsf{def}}}{{=}}P_{i}\\}_{i\in
I}\ \mathsf{in}\ P\,|\,B\,]\end{array}}}\
\footnotesize\textsc{{[TNode]}}\end{array}}\\\\[39.83385pt]
\Delta_{1}^{\prime}\mathrel{\hookrightarrow}\Delta_{0},\Delta_{1}\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{1}\mathrel{\vdash}[\,\mathsf{def}\
\\{D_{i}(\tilde{x}_{i})\stackrel{{\scriptstyle\mathsf{def}}}{{=}}P_{i}\\}_{i\in
I}\ \mathsf{in}\ P\,|\,B\,]\end{array}}}\
\footnotesize\textsc{{[TSynch]}}\end{array}}$

We type the entire network node $[\,\mathsf{def}\
\\{D_{i}(\tilde{x}_{i})\stackrel{{\scriptstyle\mathsf{def}}}{{=}}P_{i}\\}_{i\in
I}\ \mathsf{in}\ P\,|\,B\,]\,|\\!|\,N$:

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{0},\Delta_{1}\mathrel{\vdash}[\,\mathsf{def}\
\\{D_{i}(\tilde{x}_{i})\stackrel{{\scriptstyle\mathsf{def}}}{{=}}P_{i}\\}_{i\in
I}\ \mathsf{in}\ P\,|\,B\,]\\\
\Gamma;\Delta_{0},\Delta_{2}\mathrel{\vdash}N\quad\Delta_{0}\text{ only
$s$-endpoint
}\quad\Delta=\Delta_{0},\Delta_{1},\Delta_{2}\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}[\,\mathsf{def}\
\\{D_{i}(\tilde{x}_{i})\stackrel{{\scriptstyle\mathsf{def}}}{{=}}P_{i}\\}_{i\in
I}\ \mathsf{in}\ P\,|\,B\,]\,|\\!|\,N\end{array}}}\
\footnotesize\textsc{{[TPar]}}\end{array}$

We can use the above information to produce the typing derivation of the
network term $[\,P\,|\,B\,]\,|\\!|\,N$ in the premise of the reduction:

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}\footnotesize\textsc{{[TNode]}}\\\
{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{1}^{\prime\prime}\mathrel{\vdash}P\quad\Gamma;\Theta\mathrel{\vdash}B\quad\Delta_{1}^{\prime}=\Delta_{1}^{\prime\prime}\circ\Theta\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{1}^{\prime}\mathrel{\vdash}[\,P\,|\,B\,]\end{array}}}\end{array}}\quad\Delta_{1}^{\prime}\mathrel{\hookrightarrow}\Delta_{0},\Delta_{1}\\\\[25.60747pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{1}\mathrel{\vdash}[\,P\,|\,B\,]\end{array}}}\
\footnotesize\textsc{{[TSynch]}}\end{array}}\\\\[39.83385pt]
\Gamma;\Delta_{0},\Delta_{2}\mathrel{\vdash}N\quad\Delta_{0}\text{ only
$s$-endpoint }\quad\Delta=\Delta_{0},\Delta_{1},\Delta_{2}\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}[\,\mathsf{def}\
P\,|\,B\ \mathsf{in}\ \,|\\!|\,N\,]\end{array}}}\
\footnotesize\textsc{{[TPar]}}\end{array}}$

The results then comes from the induction hypothesis; the latter typing
derivation and the reduction on the premise of the case implies typing
derivation $\Gamma;\Delta^{\prime}\mathrel{\vdash}[\,\mathsf{def}\
P^{\prime}\,|\,B^{\prime}\ \mathsf{in}\ \,|\\!|\,N^{\prime}\,]$ and
$\Delta\mathrel{\shortrightarrow}\Delta^{\prime}$, which concludes the case.

  * •

Rule [TPar].

Assume

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}N\mathrel{\longrightarrow}N^{\prime}\end{array}}{\begin{array}[]{l}N\,|\\!|\,M\mathrel{\longrightarrow}N^{\prime}\,|\\!|\,M\end{array}}}\
\footnotesize\textsc{{[RPar]}}\end{array}$

with

$\Gamma;\Delta\mathrel{\vdash}N\,|\\!|\,M$

and $\Delta$ well-formed.

We provide with the typing derivation for the latter typing judgement.

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{0},\Delta_{1}\mathrel{\vdash}N\quad\Gamma;\Delta_{0},\Delta_{2}\mathrel{\vdash}M\\\
\mathrm{dom}(\Delta_{0})\text{ only
$s$-endpoints}\quad\Delta=\Delta_{0},\Delta_{1},\Delta_{2}\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}N\,|\\!|\,M\end{array}}}\
\footnotesize\textsc{{[TPar]}}\end{array}$

From the fact that $\Gamma;\Delta_{0},\Delta_{1}\mathrel{\vdash}N$, the
reduction, and the induction hypothesis we can conclude that
$\Gamma;\Delta^{\prime}\mathrel{\vdash}N$ and
$\Delta_{0},\Delta_{1}\mathrel{\shortrightarrow}\Delta^{\prime}$. It remains
to type the network term $N\,|\\!|\,M$ and show the Typing Preservation
requirements for $\Delta^{\prime}$. This can be analysed in several sub-cases.

    * –

$\Delta^{\prime}=\Delta_{0}^{\prime},\Delta_{1}^{\prime}$ with
$\Delta_{0}^{\prime}=\Delta_{0},\\{s_{i}:(c_{i},T_{i})\\}_{i\in I}$ and
$\Delta_{1}=\Delta_{1}^{\prime},\\{s_{j}:(c_{j},T_{j})\\}_{j\in J}$. This
implies derivation:

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{0}^{\prime},\Delta_{1}^{\prime}\mathrel{\vdash}N^{\prime}\quad\quad\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Delta_{0}=\Delta_{0}^{\prime},\Delta_{0}^{\prime\prime}\quad\Gamma;\Delta_{0},\Delta_{2}\mathrel{\vdash}M\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0}^{\prime},\Delta_{0}^{\prime\prime},\Delta_{2}\mathrel{\vdash}M\end{array}}}\end{array}\\\\[17.07164pt]
\begin{array}[]{l}\mathrm{dom}(\Delta_{0})\text{ only $s$-endpoints and
}\Delta_{0}^{\prime}\subseteq\Delta_{0}\text{ implies }\\\
\mathrm{dom}(\Delta_{0}^{\prime})\text{ only
$s$-endpoints}\end{array}\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0}^{\prime},\Delta_{0}^{\prime\prime},\Delta_{1}^{\prime},\Delta_{2}\mathrel{\vdash}N\,|\\!|\,M\end{array}}}\
\footnotesize\textsc{{[TPar]}}\end{array}}$

as required, because
$\Delta=\Delta_{0},\Delta_{1},\Delta_{2}\mathrel{\shortrightarrow}\Delta_{0}^{\prime},\Delta_{0}^{\prime\prime},\Delta_{1}^{\prime},\Delta_{2}=\Delta_{0},\Delta_{1}^{\prime},\Delta_{2}$

    * –

$\Delta^{\prime}=\Delta_{0},\Delta_{1}^{\prime}$ and
$\Delta_{1}\mathrel{\shortrightarrow}\Delta_{1}^{\prime}$ implies:

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{0},\Delta_{1}^{\prime}\mathrel{\vdash}N^{\prime}\quad\Gamma;\Delta_{0},\Delta_{2}\mathrel{\vdash}M\quad\mathrm{dom}(\Delta_{0})\text{
only
$s$-endpoints}\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0},\Delta_{1}^{\prime},\Delta_{2}\mathrel{\vdash}N\,|\\!|\,M\end{array}}}\
\footnotesize\textsc{{[TPar]}}\end{array}$

as required, because
$\Delta=\Delta_{0},\Delta_{1},\Delta_{2}\mathrel{\shortrightarrow}\Delta_{0},\Delta_{1}^{\prime},\Delta_{2}$.

    * –

$\Delta^{\prime}=\Delta_{0}^{\prime},\Delta_{1}^{\prime}$ with
$\Delta_{0},\Delta_{1}\mathrel{\shortrightarrow}\Delta_{0}^{\prime},\Delta_{1}^{\prime}$.
The latter assumption, the fact that $\mathrm{dom}(\Delta_{0})$ contains only
$s$-endpoints, and Linear Context Advancement (Definition 5) imply that
$\Delta_{0}=\Delta_{0}^{\prime\prime},s:(c,T)$ and
$\Delta_{1}=\Delta_{1}^{\prime\prime},\breve{s}:(c,\overline{T})$ and
furthermore $\Delta_{0}=\Delta_{0}^{\prime\prime},s:(c+1,T^{\prime})$ and
$\Delta_{1}^{\prime}=\Delta_{1}^{\prime\prime},\breve{s}:(c+1,\overline{T^{\prime}})$.
Note that $T\mathrel{\shortrightarrow}T^{\prime}$. These last equations allows
to type the resulting network of the reduction:

$\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta_{0},\Delta_{2}\mathrel{\vdash}M\quad\Delta_{0}=\Delta_{0}^{\prime\prime},s:(c,T)\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0}^{\prime\prime},s:(c,T),\Delta_{2}\mathrel{\vdash}M\end{array}}}\end{array}}\\\\[17.07164pt]
\boxed{\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Delta_{0}^{\prime\prime},\Delta_{2}\mathrel{\hookrightarrow}\Delta_{0}^{\prime\prime},\Delta_{2}\quad
T\mathrel{\shortrightarrow}^{c+1-c}T^{\prime}\end{array}}{\begin{array}[]{l}\Delta_{0}^{\prime\prime},s:(c,T),\Delta_{2}\mathrel{\hookrightarrow}\Delta_{0}^{\prime\prime},s:(c+1,T^{\prime}),\Delta_{2}\end{array}}}\end{array}}\\\\[17.07164pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0}^{\prime\prime},s:(c+1,T^{\prime}),\Delta_{2}\mathrel{\vdash}M\end{array}}}\
\footnotesize\textsc{{[TSynch]}}\end{array}}\\\\[51.21495pt]
\Gamma;\Delta_{0}^{\prime\prime},s:(c+1,T^{\prime}),\Delta_{1}^{\prime\prime},\breve{s}:(c+1,\overline{T^{\prime}})\mathrel{\vdash}N^{\prime}\\\
\mathrm{dom}(\Delta_{0}^{\prime\prime},s:(c+1,T^{\prime}))\text{ only
$s$-endpoints}\\\\[2.84526pt]
\end{array}}{\begin{array}[]{l}\Gamma;\Delta_{0}^{\prime\prime},s:(c+1,T^{\prime}),\Delta_{1}^{\prime\prime},\breve{s}:(c+1,\overline{T^{\prime}}),\Delta_{2}\mathrel{\vdash}N\,|\\!|\,M\end{array}}}\
\footnotesize\textsc{{[TPar]}}\end{array}}$

as required, because
$\Delta=\Delta_{0},\Delta_{1},\Delta_{2}\mathrel{\shortrightarrow}\Delta_{0}^{\prime},\Delta_{1}^{\prime},\Delta_{2}=\Delta_{0}^{\prime},s:(c+1,T^{\prime}),\Delta_{1}^{\prime\prime},\breve{s}:(c+1,\overline{T^{\prime}}),\Delta_{2}$.

    * –

$\Delta=\Delta_{0}^{\prime},\Delta_{1}$ and
$\Delta_{0}\mathrel{\shortrightarrow}\Delta_{0}^{\prime}$ cannot happen
because $\mathrm{dom}(\Delta_{0})$ has only $s$-endpoints.

  * •

Rule [RCong]. The result is immediate by applying Congruence Invariant (Lemma
8) on the induction hypothesis.

  * •

Rule [RRes].

Assume

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}N\mathrel{\longrightarrow}N^{\prime}\end{array}}{\begin{array}[]{l}(\nu\,n)N\mathrel{\longrightarrow}(\nu\,n)N^{\prime}\end{array}}}\
\footnotesize\textsc{{[RRes]}}\end{array}$

with

$\Gamma;\Delta\mathrel{\vdash}(\nu\,n)N$

and $\Delta$ well-formed.

There are two sub-cases for the typing derivation of the latter judgement:

    * –

$n=a$. Restrict shared name. In this sub-case the typing derivation for
network term $(\nu\,a)N$ is as:

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma,a:T;\Delta\mathrel{\vdash}N\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}(\nu\,a)N\end{array}}}\
\footnotesize\textsc{{[TCRes]}}\end{array}$

From $\Gamma,a:T;\Delta\mathrel{\vdash}N$, well-formed $\Delta$, and the
induction hypothesis we conclude that
$\Gamma,a:T;\Delta^{\prime}\mathrel{\vdash}N^{\prime}$ and either
$\Delta^{\prime}\subseteq\Delta$ or
$\Delta\mathrel{\shortrightarrow}\Delta^{\prime}$. From the last typing
judgement we can type the result of the reduction $(\nu\,a)N$:

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma,a:T;\Delta^{\prime}\mathrel{\vdash}N^{\prime}\end{array}}{\begin{array}[]{l}\Gamma;\Delta^{\prime}\mathrel{\vdash}N^{\prime}\end{array}}}\
\footnotesize\textsc{{[TCRes]}}\end{array}$

to conclude the sub-case.

    * –

$n=s$. Restrict session name. In this sub-case the typing derivation for
network term $(\nu\,s)N$ is as:

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta,\Delta^{\prime\prime\prime},\breve{s}:(c,T)\mathrel{\vdash}N\quad\Delta^{\prime\prime\prime}=s:(c,\overline{T})\lor\Delta^{\prime\prime\prime}=\emptyset\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}(\nu\,s)N\end{array}}}\
\footnotesize\textsc{{[TSRes]}}\end{array}$

Typing context $\Delta,\breve{s}:(c,T)$ is well-formed because $\Delta$ is
well-formed, see well-formedmess Definition 5.

From $\Gamma;\Delta,\breve{s}:(c,T),s:(c,\overline{T})\mathrel{\vdash}N$,
well-formed $\Delta,\breve{s}:(c,T),s:(c,\overline{T})$, and the induction
hypothesis we conclude that $\Gamma;\Delta^{\prime}\mathrel{\vdash}N^{\prime}$
and
$\Delta,\breve{s}:(c,T),s:(c,\overline{T})\mathrel{\shortrightarrow}\Delta^{\prime}$.
All it remains is to conclude te case, is the typing derivation of the result
of the reduction $(\nu\,s)N^{\prime}$.

If
$\Delta,\breve{s}:(c,T),s:(c,\overline{T})\mathrel{\shortrightarrow}\Delta^{\prime}$
then there are two sub-cases:

      * *

$\Delta^{\prime}=\Delta^{\prime\prime},\breve{s}:(c,T),s:(c,\overline{T})$
with $\Delta\mathrel{\shortrightarrow}\Delta^{\prime\prime}$, which implies

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta^{\prime\prime},\breve{s}:(c,T),s:(c,\overline{T})\mathrel{\vdash}N^{\prime}\end{array}}{\begin{array}[]{l}\Gamma;\Delta^{\prime\prime}\mathrel{\vdash}(\nu\,s)N^{\prime}\end{array}}}\
\footnotesize\textsc{{[TSRes]}}\end{array}$

as required.

      * *

$\Delta^{\prime}=\Delta,\breve{s}:(c,T),s:(c,\overline{T})$ with
$\breve{s}:(c,T),s:(c,\overline{T})\mathrel{\shortrightarrow}\breve{s}:(c+1,T_{1}),s:(c+1,T_{2})$,
which implies

$\begin{array}[]{l}{\textstyle\frac{\begin{array}[]{c}\Gamma;\Delta,\breve{s}:(c+1,T^{\prime}),s:(c+1,\overline{T^{\prime}})\mathrel{\vdash}(\nu\,n)N^{\prime}\\\
\text{From the definition of $\mathrel{\shortrightarrow}$ we get that
}T_{1}^{\prime}=\overline{T}_{2}^{\prime}\end{array}}{\begin{array}[]{l}\Gamma;\Delta\mathrel{\vdash}(\nu\,s)N^{\prime}\end{array}}}\
\footnotesize\textsc{{[TSRes]}}\end{array}$

as required.