* $\mathbf{N}_{k}=\mathbf{s}\,\mathbf{N}^{\prime}_{m}$ with either $k>0$ and $m=k-1$, or $k=m=\omega$: Then $\mathbf{t}=\mathbf{s}\,\mathbf{N}^{\prime}_{m}\\!\left<\mathbf{t}_{r}\right>$ and $\mathbf{u}=\mathbf{s}\,\mathbf{N}^{\prime}_{m}\\!\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{N}^{\prime}_{m}\\!\left<\mathbf{t}_{r}\right>\leq\mathbf{t}^{\prime}_{1}$. Since $\mathbf{N}^{\prime}_{m}\\!\left<\mathbf{t}_{r}\right>\rightarrow_{\mathbf{n}_{m}}\mathbf{N}^{\prime}_{m}\\!\left<\mathbf{u}_{r}\right>$, by i.h. on $\mathbf{N}^{\prime}_{m}$, one obtains $\mathbf{u}^{\prime}_{1}\in\mathbf{\Lambda}$ such that $\mathbf{t}^{\prime}_{1}\rightarrow_{\mathbf{n}_{m}}\mathbf{u}^{\prime}_{1}$ and $\mathbf{N}^{\prime}_{m}\\!\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_{\mathbf{n}_{k}}\mathbf{s}^{\prime}\mathbf{u}^{\prime}_{1}=\mathbf{u}^{\prime}$ and $\mathbf{u}=\mathbf{s}\,\mathbf{N}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>\leq\mathbf{s}^{\prime}\mathbf{u}^{\prime}_{1}=\mathbf{u}^{\prime}$ by transitivity.

  * $\mathbf{N}_{k}=\mathbf{N}^{\prime}_{k}[x\backslash\mathbf{s}]$: Then $\mathbf{t}=\mathbf{N}^{\prime}_{k}\\!\left<\mathbf{t}_{r}\right>[x\backslash\mathbf{s}]$ and $\mathbf{u}=\mathbf{N}^{\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{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}[x\backslash\mathbf{s}^{\prime}]$ concludes this case since $\mathbf{t}^{\prime}=\mathbf{t}^{\prime}_{1}[x\backslash\mathbf{s}^{\prime}]\rightarrow_{\mathbf{n}_{k}}\mathbf{u}^{\prime}_{1}[x\backslash\mathbf{s}^{\prime}]=\mathbf{u}^{\prime}$ and $\mathbf{u}=\mathbf{N}^{\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{N}_{k}=\mathbf{s}[x\backslash\mathbf{N}^{\prime}_{m}]$ with either $k>0$ and $m=k-1$, or $k=m=\omega$: Then $\mathbf{t}=\mathbf{s}[x\backslash\mathbf{N}^{\prime}_{m}\\!\left<\mathbf{t}_{r}\right>]$ and $\mathbf{u}=\mathbf{s}[x\backslash\mathbf{N}^{\prime}_{m}\\!\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{N}^{\prime}_{m}\\!\left<\mathbf{t}_{r}\right>\leq\mathbf{t}^{\prime}_{1}$. Since $\mathbf{N}^{\prime}_{m}\\!\left<\mathbf{t}_{r}\right>\rightarrow_{\mathbf{n}_{m}}\mathbf{N}^{\prime}_{m}\\!\left<\mathbf{u}_{r}\right>$, by i.h. on $\mathbf{N}^{\prime}_{m}$, one obtains $\mathbf{u}^{\prime}_{1}\in\mathbf{\Lambda}$ such that $\mathbf{t}^{\prime}_{1}\rightarrow_{\mathbf{n}_{m}}\mathbf{u}^{\prime}_{1}$ and $\mathbf{N}^{\prime}_{m}\\!\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_{\mathbf{n}_{k}}\mathbf{s}^{\prime}[x\backslash\mathbf{u}^{\prime}_{1}]=\mathbf{u}^{\prime}$ and $\mathbf{u}=\mathbf{s}[x\backslash\mathbf{N}^{\prime}_{k}\\!\left<\mathbf{u}_{r}\right>]\leq\mathbf{s}^{\prime}[x\backslash\mathbf{u}^{\prime}_{1}]=\mathbf{u}^{\prime}$ by transitivity. ∎

#### Observability.

Let us recall the mutual inductive definitions of ${\tt bne}_{\mathbf{n}_{k}}$
and ${\tt bno}_{\mathbf{n}_{k}}$:

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

We now prove the instance of Axiom C for dCBN.

###### Lemma C.11 (dCBN Observability of Normal Form Approximants).

Let $k\in\mathbb{N}^{\omega}$ and $\mathbf{t}\in{\tt no}_{\mathrm{n}_{k}}$,
then $\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)\in{\tt
bno}_{\mathbf{n}_{k}}$.

###### Proof.

We strengthen the induction hypothesis:

Let $t\in\Lambda$ such that ${\tt NF}_{\mathrm{n}_{k}}(t)$, then
$\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)\in{\tt bno}_{\mathbf{n}_{k}}$. And
if, moreover, $\neg{\tt Abs}\left(t\right)$ then $\mathcal{M\\!A}_{{\tt
N}}\\!\left(t\right)\in{\tt bne}_{\mathbf{n}_{k}}$.

Since ${\tt NF}_{\mathrm{n}_{k}}(t)$, then in particular ${\tt
NF}_{\mathrm{n}}(t)$, so that $t$ is meaningful. We reason by induction on
$t\in\Lambda$:

  * $t=x$: Then $\neg{\tt Abs}\left(t\right)$ and $\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)=x\in{\tt bne}_{\mathbf{n}_{k}}$.

  * $t=\lambda x.t^{\prime}$: Then ${\tt NF}_{\mathrm{n}_{k}}(t^{\prime})$ and ${\tt Abs}\left(t\right)$, thus $\mathcal{M\\!A}_{{\tt N}}\\!\left(t^{\prime}\right)\in{\tt bno}_{\mathbf{n}_{k}}$ by i.h. on $t^{\prime}$. Hence, $\mathcal{M\\!A}_{{\tt N}}\\!\left(t\right)=\lambda y.\mathcal{M\\!A}_{{\tt N}}\\!\left(t^{\prime}\right)\in\lambda y.{\tt bno}_{\mathbf{n}_{k}}\subseteq{\tt bno}_{\mathbf{n}_{k}}$.

  * $t=t_{1}t_{2}$: Then $\neg{\tt Abs}\left(t\right)$, ${\tt NF}_{\mathrm{n}_{k}}(t_{1})$ and $\neg{\tt Abs}\left(t_{1}\right)$. By i.h. on $t_{1}$, one has that $\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{1}\right)\in{\tt bne}_{\mathbf{n}_{k}}$. We distinguish two cases:

    * –

$k=0$: 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)\in{\tt
bne}_{\mathbf{n}_{0}}\mathbf{t}\subseteq{\tt bno}_{\mathbf{n}_{0}}$.

    * –

$k\in\mathbb{N}\setminus\\{0\\}$ (resp. $k=\omega$): Then ${\tt
NF}_{\mathrm{n}_{m}}(t_{2})$ with $m=k-1$ (resp. $m=\omega$). By i.h. on
$t_{2}$, one has that $\mathcal{M\\!A}_{{\tt N}}\\!\left(t_{2}\right)\in{\tt
bno}_{\mathbf{n}_{m}}$ thus $\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)\in{\tt
bne}_{\mathbf{n}_{k}}{\tt bno}_{\mathbf{n}_{m}}\subseteq{\tt
bne}_{\mathbf{n}_{k}}$.

  * $t=t_{1}[x\backslash t_{2}]$: Impossible since ${\tt NF}_{\mathrm{n}_{k}}(t)$. ∎

Let us recall the inductive definition of dCBN stratified equality:

$\begin{array}[]{c}\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
1.64755pt\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
i}{\approx}x$}}\par}\par}}}$}\hskip
42.67912pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
12.41144pt\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}{\approx}\lambda x.u$}}\par}\par}}}$}\\\\[14.22636pt]
\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
2.30338pt\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{\hbox{\hbox{}\hbox{$t_{1}\overset{\scriptscriptstyle
0}{\approx}u_{1}\hfil\lx@intercol$}}\hbox{$t_{1}t_{2}\overset{\scriptscriptstyle
0}{\approx}u_{1}u_{2}$}}\par}\par}}}$}\hskip
14.22636pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
3.55331pt\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{\hbox{\hbox{}\hbox{\hbox{}\hskip
15.00002pt\hbox{\hbox{\hbox{}\hbox{$t_{1}\overset{\scriptscriptstyle
i+1}{\approx}u_{1}$}}\hbox{$t_{2}\overset{\scriptscriptstyle
i}{\approx}u_{2}$}}}}\hbox{$t_{1}t_{2}\overset{\scriptscriptstyle
i+1}{\approx}u_{1}u_{2}$}}\par}\par}}}$}\hskip
14.22636pt\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.86331pt\hbox{\hbox{\hbox{}\hbox{\hbox{}\hskip
15.00002pt\hbox{\hbox{\hbox{}\hbox{$t_{1}\overset{\scriptscriptstyle\omega}{\approx}u_{1}$}}\hbox{$t_{2}\overset{\scriptscriptstyle\omega}{\approx}u_{2}$}}}}\hbox{$t_{1}t_{2}\overset{\scriptscriptstyle\omega}{\approx}u_{1}u_{2}$}}}\par}\par}}}$}\\\\[14.22636pt]
\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
18.95084pt\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{$t_{1}\overset{\scriptscriptstyle
0}{\approx}u_{1}\hfil\lx@intercol$}}\hbox{$t_{1}[x\backslash
t_{2}]\overset{\scriptscriptstyle 0}{\approx}u_{1}[x\backslash
u_{2}]$}}\par}\par}}}$}\hskip
2.84544pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
20.20079pt\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
i+1}{\approx}u_{1}$}}\hbox{$t_{2}\overset{\scriptscriptstyle
i}{\approx}u_{2}$}}}}\hbox{$t_{1}[x\backslash
t_{2}]\overset{\scriptscriptstyle i+1}{\approx}u_{1}[x\backslash
u_{2}]$}}\par}\par}}}$}\hskip
2.84544pt\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\omega}{\approx}u_{1}$}}\hbox{$t_{2}\overset{\scriptscriptstyle\omega}{\approx}u_{2}$}}}}\hbox{$t_{1}[x\backslash
t_{2}]\overset{\scriptscriptstyle\omega}{\approx}u_{1}[x\backslash
u_{2}]$}}\par}\par}}}$}\end{array}$

We now prove the instance of Axiom D for dCBN.

###### Lemma C.12 (dCBN Stability of Meaningful Observables).

Let $k\in\mathbb{N}^{\omega}$ and $\mathbf{t}\in{\tt bno}_{\mathbf{n}_{k}}$.
Then for any $\mathbf{u}\in\mathbf{\Lambda}$ such that
$\mathbf{t}\leq\mathbf{u}$, one has that $\mathbf{u}\in{\tt
bno}_{\mathbf{n}_{k}}$ and $\mathbf{t}\overset{\scriptscriptstyle
k}{\approx}\mathbf{u}$.

###### 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 bne}_{\mathbf{n}_{k}}$ then $\mathbf{u}\in{\tt bne}_{\mathbf{n}_{k}}$.

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

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

By mutual induction on $\mathbf{t}\in{\tt bno}_{\mathbf{n}_{k}}$ and
$\mathbf{t}\in{\tt bne}_{\mathbf{n}_{k}}$:

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

    * $\mathbf{t}=x$: Then $\mathbf{u}=x\in{\tt bne}_{\mathbf{n}}$ and $\mathbf{t}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}$ using $({\tt var})$.

    * $\mathbf{t}=\mathbf{t}_{1}\mathbf{t}_{2}$: 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}$. Moreover $\mathbf{t}_{1}\in{\tt bne}_{\mathbf{n}_{k}}$ thus by i.h. on $\mathbf{t}_{1}$, one has that $\mathbf{u}_{1}\in{\tt bne}_{\mathbf{n}_{k}}$ and $\mathbf{t}_{1}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}_{1}$. We distinguish two cases:

      * $\bullet$

$k=0$: Then $\mathbf{u}=\mathbf{u}_{1}\mathbf{u}_{2}\in{\tt
bne}_{\mathbf{n}_{0}}\mathbf{t}\subseteq{\tt bne}_{\mathbf{n}_{0}}$ and
$\mathbf{t}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}$ using $({\tt
app})$.

      * $\bullet$

$k\in\mathbb{N}\setminus\\{0\\}$ (resp. $k=\omega$): Then $m=k-1$ (resp.
$m=\omega$) and $\mathbf{t}_{2}\in{\tt bno}_{\mathbf{n}_{m}}$. By i.h. on
$t_{2}$, one has that $\mathbf{u}_{2}\in{\tt bno}_{\mathbf{n}_{m}}$ and
$\mathbf{t}_{2}\overset{\scriptscriptstyle m}{\approx}\mathbf{u}_{2}$. Thus
$\mathbf{u}=\mathbf{u}_{1}\mathbf{u}_{2}\in{\tt bne}_{\mathbf{n}_{k}}{\tt
bno}_{\mathbf{n}_{m}}\subseteq{\tt bne}_{\mathbf{n}_{k}}$ and
$\mathbf{t}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}$ using $({\tt
app})$.

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

    * $\mathbf{t}=\lambda x.\mathbf{t}^{\prime}$: Then $\mathbf{t}^{\prime}\in{\tt bno}_{\mathbf{n}_{k}}$ and $\mathbf{u}=\lambda x.\mathbf{u}^{\prime}$ with $\mathbf{t}^{\prime}\leq\mathbf{u}^{\prime}$. By i.h. on $\mathbf{t}^{\prime}$, one has $\mathbf{u}^{\prime}\in{\tt bno}_{\mathbf{n}_{k}}$ and $\mathbf{t}^{\prime}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}^{\prime}$. Thus $\mathbf{u}=\lambda x.\mathbf{u}^{\prime}\in\lambda x.{\tt bno}_{\mathbf{n}_{k}}\subseteq{\tt bno}_{\mathbf{n}_{k}}$ and $\mathbf{t}\overset{\scriptscriptstyle k}{\approx}\mathbf{u}$ using $({\tt abs})$.

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

*

###### Proof.

By definition, there exists $s\in{\tt no}_{\mathrm{n}_{k}}$ such that
$\mathtt{C}\\!\left<t\right>\rightarrow^{*}_{\mathrm{n}_{k}}s$. By iterating
Lemmas C.9 and C.10, there exist $\mathbf{s}\in\mathbf{\Lambda}$ and
$n\in\mathbb{N}$ such that $\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{C}\\!\left<t\right>\right)\rightarrow^{n}_{\mathbf{n}_{k}}\mathbf{s}\geq\mathcal{M\\!A}_{{\tt
N}}\\!\left(s\right)$. Since $s\in{\tt no}_{\mathrm{n}_{k}}$, then
$\mathcal{M\\!A}_{{\tt N}}\\!\left(s\right)\in{\tt bno}_{\mathbf{n}_{k}}$
using Lemma C.11, thus $\mathbf{s}\in{\tt bno}_{\mathbf{n}_{k}}$ using Lemma
C.12. On one hand, by Section 5.2, one has that $\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{C}\\!\left<t\right>\right)\leq\mathtt{C}\\!\left<t\right>$
thus, by iterating Lemma C.10, one has that
$\mathtt{C}\\!\left<t\right>\rightarrow^{n}_{\mathrm{n}_{k}}t^{\prime}$ for
some $t^{\prime}\in\Lambda$ such that $\mathbf{s}\leq t^{\prime}$. By Lemma
C.12, one deduces that $t^{\prime}\in{\tt no}_{\mathrm{n}_{k}}$ and
$t^{\prime}\overset{\scriptscriptstyle k}{\approx}\mathbf{s}$. One the other
hand, using Section 5.2, one has that $\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{C}\\!\left<t\right>\right)\leq\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{C}\\!\left<u\right>\right)$ thus $\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{C}\\!\left<t\right>\right)\leq\mathtt{C}\\!\left<u\right>$
using Section 5.2 and transitivity. By iterating Lemma C.10 again, one has
that $\mathtt{C}\\!\left<u\right>\rightarrow^{n}_{\mathrm{n}_{k}}u^{\prime}$
for some $u^{\prime}\in\Lambda$ such that $\mathbf{s}\leq u^{\prime}$. By
Lemma C.12, one deduces that $u^{\prime}\in{\tt no}_{\mathrm{n}_{k}}$ and
$u^{\prime}\overset{\scriptscriptstyle k}{\approx}\mathbf{s}$. Finally, by
transitivity of $\overset{\scriptscriptstyle k}{\approx}$, one deduces that
$t^{\prime}\overset{\scriptscriptstyle k}{\approx}u^{\prime}$.

Graphically, these are the main steps of the proof:

$\mathcal{M\\!A}_{{\tt
N}}\\!\left(\mathtt{C}\\!\left<t\right>\right)$$\mathbf{s}\\!$$\mathtt{C}\\!\left<t\right>$$t^{\prime}\\!$$\in$${\tt
no}_{\mathrm{n}_{k}}$$\mathtt{C}\\!\left<u\right>$$u^{\prime}\\!$$\in$${\tt
no}_{\mathrm{n}_{k}}$$\scriptscriptstyle
n$$\scriptscriptstyle\mathbf{n}_{k}$$\scriptscriptstyle
n$$\scriptscriptstyle\mathrm{n}_{k}$$\scriptscriptstyle
n$$\scriptscriptstyle\mathrm{n}_{k}$$\leftsquigarrow$$\scriptscriptstyle{\tt
Lem}.\ref{lem:cbn_t_->Sn_u_and_t_<=_t'_==>_t'_->Sn_u'_and_u_<=_u'}$$\rightsquigarrow$$\scriptscriptstyle{\tt
Lem}.\ref{lem:cbn_t_->Sn_u_=>_MA(t)_->*Sn_MA(u)}$$\rightsquigarrow$$\scriptscriptstyle{\tt
Lem}.\ref{lem:cbn_t_->Sn_u_and_t_<=_t'_==>_t'_->Sn_u'_and_u_<=_u'}$$\geq$$\scriptscriptstyle{\tt
Lem.}\ref{lem:Cbn_MA(t)_<=_t}$$\geq$$\leq$$\scriptscriptstyle{\tt
Lem.}\ref{lem:cbn_Approximant_Genericity}\;\&\;{\tt
Lem.}\ref{lem:Cbn_MA(t)_<=_t}$$\leq$$\overset{\scriptscriptstyle
k}{\scalebox{4.0}[1.0]{$\approx$}}$$\scriptscriptstyle{\tt
Lem.}\ref{lem:cbn_t_in_bnoSn_and_t_<=_u_==>_u_in_BnoSn}$

∎

##  Appendix D Proofs of Section 6

###  D.1. Proofs of Subsection 6.1

Let us recall the rules of the congruence $\mathcal{C}_{\mathsf{B}}$.

$\begin{array}[]{c}\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
14.3055pt\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
ref})$}}}\hbox{\hbox{\hbox{}\hbox{}}\hbox{$t\doteq
t\hfil\lx@intercol$}}\par}\par}}}$}\hskip
17.07182pt\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
sym})$}}}\hbox{\hbox{\hbox{}\hbox{$t\doteq u$}}\hbox{$u\doteq
t$}}\par}\par}}}$}\hskip
17.07182pt\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 tra})$}}}\hbox{\hskip
8.03821pt\hbox{\hbox{\hbox{}\hbox{\hbox{}\hskip
15.00002pt\hbox{\hbox{\hbox{}\hbox{$t\doteq s$}}\hbox{$s\doteq
u$}}}}\hbox{$t\doteq u$}}}\par}\par}}}$}\hskip
17.07182pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
18.3335pt\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
ctx})$}}}\hbox{\hbox{\hbox{}\hbox{$t\doteq
u$}}\hbox{$\mathtt{C}\\!\left<t\right>\doteq\mathtt{C}\\!\left<u\right>$}}\par}\par}}}$}\hskip
17.07182pt\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
base})$}}}\hbox{\hskip
7.5695pt\hbox{\hbox{\hbox{}\hbox{$(t,u)\\!\in\\!\mathsf{B}$}}\hbox{$t\doteq
u$}}}\par}\par}}}$}\end{array}$

We define the theory $\bm{\mathcal{H}}^{\tt ax}$ to be the set of equations
generated by the following rules.

$\begin{array}[]{c}\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
14.4444pt\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
Refl})$}}}\hbox{\hbox{\hbox{}\hbox{}}\hbox{$t\approx
t\hfil\lx@intercol$}}\par}\par}}}$}\hskip
14.22636pt\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
Base})$}}}\hbox{\hskip
7.9167pt\hbox{\hbox{\hbox{}\hbox{$(t,u\in\mathsf{H})$}}\hbox{$t\approx
u$}}}\par}\par}}}$}\hskip
14.22636pt\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
Sym})$}}}\hbox{\hbox{\hbox{}\hbox{$t\approx u$}}\hbox{$u\approx
t$}}\par}\par}}}$}\hskip
14.22636pt\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
Conv})$}}}\hbox{\hbox{\hbox{}\hbox{$t\approx u$}}\hbox{$t\sim
u$}}\par}\par}}}$}\hskip
14.22636pt\hbox{$\vbox{\hbox{\hbox{}\vbox{\hbox{\hskip
18.3335pt\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
Ctxt})$}}}\hbox{\hbox{\hbox{}\hbox{$t\sim
u$}}\hbox{$\mathtt{C}\\!\left<t\right>\sim\mathtt{C}\\!\left<u\right>$}}\par}\par}}}$}\hskip
14.22636pt\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
Conv})$}}}\hbox{\hskip 0.1389pt\hbox{\hbox{\hbox{}\hbox{$t\sim
u$}}\hbox{$t\doteq u$}}}\par}\par}}}$}\hskip
14.22636pt\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
Trans})$}}}\hbox{\hskip 8.03821pt\hbox{\hbox{\hbox{}\hbox{\hbox{}\hskip
15.00002pt\hbox{\hbox{\hbox{}\hbox{$t\doteq s$}}\hbox{$s\doteq
u$}}}}\hbox{$t\doteq u$}}}\par}\par}}}$}\end{array}$

We write $\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq u$ (resp.
$\bm{\mathcal{H}}^{\tt ax}\vdash t\approx u$, $\bm{\mathcal{H}}^{\tt ax}\vdash
t\sim u$) if $t\doteq u\in\bm{\mathcal{H}}^{\tt ax}$ (resp. $t\approx
u\in\bm{\mathcal{H}}^{\tt ax}$, $t\sim u\in\bm{\mathcal{H}}^{\tt ax}$).

lemmaGenTheoryTaxEquivalentTheoryH Let $t,u\in\Lambda$. Then
$\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq u$ iff $\mathsf{H}\vdash t\doteq u$.

###### Proof.

By double implication:

  * $(\Rightarrow)$

By mutual induction on the length of the proof of $\bm{\mathcal{H}}^{\tt
ax}\vdash t\doteq u$, $\bm{\mathcal{H}}^{\tt ax}\vdash t\approx u$ and
$\bm{\mathcal{H}}^{\tt ax}\vdash t\sim u$, one shows that $\mathsf{H}\vdash
t\doteq u$. Cases on the last rule applied:

    * $({\tt Refl})$: Then $t=u$ and using $({\tt ref})$, one concludes that $\mathsf{H}\vdash t\doteq u$.

    * $({\tt Base})$: Then $(t,u)\in\mathsf{H}$ and using $({\tt base})$, one concludes that $\mathsf{H}\vdash t\doteq u$.

    * $({\tt Sym})$: Then $\bm{\mathcal{H}}^{\tt ax}\vdash u\approx t$ and by i.h., one obtains $\mathsf{H}\vdash u\doteq t$ thus using $({\tt sym})$, one concludes that $\mathsf{H}\vdash t\doteq u$.

    * $({\tt Conv})$: Then $\bm{\mathcal{H}}^{\tt ax}\vdash t\approx u$ thus by i.h., one concludes that $\mathsf{H}\vdash t\doteq u$.

    * $({\tt Ctxt})$: Then $t=\mathtt{C}\\!\left<t^{\prime}\right>$ and $u=\mathtt{C}\\!\left<u^{\prime}\right>$ for some $t^{\prime},u^{\prime}\in\Lambda$ such that $\bm{\mathcal{H}}^{\tt ax}\vdash t^{\prime}\sim u^{\prime}$. By i.h., one obtains that $\mathsf{H}\vdash t^{\prime}\doteq u^{\prime}$ thus using $({\tt ctx})$, one concludes that $\mathsf{H}\vdash t\doteq u$.

    * $({\tt Conv})$: Then $\bm{\mathcal{H}}^{\tt ax}\vdash t\sim u$ and by i.h., one concludes that $\mathsf{H}\vdash t\doteq u$.

    * $({\tt Trans})$: Then $\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq s$ and $\bm{\mathcal{H}}^{\tt ax}\vdash s\doteq u$ for some $s\in\Lambda$. By i.h. on both, one has that $\mathsf{H}\vdash t\doteq s$ and $\mathsf{H}\vdash s\doteq u$ thus using $({\tt tra})$, one concludes that $\mathsf{H}\vdash t\doteq u$.

  * $(\Leftarrow)$

Let us first show the following property (P1): provability of
$\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq u$ and $\bm{\mathcal{H}}^{\tt
ax}\vdash t\sim u$ is symmetric. By mutual induction on $\bm{\mathcal{H}}^{\tt
ax}\vdash t\doteq u$ and $\bm{\mathcal{H}}^{\tt ax}\vdash t\sim u$. Cases on
the last rule applied:

    * $({\tt Conv})$: Then $\bm{\mathcal{H}}^{\tt ax}\vdash t\approx u$ and using $({\tt Sym})$, one has that $\bm{\mathcal{H}}^{\tt ax}\vdash u\approx t$ thus using $({\tt Conv})$, one concludes that $\bm{\mathcal{H}}^{\tt ax}\vdash u\sim t$.

    * $({\tt Ctxt})$: Then $t=\mathtt{C}\\!\left<t^{\prime}\right>$, $u=\mathtt{C}\\!\left<u^{\prime}\right>$ for some $t^{\prime},u^{\prime}\in\Lambda$ such that $\bm{\mathcal{H}}^{\tt ax}\vdash t^{\prime}\sim u^{\prime}$. By i.h., one has that $\bm{\mathcal{H}}^{\tt ax}\vdash u^{\prime}\sim t^{\prime}$ thus using $({\tt Ctxt})$, one concludes that $\bm{\mathcal{H}}^{\tt ax}\vdash u\sim t$.

    * $({\tt Conv})$: Then $\bm{\mathcal{H}}^{\tt ax}\vdash t\sim u$ and by i.h., one has that $\bm{\mathcal{H}}^{\tt ax}\vdash u\sim t$ thus using $({\tt Conv})$, one concludes that $\bm{\mathcal{H}}^{\tt ax}\vdash u\doteq t$.

    * $({\tt Trans})$: Then $\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq s$ and $\bm{\mathcal{H}}^{\tt ax}\vdash s\doteq u$ for some $s\in\Lambda$. By i.h. on both, one has that $\bm{\mathcal{H}}^{\tt ax}\vdash s\doteq t$ and $\bm{\mathcal{H}}^{\tt ax}\vdash u\doteq s$ thus, using $({\tt Trans})$, one concludes that $\bm{\mathcal{H}}^{\tt ax}\vdash u\doteq t$.

We then show the following property (P2): provability of
$\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq u$ is a congruence. Let
$\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq u$, let us show that
$\bm{\mathcal{H}}^{\tt
ax}\vdash\mathtt{C}\\!\left<t\right>\doteq\mathtt{C}\\!\left<u\right>$. By
induction on the length of the proof of $\bm{\mathcal{H}}^{\tt ax}\vdash
t\doteq u$. Cases on the last rule applied:

    * $({\tt Conv})$: Then $\bm{\mathcal{H}}^{\tt ax}\vdash t\sim u$ thus using $({\tt Ctxt})$, one obtains $\bm{\mathcal{H}}^{\tt ax}\vdash\mathtt{C}\\!\left<t\right>\sim\mathtt{C}\\!\left<u\right>$ and using $({\tt Conv})$, one concludes that $\bm{\mathcal{H}}^{\tt ax}\vdash\mathtt{C}\\!\left<t\right>\doteq\mathtt{C}\\!\left<u\right>$.

    * $({\tt Trans})$: Then $\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq s$ and $\bm{\mathcal{H}}^{\tt ax}\vdash s\doteq u$ for some $s\in\Lambda$. By i.h. on both, one has that $\bm{\mathcal{H}}^{\tt ax}\vdash\mathtt{C}\\!\left<t\right>\doteq\mathtt{C}\\!\left<s\right>$ and $\bm{\mathcal{H}}^{\tt ax}\vdash\mathtt{C}\\!\left<s\right>\doteq\mathtt{C}\\!\left<u\right>$ thus using $({\tt Trans})$, one concludes that $\bm{\mathcal{H}}^{\tt ax}\vdash\mathtt{C}\\!\left<t\right>\doteq\mathtt{C}\\!\left<u\right>$.

Let us now show the main property. By induction on the length of the proof of
$\mathsf{H}\vdash t\doteq u$. Cases on the last rule applied:

    * $({\tt ref})$: Then $t=u$ and using $({\tt Refl})$, $({\tt Conv})$ and $({\tt Conv})$, one concludes that $\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq u$.

    * $({\tt base})$: Then $(t,u)\in\mathsf{H}$ and using $({\tt Base})$, $({\tt Conv})$ and $({\tt Conv})$, one concludes that $\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq u$.

    * $({\tt sym})$: Then $\mathsf{H}\vdash u\doteq t$ thus by i.h. $\bm{\mathcal{H}}^{\tt ax}\vdash u\doteq t$ and by property (P1), one concludes that $\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq u$.

    * $({\tt tra})$: Then $\mathsf{H}\vdash t\doteq s$ and $\mathsf{H}\vdash s\doteq u$ and by i.h. on both, one has that $\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq s$ and $\bm{\mathcal{H}}^{\tt ax}\vdash s\doteq u$ thus using $({\tt Trans})$, one concludes that $\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq u$.

    * $({\tt ctx})$: Then $t=\mathtt{C}\\!\left<t^{\prime}\right>$ and $u=\mathtt{C}\\!\left<u^{\prime}\right>$ for some $t^{\prime},u^{\prime}\in\Lambda$ such that and $\mathsf{H}\vdash t^{\prime}\doteq u^{\prime}$. By i.h., one has $\bm{\mathcal{H}}^{\tt ax}\vdash t^{\prime}\doteq u^{\prime}$ and by property (P2), one concludes that $\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq u$. ∎

###### Lemma D.1.

Let $t,u\in\Lambda$, then

  1. (1)

If $\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq u$, then there exist
$n\in\mathbb{N}$ and $s_{0},\dots,s_{n}\in\Lambda$ such that $t=s_{0}$,
$u=s_{n}$ and $\bm{\mathcal{H}}^{\tt ax}\vdash s_{i}\sim s_{i+1}$ for $0\leq
i<n$.

  2. (2)

$\bm{\mathcal{H}}^{\tt ax}\vdash t\approx u$ if and only if $\mathsf{R}\vdash
t\doteq u$ or $\mathsf{R}\vdash u\doteq t$ from an axiom, or $t$ and $u$ are
meaningless.

###### Proof.

  1. (1)

By induction on the length of the proof of $\bm{\mathcal{H}}^{\tt ax}\vdash
t\doteq u$. Cases on the last rule applied:

     * $({\tt Conv})$: Then $\bm{\mathcal{H}}^{\tt ax}\vdash t\sim u$ and we set $n:=0$ with $s_{0}:=t=u$ which concludes this case since using $({\tt Refl})$ and $({\tt Conv})$, one has $\bm{\mathcal{H}}^{\tt ax}\vdash s_{0}\sim s_{0}$.

     * $({\tt Trans})$: Then $\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq s^{\prime}$ and $\bm{\mathcal{H}}^{\tt ax}\vdash s^{\prime}\doteq u$ for some $s^{\prime}\in\Lambda$. By i.h. on both, one has $n_{1},n_{2}\in\mathbb{N}$ and $s_{1}^{0},\dots,s_{1}^{n_{1}},s_{2}^{0},\dots,s_{2}^{n_{2}}\in\Lambda$ such that $t=s_{1}^{0}$, $s^{\prime}=s_{1}^{n_{1}}$, $s^{\prime}=s_{2}^{0}$, $u=s_{2}^{n_{2}}$, $\bm{\mathcal{H}}^{\tt ax}\vdash s_{1}^{i}\sim s_{1}^{i+1}$ for all $0\leq i<n_{1}$ and $\bm{\mathcal{H}}^{\tt ax}\vdash s_{2}^{i}\sim s_{2}^{i+1}$ for all $0\leq i<n_{2}$. We set $n:=n_{1}+n_{2}$, $s_{i}:=s_{1}^{i}$ for $0\leq i\leq n_{1}$ and $s_{n_{1}+i}:=s_{2}^{i}$ for $0<i\leq n_{2}$ which concludes this case since $s_{1}^{n_{1}}=s^{\prime}=s_{2}^{0}$.

  2. (2)

By double implication:

     * $(\Rightarrow)$

By induction on the length of the proof of $\bm{\mathcal{H}}^{\tt ax}\vdash
t\approx u$. Cases on the last rule applied:

       * $({\tt Refl})$: Then $\mathsf{R}\vdash t\doteq u$ using $({\tt Refl})$.

       * $({\tt Base})$: Then $(t,u)\in\mathsf{H}$. We distinguish two cases:

         * $(t,u\in\mathsf{R})$: Then $\mathsf{R}\vdash t\doteq u$ using $({\tt Base})$.

         * $t,u$ meaningless.

       * $({\tt Sym})$: Then $\bm{\mathcal{H}}^{\tt ax}\vdash u\approx t$ and by i.h., one has that either $\mathsf{R}\vdash u\doteq t$ or $\mathsf{R}\vdash t\doteq u$ from an axiom, or $t$ and $u$ are meaningless, thus concluding this case.

     * $(\Leftarrow)$

We distinguish three cases:

       * $\mathsf{R}\vdash t\doteq u$ from an axiom: We distinguish two cases:

         * $({\tt Refl})$: Then $t=u$ and using $({\tt Refl})$, one concludes that $\bm{\mathcal{H}}^{\tt ax}\vdash t\approx u$.

         * $({\tt Base})$: Then $(t,u)\in\mathsf{R}$ thus $\bm{\mathcal{H}}^{\tt ax}\vdash t\approx u$ using $({\tt Base})$.

       * $\mathsf{R}\vdash u\doteq t$ from an axiom: We distinguish two cases:

         * $({\tt Refl})$: Then $u=t$ and using $({\tt Refl})$, one concludes that $\bm{\mathcal{H}}^{\tt ax}\vdash t\approx u$.

         * $({\tt Base})$: Then $(t,u)\in\mathsf{R}$ thus $\bm{\mathcal{H}}^{\tt ax}\vdash t\approx u$ using $({\tt Base})$ and $({\tt Sym})$.

       * $t$ and $u$ are meaningless: Then using $({\tt Base})$, one concludes that $\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq u$. ∎

###### Lemma D.2.

Let $t,u\in\Lambda$ such that $\bm{\mathcal{H}}^{\tt ax}\vdash t\sim u$, then
there exist a context $\mathtt{C}$ and terms $t^{\prime},u^{\prime}\in\Lambda$
such that $t=\mathtt{C}\\!\left<t^{\prime}\right>$,
$u=\mathtt{C}\\!\left<u^{\prime}\right>$ and $\bm{\mathcal{H}}^{\tt ax}\vdash
t^{\prime}\approx u^{\prime}$.

###### Proof.

By induction on the length of the proof of $\bm{\mathcal{H}}^{\tt ax}\vdash
t\sim u$. Cases on the last rule applied:

  * $({\tt Conv})$: Then $\bm{\mathcal{H}}^{\tt ax}\vdash t\approx u$ and we set $\mathtt{C}:=\diamond$, $t^{\prime}:=t$ and $u^{\prime}:=u$ which concludes this case since $t=\diamond\\!\left<t\right>=\mathtt{C}\\!\left<t^{\prime}\right>$, $u=\diamond\\!\left<u\right>=\mathtt{C}\\!\left<u^{\prime}\right>$ and $\bm{\mathcal{H}}^{\tt ax}\vdash t^{\prime}\approx u^{\prime}$ by hypothesis.

  * $({\tt Ctxt})$: Then $t=\mathtt{C}^{\prime\prime}\\!\left<t^{\prime\prime}\right>$ and $u=\mathtt{C}^{\prime\prime}\\!\left<u^{\prime\prime}\right>$ for some terms $t^{\prime},u^{\prime}\in\Lambda$ such that $\bm{\mathcal{H}}^{\tt ax}\vdash t^{\prime\prime}\sim u^{\prime\prime}$. By i.h., there exists a context $\mathtt{C}^{\prime}$ and terms $t^{\prime},u^{\prime}\in\Lambda$ such that $t^{\prime\prime}=\mathtt{C}^{\prime}\\!\left<t^{\prime}\right>$, $u^{\prime\prime}=\mathtt{C}^{\prime}\\!\left<u^{\prime}\right>$ and $\bm{\mathcal{H}}^{\tt ax}\vdash t^{\prime}\approx u^{\prime}$. We set $\mathtt{C}:=\mathtt{C}^{\prime\prime}\\!\left<\mathtt{C}^{\prime}\right>$ which concludes this case since $t=\mathtt{C}^{\prime\prime}\\!\left<t^{\prime\prime}\right>=\mathtt{C}^{\prime\prime}\\!\left<\mathtt{C}^{\prime}\\!\left<t^{\prime}\right>\right>=(\mathtt{C}^{\prime\prime}\\!\left<\mathtt{C}^{\prime}\right>)\\!\left<t^{\prime}\right>=\mathtt{C}\\!\left<t^{\prime}\right>$ and $u=\mathtt{C}^{\prime\prime}\\!\left<u^{\prime\prime}\right>=\mathtt{C}^{\prime\prime}\\!\left<\mathtt{C}^{\prime}\\!\left<u^{\prime}\right>\right>=(\mathtt{C}^{\prime\prime}\\!\left<\mathtt{C}^{\prime}\right>)\\!\left<t^{\prime}\right>=\mathtt{C}\\!\left<u^{\prime}\right>$. ∎

Let us recall the first axiom:

*

###### Lemma D.3.

Let $t,u\in\Lambda$ such that $\mathsf{R}\vdash t\doteq u$. Then $t$ has a
$\omega$-normal form if and only if $u$ has a $\omega$-normal form.

Moreover, they share the same $\mathtt{S}_{\omega}$-normal form.

###### Proof.

Let $t,u\in\Lambda$ such that $\mathsf{R}\vdash t\doteq u$. Using Section 6.1,
one deduces that $t\mathbin{={{}_{\\!\\!\mathsf{R}}}}u$. By induction on the
length of the sequence $t\mathbin{={{}_{\\!\\!\mathsf{R}}}}u$.

  * $({\tt refl})$: Then $t$ is equal to $u$ and trivially $t$ has a $\omega$-normal form if and only if $u$ has a $\omega$-normal form. Moreover, they also share the same $\omega$-normal form.

  * $({\tt one-step})$: Then $t\rightarrow_{\omega}u$ and one concludes by Confluence (Axiom E).

  * $({\tt sym})$: Then $t\mathbin{={{}_{\\!\\!\mathsf{R}}}}u$ and one concludes by i.h..

  * $({\tt trans})$: Then $t\mathbin{={{}_{\\!\\!\mathsf{R}}}}s$ and $s\mathbin{={{}_{\\!\\!\mathsf{R}}}}u$ for some $s\in\Lambda$. We distinguish two cases:

    * $t$ has a $\omega$-normal form: Then by i.h. on $t\mathbin{={{}_{\\!\\!\mathsf{R}}}}s$, one deduces that $s$ has the same $\omega$-normal form as $t$ thus by i.h. on $s\mathbin{={{}_{\\!\\!\mathsf{R}}}}u$, one concludes that $u$ has the same $\omega$-normal form as $t$.

    * $u$ has a $\omega$-normal form: Symmetric of the previous case.

∎

lemmaGenTheoryHAndTaxAgreeFNF If $u\in\Lambda$ has a $\omega$-normal form,
then for any $t\in\Lambda$, if $\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq u$
then $\mathsf{R}\vdash t\doteq u$.

###### Proof.

Let $t,u\in\Lambda$ such that $u$ has a $\omega$-normal form and
$\bm{\mathcal{H}}^{\tt ax}\vdash t\doteq u$. Using Lemma D.1:1, one has
$n\in\mathbb{N}$ and $s_{0},\dots,s_{n}\in\Lambda$ such that $t=s_{0}$,
$u=s_{n}$ and $\bm{\mathcal{H}}^{\tt ax}\vdash s_{i}\sim s_{i+1}$ for $0\leq
i<n$. Let us show the following:

If $s_{n}$ has a $\omega$-normal form, and $\bm{\mathcal{H}}^{\tt ax}\vdash
s_{i}\sim s_{i+1}$ for $0\leq i<n$, then $\mathsf{R}\vdash s_{0}\doteq s_{n}$.

We reason by induction on $n\in\mathbb{N}$. Cases:

  * $n=0$: Then $s_{0}=s_{n}$ and thus $\mathsf{R}\vdash s_{0}\doteq s_{n}$ by $({\tt Refl})$.

  * $n=m+1$: Then using Lemma D.2, there exist a context $\mathtt{C}$ and terms $s^{\prime}_{m},s^{\prime}_{m+1}\in\Lambda$ such that $s_{m}=\mathtt{C}\\!\left<s^{\prime}_{m}\right>$, $s_{m+1}=\mathtt{C}\\!\left<s^{\prime}_{m+1}\right>$ and $\bm{\mathcal{H}}^{\tt ax}\vdash s^{\prime}_{m}\approx s^{\prime}_{m+1}$. By Lemma D.1:2, we distinguish two cases:

    * $\mathsf{R}\vdash s^{\prime}_{m}\doteq s^{\prime}_{m+1}$ (resp. $\mathsf{R}\vdash s^{\prime}_{m+1}\doteq s^{\prime}_{m}$) from an axiom: Then $\mathsf{R}$ $\vdash\mathtt{C}\\!\left<s^{\prime}_{m}\right>\doteq\mathtt{C}\\!\left<s^{\prime}_{m+1}\right>$ by contextuality (resp. and symmetry) thus using Lemma D.3, one deduces that $s_{m}=\mathtt{C}\\!\left<s^{\prime}_{m}\right>$ has a $\omega$-norm form. By i.h., one concludes that $\mathsf{R}\vdash s_{0}\doteq s_{m}$, thus $\mathsf{R}\vdash s_{0}\doteq s_{m+1}$ holds by $({\tt Trans})$.

    * $s^{\prime}_{m}$ and $s^{\prime}_{m+1}$ are meaningless: Since $s_{m+1}=\mathtt{C}\\!\left<s^{\prime}_{m+1}\right>$ has a $\omega$-normal form, let say $s\in\Lambda$, then $s_{m+1}\mathbin{={{}_{\\!\\!\mathsf{R}}}}s$, which implies $\mathsf{R}\vdash s_{m+1}\doteq s$ by Section 6.1. Using Full Genericity (Axiom F), one deduces that $s_{m}=\mathtt{C}\\!\left<s^{\prime}_{m}\right>$ has the same $\omega$-normal form $s$ thus $\mathsf{R}\vdash s_{m}\doteq s$ by Section 6.1. Therefore $\mathsf{R}\vdash s_{m}\doteq s_{m+1}$ using $({\tt Sym})$ and $({\tt Trans})$. By i.h., one has that $\mathsf{R}\vdash s_{0}\doteq s_{m}$ and we conclude that $\mathsf{R}\vdash s_{0}\doteq s_{m+1}$ using $({\tt Trans})$. ∎

*

###### Proof.

Using Lemma D.3 and Section D.1. ∎

###### Lemma D.4.

  1. (1)

$\bm{\mathcal{R}}\subseteq\bm{\mathcal{H}}^{*}$.

  2. (2)

$\bm{\mathcal{H}}\subseteq\bm{\mathcal{H}}^{*}$.

###### Proof.

  1. (1)

Let $\mathsf{R}\vdash t\doteq u$. Let us show that
$(t,u)\in\bm{\mathcal{H}}^{*}$ by induction on the length of the proof
$\mathsf{R}\vdash t\doteq u$. Cases on the last rule applied:

     * $({\tt ref})$: Then $t=u$ thus $(t,u)\in\bm{\mathcal{H}}^{*}$ trivially holds.

     * $({\tt base})$: Then $(t,u)\in\mathsf{R}$ and using Axiom G, one deduces that $t$ is meaningful if and only if $u$ is meaningful so that $(t,u)\in\bm{\mathcal{H}}^{*}$.

     * $({\tt sym})$: Then $\mathsf{R}\vdash u\doteq t$ and, by i.h., $(u,t)\in\bm{\mathcal{H}}^{*}$; one concludes by symmetry of the logical equivalence in the definition of $\bm{\mathcal{H}}^{*}$.

     * $({\tt tra})$: Then $\mathsf{R}\vdash t\doteq s$ and $\mathsf{R}\vdash s\doteq u$ for some $s\in\Lambda$, and by i.h. on both, one deduces that $(t,s)\in\bm{\mathcal{H}}^{*}$ and $(s,u)\in\bm{\mathcal{H}}^{*}$ respectively. Therefore one concludes by transitivity of the logical equivalence in the definition of $\bm{\mathcal{H}}^{*}$.

  2. (2)

By (1) one has that $\bm{\mathcal{R}}\subseteq\bm{\mathcal{H}}^{*}$, then it
is sufficient to show that $\bm{\mathcal{H}}^{*}$ equates all meaningless
terms. Let $t,u\in\Lambda$ be both meaningless. By Surface Genericity (Axiom
H), one has that $\mathtt{C}\\!\left<t\right>$ is meaningful if and only if
$\mathtt{C}\\!\left<u\right>$ is meaningful, thus
$(t,u)\in\bm{\mathcal{H}}^{*}$. ∎

###  D.2. Proofs of Subsection 6.2

###### Lemma D.5.

Let $t,u\in\Lambda$ and $x\in\mathcal{X}$ such that $t$ is meaningful, $x$ is
fresh in $t$ and $u$ and $\lambda x.tu$ is meaningful, then $u$ is meaningful.

###### Proof.

Let $t,u\in\Lambda$ and $x\in\mathcal{X}$ such that $t$ is meaningful, $x$ is
fresh in $t$ and $u$ and $(\lambda x.t)u$ is meaningful. Then by Lemma 2.4,
there exists $\Pi\triangleright_{\mathcal{V}}\Gamma\vdash(\lambda
x.t)u:\sigma$. Then $\Pi$ is necessarily of the following form:

$({\tt app})$ $\Pi_{1}\triangleright_{\mathcal{V}}\Gamma_{1}\vdash\lambda
x.t:\mathcal{M}\Rightarrow\sigma$$\Pi_{2}\triangleright_{\mathcal{V}}\Gamma_{2}\vdash
u:\mathcal{M}$$\Gamma_{1}+\Gamma_{2}\vdash(\lambda x.t)u:\sigma$

with $\Gamma=\Gamma_{1}+\Gamma_{2}$. Since
$\Pi_{2}\triangleright_{\mathcal{V}}\Gamma_{2}\vdash u:\mathcal{M}$, one then
deduces that $u$ is meaningful using (Logical). ∎

*

###### Proof.

Let $t,u\in\Lambda$ such that
$\mathcal{C}_{\mathsf{H}_{\mathsf{v}}\cup\\{(t,u)\\}}$ is consistent. Suppose
by absurd that there exists a context $\mathtt{C}$ such that
$\mathtt{C}\\!\left<t\right>$ is meaningful and $\mathtt{C}\\!\left<u\right>$
is meaningless. Let us show that
$\mathcal{C}_{\mathsf{H}_{\mathsf{v}}\cup\\{(t,u)\\}}$ is inconsistent.

Let $s\in\Lambda$ be a meaningful term and $x\in\mathcal{X}$ fresh. On one
hand, by definition of meaningfulness, there exists a testing context
$\mathtt{T}$ such that
$\mathtt{T}\\!\left<\mathtt{C}\\!\left<t\right>\right>\rightarrow^{*}_{\mathrm{v}}v$
for some value $v\in\Upsilon$. In particular, $(\lambda
x.s)\mathtt{T}\\!\left<\mathtt{C}\\!\left<t\right>\right>\rightarrow^{*}_{\mathrm{v}}(\lambda
x.s)v\rightarrow^{*}_{\mathrm{v}}s$ thus using Section 6.1, one deduces that
$\bm{\mathcal{T}}_{{\tt V}}\vdash(\lambda
x.s)\mathtt{T}\\!\left<\mathtt{C}\\!\left<t\right>\right>\doteq_{{\tt V}}s$.
Since $\bm{\mathcal{H}}_{{\tt dCBV}}$ is a $\lambda_{{\tt dCBV}}$-theory, then
$\bm{\mathcal{H}}_{{\tt V}}\vdash(\lambda
x.s)\mathtt{T}\\!\left<\mathtt{C}\\!\left<t\right>\right>\doteq_{{\tt V}}s$
and thus $\mathcal{C}_{\mathsf{H}_{\mathsf{v}}\cup\\{(t,u)\\}}$
$\vdash(\lambda
x.s)\mathtt{T}\\!\left<\mathtt{C}\\!\left<t\right>\right>\doteq s$. On the
other hand, by definition of meaninglesness,
$\mathtt{T}\\!\left<\mathtt{C}\\!\left<u\right>\right>$ necessarily
meaningless. Suppose by absurd that $(\lambda
x.s)\mathtt{T}\\!\left<\mathtt{C}\\!\left<u\right>\right>$ is meaningful, then
using Lemma D.5, one deduces that
$\mathtt{T}\\!\left<\mathtt{C}\\!\left<t\right>\right>$ is meaningful which is
impossible thus $(\lambda
x.s)\mathtt{T}\\!\left<\mathtt{C}\\!\left<u\right>\right>$ is therefore
meaningless. By contextuality and transitivity
$\mathcal{C}_{\mathsf{H}_{\mathsf{v}}\cup\\{(t,u)\\}}$ $\vdash(\lambda
x.s)\mathtt{T}\\!\left<\mathtt{C}\\!\left<u\right>\right>\doteq s$ and by
sensibility
$\mathcal{C}_{\mathsf{H}_{\mathsf{v}}\cup\\{(t,u)\\}}\vdash\Omega\doteq s$.
Since $s$ is an arbitrary meaningful term, one deduces that
$\mathcal{C}_{\mathsf{H}_{\mathsf{v}}\cup\\{(t,u)\\}}$ is inconsistent
contradicting the hypothesis and concluding this proof. ∎

*

###### Proof.

We first prove that $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}$ is a maximal
consistent and sensible $\lambda_{{\tt dCBV}}$-theory and then show that it is
unique.

  1. (1)

Maximality: By Corollary 6.3, $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}$ is a
consistent and sensible $\lambda_{{\tt dCBV}}$-theory. Let $t,u\in\Lambda$
such that $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}\cup\\{(t,u)\\}$ is consistent. By
inclusion, one deduces that
$\mathcal{C}_{\mathsf{H}_{\mathsf{v}}\cup\\{(t,u)\\}}$ is consistent, thus
that $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}\vdash t\doteq u$ using Corollary 6.3.
The theory $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}$ is therefore maximal.

  2. (2)

Unicity: Let $\mathcal{E}$ be a maximal consistent and sensible $\lambda_{{\tt
dCBV}}$-theory. Let $t,u\in\Lambda$ such that $\mathcal{E}\vdash t\doteq u$.
By inclusion, one deduces that
$\mathcal{C}_{\mathsf{H}_{\mathsf{v}}\cup\\{(t,u)\\}}$ is consistent thus
using Corollary 6.3, one has that $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}\vdash
t\doteq u$ and therefore $\mathcal{E}\subseteq\bm{\mathcal{H}}^{*}_{{\tt
dCBV}}$. Suppose by absurd that there exists $t,u\in\Lambda$ such that
$\bm{\mathcal{H}}^{*}_{{\tt dCBV}}\vdash t\doteq u$ but not $\mathcal{E}\vdash
t\doteq u$. Since $\bm{\mathcal{H}}^{*}_{{\tt dCBV}}$ is consistent, then by
inclusion, one deduces that $\mathcal{E}\cup\\{(t,u)\\}$ is consistent which
contradict the fact that $\mathcal{E}$ is a maximal consistent and sensible
$\lambda_{{\tt dCBV}}$-theory. One concludes that
$\mathcal{E}=\bm{\mathcal{H}}^{*}_{{\tt dCBV}}$. ∎