{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[q@\\#\mathsf{l}]\;y]{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
S\\}]\equiv Q$, and $D\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$ and
$enc(Q)=C$.

(Case of [S$\mathbin{\binampersand}$]) Similar to
[S$\mathbin{\bindnasrepma}$].

See 8

###### Proof

The property trivially holds for $(P,\emptyset)$ for
$\mathsf{fn}(P)=\emptyset$ and $H=\emptyset$. We proceed by transition
induction, assuming that $S=(P,H)$ is ready, and
$\mathcal{S}\Mapsto\mathcal{S}^{\prime}=(P,H^{\prime})$, we check that
$S^{\prime}$ is ready.

(Case of [Sfwd]) Let
$R={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\ y$ and $S=(R,H^{\prime})\Mapsto S^{\prime}=(P,H^{\prime\prime})$, where
$H^{\prime}=H[z\\!\left<q_{1},Q\right>\\!x][y\\!\left<q_{2},P\right>\\!w]$ and
$H^{\prime\prime}=H[z\\!\left<q_{2}@q_{1},Q\right>\\!w]$. By i.h, $R$ is
$H^{\prime}$-ready and $H^{\prime}$ is ready. Thus $z:A$ is negative or void ,
$Q(z)$ is $H^{\prime}$-ready, and $P(w)$ is $H^{\prime},\\{w\\}$-ready. Then
$Q(z)$ is $H^{\prime\prime}$-ready, and $H^{\prime\prime}$ is ready. Then
$P(w)$ is $H^{\prime\prime}$-ready and $S^{\prime}$ is ready.

(Case of [SCut]) Let
$R={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}:T\;[q]\;y:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}$ and $S=(R,H)\Mapsto S^{\prime}=(P,H^{\prime})$, where
$H^{\prime}=H[x\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},Q\right>\\!y]$
and $T$ positive. By i.h., $R$ is $H$-ready hence $P(x)$ is $H,\\{x\\}$-ready
and $Q(y)$ is $H,\\{y\\}$-ready. Then $P(x)$ is $H^{\prime}$-ready, and
$H^{\prime}$ is ready. We conclude that $S^{\prime}$ is ready.

(Case of [S${\mathbf{1}}$]) Let
$R={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
x$ and $S=(R,H^{\prime})\Mapsto(Q,H^{\prime\prime})=S^{\prime}$ where
$H^{\prime}=H[x:A\\!\left<q,Q\right>\\!y]$ and
$H^{\prime\prime}=H[x:\emptyset\\!\left<q@{\checkmark},{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!y]$.
By the i.h, $H^{\prime}$ is ready and $Q(y)$ is $H^{\prime},\\{y\\}$-ready.
Hence $Q(y)$ is $H^{\prime\prime}$-ready, since $x:\emptyset$. Clearly,
$H^{\prime\prime}$ is ready, since
${{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}(x)$
is $H^{\prime\prime}$-ready. We conclude $S^{\prime}$ ready.

(Case of [S$\bot$]) Let
$R={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
y;U$,
$H^{\prime}=H[x\\!\left<{\checkmark},{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!y]$
and $S=(R,H^{\prime})\Mapsto(U,H)=S^{\prime}$. By the i.h, $R$ is
$H^{\prime}$-ready and $H^{\prime}$ is ready. Therefore $U$ is $H$-ready and
$H^{\prime}$-ready. We conclude $\mathcal{S}^{\prime}$ ready.

(Case of [S$-$]) Let $R=\mathcal{A}^{-}(x)$ and
$S=(R,H^{\prime})\Mapsto(Q,H^{\prime\prime})=S^{\prime}$ where
$H^{\prime}=H[x{:}A\\!\left<{q},Q\right>\\!y]$ and
$H^{\prime\prime}=H[x\\!\left<{q},\mathcal{A}^{-}(x)\right>\\!y]$ with $A-$.
By i.h., $\mathcal{A}^{-}(x)$ is $H^{\prime}$-ready and $H^{\prime}$ is ready.
Hence, $Q(y)$ is $H^{\prime},\\{y\\}$-ready. We have $\mathcal{A}^{-}(x)$ is
$H^{\prime\prime}$-ready ($x$ positive endpoint). Thus $H^{\prime\prime}$ is
ready, $Q$ is $H^{\prime\prime}$-ready (since $A$ is negative), and
$S^{\prime}$ is ready.

(Case of [S$\otimes$]) Let
$R={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
x(z.V);U$ and $S=(R,H^{\prime})\Mapsto(U,H^{\prime\prime})=S^{\prime}$ where
$H^{\prime}=H[x\\!\left<q,Q\right>\\!y]$ and
$H^{\prime\prime}=H[x\\!\left<q@{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,V),Q\right>\\!y]$.
By i.h, $H^{\prime}$ is ready and $R$ is $H^{\prime}$-ready. $V$ is
$H^{\prime},\\{z\\}$-ready and $U$ is $H^{\prime}$-ready. Then $V$ is
$H^{\prime\prime},\\{z\\}$-ready and $U$ is $H^{\prime\prime}$-ready. Also
$Q(y)$ is $H^{\prime},\\{y\\}$-ready, and $Q(y)$ is
$H^{\prime\prime},\\{y\\}$-ready. We conclude $H^{\prime\prime}$-ready and
thus $S^{\prime}$ ready.

(Case of [S$\mathbin{\bindnasrepma}$]) Let
$R={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
y(w:-);U$ and $S=(R,H^{\prime})\Mapsto(V,H^{\prime\prime})=S^{\prime}$ where
$H^{\prime}=H[x\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,V)@q,Q\right>\\!y]$
and
$H^{\prime\prime}=H[z\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},U\right>\\!w][x\\!\left<q\right>^{s}\\!y]$.
By i.h, $V$ is $H^{\prime}$-ready since $z$ is positive, and thus
$H^{\prime\prime}$-ready. By typing we have $Q(x)$ and thus $Q(x)$ is
$H^{\prime}$-ready. Also $R$ is $H^{\prime}$-ready, so $U$ is
$H^{\prime},\\{w\\}$-ready.

If
$q\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$
then
$H^{\prime\prime}=H[z\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},U\right>\\!w][x\\!\left<q,Q\right>\\!y]$.
Then $U$ is $H^{\prime\prime},\\{w\\}$-ready, $Q(x)$ is
$H^{\prime\prime}$-ready, $H^{\prime\prime}$ is ready, and $S^{\prime}$ is
ready.

If
$q={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$
then
$H^{\prime\prime}=H[z\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},U\right>\\!w][y\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},Q\right>\\!x]$.
Then $U$ is $H^{\prime\prime},\\{w\\}$-ready , $Q(x)$ is
$H^{\prime\prime},\\{x\\}$-ready ($x$ changed polarity), $H^{\prime\prime}$ is
ready, and $S^{\prime}$ is ready. The case $w-$ is handled in the same way.

(Case of [S$\oplus$]) Let $R=\\#\mathsf{l}\ x;U$ and
$S=(R,H^{\prime})\Mapsto(U,H^{\prime\prime})=S^{\prime}$ where
$H^{\prime}=H[x\\!\left<q,Q\right>\\!y]$ and
$H^{\prime\prime}=H[x\\!\left<q@\\#\mathsf{l},Q\right>\\!y]$. By i.h,
$H^{\prime}$ is ready and $R$ is $H^{\prime}$-ready. Therefore $U$ is
$H^{\prime\prime}$-ready. We conclude that $S^{\prime}$ is ready.

(Case of [S$\mathbin{\binampersand}$]) Let
$R={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{case}}\
y\ \\{|{\\#\mathsf{\ell}\in L}{:}P_{\ell}\\}$ and
$S=(R,H^{\prime})\Mapsto(P_{\\#\mathsf{l}},H^{\prime\prime})=S^{\prime}$ where
$H^{\prime}=H[x\\!\left<\\#\mathsf{l}@q,Q\right>\\!y]$ and
$H^{\prime\prime}=H[x\\!\left<q\right>^{s}\\!y]$. By i.h, $H^{\prime}$ is
ready, $R$ is $H^{\prime}$-ready, so $Q(x)$ is $H^{\prime}$-ready, and
$P_{\\#\mathsf{l}}$ is $H^{\prime}$-ready.

If
$q\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$
then $H^{\prime\prime}=H[x\\!\left<q,Q\right>\\!y]$ is ready and
$P_{\\#\mathsf{l}}$ is $H^{\prime\prime}$-ready since $Q(x)$ is
$H^{\prime}$-ready, so $S^{\prime}$ is ready.

If
$q={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$
then
$H^{\prime\prime}=H[y\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},Q\right>\\!x]$.
Notice that $Q$ is $H^{\prime\prime},\\{x\\}$-ready ($x$ changed polarity).
Then $H^{\prime\prime}$ is ready. $P_{\\#\mathsf{l}}$ is
$H^{\prime\prime}$-ready, so $S^{\prime}$ is ready.

See 5.3

###### Proof

Since $P$ is live then $enc(P)=S=({\mathcal{A}},H)$ for some action
$\mathcal{A}$.

(Case of [fwdB])
$\mathcal{A}={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\ y$. Wlog, assume that $x{:}A$ is negative, so $y{:}\overline{A}$ is
positive. By typing, $x$ and $y$ must be endpoints of different cuts (and
session records). Case
$H=H^{\prime}[z\\!\left<q_{1},U(z)\right>\\!x][y\\!\left<q_{2},V(w)\right>\\!w]$.
We have $S\Mapsto S^{\prime}$ by [Sfwd]. Case
$H=H^{\prime}[x\\!\left<q_{1},U(z)\right>\\!z][y\\!\left<q_{2},V(w)\right>\\!w]$.
Then
${\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\ y=\mathcal{A}^{-}(x)$, and $S\Mapsto S^{\prime}$ by [S$-$].

(Case of [${\mathbf{1}}$])
$\mathcal{A}={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
x$ so $S\Mapsto S^{\prime}$ by [S${\mathbf{1}}$].

(Case of [$\bot$])
$\mathcal{A}={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
y;R^{\prime}$. If $H=H^{\prime}[y{:}A\\!\left<q,Q\right>\\!x]$, then $S\Mapsto
S^{\prime}$ by [S$-$]. Otherwise, let
$H=H^{\prime}[x{:}A\\!\left<q,\mathcal{A}\right>\\!y]$. By Lemma 8,
$\mathcal{A}$ is $H^{\prime}$-ready, so $A$ is negative or void. By Lemma 3
$q\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$.
By Lemma 2, $q=\checkmark$. So $S\Mapsto S^{\prime}$ by [S$\bot$].

(Case of [$\otimes$])
$\mathcal{A}={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
x(z.R);Q{}$ so $S\Mapsto S^{\prime}$ by [S$\otimes$].

(Case of [$\mathbin{\bindnasrepma}$])
$\mathcal{A}={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
y(w);U$. If $H=H^{\prime}[y{:}A\\!\left<q,Q\right>\\!x]$, then $S\Mapsto
S^{\prime}$ by [S$-$]. Otherwise, $H=H^{\prime}[x:A\\!\left<q,Q\right>\\!y]$.
By Lemma 8, $\mathcal{A}$ is $H^{\prime}$-ready, so $A$ is negative or void.
By Lemma 3
$q\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$.
By Lemma 1 or Lemma 2, we must have
$q={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,R)@q^{\prime}$.
So $S\Mapsto S^{\prime}$ by [S$\mathbin{\bindnasrepma}$].

(Case of [$\oplus$]) By [S$\oplus$].

(Case of [$\mathbin{\binampersand}$])
$\mathcal{A}={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{case}}\
y\ \\{|{\\#\mathsf{\ell}\in L}{:}P_{\ell}\\}$. If
$H=H^{\prime}[y{:}A\\!\left<q,Q\right>\\!x]$, then $S\Mapsto S^{\prime}$ by
[S$-$]. Otherwise, $H=H^{\prime}[x{:}A\\!\left<q,Q\right>\\!y]$. By Lemma 8,
$\mathcal{A}$ is $H^{\prime}$-ready, so $A$ is negative or void. By Lemma 3
$q\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$.
By Lemma 1 or Lemma 2, we must have $q=\\#\mathsf{l}@q^{\prime}$ so $S\Mapsto
S^{\prime}$ by [S$\mathbin{\binampersand}$].

###  0.A.4 Proofs and Additional Definitions of Section 6: The SAM for full
$\mathsf{CLL}$

To alleviate the proofs we assume that only the unrestricted names are
recorded in environment, for the linear names we use names as heap locations,
and $\alpha$-conversion as needed to generate fresh names.

######  Definition 11 (Encode)

Given $P\vdash^{\mathsf{B}}\emptyset;\emptyset$ we define $enc(P)=C$ as
$enc(\emptyset,P,\emptyset)\stackrel{{\scriptstyle\mathsf{cut}*}}{{\Mapsto}}C$
where $enc(\mathcal{E},P,H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$
is defined by the rules

$\begin{array}[]{clll}\displaystyle\frac{enc(P(x),H[x{:}A\\!\left<q,Q\right>\\!y{:}B])\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C}{enc({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}{:}A[q]\;y{:}B]{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\},H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C}&\mbox{\rm($A+$
)}\vspace{6pt}\\\
\displaystyle\frac{enc(Q(y),H[x{:}A\\!\left<q,P\right>\\!y{:}B])\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C}{enc({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}{:}A\;[q]\;y{:}B]{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\},H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C}&\mbox{\rm($A-$ or
$P={{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}$
)}\vspace{6pt}\\\
\displaystyle\frac{enc(\mathcal{E}\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(y,\mathcal{E},R)/x\\},P),H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C}{enc(\mathcal{E},{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.R\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
P\\},H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C}&\vspace{6pt}\\\
enc(\mathcal{A},H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}(\mathcal{A},H)&\mbox{\rm($A\in\mathcal{A}$)}\end{array}$

######  Lemma 16 (Soundness-!)

Let $P\vdash^{\mathsf{B}}\emptyset;\emptyset$.

1\. If $enc(P)\Mapsto D\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$
then there is $Q$ such that $P\to\cup\equiv Q$ and $C=enc(Q)$.

2\. Let $P(H)$ denote property: If $x{:}A\\!\left<q,P\right>\\!y{:}B\in H$
then $B-$ and if ($x\in\mathsf{fn}(P)$ or
$P={{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}$)
then $A-$ else $A+$.

Then if $enc(P)=(\mathcal{E},\mathcal{A},H)\Mapsto(\mathcal{E},Q,H^{\prime})$
and $P(H)$ then $P(H^{\prime})$.

###### Proof

(1) Let $enc(P)\Mapsto D\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$.
Let $enc(P)=(\mathcal{A},H)$ for some action $\mathcal{A}$. Then $P\equiv
E[\mathcal{A}]$ for some cut context $E[-]$. We consider each reduction
$\Mapsto$.

(Case of [S$!$]) Let
$enc(P)=(\mathcal{E},{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{!}}x(z);U,H[x\\!\left<q,R\right>\\!y])\Mapsto
D$ where
$D=(R,H[x\\!\left<q@{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,\mathcal{E},U),{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!y])\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$.

Therefore, $P\equiv
E[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{!}}x(z);U]
\equiv
E^{\prime}[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{!}}x(z);U\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[q]\;y]{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\}]$ and $P\to
Q=E^{\prime}[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}\;[q@{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,\mathcal{E},U)]\;y]{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
R\\}]$ and $enc(Q)=C$.

(Case of [S$?$]) Let
$enc(P)=(\mathcal{E},{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{?}}y;R,{H}[x\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,\mathcal{E},U),{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!y])\Mapsto
D$ and
$D=(\mathcal{E}^{\prime}\\{y/{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,\mathcal{E},U)\\},R,{H})\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$.

Hence, $P\equiv
E[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{?}}y;R]
\equiv
E^{\prime}[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}:\emptyset\;[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,\mathcal{E},U)]\;y]{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{?}}y;R\\}]\to
Q=E^{\prime}[R]$ and $D\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$ and
$enc(Q)=C$.

(Case of [Scall]) Let
$enc(P)=(\mathcal{E},{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{call}}\
y(w{:}-);U,H)\Mapsto D$ where
$D=(R,H[z\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},U\right>\\!w])\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C$.
Let
$\mathcal{E}(y)={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,\mathcal{E},R)$.

So, $P\equiv
E[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{call}}\
y(w{:}-);U]\equiv
E^{\prime}[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{z.R\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!y{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{call}}\
y(w{:}-);U\\}]\to Q$.

Then
$Q=E^{\prime}[{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut}}\;\\{R\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}z[{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}]
w{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
{U}\\}\\}]$ and $enc(Q)=C$.

######  Lemma 17 (Readiness-!)

Let $P\vdash\emptyset;\emptyset$ and
$(\emptyset,P,\emptyset)\stackrel{{\scriptstyle*}}{{\Mapsto}}S$. Then
$\mathcal{S}$ is ready.

###### Proof

The property trivially holds for $(\emptyset,P,\emptyset)$ for
$\mathsf{fn}(P)=\emptyset$ and $H=\emptyset$. We proceed by transition
induction, assuming that $S=(\mathcal{E},P,H)$ is ready, and
$\mathcal{S}\Mapsto\mathcal{S}^{\prime}=(\mathcal{E}^{\prime},P,H^{\prime})$,
we check that $S^{\prime}$ is ready.

(Case of [SCut!]) Let
$R={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{cut!}}\;\\{y.R\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}!x{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}$ and $S=(\mathcal{E},Q,H)\Mapsto S^{\prime}=(\mathcal{E}^{\prime}P,H)$,
where
$E^{\prime}=\mathcal{E}\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(y,\mathcal{E},R)/x\\}$.
By i.h., $P$ is $H$-ready but then $Q$ is $H$ since $x$ is unrestricted. We
conclude that $S^{\prime}$ is ready. $R$ is also $H,\\{y\\}$-ready, since by
typing the only free linear name in $R$ is $y$.

(Case of [S$!$]) Let
$R={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{!}}x(z);U$
and
$S=(\mathcal{E},R,H^{\prime})\Mapsto(\mathcal{G},Q,H^{\prime\prime})=S^{\prime}$
where $H^{\prime}=H[x:!A\\!\left<q,\mathcal{G},Q\right>\\!y]$ and
$H^{\prime\prime}=H[x:\emptyset\\!\left<q@{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,\mathcal{E},U),\emptyset,{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!y]$.

By the i.h, $H^{\prime}$ is ready and $U(z)$ is $H^{\prime},\\{z\\}$-ready.

Hence $Q(y)$ is $H^{\prime\prime}$-ready, since $x:\emptyset$.

Clearly, $H^{\prime\prime}$ is ready, since
${{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}(x)$
is $H^{\prime\prime}$-ready. We conclude $S^{\prime}$ ready.

(Case of [S$?$]) Let
$R={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{?}}y;Q$,
$H^{\prime}=H[x\\!\left<{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,\mathcal{E},U)},\emptyset,{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\right>\\!y]$
and
$S=(\mathcal{E},R,H^{\prime})\Mapsto(\mathcal{E}\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,\mathcal{E},U)/y\\},Q,H)=S^{\prime}$.
By the i.h, $R$ is $H^{\prime}$-ready and $H^{\prime}$ is ready. Therefore $Q$
is $H$-ready and $H^{\prime}$-ready. Also $U$ is $H^{\prime},\\{z\\}$-ready
(no linear names). We conclude $S^{\prime}$ ready.

(Case of [Scall]) Let
$R={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{call}}\
y(w:-);U$ and
$S=(\mathcal{E},R,H)\Mapsto(\mathcal{F},V,H^{\prime})=S^{\prime}$ where
$\mathcal{E}(y)={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,\mathcal{F},V)$
and
$H^{\prime}=H[z\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},\mathcal{E},U\right>\\!w]$.

By i.h, $U$ is $H,\\{w\\}$-ready and $V$ is $H$-ready since $z$ is positive.
Hence $U$ is $H^{\prime},\\{w\\}$-ready, so $H^{\prime}$ is ready, and $V$ is
$H^{\prime}$-ready. $U$ is $H^{\prime},\\{w\\}$-ready. We conclude
$S^{\prime}$ ready.

######  Theorem 0.A.1 (Progress-!)

Let $P\vdash\emptyset;\emptyset$ and $P$ live. Then $enc(P)=S\Mapsto
S^{\prime}$.

###### Proof

Since $P$ is live then $enc(P)=S=(\mathcal{E},{\mathcal{A}},H)$ for some
action $\mathcal{A}$. The interesting case is:

(Case of [$?$])
$\mathcal{A}={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{?}}y;U$.
If $H=H^{\prime}[y{:}A\\!\left<q,\mathcal{F},Q\right>\\!x]$, then $S\Mapsto
S^{\prime}$ by [S$-$]. Otherwise, $H=H^{\prime}[x:A\\!\left<q,Q\right>\\!y]$.
By Lemma 17, $\mathcal{A}$ is $H^{\prime}$-ready, so $A$ is negative or void.
By Lemma 3
$q\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$.
By Lemma 2, we must have
$q={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos!}}(z,\mathcal{G},R)$.
So $S\Mapsto S^{\prime}$ by [S$?$].

###  0.A.5 Proofs of Section 6.1: Concurrent Semantics of Cut and Mix

Here we sketch the basic structure of progress for the SAM with concurrent cut
and sequential threads. First we define the encoding of $\mathsf{CLLB}$
processes with annotated concurrent cuts (such annotation is silent for any
purpose other than the concurrent execution strategy in the SAM). For
simplicity we address core SAM (no exponentials) and concurrent cuts. The
proof can be easily extended to any other pair of dual types types, and
already allow the concurrent non-deterministic sychronisation of different
threads.

$\begin{array}[]{clll}\displaystyle\frac{enc(P,H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}(A,H^{\prime})\quad
enc^{c}(T,H^{\prime})\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}(T^{\prime},H^{\prime\prime})}{enc^{c}(\\{P\\}\uplus
T,H^{\prime})\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}(\\{A\\}\uplus
T^{\prime},H^{\prime\prime})}&\rm{[thr]\vspace{6pt}}\\\
\displaystyle\frac{enc^{c}(T,H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C}{enc^{c}(\\{{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\\}\uplus
T,H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C}&\rm{[{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}]\vspace{6pt}}\\\
\displaystyle\frac{enc^{c}(\\{P,Q\\}\uplus
T,H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C}{enc^{c}({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{par}}\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
Q\\} \uplus
T,H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C}&\rm{[mix]\vspace{6pt}}\\\
\displaystyle\frac{enc^{c}(\\{P,Q\\}\uplus
T,H[x\left<q\right>y])\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C}{enc^{c}({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{pcut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x:A^{+}[q]y:B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\uplus
T,H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}C}&\rm{[pcut]}\end{array}$
Figure 12: Encoding of annotated $\mathsf{CLLB}$ of into concurrent SAM
$\begin{array}[]{ll}({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{close}}\
x,H[x\left<q\right>y])\Mapsto({{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}},H[x\left<q@{\checkmark}\right>y])&\text{\rm[S${\mathbf{1}}$c]}\vspace{6pt}\\\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{wait}}\
y;P,H[x\\!\left<{\checkmark},y\right>\\!])\Mapsto(P,H)&\text{\rm[S$\bot$c]}\vspace{6pt}\\\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{send}}\
x(z.R);Q,H[x\left<q\right>y])\Mapsto(Q,H[x\left<q@{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,R)\right>y])&\text{\rm[S$\otimes$c]}\vspace{6pt}\\\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{recv}}\
y(w{:}-);Q,H[x\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{clos}}(z,R)@q\right>y{}])\Mapsto(R,H[z\\!\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}},Q\right>\\!w][x\\!\left<q\right>^{s}\\!y])&\text{\rm[S$\mathbin{\bindnasrepma}-$c]}\vspace{6pt}\\\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{fwd}}\
x\
y,H[z\left<q_{1}\right>x[y\left<q_{2}\right>w]])\Mapsto({{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}},H[z\left<q_{2}@q_{1}\right>w])&\text{\rm[SfwdPc]}\\\
\\\ a\\!\left<q\right>^{s}\\!b\triangleq\mbox{if
}(q={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}})\mbox{
then }b\left<q\right>{a}\mbox{ else }a\left<q\right>{b}\end{array}$ Figure 13:
Transition rules for concurrent actions (sample)
$\begin{array}[]{c}\displaystyle\frac{(P,H)\Mapsto(P^{\prime},H^{\prime})}{(P\uplus
T,H)\Mapsto(P^{\prime}\uplus
T,H^{\prime})}\;\text{\rm[Srun]}\quad\displaystyle\frac{(T,H)\Mapsto(T^{\prime},H^{\prime})}{({{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}\uplus
T,H)\Mapsto(T^{\prime},H^{\prime})}\quad\text{\rm[S${{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}$p]}\vspace{6pt}\\\
({\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{pcut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}x:A^{+}{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\uplus T,H)\Mapsto(\\{P,Q\\{y/x\\}\\}\uplus
T\\},H[x\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}\right>y])\quad\text{\rm[SCutp]}\vspace{6pt}\\\
((P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{||}}\
Q)\uplus T,H)\Mapsto(\\{P,Q\\}\uplus
T\\},H[x\left<{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}\right>y])\quad\text{\rm[SMixp]}\end{array}$
Figure 14: Transition rules for concurrent actions

We show that SAM execution on well-typed processes simulates $\mathsf{CLLB}$
reduction. See 6.3

###### Proof

Induction of $enc(P)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}B$.

To prove progress along the lines of Theorem 4.2 we introduce a simplified
notion of observation (cf. Fig. 9) for our scenario of concurrent actions on
heap allocated concurrent sessions, as follows.

$P\downarrow_{x}^{H}$ iff $P\downarrow_{x}$ and ($x\left<q\right>y\in H$ or
$x\left<q\right>y\in H$).

######  Lemma 18 (Liveness-c)

Let $P\vdash\Delta$ and
$enc^{c}(P,H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}(T,H^{\prime})$.
For every non-empty $S\subseteq T$ there is $P_{i}\in S$ such that (a)
$(P_{i},H^{\prime})\Mapsto C$ or (b) $P_{i}\downarrow_{y}^{H^{\prime}}$.

###### Proof

By induction on the derivation of
$enc(P,H)\stackrel{{\scriptstyle\mathsf{cut*}}}{{\Mapsto}}(T,H)$.

(Case of [thr]) By Theorem 5.3 (Progress), we have
$(P,H)\Mapsto(A,H^{\prime})$ for any action on a sequential cut. Otherwise $P$
is an action in a concurrent cut, and we have (b). By i.h., the property holds
for $T^{\prime},H^{\prime\prime}$. Hence it holds for $(\\{A\\}\uplus
T^{\prime},H^{\prime\prime})$.

(Case of [mix]) Let $enc^{c}(\\{P,Q\\}\uplus
T,H[x\left<q\right>y])\Mapsto(T^{\prime},H^{\prime})$

By i.h. (a) holds for $T^{\prime},H^{\prime}$ and we conclude.

(Case of [cutp]) Let
$R={\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{pcut}}\;\\{P\
{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\overline{x}{:}A\;[q]\;y{:}B{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{|}}\
Q\\}\uplus T$ and $enc(R,H)\Mapsto(T^{\prime},H^{\prime})$. Let
$U_{Q}=T\downarrow\mathsf{fn}(Q)$. By i.h., there is $Q_{i}\in U_{P}$ such
that (a) $(Q_{i},H^{\prime})\Mapsto$ or (b)
$Q_{i}\downarrow_{z}^{H^{\prime}}$. In case (a) we conclude (a). Otherwise
assume (b). If $z\neq y$ then (a) holds for $T^{\prime},H^{\prime}$. If $z=y$
then (by typing) $B$ is negative and $Q_{i}={\mathcal{A}}^{B}(y)$ is a
negative action on $y$ of type $B$ and $w\left<q\right>y\in H$.

If
$q\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$
then we have $(Q_{i},H)\Mapsto$ by [S$B$c] (we denote by [S$B$c] the negative
reduction rule associated to the negative type $B$).

Otherwise
$q={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$
and $A=\overline{B}$ so
$P\neq{{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}}$.

Let $U_{P}=T\downarrow\mathsf{fn}(P)$. By i.h., there is $P_{i}\in U_{P}$ such
that $(P_{i},H)\Mapsto$ or (b) and $P_{j}\downarrow_{u}^{H^{\prime}}$. In case
(a) we conclude. Otherwise assume (b). If $u\neq x$ then (a) holds for
$T^{\prime},H^{\prime}$. So $u=x=w$. Now, if $A$ is negative or void, then by
Lemma 3
$q\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathsf{nil}}$,
contradiction. So $A$ is positive and $P_{j}={\mathcal{A}}^{A}(x)$ is a
positive action on $x$ of type $A$. So we have
$(P_{j},H^{\prime}[x\left<q\right>y])\Mapsto({{\color[rgb]{0.61328125,0.3515625,0.41796875}\definecolor[named]{pgfstrokecolor}{rgb}{0.61328125,0.3515625,0.41796875}\mathsf{0}}},H^{\prime}[x\left<q@c\right>y])$
by [S$A$c] and $(Q_{i},H^{\prime}[x\\!\left<q\right>^{s}\\!y])\Mapsto C$ by
[S$B$c].