L},{\uparrow_{L}^{S}}C_{\scriptscriptstyle L},\top)$ $\displaystyle\in
F(\text{ssync}^{\prime})$ (by $D{\uparrow_{L}^{S}}$)

######  Subcase 2.

$B={\uparrow_{L}^{S}}B_{\scriptscriptstyle L}$ and
$C={\uparrow_{L}^{L}}C_{\scriptscriptstyle L}$ with $A_{\scriptscriptstyle
L}\leq B_{\scriptscriptstyle L}\leq C_{\scriptscriptstyle L}$.

$\displaystyle({\uparrow_{L}^{S}}A_{\scriptscriptstyle
L},{\uparrow_{L}^{L}}C_{\scriptscriptstyle L},\top)$
$\displaystyle\in\text{ssync}_{\Uparrow},({\uparrow_{L}^{S}}A_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}B_{\scriptscriptstyle L},\top)\in\text{ssync}$ (this
case) $\displaystyle(A_{\scriptscriptstyle L},B_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}A_{\scriptscriptstyle L})$ $\displaystyle\in\text{ssync}$
(by inversion on $D{\uparrow_{L}^{S}}$) $\displaystyle(A_{\scriptscriptstyle
L},C_{\scriptscriptstyle L},{\uparrow_{L}^{S}}A_{\scriptscriptstyle L})$
$\displaystyle\in\text{ssync}_{\Uparrow}$ (by definition of
$\text{ssync}_{\Uparrow}$ with $A_{\scriptscriptstyle L}\leq
B_{\scriptscriptstyle L}$) $\displaystyle(A_{\scriptscriptstyle
L},C_{\scriptscriptstyle L},{\uparrow_{L}^{S}}A_{\scriptscriptstyle L})$
$\displaystyle\in\text{ssync}^{\prime}$ (since
$\text{ssync}_{\Uparrow}\subseteq\text{ssync}^{\prime}$)
$\displaystyle({\uparrow_{L}^{S}}A_{\scriptscriptstyle
L},{\uparrow_{L}^{L}}C_{\scriptscriptstyle L},\top)$ $\displaystyle\in
F(\text{ssync}^{\prime})$ (by $D{\uparrow_{L}^{S}}$)

######  Subcase 3.

$B={\uparrow_{L}^{L}}B_{\scriptscriptstyle L}$ and
$C={\uparrow_{L}^{L}}C_{\scriptscriptstyle L}$ with $A_{\scriptscriptstyle
L}\leq B_{\scriptscriptstyle L}\leq C_{\scriptscriptstyle L}$.

$\displaystyle({\uparrow_{L}^{S}}A_{\scriptscriptstyle
L},{\uparrow_{L}^{L}}C_{\scriptscriptstyle L},\top)$
$\displaystyle\in\text{ssync}_{\Uparrow},({\uparrow_{L}^{S}}A_{\scriptscriptstyle
L},{\uparrow_{L}^{L}}B_{\scriptscriptstyle L},\top)\in\text{ssync}$ (this
case) $\displaystyle(A_{\scriptscriptstyle L},B_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}A_{\scriptscriptstyle L})$ $\displaystyle\in\text{ssync}$
(by inversion on $D{\uparrow_{L}^{S}}{\uparrow_{L}^{L}}$)
$\displaystyle(A_{\scriptscriptstyle L},C_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}A_{\scriptscriptstyle L})$
$\displaystyle\in\text{ssync}_{\Uparrow}$ (by definition of
$\text{ssync}_{\Uparrow}$ with $A_{\scriptscriptstyle L}\leq
B_{\scriptscriptstyle L}$) $\displaystyle(A_{\scriptscriptstyle
L},C_{\scriptscriptstyle L},{\uparrow_{L}^{S}}A_{\scriptscriptstyle L})$
$\displaystyle\in\text{ssync}^{\prime}$ (since
$\text{ssync}_{\Uparrow}\subseteq\text{ssync}^{\prime}$)
$\displaystyle({\uparrow_{L}^{S}}A_{\scriptscriptstyle
L},{\uparrow_{L}^{L}}C_{\scriptscriptstyle L},\top)$ $\displaystyle\in
F(\text{ssync}^{\prime})$ (by $D{\uparrow_{L}^{S}}$)

We missed one case, when $A=B=C=1$, but this case is trivial since
$\text{ssync}_{\Uparrow}$ does not add any new members to the set.

######  Lemma 27.

If $A\leq B\leq C$ with all same modalities,
$\vdash(B,C,\hat{D})\;\text{ssync}$, and
$\vdash(A,C,\hat{E})\;\text{ssync}$, then $\vdash(A,C,\hat{D})\;\text{ssync}$
for some $\hat{D}$ and $\hat{E}$.

######  Proof B.9.

We want to show that

$\text{ssync}^{\prime}\;::=\;\text{ssync}\cup\text{ssync}_{\Downarrow}$

is $F$-consistent with

$\displaystyle\text{ssync}_{\Downarrow}$
$\displaystyle\;::=\;\\{(A,C,\hat{D})\;|\;\exists B.A\leq
B\land(B,C,\hat{D})\in\text{ssync}\land\exists\hat{E}.(A,C,\hat{E})\in\text{ssync}\\}$

The proof is very similar in style to the previous lemma, but there is one
additional constraint that $(A,C,\hat{E})\in\text{ssync}$ for any constraint
$\hat{E}$. This assumption is only necessary for the ${\uparrow_{L}^{S}}$
case.
In any case, we will prove $F$-consistency of $\text{ssync}^{\prime}$, that
is, $\text{ssync}^{\prime}\in F(\text{ssync}^{\prime})$ by showing that each
of the three sets ssync and $\text{ssync}_{\Downarrow}$ are subsets of
$F(\text{ssync}^{\prime})$.
First, $\text{ssync}\subseteq F(\text{ssync}^{\prime})$ immediately follows
from the same argument as in the previous proof.

We will now consider $\text{ssync}_{\Downarrow}\in F(\text{ssync}^{\prime})$
by case analysis on the structure of $B$. Because all of $A,B,C$ have the same
modality, we can uniquely infer the structure of $A$ and $C$ from the
structure of $B$ by inversion on the appropriate subtyping rule.

######  Case 1.

$A={\uparrow_{L}^{L}}A^{\prime}_{\scriptscriptstyle L}$; then
$B={\uparrow_{L}^{L}}B^{\prime}_{\scriptscriptstyle L}$ and
$C={\uparrow_{L}^{L}}C^{\prime}_{\scriptscriptstyle L}$ with
$A^{\prime}_{\scriptscriptstyle L}\leq B^{\prime}_{\scriptscriptstyle L}\leq
C^{\prime}_{\scriptscriptstyle L}$.

$\displaystyle({\uparrow_{L}^{L}}A^{\prime}_{\scriptscriptstyle
L},{\uparrow_{L}^{L}}C^{\prime}_{\scriptscriptstyle L},\hat{D})$
$\displaystyle\in\text{ssync}_{\Downarrow},({\uparrow_{L}^{L}}B^{\prime}_{\scriptscriptstyle
L},{\uparrow_{L}^{L}}C^{\prime}_{\scriptscriptstyle
L},\hat{D})\in\text{ssync}$ (this case)
$\displaystyle(B^{\prime}_{\scriptscriptstyle
L},C^{\prime}_{\scriptscriptstyle L},\hat{D})$ $\displaystyle\in\text{ssync}$
(by inversion on $D{\uparrow_{L}^{L}}$)
$\displaystyle(A^{\prime}_{\scriptscriptstyle
L},C^{\prime}_{\scriptscriptstyle L},\hat{D})$
$\displaystyle\in\text{ssync}_{\Downarrow}$ (by definition of
$\text{ssync}_{\Downarrow}$ with $A^{\prime}_{\scriptscriptstyle L}\leq
B^{\prime}_{\scriptscriptstyle L}$)
$\displaystyle(A^{\prime}_{\scriptscriptstyle
L},C^{\prime}_{\scriptscriptstyle L},\hat{D})$
$\displaystyle\in\text{ssync}^{\prime}$ (since
$\text{ssync}_{\Downarrow}\subseteq\text{ssync}^{\prime}$)
$\displaystyle({\uparrow_{L}^{L}}A^{\prime}_{\scriptscriptstyle
L},{\uparrow_{L}^{L}}C^{\prime}_{\scriptscriptstyle L},\hat{D})$
$\displaystyle\in F(\text{ssync}^{\prime})$ (by $D{\uparrow_{L}^{L}}$)

${\downarrow_{L}^{L}},\otimes,$ and $\multimap$ follow a similar pattern of
appealing to the covariance of subtyping on the continuation types.

######  Case 2.

$A=\oplus\\{{\overline{l{:}A_{\scriptscriptstyle L}}}\\}$; then
$B=\oplus\\{{\overline{l{:}B_{\scriptscriptstyle
L}},\overline{m{:}B_{\scriptscriptstyle L}}}\\}$ and
$C=\oplus\\{{\overline{l{:}C_{\scriptscriptstyle
L}},\overline{m{:}C_{\scriptscriptstyle
L}},\overline{n{:}C_{\scriptscriptstyle L}}}\\}$ with
${A_{i}}_{\scriptscriptstyle L}\leq{B_{i}}_{\scriptscriptstyle
L}\leq{C_{i}}_{\scriptscriptstyle L}\;\forall i\in\overline{l}$ and
${B_{i}}_{\scriptscriptstyle L}\leq{C_{i}}_{\scriptscriptstyle L}\;\forall
i\in\overline{m}$.

$\displaystyle(\oplus\\{{\overline{l{:}A_{\scriptscriptstyle
L}}}\\},\oplus\\{{\overline{l{:}C_{\scriptscriptstyle
L}},\overline{m{:}C_{\scriptscriptstyle
L}},\overline{n{:}C_{\scriptscriptstyle L}}}\\},\hat{D})$
$\displaystyle\in\text{ssync}_{\Downarrow}$
$\displaystyle(\oplus\\{{\overline{l{:}B_{\scriptscriptstyle
L}},\overline{m{:}B_{\scriptscriptstyle
L}}}\\},\oplus\\{{\overline{l{:}C_{\scriptscriptstyle
L}},\overline{m{:}C_{\scriptscriptstyle
L}},\overline{n{:}C_{\scriptscriptstyle L}}}\\},\hat{D})$
$\displaystyle\in\text{ssync}$ (this case) $\displaystyle(\forall
i\in\overline{l},\overline{m})\;({B_{i}}_{\scriptscriptstyle
L},{C_{i}}_{\scriptscriptstyle L},\hat{D})$ $\displaystyle\in\text{ssync}$ (by
inversion on $D{\oplus}$) $\displaystyle(\forall
i\in\overline{l})\;({A_{i}}_{\scriptscriptstyle L},{C_{i}}_{\scriptscriptstyle
L},\hat{D})$ $\displaystyle\in\text{ssync}_{\Downarrow}$
$\displaystyle(\forall i\in\overline{l})\;({A_{i}}_{\scriptscriptstyle
L},{C_{i}}_{\scriptscriptstyle L},\hat{D})$
$\displaystyle\in\text{ssync}^{\prime}$ (since
$\text{ssync}_{\Downarrow}\subseteq\text{ssync}^{\prime}$)
$\displaystyle(\oplus\\{{\overline{l{:}A_{\scriptscriptstyle
L}}}\\},\oplus\\{{\overline{l{:}C_{\scriptscriptstyle
L}},\overline{m{:}C_{\scriptscriptstyle
L}},\overline{n{:}C_{\scriptscriptstyle L}}}\\},\hat{D})$ $\displaystyle\in
F(\text{ssync}^{\prime})$ (by $D{\oplus}$)

$D{\&}$ follows a similar pattern.

######  Case 3.

$A={\downarrow_{L}^{S}}A_{\scriptscriptstyle S}$; similar to the proof of
Lemma 11, there are three possible assignments for $B$ and $C$. We will
present one of those subcases: let
$B={\downarrow_{L}^{S}}B_{\scriptscriptstyle S}$ and
$C={\downarrow_{L}^{S}}C_{\scriptscriptstyle S}$ with $A_{\scriptscriptstyle
S}\leq B_{\scriptscriptstyle S}\leq C_{\scriptscriptstyle S}$. The other two
cases are similar.

$\displaystyle({\downarrow_{L}^{S}}A_{\scriptscriptstyle
S},{\downarrow_{L}^{S}}C_{\scriptscriptstyle S},\hat{D})$
$\displaystyle\in\text{ssync}_{\Downarrow},({\downarrow_{L}^{S}}B_{\scriptscriptstyle
S},{\downarrow_{L}^{S}}C_{\scriptscriptstyle S},\hat{D})\in\text{ssync}$ (this
case) $\displaystyle(B_{\scriptscriptstyle S},C_{\scriptscriptstyle S},\top)$
$\displaystyle\in\text{ssync},B_{\scriptscriptstyle S}\leq\hat{D}$ (by
inversion on $D{\downarrow_{L}^{S}}$) $\displaystyle(A_{\scriptscriptstyle
S},C_{\scriptscriptstyle S},\top)$ $\displaystyle\in\text{ssync}_{\Downarrow}$
(by definition of $\text{ssync}_{\Downarrow}$ with $A_{\scriptscriptstyle
S}\leq B_{\scriptscriptstyle S}$) $\displaystyle(A_{\scriptscriptstyle
S},C_{\scriptscriptstyle S},\top)$ $\displaystyle\in\text{ssync}^{\prime}$
(since $\text{ssync}_{\Downarrow}\subseteq\text{ssync}^{\prime}$)
$\displaystyle A_{\scriptscriptstyle S}\leq\hat{D}$ (because
$A_{\scriptscriptstyle S}\leq B_{\scriptscriptstyle S}\leq\hat{D}$)
$\displaystyle({\downarrow_{L}^{S}}A_{\scriptscriptstyle
S},{\downarrow_{L}^{S}}C_{\scriptscriptstyle S},\hat{D})$ $\displaystyle\in
F{\text{ssync}^{\prime}}$ (by $D{\downarrow_{L}^{S}}$)

######  Case 4.

$A={\uparrow_{L}^{S}}A_{\scriptscriptstyle L}$; again, there are three
possible assignments for $B$ and $C$, and we will take the subcase when
$B={\uparrow_{L}^{S}}B_{\scriptscriptstyle L}$ and
$C={\uparrow_{L}^{S}}C_{\scriptscriptstyle L}$ with $A_{\scriptscriptstyle
L}\leq B_{\scriptscriptstyle L}\leq C_{\scriptscriptstyle L}$. The other two
cases are similar. This case finally uses our assumption that
$(A,C,\hat{E})\in\text{ssync}$ – $\hat{E}$ must be $\top$ due to
$A={\uparrow_{L}^{S}}A_{\scriptscriptstyle L}$.

$\displaystyle({\uparrow_{L}^{S}}A_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}C_{\scriptscriptstyle L},\top)$
$\displaystyle\in\text{ssync}_{\Downarrow},({\uparrow_{L}^{S}}B_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}C_{\scriptscriptstyle L},\top)\in\text{ssync}$ (this
case) $\displaystyle({\uparrow_{L}^{S}}A_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}C_{\scriptscriptstyle L},\top)$
$\displaystyle\in\text{ssync}$ (By assumption with $\hat{E}=\top$)
$\displaystyle(A_{\scriptscriptstyle L},C_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}A_{\scriptscriptstyle L})$ $\displaystyle\in\text{ssync}$
(by inversion on $D{\uparrow_{L}^{S}}$) $\displaystyle(A_{\scriptscriptstyle
L},C_{\scriptscriptstyle L},{\uparrow_{L}^{S}}A_{\scriptscriptstyle L})$
$\displaystyle\in\text{ssync}^{\prime}$ (since
$\text{ssync}\subseteq\text{ssync}^{\prime}$)
$\displaystyle({\uparrow_{L}^{S}}A_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}C_{\scriptscriptstyle L},\top)$ $\displaystyle\in
F(\text{ssync}^{\prime})$ (by $D{\uparrow_{L}^{S}}$)

We missed one case, when $A=B=C=1$, but this case is trivial since
$\text{ssync}_{\Downarrow}$ does not add any new members to the set.

######  Lemma 28.

If $\vdash(A_{\scriptscriptstyle L},B_{\scriptscriptstyle
L},\hat{C})\;\text{ssync}$ and $\hat{D}\leq\hat{C}$, then
$\vdash(A_{\scriptscriptstyle L},B_{\scriptscriptstyle
L},\hat{D})\;\text{ssync}$ for some $A_{\scriptscriptstyle
L},B_{\scriptscriptstyle L},\hat{C},$ and $\hat{D}$.

######  Proof B.10.

We want to show that

$\text{ssync}^{\prime}\;::=\;\text{ssync}\cup\text{ssync}_{\Downarrow}$

is $F$-consistent with

$\displaystyle\text{ssync}_{\Downarrow}$
$\displaystyle\;::=\;\\{(A,C,\hat{D})\;|\;\exists B.A\leq
B\land(B,C,\hat{D})\in\text{ssync}\land\exists\hat{E}.(A,C,\hat{E})\in\text{ssync}\\}$

The proof is very similar in style to the previous lemma, but there is one
additional constraint that $(A,C,\hat{E})\in\text{ssync}$ for any constraint
$\hat{E}$. This assumption is only necessary for the ${\uparrow_{L}^{S}}$
case.
In any case, we will prove $F$-consistency of $\text{ssync}^{\prime}$, that
is, $\text{ssync}^{\prime}\in F(\text{ssync}^{\prime})$ by showing that each
of the three sets ssync and $\text{ssync}_{\Downarrow}$ are subsets of
$F(\text{ssync}^{\prime})$.
First, $\text{ssync}\subseteq F(\text{ssync}^{\prime})$ immediately follows
from the same argument as in the previous proof.

We will now consider $\text{ssync}_{\Downarrow}\in F(\text{ssync}^{\prime})$
by case analysis on the structure of $B$. Because all of $A,B,C$ have the same
modality, we can uniquely infer the structure of $A$ and $C$ from the
structure of $B$ by inversion on the appropriate subtyping rule.

######  Case 1.

$A={\uparrow_{L}^{L}}A^{\prime}_{\scriptscriptstyle L}$; then
$B={\uparrow_{L}^{L}}B^{\prime}_{\scriptscriptstyle L}$ and
$C={\uparrow_{L}^{L}}C^{\prime}_{\scriptscriptstyle L}$ with
$A^{\prime}_{\scriptscriptstyle L}\leq B^{\prime}_{\scriptscriptstyle L}\leq
C^{\prime}_{\scriptscriptstyle L}$.

$\displaystyle({\uparrow_{L}^{L}}A^{\prime}_{\scriptscriptstyle
L},{\uparrow_{L}^{L}}C^{\prime}_{\scriptscriptstyle L},\hat{D})$
$\displaystyle\in\text{ssync}_{\Downarrow},({\uparrow_{L}^{L}}B^{\prime}_{\scriptscriptstyle
L},{\uparrow_{L}^{L}}C^{\prime}_{\scriptscriptstyle
L},\hat{D})\in\text{ssync}$ (this case)
$\displaystyle(B^{\prime}_{\scriptscriptstyle
L},C^{\prime}_{\scriptscriptstyle L},\hat{D})$ $\displaystyle\in\text{ssync}$
(by inversion on $D{\uparrow_{L}^{L}}$)
$\displaystyle(A^{\prime}_{\scriptscriptstyle
L},C^{\prime}_{\scriptscriptstyle L},\hat{D})$
$\displaystyle\in\text{ssync}_{\Downarrow}$ (by definition of
$\text{ssync}_{\Downarrow}$ with $A^{\prime}_{\scriptscriptstyle L}\leq
B^{\prime}_{\scriptscriptstyle L}$)
$\displaystyle(A^{\prime}_{\scriptscriptstyle
L},C^{\prime}_{\scriptscriptstyle L},\hat{D})$
$\displaystyle\in\text{ssync}^{\prime}$ (since
$\text{ssync}_{\Downarrow}\subseteq\text{ssync}^{\prime}$)
$\displaystyle({\uparrow_{L}^{L}}A^{\prime}_{\scriptscriptstyle
L},{\uparrow_{L}^{L}}C^{\prime}_{\scriptscriptstyle L},\hat{D})$
$\displaystyle\in F(\text{ssync}^{\prime})$ (by $D{\uparrow_{L}^{L}}$)

${\downarrow_{L}^{L}},\otimes,$ and $\multimap$ follow a similar pattern of
appealing to the covariance of subtyping on the continuation types.

######  Case 2.

$A=\oplus\\{{\overline{l{:}A_{\scriptscriptstyle L}}}\\}$; then
$B=\oplus\\{{\overline{l{:}B_{\scriptscriptstyle
L}},\overline{m{:}B_{\scriptscriptstyle L}}}\\}$ and
$C=\oplus\\{{\overline{l{:}C_{\scriptscriptstyle
L}},\overline{m{:}C_{\scriptscriptstyle
L}},\overline{n{:}C_{\scriptscriptstyle L}}}\\}$ with
${A_{i}}_{\scriptscriptstyle L}\leq{B_{i}}_{\scriptscriptstyle
L}\leq{C_{i}}_{\scriptscriptstyle L}\;\forall i\in\overline{l}$ and
${B_{i}}_{\scriptscriptstyle L}\leq{C_{i}}_{\scriptscriptstyle L}\;\forall
i\in\overline{m}$.

$\displaystyle(\oplus\\{{\overline{l{:}A_{\scriptscriptstyle
L}}}\\},\oplus\\{{\overline{l{:}C_{\scriptscriptstyle
L}},\overline{m{:}C_{\scriptscriptstyle
L}},\overline{n{:}C_{\scriptscriptstyle L}}}\\},\hat{D})$
$\displaystyle\in\text{ssync}_{\Downarrow}$
$\displaystyle(\oplus\\{{\overline{l{:}B_{\scriptscriptstyle
L}},\overline{m{:}B_{\scriptscriptstyle
L}}}\\},\oplus\\{{\overline{l{:}C_{\scriptscriptstyle
L}},\overline{m{:}C_{\scriptscriptstyle
L}},\overline{n{:}C_{\scriptscriptstyle L}}}\\},\hat{D})$
$\displaystyle\in\text{ssync}$ (this case) $\displaystyle(\forall
i\in\overline{l},\overline{m})\;({B_{i}}_{\scriptscriptstyle
L},{C_{i}}_{\scriptscriptstyle L},\hat{D})$ $\displaystyle\in\text{ssync}$ (by
inversion on $D{\oplus}$) $\displaystyle(\forall
i\in\overline{l})\;({A_{i}}_{\scriptscriptstyle L},{C_{i}}_{\scriptscriptstyle
L},\hat{D})$ $\displaystyle\in\text{ssync}_{\Downarrow}$
$\displaystyle(\forall i\in\overline{l})\;({A_{i}}_{\scriptscriptstyle
L},{C_{i}}_{\scriptscriptstyle L},\hat{D})$
$\displaystyle\in\text{ssync}^{\prime}$ (since
$\text{ssync}_{\Downarrow}\subseteq\text{ssync}^{\prime}$)
$\displaystyle(\oplus\\{{\overline{l{:}A_{\scriptscriptstyle
L}}}\\},\oplus\\{{\overline{l{:}C_{\scriptscriptstyle
L}},\overline{m{:}C_{\scriptscriptstyle
L}},\overline{n{:}C_{\scriptscriptstyle L}}}\\},\hat{D})$ $\displaystyle\in
F(\text{ssync}^{\prime})$ (by $D{\oplus}$)

$D{\&}$ follows a similar pattern.

######  Case 3.

$A={\downarrow_{L}^{S}}A_{\scriptscriptstyle S}$; similar to the proof of
Lemma 11, there are three possible assignments for $B$ and $C$. We will
present one of those subcases: let
$B={\downarrow_{L}^{S}}B_{\scriptscriptstyle S}$ and
$C={\downarrow_{L}^{S}}C_{\scriptscriptstyle S}$ with $A_{\scriptscriptstyle
S}\leq B_{\scriptscriptstyle S}\leq C_{\scriptscriptstyle S}$. The other two
cases are similar.

$\displaystyle({\downarrow_{L}^{S}}A_{\scriptscriptstyle
S},{\downarrow_{L}^{S}}C_{\scriptscriptstyle S},\hat{D})$
$\displaystyle\in\text{ssync}_{\Downarrow},({\downarrow_{L}^{S}}B_{\scriptscriptstyle
S},{\downarrow_{L}^{S}}C_{\scriptscriptstyle S},\hat{D})\in\text{ssync}$ (this
case) $\displaystyle(B_{\scriptscriptstyle S},C_{\scriptscriptstyle S},\top)$
$\displaystyle\in\text{ssync},B_{\scriptscriptstyle S}\leq\hat{D}$ (by
inversion on $D{\downarrow_{L}^{S}}$) $\displaystyle(A_{\scriptscriptstyle
S},C_{\scriptscriptstyle S},\top)$ $\displaystyle\in\text{ssync}_{\Downarrow}$
(by definition of $\text{ssync}_{\Downarrow}$ with $A_{\scriptscriptstyle
S}\leq B_{\scriptscriptstyle S}$) $\displaystyle(A_{\scriptscriptstyle
S},C_{\scriptscriptstyle S},\top)$ $\displaystyle\in\text{ssync}^{\prime}$
(since $\text{ssync}_{\Downarrow}\subseteq\text{ssync}^{\prime}$)
$\displaystyle A_{\scriptscriptstyle S}\leq\hat{D}$ (because
$A_{\scriptscriptstyle S}\leq B_{\scriptscriptstyle S}\leq\hat{D}$)
$\displaystyle({\downarrow_{L}^{S}}A_{\scriptscriptstyle
S},{\downarrow_{L}^{S}}C_{\scriptscriptstyle S},\hat{D})$ $\displaystyle\in
F{\text{ssync}^{\prime}}$ (by $D{\downarrow_{L}^{S}}$)

######  Case 4.

$A={\uparrow_{L}^{S}}A_{\scriptscriptstyle L}$; again, there are three
possible assignments for $B$ and $C$, and we will take the subcase when
$B={\uparrow_{L}^{S}}B_{\scriptscriptstyle L}$ and
$C={\uparrow_{L}^{S}}C_{\scriptscriptstyle L}$ with $A_{\scriptscriptstyle
L}\leq B_{\scriptscriptstyle L}\leq C_{\scriptscriptstyle L}$. The other two
cases are similar. This case finally uses our assumption that
$(A,C,\hat{E})\in\text{ssync}$ – $\hat{E}$ must be $\top$ due to
$A={\uparrow_{L}^{S}}A_{\scriptscriptstyle L}$.

$\displaystyle({\uparrow_{L}^{S}}A_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}C_{\scriptscriptstyle L},\top)$
$\displaystyle\in\text{ssync}_{\Downarrow},({\uparrow_{L}^{S}}B_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}C_{\scriptscriptstyle L},\top)\in\text{ssync}$ (this
case) $\displaystyle({\uparrow_{L}^{S}}A_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}C_{\scriptscriptstyle L},\top)$
$\displaystyle\in\text{ssync}$ (By assumption with $\hat{E}=\top$)
$\displaystyle(A_{\scriptscriptstyle L},C_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}A_{\scriptscriptstyle L})$ $\displaystyle\in\text{ssync}$
(by inversion on $D{\uparrow_{L}^{S}}$) $\displaystyle(A_{\scriptscriptstyle
L},C_{\scriptscriptstyle L},{\uparrow_{L}^{S}}A_{\scriptscriptstyle L})$
$\displaystyle\in\text{ssync}^{\prime}$ (since
$\text{ssync}\subseteq\text{ssync}^{\prime}$)
$\displaystyle({\uparrow_{L}^{S}}A_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}C_{\scriptscriptstyle L},\top)$ $\displaystyle\in
F(\text{ssync}^{\prime})$ (by $D{\uparrow_{L}^{S}}$)

We missed one case, when $A=B=C=1$, but this case is trivial since
$\text{ssync}_{\Downarrow}$ does not add any new members to the set.

######  Lemma 29.

If $\vdash(A_{\scriptscriptstyle L},B_{\scriptscriptstyle
L},\hat{C})\;\text{ssync}$ and $\vdash(A_{\scriptscriptstyle
L},B_{\scriptscriptstyle L},\hat{D})\;\text{ssync}$, then
${\vdash(A_{\scriptscriptstyle L},B_{\scriptscriptstyle
L},\hat{C}\land\hat{D})\;\text{ssync}}$ for some $A_{\scriptscriptstyle
L},B_{\scriptscriptstyle L},\hat{C},$ and $\hat{D}$.

######  Proof B.11.

First, recall that $\vdash(A_{\scriptscriptstyle L},B_{\scriptscriptstyle
L},-)\;\text{ssync}$ requires that $A_{\scriptscriptstyle L}\leq
B_{\scriptscriptstyle L}$. We want to show that

$\text{ssync}^{\prime}\;::=\;\text{ssync}\cup\text{ssync}_{\land}$

is $F$-consistent with

$\displaystyle\text{ssync}_{\land}\;::=\;\\{(A_{\scriptscriptstyle
L},B_{\scriptscriptstyle L},\hat{C}\land\hat{D})\;|\;(A_{\scriptscriptstyle
L},B_{\scriptscriptstyle L},\hat{C})\in\text{ssync}\land(A_{\scriptscriptstyle
L},B_{\scriptscriptstyle L},\hat{D})\in\text{ssync}$

As per usual, we will prove $F$-consistency of $\text{ssync}^{\prime}$, that
is, $\text{ssync}^{\prime}\in F(\text{ssync}^{\prime})$ by showing that each
of the two sets ssync and $\text{ssync}_{\land}$ are subsets of
$F(\text{ssync}^{\prime})$.
$\text{ssync}\subseteq F(\text{ssync}^{\prime})$ immediately follows from the
same argument as in previous lemmas.
We will now consider $\text{ssync}_{\land}\in F(\text{ssync}^{\prime})$ by
case analysis on the structure of $A_{\scriptscriptstyle L}$. We can infer the
structure of $B_{\scriptscriptstyle L}$ by inversion on the appropriate
subtyping rule. For ease of presentation, let $\hat{E}=\hat{C}\land\hat{D}$;
we will expand $\hat{E}$ whenever necessary.

######  Case 1.

$A_{\scriptscriptstyle L}={\uparrow_{L}^{L}}A^{\prime}_{\scriptscriptstyle
L}$; then $B_{\scriptscriptstyle
L}={\uparrow_{L}^{L}}B^{\prime}_{\scriptscriptstyle L}$ with
$A^{\prime}_{\scriptscriptstyle L}\leq B^{\prime}_{\scriptscriptstyle L}$.

$\displaystyle({\uparrow_{L}^{L}}A^{\prime}_{\scriptscriptstyle
L},{\uparrow_{L}^{L}}B^{\prime}_{\scriptscriptstyle L},\hat{E})$
$\displaystyle\in\text{ssync}_{\land},({\uparrow_{L}^{L}}A^{\prime}_{\scriptscriptstyle
L},{\uparrow_{L}^{L}}B^{\prime}_{\scriptscriptstyle
L},\hat{C})\in\text{ssync},({\uparrow_{L}^{L}}A^{\prime}_{\scriptscriptstyle
L},{\uparrow_{L}^{L}}B^{\prime}_{\scriptscriptstyle
L},\hat{D})\in\text{ssync}$ (this case)
$\displaystyle(A^{\prime}_{\scriptscriptstyle
L},B^{\prime}_{\scriptscriptstyle L},\hat{C})$
$\displaystyle\in\text{ssync},(A^{\prime}_{\scriptscriptstyle
L},B^{\prime}_{\scriptscriptstyle L},\hat{D})\in\text{ssync}$ (by inversion on
$D{\uparrow_{L}^{L}}$) $\displaystyle(A^{\prime}_{\scriptscriptstyle
L},B^{\prime}_{\scriptscriptstyle L},\hat{E})$
$\displaystyle\in\text{ssync}_{\land}$ (by definition of
$\text{ssync}_{\land}$) $\displaystyle(A^{\prime}_{\scriptscriptstyle
L},B^{\prime}_{\scriptscriptstyle L},\hat{E})$
$\displaystyle\in\text{ssync}^{\prime}$ (since
$\text{ssync}_{\land}\subseteq\text{ssync}^{\prime}$)
$\displaystyle({\uparrow_{L}^{L}}A^{\prime}_{\scriptscriptstyle
L},{\uparrow_{L}^{L}}B^{\prime}_{\scriptscriptstyle L},\hat{E})$
$\displaystyle\in F(\text{ssync}^{\prime})$ (by $D{\uparrow_{L}^{L}}$)

${\downarrow_{L}^{L}},\otimes,$ and $\multimap$ follow a similar pattern of
appealing to the continuation types.

######  Case 2.

$A_{\scriptscriptstyle L}=\oplus\\{{\overline{l{:}A_{\scriptscriptstyle
L}}}\\}$; then $B_{\scriptscriptstyle
L}=\oplus\\{{\overline{l{:}B_{\scriptscriptstyle
L}},\overline{m{:}B_{\scriptscriptstyle L}}}\\}$; with
${A_{i}}_{\scriptscriptstyle L}\leq{B_{i}}_{\scriptscriptstyle L}\;\forall
i\in\overline{l}$.

$\displaystyle(\oplus\\{{\overline{l{:}A_{\scriptscriptstyle
L}}}\\},\oplus\\{{\overline{l{:}B_{\scriptscriptstyle
L}},\overline{m{:}B_{\scriptscriptstyle L}}}\\},\hat{E})$
$\displaystyle\in\text{ssync}_{\land}$
$\displaystyle(\oplus\\{{\overline{l{:}A_{\scriptscriptstyle
L}}}\\},\oplus\\{{\overline{l{:}B_{\scriptscriptstyle
L}},\overline{m{:}B_{\scriptscriptstyle L}}}\\},\hat{C})$
$\displaystyle\in\text{ssync},(\oplus\\{{\overline{l{:}A_{\scriptscriptstyle
L}}}\\},\oplus\\{{\overline{l{:}B_{\scriptscriptstyle
L}},\overline{m{:}B_{\scriptscriptstyle L}}}\\},\hat{D})\in\text{ssync}$ (this
case) $\displaystyle(\forall i\in\overline{l})\;({A_{i}}_{\scriptscriptstyle
L},{B_{i}}_{\scriptscriptstyle L},\hat{C})$
$\displaystyle\in\text{ssync},({A_{i}}_{\scriptscriptstyle
L},{B_{i}}_{\scriptscriptstyle L},\hat{D})\in\text{ssync},$ (by inversion on
$D{\oplus}$) $\displaystyle(\forall
i\in\overline{l})\;({A_{i}}_{\scriptscriptstyle L},{B_{i}}_{\scriptscriptstyle
L},\hat{E})$ $\displaystyle\in\text{ssync}_{\land}$ (by definition of
$\text{ssync}_{\land}$) $\displaystyle(\forall
i\in\overline{l})\;({A_{i}}_{\scriptscriptstyle L},{B_{i}}_{\scriptscriptstyle
L},\hat{E})$ $\displaystyle\in\text{ssync}^{\prime}$ (since
$\text{ssync}_{\land}\subseteq\text{ssync}^{\prime}$)
$\displaystyle(\oplus\\{{\overline{l{:}A_{\scriptscriptstyle
L}}}\\},\oplus\\{{\overline{l{:}B_{\scriptscriptstyle
L}},\overline{m{:}B_{\scriptscriptstyle L}}}\\},\hat{E})$ $\displaystyle\in
F(\text{ssync}^{\prime})$ (by $D{\oplus}$)

$D{\&}$ follows a similar pattern.

######  Case 3.

$A_{\scriptscriptstyle L}={\downarrow_{L}^{S}}A_{\scriptscriptstyle S}$; then
there are two subcases for the structure of $B_{\scriptscriptstyle L}$. We
shall take the case when $B_{\scriptscriptstyle
L}={\downarrow_{L}^{S}}B_{\scriptscriptstyle S}$ with $A_{\scriptscriptstyle
S}\leq B_{\scriptscriptstyle S}$, but the other case, when
$B_{\scriptscriptstyle L}={\downarrow_{L}^{L}}B^{\prime}_{\scriptscriptstyle
L}$ follows a similar pattern.
At this point we realize what $\hat{E}$ has to be – either $\hat{E}=\bot$, in
which case we want to derive a contradiction for this case (the $\bot$
constraint requires that there be no releases) or
$\hat{E}=E_{\scriptscriptstyle S}$ meaning $\hat{E}$ is a non-trivial meet.

######  Subcase 1.

$\hat{E}=\bot$.

$\displaystyle({\downarrow_{L}^{S}}A_{\scriptscriptstyle
S},{\downarrow_{L}^{S}}B_{\scriptscriptstyle S},\bot)$
$\displaystyle\in\text{ssync}_{\land},({\downarrow_{L}^{S}}A_{\scriptscriptstyle
S},{\downarrow_{L}^{S}}B_{\scriptscriptstyle
S},\hat{C})\in\text{ssync},({\downarrow_{L}^{S}}A_{\scriptscriptstyle
S},{\downarrow_{L}^{S}}B_{\scriptscriptstyle S},\hat{D})\in\text{ssync}$ (this
case) $\displaystyle(A_{\scriptscriptstyle S},B_{\scriptscriptstyle S},\top)$
$\displaystyle\in\text{ssync},A_{\scriptscriptstyle S}\leq\hat{C}$ (by
inversion on $D{\downarrow_{L}^{S}}$) $\displaystyle(A_{\scriptscriptstyle
S},B_{\scriptscriptstyle S},\top)$
$\displaystyle\in\text{ssync},A_{\scriptscriptstyle S}\leq\hat{D}$ (by
inversion on $D{\downarrow_{L}^{S}}$) Contradiction (since
$A_{\scriptscriptstyle S}$ is a lower bound of $\hat{C}\land\hat{D}$ but
$A_{\scriptscriptstyle S}$ is strictly greater than $\bot$)

######  Subcase 2.

$\hat{E}=E_{\scriptscriptstyle S}$ for some $E_{\scriptscriptstyle S}$.

$\displaystyle({\downarrow_{L}^{S}}A_{\scriptscriptstyle
S},{\downarrow_{L}^{S}}B_{\scriptscriptstyle S},E_{\scriptscriptstyle S})$
$\displaystyle\in\text{ssync}_{\land},({\downarrow_{L}^{S}}A_{\scriptscriptstyle
S},{\downarrow_{L}^{S}}B_{\scriptscriptstyle
S},\hat{C})\in\text{ssync},({\downarrow_{L}^{S}}A_{\scriptscriptstyle
S},{\downarrow_{L}^{S}}B_{\scriptscriptstyle S},\hat{D})\in\text{ssync}$ (this
case) $\displaystyle(A_{\scriptscriptstyle S},B_{\scriptscriptstyle S},\top)$
$\displaystyle\in\text{ssync},A_{\scriptscriptstyle
S}\leq\hat{C},A_{\scriptscriptstyle S}\leq\hat{D}$ (by inversion on
$D{\downarrow_{L}^{S}}$) $\displaystyle(A_{\scriptscriptstyle
S},B_{\scriptscriptstyle S},\top)$ $\displaystyle\in\text{ssync}^{\prime}$
(since $\text{ssync}\subseteq\text{ssync}^{\prime}$)
$\displaystyle({\downarrow_{L}^{S}}A_{\scriptscriptstyle
S},{\downarrow_{L}^{S}}C_{\scriptscriptstyle S},E_{\scriptscriptstyle S})$
$\displaystyle\in F(\text{ssync}^{\prime})$ (by $D{\downarrow_{L}^{S}}$ with
$A_{\scriptscriptstyle S}\leq E_{\scriptscriptstyle S}$ because
$A_{\scriptscriptstyle S}$ is a lower bound of $\hat{C}$ and $\hat{D}$ and
$E_{\scriptscriptstyle S}$ is the greatest lower bound)

Unlike the previous lemmas, we require $A_{\scriptscriptstyle L}$ to be
linear, so we do not need to consider ${\uparrow_{L}^{S}}$. The case when
$A=B=1$ is trivial.

##  Appendix C Preservation Theorem

######  Theorem 30 (Preservation).

If ${\Gamma\models\Lambda;\Theta::(\Gamma;\Delta)}$ for some
$\Lambda,\Theta,\Gamma,$ and $\Delta$, and
$\Lambda;\Theta\rightarrow\Lambda^{\prime};\Theta^{\prime}$ for some
$\Lambda^{\prime};\Theta^{\prime}$, then
${\Gamma^{\prime}\models\Lambda^{\prime};\Theta^{\prime}::(\Gamma^{\prime};\Delta)}$
where $\Gamma^{\prime}\preceq\Gamma$.

######  Proof C.1.

By induction on the dynamics to construct a well-formed and well-typed
configuration starting with ${\Gamma\models\Lambda;\Theta::(\Gamma;\Delta)}$.

##### Notation

Many of the proof cases involve transitions between linear process terms
(either proc or connect). When reasoning with these transitions, we adopt the
notation that $\Psi_{a}\to\Psi_{a}^{\prime}$ that is, $\Psi_{a}$ represents
the process term offering $a$ before the transition and $\Psi_{a}^{\prime}$
represents the process term offering $a$ after the transition.

######  Case 1.

D-FWDLS

$\text{proc}(a_{\scriptscriptstyle L},\text{fwd}\;a_{\scriptscriptstyle L}\
b_{\scriptscriptstyle S})\to\text{connect}(a_{\scriptscriptstyle
L},b_{\scriptscriptstyle S})$

where $\Psi_{a}=\text{proc}(a_{\scriptscriptstyle
L},\text{fwd}\;a_{\scriptscriptstyle L}\ b_{\scriptscriptstyle S})$ and
$\Psi_{a}^{\prime}=\text{connect}(a_{\scriptscriptstyle
L},b_{\scriptscriptstyle S})$ (for the remaining cases, these metavariable
assignments are implicit). Let $\Theta=\Theta_{1},\Psi_{a},\Theta_{2}$. Then
by well-formedness, $\Lambda=\text{unavail}(a_{\scriptscriptstyle
S}),\Lambda_{1}$.

$\displaystyle{\Gamma\models\Lambda;\Theta_{1},\Psi_{a},\Theta_{2}::(\Gamma;\Delta)}$
(assumption)
$\displaystyle{\Gamma\models\Lambda::(\Gamma)}\quad{\Gamma\models\Theta_{1},\Psi_{a},\Theta_{2}::(\Delta)}$
(by inversion on $\Omega$)
$\displaystyle{\Gamma\models\text{proc}(a_{\scriptscriptstyle
L},\text{fwd}\;a_{\scriptscriptstyle L}\ b_{\scriptscriptstyle
S}),\Theta_{2}::(a_{\scriptscriptstyle L}{:}A_{\scriptscriptstyle
L},\Delta_{p})}$ (by Lemma 4 and expanding $\Psi_{a}$)
$\displaystyle{\Gamma\models\Theta_{2}::(\Delta_{p})}\quad{\Gamma;\cdot\vdash\text{fwd}\;a_{\scriptscriptstyle
L}\ b_{\scriptscriptstyle S}::(a_{\scriptscriptstyle
L}{:}A^{\prime}_{\scriptscriptstyle L})}$ (by inversion on $\Theta 3$)
$\displaystyle b_{\scriptscriptstyle S}{:}\hat{B}\in\Gamma\quad\hat{B}\leq
A^{\prime}_{\scriptscriptstyle L}$ (by inversion on
$ID_{\scriptscriptstyle{LS}}$) $\displaystyle\hat{B}\leq A_{\scriptscriptstyle
L}$ (by transitivity of $\leq$)
$\displaystyle{\Gamma\models\text{connect}(a_{\scriptscriptstyle
L},b_{\scriptscriptstyle S}),\Theta_{2}::(a:A_{\scriptscriptstyle
L},\Delta_{p})}$ (by $\Theta 2$)
$\displaystyle{\Gamma\models\Theta_{1},\Psi_{a}^{\prime},\Theta_{2}::(\Delta)}$
(by Lemma 7)
$\displaystyle{\Gamma\models\Lambda;\Theta_{1},\Psi_{a}^{\prime},\Theta_{2}::(\Gamma;\Delta)}$
(by $\Omega$)

The well-formedness conditions are maintained because only $\Psi_{a}\in\Theta$
was replaced by $\Psi_{a}^{\prime}$.

######  Case 2.

D-$\&$

$\text{proc}(a_{\scriptscriptstyle L},b.i;P),\text{proc}(b_{\scriptscriptstyle
L},\text{case}\;b_{\scriptscriptstyle L}\;\text{of}\;\\{\overline{l\Rightarrow
Q},\overline{m\Rightarrow Q}\\})\to\text{proc}(a_{\scriptscriptstyle
L},P),\text{proc}(b_{\scriptscriptstyle L},Q_{i})\quad(i\in\overline{l})$

Then $\Theta=\Theta_{1},\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3}$

$\displaystyle{\Gamma\models\Lambda;\Theta_{1},\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3}::(\Gamma;\Delta)}$
(assumption)
$\displaystyle{\Gamma\models\Lambda::(\Gamma)}\quad{\Gamma\models\Theta_{1},\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3}::(\Delta)}$
(by inversion on $\Omega$)
$\displaystyle{\Gamma\models\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3}::(a_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L},\Delta_{r})}$ (by Lemma 4)
$\displaystyle{\Gamma\models\Psi_{a},\Psi_{b},\Theta_{r}::(a_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L},\Delta_{r})}$ (by Lemma 6 and
$\Theta_{r}=\Theta_{2},\Theta_{3}$)
$\displaystyle{\Gamma\models\Psi_{b},\Theta_{r}::(b_{\scriptscriptstyle
L}{:}\&\\{{\overline{l{:}B_{\scriptscriptstyle
L}}}\\},\Delta_{a},\Delta_{r})}\quad{\Gamma;\Delta_{a}\vdash
b.i;P::(a_{\scriptscriptstyle L}{:}A^{\prime}_{\scriptscriptstyle L})}$
$\displaystyle\quad a_{\scriptscriptstyle
S}{:}\hat{A}\in\Gamma\quad\vdash(A^{\prime}_{\scriptscriptstyle
L},A_{\scriptscriptstyle L},\hat{A})\;\text{ssync}$ (by inversion on $\Theta
3$)
$\displaystyle{\Gamma\models\Theta_{r}::(\Delta_{a},\Delta_{b},\Delta_{r})}\quad{\Gamma;\Delta_{b}\vdash\text{case}\;b_{\scriptscriptstyle
L}\;\text{of}\;\\{\overline{l\Rightarrow Q},\overline{m\Rightarrow
Q}\\}::(b_{\scriptscriptstyle
L}{:}\&\\{{\overline{l{:}B^{\prime}_{\scriptscriptstyle
L}},\overline{m{:}B^{\prime}_{\scriptscriptstyle L}}}\\})}$
$\displaystyle\quad b_{\scriptscriptstyle
S}{:}\hat{B}\in\Gamma\quad\vdash(\&\\{{\overline{l{:}B^{\prime}_{\scriptscriptstyle
L}},\overline{m{:}B^{\prime}_{\scriptscriptstyle
L}}}\\},\&\\{{\overline{l{:}B_{\scriptscriptstyle
L}}}\\},\hat{B})\;\text{ssync}$ (by inversion on $\Theta 3$)
$\displaystyle{\Gamma;\Delta_{b}\vdash Q_{i}::(b_{\scriptscriptstyle
L}{:}{B_{i}}^{\prime}_{\scriptscriptstyle L})}$ (inversion on ${\&}R$)
$\displaystyle{B_{i}}^{\prime}_{\scriptscriptstyle
L}\leq{B_{i}}_{\scriptscriptstyle
L}\quad\vdash({B_{i}^{\prime}}_{\scriptscriptstyle
L},{B_{i}}_{\scriptscriptstyle L},\hat{B})\;\text{ssync}$ (by inversion on
$\leq_{\&}$ and E& respectively)
$\displaystyle{\Gamma\models\Psi_{b}^{\prime},\Theta_{r}::(b_{\scriptscriptstyle
L}{:}{B_{i}}_{\scriptscriptstyle L},\Delta_{r},\Delta_{a})}$ (by $\Theta 3$)
$\displaystyle{\Gamma;\Delta_{a},b_{\scriptscriptstyle
L}{:}{B_{i}}_{\scriptscriptstyle L}\vdash P::(a_{\scriptscriptstyle
L}{:}A^{\prime}_{\scriptscriptstyle L})}$ (inversion on ${\&}L$)
$\displaystyle{\Gamma\models\Psi_{a}^{\prime},\Psi_{b}^{\prime},\Theta_{r}::(a_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L},\Delta_{r})}$ (by $\Theta 3$)
$\displaystyle{\Gamma\models\Theta_{1},\Psi_{a}^{\prime},\Psi_{b}^{\prime},\Theta_{r}::(\Delta)}$
(by Lemma 7)
$\displaystyle{\Gamma\models\Lambda;\Theta_{1},\Psi_{a}^{\prime},\Psi_{b}^{\prime},\Theta_{r}::(\Gamma;\Delta)}$
(by $\Omega$)

The well-formedness conditions are maintained because $\Psi_{a}$ and
$\Psi_{b}$ were replaced by $\Psi_{a}^{\prime}$ and $\Psi_{b}^{\prime}$
respectively in $\Theta$.

The proof of D-$\oplus$ is similar to D-$\&$.

######  Case 3.

D-$\otimes$

$\text{proc}(a_{\scriptscriptstyle L},y_{\scriptscriptstyle
L}\leftarrow\text{recv}\;b_{\scriptscriptstyle
L};P),\text{proc}(b_{\scriptscriptstyle L},\text{send}\;b_{\scriptscriptstyle
L}\ c_{\scriptscriptstyle L};Q),\Psi_{c}\to\text{proc}(a_{\scriptscriptstyle
L},[c_{\scriptscriptstyle L}/y_{\scriptscriptstyle
L}]P),\text{proc}(b_{\scriptscriptstyle L},Q),\Psi_{c}$

Then
$\Theta=\Theta_{1},\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3},\Psi_{c},\Theta_{4}$.

$\displaystyle{\Gamma\models\Lambda;\Theta_{1},\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3},\Psi_{c},\Theta_{4}::(\Gamma;\Delta)}$
(assumption)
$\displaystyle{\Gamma\models\Lambda::(\Gamma)}\quad{\Gamma\models\Theta_{1},\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3},\Psi_{c},\Theta_{4}::(\Delta)}$
(by inversion on $\Omega$)
$\displaystyle{\Gamma\models\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3},\Psi_{c},\Theta_{4}::(a_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L},\Delta_{r})}$ (by Lemma 4)
$\displaystyle{\Gamma\models\Psi_{a},\Psi_{b},\Psi_{c},\Theta_{r}::(a_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L},\Delta_{r})}$ (by Lemma 6 and
$\Theta_{r}=\Theta_{2},\Theta_{3},\Theta_{4}$)
$\displaystyle{\Gamma\models\Psi_{b},\Psi_{c},\Theta_{r}::(b_{\scriptscriptstyle
L}{:}C^{a}_{\scriptscriptstyle L}\otimes B_{\scriptscriptstyle
L},\Delta_{a},\Delta_{r})}\quad{\Gamma;\Delta_{a},b_{\scriptscriptstyle
L}{:}B_{\scriptscriptstyle L}\vdash y_{\scriptscriptstyle
L}\leftarrow\text{recv}\;b_{\scriptscriptstyle L};P::(a_{\scriptscriptstyle
L}{:}A^{\prime}_{\scriptscriptstyle L})}$ $\displaystyle a_{\scriptscriptstyle
S}{:}\hat{A}\in\Gamma\quad\vdash(A^{\prime}_{\scriptscriptstyle
L},A_{\scriptscriptstyle L},\hat{A})\;\text{ssync}$ (by inversion on $\Theta
3$) $\displaystyle{\Gamma;\Delta_{a},b_{\scriptscriptstyle
L}{:}B_{\scriptscriptstyle L},c_{\scriptscriptstyle
L}{:}C^{a}_{\scriptscriptstyle L}\vdash[c_{\scriptscriptstyle
L}/y_{\scriptscriptstyle L}]P::(a_{\scriptscriptstyle
L}{:}A^{\prime}_{\scriptscriptstyle L})}$ (by inversion on ${\otimes}L$ and
$\alpha$ equivalance)
$\displaystyle{\Gamma\models\Psi_{c},\Theta_{r}::(c_{\scriptscriptstyle
L}{:}C_{\scriptscriptstyle
L},\Delta_{a},\Delta_{b},\Delta_{r})}\quad{\Gamma;\Delta_{b},c_{\scriptscriptstyle
L}{:}C_{\scriptscriptstyle L}\vdash\text{send}\;b_{\scriptscriptstyle L}\
c_{\scriptscriptstyle L};Q::(b_{\scriptscriptstyle
L}{:}C^{b}_{\scriptscriptstyle L}\otimes B^{\prime}_{\scriptscriptstyle L})}$
$\displaystyle b_{\scriptscriptstyle
S}{:}\hat{B}\in\Gamma\quad\vdash(C^{b}_{\scriptscriptstyle L}\otimes
B^{\prime}_{\scriptscriptstyle L},C^{a}_{\scriptscriptstyle L}\otimes
B_{\scriptscriptstyle L},\hat{B})\;\text{ssync}$ (by inversion on $\Theta 3$)
$\displaystyle{\Gamma;\Delta_{b}\vdash Q::(b_{\scriptscriptstyle
L}{:}B^{\prime}_{\scriptscriptstyle L})}\quad C_{\scriptscriptstyle L}\leq
C^{b}_{\scriptscriptstyle L}$ (by inversion on ${\otimes}R$) $\displaystyle
C^{b}_{\scriptscriptstyle L}\leq C^{a}_{\scriptscriptstyle L}\quad
B^{\prime}_{\scriptscriptstyle L}\leq B_{\scriptscriptstyle
L}\quad\vdash(B^{\prime}_{\scriptscriptstyle L},B_{\scriptscriptstyle
L},\hat{B})\;\text{ssync}$ (by inversion on $\leq_{\otimes}$ and $E{\otimes}$
respectively)
$\displaystyle{\Gamma\models\Psi_{c},\Theta_{r}::(c_{\scriptscriptstyle
L}{:}C^{a}_{\scriptscriptstyle L},\Delta_{a},\Delta_{b},\Delta_{r})}$ (by
Lemma 8 since $C_{\scriptscriptstyle L}\leq C^{b}_{\scriptscriptstyle L}\leq
C^{a}_{\scriptscriptstyle L}$.)
$\displaystyle{\Gamma\models\Psi_{b}^{\prime},\Psi_{c},\Theta_{r}::(b_{\scriptscriptstyle
L}{:}B_{\scriptscriptstyle L},c_{\scriptscriptstyle
L}{:}C^{a}_{\scriptscriptstyle L},\Delta_{a},\Delta_{r})}$ (by $\Theta 3$)
$\displaystyle{\Gamma\models\Psi_{a}^{\prime},\Psi_{b}^{\prime},\Psi_{c},\Theta_{r}::(a_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L},\Delta_{r})}$ (by $\Theta 3$)
$\displaystyle{\Gamma\models\Theta_{1},\Psi_{a}^{\prime},\Psi_{b}^{\prime},\Psi_{c},\Theta_{r}::(\Delta)}$
(by Lemma 7)
$\displaystyle{\Gamma\models\Lambda;\Theta_{1},\Psi_{a}^{\prime},\Psi_{b}^{\prime},\Psi_{c},\Theta_{r}::(\Gamma;\Delta)}$
(by $\Omega$)

The well-formedness conditions are maintained because $\Psi_{a}$ and
$\Psi_{b}$ were replaced by $\Psi_{a}^{\prime}$ and $\Psi_{b}^{\prime}$
respectively in $\Theta$.

######  Case 4.

D-$\otimes$2

$\displaystyle\text{proc}(a_{\scriptscriptstyle L},y_{\scriptscriptstyle
L}\leftarrow\text{recv}\;b_{\scriptscriptstyle
L};P),\text{proc}(b_{\scriptscriptstyle L},\text{send}\;b_{\scriptscriptstyle
L}\ c_{\scriptscriptstyle S};Q)$ $\displaystyle\to\quad$
$\displaystyle\text{proc}(a_{\scriptscriptstyle L},[d_{\scriptscriptstyle
L}/y_{\scriptscriptstyle L}]P),\text{proc}(b_{\scriptscriptstyle
L},Q),\text{connect}(d_{\scriptscriptstyle L},c_{\scriptscriptstyle
S}),\text{unavail}(d_{\scriptscriptstyle S})\quad(d\;\;\text{fresh})$

Then $\Theta=\Theta_{1},\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3}$.

$\displaystyle{\Gamma\models\Lambda;\Theta_{1},\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3}::(\Gamma;\Delta)}$
(assumption)
$\displaystyle{\Gamma\models\Lambda::(\Gamma)}\quad{\Gamma\models\Theta_{1},\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3}::(\Delta)}$
(by inversion on $\Omega$)
$\displaystyle{\Gamma\models\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3}::(a_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L},\Delta_{r})}$ (by Lemma 4)
$\displaystyle{\Gamma\models\Psi_{a},\Psi_{b},\Theta_{r}::(a_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L},\Delta_{r})}$ (by Lemma 6 and
$\Theta_{r}=\Theta_{2},\Theta_{3}$)
$\displaystyle{\Gamma\models\Psi_{b},\Theta_{r}::(b_{\scriptscriptstyle
L}{:}C^{a}_{\scriptscriptstyle L}\otimes B_{\scriptscriptstyle
L},\Delta_{a},\Delta_{r})}\quad{\Gamma;\Delta_{a},b_{\scriptscriptstyle
L}{:}B_{\scriptscriptstyle L}\vdash y_{\scriptscriptstyle
L}\leftarrow\text{recv}\;b_{\scriptscriptstyle L};P::(a_{\scriptscriptstyle
L}{:}A^{\prime}_{\scriptscriptstyle L})}$ $\displaystyle a_{\scriptscriptstyle
S}{:}\hat{A}\in\Gamma\quad\vdash(A^{\prime}_{\scriptscriptstyle
L},A_{\scriptscriptstyle L},\hat{A})\;\text{ssync}$ (by inversion on $\Theta
3$) $\displaystyle{\Gamma;\Delta_{a},b_{\scriptscriptstyle
L}{:}B_{\scriptscriptstyle L},d_{\scriptscriptstyle
L}{:}C^{a}_{\scriptscriptstyle L}\vdash[d_{\scriptscriptstyle
L}/y_{\scriptscriptstyle L}]P::(a_{\scriptscriptstyle
L}{:}A^{\prime}_{\scriptscriptstyle L})}$ (by inversion on ${\otimes}L$ and
$\alpha$ equivalance)
$\displaystyle{\Gamma\models\Theta_{r}::(\Delta_{a},\Delta_{b},\Delta_{r})}\quad{\Gamma;\Delta_{b},c_{\scriptscriptstyle
L}{:}C_{\scriptscriptstyle L}\vdash\text{send}\;b_{\scriptscriptstyle L}\
c_{\scriptscriptstyle S};Q::(b_{\scriptscriptstyle
L}{:}C^{b}_{\scriptscriptstyle L}\otimes B^{\prime}_{\scriptscriptstyle L})}$
$\displaystyle b_{\scriptscriptstyle
S}{:}\hat{B}\in\Gamma\quad\vdash(C^{b}_{\scriptscriptstyle L}\otimes
B^{\prime}_{\scriptscriptstyle L},C^{a}_{\scriptscriptstyle L}\otimes
B_{\scriptscriptstyle L},\hat{B})\;\text{ssync}$ (by inversion on $\Theta 3$)
$\displaystyle{\Gamma;\Delta_{b}\vdash Q::(b_{\scriptscriptstyle
L}{:}B^{\prime}_{\scriptscriptstyle L})}\quad\hat{C}\leq
C^{b}_{\scriptscriptstyle L}$ (by inversion on ${\otimes}R_{\scriptscriptstyle
S}$) $\displaystyle{\Gamma\models\text{connect}(d_{\scriptscriptstyle
L},c_{\scriptscriptstyle S}),\Theta_{r}::(d:C^{a}_{\scriptscriptstyle
L},\Delta_{a},\Delta_{b},\Delta_{r})}$
$\displaystyle{\Gamma\models\Psi_{b}^{\prime},\Psi_{d},\Theta_{r}::(b_{\scriptscriptstyle
L}{:}B_{\scriptscriptstyle L},d_{\scriptscriptstyle
L}{:}C^{a}_{\scriptscriptstyle L},\Delta_{a},\Delta_{r})}$ (by $\Theta 3$
where $\Psi_{d}=\text{connect}(d_{\scriptscriptstyle L},c_{\scriptscriptstyle
S})$)
$\displaystyle{\Gamma\models\Psi_{a}^{\prime},\Psi_{b}^{\prime},\Psi_{d},\Theta_{r}::(a_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L},\Delta_{r})}$ (by $\Theta 3$)
$\displaystyle{\Gamma\models\Theta_{1},\Psi_{a}^{\prime},\Psi_{b}^{\prime},\Psi_{d},\Theta_{r}::(\Delta)}$
(by Lemma 7)
$\displaystyle{\Gamma^{\prime}\models\Theta_{1},\Psi_{a}^{\prime},\Psi_{b}^{\prime},\Psi_{d},\Theta_{r}::(\Delta)}$
(by Lemma 10 with $\Gamma^{\prime}=\Gamma,d_{\scriptscriptstyle S}{:}\bot$)
$\displaystyle{\Gamma^{\prime}\models\Lambda::(\Gamma)}$ (by Lemma 10)
$\displaystyle{\Gamma^{\prime}\models\text{unavail}(d_{\scriptscriptstyle
S})::(d_{\scriptscriptstyle S}{:}\bot)}$ (by $\Lambda 4$)
$\displaystyle{\Gamma^{\prime}\models\Lambda,\text{unavail}(d_{\scriptscriptstyle
S})::(\Gamma^{\prime})}$ (by $\Lambda 2$)
$\displaystyle{\Gamma^{\prime}\models\Lambda,\text{unavail}(d_{\scriptscriptstyle
S});\Theta_{1},\Psi_{a}^{\prime},\Psi_{b}^{\prime},\Psi_{d},\Theta_{r}::(\Gamma^{\prime};\Delta)}$
(by $\Omega$)

The well-formedness conditions are maintained because $\Psi_{a}$ and
$\Psi_{b}$ were replaced by $\Psi_{a}^{\prime}$ and $\Psi_{b}^{\prime}$
respectively in $\Theta$ and a $\Psi_{d}$ was added in $\Theta$ where $d$ is
fresh along with a corresponding $\text{unavail}(d_{\scriptscriptstyle S})$ in
$\Lambda^{\prime}=\Lambda,\text{unavail}(d_{\scriptscriptstyle S})$.

The proofs of D-$\multimap$ and D-$\multimap$2 are similar to D-$\otimes$ and
D-$\otimes$2 respectively.
We will now present some of the harder cases:

######  Case 5.

D-FWDLL

$\text{proc}(a_{\scriptscriptstyle L},\text{fwd}\;a_{\scriptscriptstyle L}\
b_{\scriptscriptstyle L}),\Psi_{b}\to\Psi_{b}\quad(a_{\scriptscriptstyle
L}:=b_{\scriptscriptstyle L},a_{\scriptscriptstyle S}:=b_{\scriptscriptstyle
S})$

Then $\Theta=\Theta_{1},\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3}$ and
$\Lambda=\text{unavail}(a_{\scriptscriptstyle
S}),\text{unavail}(b_{\scriptscriptstyle S}),\Lambda_{1}$ by Lemma 5.

$\displaystyle{\Gamma\models\Lambda;\Theta_{1},\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3}::(\Gamma;\Delta)}$
(assumption)
$\displaystyle{\Gamma\models\Lambda::(\Gamma)}\quad{\Gamma\models\Theta_{1},\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3}::(\Delta)}$
(by inversion on $\Omega$)
$\displaystyle{\Gamma\models\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3}::(a_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L},\Delta_{r})}$ (by Lemma 4)
$\displaystyle{\Gamma\models\Psi_{a},\Psi_{b},\Theta_{r}::(a_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L},\Delta_{r})}$ (by Lemma 6 and
$\Theta_{r}=\Theta_{2},\Theta_{3}$)
$\displaystyle{\Gamma\models\Psi_{b},\Theta_{r}::(b_{\scriptscriptstyle
L}{:}b_{\scriptscriptstyle L}{:}B_{\scriptscriptstyle
L},\Delta_{r})}\;{\Gamma;b_{\scriptscriptstyle L}{:}B_{\scriptscriptstyle
L}\vdash\text{fwd}\;a_{\scriptscriptstyle L}\ b_{\scriptscriptstyle
L}::(a_{\scriptscriptstyle L}{:}A^{\prime}_{\scriptscriptstyle
L})}\;a_{\scriptscriptstyle
S}{:}\hat{A}\in\Gamma\;\vdash(A^{\prime}_{\scriptscriptstyle
L},A_{\scriptscriptstyle L},\hat{A})\;\text{ssync}$ (by inversion on $\Theta
3$) $\displaystyle B_{\scriptscriptstyle L}\leq A^{\prime}_{\scriptscriptstyle
L}$ (by inversion on $ID_{\scriptscriptstyle L}$)

At this point we need to case on the structure of $\Psi_{b}$. In both cases we
will show that
${\Gamma^{\prime}\models\Psi_{a}^{\prime},\Theta_{r}::(a_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L},\Delta_{r})}$ for some
$\Gamma^{\prime}\preceq\Gamma$ and $\Psi_{a}^{\prime}$ being directly defined
from $\Psi_{b}$.

######  Subcase 1.

$\Psi_{b}=\text{connect}(b_{\scriptscriptstyle L},c_{\scriptscriptstyle S})$
for some $c_{\scriptscriptstyle S}$.

$\displaystyle{\Gamma\models\text{connect}(b_{\scriptscriptstyle
L},c_{\scriptscriptstyle S}),\Theta_{r}::(b:B_{\scriptscriptstyle
L},\Delta_{r})}\quad c_{\scriptscriptstyle
S}{:}\hat{C}\in\Gamma\quad\hat{C}\leq B_{\scriptscriptstyle L}$ (by inversion
on $\Theta 2$) $\displaystyle\hat{C}\leq A_{\scriptscriptstyle L}$ (by
transitivity of $\leq$)
$\displaystyle{\Gamma\models\text{connect}(b_{\scriptscriptstyle
L},c_{\scriptscriptstyle S}),\Theta_{r}::(b:A_{\scriptscriptstyle
L},\Delta_{r})}$ (by $\Theta 2$)
$\displaystyle{\Gamma\models\text{connect}(a_{\scriptscriptstyle
L},c_{\scriptscriptstyle S}),\Theta_{r}::(a:A_{\scriptscriptstyle
L},\Delta_{r})}$ (from renaming)

######  Subcase 2.

$\Psi_{b}=\text{proc}(b_{\scriptscriptstyle L},P)$ for some process term $P$.

$\displaystyle{\Gamma\models\Theta_{r}::(\Delta_{b},\Delta_{r})}\quad{\Gamma;\Delta_{b}\vdash
P::(b_{\scriptscriptstyle L}{:}B^{\prime}_{\scriptscriptstyle L})}\quad
b_{\scriptscriptstyle
S}{:}\hat{B}\in\Gamma\quad\vdash(B^{\prime}_{\scriptscriptstyle
L},B_{\scriptscriptstyle L},\hat{B})\;\text{ssync}$ (by inversion on $\Theta
3$) $\displaystyle B^{\prime}_{\scriptscriptstyle L}\leq B_{\scriptscriptstyle
L}\leq A^{\prime}_{\scriptscriptstyle L}\leq A_{\scriptscriptstyle L}$
$\displaystyle\vdash(B^{\prime}_{\scriptscriptstyle L},A_{\scriptscriptstyle
L},\hat{B})\;\text{ssync}\quad\vdash(B^{\prime}_{\scriptscriptstyle
L},A_{\scriptscriptstyle L},\hat{A})\;\text{ssync}$ (by Lemma 11 and Lemma 12
respectively) $\displaystyle\vdash(B^{\prime}_{\scriptscriptstyle
L},A_{\scriptscriptstyle L},\hat{B}\land\hat{A})\;\text{ssync}$ (by Lemma 14)
$\displaystyle{\Gamma^{\prime}\models\Theta_{r}::(\Delta_{b},\Delta_{r})}$ (by
Lemma 10 with $\Gamma^{\prime}=[a_{\scriptscriptstyle
S}{:}\hat{B}\land\hat{A}/a_{\scriptscriptstyle S}{:}\hat{A}]\Gamma$)
$\displaystyle{\Gamma^{\prime};\Delta_{b}\vdash P::(b_{\scriptscriptstyle
L}{:}B^{\prime}_{\scriptscriptstyle L})}$ (by Lemma 9)
$\displaystyle{\Gamma^{\prime};\Delta_{b}\vdash[a_{\scriptscriptstyle
L}/b_{\scriptscriptstyle L},a_{\scriptscriptstyle S}/b_{\scriptscriptstyle
S}]P::(a_{\scriptscriptstyle L}{:}B^{\prime}_{\scriptscriptstyle L})}$ (by
$\alpha$ equivalence for $a_{\scriptscriptstyle L}/b_{\scriptscriptstyle L}$
and a combination of $\alpha$ equivalence and Lemma 10 for
$a_{\scriptscriptstyle S}/b_{\scriptscriptstyle S}$)
$\displaystyle{\Gamma^{\prime}\models\text{proc}(a_{\scriptscriptstyle
L},[a_{\scriptscriptstyle L}/b_{\scriptscriptstyle L},a_{\scriptscriptstyle
S}/b_{\scriptscriptstyle S}]P),\Theta_{r}::(a:A_{\scriptscriptstyle
L},\Delta_{r})}$ (by $\Theta 3$)

We will now continue assuming
${\Gamma^{\prime}\models\Psi_{a}^{\prime},\Theta_{r}::(a_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L},\Delta_{r})}$ with
$\Gamma^{\prime}\preceq\Gamma$ and $\Psi_{a}^{\prime}=[a_{\scriptscriptstyle
L}/b_{\scriptscriptstyle L},a_{\scriptscriptstyle S}/b_{\scriptscriptstyle
S}]\Psi_{b}$. For the connect case that did not require a smaller $\Gamma$,
simply set $\Gamma^{\prime}=\Gamma$ since $\Gamma^{\prime}\preceq\Gamma$ by
reflexivity.

$\displaystyle{\Gamma^{\prime}\models\Theta_{1},\Psi_{a},\Theta_{r}::(\Delta)}$
(by Lemma 10)
$\displaystyle{\Gamma^{\prime}\models\Theta_{1},\Psi_{a}^{\prime},\Theta_{r}::(\Delta)}$
(by Lemma 7) $\displaystyle{\Gamma^{\prime}\models\Lambda::(\Gamma)}$ (by
Lemma 7)
$\displaystyle{\Gamma^{\prime}\models\text{unavail}(a_{\scriptscriptstyle
S})::(a_{\scriptscriptstyle S}{:}\bot)}$ (by $\Lambda 4$)
$\displaystyle{\Gamma^{\prime}\models\text{unavail}(b_{\scriptscriptstyle
S}),\Theta_{1}::(\Gamma^{\prime\prime})}$ (by inversion on $\Lambda 2$ where
$\Gamma^{\prime}=\Gamma^{\prime\prime},a_{\scriptscriptstyle S}{:}\bot$)
$\displaystyle{\Gamma^{\prime}\models\Lambda::(\Gamma^{\prime})}$ (by $\Lambda
2$) $\displaystyle{\Gamma^{\prime}\models[a_{\scriptscriptstyle
S}/b_{\scriptscriptstyle S}]\Lambda::(\Gamma^{\prime})}$ (by $\alpha$
equivalence) $\displaystyle{\Gamma^{\prime}\models[a_{\scriptscriptstyle
S}/b_{\scriptscriptstyle
S}]\Theta_{1},\Psi_{a}^{\prime},[a_{\scriptscriptstyle
S}/b_{\scriptscriptstyle S}]\Theta_{r}::(\Delta)}$ (by $\alpha$ equivalence)
$\displaystyle{\Gamma^{\prime}\models\Lambda;[a_{\scriptscriptstyle
S}/b_{\scriptscriptstyle S},a_{\scriptscriptstyle L}/b_{\scriptscriptstyle
L}]\Theta_{1},\Psi_{a}^{\prime},[a_{\scriptscriptstyle
S}/b_{\scriptscriptstyle S}]\Theta_{r}::(\Gamma^{\prime};\Delta)}$ (by
$\Omega$)

Well-formedness is easily maintained because we only removed something from
the linear fragment (it is okay to have dangling unavail terms in the shared
fragment).

######  Case 6.

D-${\uparrow_{L}^{S}}$

$\displaystyle\text{proc}(a_{\scriptscriptstyle L},x_{\scriptscriptstyle
L}\leftarrow\text{acq}_{\scriptscriptstyle S}\;b_{\scriptscriptstyle
S};P),\text{proc}(b_{\scriptscriptstyle S},x_{\scriptscriptstyle
L}\leftarrow\text{acc}_{\scriptscriptstyle S}\;b_{\scriptscriptstyle S};Q)$
$\displaystyle\to\quad$ $\displaystyle\text{proc}(a_{\scriptscriptstyle
L},[b_{\scriptscriptstyle L}/x_{\scriptscriptstyle
L}]P),\text{proc}(b_{\scriptscriptstyle L},[b_{\scriptscriptstyle
L}/x_{\scriptscriptstyle L}]Q),\text{unavail}(b_{\scriptscriptstyle S})$

Then $\Lambda=\Lambda_{b},\Lambda_{1}$ and
$\Theta=\Theta_{1},\Psi_{a},\Theta_{2}$ with
$\Lambda_{b}=\text{proc}(b_{\scriptscriptstyle S},x_{\scriptscriptstyle
L}\leftarrow\text{acc}_{\scriptscriptstyle S}\;b_{\scriptscriptstyle S};Q)$.
We also define $\Psi_{b}^{\prime}=\text{proc}(b_{\scriptscriptstyle
L},[b_{\scriptscriptstyle L}/x_{\scriptscriptstyle L}]Q)$.

$\displaystyle{\Gamma\models\Lambda_{b},\Lambda_{1};\Theta_{1},\Psi_{a},\Theta_{2}::(\Gamma;\Delta)}$
(assumption)
$\displaystyle{\Gamma\models\Lambda_{b},\Lambda_{1}::(\Gamma)}\quad{\Gamma\models\Theta_{1},\Psi_{a},\Theta_{2}::(\Delta)}$
(by inversion on $\Omega$)
$\displaystyle{\Gamma\models\Lambda_{b}::(b_{\scriptscriptstyle
S}{:}{\uparrow_{L}^{S}}B_{\scriptscriptstyle
L})}\quad{\Gamma\models\Lambda_{1}::(\Gamma^{\prime})}$ (by inversion on
$\Lambda 2$ with $\Gamma=b_{\scriptscriptstyle
S}{:}{\uparrow_{L}^{S}}B_{\scriptscriptstyle L},\Gamma^{\prime}$)
$\displaystyle\vdash({\uparrow_{L}^{S}}B^{\prime}_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}B_{\scriptscriptstyle
L},\top)\;\text{ssync}\quad{\Gamma\vdash x_{\scriptscriptstyle
L}\leftarrow\text{acc}_{\scriptscriptstyle S}\;b_{\scriptscriptstyle
S};Q::(b_{\scriptscriptstyle
S}{:}{\uparrow_{L}^{S}}B^{\prime}_{\scriptscriptstyle L})}$ (by inversion on
$\Lambda 3$) $\displaystyle{\Gamma;\cdot\vdash[b_{\scriptscriptstyle
L}/x_{\scriptscriptstyle L}]Q::(b_{\scriptscriptstyle
L}{:}B^{\prime}_{\scriptscriptstyle L})}$ (by inversion on
${\uparrow_{L}^{S}}R$ and $\alpha$ equivalence)
$\displaystyle\vdash(B^{\prime}_{\scriptscriptstyle L},B_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}B^{\prime}_{\scriptscriptstyle L})\;\text{ssync}$ (by
inversion on $D{\uparrow_{L}^{S}}$)
$\displaystyle{\Gamma\models\Psi_{a},\Theta_{2}::(a_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L},\Delta_{p})}$ (by Lemma 4)
$\displaystyle{\Gamma\models\Theta_{2}::(\Delta_{a},\Delta_{p})}\quad{\Gamma;\Delta_{a}\vdash
x_{\scriptscriptstyle L}\leftarrow\text{acq}_{\scriptscriptstyle
S}\;b_{\scriptscriptstyle S}::(a_{\scriptscriptstyle
L}{:}A^{\prime}_{\scriptscriptstyle L})}$ $\displaystyle a_{\scriptscriptstyle
S}{:}\hat{A}\in\Gamma\quad\vdash(A^{\prime}_{\scriptscriptstyle
L},A_{\scriptscriptstyle L},\hat{A})\;\text{ssync}$ (by inversion on $\Theta
3$) $\displaystyle{\Gamma;\Delta_{a},b_{\scriptscriptstyle
L}{:}B^{a}_{\scriptscriptstyle L}\vdash[b_{\scriptscriptstyle
L}/x_{\scriptscriptstyle L}]P::(a_{\scriptscriptstyle
L}{:}A^{\prime}_{\scriptscriptstyle
L})}\quad{\uparrow_{L}^{S}}B_{\scriptscriptstyle
L}\leq{\uparrow_{L}^{S}}B^{a}_{\scriptscriptstyle L}$ (by inversion on
${\uparrow_{L}^{S}}L$ and $\alpha$ equivalence)
$\displaystyle{\Gamma\models\Psi_{b}^{\prime},\Theta_{2}::(b_{\scriptscriptstyle
L}{:}B_{\scriptscriptstyle L},\Delta_{a},\Delta_{p})}$ (by $\Lambda 3$)
$\displaystyle{\Gamma\models\Psi_{b}^{\prime},\Theta_{2}::(b_{\scriptscriptstyle
L}{:}B^{a}_{\scriptscriptstyle L},\Delta_{a},\Delta_{p})}$ (by Lemma 8)
$\displaystyle{\Gamma\models\Psi_{a}^{\prime},\Psi_{b}^{\prime},\Theta_{2}::(a_{\scriptscriptstyle
L}{:}A,\Delta_{p})}$ (by $\Theta 3$)
$\displaystyle{\Gamma\models\Theta_{1},\Psi_{a}^{\prime},\Psi_{b}^{\prime},\Theta_{2}::(\Delta)}$
(by Lemma 7) $\displaystyle{\Gamma\models\text{unavail}(b_{\scriptscriptstyle
S})::(b_{\scriptscriptstyle S}{:}{\uparrow_{L}^{S}}B_{\scriptscriptstyle L})}$
(by $\Lambda 4$)
$\displaystyle{\Gamma\models\text{unavail}(b_{\scriptscriptstyle
S}),\Lambda_{1}::(\Gamma)}$ (by $\Lambda 2$)
$\displaystyle{\Gamma\models\Lambda;\Theta_{1},\Psi_{a}^{\prime},\Psi_{b}^{\prime},\Theta_{2}::(\Gamma;\Delta)}$
(by $\Omega$)

Well-formedness is maintained because $\Psi_{b}\notin\Theta$ and there is a
corresponding $\text{unavail}(b_{\scriptscriptstyle S})$ to the newly added
$\Psi_{b}^{\prime}$.

######  Case 7.

D-${\uparrow_{L}^{S}}$2

$\displaystyle\text{proc}(a_{\scriptscriptstyle L},x_{\scriptscriptstyle
L}\leftarrow\text{acq}_{\scriptscriptstyle L}\;b_{\scriptscriptstyle
L};P),\text{connect}(b_{\scriptscriptstyle L},c_{\scriptscriptstyle
S}),\text{proc}(c_{\scriptscriptstyle S},x_{\scriptscriptstyle
L}\leftarrow\text{acc}_{\scriptscriptstyle S}\;c_{\scriptscriptstyle S};Q)$
$\displaystyle\to\quad$ $\displaystyle\text{proc}(a_{\scriptscriptstyle
L},[c_{\scriptscriptstyle L}/x_{\scriptscriptstyle
L}]P),\text{proc}(c_{\scriptscriptstyle L},[c_{\scriptscriptstyle
L}/x_{\scriptscriptstyle L}]Q),\text{unavail}(c_{\scriptscriptstyle S})$

Then $\Lambda=\Lambda_{c},\Lambda_{1}$ and
$\Theta=\Theta_{1},\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3}$ with
$\Lambda_{c}=\text{proc}(c_{\scriptscriptstyle S},x_{\scriptscriptstyle
L}\leftarrow\text{acc}_{\scriptscriptstyle S}\;c_{\scriptscriptstyle S};Q)$.
We also define $\Psi_{c}^{\prime}=\text{proc}(c_{\scriptscriptstyle
L},[c_{\scriptscriptstyle L}/x_{\scriptscriptstyle L}]Q)$.

$\displaystyle{\Gamma\models\Lambda_{c},\Lambda_{1};\Theta_{1},\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3}::(\Gamma;\Delta)}$
(assumption)
$\displaystyle{\Gamma\models\Lambda_{c},\Lambda_{1}::(\Gamma)}\quad{\Gamma\models\Theta_{1},\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3}::(\Delta)}$
(by inversion on $\Omega$)
$\displaystyle{\Gamma\models\Lambda_{c}::(c_{\scriptscriptstyle
S}{:}{\uparrow_{L}^{S}}C_{\scriptscriptstyle
L})}\quad{\Gamma\models\Lambda_{1}::(\Gamma^{\prime})}$ (by inversion on
$\Lambda 2$ with $\Gamma=c_{\scriptscriptstyle
S}{:}{\uparrow_{L}^{S}}C_{\scriptscriptstyle L},\Gamma^{\prime}$)
$\displaystyle\vdash({\uparrow_{L}^{S}}C^{\prime}_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}C_{\scriptscriptstyle
L},\top)\;\text{ssync}\quad{\Gamma\vdash x_{\scriptscriptstyle
L}\leftarrow\text{acc}_{\scriptscriptstyle S}\;c_{\scriptscriptstyle
S};Q::(c_{\scriptscriptstyle
S}{:}{\uparrow_{L}^{S}}C^{\prime}_{\scriptscriptstyle L})}$ (by inversion on
$\Lambda 3$) $\displaystyle{\Gamma;\cdot\vdash[c_{\scriptscriptstyle
L}/x_{\scriptscriptstyle L}]Q::(c_{\scriptscriptstyle
L}{:}C^{\prime}_{\scriptscriptstyle L})}$ (by inversion on
${\uparrow_{L}^{S}}R$ and $\alpha$ equivalence)
$\displaystyle\vdash(C^{\prime}_{\scriptscriptstyle L},C_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}C^{\prime}_{\scriptscriptstyle L})\;\text{ssync}$ (by
inversion on $D{\uparrow_{L}^{S}}$)
$\displaystyle{\Gamma\models\Psi_{a},\Theta_{2},\Psi_{b},\Theta_{3}::(a_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L},\Delta_{p})}$ (by Lemma 4)
$\displaystyle{\Gamma\models\Psi_{a},\Psi_{b},\Theta_{r}::(a_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L},\Delta_{p})}$ (by Lemma 6 with
$\Theta_{r}=\Theta_{2},\Theta_{3}$)
$\displaystyle{\Gamma\models\text{connect}(b_{\scriptscriptstyle
L},c_{\scriptscriptstyle S}),\Theta_{2}::(b_{\scriptscriptstyle
S}{:}{\uparrow_{L}^{L}}B_{\scriptscriptstyle
L},\Delta_{a},\Delta_{p})}\quad{\Gamma;\Delta_{a},b_{\scriptscriptstyle
S}{:}{\uparrow_{L}^{L}}B_{\scriptscriptstyle L}\vdash x_{\scriptscriptstyle
L}\leftarrow\text{acq}_{\scriptscriptstyle L}\;b_{\scriptscriptstyle
L}::(a_{\scriptscriptstyle L}{:}A^{\prime}_{\scriptscriptstyle L})}$
$\displaystyle a_{\scriptscriptstyle
S}{:}\hat{A}\in\Gamma\quad\vdash(A^{\prime}_{\scriptscriptstyle
L},A_{\scriptscriptstyle L},\hat{A})\;\text{ssync}$ (by inversion on $\Theta
3$)
$\displaystyle{\Gamma\models\Theta_{r}::(\Delta_{a},\Delta_{p})}\quad{\uparrow_{L}^{S}}C_{\scriptscriptstyle
L}\leq{\uparrow_{L}^{L}}B_{\scriptscriptstyle L}$ (by inversion on $\Theta 2$)
$\displaystyle C_{\scriptscriptstyle L}\leq B_{\scriptscriptstyle
L}\quad\vdash(C^{\prime}_{\scriptscriptstyle L},B_{\scriptscriptstyle
L},{\uparrow_{L}^{S}}C^{\prime}_{\scriptscriptstyle L})\;\text{ssync}$ (by
inversion on $\leq_{{\uparrow_{L}^{S}}{\uparrow_{L}^{L}}}$ and Lemma 11
respectively)
$\displaystyle{\Gamma\models\Psi_{c}^{\prime},\Theta_{r}::(c_{\scriptscriptstyle
L}{:}C_{\scriptscriptstyle L},\Delta_{a},\Delta_{p})}$ (by $\Lambda 3$)
$\displaystyle{\Gamma;\Delta_{a},c_{\scriptscriptstyle
L}{:}C_{\scriptscriptstyle L}\vdash[c_{\scriptscriptstyle
L}/x_{\scriptscriptstyle L}]P::(a_{\scriptscriptstyle
L}{:}A^{\prime}_{\scriptscriptstyle L})}$ (by inversion on
${\uparrow_{L}^{S}}L$ and $\alpha$ equivalence)
$\displaystyle{\Gamma\models\Psi_{a}^{\prime},\Psi_{c}^{\prime},\Theta_{2}::(a_{\scriptscriptstyle
L}{:}A,\Delta_{p})}$ (by $\Theta 3$)
$\displaystyle{\Gamma\models\Theta_{1},\Psi_{a}^{\prime},\Psi_{b}^{\prime},\Theta_{2}::(\Delta)}$
(by Lemma 7) $\displaystyle{\Gamma\models\text{unavail}(c_{\scriptscriptstyle
S})::(c_{\scriptscriptstyle S}{:}{\uparrow_{L}^{S}}C_{\scriptscriptstyle L})}$
(by $\Lambda 4$)
$\displaystyle{\Gamma\models\text{unavail}(c_{\scriptscriptstyle
S}),\Lambda_{1}::(\Gamma)}$ (by $\Lambda 2$)
$\displaystyle{\Gamma\models\Lambda;\Theta_{1},\Psi_{a}^{\prime},\Psi_{c}^{\prime},\Theta_{2}::(\Gamma;\Delta)}$
(by $\Omega$)

Well-formedness is maintained because $\Psi_{c}\notin\Theta$ and there is a
corresponding $\text{unavail}(c_{\scriptscriptstyle S})$ to the newly added
$\Psi_{c}^{\prime}$.

Other omitted cases follow a similar strategy as presented.

##  Appendix D Progress Theorem

######  Theorem 31 (Progress).

If ${\Gamma\models\Lambda;\Theta::(\Gamma;\Delta)}$ then either:

  1. (1)

$\Lambda;\Theta\rightarrow\Lambda^{\prime};\Theta$ for some $\Lambda^{\prime}$
or

  2. (2)

$\Lambda$ is poised and one of:

    1. (a)

$\Lambda;\Theta\rightarrow\Lambda^{\prime};\Theta^{\prime}$ or

    2. (b)

$\Theta$ is poised or

    3. (c)

a linear process in $\Theta$ is stuck and therefore unable to acquire

######  Proof D.1.

$\displaystyle{\Gamma\models\Lambda;\Theta::(\Gamma;\Delta)}$ (by assumption)
$\displaystyle{\Gamma\models\Lambda::(\Gamma)}\quad{\Gamma\models\Theta::(\Delta)}$
(by inversion on $\Omega$)

for some $\Gamma,\Lambda,\Theta,$ and $\Delta$.

We first show that either $\Lambda\to\Lambda^{\prime}$ for some
$\Lambda^{\prime}$ or that $\Lambda$ is poised by induction on the derivation
of ${\Gamma\models\Lambda::(\Gamma)}$.

######  Case 1.

${\Gamma\models\cdot::(\cdot)}$

$(\cdot)$ is poised since there is no proc term.

######  Case 2.

${\Gamma\models\Lambda_{1},\Lambda_{2}::(\Gamma_{1},\Gamma_{2})}\lx@proof@logical@and{\Gamma\models\Lambda_{1}::(\Gamma_{1})}{\Gamma\models\Lambda_{2}::(\Gamma_{2})}$

Then either $\Lambda_{1}\to\Lambda_{1}^{\prime}$ or $\Lambda_{1}$ is poised by
IH, and similarly, either $\Lambda_{2}\to\Lambda_{2}^{\prime}$ or
$\Lambda_{2}$ is poised by IH. If both $\Lambda_{1}$ and $\Lambda_{2}$ are
poised, then the concatenation $\Lambda_{1},\Lambda_{2}$ is poised. Otherwise,
we take the concatenation of the components that progresses. In particular, if
$\Lambda_{1}\to\Lambda_{1}^{\prime}$ and $\Lambda_{2}$ is poised,
$\Lambda_{1},\Lambda_{2}\to\Lambda_{1}^{\prime},\Lambda_{2}$ (and similarly
for the other two combinations).

######  Case 3.

${\Gamma\models\text{proc}(a_{\scriptscriptstyle S},P)::(a_{\scriptscriptstyle
S}{:}A_{\scriptscriptstyle
S})}\lx@proof@logical@and\vdash(A^{\prime}_{\scriptscriptstyle
S},A_{\scriptscriptstyle S},\top)\;\text{ssync}{\Gamma\vdash
P::(a_{\scriptscriptstyle S}{:}A^{\prime}_{\scriptscriptstyle S})}$

We proceed by case analysis on the syntactic form of $P$ inferred from
inversion on the appropriate typing rule on the derivation of ${\Gamma\vdash
P::(a_{\scriptscriptstyle S}{:}A^{\prime}_{\scriptscriptstyle S})}$.

######  Subcase 1.

$P=\text{fwd}\;a_{\scriptscriptstyle S}\ b_{\scriptscriptstyle S}$. This case
requires a global substitution on the top level $\Lambda$. Since there is no
ordering constraint on $\Lambda$, let
$\Lambda=\text{proc}(a_{\scriptscriptstyle
S},\text{fwd}\;a_{\scriptscriptstyle S}\ b_{\scriptscriptstyle
S}),\Lambda_{1}$ without loss of generality. Then by D-FWDSS,

$\Lambda\to[a_{\scriptscriptstyle S}/b_{\scriptscriptstyle S}]\Lambda_{1}$

######  Subcase 2.

${P=x_{\scriptscriptstyle S}\leftarrow X_{\scriptscriptstyle
S}\leftarrow\overline{b_{\scriptscriptstyle S}};Q}$, then by D-SPAWNSS,

$\text{proc}(a_{\scriptscriptstyle S},x_{\scriptscriptstyle S}\leftarrow
X_{\scriptscriptstyle S}\leftarrow\overline{b_{\scriptscriptstyle
S}};Q)\to\text{proc}(a_{\scriptscriptstyle S},[c_{\scriptscriptstyle
S}/x_{\scriptscriptstyle S}]Q),\text{proc}(c_{\scriptscriptstyle
S},[c_{\scriptscriptstyle S}/x^{\prime}_{\scriptscriptstyle
S},\overline{b_{\scriptscriptstyle
S}}/\overline{y^{\prime}_{\scriptscriptstyle S}}]P)\quad(c\;\;\text{fresh})$

######  Subcase 3.

${P=a_{\scriptscriptstyle L}\leftarrow\text{acc}_{\scriptscriptstyle
S}\;a_{\scriptscriptstyle S};Q}$, then $\text{proc}(a_{\scriptscriptstyle
S},P)$ is poised by definition.

######  Case 4.

${\Gamma\models\text{unavail}(a_{\scriptscriptstyle
S})::(a_{\scriptscriptstyle S}{:}\hat{A})}$

$\text{unavail}(a_{\scriptscriptstyle S})$ is poised since there is no proc
term.

That concludes the first part of the proof. Now to show the second part, we
will assume that $\Lambda$ is poised and proceed by induction on the
derivation of ${\Gamma\models\Theta::(\Delta)}$ to show one of:

  1. (a)

$\Lambda;\Theta\to\Lambda^{\prime};\Theta^{\prime}$ for some
$\Lambda^{\prime}$ and $\Theta^{\prime}$

  2. (b)

$\Theta$ poised

  3. (c)

some $\Psi\in\Theta$ is stuck

We will showcase the style of the proof along with the interesting cases.

######  Case 1.

${\Gamma\models\cdot::(\cdot)}$

$(\cdot)$ is poised since there is no proc term.

######  Case 2.

${\Gamma\models\text{connect}(a_{\scriptscriptstyle L},b_{\scriptscriptstyle
S}),\Theta_{1}::(a:A_{\scriptscriptstyle L},\Delta_{1})}\lx@proof@logical@and
b_{\scriptscriptstyle S}{:}\hat{B}\in\Gamma b_{\scriptscriptstyle S}\leq
A_{\scriptscriptstyle L}{\Gamma\models\Theta_{1}::(\Delta_{1})}$

By the IH, $\Theta_{1}$ either steps, is poised, or contains a $\Psi$ that is
stuck.

If $\Theta_{1}$ steps, then
${\Lambda;\Theta_{1}\to\Lambda^{\prime};\Theta_{1}^{\prime}}$ for some
$\Lambda^{\prime}$ and $\Theta_{1}^{\prime}$. Then
${\Lambda;\text{connect}(a_{\scriptscriptstyle L},b_{\scriptscriptstyle
S}),\Theta_{1}\to\Lambda^{\prime};\text{connect}(a_{\scriptscriptstyle
L},b_{\scriptscriptstyle S}),\Theta_{1}^{\prime}}$

If $\Theta_{1}$ is poised, then $\text{connect}(a_{\scriptscriptstyle
L},b_{\scriptscriptstyle S}),\Theta_{1}$ is poised because
$\text{connect}(-_{\scriptscriptstyle L},-_{\scriptscriptstyle S})$ is not a
proc term.

Finally, if there is some $\Psi\in\Theta_{1}$ that is stuck, then course
${\Psi\in(\text{connect}(a_{\scriptscriptstyle L},b_{\scriptscriptstyle
S}),\Theta_{1})}$ is stuck.

######  Case 3.

${\Gamma\models\text{proc}(c_{\scriptscriptstyle
L},P),\Theta_{1}::(c:C_{\scriptscriptstyle
L},\Delta_{1})}\lx@proof@logical@and c_{\scriptscriptstyle
S}{:}\hat{C}\in\Gamma\vdash(C^{\prime}_{\scriptscriptstyle
L},C_{\scriptscriptstyle L},\hat{C})\;\text{ssync}{\Gamma;\Delta_{c}\vdash
P::(c_{\scriptscriptstyle L}{:}C^{\prime}_{\scriptscriptstyle
L})}{\Gamma\models\Theta_{1}::(\Delta_{c},\Delta_{1})}$

By the IH, $\Theta_{1}$ either steps, is poised, or contains a $\Psi$ that is
stuck. We first cover two of the cases:

If $\Theta_{1}$ steps, then
${\Lambda;\Theta_{1}\to\Lambda^{\prime};\Theta_{1}^{\prime}}$ for some
$\Lambda^{\prime}$ and $\Theta_{1}^{\prime}$. Then
${\Lambda;\text{proc}(c_{\scriptscriptstyle
L},P),\Theta_{1}\to\Lambda^{\prime};\text{proc}(c_{\scriptscriptstyle
L},P),\Theta_{1}^{\prime}}$.

If there is some $\Psi\in\Theta_{1}$ that is stuck, then of course the same
${\Psi\in(\text{proc}(c_{\scriptscriptstyle L},P),\Theta_{1})}$ is stuck.

For the final case, we will assume that $\Theta_{1}$ is poised and proceed by
case analysis on the derivation of ${\Gamma;\Delta_{c}\vdash
P::(c_{\scriptscriptstyle L}{:}C^{\prime}_{\scriptscriptstyle L})}$. Unlike in
the first part, we make the step between identifying the appropriate typing
rule and inferring the form of $P$ explicit because some of the cases are more
complicated. In the typing judgment, we replace instantiated channel variables
in the context such as $x$ by actual channel names since they must already
exist in the configuration.

######  Subcase 1.

The form of $P$ inferred from all linear right rules
$(1R,{\otimes}R,{\otimes}R_{\scriptscriptstyle
S},{\multimap}R,{\oplus}R,{\&}R,\\\ {\uparrow_{L}^{L}}R,$ and
${\downarrow_{L}^{L}}R)$ directly coincide with the definition of poised. For
example, $1R$ implies that $P=\text{close}\;a_{\scriptscriptstyle L}$, which
is poised, and so on. Since $\Theta_{1}$ is poised,
$\text{proc}(a_{\scriptscriptstyle L},P),\Theta_{1}$ is poised.

######  Subcase 2.

${\Gamma;\Delta_{c}^{\prime},b_{\scriptscriptstyle L}{:}A_{\scriptscriptstyle
L}\otimes B_{\scriptscriptstyle L}\vdash y_{\scriptscriptstyle
L}\leftarrow\text{recv}\;b_{\scriptscriptstyle L};P::(c_{\scriptscriptstyle
L}{:}C^{\prime}_{\scriptscriptstyle
L})}{\Gamma;\Delta_{c}^{\prime},b_{\scriptscriptstyle
L}{:}B_{\scriptscriptstyle L},y_{\scriptscriptstyle L}{:}A_{\scriptscriptstyle
L}\vdash P::(c_{\scriptscriptstyle L}{:}C^{\prime}_{\scriptscriptstyle L})}$

where $\Delta_{c}=\Delta_{c}^{\prime},b_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L}\otimes B_{\scriptscriptstyle L}$. Then
$\Theta_{1}=\Theta_{2},\text{proc}(b_{\scriptscriptstyle L},-),\Theta_{3}$ for
some $\Theta_{2}$ and $\Theta_{3}$ (we know $b_{\scriptscriptstyle L}$ is not
provided by a connect term since connect terms offer channels of type
${\uparrow_{L}^{L}}D_{\scriptscriptstyle L}$). Since
$\text{proc}(b_{\scriptscriptstyle L},-)$ is poised and must offer a channel
of type $A_{\scriptscriptstyle L}\otimes B_{\scriptscriptstyle L}$, it must be
of form $\text{proc}(b_{\scriptscriptstyle
L},\text{send}\;b_{\scriptscriptstyle L}\ a_{\scriptscriptstyle L};Q)$. Thus,
by D-$\otimes$,

$\displaystyle\Lambda;\begin{subarray}{c}\text{proc}(c_{\scriptscriptstyle
L},y_{\scriptscriptstyle L}\leftarrow\text{recv}\;b_{\scriptscriptstyle
L};P),\Theta_{2},\\\ \text{proc}(b_{\scriptscriptstyle
L},\text{send}\;b_{\scriptscriptstyle L}\ a_{\scriptscriptstyle
L};Q),\Theta_{3}\end{subarray}\to\Lambda;\begin{subarray}{c}\text{proc}(c_{\scriptscriptstyle
L},[a_{\scriptscriptstyle L}/y_{\scriptscriptstyle L}]P),\Theta_{2},\\\
\text{proc}(b_{\scriptscriptstyle L},Q),\Theta_{3}\end{subarray}$

All the remaining linear left rules except ${\uparrow_{L}^{L}}L$ and
${\uparrow_{L}^{L}}R$ $(1L,{\multimap}L,{\multimap}L_{\scriptscriptstyle
S},{\oplus}L,{\&}L)$ follow a similar pattern.

######  Subcase 3.

${\Gamma,a_{\scriptscriptstyle S}{:}\hat{A};\Delta_{c}\vdash
x_{\scriptscriptstyle L}\leftarrow\text{acq}_{\scriptscriptstyle
S}\;a_{\scriptscriptstyle S};P::(c_{\scriptscriptstyle
L}{:}C^{\prime}_{\scriptscriptstyle
L})}\lx@proof@logical@and\hat{A}\leq{\uparrow_{L}^{S}}A_{\scriptscriptstyle
L}{\Gamma,a_{\scriptscriptstyle S}{:}\hat{A};\Delta,x_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L}\vdash P::(c_{\scriptscriptstyle
L}{:}C^{\prime}_{\scriptscriptstyle L})}$

Since $\Lambda$ is poised, either
${\Lambda=\text{unavail}(a_{\scriptscriptstyle S}),\Lambda_{1}}$ or
${\Lambda=\text{proc}(a_{\scriptscriptstyle S},x_{\scriptscriptstyle
L}\leftarrow\text{acc}_{\scriptscriptstyle S}\;a_{\scriptscriptstyle
S};Q),\Lambda_{1}}$ for some $\Lambda_{1}$. In the first case,
$\text{proc}(c_{\scriptscriptstyle L},a_{\scriptscriptstyle
L}\leftarrow\text{acq}_{\scriptscriptstyle S}\;a_{\scriptscriptstyle S};P)$ is
stuck, so we are done. In the second case, by D-${\uparrow_{L}^{S}}$, we have

$\displaystyle\text{proc}(a_{\scriptscriptstyle S},x_{\scriptscriptstyle
L}\leftarrow\text{acc}_{\scriptscriptstyle S}\;a_{\scriptscriptstyle
S};Q),\Lambda_{1};\text{proc}(c_{\scriptscriptstyle L},a_{\scriptscriptstyle
L}\leftarrow\text{acq}_{\scriptscriptstyle S}\;a_{\scriptscriptstyle
S};P),\Theta_{1}$ $\displaystyle\to\quad$
$\displaystyle\text{unavail}(a_{\scriptscriptstyle
S}),\Lambda_{1};\text{proc}(c_{\scriptscriptstyle L},[a_{\scriptscriptstyle
L}/x_{\scriptscriptstyle L}]P),\text{proc}(a_{\scriptscriptstyle
L},[a_{\scriptscriptstyle L}/x_{\scriptscriptstyle L}]Q),\Theta_{1}$

######  Subcase 4.

${\Gamma;\Delta_{c}^{\prime},a_{\scriptscriptstyle
L}{:}{\downarrow_{L}^{S}}A_{\scriptscriptstyle S}\vdash x_{\scriptscriptstyle
S}\leftarrow\text{rel}_{\scriptscriptstyle S}\;a_{\scriptscriptstyle
S};P::(c_{\scriptscriptstyle L}{:}C^{\prime}_{\scriptscriptstyle
L})}{\Gamma,x_{\scriptscriptstyle S}{:}A_{\scriptscriptstyle
S};\Delta_{c}^{\prime}\vdash P::(c_{\scriptscriptstyle
L}{:}C^{\prime}_{\scriptscriptstyle L})}$

where $\Delta_{c}=\Delta_{c}^{\prime},a_{\scriptscriptstyle
L}{:}{\downarrow_{L}^{S}}A_{\scriptscriptstyle S}$. Then
$\Theta_{1}=\Theta_{2},\text{proc}(a_{\scriptscriptstyle L},-),\Theta_{3}$ for
some $\Theta_{2}$ and $\Theta_{3}$. Since there is a
$\text{proc}(a_{\scriptscriptstyle L},-)$ in the linear configuration, by
well-formedness condition, there must be a corresponding
$\text{unavail}(a_{\scriptscriptstyle S})\in\Lambda$, so
$\Lambda=\text{unavail}(a_{\scriptscriptstyle S}),\Lambda_{1}$. Furthermore,
since $\Theta_{1}$ is poised, the proc term must be of form
$\text{proc}(a_{\scriptscriptstyle L},x_{\scriptscriptstyle
S}\leftarrow\text{det}_{\scriptscriptstyle S}\;a_{\scriptscriptstyle S};Q)$.
By D-${\downarrow_{L}^{S}}$, we have

$\displaystyle\text{unavail}(a_{\scriptscriptstyle
S}),\Lambda_{1};\text{proc}(c_{\scriptscriptstyle L},x_{\scriptscriptstyle
S}\leftarrow\text{rel}_{\scriptscriptstyle S}\;a_{\scriptscriptstyle
S};P),\Theta_{2},\text{proc}(a_{\scriptscriptstyle L},x_{\scriptscriptstyle
S}\leftarrow\text{det}_{\scriptscriptstyle S}\;a_{\scriptscriptstyle
S};Q),\Theta_{3}$ $\displaystyle\to\quad$
$\displaystyle\text{proc}(a_{\scriptscriptstyle S},[a_{\scriptscriptstyle
S}/x_{\scriptscriptstyle S}]Q),\Lambda_{1};\text{proc}(c_{\scriptscriptstyle
L},[a_{\scriptscriptstyle L}/x_{\scriptscriptstyle
L}]P),\Theta_{2},\Theta_{3}$

######  Subcase 5.

${\Gamma;\Delta_{c}^{\prime},a_{\scriptscriptstyle
L}{:}{\uparrow_{L}^{L}}A_{\scriptscriptstyle L}\vdash x_{\scriptscriptstyle
L}\leftarrow\text{acq}_{\scriptscriptstyle L}\;a_{\scriptscriptstyle
L};P::(c_{\scriptscriptstyle L}{:}C^{\prime}_{\scriptscriptstyle
L})}{\Gamma;\Delta_{c}^{\prime},x_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L}\vdash P::(c_{\scriptscriptstyle
L}{:}C^{\prime}_{\scriptscriptstyle L})}$

where $\Delta_{c}=\Delta_{c}^{\prime},a_{\scriptscriptstyle
L}{:}{\uparrow_{L}^{L}}A_{\scriptscriptstyle L}$. Then
$\Theta_{1}=\Theta_{2},\Psi_{a},\Theta_{3}$ where $\Psi_{a}$ is either of form
$\text{connect}(a_{\scriptscriptstyle L},b_{\scriptscriptstyle S})$ for some
$b_{\scriptscriptstyle S}$ or $\text{proc}(a_{\scriptscriptstyle L},-)$. In
the latter case, we appeal to the term being poised and the proof proceeds
like the other left rules. In the former case, there must be a term in
$\Lambda$ that provides $b_{\scriptscriptstyle S}$. Since $\Lambda$ is poised,
either ${\Lambda=\text{unavail}(b_{\scriptscriptstyle S}),\Lambda_{1}}$ or
${\Lambda=\text{proc}(b_{\scriptscriptstyle S},x_{\scriptscriptstyle
L}\leftarrow\text{acc}_{\scriptscriptstyle S}\;b_{\scriptscriptstyle
S};Q),\Lambda_{1}}$. In the former case, we can conclude that
$\text{proc}(c_{\scriptscriptstyle L},-)$ is stuck, so we are done. In the
latter case, by D-${\uparrow_{L}^{S}}$2, we have

$\displaystyle\text{proc}(b_{\scriptscriptstyle S},x_{\scriptscriptstyle
L}\leftarrow\text{acc}_{\scriptscriptstyle S}\;b_{\scriptscriptstyle
S};Q),\Lambda_{1};\text{proc}(c_{\scriptscriptstyle L},x_{\scriptscriptstyle
L}\leftarrow\text{acq}_{\scriptscriptstyle L}\;a_{\scriptscriptstyle
L};P),\Theta_{2},\text{connect}(a_{\scriptscriptstyle L},b_{\scriptscriptstyle
S}),\Theta_{3}$ $\displaystyle\to\quad$
$\displaystyle\text{unavail}(b_{\scriptscriptstyle
S}),\Lambda_{1};\text{proc}(c_{\scriptscriptstyle L},[b_{\scriptscriptstyle
L}/x_{\scriptscriptstyle L}]P),\text{proc}(b_{\scriptscriptstyle
L},[b_{\scriptscriptstyle L}/x_{\scriptscriptstyle
L}]Q),\Theta_{2},\Theta_{3}$

######  Subcase 6.

${\Gamma;\Delta_{c}^{\prime},a_{\scriptscriptstyle
L}{:}{\downarrow_{L}^{L}}A_{\scriptscriptstyle L}\vdash x_{\scriptscriptstyle
L}\leftarrow\text{rel}_{\scriptscriptstyle L}\;a_{\scriptscriptstyle
L};P::(c_{\scriptscriptstyle L}{:}C^{\prime}_{\scriptscriptstyle
L})}{\Gamma;\Delta_{c}^{\prime},x_{\scriptscriptstyle
L}{:}A_{\scriptscriptstyle L}\vdash P::(c_{\scriptscriptstyle
L}{:}C^{\prime}_{\scriptscriptstyle L})}$

where $\Delta_{c}=\Delta_{c}^{\prime},a_{\scriptscriptstyle
L}{:}{\downarrow_{L}^{L}}A_{\scriptscriptstyle L}$. Then
$\Theta_{1}=\Theta_{2},\text{proc}(a_{\scriptscriptstyle L},-),\Theta_{3}$.
Since $\Theta_{1}$ is poised, there are two possible forms of
$\text{proc}(a_{\scriptscriptstyle L},-)$. If we have
$\text{proc}(a_{\scriptscriptstyle L},x_{\scriptscriptstyle
L}\leftarrow\text{det}_{\scriptscriptstyle L}\;a_{\scriptscriptstyle L};Q)$,
then we appeal to the term being poised like the other left rules. If we
instead have $\text{proc}(a_{\scriptscriptstyle L},x_{\scriptscriptstyle
S}\leftarrow\text{det}_{\scriptscriptstyle S}\;a_{\scriptscriptstyle S};Q)$,
then we first identify that $\Lambda=\text{unavail}(a_{\scriptscriptstyle
S}),\Lambda_{1}$ for some $\Lambda_{1}$ by the well-formedness condition. By
D-${\downarrow_{L}^{S}}$2, we have

$\displaystyle\text{unavail}(a_{\scriptscriptstyle
S}),\Lambda_{1};\text{proc}(c_{\scriptscriptstyle L},x_{\scriptscriptstyle
L}\leftarrow\text{rel}_{\scriptscriptstyle L}\;a_{\scriptscriptstyle
L};P),\Theta_{2},\text{proc}(a_{\scriptscriptstyle L},x_{\scriptscriptstyle
S}\leftarrow\text{det}_{\scriptscriptstyle S}\;a_{\scriptscriptstyle
S};Q),\Theta_{3}$ $\displaystyle\to\quad$
$\displaystyle\text{proc}(a_{\scriptscriptstyle S},[a_{\scriptscriptstyle
S}/x_{\scriptscriptstyle S}]Q),\Lambda_{1};\text{proc}(c_{\scriptscriptstyle
L},[b_{\scriptscriptstyle L}/x_{\scriptscriptstyle
L}]P),\text{connect}(b_{\scriptscriptstyle L},a_{\scriptscriptstyle
S}),\Theta_{2},\Theta_{3}\quad(b\;\;\text{fresh})$