$\star\,[x^{\alpha}:\mathtt{A}],\mathsf{Cfg}_{x^{\alpha}:\mathtt{A},y^{\beta}:\mathtt{B}}(\mathcal{C})\vdash[y^{\beta}:\mathtt{B}]$
for an open configuration
$x^{\alpha}:\mathtt{A}\vdash\mathcal{C}::y^{\beta}{:}\mathtt{B}$. if the
configuration is closed, it is enough to build a derivation
$\star\;\mathsf{Cfg}_{\cdot,y^{\beta}:\mathtt{B}}(\mathcal{C})\vdash[y^{\beta}{:}\mathtt{B}]$
for a closed configuration $\cdot\vdash\mathcal{C}::y^{\beta}:\mathtt{B}$. For
the sake of brevity we write
$\star\,\overline{[\bar{x}^{\alpha}:\omega]},\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,y^{\beta}:\mathtt{B}}(\mathcal{C})\vdash[y^{\beta}:\mathtt{B}]$
as a generalization for both open and closed configurations, where
$\overline{[\bar{x}^{\alpha}:\omega]}$ is either empty or
$[\bar{x}^{\alpha}:\omega]$, and it is empty if and only if $\bar{x}:\omega$
is empty. We provide a circular derivation for each possible pattern of
$\mathcal{C}$. Here are the circular derivations when $\mathcal{C}$ is an
empty configuration and a composition of configurations, respectively:

$\begin{array}[]{lr}\star\;{[x^{\alpha}:\mathtt{A}]},\mathsf{Cfg}_{x^{\alpha}:\mathtt{A},x^{\alpha}:\mathtt{A}}(\cdot)\vdash{[x^{\beta}:\mathtt{A}]}{[x^{\alpha}:\mathtt{A}]},1\vdash{[x^{\alpha}:\mathtt{A}]}[x^{\alpha}:\mathtt{A}]\vdash[x^{\alpha}:\mathtt{A}]&\star\;\overline{[\bar{x}^{\alpha}:\omega]},\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,y^{\beta}:\mathtt{B}}(\mathcal{C}_{1}\mid_{z:\mathtt{C}}\mathcal{C}_{2})\vdash{[y^{\beta}:\mathtt{B}]}\overline{[\bar{x}^{\alpha}:\omega]},\exists
z.\exists\zeta.(\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,z^{\zeta}:\mathtt{C}}(\mathcal{C}_{1})\otimes\mathsf{Cfg}_{z^{\zeta}:\mathtt{C},y^{\beta}:\mathtt{B}}(\mathcal{C}_{2}))\vdash{[y^{\beta}:\mathtt{B}]}\overline{[\bar{x}^{\alpha}:\omega]},\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,z^{\zeta}:\mathtt{C}}(\mathcal{C}_{1})\otimes\mathsf{Cfg}_{z^{\zeta}:\mathtt{C},y^{\beta}:\mathtt{B}}(\mathcal{C}_{2}))\vdash{[y^{\beta}:\mathtt{B}]}\overline{[\bar{x}^{\alpha}:\omega]},\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,z^{\zeta}:\mathtt{C}}(\mathcal{C}_{1}),\mathsf{Cfg}_{z^{\zeta}:\mathtt{C},y^{\beta}:\mathtt{B}}(\mathcal{C}_{2}))\vdash{[y^{\beta}:\mathtt{B}]}\lx@proof@logical@and\overline{[\bar{x}^{\alpha}:\omega]},\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,z^{\zeta}:\mathtt{C}}(\mathcal{C}_{1})\vdash{[z^{\zeta}:\mathtt{C}]}\star{[z^{\zeta}:\mathtt{C}]},\mathsf{Cfg}_{z^{\zeta}:\mathtt{C},y^{\beta}:\mathtt{B}}(\mathcal{C}_{2})\vdash{[y^{\beta}:\mathtt{B}]}\star\end{array}$

It should be clear how to unfold the derivation given based on patterns to a
circular definition in the system of Figure 6. Consider the first two lines in
expanded definition of predicate $\mathsf{Cfg}$:

$\begin{array}[]{cl}\mathsf{Cfg}_{\bar{x}^{\alpha}:d_{1},y^{\beta}:d_{2}}(d_{3})=&(\exists
c_{1},c_{2},z,c.\,(d_{3}=c_{1}|_{z:c}c_{2})\,\otimes\,\exists
z.\exists\eta.\mathsf{Cfg}_{\bar{x}^{\alpha}:d_{1},z^{\eta}:c}(c_{1})\otimes\mathsf{Cfg}_{z^{\eta}:c,y^{\beta}:d_{2}}(c_{2}))\\\
&\oplus((d_{3}=\cdot)\otimes 1)\oplus\cdots\end{array}$

To prove the judgment
$\star[x^{\alpha}:\mathtt{A}],\mathsf{Cfg}_{x^{\alpha}:\mathtt{A},y^{\beta}:\mathtt{B}}(\mathcal{C})\vdash[y^{\beta}:\mathtt{B}]$
without pattern matching, we first need to unfold the definition of
$\mathsf{Cfg}_{x^{\alpha}:\mathtt{A},y^{\beta}:\mathtt{B}}$ with a $\mu L$
rule. Next, we apply an $\oplus L$ rule on the resulting formula which is the
right side of the above definition. After this step, we are in a quite similar
situation to the pattern matching argument: we have to prove several branches
each corresponding to a pattern of $\mathcal{C}$. In some cases, we may need
to apply extra equality and $\oplus$ rules in the derivation without pattern
matching. However, for all cases the fixed point rules applied in a cycle are
the same in the derivations built with and without pattern matching.

For the cases in which the configuration consists of a single process we give
an annotated derivation with position variables and track the relationship
between their generations. Without loss of generality, we annotate predicates
of the form $[z^{\eta}:\mathtt{C}]$ with a matching position variable
$\mathbf{z}^{\eta}$ at the start (the bottom) of each cycle. We leave it to
the reader to check that this assumption holds as an invariant at the end (the
top) of each cycle in the derivation.

Case 1. $(y\leftarrow x)$

$\star\;{\mathbf{x^{\alpha}}:[x^{\alpha}:\mathtt{A}]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{x^{\alpha}:\mathtt{A},y^{\beta}:\mathtt{A}}(y\leftarrow
x)\vdash_{\Lambda}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{A}]}\mathbf{x}^{\alpha}:{[x^{\alpha}:\mathtt{A}]},\mathbf{c}^{\eta+1}:(x^{\alpha}=y^{\beta})\vdash_{\Lambda_{1}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{A}]}\mathbf{x}^{\alpha}:{[y^{\beta}:\mathtt{A}]}\vdash_{\Lambda_{1}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{A}]}$

$\Lambda_{1}=\Lambda\cup\\{\mathbf{c}^{\eta+1}_{n+2}<\mathbf{c}^{\eta}_{n+2}\\}\cup\\{\mathbf{c}^{\eta+1}_{i}=\mathbf{c}^{\eta}_{i}\mid
i\neq n+2\\}.$

Case 2. $(\mathtt{close}\,Ry)$

$\star\;\mathbf{c}^{\eta}:\mathsf{Cfg}_{\cdot,y^{\beta}:1}(\mathtt{close}\,Ry)\vdash_{\Lambda}\mathbf{y}^{\beta}:{[y^{\beta}:1]}\mathbf{c}^{\eta+1}:\mathsf{Msg}(y^{\beta}.\mbox{closed})\otimes
1\vdash_{\Lambda_{1}}\mathbf{y}^{\beta}:{[y^{\beta}:1]}\mathbf{c}^{\eta+1}:\mathsf{Msg}(y^{\beta}.\mbox{closed})\otimes
1\vdash_{\Lambda_{2}}\mathbf{y}^{\beta+1}:\mathsf{Msg}(y^{\beta}.\mbox{closed})\otimes[\cdot:\cdot]{\mathbf{w}^{\delta}:\mathsf{Msg}(y^{\beta}.\mbox{closed}),\mathbf{c}^{\eta+1}:1\vdash_{\Lambda_{3}}\mathbf{y}^{\beta+1}:\mathsf{Msg}(y^{\beta}.\mbox{closed})\otimes[\cdot:\cdot]\lx@proof@logical@and\mathbf{w}^{\delta}:\mathsf{Msg}(y^{\beta}.\mbox{closed})\vdash_{\Lambda_{4}}\mathbf{z}^{\gamma}:\mathsf{Msg}(y^{\beta}.\mbox{closed})\mathbf{c}^{\eta+1}:1\vdash_{\Lambda_{3}}\mathbf{y}^{\beta+1}:[\cdot:\cdot]\mathbf{c}^{\eta+1}:1\vdash_{\Lambda_{5}}\mathbf{y}^{\beta+2}:1\cdot\vdash_{\Lambda_{5}}\mathbf{y}^{\beta+2}:1}$

$\Lambda_{1}=\Lambda\cup\\{\mathbf{c}^{\eta+1}_{n+2}<\mathbf{c}^{\eta}_{n+2}\\}\cup\\{\mathbf{c}^{\eta+1}_{i}=\mathbf{c}^{\eta}_{i}\mid
i\neq n+2\\},\quad$
$\Lambda_{2}=\Lambda_{1}\cup\\{\mathbf{y}^{\beta+1}_{n+2}<\mathbf{y}^{\beta}_{n+2}\\}\cup\\{\mathbf{y}^{\beta+1}_{i}=\mathbf{y}^{\beta}_{i}\mid
i\neq n+2\\}\,\quad$
$\Lambda_{3}=\Lambda_{2}\cup\\{\mathbf{c}^{\eta+1}=\mathbf{w}^{\delta}\\},$
$\Lambda_{4}=\Lambda_{3}\cup\\{\mathbf{y}^{\beta+1}=\mathbf{z}^{\gamma}\\},\Lambda_{5}=\Lambda_{3}\cup\\{\mathbf{y}^{\beta+2}_{n+2}<\mathbf{y}^{\beta+1}_{n+2}\\}\cup\\{\mathbf{y}^{\beta+2}_{i}=\mathbf{y}^{\beta+1}_{i}\mid
i\neq n+2\\}\,\quad$

Case 3. $(\mathtt{wait}\,Lx;\mathsf{Q})$

$\star\;\mathbf{x}^{\alpha}:{[x^{\alpha}:1]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{x^{\alpha}:1,y^{\beta}:\mathtt{B}}(\mathtt{wait}\,Lx;\mathsf{Q})\vdash_{\Lambda}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\mathbf{x}^{\alpha}:{[x^{\alpha}:1]},\mathbf{c}^{\eta+1}:\mathsf{Msg}(x^{\alpha}.\mbox{closed})\multimap\mathsf{Cfg}_{\cdot,y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{1}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\mathbf{x}^{\alpha+1}:\mathsf{Msg}(x^{\alpha}.\mbox{closed})\otimes[\cdot:\cdot],\mathbf{c}^{\eta+1}:\mathsf{Msg}(x^{\alpha}.\mbox{closed})\multimap\mathsf{Cfg}_{\cdot,y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{2}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\mathtt{w}^{\omega}:\mathsf{Msg}(x^{\alpha}.\mbox{closed}),\mathbf{x}^{\alpha+1}:[\cdot:\cdot],\mathbf{c}^{\eta+1}:\mathsf{Msg}(x^{\alpha}.\mbox{closed})\multimap\mathsf{Cfg}_{\cdot,y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{3}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\lx@proof@logical@and\mathtt{w}^{\omega}:\mathsf{Msg}(x^{\alpha}.\mbox{closed})\vdash_{\Lambda_{3}}\mathbf{z}^{\kappa}:\mathsf{Msg}(x^{\alpha}.\mbox{closed})\mathbf{x}^{\alpha+1}:[\cdot:\cdot],\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{\cdot,y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{3}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\mathbf{x}^{\alpha+2}:1,\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{\cdot,y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{4}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{\cdot,y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{4}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\star$

$\Lambda_{1}=\Lambda\cup\\{\mathbf{c}^{\eta+1}_{n+2}<\mathbf{c}^{\eta}_{n+2}\\}\cup\\{\mathbf{c}^{\eta+1}_{i}=\mathbf{c}^{\eta}_{i}\mid
i\neq n+2\\},$
$\Lambda_{2}=\Lambda_{1}\cup\\{\mathbf{x}^{\alpha+1}_{n+2}<\mathbf{x}^{\alpha}_{n+2}\\}\cup\\{\mathbf{x}^{\alpha+1}_{i}=\mathbf{x}^{\alpha}_{i}\mid
i\neq n+2\\}\,,$
$\Lambda_{3}=\Lambda_{2}\cup\\{\mathbf{x}^{\alpha+1}=\mathbf{w}^{\omega}\\},$
$\Lambda_{4}=\Lambda_{3}\cup\\{\mathbf{x}^{\alpha+2}_{n+2}<\mathbf{x}^{\alpha+1}_{n+2}\\}\cup\\{\mathbf{x}^{\alpha+2}_{i}=\mathbf{x}^{\alpha+1}_{i}\mid
i\neq n+2\\}\,\quad$

Case 4. $((z:\mathtt{C})\leftarrow\mathsf{Q}_{1};\mathsf{Q}_{2})$

$\star\;\overline{\mathbf{x}^{\alpha}:{[\bar{x}^{\alpha}:\omega]}},\mathbf{c}^{\eta}:\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,y^{\beta}:\mathtt{B}}((z:\mathtt{C})\leftarrow\mathsf{Q}_{1};\mathsf{Q}_{2})\vdash_{\Lambda}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\overline{\mathbf{x}^{\alpha}:{[\bar{x}^{\alpha}:\omega]}},\mathbf{c}^{\eta+1}:\exists
z.\exists\zeta.(\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,z^{\zeta}:\mathtt{C}}(\mathsf{Q}_{1})\otimes\mathsf{Cfg}_{z^{\zeta}:\mathtt{C},y^{\beta}:\mathtt{B}}(\mathsf{Q}_{2}))\vdash_{\Lambda_{1}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\overline{\mathbf{x}^{\alpha}:{[\bar{x}^{\alpha}:\omega]}},\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,z^{\zeta}:\mathtt{C}}(\mathsf{Q}_{1})\otimes\mathsf{Cfg}_{z^{\zeta}:\mathtt{C},y^{\beta}:\mathtt{B}}(\mathsf{Q}_{2}))\vdash_{\Lambda_{1}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\overline{\mathbf{x}^{\alpha}:{[\bar{x}^{\alpha}:\omega]}},\mathbf{w}^{\omega}:\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,z^{\zeta}:\mathtt{C}}(\mathsf{Q}_{1}),\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{z^{\zeta}:\mathtt{C},y^{\beta}:\mathtt{B}}(\mathsf{Q}_{2}))\vdash_{\Lambda_{2}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\lx@proof@logical@and\overline{\mathbf{x}^{\alpha}:{[\bar{x}^{\alpha}:\omega]}},\mathbf{w}^{\omega}:\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,z^{\zeta}:\mathtt{C}}(\mathsf{Q}_{1})\vdash_{\Lambda_{2}}\mathbf{z}^{\zeta}:{[z^{\zeta}:\mathtt{C}]}\star\mathbf{z}^{\zeta}:{[z^{\zeta}:\mathtt{C}]},\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{z^{\zeta}:\mathtt{C},y^{\beta}:\mathtt{B}}(\mathsf{Q}_{2})\vdash_{\Lambda_{2}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\star$

$\Lambda_{1}=\Lambda\cup\\{\mathbf{c}^{\eta+1}_{n+2}<\mathbf{c}^{\eta}_{n+2}\\}\cup\\{\mathbf{c}^{\eta+1}_{i}=\mathbf{c}^{\eta}_{i}\mid
i\neq n+2\\}\,\mathit{and}$
$\Lambda_{2}=\Lambda_{1}\cup\\{\mathbf{w}^{\omega}=\mathbf{c}^{\eta+1}\\}.$

Case 5.$(Lx.k;\mathsf{Q})$

$\star\;\mathbf{x}^{\alpha}:{[x^{\alpha}:\&\\{\ell:\mathtt{A}_{\ell}\\}_{\ell\in
L}]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{x^{\alpha}:\&\\{\ell:\mathtt{A}_{\ell}\\}_{\ell\in
L},y^{\beta}:\mathtt{B}}(Lx.k;\mathsf{Q})\vdash_{\Lambda}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\mathbf{x}^{\alpha}:{[x^{\alpha}:\&\\{\ell:\mathtt{A}_{\ell}\\}_{\ell\in
L}]},\mathbf{c}^{\eta+1}:\mathsf{Msg}(x^{\alpha}.k)\otimes\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{A}_{k},y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{1}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\mathbf{x}^{\alpha+1}:\&\\{\ell:{\mathsf{Msg}(\ell,x^{\alpha+1}:\mathtt{A}_{\ell})\multimap[x^{\alpha+1}:A_{\ell}]}\\}_{\ell\in
L},\mathbf{c}^{\eta+1}:\mathsf{Msg}(x^{\alpha}.k)\otimes\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{A}_{k},y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{2}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\mathbf{x}^{\alpha+1}:\mathsf{Msg}(x^{\alpha}.k)\multimap{[x^{\alpha+1}:\mathtt{A}_{k}]}\\},\mathbf{c}^{\eta+1}:\mathsf{Msg}(x^{\alpha}.k)\otimes\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{A}_{k},y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{2}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\mathbf{x}^{\alpha+1}:\mathsf{Msg}(x^{\alpha}.k)\multimap{[x^{\alpha+1}:\mathtt{A}_{k}]},\mathbf{w}^{\omega}:\mathsf{Msg}(x^{\alpha}.k),\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{A}_{k},y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{3}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\lx@proof@logical@and\mathbf{w}^{\omega}:\mathsf{Msg}(x^{\alpha}.k)\vdash_{\Lambda_{3}}\mathbf{z}^{\kappa}:\mathsf{Msg}(x^{\alpha}.k)\mathbf{x}^{\alpha+1}:{[x^{\alpha+1}:\mathtt{A}_{k}]},\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{A}_{k},y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{3}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\star$

$\Lambda_{1}=\Lambda\cup\\{\mathbf{c}^{\eta+1}_{n+2}<\mathbf{c}^{\eta}_{n+2}\\}\cup\\{\mathbf{c}^{\eta+1}_{i}=\mathbf{c}^{\eta}_{i}\mid
i\neq n+2\\},$
$\Lambda_{2}=\Lambda_{1}\cup\\{\mathbf{x}^{\alpha+1}_{n+2}<\mathbf{x}^{\alpha}_{n+2}\\}\cup\\{\mathbf{x}^{\alpha+1}_{i}=\mathbf{x}^{\alpha}_{i}\mid
i\neq n+2\\}\,,$
$\Lambda_{3}=\Lambda_{2}\cup\\{\mathbf{c}^{\eta+1}=\mathbf{w}^{\omega}\\}.$

Case 6. $(Ry.k;\mathsf{Q})$ Dual to Case 5.

Case 7. $(\mathbf{case}Lx(\ell\Rightarrow\mathsf{Q}_{\ell})_{\ell\in L})$

$\star\;\mathbf{x}^{\alpha}:{[x^{\alpha}:\oplus\\{\ell:\mathtt{A}_{\ell}\\}_{\ell\in
L}]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{x^{\alpha}:\oplus\\{\ell:A_{\ell}\\}_{\ell\in
L},y^{\beta}:\mathtt{B}}(\mathbf{case}Lx(\ell\Rightarrow\mathsf{Q}_{\ell})_{\ell\in
L})\vdash_{\Lambda}{\mathbf{y}^{\beta}:[y^{\beta}:\mathtt{B}]}\mathbf{x}^{\alpha}:{[x^{\alpha}:\oplus\\{\ell:\mathtt{A}_{\ell}\\}_{\ell\in
L}]},\mathbf{c}^{\eta+1}:\&\\{\ell:\mathsf{Msg}(y^{\beta}.\ell)\multimap\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{A}_{\ell},y^{\beta}:\mathtt{B}}(\mathsf{Q}_{\ell})\\}_{\ell\in
L}\vdash_{\Lambda_{1}}{\mathbf{y}^{\beta}:[y^{\beta}:\mathtt{B}]}\mathbf{x}^{\alpha+1}:\oplus\\{\ell:\mathsf{Msg}(y^{\beta}.\ell)\otimes{[x^{\alpha+1}:A_{\ell}]}\\}_{\ell\in
L},\mathbf{c}^{\eta+1}:\&\\{\ell:\mathsf{Msg}(y^{\beta}.\ell)\multimap\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{A}_{\ell},y^{\beta}:\mathtt{B}}(\mathsf{Q}_{\ell})\\}_{\ell\in
L}\vdash_{\Lambda_{2}}{\mathbf{y}^{\beta}:[y^{\beta}:\mathtt{B}]}\lx@proof@logical@and\forall
k\in
L{\mathbf{x}^{\alpha+1}:\mathsf{Msg}(y^{\beta}.k)\otimes[x^{\alpha+1}:\mathtt{A}_{k}]},\mathbf{c}^{\eta+1}:\&\\{\ell:\mathsf{Msg}(y^{\beta}.\ell)\multimap\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{A}_{\ell},y^{\beta}:\mathtt{B}}(\mathsf{Q}_{\ell})\\}_{\ell\in
L}\vdash_{\Lambda_{2}}{\mathbf{y}^{\beta}:[y^{\beta}:\mathtt{B}]}{\mathbf{x}^{\alpha+1}:\mathsf{Msg}(y^{\beta}.k)\otimes[x^{\alpha+1}:\mathtt{A}_{k}]},\mathbf{c}^{\eta+1}:\mathsf{Msg}(y^{\beta}.k)\multimap\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{A}_{k},y^{\beta}:\mathtt{B}}(\mathsf{Q}_{k})\vdash_{\Lambda_{2}}{\mathbf{y}^{\beta}:[y^{\beta}:\mathtt{B}]}\mathbf{w}^{\omega}:\mathsf{Msg}(y^{\beta}.k),\mathbf{x}^{\alpha+1}:[x^{\alpha+1}:\mathtt{A}_{k}],\mathbf{c}^{\eta+1}:\mathsf{Msg}(y^{\beta}.k)\multimap\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{A}_{k},y^{\beta}:\mathtt{B}}(\mathsf{Q}_{k})\vdash_{\Lambda_{3}}{\mathbf{y}^{\beta}:[y^{\beta}:\mathtt{B}]}\lx@proof@logical@and\mathbf{w}^{\omega}:\mathsf{Msg}(y^{\beta}.k)\vdash_{\Lambda_{3}}\mathbf{z}^{\zeta}:\mathsf{Msg}(y^{\beta}.k)\mathbf{x}^{\alpha+1}:[x^{\alpha+1}:\mathtt{A}_{k}],\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{A}_{k},y^{\beta}:\mathtt{B}}(\mathsf{Q}_{k})\vdash_{\Lambda_{3}}{\mathbf{y}^{\beta}:[y^{\beta}:\mathtt{B}]}\star$

$\Lambda_{1}=\Lambda\cup\\{\mathbf{c}^{\eta+1}_{n+2}<\mathbf{c}^{\eta}_{n+2}\\}\cup\\{\mathbf{c}^{\eta+1}_{i}=\mathbf{c}^{\eta}_{i}\mid
i\neq n+2\\},$
$\Lambda_{2}=\Lambda_{1}\cup\\{\mathbf{x}^{\alpha+1}_{n+2}<\mathbf{x}^{\alpha}_{n+2}\\}\cup\\{\mathbf{x}^{\alpha+1}_{i}=\mathbf{x}^{\alpha}_{i}\mid
i\neq n+2\\}\,,$
$\Lambda_{3}=\Lambda_{2}\cup\\{\mathbf{x}^{\alpha+1}=\mathbf{w}^{\omega}\\}.$

Case 8. $(\mathbf{case}Ry(\ell\Rightarrow\mathsf{Q}_{\ell})_{\ell\in L})$ Dual
to Case 7.

Case 9. $(Lx.\nu_{\mathtt{t}};\mathsf{Q})$ where
$\mathtt{t}=^{k}_{\nu}\mathtt{C}$

$\star\;\mathbf{x}^{\alpha}:{[x^{\alpha}:\mathtt{t}]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{x^{\alpha}:\mathtt{t},y^{\beta}:B}(Lx.\nu_{\mathtt{t}};\mathsf{Q})\vdash_{\Lambda}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\mathbf{x}^{\alpha}:{[x^{\alpha}:\mathtt{t}]},\mathbf{c}^{\eta+1}:\mathsf{Msg}(x^{\alpha}.\nu_{t})\otimes\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{C},y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{1}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\mathbf{x}^{\alpha+1}:\mathsf{Msg}(x^{\alpha}.\nu_{t})\multimap{[x^{\alpha+1}:\mathtt{C}]},\mathbf{c}^{\eta+1}:\mathsf{Msg}(x^{\alpha}.\nu_{t})\otimes\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{C},y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{2}}\mathbf{y}^{\beta}:{[y^{\beta}:B]}\mathbf{x}^{\alpha+1}:\mathsf{Msg}(x^{\alpha}.\nu_{t})\multimap{[x^{\alpha+1}:\mathtt{C}]},\mathbf{w}^{\omega}:\mathsf{Msg}(x^{\alpha}.\nu_{t}),\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{C},y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{3}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\lx@proof@logical@and\mathbf{w}^{\omega}:\mathsf{Msg}(x^{\alpha}.\nu_{t})\vdash_{\Lambda_{3}}\mathbf{z}^{\zeta}:\mathsf{Msg}(x^{\alpha}.\nu_{t})\mathbf{x}^{\alpha+1}:{[x^{\alpha+1}:\mathtt{C}]},\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{C},y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{3}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\star$

$\Lambda_{2}=\Lambda_{1}\cup\\{\mathbf{c}^{\eta+1}_{n+2}<\mathbf{c}^{\eta}_{n+2}\\}\cup\\{\mathbf{c}^{\eta+1}_{i}=\mathbf{c}^{\eta}_{i}\mid
i\neq n+2\\},$
$\Lambda_{1}=\Lambda\cup\\{\mathbf{x}^{\alpha+1}_{i}=\mathbf{x}^{\alpha}_{i}\mid
i\neq k\\}\,,$
$\Lambda_{3}=\Lambda_{2}\cup\\{\mathbf{c}^{\eta+1}=\mathbf{w}^{\omega}\\}.$

In the proof of this case, we use the abbreviated definition of
$[x^{\alpha}:\mathtt{t}]$. If we use the following expanded definition instead

$\begin{array}[]{lcll}{[y^{\beta}:\mathtt{t}]}&=^{n+2}_{\mu}&\mathsf{Unfold}_{\mathtt{t}}(y^{\beta})\\\
\mathsf{Unfold}_{\mathtt{t}}(y^{\beta})&=^{i}_{\nu}&(\mathsf{Msg}(y^{\beta}.\nu_{t})\multimap[y^{\beta+1}:\mathtt{A}]),\par\end{array}$

we need to apply an extra $\mu L$ rule with priority $n+2$ on the predicate
$[x^{\alpha}:\mathtt{t}]$. Immediately after this $\mu L$ rule, we apply the
$\nu L$ rule with priority $k<n+1$. This implies that the extra $\mu L$ rule
does not play a role in validity of the derivation. As a result, the validity
of the derivation given here implies validity of the derivation using the non-
abbreviated definition. Furthermore, if we use the non-abbreviated definition
we will have $\mathbf{x}^{\alpha+2}:[x^{\alpha+1}:\mathtt{C}]$ at the end (the
top) of the cycle. Thus, we decided to use the abbreviated definition to make
sure that the generation of position variables steps at the same pace as the
generation of channels. This decision will help us to describe the
bisimulation between the derivation built here and the typing derivation of
processes in a more elegant way.

Case 10. $(Ry.\mu_{\mathtt{t}};\mathsf{Q})$ Dual to Case 9.

Case 11. $(\mathbf{case}Lx(\mu_{\mathtt{t}}\Rightarrow\mathsf{Q}))$ where
$\mathtt{t}=^{k}_{\mu}\mathtt{C}$

$\star\;{\mathbf{x}^{\alpha}:[x^{\alpha}:\mathtt{t}]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{x^{\alpha}:\mathtt{t},y^{\beta}:\mathtt{B}}(\mathbf{case}Lx(\mu_{\mathtt{t}}\Rightarrow\mathsf{Q}))\vdash_{\Lambda}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\mathbf{x}^{\alpha}:[x^{\alpha}:\mathtt{t}],\mathbf{c}^{\eta+1}:\mathsf{Msg}(x^{\alpha}.\mu_{t})\multimap\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{C},y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{1}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\mathbf{x}^{\alpha+1}:\mathsf{Msg}(x^{\alpha}.\mu_{t})\otimes{[x^{\alpha+1}:\mathtt{C}]},\mathbf{c}^{\eta+1}:\mathsf{Msg}(x^{\alpha}.\mu_{t})\multimap\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{C},y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{2}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\mathbf{w}^{\omega}:\mathsf{Msg}(x^{\alpha}.\mu_{t}),\mathbf{x}^{\alpha+1}:{[x^{\alpha+1}:\mathtt{C}]},\mathbf{c}^{\eta+1}:\mathsf{Msg}(x^{\alpha}.\mu_{t})\multimap\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{C},y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{3}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\lx@proof@logical@and\mathbf{w}^{\omega}:\mathsf{Msg}(x^{\alpha}.\mu_{t})\vdash_{\Lambda_{3}}\mathbf{z}^{\zeta}:\mathsf{Msg}(x^{\alpha}.\mu_{t})\mathbf{x}^{\alpha+1}:{[x^{\alpha+1}:\mathtt{C}]},\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{C},y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda_{3}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\star$

$\Lambda_{1}=\Lambda\cup\\{\mathbf{c}^{\eta+1}_{n+2}<\mathbf{c}^{\eta}_{n+2}\\}\cup\\{\mathbf{c}^{\eta+1}_{i}=\mathbf{c}^{\eta}_{i}\mid
i\neq n+2\\},$
$\Lambda_{2}=\Lambda_{1}\cup\\{\mathbf{x}^{\alpha+1}_{k}<\mathbf{x}^{\alpha}_{k}\\}\cup\\{\mathbf{x}^{\alpha+1}_{i}=\mathbf{x}^{\alpha}_{i}\mid
i\neq k\\}\,,$
$\Lambda_{3}=\Lambda_{2}\cup\\{\mathbf{x}^{\alpha+1}=\mathbf{w}^{\omega}\\}.$

Case 12 $(\mathbf{case}Ry(\nu_{\mathtt{t}}\Rightarrow\mathsf{Q}))$ Dual to
Case 11.

Case 13. $(y\leftarrow\mathsf{Y}\leftarrow x)$

${\star\;\mathbf{x}^{\alpha}:[x^{\alpha}:\mathtt{A}]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{x^{\alpha}:\mathtt{A},y^{\beta}:\mathtt{B}}(y\leftarrow\mathsf{Y}\leftarrow
x)\vdash_{\Lambda}{\mathbf{y}^{\beta}:[y^{\beta}:\mathtt{B}]}{\mathbf{x}^{\alpha}:[x^{\alpha}:\mathtt{A}]},\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{x^{\alpha}:\mathtt{A},y^{\beta}:\mathtt{B}}(Q)\vdash_{\Lambda\cup\\{c^{\eta+1}_{i}=c^{\eta}_{i}\mid
i\neq n+1\\}}{\mathbf{y}^{\beta}:[y^{\beta}:\mathtt{B}]}\star$

In cases 1-13 a predicate annotated with a position variable $\mathbf{c}$ in a
branch can be interpreted as the (potential) computational continuation of the
predicate $\mathsf{Cfg}()$ in the conclusion (at the bottom) of the block.
Also, the only predicates that occur as a cut formula are of the form
$[x^{\alpha}:\mathtt{A}]$.

Furthermore, in all the cases a rule is applied on $[x^{\alpha}:\mathtt{A}]$
only if there is a process in the antecedents willing to receive or send a
message along channels $x$ or $y$ via a $\mathsf{Msg}$ predicate: there is a
predicate in the antecedents of the form
$\mathsf{Msg}(x^{\alpha}.b)\circ\mathsf{Cfg}_{x^{\alpha+1}:p,\\_}(P)$ (or
$\&\\{\mathsf{Msg}(x^{\alpha}.b_{\ell})\circ\mathsf{Cfg}_{\\_,x^{\alpha+1}:p_{\ell}}(P_{\ell})\\}_{\ell\in
L}$ in cases 7 and 8 where $\circ\in\\{\otimes,\multimap\\}$.

Observe that in each circular branch a position variable $\mathbf{v}^{\delta}$
annotating a predicate $[v^{\delta}:\mathtt{D}]$ is only related by $<$ with
its own other generations $\mathbf{v}^{\gamma}$. These observations are
important in particular in the proof of Theorem 7.3.

We need to show that when defined over a guarded program the derivation
introduced above is a valid proof. Since a configuration is always finite, it
is enough to prove validity of the annotated derivation built using Cases 1-13
for a single process $\mathsf{P}$.

We use a validity-preserving bisimulation between the annotated derivation and
the typing derivation of process $\mathsf{P}$. The notation $\Omega\vDash
a\leq b$ stands for “the relation $a\leq b$ can be deduced from the reflexive
transitive closure of set $\Omega$".

######  Definition A.9.

Define relation $\mathcal{R}$ between process typing judgments

$y^{\beta}:B\vdash_{\Omega}\mathtt{P}::(x^{\alpha}:A)$

defined over $\mathbf{\Sigma}$ and annotated sequents in
$\mathit{FIMALL}^{\infty}_{\mu,\nu}$:

$\begin{array}[]{lcl}x^{\alpha}:\mathtt{A}\vdash_{\Omega}\mathsf{P}::(y^{\beta}:\mathtt{B})&\mathcal{R}&\mathbf{x}^{\alpha}:{[x^{\alpha}:\mathtt{A}]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{x^{\alpha}:\mathtt{A},y^{\beta}:\mathtt{B}}(\mathsf{P})\vdash_{\Omega^{\prime}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]},\\\
\cdot\vdash_{\Omega}\mathsf{P}::(y^{\beta}:\mathtt{B})&\mathcal{R}&\mathbf{c}^{\eta}:\mathsf{Cfg}_{\cdot,y^{\beta}:\mathtt{B}}(\mathsf{P})\vdash_{\Omega^{\prime}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]},\end{array}$

where333 $n$ is the maximum priority of fixed points in $\mathbf{\Sigma}$. for
$i\leq n$,

  * •

$\Omega\vDash x^{\alpha}_{i}\leq w^{\zeta}_{i}$ iff
$\Omega^{\prime}\vDash\mathbf{x}^{\alpha}_{i}\leq\mathbf{w}^{\zeta}_{i}$, and

  * •

$\Omega\vDash y^{\beta}_{i}\leq w^{\zeta}_{i}$ iff
$\Omega^{\prime}\vDash\mathbf{y}^{\beta}_{i}\leq\mathbf{w}^{\zeta}_{i}$.

We define two stepping rules over the typing derivation of a process and the
derivation built in the proof of Lemma 1.

######  Definition A.10.

We define two stepping rules $\hookrightarrow$ and $\Rightarrow$ over
processes and annotated sequents, respectively:

  * •

$\bar{x}^{\alpha}:\omega\vdash_{\Omega}\mathsf{P}::(y^{\beta}:\mathtt{B})\hookrightarrow\bar{z}^{\delta}:\omega^{\prime}\vdash_{\Lambda}\mathsf{Q}::(w^{\gamma}:\mathtt{D})$
iff there is a rule in the infinitary system of Figure 8 of the form

$\bar{x}^{\alpha}:\omega\vdash_{\Omega}\mathsf{P}::(y^{\beta}:\mathtt{B})\lx@proof@logical@and\cdots\bar{z}^{\delta}:\omega^{\prime}\vdash_{\Lambda}\mathsf{Q}::(w^{\gamma}:\mathtt{D})\cdots$

  * •

${(i)\;\overline{\mathbf{x}^{\alpha}:{[\bar{x}^{\alpha}:\omega]}},\mathbf{c}^{\eta_{1}}:\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,y^{\beta}:\mathtt{B}}(\mathsf{P})\vdash_{\Omega}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\Rightarrow(ii)\;\overline{\mathbf{z}^{\delta}:{[\bar{z}^{\delta}:\omega^{\prime}]}},\mathbf{d}^{\eta_{2}}:\mathsf{Cfg}_{\bar{z}^{\delta}:\omega^{\prime},w^{\gamma}:\mathtt{D}}(\mathsf{Q})\vdash_{\Lambda}\mathbf{w}^{\gamma}:{[w^{\gamma}:\mathtt{D}]}}$
iff (i) is the conclusion of one of the blocks 1-13 in the proof of Lemma 1
and (ii) is a $\star$ assumption of it.

Next we prove that relation $\mathcal{R}$ is a validity preserving
bisimulation with regard to the steppings $\hookrightarrow$ and $\Rightarrow$.

######  Lemma A.11.

$\mathcal{R}$ forms a bisimulation between the derivation given for

$\star\,\overline{\mathbf{x}^{\alpha}:[\bar{x}^{\alpha}:\omega]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,y^{\beta}:\mathtt{B}}(\mathsf{P})\vdash_{\Omega^{\prime}}\mathbf{y}^{\beta}:[y^{\beta}:\mathtt{B}]$

and the typing derivation of process

$\bar{x}^{\alpha}:\omega\vdash_{\Omega}\mathsf{P}::(y^{\beta}:\mathtt{B}).$

######  Proof A.12.

The proof of this bisimulation is straightforward. It follows from the way we
built proof blocks for each case in Lemma 1, and the typing rules for
annotated processes in Figure 8:

$\rightarrow$:

${\bar{x}^{\alpha}:\omega\vdash_{\Omega}\mathsf{P}::(y^{\beta}:\mathtt{B})}$${\overline{\mathbf{x}^{\alpha}:[\bar{x}^{\alpha}:\omega]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,y^{\beta}:\mathtt{B}}(\mathsf{P})\vdash_{\Omega^{\prime}}\mathbf{y}^{\beta}:[y^{\beta}:\mathtt{B}]}$${\bar{z}^{\gamma}:\omega^{\prime}\vdash_{\Lambda}\mathsf{Q}::(w^{\delta}:\mathtt{D})}$${\overline{\mathbf{z}^{\gamma}:{[\bar{z}^{\gamma}:\omega^{\prime}]}},\mathbf{d}^{\theta}:\mathsf{Cfg}_{\bar{z}^{\gamma}:\omega^{\prime},w^{\delta}:\mathtt{D}}(\mathsf{Q})\vdash_{\Lambda^{\prime}}\mathbf{w}^{\delta}:{[w^{\delta}:\mathtt{D}]}}$$\scriptstyle{\mathcal{R}}$$\scriptstyle{\mathcal{R}}$

The proof is by considering different cases for $\hookrightarrow$:

Case 1. ($\mathbf{wait}Lx;\mathsf{Q}$)

$\begin{array}[]{lr}1.\mbox{Premise}&x^{\alpha}:1\vdash_{\Omega}\mathbf{wait}Lx;\mathsf{Q}::y^{\beta}:\mathtt{B}\hookrightarrow\cdot\vdash_{\Omega}\mathsf{Q}::y^{\beta}:\mathtt{B}\\\
2.\mbox{Block
3}&\mathbf{x}^{\alpha}:{[x^{\alpha}:1]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{x^{\alpha}:1,y^{\beta}:B}(\mathbf{wait}Lx;\mathsf{Q})\vdash_{\Omega^{\prime}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\Rightarrow\\\
&\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{\cdot,y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda^{\prime}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\\\
3.\mbox{Definition of $\Lambda^{\prime}$}&\mbox{for}\,i\leq
n,\Lambda^{\prime}\vDash\mathbf{y}^{\beta}_{i}\leq\mathbf{z}_{i}^{\gamma}\;\mbox{iff}\;\Omega^{\prime}\vDash\mathbf{y}^{\beta}_{i}\leq\mathbf{z}_{i}^{\gamma}.\\\
4.\mbox{By assumption and line 3}&\mbox{for}\,i\leq
n,\Lambda^{\prime}\vDash\mathbf{y}^{\beta}_{i}\leq\mathbf{z}_{i}^{\gamma}\;\mbox{iff}\;\Omega\vDash
y^{\beta}_{i}\leq z_{i}^{\gamma}\\\ 5.\mbox{By line
4}&\cdot\vdash_{\Omega}\mathsf{Q}::y^{\beta}:\mathtt{B}\;\mathcal{R}\;\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{\cdot,y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda^{\prime}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\end{array}$

Case 2. ($Lx.\nu_{\mathtt{t}};\mathsf{Q}$)

$\begin{array}[]{lr}1.\mbox{Premise}&x^{\alpha}:\mathtt{t}\vdash_{\Omega}\mathtt{Lx.\nu_{\mathtt{t}};\mathsf{Q}}::y^{\beta}:\mathtt{B}\hookrightarrow
x^{\alpha+1}:\mathtt{C}\vdash_{\Lambda}Q::y^{\beta}:\mathtt{B}\\\
2.\mbox{Block
9}&\mathbf{x}^{\alpha}:{[x^{\alpha}:\mathtt{t}]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{x^{\alpha}:\mathtt{t},y^{\beta}:\mathtt{B}}(Lx.\nu_{\mathtt{t}};\mathsf{Q})\vdash_{\Omega^{\prime}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\Rightarrow\\\
&\mathbf{x}^{\alpha+1}:{[x^{\alpha+1}:\mathtt{C}]},\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{C},y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda^{\prime}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\\\
3.\mbox{Definition of $\Lambda^{\prime}$}&\mbox{for}\,i\leq
n,\Lambda^{\prime}\vDash\mathbf{y}^{\beta}_{i}\leq\mathbf{z}_{i}^{\gamma}\;\mbox{iff}\;\Omega^{\prime}\vDash\mathbf{y}^{\beta}_{i}\leq\mathbf{z}_{i}^{\gamma}.\\\
4.\mbox{Definition of $\Lambda$}&\mbox{for}\,i\leq n,\Lambda\vDash
y^{\beta}_{i}\leq z_{i}^{\gamma}\;\mbox{iff}\;\Omega\vDash y^{\beta}_{i}\leq
z_{i}^{\gamma}.\\\ 5.\mbox{By assumption}&\mbox{for}\,i\leq
n,\Lambda^{\prime}\vDash\mathbf{y}^{\beta}_{i}\leq\mathbf{z}_{i}^{\gamma}\;\mbox{iff}\;\Lambda\vDash
y^{\beta}_{i}\leq z_{i}^{\gamma}\\\ 6.\mbox{Definition of
$\Lambda^{\prime}$}&\mbox{for}\,i\leq n\;\mbox{and}\;z^{\gamma}\neq
x^{\alpha+1},\Lambda^{\prime}\vDash\mathbf{x}^{\alpha+1}_{i}\leq\mathbf{z}_{i}^{\gamma}\;\mbox{iff}\;\Omega^{\prime}\vDash\mathbf{x}^{\alpha}_{i}\leq\mathbf{z}_{i}^{\gamma}.\\\
7.\mbox{Definition of $\Lambda$}&\mbox{for}\,i\leq
n,\;\mbox{and}\;z^{\gamma}\neq x^{\alpha+1},\Lambda\vDash x^{\alpha+1}_{i}\leq
z_{i}^{\gamma}\;\mbox{iff}\;\Omega\vDash x^{\alpha}_{i}\leq z_{i}^{\gamma}.\\\
8.\mbox{By assumption}&\mbox{for}\,i\leq
n,\Lambda^{\prime}\vDash\mathbf{x}^{\alpha+1}_{i}\leq\mathbf{z}_{i}^{\gamma}\;\mbox{iff}\;\Lambda\vDash
x^{\alpha+1}_{i}\leq z_{i}^{\gamma}\\\ 9.\mbox{By lines 5 and
9}&x^{\alpha+1}:\mathtt{C}\vdash_{\Lambda}Q::y^{\beta}:\mathtt{B}\;\mathcal{R}\;\mathbf{x}^{\alpha+1}:{[x^{\alpha+1}:\mathtt{C}]},\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{C},y^{\beta}:\mathtt{B}}(Q)\vdash_{\Lambda^{\prime}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\end{array}$

Cases. The proof of other cases is similar to the previous ones.

$\leftarrow$.

${\bar{x}^{\alpha}:\omega\vdash_{\Omega}\mathsf{P}::(y^{\beta}:\mathtt{B})}$${\overline{\mathbf{x}^{\alpha}:[\bar{x}^{\alpha}:\omega]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,y^{\beta}:\mathtt{B}}(\mathsf{P})\vdash_{\Omega^{\prime}}\mathbf{y}^{\beta}:[y^{\beta}:\mathtt{B}]}$${\bar{z}^{\gamma}:\omega^{\prime}\vdash_{\Lambda}\mathsf{\mathsf{Q}}::(w^{\delta}:\mathtt{D})}$${\overline{\mathbf{z}^{\gamma}:{[\bar{z}^{\gamma}:\omega^{\prime}}]},\mathbf{d}^{\theta}:\mathsf{Cfg}_{\bar{z}^{\gamma}:\omega^{\prime},w^{\delta}:\mathtt{D}}(\mathsf{Q})\vdash_{\Lambda^{\prime}}\mathbf{w}^{\delta}:{[w^{\delta}:D]}}$$\scriptstyle{\mathcal{R}}$$\scriptstyle{\mathcal{R}}$

The proof is by considering different cases for $\Rightarrow$.

Case 1. ($\mathbf{wait}Lx;\mathsf{Q}$)

$\begin{array}[]{lr}1.\mbox{Premise}&\mathbf{x}^{\alpha}:{[x^{\alpha}:1]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{x^{\alpha}:1,y^{\beta}:B}(\mathbf{wait}Lx;\mathsf{Q})\vdash_{\Omega^{\prime}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\Rightarrow\\\
&\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{\cdot,y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda^{\prime}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\\\
2.\mbox{By $1L$ typing
rule}&x^{\alpha}:1\vdash_{\Omega}\mathbf{wait}Lx;\mathsf{Q}::y^{\beta}:\mathtt{B}\hookrightarrow\cdot\vdash_{\Omega}\mathsf{Q}::y^{\beta}:\mathtt{B}\\\
3.\mbox{Definition of $\Lambda^{\prime}$}&\mbox{for}\,i\leq
n,\Lambda^{\prime}\vDash\mathbf{y}^{\beta}_{i}\leq\mathbf{z}_{i}^{\gamma}\;\mbox{iff}\;\Omega^{\prime}\vDash\mathbf{y}^{\beta}_{i}\leq\mathbf{z}_{i}^{\gamma}.\\\
4.\mbox{By assumption and line 3}&\mbox{for}\,i\leq
n,\Lambda^{\prime}\vDash\mathbf{y}^{\beta}_{i}\leq\mathbf{z}_{i}^{\gamma}\;\mbox{iff}\;\Omega\vDash
y^{\beta}_{i}\leq z_{i}^{\gamma}\\\ 5.\mbox{By line
4}&\cdot\vdash_{\Omega}\mathsf{Q}::y^{\beta}:\mathtt{B}\;\mathcal{R}\;\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{\cdot,y^{\beta}:\mathtt{B}}(\mathsf{Q})\vdash_{\Lambda^{\prime}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\end{array}$

Case 2. ($Lx.\nu_{t};\mathsf{Q}$)

$\begin{array}[]{lr}1.\mbox{Premise}&\mathbf{x}^{\alpha}:{[x^{\alpha}:\mathtt{t}]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{x^{\alpha}:\mathtt{t},y^{\beta}:\mathtt{B}}(Lx.\nu_{\mathtt{t}};Q)\vdash_{\Omega^{\prime}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\Rightarrow\\\
&\mathbf{x}^{\alpha+1}:{[x^{\alpha+1}:\mathtt{C}]},\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{C},y^{\beta}:\mathtt{B}}(Q)\vdash_{\Lambda^{\prime}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\\\
2.\mbox{By $\nu L$ typing
rule}&x^{\alpha}:\mathtt{t}\vdash_{\Omega}\mathtt{Lx.\nu_{t};Q}::y^{\beta}:\mathtt{B}\hookrightarrow
x^{\alpha+1}:\mathtt{C}\vdash_{\Lambda}Q::y^{\beta}:\mathtt{B}\\\
3.\mbox{Definition of $\Lambda^{\prime}$}&\mbox{for}\,i\leq
n,\Lambda^{\prime}\vDash\mathbf{y}^{\beta}_{i}\leq\mathbf{z}_{i}^{\gamma}\;\mbox{iff}\;\Omega^{\prime}\vDash\mathbf{y}^{\beta}_{i}\leq\mathbf{z}_{i}^{\gamma}.\\\
4.\mbox{Definition of $\Lambda$}&\mbox{for}\,i\leq n,\Lambda\vDash
y^{\beta}_{i}\leq z_{i}^{\gamma}\;\mbox{iff}\;\Omega\vDash y^{\beta}_{i}\leq
z_{i}^{\gamma}.\\\ 5.\mbox{By assumption}&\mbox{for}\,i\leq
n,\Lambda^{\prime}\vDash\mathbf{y}^{\beta}_{i}\leq\mathbf{z}_{i}^{\gamma}\;\mbox{iff}\;\Lambda\vDash
y^{\beta}_{i}\leq z_{i}^{\gamma}\\\ 6.\mbox{Definition of
$\Lambda^{\prime}$}&\mbox{for}\,i\leq n\;\mbox{and}\;z^{\gamma}\neq
x^{\alpha+1},\Lambda^{\prime}\vDash\mathbf{x}^{\alpha+1}_{i}\leq\mathbf{z}_{i}^{\gamma}\;\mbox{iff}\;\Omega^{\prime}\vDash\mathbf{x}^{\alpha}_{i}\leq\mathbf{z}_{i}^{\gamma}.\\\
7.\mbox{Definition of $\Lambda$}&\mbox{for}\,i\leq
n,\;\mbox{and}\;z^{\gamma}\neq x^{\alpha+1},\Lambda\vDash x^{\alpha+1}_{i}\leq
z_{i}^{\gamma}\;\mbox{iff}\;\Omega\vDash x^{\alpha}_{i}\leq z_{i}^{\gamma}.\\\
8.\mbox{By assumption}&\mbox{for}\,i\leq
n,\Lambda^{\prime}\vDash\mathbf{x}^{\alpha+1}_{i}\leq\mathbf{z}_{i}^{\gamma}\;\mbox{iff}\;\Lambda\vDash
x^{\alpha+1}_{i}\leq z_{i}^{\gamma}\\\ 9.\mbox{By lines 5 and
9}&x^{\alpha+1}:\mathtt{C}\vdash_{\Lambda}Q::y^{\beta}:\mathtt{B}\;\mathcal{R}\;\mathbf{x}^{\alpha+1}:{[x^{\alpha+1}:\mathtt{C}]},\mathbf{c}^{\eta+1}:\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{C},y^{\beta}:\mathtt{B}}(Q)\vdash_{\Lambda^{\prime}}\mathbf{y}^{\beta}:{[y^{\beta}:\mathtt{B}]}\end{array}$

Cases. Similar to the previous cases.

######  Lemma A.13.

If

$\bar{x}^{\alpha}:\omega\vdash_{\emptyset}\mathsf{P}::(y^{\beta}:B)$

is a guarded process, then a derivation built in Lemma 1 for

$\star\,\overline{\mathbf{x^{\alpha}}:[\bar{x}^{\alpha}:\omega]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,y^{\beta}:\mathtt{B}}(\mathsf{P})\vdash_{\emptyset}\mathbf{y}^{\beta}:[y^{\beta}:\mathtt{B}]$

is valid.

######  Proof A.14.

By assumption there is an (infinitary) guarded typing derivation
$\mathcal{D}_{1}$ for process
$\bar{x}^{\alpha}:\omega\vdash_{\emptyset}\mathsf{P}::(y^{\beta}:\mathtt{B})$.
By Lemma A.11, we build a bisimilar (infinite) derivation for
$\star\,\overline{\mathbf{x^{\alpha}}:[\bar{x}^{\alpha}:\omega]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,y^{\beta}:\mathtt{B}}(\mathsf{P})\vdash_{\emptyset}\mathbf{y}^{\beta}:[y^{\beta}:\mathtt{B}]$
using Cases (1-13) in Lemma 1. Consider an infinite path $\mathtt{p}_{2}$ in
$\mathcal{D}_{2}$ and its bisimilar path $\mathtt{p}_{1}$ in
$\mathcal{D}_{1}$:

${\cdots}$${\cdots}$${\bar{x}^{\alpha}:\omega\vdash_{\Omega}\mathsf{P}::(y^{\beta}:\mathtt{B})}$${\overline{\mathbf{x}^{\alpha}:[\bar{x}^{\alpha}:\omega]},\mathbf{c}^{\eta}:\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,y^{\beta}:\mathtt{B}}(\mathsf{P})\vdash_{\Omega^{\prime}}\mathbf{y}^{\beta}:[y^{\beta}:\mathtt{B}]}$${\bar{z}^{\gamma}:\omega^{\prime}\vdash_{\Lambda}\mathsf{Q}::(w^{\delta}:\mathtt{D})}$${\overline{\mathbf{z}^{\gamma}:{[\bar{z}^{\gamma}:\omega^{\prime}]}},\mathbf{d}^{\theta}:\mathsf{Cfg}_{\bar{z}^{\gamma}:\omega^{\prime},w^{\delta}:\mathtt{D}}(\mathsf{Q})\vdash_{\Lambda^{\prime}}\mathbf{w}^{\delta}:{[w^{\delta}:\mathtt{D}]}}$${\cdots}$${\cdots}$$\scriptstyle{*}$$\scriptstyle{*}$$\scriptstyle{\mathcal{R}}$$\scriptstyle{k}$$\scriptstyle{k}$$\scriptstyle{\mathcal{R}}$$\scriptstyle{*}$$\scriptstyle{*}$

By definition of $\mathcal{R}$,

  * •

if $\Lambda\vDash\mathsf{snap}(z^{\gamma})<\mathsf{snap}(x^{\alpha})$, then
$\Lambda^{\prime}\vDash\mathsf{snap}(\mathtt{z}^{\gamma})<\mathtt{snap}(\mathsf{x}^{\alpha})$,
and

  * •

if $\Lambda\vDash\mathsf{snap}(w^{\delta})<\mathsf{snap}(y^{\beta})$, then
$\Lambda^{\prime}\vDash\mathsf{snap}(\mathtt{w}^{\delta})<\mathtt{snap}(\mathsf{y}^{\beta})$.

By the above property if path $\mathtt{p}_{1}$ is guarded, then
$\mathtt{p}_{2}$ is valid.

######  Theorem 2..

For the judgment
$\bar{x}^{\alpha}:\omega\Vdash\mathcal{C}::(y^{\beta}:\mathtt{B})$ where
$\mathcal{C}$ is a configuration of guarded processes, there is a valid cut-
free proof for $\mathcal{C}\in\llbracket\bar{x}^{\alpha}:\omega\vdash
y^{\beta}:\mathtt{B}\rrbracket$ in $\mathit{FIMALL}^{\infty}_{\mu,\nu}$.
Validity of this proof ensures the strong progress property of $\mathcal{C}$.

######  Proof A.15.

It is enough to show that the valid proof we built for

$\star{\,\overline{[\bar{x}^{\alpha}:\omega]},\mathsf{Cfg}_{\bar{x}^{\alpha}:\omega,y^{\beta}:\mathtt{B}}(\mathcal{C})\vdash[y^{\beta}:\mathtt{B}]}$

in $\mathit{FIMALL}^{\infty}_{\mu,\nu}$ ensures the strong progress property
of configuration $\mathcal{C}$. Here $\bar{x}^{\alpha}$ and $y^{\beta}$ are
external channels of the configuration $\mathcal{C}$.

We run the cut elimination algorithm on the valid proof we built in Lemma 1.
By the structure of the proof, we know that the first step in the cut
elimination algorithm is to apply an external reduction (Flip rule) on
$\mathsf{Cfg}_{x^{\alpha}:\omega,y^{\beta}:\mathtt{B}}(\mathcal{C})$ to unfold
its definition. The tape transforms to

${\,\overline{[\bar{x}^{\alpha}:\omega]},T\vdash[y^{\beta}:\mathtt{B}]}$

where $T$ is the definition given based on the pattern of $\mathcal{C}$.

In fact, we can prove that throughout the cut elimination procedure, we
repeatedly get a branching tape of the form444There may be other judgments of
the form $T\vdash T$ on the tape that do not contribute to the computational
meaning of the tape. Without loss of generality, we do not present them in the
next line, but we will explain how to deal with them in the proof.

${\overline{[\bar{x}^{\alpha}:\omega]},T_{1}\vdash[z_{1}^{\eta_{1}}:\mathtt{D_{1}}],[z_{1}^{\eta_{1}}:\mathtt{D_{1}}],T_{2}\vdash[z_{2}^{\eta_{2}}:\mathtt{D_{2}}],\cdots[z_{m}^{\eta_{m}}:\mathtt{D_{m}}],T_{m+1}\vdash[y^{\beta}:\mathtt{B}]}$

where $T_{i+1}$ is the definition of a predicate
$\mathsf{Cfg}_{z_{i}^{\eta_{i}}:\mathtt{D}_{i},z_{i+1}^{\eta_{i+1}}:\mathtt{D}_{i+1}}(\mathcal{C}_{i+1})$,
and it explains the behavior of the computational continuation of
$\mathcal{C}$ with regards to channels $\bar{z}_{i}^{\eta_{i}}$ and
$\bar{z}_{i+1}^{\eta_{i+1}}$. Moreover, if an external reduction rule is
applied on $[x^{\alpha}:\omega]$ or $[y^{\beta}:\mathtt{B}]$, there is a
process willing to send or receive a message along $x^{\alpha}$ or
$y^{\beta}$. 555Put $z_{0}^{\eta_{0}}=x^{\alpha}$ and
$z_{m+1}^{\eta_{m+1}}=y^{\beta}$. Note that channels $z_{i}^{\eta_{i}}$ for
$1\leq i\leq m$ are the internal channels of the configuration, and channels
$x^{\alpha}$ and $y^{\beta}$ are the external channels.

This property holds after the very first rule of cut elimination (an external
reduction on $\mathsf{Cfg}(\mathcal{C})$ which leads to the tape
${\,\overline{[\bar{x}^{\alpha}:\omega]},T\vdash[y^{\beta}:\mathtt{B}]}$). We
want to prove that the property explained in the previous paragraph holds as
an invariant on the tapes being produced by the cut elimination algorithm if
we apply the cut elimination algorithm in the following order 666Our cut
elimination algorithm is non-deterministic in the sense that there might be
two applicable reductions at each time. However, we proved that no matter what
rule we choose, the algorithm will terminate on valid proofs. Here, we single
out one particular way of running the cut-elimination property.:

Step 1. Communication along an external channel: an external reduction can be
applied on predicates $[x^{\alpha}:\omega]$ or $[y^{\beta}:\mathtt{B}]$.
In Figure 13 we provide the steps of our cut elimination algorithm when a rule
can be applied on a predicate
$[x^{\alpha}:\oplus\\{\ell:\mathtt{A}_{\ell}\\}_{\ell\in L}]$. The cases for
other types are similar. First observe that by the structure of the proof,
this is only the case if in the configuration a process communicates along a
left external channel $x^{\alpha}$ of type
$\oplus\\{\ell:\mathtt{A}_{\ell}\\}_{\ell\in L}$. Moreover, in Line 4 of
Figure 13 the algorithm creates multiple branches: the continuation of
processes $\mathbf{case}Lx(\ell\Rightarrow\mathsf{Q}_{\ell})_{\ell\in L}$
depends on the potential label $k\in L$ that it receives along the external
channel $x^{\alpha}$. The tape we have at the end of each branch corresponds
to a potential configuration in the computation. On line (8) we unfold the
definition of
$\mathsf{Cfg}_{x^{\alpha+1};\mathtt{A}_{k},v^{\delta}:\mathtt{D}}(Q_{k})$
predicate to get the invariant we are looking for. We start over the cut
elimination procedure for the new tape.

On line (7) we create an extra branch containing a single (green) judgment

${\mathsf{Msg}(x^{\alpha}.k)\vdash\mathsf{Msg}(x^{\alpha}.k)}.$

This tape can be closed by a single ID-elim rule.

${\begin{array}[]{ll}(1)\qquad{[x^{\alpha}:\oplus\\{\ell:\mathtt{A}_{\ell}\\}_{\ell\in
L}]},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{Cfg}_{x^{\alpha}:\oplus\\{\ell:A_{\ell}\\}_{\ell\in
L},v^{\delta}:\mathtt{D}}(\mathbf{case}Lx(\ell\Rightarrow\mathsf{Q}_{\ell})_{\ell\in
L})}\vdash{[v^{\delta}:\mathtt{D}]}\\\ \hskip
256.0748pt\Downarrow\mbox{External reduction}(\mu)\\\ \hline\cr\\\
(2)\qquad{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}[x^{\alpha}:\oplus\\{\ell:\mathtt{A}_{\ell}\\}_{\ell\in
L}]},\&\\{\ell:\mathsf{Msg}(x^{\alpha}.\ell)\multimap\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{A}_{\ell},v^{\delta}:\mathtt{D}}(\mathsf{Q}_{\ell})\\}_{\ell\in
L}\vdash{[v^{\delta}:\mathtt{D}]}\\\ \hskip 256.0748pt\Downarrow\mbox{External
reduction}(\mu)\\\ \hline\cr\\\
(3)\qquad{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\oplus\\{\ell:(\mathsf{Msg}(x^{\alpha}.\ell)\otimes[x^{\alpha+1}:\mathtt{A}_{\ell}])\\}_{\ell\in
L}},\&\\{\ell:\mathsf{Msg}(x^{\alpha}.\ell)\multimap\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{A}_{\ell},v^{\delta}:\mathtt{D}}(\mathsf{Q}_{\ell})\\}_{\ell\in
L}\vdash{[v^{\delta}:\mathtt{D}]}\\\ \hskip
256.0748pt\Downarrow\color[rgb]{.75,0,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,0,.25}{\mbox{External
reduction}(\oplus)}\\\ \hline\cr\\\ (4)\qquad\forall k\in
L\qquad(\mathsf{Msg}(x^{\alpha}.k)\otimes[x^{\alpha+1}:\mathtt{A}_{k}]),{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\&\\{\ell:\mathsf{Msg}(x^{\alpha}.\ell)\multimap\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{A}_{\ell},v^{\delta}:\mathtt{D}}(\mathsf{Q}_{\ell})\\}_{\ell\in
L}}\vdash{[v^{\delta}:\mathtt{D}]}\\\ \hskip
256.0748pt\Downarrow\mbox{External reduction}(\&)\\\ \hline\cr\\\
(5)\qquad\forall k\in
L\qquad{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(\mathsf{Msg}(x^{\alpha}.k)\otimes[x^{\alpha+1}:\mathtt{A}_{k}])},(\mathsf{Msg}(x^{\alpha}.k)\multimap\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{A}k,v^{\delta}:\mathtt{D}}(\mathsf{Q}_{k})\vdash{[v^{\delta}:\mathtt{D}]}\\\
\hskip 256.0748pt\Downarrow\mbox{External reduction}(\otimes)\\\ \hline\cr\\\
(6)\qquad\forall k\in
L\qquad\mathsf{Msg}(x^{\alpha}.k),[x^{\alpha+1}:\mathtt{A}_{k}],{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{Msg}(x^{\alpha}.k)\multimap\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{A}k,v^{\delta}:\mathtt{D}}(\mathsf{Q}_{k})}\vdash{[v^{\delta}:\mathtt{D}]}\\\
\hskip 256.0748pt\Downarrow\mbox{External reduction}(\multimap)\\\
\hline\cr\\\ (7)\qquad\forall k\in
L\qquad[x^{\alpha+1}:\mathtt{A}_{k}],{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{Cfg}_{x^{\alpha+1}:\mathtt{A}k,v^{\delta}:\mathtt{D}}(\mathsf{Q}_{k})}\vdash{[v^{\delta}:\mathtt{D}]}\quad\hskip
47.80042pt{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\mathsf{Msg}(x^{\alpha}.k)\vdash\mathsf{Msg}(x^{\alpha}.k)}(\mbox{Identity
elimination})\\\ \hskip 170.71652pt\Downarrow\mbox{External Reduction}(\mu)\\\
\hline\cr\\\ (8)\qquad\forall k\in
L\qquad[x^{\alpha+1}:\mathtt{A}_{k}],T_{k}\vdash{[v^{\delta}:\mathtt{D}]}\\\
\end{array}}$ Figure 13: A run of the cut elimination algorithm when there is
a process communicating along an external channel.

Step 2. An external reduction rule can be applied on a $T_{i}$:

  * •

2.1. Identity: Consider all judgments on the tape which are of the form

$[u^{\gamma}:\mathtt{F}],u^{\gamma}=w^{\delta}\vdash[w^{\delta}:\mathtt{F}].$

We first apply external reductions ($=L$) on the antecedents of the form
$u^{\gamma}=w^{\delta}$. This rule renames channels $u^{\gamma}$ and
$w^{\delta}$ with their most general unifier $z^{\eta}$.

We ignore the remainder of the judgments of the form
$[z^{\eta}:\mathtt{F}]\vdash[z^{\eta}:\mathtt{F}]$ until Step 2.4. The rest of
the tape preserves the property of interest, since we only renamed
computationally identical channels in it.

  * •

2.2. Spawn: Consider all the judgments on the tape that are of the form

$[\bar{u}^{\gamma}:\omega^{\prime}],\exists
v.\exists\zeta.(\mathsf{Cfg}_{\bar{u}^{\gamma}:\omega^{\prime},v^{\zeta}:\mathtt{E}}(\mathcal{C}_{1})\otimes\mathsf{Cfg}_{v^{\zeta}:\mathtt{E},w^{\delta}:\mathtt{F}}(\mathcal{C}_{2}))\vdash[w^{\delta}:\mathtt{F}].$

We apply two external reduction rules ($\exists$ and $\otimes$) on them to get
judgments of the form
$[\bar{u}^{\gamma}:\omega^{\prime}],(\mathsf{Cfg}_{\bar{u}^{\gamma}:\omega^{\prime},v^{\zeta}:\mathtt{E}}(\mathcal{C}_{1}),\mathsf{Cfg}_{v^{\zeta}:\mathtt{E},w^{\delta}:\mathtt{F}}(\mathcal{C}_{2})))\vdash[w^{\delta}:\mathtt{F}]$.

  * •

2.3. We apply identity elimination on all the remainder identity judgments
that we have ignored (including the ones from Step 2.1).

  * •

2.4. We apply a Merge rule on all judgments remaining from Step 2.2 which are
of the form

$[\bar{u}^{\gamma}:\omega^{\prime}],(\mathsf{Cfg}_{\bar{u}^{\gamma}:\omega^{\prime},v^{\zeta}:\mathtt{E}}(\mathcal{C}_{1}),\mathsf{Cfg}_{v^{\zeta}:\mathtt{E},w^{\delta}:\mathtt{F}}(\mathcal{C}_{2})))\vdash[w^{\delta}:\mathtt{F}].$

It replaces them with two judgments connected with a fresh internal channel
$v^{\zeta}$:

$[\bar{u}^{\gamma}:\omega^{\prime}],(\mathsf{Cfg}_{\bar{u}^{\gamma}:\omega^{\prime},v^{\zeta}:\mathtt{E}}(\mathcal{C}_{1})\vdash[v^{\zeta}:\mathtt{E}]\qquad[v^{\zeta}:\mathtt{E}],\mathsf{Cfg}_{v^{\zeta}:\mathtt{E},w^{\delta}:\mathtt{F}}(\mathcal{C}_{2}))\vdash[w^{\delta}:\mathtt{F}].$

$\mathcal{C}_{1}$ is the configuration (or a process) spawned and
$\mathcal{C}_{2}$ is the continuation. With two other external reductions on
the $\mathsf{Cfg}$ predicates, we unfold the definition of the predicates
based on their pattern and get back to a tape satisfying the invariant. We
start over the procedure from Step 1. 777We need to break down this step to be
compatible with the order enforced by the cut elimination algorithm.

Step 3. Communication along an internal channel: an internal reduction can be
applied on predicates of the form $[w^{\gamma}:\mathtt{A}]$.
We provide the steps of the cut elimination algorithm for a case in which the
protocol of communication is an internal choice ($\oplus$) in Figure 14. The
other cases are similar.888Our system is based on an asynchronous semantics.
However, cut elimination is a synchronous procedure. When we run our cut
elimination algorithm on this particular derivation, it models a synchronized
sending and receiving messages between processes. It is straightforward to
observe that both processes $\mathsf{P}$ and $\mathsf{Q}_{k}$ are the
computational continuations of the original processes in the configuration:
$(Rw.k;\mathsf{P})$ sends the label $k$ along the internal channel
$w^{\gamma}$ and steps to $\mathsf{P}$. Process
$\mathbf{case}Lw(\ell\Rightarrow\mathsf{Q}_{\ell})_{\ell\in L}$ when receiving
label $k$ along channel $w^{\gamma}$ steps to $\mathsf{Q}_{k}$. Similar to
Step 1. with two external reductions on the $\mathsf{Cfg}$ predicates, we get
back to a tape satisfying the invariant.

Similar to Step 1. here we get an extra (green) tape with the single judgment
${{\mathsf{Msg}(w^{\gamma}.k)\vdash\mathsf{Msg}(w^{\gamma}.k)}}$ that can be
closed by an ID-elim. We also add a similar extra judgment
${{\mathsf{Msg}(w^{\gamma}.k)\vdash\mathsf{Msg}(w^{\gamma}.k)}}$ to the
current tape by a $\otimes$ principal reduction. To be compatible with the
order enforced by the cut elimination algorithm, we ignore this judgment until
the next Step 2.3.

${\begin{array}[]{ll}{[z^{\eta}:\mathtt{C}]},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{Cfg}_{z^{\eta}:\mathtt{C},w^{\gamma}:\oplus\\{\ell:A_{\ell}\\}_{\ell\in
L}}(Rw.k;\mathsf{P})}\vdash{[w^{\gamma}:\oplus\\{\ell:\mathtt{A}_{\ell}\\}_{\ell\in
L}]}\\\ \hskip
56.9055pt{[w^{\gamma}:\oplus\\{\ell:\mathtt{A}_{\ell}\\}_{\ell\in
L}]},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{Cfg}_{w^{\gamma}:\oplus\\{\ell:A_{\ell}\\}_{\ell\in
L},v^{\delta}:\mathtt{D}}(\mathbf{case}Lw(\ell\Rightarrow\mathsf{Q}_{\ell})_{\ell\in
L})}\vdash{[v^{\delta}:\mathtt{D}]}\\\ \hskip
256.0748pt\Downarrow\mbox{External reduction}(\mu)\\\ \hline\cr\\\
{[\bar{z}^{\eta}:\omega]},\mathsf{Msg}(w^{\gamma}.k)\otimes\mathsf{Cfg}_{\bar{z}^{\eta}:\omega,w^{\gamma+1}:\mathtt{A}_{k}}(\mathsf{P})\vdash{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[w^{\gamma}:\oplus\\{\ell:\mathtt{A}_{\ell}\\}_{\ell\in
L}]}\\\ \hskip
56.9055pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}[w^{\gamma}:\oplus\\{\ell:\mathtt{A}_{\ell}\\}_{\ell\in
L}]},\&\\{\ell:\mathsf{Msg}(w^{\gamma}.\ell)\multimap\mathsf{Cfg}_{w^{\gamma+1}:\mathtt{A}_{\ell},v^{\delta}:\mathtt{D}}(\mathsf{Q}_{\ell})\\}_{\ell\in
L}\vdash{[v^{\delta}:\mathtt{D}]}\\\ \hskip
256.0748pt\Downarrow\mbox{principal reduction}(\mu)\\\ \hline\cr\\\
{[\bar{z}^{\eta}:\omega]},\mathsf{Msg}(w^{\gamma}.k)\otimes\mathsf{Cfg}_{\bar{z}^{\eta}:\omega,w^{\gamma+1}:\mathtt{A}_{k}}(\mathsf{P})\vdash{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\oplus\\{\ell:(\mathsf{Msg}(w^{\gamma}.\ell)\otimes[w^{\gamma+1}:\mathtt{A}_{\ell}])\\}_{\ell\in
L}}\\\ \hskip
56.9055pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\oplus\\{\ell:(\mathsf{Msg}(w^{\gamma}.\ell)\otimes[w^{\gamma+1}:\mathtt{A}_{\ell}])\\}_{\ell\in
L}},\&\\{\ell:\mathsf{Msg}(w^{\gamma}.\ell)\multimap\mathsf{Cfg}_{w^{\gamma+1}:\mathtt{A}_{\ell},v^{\delta}:\mathtt{D}}(\mathsf{Q}_{\ell})\\}_{\ell\in
L}\vdash{[v^{\delta}:\mathtt{D}]}\\\ \hskip
256.0748pt\Downarrow\mbox{principal reduction}(\oplus)\\\ \hline\cr\\\
{[\bar{z}^{\eta}:\omega]},\mathsf{Msg}(w^{\gamma}.k)\otimes\mathsf{Cfg}_{\bar{z}^{\eta}:\omega,w^{\gamma+1}:\mathtt{A}_{k}}(\mathsf{P})\vdash(\mathsf{Msg}(w^{\gamma}.k)\otimes[w^{\gamma+1}:\mathtt{A}_{k}])\\\
\hskip
56.9055pt(\mathsf{Msg}(w^{\gamma}.k)\otimes[w^{\gamma+1}:\mathtt{A}_{k}]),{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\&\\{\ell:\mathsf{Msg}(w^{\gamma}.\ell)\multimap\mathsf{Cfg}_{w^{\gamma+1}:\mathtt{A}_{\ell},v^{\delta}:\mathtt{D}}(\mathsf{Q}_{\ell})\\}_{\ell\in
L}}\vdash{[v^{\delta}:\mathtt{D}]}\\\ \hskip
256.0748pt\Downarrow\mbox{External reduction}(\&)\\\ \hline\cr\\\
{[\bar{z}^{\eta}:\omega]},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{Msg}(w^{\gamma}.k)\otimes\mathsf{Cfg}_{\bar{z}^{\eta}:\omega,w^{\gamma+1}:\mathtt{A}_{k}}(\mathsf{P})}\vdash(\mathsf{Msg}(w^{\gamma}.k)\otimes[w^{\gamma+1}:\mathtt{A}_{k}])\\\
\hskip
56.9055pt(\mathsf{Msg}(w^{\gamma}.k)\otimes[w^{\gamma+1}:\mathtt{A}_{k}]),(\mathsf{Msg}(w^{\gamma}.k)\multimap\mathsf{Cfg}_{w^{\gamma+1}:\mathtt{A}k,v^{\delta}:\mathtt{D}}(\mathsf{Q}_{k})\vdash{[v^{\delta}:\mathtt{D}]}\\\
\hskip 256.0748pt\Downarrow\mbox{External reduction}(\otimes)\\\ \hline\cr\\\
{[\bar{z}^{\eta}:\omega]},\mathsf{Msg}(w^{\gamma}.k),\mathsf{Cfg}_{\bar{z}^{\eta}:\omega,w^{\gamma+1}:\mathtt{A}_{k}}(\mathsf{P})\vdash{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\mathsf{Msg}(w^{\gamma}.k)\otimes[w^{\gamma+1}:\mathtt{A}_{k}])}\\\
\hskip
56.9055pt{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\mathsf{Msg}(w^{\gamma}.k)\otimes[w^{\gamma+1}:\mathtt{A}_{k}])},(\mathsf{Msg}(w^{\gamma}.k)\multimap\mathsf{Cfg}_{w^{\gamma+1}:\mathtt{A}k,v^{\delta}:\mathtt{D}}(\mathsf{Q}_{k})\vdash{[v^{\delta}:\mathtt{D}]}\\\
\hskip 256.0748pt\Downarrow\mbox{Principal reduction}(\otimes)\\\ \hline\cr\\\
{\mathsf{Msg}(w^{\gamma}.k)\vdash\mathsf{Msg}(w^{\gamma}.k)}\quad{[\bar{z}^{\eta}:\omega]}\mathsf{Cfg}_{\bar{z}^{\eta}:\omega,w^{\gamma+1}:\mathtt{A}_{k}}(\mathsf{P})\vdash[w^{\gamma+1}:\mathtt{A}_{k}]\\\
\hskip
56.9055pt\mathsf{Msg}(w^{\gamma}.k),[w^{\gamma+1}:\mathtt{A}_{k}],{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\mathsf{Msg}(w^{\gamma}.k)\multimap\mathsf{Cfg}_{w^{\gamma+1}:\mathtt{A}k,v^{\delta}:\mathtt{D}}(\mathsf{Q}_{k})}\vdash{[v^{\delta}:\mathtt{D}]}\\\
\hskip 256.0748pt\Downarrow\mbox{External reduction}(\multimap)\\\
\hline\cr\\\
{\mathsf{Msg}(w^{\gamma}.k)\vdash\mathsf{Msg}(w^{\gamma}.k)}\quad{[\bar{z}^{\eta}:\omega]},\mathsf{Cfg}_{\bar{z}^{\eta}:\omega,w^{\gamma+1}:\mathtt{A}_{k}}(\mathsf{P})\vdash[w^{\gamma+1}:\mathtt{A}_{k}]\\\
\hskip
56.9055pt[w^{\gamma+1}:\mathtt{A}_{k}],\mathsf{Cfg}_{w^{\gamma+1}:\mathtt{A}k,v^{\delta}:\mathtt{D}}(\mathsf{Q}_{k})\vdash{[v^{\delta}:\mathtt{D}]}\quad{\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}{\mathsf{Msg}(w^{\gamma}.k)\vdash\mathsf{Msg}(w^{\gamma}.k)}}(\mbox{identity
elimination})\\\ \hskip 256.0748pt\Downarrow\mbox{External reduction}\times
2\\\ \hline\cr\\\
{{\mathsf{Msg}(w^{\gamma}.k)\vdash\mathsf{Msg}(w^{\gamma}.k)}}\quad{[\bar{z}^{\eta}:\omega]},T_{P}\vdash[w^{\gamma+1}:\mathtt{A}_{k}]\\\
\hskip
56.9055pt[w^{\gamma+1}:\mathtt{A}_{k}],T_{Q_{k}}\vdash{[v^{\delta}:\mathtt{D}]}\\\
\end{array}}$ Figure 14: A run of the cut elimination algorithm on
communicating processes.

By the definition of predicates $\mathsf{Cfg}$ and $[x^{\alpha}:\mathtt{A}]$,
and the observations we made in the proof of Lemma 1, these are the only steps
we need to consider for the cut elimination algorithm.

Consider the cut-free proof returned by our algorithm. By the property proved
above, it is enough to show that an external reduction will be applied on
$[x^{\alpha}:\omega]$ or $[y^{\beta}:\mathtt{B}]$. We use linearity and
validity of the cut-free output derivation. If there are no infinite branches
in the proof then by linearity of the calculus we know that a rule is applied
on $\overline{[\bar{x}^{\alpha}:\omega]}$ and $[y^{\beta}:\mathtt{B}]$. In the
infinite case, recall that the predicate $\mathsf{Cfg}$ for a recursive
process is defined coinductively; no subformula of it in the antecedents can
be a part of an infinite $\mu$-trace. Thus an external reduction (flip rule)
has to be applied on $[x^{\alpha}:\omega]$ or $[y^{\beta}:\mathtt{B}]$ to
produce a judgment of the derivation. This completes the proof as it shows
that the configuration will eventually communicate with one of its external
channels.

We can take one step further, and show that the configuration either
terminates or it will eventually communicate with one of its external channels
by _receiving a message_. Consider a branch in the cut-free valid proof as
described above. If the branch is finite it is straightforward to see that the
computation terminates. By a similar reasoning to the previous paragraph, in
an infinite branch either $[x^{\alpha}:\omega]$ has to be a part of an
(infinite) $\mu$-trace or $[y^{\beta}:\mathtt{B}]$ has to be a part of an
(infinite) $\nu$-trace. Without loss of generality assume that
$[x^{\alpha}:\omega]$ is a part of a $\mu$-trace. Since the traces are
infinite, there has to be an occurrence of a least fixed point type
$\mathtt{t}$ in a predicate $[x^{\gamma}:\mathtt{t}]$ on the branch. As a
result, there will be a process in the computation such that it communicates
along $x^{\gamma}$, and by the type of $x^{\gamma}$, we know that it will be
receiving a fixed point unfolding message.