the identity ${\tt I}$ becomes persistent on the right-hand side, a phenomenon
which is naturally captured by the tight type $\mathtt{vl}$. This observation
also applies to the tight typing system of CBPV in Sec. 6.

######  Theorem 4.15 (Soundness).

If
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
is tight, then there exists $p$ such that $p\in\mathsf{no}_{\mathtt{v}}$ and
$t\twoheadrightarrow_{\mathtt{v}}^{(\mathit{m},\mathit{e})}p$ with
$\mathit{m}$ $\mathtt{m}$-steps, $\mathit{e}$ $\mathtt{e}$-steps, and
$|{p}|_{\mathtt{v}}=\mathit{s}$.

######  Proof 4.16.

We prove the statement for $\rightarrow_{\mathtt{dv}}$ and then conclude for
the general notion of reduction $\rightarrow_{\mathtt{v}}$ by the observation
that all reduction sequences to normal form have the same number of
multiplicative and exponential steps. Let
${\Phi}\rhd_{\mathcal{B}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$.
We proceed by induction on $\mathit{m}+\mathit{e}$:

  * •

If $\mathit{m}+\mathit{e}=0$, then $\mathit{m}=\mathit{e}=0$ and Lem. 4.5
gives $t\in\mathsf{no}_{\mathtt{v}}$. Moreover, by Lem. 4.7 we get
$|{t}|_{\mathtt{v}}=\mathit{s}$. Thus, we conclude with $p=t$.

  * •

If $\mathit{m}+\mathit{e}>0$, then $t\notin\mathsf{no}_{\mathtt{v}}$ holds by
Lem. 4.5 and thus there exists $t^{\prime}$ such that
$t\twoheadrightarrow_{\mathtt{dv}}^{(1,0)}t^{\prime}$ or
$t\twoheadrightarrow_{\mathtt{dv}}^{(0,1)}t^{\prime}$ by Prop. 2.1. By Lem.
4.13 there exists a type derivation
${\Phi^{\prime}}\rhd_{\mathcal{B}}{{\Gamma}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}})}{{t^{\prime}}:{\sigma}}}$
such that $1+\mathit{m}^{\prime}+\mathit{e}^{\prime}=\mathit{m}+\mathit{e}$.
By the i.h. there exists $p\in\mathsf{no}_{\mathtt{v}}$ such that
$t^{\prime}\twoheadrightarrow_{\mathtt{dv}}^{(\mathit{m}^{\prime},\mathit{e}^{\prime})}p$
with $\mathit{s}=|{p}|_{\mathtt{v}}$. Then
$t\twoheadrightarrow_{\mathtt{dv}}^{(1,0)}t^{\prime}\twoheadrightarrow_{\mathtt{dv}}^{(\mathit{m}^{\prime},\mathit{e}^{\prime})}p$
or
$t\twoheadrightarrow_{\mathtt{dv}}^{(0,1)}t^{\prime}\twoheadrightarrow_{\mathtt{dv}}^{(\mathit{m}^{\prime},\mathit{e}^{\prime})}p$
which means $t\twoheadrightarrow_{\mathtt{dv}}^{(\mathit{m},\mathit{e})}p$, as
expected.

As in CBN, the previous theorem is stated by using the general notion of
reduction $\rightarrow_{\mathtt{v}}$, but the proofs (notably Lem. 4.13) are
done using the deterministic reduction $\rightarrow_{\mathtt{dv}}$. Similar
comment applies to the forthcoming Thm. 4.25.

Completeness. The completeness result is also based on intermediate lemmas,
most notably the so-called _tight typing of normal forms_ and _subject
expansion_ properties:

######  Lemma 4.17 (Tight Typing of Normal Forms).

If $t\in\mathsf{no}_{\mathtt{v}}$, then there is a tight derivation
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({0},{0},{|{t}|_{\mathtt{v}}})}{{t}:{\sigma}}}$.

######  Proof 4.18.

By simultaneous induction on the following claims:

  1. 1.

If $t\in\mathsf{vr}_{\mathtt{v}}$, then there exists a tight derivation
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({0},{0},{|{t}|_{\mathtt{v}}})}{{t}:{\mathtt{vr}}}}$.

  2. 2.

If $t\in\mathsf{vr}_{\mathtt{v}}$, then there exists a tight derivation
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({0},{0},{|{t}|_{\mathtt{v}}})}{{t}:{\mathtt{vl}}}}$.

  3. 3.

If $t\in\mathsf{ne}_{\mathtt{v}}$, then there exists a tight derivation
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({0},{0},{|{t}|_{\mathtt{v}}})}{{t}:{\mathtt{n}}}}$.

  4. 4.

If $t\in\mathsf{no}_{\mathtt{v}}$, then there exists a tight derivation
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({0},{0},{|{t}|_{\mathtt{v}}})}{{t}:{\mathtt{tt}}}}$.

  * •

$t=x$. Then, $t\in\mathsf{vr}_{\mathtt{v}}$ and we conclude (1) by
$\mathtt{({var_{p}})}$ or (2) by $\mathtt{({val_{p}})}$, since
$|{x}|_{\mathtt{v}}=0$ by definition.

  * •

$t={r}\,{u}$. Then, $t\in\mathsf{ne}_{\mathtt{v}}$ with
$r\in\mathsf{vr}_{\mathtt{v}}\cup\mathsf{ne}_{\mathtt{v}}$ and
$u\in\mathsf{no}_{\mathtt{v}}$. By i.h. (4) on $u$ we have
${\Phi_{u}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({0},{0},{|{u}|_{\mathtt{v}}})}{{u}:{\mathtt{tt}}}}$
with $\Delta$ tight. There are two options for $r$, namely
$r\in\mathsf{vr}_{\mathtt{v}}$ or $r\in\mathsf{ne}_{\mathtt{v}}$. By i.h. (1)
or (3) resp. there exists a tight derivation
${\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma^{\prime}}\vdash^{({0},{0},{|{t}|_{\mathtt{v}}})}{{r}:{\overline{\mathtt{vl}}}}}$.
We conclude (3) by $\mathtt{({app^{\mathcal{V}}_{p}})}$ with $\Phi_{r}$ and
$\Phi_{u}$, obtaining $\Gamma={\Gamma^{\prime}}\mathrel{+}{\Delta}$ and
$|{t}|_{\mathtt{v}}=|{r}|_{\mathtt{v}}+|{u}|_{\mathtt{v}}+1$ as expected.

  * •

$t=\lambda{x}.{r}$. Then, we conclude (4) by
$\mathtt{({abs^{\mathcal{V}}_{p}})}$ since $|{t}|_{\mathtt{v}}=0$ by
definition.

  * •

$t={r}[{x}\backslash{u}]$. Then, there are three cases to consider:
$t\in\mathsf{vr}_{\mathtt{v}}$, $t\in\mathsf{ne}_{\mathtt{v}}$ or
$t\in\mathsf{no}_{\mathtt{v}}$. In either of them we have
$u\in\mathsf{ne}_{\mathtt{v}}$. Thus, by i.h. (3) there exists a tight
derivation
${\Phi_{u}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({0},{0},{|{u}|_{\mathtt{v}}})}{{u}:{\mathtt{n}}}}$.
Moreover, in each case we get $r$ in the same set as $t$ by definition. By
applying the respective i.h. on $r$ we get a tight derivation
${\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma^{\prime}}\vdash^{({0},{0},{|{r}|_{\mathtt{v}}})}{{r}:{\sigma}}}$
with the appropiate type for each case. Finally, since $\Gamma^{\prime}$ tight
implies $\Gamma^{\prime}(x)$ tight, we conclude each respective claim by
$\mathtt{({es_{p}})}$ with
$\Gamma={{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\mathrel{+}{\Delta}$
tight and, hence,
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({0},{0},{|{r}|_{\mathtt{v}}+|{u}|_{\mathtt{v}}})}{{{r}[{x}\backslash{u}]}:{\sigma}}}$
tight as well. Note that
$|{t}|_{\mathtt{v}}=|{r}|_{\mathtt{v}}+|{u}|_{\mathtt{v}}$.

Analogously to the soundness case, we may obtain a single type derivation for
a value with multiset type from several ones, properly combining their
counters, and hence leading to an anti-subtitution result.

######  Lemma 4.19 (Merge type for value).

Let
$({{\Phi_{v}^{i}}\rhd_{\mathcal{V}}{{\Gamma_{i}}\vdash^{({\mathit{m}_{i}},{\mathit{e}_{i}},{\mathit{s}_{i}})}{{v}:{\mathcal{M}_{i}}}}})_{i\in
I}$. Then, there exists
${\Phi_{v}}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{v}:{\mathcal{M}}}}$.
such that $\Gamma={\\!}\mathrel{+_{i\in I}}{\Gamma_{i}}$,
$\mathcal{M}={\\!}\mathrel{+_{i\in I}}{\mathcal{M}_{i}}$, $\mathit{m}=+_{i\in
I}{\mathit{m}_{i}}$, $\mathit{e}=1+_{i\in I}{\mathit{e}_{i}}-|I|$, and
$\mathit{s}=+_{i\in I}{\mathit{s}_{i}}$.

######  Proof 4.20.

By case analysis on the form of $v$.

  * •

$v=x$. By $\mathtt{({var^{\mathcal{V}}_{c}})}$, we have
$({{\Phi^{i}_{v}}\rhd_{\mathcal{V}}{{{x}:{\mathcal{M}_{i}}}\vdash^{({0},{1},{0})}{{x}:{\mathcal{M}_{i}}}}})_{i\in
I}$. Then, we conclude by $\mathtt{({var^{\mathcal{V}}_{c}})}$ with
${\Phi_{v}}\rhd_{\mathcal{V}}{{{x}:{\mathcal{M}}}\vdash^{({0},{1},{0})}{{x}:{\mathcal{M}}}}$,
where $\mathcal{M}={\\!}\mathrel{+_{i\in I}}{\mathcal{M}_{i}}$ and hence
$\Gamma={\\!}\mathrel{+_{i\in I}}{\Gamma_{i}}$ as expected. Moreover, $+_{i\in
I}{\mathit{m}_{i}}=+_{i\in I}{\mathit{s}_{i}}=0$ and $+_{i\in
I}{\mathit{e}_{i}}=|I|$, hence $\mathit{e}=1+_{i\in I}{\mathit{e}_{i}}-|I|$.
Note that the persistent rules $\mathtt{({var_{p}})}$ and
$\mathtt{({val_{p}})}$ do not apply since they do not conclude with a multiset
type.

  * •

$v=\lambda{x}.{r}$. By $\mathtt{({abs^{\mathcal{V}}_{c}})}$, for each $i\in I$
we have $\Gamma_{i}={\\!}\mathrel{+_{k\in
K_{i}}}{{\Gamma_{k}}\mathrel{\setminus\\!\\!\setminus}{x}}$,
$\mathcal{M}_{i}=[{\Gamma_{k}(x)}\to{\tau_{k}}]_{k\in K_{i}}$ with
$\mathit{m}_{i}=+_{k\in K_{i}}{\mathit{m}_{k}}$, $\mathit{e}_{i}=1+_{k\in
K_{i}}{\mathit{e}_{k}}$, $\mathit{s}_{i}=+_{k\in K_{i}}{\mathit{s}_{k}}$ and
type derivations
$({{\Phi^{k}_{r}}\rhd_{\mathcal{V}}{{\Gamma_{k}}\vdash^{({\mathit{m}_{k}},{\mathit{e}_{k}},{\mathit{s}_{k}})}{{r}:{\tau_{k}}}}})_{k\in
K_{i}}$ for each $i\in I$. Let $J=\biguplus_{i\in I}{K_{i}}$ and
$\mathcal{M}=[{\Gamma_{j}(x)}\to{\tau_{j}}]_{j\in
J}=[{\Gamma_{k}(x)}\to{\tau_{k}}]_{k\in+_{i\in I}{K_{i}}}$ We conclude since,
by $\mathtt{({abs^{\mathcal{V}}_{c}})}$, we can build the derivation
${\Phi_{v}}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({+_{j\in
J}{\mathit{m}_{j}}},{1+_{j\in J}{\mathit{e}_{j}}},{+_{j\in
J}{\mathit{s}_{j}}})}{{v}:{\mathcal{M}}}}$ where:

    * –

$\Gamma={\\!}\mathrel{+_{j\in
J}}{{\Gamma_{j}}\mathrel{\setminus\\!\\!\setminus}{x}}={\\!}\mathrel{+_{i\in
I}}{({\\!}\mathrel{+_{k\in
K_{i}}}{{\Gamma_{k}}\mathrel{\setminus\\!\\!\setminus}{x}})}={\\!}\mathrel{+_{i\in
I}}{\Gamma_{i}}$

    * –

$\mathit{m}=+_{j\in J}{\mathit{m}_{j}}=+_{i\in I}{(+_{k\in
K_{i}}{\mathit{m}_{k}})}=+_{i\in I}{\mathit{m}_{i}}$

    * –

$\mathit{e}=1+_{j\in J}{\mathit{e}_{j}}=1+_{i\in I}{(1+_{k\in
K_{i}}{\mathit{e}_{k}})}-|I|=1+_{i\in I}{\mathit{e}_{i}}-|I|$

    * –

$\mathit{s}=+_{j\in J}{\mathit{s}_{j}}=+_{i\in I}{(+_{k\in
K_{i}}{\mathit{s}_{k}})}=+_{i\in I}{\mathit{s}_{i}}$

As before, the persistent rule $\mathtt{({abs^{\mathcal{V}}_{p}})}$ does not
apply since it does not conclude with a multiset type.

Dually to the substitution lemma, the following property states how to extract
type derivations (and thus counters) from substituted term.

######  Lemma 4.21 (Anti-Substitution).

Let
${\Phi_{{{t}\left\\{{x}\backslash{v}\right\\}}}}\rhd_{\mathcal{V}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}^{\prime\prime}},{\mathit{e}^{\prime\prime}},{\mathit{s}^{\prime\prime}})}{{{{t}\left\\{{x}\backslash{v}\right\\}}}:{\tau}}}$.
Then, there exist
${\Phi_{t}}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\tau}}}$
and
${\Phi_{v}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{v}:{\Gamma(x)}}}$
such that
$\Gamma^{\prime}={{\Gamma}\mathrel{\setminus\\!\\!\setminus}{x}}\mathrel{+}{\Delta}$,
$\mathit{m}^{\prime\prime}=\mathit{m}+\mathit{m}^{\prime}$,
$\mathit{e}^{\prime\prime}=\mathit{e}+\mathit{e}^{\prime}-1$ and
$\mathit{s}^{\prime\prime}=\mathit{s}+\mathit{s}^{\prime}$.

######  Proof 4.22.

By induction on $t$.

  * •

$t=x$. Then, ${{t}\left\\{{x}\backslash{v}\right\\}}=v$ and we analyze the
shape of $\tau$:

    * –

$\tau\in\mathtt{tt}$. Then, there are three further possibilities:

      * *

$\tau=\mathtt{n}$. This case does not apply since there is no way to derive
type $\mathtt{n}$ for a value.

      * *

$\tau=\mathtt{vl}$. Then, $\Phi_{{{t}\left\\{{x}\backslash{v}\right\\}}}$ can
only be $\mathtt{({val_{p}})}$ or $\mathtt{({abs^{\mathcal{V}}_{p}})}$. Thus,
$\Gamma^{\prime}$ is empty and
$\mathit{m}^{\prime\prime}=\mathit{e}^{\prime\prime}=\mathit{s}^{\prime\prime}=0$.
We conclude with
${\Phi_{t}}\rhd_{\mathcal{V}}{{}\vdash^{({0},{0},{0})}{{x}:{\mathtt{vl}}}}$ by
$\mathtt{({val_{p}})}$, and
${\Phi_{v}}\rhd_{\mathcal{V}}{{}\vdash^{({0},{1},{0})}{{v}:{[\,]}}}$ by either
$\mathtt{({var^{\mathcal{V}}_{c}})}$ or $\mathtt{({abs^{\mathcal{V}}_{c}})}$
with $I=\emptyset$.

      * *

$\tau=\mathtt{vr}$. Then, $v$ is necessarily a variable $z$, since
abstractions cannot be assigned $\mathtt{vr}$, and
$\Phi_{{{t}\left\\{{x}\backslash{v}\right\\}}}$ can only be
$\mathtt{({var_{p}})}$. Thus, $\Gamma^{\prime}={z}:{[\mathtt{vr}]}$ and
$\mathit{m}^{\prime\prime}=\mathit{e}^{\prime\prime}=\mathit{s}^{\prime\prime}=0$.
We conclude with
${\Phi_{t}}\rhd_{\mathcal{V}}{{{x}:{[\mathtt{vr}]}}\vdash^{({0},{0},{0})}{{x}:{\mathtt{vr}}}}$
by $\mathtt{({var_{p}})}$ and
${\Phi_{v}}\rhd_{\mathcal{V}}{{{z}:{[\mathtt{vr}]}}\vdash^{({0},{1},{0})}{{z}:{[\mathtt{vr}]}}}$
by $\mathtt{({var^{\mathcal{V}}_{c}})}$.

    * –

$\tau=\mathcal{M}$. Then, we take
$\Phi_{v}=\Phi_{{{t}\left\\{{x}\backslash{v}\right\\}}}$ and
${\Phi_{t}}\rhd_{\mathcal{V}}{{{x}:{\tau}}\vdash^{({0},{1},{0})}{{x}:{\tau}}}$
by $\mathtt{({var^{\mathcal{V}}_{c}})}$ to conclude. Note that the counters
are as expected.

    * –

$\tau={\mathcal{M}}\to{\sigma}$. This case does not apply since there is no
way to derive an arrow type for a value.

  * •

$t=y\neq x$. Then, ${{t}\left\\{{x}\backslash{v}\right\\}}=y$ and
$\Phi_{{{t}\left\\{{x}\backslash{v}\right\\}}}$ is either
${{y}:{[\mathtt{vr}]}}\vdash^{({0},{0},{0})}{{y}:{\mathtt{vr}}}$ by
$\mathtt{({var_{p}})}$, or ${}\vdash^{({0},{0},{0})}{{y}:{\mathtt{vl}}}$ by
$\mathtt{({val_{p}})}$, or ${}\vdash^{({0},{1},{0})}{{y}:{[\,]}}$ by
$\mathtt{({var^{\mathcal{V}}_{c}})}$. In either case we have
$\Gamma^{\prime}(x)=[\,]$, thus we take
$\Phi_{t}=\Phi_{{{t}\left\\{{x}\backslash{v}\right\\}}}$ and conclude with
${\Phi_{v}}\rhd_{\mathcal{V}}{{}\vdash^{({0},{1},{0})}{{v}:{[\,]}}}$ by either
$\mathtt{({var^{\mathcal{V}}_{c}})}$ or $\mathtt{({abs^{\mathcal{V}}_{c}})}$
with $I=\emptyset$. Note that the counters are as expected.

  * •

All the other cases are straightforward by the i.h. and Lem. 4.19.

######  Lemma 4.23 (Exact Subject Expansion).

Let
${\Phi^{\prime}}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}})}{{t^{\prime}}:{\sigma}}}$
be a tight derivation. If $t\rightarrow_{\mathtt{dv}}t^{\prime}$, then there
is
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
such that  (1) $\mathit{m}^{\prime}=\mathit{m}-1$and
$\mathit{e}^{\prime}=\mathit{e}$ if $t\rightarrow_{\mathtt{dv}}t^{\prime}$ is
an $\mathtt{m}$-step;  (2) $\mathit{e}^{\prime}=\mathit{e}-1$and
$\mathit{m}^{\prime}=\mathit{m}$ if $t\rightarrow_{\mathtt{dv}}t^{\prime}$ is
an $\mathtt{e}$-step.

######  Proof 4.24.

We actually prove the following stronger statement that allows us to reason
inductively:

Let $t\rightarrow_{\mathtt{dv}}t^{\prime}$ and
${\Phi^{\prime}}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}})}{{t^{\prime}}:{\sigma}}}$
such that $\Gamma$ is tight, and either $\sigma\in\mathtt{tt}$ or
$\neg\mathsf{abs}(t)$. Then, there exists
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
such that

  1. 1.

$\mathit{m}^{\prime}=\mathit{m}-1$ and $\mathit{e}^{\prime}=\mathit{e}$ if
$t\rightarrow_{\mathtt{dv}}t^{\prime}$ is an $\mathtt{m}$-step.

  2. 2.

$\mathit{e}^{\prime}=\mathit{e}-1$ and $\mathit{m}^{\prime}=\mathit{m}$ if
$t\rightarrow_{\mathtt{dv}}t^{\prime}$ is an $\mathtt{e}$-step.

We proceed by induction on $t\rightarrow_{\mathtt{dv}}t^{\prime}$.

  * •

$t={{\mathtt{L}}\langle{\lambda{x}.{r}}\rangle}\,{u}\rightarrow_{\mathtt{dv}}{\mathtt{L}}\langle{{r}[{x}\backslash{u}]}\rangle=t^{\prime}$
is an $\mathtt{m}$-step. We proceed by induction on $\mathtt{L}$. We only show
here the case $\mathtt{L}=\Box$ as the inductive case is straightforward.

Then, $t^{\prime}={r}[{x}\backslash{u}]$ and there are two possibilities for
$\Phi^{\prime}$.

    1. 1.

$\mathtt{({es_{p}})}$. Then $\Phi^{\prime}$ has the following form:

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}\quad{\Phi_{u}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{u}:{\mathtt{n}}}}\quad\mathsf{tight}(\Gamma^{\prime}(x))$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=215.90695pt\hbox{\kern
3.00003pt$\mathtt{({es_{p}})}$}}}\hbox{\kern 0.0pt\kern
36.90915pt\hbox{$\displaystyle{{{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}},{\mathit{e}_{1}+\mathit{e}_{2}},{\mathit{s}_{1}+\mathit{s}_{2}})}{{{r}[{x}\backslash{u}]}:{\sigma}}$}}}}$

with $\mathit{m}^{\prime}=\mathit{m}_{1}+\mathit{m}_{2}$,
$\mathit{e}^{\prime}=\mathit{e}_{1}+\mathit{e}_{2}$ and
$\mathit{s}=\mathit{s}_{1}+\mathit{s}_{2}$. We conclude by
$\mathtt{({appt^{\mathcal{V}}_{c}})}$ and $\mathtt{({abs^{\mathcal{V}}_{c}})}$
with the following type derivation

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 28.29913pt\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=127.29387pt\hbox{\kern
3.00003pt$\mathtt{({abs^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\vdash^{({\mathit{m}_{1}},{1+\mathit{e}_{1}},{\mathit{s}_{1}})}{{\lambda{x}.{r}}:{[{\Gamma^{\prime}(x)}\to{\sigma}]}}$}}}}\hskip
5.0pt plus 1.0fil\penalty
2{\Phi_{u}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{u}:{\mathtt{n}}}}\quad\mathsf{tight}(\Gamma^{\prime}(x))$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=323.20186pt\hbox{\kern
3.00003pt$\mathtt{({appt^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
76.40651pt\hbox{$\displaystyle{\Phi}\rhd_{\mathcal{V}}{{{{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}+1},{\mathit{e}_{1}+\mathit{e}_{2}},{\mathit{s}_{1}+\mathit{s}_{2}})}{{{(\lambda{x}.{r})}\,{u}}:{\sigma}}}$}}}}$

taking $\mathit{m}=\mathit{m}_{1}+\mathit{m}_{2}+1=\mathit{m}^{\prime}+1$ and
$\mathit{e}=\mathit{e}_{1}+\mathit{e}_{2}=\mathit{e}^{\prime}$.

    2. 2.

$\mathtt{({es_{c}})}$. Then $\Phi^{\prime}$ has the following form:

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}\quad{\Phi_{u}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{u}:{\Gamma^{\prime}(x)}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=171.74017pt\hbox{\kern
3.00003pt$\mathtt{({es_{c}})}$}}}\hbox{\kern 0.0pt\kern
14.82576pt\hbox{$\displaystyle{{{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}},{\mathit{e}_{1}+\mathit{e}_{2}},{\mathit{s}_{1}+\mathit{s}_{2}})}{{{r}[{x}\backslash{u}]}:{\sigma}}$}}}}$

with $\mathit{m}^{\prime}=\mathit{m}_{1}+\mathit{m}_{2}$,
$\mathit{e}^{\prime}=\mathit{e}_{1}+\mathit{e}_{2}$ and
$\mathit{s}=\mathit{s}_{1}+\mathit{s}_{2}$. We conclude by
$\mathtt{({app^{\mathcal{V}}_{c}})}$ and $\mathtt{({abs^{\mathcal{V}}_{c}})}$
with the following type derivation

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 28.29913pt\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=127.29387pt\hbox{\kern
3.00003pt$\mathtt{({abs^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\vdash^{({\mathit{m}_{1}},{1+\mathit{e}_{1}},{\mathit{s}_{1}})}{{\lambda{x}.{r}}:{[{\Gamma^{\prime}(x)}\to{\sigma}]}}$}}}}\hskip
5.0pt plus 1.0fil\penalty
2{\Phi_{u}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{u}:{\Gamma^{\prime}(x)}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=279.03508pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
54.32312pt\hbox{$\displaystyle{\Phi}\rhd_{\mathcal{V}}{{{{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}+1},{\mathit{e}_{1}+\mathit{e}_{2}},{\mathit{s}_{1}+\mathit{s}_{2}})}{{{(\lambda{x}.{r})}\,{u}}:{\sigma}}}$}}}}$

taking $\mathit{m}=\mathit{m}_{1}+\mathit{m}_{2}+1=\mathit{m}^{\prime}+1$ and
$\mathit{e}=\mathit{e}_{1}+\mathit{e}_{2}=\mathit{e}^{\prime}$.

  * •

$t={r}[{x}\backslash{{\mathtt{L}}\langle{v}\rangle}]\rightarrow_{\mathtt{dv}}{\mathtt{L}}\langle{{{r}\left\\{{x}\backslash{v}\right\\}}}\rangle=t^{\prime}$
is an $\mathtt{e}$-step. We proceed by induction on $\mathtt{L}$. We only show
here the case $\mathtt{L}=\Box$ as the inductive case is straightforward.

Then, $t^{\prime}={{r}\left\\{{x}\backslash{v}\right\\}}$. Lem. 4.21 with
$\Phi^{\prime}$, there exist type derivations
${\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}$
and
${\Phi_{v}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{v}:{\Gamma^{\prime}(x)}}}$
such that
$\Gamma={{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\mathrel{+}{\Delta}$,
$\mathit{m}^{\prime}=\mathit{m}_{1}+\mathit{m}_{2}$,
$\mathit{e}^{\prime}=\mathit{e}_{1}+\mathit{e}_{2}-1$ and
$\mathit{s}=\mathit{s}_{1}+\mathit{s}_{2}$. We conclude by
$\mathtt{({es_{c}})}$ with the following type derivation

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma^{\prime}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}\quad{\Phi_{v}}\rhd_{\mathcal{V}}{{\Delta}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{v}:{\Gamma^{\prime}(x)}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=170.93121pt\hbox{\kern
3.00003pt$\mathtt{({es_{c}})}$}}}\hbox{\kern 0.0pt\kern
5.6361pt\hbox{$\displaystyle{\Phi}\rhd_{\mathcal{V}}{{{{\Gamma^{\prime}}\mathrel{\setminus\\!\\!\setminus}{x}}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}},{\mathit{e}_{1}+\mathit{e}_{2}},{\mathit{s}_{1}+\mathit{s}_{2}})}{{{r}[{x}\backslash{v}]}:{\sigma}}}$}}}}$

taking $\mathit{m}=\mathit{m}_{1}+\mathit{m}_{2}=\mathit{m}^{\prime}$ and
$\mathit{e}=\mathit{e}_{1}+\mathit{e}_{2}=\mathit{e}^{\prime}+1$.

  * •

$t={r}\,{u}\rightarrow_{\mathtt{dv}}{r^{\prime}}\,{u}=t^{\prime}$, where
$r\rightarrow_{\mathtt{dv}}r^{\prime}$ and $\neg\mathsf{abs}(r)$. Then,
$\Phi^{\prime}$ ends with rule $\mathtt{({app^{\mathcal{V}}_{p}})}$,
$\mathtt{({app^{\mathcal{V}}_{c}})}$ or $\mathtt{({appt^{\mathcal{V}}_{c}})}$,
and in either case the subterm $r^{\prime}$ has an associated typing
derivation $\Phi_{r^{\prime}}$ which verifies the hypothesis since
$\neg\mathsf{abs}(r)$. Hence, by i.h. there exists a $\Phi_{r}$ with proper
counters such that we can derive $\Phi$ applying the same rule as in
$\Phi^{\prime}$ to conclude.

  * •

$t={r}\,{u}\rightarrow_{\mathtt{dv}}{r}\,{u^{\prime}}=t^{\prime}$, where
$u\rightarrow_{\mathtt{dv}}u^{\prime}$ and
$r\in\mathsf{ne}_{\mathtt{v}}\cup\mathsf{vr}_{\mathtt{v}}$. There are two
further cases to consider:

    1. 1.

If $\Phi^{\prime}$ ends with rule $\mathtt{({app^{\mathcal{V}}_{p}})}$, then
the subterm $u^{\prime}$ has an associated typing derivation which verifies
the hypothesis (context and type are tight). Then the property holds by i.h.

    2. 2.

If $\Phi^{\prime}$ ends with rule $\mathtt{({app^{\mathcal{V}}_{c}})}$ or
$\mathtt{({appt^{\mathcal{V}}_{c}})}$, then the subterm $r$ has an associated
typing derivation with a tight context and a functional type
$[{\mathcal{M}}\to{\sigma}]$. Lem. 4.3 (2) gives
$r\notin\mathsf{vr}_{\mathtt{v}}$ so that $r\in\mathsf{ne}_{\mathtt{v}}$.
Then, Lem. 4.3 (1) gives $[{\mathcal{M}}\to{\sigma}]\in\mathtt{tt}$ which
leads to a contradiction. So this case is not possible.

  * •

$t={r}[{x}\backslash{u}]\rightarrow_{\mathtt{dv}}{r^{\prime}}[{x}\backslash{u}]=t^{\prime}$,
where $r\rightarrow_{\mathtt{dv}}r^{\prime}$ and
$u\in\mathsf{ne}_{\mathtt{v}}$. There are two further cases to consider:

    1. 1.

If $\Phi^{\prime}$ ends with rule $\mathtt{({es_{p}})}$ then the subterm
$r^{\prime}$ has an associated typing derivation which verifies the hypothesis
(context tight and $\neg\mathsf{abs}(r)$). Then the property holds by i.h.

    2. 2.

If $\Phi^{\prime}$ ends with rule $\mathtt{({es_{c}})}$ then the subterm $u$
has an associated typing derivation with a tight context and a multiset type
$\mathcal{M}$. Lem. 4.3 (1) gives $\mathcal{M}\in\mathtt{tt}$ which leads to a
contradiction. So this case is not possible.

  * •

$t={r}[{x}\backslash{u}]\rightarrow_{\mathtt{dv}}{r}[{x}\backslash{u^{\prime}}]=t^{\prime}$,
where $u\rightarrow_{\mathtt{dv}}u^{\prime}$ and $\neg\mathsf{val}(u)$. There
are two further cases to consider:

    1. 1.

If $\Phi^{\prime}$ ends with rule $\mathtt{({es_{p}})}$ then the subterm
$u^{\prime}$ has an associated typing derivation which verifies the hypothesis
(context and type are tight). Then the property holds by the i.h. .

    2. 2.

If $\Phi^{\prime}$ ends with rule $\mathtt{({es_{c}})}$ then the subterm
$u^{\prime}$ has an associated typing derivation $\Phi_{u^{\prime}}$ which
verifies the hypothesis since $\neg\mathsf{val}(u)$ implies
$\neg\mathsf{abs}(u)$. Hence, by i.h. there exists a $\Phi_{u}$ with proper
counters such that we can derive $\Phi$ applying $\mathtt{({es_{c}})}$ as in
$\Phi^{\prime}$ to conclude.

Notice that tight derivations properly counts, separately, $\mathtt{m}$-steps
and $\mathtt{e}$-steps. As a consequence, completeness follows.

######  Theorem 4.25 (Completeness).

If $t\twoheadrightarrow_{\mathtt{v}}^{(\mathit{m},\mathit{e})}p$ with
$p\in\mathsf{no}_{\mathtt{v}}$, then there exists a tight type derivation
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{|{p}|_{\mathtt{v}}})}{{t}:{\sigma}}}$.

######  Proof 4.26.

As for soundness (Thm. 4.15) prove the statement for
$\rightarrow_{\mathtt{dv}}$ and then conclude for the general notion of
reduction $\rightarrow_{\mathtt{v}}$. Let
$t\twoheadrightarrow_{\mathtt{dv}}^{(\mathit{m},\mathit{e})}p$. We proceed by
induction on $\mathit{m}+\mathit{e}$:

  * •

If $\mathit{m}+\mathit{e}=0$, then $\mathit{m}=\mathit{e}=0$ and thus $t=p$,
which implies $t\in\mathsf{no}_{\mathtt{v}}$. Lem. 4.17 allows to conclude.

  * •

If $\mathit{m}+\mathit{e}>0$, then there is $t^{\prime}$ such that
$t\twoheadrightarrow_{\mathtt{dv}}^{(1,0)}t^{\prime}\twoheadrightarrow_{\mathtt{dv}}^{(\mathit{m}-1,\mathit{e})}p$
or
$t\twoheadrightarrow_{\mathtt{dv}}^{(0,1)}t^{\prime}\twoheadrightarrow_{\mathtt{dv}}^{(\mathit{m},\mathit{e}-1)}p$.
By the i.h. there is a tight derivation
${\Phi^{\prime}}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{|{p}|_{\mathtt{v}}})}{{t^{\prime}}:{\sigma}}}$
such $\mathit{m}^{\prime}+\mathit{e}^{\prime}=\mathit{m}+\mathit{e}-1$. Lem.
4.23 gives a tight derivation
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}^{\prime\prime}},{\mathit{e}^{\prime\prime}},{|{p}|_{\mathtt{v}}})}{{t}:{\sigma}}}$
such
$\mathit{m}^{\prime\prime}+\mathit{e}^{\prime\prime}=\mathit{m}^{\prime}+\mathit{e}^{\prime}+1$.
We then have
$\mathit{m}^{\prime\prime}+\mathit{e}^{\prime\prime}=\mathit{m}+\mathit{e}$.
The fact that $\mathit{m}^{\prime\prime}=\mathit{m}$ and
$\mathit{e}^{\prime\prime}=\mathit{e}$ holds by a simple case analysis.

######  Example 4.27.

Consider $t_{0}={{{\tt K}}\,{({z}\,{{\tt I}})}}\,{({{\tt I}}\,{{\tt I}})}$
from Ex. 3.21 but now in the CBV setting. It
$\rightarrow_{\mathtt{v}}$-reduces in 3 $\mathtt{m}$-steps and 2
$\mathtt{e}$-steps to ${x}[{x}\backslash{{z}\,{{\tt
I}}}]\in\mathsf{no}_{\mathtt{v}}$, whose $\mathtt{v}$-size is 1, as follows:

$\begin{array}[]{lllllllll}t_{0}&=&{\underline{{{\tt K}}\,{({z}\,{{\tt
I}})}}}\,{({{\tt I}}\,{{\tt
I}})}&\rightarrow_{\mathtt{dB}}&\underline{{{(\lambda{y}.{x})}[{x}\backslash{{z}\,{{\tt
I}}}]}\,{({{\tt I}}\,{{\tt
I}})}}&\rightarrow_{\mathtt{dB}}&{{x}[{y}\backslash{\underline{{{\tt
I}}\,{{\tt I}}}}]}[{x}\backslash{{z}\,{{\tt I}}}]\\\
&\rightarrow_{\mathtt{dB}}&{\underline{{x}[{y}\backslash{{w}[{w}\backslash{{\tt
I}}]}]}}[{x}\backslash{{z}\,{{\tt
I}}}]&\rightarrow_{\mathtt{sv}}&{\underline{{x}[{w}\backslash{{\tt
I}}]}}[{x}\backslash{{z}\,{{\tt
I}}}]&\rightarrow_{\mathtt{sv}}&{x}[{x}\backslash{{z}\,{{\tt I}}}]\end{array}$

System $\mathcal{V}$ admits a proper tight type derivation for $t_{0}={{{\tt
K}}\,{({z}\,{{\tt I}})}}\,{({{\tt I}}\,{{\tt I}})}$ from Ex. 4.27, with the
expected final counter $(3,2,1)$, as shown in Fig. 5.

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 35.62077pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=71.24155pt\hbox{\kern
3.00003pt$\mathtt{({var_{p}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{x}:{[\mathtt{vr}]}}\vdash^{({0},{0},{0})}{{x}:{\mathtt{vr}}}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=129.98822pt\hbox{\kern
3.00003pt$\mathtt{({abs^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
13.54808pt\hbox{$\displaystyle{{x}:{[\mathtt{vr}]}}\vdash^{({0},{1},{0})}{{\lambda{y}.{x}}:{[{[\,]}\to{\mathtt{vr}}]}}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=190.68488pt\hbox{\kern
3.00003pt$\mathtt{({abs^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
50.1591pt\hbox{$\displaystyle{}\vdash^{({0},{2},{0})}{{{\tt
K}}:{[{[\mathtt{vr}]}\to{[{[\,]}\to{\mathtt{vr}}]}]}}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt
plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 34.9958pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=69.99161pt\hbox{\kern
3.00003pt$\mathtt{({var_{p}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{z}:{[\mathtt{vr}]}}\vdash^{({0},{0},{0})}{{z}:{\mathtt{vr}}}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
18.21114pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=36.42227pt\hbox{\kern
3.00003pt$\mathtt{({abs^{\mathcal{V}}_{p}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{}\vdash^{({0},{0},{0})}{{{\tt
I}}:{\mathtt{vl}}}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=225.85721pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{V}}_{p}})}$}}}\hbox{\kern 0.0pt\kern
78.50224pt\hbox{$\displaystyle{{z}:{[\mathtt{vr}]}}\vdash^{({0},{0},{1})}{{{z}\,{{\tt
I}}}:{\mathtt{n}}}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=534.54652pt\hbox{\kern
3.00003pt$\mathtt{({appt^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
212.13858pt\hbox{$\displaystyle{{z}:{[\mathtt{vr}]}}\vdash^{({1},{1},{1})}{{{{\tt
K}}\,{({z}\,{{\tt I}})}}:{[{[\,]}\to{\mathtt{vr}}]}}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt
plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 22.48071pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=44.96143pt\hbox{\kern
3.00003pt$\mathtt{({var^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{}\vdash^{({0},{1},{0})}{{w}:{[\,]}}$}}}}\hskip 5.0pt
plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=104.79698pt\hbox{\kern
3.00003pt$\mathtt{({abs^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
24.3263pt\hbox{$\displaystyle{}\vdash^{({0},{2},{0})}{{{\tt
I}}:{[{[\,]}\to{[\,]}]}}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\hskip 5.0pt
plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 19.18329pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=38.36658pt\hbox{\kern
3.00003pt$\mathtt{({abs^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{}\vdash^{({0},{1},{0})}{{{\tt I}}:{[\,]}}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=264.55687pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
110.45627pt\hbox{$\displaystyle{}\vdash^{({1},{2},{0})}{{{{\tt I}}\,{{\tt
I}}}:{[\,]}}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=563.76535pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
227.8591pt\hbox{$\displaystyle{{z}:{[\mathtt{vr}]}}\vdash^{({3},{2},{1})}{{{{{\tt
K}}\,{({z}\,{{\tt I}})}}\,{({{\tt I}}\,{{\tt I}})}}:{\mathtt{vr}}}$}}}}$

Figure 5: Tight type derivation for $t_{0}$ in System $\mathcal{V}$.

##  5 The $\lambda!$-Calculus

This section briefly presents the _bang calculus at a distance_ [12], called
$\lambda!$-calculus. It is a (conservative) extension of the original bang
calculus [25, 26], it uses ES operators and _reduction at a distance_ [5],
thus integrating commutative conversions without jeopardising confluence (see
[12] for a discussion). Indeed, T. Ehrhard [25] studies the CBPV from a Linear
Logic (LL) point of view by extending the $\lambda$-calculus with two new
unary constructors _bang_ ($\mathop{!}{\\!}$) and _dereliction_
($\mathop{\textnormal{der}}{\\!}$), playing the role of the CBPV primitives
$\mathtt{thunk}$/$\mathtt{force}$ respectively. His calculus suffers from the
absence of _commutative conversions_ [44, 15], making some redexes to be
syntactically blocked when open terms are considered. As a consequence, some
normal forms are semantically equivalent to non-terminating programs, a
situation which is clearly unsound. The bang calculus [26] adds commutative
conversions specified by means of $\sigma$-reduction rules, which are crucial
to unveil hidden (blocked) redexes. This approach, however, presents a major
drawback since the resulting combined reduction relation is not confluent. The
$\lambda!$-calculus [12] fixes these two problems at the same time. Indeed,
the syntax of the bang calculus is enriched with explicit substitutions (ES),
and $\sigma$-equivalence is integrated in the primary reduction system by
using the _distance_ paradigm [5], without any need to unveil hidden redexes
by means of an independent relation.

We consider the following grammar for terms (denoted by $\mathcal{T}$) and
contexts:

_(Terms)_ | $t,u$ | $::=$ | $x\in\mathcal{X}\mid{t}\,{u}\mid\lambda{x}.{t}\mid\mathop{!}{t}\mid\mathop{\textnormal{der}}{t}\mid{t}[{x}\backslash{u}]$
---|---|---|---
_(List contexts)_ | $\mathtt{L}$ | $::=$ | $\Box\mid{\mathtt{L}}[{x}\backslash{t}]$
_(Surface contexts)_ | $\mathtt{S}$ | $::=$ | $\Box\mid{\mathtt{S}}\,{t}\mid{t}\,{\mathtt{S}}\mid\lambda{x}.{\mathtt{S}}\mid\mathop{\textnormal{der}}{\mathtt{S}}\mid{\mathtt{S}}[{x}\backslash{u}]\mid{t}[{x}\backslash{\mathtt{S}}]$

Special terms are $\Delta_{\mathop{!}{}}=\lambda{x}.{{x}\,{\mathop{!}{x}}}$,
and
$\Omega_{\mathop{!}{}}={\Delta_{\mathop{!}{}}}\,{\mathop{!}{\Delta_{\mathop{!}{}}}}$.
Surface contexts do not allow the symbol $\Box$ to occur inside the bang
constructor $\mathop{!}{}$. This is similar to _weak_ contexts in
$\lambda$-calculus, where $\Box$ cannot occur inside $\lambda$-abstractions.
As we will see in Sec. 7, surface reduction in the $\lambda!$-calculus is
perfectly sufficient to capture head reduction in CBN, disallowing reduction
inside arguments, as well as open CBV, disallowing reduction inside
abstractions. Finally, we define the _$\mathtt{f}$ -size_ of terms as follows:

$\begin{array}[]{lll@{\hspace{1cm}}lll@{\hspace{1cm}}lll}|{x}|_{\mathtt{f}}&:=&0\hfil\hskip
28.45274pt&|{\mathop{\textnormal{der}}{t}}|_{\mathtt{f}}&:=&|{t}|_{\mathtt{f}}\hfil\hskip
28.45274pt&|{{t}[{x}\backslash{u}]}|_{\mathtt{f}}&:=&|{t}|_{\mathtt{f}}+|{u}|_{\mathtt{f}}\\\
|{\mathop{!}{t}}|_{\mathtt{f}}&:=&0\hfil\hskip
28.45274pt&|{\lambda{x}.{t}}|_{\mathtt{f}}&:=&1+|{t}|_{\mathtt{f}}\hfil\hskip
28.45274pt&|{{t}\,{u}}|_{\mathtt{f}}&:=&1+|{t}|_{\mathtt{f}}+|{u}|_{\mathtt{f}}\end{array}$

The _$\lambda!$ -calculus_ is given by the set of terms $\mathcal{T}$ and the
_(surface) reduction relation_ $\rightarrow_{\mathtt{f}}$, which is defined as
the _union_ of $\rightarrow_{\mathtt{dB}}$, $\rightarrow_{\mathtt{s!}}$
(substitute bang) and $\rightarrow_{\mathtt{d!}}$ (distant bang), defined
respectively as the closure by contexts $\mathtt{S}$ of the following three
rewriting rules:

$\begin{array}[]{lll}{{\mathtt{L}}\langle{\lambda{x}.{t}}\rangle}\,{u}&\mathrel{\mapsto_{\mathtt{dB}}}&{\mathtt{L}}\langle{{t}[{x}\backslash{u}]}\rangle\\\
{t}[{x}\backslash{{\mathtt{L}}\langle{\mathop{!}{u}}\rangle}]&\mathrel{\mapsto_{\mathtt{s!}}}&{\mathtt{L}}\langle{{{t}\left\\{{x}\backslash{u}\right\\}}}\rangle\\\
\mathop{\textnormal{der}}{({\mathtt{L}}\langle{\mathop{!}{t}}\rangle)}&\mathrel{\mapsto_{\mathtt{d!}}}&{\mathtt{L}}\langle{t}\rangle\end{array}$

The rules are defined _at a distance_ , as in CBN/CBV, in the sense that the
list context $\mathtt{L}$ allows the main constructors involved in the rules
to be separated by an arbitrary finite list of substitutions. This new
formulation integrates commutative conversions inside the main (logical)
reduction rules of the calculus, thus inheriting the benefits enumerated in
Sec. 1. Indeed, rule $\mathtt{s!}$ can be decomposed in two different rules
${t}[{x}\backslash{\mathop{!}{u}}]\mathrel{\mapsto}{{t}\left\\{{x}\backslash{u}\right\\}}$
and
${t}[{x}\backslash{{\mathtt{L}}\langle{\mathop{!}{u}}\rangle}]\mathrel{\mapsto}{\mathtt{L}}\langle{{t}[{x}\backslash{\mathop{!}{u}}]}\rangle$,
while $\mathtt{d!}$ can be decomposed in
$\mathop{\textnormal{der}}{(\mathop{!}{t})}\mathrel{\mapsto}t$ and
$\mathop{\textnormal{der}}{({\mathtt{L}}\langle{\mathop{!}{t}}\rangle)}\mathrel{\mapsto}{\mathtt{L}}\langle{\mathop{\textnormal{der}}{\mathop{!}{t}}}\rangle$.
We write $\twoheadrightarrow_{\mathtt{f}}$ for the reflexive-transitive
closure of $\rightarrow_{\mathtt{f}}$. Given the translation of the bang
calculus into LL proof-nets [25], we refer to $\mathtt{dB}$-steps as
_$\mathtt{m}$ ultiplicative_ and $\mathtt{s!}$/$\mathtt{d!}$-steps as
_$\mathtt{e}$ xponential_ steps. We write
$t\twoheadrightarrow_{\mathtt{f}}^{(\mathit{m},\mathit{e})}u$ if
$t\twoheadrightarrow_{\mathtt{f}}u$ using $\mathit{m}$ $\mathtt{m}$-steps and
$\mathit{e}$ $\mathtt{e}$-steps.

######  Example 5.1.

Consider the following reduction sequence from $t^{\prime}_{0}={{{\tt
K}}\,{(\mathop{!}{({z}\,{\mathop{!}{{\tt I}}})})}}\,{(\mathop{!}{({{\tt
I}}\,{\mathop{!}{{\tt I}}})})}$:

$\begin{array}[]{lllll}t^{\prime}_{0}={\underline{{{\tt
K}}\,{(\mathop{!}{({z}\,{\mathop{!}{{\tt I}}})})}}}\,{(\mathop{!}{({{\tt
I}}\,{\mathop{!}{{\tt
I}}})})}&\rightarrow_{\mathtt{dB}}&\underline{{{(\lambda{y}.{x})}[{x}\backslash{\mathop{!}{({z}\,{\mathop{!}{{\tt
I}}})}}]}\,{(\mathop{!}{({{\tt I}}\,{\mathop{!}{{\tt
I}}})})}}&\rightarrow_{\mathtt{dB}}&\underline{{{x}[{y}\backslash{\mathop{!}{({{\tt
I}}\,{\mathop{!}{{\tt
I}}})}}]}[{x}\backslash{\mathop{!}{({z}\,{\mathop{!}{{\tt I}}})}}]}\\\
&\rightarrow_{\mathtt{s!}}&\underline{{({z}\,{\mathop{!}{{\tt
I}}})}[{y}\backslash{\mathop{!}{({{\tt I}}\,{\mathop{!}{{\tt
I}}})}}]}&\rightarrow_{\mathtt{s!}}&{z}\,{\mathop{!}{{\tt I}}}\end{array}$

Notice that the second $\mathtt{dB}$-step uses action at a distance, where
$\mathtt{L}$ is ${\Box}[{x}\backslash{\mathop{!}{({z}\,{\mathop{!}{{\tt
I}}})}}]$.

The relation $\rightarrow_{\mathtt{f}}$ enjoys a weak diamond property, i.e.
one-step divergence can be closed in one step if the diverging terms are
different. This property has two important consequences.

######  Theorem 5.2 (Confluence [12]).

The reduction relation $\rightarrow_{\mathtt{f}}$ is confluent. Moreover, any
two different $\rightarrow_{\mathtt{f}}$-reduction paths to normal form have
the same length.

The second point relies essentially on the fact that reductions are disallowed
under bangs. An important consequence is that we can focus on any particular
_deterministic_ strategy for the $\lambda!$-calculus, without changing the
number of steps to $\mathtt{f}$-normal form.

Neutral, Normal, and Clash-Free Terms. A term is said to be _$\mathtt{f}$
-normal_ if there is no $t^{\prime}$ such that
$t\rightarrow_{\mathtt{f}}t^{\prime}$, in which case we write
$t\not\rightarrow_{\mathtt{f}}$. However, some ill-formed $\mathtt{f}$-normal
terms are not still the ones that represent a desired result for a
computation, they are called _clashes_ (meta-variable $c$), and take one of
the following forms: ${{\mathtt{L}}\langle{\mathop{!}{t}}\rangle}\,{u}$,
${t}[{y}\backslash{{\mathtt{L}}\langle{\lambda{x}.{u}}\rangle}]$,
$\mathop{\textnormal{der}}{({\mathtt{L}}\langle{\lambda{x}.{u}}\rangle)}$, or
${t}\,{({{\mathtt{L}}\langle{\lambda{x}.{u}}\rangle})}$. Remark that in the
three first kind of clashes, replacing $\lambda{x}.{\\!}$ by
$\mathop{!}{\\!}$, and inversely, creates a (root) redex, namely
${({\mathtt{L}}\langle{\lambda{x}.{t}}\rangle)}\,{u}$,
${t}[{x}\backslash{{\mathtt{L}}\langle{\mathop{!}{t}}\rangle}]$ and
$\mathop{\textnormal{der}}{({\mathtt{L}}\langle{\mathop{!}{t}}\rangle)}$,
respectively.

A term is _clash free_ if it does not reduce to a term containing a clash, it
is _surface clash free_ , written ${\tt scf}$, if it does not reduce to a term
containing a clash outside the scope of any constructor $!$. Thus, $t$ is not
${\tt scf}$ if and only if there exist a surface context $\mathtt{S}$ and a
clash $c$ such that
$t\twoheadrightarrow_{\mathtt{f}}{\mathtt{S}}\langle{c}\rangle$. Surface clash
free normal terms can be characterised as follows:

_(Neutral ${\tt scf}$)_ | $\mathsf{ne}_{{\tt scf}}$ | $::=$ | $x\in\mathcal{X}\mid{\mathsf{ne}_{{\tt scf}}}\,{\mathsf{na}_{{\tt scf}}}\mid\mathop{\textnormal{der}}{(\mathsf{ne}_{{\tt scf}})}\mid{\mathsf{ne}_{{\tt scf}}}[{x}\backslash{\mathsf{ne}_{{\tt scf}}}]$
---|---|---|---
_(Neutral-Abs ${\tt scf}$)_ | $\mathsf{na}_{{\tt scf}}$ | $::=$ | $\mathop{!}{t}\mid\mathsf{ne}_{{\tt scf}}\mid{\mathsf{na}_{{\tt scf}}}[{x}\backslash{\mathsf{ne}_{{\tt scf}}}]$
_(Neutral-Bang ${\tt scf}$)_ | $\mathsf{nb}_{{\tt scf}}$ | $::=$ | $\mathsf{ne}_{{\tt scf}}\mid\lambda{x}.{\mathsf{no}_{{\tt scf}}}\mid{\mathsf{nb}_{{\tt scf}}}[{x}\backslash{\mathsf{ne}_{{\tt scf}}}]$
_(Normal ${\tt scf}$)_ | $\mathsf{no}_{{\tt scf}}$ | $::=$ | $\mathsf{na}_{{\tt scf}}\mid\mathsf{nb}_{{\tt scf}}$

######  Proposition 5.3 (Clash-Free Normal Terms [12]).

Let $t\in\mathcal{T}$. Then $t$ is a surface clash free $\mathtt{f}$-normal
term iff ${t}\in\mathsf{no}_{{\tt scf}}$.

##  6 A Tight Type System for the $\lambda!$-Calculus

The methodology used to define the type system $\mathcal{B}$ for the
$\lambda!$-calculus is based on [12], inspired in turn from [19, 9, 1], which
defines non-idempotent intersection type systems to count reduction lengths
for different evaluation strategies in the $\lambda$-calculus. In the case of
the $\lambda!$-calculus, however, Thm. 5.2 guarantees that all reduction paths
to normal form have the same length, so that it is not necessary to reason
w.r.t. any particular evaluation strategy.

The grammar of types of system $\mathcal{B}$ is given by:

_(Tight Types)_ | $\mathtt{tt}$ | $::=$ | $\mathtt{n}\mid\mathtt{a}\mid\mathtt{vl}$
---|---|---|---
_(Types)_ | $\sigma,\tau$ | $::=$ | $\mathtt{tt}\mid\mathcal{M}\mid{\mathcal{M}}\to{\sigma}$
_(Multitype)_ | $\mathcal{M},\mathcal{N}$ | $::=$ |  $[\sigma_{i}]_{i\in I}$ where $I$ is a finite set

The constant $\mathtt{a}$ (resp. $\mathtt{vl}$) types terms whose normal form
has the shape ${\mathtt{L}}\langle{\lambda{x}.{t}}\rangle$ (resp.
${\mathtt{L}}\langle{\mathop{!}{t}}\rangle$, i.e.  _values_ in the
$\lambda!$-calculus sense), and the constant $\mathtt{n}$ types terms whose
normal form is a neutral ${\tt scf}$. As before, the notions of _tightness_
for multitypes, contexts and derivations are exactly the same used for CBN.
Typing rules are split in two groups: the _persistent_ rules (Fig. 6) and the
_consuming_ ones (Fig. 7).

$\kern-20.00003pt\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\mathtt{n}}}\quad{\Delta}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{u}:{\overline{\mathtt{a}}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=104.11012pt\hbox{\kern
3.00003pt$\mathtt{({app_{p}})}$}}}\hbox{\kern 0.0pt\kern
3.62216pt\hbox{$\displaystyle{{\Gamma}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}+\mathit{m}^{\prime}},{\mathit{e}+\mathit{e}^{\prime}},{\mathit{s}+\mathit{s}^{\prime}+1})}{{{t}\,{u}}:{\mathtt{n}}}$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\mathtt{tt}}}\quad\mathsf{tight}(\Gamma(x))$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=104.49097pt\hbox{\kern
3.00003pt$\mathtt{({abs_{p}})}$}}}\hbox{\kern 0.0pt\kern
10.02293pt\hbox{$\displaystyle{{\Gamma}\mathrel{\setminus\\!\\!\setminus}{x}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}+1})}{{\lambda{x}.{t}}:{\mathtt{a}}}$}}}}\\\
\\\ {tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\vphantom{{}\vdash^{({0},{0},{0})}{{\mathop{!}{t}}:{\mathtt{vl}}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=39.20006pt\hbox{\kern
3.00003pt$\mathtt{({bg_{p}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{}\vdash^{({0},{0},{0})}{{\mathop{!}{t}}:{\mathtt{vl}}}$}}}}\quad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
5.56949pt\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\mathtt{n}}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=55.05342pt\hbox{\kern
3.00003pt$\mathtt{({dr_{p}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{\mathop{\textnormal{der}}{t}}:{\mathtt{n}}}$}}}}\quad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\tau}}\enspace{\Delta}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{u}:{\mathtt{n}}}\enspace\mathsf{tight}(\Gamma(x))$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=154.61362pt\hbox{\kern
3.00003pt$\mathtt{({es_{p}})}$}}}\hbox{\kern 0.0pt\kern
7.88402pt\hbox{$\displaystyle{{({\Gamma}\mathrel{\setminus\\!\\!\setminus}{x})}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}+\mathit{m}^{\prime}},{\mathit{e}+\mathit{e}^{\prime}},{\mathit{s}+\mathit{s}^{\prime}})}{{{t}[{x}\backslash{u}]}:{\tau}}$}}}}\end{array}$

Figure 6: System $\mathcal{B}$ for the $\lambda!$-Calculus: Persistent Typing
Rules.

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 13.92926pt\hbox{$\displaystyle\penalty
1\vphantom{{}\vdash^{({0},{0},{0})}{{\mathop{!}{t}}:{\mathtt{vl}}}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=67.05858pt\hbox{\kern
3.00003pt$\mathtt{({var_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{x}:{[\sigma]}}\vdash^{({0},{0},{0})}{{x}:{\sigma}}$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{{\mathcal{M}}\to{\tau}}}\quad{\Delta}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{u}:{\mathcal{M}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=121.25946pt\hbox{\kern
3.00003pt$\mathtt{({app_{c}})}$}}}\hbox{\kern 0.0pt\kern
11.4pt\hbox{$\displaystyle{{\Gamma}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}+\mathit{m}^{\prime}+1},{\mathit{e}+\mathit{e}^{\prime}},{\mathit{s}+\mathit{s}^{\prime}})}{{{t}\,{u}}:{\tau}}$}}}}\\\
\\\ {tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{{\mathcal{M}}\to{\tau}}}\quad{\Delta}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{u}:{\mathtt{n}}}\quad\mathsf{tight}(\mathcal{M})$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=165.42624pt\hbox{\kern
3.00003pt$\mathtt{({appt_{c}})}$}}}\hbox{\kern 0.0pt\kern
33.48338pt\hbox{$\displaystyle{{\Gamma}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}+\mathit{m}^{\prime}+1},{\mathit{e}+\mathit{e}^{\prime}},{\mathit{s}+\mathit{s}^{\prime}})}{{{t}\,{u}}:{\tau}}$}}}}\\\
\\\ {tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 27.94803pt\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\tau}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=101.40417pt\hbox{\kern
3.00003pt$\mathtt{({abs_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{\Gamma}\mathrel{\setminus\\!\\!\setminus}{x}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{\lambda{x}.{t}}:{{\Gamma(x)}\to{\tau}}}$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
22.33336pt\hbox{$\displaystyle\penalty
1({\Gamma_{i}}\vdash^{({\mathit{m}_{i}},{\mathit{e}_{i}},{\mathit{s}_{i}})}{{t}:{\sigma_{i}}})_{i\in
I}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=115.02481pt\hbox{\kern
3.00003pt$\mathtt{({bg_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{}\mathrel{+_{i\in I}}{\Gamma_{i}}}\vdash^{({+_{i\in
I}{\mathit{m}_{i}}},{1+_{i\in I}{\mathit{e}_{i}}},{+_{i\in
I}{\mathit{s}_{i}}})}{{\mathop{!}{t}}:{[\sigma_{i}]_{i\in I}}}$}}}}\\\ \\\
{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 2.7917pt\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{[\sigma]}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=57.98969pt\hbox{\kern
3.00003pt$\mathtt{({dr_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{\mathop{\textnormal{der}}{t}}:{\sigma}}$}}}}\qquad{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
7.8105pt\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}\quad{\Delta}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{u}:{\Gamma(x)}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=140.18817pt\hbox{\kern
3.00003pt$\mathtt{({es_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{({\Gamma}\mathrel{\setminus\\!\\!\setminus}{x})}\mathrel{+}{\Delta}}\vdash^{({\mathit{m}+\mathit{m}^{\prime}},{\mathit{e}+\mathit{e}^{\prime}},{\mathit{s}+\mathit{s}^{\prime}})}{{{t}[{x}\backslash{u}]}:{\sigma}}$}}}}\end{array}$

Figure 7: System $\mathcal{B}$ for the $\lambda!$-Calculus: Consuming Typing
Rules.

As in CBV, the $\mathtt{s!}$ exponential steps do not only depend on a
(consuming) substitution constructor, but on the (bang) form of its argument.
This makes the exponential counting more subtle. Notice also that rule
$\mathtt{({dr_{p}})}$ does not count $\mathop{\textnormal{der}}{\\!}$
constructors, according to the definition of $|{\\_}|_{\mathtt{f}}$ given in
Sec. 5 and in contrast to [12]. This is to keep a more intuitive relation with
the CBN/CBV translations (Sec. 2), where $\mathop{\textnormal{der}}{\\!}$
plays a silent role.

As in [12], system $\mathcal{B}$ is quantitatively sound and complete. More
precisely,

######  Theorem 6.1 (Soundness and Completeness).

  1. 1.

If
${\Phi}\rhd_{\mathcal{B}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
is tight, then there exists $p$ such that ${p}\in\mathsf{no}_{{\tt scf}}$ and
$t\twoheadrightarrow_{\mathtt{f}}^{(\mathit{m},\mathit{e})}p$ with
$\mathit{m}$ $\mathtt{m}$-steps, $\mathit{e}$ $\mathtt{e}$-steps, and
$|{p}|_{\mathtt{f}}=\mathit{s}$.

  2. 2.

If $t\twoheadrightarrow_{\mathtt{f}}^{(\mathit{m},\mathit{e})}p$ with
${p}\in\mathsf{no}_{{\tt scf}}$, then there exists a tight type derivation
${\Phi}\rhd_{\mathcal{B}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{|{p}|_{\mathtt{f}}})}{{t}:{\sigma}}}$.

######  Proof 6.2.

Similar to [12].

######  Example 6.3.

Consider $t^{\prime}_{0}={{{\tt K}}\,{(\mathop{!}{({z}\,{\mathop{!}{{\tt
I}}})})}}\,{(\mathop{!}{({{\tt I}}\,{\mathop{!}{{\tt I}}})})}$ from Ex. 5.1,
which normalises in $2$ $\mathtt{m}$-steps and $2$ $\mathtt{e}$-steps to
${z}\,{\mathop{!}{{\tt I}}}\in\mathsf{no}_{{\tt scf}}$ of $\mathtt{f}$-size
$1$. A tight derivation for $t^{\prime}_{0}$ with appropriate final counters
$(2,2,1)$ is given below.

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 28.78377pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=57.56754pt\hbox{\kern
2.70003pt$\mathtt{({var_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{x}:{[\mathtt{n}]}}\vdash^{({0},{0},{0})}{{x}:{\mathtt{n}}}$}}}}\hskip
4.5pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=109.87952pt\hbox{\kern
2.70003pt$\mathtt{({abs_{c}})}$}}}\hbox{\kern 0.0pt\kern
15.66325pt\hbox{$\displaystyle{{x}:{[\mathtt{n}]}}\vdash^{({0},{0},{0})}{{\lambda{y}.{x}}:{{[\,]}\to{\mathtt{n}}}}$}}}}\hskip
4.5pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=162.96649pt\hbox{\kern
2.70003pt$\mathtt{({abs_{c}})}$}}}\hbox{\kern 0.0pt\kern
50.3432pt\hbox{$\displaystyle{}\vdash^{({0},{0},{0})}{{{\tt
K}}:{{[\mathtt{n}]}\to{{[\,]}\to{\mathtt{n}}}}}$}}}}\hskip 4.5pt plus
1.0fil\penalty 2\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt
plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 4.5pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 28.22127pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=56.44254pt\hbox{\kern
2.70003pt$\mathtt{({var_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{z}:{[\mathtt{n}]}}\vdash^{({0},{0},{0})}{{z}:{\mathtt{n}}}$}}}}\hskip
4.5pt plus 1.0fil\penalty 2\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
17.64001pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=35.28003pt\hbox{\kern
2.70003pt$\mathtt{({bg_{p}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{}\vdash^{({0},{0},{0})}{{\mathop{!}{{\tt
I}}}:{\mathtt{vl}}}$}}}}\hskip 4.5pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=194.13152pt\hbox{\kern
2.70003pt$\mathtt{({app_{p}})}$}}}\hbox{\kern 0.0pt\kern
67.71948pt\hbox{$\displaystyle{{z}:{[\mathtt{n}]}}\vdash^{({0},{0},{1})}{{{z}\,{\mathop{!}{{\tt
I}}}}:{\mathtt{n}}}$}}}}\hskip 4.5pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=249.2285pt\hbox{\kern
2.70003pt$\mathtt{({bg_{c}})}$}}}\hbox{\kern 0.0pt\kern
85.51797pt\hbox{$\displaystyle{{z}:{[\mathtt{n}]}}\vdash^{({0},{1},{1})}{{\mathop{!}{({z}\,{\mathop{!}{{\tt
I}}})}}:{[\mathtt{n}]}}$}}}}\hskip 4.5pt plus 1.0fil\penalty 2$}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=510.31894pt\hbox{\kern
2.70003pt$\mathtt{({app_{c}})}$}}}\hbox{\kern 0.0pt\kern
206.56319pt\hbox{$\displaystyle{{z}:{[\mathtt{n}]}}\vdash^{({1},{1},{1})}{{{{\tt
K}}\,{(\mathop{!}{({z}\,{\mathop{!}{{\tt
I}}})})}}:{{[\,]}\to{\mathtt{n}}}}$}}}}\hskip 4.5pt plus 1.0fil\penalty
2\kern-36.00006pt\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern
0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
25.64pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=51.28pt\hbox{\kern
2.70003pt$\mathtt{({bg_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{}\vdash^{({0},{1},{0})}{{\mathop{!}{({{\tt
I}}\,{\mathop{!}{{\tt I}}})}}:{[\,]}}$}}}}\hskip 4.5pt plus 1.0fil\penalty
2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.225pt,depth=0.225pt,width=536.61588pt\hbox{\kern
2.70003pt$\mathtt{({app_{c}})}$}}}\hbox{\kern 0.0pt\kern
210.96165pt\hbox{$\displaystyle{{z}:{[\mathtt{n}]}}\vdash^{({2},{2},{1})}{{{{{\tt
K}}\,{(\mathop{!}{({z}\,{\mathop{!}{{\tt I}}})})}}\,{(\mathop{!}{({{\tt
I}}\,{\mathop{!}{{\tt I}}})})}}:{\mathtt{n}}}$}}}}$

Notice that the only persistent rules are $\mathtt{({bg_{p}})}$ and
$\mathtt{({app_{p}})}$, used to type ${z}\,{\mathop{!}{{\tt I}}}$. Indeed,
${z}\,{\mathop{!}{{\tt I}}}$ is the $\mathtt{f}$-normal form of
$t^{\prime}_{0}$.

##  7 Untyped Translations

CBN/CBV (untyped) encodings into the bang calculus [32], inspired from
Girard’s encodings, establish two translations $cbn$ and $cbv$, such that when
$t$ reduces to $u$ in CBN (resp. CBV), $cbn(t)$ reduces to $cbn(u)$ (resp.
$cbv(t)$ reduces to $cbv(u)$) in the bang calculus. These two encodings are
dual: CBN forbids reduction inside arguments, which are translated to bang
terms, while CBV forbids reduction under $\lambda$-abstractions, also
translated to bang terms.

In this paper we use alternative encodings. For CBN, we slightly adapt to
explicit substitutions Girard’s translation into LL [29]. The resulting
encoding preserves normal forms and is sound and complete with respect to the
standard (quantitative) type system in [28]. For CBV, we discard the original
encoding in [32] for two reasons: CBV normal forms are not necessarily
translated to normal forms in the bang calculus (see [32]), and levels of
terms (the level of $t$ is the number of $\mathop{!}{\\!}$ surrounding $t$)
are not preserved either (see [27]). We thus adopt the CBV encoding in [12]
which preserves normal forms as well as levels.

The CBN and CBV embedding into the $\lambda!$-calculus, written
${\\_}^{\mathtt{n}}$ and ${\\_}^{\mathtt{v}}$ resp., are inductively defined
as:

<EMAIL_ADDRESS>{(\lambda{x}.{t})}^{\mathtt{n}}&\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}&\lambda{x}.{{t}^{\mathtt{n}}}\\\
{({t}\,{u})}^{\mathtt{n}}&\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}&{{t}^{\mathtt{n}}}\,{\mathop{!}{{u}^{\mathtt{n}}}}\\\
{({t}[{x}\backslash{u}])}^{\mathtt{n}}&\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}&{{t}^{\mathtt{n}}}[{x}\backslash{\mathop{!}{{u}^{\mathtt{n}}}}]\end{array}&\begin{array}[]{rcl}{x}^{\mathtt{v}}&\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}&\mathop{!}{x}\\\
{(\lambda{x}.{t})}^{\mathtt{v}}&\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}&\mathop{!}{\lambda{x}.{{t}^{\mathtt{v}}}}\\\
{({t}\,{u})}^{\mathtt{v}}&\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}&\left\\{\begin{array}[]{ll}{{\mathtt{L}}\langle{s}\rangle}\,{{u}^{\mathtt{v}}}&\text{if
${t}^{\mathtt{v}}={\mathtt{L}}\langle{\mathop{!}{s}}\rangle$}\\\
{\mathop{\textnormal{der}}{({t}^{\mathtt{v}})}}\,{{u}^{\mathtt{v}}}&\text{otherwise}\end{array}\right.\\\
{({t}[{x}\backslash{u}])}^{\mathtt{v}}&\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}&{{t}^{\mathtt{v}}}[{x}\backslash{{u}^{\mathtt{v}}}]\end{array}\end{array}$

Both translations extend to list contexts $\mathtt{L}$ as expected. Remark
that there are no two consecutive $\mathop{!}{\\!}$ constructors in the image
of the translation. The CBN embedding extends Girard’s translation to ES,
while the CBV one is different. Indeed, the translation of an application
${t}\,{u}$ is usually defined as
${\mathop{\textnormal{der}}{({t}^{\mathtt{v}})}}\,{{u}^{\mathtt{v}}}$ (see
e.g. [26]). This definition does not preserve normal forms, i.e. ${x}\,{y}$ is
a $\mathtt{v}$-normal form but its translated version
${\mathop{\textnormal{der}}{(\mathop{!}{x})}}\,{\mathop{!}{y}}$ is not a
$\mathtt{f}$-normal form. We restore this fundamental property by using the
well-known notion of superdevelopment [10], so that $\mathtt{d!}$-reductions
are applied by the translation on the fly. Moreover, simulation of CBN/CBV in
the $\lambda!$-calculus also holds.

######  Lemma 7.1 (Simulation [12]).

Let $t\in\mathcal{T_{\lambda}}$.

  1. 1.

$t\not\rightarrow_{\mathtt{n}}$ implies
${t}^{\mathtt{n}}\not\rightarrow_{\mathtt{f}}$, and
$t\rightarrow_{\mathtt{n}}s$ implies
${t}^{\mathtt{n}}\rightarrow_{\mathtt{f}}{s}^{\mathtt{n}}$.

  2. 2.

$t\not\rightarrow_{\mathtt{v}}$ implies
${t}^{\mathtt{v}}\not\rightarrow_{\mathtt{f}}$, and
$t\rightarrow_{\mathtt{v}}s$ implies
${t}^{\mathtt{v}}\twoheadrightarrow_{\mathtt{f}}{s}^{\mathtt{v}}$.

######  Example 7.2.

Consider again $t_{0}={{{\tt K}}\,{({z}\,{{\tt I}})}}\,{({{\tt I}}\,{{\tt
I}})}$. To illustrate the CBN case (Lem. 7.1:1), notice that the reduction
sequence $t_{0}\twoheadrightarrow_{\mathsf{cbn}}{z}\,{{\tt I}}=s_{0}$ given in
Ex. 3.21 is translated to the sequence ${t_{0}}^{\mathtt{n}}={{{\tt
K}}\,{(\mathop{!}{({z}\,{\mathop{!}{{\tt I}}})})}}\,{(\mathop{!}{({{\tt
I}}\,{\mathop{!}{{\tt
I}}})})}=t^{\prime}_{0}\twoheadrightarrow_{\mathtt{f}}{z}\,{\mathop{!}{{\tt
I}}}={s_{0}}^{\mathtt{n}}$ given in Ex. 5.1.

To illustrate the CBV case (Lem. 7.1:2), consider the sequence
$t_{0}\twoheadrightarrow_{\mathsf{cbv}}{x}[{x}\backslash{{z}\,{{\tt
I}}}]=s_{1}$ in Ex. 4.27. Then for ${\tt
I}^{\prime}=\lambda{w}.{\mathop{!}{w}}$ we have:

$\begin{array}[]{l@{\enskip}l@{\enskip}l@{\enskip}l@{\enskip}l}{t_{0}}^{\mathtt{v}}&=&{\mathop{\textnormal{der}}{(\underline{{(\lambda{x}.{\mathop{!}{\lambda{y}.{\mathop{!}{x}}}})}\,{({z}\,{\mathop{!}{{\tt
I}^{\prime}}})}})}}\,{({{\tt I}^{\prime}}\,{\mathop{!}{{\tt
I}^{\prime}}})}&\rightarrow_{\mathtt{dB}}&{\underline{\mathop{\textnormal{der}}{({(\mathop{!}{\lambda{y}.{\mathop{!}{x}}})}[{x}\backslash{{z}\,{\mathop{!}{{\tt
I}^{\prime}}}}])}}}\,{({{\tt I}^{\prime}}\,{\mathop{!}{{\tt I}^{\prime}}})}\\\
&\rightarrow_{\mathtt{d!}}&\underline{{{(\lambda{y}.{\mathop{!}{x}})}[{x}\backslash{{z}\,{\mathop{!}{{\tt
I}^{\prime}}}}]}\,{({{\tt I}^{\prime}}\,{\mathop{!}{{\tt
I}^{\prime}}})}}&\rightarrow_{\mathtt{dB}}&{{(\mathop{!}{x})}[{y}\backslash{\underline{{{\tt
I}^{\prime}}\,{\mathop{!}{{\tt
I}^{\prime}}}}}]}[{x}\backslash{{z}\,{\mathop{!}{{\tt I}^{\prime}}}}]\\\
&\rightarrow_{\mathtt{dB}}&{\underline{{(\mathop{!}{x})}[{y}\backslash{{(\mathop{!}{w})}[{w}\backslash{\mathop{!}{{\tt
I}^{\prime}}}]}]}}[{x}\backslash{{z}\,{\mathop{!}{{\tt
I}^{\prime}}}}]&\rightarrow_{\mathtt{s!}}&{\underline{{(\mathop{!}{x})}[{w}\backslash{\mathop{!}{{\tt
I}^{\prime}}}]}}[{x}\backslash{{z}\,{\mathop{!}{{\tt I}^{\prime}}}}]\\\
&\rightarrow_{\mathtt{s!}}&{(\mathop{!}{x})}[{x}\backslash{{z}\,{\mathop{!}{{\tt
I}^{\prime}}}}]&=&{s_{1}}^{\mathtt{v}}\end{array}$

Notice how this sequence requires extra reduction steps with respect to the
one given in Ex. 4.27. Indeed, the $\mathtt{e}$-step
$\rightarrow_{\mathtt{d!}}$ in the $\lambda!$-calculus has no counterpart in
CBV.

##  8 Typed Translations

Call-by-Name. We study the correspondence between derivations in CBN and their
encodings in the $\lambda!$-calculus. First we inject the set of types for
$\mathcal{N}$ (generated by the base types $\mathtt{n}$ and $\mathtt{a}$) into
the set of types of $\mathcal{B}$ (generated also by the base type
$\mathtt{vl}$) by means of the function:
${\mathtt{n}}^{\mathtt{n}}\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}\mathtt{n}$,
${\mathtt{a}}^{\mathtt{n}}\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}\mathtt{a}$,
${({\mathcal{M}}\to{\sigma})}^{\mathtt{n}}\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}{{\mathcal{M}}^{\mathtt{n}}}\to{{\sigma}^{\mathtt{n}}}$
and ${[\sigma_{i}]_{i\in
I}}^{\mathtt{n}}\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}[{\sigma_{i}}^{\mathtt{n}}]_{i\in
I}$. Then we translate terms, using the function ${\\_}^{\mathtt{n}}$ from
Sec. 7. Translation of contexts is defined as expected:
${\Gamma}^{\mathtt{n}}=\\{{{x_{i}}:{{\mathcal{M}_{i}}^{\mathtt{n}}}}\\}_{i\in
I}$. Another notion is needed to restrict $\mathcal{B}$ derivations to those
that come from the translation of some $\mathcal{N}$ derivation. Indeed, a
$\mathcal{B}$ derivation $\Phi$ is _$\mathtt{n}$ -relevant_ if all the
contexts and types involved in $\Phi$ are in the image of the translation
${\\_}^{\mathtt{n}}$. We then obtain:

######  Theorem 8.1.

${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
if and only if
${\Phi^{\prime}}\rhd_{\mathcal{B}}{{{\Gamma}^{\mathtt{n}}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{{t}^{\mathtt{n}}}:{{\sigma}^{\mathtt{n}}}}}$
is $\mathtt{n}$-relevant.

######  Proof 8.2.

The left-to-right implication is by induction on $\Phi$ by analysing the last
rule applied.

  * •

$\mathtt{({app^{\mathcal{N}}_{p}})}$. Then we have $t={r}\,{u}$,
$\sigma=\mathtt{n}$ and $\mathit{s}=\mathit{s}^{\prime}+1$, and $\Phi$ is

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 5.88452pt\hbox{$\displaystyle\penalty
1{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}^{\prime}})}{{r}:{\mathtt{n}}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=57.74173pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{N}}_{p}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}^{\prime}+1})}{{{r}\,{u}}:{\mathtt{n}}}$}}}}$

By applying the i.h. on the premise we may construct $\Phi^{\prime}$

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{{\Gamma}^{\mathtt{n}}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}^{\prime}})}{{{r}^{\mathtt{n}}}:{{\mathtt{n}}^{\mathtt{n}}}}\hskip
5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 23.76787pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=47.53574pt\hbox{\kern
3.00003pt$\mathtt{({bg_{p}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{}\vdash^{({0},{0},{0})}{{\mathop{!}{{u}^{\mathtt{n}}}}:{{\mathtt{vl}}^{\mathtt{n}}}}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=155.72739pt\hbox{\kern
3.00003pt$\mathtt{({app_{p}})}$}}}\hbox{\kern 0.0pt\kern
41.3817pt\hbox{$\displaystyle{{\Gamma}^{\mathtt{n}}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}^{\prime}+1})}{{{{r}^{\mathtt{n}}}\,{\mathop{!}{{u}^{\mathtt{n}}}}}:{{\mathtt{n}}^{\mathtt{n}}}}$}}}}$

  * •

$\mathtt{({abs_{p}})}$. Then we have $t=\lambda{x}.{u}$,
$\Gamma={\Gamma_{1}}\mathrel{\setminus\\!\\!\setminus}{x}$,
$\sigma=\mathtt{a}$, $\mathit{s}=\mathit{s}^{\prime}+1$, and $\Phi$ is

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Gamma_{1}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}^{\prime}})}{{u}:{\mathtt{tt}}}\quad\mathsf{tight}(\Gamma_{1}(x))$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=113.08443pt\hbox{\kern
3.00003pt$\mathtt{({abs_{p}})}$}}}\hbox{\kern 0.0pt\kern
11.42293pt\hbox{$\displaystyle{{\Gamma_{1}}\mathrel{\setminus\\!\\!\setminus}{x}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}^{\prime}+1})}{{\lambda{x}.{u}}:{\mathtt{a}}}$}}}}$

By applying the i.h. on the premise we may construct $\Phi^{\prime}$

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{{\Gamma_{1}}^{\mathtt{n}}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}^{\prime}})}{{{u}^{\mathtt{n}}}:{{\mathtt{tt}}^{\mathtt{n}}}}\quad\mathsf{tight}({\Gamma_{1}}^{\mathtt{n}}(x))$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=122.75117pt\hbox{\kern
3.00003pt$\mathtt{({abs_{p}})}$}}}\hbox{\kern 0.0pt\kern
11.58963pt\hbox{$\displaystyle{{{\Gamma_{1}}^{\mathtt{n}}}\mathrel{\setminus\\!\\!\setminus}{x}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}^{\prime}+1})}{{\lambda{x}.{{u}^{\mathtt{n}}}}:{{\mathtt{a}}^{\mathtt{n}}}}$}}}}$

  * •

$\mathtt{({var_{c}})}$. Then $\Gamma={x}:{[\sigma]}$,
$\mathit{m}=\mathit{e}=\mathit{s}=0$, and $\Phi$ is

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 30.40428pt\hbox{$\displaystyle\penalty
1\vphantom{\Gamma}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=67.05858pt\hbox{\kern
3.00003pt$\mathtt{({var_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{x}:{[\sigma]}}\vdash^{({0},{0},{0})}{{x}:{\sigma}}$}}}}$

Then we construct $\Phi^{\prime}$

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 32.29324pt\hbox{$\displaystyle\penalty
1\vphantom{\Gamma}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm}
\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=70.8365pt\hbox{\kern
3.00003pt$\mathtt{({var_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{x}:{[{\sigma}^{\mathtt{n}}]}}\vdash^{({0},{0},{0})}{{{x}^{\mathtt{n}}}:{{\sigma}^{\mathtt{n}}}}$}}}}$

  * •

$\mathtt{({app^{\mathcal{N}}_{c}})}$. Then $t={r}\,{u}$,
$\Gamma={\Gamma_{1}}\mathrel{+_{i\in I}}{\Delta_{i}}$,
$\mathit{m}=1+\mathit{m}^{\prime}+_{i\in I}{\mathit{m}_{i}}$,
$\mathit{e}=1+\mathit{e}^{\prime}+_{i\in I}{\mathit{e}_{i}}$,
$\mathit{s}=\mathit{s}^{\prime}+_{i\in I}{\mathit{s}_{i}}$, and $\Phi$ is

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Gamma_{1}}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{r}:{{[\tau_{i}]_{i\in
I}}\to{\sigma}}}\quad({{\Delta_{i}}\vdash^{({\mathit{m}_{i}},{\mathit{e}_{i}},{\mathit{s}_{i}})}{{u}:{\tau_{i}}}})_{i\in
I}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=153.76823pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{N}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
7.17569pt\hbox{$\displaystyle{{\Gamma_{1}}\mathrel{+_{i\in
I}}{\Delta_{i}}}\vdash^{({1+\mathit{m}^{\prime}+_{i\in
I}{\mathit{m}_{i}}},{1+\mathit{e}^{\prime}+_{i\in
I}{\mathit{e}_{i}}},{\mathit{s}^{\prime}+_{i\in
I}{\mathit{s}_{i}}})}{{{r}\,{u}}:{\sigma}}$}}}}$

By applying the i.h. on all the premises we may construct $\Phi^{\prime}$

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{{\Gamma_{1}}^{\mathtt{n}}}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{{r}^{\mathtt{n}}}:{{[{\tau_{i}}^{\mathtt{n}}]_{i\in
I}}\to{{\sigma}^{\mathtt{n}}}}}\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\kern 0.0pt\hskip 0.0pt plus 0.0001fil\hbox{\kern
25.11107pt\hbox{$\displaystyle\penalty
1({{{\Delta_{i}}^{\mathtt{n}}}\vdash^{({\mathit{m}_{i}},{\mathit{e}_{i}},{\mathit{s}_{i}})}{{{u}^{\mathtt{n}}}:{{\tau_{i}}^{\mathtt{n}}}}})_{i\in
I}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=127.21237pt\hbox{\kern
3.00003pt$\mathtt{({bg_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{+_{i\in
I}{\Delta_{i}}^{\mathtt{n}}}\vdash^{({+_{i\in I}\mathit{m}_{i}},{1+_{i\in
I}\mathit{e}_{i}},{+_{i\in
I}\mathit{s}_{i}})}{{\mathop{!}{{u}^{\mathtt{n}}}}:{[{\tau_{i}}^{\mathtt{n}}]_{i\in
I}}}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=268.03156pt\hbox{\kern
3.00003pt$\mathtt{({app_{c}})}$}}}\hbox{\kern 0.0pt\kern
56.52953pt\hbox{$\displaystyle{{{\Gamma_{1}}^{\mathtt{n}}}\mathrel{+_{i\in
I}}{{\Delta_{i}}^{\mathtt{n}}}}\vdash^{({1+\mathit{m}^{\prime}+_{i\in
I}{\mathit{m}_{i}}},{1+\mathit{e}^{\prime}+_{i\in
I}{\mathit{e}_{i}}},{\mathit{s}^{\prime}+_{i\in
I}{\mathit{s}_{i}}})}{{{{r}^{\mathtt{n}}}\,{\mathop{!}{{u}^{\mathtt{n}}}}}:{{\sigma}^{\mathtt{n}}}}$}}}}$

  * •

$\mathtt{({abs_{c}})}$. Then $t=\lambda{x}.{u}$,
$\Gamma={\Gamma_{1}}\mathrel{\setminus\\!\\!\setminus}{x}$,
$\sigma={\Gamma_{1}(x)}\to{\tau}$, and $\Phi$ is

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 29.34804pt\hbox{$\displaystyle\penalty
1{\Gamma_{1}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{u}:{\tau}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=109.11766pt\hbox{\kern
3.00003pt$\mathtt{({abs_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{\Gamma_{1}}\mathrel{\setminus\\!\\!\setminus}{x}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{\lambda{x}.{u}}:{{\Gamma_{1}(x)}\to{\tau}}}$}}}}$

By applying the i.h. on the premise we may construct $\Phi^{\prime}$

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 33.6813pt\hbox{$\displaystyle\penalty
1{{\Gamma_{1}}^{\mathtt{n}}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{{u}^{\mathtt{n}}}:{{\tau}^{\mathtt{n}}}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=121.56212pt\hbox{\kern
3.00003pt$\mathtt{({abs_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{{\Gamma_{1}}^{\mathtt{n}}}\mathrel{\setminus\\!\\!\setminus}{x}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{\lambda{x}.{{u}^{\mathtt{n}}}}:{{{\Gamma_{1}}^{\mathtt{n}}(x)}\to{{\tau}^{\mathtt{n}}}}}$}}}}$

  * •

$\mathtt{({es^{\mathcal{N}}_{c}})}$. Then $t={r}[{x}\backslash{u}]$,
$\Gamma={{\Gamma_{1}}\mathrel{\setminus\\!\\!\setminus}{x}}\mathrel{+_{i\in
I}}{\Delta_{i}}$, $\mathit{m}=\mathit{m}^{\prime}+_{i\in I}{\mathit{m}_{i}}$,
$\mathit{e}=1+\mathit{e}^{\prime}+_{i\in I}{\mathit{e}_{i}}$,
$\mathit{s}=\mathit{s}^{\prime}+_{i\in I}{\mathit{s}_{i}}$, and $\Phi$ is

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 4.88208pt\hbox{$\displaystyle\penalty
1{\Gamma_{1};{x}:{[\tau_{i}]_{i\in
I}}}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{r}:{\sigma}}\quad({{\Delta_{i}}\vdash^{({\mathit{m}_{i}},{\mathit{e}_{i}},{\mathit{s}_{i}})}{{u}:{\tau_{i}}}})_{i\in
I}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=179.80298pt\hbox{\kern
3.00003pt$\mathtt{({es^{\mathcal{N}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{({\Gamma_{1}}\mathrel{\setminus\\!\\!\setminus}{x})}\mathrel{+_{i\in
I}}{\Delta_{i}}}\vdash^{({\mathit{m}^{\prime}+_{i\in
I}{\mathit{m}_{i}}},{1+\mathit{e}^{\prime}+_{i\in
I}{\mathit{e}_{i}}},{\mathit{s}^{\prime}+_{i\in
I}{\mathit{s}_{i}}})}{{{r}[{x}\backslash{u}]}:{\sigma}}$}}}}$

By applying the i.h. on all the premises we may construct $\Phi^{\prime}$

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{{\Gamma_{1}}^{\mathtt{n}};{x}:{[{\tau_{i}}^{\mathtt{n}}]_{i\in
I}}}\vdash^{({\mathit{m}^{\prime}},{\mathit{e}^{\prime}},{\mathit{s}^{\prime}})}{{{r}^{\mathtt{n}}}:{{\sigma}^{\mathtt{n}}}}\hskip
5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 25.11107pt\hbox{$\displaystyle\penalty
1({{{\Delta_{i}}^{\mathtt{n}}}\vdash^{({\mathit{m}_{i}},{\mathit{e}_{i}},{\mathit{s}_{i}})}{{{u}^{\mathtt{n}}}:{{\tau_{i}}^{\mathtt{n}}}}})_{i\in
I}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=127.21237pt\hbox{\kern
3.00003pt$\mathtt{({bg_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{+_{i\in
I}{\Delta_{i}}^{\mathtt{n}}}\vdash^{({+_{i\in I}\mathit{m}_{i}},{1+_{i\in
I}\mathit{e}_{i}},{+_{i\in
I}\mathit{s}_{i}})}{{\mathop{!}{{u}^{\mathtt{n}}}}:{[{\tau_{i}}^{\mathtt{n}}]_{i\in
I}}}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=281.52443pt\hbox{\kern
3.00003pt$\mathtt{({es_{c}})}$}}}\hbox{\kern 0.0pt\kern
43.0829pt\hbox{$\displaystyle{{({{\Gamma_{1}}^{\mathtt{n}}}\mathrel{\setminus\\!\\!\setminus}{x})}\mathrel{+_{i\in
I}}{{\Delta_{i}}^{\mathtt{n}}}}\vdash^{({\mathit{m}^{\prime}+_{i\in
I}{\mathit{m}_{i}}},{1+\mathit{e}^{\prime}+_{i\in
I}{\mathit{e}_{i}}},{\mathit{s}^{\prime}+_{i\in
I}{\mathit{s}_{i}}})}{{{{r}^{\mathtt{n}}}[{x}\backslash{\mathop{!}{{u}^{\mathtt{n}}}}]}:{{\sigma}^{\mathtt{n}}}}$}}}}$

In all cases, the resulting derivation is $\mathtt{n}$-relevant by the i.h.
and the fact that the $\mathtt{({es_{c}})}$ rule (in the last case) is used as
required.

The right-to-left implication is by induction on $\Phi^{\prime}$ by analysing
the last rule applied.

  * •

$\mathtt{({app_{p}})}$. Then $t={t_{1}}\,{u}$ with
${t}^{\mathtt{n}}={{t_{1}}^{\mathtt{n}}}\,{\mathop{!}{{u}^{\mathtt{n}}}}$,
$\Gamma={\Gamma_{1}}\mathrel{+}{\Gamma_{2}}$,
${\sigma}^{\mathtt{n}}=\mathtt{n}=\sigma$ and $\Phi^{\prime}$ is of the form

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi^{\prime}_{t_{1}}}\rhd_{\mathcal{B}}{{{\Gamma_{1}}^{\mathtt{n}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{{t_{1}}^{\mathtt{n}}}:{\mathtt{n}}}}\quad{\Phi^{\prime}_{u}}\rhd_{\mathcal{B}}{{{\Gamma_{2}}^{\mathtt{n}}}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{\mathop{!}{{u}^{\mathtt{n}}}}:{\overline{\mathtt{a}}}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=168.06705pt\hbox{\kern
3.00003pt$\mathtt{({app_{p}})}$}}}\hbox{\kern 0.0pt\kern
29.39122pt\hbox{$\displaystyle{{{\Gamma_{1}}^{\mathtt{n}}}\mathrel{+}{{\Gamma_{2}}^{\mathtt{n}}}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}},{\mathit{e}_{1}+\mathit{e}_{2}},{\mathit{s}_{1}+\mathit{s}_{2}+1})}{{{t}^{\mathtt{n}}}:{\mathtt{n}}}$}}}}$

where $\mathit{m}=\mathit{m}_{1}+\mathit{m}_{2}$,
$\mathit{e}=\mathit{e}_{1}+\mathit{e}_{2}$ and
$\mathit{s}=\mathit{s}_{1}+\mathit{s}_{2}+1$. Moreover, since
${u}^{\mathtt{n}}$ is typed with $\overline{\mathtt{a}}$, then the only
possible case is $\mathtt{vl}$, i.e. ${\Gamma_{2}}^{\mathtt{n}}=\emptyset$
(and thus $\Gamma_{2}=\emptyset$) and
$\mathit{m}_{2}=\mathit{e}_{2}=\mathit{s}_{2}=0$. Then, by the i.h. on
$\Phi^{\prime}_{t_{1}}$ we have
${\Phi_{t_{1}}}\rhd_{\mathcal{N}}{{\Gamma_{1}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{t_{1}}:{\mathtt{n}}}}$.
Finally, we derive $\Phi$ as follows

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{t_{1}}}\rhd_{\mathcal{N}}{{\Gamma_{1}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{t_{1}}:{\mathtt{n}}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=74.359pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{N}}_{p}})}$}}}\hbox{\kern 0.0pt\kern
7.84448pt\hbox{$\displaystyle{\Gamma_{1}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}+1})}{{t}:{\mathtt{n}}}$}}}}$

We conclude since $\Gamma=\Gamma_{1}$, $\mathit{m}=\mathit{m}_{1}$,
$\mathit{e}=\mathit{e}_{1}$ and $\mathit{s}=\mathit{s}_{1}+1$.

  * •

$\mathtt{({abs_{p}})}$. Then ${t}^{\mathtt{n}}=\lambda{x}.{{u}^{\mathtt{n}}}$
and $t=\lambda{x}.{u}$ and since $\Phi^{\prime}$ is $\mathtt{n}$-relevant,
then it has a premise of the form
${}\rhd_{\mathcal{B}}{{{\Gamma}^{\mathtt{n}};{x}:{{\mathtt{tt}_{0}}^{\mathtt{n}}}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}-1})}{{{t}^{\mathtt{n}}}:{{\mathtt{tt}_{1}}^{\mathtt{n}}}}}$.
The i.h.  gives
${}\rhd_{\mathcal{N}}{{\Gamma;{x}:{\mathtt{tt}_{0}}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}-1})}{{t}:{\mathtt{tt}_{1}}}}$.
We thus conclude
${}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\mathtt{a}}}}$
by rule $\mathtt{({abs_{p}})}$.

  * •

$\mathtt{({bg_{p}})}$. Then ${t}^{\mathtt{n}}=\mathop{!}{u}$, which is not
possible by definition. Hence this case does not apply.

  * •

$\mathtt{({dr_{p}})}$. Then ${t}^{\mathtt{n}}=\mathop{\textnormal{der}}{(u)}$
which is not possible by definition. Hence, this case does not apply.

  * •

$\mathtt{({es_{p}})}$. Then $t={r}[{x}\backslash{u}]$ with
${t}^{\mathtt{n}}={\mathop{!}{{r}^{\mathtt{n}}}}[{x}\backslash{{u}^{\mathtt{n}}}]$,
$\Gamma={\Gamma_{1}}\mathrel{+}{\Gamma_{2}}$ and $\Phi^{\prime}$ is of the
form

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi^{\prime}_{r}}\rhd_{\mathcal{B}}{{{\Gamma_{1}}^{\mathtt{n}};{x}:{\mathcal{M}^{\prime}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{{r}^{\mathtt{n}}}:{{\sigma}^{\mathtt{n}}}}}\quad{\Phi^{\prime}_{u}}\rhd_{\mathcal{B}}{{{\Gamma_{2}}^{\mathtt{n}}}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{\mathop{!}{{u}^{\mathtt{n}}}}:{{\mathtt{n}}^{\mathtt{n}}}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=195.35916pt\hbox{\kern
3.00003pt$\mathtt{({es_{p}})}$}}}\hbox{\kern 0.0pt\kern
44.98022pt\hbox{$\displaystyle{{{\Gamma_{1}}^{\mathtt{n}}}\mathrel{+}{{\Gamma_{2}}^{\mathtt{n}}}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}},{\mathit{e}_{1}+\mathit{e}_{2}},{\mathit{s}_{1}+\mathit{s}_{2}})}{{{t}^{\mathtt{n}}}:{{\sigma}^{\mathtt{n}}}}$}}}}$

with $\mathsf{tight}(\mathcal{M}^{\prime})$. This means in particular that
$\mathop{!}{{u}^{\mathtt{n}}}$ is typed with $\mathtt{n}$ which is not
possible by construction. So this case does not apply.

  * •

$\mathtt{({var_{c}})}$. Then ${t}^{\mathtt{n}}=x$ and $t=x$. We trivially
conclude with rule $\mathtt{({var_{c}})}$.

  * •

$\mathtt{({app_{c}})}$. Then $t={t_{1}}\,{u}$ with
${t}^{\mathtt{n}}={{t_{1}}^{\mathtt{n}}}\,{\mathop{!}{{u}^{\mathtt{n}}}}$, and
$\Gamma={\Gamma_{1}}\mathrel{+}{\Gamma_{2}}$. Since $\Phi^{\prime}$ is
$\mathtt{n}$-relevant, then it is of the form

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi^{\prime}_{r}}\rhd_{\mathcal{B}}{{{\Gamma_{1}}^{\mathtt{n}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{{t_{1}}^{\mathtt{n}}}:{{{\mathcal{M}}^{\mathtt{n}}}\to{{\sigma}^{\mathtt{n}}}}}}\quad{\Phi^{\prime}_{u}}\rhd_{\mathcal{B}}{{{\Gamma_{2}}^{\mathtt{n}}}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{\mathop{!}{{u}^{\mathtt{n}}}}:{{\mathcal{M}}^{\mathtt{n}}}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=195.89232pt\hbox{\kern
3.00003pt$\mathtt{({app_{c}})}$}}}\hbox{\kern 0.0pt\kern
38.29562pt\hbox{$\displaystyle{{\Gamma_{1}}\mathrel{+}{\Gamma_{2}}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}+1},{\mathit{e}_{1}+\mathit{e}_{2}},{\mathit{s}_{1}+\mathit{s}_{2}})}{{{t_{1}}\,{\mathop{!}{{u}^{\mathtt{n}}}}}:{{\sigma}^{\mathtt{n}}}}$}}}}$

Then, by the i.h. on $\Phi^{\prime}_{t_{1}}$ there exists a type derivation
${\Phi_{t_{1}}}\rhd_{\mathcal{N}}{{\Gamma_{1}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{t_{1}}:{{\mathcal{M}}\to{\sigma}}}}$.
On the other hand, $\Phi^{\prime}_{u}$ necessarily commes from a rule
$\mathtt{({dr_{c}})}$, and thus there exist type derivations
${\Phi^{i}_{u}}\rhd_{\mathcal{B}}{{{\Gamma^{i}_{2}}^{\mathtt{n}}}\vdash^{({\mathit{m}^{i}_{2}},{\mathit{e}^{i}_{2}},{\mathit{s}^{i}_{2}})}{{{u}^{\mathtt{n}}}:{{\sigma_{i}}^{\mathtt{n}}}}}$
with ${\mathcal{M}}^{\mathtt{n}}=[{\sigma_{i}}^{\mathtt{n}}]_{i\in I}$,
${\Gamma_{2}}^{\mathtt{n}}=+_{i\in I}{\Gamma^{i}_{2}}$,
$\mathit{m}_{2}=+_{i\in I}{\mathit{m}^{i}_{2}}$, $\mathit{e}_{2}=+_{i\in
I}{\mathit{e}^{i}_{2}}$ and $\mathit{s}_{2}=+_{i\in I}{\mathit{s}^{i}_{2}}$.
We conclude by applying $\mathtt{({app^{\mathcal{N}}_{c}})}$ to derive $\Phi$
as follows

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{t_{1}}}\rhd_{\mathcal{B}}{{\Gamma_{1}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}+1},{\mathit{s}_{1}})}{{t_{1}}:{[{\mathcal{M}}\to{\sigma}]}}}\quad({{\Phi^{i}_{u}}\rhd_{\mathcal{N}}{{\Gamma^{i}_{2}}\vdash^{({\mathit{m}^{i}_{2}},{\mathit{e}^{i}_{2}},{\mathit{s}^{i}_{2}})}{{u}:{\sigma_{i}}}}})_{i\in
I}$}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=207.54065pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{N}}_{p}})}$}}}\hbox{\kern 0.0pt\kern
80.34497pt\hbox{$\displaystyle{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}$}}}}$

  * •

$\mathtt{({appt_{c}})}$. This case is similar to the previous one, resorting
to the fact that $\mathsf{tight}({\mathcal{M}}^{\mathtt{n}})$ implies
$\mathsf{tight}(\mathcal{M})$.

  * •

$\mathtt{({abs_{c}})}$. Then ${t}^{\mathtt{n}}=\lambda{x}.{{u}^{\mathtt{n}}}$
and $t=\lambda{x}.{u}$ and since $\Phi^{\prime}$ is $\mathtt{n}$-relevant,
then it has a premise of the form
${}\rhd_{\mathcal{B}}{{{\Gamma}^{\mathtt{n}};{x}:{{\mathcal{M}}^{\mathtt{n}}}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{{t}^{\mathtt{n}}}:{{\tau}^{\mathtt{n}}}}}$.
The i.h.  gives
${}\rhd_{\mathcal{N}}{{\Gamma;{x}:{\mathcal{M}}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\tau}}}$.
We thus conclude
${}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{{\mathcal{M}}\to{\tau}}}}$
by rule $\mathtt{({abs_{c}})}$.

  * •

$\mathtt{({bg_{c}})}$. Then ${t}^{\mathtt{n}}=\mathop{!}{u}$, which is not
possible by definition. Hence this case does not apply.

  * •

$\mathtt{({dr_{c}})}$. Then
${t}^{\mathtt{n}}=\mathop{\textnormal{der}}{(t^{\prime})}$ which is not
possible by definition. Hence, this case does not apply.

  * •

$\mathtt{({es_{c}})}$. This case is similar to $\mathtt{({es_{p}})}$.

This result is illustrated by the tight type derivations in Ex. 3.21 and 6.3
for the terms $t_{0}$ and $t^{\prime}_{0}$ resp. Moreover, tightness is
preserved by the translation of contexts and types, hence:

######  Corollary 8.3.

If
${\Phi}\rhd_{\mathcal{N}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
is tight, then there exists ${p}\in\mathsf{no}_{{\tt scf}}$ such that
${t}^{\mathtt{n}}\twoheadrightarrow_{\mathtt{f}}^{(\mathit{m},\mathit{e})}p$
with $\mathit{m}$ $\mathtt{m}$-steps, $\mathit{e}$ $\mathtt{e}$-steps, and
$|{p}|_{\mathtt{f}}=\mathit{s}$. Conversely, if
${{\Phi^{\prime}}}\rhd_{\mathcal{B}}{{{\Gamma}^{\mathtt{n}}}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{{t}^{\mathtt{n}}}:{{\sigma}^{\mathtt{n}}}}}$
is tight and $\mathtt{n}$-relevant, then there exists
$p\in\mathsf{no}_{\mathtt{n}}$ such that
$t\twoheadrightarrow_{\mathtt{n}}^{(\mathit{m},\mathit{e})}p$ with
$\mathit{m}$ $\mathtt{m}$-steps, $\mathit{e}$ $\mathtt{e}$-steps, and
$|{p}|_{\mathtt{n}}=\mathit{s}$.

This result shows that not only from the tight type system $\mathcal{N}$ it is
possible to extract exact measures for the image of the CBN in the
$\lambda!$-calculus, but more interestingly, also that from the tight type
system $\mathcal{B}$ for the $\lambda!$-calculus it is possible to extract
exact measures for CBN. In this sense, the goal of encoding tight typing in a
unified framework is achieved.

Call-by-Value. In contrast with the CBN case, the set of type for system
$\mathcal{V}$ is not a subset of that for $\mathcal{B}$, and we need to
properly translate types. To that end, we introduce two mutually dependent
translations ${\\_}^{\overline{\mathtt{v}}}$ and ${\\_}^{\mathtt{v}}$:

<EMAIL_ADDRESS>$\mathtt{tt}\neq\mathtt{vr}$}\\\
{\mathtt{vr}}^{\overline{\mathtt{v}}}&\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}&\mathtt{n}\\\
{({\mathcal{M}}\to{\sigma})}^{\overline{\mathtt{v}}}&\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}&{{\mathcal{M}}^{\overline{\mathtt{v}}}}\to{{\sigma}^{\mathtt{v}}}\\\
{([\sigma]_{i\in
I})}^{\overline{\mathtt{v}}}&\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}&[{\sigma_{i}}^{\overline{\mathtt{v}}}]_{i\in
I}\end{array}&\begin{array}[]{rcll}{\mathtt{tt}}^{\mathtt{v}}&\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}&\mathtt{tt}&\text{if
$\mathtt{tt}\neq\mathtt{vr}$}\\\
{\mathtt{vr}}^{\mathtt{v}}&\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}&[\mathtt{n}]\\\
{({\mathcal{M}}\to{\sigma})}^{\mathtt{v}}&\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}&{{\mathcal{M}}^{\overline{\mathtt{v}}}}\to{{\sigma}^{\mathtt{v}}}\\\
{([\sigma]_{i\in
I})}^{\mathtt{v}}&\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}&[{\sigma_{i}}^{\overline{\mathtt{v}}}]_{i\in
I}\end{array}\end{array}$

Remark that ${\mathcal{M}}^{\overline{\mathtt{v}}}={\mathcal{M}}^{\mathtt{v}}$
for every multitype $\mathcal{M}$. Translation ${\\_}^{\overline{\mathtt{v}}}$
for a context $\Gamma$ is defined as expected:
${\Gamma}^{\overline{\mathtt{v}}}=\\{{{x_{i}}:{{\mathcal{M}_{i}}^{\overline{\mathtt{v}}}}}\\}_{i\in
I}$. To translate terms, we resort to the function ${\\_}^{\mathtt{v}}$
defined in Sec. 7. We also restrict $\mathcal{B}$ derivations to those that
come from the translation of some $\mathcal{V}$ derivation. Indeed, a
$\mathcal{B}$ derivation $\Phi$ is _$\mathtt{v}$ -relevant_ if:  (1) all the
contexts and types involved in $\Phi$ are in the image of the translations
${\\_}^{\overline{\mathtt{v}}}$ and ${\\_}^{\mathtt{v}}$ respectively; and
(2) rule $\mathtt{({dr_{c}})}$ is only applied to terms having a type of the
form $[{\mathcal{M}}\to{\tau}]$.  To state the preservation of typing
derivations between systems $\mathcal{V}$ and $\mathcal{B}$ we define measures
over type derivations in both systems to conveniently capture the relationship
between the exponential steps in the source and the target derivation. The
intuition is that we need to compensate for those $\mathtt{d!}$-redexes of the
$\lambda!$-calculus that might be introduced when translating. For all the
typing rules with two premises, we write $\Phi_{t}$ and $\Phi_{u}$ for the
first and second premise respectively. The first measure for system
$\mathcal{V}$ is given by induction on $\Phi$ as follows:  (1) for
$\mathtt{({var_{p}})}$,
$\mathtt{e}\\!\left({\Phi}\right)\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}1$;
(2) for $\mathtt{({val_{p}})}$, $\mathtt{({abs^{\mathcal{V}}_{p}})}$ and
$\mathtt{({var^{\mathcal{V}}_{c}})}$,
$\mathtt{e}\\!\left({\Phi}\right)\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}0$;
(3) for $\mathtt{({app^{\mathcal{V}}_{p}})}$,
$\mathtt{e}\\!\left({\Phi}\right)\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}\mathtt{e}\\!\left({\Phi_{t}}\right)+\mathtt{e}\\!\left({\Phi_{u}}\right)-1$
if $\mathsf{val}(t)$;  (4) for $\mathtt{({app^{\mathcal{V}}_{c}})}$ and
$\mathtt{({appt^{\mathcal{V}}_{c}})}$,
$\mathtt{e}\\!\left({\Phi}\right)\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}\mathtt{e}\\!\left({\Phi_{t}}\right)+\mathtt{e}\\!\left({\Phi_{u}}\right)+1$
if $\neg\mathsf{val}(t)$; and  (5) in any other case
$\mathtt{e}\\!\left({\Phi}\right)$ is defined as the sum of the recursive
calls over all premises.  The second measure for system $\mathcal{B}$ is also
defined by induction on $\Phi$ as follows:  (1) for $\mathtt{({bg_{p}})}$ and
$\mathtt{({var_{c}})}$,
$\widehat{\mathtt{e}}\\!\left({\Phi}\right)\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}0$;
(2) for $\mathtt{({app_{p}})}$,
$\widehat{\mathtt{e}}\\!\left({\Phi}\right)\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}\widehat{\mathtt{e}}\\!\left({\Phi_{t}}\right)+\widehat{\mathtt{e}}\\!\left({\Phi_{u}}\right)-1$
if $\mathsf{val}(t)$;  (3) for $\mathtt{({app_{c}})}$ and
$\mathtt{({appt_{c}})}$,
$\widehat{\mathtt{e}}\\!\left({\Phi}\right)\mathrel{\raisebox{-1.0pt}{$\stackrel{{\scriptstyle\textit{\tiny{def}}}}{{=}}$}}\widehat{\mathtt{e}}\\!\left({\Phi_{t}}\right)+\widehat{\mathtt{e}}\\!\left({\Phi_{u}}\right)+1$
if $\neg\mathsf{val}(t)$; and  (4) in any other case
$\widehat{\mathtt{e}}\\!\left({\Phi}\right)$ is defined as the sum of the
recursive calls over all premises.  Then, we obtain:

######  Theorem 8.4.

  1. 1.

If
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$,
then
${\Phi^{\prime}}\rhd_{\mathcal{B}}{{{\Gamma}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}},{\mathit{e}^{\prime}},{\mathit{s}})}{{{t}^{\mathtt{v}}}:{{\sigma}^{\mathtt{v}}}}}$
is $\mathtt{v}$-relevant with
$\mathit{e}^{\prime}=\mathit{e}+\mathtt{e}\\!\left({\Phi}\right)$.

  2. 2.

If
${\Phi^{\prime}}\rhd_{\mathcal{B}}{{{\Gamma}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}},{\mathit{e}^{\prime}},{\mathit{s}})}{{{t}^{\mathtt{v}}}:{{\sigma}^{\mathtt{v}}}}}$
is $\mathtt{v}$-relevant, then
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
with
$\mathit{e}=\mathit{e}^{\prime}-\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}}\right)$.

######  Proof 8.5.

  1. 1.

By induction on $\Phi$ by analysing the last rule applied.

     * •

$\mathtt{({var_{p}})}$. Then
${\Phi}\rhd_{\mathcal{V}}{{{x}:{[\mathtt{vr}]}}\vdash^{({0},{0},{0})}{{x}:{\mathtt{vr}}}}$
and ${t}^{\mathtt{v}}=\mathop{!}{x}$. We conclude by applying
$\mathtt{({var_{c}})}$ and $\mathtt{({bg_{c}})}$, obtaining
${\Phi^{\prime}}\rhd_{\mathcal{B}}{{{x}:{[\mathtt{n}]}}\vdash^{({0},{1},{0})}{{\mathop{!}{x}}:{[\mathtt{n}]}}}$,
which is trivially $\mathtt{v}$-relevant. The counters are as expected since
$\mathtt{e}\\!\left({\Phi}\right)=1$.

     * •

$\mathtt{({val_{p}})}$. Then
${\Phi}\rhd_{\mathcal{V}}{{}\vdash^{({0},{0},{0})}{{x}:{\mathtt{vl}}}}$ and
${t}^{\mathtt{v}}=\mathop{!}{x}$. We conclude by $\mathtt{({bg_{p}})}$ with
${\Phi^{\prime}}\rhd_{\mathcal{B}}{{}\vdash^{({0},{0},{0})}{{\mathop{!}{x}}:{\mathtt{vl}}}}$,
which is trivially $\mathtt{v}$-relevant. Note that the counters are as
expected since $\mathtt{e}\\!\left({\Phi}\right)=0$.

     * •

$\mathtt{({abs^{\mathcal{V}}_{p}})}$. Then
${\Phi}\rhd_{\mathcal{V}}{{}\vdash^{({0},{0},{0})}{{\lambda{x}.{r}}:{\mathtt{vl}}}}$
and ${t}^{\mathtt{v}}=\mathop{!}{\lambda{x}.{{r}^{\mathtt{v}}}}$. We conclude
by $\mathtt{({bg_{p}})}$ with
${\Phi^{\prime}}\rhd_{\mathcal{B}}{{}\vdash^{({0},{0},{0})}{{\mathop{!}{\lambda{x}.{{r}^{\mathtt{v}}}}}:{\mathtt{vl}}}}$,
which is trivially $\mathtt{v}$-relevant. Note that the counters are as
expected since $\mathtt{e}\\!\left({\Phi}\right)=0$.

     * •

$\mathtt{({app^{\mathcal{V}}_{p}})}$. Then $t={r}\,{u}$, $\sigma=\mathtt{n}$
and $\Phi$ is of the form

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma_{1}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\overline{\mathtt{vl}}}}}\quad{\Phi_{u}}\rhd_{\mathcal{V}}{{\Gamma_{2}}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{u}:{\overline{\mathtt{vr}}}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=153.94196pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{V}}_{p}})}$}}}\hbox{\kern 0.0pt\kern
22.71062pt\hbox{$\displaystyle{{\Gamma_{1}}\mathrel{+}{\Gamma_{2}}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}},{\mathit{e}_{1}+\mathit{e}_{2}},{\mathit{s}_{1}+\mathit{s}_{2}+1})}{{{r}\,{u}}:{\mathtt{n}}}$}}}}$

where $\mathit{e}=\mathit{e}_{1}+\mathit{e}_{2}$. By the i.h. we have
$\mathtt{v}$-relevant derivations
${\Phi^{\prime}_{r}}\rhd_{\mathcal{B}}{{{\Gamma_{1}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}^{\prime}_{1}},{\mathit{s}_{1}})}{{{r}^{\mathtt{v}}}:{{\overline{\mathtt{vl}}}^{\mathtt{v}}}}}$
and
${\Phi^{\prime}_{u}}\rhd_{\mathcal{B}}{{{\Gamma_{2}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{2}},{\mathit{e}^{\prime}_{2}},{\mathit{s}_{2}})}{{{u}^{\mathtt{v}}}:{{\overline{\mathtt{vr}}}^{\mathtt{v}}}}}$
with
$\mathit{e}^{\prime}_{1}=\mathit{e}_{1}+\mathtt{e}\\!\left({\Phi_{r}}\right)$
and
$\mathit{e}^{\prime}_{2}=\mathit{e}_{2}+\mathtt{e}\\!\left({\Phi_{u}}\right)$.
Moreover, since $u$ is typed with $\overline{\mathtt{vr}}$, then it is typed
with $\mathtt{n}$ or $\mathtt{vl}$, and thus
${\overline{\mathtt{vr}}}^{\mathtt{v}}=\overline{\mathtt{a}}$. There are three
possible cases for $r$:

       1. (a)

$r={\mathtt{L}}\langle{x}\rangle$. Then $\overline{\mathtt{vl}}=\mathtt{vr}$
with ${\overline{\mathtt{vl}}}^{\mathtt{v}}=[\mathtt{n}]$. Moreover, by
definition
${r}^{\mathtt{v}}={{\mathtt{L}}^{\mathtt{v}}}\langle{\mathop{!}{x}}\rangle$.
Thus, we have
${\Phi^{\prime}_{r}}\rhd_{\mathcal{B}}{{{\Gamma_{1}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}^{\prime}_{1}},{\mathit{s}_{1}})}{{{{\mathtt{L}}^{\mathtt{v}}}\langle{\mathop{!}{x}}\rangle}:{[\mathtt{n}]}}}$.
With a simple induction on $\mathtt{L}$ we can show that there exists a
$\mathtt{v}$-relevant type derivation
${\Phi^{\prime\prime}}\rhd_{\mathcal{B}}{{{\Gamma_{1}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}^{\prime}_{1}-1},{\mathit{s}_{1}})}{{{{\mathtt{L}}^{\mathtt{v}}}\langle{x}\rangle}:{\mathtt{n}}}}$,
that results from removing the occurrence of rule $\mathtt{({bg_{c}})}$ in the
base case. Finally, we conclude by applying $\mathtt{({app_{p}})}$ to derive a
$\mathtt{v}$-relevant derivation $\Phi^{\prime}$ as follows

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi^{\prime\prime}}\rhd_{\mathcal{B}}{{{\Gamma_{1}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}^{\prime}_{1}-1},{\mathit{s}_{1}})}{{{{\mathtt{L}}^{\mathtt{v}}}\langle{x}\rangle}:{\mathtt{n}}}}\quad{\Phi^{\prime}_{u}}\rhd_{\mathcal{B}}{{{\Gamma_{2}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{2}},{\mathit{e}^{\prime}_{2}},{\mathit{s}_{2}})}{{{u}^{\mathtt{v}}}:{\overline{\mathtt{a}}}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=184.85457pt\hbox{\kern
3.00003pt$\mathtt{({app_{p}})}$}}}\hbox{\kern 0.0pt\kern
67.94113pt\hbox{$\displaystyle{{\Gamma}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}},{\mathit{e}^{\prime}},{\mathit{s}})}{{{t}^{\mathtt{v}}}:{\mathtt{n}}}$}}}}$

where
$\mathit{e}^{\prime}=\mathit{e}^{\prime}_{1}-1+\mathit{e}^{\prime}_{2}=\mathit{e}_{1}+\mathtt{e}\\!\left({\Phi_{r}}\right)-1+\mathit{e}_{2}+\mathtt{e}\\!\left({\Phi_{u}}\right)=\mathit{e}+\mathtt{e}\\!\left({\Phi}\right)$
as expected.

       2. (b)

$r={\mathtt{L}}\langle{{r^{\prime}}\,{r^{\prime\prime}}}\rangle$. Then, we
have
${\Phi^{\prime}_{r}}\rhd_{\mathcal{B}}{{{\Gamma_{1}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}^{\prime}_{1}},{\mathit{s}_{1}})}{{{r}^{\mathtt{v}}}:{\mathtt{n}}}}$.
We conclude by applying $\mathtt{({dr_{p}})}$ and $\mathtt{({app_{p}})}$ to
derive $\Phi^{\prime}$ as follows

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 0.59389pt\hbox{$\displaystyle\penalty
1{\Phi^{\prime}_{r}}\rhd_{\mathcal{B}}{{{\Gamma_{1}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}^{\prime}_{1}},{\mathit{s}_{1}})}{{{r}^{\mathtt{v}}}:{\mathtt{n}}}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=77.84503pt\hbox{\kern
3.00003pt$\mathtt{({dr_{p}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{\Gamma_{1}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}^{\prime}_{1}},{\mathit{s}_{1}})}{{\mathop{\textnormal{der}}{({r}^{\mathtt{v}})}}:{\mathtt{n}}}$}}}}\hskip
5.0pt plus 1.0fil\penalty
2{\Phi^{\prime}_{u}}\rhd_{\mathcal{B}}{{{\Gamma_{2}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{2}},{\mathit{e}^{\prime}_{2}},{\mathit{s}_{2}})}{{{u}^{\mathtt{v}}}:{\overline{\mathtt{a}}}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=209.46193pt\hbox{\kern
3.00003pt$\mathtt{({app_{p}})}$}}}\hbox{\kern 0.0pt\kern
80.24481pt\hbox{$\displaystyle{{\Gamma}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}},{\mathit{e}^{\prime}},{\mathit{s}})}{{{t}^{\mathtt{v}}}:{\mathtt{n}}}$}}}}$

where $\mathit{e}^{\prime}=\mathit{e}^{\prime}_{1}+\mathit{e}^{\prime}_{2}$.
Hence,
$\mathit{e}^{\prime}=\mathit{e}^{\prime}_{1}+\mathit{e}^{\prime}_{2}=\mathit{e}_{1}+\mathtt{e}\\!\left({\Phi_{r}}\right)+\mathit{e}_{2}+\mathtt{e}\\!\left({\Phi_{u}}\right)=\mathit{e}+\mathtt{e}\\!\left({\Phi}\right)$
as expected. Notice that $\Phi^{\prime}$ is $\mathtt{v}$-relevant by the i.h.
and the fact that no $\mathtt{({dr_{c}})}$ rule was added in the final step.

       3. (c)

$r={\mathtt{L}}\langle{\lambda{x}.{r^{\prime}}}\rangle$. Then, it is
necessarily the case that $\Phi$ has a $\mathtt{v}$-relevant subderivation for
a judgement of the form
${\Gamma^{\prime\prime}}\vdash^{({\mathit{m}^{\prime\prime}},{\mathit{e}^{\prime\prime}},{\mathit{s}^{\prime\prime}})}{{\lambda{x}.{r^{\prime}}}:{\overline{\mathtt{vl}}}}$
for some appropriate $\Gamma^{\prime\prime}$, $\mathit{m}^{\prime\prime}$,
$\mathit{e}^{\prime\prime}$ and $\mathit{s}^{\prime\prime}$. Since
$\overline{\mathtt{vl}}$ is $\mathtt{vr}$ or $\mathtt{n}$, this leads to a
contradiction because abstractions cannot be assigned type $\mathtt{vr}$ or
$\mathtt{n}$ in system $\mathcal{V}$. Hence, this case does not apply.

     * •

$\mathtt{({es_{p}})}$. Then $t={r}[{x}\backslash{u}]$ and $\Phi$ is of the
form

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma_{1}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}\quad{\Phi_{u}}\rhd_{\mathcal{V}}{{\Gamma_{2}}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{u}:{\mathtt{n}}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=155.21162pt\hbox{\kern
3.00003pt$\mathtt{({es_{p}})}$}}}\hbox{\kern 0.0pt\kern
16.76413pt\hbox{$\displaystyle{{\Gamma_{1}}\mathrel{+}{\Gamma_{2}}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}},{\mathit{e}_{1}+\mathit{e}_{2}},{\mathit{s}_{1}+\mathit{s}_{2}})}{{{r}[{x}\backslash{u}]}:{\sigma}}$}}}}$

with $\mathsf{tight}(\Gamma_{1}(x))$ and
$\mathit{e}=\mathit{e}_{1}+\mathit{e}_{2}$. By the i.h. on $\Phi_{u}$ there
exists a $\mathtt{v}$-relevant derivation
${\Phi^{\prime}_{u}}\rhd_{\mathcal{B}}{{{\Gamma_{2}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{2}},{\mathit{e}^{\prime}_{2}},{\mathit{s}_{2}})}{{{u}^{\mathtt{v}}}:{\mathtt{n}}}}$
with
$\mathit{e}^{\prime}_{2}=\mathit{e}_{2}+\mathtt{e}\\!\left({\Phi_{u}}\right)$.
By the i.h. again there exists a $\mathtt{v}$-relevant derivation
${\Phi^{\prime}_{r}}\rhd_{\mathcal{B}}{{{\Gamma_{1}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}^{\prime}_{1}},{\mathit{s}_{1}})}{{{r}^{\mathtt{v}}}:{{\sigma}^{\mathtt{v}}}}}$
with
$\mathit{e}^{\prime}_{1}=\mathit{e}_{1}+\mathtt{e}\\!\left({\Phi_{r}}\right)$.
Thus, we conclude by applying $\mathtt{({es_{p}})}$ with $\Phi^{\prime}_{r}$,
$\Phi^{\prime}_{u}$ and
$\mathsf{tight}({\Gamma_{1}}^{\overline{\mathtt{v}}}(x))$, hence obtaining the
$\mathtt{v}$-relevant derivation
${\Phi^{\prime}}\rhd_{\mathcal{B}}{{{\Gamma}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}},{\mathit{e}^{\prime}},{\mathit{s}})}{{{t}^{\mathtt{v}}}:{{\sigma}^{\mathtt{v}}}}}$
where
$\mathit{e}^{\prime}=\mathit{e}^{\prime}_{1}+\mathit{e}^{\prime}_{2}=\mathit{e}_{1}+\mathtt{e}\\!\left({\Phi_{r}}\right)+\mathit{e}_{2}+\mathtt{e}\\!\left({\Phi_{u}}\right)=\mathit{e}+\mathtt{e}\\!\left({\Phi}\right)$
as expected.

     * •

$\mathtt{({var^{\mathcal{V}}_{c}})}$. Then
${\Phi}\rhd_{\mathcal{V}}{{{x}:{\mathcal{M}}}\vdash^{({0},{1},{0})}{{x}:{\mathcal{M}}}}$
with $\mathcal{M}=[\sigma_{i}]_{i\in I}$. We conclude by
$\mathtt{({var_{c}})}$ and $\mathtt{({bg_{c}})}$, deriving a
$\mathtt{v}$-relevant derivation $\Phi^{\prime}$ as follows

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\left(\raisebox{-10.00002pt}{ \hskip
5.0pt plus 1.0fil{ tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 38.06972pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt
plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=76.13943pt\hbox{\kern
3.00003pt$\mathtt{({var_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{x}:{[{\sigma_{i}}^{\overline{\mathtt{v}}}]}}\vdash^{({0},{0},{0})}{{x}:{{\sigma_{i}}^{\overline{\mathtt{v}}}}}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2 }\right)_{i\in I}$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=162.83104pt\hbox{\kern
3.00003pt$\mathtt{({bg_{c}})}$}}}\hbox{\kern 0.0pt\kern
45.98912pt\hbox{$\displaystyle{{x}:{{\mathcal{M}}^{\overline{\mathtt{v}}}}}\vdash^{({0},{1},{0})}{{\mathop{!}{x}}:{{\mathcal{M}}^{\overline{\mathtt{v}}}}}$}}}}$

Note that the counters are as expected since
$\mathtt{e}\\!\left({\Phi}\right)=0$. We conclude since
${\mathcal{M}}^{\overline{\mathtt{v}}}={\mathcal{M}}^{\mathtt{v}}$.

     * •

$\mathtt{({app^{\mathcal{V}}_{c}})}$. Then $t={r}\,{u}$ and $\Phi$ is of the
form

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma_{1}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{[{\mathcal{M}}\to{\sigma}]}}}\quad{\Phi_{u}}\rhd_{\mathcal{V}}{{\Gamma_{2}}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{u}:{\mathcal{M}}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=181.32272pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
32.59953pt\hbox{$\displaystyle{{\Gamma_{1}}\mathrel{+}{\Gamma_{2}}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}+1},{\mathit{e}_{1}+\mathit{e}_{2}-1},{\mathit{s}_{1}+\mathit{s}_{2}})}{{{r}\,{u}}:{\sigma}}$}}}}$

where $\mathit{m}=\mathit{m}_{1}+\mathit{m}_{2}+1$,
$\mathit{e}=\mathit{e}_{1}+\mathit{e}_{2}-1$, and
$\mathit{s}=\mathit{s}_{1}+\mathit{s}_{2}$. By the i.h. on $\Phi_{u}$ there
exists a $\mathtt{v}$-relevant derivation
${\Phi^{\prime}_{u}}\rhd_{\mathcal{B}}{{{\Gamma_{2}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{2}},{\mathit{e}^{\prime}_{2}},{\mathit{s}_{2}})}{{{u}^{\mathtt{v}}}:{{\mathcal{M}}^{\mathtt{v}}}}}$
with
$\mathit{e}^{\prime}_{2}=\mathit{e}_{2}+\mathtt{e}\\!\left({\Phi_{u}}\right)$.
And by the i.h. on $\Phi_{r}$ there exists a $\mathtt{v}$-relevant derivation
${\Phi^{\prime}_{r}}\rhd_{\mathcal{B}}{{{\Gamma_{1}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}^{\prime}_{1}},{\mathit{s}_{1}})}{{{r}^{\mathtt{v}}}:{[{{\mathcal{M}}^{\overline{\mathtt{v}}}}\to{{\sigma}^{\mathtt{v}}}]}}}$
with
$\mathit{e}^{\prime}_{1}=\mathit{e}_{1}+\mathtt{e}\\!\left({\Phi_{r}}\right)$.
We should consider two cases based on the shape of $r$:

       1. (a)

$r={\mathtt{L}}\langle{v}\rangle$. Then
${r}^{\mathtt{v}}={{\mathtt{L}}^{\mathtt{v}}}\langle{\mathop{!}{r^{\prime}}}\rangle$
and
${t}^{\mathtt{v}}={{{\mathtt{L}}^{\mathtt{v}}}\langle{r^{\prime}}\rangle}\,{{u}^{\mathtt{v}}}$.
With a simple induction on $\mathtt{L}$ we can show from $\Phi^{\prime}_{r}$
that there exists a $\mathtt{v}$-relevant type derivation
${\Phi^{\prime\prime}}\rhd_{\mathcal{B}}{{{\Gamma_{1}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}^{\prime}_{1}-1},{\mathit{s}_{1}})}{{{{\mathtt{L}}^{\mathtt{v}}}\langle{r^{\prime}}\rangle}:{{{\mathcal{M}}^{\overline{\mathtt{v}}}}\to{{\sigma}^{\mathtt{v}}}}}}$,
that results from removing the occurrence of rule $\mathtt{({bg_{c}})}$ in the
base case. Finally, since
${\mathcal{M}}^{\overline{\mathtt{v}}}={\mathcal{M}}^{\mathtt{v}}$, we
conclude by applying $\mathtt{({app_{c}})}$ with $\Phi^{\prime\prime}$ and
$\Phi_{u}$ to derive a $\mathtt{v}$-relevant derivation
${\Phi^{\prime}}\rhd_{\mathcal{B}}{{{\Gamma}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}},{\mathit{e}^{\prime}},{\mathit{s}})}{{{t}^{\mathtt{v}}}:{{\sigma}^{\mathtt{v}}}}}$
where
$\mathit{e}^{\prime}=\mathit{e}^{\prime}_{1}-1+\mathit{e}^{\prime}_{2}=\mathit{e}_{1}+\mathtt{e}\\!\left({\Phi_{r}}\right)-1+\mathit{e}_{2}+\mathtt{e}\\!\left({\Phi_{u}}\right)=\mathit{e}+\mathtt{e}\\!\left({\Phi}\right)$
as expected.

       2. (b)

$r\neq{\mathtt{L}}\langle{v}\rangle$. Then
${t}^{\mathtt{v}}={\mathop{\textnormal{der}}{({r}^{\mathtt{v}})}}\,{{u}^{\mathtt{v}}}$.
Since ${\mathcal{M}}^{\overline{\mathtt{v}}}={\mathcal{M}}^{\mathtt{v}}$, we
conclude by deriving $\Phi^{\prime}$ as follows

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi^{\prime}_{r}}\rhd_{\mathcal{B}}{{{\Gamma_{1}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}^{\prime}_{1}},{\mathit{s}_{1}})}{{{r}^{\mathtt{v}}}:{[{{\mathcal{M}}^{\overline{\mathtt{v}}}}\to{{\sigma}^{\mathtt{v}}}]}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=103.49367pt\hbox{\kern
3.00003pt$\mathtt{({dr_{c}})}$}}}\hbox{\kern 0.0pt\kern
2.18388pt\hbox{$\displaystyle{{\Gamma_{1}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}^{\prime}_{1}},{\mathit{s}_{1}})}{{\mathop{\textnormal{der}}{({r}^{\mathtt{v}})}}:{{{\mathcal{M}}^{\overline{\mathtt{v}}}}\to{{\sigma}^{\mathtt{v}}}}}$}}}}\hskip
5.0pt plus 1.0fil\penalty
2{\Phi^{\prime}_{u}}\rhd_{\mathcal{B}}{{{\Gamma_{2}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{2}},{\mathit{e}^{\prime}_{2}},{\mathit{s}_{2}})}{{{u}^{\mathtt{v}}}:{{\mathcal{M}}^{\mathtt{v}}}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=241.61058pt\hbox{\kern
3.00003pt$\mathtt{({app_{c}})}$}}}\hbox{\kern 0.0pt\kern
94.76207pt\hbox{$\displaystyle{{\Gamma}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}},{\mathit{e}^{\prime}},{\mathit{s}})}{{{t}^{\mathtt{v}}}:{{\sigma}^{\mathtt{v}}}}$}}}}$

where
$\mathit{e}^{\prime}=\mathit{e}^{\prime}_{1}+\mathit{e}^{\prime}_{2}=\mathit{e}_{1}+\mathtt{e}\\!\left({\Phi_{r}}\right)+\mathit{e}_{2}+\mathtt{e}\\!\left({\Phi_{u}}\right)=\mathit{e}+1+\mathtt{e}\\!\left({\Phi_{r}}\right)+\mathtt{e}\\!\left({\Phi_{u}}\right)=\mathit{e}+\mathtt{e}\\!\left({\Phi}\right)$
as expected. Notice that the resulting derivation $\Phi^{\prime}$ is
$\mathtt{v}$-relevantsince the added $\mathtt{({dr_{c}})}$ rule acts on a
multiset of the required form.

     * •

$\mathtt{({appt^{\mathcal{V}}_{c}})}$. This case is similar to the previous
one.

     * •

$\mathtt{({abs^{\mathcal{V}}_{c}})}$. Then $t=\lambda{x}.{r}$ and $\Phi$ is of
the form

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 42.07019pt\hbox{$\displaystyle\penalty
1({{\Phi_{i}}\rhd_{\mathcal{V}}{{\Gamma_{i}}\vdash^{({\mathit{m}_{i}},{\mathit{e}_{i}},{\mathit{s}_{i}})}{{r}:{\tau_{i}}}}})_{i\in
I}$}}\hskip 0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=175.46344pt\hbox{\kern
3.00003pt$\mathtt{({abs^{\mathcal{V}}_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{}\mathrel{+_{i\in
I}}{{\Gamma_{i}}\mathrel{\setminus\\!\\!\setminus}{x}}}\vdash^{({+_{i\in
I}{\mathit{m}_{i}}},{1+_{i\in I}{\mathit{e}_{i}}},{+_{i\in
I}{\mathit{s}_{i}}})}{{\lambda{x}.{r}}:{[{\Gamma_{i}(x)}\to{\tau_{i}}]_{i\in
I}}}$}}}}$

where $\mathit{e}=1+_{i\in I}{\mathit{e}_{i}}$. By the i.h. there exists a
derivation
${\Phi^{\prime}_{i}}\rhd_{\mathcal{B}}{{{\Gamma_{i}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{i}},{\mathit{e}^{\prime}_{i}},{\mathit{s}_{i}})}{{{r}^{\mathtt{v}}}:{{\tau_{i}}^{\mathtt{v}}}}}$,
which is $\mathtt{v}$-relevant, where
$\mathit{e}^{\prime}_{i}=\mathit{e}_{i}+\mathtt{e}\\!\left({\Phi_{i}}\right)$
for each $i\in I$. We then conclude by applying $\mathtt{({abs_{c}})}$ and
$\mathtt{({bg_{c}})}$, hence deriving a $\mathtt{v}$-relevant derivation
$\Phi^{\prime}$ as follows

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\left(\raisebox{-10.00002pt}{ \hskip
5.0pt plus 1.0fil{ tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{\kern 23.43703pt\hbox{$\displaystyle\penalty
1{\Phi^{\prime}_{i}}\rhd_{\mathcal{B}}{{{\Gamma_{i}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{i}},{\mathit{e}^{\prime}_{i}},{\mathit{s}_{i}})}{{{r}^{\mathtt{v}}}:{{\tau_{i}}^{\mathtt{v}}}}}$}}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=125.36627pt\hbox{\kern
3.00003pt$\mathtt{({abs_{c}})}$}}}\hbox{\kern 0.0pt\kern
0.0pt\hbox{$\displaystyle{{{\Gamma_{i}}^{\overline{\mathtt{v}}}}\mathrel{\setminus\\!\\!\setminus}{x}}\vdash^{({\mathit{m}_{i}},{\mathit{e}^{\prime}_{i}},{\mathit{s}_{i}})}{{\lambda{x}.{{r}^{\mathtt{v}}}}:{{{\Gamma_{i}(x)}^{\overline{\mathtt{v}}}}\to{{\tau_{i}}^{\mathtt{v}}}}}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2 }\right)_{i\in I}$}\hskip 0.0pt plus
0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=212.91898pt\hbox{\kern
3.00003pt$\mathtt{({bg_{c}})}$}}}\hbox{\kern 0.0pt\kern
20.2469pt\hbox{$\displaystyle{{}\mathrel{+_{i\in
I}}{{{\Gamma_{i}}^{\overline{\mathtt{v}}}}\mathrel{\setminus\\!\\!\setminus}{x}}}\vdash^{({+_{i\in
I}{\mathit{m}_{i}}},{1+_{i\in I}{\mathit{e}^{\prime}_{i}}},{+_{i\in
I}{\mathit{s}_{i}}})}{{{t}^{\mathtt{v}}}:{{[{\Gamma_{i}(x)}\to{\tau_{i}}]_{i\in
I}}^{\mathtt{v}}}}$}}}}$

taking $\mathit{e}^{\prime}=1+_{i\in I}{\mathit{e}^{\prime}_{i}}=1+_{i\in
I}{(\mathit{e}_{i}+\mathtt{e}\\!\left({\Phi_{i}}\right))}=\mathit{e}+\mathtt{e}\\!\left({\Phi}\right)$
as expected.

     * •

$\mathtt{({es_{c}})}$. This case is similar to $\mathtt{({es_{p}})}$.

  1. 1.

By induction on $\Phi^{\prime}$ analysing the last rule applied.

     * •

$\mathtt{({app_{p}})}$. Then $t={t_{1}}\,{u}$ with
${t}^{\mathtt{v}}={r}\,{{u}^{\mathtt{v}}}$ for some term $r$,
$\Gamma={\Gamma_{1}}\mathrel{+}{\Gamma_{2}}$,
${\sigma}^{\mathtt{v}}=\mathtt{n}=\sigma$ and $\Phi^{\prime}$ is of the form

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi^{\prime}_{r}}\rhd_{\mathcal{B}}{{{\Gamma_{1}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}^{\prime}_{1}},{\mathit{s}_{1}})}{{r}:{\mathtt{n}}}}\quad{\Phi^{\prime}_{u}}\rhd_{\mathcal{B}}{{{\Gamma_{2}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{2}},{\mathit{e}^{\prime}_{2}},{\mathit{s}_{2}})}{{{u}^{\mathtt{v}}}:{\overline{\mathtt{a}}}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=160.73862pt\hbox{\kern
3.00003pt$\mathtt{({app_{p}})}$}}}\hbox{\kern 0.0pt\kern
25.63588pt\hbox{$\displaystyle{{{\Gamma_{1}}^{\overline{\mathtt{v}}}}\mathrel{+}{{\Gamma_{2}}^{\overline{\mathtt{v}}}}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}},{\mathit{e}^{\prime}_{1}+\mathit{e}^{\prime}_{2}},{\mathit{s}_{1}+\mathit{s}_{2}+1})}{{{t}^{\mathtt{v}}}:{\mathtt{n}}}$}}}}$

where $\mathit{e}^{\prime}=\mathit{e}^{\prime}_{1}+\mathit{e}^{\prime}_{2}$.
Moreover, since ${u}^{\mathtt{v}}$ is typed with $\overline{\mathtt{a}}$, then
it is typed with $\mathtt{n}$ or $\mathtt{vl}$, i.e.
${\overline{\mathtt{vr}}}^{\mathtt{v}}$. Then, by the i.h. on
$\Phi^{\prime}_{u}$ we have
${\Phi_{u}}\rhd_{\mathcal{V}}{{\Gamma_{2}}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{u}:{\overline{\mathtt{vr}}}}}$
with
$\mathit{e}_{2}=\mathit{e}^{\prime}_{2}-\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{u}}\right)$.
There are two possible cases for ${t_{1}}^{\mathtt{v}}$ and, hence, for $r$:

       1. (a)

${t_{1}}^{\mathtt{v}}={{\mathtt{L}}^{\mathtt{v}}}\langle{\mathop{!}{r^{\prime}}}\rangle$
(i.e. $\mathsf{val}(t_{1})$). Then,
$r={{\mathtt{L}}^{\mathtt{v}}}\langle{r^{\prime}}\rangle$. Moreover, by a
simple induction on $\mathtt{L}$, from $\Phi^{\prime}_{r}$ we get the
$\mathtt{v}$-relevant type derivation
${\Phi^{\prime}_{t_{1}}}\rhd_{\mathcal{B}}{{{\Gamma_{1}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}^{\prime}_{1}+1},{\mathit{s}_{1}})}{{{{\mathtt{L}}^{\mathtt{v}}}\langle{\mathop{!}{r^{\prime}}}\rangle}:{[\mathtt{n}]}}}$
such that
$\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{t_{1}}}\right)=\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{r}}\right)$.
Note that $[\mathtt{n}]={\mathtt{vr}}^{\mathtt{v}}$. Then, by the i.h. we get
${\Phi_{t_{1}}}\rhd_{\mathcal{V}}{{\Gamma_{1}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}+1},{\mathit{s}_{1}})}{{t_{1}}:{\mathtt{vr}}}}$
with
$\mathit{e}_{1}=\mathit{e}^{\prime}_{1}-\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{t_{1}}}\right)=\mathit{e}^{\prime}_{1}-\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{r}}\right)$.
Finally, we conclude by applying $\mathtt{({app^{\mathcal{V}}_{p}})}$ to
derive $\Phi$ as follows

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{t_{1}}}\rhd_{\mathcal{V}}{{\Gamma_{1}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}+1},{\mathit{s}_{1}})}{{t_{1}}:{\mathtt{vr}}}}\quad{\Phi_{u}}\rhd_{\mathcal{V}}{{\Gamma_{2}}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{u}:{\overline{\mathtt{vr}}}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=167.85391pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{V}}_{p}})}$}}}\hbox{\kern 0.0pt\kern
61.96974pt\hbox{$\displaystyle{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\mathtt{n}}}$}}}}$

where
$\mathit{e}=\mathit{e}_{1}+1+\mathit{e}_{2}=\mathit{e}^{\prime}_{1}-\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{r}}\right)+1+\mathit{e}^{\prime}_{2}-\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{u}}\right)=\mathit{e}^{\prime}_{1}+\mathit{e}^{\prime}_{2}-(\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{r}}\right)+\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{u}}\right)-1)=\mathit{e}^{\prime}-\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}}\right)$
as expected.

       2. (b)

${t_{1}}^{\mathtt{v}}\neq{\mathtt{L}}\langle{\mathop{!}{r^{\prime}}}\rangle$
(i.e. $\neg\mathsf{val}(t_{1})$). Then,
$r=\mathop{\textnormal{der}}{({t_{1}}^{\mathtt{v}})}$. Since $\Phi^{\prime}$
is $\mathtt{v}$-relevant, it is necessarily the case where $\Phi^{\prime}_{r}$
comes from an application of rule $\mathtt{({dr_{p}})}$. Moreover,
$\mathtt{n}={\mathtt{n}}^{\mathtt{v}}$, hence we have a $\mathtt{v}$-relevant
type derivation
${\Phi^{\prime}_{t_{1}}}\rhd_{\mathcal{B}}{{{\Gamma_{1}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}^{\prime}_{1}},{\mathit{s}_{1}})}{{{t_{1}}^{\mathtt{v}}}:{{\mathtt{n}}^{\mathtt{v}}}}}$
satisfying the hypothesis of the theorem. By the i.h. we get a type derivation
${\Phi_{t_{1}}}\rhd_{\mathcal{V}}{{\Gamma_{1}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{t_{1}}:{\mathtt{n}}}}$
with
$\mathit{e}_{1}=\mathit{e}^{\prime}_{1}-\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{t_{1}}}\right)=\mathit{e}^{\prime}_{1}-\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{r}}\right)$.
We conclude by applying $\mathtt{({app^{\mathcal{V}}_{p}})}$ to derive $\Phi$

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi_{t_{1}}}\rhd_{\mathcal{V}}{{\Gamma_{1}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{t_{1}}:{\mathtt{n}}}}\quad{\Phi_{u}}\rhd_{\mathcal{V}}{{\Gamma_{2}}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{u}:{\overline{\mathtt{vr}}}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=157.05945pt\hbox{\kern
3.00003pt$\mathtt{({app^{\mathcal{V}}_{p}})}$}}}\hbox{\kern 0.0pt\kern
56.57251pt\hbox{$\displaystyle{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\mathtt{n}}}$}}}}$

where
$\mathit{e}=\mathit{e}_{1}+\mathit{e}_{2}=\mathit{e}^{\prime}_{1}-\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{r}}\right)+\mathit{e}^{\prime}_{2}-\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{u}}\right)=\mathit{e}^{\prime}_{1}+\mathit{e}^{\prime}_{2}-(\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{r}}\right)+\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{u}}\right))=\mathit{e}^{\prime}-\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}}\right)$
as expected.

     * •

$\mathtt{({abs_{p}})}$. Then ${t}^{\mathtt{v}}=\lambda{x}.{t^{\prime}}$ which
is not possible by definition. Hence, this case does not apply.

     * •

$\mathtt{({bg_{p}})}$. Then ${t}^{\mathtt{v}}=\mathop{!}{t^{\prime}}$,
${\sigma}^{\mathtt{v}}=\mathtt{vl}=\sigma$ and
${\Phi^{\prime}}\rhd_{\mathcal{B}}{{}\vdash^{({0},{0},{0})}{{\mathop{!}{t^{\prime}}}:{\mathtt{vl}}}}$.
There are two possible cases: either  (1) $t=x=t^{\prime}$; or  (2)
$t=\lambda{x}.{u}$with $t^{\prime}=\lambda{x}.{{u}^{\mathtt{v}}}$.  We resort
to $\mathtt{({val_{p}})}$ or $\mathtt{({abs^{\mathcal{V}}_{p}})}$ resp. to
conclude with
${\Phi}\rhd_{\mathcal{V}}{{}\vdash^{({0},{0},{0})}{{t}:{\mathtt{vl}}}}$. Note
that the counters are as expected since
$\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}}\right)=0$.

     * •

$\mathtt{({dr_{p}})}$. Then
${t}^{\mathtt{v}}=\mathop{\textnormal{der}}{(t^{\prime})}$ which is not
possible by definition. Hence, this case does not apply.

     * •

$\mathtt{({es_{p}})}$. Then $t={r}[{x}\backslash{u}]$ with
${t}^{\mathtt{v}}={{r}^{\mathtt{v}}}[{x}\backslash{{u}^{\mathtt{v}}}]$,
$\Gamma={\Gamma_{1}}\mathrel{+}{\Gamma_{2}}$ and $\Phi^{\prime}$ is of the
form

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1{\Phi^{\prime}_{r}}\rhd_{\mathcal{B}}{{{\Gamma_{1}}^{\overline{\mathtt{v}}};{x}:{\mathcal{M}^{\prime}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}^{\prime}_{1}},{\mathit{s}_{1}})}{{{r}^{\mathtt{v}}}:{{\sigma}^{\mathtt{v}}}}}\quad{\Phi^{\prime}_{u}}\rhd_{\mathcal{B}}{{{\Gamma_{2}}^{\overline{\mathtt{v}}}}\vdash^{({\mathit{m}_{2}},{\mathit{e}^{\prime}_{2}},{\mathit{s}_{2}})}{{{u}^{\mathtt{v}}}:{{\mathtt{n}}^{\mathtt{v}}}}}$}\hskip
0.0pt plus 0.0001fil}\vspace{0cm} \hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=192.29695pt\hbox{\kern
3.00003pt$\mathtt{({es_{p}})}$}}}\hbox{\kern 0.0pt\kern
43.43576pt\hbox{$\displaystyle{{{\Gamma_{1}}^{\overline{\mathtt{v}}}}\mathrel{+}{{\Gamma_{2}}^{\overline{\mathtt{v}}}}}\vdash^{({\mathit{m}_{1}+\mathit{m}_{2}},{\mathit{e}^{\prime}_{1}+\mathit{e}^{\prime}_{2}},{\mathit{s}_{1}+\mathit{s}_{2}})}{{{t}^{\mathtt{v}}}:{{\sigma}^{\mathtt{v}}}}$}}}}$

with $\mathsf{tight}(\mathcal{M}^{\prime})$ and
$\mathit{e}^{\prime}=\mathit{e}^{\prime}_{1}+\mathit{e}^{\prime}_{2}$.
Moreover, since $\Phi^{\prime}$ is $\mathtt{v}$-relevant,
$\mathcal{M}^{\prime}$ is of the form ${\mathcal{M}}^{\overline{\mathtt{v}}}$.
Then, by the i.h. there exists type derivations
${\Phi_{r}}\rhd_{\mathcal{V}}{{\Gamma_{1};{x}:{\mathcal{M}}}\vdash^{({\mathit{m}_{1}},{\mathit{e}_{1}},{\mathit{s}_{1}})}{{r}:{\sigma}}}$
and
${\Phi_{u}}\rhd_{\mathcal{V}}{{\Gamma_{2}}\vdash^{({\mathit{m}_{2}},{\mathit{e}_{2}},{\mathit{s}_{2}})}{{u}:{\mathtt{n}}}}$
with
$\mathit{e}_{1}=\mathit{e}^{\prime}_{1}-\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{r}}\right)$
and
$\mathit{e}_{2}=\mathit{e}^{\prime}_{2}-\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{u}}\right)$
resp. Finally, since $\mathsf{tight}({\mathcal{M}}^{\overline{\mathtt{v}}})$
implies $\mathsf{tight}(\mathcal{M})$, we conclude by applying rule
$\mathtt{({es_{p}})}$ with $\Phi_{r}$, $\Phi_{u}$ obtaining the type
derivation
${\Phi}\rhd_{\mathcal{V}}{{\Gamma}\vdash^{({\mathit{m}},{\mathit{e}},{\mathit{s}})}{{t}:{\sigma}}}$
where
$\mathit{e}=\mathit{e}_{1}+\mathit{e}_{2}=\mathit{e}^{\prime}_{1}-\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{r}}\right)+\mathit{e}^{\prime}_{2}-\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}_{u}}\right)=\mathit{e}^{\prime}-\widehat{\mathtt{e}}\\!\left({\Phi^{\prime}}\right)$
as expected.

     * •

$\mathtt{({var_{c}})}$. Then ${t}^{\mathtt{v}}=x$ which is not possible by
definition. Hence, this case does not apply.

     * •

$\mathtt{({app_{c}})}$. Then $t={t_{1}}\,{u}$ with
${t}^{\mathtt{v}}={r}\,{{u}^{\mathtt{v}}}$ for some term $r$,
$\Gamma={\Gamma_{1}}\mathrel{+}{\Gamma_{2}}$. Moreover, since $\Phi^{\prime}$
is $\mathtt{v}$-relevant, then it is of the form

${tensy\vbox{\hbox spread0.0pt{\kern 0.0pt\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty