$\Delta,t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]:T,\Gamma_{2},\dots,\Gamma_{h}\vdash^{1+n^{\prime}+\sum_{i=2}^{h}n_{i}}(s)(R\mathbin{\mid}\overline{P})$
with an application of [t-par]. We conclude with an application of [t-cast] by
taking $m\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}n$.

Case [s-call]. Then $P=A\langle\overline{u}\rangle\preccurlyeq
R\\{\overline{u}/\overline{x}\\}=Q$ and
$A(\overline{x})\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}R$.
From [t-call] we conclude that there exist $\overline{S}$ and $m$ such that
$A:[\overline{S};m]$ and $\Gamma=\overline{u:S}$ and
$\overline{u:S}\vdash^{m}Q$ and $m\leq n$.

######  Lemma C.5 (Subject Reduction).

If $\Gamma\vdash^{n}P$ and $P\rightarrow Q$, then $\Gamma\vdash^{m}Q$ for some
$m$.

######  Proof C.6.

By induction on the derivation of $P\rightarrow Q$ and by cases on the last
rule applied.

Case [r-choice]. Then $P=P_{1}\oplus P_{2}\rightarrow P_{k}=Q$ and
$k\in\\{1,2\\}$. From [t-choice] we deduce that $\Gamma\vdash^{m}Q$ for some
$m$.

Case [r-signal]. Then
$P=(s)(\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}].{Q}\mathrel{|}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{1}]\mathrel{|}\cdots\mathrel{|}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{h}])\rightarrow
Q$. From [t-par], [t-wait] and [t-close] we deduce that there exist $m$ and
$n_{i}$ for $i=1,\dots,h$ such that

  * •

$n=1+m+\sum_{i=1}^{h}n_{i}$

  * •

$\Gamma,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]:{?}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}\vdash^{m}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}].{Q}$

  * •

$\Gamma\vdash^{m}Q$

  * •

$s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i}]:{!}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}\vdash^{n_{i}}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i}]$
for $i=1,\dots,h$

There is nothing left to prove.

Case [r-channel]. Then
$P=(s)(s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]\mathsf{!}v.P^{\prime}\mathrel{|}s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\mathsf{?}(x).Q^{\prime}\mathrel{|}\overline{R})\rightarrow(s)(P^{\prime}\mathrel{|}Q^{\prime}\\{v/x\\}\mathrel{|}\overline{R})=Q$.
From [t-par] we deduce that there exist
$\Gamma_{i},S_{i},\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i},n_{i}$
for $i=1,\dots,h$ such that

  * •

$\Gamma=\Gamma_{1},\dots,\Gamma_{h}$

  * •

$n=1+\sum_{i=1}^{h}n_{i}$

  * •

$\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$

  * •

$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}$
and
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}$

  * •

$\Gamma_{1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]:S_{1}\vdash^{n_{1}}s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]\mathsf{!}v.P^{\prime}$

  * •

$\Gamma_{2},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]:S_{2}\vdash^{n_{2}}s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\mathsf{?}(x).Q^{\prime}$

  * •

$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vdash^{n_{i}}R_{i}$
for $i=3,\dots,h$

From [t-channel-out] and [t-channel-in] we deduce that there exist
$S_{v},T_{1},T_{2},\Delta_{1}$ such that

  * •

$S_{1}=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}{!}{S_{v}}.T_{1}$

  * •

$\Gamma_{1}=\Delta_{1},v:S_{v}$

  * •

$\Delta_{1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]:T_{1}\vdash^{n_{1}}P^{\prime}$

  * •

$S_{2}=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}{?}{S_{v}}.T_{2}$

  * •

$\Gamma_{2},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]:T_{2},x:S_{v}\vdash^{n_{2}}Q^{\prime}$

Using Lemma C.1 we deduce
$\Gamma_{2},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]:T_{2},v:S_{v}\vdash^{n_{2}}Q^{\prime}\\{v/x\\}$.
Using Definition 4.2 we deduce
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{T_{1}}\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}\triangleright{T_{2}}\mathrel{|}\prod_{i=3}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$. We conclude with one application of [t-par] taking
$m\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}n$.

Case [r-pick]. Then
$P=(s)(s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]\mathsf{!}\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.P_{i}\\}_{i\in
I}\mathrel{|}\overline{Q})\rightarrow(s)(s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{k}.P_{k}\mathrel{|}\overline{Q})=Q$
and $k\in I$. From [t-par] we deduce that there exist
$\Gamma_{i},\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i},n_{i},S_{i}$
for $i=1,\dots,h$ such that

  * •

$\Gamma=\Gamma_{1},\dots,\Gamma_{h}$

  * •

$n=1+\sum_{i=1}^{h}n_{i}$

  * •

$\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$

  * •

$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}$
and
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}$
for some $i\in\\{2,\dots,h\\}$

  * •

$\Gamma_{1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]:S_{1}\vdash^{n_{1}}s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]\mathsf{!}\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.P_{i}\\}_{i\in
I}$

  * •

$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vdash^{n_{i}}Q_{i}$
for $i=2,\dots,h$

From [t-tag] we deduce that there exist $T_{i}$ for all $i\in I$ such that

  * •

$S_{1}=\sum_{i\in
I}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.T_{i}$

  * •

$\Gamma_{1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]:T_{i}\vdash^{n_{1}}P_{i}\leavevmode\nobreak\
{}^{(i\in I)}$

From the hypothesis that $k\in I$ we deduce that
$\Gamma_{1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]:T_{k}\vdash^{n_{1}}P_{k}$
and from [t-tag] we deduce
$\Gamma_{1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]:\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{k}.T_{k}\vdash^{n_{1}}s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{k}.P_{k}$.
From Definition 4.2 we deduce that
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{k}.T_{k}\mathrel{|}\prod_{i=2}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$. We conclude with an application of [t-par] taking
$m\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}n$.

Case [r-tag]. Then
$P=(s)(s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{k}.P^{\prime}\mathrel{|}s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\mathsf{?}\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.Q_{i}\\}_{i\in
I}\mathrel{|}\overline{R})\rightarrow(s)(P^{\prime}\mathrel{|}Q_{k}\mathrel{|}\overline{R})=Q$
and $k\in I$. From [t-par] we deduce that there exist
$\Gamma_{i},S_{i},\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i},n_{i}$
for $i=1,\dots,h$ such that

  * •

$\Gamma=\Gamma_{1},\dots,\Gamma_{h}$

  * •

$n=1+\sum_{i=1}^{h}n_{i}$

  * •

$\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$

  * •

$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}$
and
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}$

  * •

$\Gamma_{1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]:S_{1}\vdash^{n_{1}}s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]\mathsf{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{k}.P^{\prime}$

  * •

$\Gamma_{2},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]:S_{2}\vdash^{n_{2}}s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\mathsf{?}\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.Q_{i}\\}_{i\in
I}$

  * •

$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vdash^{n_{i}}R_{i}$
for $i=3,\dots,h$

From [t-tag] we deduce that there exist $S^{\prime}_{1}$ and $T_{i}$ for every
$i\in I$ such that

  * •

$S_{1}=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{k}.S^{\prime}_{1}$

  * •

$\Gamma_{1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]:S^{\prime}_{1}\vdash^{n_{1}}P^{\prime}$

  * •

$S_{2}=\sum_{i\in
I}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.T_{i}$

  * •

$\Gamma_{2},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]:T_{i}\vdash^{n_{2}}Q_{i}\leavevmode\nobreak\
{}^{(i\in I)}$

From Definition 4.2 we deduce that
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{S^{\prime}_{1}}\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}\triangleright{T_{k}}\mathrel{|}\prod_{i=2}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$. We conclude with an application of [t-par] by taking
$m\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}n$.

Case [r-par]. Then
$P=(s)(P^{\prime}\mathrel{|}\overline{R})\rightarrow(s)(Q^{\prime}\mathrel{|}\overline{R})=Q$
and $P^{\prime}\rightarrow Q^{\prime}$. From [t-par] we deduce that there
exist
$\Gamma_{i},\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i},S_{i},n_{i}$
for $i=1,\dots,h$ such that

  * •

$\Gamma=\Gamma_{1},\dots,\Gamma_{h}$

  * •

$n=1+\sum_{i=1}^{h}n_{i}$

  * •

$\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$

  * •

$\Gamma_{1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}]:S_{1}\vdash^{n_{1}}P^{\prime}$

  * •

$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vdash^{n_{i}}R_{i}$
for $i=2,\dots,h$

Using the induction hypothesis on
$\Gamma_{1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}]:S_{1}\vdash^{n_{1}}P^{\prime}$
and $P^{\prime}\rightarrow Q^{\prime}$ we deduce
$\Gamma_{1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}]:S_{1}\vdash^{n^{\prime}_{1}}Q^{\prime}$
for some $n^{\prime}_{1}$. We conclude with an application of [t-par] taking
$m\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}1+n^{\prime}_{1}+\sum_{i=2}^{h}n_{i}$.

Case [r-cast]. Then $P=\lceil u\rceil{P^{\prime}}\rightarrow\lceil
u\rceil{Q^{\prime}}=Q$ and $P^{\prime}\rightarrow Q^{\prime}$. From [t-cast]
we deduce that there exist $S,T,\Gamma^{\prime},n^{\prime},m_{u}$ such that

  * •

$\Gamma=\Gamma^{\prime},u:S$

  * •

$S\leqslant_{m_{u}}T$

  * •

$n=m_{u}+n^{\prime}$

  * •

$\Gamma^{\prime},u:T\vdash^{n^{\prime}}P^{\prime}$

Using the induction hypothesis on
$\Gamma^{\prime},u:T\vdash^{n^{\prime}}P^{\prime}$ and $P^{\prime}\rightarrow
Q^{\prime}$ we deduce $\Gamma^{\prime},u:T\vdash^{m^{\prime}}Q^{\prime}$ for
some $m^{\prime}$. We conclude with an application of [t-cast] taking
$m\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}m_{u}+m^{\prime}$.

Case [r-struct]. Then $P\preccurlyeq P^{\prime}\rightarrow
Q^{\prime}\preccurlyeq Q$. From Lemma C.3 we deduce that
$\Gamma\vdash^{n^{\prime}}P^{\prime}$ for some $n^{\prime}\leq n$. Using the
induction hypothesis on $\Gamma\vdash^{n^{\prime}}P^{\prime}$ and
$P^{\prime}\rightarrow Q^{\prime}$ we deduce
$\Gamma\vdash^{m^{\prime}}Q^{\prime}$ for some $m^{\prime}$. We conclude using
Lemma C.3 once more.

###  C.2 Measure

######  Definition C.7 (rank).

The _rank_ of a session map
$M=\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}$,
written $\|M\|$, is the element of $\mathbb{N}\cup\\{\infty\\}$ defined as

$\|M\|\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\min|M\stackrel{{\scriptstyle{?}\checkmark}}{{\Longrightarrow}}|$

where $|M\stackrel{{\scriptstyle\alpha}}{{\Longrightarrow}}N|$ denotes the
length of the sequence $\tau,\dots,\tau,\alpha$ and we postulate that
$\min\emptyset=\infty$.

######  Definition C.8 (Measure).

The measure of a process is a lexicographically ordered pair of natural
numbers $(m,n)$ where:

  * •

$m$ is an upper bound to the number of sessions that the process may open and
of weights of casts that the process may perform _in the future_ before it
terminates;

  * •

$n$ is the overall effort for terminating the sessions that have been already
opened _in the past_ , _i.e._ the sum of their rank (Definition C.7).

We now introduce a refined set of typing rules for processes that allow us to
associate them with their measure, not just with their rank.

$\displaystyle{\vbox{\hbox{\hypertarget{rule:mt-thread}{{{\small[mt-
thread]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
17.51016pt\vbox{\vbox{}\hbox{\hskip-17.51015pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vDash^{(n,0)}P$}}}}}}$}}}\Gamma\vdash^{n}P\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt{\vbox{\hbox{\hypertarget{rule:mt-
cast}{{{\small[mt-cast]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
25.47295pt\vbox{\hbox{\hskip-25.47293pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,u:T\vDash^{\mu}P$}}}\vbox{}}}\over\hbox{\hskip
40.7315pt\vbox{\vbox{}\hbox{\hskip-40.7315pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,u:S\vDash^{\mu+(n,0)}\lceil
u\rceil P$}}}}}}$}}}\leavevmode\nobreak\ S\leqslant_{n}T\penalty 50\hskip
20.00003pt plus 0.5fil minus 5.0pt{\vbox{\hbox{\hypertarget{rule:mt-
par}{{{\small[mt-par]}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
48.31328pt\vbox{\hbox{\hskip-48.31328pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vDash^{\mu_{i}}P_{i}\leavevmode\nobreak\
{}^{(i=1,\dots,h)}$}}}\vbox{}}}\over\hbox{\hskip
80.65053pt\vbox{\vbox{}\hbox{\hskip-80.65051pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma_{1},\dots,\Gamma_{h}\vDash^{\sum_{i=1}^{h}\mu_{i}+(0,\|\\{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\\}_{i=1,\dots,h}\|)}(s)(P_{1}\mathrel{|}\dots\mathrel{|}P_{h})$}}}}}}$}}}\leavevmode\nobreak\
{\\#}{\\{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\\}_{i=1..h}}$

The idea behind these rules is that they distinguish between _past_ and
_future_ of a process by looking at its structure. Indeed, unguarded sessions
have been created, casts have not been performed yet and sessions that occur
guarded have not been created yet. [mt-thread] adopts the rank of the process
inside the usual typing judgment (Table 6) as first component of the measure.
This rule has lower priority with respect to the other rules so that it is
applied to processes that are not casts or restrictions. In [mt-cast] the
first component of the measure is increased by the weight of the cast. [mt-
par] increases the second component of the measure by the rank of the involved
session.

######  Lemma C.9.

The following properties hold:

  1. 1.

$\Gamma\vdash^{n}P$ implies $\Gamma\vDash^{\mu}P$ for some $\mu\leq(n,0)$;

  2. 2.

$\Gamma\vDash^{\mu}P$ implies $\Gamma\vdash^{n}P$ for some $n$ such that
$\mu\leq(n,0)$.

######  Proof C.10.

We prove item 1 by induction on the structure of $P$. The proof of item 2 is
by a straightforward induction over $\Gamma\vDash^{\mu}P$.

Case $P=(s)(\overline{P})$. From [t-par] we deduce that there exist
$\Gamma_{i},\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i},S_{i},n_{i}$
for $i=1,\dots,h$ such that

  * •

$\Gamma=\Gamma_{1},\dots,\Gamma_{h}$

  * •

$n=1+\sum_{i=1}^{h}n_{i}$

  * •

$\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$

  * •

$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vdash^{n_{i}}P_{i}\leavevmode\nobreak\
{}^{(i=1,\dots,h)}$

Using the induction hypothesis on
$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vdash^{n_{i}}P_{i}\leavevmode\nobreak\
{}^{(i=1,\dots,h)}$ we deduce that there exist $\mu_{i}$ for $i=1,\dots,h$
such that

  * •

$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vDash^{\mu_{i}}P_{i}\leavevmode\nobreak\
{}^{(i=1,\dots,h)}$

  * •

$\mu_{i}\leq(n_{i},0)$ for $i=1,\dots,h$

We conclude with one application of [mt-par] by taking
$\mu\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\sum_{i=1}^{h}\mu_{i}+(0,\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)$
and observing that $\mu<(n_{1},0)+(n_{2},0)+\dots+(n_{h},0)+(1,0)=(n,0)$.

Case $P=\lceil u\rceil{Q}$. From [t-cast] we deduce that there exist
$\Delta,S,T,m,m_{u}$ such that

  * •

$\Gamma=\Delta,u:S$

  * •

$S\leqslant_{m_{u}}T$

  * •

$n=m_{u}+m$

  * •

$\Delta,u:T\vdash^{m}Q$

Using the induction hypothesis on $\Delta,u:T\vdash^{m}Q$ we deduce
$\Delta,u:T\vDash^{\nu}Q$ for some $\nu\leq(m,0)$. We conclude with an
application of [mt-cast] by taking $\mu\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\nu+(m_{u},0)$ and observing that $\mu\leq(m,0)+(m_{u},0)=(n,0)$.

In all the other cases. We conclude with an application of [mt-thread] by
taking $\mu\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}(n,0)$.

######  Lemma C.11.

If $\Gamma\vDash^{\mu}P$ and $P\preccurlyeq Q$, then there exists $\nu\leq\mu$
such that $\Gamma\vDash^{\nu}Q$.

######  Proof C.12.

By induction on the derivation of $P\preccurlyeq Q$ and by cases on the last
rule applied. We only consider the base cases.

Case [s-par-comm]. Then
$P=(s)(\overline{P}\mathbin{\mid}P^{\prime}\mathbin{\mid}Q^{\prime}\mathbin{\mid}\overline{Q})\preccurlyeq(s)(\overline{P}\mathbin{\mid}Q^{\prime}\mathbin{\mid}P^{\prime}\mathbin{\mid}\overline{Q})=Q$.
From rule [mt-par] we deduce that there exist
$\Gamma_{i},\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i},S_{i},\mu_{i}$
for $i=1,\dots,h$ such that

  * •

$\Gamma=\Gamma_{1},\dots,\Gamma_{h}$

  * •

$\mu=\sum_{i=1}^{h}\mu_{i}+(0,\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)$

  * •

$\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$

  * •

$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vDash^{\mu_{i}}P_{i}$
for $i=1,\dots,k$

  * •

$\Gamma_{k+1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{k+1}]:S_{k+1}\vDash^{\mu_{k+1}}P^{\prime}$

  * •

$\Gamma_{k+2},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{k+2}]:S_{k+2}\vDash^{\mu_{k+2}}Q^{\prime}$

  * •

$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vDash^{\mu_{i}}Q_{i}$
for $i=k+3,\dots,h$

We conclude $\Gamma\vDash^{\nu}Q$ with one application of [mt-par] by taking
$\nu\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}\mu$.

Case [s-par-assoc]. Then
$P=(s)(\overline{P}\mathbin{\mid}(t)(R\mathbin{\mid}\overline{Q}))\preccurlyeq(t)((s)(\overline{P}\mathbin{\mid}R)\mathbin{\mid}\overline{Q})=Q$
and $s\in\mathsf{fn}(R)$. From rule [mt-par] we deduce that there exist
$\Gamma_{i},\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i},S_{i},\mu_{i}$
for $i=1,\dots,h$ such that

  * •

$\Gamma=\Gamma_{1},\dots,\Gamma_{h}$

  * •

$\mu=\sum_{i=1}^{h}\mu_{i}+(0,\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)$

  * •

$\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$

  * •

$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vDash^{\mu_{i}}P_{i}$
for $i=1,\dots,h-1$

  * •

$\Gamma_{h},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{h}]:S_{h}\vDash^{\mu_{h}}(t)(R\mathbin{\mid}\overline{Q})$

From rule [mt-par] and the hypothesis that $s\in\mathsf{fn}(R)$ we deduce that
there exist
$\Delta_{i},\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i},T_{i},\nu_{i}$
for $i=1,\dots,k$ such that

  * •

$\Gamma_{h}=\Delta_{1},\dots,\Delta_{k}$

  * •

$\mu_{h}=\sum_{1}^{k}\nu_{i}+(0,\|\prod_{i=1}^{k}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i}\triangleright{T_{i}}\|)$

  * •

$\prod_{i=1}^{k}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i}\triangleright{T_{i}}\leavevmode\nobreak\
\text{coherent}$

  * •

$\Delta_{1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{h}]:S_{h},t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{1}]:T_{1}\vDash^{\nu_{1}}R$

  * •

$\Delta_{i+1},t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i+1}]:T_{i+1}\vDash^{\nu_{i+1}}Q_{i}$
for $i=1,\dots,k-1$

Using [t-par] we deduce
$\Gamma_{1},\dots,\Gamma_{h-1},\Delta_{1},t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{1}]:T_{1}\vDash^{\sum_{i=1}^{h-1}{\mu_{i}}+\nu_{1}+\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|}(s)(\overline{P}\mathbin{\mid}R)$.
We conclude
$\Gamma\vDash^{\nu}(t)((s)(\overline{P}\mathbin{\mid}R)\mathbin{\mid}\overline{Q})$
with another application of [mt-par] by taking
$\nu\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}\mu$.

Case [s-cast-comm]. Then $P=\lceil u\rceil{\lceil
v\rceil{R}}\preccurlyeq\lceil v\rceil{\lceil u\rceil{R}}=Q$. We can assume
$u\neq v$ or else $P=Q$. From rule [mt-cast] we deduce that there exist
$\Gamma_{1},S,T,\mu_{1},m_{u}$ such that

  * •

$\Gamma=\Gamma_{1},u:S$

  * •

$S\leqslant_{m_{u}}T$

  * •

$\mu=\mu_{1}+(m_{u},0)$

  * •

$\Gamma_{1},u:T\vDash^{\mu_{1}}\lceil v\rceil{R}$

From rule [t-cast] we deduce that there exist
$\Gamma_{2},S^{\prime},T^{\prime},\mu_{2},m_{v}$ such that

  * •

$\Gamma_{1}=\Gamma_{2},v:S^{\prime}$

  * •

$S^{\prime}\leqslant_{m_{v}}T^{\prime}$

  * •

$\mu_{1}=\mu_{2}+(m_{v},0)$

  * •

$\Gamma_{2},u:T,v:T^{\prime}\vDash^{\mu_{2}}R$

We derive $\Gamma_{2},u:S,v:T^{\prime}\vDash^{\mu_{2}+(m_{u},0)}\lceil
u\rceil{R}$ with one application of [mt-cast] and we conclude with another
application of [mt-cast] by taking $\nu\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\mu$.

Case [s-cast-new]. Then $P=(s)(\lceil
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\rceil{R}\mathbin{\mid}\overline{P})\preccurlyeq(s)(R\mathbin{\mid}\overline{P})=Q$.
From rule [mt-par] we deduce that there exist $\Delta,\mu^{\prime},S$ and
$\Gamma_{i},\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i},S_{i},\mu_{i}$
for $i=1,\dots,h$ such that

  * •

$\Gamma=\Delta,\Gamma_{1},\dots,\Gamma_{h}$

  * •

$\mu=\mu^{\prime}+\sum_{i=1}^{h}\mu_{i}+(0,\|\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{S}\mathbin{\mid}\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i}\triangleright{S_{i}}\|)$

  * •

$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{S}\mathrel{|}\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$

  * •

$\Delta,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]:S\vDash^{\mu^{\prime}}\lceil
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\rceil{R}$

  * •

$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i}]:S_{i}\vDash^{\mu_{i}}P_{i}$
for $i=1,\dots,h$

From rule [mt-cast] we deduce that there exist $T,\nu^{\prime},m_{s}$ such
that

  * •

$S\leqslant_{m_{s}}T$

  * •

$\nu^{\prime}=\mu^{\prime}+(m_{s},0)$

  * •

$\Delta,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]:T\vDash^{\nu^{\prime}}R$

From
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{S}\mathbin{\mid}\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$, $S\leqslant_{m_{s}}T$ and Definition 4.4 we deduce
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{T}\mathbin{\mid}\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$. We conclude with an application of [mt-par] by taking
$\nu=\nu^{\prime}+\sum_{i=1}^{h}\mu_{i}+(0,\|\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}\triangleright{S}\mathbin{\mid}\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i}\triangleright{S_{i}}\|)\leq
n$.

Case [s-cast-swap]. Then $P=(s)(\lceil
t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\rceil{R}\mathbin{\mid}\overline{P})\preccurlyeq\lceil
t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\rceil{(s)(R\mathbin{\mid}\overline{P})}=Q$
and $t\neq s$. From rule [mt-par] we deduce that there exist
$\Gamma_{i},\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i},\mu_{i}$
for $i=1,\dots,h$ such that

  * •

$\Gamma=\Gamma_{1},\dots,\Gamma_{h}$

  * •

$\mu=\sum_{i=1}^{h}\mu_{i}+(0,\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i}\triangleright{S_{i}}\|)$

  * •

$\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$

  * •

$\Gamma_{1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{1}]:S_{1}\vDash^{\mu_{1}}\lceil
t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\rceil{R}$

  * •

$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i}]:S_{i}\vDash^{\mu_{i}}P_{i}$
for $i=2,\dots,h$

From rule [mt-cast] we deduce that there exist $\Delta,T,\mu^{\prime},m_{t}$
such that

  * •

$\Gamma_{1}=\Delta,t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]:S$

  * •

$S\leqslant_{m_{t}}T$

  * •

$\mu_{1}=\mu^{\prime}+(m_{t},0)$

  * •

$\Delta,t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]:T,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{1}]:S_{1}\vDash^{\mu^{\prime}}R$

We derive
$\Delta,t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]:T,\Gamma_{2},\dots,\Gamma_{h}\vDash^{\mu^{\prime}+\sum_{i=2}^{h}\mu_{i}+(0,\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}_{i}\triangleright{S_{i}}\|)}(s)(R\mathbin{\mid}\overline{P})$
with an application of [mt-par]. We conclude with an application of [mt-cast]
by taking $m\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}n$.

Case [s-call]. Then $P=A\langle\overline{u}\rangle\preccurlyeq
R\\{\overline{x}/\overline{u}\\}=Q$ and
$A(\overline{x})\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}R$.
From [mt-thread] we deduce that $\Gamma\vDash^{n}A\langle\overline{u}\rangle$
for some $n$ such that $\mu=(n,0)$. Using Lemma C.3 we deduce
$\Gamma\vdash^{m}Q$ for some $m\leq n$. Using Lemma C.9 we deduce that
$\Gamma\vDash^{\nu}Q$ for some $\nu\leq(m,0)$. We conclude observing that
$\nu\leq(m,0)\leq(n,0)=\mu$.

###  C.3 Normal Forms

We introduce _process contexts_ to easily refer to unguarded sub-processes:

$\textbf{Process context}\quad\mathcal{C},\mathcal{D}\leavevmode\nobreak\
\leavevmode\nobreak\ ::=\leavevmode\nobreak\ \leavevmode\nobreak\
[\leavevmode\nobreak\
]\mid(s)(\overline{P}\mathrel{|}\mathcal{C}\mathrel{|}\overline{Q})\mid\lceil
u\rceil\mathcal{C}$

######  Definition C.13 (Choice Normal Form).

We say that $P_{1}\oplus P_{2}$ is an _unguarded choice_ of $P$ if there
exists $\mathcal{C}$ such that $P\preccurlyeq\mathcal{C}[P_{1}\oplus P_{2}]$.
We say that $P$ is in _choice normal form_ if it has no unguarded choices.

######  Definition C.14 (Thread Normal Form).

A process is in _thread normal form_ if it is generated by the grammar below:

$\begin{array}[]{@{}rcl@{}}P^{\mathit{nf}},Q^{\mathit{nf}}&::=&\lceil u\rceil
P^{\mathit{nf}}\mid P^{\mathit{par}}\\\
P^{\mathit{par}},Q^{\mathit{par}}&::=&(s)(\overline{P^{\mathit{par}}})\mid
P^{\mathit{th}}\\\
P^{\mathit{th}}&::=&\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}\mid\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,u\mid\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,u.{P}\mid
u[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\pi\\{l_{i}.P_{i}\\}_{i\in
I}\mid
u[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\mathsf{!}v.P\mid
u[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\mathsf{?}(x).P\end{array}$

Intuitively, a process is in _thread normal form_ if it consists of an initial
prefix of casts followed by a parallel composition of threads, where a thread
is either done or a process waiting to perform an input/output action on some
channel
$u=s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]$
for some
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}$.
In this latter case, we say that the thread is an $s$-thread.

######  Definition C.15 (Proximity Normal Form).

We say that $P^{\mathit{nf}}$ is in _proximity normal form_ if
$P^{\mathit{nf}}=\mathcal{C}[(s)(\overline{P^{\mathit{th}}})]$ for some
$\mathcal{C}$, $s$, $\overline{P^{\mathit{th}}}$ where each
$P^{\mathit{th}}_{i}$ for $i=1,\dots,h$ is a $s$-thread.

######  Lemma C.16.

If $\Gamma\vdash^{n}P$ and $\Gamma\vdash_{\mathsf{ind}}P$, then there exists
$Q$ in choice normal form such that $P\Rightarrow Q$ and $\Gamma\vdash^{m}Q$
for some $m\leq n$.

######  Proof C.17.

By induction on $\Gamma\vdash_{\mathsf{ind}}P$ and by cases on the last rule
applied.

Case $P$ is already in choice normal form. We conclude taking
$Q\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}P$ and
$m\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}n$.

Case [t-call]. Then $P=A\langle\overline{u}\rangle$ and
$A(\overline{x})\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}R$.
We deduce $\Gamma=\overline{u:S}$, $A:[\overline{S};n^{\prime}]$ and
$\Gamma\vdash_{\mathsf{ind}}R\\{\overline{u}/\overline{x}\\}$. Moreover, it
must be the case that
$\Gamma\vdash^{n^{\prime}}R\\{\overline{u}/\overline{x}\\}$ and
$n^{\prime}\leq n$ since [t-call] is used in the coinductive judgment as well.
Using the induction hypothesis we deduce that there exist $Q$ in choice normal
form and $m\leq n^{\prime}$ such that
$R\\{\overline{u}/\overline{x}\\}\Rightarrow Q$ and $\Gamma\vdash^{m}Q$. We
conclude by observing that $P\Rightarrow Q$ using [r-struct] and that $m\leq
n^{\prime}\leq n$.

Case [co-choice]. Then $P=P_{1}\oplus P_{2}$. We deduce
$\Gamma\vdash_{\mathsf{ind}}P_{k}$ with $k\in\\{1,2\\}$. Moreover, it must be
the case that $\Gamma\vdash^{n}P_{k}$ since [t-choice] is used in the
coinductive judgment. Using the induction hypothesis we deduce that there
exist $Q$ in choice normal form and $m\leq n$ such that $P_{k}\Rightarrow Q$
and $\Gamma\vdash^{m}Q$. We conclude by observing that $P\rightarrow P_{k}$ by
[r-choice].

Case [t-choice]. Analogous to the previous case but we consider the premise in
which the rank is the same of the conclusion to keep sure that it does not
increase.

Case [t-par]. Then $P=(s)(P_{1}\mathrel{|}\dots\mathrel{|}P_{h})$. We deduce

  * •

$\Gamma=\Gamma_{1},\dots,\Gamma_{h}$

  * •

$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vdash_{\mathsf{ind}}P_{i}$
for $i=1,\dots,h$

  * •

$\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$

Furthermore, it must be the case that
$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vdash^{n_{i}}P_{i}$
for $i=1,\dots,h$ and $n=1+\sum_{i=1}^{h}n_{i}$ since [t-par] is used in the
coinductive judgment as well. Using the induction hypothesis we deduce that
there exist $Q_{i}$ in choice normal form and $m_{i}\leq n_{i}$ such that
$P_{i}\Rightarrow Q_{i}$ and
$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vdash^{m_{i}}Q_{i}$
for $i=1,\dots,h$. We conclude by taking
$m\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}1+\sum_{i=1}^{h}m_{i}$ and
$Q\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}(s)(Q_{1}\mathrel{|}\cdots\mathrel{|}Q_{h})$ with one application
of [t-par], observing that $m=1+\sum_{i=1}^{h}m_{i}\leq
1+\sum_{i=1}^{h}n_{i}=n$ and that $P\Rightarrow Q$ by [r-par].

Case [t-cast]. Then $P=\lceil u\rceil P^{\prime}$. Analogous to the previous
case, just simpler.

######  Lemma C.18.

If $\Gamma\vdash^{n}P$, then there exists $Q$ in choice normal form such that
$P\Rightarrow Q$ and $\Gamma\vdash^{m}Q$ for some $m\leq n$.

######  Proof C.19.

Consequence of Lemma C.16 noting that $\Gamma\vdash^{n}P$ implies
$\Gamma\vdash_{\mathsf{ind}}P$.

######  Lemma C.20.

If $\Gamma\vDash^{\mu}P$, then there exist $Q$ in choice normal form and
$\nu\leq\mu$ such that $P\Rightarrow Q$ and $\Gamma\vDash^{\nu}Q$.

######  Proof C.21.

By induction on $\Gamma\vDash^{\mu}P$ and by cases on the last rule applied.

Case [mt-thread]. Then $P$ is a thread. We deduce that

  * •

$\mu=(n,0)$ for some $n$

  * •

$\Gamma\vdash^{n}P$

From Lemma C.18 we deduce that there exist $Q$ and $m\leq n$ such that
$P\Rightarrow Q$ and $\Gamma\vdash^{m}Q$. From Lemma C.9 we deduce
$\Gamma\vDash^{\nu}Q$ for some $\nu\leq(m,0)$. We conclude observing that
$\nu\leq(m,0)\leq(n,0)=\mu$.

Case [mt-cast]. Then $P=\lceil u\rceil{P^{\prime}}$. We deduce that

  * •

$\Gamma=\Delta,u:S$

  * •

$S\leqslant_{n}T$

  * •

$\mu=\mu^{\prime}+(n,0)$

  * •

$\Gamma^{\prime},u:T\vDash^{\mu^{\prime}}P^{\prime}$

Using the induction hypothesis we deduce that there exist $Q^{\prime}$ and
$\nu^{\prime}\leq\mu^{\prime}$ such that $P^{\prime}\Rightarrow Q^{\prime}$
and $\Gamma^{\prime},u:T\vDash^{\nu^{\prime}}Q^{\prime}$. We conclude with an
application of [mt-cast] taking $Q\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\lceil u\rceil{Q^{\prime}}$,
$\nu\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}\nu^{\prime}+(n,0)$ and
observing that $P\Rightarrow Q$ using [r-cast].

Case [mt-par]. Then $P=(s)(P_{1}\mathrel{|}\dots\mathrel{|}P_{h})$. We deduce

  * •

$\Gamma=\Gamma_{1},\dots,\Gamma_{h}$

  * •

$\mu=\sum_{i=1}^{h}\mu_{i}+(0,\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)$

  * •

$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vDash^{\mu_{i}}P_{i}$
for $i=1,\dots,h$

  * •

$\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$

Using the induction hypothesis we deduce that there exist $Q_{i}$ in choice
normal form and $\nu_{i}\leq\mu_{i}$ such that $P_{i}\Rightarrow Q_{i}$ and
$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vDash^{\nu_{i}}Q_{i}$
for $i=1,\dots,h$. We conclude by taking
$\nu\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\sum_{i=1}^{h}\nu_{i}+(0,\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)$
and $Q\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}(s)(Q_{1}\mathrel{|}\cdots\mathrel{|}Q_{h})$ with one application
of [mt-par], observing that
$\nu=\sum_{i=1}^{h}\nu_{i}+(0,\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)\leq\sum_{i=1}^{h}\mu_{i}+(0,\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)=\mu$
and that $P\Rightarrow Q$ by [r-par].

######  Lemma C.22.

If $\Gamma\vdash_{\mathsf{ind}}P$ and $P$ is in choice normal form, then there
exists $P^{\mathit{nf}}$ such that $P\preccurlyeq P^{\mathit{nf}}$.

######  Proof C.23.

By induction on $\Gamma\vdash_{\mathsf{ind}}P$ and by cases on the last rule
applied.

Cases [t-choice] and [co-choice]. These cases are impossible from the
hypothesis that $P$ is in choice normal form.

Cases [t-done], [t-wait], [t-close], [t-channel-in], [t-channel-out], [t-tag],
[co-tag]. Then $P$ is a thread and is already in thread normal form and we
conclude by reflexivity of $\preccurlyeq$.

Case [t-call]. Then there exist $A$, $Q$, $\overline{u}$ and $\overline{S}$
such that

  * •

$P=A\langle\overline{u}\rangle$

  * •

$A(\overline{x})\mathrel{\smash{\stackrel{{\scriptstyle\vartriangle}}{{=}}}}Q$

  * •

$\Gamma=\overline{u:S}$

  * •

$\overline{u:S}\vdash_{\mathsf{ind}}Q\\{\overline{u}/\overline{x}\\}$

Using the induction hypothesis on
$\overline{u:S}\vdash_{\mathsf{ind}}Q\\{\overline{u}/\overline{x}\\}$ we
deduce that there exists $P^{\mathit{nf}}$ such that
$Q\\{\overline{u}/\overline{x}\\}\preccurlyeq P^{\mathit{nf}}$. We conclude
$P\preccurlyeq P^{\mathit{nf}}$ using [s-call] and the transitivity of
$\preccurlyeq$.

Case [t-par]. Then there exist $s$ and
$P_{i},\Gamma_{i},S_{i},\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}$
for $i=1,\dots,h$ such that

  * •

$P=(s)(P_{1}\mathrel{|}\cdots\mathrel{|}P_{h})$

  * •

$\Gamma=\Gamma_{1},\dots,\Gamma_{h}$

  * •

$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vdash_{\mathsf{ind}}P_{i}$
for $i=1,\dots,h$

Using the induction hypothesis on
$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vdash_{\mathsf{ind}}P_{i}$
we deduce that there exist $P^{\mathit{nf}}_{i}$ such that $P_{i}\preccurlyeq
P^{\mathit{nf}}_{i}$ for $i=1,\dots,h$. By definition of thread normal form,
it must be the case that $P^{\mathit{nf}}_{i}=\lceil\overline{u_{i}}\rceil
P^{\mathit{par}}_{i}$ for some $\overline{u_{i}}$ and $P^{\mathit{par}}_{i}$.
Let $\overline{v_{i}}$ be the same sequence as $\overline{u_{i}}$ except that
occurrences of
$s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]$
have been removed. We conclude by taking
$P^{\mathit{nf}}\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\lceil\overline{v_{1}}\dots\overline{v_{h}}\rceil(s)(P^{\mathit{par}}_{1}\mathrel{|}\dots\mathrel{|}P^{\mathit{par}}_{h})$
and using the fact that $\preccurlyeq$ is a pre-congruence and observing that

$\begin{array}[]{rcll}P&=&(s)(P_{1}\mathrel{|}\cdots\mathrel{|}P_{h})&\text{by
definition of $P$}\\\
&\preccurlyeq&(s)(P^{\mathit{nf}}_{1}\mathrel{|}\cdots\mathrel{|}P^{\mathit{nf}}_{h})&\text{using
the induction hypothesis}\\\ &=&(s)(\lceil\overline{u_{1}}\rceil
P^{\mathit{par}}_{1}\mathrel{|}\cdots\mathrel{|}\lceil\overline{u_{h}}\rceil
P^{\mathit{par}}_{h})&\text{by definition of thread normal form}\\\
&\preccurlyeq&\lceil\overline{v_{1}}\dots\overline{v_{h}}\rceil(s)(P^{\mathit{par}}_{1}\mathrel{|}\cdots\mathrel{|}P^{\mathit{par}}_{h})&\text{by
\hyperlink{rule:s-cast-new}{{{\small[s-cast-new]}}}, \hyperlink{rule:s-cast-
swap}{{{\small[s-cast-swap]}}}, \hyperlink{rule:s-par-comm}{{{\small[s-par-
comm]}}}}\\\ &=&P^{\mathit{nf}}&\text{by definition of
$P^{\mathit{nf}}$}\end{array}$

Case [t-cast]. Then there exist $u$, $Q$, $\Gamma^{\prime}$, $S$ and $T$ such
that

  * •

$P=\lceil u\rceil Q$

  * •

$\Gamma=\Gamma^{\prime},u:S$

  * •

$\Gamma^{\prime},u:T\vdash_{\mathsf{ind}}Q$

  * •

$S\leqslant T$

Using the induction hypothesis on $\Gamma^{\prime},u:T\vdash_{\mathsf{ind}}Q$
we deduce that there exists $Q^{\mathit{nf}}$ such that $Q\preccurlyeq
Q^{\mathit{nf}}$. We conclude by taking
$P^{\mathit{nf}}\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}\lceil
u\rceil Q^{\mathit{nf}}$ using the fact that $\preccurlyeq$ is a pre-
congruence.

######  Lemma C.24 (Proximity).

If $s\in\mathsf{fn}(P)\setminus\mathsf{bn}(\mathcal{C})$, then
$(s)(\mathcal{C}[P]\mathrel{|}\overline{Q})\preccurlyeq\mathcal{D}[(s)(P\mathrel{|}\overline{Q})]$
for some $\mathcal{D}$.

######  Proof C.25.

By induction on the structure of $\mathcal{C}$ and by cases on its shape.

Case $\mathcal{C}=[\leavevmode\nobreak\ ]$. We conclude by taking
$\mathcal{D}\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}[\leavevmode\nobreak\ ]$ using the reflexivity of $\preccurlyeq$.

Case
$\mathcal{C}=(t)(\overline{P^{\prime}}\mathrel{|}\mathcal{C}^{\prime}\mathrel{|}\overline{Q^{\prime}})$.
From the hypothesis $s\in\mathsf{fn}(P)\setminus\mathsf{bn}(\mathcal{C})$ we
deduce $s\neq t$ and
$s\in\mathsf{fn}(P)\setminus\mathsf{bn}(\mathcal{C}^{\prime})$. Using the
induction hypothesis and [s-par-comm] we deduce that there exists
$\mathcal{D}^{\prime}$ such that
$(s)(\mathcal{C}^{\prime}[P]\mathrel{|}\overline{Q})\preccurlyeq\mathcal{D}^{\prime}[(s)(P\mathrel{|}\overline{Q})]$.
Take $\mathcal{D}\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}(t)(\mathcal{D}^{\prime}\mathrel{|}\overline{P^{\prime}}\mathrel{|}\overline{Q^{\prime}})$.
We conclude

$\begin{array}[]{rcll}(s)(\mathcal{C}[P]\mathrel{|}\overline{Q})&=&(s)((t)(\overline{P^{\prime}}\mathrel{|}\mathcal{C}^{\prime}[P]\mathrel{|}\overline{Q^{\prime}})\mathrel{|}\overline{Q})&\text{by
definition of $\mathcal{C}$}\\\
&\preccurlyeq&(s)(\overline{Q}\mathrel{|}(t)(\mathcal{C}^{\prime}[P]\mathrel{|}\overline{P^{\prime}}\mathrel{|}\overline{Q^{\prime}}))&\text{by
\hyperlink{rule:s-par-comm}{{{\small[s-par-comm]}}}}\\\
&\preccurlyeq&(t)((s)(\overline{Q}\mathrel{|}\mathcal{C}^{\prime}[P])\mathrel{|}\overline{P^{\prime}}\mathrel{|}\overline{Q^{\prime}})&\text{by
\hyperlink{rule:s-par-assoc}{{{\small[s-par-assoc]}}} and
$s\in\mathsf{fn}(\mathcal{C}^{\prime}[P])$}\\\
&\preccurlyeq&(t)((s)(\mathcal{C}^{\prime}[P]\mathrel{|}\overline{Q})\mathrel{|}\overline{P^{\prime}}\mathrel{|}\overline{Q^{\prime}})&\text{by
\hyperlink{rule:s-par-comm}{{{\small[s-par-comm]}}}}\\\
&\preccurlyeq&(t)(\mathcal{D}^{\prime}[(s)(P\mathrel{|}\overline{Q})]\mathrel{|}\overline{P^{\prime}}\mathrel{|}\overline{Q^{\prime}})&\text{using
the induction hypothesis}\\\
&=&\mathcal{D}[(s)(P\mathrel{|}\overline{Q})]&\text{by definition of
$\mathcal{D}$}\end{array}$

Case $\mathcal{C}=\lceil
t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\rceil\mathcal{C}^{\prime}$
and $s\neq t$. Using the induction hypothesis we deduce that there exists
$\mathcal{D}^{\prime}$ such that
$(s)(\mathcal{C}^{\prime}[P]\mathrel{|}\overline{Q})\preccurlyeq\mathcal{D}^{\prime}[(s)(P\mathrel{|}\overline{Q})]$.
Take $\mathcal{D}\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}\lceil
t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\rceil\mathcal{D}^{\prime}$.
We conclude

$\begin{array}[]{rcll}(s)(\mathcal{C}[P]\mathrel{|}\overline{Q})&=&(s)(\lceil
t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\rceil\mathcal{C}^{\prime}[P]\mathrel{|}\overline{Q})&\text{by
definition of $\mathcal{C}$}\\\ &\preccurlyeq&\lceil
t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\rceil(s)(\mathcal{C}^{\prime}[P]\mathrel{|}\overline{Q})&\text{by
\hyperlink{rule:s-cast-swap}{{{\small[s-cast-swap]}}} and $t\neq s$}\\\
&\preccurlyeq&\lceil
t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\rceil\mathcal{D}^{\prime}[(s)(P\mathrel{|}\overline{Q})]&\text{using
the induction hypothesis}\\\
&=&\mathcal{D}[(s)(P\mathrel{|}\overline{Q})]&\text{by definition of
$\mathcal{D}$}\end{array}$

Case $\mathcal{C}=\lceil
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\rceil\mathcal{C}^{\prime}$.
Using the induction hypothesis we deduce that there exists $\mathcal{D}$ such
that
$(s)(\mathcal{C}^{\prime}[P]\mathrel{|}\overline{Q})\preccurlyeq\mathcal{D}[(s)(P\mathrel{|}\overline{Q})]$.
We conclude

$\begin{array}[b]{rcll}(s)(\mathcal{C}[P]\mathrel{|}\overline{Q})&=&(s)(\lceil
s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}]\rceil\mathcal{C}^{\prime}[P]\mathrel{|}\overline{Q})&\text{by
definition of $\mathcal{C}$}\\\
&\preccurlyeq&(s)(\mathcal{C}^{\prime}[P]\mathrel{|}\overline{Q})&\text{by
\hyperlink{rule:s-cast-new}{{{\small[s-cast-new]}}}}\\\
&\preccurlyeq&\mathcal{D}[(s)(P\mathrel{|}\overline{Q})]&\text{using the
induction hypothesis}\end{array}$

######  Lemma C.26 (Quasi - Deadlock Freedom).

If $\emptyset\vDash^{\mu}P^{\mathit{nf}}$, then
$P^{\mathit{nf}}=\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}$
or $P^{\mathit{nf}}\preccurlyeq Q^{\mathit{nf}}$ for some $Q^{\mathit{nf}}$ in
proximity normal form.

######  Proof C.27.

By induction on the derivation of $\emptyset\vDash^{\mu}P^{\mathit{nf}}$ we
deduce that $P^{\mathit{nf}}$ consists of $s_{1},\dots,s_{h}$ sessions and
$\sum_{i=1}^{h}k_{i}-h+1$ threads where $k_{i}$ is the number of roles in
$s_{i}$. The scenarios in which no communication is possible are those in
which for each session $s_{i}$ there are less than $k_{i}$ $s_{i}$-threads. If
we assume that for each $s_{i}$ there are $k_{i}-1$ threads, then we obtain

$\sum_{i=1}^{h}k_{i}-h+1-\sum_{i=1}^{h}(k_{i}-1)=\sum_{i=1}^{h}k_{i}-h+1-\sum_{i=1}^{h}k_{i}+h=1$

$s_{i}$-thread for some $s_{i}$; hence, there exist $k_{i}$ $s_{i}$-threads.
In other words, there exist
$\mathcal{D},\mathcal{C}_{1},\dots,\mathcal{C}_{k_{i}}$ and
$P^{\mathit{th}}_{1},\dots,P^{\mathit{th}}_{k_{i}}$ $s_{i}$-threads such that
$P^{\mathit{nf}}=\mathcal{D}[(s_{i})(\mathcal{C}_{1}[P^{\mathit{th}}_{1}]\mathrel{|}\cdots\mathrel{|}\mathcal{C}_{k_{i}}[P^{\mathit{th}}_{k_{i}}])]$.
We conclude

$\begin{array}[]{rcll}P^{\mathit{nf}}&=&\mathcal{D}[(s_{i})(\mathcal{C}_{1}[P^{\mathit{th}}_{1}]\mathrel{|}\cdots\mathrel{|}\mathcal{C}_{k_{i}}[P^{\mathit{th}}_{k_{i}}])]&\text{by
definition of $P^{\mathit{nf}}$}\\\
&\preccurlyeq&\mathcal{D}[\mathcal{D}_{1}[(s_{i})(P^{\mathit{th}}_{1}\mathrel{|}\mathcal{C}_{2}[P^{\mathit{th}}_{2}]\mathrel{|}\cdots\mathrel{|}\mathcal{C}_{k_{i}}[P^{\mathit{th}}_{k_{i}}])]]&\text{by
\lx@cref{creftype~refnum}{lem:proximity}}\\\
&\preccurlyeq&\mathcal{D}[\mathcal{D}_{1}[(s_{i})(\mathcal{C}_{2}[P^{\mathit{th}}_{2}]\mathrel{|}P^{\mathit{th}}_{1}\mathrel{|}\cdots\mathrel{|}\mathcal{C}_{k_{i}}[P^{\mathit{th}}_{k_{i}}])]]&\text{by
\hyperlink{rule:s-par-comm}{{{\small[s-par-comm]}}}}\\\ &\dots\\\
&\preccurlyeq&\mathcal{D}[\mathcal{D}_{1}[\mathcal{D}_{2}[\dots\mathcal{D}_{k_{i}}[(s_{i})(P^{\mathit{th}}_{k_{i}}\mathrel{|}\cdots\mathrel{|}P^{\mathit{th}}_{2}\mathrel{|}P^{\mathit{th}}_{1})]\dots]]]&\text{for
some $\mathcal{D}_{2},\dots,\mathcal{D}_{k_{i}}$}\\\
&\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}&Q^{\mathit{nf}}\end{array}$

The fact that $Q^{\mathit{nf}}$ is in thread normal form follows from the
observation that $P^{\mathit{nf}}$ does not have unguarded casts (it is a
closed process in thread normal form) so the pre-congruence rules applied here
and in Lemma C.24 do not move casts around. We conclude that $Q^{\mathit{nf}}$
is in proximity normal form by its shape.

Lemma C.26 is dubbed “quasi-deadlock freedom” because it does not say that
$Q^{\mathit{nf}}$ reduces. Indeed, a process in proximity normal form is only
_ready to communicate_ thanks to its shape (see reduction rules). We can prove
that a well typed process of such kind actually reduces by observing that
[t-par] requires that the involved session is coherent. This result is the key
ingredient for proving Lemma C.28.

###  C.4 Soundness

######  Lemma C.28.

If $\Gamma\vDash^{\mu}P^{\mathit{nf}}$ where $P^{\mathit{nf}}$ is in proximity
normal form, then there exist $Q$ and $\nu<\mu$ such that
$P^{\mathit{nf}}\Rightarrow^{+}Q$ and $\Gamma\vDash^{\nu}Q$.

######  Proof C.29.

From the hypothesis that $P^{\mathit{nf}}$ is in proximity normal form we know
that
$P^{\mathit{nf}}=\mathcal{C}[(s)(P^{\mathit{th}}_{1}\mathrel{|}\cdots\mathrel{|}P^{\mathit{th}}_{h})]$
for some $\mathcal{C}$, $s$ and
$P^{\mathit{th}}_{1},\dots,P^{\mathit{th}}_{h}$ $s$-threads. We reason by
induction on $\mathcal{C}$ and by cases on its shape.

Case $\mathcal{C}=[\leavevmode\nobreak\ ]$. From [mt-thread] and [mt-par] we
deduce that there exist
$\Gamma_{i},S_{i},\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i},n_{i}$
for $i=1,\dots,h$ such that

  * •

$\Gamma=\Gamma_{1},\dots,\Gamma_{h}$

  * •

$\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$

  * •

$\mu=(\sum_{i=1}^{h}n_{i},\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)$

  * •

$\Gamma_{i},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vdash^{n_{i}}P^{\mathit{th}}_{i}$
for $i=1,\dots,h$

From the hypothesis that
$\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$ we deduce
$\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\stackrel{{\scriptstyle{?}\checkmark}}{{\Longrightarrow}}$.
We now reason on the rank of the session and on the shape of $S_{i}$. For the
sake of simplicity, we implicitly apply [s-par-comm] at process level.

If
$\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|=1$,
then
$\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\stackrel{{\scriptstyle{?}\checkmark}}{{\longrightarrow}}$
using [l-terminate].

  * •

Case
$S_{1}={?}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}$
and
$S_{j}={!}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}end}$
for $j=2,\dots,h$. Then

    * –

$\Gamma_{j}=\emptyset$ and
$P^{\mathit{th}}_{j}=\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}close}\,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{j}]$
for $j=2,\dots,h$

    * –

$P^{\mathit{th}}_{1}=\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}wait}\,s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}].{Q}$

    * –

$\Gamma_{1}\vdash^{n_{1}}Q$

From Lemma C.9 we deduce that $\Gamma_{1}\vDash^{\nu}Q$ for some
$\nu\leq(n_{1},0)$. We conclude observing that $P^{\mathit{nf}}\rightarrow Q$
by [r-signal] and that
$\nu\leq(n_{1},0)<(\sum_{i=1}^{h}n_{i},\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)=\mu$.

If
$\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|>1$,
then
$\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}\dots\stackrel{{\scriptstyle{?}\checkmark}}{{\longrightarrow}}$
first using [l-tau] and [l-sync]. Observe that [l-pick] is never used since we
are considering the minimum reduction sequence; a synchronization through
[l-pick] and [l-sync] would lead to a longer reduction. Then
$S_{1}\xrightarrow{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}\triangleright{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{k}}}$
and
$S_{2}\xrightarrow{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}\triangleright{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{k}}}$
for some
$\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{k}$
or
$S_{1}\xrightarrow{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}\triangleright{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}}{!}S}$
and
$S_{2}\xrightarrow{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}\triangleright{\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}}{?}S}$.

  * •

Case $S_{1}=\sum_{i\in
I}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}{!}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.S^{\prime}_{i}$
and $S_{2}=\sum_{j\in
J}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}{?}\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{j}.T_{j}$
with $k\in I$. From the hypothesis that
$\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$ we deduce $I\subseteq J$. From Definition 4.2 we deduce
$\prod_{i=3}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}\triangleright{S^{\prime}_{k}}\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}\triangleright{T_{k}}\leavevmode\nobreak\
\text{coherent}$ and from [t-tag] we deduce that

    * –

$P^{\mathit{th}}_{1}=s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}]{!}\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{i}.P^{\prime}_{i}\\}_{i\in
I}$

    * –

$P^{\mathit{th}}_{2}=s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}]{?}\\{\textsf{\color[rgb]{0,0.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.5,0}m}_{j}.Q_{j}\\}_{j\in
J}$

    * –

$\Gamma_{1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}]:S^{\prime}_{i}\vdash^{n_{1}}P^{\prime}_{i}$
for all $i\in I$

    * –

$\Gamma_{2},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}]:T_{j}\vdash^{n_{2}}Q_{j}$
for all $j\in J$

Let $Q\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}(s)(P^{\prime}_{k}\mathrel{|}Q_{k}\mathrel{|}P_{3}\mathrel{|}\dots\mathrel{|}P_{h})$
and observe that $P^{\mathit{nf}}\Rightarrow^{+}Q$ by [r-pick] and [r-tag].
From Lemma C.9 we deduce that there exist
$\mu_{1}\leq(n_{1},0),\mu_{2}\leq(n_{2},0)$ such that

    * –

$\Gamma_{1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}]:S^{\prime}_{k}\vDash^{\mu_{1}}P^{\prime}_{k}$

    * –

$\Gamma_{2},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}]:T_{k}\vDash^{\mu_{2}}Q_{k}$

Let $\nu\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\mu_{1}+\mu_{2}+(\sum_{i=3}^{h}n_{i},\|\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}\triangleright{S^{\prime}_{k}}\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}\triangleright{T_{k}}\mathrel{|}\prod_{i=3}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)$.
We conclude with one application of [mt-par] observing that

$\begin{array}[]{rcll}\nu&=&\mu_{1}+\mu_{2}+(\sum_{i=3}^{h}n_{i},\|\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}\triangleright{S^{\prime}_{k}}\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}\triangleright{T_{k}}\mathrel{|}\prod_{i=3}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)\\\
&\leq&(\sum_{i=1}^{h}n_{i},\|\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}\triangleright{S^{\prime}_{k}}\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}\triangleright{T_{k}}\mathrel{|}\prod_{i=3}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)&\text{by
\lx@cref{creftype~refnum}{lem:measure_rank}}\\\
&<&(\sum_{i=1}^{h}n_{i},\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)&\text{before
reductions}\\\ &=&\mu\end{array}$

  * •

Case
$S_{1}=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}{!}{S}.T_{1}$
and
$S_{2}=\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}{?}{S}.T_{2}$.

From the hypothesis that
$\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$ and Definition 4.2 we deduce
$\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}\triangleright{T_{1}}\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}\triangleright{T_{2}}\mathrel{|}\prod_{i=3}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\leavevmode\nobreak\
\text{coherent}$ and from [t-channel-out] and [t-channel-in] we deduce that

  * •

$P^{\mathit{th}}_{1}=s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}]\mathsf{!}u.P^{\prime}_{1}$

  * •

$P^{\mathit{th}}_{2}=s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}][\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}]\mathsf{?}(x).P^{\prime}_{2}$

  * •

$\Gamma_{1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}]:T_{1}\vdash^{n_{1}}P^{\prime}_{1}$

  * •

$\Gamma_{2},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}]:T_{2},x:S\vdash^{n_{2}}P^{\prime}_{2}$

Let $Q\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}(s)(P^{\prime}_{1}\mathrel{|}P^{\prime}_{2}\\{u/x\\}\mathrel{|}P^{\mathit{th}}_{3}\mathrel{|}\cdots\mathrel{|}P^{\mathit{th}}_{h})$
and observe that $P^{\mathit{nf}}\rightarrow Q$ by [r-channel]. Using Lemma
C.1 we deduce
$\Gamma_{2},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}]:T_{2},u:S\vdash^{n_{2}}P^{\prime}_{2}\\{u/x\\}$
and from Lemma C.9 we deduce that there exist
$\mu_{1}\leq(n_{1},0),\mu_{2}\leq(n_{2},0)$ such that

  * •

$\Gamma_{1},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}]:T_{1}\vDash^{\mu_{1}}P^{\prime}_{1}$

  * •

$\Gamma_{2},s[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}]:T_{2},u:S\vDash^{\mu_{2}}P^{\prime}_{2}\\{u/x\\}$

Let $\nu\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\mu_{1}+\mu_{2}+(\sum_{i=3}^{h}n_{i},\|\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}\triangleright{T_{1}}\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}\triangleright{T_{2}}\mathrel{|}\prod_{i=3}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)$.
We conclude with one application of [mt-par] observing that

$\begin{array}[]{rcll}\nu&=&\mu_{1}+\mu_{2}+(\sum_{i=3}^{h}n_{i},\|\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}\triangleright{T_{1}}\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}\triangleright{T_{2}}\mathrel{|}\prod_{i=3}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)\\\
&\leq&(\sum_{i=1}^{h}n_{i},\|\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}\triangleright{T_{1}}\mathrel{|}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{2}\triangleright{T_{2}}\mathrel{|}\prod_{i=3}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)&\text{by
\lx@cref{creftype~refnum}{lem:measure_rank}}\\\
&<&(\sum_{i=1}^{h}n_{i},\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)&\text{before
reductions}\\\ &=&\mu\end{array}$

Case
$\mathcal{C}=(t)(\overline{P^{\mathit{par}}}\mathrel{|}\mathcal{D}\mathrel{|}\overline{Q^{\mathit{par}}})$.
Let $R^{\mathit{nf}}\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\mathcal{D}[(s)(P^{\mathit{th}}_{1}\mathrel{|}\dots\mathrel{|}P^{\mathit{th}}_{h})]$
and observe that $R^{\mathit{nf}}$ is in proximity normal form. From [mt-par]
we deduce that there exist
$\Gamma_{i},S_{i},\mu_{i},\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}$
for $i=1,\dots,h$ and $k\leq h$ such that

  * •

$\Gamma=\Gamma_{1},\dots,\Gamma_{h}$

  * •

$\Gamma_{1},t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}]:S_{1}\vDash^{\mu_{1}}R^{\mathit{nf}}$

  * •

$\Gamma_{i},t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vDash^{\mu_{i}}P^{\mathit{par}}_{i}$
for $i=1,\dots,k$

  * •

$\Gamma_{i},t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}]:S_{i}\vDash^{\mu_{i}}Q^{\mathit{par}}_{i}$
for $i=k+1,\dots,h$

  * •

$\mu=\sum_{i=1}^{h}\mu_{i}+(0,\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)$

Using the induction hypothesis on
$\Gamma_{1},t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}]:S_{1}\vDash^{\mu_{1}}R^{\mathit{nf}}$
we deduce that there exists $Q^{\prime}$ and $\nu^{\prime}<\mu_{1}$ such that

  * •

$R^{\mathit{nf}}\Rightarrow^{+}Q^{\prime}$

  * •

$\Gamma_{1},t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{1}]:S_{1}\vDash^{\nu^{\prime}}Q^{\prime}$

We conclude taking $Q\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}(t)(Q^{\prime}\mathrel{|}\overline{P^{\mathit{par}}}\mathrel{|}\overline{Q^{\mathit{par}}})$
and $\nu\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\nu^{\prime}+\sum_{i=2}^{h}\mu_{i}+(0,\|\prod_{i=1}^{h}\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}p}_{i}\triangleright{S_{i}}\|)$
and observing that $\nu<\mu$ and $P^{\mathit{nf}}\Rightarrow^{+}Q$ by [r-par].

Case $\mathcal{C}=\lceil
t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]\rceil{\mathcal{D}}$.
Observe that $t\neq s$. Let
$R^{\mathit{nf}}\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\mathcal{D}[(s)(P^{\mathit{th}}_{1}\mathrel{|}\cdots\mathrel{|}P^{\mathit{th}}_{h})]$
and note that $R^{\mathit{nf}}$ is in proximity normal form. From [mt-cast] we
deduce that there exists $\Delta,\mu^{\prime},S,T,m_{t}$ such that

  * •

$\Gamma=\Delta,t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]:S$

  * •

$S\leqslant_{m_{t}}T$

  * •

$\mu=\mu^{\prime}+(m_{t},0)$

  * •

$\Delta,t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]:T\vDash^{\mu^{\prime}}R^{\mathit{nf}}$

Using the induction hypothesis on
$\Delta,t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]:T\vDash^{\mu^{\prime}}R^{\mathit{nf}}$
we deduce that there exist $Q^{\prime}$ and $\nu^{\prime}<\mu^{\prime}$ such
that $R^{\mathit{nf}}\Rightarrow^{+}Q^{\prime}$ and
$\Delta,t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]:T\vDash^{\nu^{\prime}}Q^{\prime}$.
We conclude taking $Q\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}\lceil
t[\mathsf{\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}q}]\rceil{Q^{\prime}}$
and $\nu\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\nu^{\prime}+(m_{t},0)$ and observing that $\nu<\mu$ and
$P^{\mathit{nf}}\Rightarrow^{+}Q$ by [r-cast].

######  Lemma C.30.

If $\emptyset\vDash^{\mu}P$, then either
$P\preccurlyeq\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}$
or $P\Rightarrow^{+}Q$ and $\emptyset\vDash^{\nu}Q$ for some $Q$ and
$\nu<\mu$.

######  Proof C.31.

Using Lemma C.20 we deduce that there exist $P^{\prime}$ in choice normal form
such that $P\Rightarrow P^{\prime}$ and
$\emptyset\vDash^{\mu^{\prime}}P^{\prime}$ and $\mu^{\prime}\leq\mu$. By Lemma
C.9 we deduce $\emptyset\vdash P^{\prime}$. Using Lemma C.22 we deduce that
there exist $P^{\mathit{nf}}$ such that $P^{\prime}\preccurlyeq
P^{\mathit{nf}}$.

If
$P^{\mathit{nf}}=\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}$
there is nothing left to prove.

If
$P^{\mathit{nf}}\neq\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}$,
by Lemma C.26 we deduce $P^{\mathit{nf}}\preccurlyeq Q^{\mathit{nf}}$ for some
$Q^{\mathit{nf}}$ in proximity normal form. From Lemma C.11 we deduce
$\emptyset\vDash^{\mu^{\prime\prime}}Q^{\mathit{nf}}$ for some
$\mu^{\prime\prime}\leq\mu^{\prime}$. Using Lemma C.28 we conclude that
$Q^{\mathit{nf}}\Rightarrow^{+}Q$ and $\emptyset\vDash^{\nu}Q$ for some $Q$
and $\nu<\mu^{\prime\prime}\leq\mu^{\prime}\leq\mu$.

######  Lemma C.32.

If $\emptyset\vdash^{n}P$, then either
$P\preccurlyeq\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}$
or
$P\Rightarrow^{+}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}$.

######  Proof C.33.

From Lemma C.9 we deduce that there exists $\mu\leq(n,0)$ such that
$\emptyset\vDash^{\mu}P$. We proceed doing an induction on the
lexicographically ordered pair $\mu$. From Lemma C.30 we deduce either
$P\preccurlyeq\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}$
or $P\Rightarrow^{+}Q$ and $\emptyset\vDash^{\nu}Q$ for some $\nu<\mu$. In the
first case there is nothing left to prove. In the second case we use the
induction hypothesis to deduce that either
$Q\preccurlyeq\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}$
or
$Q\Rightarrow^{+}\textsf{\color[rgb]{0,0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.5}done}$.
We conclude using either [r-struct] or the transitivity of $\Rightarrow^{+}$,
respectively.

######  Proof C.34 (Proof of Theorem 5.4).

Immediate consequence of Lemmas C.5 and C.32.