* Ehrhard (2016) Thomas Ehrhard. 2016\.  Call-By-Push-Value from a Linear Logic Point of View. In _Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings_ (April 2-8, 2016) _(Lecture Notes in Computer Science, Vol. 9632)_ , Peter Thiemann (Ed.). Springer, Eindhoven, The Netherlands, 202–228.  https://doi.org/10.1007/978-3-662-49498-1_9
  * Ehrhard and Guerrieri (2016) Thomas Ehrhard and Giulio Guerrieri. 2016.  The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In _Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming_ (September 5-7, 2016), James Cheney and Germán Vidal (Eds.). ACM, Edinburgh, United Kingdom, 174–187.  https://doi.org/10.1145/2967973.2968608
  * García-Pérez and Nogueira (2016) Álvaro García-Pérez and Pablo Nogueira. 2016.  No solvable lambda-value term left behind.  _Logical Methods in Computer Science_ 12, 2 (2016), 1–43.  https://doi.org/10.2168/LMCS-12(2:12)2016
  * Grégoire and Leroy (2002) Benjamin Grégoire and Xavier Leroy. 2002.  A compiled implementation of strong reduction. In _Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002_ , Mitchell Wand and Simon L. Peyton Jones (Eds.). ACM, 235–246.  https://doi.org/10.1145/581478.581501
  * Guerrieri and Manzonetto (2018) Giulio Guerrieri and Giulio Manzonetto. 2018.  The Bang Calculus and the Two Girard’s Translations. In _Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018_ _(EPTCS, Vol. 292)_. Oxford, UK, 15–30.  https://doi.org/10.4204/EPTCS.292.2
  * Guerrieri et al. (2017) Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca. 2017\.  Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus.  _Logical Methods Computer Science_ 13, 4 (2017), 1–27.  https://doi.org/10.23638/LMCS-13(4:29)2017
  * Herbelin and Zimmermann (2009) Hugo Herbelin and Stéphane Zimmermann. 2009\.  An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in ”Natural Deduction” Form. In _Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings_ _(Lecture Notes in Computer Science, Vol. 5608)_ , Pierre-Louis Curien (Ed.). Springer, 142–156.  https://doi.org/10.1007/978-3-642-02273-9_12
  * Hutton (2023) Graham Hutton. 2023\.  Programming language semantics: It’s easy as 1,2,3.  _Journal of Functional Programming_ 33 (2023), e9.  https://doi.org/10.1017/S0956796823000072
  * Hyland (1975) J. M. E. Hyland. 1975\.  A survey of some useful partial order relations on terms of the lambda calculus. In _Lambda-Calculus and Computer Science Theory, Proceedings of the Symposium Held in Rome, Italy, March 25-27, 1975_ _(Lecture Notes in Computer Science, Vol. 37)_ , Corrado Böhm (Ed.). Springer, 83–95.  https://doi.org/10.1007/BFB0029520
  * Kennaway et al. (1999) Richard Kennaway, Vincent van Oostrom, and Fer-Jan de Vries. 1999\.  Meaningless Terms in Rewriting.  _Journal of Functional and Logic Programming_ 1999, 1 (1999), 1–35.  http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/1999/A99-01/A99-01.html
  * Kerinec et al. (2020) Axel Kerinec, Giulio Manzonetto, and Michele Pagani. 2020\.  Revisiting Call-by-value Böhm trees in light of their Taylor expansion.  _Logical Methods in Computer Science_ 16, 3 (2020), 6:1–6:26.  https://lmcs.episciences.org/6638
  * Kerinec et al. (2021) Axel Kerinec, Giulio Manzonetto, and Simona Ronchi Della Rocca. 2021\.  Call-By-Value, Again!. In _6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021 (Virtual Conference)_ (July 17-24, 2021) _(LIPIcs, Vol. 195)_ , Naoki Kobayashi (Ed.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, Buenos Aires, Argentina, 7:1–7:18.  https://doi.org/10.4230/LIPIcs.FSCD.2021.7
  * Kesner and Ventura (2014) Delia Kesner and Daniel Ventura. 2014.  Quantitative Types for the Linear Substitution Calculus. In _Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Proceedings_ (September 1-3, 2014.) _(Lecture Notes in Computer Science, Vol. 8705)_ , Josep Díaz, Ivan Lanese, and Davide Sangiorgi (Eds.). Springer, Rome, Italy, 296–310.  https://doi.org/10.1007/978-3-662-44602-7_23
  * Kuper (1995) Jan Kuper. 1995\.  Proving the Genericity Lemma by Leftmost Reduction is Simple. In _Rewriting Techniques and Applications, 6th International Conference, RTA-95, Proceedings_ (April 5-7, 1995) _(Lecture Notes in Computer Science, Vol. 914)_ , Jieh Hsiang (Ed.). Springer, Kaiserslautern, Germany, 271–278.  https://doi.org/10.1007/3-540-59200-8_63
  * Levy (1999) Paul Blain Levy. 1999\.  Call-by-Push-Value: A Subsuming Paradigm. In _Typed Lambda Calculi and Applications_ , Jean-Yves Girard (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 228–243.  https://doi.org/10.1007/3-540-48959-2_17
  * Paolini et al. (2006) Luca Paolini, Elaine Pimentel, and Simona Ronchi Della Rocca. 2006\.  An Operational Characterization of Strong Normalization. In _Foundations of Software Science and Computation Structures, 9th International Conference, FOSSACS 2006, Proceedings_ (March 25-31, 2006) _(Lecture Notes in Computer Science, Vol. 3921)_ , Luca Aceto and Anna Ingólfsdóttir (Eds.). Springer, Vienna, Austria, 367–381.  https://doi.org/10.1007/11690634_25
  * Paolini and Ronchi Della Rocca (1999) Luca Paolini and Simona Ronchi Della Rocca. 1999.  Call-By-Value Solvability.  _RAIRO Theoretical Informatics and Applications_ 33, 6 (1999), 507–534.  https://doi.org/10.1051/ita:1999130
  * Plotkin (1975) Gordon D. Plotkin. 1975\.  Call-by-Name, Call-by-Value and the lambda-Calculus.  _Theoretical Computer Science_ 1, 2 (1975), 125–159.  https://doi.org/10.1016/0304-3975(75)90017-1
  * Rocca and Paolini (2004) Simona Ronchi Della Rocca and Luca Paolini. 2004.  _The Parametric Lambda Calculus - A Metamodel for Computation_.  Springer.  https://doi.org/10.1007/978-3-662-10394-4
  * Scott and Strachey (1971) Dana Scott and Christopher Strachey. 1971.  _Toward a Mathematical Semantics for Computer Languages_.  Technical Report PRG06. OUCL. 49 pages.
  * Scott (1970) Dana S. Scott. 1970\.  Outline of a mathematical theory of computation. In _Fourth Annual Princeton Conference on Information Sciences and Systems_. Departement of Elctrical Engeneering, Princeton Univ., 169–176.
  * Scott (1972) Dana S. Scott. 1972\.  Mathematical concepts in programming language semantics. In _American Federation of Information Processing Societies: AFIPS Conference Proceedings: 1972 Spring Joint Computer Conference, Atlantic City, NJ, USA, May 16-18, 1972_ _(AFIPS Conference Proceedings, Vol. 40)_. AFIPS, 225–234.  https://doi.org/10.1145/1478873.1478903
  * Takahashi (1994) Masako Takahashi. 1994\.  A simple proof of the genericity lemma.  In _Logic, Language and Computation_. Springer-Verlag, 117–118.  https://doi.org/10.1007/bfb0032397
  * Wadsworth (1971) Christopher P. Wadsworth. 1971\.  _Semantics and pragmatics of the lambda-calculus_.  Ph.D. University of Oxford.  https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.476186 Accepted: 1971.
  * Wadsworth (1976) Christopher P. Wadsworth. 1976\.  The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus.  _SIAM J. Comput._ 5, 3 (Sept. 1976), 488–521.  https://doi.org/10.1137/0205036 Publisher: Society for Industrial and Applied Mathematics.

## Technical Appendix

##  Appendix A Proofs of Section 2

Let us recall the mutual inductive definitions of ${\tt vr}_{\mathrm{v}_{k}}$,
${\tt ne}_{\mathrm{v}_{k}}$ and ${\tt no}_{\mathrm{v}_{k}}$ for
$k\in\mathbb{N}^{\omega}$:

$\begin{array}[]{c}\begin{array}[]{rcl}{\tt
vr}_{\mathrm{v}_{k}}&\coloneqq&x\;|\;{\tt vr}_{\mathrm{v}_{k}}[x\backslash{\tt
ne}_{\mathrm{v}_{k}}]\\\\[5.69046pt] {\tt ne}_{\mathrm{v}_{k}}&\coloneqq&{\tt
vr}_{\mathrm{v}_{k}}\,{\tt no}_{\mathrm{v}_{k}}\;|\;{\tt
ne}_{\mathrm{v}_{k}}\,{\tt no}_{\mathrm{v}_{k}}\;|\;{\tt
ne}_{\mathrm{v}_{k}}[x\backslash{\tt ne}_{\mathrm{v}_{k}}]\\\\[5.69046pt] {\tt
no}_{\mathrm{v}_{0}}&\coloneqq&\lambda x.t\;|\;{\tt
ne}_{\mathrm{v}_{0}}\;|\;{\tt vr}_{\mathrm{v}_{0}}\;|\;{\tt
no}_{\mathrm{v}_{0}}[x\backslash{\tt ne}_{\mathrm{v}_{0}}]\\\ {\tt
no}_{\mathrm{v}_{i+1}}&\coloneqq&\lambda x.{\tt no}_{\mathrm{v}_{i}}\;|\;{\tt
ne}_{\mathrm{v}_{i+1}}\;|\;{\tt vr}_{\mathrm{v}_{i+1}}\;|\;{\tt
no}_{\mathrm{v}_{i+1}}[x\backslash{\tt ne}_{\mathrm{v}_{i+1}}]\
(i\in\mathbb{N})\\\ {\tt no}_{\mathrm{v}_{\omega}}&\coloneqq&\lambda x.{\tt
no}_{\mathrm{v}_{\omega}}\;|\;{\tt vr}_{\mathrm{v}_{\omega}}\;|\;{\tt
ne}_{\mathrm{v}_{\omega}}\;|\;{\tt no}_{\mathrm{v}_{\omega}}[x\backslash{\tt
ne}_{\mathrm{v}_{\omega}}]\end{array}\end{array}$

From now on we write ${\tt Var}\\!\left(t\right)$ iff
$t=\mathtt{L}\\!\left<x\right>$ for some list context $\mathtt{L}$ and some
$x$, and ${\tt Abs}\\!\left(t\right)$ iff $t=\mathtt{L}\\!\left<\lambda
x.u\right>$ for some list context $\mathtt{L}$ and some $u$.

*

###### Proof.

Let $k\in\mathbb{N}^{\omega}$ and $t\in\Lambda$. We strengthen the property as
follows:

  * $t\in{\tt vr}_{\mathrm{v}_{k}}$ if and only if $t$ is a $\mathrm{v}_{k}$-normal form and ${\tt Var}\\!\left(t\right)$.

  * $t\in{\tt ne}_{\mathrm{v}_{k}}$ if and only if $t$ is a $\mathrm{v}_{k}$-normal form and $\neg{\tt Abs}\\!\left(t\right)$ and $\neg{\tt Var}\\!\left(t\right)$.

  * $t\in{\tt no}_{\mathrm{v}_{k}}$ if and only if $t$ is a $\mathrm{v}_{k}$-normal form.

By double implication:

  * $(\Rightarrow)$

By mutual induction on $t\in{\tt vr}_{\mathrm{v}_{k}}$, $t\in{\tt
ne}_{\mathrm{v}_{k}}$ and $t\in{\tt no}_{\mathrm{v}_{k}}$:

    * $t\in{\tt vr}_{\mathrm{v}_{k}}$: We distinguish two cases:

      * $t=x$: Then $t$ is a $\mathrm{v}_{k}$-normal form and in particular ${\tt Var}\\!\left(t\right)$.

      * $t=t_{1}[x\backslash t_{2}]$ with $t_{1}\in{\tt vr}_{\mathrm{v}_{k}}$ and $t_{2}\in{\tt ne}_{\mathrm{v}_{k}}$: By i.h. on $t_{1}$ and $t_{2}$, one has that both are $\mathrm{v}_{k}$-normal forms and in particular ${\tt Var}\\!\left(t_{1}\right)$, $\neg{\tt Abs}\\!\left(t_{2}\right)$ and $\neg{\tt Var}\\!\left(t_{2}\right)$. Thus $t=t_{1}[x\backslash t_{2}]$ is a $\mathrm{v}_{k}$-normal form and ${\tt Var}\\!\left(t\right)$.

    * $t\in{\tt ne}_{\mathrm{v}_{k}}$: We distinguish three cases:

      * $t=t_{1}t_{2}$ with $t_{1}\in{\tt vr}_{\mathrm{v}_{k}}$ and $t_{2}\in{\tt no}_{\mathrm{v}_{k}}$: Then by i.h. on $t_{1}$ and $t_{2}$, one has that both are $\mathrm{v}_{k}$-normal forms and ${\tt Var}\\!\left(t_{1}\right)$. Thus, $t=t_{1}t_{2}$ is also a $\mathrm{v}_{k}$-normal form and in particular $\neg{\tt Abs}\\!\left(t\right)$ and $\neg{\tt Var}\\!\left(t\right)$.

      * $t=t_{1}t_{2}$ with $t_{1}\in{\tt ne}_{\mathrm{v}_{k}}$ and $t_{2}\in{\tt no}_{\mathrm{v}_{k}}$: Then by i.h. on $t_{1}$ and $t_{2}$, one has that both are $\mathrm{v}_{k}$-normal forms and $\neg{\tt Abs}\\!\left(t_{1}\right)$. Thus, $t=t_{1}t_{2}$ is also a $\mathrm{v}_{k}$-normal form and in particular $\neg{\tt Abs}\\!\left(t\right)$ and $\neg{\tt Var}\\!\left(t\right)$.

      * $t=t_{1}[x\backslash t_{2}]$ with $t_{1},t_{2}\in{\tt ne}_{\mathrm{v}_{k}}$: Then by i.h. on $t_{1}$ and $t_{2}$, one has that both are $\mathrm{v}_{k}$-normal forms and $\neg{\tt Abs}\\!\left(t_{1}\right)$, $\neg{\tt Var}\\!\left(t_{1}\right)$, $\neg{\tt Var}\\!\left(t_{2}\right)$ and $\neg{\tt Var}\\!\left(t_{2}\right)$. Thus, $t=t_{1}[x\backslash t_{2}]$ is also a $\mathrm{v}_{k}$-normal form and in particular $\neg{\tt Abs}\\!\left(t\right)$ and $\neg{\tt Var}\\!\left(t\right)$.

    * $t\in{\tt no}_{\mathrm{v}_{k}}$: We distinguish four cases:

      * $t=\lambda x.t^{\prime}$: We distinguish three cases:

        * $\bullet$

$k=0$: Then $t=\lambda x.t^{\prime}$ is a $\mathrm{v}_{0}$-normal form.

        * $\bullet$

$k=i+1$ and $t^{\prime}\in{\tt no}_{\mathrm{v}_{i}}$ for some
$i\in\mathbb{N}$: By i.h. on $t^{\prime}$, one has that $t^{\prime}$ is a
$\mathrm{v}_{i}$-normal form thus $t=\lambda x.t^{\prime}$ is a
$\mathrm{v}_{k}$-normal form.

        * $\bullet$

$k=\omega$ and $t^{\prime}\in{\tt no}_{\mathrm{v}_{\omega}}$: By i.h. on
$t^{\prime}$, one has that $t^{\prime}$ is a $\mathrm{v}_{\omega}$-normal form
thus $t=\lambda x.t^{\prime}$ is also a $\mathrm{v}_{\omega}$-normal form.

      * $t\in{\tt vr}_{\mathrm{v}_{k}}$: Then by i.h. on $t$, it is a $\mathrm{v}_{k}$-normal form.

      * $t\in{\tt ne}_{\mathrm{v}_{k}}$: Then by i.h. on $t$, it is a $\mathrm{v}_{k}$-normal form.

      * $t=t_{1}[x\backslash t_{2}]$ with $t_{1}\in{\tt no}_{\mathrm{v}_{k}}$ and $t_{2}\in{\tt ne}_{\mathrm{v}_{k}}$: Then by i.h. on $t_{1}$ and $t_{2}$, one has that both are $\mathrm{v}_{k}$-normal forms and, $\neg{\tt Abs}\\!\left(t_{2}\right)$ and $\neg{\tt Var}\\!\left(t_{2}\right)$. Thus, $t=t_{1}[x\backslash t_{2}]$ is also a $\mathrm{v}_{k}$-normal form.

  * $(\Leftarrow)$

By induction on $t$:

    * $t=x$: Then ${\tt Var}\\!\left(t\right)$ and $t\in{\tt vr}_{\mathrm{v}_{k}}$.

    * $t=\lambda x.t^{\prime}$: Then ${\tt Abs}\\!\left(t\right)$. We distinguish three cases:

      * $k=0$: Then $t=\lambda x.t^{\prime}\in{\tt no}_{\mathrm{v}_{0}}$.

      * $k=i+1$ for some $i\in\mathbb{N}$: Then, $t^{\prime}$ is necessarily a $\mathrm{v}_{i}$-normal form. By i.h. on $t^{\prime}$, one has that $t^{\prime}\in{\tt no}_{\mathrm{v}_{i}}$ thus $t=\lambda x.t^{\prime}\in\lambda x.{\tt no}_{\mathrm{v}_{i}}\subseteq{\tt no}_{\mathrm{v}_{k}}$.

      * $k=\omega$: By i.h. on $t^{\prime}$, one has that $t^{\prime}\in{\tt no}_{\mathrm{v}_{\omega}}$ thus $t=\lambda x.t^{\prime}\in\lambda x.{\tt no}_{\mathrm{v}_{\omega}}\subseteq{\tt no}_{\mathrm{v}_{\omega}}$.

    * $t=t_{1}t_{2}$: Then $\neg{\tt Abs}\\!\left(t\right)$ and $\neg{\tt Var}\\!\left(t\right)$. Moreover, $t_{1}$ and $t_{2}$ are necessarily $\mathrm{v}_{k}$-normal forms and $\neg{\tt Abs}\\!\left(t_{1}\right)$. By i.h. on $t_{2}$, one has that $t_{2}\in{\tt no}_{\mathrm{v}_{k}}$. We distinguish two cases:

      * ${\tt Var}\\!\left(t_{1}\right)$: Then, by i.h. on $t_{1}$, one has that $t_{1}\in{\tt vr}_{\mathrm{v}_{k}}$, thus $t=t_{1}t_{2}\in{\tt vr}_{\mathrm{v}_{k}}{\tt no}_{\mathrm{v}_{k}}\subseteq{\tt ne}_{\mathrm{v}_{k}}$.

      * $\neg{\tt Var}\\!\left(t_{1}\right)$: Then, by i.h. on $t_{1}$, one has that $t_{1}\in{\tt ne}_{\mathrm{v}_{k}}$, thus $t=t_{1}t_{2}\in{\tt ne}_{\mathrm{v}_{k}}{\tt no}_{\mathrm{v}_{k}}\subseteq{\tt ne}_{\mathrm{v}_{k}}$.

    * $t=t_{1}[x\backslash t_{2}]$: Then both $t_{1}$ and $t_{2}$ are necessarily $\mathrm{v}_{k}$-normal forms and, $\neg{\tt Abs}\\!\left(t_{2}\right)$ and $\neg{\tt Var}\\!\left(t_{2}\right)$. By i.h. on $t_{2}$, one has that $t_{2}\in{\tt ne}_{\mathrm{v}_{k}}$. We distinguish three cases:

      * ${\tt Var}\\!\left(t_{1}\right)$: Then, by i.h. on $t_{1}$, one has that $t_{1}\in{\tt vr}_{\mathrm{v}_{k}}$ thus $t=t_{1}[x\backslash t_{2}]\in{\tt vr}_{\mathrm{v}_{k}}[x\backslash{\tt ne}_{\mathrm{v}_{k}}]\subseteq{\tt vr}_{\mathrm{v}_{k}}$.

      * $\neg{\tt Var}\\!\left(t_{1}\right)$ and $\neg{\tt Abs}\\!\left(t_{1}\right)$: Then, by i.h. on $t_{1}$, one has that $t_{1}\in{\tt ne}_{\mathrm{v}_{k}}$ thus $t=t_{1}[x\backslash t_{2}]\in{\tt ne}_{\mathrm{v}_{k}}[x\backslash{\tt ne}_{\mathrm{v}_{k}}]\subseteq{\tt ne}_{\mathrm{v}_{k}}$.

      * otherwise: Then, by i.h. on $t_{1}$, one has that $t_{1}\in{\tt no}_{\mathrm{v}_{k}}$ thus $t=t_{1}[x\backslash t_{2}]\in{\tt no}_{\mathrm{v}_{k}}[x\backslash{\tt ne}_{\mathrm{v}_{k}}]\subseteq{\tt no}_{\mathrm{v}_{k}}$.

∎

*

###### Proof.

By induction on $\mathtt{C}$:

  * $\mathtt{C}=\diamond$: Then $\mathtt{C}\\!\left<t\right>=t$ thus $\mathtt{C}\\!\left<t\right>$ is meaningless which is impossible since it contradicts Lemma 2.4.

  * $\mathtt{C}=\lambda x.\mathtt{C}^{\prime}$: Then $\Pi$ is necessarily of the following form, for some finite set $I$:

$({\tt abs})$ $\left(\vrule
height=10.33331pt,depth=0.0pt,width=0.0pt\right.$$\left.\hbox{$\vbox{\hbox{\hbox{}\hbox{$\Pi_{i}\triangleright_{\mathcal{V}}\Gamma_{i},x:\mathcal{M}_{i}\vdash\mathtt{C}^{\prime}\\!\left<t\right>:\tau_{i}$}}}$}\right)_{i\in
I}$$\quad+_{i\in I}\Gamma_{i}\vdash\lambda
x.\mathtt{C}^{\prime}\\!\left<t\right>:\left[\mathcal{M}_{i}\Rightarrow\tau_{i}\right]_{i\in
I}\quad$

with $\Gamma=+_{i\in I}\Gamma_{i}$ and
$\sigma=\left[\mathcal{M}_{i}\Rightarrow\tau_{i}\right]_{i\in I}$. For each
$i\in I$, by i.h. on $\Pi_{i}$, one has
$\Pi^{\prime}_{i}\triangleright_{\mathcal{V}}\Gamma_{i},x:\mathcal{M}_{i}\triangleright_{\mathcal{V}}\mathtt{C}^{\prime}\\!\left<u\right>:\tau_{i}$
and we set $\Pi^{\prime}$ as the following derivation:

$({\tt abs})$ $\left(\vrule
height=10.33331pt,depth=0.0pt,width=0.0pt\right.$$\left.\hbox{$\vbox{\hbox{\hbox{}\hbox{$\Pi^{\prime}_{i}\triangleright_{\mathcal{V}}\Gamma_{i},x:\mathcal{M}_{i}\vdash\mathtt{C}^{\prime}\\!\left<u\right>:\tau_{i}$}}}$}\right)_{i\in
I}$$\quad+_{i\in I}\Gamma_{i}\vdash\lambda
x.\mathtt{C}^{\prime}\\!\left<u\right>:\left[\mathcal{M}_{i}\Rightarrow\tau_{i}\right]_{i\in
I}\quad$

  * $\mathtt{C}=\mathtt{C}^{\prime}s$: Then $\Pi$ is necessarily of the following form:

$({\tt app})$
$\Pi_{1}\triangleright_{\mathcal{V}}\Gamma_{1}\vdash\mathtt{C}^{\prime}\\!\left<t\right>:\left[\mathcal{M}\Rightarrow\sigma\right]$$\Pi_{2}\triangleright_{\mathcal{V}}\Gamma_{2}\vdash
s:\mathcal{M}$$\Gamma_{1}+\Gamma_{2}\vdash\mathtt{C}^{\prime}\\!\left<t\right>s:\sigma$

with $\Gamma=\Gamma_{1}+\Gamma_{2}$. By i.h. on $\Pi_{1}$, one has
$\Pi^{\prime}_{1}\triangleright_{\mathcal{V}}\Gamma_{1}\vdash\mathtt{C}^{\prime}\\!\left<u\right>:\left[\mathcal{M}\Rightarrow\sigma\right]$
and we set $\Pi^{\prime}$ as the following derivation:

$({\tt app})$
$\Pi^{\prime}_{1}\triangleright_{\mathcal{V}}\Gamma_{1}\vdash\mathtt{C}^{\prime}\\!\left<u\right>:\left[\mathcal{M}\Rightarrow\sigma\right]$$\Pi_{2}\triangleright_{\mathcal{V}}\Gamma_{2}\vdash
s:\mathcal{M}$$\Gamma_{1}+\Gamma_{2}\vdash\mathtt{C}^{\prime}\\!\left<u\right>s:\sigma$

  * $\mathtt{C}=s\,\mathtt{C}^{\prime}$: Then $\Pi$ is necessarily of the following form:

$({\tt app})$ $\Pi_{1}\triangleright_{\mathcal{V}}\Gamma_{1}\vdash
s:\left[\mathcal{M}\Rightarrow\sigma\right]$$\Pi_{2}\triangleright_{\mathcal{V}}\Gamma_{2}\vdash\mathtt{C}^{\prime}\\!\left<t\right>:\mathcal{M}$$\Gamma_{1}+\Gamma_{2}\vdash
s\mathtt{C}^{\prime}\\!\left<t\right>:\sigma$

with $\Gamma=\Gamma_{1}+\Gamma_{2}$. By i.h. on $\Pi_{2}$, one has
$\Pi^{\prime}_{2}\triangleright_{\mathcal{V}}\Gamma_{2}\vdash\mathtt{C}^{\prime}\\!\left<u\right>:\mathcal{M}$
and we set $\Pi^{\prime}$ as the following derivation:

$({\tt app})$ $\Pi_{1}\triangleright_{\mathcal{V}}\Gamma_{1}\vdash
s:\left[\mathcal{M}\Rightarrow\sigma\right]$$\Pi^{\prime}_{2}\triangleright_{\mathcal{V}}\Gamma_{2}\vdash\mathtt{C}^{\prime}\\!\left<u\right>:\mathcal{M}$$\Gamma_{1}+\Gamma_{2}\vdash
s\mathtt{C}^{\prime}\\!\left<u\right>:\sigma$

  * $\mathtt{C}=\mathtt{C}^{\prime}[x\backslash s]$: Then $\Pi$ is necessarily of the following form:

$({\tt es})$
$\Pi_{1}\triangleright_{\mathcal{V}}\Gamma_{1},x:\mathcal{M}\vdash\mathtt{C}^{\prime}\\!\left<t\right>:\sigma$$\Pi_{2}\triangleright_{\mathcal{V}}\Gamma_{2}\vdash
s:\mathcal{M}$$\Gamma_{1}+\Gamma_{2}\vdash\mathtt{C}^{\prime}\\!\left<t\right>[x\backslash
s]:\sigma$

with $\Gamma=\Gamma_{1}+\Gamma_{2}$. By i.h. on $\Pi_{1}$, one has
$\Pi^{\prime}_{1}\triangleright_{\mathcal{V}}\Gamma_{1},x:\mathcal{M}\vdash\mathtt{C}^{\prime}\\!\left<u\right>:\sigma$
and we set $\Pi^{\prime}$ as the following derivation:

$({\tt es})$
$\Pi^{\prime}_{1}\triangleright_{\mathcal{V}}\Gamma_{1},x:\mathcal{M}\vdash\mathtt{C}^{\prime}\\!\left<u\right>:\sigma$$\Pi_{2}\triangleright_{\mathcal{V}}\Gamma_{2}\vdash
s:\mathcal{M}$$\Gamma_{1}+\Gamma_{2}\vdash\mathtt{C}^{\prime}\\!\left<u\right>[x\backslash
s]:\sigma$

  * $\mathtt{C}=s[x\backslash\mathtt{C}^{\prime}]$: Then $\Pi$ is necessarily of the following form:

$({\tt es})$
$\Pi_{1}\triangleright_{\mathcal{V}}\Gamma_{1},x:\mathcal{M}\vdash
s:\sigma$$\Pi_{2}\triangleright_{\mathcal{V}}\Gamma_{2}\vdash\mathtt{C}^{\prime}\\!\left<t\right>:\mathcal{M}$$\Gamma_{1}+\Gamma_{2}\vdash
s[x\backslash\mathtt{C}^{\prime}\\!\left<t\right>]:\sigma$

with $\Gamma=\Gamma_{1}+\Gamma_{2}$. By i.h. on $\Pi_{2}$, one has
$\Pi_{1}\triangleright_{\mathcal{V}}\Gamma_{1},x:\mathcal{M}\vdash\mathtt{C}^{\prime}\\!\left<u\right>:\sigma$
and we set $\Pi^{\prime}$ as the following derivation:

$({\tt es})$
$\Pi_{1}\triangleright_{\mathcal{V}}\Gamma_{1},x:\mathcal{M}\vdash
s:\sigma$$\Pi^{\prime}_{2}\triangleright_{\mathcal{V}}\Gamma_{2}\vdash\mathtt{C}^{\prime}\\!\left<u\right>:\mathcal{M}$$\Gamma_{1}+\Gamma_{2}\vdash
s[x\backslash\mathtt{C}^{\prime}\\!\left<u\right>]:\sigma$

∎

##  Appendix B Proofs of Section 4

###  B.1. Technical Lemmas

###### Lemma B.1.

Let $\mathbf{t}_{1},\mathbf{t}_{2}\in\mathbf{\Lambda}$ and
$\mathbf{v}_{1},\mathbf{v}_{2}\in\mathbf{\Upsilon}$ such that
$\mathbf{t}_{1}\leq\mathbf{t}_{2}$ and $\mathbf{v}_{1}\leq\mathbf{v}_{2}$,
then
$\mathbf{t}_{1}\\{x\backslash\mathbf{v}_{1}\\}\leq\mathbf{t}_{2}\\{x\backslash\mathbf{v}_{2}\\}$.

###### Proof.

By induction on $\mathbf{t}_{1}$:

  * $\mathbf{t}_{1}=\bot$: Then $\mathbf{t}_{1}\\{x\backslash\mathbf{v}_{1}\\}=\bot\leq\mathbf{t}_{2}\\{x\backslash\mathbf{v}_{2}\\}$.

  * $\mathbf{t}_{1}=y$: Then $\mathbf{t}_{2}=y$ and we distinguish two cases:

    * $x=y$: Thus $\mathbf{t}_{1}\\{x\backslash\mathbf{v}_{1}\\}=\mathbf{v}_{1}\leq\mathbf{v}_{2}=\mathbf{t}_{2}\\{x\backslash\mathbf{v}_{2}\\}$.

    * $x\neq y$: Thus $\mathbf{t}_{1}\\{x\backslash\mathbf{v}_{1}\\}=y=\mathbf{t}_{2}\\{x\backslash\mathbf{v}_{2}\\}$, thus $\mathbf{t}_{1}\\{x\backslash\mathbf{v}_{1}\\}\leq\mathbf{t}_{2}\\{x\backslash\mathbf{v}_{2}\\}$ by reflexivity of $\leq$.

  * $\mathbf{t}_{1}=\lambda y.\mathbf{t}^{\prime}_{1}$: Then $\mathbf{t}_{1}\\{x\backslash\mathbf{v}_{1}\\}=\lambda y.\mathbf{t}^{\prime}_{1}\\{x\backslash\mathbf{v}_{1}\\}$ (by supposing $y\notin{\tt fv}(\mathbf{v}_{1})\cup{\tt fv}(\mathbf{v}_{2})$ without loss of generality) and necessarily $\mathbf{t}_{2}=\lambda y.\mathbf{t}^{\prime}_{2}$ with $\mathbf{t}^{\prime}_{1}\leq\mathbf{t}^{\prime}_{2}$ thus $\mathbf{t}_{2}\\{x\backslash\mathbf{v}_{2}\\}=\lambda y.\mathbf{t}^{\prime}_{2}\\{y\backslash\mathbf{v}_{2}\\}$. By i.h. on $\mathbf{t}^{\prime}_{1}$, one has that $\mathbf{t}^{\prime}_{1}\\{x\backslash\mathbf{v}_{1}\\}\leq\mathbf{t}^{\prime}_{2}\\{x\backslash\mathbf{v}_{2}\\}$ hence $\mathbf{t}_{1}\\{x\backslash\mathbf{v}_{1}\\}=\lambda y.\mathbf{t}^{\prime}_{1}\\{x\backslash\mathbf{v}_{1}\\}\leq\lambda y.\mathbf{t}^{\prime}_{2}\\{x\backslash\mathbf{v}_{2}\\}=\mathbf{t}_{2}\\{x\backslash\mathbf{v}_{2}\\}$ by contextual closure.

  * $\mathbf{t}_{1}=\mathbf{t}_{1}^{1}\mathbf{t}_{1}^{2}$: Then $\mathbf{t}_{1}\\{x\backslash\mathbf{v}_{1}\\}=(\mathbf{t}_{1}^{1}\\{x\backslash\mathbf{v}_{1}\\})(\mathbf{t}_{1}^{2}\\{x\backslash\mathbf{v}_{1}\\})$ and necessarily $\mathbf{t}_{2}=\mathbf{t}_{2}^{1}\,\mathbf{t}_{2}^{2}$ with $\mathbf{t}_{1}^{1}\leq\mathbf{t}_{2}^{1}$ and $\mathbf{t}_{1}^{2}\leq\mathbf{t}_{2}^{2}$, thus $\mathbf{t}_{2}\\{y\backslash\mathbf{v}_{2}\\}=(\mathbf{t}_{2}^{1}\\{x\backslash\mathbf{v}_{2}\\})(\mathbf{t}_{2}^{2}\\{x\backslash\mathbf{v}_{2}\\})$. By i.h. on $\mathbf{t}_{1}^{1}$ and $\mathbf{t}_{1}^{2}$, one obtains that $\mathbf{t}_{1}^{1}\\{x\backslash\mathbf{v}_{1}\\}\leq\mathbf{t}_{2}^{1}\\{x\backslash\mathbf{v}_{2}\\}$ and $\mathbf{t}_{1}^{2}\\{x\backslash\mathbf{v}_{1}\\}\leq\mathbf{t}_{2}^{2}\\{x\backslash\mathbf{v}_{2}\\}$, hence $\mathbf{t}_{1}\\{x\backslash\mathbf{v}_{1}\\}=(\mathbf{t}_{1}^{1}\\{x\backslash\mathbf{v}_{1}\\})(\mathbf{t}_{1}^{2}\\{x\backslash\mathbf{v}_{1}\\})\leq(\mathbf{t}_{2}^{1}\\{x\backslash\mathbf{v}_{2}\\})(\mathbf{t}_{2}^{2}\\{x\backslash\mathbf{v}_{2}\\})=\mathbf{t}_{2}\\{x\backslash\mathbf{v}_{2}\\}$ by contextual closure.

  * $\mathbf{t}_{1}=\mathbf{t}_{1}^{1}[y\backslash\mathbf{t}_{1}^{2}]$: Then $\mathbf{t}_{1}\\{x\backslash\mathbf{v}_{1}\\}=\mathbf{t}_{1}^{1}\\{x\backslash\mathbf{v}_{1}\\}[y\backslash\mathbf{t}_{1}^{2}\\{x\backslash\mathbf{v}_{1}\\}]$ and necessarily $\mathbf{t}_{2}=\mathbf{t}_{2}^{1}[y\backslash\mathbf{t}_{2}^{2}]$ with $\mathbf{t}_{1}^{1}\leq\mathbf{t}_{2}^{1}$ and $\mathbf{t}_{1}^{2}\leq\mathbf{t}_{2}^{2}$, thus $\mathbf{t}_{2}\\{y\backslash\mathbf{v}_{2}\\}=\mathbf{t}_{2}^{1}\\{x\backslash\mathbf{v}_{2}\\}[y\backslash\mathbf{t}_{2}^{2}\\{x\backslash\mathbf{v}_{2}\\}]$. By i.h. on $\mathbf{t}_{1}^{1}$ and $\mathbf{t}_{1}^{2}$, one has $\mathbf{t}_{1}^{1}\\{x\backslash\mathbf{v}_{1}\\}\leq\mathbf{t}_{2}^{1}\\{x\backslash\mathbf{v}_{2}\\}$ and $\mathbf{t}_{1}^{2}\\{x\backslash\mathbf{v}_{1}\\}\leq\mathbf{t}_{2}^{2}\\{x\backslash\mathbf{v}_{2}\\}$, so by contextual closure $\mathbf{t}_{1}\\{x\backslash\mathbf{v}_{1}\\}=\mathbf{t}_{1}^{1}\\{x\backslash\mathbf{v}_{1}\\}[y\backslash\mathbf{t}_{1}^{2}\\{x\backslash\mathbf{v}_{1}\\}]\leq\mathbf{t}_{2}^{1}\\{x\backslash\mathbf{v}_{2}\\}[y\backslash\mathbf{t}_{2}^{2}\\{x\backslash\mathbf{v}_{2}\\}]=\mathbf{t}_{2}\\{x\backslash\mathbf{v}_{2}\\}$. ∎

###### Definition B.2.

The partial order $\leq$ is extended to dCBV contexts by setting
$\diamond\leq\diamond$.

For example, $\diamond[x\backslash\lambda
y.\bot](z\bot)\leq\diamond[x\backslash\lambda y.(zz)](z\bot)$.

###### Lemma B.3.

Let $\mathbf{L}_{1}\leq\mathbf{L}_{2}$ and $\mathbf{t}_{1}\leq\mathbf{t}_{2}$
for some list contexts $\mathbf{L}_{1},\mathbf{L}_{2}$ and some
$\mathbf{t}_{1},\mathbf{t}_{2}\in\mathbf{\Lambda}$, then
$\mathbf{L}_{1}\\!\left<\mathbf{t}_{1}\right>\leq\mathbf{L}_{2}\\!\left<\mathbf{t}_{2}\right>$.

###### Proof.

By induction on $\mathbf{L}_{1}$:

  * $\mathbf{L}_{1}=\diamond$: Then necessarily $\mathbf{L}_{2}=\diamond$ thus $\mathbf{L}_{1}\\!\left<\mathbf{t}_{1}\right>=\mathbf{t}_{1}\leq\mathbf{t}_{2}=\mathbf{L}_{2}\\!\left<\mathbf{t}_{2}\right>$.

  * $\mathbf{L}_{1}=\mathbf{L}^{\prime}_{1}[x\backslash\mathbf{u}_{1}]$: Then necessarily $\mathbf{L}_{2}=\mathbf{L}^{\prime}_{2}[x\backslash\mathbf{u}_{2}]$ with $\mathbf{L}^{\prime}_{1}\leq\mathbf{L}^{\prime}_{2}$ and $\mathbf{u}_{1}\leq\mathbf{u}_{2}$. By i.h. on $\mathbf{L}^{\prime}_{1}$, one has that $\mathbf{L}^{\prime}_{1}\\!\left<\mathbf{t}_{1}\right>\leq\mathbf{L}^{\prime}_{2}\\!\left<\mathbf{t}_{2}\right>$ thus $\mathbf{L}_{1}\\!\left<\mathbf{t}_{1}\right>=\mathbf{L}^{\prime}_{1}\\!\left<\mathbf{t}_{1}\right>[x\backslash\mathbf{u}_{1}]\leq\mathbf{L}^{\prime}_{2}\\!\left<\mathbf{t}_{2}\right>[x\backslash\mathbf{u}_{2}]=\mathbf{L}_{2}\\!\left<\mathbf{t}_{2}\right>$ by contextual closure. ∎

###### Lemma B.4.

Let $t,u\in\Lambda$ such that $t\rightarrow_{\mathrm{v}_{k}}u$. Then, $t$ is
dCBV-meaningful if and only if $u$ is dCBV-meaningful.

###### Proof.

According to qualitative subject reduction and expansion (Accattoli and
Guerrieri, 2022, Prop. 7.4), given $t\rightarrow_{\mathrm{v}_{\omega}}u$,
there is a derivation $\Pi\triangleright_{\mathcal{V}}\Gamma\vdash t:\sigma$
if and only if there is a derivation
$\Pi^{\prime}\triangleright_{\mathcal{V}}\Gamma\vdash u:\sigma$. As
$\rightarrow_{\mathrm{v}_{k}}\subseteq\rightarrow_{\mathrm{v}_{\omega}}$ for
all $k\in\mathbb{N}$, the same equivalence also holds if we replace the
hypothesis $t\rightarrow_{\mathrm{v}_{\omega}}u$ with
$t\rightarrow_{\mathrm{v}_{k}}u$, for all $k\in\mathbb{N}$. We conclude thanks
to the type-theoretical characterization of dCBV-meaningfulness (Lemma 2.4). ∎

###### Lemma B.5.

Let $t,u\in\Lambda$ and $v\in\Upsilon$. Then

  1. (1)

If $tu$ is dCBV-meaningful then $t$ and $u$ are dCBV-meaningful.

  2. (2)

If $t[x\backslash u]$ is dCBV-meaningful then $t$ and $u$ are dCBV-meaningful.

  3. (3)

If $t\\{x\backslash v\\}$ is dCBV-meaningful then $t$ is dCBV-meaningful.

###### Proof.

  1. (1)

Let $tu$ be dCBV-meaningful and suppose by absurd that $t$ is dCBV-
meaningless. Using Lemma 2.4, we know that $tu$ surface normalizes. Since $t$
is dCBV-meaningless, there exists a $(t_{i})_{i\in\mathbb{N}}$ with $t_{0}=t$
and $t_{i}\rightarrow_{\mathrm{v}_{0}}t_{i+1}$ yielding the infinite path
$tu\rightarrow_{\mathrm{v}_{0}}t_{1}u\rightarrow_{\mathrm{v}_{0}}t_{2}u\rightarrow_{\mathrm{v}_{0}}\dots$
obtained by always reducing $t$. Since surface reduction is diamond, this
contradicts the fact that $tu$ is surface normalizing. And similarly for $ut$.

  2. (2)

Same principle as the previous item.

  3. (3)

Let $t\\{x\backslash v\\}$ be dCBV-meaningful. By induction on $t$, one can
show that if $t\rightarrow_{\mathrm{v}_{0}}u$ then $t\\{x\backslash
v\\}\rightarrow_{\mathrm{v}_{0}}u\\{x\backslash v\\}$. Using this, one applied
the same principles as the two previous points.

∎

###### Definition B.6.

Meaningful approximation is extended to list contexts $\mathtt{L}$ inductively
as follows:

$\mathcal{M\\!A}_{{\tt V}}\\!\left(\diamond\right)\coloneqq\diamond\hskip
56.9055pt\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{L}[x\backslash
s]\right)\coloneqq\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}\right)[x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(s\right)]$

###### Corollary B.7.

Let $\mathtt{L}\\!\left<t\right>$ be dCBV-meaningful, then
$\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}\\!\left<t\right>\right)=\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}\right)\\!\left<\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)\right>$.

###### Proof.

By induction on $\mathtt{L}$:

  * $\mathtt{L}=\diamond$: Then $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{L}\\!\left<t\right>\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\diamond\\!\left<\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)\right>=\mathcal{M\\!A}_{{\tt V}}\\!\left(\diamond\right)\\!\left<\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)\right>$.

  * $\mathtt{L}=\mathtt{L}^{\prime}[x\backslash u]$: Then $\mathtt{L}\\!\left<t\right>=\mathtt{L}^{\prime}\\!\left<t\right>[x\backslash u]$ is dCBV-meaningful so that $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{L}\\!\left<t\right>\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{L}^{\prime}\\!\left<t\right>\right)[x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(u\right)]$. Moreover, using Lemma B.5.(2), one has that $\mathtt{L}^{\prime}\\!\left<t\right>$ is dCBV-meaningful. By i.h. on $\mathtt{L}^{\prime}$, one obtains that $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{L}^{\prime}\\!\left<t\right>\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{L}^{\prime}\right)\\!\left<\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)\right>$. Then:

$\begin{array}[]{r cl cl}\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}\\!\left<t\right>\right)&=&\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}^{\prime}\\!\left<t\right>\right)[x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(u\right)]\\\ &\overset{\textit{i.h.}}{=}&\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}^{\prime}\right)\\!\left<\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)\right>[x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(u\right)]\\\ &=&\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}^{\prime}\right)[x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(u\right)]\\!\left<\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)\right>\\\ &=&\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}^{\prime}[x\backslash
u]\right)\\!\left<\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)\right>&=&\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}\right)\\!\left<\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)\right>\end{array}$

∎

###### Lemma B.8.

Let $t\in\Lambda$ and $v\in\Upsilon$, then $\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\\{x\backslash v\\}\right)\leq\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\}$.

###### Proof.

Let $t\in\Lambda$ and $v\in\Upsilon$. Cases:

  * $t\\{x\backslash v\\}$ is dCBV-meaningless: Then $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\\{x\backslash v\\}\right)=\bot\leq\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)\\{x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(v\right)\\}$.

  * $t\\{x\backslash v\\}$ is dCBV-meaningful: Using Lemma B.5.(3), one deduces that $t$ is dCBV-meaningful. We proceed by induction on $t$. Cases:

    * $t=y$: Then $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=y$ and we distinguish two cases:

      * $\bullet$

$y=x$: Then $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\\{x\backslash
v\\}\right)=\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)=x\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\}=\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\}$.

      * $\bullet$

$y\neq x$: Then $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\\{x\backslash
v\\}\right)=\mathcal{M\\!A}_{{\tt
V}}\\!\left(y\right)=y=y\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\}=\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\}$.

    * $t=\lambda y.t^{\prime}$: Then $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\lambda y.\mathcal{M\\!A}_{{\tt V}}\\!\left(t^{\prime}\right)$. By i.h. on $t^{\prime}$, one has that $\mathcal{M\\!A}_{{\tt V}}\\!\left(t^{\prime}\\{x\backslash v\\}\right)\leq\mathcal{M\\!A}_{{\tt V}}\\!\left(t^{\prime}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(v\right)\\}$. Therefore:

$\begin{array}[]{r cl cl}\mathcal{M\\!A}_{{\tt V}}\\!\left(t\\{x\backslash
v\\}\right)&=&\mathcal{M\\!A}_{{\tt V}}\\!\left(\lambda
y.(t^{\prime}\\{x\backslash v\\})\right)\\\ &=&\lambda y.\mathcal{M\\!A}_{{\tt
V}}\\!\left(t^{\prime}\\{x\backslash v\\}\right)\\\
&\overset{\textit{i.h.}}{\leq}&\lambda y.\mathcal{M\\!A}_{{\tt
V}}\\!\left(t^{\prime}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\}\\\ &=&(\lambda y.\mathcal{M\\!A}_{{\tt
V}}\\!\left(t^{\prime}\right))\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\}&=&\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\}\end{array}$

    * $t=t_{1}t_{2}$: Thus $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)$. By i.h. on $t_{1}$ and $t_{2}$, one has that $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\\{x\backslash v\\}\right)\leq\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(v\right)\\}$ and $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\\{x\backslash v\\}\right)\leq\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(v\right)\\}$. Therefore:

$\begin{array}[]{r cl cl}\mathcal{M\\!A}_{{\tt V}}\\!\left(t\\{x\backslash
v\\}\right)&=&\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\\{x\backslash
v\\}t_{2}\\{x\backslash v\\}\right)\\\ &=&\mathcal{M\\!A}_{{\tt
V}}\\!\left(t_{1}\\{x\backslash v\\}\right)\mathcal{M\\!A}_{{\tt
V}}\\!\left(t_{2}\\{x\backslash v\\}\right)\\\
&\overset{\textit{i.h.}}{\leq}&(\mathcal{M\\!A}_{{\tt
V}}\\!\left(t_{1}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\})(\mathcal{M\\!A}_{{\tt
V}}\\!\left(t_{2}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\})\\\ &=&(\mathcal{M\\!A}_{{\tt
V}}\\!\left(t_{1}\right)\mathcal{M\\!A}_{{\tt
V}}\\!\left(t_{2}\right))\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\}&=&\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\}\end{array}$

    * $t=t_{1}[y\backslash t_{2}]$: Thus $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)[y\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)]$. By i.h. on $t_{1}$ and $t_{2}$, one has that $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\\{x\backslash v\\}\right)\leq\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(v\right)\\}$ and $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\\{x\backslash v\\}\right)\leq\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(v\right)\\}$. Therefore:

$\begin{array}[]{r cl cl}\mathcal{M\\!A}_{{\tt V}}\\!\left(t\\{x\backslash
v\\}\right)&=&\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\\{x\backslash
v\\}[y\backslash t_{2}\\{x\backslash v\\}]\right)\\\ &=&\mathcal{M\\!A}_{{\tt
V}}\\!\left(t_{1}\\{x\backslash v\\}\right)[y\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(t_{2}\\{x\backslash v\\}\right)]\\\
&\overset{\textit{i.h.}}{\leq}&\mathcal{M\\!A}_{{\tt
V}}\\!\left(t_{1}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\}[y\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(t_{2}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\}]\\\ &=&(\mathcal{M\\!A}_{{\tt
V}}\\!\left(t_{1}\right)[y\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(t_{2}\right)])\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\}&=&\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\}\end{array}$

∎

###  B.2. Proofs of Subsection 4.2

*

###### Proof.

We distinguish two cases:

  * $t$ is meaningless: Then $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\bot\leq t$.

  * $t$ is meaningful: We proceed by induction on $t$. Subcases:

    * $t=x$: Then $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=x\leq x=t$.

    * $t=\lambda x.t^{\prime}$: By i.h. on $t^{\prime}$, one has that $\mathcal{M\\!A}_{{\tt V}}\\!\left(t^{\prime}\right)\leq t^{\prime}$ thus $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\lambda x.\mathcal{M\\!A}_{{\tt V}}\\!\left(t^{\prime}\right)\leq\lambda x.t^{\prime}=t$.

    * $t=t_{1}t_{2}$: By i.h. on $t_{1}$ and $t_{2}$, one has that $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)\leq t_{1}$ and $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)\leq t_{2}$ so that $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)\leq t_{1}t_{2}=t$.

    * $t=t_{1}[x\backslash t_{2}]$: By i.h. on $t_{1}$ and $t_{2}$, $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)\leq t_{1}$ and $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)\leq t_{2}$, hence $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)[x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)]\leq t_{1}[x\backslash t_{2}]=t$. ∎

*

###### Proof.

Let $\mathtt{C}$ be a full context and $t,u\in\Lambda$ be such that $t$ is
dCBV-meaningless. We distinguish two cases:

  * $\mathtt{C}\\!\left<t\right>$ is dCBV-meaningless: Then $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}\\!\left<t\right>\right)=\bot\leq\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}\\!\left<u\right>\right)$.

  * $\mathtt{C}\\!\left<t\right>$ is meaningful: Then by surface genericity (Section 2), one has that $\mathtt{C}\\!\left<u\right>$ is also meaningful. We proceed by induction on $\mathtt{C}$:

    * $\mathtt{C}=\diamond$: This case is impossible because it would mean $\mathtt{C}\\!\left<t\right>=t$ is dCBV-meaningless (by hypothesis) and meaningful at the same time.

    * $\mathtt{C}=\lambda x.\mathtt{C}^{\prime}$: By i.h. on $\mathtt{C}^{\prime}$, one has $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)\leq\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)$, thus $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}\\!\left<t\right>\right)=\lambda x.\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)\overset{\textit{i.h.}}{\leq}\lambda x.\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}\\!\left<u^{\prime}\right>\right)$ by contextual closure.

    * $\mathtt{C}=\mathtt{C}^{\prime}s$: By i.h. on $\mathtt{C}^{\prime}$, one has $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)\leq\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)$, thus $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}\\!\left<t\right>\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)\overset{\textit{i.h.}}{\leq}\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)\allowbreak=\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}\\!\left<u^{\prime}\right>\right)$ by contextual closure.

    * $\mathtt{C}=s\,\mathtt{C}^{\prime}$: By i.h. on $\mathtt{C}^{\prime}$, one has $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)\leq\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)$, thus $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}\\!\left<t\right>\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)\overset{\textit{i.h.}}{\leq}\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)\allowbreak=\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}\\!\left<u^{\prime}\right>\right)$ by contextual closure.

    * $\mathtt{C}=\mathtt{C}^{\prime}[x\backslash s]$: By i.h. on $\mathtt{C}^{\prime}$, one has $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)\leq\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)$, and hence $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}\\!\left<t\right>\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)[x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)]\overset{\textit{i.h.}}{\leq}\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)[x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)]=\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}\\!\left<u^{\prime}\right>\right)$ by contextual closure.

    * $\mathtt{C}=s[x\backslash\mathtt{C}^{\prime}]$: By i.h. on $\mathtt{C}^{\prime}$, one has $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)\leq\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)$, and hence $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}\\!\left<t\right>\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)[x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)]\overset{\textit{i.h.}}{\leq}\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)[x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)]=\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{C}\\!\left<u^{\prime}\right>\right)$ by contextual closure. ∎

*

###### Proof.

We distinguish two cases:

  * $t$ is dCBV-meaningless: Then $u$ is necessarily dCBV-meaningless by Lemma B.4, thus $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\bot$ and $\mathcal{M\\!A}_{{\tt V}}\\!\left(u\right)=\bot$. We set $\mathbf{u}\coloneqq\mathcal{M\\!A}_{{\tt V}}\\!\left(u\right)$, therefore by reflexivity of both relations $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)\rightarrow^{=}_{\textbf{v}_{k}}\mathbf{u}\geq\mathcal{M\\!A}_{{\tt V}}\\!\left(u\right)$.

  * $t$ is dCBV-meaningful: Then $u$ is necessarily dCBV-meaningful by Lemma B.4. Let $t,u\in\Lambda$ such that $t\rightarrow_{\mathrm{v}_{k}}u$. Then there exists a context $\mathtt{V}_{k}$ and $t^{\prime},u^{\prime}\in\Lambda$ such that $t=\mathtt{V}_{k}\\!\left<t^{\prime}\right>$, $u=\mathtt{V}_{k}\\!\left<u^{\prime}\right>$ and $t^{\prime}\mapsto_{\mathcal{R}}u^{\prime}$ for some $\mathcal{R}\in\\{{\tt dB},{\tt sV}\\}$. We reason by induction on $\mathtt{V}_{k}$:

    * $\mathtt{V}_{k}=\diamond$: Then $t=t^{\prime}$ and $u=u^{\prime}$. We distinguish two cases:

      * $\bullet$

$\mathcal{R}={\tt dB}$: Then $t^{\prime}=\mathtt{L}\\!\left<\lambda
x.s_{1}\right>s_{2}$ and $u^{\prime}=\mathtt{L}\\!\left<s_{1}[x\backslash
s_{2}]\right>$ for some list context $\mathtt{L}$ and some
$s_{1},s_{2}\in\Lambda$. Since $t^{\prime}$ is dCBV-meaningful, then using
Lemma B.5.(1), one deduces in particular that $\mathtt{L}\\!\left<\lambda
x.s_{1}\right>$ is dCBV-meaningful. Since $u^{\prime}$ is dCBV-meaningful,
then using Lemma B.5.(2), one deduces in particular that $s_{1}[x\backslash
s_{2}]$ is dCBV-meaningful. Thus, using Corollary B.7, one has that
$\mathcal{M\\!A}_{{\tt V}}\\!\left(t^{\prime}\right)=\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}\\!\left<\lambda
x.s_{1}\right>\right)\mathcal{M\\!A}_{{\tt
V}}\\!\left(s_{2}\right)=\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}\right)\\!\left<\lambda x.\mathcal{M\\!A}_{{\tt
V}}\\!\left(s_{1}\right)\right>\mathcal{M\\!A}_{{\tt V}}\\!\left(s_{2}\right)$
and $\mathcal{M\\!A}_{{\tt V}}\\!\left(u^{\prime}\right)=\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}\\!\left<s_{1}[x\backslash
s_{2}]\right>\right)=\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}\right)\\!\left<\mathcal{M\\!A}_{{\tt
V}}\\!\left(s_{1}[x\backslash s_{2}]\right)\right>=\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}\right)\\!\left<\mathcal{M\\!A}_{{\tt
V}}\\!\left(s_{1}\right)[x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(s_{2}\right)]\right>$. Thus $\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt
V}}\\!\left(t^{\prime}\right)\mapsto_{{\tt dB}}\mathcal{M\\!A}_{{\tt
V}}\\!\left(u^{\prime}\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(u\right)$. We
set $\mathbf{u}:=\mathcal{M\\!A}_{{\tt V}}\\!\left(u\right)$, therefore by
reflexivity $\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)\rightarrow_{\textbf{v}_{k}}\mathbf{u}\geq\mathcal{M\\!A}_{{\tt
V}}\\!\left(u\right)$.

      * $\bullet$

$\mathcal{R}={\tt sV}$: Then
$t^{\prime}=s[x\backslash\mathtt{L}\\!\left<v\right>]$ and
$u^{\prime}=\mathtt{L}\\!\left<s\\{x\backslash v\\}\right>$ for some list
context $\mathtt{L}$, and some $s\in\Lambda$ and $v\in\Upsilon$. Since
$t^{\prime}$ is dCBV-meaningful, then $\mathtt{L}\\!\left<v\right>$ is dCBV-
meaningful by Lemma B.5.(2). Since $u^{\prime}$ is dCBV-meaningful, then using
Lemma B.5.(2), one deduces that $s\\{x\backslash v\\}$ is dCBV-meaningful.
Using Corollaries B.7 and LABEL:lem:cbv_MA(t{x:=v})_<=_MA(t){x:=MA(v)}, one
has that $\mathcal{M\\!A}_{{\tt
V}}\\!\left(t^{\prime}\right)=\mathcal{M\\!A}_{{\tt
V}}\\!\left(s\right)[x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}\right)\\!\left<\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\right>]$ and $\mathcal{M\\!A}_{{\tt
V}}\\!\left(u^{\prime}\right)\leq\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}\right)\\!\left<\mathcal{M\\!A}_{{\tt
V}}\\!\left(s\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\}\right>$. Thus $\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt
V}}\\!\left(t^{\prime}\right)\mapsto_{{\tt sV}}\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}\right)\\!\left<\mathcal{M\\!A}_{{\tt
V}}\\!\left(s\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\}\right>\geq\mathcal{M\\!A}_{{\tt
V}}\\!\left(u^{\prime}\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(u\right)$. We
set $\mathbf{u}\coloneqq\mathcal{M\\!A}_{{\tt
V}}\\!\left(\mathtt{L}\right)\\!\left<\mathcal{M\\!A}_{{\tt
V}}\\!\left(s\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
V}}\\!\left(v\right)\\}\right>$, therefore $\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)\rightarrow_{\textbf{v}_{k}}\mathbf{u}\geq\mathcal{M\\!A}_{{\tt
V}}\\!\left(u\right)$.

    * $\mathtt{V}_{k}=\lambda x.\mathtt{V}_{k-1}$ with $k>0$ or $k=\omega$: By i.h. on $\mathtt{V}_{k-1}$, there is $\mathbf{u}^{\prime}$ such that $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}_{k-1}\\!\left<t^{\prime}\right>\right)\rightarrow^{=}_{\textbf{v}_{k-1}}\mathbf{u}^{\prime}\geq\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}_{k-1}\\!\left<u^{\prime}\right>\right)$. We set $\mathbf{u}\coloneqq\lambda x.\mathbf{u}^{\prime}$, therefore $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}_{k}\\!\left<t^{\prime}\right>\right)=\lambda x.\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}_{k-1}\\!\left<t^{\prime}\right>\right)\rightarrow^{=}_{\textbf{v}_{k}}\mathbf{u}\geq\lambda x.\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}_{k-1}\\!\left<u^{\prime}\right>\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}_{k}\\!\left<u^{\prime}\right>\right)$.

    * $\mathtt{V}_{k}=\mathtt{V}^{\prime}_{k}s$: Thus $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}_{k}\\!\left<t^{\prime}\right>\right)\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)$ and $\mathcal{M\\!A}_{{\tt V}}\\!\left(u\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}_{k}\\!\left<u^{\prime}\right>\right)\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)$. By i.h. on $\mathtt{V}^{\prime}_{k}$, there is $\mathbf{u}^{\prime}\in\mathbf{\Lambda}$ such that $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}^{\prime}_{k}\\!\left<t^{\prime}\right>\right)\rightarrow^{=}_{\textbf{v}_{k}}\mathbf{u}^{\prime}\geq\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}^{\prime}_{k}\\!\left<u^{\prime}\right>\right)$. We set $\mathbf{u}\coloneqq\mathbf{u}^{\prime}\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)$, therefore $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)\rightarrow^{=}_{\textbf{v}_{k}}\mathbf{u}\geq\mathcal{M\\!A}_{{\tt V}}\\!\left(u\right)$.

    * $\mathtt{V}_{k}=s\,\mathtt{V}^{\prime}_{k}$: Thus $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}_{k}\\!\left<t^{\prime}\right>\right)$ and $\mathcal{M\\!A}_{{\tt V}}\\!\left(u\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}_{k}\\!\left<u^{\prime}\right>\right)$. By i.h. on $\mathtt{V}^{\prime}_{k}$, there is $\mathbf{u}^{\prime}\in\mathbf{\Lambda}$ such that $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}^{\prime}_{k}\\!\left<t^{\prime}\right>\right)\rightarrow^{=}_{\textbf{v}_{k}}\mathbf{u}^{\prime}\geq\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}^{\prime}_{k}\\!\left<u^{\prime}\right>\right)$. We set $\mathbf{u}\coloneqq\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)\mathbf{u}^{\prime}$, therefore $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)\rightarrow^{=}_{\textbf{v}_{k}}\mathbf{u}\geq\mathcal{M\\!A}_{{\tt V}}\\!\left(u\right)$.

    * $\mathtt{V}_{k}=\mathtt{V}^{\prime}_{k}[x\backslash s]$: Thus $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}_{k}\\!\left<t^{\prime}\right>\right)[x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)]$ and $\mathcal{M\\!A}_{{\tt V}}\\!\left(u\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}_{k}\\!\left<u^{\prime}\right>\right)[x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)]$. By i.h. on $\mathtt{V}^{\prime}_{k}$, there is $\mathbf{u}^{\prime}\in\mathbf{\Lambda}$ such that $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}^{\prime}_{k}\\!\left<t^{\prime}\right>\right)\rightarrow^{=}_{\textbf{v}_{k}}\mathbf{u}^{\prime}\geq\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}^{\prime}_{k}\\!\left<u^{\prime}\right>\right)$. We set $\mathbf{u}\coloneqq\mathbf{u}^{\prime}[x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)]$, hence $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)\rightarrow^{=}_{\textbf{v}_{k}}\mathbf{u}\geq\mathcal{M\\!A}_{{\tt V}}\\!\left(u\right)$.

    * $\mathtt{V}_{k}=s[x\backslash\mathtt{V}^{\prime}_{k}]$: Thus $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)[x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}_{k}\\!\left<t^{\prime}\right>\right)]$ and $\mathcal{M\\!A}_{{\tt V}}\\!\left(u\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)[x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}_{k}\\!\left<u^{\prime}\right>\right)]$. By i.h. on $\mathtt{V}^{\prime}_{k}$, there is $\mathbf{u}^{\prime}\in\mathbf{\Lambda}$ such that $\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}^{\prime}_{k}\\!\left<t^{\prime}\right>\right)\rightarrow^{=}_{\textbf{v}_{k}}\mathbf{u}^{\prime}\geq\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{V}^{\prime}_{k}\\!\left<u^{\prime}\right>\right)$. We set $\mathbf{u}\coloneqq\mathcal{M\\!A}_{{\tt V}}\\!\left(s\right)[x\backslash\mathbf{u}^{\prime}]$, hence $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)\rightarrow^{=}_{\textbf{v}_{k}}\mathbf{u}\geq\mathcal{M\\!A}_{{\tt V}}\\!\left(u\right)$. ∎

*

###### Proof.

Let $\mathbf{t},\mathbf{u},\mathbf{t}^{\prime}\in\mathbf{\Lambda}$ such that
$\mathbf{t}\leq\mathbf{t}^{\prime}$ and
$\mathbf{t}\rightarrow_{\textbf{v}_{k}}\mathbf{u}$. Then
$\mathbf{t}=\mathbf{V}_{k}\\!\left<\mathbf{t}_{r}\right>$ and
$\mathbf{u}=\mathbf{V}_{k}\\!\left<\mathbf{u}_{r}\right>$ with
$\mathbf{t}_{r}\mapsto_{\mathcal{R}}\mathbf{u}_{r}$ for some
$\mathbf{t}_{r},\mathbf{u}_{r}\in\mathbf{\Lambda}$ and $\mathcal{R}\in\\{{\tt
dB},{\tt sV}\\}$. Let us proceed by induction on $\mathbf{V}_{k}$:

  * $\mathbf{V}_{k}=\diamond$: Then $\mathbf{t}=\mathbf{t}_{r}$ and $\mathbf{u}=\mathbf{u}_{r}$. We distinguish two cases:

    * $\mathcal{R}={\tt dB}$: Then $\mathbf{t}_{r}=\mathbf{L}\\!\left<\lambda x.\mathbf{s}_{1}\right>\mathbf{s}_{2}$ and $\mathbf{u}_{r}=\mathbf{L}\\!\left<\mathbf{s}_{1}[x\backslash\mathbf{s}_{2}]\right>$ for some list context $\mathbf{L}$ and $\mathbf{s}_{1},\mathbf{s}_{2}\in\mathbf{\Lambda}$. Since $\mathbf{t}\leq\mathbf{t}^{\prime}$, by induction on $\mathbf{L}$, one can prove that $\mathbf{t}^{\prime}=\mathbf{L}^{\prime}\\!\left<\lambda x.\mathbf{s}^{\prime}_{1}\right>\mathbf{s}^{\prime}_{2}$ with $\mathbf{L}\leq\mathbf{L}^{\prime}$, $\mathbf{s}_{1}\leq\mathbf{s}^{\prime}_{1}$ and $\mathbf{s}_{2}\leq\mathbf{s}^{\prime}_{2}$ for some list context $\mathbf{L}^{\prime}$ and $\mathbf{s}^{\prime}_{1},\mathbf{s}^{\prime}_{2}\in\mathbf{\Lambda}$. Taking $\mathbf{u}^{\prime}=\mathbf{L}^{\prime}\\!\left<\mathbf{s}^{\prime}_{1}[x\backslash\mathbf{s}^{\prime}_{2}]\right>$ concludes this case since $\mathbf{t}^{\prime}=\mathbf{L}^{\prime}\\!\left<\lambda x.\mathbf{s}^{\prime}_{1}\right>\mathbf{s}^{\prime}_{2}\rightarrow_{\textbf{v}_{k}}\mathbf{L}^{\prime}\\!\left<\mathbf{s}^{\prime}_{1}[x\backslash\mathbf{s}^{\prime}_{2}]\right>=\mathbf{u}^{\prime}$ and by transitivity $\mathbf{s}_{1}[x\backslash\mathbf{s}_{2}]\leq\mathbf{s}^{\prime}_{1}[x\backslash\mathbf{s}^{\prime}_{2}]$ thus $\mathbf{L}\\!\left<\mathbf{s}_{1}[x\backslash\mathbf{s}_{2}]\right>\leq\mathbf{L}^{\prime}\\!\left<\mathbf{s}^{\prime}_{1}[x\backslash\mathbf{s}^{\prime}_{2}]\right>=\mathbf{u}^{\prime}$ using Lemma B.3.

    * $\mathcal{R}={\tt sV}$: Then $\mathbf{t}_{r}=\mathbf{s}[x\backslash\mathbf{L}\\!\left<\mathbf{v}\right>]$ and $\mathbf{u}_{r}=\mathbf{L}\\!\left<\mathbf{s}\\{x\backslash\mathbf{v}\\}\right>$ for some list context $\mathbf{L}$, $\mathbf{s}\in\mathbf{\Lambda}$ and $\mathbf{v}\in\mathbf{\Upsilon}$. Since $\mathbf{t}\leq\mathbf{t}^{\prime}$, by induction on $\mathbf{L}$, one can prove that $\mathbf{t}^{\prime}=\mathbf{s}^{\prime}[x\backslash\mathbf{L}^{\prime}\\!\left<\mathbf{v}^{\prime}\right>]$ with $\mathbf{L}\leq\mathbf{L}^{\prime}$, $\mathbf{s}\leq\mathbf{s}^{\prime}$ and $\mathbf{v}\leq\mathbf{v}^{\prime}$ for some list context $\mathbf{L}^{\prime}$, $\mathbf{s}^{\prime}\in\mathbf{\Lambda}$ and $\mathbf{v}^{\prime}\in\mathbf{\Upsilon}$. Taking $\mathbf{u}^{\prime}=\mathbf{L}^{\prime}\\!\left<\mathbf{s}^{\prime}\\{x\backslash\mathbf{v}^{\prime}\\}\right>$ concludes this case since $\mathbf{t}^{\prime}=\mathbf{s}^{\prime}[x\backslash\mathbf{L}^{\prime}\\!\left<\mathbf{v}^{\prime}\right>]\rightarrow_{\textbf{v}_{k}}\mathbf{L}^{\prime}\\!\left<\mathbf{s}^{\prime}\\{x\backslash\mathbf{v}^{\prime}\\}\right>$ and by LABEL:lem:cbv_t1_<=_t2_and_v1_<=_v2_==>_t1{x:=v1}_<=_t2{x:=v2} $\mathbf{s}\\{x\backslash\mathbf{v}\\}\leq\mathbf{s}^{\prime}\\{x\backslash\mathbf{v}^{\prime}\\}$, thus $\mathbf{L}\\!\left<\mathbf{s}\\{x\backslash\mathbf{v}\\}\right>\leq\mathbf{L}^{\prime}\\!\left<\mathbf{s}^{\prime}\\{x\backslash\mathbf{v}^{\prime}\\}\right>=\mathbf{u}^{\prime}$ using Lemma B.3.

  * $\mathbf{V}_{k}=\lambda x.\mathbf{V}^{\prime}_{m}$ with either $k>0$ and $m=k-1$, or $k=m=\omega$: Then $\mathbf{t}=\lambda x.\mathbf{V}^{\prime}_{m}\\!\left<\mathbf{t}_{r}\right>$ and $\mathbf{u}=\lambda x.\mathbf{V}^{\prime}_{m}\\!\left<\mathbf{u}_{r}\right>$ thus $\mathbf{t}^{\prime}=\lambda x.\mathbf{t}^{\prime}_{1}$ for some $\mathbf{t}^{\prime}_{1}\in\mathbf{\Lambda}$ such that $\mathbf{V}^{\prime}_{m}\\!\left<\mathbf{t}_{r}\right>\leq\mathbf{t}^{\prime}_{1}$. Since $\mathbf{V}^{\prime}_{m}\\!\left<\mathbf{t}_{r}\right>\rightarrow_{\textbf{v}_{m}}\mathbf{V}^{\prime}_{m}\\!\left<\mathbf{u}_{r}\right>$, by i.h. on $\mathbf{V}^{\prime}_{m}$, one obtains $\mathbf{u}^{\prime}_{1}\in\mathbf{\Lambda}$ such that $\mathbf{t}^{\prime}_{1}\rightarrow_{\textbf{v}_{m}}\mathbf{u}^{\prime}_{1}$ and $\mathbf{V}^{\prime}_{m}\\!\left<\mathbf{u}_{r}\right>\leq\mathbf{u}^{\prime}_{1}$. Taking $\mathbf{u}^{\prime}=\lambda x.\mathbf{u}^{\prime}_{1}$ concludes this case since $\mathbf{t}^{\prime}=\lambda x.\mathbf{t}^{\prime}_{1}\rightarrow_{\textbf{v}_{k}}\lambda x.\mathbf{u}^{\prime}_{1}=\mathbf{u}^{\prime}$ and $\mathbf{u}=\lambda x.\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>\leq\lambda x.\mathbf{u}^{\prime}_{1}=\mathbf{u}^{\prime}$.

  * $\mathbf{V}_{k}=\mathbf{V}^{\prime}_{k}\,\mathbf{s}$: Then $\mathbf{t}=\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>\mathbf{s}$ and $\mathbf{u}=\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>\mathbf{s}$ thus $\mathbf{t}^{\prime}=\mathbf{t}^{\prime}_{1}\,\mathbf{s}^{\prime}$ for some $\mathbf{t}^{\prime}_{1},\mathbf{s}\in\mathbf{\Lambda}$ such that $\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>\leq\mathbf{t}^{\prime}_{1}$ and $\mathbf{s}\leq\mathbf{s}^{\prime}$. Since $\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>\rightarrow_{\textbf{v}_{k}}\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>$, by i.h. on $\mathbf{V}^{\prime}_{k}$, one obtains $\mathbf{u}^{\prime}_{1}\in\mathbf{\Lambda}$ such that $\mathbf{t}^{\prime}_{1}\rightarrow_{\textbf{v}_{k}}\mathbf{u}^{\prime}_{1}$ and $\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>\leq\mathbf{u}^{\prime}_{1}$. Taking $\mathbf{u}^{\prime}=\mathbf{u}^{\prime}_{1}\mathbf{s}^{\prime}$ concludes this case since $\mathbf{t}^{\prime}=\mathbf{t}^{\prime}_{1}\mathbf{s}^{\prime}\rightarrow_{\textbf{v}_{k}}\mathbf{u}^{\prime}_{1}\mathbf{s}^{\prime}=\mathbf{u}^{\prime}$ and $\mathbf{u}=\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>\mathbf{s}\leq\mathbf{u}^{\prime}_{1}\mathbf{s}^{\prime}=\mathbf{u}^{\prime}$ by transitivity.

  * $\mathbf{V}_{k}=\mathbf{s}\,\mathbf{V}^{\prime}_{k}$: Then $\mathbf{t}=\mathbf{s}\,\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>$ and $\mathbf{u}=\mathbf{s}\,\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>$ thus $\mathbf{t}^{\prime}=\mathbf{s}^{\prime}\,\mathbf{t}^{\prime}_{1}$ for some $\mathbf{s},\mathbf{t}^{\prime}_{1}\in\mathbf{\Lambda}$ such that $\mathbf{s}\leq\mathbf{s}^{\prime}$ and $\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>\leq\mathbf{t}^{\prime}_{1}$. Since $\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>\rightarrow_{\textbf{v}_{k}}\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>$, by i.h. on $\mathbf{V}^{\prime}_{k}$, one obtains $\mathbf{u}^{\prime}_{1}\in\mathbf{\Lambda}$ such that $\mathbf{t}^{\prime}_{1}\rightarrow_{\textbf{v}_{k}}\mathbf{u}^{\prime}_{1}$ and $\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>\leq\mathbf{u}^{\prime}_{1}$. Taking $\mathbf{u}^{\prime}=\mathbf{s}^{\prime}\mathbf{u}^{\prime}_{1}$ concludes this case since $\mathbf{t}^{\prime}=\mathbf{s}^{\prime}\mathbf{t}^{\prime}_{1}\rightarrow_{\textbf{v}_{k}}\mathbf{s}^{\prime}\mathbf{u}^{\prime}_{1}=\mathbf{u}^{\prime}$ and $\mathbf{u}=\mathbf{s}\,\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>\leq\mathbf{s}^{\prime}\mathbf{u}^{\prime}_{1}=\mathbf{u}^{\prime}$ by transitivity.

  * $\mathbf{V}_{k}=\mathbf{V}^{\prime}_{k}[x\backslash\mathbf{s}]$: Then $\mathbf{t}=\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>[x\backslash\mathbf{s}]$ and $\mathbf{u}=\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>[x\backslash\mathbf{s}]$ thus $\mathbf{t}^{\prime}=\mathbf{t}^{\prime}_{1}[x\backslash\mathbf{s}^{\prime}]$ for some $\mathbf{t}^{\prime}_{1},\mathbf{s}\in\mathbf{\Lambda}$ such that $\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>\leq\mathbf{t}^{\prime}_{1}$ and $\mathbf{s}\leq\mathbf{s}^{\prime}$. Since $\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>\rightarrow_{\textbf{v}_{k}}\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>$, by i.h. on $\mathbf{V}^{\prime}_{k}$, one obtains $\mathbf{u}^{\prime}_{1}\in\mathbf{\Lambda}$ such that $\mathbf{t}^{\prime}_{1}\rightarrow_{\textbf{v}_{k}}\mathbf{u}^{\prime}_{1}$ and $\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>\leq\mathbf{u}^{\prime}_{1}$. Taking $\mathbf{u}^{\prime}=\mathbf{u}^{\prime}_{1}[x\backslash\mathbf{s}^{\prime}]$ concludes this case since $\mathbf{t}^{\prime}=\mathbf{t}^{\prime}_{1}[x\backslash\mathbf{s}^{\prime}]\rightarrow_{\textbf{v}_{k}}\mathbf{u}^{\prime}_{1}[x\backslash\mathbf{s}^{\prime}]=\mathbf{u}^{\prime}$ and $\mathbf{u}=\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>[x\backslash\mathbf{s}]\leq\mathbf{u}^{\prime}_{1}[x\backslash\mathbf{s}^{\prime}]=\mathbf{u}^{\prime}$ by transitivity.

  * $\mathbf{V}_{k}=\mathbf{s}[x\backslash\mathbf{V}^{\prime}_{k}]$: Then $\mathbf{t}=\mathbf{s}[x\backslash\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>]$ and $\mathbf{u}=\mathbf{s}[x\backslash\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>]$ thus $\mathbf{t}^{\prime}=\mathbf{s}^{\prime}[x\backslash\mathbf{t}^{\prime}_{1}]$ for some $\mathbf{s},\mathbf{t}^{\prime}_{1}\in\mathbf{\Lambda}$ such that $\mathbf{s}\leq\mathbf{s}^{\prime}$ and $\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>\leq\mathbf{t}^{\prime}_{1}$. Since $\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>\rightarrow_{\textbf{v}_{k}}\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>$, by i.h. on $\mathbf{V}^{\prime}_{k}$, one obtains $\mathbf{u}^{\prime}_{1}\in\mathbf{\Lambda}$ such that $\mathbf{t}^{\prime}_{1}\rightarrow_{\textbf{v}_{k}}\mathbf{u}^{\prime}_{1}$ and $\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>\leq\mathbf{u}^{\prime}_{1}$. Taking $\mathbf{u}^{\prime}=\mathbf{s}^{\prime}[x\backslash\mathbf{u}^{\prime}_{1}]$ concludes this case since $\mathbf{t}^{\prime}=\mathbf{s}^{\prime}[x\backslash\mathbf{t}^{\prime}_{1}]\rightarrow_{\textbf{v}_{k}}\mathbf{s}^{\prime}[x\backslash\mathbf{u}^{\prime}_{1}]=\mathbf{u}^{\prime}$ and $\mathbf{u}=\mathbf{s}[x\backslash\mathbf{V}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>]\leq\mathbf{s}^{\prime}[x\backslash\mathbf{u}^{\prime}_{1}]=\mathbf{u}^{\prime}$ by transitivity. ∎

Let us recall mutual inductive definitions of ${\tt bvr}_{\textbf{v}_{k}}$,
${\tt bne}_{\textbf{v}_{k}}$ and ${\tt bno}_{\textbf{v}_{k}}$ for
$k\in\mathbb{N}^{\omega}$:

$\begin{array}[]{rcl}{\tt bvr}_{\textbf{v}_{k}}&\coloneqq&x\;|\;{\tt
bvr}_{\textbf{v}_{k}}[x\backslash{\tt bne}_{\textbf{v}_{k}}]\\\\[5.69046pt]
{\tt bne}_{\textbf{v}_{k}}&\coloneqq&{\tt bvr}_{\textbf{v}_{k}}\,{\tt
bno}_{\textbf{v}_{k}}\;|\;{\tt bne}_{\textbf{v}_{k}}\,{\tt
bno}_{\textbf{v}_{k}}\;|\;{\tt bne}_{\textbf{v}_{k}}[x\backslash{\tt
bne}_{\textbf{v}_{k}}]\\\\[5.69046pt] {\tt
bno}_{\textbf{v}_{0}}&\coloneqq&\lambda x.\mathbf{t}\;|\;{\tt
bvr}_{\textbf{v}_{0}}\;|\;{\tt bne}_{\textbf{v}_{0}}\;|\;{\tt
bno}_{\textbf{v}_{0}}[x\backslash{\tt bne}_{\textbf{v}_{0}}]\\\ {\tt
bno}_{\textbf{v}_{i+1}}&\coloneqq&\lambda x.{\tt
bno}_{\textbf{v}_{i}}\;|\;{\tt bvr}_{\textbf{v}_{i+1}}\;|\;{\tt
bne}_{\textbf{v}_{i+1}}\;|\;{\tt bno}_{\textbf{v}_{i+1}}[x\backslash{\tt
bne}_{\textbf{v}_{i+1}}]\qquad(i\in\mathbb{N})\\\ {\tt
bno}_{\textbf{v}_{\omega}}&\coloneqq&\lambda x.{\tt
bno}_{\textbf{v}_{\omega}}\;|\;{\tt bvr}_{\textbf{v}_{\omega}}\;|\;{\tt
bne}_{\textbf{v}_{\omega}}\;|\;{\tt bno}_{\textbf{v}_{\omega}}[x\backslash{\tt
bne}_{\textbf{v}_{\omega}}]\end{array}$

*

###### Proof.

We strengthen the induction hypothesis:

  * If $t\in{\tt vr}_{\mathrm{v}_{k}}$ then $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)\in{\tt bvr}_{\textbf{v}_{k}}$.

  * If $t\in{\tt ne}_{\mathrm{v}_{k}}$ then $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)\in{\tt bne}_{\textbf{v}_{k}}$.

  * If $t\in{\tt no}_{\mathrm{v}_{k}}$ then $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)\in{\tt bno}_{\textbf{v}_{k}}$.

Since $t\in{\tt no}_{\mathrm{n}_{k}}$ then in particular $t\in{\tt
no}_{\mathrm{n}_{0}}$ thus $t$ is dCBV-meaningful. By mutual induction on
$t\in{\tt vr}_{\mathrm{v}_{k}}$, $t\in{\tt ne}_{\mathrm{v}_{k}}$ and $t\in{\tt
no}_{\mathrm{v}_{k}}$. Cases:

  * $t\in{\tt vr}_{\mathrm{v}_{k}}$: We distinguish two cases:

    * $t=x$: Then $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=x\in{\tt bvr}_{\textbf{v}_{k}}$.

    * $t=t_{1}[x\backslash t_{2}]$ with $t_{1}\in{\tt vr}_{\mathrm{v}_{k}}$ and $t_{2}\in{\tt ne}_{\mathrm{v}_{k}}$: By i.h. on $t_{1}$ and $t_{2}$, one has that $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)\in{\tt bvr}_{\textbf{v}_{k}}$ and $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)\in{\tt bne}_{\textbf{v}_{k}}$ thus $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)[x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)]\subseteq{\tt bvr}_{\textbf{v}_{k}}[x\backslash{\tt bne}_{\textbf{v}_{k}}]\subseteq{\tt bvr}_{\textbf{v}_{k}}$.

  * $t\in{\tt ne}_{\mathrm{v}_{k}}$: We distinguish three cases:

    * $t=t_{1}t_{2}$ with $t_{1}\in{\tt vr}_{\mathrm{v}_{k}}$ and $t_{2}\in{\tt no}_{\mathrm{v}_{k}}$: Then by i.h. on $t_{1}$ and $t_{2}$, one has that $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)\in{\tt bvr}_{\textbf{v}_{k}}$ and $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)\in{\tt bno}_{\textbf{v}_{k}}$ thus $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)\in{\tt bvr}_{\textbf{v}_{k}}{\tt bno}_{\textbf{v}_{k}}\subseteq{\tt bne}_{\textbf{v}_{k}}$.

    * $t=t_{1}t_{2}$ with $t_{1}\in{\tt ne}_{\mathrm{v}_{k}}$ and $t_{2}\in{\tt no}_{\mathrm{v}_{k}}$: Then by i.h. on $t_{1}$ and $t_{2}$, one has that $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)\in{\tt bne}_{\textbf{v}_{k}}$ and $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)\in{\tt bno}_{\textbf{v}_{k}}$ thus $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)\in{\tt bne}_{\textbf{v}_{k}}{\tt bno}_{\textbf{v}_{k}}\subseteq{\tt bne}_{\textbf{v}_{k}}$.

    * $t=t_{1}[x\backslash t_{2}]$ with $t_{1},t_{2}\in{\tt ne}_{\mathrm{v}_{k}}$: By i.h. on $t_{1}$ and $t_{2}$, one has that $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)\in{\tt bne}_{\textbf{v}_{k}}$ and $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)\in{\tt bne}_{\textbf{v}_{k}}$ thus $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)[x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)]\subseteq{\tt bne}_{\textbf{v}_{k}}[x\backslash{\tt bne}_{\textbf{v}_{k}}]\subseteq{\tt bne}_{\textbf{v}_{k}}$.

  * $t\in{\tt no}_{\mathrm{v}_{k}}$: We distinguish four cases:

    * $t=\lambda x.t^{\prime}$: We distinguish three cases:

      * $\bullet$

$k=0$: Then $t=\lambda x.t^{\prime}$ and $\mathcal{M\\!A}_{{\tt
V}}\\!\left(t\right)=\lambda x.\mathcal{M\\!A}_{{\tt
V}}\\!\left(t^{\prime}\right)\in{\tt bno}_{\textbf{v}_{0}}$.

      * $\bullet$

$k=i+1$ and $t^{\prime}\in{\tt no}_{\mathrm{v}_{i}}$ for some
$i\in\mathbb{N}$: By i.h. on $t^{\prime}$, one has that $\mathcal{M\\!A}_{{\tt
V}}\\!\left(t^{\prime}\right)\in{\tt bno}_{\textbf{v}_{i}}$ thus
$\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\lambda x.\mathcal{M\\!A}_{{\tt
V}}\\!\left(t^{\prime}\right)\in\lambda x.{\tt
bno}_{\textbf{v}_{i}}\subseteq{\tt bno}_{\textbf{v}_{k}}$.

      * $\bullet$

$k=\omega$ and $t^{\prime}\in{\tt no}_{\mathrm{v}_{\omega}}$: By i.h. on
$t^{\prime}$, one has that $\mathcal{M\\!A}_{{\tt
V}}\\!\left(t^{\prime}\right)\in{\tt bno}_{\textbf{v}_{\omega}}$ thus
$\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\lambda x.\mathcal{M\\!A}_{{\tt
V}}\\!\left(t^{\prime}\right)\in\lambda x.{\tt
bno}_{\textbf{v}_{\omega}}\subseteq{\tt bno}_{\textbf{v}_{\omega}}$.

    * $t\in{\tt vr}_{\mathrm{v}_{k}}$: Then by i.h. on $t$, one has that $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)\in{\tt bvr}_{\textbf{v}_{k}}\subseteq{\tt bno}_{\textbf{v}_{k}}$.

    * $t\in{\tt ne}_{\mathrm{v}_{k}}$: Then by i.h. on $t$, one has that $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)\in{\tt bne}_{\textbf{v}_{k}}\subseteq{\tt bno}_{\textbf{v}_{k}}$.

    * $t=t_{1}[x\backslash t_{2}]$ with $t_{1}\in{\tt no}_{\mathrm{v}_{k}}$ and $t_{2}\in{\tt ne}_{\mathrm{v}_{k}}$: By i.h. on $t_{1}$ and $t_{2}$, one has that $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)\in{\tt bno}_{\textbf{v}_{k}}$ and $\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)\in{\tt bne}_{\textbf{v}_{k}}$ thus $\mathcal{M\\!A}_{{\tt V}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{1}\right)[x\backslash\mathcal{M\\!A}_{{\tt V}}\\!\left(t_{2}\right)]\subseteq{\tt bno}_{\textbf{v}_{k}}[x\backslash{\tt bne}_{\textbf{v}_{k}}]\subseteq{\tt bno}_{\textbf{v}_{k}}$.

∎

Let us recall inductive definitions of stratified equality, where
$k\in\mathbb{N}^{\omega}$ and $i\in\mathbb{N}$:

$\begin{array}[]{c}\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
2.16647pt\hbox{}}\vbox{\hbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hskip 5.0pt\hbox{\lower
2.15277pt\hbox{\\!\scriptsize$({\tt
var})$}}}\hbox{\hbox{\hbox{}\hbox{$\phantom{\overset{\scriptscriptstyle
i}{\approx}}\hfil\lx@intercol$}}\hbox{$x\overset{\scriptscriptstyle
k}{\approx}x$}}\par}\par}}}$}\hskip
11.38092pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{}\vbox{\hbox{\hbox{\lower
18.0pt\vbox{\vskip 3.01385pt\hrule height=0.4pt\vskip 3.01385pt\par}}\hskip
5.0pt\hbox{\lower 2.15277pt\hbox{\\!\scriptsize$({\tt app})$}}}\hbox{\hskip
1.8633pt\hbox{\hbox{\hbox{}\hbox{\hbox{}\hskip
15.00002pt\hbox{\hbox{\hbox{}\hbox{$t_{1}\overset{\scriptscriptstyle
k}{\approx}u_{1}$}}\hbox{$t_{2}\overset{\scriptscriptstyle
k}{\approx}u_{2}$}}}}\hbox{$t_{1}t_{2}\overset{\scriptscriptstyle
k}{\approx}u_{1}u_{2}$}}}\par}\par}}}$}\hskip
11.38092pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
14.78416pt\hbox{}}\vbox{\hbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hskip 5.0pt\hbox{\lower
2.15277pt\hbox{\\!\scriptsize$({\tt
es})$}}}\hbox{\hbox{\hbox{}\hbox{\hbox{}\hskip
15.00002pt\hbox{\hbox{\hbox{}\hbox{$t_{1}\overset{\scriptscriptstyle
k}{\approx}u_{1}$}}\hbox{$t_{2}\overset{\scriptscriptstyle
k}{\approx}u_{2}$}}}}\hbox{$t_{1}[x\backslash
t_{2}]\overset{\scriptscriptstyle k}{\approx}u_{1}[x\backslash
u_{2}]$}}\par}\par}}}$}\\\\[11.38092pt]
\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
9.5289pt\hbox{}}\vbox{\hbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hskip 5.0pt\hbox{\lower
2.15277pt\hbox{\\!\scriptsize$({\tt
abs})$}}}\hbox{\hbox{\hbox{}\hbox{$\phantom{t\overset{\scriptscriptstyle
k}{\approx}u}\hfil\lx@intercol$}}\hbox{$\lambda x.t\overset{\scriptscriptstyle
0}{\approx}\lambda y.u$}}\par}\par}}}$}\hskip
22.76228pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
17.82805pt\hbox{}}\vbox{\hbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hskip 5.0pt\hbox{\lower
2.15277pt\hbox{\\!\scriptsize$({\tt
abs})$}}}\hbox{\hbox{\hbox{}\hbox{$t\overset{\scriptscriptstyle
i}{\approx}u$}}\hbox{$\lambda x.t\overset{\scriptscriptstyle
i+1}{\approx}\lambda x.u$}}\par}\par}}}$}\hskip
22.76228pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
12.41142pt\hbox{}}\vbox{\hbox{\hbox{\lower 18.0pt\vbox{\vskip 3.01385pt\hrule
height=0.4pt\vskip 3.01385pt\par}}\hskip 5.0pt\hbox{\lower
2.15277pt\hbox{\\!\scriptsize$({\tt
abs})$}}}\hbox{\hbox{\hbox{}\hbox{$t\overset{\scriptscriptstyle\omega}{\approx}u$}}\hbox{$\lambda
x.t\overset{\scriptscriptstyle\omega}{\approx}\lambda
x.u$}}\par}\par}}}$}\end{array}$

*

###### Proof.

Let $\mathbf{t},\mathbf{u}\in\mathbf{\Lambda}$ such that
$\mathbf{t}\leq\mathbf{u}$ We strengthen the induction hypothesis:

  * If $\mathbf{t}\in{\tt bvr}_{\textbf{v}_{k}}$ then $\mathbf{u}\in{\tt bvr}_{\textbf{v}_{k}}$.

  * If $\mathbf{t}\in{\tt bne}_{\textbf{v}_{k}}$ then $\mathbf{u}\in{\tt bne}_{\textbf{v}_{k}}$.

  * If $\mathbf{t}\in{\tt bno}_{\textbf{v}_{k}}$ then $\mathbf{u}\in{\tt bno}_{\textbf{v}_{k}}$.

Moreover, $\mathbf{t}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}$.

We prove it by mutual induction on $\mathbf{t}\in{\tt bvr}_{\textbf{v}_{k}}$,
$\mathbf{t}\in{\tt bne}_{\textbf{v}_{k}}$ and $\mathbf{t}\in{\tt
bno}_{\textbf{v}_{k}}$:

  * $\mathbf{t}\in{\tt bvr}_{\textbf{v}_{k}}$:

    * $\mathbf{t}=x$: Then necessarily $\mathbf{u}=x$ thus $\mathbf{u}\in{\tt bvr}_{\textbf{v}_{k}}$ and $\mathbf{t}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}$ using $({\tt var})$.

    * $\mathbf{t}=\mathbf{t}_{1}[x\backslash\mathbf{t}_{2}]$ with $\mathbf{t}_{1}\in{\tt bvr}_{\textbf{v}_{k}}$ and $\mathbf{t}_{2}\in{\tt bne}_{\textbf{v}_{k}}$. Then necessarilyn $\mathbf{u}=\mathbf{u}_{1}[x\backslash\mathbf{u}_{2}]$ with $\mathbf{t}_{1}\leq\mathbf{u}_{1}$ and $\mathbf{t}_{2}\leq\mathbf{u}_{2}$ for some $\mathbf{u}_{1},\mathbf{u}_{2}\in\mathbf{\Lambda}$. By i.h. on $\mathbf{t}_{1}$ and $\mathbf{t}_{2}$, one has that $\mathbf{u}_{1}\in{\tt bvr}_{\textbf{v}_{k}}$, $\mathbf{u}_{2}\in{\tt bne}_{\textbf{v}_{k}}$, $\mathbf{t}_{1}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}_{1}$ and $\mathbf{t}_{2}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}_{2}$. Thus $\mathbf{u}=\mathbf{u}_{1}[x\backslash\mathbf{u}_{2}]\in{\tt bvr}_{\textbf{v}_{k}}[x\backslash{\tt bne}_{\textbf{v}_{k}}]\subseteq{\tt bvr}_{\textbf{v}_{k}}$ and $\mathbf{t}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}$ using $({\tt es})$.

  * $\mathbf{t}\in{\tt bne}_{\textbf{v}_{k}}$:

    * $\mathbf{t}=\mathbf{t}_{1}\mathbf{t}_{2}$ with $\mathbf{t}_{1}\in{\tt bvr}_{\textbf{v}_{k}}$ and $\mathbf{t}_{2}\in{\tt bno}_{\textbf{v}_{k}}$: Necessarily $\mathbf{u}=\mathbf{u}_{1}\mathbf{u}_{2}$ with $\mathbf{t}_{1}\leq\mathbf{u}_{1}$ and $\mathbf{t}_{2}\leq\mathbf{u}_{2}$. By i.h. on $\mathbf{t}_{1}$ and $\mathbf{t}_{2}$, one has $\mathbf{u}_{1}\in{\tt bvr}_{\textbf{v}_{k}}$, $\mathbf{u}_{2}\in{\tt bno}_{\textbf{v}_{k}}$, $\mathbf{t}_{1}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}_{1}$ and $\mathbf{t}_{2}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}_{2}$. Thus $\mathbf{u}=\mathbf{u}_{1}\mathbf{u}_{2}\in{\tt bvr}_{\textbf{v}_{k}}\,{\tt bno}_{\textbf{v}_{k}}\subseteq{\tt bne}_{\textbf{v}_{k}}$ and $\mathbf{t}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}$ using $({\tt app})$.

    * $\mathbf{t}=\mathbf{t}_{1}\mathbf{t}_{2}$ with $\mathbf{t}_{1}\in{\tt bne}_{\textbf{v}_{k}}$ and $\mathbf{t}_{2}\in{\tt bno}_{\textbf{v}_{k}}$: Then necessarily $\mathbf{u}=\mathbf{u}_{1}\mathbf{u}_{2}$ with $\mathbf{t}_{1}\leq\mathbf{u}_{1}$ and $\mathbf{t}_{2}\leq\mathbf{u}_{2}$. By i.h. on $\mathbf{t}_{1}$ and $\mathbf{t}_{2}$, one has that $\mathbf{u}_{1}\in{\tt bne}_{\textbf{v}_{k}}$, $\mathbf{u}_{2}\in{\tt bno}_{\textbf{v}_{k}}$, $\mathbf{t}_{1}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}_{1}$ and $\mathbf{t}_{2}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}_{2}$. Thus $\mathbf{u}=\mathbf{u}_{1}\mathbf{u}_{2}\in{\tt bne}_{\textbf{v}_{k}}{\tt bno}_{\textbf{v}_{k}}\subseteq{\tt bne}_{\textbf{v}_{k}}$ and $\mathbf{t}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}$ using $({\tt app})$.

    * $\mathbf{t}=\mathbf{t}_{1}[x\backslash\mathbf{t}_{2}]$ with $\mathbf{t}_{1},\mathbf{t}_{2}\in{\tt bne}_{\textbf{v}_{k}}$: Then necessarily $\mathbf{u}=\mathbf{u}_{1}[x\backslash\mathbf{u}_{2}]$ with $\mathbf{t}_{1}\leq\mathbf{u}_{1}$ and $\mathbf{t}_{2}\leq\mathbf{u}_{2}$. By i.h. on $\mathbf{t}_{1}$ and $\mathbf{t}_{2}$, one has that $\mathbf{u}_{1}\in{\tt bne}_{\textbf{v}_{k}}$, $\mathbf{u}_{2}\in{\tt bne}_{\textbf{v}_{k}}$, $\mathbf{t}_{1}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}_{1}$ and $\mathbf{t}_{2}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}_{2}$. Thus $\mathbf{u}=\mathbf{u}_{1}[x\backslash\mathbf{u}_{2}]\in{\tt bne}_{\textbf{v}_{k}}[x\backslash{\tt bne}_{\textbf{v}_{k}}]\subseteq{\tt bne}_{\textbf{v}_{k}}$ and $\mathbf{t}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}$ using $({\tt es})$.

  * $\mathbf{t}\in{\tt bno}_{\textbf{v}_{k}}$:

    * $\mathbf{t}=\lambda x.\mathbf{t}^{\prime}$: Then necessarily $\mathbf{u}=\lambda x.\mathbf{u}^{\prime}$ with $\mathbf{t}^{\prime}\leq\mathbf{u}^{\prime}$. We distinguish three cases:

      * $\bullet$

$k=0$: Then $\mathbf{u}=\lambda x.\mathbf{u}^{\prime}\in{\tt
bno}_{\textbf{v}_{0}}$.

      * $\bullet$

$k=i+1$ for some $i\in\mathbb{N}$: Then $\mathbf{t}^{\prime}\in{\tt
bno}_{\textbf{v}_{i}}$ and by i.h. on $\mathbf{t}^{\prime}$ one has
$\mathbf{u}^{\prime}\\!\in{\tt bno}_{\textbf{v}_{i}}$ and
$\mathbf{t}^{\prime}\overset{\scriptscriptstyle
i}{\approx}\mathbf{u}^{\prime}$. Thus $\mathbf{u}=\lambda
x.\mathbf{u}^{\prime}\\!\in\lambda x.{\tt bno}_{\textbf{v}_{i}}\subseteq{\tt
bno}_{\textbf{v}_{k}}$ and $\mathbf{t}\overset{\scriptscriptstyle
k}{\approx}\mathbf{u}$ using $({\tt abs})$.

      * $\bullet$

$k=\omega$: Then $\mathbf{t}^{\prime}\in{\tt bno}_{\textbf{v}_{\omega}}$ and
by i.h. on $\mathbf{t}^{\prime}$ one has $\mathbf{u}^{\prime}\\!\in{\tt
bno}_{\textbf{v}_{\omega}}$, so $\mathbf{u}=\lambda
x.\mathbf{u}^{\prime}\\!\in\lambda x.{\tt
bno}_{\textbf{v}_{\omega}}\subseteq{\tt bno}_{\textbf{v}_{k}}$ and
$\mathbf{t}\overset{\scriptscriptstyle\omega}{\approx}\mathbf{u}$ using $({\tt
abs})$.

    * $\mathbf{t}\in{\tt bvr}_{\textbf{v}_{k}}$: By i.h. on $\mathbf{t}$, one has that $\mathbf{u}\in{\tt bvr}_{\textbf{v}_{k}}\subseteq{\tt bno}_{\textbf{v}_{k}}$ and $\mathbf{t}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}$.

    * $\mathbf{t}\in{\tt bne}_{\textbf{v}_{k}}$: By i.h. on $\mathbf{t}$, one has that $\mathbf{u}\in{\tt bne}_{\textbf{v}_{k}}\subseteq{\tt bno}_{\textbf{v}_{k}}$ and $\mathbf{t}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}$.

    * $\mathbf{t}=\mathbf{t}_{1}[x\backslash\mathbf{t}_{2}]$ with $\mathbf{t}_{1}\in{\tt bno}_{\textbf{v}_{k}}$ and $\mathbf{t}_{2}\in{\tt bne}_{\textbf{v}_{k}}$: Then necessarily $\mathbf{u}=\mathbf{u}_{1}[x\backslash\mathbf{u}_{2}]$ with $\mathbf{t}_{1}\leq\mathbf{u}_{1}$ and $\mathbf{t}_{2}\leq\mathbf{u}_{2}$. By i.h. on $\mathbf{t}_{1}$ and $\mathbf{t}_{2}$, one has that $\mathbf{u}_{1}\in{\tt bno}_{\textbf{v}_{k}}$, $\mathbf{u}_{2}\in{\tt bne}_{\textbf{v}_{k}}$, $\mathbf{t}_{1}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}_{1}$ and $\mathbf{t}_{2}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}_{2}$. Thus $\mathbf{u}=\mathbf{u}_{1}[x\backslash\mathbf{u}_{2}]\in{\tt bno}_{\textbf{v}_{k}}[x\backslash{\tt bne}_{\textbf{v}_{k}}]\subseteq{\tt bno}_{\textbf{v}_{k}}$ and $\mathbf{t}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}$ using $({\tt es})$. ∎

##  Appendix C Proof of Section 5

###  C.1. Proof of Subsection 5.1

Let us recall the mutual inductive definitions of ${\tt ne}_{\mathrm{n}_{k}}$
and ${\tt no}_{\mathrm{n}_{k}}$:

$\begin{array}[]{c}\begin{array}[]{rcl}{\tt
ne}_{\mathrm{n}_{0}}&\coloneqq&x\;|\;{\tt ne}_{\mathrm{n}_{0}}t\\\ {\tt
ne}_{\mathrm{n}_{i+1}}&\coloneqq&x\;|\;{\tt ne}_{\mathrm{n}_{i+1}}{\tt
no}_{\mathrm{n}_{i}}\qquad(i\in\mathbb{N})\\\ {\tt
ne}_{\mathrm{n}_{\omega}}&\coloneqq&x\;|\;{\tt ne}_{\mathrm{n}_{\omega}}{\tt
no}_{\mathrm{n}_{\omega}}\\\\[5.69046pt] {\tt
no}_{\mathrm{n}_{k}}&\coloneqq&\lambda x.{\tt no}_{\mathrm{n}_{k}}\;|\;{\tt
ne}_{\mathrm{n}_{k}}\qquad(k\in\mathbb{N}^{\omega})\end{array}\end{array}$

*

###### Proof.

Let $k\in\mathbb{N}^{\omega}$ and $t\in\Lambda$. We strengthen the property as
follows:

  * $t\in{\tt ne}_{\mathrm{n}_{k}}$ if and only if $t$ is a $\mathrm{n}_{k}$-normal form and $\neg{\tt Abs}\\!\left(t\right)$.

  * $t\in{\tt no}_{\mathrm{n}_{k}}$ if and only if $t$ is a $\mathrm{n}_{k}$-normal form.

By double implication:

  * $(\Rightarrow)$

By mutual induction on $t\in{\tt ne}_{\mathrm{n}_{k}}$ and $t\in{\tt
no}_{\mathrm{n}_{k}}$:

    * $t\in{\tt ne}_{\mathrm{n}_{k}}$: We distinguish two cases:

      * $t=x$: Then $t$ is a $\mathrm{n}_{k}$-normal form and $\neg{\tt Abs}\left(t\right)$.

      * $t=t_{1}t_{2}$ with $t_{1}\in{\tt ne}_{\mathrm{n}_{k}}$: Then, by i.h. on $t_{1}$, one has that $t_{1}$ is a $\mathrm{n}_{k}$-normal form and $\neg{\tt Abs}\left(t_{1}\right)$ thus $t=t_{1}t_{2}$ is not a redex. Moreover, $\neg{\tt Abs}\left(t\right)$. We distinguish three cases:

        * $\bullet$

$k=0$: Then $t=t_{1}t_{2}$ is $\mathrm{n}_{0}$-normal form.

        * $\bullet$

$k=i+1$ for some $i\in\mathbb{N}$: Then $t_{2}\in{\tt no}_{\mathrm{n}_{i}}$
thus by i.h., one has that $t_{2}$ is a $\mathrm{n}_{i}$-normal form. Since
$t$ is not a redex then it is a $\mathrm{n}_{k}$-normal form.

        * $\bullet$

$k=\omega$: Then $t_{2}\in{\tt no}_{\mathrm{n}_{\omega}}$ thus by i.h., one
has that $t_{2}$ is a $\mathrm{n}_{\omega}$-normal form. Since $t$ is not a
redex then it is a $\mathrm{n}_{\omega}$-normal form.

    * $t\in{\tt no}_{\mathrm{n}_{k}}$: We distinguish two cases:

      * $t=\lambda x.t^{\prime}$ with $t^{\prime}\in{\tt no}_{\mathrm{n}_{k}}$: By i.h. on $t^{\prime}$, one has that $t^{\prime}$ is a $\mathrm{n}_{k}$-normal form thus $\lambda x.t^{\prime}$ is also a $\mathrm{n}_{k}$-normal form.

      * $t\in{\tt ne}_{\mathrm{n}_{k}}$: Then by i.h. on $t$, one deduces that $t$ is a $\mathrm{n}_{k}$-normal form.

  * $(\Leftarrow)$

By induction on $t$:

    * $t=x$: Then $\neg{\tt Abs}\left(t\right)$ and $t\in{\tt ne}_{\mathrm{n}_{k}}$.

    * $t=\lambda x.t^{\prime}$: Then ${\tt Abs}\left(t\right)$ and $t^{\prime}$ is necessarily a $\mathrm{n}_{k}$-normal form. By i.h. on $t^{\prime}$, one has that $t^{\prime}\in{\tt no}_{\mathrm{n}_{k}}$ thus $t=\lambda x.t^{\prime}\in\lambda x.{\tt no}_{\mathrm{n}_{k}}\subseteq{\tt no}_{\mathrm{n}_{k}}$.

    * $t=t_{1}t_{2}$: Then $\neg{\tt Abs}\left(t\right)$ and necessarily, $\neg{\tt Abs}\\!\left(t\right)$ and $t_{1}$ is a $\mathrm{n}_{k}$-normal form. By i.h. on $t_{1}$, one deduces that $t_{1}\in{\tt ne}_{\mathrm{n}_{k}}$. We distinguish three cases:

      * $k=0$: Then $t=t_{1}t_{2}\in{\tt ne}_{\mathrm{n}_{0}}t_{2}\subseteq{\tt ne}_{\mathrm{n}_{0}}$.

      * $k=i+1$ for some $i\in\mathbb{N}$: Then $t_{2}\in{\tt no}_{\mathrm{n}_{i}}$. By i.h. on $t_{2}$, one has that $t_{2}\in{\tt no}_{\mathrm{n}_{i}}$ thus $t=t_{1}t_{2}\in{\tt ne}_{\mathrm{n}_{k}}{\tt no}_{\mathrm{n}_{i}}\subseteq{\tt ne}_{\mathrm{n}_{k}}$.

      * $k=\omega$: Then $t_{2}\in{\tt no}_{\mathrm{n}_{\omega}}$. By i.h. on $t_{2}$, one has that $t_{2}\in{\tt no}_{\mathrm{n}_{\omega}}$ thus $t=t_{1}t_{2}\in{\tt ne}_{\mathrm{n}_{\omega}}{\tt no}_{\mathrm{n}_{\omega}}\subseteq{\tt ne}_{\mathrm{n}_{\omega}}$.

    * $t=t_{1}[x\backslash t_{2}]$: Impossible since it contradict the fact that $t$ is a $\mathrm{n}_{k}$.

∎

*

###### Proof.

By induction on $\mathtt{C}$:

  * $\mathtt{C}=\diamond$: Then $\mathtt{C}\\!\left<t\right>=t$ is meaningless, which is impossible since it contradicts Lemma 5.4.

  * $\mathtt{C}=\lambda x.\mathtt{C}^{\prime}$: Then $\Pi$ is necessarily of the following form:

$({\tt abs})$
$\Phi\triangleright_{\mathcal{N}}\Gamma,x:\mathcal{M}\vdash\mathtt{C}^{\prime}\\!\left<t\right>:\tau$$\Gamma\vdash\lambda
x.\mathtt{C}^{\prime}\\!\left<t\right>:\mathcal{M}\Rightarrow\tau\quad$

with $\sigma=\mathcal{M}\Rightarrow\tau$. By i.h. on $\Phi$, one has
$\Phi^{\prime}\triangleright_{\mathcal{N}}\Gamma,x:\mathcal{M}\triangleright_{\mathcal{N}}\mathtt{C}^{\prime}\\!\left<u\right>:\tau$
and we set $\Pi^{\prime}$ as the following derivation:

$({\tt abs})$
$\Phi^{\prime}\triangleright_{\mathcal{N}}\Gamma,x:\mathcal{M}\vdash\mathtt{C}^{\prime}\\!\left<u\right>:\tau$$\Gamma\vdash\lambda
x.\mathtt{C}^{\prime}\\!\left<u\right>:\mathcal{M}\Rightarrow\tau\quad$

  * $\mathtt{C}=\mathtt{C}^{\prime}s$: Then $\Pi$ is necessarily of the following form:

$({\tt app})$ $\left(\vrule
height=11.17998pt,depth=0.0pt,width=0.0pt\right.$$\left.\hbox{$\vbox{\hbox{\hbox{\hbox{}\hbox{$\Pi_{1}\triangleright_{\mathcal{N}}\Gamma_{1}\vdash\mathtt{C}^{\prime}\\!\left<t\right>:\left[\tau_{i}\right]_{i\in
I}\Rightarrow\sigma$}}\hbox{$\Pi_{2}^{i}\triangleright_{\mathcal{N}}\Gamma_{2}^{i}\vdash
s:\tau_{i}$}}}$}\right)_{i\in I}$$\Gamma_{1}+_{i\in
I}\Gamma_{2}^{i}\mathrel{}$$\mathrel{}\vdash\mathtt{C}^{\prime}\\!\left<t\right>s:\sigma\hskip
71.13188pt$

with $I$ finite and $\Gamma=\Gamma_{1}+_{i\in I}\Gamma_{2}^{i}$. By i.h. on
$\Pi_{1}$, one has
$\Pi^{\prime}_{1}\triangleright_{\mathcal{N}}\Gamma_{1}\vdash\mathtt{C}^{\prime}\\!\left<u\right>:\left[\tau_{i}\right]_{i\in
I}\Rightarrow\sigma$ and we set $\Pi^{\prime}$ as the following derivation:

$({\tt app})$ $\left(\vrule
height=11.17998pt,depth=0.0pt,width=0.0pt\right.$$\left.\hbox{$\vbox{\hbox{\hbox{\hbox{}\hbox{$\Pi^{\prime}_{1}\triangleright_{\mathcal{N}}\Gamma_{1}\vdash\mathtt{C}^{\prime}\\!\left<u\right>:\left[\tau_{i}\right]_{i\in
I}\Rightarrow\sigma$}}\hbox{$\Pi_{2}^{i}\triangleright_{\mathcal{N}}\Gamma_{2}^{i}\vdash
s:\tau_{i}$}}}$}\right)_{i\in I}$$\Gamma_{1}+_{i\in
I}\Gamma_{2}^{i}\mathrel{}$$\mathrel{}\vdash\mathtt{C}^{\prime}\\!\left<t\right>s:\sigma\hskip
71.13188pt$

  * $\mathtt{C}=s\,\mathtt{C}^{\prime}$: Then $\Pi$ is necessarily of the following form:

$({\tt app})$ $\left(\vrule
height=11.17998pt,depth=0.0pt,width=0.0pt\right.$$\left.\hbox{$\vbox{\hbox{\hbox{\hbox{}\hbox{$\Pi_{1}\triangleright_{\mathcal{N}}\Gamma_{1}\vdash
s:\left[\tau_{i}\right]_{i\in
I}\Rightarrow\sigma$}}\hbox{$\Pi_{2}^{i}\triangleright_{\mathcal{N}}\Gamma_{2}^{i}\vdash\mathtt{C}^{\prime}\\!\left<t\right>:\tau_{i}$}}}$}\right)_{i\in
I}$$\Gamma_{1}+_{i\in I}\Gamma_{2}^{i}\mathrel{}$$\mathrel{}\vdash
s\,\mathtt{C}^{\prime}\\!\left<t\right>:\sigma\hskip 71.13188pt$

with $I$ finite and $\Gamma=\Gamma_{1}+_{i\in I}\Gamma_{2}^{i}$. For each
$i\in I$, by i.h. on $\Pi_{2}^{i}$, one has
${\Pi_{2}^{i}}^{\prime}\triangleright_{\mathcal{N}}\Gamma_{2}^{i}\vdash\mathtt{C}^{\prime}\\!\left<u\right>:\tau_{i}$
and we set $\Pi^{\prime}$ as the following derivation:

$({\tt app})$ $\left(\vrule
height=12.73553pt,depth=0.0pt,width=0.0pt\right.$$\left.\hbox{$\vbox{\hbox{\hbox{\hbox{}\hbox{$\Pi_{1}\triangleright_{\mathcal{N}}\Gamma_{1}\vdash
s:\left[\tau_{i}\right]_{i\in
I}\Rightarrow\sigma$}}\hbox{${\Pi_{2}^{i}}^{\prime}\triangleright_{\mathcal{N}}\Gamma_{2}^{i}\vdash\mathtt{C}^{\prime}\\!\left<u\right>:\tau_{i}$}}}$}\right)_{i\in
I}$$\Gamma_{1}+_{i\in I}\Gamma_{2}^{i}\mathrel{}$$\mathrel{}\vdash
s\,\mathtt{C}^{\prime}\\!\left<u\right>:\sigma\hskip 71.13188pt$

  * $\mathtt{C}=\mathtt{C}^{\prime}[x\backslash s]$: Then $\Pi$ is necessarily of the following form:

$({\tt es})$ $\left(\vrule
height=11.17998pt,depth=0.0pt,width=0.0pt\right.$$\left.\hbox{$\vbox{\hbox{\hbox{\hbox{}\hbox{$\Pi_{1}\triangleright_{\mathcal{N}}\Gamma_{1},x:\left[\tau_{i}\right]_{i\in
I}\vdash\mathtt{C}^{\prime}\\!\left<t\right>:\sigma$}}\hbox{$\Pi_{2}^{i}\triangleright_{\mathcal{N}}\Gamma_{2}^{i}\vdash
s:\tau_{i}$}}}$}\right)_{i\in I}$$\Gamma_{1}+_{i\in
I}\Gamma_{2}^{i}\mathrel{}$$\mathrel{}\vdash\mathtt{C}^{\prime}\\!\left<t\right>[x\backslash
s]:\sigma\hskip 54.06006pt$

with $I$ finite and $\Gamma=\Gamma_{1}+_{i\in I}\Gamma_{2}^{i}$. By i.h. on
$\Pi_{1}$, one has
$\Pi^{\prime}_{1}\triangleright_{\mathcal{N}}\Gamma_{1},x:\left[\tau_{i}\right]_{i\in
I}\vdash\mathtt{C}^{\prime}\\!\left<u\right>:\sigma$ and we set $\Pi^{\prime}$
as the following derivation:

$({\tt es})$ $\left(\vrule
height=11.17998pt,depth=0.0pt,width=0.0pt\right.$$\left.\hbox{$\vbox{\hbox{\hbox{\hbox{}\hbox{$\Pi^{\prime}_{1}\triangleright_{\mathcal{N}}\Gamma_{1},x:\left[\tau_{i}\right]_{i\in
I}\vdash\mathtt{C}^{\prime}\\!\left<u\right>:\sigma$}}\hbox{$\Pi_{2}^{i}\triangleright_{\mathcal{N}}\Gamma_{2}^{i}\vdash
s:\tau_{i}$}}}$}\right)_{i\in I}$$\Gamma_{1}+_{i\in
I}\Gamma_{2}^{i}\mathrel{}$$\mathrel{}\vdash\mathtt{C}^{\prime}\\!\left<u\right>[x\backslash
s]:\sigma\hskip 54.06006pt$

  * $\mathtt{C}=s[x\backslash\mathtt{C}^{\prime}]$: Then $\Pi$ is necessarily of the following form:

$({\tt es})$ $\left(\vrule
height=11.17998pt,depth=0.0pt,width=0.0pt\right.$$\left.\hbox{$\vbox{\hbox{\hbox{\hbox{}\hbox{$\Pi_{1}\triangleright_{\mathcal{N}}\Gamma_{1},x:\left[\tau_{i}\right]_{i\in
I}\vdash
s:\sigma$}}\hbox{$\Pi_{2}^{i}\triangleright_{\mathcal{N}}\Gamma_{2}^{i}\vdash\mathtt{C}^{\prime}\\!\left<t\right>:\tau_{i}$}}}$}\right)_{i\in
I}$$\Gamma_{1}+_{i\in I}\Gamma_{2}^{i}\mathrel{}$$\mathrel{}\vdash
s[x\backslash\mathtt{C}^{\prime}\\!\left<t\right>]:\sigma\hskip 54.06006pt$

with $I$ finite and $\Gamma=\Gamma_{1}+_{i\in I}\Gamma_{2}^{i}$. For each
$i\in I$, by i.h. on $\Pi_{2}^{i}$, one has
$\Pi_{2}^{i}\triangleright_{\mathcal{N}}\Gamma_{2}^{i}\vdash\mathtt{C}^{\prime}\\!\left<u\right>:\tau_{i}$
and we set $\Pi^{\prime}$ as the following derivation:

$({\tt es})$ $\left(\vrule
height=12.73553pt,depth=0.0pt,width=0.0pt\right.$$\left.\hbox{$\vbox{\hbox{\hbox{\hbox{}\hbox{$\Pi_{1}\triangleright_{\mathcal{N}}\Gamma_{1},x:\left[\tau_{i}\right]_{i\in
I}\vdash
s:\sigma$}}\hbox{${\Pi_{2}^{i}}^{\prime}\triangleright_{\mathcal{N}}\Gamma_{2}^{i}\vdash\mathtt{C}\\!\left<u\right>:\tau_{i}$}}}$}\right)_{i\in
I}$$\Gamma_{1}+_{i\in I}\Gamma_{2}^{i}\mathrel{}$$\mathrel{}\vdash
s[x\backslash\mathtt{C}\\!\left<u\right>]:\sigma\hskip 54.06006pt$

∎

*

###### Proof.

Let $t\in\Lambda$ such that $t$ is dCBN-meaningless and
$\mathtt{C}\\!\left<t\right>$ is dCBN-meaningful. Using Lemma 5.4, one has
$\Pi\triangleright_{\mathcal{N}}\Gamma\vdash\mathtt{C}\\!\left<t\right>:\sigma$
for some context $\Gamma$ and some type $\sigma$. By Section 5.1, there is
$\Pi^{\prime}\triangleright_{\mathcal{N}}\Gamma\vdash\mathtt{C}\\!\left<u\right>:\sigma$,
thus using Lemma 5.4 again, one concludes that $\mathtt{C}\\!\left<u\right>$
is dCBN-meaningful. ∎

###  C.2. Technical Lemmas

###### Lemma C.1.

Let
$\mathbf{t}_{1},\mathbf{t}_{2},\mathbf{u}_{1},\mathbf{u}_{2}\in\mathbf{\Lambda}$
such that $\mathbf{t}_{1}\leq\mathbf{t}_{2}$ and
$\mathbf{u}_{1}\leq\mathbf{u}_{2}$, then
$\mathbf{t}_{1}\\{x\backslash\mathbf{u}_{1}\\}\leq\mathbf{t}_{2}\\{x\backslash\mathbf{u}_{2}\\}$.

###### Proof.

By induction on $\mathbf{t}_{1}$:

  * $\mathbf{t}_{1}=\bot$: Then $\mathbf{t}_{1}\\{x\backslash\mathbf{u}_{1}\\}=\bot\leq\mathbf{t}_{2}\\{x\backslash\mathbf{u}_{2}\\}$.

  * $\mathbf{t}_{1}=y$: Then $\mathbf{t}_{2}=y$ and we distinguish two cases:

    * $x=y$: Thus $\mathbf{t}_{1}\\{x\backslash\mathbf{u}_{1}\\}=\mathbf{u}_{1}\leq\mathbf{u}_{2}=\mathbf{t}_{2}\\{x\backslash\mathbf{u}_{2}\\}$.

    * $x\neq y$: Thus $\mathbf{t}_{1}\\{x\backslash\mathbf{u}_{1}\\}=y=\mathbf{t}_{2}\\{x\backslash\mathbf{u}_{2}\\}$, thus $\mathbf{t}_{1}\\{x\backslash\mathbf{u}_{1}\\}\leq\mathbf{t}_{2}\\{x\backslash\mathbf{u}_{2}\\}$ by reflexivity of $\leq$.

  * $\mathbf{t}_{1}=\lambda y.\mathbf{t}^{\prime}_{1}$: Then $\mathbf{t}_{1}\\{x\backslash\mathbf{u}_{1}\\}=\lambda y.\mathbf{t}^{\prime}_{1}\\{x\backslash\mathbf{u}_{1}\\}$ (by supposing $y\notin{\tt fv}(\mathbf{u}_{1})\cup{\tt fv}(\mathbf{u}_{2})$ without loss of generality) and necessarily $\mathbf{t}_{2}=\lambda y.\mathbf{t}^{\prime}_{2}$ with $\mathbf{t}^{\prime}_{1}\leq\mathbf{t}^{\prime}_{2}$ thus $\mathbf{t}_{2}\\{x\backslash\mathbf{u}_{2}\\}=\lambda y.\mathbf{t}^{\prime}_{2}\\{y\backslash\mathbf{u}_{2}\\}$. By i.h. on $\mathbf{t}^{\prime}_{1}$, one has that $\mathbf{t}^{\prime}_{1}\\{x\backslash\mathbf{u}_{1}\\}\leq\mathbf{t}^{\prime}_{2}\\{x\backslash\mathbf{u}_{2}\\}$ hence $\mathbf{t}_{1}\\{x\backslash\mathbf{u}_{1}\\}=\lambda y.\mathbf{t}^{\prime}_{1}\\{x\backslash\mathbf{u}_{1}\\}\leq\lambda y.\mathbf{t}^{\prime}_{2}\\{x\backslash\mathbf{u}_{2}\\}=\mathbf{t}_{2}\\{x\backslash\mathbf{u}_{2}\\}$ by contextual closure.

  * $\mathbf{t}_{1}=\mathbf{t}_{1}^{1}\mathbf{t}_{1}^{2}$: Then $\mathbf{t}_{1}\\{x\backslash\mathbf{u}_{1}\\}=(\mathbf{t}_{1}^{1}\\{x\backslash\mathbf{u}_{1}\\})(\mathbf{t}_{1}^{2}\\{x\backslash\mathbf{u}_{1}\\})$ and necessarily $\mathbf{t}_{2}=\mathbf{t}_{2}^{1}\mathbf{t}_{2}^{2}$ with $\mathbf{t}_{1}^{1}\leq\mathbf{t}_{2}^{1}$ and $\mathbf{t}_{1}^{2}\leq\mathbf{t}_{2}^{2}$, thus $\mathbf{t}_{2}\\{y\backslash\mathbf{u}_{2}\\}=(\mathbf{t}_{2}^{1}\\{x\backslash\mathbf{u}_{2}\\})(\mathbf{t}_{2}^{2}\\{x\backslash\mathbf{u}_{2}\\})$. By i.h. on $\mathbf{t}_{1}^{1}$ and $\mathbf{t}_{1}^{2}$, one obtains that $\mathbf{t}_{1}^{1}\\{x\backslash\mathbf{u}_{1}\\}\leq\mathbf{t}_{2}^{1}\\{x\backslash\mathbf{u}_{2}\\}$ and $\mathbf{t}_{1}^{2}\\{x\backslash\mathbf{u}_{1}\\}\leq\mathbf{t}_{2}^{2}\\{x\backslash\mathbf{u}_{2}\\}$, hence $\mathbf{t}_{1}\\{x\backslash\mathbf{u}_{1}\\}=(\mathbf{t}_{1}^{1}\\{x\backslash\mathbf{u}_{1}\\})(\mathbf{t}_{1}^{2}\\{x\backslash\mathbf{u}_{1}\\})\leq(\mathbf{t}_{2}^{1}\\{x\backslash\mathbf{u}_{2}\\})(\mathbf{t}_{2}^{2}\\{x\backslash\mathbf{u}_{2}\\})=\mathbf{t}_{2}\\{x\backslash\mathbf{u}_{2}\\}$ by contextual closure.

  * $\mathbf{t}_{1}=\mathbf{t}_{1}^{1}[y\backslash\mathbf{t}_{1}^{2}]$: Then $\mathbf{t}_{1}\\{x\backslash\mathbf{u}_{1}\\}=\mathbf{t}_{1}^{1}\\{x\backslash\mathbf{u}_{1}\\}[y\backslash\mathbf{t}_{1}^{2}\\{x\backslash\mathbf{u}_{1}\\}]$ and necessarily $\mathbf{t}_{2}=\mathbf{t}_{2}^{1}[y\backslash\mathbf{t}_{2}^{2}]$ with $\mathbf{t}_{1}^{1}\leq\mathbf{t}_{2}^{1}$ and $\mathbf{t}_{1}^{2}\leq\mathbf{t}_{2}^{2}$, thus $\mathbf{t}_{2}\\{y\backslash\mathbf{u}_{2}\\}=\mathbf{t}_{2}^{1}\\{x\backslash\mathbf{u}_{2}\\}[y\backslash\mathbf{t}_{2}^{2}\\{x\backslash\mathbf{u}_{2}\\}]$. By i.h. on $\mathbf{t}_{1}^{1}$ and $\mathbf{t}_{1}^{2}$, one has $\mathbf{t}_{1}^{1}\\{x\backslash\mathbf{u}_{1}\\}\leq\mathbf{t}_{2}^{1}\\{x\backslash\mathbf{u}_{2}\\}$ and $\mathbf{t}_{1}^{2}\\{x\backslash\mathbf{u}_{1}\\}\leq\mathbf{t}_{2}^{2}\\{x\backslash\mathbf{u}_{2}\\}$, so by contextual closure $\mathbf{t}_{1}\\{x\backslash\mathbf{u}_{1}\\}=\mathbf{t}_{1}^{1}\\{x\backslash\mathbf{u}_{1}\\}[y\backslash\mathbf{t}_{1}^{2}\\{x\backslash\mathbf{u}_{1}\\}]\leq\mathbf{t}_{2}^{1}\\{x\backslash\mathbf{u}_{2}\\}[y\backslash\mathbf{t}_{2}^{2}\\{x\backslash\mathbf{u}_{2}\\}]=\mathbf{t}_{2}\\{x\backslash\mathbf{u}_{2}\\}$. ∎

###### Definition C.2.

The partial order $\leq$ is extended to dCBN contexts by setting
$\diamond\leq\diamond$.

For example, $\diamond[x\backslash\lambda
y.\bot](z\bot)\leq\diamond[x\backslash\lambda y.(zz)](z\bot)$.

###### Lemma C.3.

Let $\mathbf{L}_{1}\leq\mathbf{L}_{2}$ and $\mathbf{t}_{1}\leq\mathbf{t}_{2}$
for some list contexts $\mathbf{L}_{1},\mathbf{L}_{2}$ and some
$\mathbf{t}_{1},\mathbf{t}_{2}\in\mathbf{\Lambda}$, then
$\mathbf{L}_{1}\\!\left<\mathbf{t}_{1}\right>\leq\mathbf{L}_{2}\\!\left<\mathbf{t}_{2}\right>$.

###### Proof.

By induction on $\mathbf{L}_{1}$:

  * $\mathbf{L}_{1}=\diamond$: Then necessarily $\mathbf{L}_{2}=\diamond$ thus $\mathbf{L}_{1}\\!\left<\mathbf{t}_{1}\right>=\mathbf{t}_{1}\leq\mathbf{t}_{2}=\mathbf{L}_{2}\\!\left<\mathbf{t}_{2}\right>$.

  * $\mathbf{L}_{1}=\mathbf{L}^{\prime}_{1}[x\backslash\mathbf{u}_{1}]$: Then necessarily $\mathbf{L}_{2}=\mathbf{L}^{\prime}_{2}[x\backslash\mathbf{u}_{2}]$ with $\mathbf{L}^{\prime}_{1}\leq\mathbf{L}^{\prime}_{2}$ and $\mathbf{u}_{1}\leq\mathbf{u}_{2}$. By i.h. on $\mathbf{L}^{\prime}_{1}$, one has that $\mathbf{L}^{\prime}_{1}\\!\left<\mathbf{t}_{1}\right>\leq\mathbf{L}^{\prime}_{2}\\!\left<\mathbf{t}_{2}\right>$ thus $\mathbf{L}_{1}\\!\left<\mathbf{t}_{1}\right>=\mathbf{L}^{\prime}_{1}\\!\left<\mathbf{t}_{1}\right>[x\backslash\mathbf{u}_{1}]\leq\mathbf{L}^{\prime}_{2}\\!\left<\mathbf{t}_{2}\right>[x\backslash\mathbf{u}_{2}]=\mathbf{L}_{2}\\!\left<\mathbf{t}_{2}\right>$ by contextual closure. ∎

###### Lemma C.4.

Let $t,u\in\Lambda$ such that $t\rightarrow_{\mathrm{n}_{k}}u$. Then, $t$ is
dCBN-meaningful if and only if $u$ is dCBN-meaningful.

###### Proof.

According to qualitative subject reduction and expansion (deCarvalho18), given
$t\rightarrow_{\mathrm{n}_{\omega}}u$, there is a derivation
$\Pi\triangleright_{\mathcal{N}}\Gamma\vdash t:\sigma$ if and only if there is
a derivation $\Pi^{\prime}\triangleright_{\mathcal{N}}\Gamma\vdash u:\sigma$.
As $\rightarrow_{\mathrm{n}_{k}}\subseteq\rightarrow_{\mathrm{n}_{\omega}}$
for all $k\in\mathbb{N}$, the same equivalence also holds if we replace the
hypothesis $t\rightarrow_{\mathrm{n}_{\omega}}u$ with
$t\rightarrow_{\mathrm{n}_{k}}u$, for all $k\in\mathbb{N}$. We conclude thanks
to the type-theoretical characterization of dCBN-meaningfulness (Lemma 5.4). ∎

###### Lemma C.5.

Let $t,u\in\Lambda$. Then

  1. (1)

If $tu$ is dCBN-meaningful then $t$ is dCBN-meaningful.

  2. (2)

If $t[x\backslash u]$ is dCBN-meaningful then $t$ is dCBN-meaningful.

  3. (3)

If $t\\{x\backslash u\\}$ is dCBN-meaningful then $t$ is dCBN-meaningful.

###### Proof.

  1. (1)

Let $tu$ be dCBN-meaningful and suppose by absurd that $t$ is dCBN-
meaningless. Using Lemma 5.4, we know that $tu$ surface normalizes. Since $t$
is dCBN-meaningless, there exists a $(t_{i})_{i\in\mathbb{N}}$ with $t_{0}=t$
and $t_{i}\rightarrow_{\mathrm{v}_{0}}t_{i+1}$ yielding the infinite path
$tu\rightarrow_{\mathrm{v}_{0}}t_{1}u\rightarrow_{\mathrm{v}_{0}}t_{2}u\rightarrow_{\mathrm{v}_{0}}\dots$
obtained by always reducing $t$. Since surface reduction is diamond, this
contradicts the fact that $tu$ is surface normalizing.

  2. (2)

Same principle as the previous item.

  3. (3)

Let $t\\{x\backslash v\\}$ be dCBN-meaningful. By induction on $t$, one can
show that if $t\rightarrow_{\mathrm{v}_{0}}u$ then $t\\{x\backslash
v\\}\rightarrow_{\mathrm{v}_{0}}u\\{x\backslash v\\}$. Using this, one applied
the same principles as the two previous points.

∎

###### Definition C.6.

Meaningful approximation is extended to list contexts $\mathtt{L}$ inductively
as follows:

$\mathcal{M\\!A}_{{\tt N}}\\!\left(\diamond\right)\coloneqq\diamond\hskip
56.9055pt\mathcal{M\\!A}_{{\tt V}}\\!\left(\mathtt{L}[x\backslash
s]\right)\coloneqq\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{L}\right)[x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(s\right)]$

###### Corollary C.7.

Let $\mathtt{L}\\!\left<t\right>$ be dCBN-meaningful, then
$\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{L}\\!\left<t\right>\right)=\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{L}\right)\\!\left<\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)\right>$.

###### Proof.

By induction on $\mathtt{L}$. Cases:

  * $\mathtt{L}=\diamond$: Then $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{L}\\!\left<t\right>\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)=\diamond\\!\left<\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)\right>=\mathcal{M\\!A}_{{\tt N}}\\!\left(\diamond\right)\\!\left<\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)\right>$.

  * $\mathtt{L}=\mathtt{L}^{\prime}[x\backslash u]$: Then $\mathtt{L}\\!\left<t\right>=\mathtt{L}^{\prime}\\!\left<t\right>[x\backslash u]$ is dCBN-meaningful, hence by Lemma C.5.(2) $\mathtt{L}^{\prime}\\!\left<t\right>$ is dCBN-meaningful. By i.h. on $\mathtt{L}^{\prime}$, one obtains that $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{L}^{\prime}\\!\left<t\right>\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{L}^{\prime}\right)\\!\left<\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)\right>$, thus:

$\begin{array}[]{r cl cl}\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{L}\\!\left<t\right>\right)&=&\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{L}^{\prime}\\!\left<t\right>[x\backslash u]\right)\\\
&=&\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{L}^{\prime}\\!\left<t\right>\right)[x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)]\\\ &\overset{\textit{i.h.}}{=}&\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{L}^{\prime}\right)\\!\left<\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)\right>[x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)]\\\ &=&\big{(}\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{L}^{\prime}\right)[x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)]\big{)}\\!\left<\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)\right>\\\ &=&\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{L}^{\prime}[x\backslash
u]\right)\\!\left<\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)\right>&=&\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{L}\right)\\!\left<\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)\right>\end{array}$

∎

###### Lemma C.8.

Let $t,u\in\Lambda$, then $\mathcal{M\\!A}_{{\tt N}}\\!\left(t\\{x\backslash
u\\}\right)\leq\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\}$.

###### Proof.

We distinguish two cases:

  * $t\\{x\backslash u\\}$ is dCBN-meaningless. Then $\mathcal{M\\!A}_{{\tt N}}\\!\left(t\\{x\backslash u\\}\right)=\bot\leq\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)\\{x\backslash\mathcal{M\\!A}_{{\tt N}}\\!\left(u\right)\\}$.

  * $t\\{x\backslash u\\}$ is dCBN-meaningful. By Lemma C.5.(3), $t$ is dCBN-meaningful. We reason by induction on $t$. Cases:

    * $t=y$: Then $\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)=y$ and we distinguish two subcases:

      * $\bullet$

$y=x$: Then $t\\{x\backslash u\\}=u$ and so $\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\\{x\backslash u\\}\right)=\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)=x\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\}=\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\}$.

      * $\bullet$

$y\neq x$: Then $t\\{x\backslash u\\}=y$ and so $\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\\{x\backslash u\\}\right)=\mathcal{M\\!A}_{{\tt
N}}\\!\left(y\right)=y=y\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\}=\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\}$.

    * $t=\lambda y.t^{\prime}$: Then $\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)=\lambda y.\mathcal{M\\!A}_{{\tt N}}\\!\left(t^{\prime}\right)$ and $t\\{x\backslash u\\}=\lambda y.(t^{\prime}\\{x\backslash u\\})$ (we suppose without loss of generality that $y\notin{\tt fv}(u)\cup\\{x\\}$). By i.h. on $t^{\prime}$, one has $\mathcal{M\\!A}_{{\tt N}}\\!\left(t^{\prime}\\{x\backslash u\\}\right)\leq\mathcal{M\\!A}_{{\tt N}}\\!\left(t^{\prime}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt N}}\\!\left(u\right)\\}$. Thus:

$\begin{array}[]{r cl cl}\mathcal{M\\!A}_{{\tt N}}\\!\left(t\\{x\backslash
u\\}\right)&=&\mathcal{M\\!A}_{{\tt N}}\\!\left(\lambda
y.(t^{\prime}\\{x\backslash u\\})\right)\\\ &=&\lambda y.\mathcal{M\\!A}_{{\tt
N}}\\!\left(t^{\prime}\\{x\backslash u\\}\right)\\\
&\overset{\textit{i.h.}}{\leq}&\lambda y.\mathcal{M\\!A}_{{\tt
N}}\\!\left(t^{\prime}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\}\\\ &=&(\lambda y.\mathcal{M\\!A}_{{\tt
N}}\\!\left(t^{\prime}\right))\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\}\\\ &=&\mathcal{M\\!A}_{{\tt N}}\\!\left(\lambda
y.t^{\prime}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\}&=&\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\}\end{array}$

    * $t=t_{1}t_{2}$: Then $\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{1}\right)\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{2}\right)$ and $t\\{x\backslash u\\}=(t_{1}\\{x\backslash u\\})[y\backslash t_{2}\\{x\backslash u\\}]$ (we suppose without loss of generality that $y\notin{\tt fv}(u)\cup\\{x\\}$). By i.h. on $t_{1}$ and $t_{2}$, one has $\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{1}\\{x\backslash u\\}\right)\leq\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{1}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt N}}\\!\left(u\right)\\}$ and $\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{2}\\{x\backslash u\\}\right)\leq\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{2}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt N}}\\!\left(u\right)\\}$. Thus:

$\begin{array}[]{r cl cl}\mathcal{M\\!A}_{{\tt N}}\\!\left(t\\{x\backslash
u\\}\right)&=&\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{1}\\{x\backslash
u\\}t_{2}\\{x\backslash u\\}\right)\\\ &=&\mathcal{M\\!A}_{{\tt
N}}\\!\left(t_{1}\\{x\backslash u\\}\right)\mathcal{M\\!A}_{{\tt
N}}\\!\left(t_{2}\\{x\backslash u\\}\right)\\\
&\overset{\textit{i.h.}}{\leq}&(\mathcal{M\\!A}_{{\tt
N}}\\!\left(t_{1}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\})(\mathcal{M\\!A}_{{\tt
N}}\\!\left(t_{2}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\})\\\ &=&(\mathcal{M\\!A}_{{\tt
N}}\\!\left(t_{1}\right)\mathcal{M\\!A}_{{\tt
N}}\\!\left(t_{2}\right))\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\}\\\ &=&\mathcal{M\\!A}_{{\tt
N}}\\!\left(t_{1}t_{2}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\}&=&\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\}\end{array}$

    * $t=t_{1}[y\backslash t_{2}]$: Thus $\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{1}\right)[y\backslash\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{2}\right)]$ and $t\\{x\backslash u\\}=(t_{1}\\{x\backslash u\\})[y\backslash t_{2}\\{x\backslash u\\}]$ (we suppose without loss of generality that $y\notin{\tt fv}(u)\cup\\{x\\}$). By i.h. on $t_{1}$ and $t_{2}$, one has $\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{1}\\{x\backslash u\\}\right)\leq\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{1}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt N}}\\!\left(u\right)\\}$ and $\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{2}\\{x\backslash u\\}\right)\leq\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{2}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt N}}\\!\left(u\right)\\}$. Thus:

$\begin{array}[]{r cl cl}\mathcal{M\\!A}_{{\tt N}}\\!\left(t\\{x\backslash
u\\}\right)&=&\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{1}\\{x\backslash
u\\}[y\backslash t_{2}\\{x\backslash u\\}]\right)\\\ &=&\mathcal{M\\!A}_{{\tt
N}}\\!\left(t_{1}\\{x\backslash u\\}\right)[y\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(t_{2}\\{x\backslash u\\}\right)]\\\
&\overset{\textit{i.h.}}{\leq}&(\mathcal{M\\!A}_{{\tt
N}}\\!\left(t_{1}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\})[y\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(t_{2}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\}]\\\ &=&(\mathcal{M\\!A}_{{\tt
N}}\\!\left(t_{1}\right)[y\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(t_{2}\right)])\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\}\\\ &=&\mathcal{M\\!A}_{{\tt
N}}\\!\left(t_{1}[y\backslash t_{2}]\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\}&=&\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)\\}\end{array}$

∎

###  C.3. Proofs of Section 5.2

*

###### Proof.

We distinguish two cases:

  * $t$ is meaningless. Then $\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)=\bot\leq t$.

  * $t$ is meaningful. We then reason by cases on $t$:

    * $t=x$: Then $\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)=x\leq x=t$.

    * $t=\lambda x.t^{\prime}$: By i.h. on $t^{\prime}$, one has that $\mathcal{M\\!A}_{{\tt N}}\\!\left(t^{\prime}\right)\leq t^{\prime}$ thus $\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)=\lambda x.\mathcal{M\\!A}_{{\tt N}}\\!\left(t^{\prime}\right)\leq\lambda x.t^{\prime}=t$.

    * $t=t_{1}t_{2}$: By i.h. on $t_{1}$ and $t_{2}$, one has that $\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{1}\right)\leq t_{1}$ and $\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{2}\right)\leq t_{2}$ so that $\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{1}\right)\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{2}\right)\leq t_{1}t_{2}=t$.

    * $t=t_{1}[x\backslash t_{2}]$: By i.h. on $t_{1}$ and $t_{2}$, $\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{1}\right)\leq t_{1}$ and $\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{2}\right)\leq t_{2}$. So, $\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{1}\right)[x\backslash\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{2}\right)]\leq t_{1}[x\backslash t_{2}]=t$. ∎

*

###### Proof.

Let $\mathtt{C}$ be a full context and $t,u\in\Lambda$ be such that $t$ is
meaningless. We distinguish two cases:

  * $\mathtt{C}\\!\left<t\right>$ is meaningless. Then $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}\\!\left<t\right>\right)=\bot\leq\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}\\!\left<u\right>\right)$.

  * $\mathtt{C}\\!\left<t\right>$ is meaningful: Then by surface genericity (Section 5.1), one has that $\mathtt{C}\\!\left<u\right>$ is also meaningful. We reason by induction on $\mathtt{C}$:

    * $\mathtt{C}=\diamond$: This case is impossible because it would mean $\mathtt{C}\\!\left<t\right>=t$ is meaningless (by hypothesis) and meaningful at the same time.

    * $\mathtt{C}=\lambda x.\mathtt{C}^{\prime}$: By i.h. on $\mathtt{C}^{\prime}$, one has $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)\leq\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)$, thus $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}\\!\left<t\right>\right)=\lambda x.\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)\overset{\textit{i.h.}}{\leq}\lambda x.\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}\\!\left<u^{\prime}\right>\right)$ by contextual closure.

    * $\mathtt{C}=\mathtt{C}^{\prime}s$: By i.h. on $\mathtt{C}^{\prime}$, one has $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)\leq\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)$, thus $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}\\!\left<t\right>\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)\overset{\textit{i.h.}}{\leq}\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)\allowbreak=\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}\\!\left<u^{\prime}\right>\right)$ by contextual closure.

    * $\mathtt{C}=s\,\mathtt{C}^{\prime}$: By i.h. on $\mathtt{C}^{\prime}$, one has $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)\leq\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)$, thus $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}\\!\left<t\right>\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)\overset{\textit{i.h.}}{\leq}\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)\allowbreak=\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}\\!\left<u^{\prime}\right>\right)$ by contextual closure.

    * $\mathtt{C}=\mathtt{C}^{\prime}[x\backslash s]$: By i.h. on $\mathtt{C}^{\prime}$, one has $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)\leq\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)$, and hence $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}\\!\left<t\right>\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)[x\backslash]{\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)}\overset{\textit{i.h.}}{\leq}\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)[x\backslash]{\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)}=\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}\\!\left<u^{\prime}\right>\right)$ by contextual closure.

    * $\mathtt{C}=s[x\backslash\mathtt{C}^{\prime}]$: By i.h. on $\mathtt{C}^{\prime}$, one has $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)\leq\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)$, and hence $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}\\!\left<t\right>\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)[x\backslash\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<t\right>\right)]\overset{\textit{i.h.}}{\leq}\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)[x\backslash\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}^{\prime}\\!\left<u\right>\right)]=\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{C}\\!\left<u^{\prime}\right>\right)$ by contextual closure. ∎

#### Dynamic Approximation and Lifting.

We now prove the instance of Axiom A for dCBN.

###### Lemma C.9 (dCBN Dynamic Approximation).

Let $k\in\mathbb{N}^{\omega}$ and $t,u\in\Lambda$ such that
$t\rightarrow_{\mathrm{n}_{k}}u$, then there exists
$\mathbf{u}\in\mathbf{\Lambda}$ such that $\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)\rightarrow^{=}_{\mathbf{n}_{k}}\mathbf{u}\geq\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)$.

###### Proof.

Let $t,u\in\Lambda$ such that $t\rightarrow_{\mathrm{n}_{k}}u$. We distinguish
two cases:

  * $t$ dCBN-meaningless: Then $u$ is dCBN-meaningful using Lemma C.4 thus $\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)=\bot$ and $\mathcal{M\\!A}_{{\tt N}}\\!\left(u\right)=\bot$. We set $\mathbf{u}\coloneqq\mathcal{M\\!A}_{{\tt N}}\\!\left(u\right)$ therefore by reflexivity of both relations, $\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)\rightarrow^{=}_{\mathbf{n}_{k}}\mathbf{u}\geq\mathcal{M\\!A}_{{\tt N}}\\!\left(u\right)$.

  * $t$ dCBN-meaningful: Then $u$ is dCBN-meaningful using Lemma C.4. By definition, there exist a context $\mathtt{N}_{k}$ and $t^{\prime},u^{\prime}\in\Lambda$ such that $t=\mathtt{N}_{k}\\!\left<t^{\prime}\right>$, $u=\mathtt{N}_{k}\\!\left<u^{\prime}\right>$ and $t^{\prime}\mapsto_{\mathcal{R}}u^{\prime}$ for some $\mathcal{R}\in\\{{\tt dB},{\tt s}\\}$. We reason by induction on $\mathtt{N}_{k}$:

    * $\mathtt{N}_{k}=\diamond$: Then $t=t^{\prime}$ and $u=u^{\prime}$. We distinguish two cases:

      * $\bullet$

$\mathcal{R}={\tt dB}$: Then $t^{\prime}=\mathtt{L}\\!\left<\lambda
x.s_{1}\right>s_{2}$ and $u^{\prime}=\mathtt{L}\\!\left<s_{1}[x\backslash
s_{2}]\right>$ for some list context $\mathtt{L}$ and some
$s_{1},s_{2}\in\Lambda$. Since $t^{\prime}$ is dCBN-meaningful, then using
Lemma C.5.(1), one deduces in particular that $\mathtt{L}\\!\left<\lambda
x.s_{1}\right>$ is dCBN-meaningful. Since $u^{\prime}$ is dCBN-meaningful,
then using Lemma C.5.(2), one deduces in particular that $s_{1}[x\backslash
s_{2}]$ is dCBN-meaningful. Thus, by Corollary C.7, one has
$\mathcal{M\\!A}_{{\tt N}}\\!\left(t^{\prime}\right)=\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{L}\\!\left<\lambda
x.s_{1}\right>\right)\mathcal{M\\!A}_{{\tt
N}}\\!\left(s_{2}\right)=\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{L}\right)\\!\left<\lambda x.\mathcal{M\\!A}_{{\tt
N}}\\!\left(s_{1}\right)\right>\mathcal{M\\!A}_{{\tt N}}\\!\left(s_{2}\right)$
and $\mathcal{M\\!A}_{{\tt N}}\\!\left(u^{\prime}\right)=\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{L}\\!\left<s_{1}[x\backslash
s_{2}]\right>\right)=\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{L}\right)\\!\left<\mathcal{M\\!A}_{{\tt
N}}\\!\left(s_{1}[x\backslash s_{2}]\right)\right>=\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{L}\right)\\!\left<\mathcal{M\\!A}_{{\tt
N}}\\!\left(s_{1}\right)[x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(s_{2}\right)]\right>$. Hence, $\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt
N}}\\!\left(t^{\prime}\right)\mapsto_{{\tt dB}}\mathcal{M\\!A}_{{\tt
N}}\\!\left(u^{\prime}\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(u\right)$. We
set $\mathbf{u}\coloneqq\mathcal{M\\!A}_{{\tt N}}\\!\left(u\right)$, therefore
by reflexivity $\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)\rightarrow_{\mathbf{n}_{k}}\mathbf{u}\geq\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)$.

      * $\bullet$

$\mathcal{R}={\tt s}$: Then $t^{\prime}=s_{1}[x\backslash s_{2}]$ and
$u^{\prime}=s_{1}\\{x\backslash s_{2}\\}$ for some $s_{1},s_{2}\in\Lambda$.
Using LABEL:lem:cbn_MA(t{x:=u})_<=_MA(t){x:=MA(u)}, one has that
$\mathcal{M\\!A}_{{\tt N}}\\!\left(t^{\prime}\right)=\mathcal{M\\!A}_{{\tt
N}}\\!\left(s_{1}\right)[x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(s_{2}\right)]$ and $\mathcal{M\\!A}_{{\tt
N}}\\!\left(u^{\prime}\right)\leq\mathcal{M\\!A}_{{\tt
N}}\\!\left(s_{1}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(s_{2}\right)\\}$. Thus $\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)=\mathcal{M\\!A}_{{\tt
N}}\\!\left(t^{\prime}\right)\mapsto_{{\tt s}}\mathcal{M\\!A}_{{\tt
N}}\\!\left(s_{1}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(s_{2}\right)\\}\geq\mathcal{M\\!A}_{{\tt
N}}\\!\left(u^{\prime}\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(u\right)$. We
set $\mathbf{u}\coloneqq\mathcal{M\\!A}_{{\tt
N}}\\!\left(s_{1}\right)\\{x\backslash\mathcal{M\\!A}_{{\tt
N}}\\!\left(s_{2}\right)\\}$, therefore $\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)\rightarrow_{\mathbf{n}_{k}}\mathbf{u}\geq\mathcal{M\\!A}_{{\tt
N}}\\!\left(u\right)$.

    * $\mathtt{N}_{k}=\lambda x.\mathtt{N}^{\prime}_{k}$: By i.h. on $\mathtt{N}^{\prime}_{k}$, one has $\mathbf{u}^{\prime}\in\mathbf{\Lambda}$ such that $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}^{\prime}_{k}\\!\left<t^{\prime}\right>\right)\rightarrow^{=}_{\mathbf{n}_{k}}\mathbf{u}^{\prime}\geq\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}^{\prime}_{k}\\!\left<u^{\prime}\right>\right)$. We set $\mathbf{u}\coloneqq\lambda x.\mathbf{u}^{\prime}$, therefore $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{k}\\!\left<t^{\prime}\right>\right)=\lambda x.\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}^{\prime}_{k}\\!\left<t^{\prime}\right>\right)\rightarrow^{=}_{\mathbf{n}_{k}}\mathbf{u}\geq\lambda x.\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}^{\prime}_{k}\\!\left<u^{\prime}\right>\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{k}\\!\left<u^{\prime}\right>\right)$.

    * $\mathtt{N}_{k}=\mathtt{N}^{\prime}_{k}\,s$: By i.h. on $\mathtt{N}^{\prime}_{k}$, one has $\mathbf{u}^{\prime}\in\mathbf{\Lambda}$ such that $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}^{\prime}_{k}\\!\left<t^{\prime}\right>\right)\rightarrow^{=}_{\mathbf{n}_{k}}\mathbf{u}^{\prime}\geq\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}^{\prime}_{k}\\!\left<u^{\prime}\right>\right)$. We set $\mathbf{u}\coloneqq\mathbf{u}^{\prime}\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)$, therefore $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{k}\\!\left<t^{\prime}\right>\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}^{\prime}_{k}\\!\left<t^{\prime}\right>\right)\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)\rightarrow^{=}_{\mathbf{n}_{k}}\mathbf{u}\geq\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}^{\prime}_{k}\\!\left<u^{\prime}\right>\right)\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{k}\\!\left<u^{\prime}\right>\right)$.

    * $\mathtt{N}_{k}=s\,\mathtt{N}_{m}$ with either $k>0$ and $m=k-1$, or $k=m=\omega$: By i.h. on $\mathtt{N}^{\prime}_{m}$, one has $\mathbf{u}^{\prime}\in\mathbf{\Lambda}$ such that $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{m}\\!\left<t^{\prime}\right>\right)\rightarrow^{=}_{\mathbf{n}_{m}}\mathbf{u}^{\prime}\geq\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{m}\\!\left<u^{\prime}\right>\right)$. We set $\mathbf{u}\coloneqq\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)\mathbf{u}^{\prime}$, therefore $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{k}\\!\left<t^{\prime}\right>\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{m}\\!\left<t^{\prime}\right>\right)\rightarrow^{=}_{\mathbf{n}_{k}}\mathbf{u}\geq\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{m}\\!\left<u^{\prime}\right>\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{k}\\!\left<u^{\prime}\right>\right)$.

    * $\mathtt{N}_{k}=\mathtt{N}^{\prime}_{k}[x\backslash s]$: By i.h. on $\mathtt{N}^{\prime}_{k}$, one has $\mathbf{u}^{\prime}\in\mathbf{\Lambda}$ such that $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}^{\prime}_{k}\\!\left<t^{\prime}\right>\right)\rightarrow^{=}_{\mathbf{n}_{k}}\mathbf{u}^{\prime}\geq\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}^{\prime}_{k}\\!\left<u^{\prime}\right>\right)$. We set $\mathbf{u}\coloneqq\mathbf{u}^{\prime}[x\backslash\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)]$, therefore $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{k}\\!\left<t^{\prime}\right>\right)=\mathbf{u}^{\prime}[x\backslash\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)]\rightarrow^{=}_{\mathbf{n}_{k}}\mathbf{u}\geq\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}^{\prime}_{k}\\!\left<u^{\prime}\right>\right)[x\backslash\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)]=\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{k}\\!\left<u^{\prime}\right>\right)$.

    * $\mathtt{N}_{k}=s[x\backslash\mathtt{N}_{m}]$ with either $k>0$ and $m=k-1$, or $k=m=\omega$: By i.h. on $\mathtt{N}_{m}$, one has $\mathbf{u}^{\prime}\in\mathbf{\Lambda}$ such that $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{m}\\!\left<t^{\prime}\right>\right)\rightarrow^{=}_{\mathbf{n}_{m}}\mathbf{u}^{\prime}\geq\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{m}\\!\left<u^{\prime}\right>\right)$. We set $\mathbf{u}\coloneqq\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)[x\backslash\mathbf{u}^{\prime}]$, therefore $\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{k}\\!\left<t^{\prime}\right>\right)=\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)[x\backslash\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{m}\\!\left<t^{\prime}\right>\right)]\rightarrow^{=}_{\mathbf{n}_{k}}\mathbf{u}\geq\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)[x\backslash\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{m}\\!\left<u^{\prime}\right>\right)]=\mathcal{M\\!A}_{{\tt N}}\\!\left(\mathtt{N}_{k}\\!\left<u^{\prime}\right>\right)$. ∎

We now prove the instance of Axiom B for dCBN.

###### Lemma C.10 (dCBN Dynamic Partial Lift).

lemma Let $k\in\mathbb{N}^{\omega}$ and
$\mathbf{t},\mathbf{u},\mathbf{t}^{\prime}\in\mathbf{\Lambda}$. If
$\mathbf{t}\rightarrow_{\mathbf{n}_{k}}\mathbf{u}$ and
$\mathbf{t}\leq\mathbf{t}^{\prime}$, then there is
$\mathbf{u}^{\prime}\in\mathbf{\Lambda}$ such that
$\mathbf{t}^{\prime}\rightarrow_{\mathbf{n}_{k}}\mathbf{u}^{\prime}$ and
$\mathbf{u}\leq\mathbf{u}^{\prime}$.

###### Proof.

Let $\mathbf{t},\mathbf{u},\mathbf{t}^{\prime}\in\mathbf{\Lambda}$ such that
$\mathbf{t}\leq\mathbf{t}^{\prime}$ and
$\mathbf{t}\rightarrow_{\mathbf{n}_{k}}\mathbf{u}$. Then
$\mathbf{t}=\mathbf{N}_{k}\\!\left<\mathbf{t}_{r}\right>$ and
$\mathbf{u}=\mathbf{N}_{k}\\!\left<\mathbf{u}_{r}\right>$ with
$\mathbf{t}_{r}\mapsto_{\mathcal{R}}\mathbf{u}_{r}$ for some
$\mathbf{t}_{r},\mathbf{u}_{r}\in\mathbf{\Lambda}$ and $\mathcal{R}\in\\{{\tt
dB},{\tt s}\\}$. Let us proceed by induction on $\mathbf{N}_{k}$:

  * $\mathbf{N}_{k}=\diamond$: Then $\mathbf{t}=\mathbf{t}_{r}$ and $\mathbf{u}=\mathbf{u}_{r}$. We distinguish two cases:

    * $\mathcal{R}={\tt dB}$: Then $\mathbf{t}_{r}=\mathbf{L}\\!\left<\lambda x.\mathbf{s}_{1}\right>\mathbf{s}_{2}$ and $\mathbf{u}_{r}=\mathbf{L}\\!\left<\mathbf{s}_{1}[x\backslash\mathbf{s}_{2}]\right>$ for some list context $\mathbf{L}$ and some $\mathbf{s}_{1},\mathbf{s}_{2}\in\mathbf{\Lambda}$. Since $\mathbf{t}\leq\mathbf{t}^{\prime}$, by induction on $\mathbf{L}$, one has that $\mathbf{t}=\mathbf{L}^{\prime}\\!\left<\lambda x.\mathbf{s}^{\prime}_{1}\right>\mathbf{s}^{\prime}_{2}$ with $\mathbf{L}\leq\mathbf{L}^{\prime}$, $\mathbf{s}_{1}\leq\mathbf{s}^{\prime}_{1}$ and $\mathbf{s}_{2}\leq\mathbf{s}^{\prime}_{2}$ for some list context $\mathbf{L}^{\prime}$ and some $\mathbf{s}^{\prime}_{1},\mathbf{s}^{\prime}_{2}\in\mathbf{\Lambda}$. Taking $\mathbf{u}^{\prime}=\mathbf{L}^{\prime}\\!\left<\mathbf{s}^{\prime}_{1}[x\backslash\mathbf{s}^{\prime}_{2}]\right>$ concludes this case since $\mathbf{t}^{\prime}=\mathbf{L}^{\prime}\\!\left<\lambda x.\mathbf{s}^{\prime}_{1}\right>\mathbf{s}^{\prime}_{2}\rightarrow_{\mathbf{n}_{k}}\mathbf{L}^{\prime}\\!\left<\mathbf{s}^{\prime}_{1}[x\backslash\mathbf{s}^{\prime}_{2}]\right>=\mathbf{u}^{\prime}$ and by transitivity $\mathbf{s}_{1}[x\backslash\mathbf{s}_{2}]\leq\mathbf{s}^{\prime}_{1}[x\backslash\mathbf{s}^{\prime}_{2}]$ thus $\mathbf{L}\\!\left<\mathbf{s}_{1}[x\backslash\mathbf{s}_{2}]\right>\leq\mathbf{L}^{\prime}\\!\left<\mathbf{s}^{\prime}_{1}[x\backslash\mathbf{s}^{\prime}_{2}]\right>=\mathbf{u}^{\prime}$ using lemma C.3.

    * $\mathcal{R}={\tt s}$: Then $\mathbf{t}_{r}=\mathbf{s}_{1}[x\backslash\mathbf{s}_{2}]$ and $\mathbf{u}_{r}=\mathbf{s}_{1}\\{x\backslash\mathbf{s}_{2}\\}$ for some partial terms $\mathbf{s}_{1},\mathbf{s}_{2}\in\mathbf{\Lambda}$. Since $\mathbf{t}\leq\mathbf{t}^{\prime}$, one has that $\mathbf{t}^{\prime}=\mathbf{s}^{\prime}_{1}[x\backslash\mathbf{s}^{\prime}_{2}]$ with $\mathbf{s}_{1}\leq\mathbf{s}^{\prime}_{1}$ and $\mathbf{s}_{2}\leq\mathbf{s}^{\prime}_{2}$ for some some partial terms $\mathbf{s}^{\prime}_{1},\mathbf{s}^{\prime}_{2}\in\mathbf{\Lambda}$. Taking $\mathbf{u}^{\prime}=\mathbf{s}^{\prime}_{1}\\{x\backslash\mathbf{s}^{\prime}_{2}\\}$ concludes this case since $\mathbf{t}^{\prime}=\mathbf{s}^{\prime}_{1}[x\backslash\mathbf{s}^{\prime}_{2}]\rightarrow_{\mathbf{n}_{k}}\mathbf{s}^{\prime}_{1}\\{x\backslash\mathbf{s}^{\prime}_{2}\\}$ and using LABEL:lem:Cbn_t1_<=_t2_and_u1_<=_u2_==>_t1{x:=u1}_<=_t2{x:=u2}, one has that $\mathbf{s}_{1}\\{x\backslash\mathbf{s}_{2}\\}\leq\mathbf{s}^{\prime}_{1}\\{x\backslash\mathbf{s}^{\prime}_{2}\\}$.

  * $\mathbf{N}_{k}=\lambda x.\mathbf{N}^{\prime}_{k}$: Then $\mathbf{t}=\lambda x.\mathbf{N}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>$ and $\mathbf{u}=\lambda x.\mathbf{N}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>$ thus $\mathbf{t}^{\prime}=\lambda x.\mathbf{t}^{\prime}_{1}$ for some $\mathbf{t}^{\prime}_{1}\in\mathbf{\Lambda}$ such that $\mathbf{N}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>\leq\mathbf{t}^{\prime}_{1}$. Since $\mathbf{N}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>\rightarrow_{\mathbf{n}_{k}}\mathbf{N}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>$, by i.h. on $\mathbf{N}^{\prime}_{k}$, one obtains $\mathbf{u}^{\prime}_{1}\in\mathbf{\Lambda}$ such that $\mathbf{t}^{\prime}_{1}\rightarrow_{\mathbf{n}_{k}}\mathbf{u}^{\prime}_{1}$ and $\mathbf{N}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>\leq\mathbf{u}^{\prime}_{1}$. Taking $\mathbf{u}^{\prime}=\lambda x.\mathbf{u}^{\prime}_{1}$ concludes this case since $\mathbf{t}^{\prime}=\lambda x.\mathbf{t}^{\prime}_{1}\rightarrow_{\mathbf{n}_{k}}\lambda x.\mathbf{u}^{\prime}_{1}=\mathbf{u}^{\prime}$ and $\mathbf{u}=\lambda x.\mathbf{N}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>\leq\lambda x.\mathbf{u}^{\prime}_{1}=\mathbf{u}^{\prime}$.

  * $\mathbf{N}_{k}=\mathbf{N}^{\prime}_{k}\,\mathbf{s}$: Then $\mathbf{t}=\mathbf{N}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>\mathbf{s}$ and $\mathbf{u}=\mathbf{N}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>\mathbf{s}$ thus $\mathbf{t}^{\prime}=\mathbf{t}^{\prime}_{1}\,\mathbf{s}^{\prime}$ for some partial term $\mathbf{t}^{\prime}_{1},\mathbf{s}\in\mathbf{\Lambda}$ such that $\mathbf{N}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>\leq\mathbf{t}^{\prime}_{1}$ and $\mathbf{s}\leq\mathbf{s}^{\prime}$. Since $\mathbf{N}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>\rightarrow_{\mathbf{n}_{k}}\mathbf{N}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>$, by i.h. on $\mathbf{N}^{\prime}_{k}$, one obtains $\mathbf{u}^{\prime}_{1}\in\mathbf{\Lambda}$ such that $\mathbf{t}^{\prime}_{1}\rightarrow_{\mathbf{n}_{k}}\mathbf{u}^{\prime}_{1}$ and $\mathbf{N}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>\leq\mathbf{u}^{\prime}_{1}$. Taking $\mathbf{u}^{\prime}=\mathbf{u}^{\prime}_{1}\mathbf{s}^{\prime}$ concludes this case since $\mathbf{t}^{\prime}=\mathbf{t}^{\prime}_{1}\mathbf{s}^{\prime}\rightarrow_{\mathbf{n}_{k}}\mathbf{u}^{\prime}_{1}\mathbf{s}^{\prime}=\mathbf{u}^{\prime}$ and $\mathbf{u}=\mathbf{N}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>\mathbf{s}\leq\mathbf{u}^{\prime}_{1}\mathbf{s}^{\prime}=\mathbf{u}^{\prime}$ by transitivity.