* if $D$ ends by any rule of the form

$$ \frac{\{\Delta \vdash?? : e_i \to??\}_i \quad \text{other conditions}}{\Delta \vdash?? : \beta \to??} $$

where $\beta \vdash e_i$ (this includes the rules for $\oplus_a^i$, $\lambda$ and application), then from the induction hypothesis $e_i \vdash c$ holds, where $i$ is the index of the derivation where $c$ occurs, and we can thus conclude $\beta \vdash c$.

* if $D$ ends by a $\vee\mu$-pattern as in Eq. (1), then by the induction hypothesis $\beta \wedge d_{ij} \vdash c$, where $i$ and $j$ are chosen so that $c$ occurs in the associated sub-derivation. Since $\mathrm{FN}(d_{ij}) \cap \mathrm{FN}(c) = \emptyset$ and the $d_{ij}$ are all satisfiable, we can conclude $\beta \vdash c$ by Lemma D.5. $\square$

**Remark 3.** It is not difficult to see that the property of Lemma D.11 fails for non-canonical derivations. For example, consider the non-canonical derivation below:

$$ \frac{\frac{x : C^q \sigma \vdash^{(a,b)} x : x_a^1 \to C^q \sigma \qquad \mu(x_b^0) \ge \frac{1}{2} \quad (\mu)}{x : C^q \sigma \vdash^{(a,b)} x \oplus_b^0 x : x_b^0 \wedge x_a^1 \to C^q \sigma} \qquad \frac{x : C^q \sigma \vdash^{(a,b)} x : \neg x_a^1 \to C^q \sigma \qquad \mu(\neg x_b^0) \ge \frac{1}{2} \quad (\mu)}{x : C^q \sigma \vdash^{(a,b)} x \oplus_b^0 x : \neg x_a^1 \to C^q \sigma} \qquad \frac{x : C^q \sigma \vdash^{(a,b)} v_b, x \oplus_b^0 x : x_a^1 \to C^q \sigma}{x : C^q \sigma \vdash^{(a)} v_b, x \oplus_b^0 x : \tau \to C^q \sigma} \qquad \mu(x_b^0) \ge \frac{1}{2} \quad (\mu)}{\tau \vdash x_a^i \wedge \neg x_a^1} \quad (\vee) $$

where $d = (x_b^0 \wedge x_a^1) \vee (\neg x_b^0 \wedge \neg x_a^1)$. While the literal $x_a^1$ occurs in an axiom, it is not true that $\tau \vdash x_a^1$.

Observe that the derivation above is pseudo-canonical. Instead, the derivation below is neither canonical nor pseudo-canonical, and similarly violates the property of Lemma D.11.

$$ \frac{\frac{x : C^q \sigma \vdash^{(a,b)} x : x_a^1 \to C^q \sigma \qquad \mu(x_b^0) \ge \frac{1}{2} \quad (\mu)}{x : C^q \sigma \vdash^{(a,b)} x \oplus_b^0 x : x_b^0 \wedge x_a^1 \to C^q \sigma} \qquad \frac{x : C^q \sigma \vdash^{(a,b)} x : \neg x_a^1 \to C^q \sigma \qquad \mu(x_b^0) \ge \frac{1}{2} \quad (\mu)}{x : C^q \sigma \vdash^{(a,b)} x \oplus_b^0 x : x_b^0 \wedge \neg x_a^1 \to C^q \sigma} \qquad \frac{x : C^q \sigma \vdash^{(a)} v_b, x \oplus_b^0 x : \tau \to C^q \sigma}{x : C^q \sigma \vdash^{(a)} v_b, x \oplus_b^0 x : \tau \to C^q \sigma} \qquad \mu(x_b^0) \ge \frac{1}{2} \quad (\mu)}{\tau \vdash x_a^i \wedge \neg x_a^1} \quad (\vee) $$

The following is the fundamental structural result we need to establish subject $\beta$-expansion.

**Theorem D.12.** Any typing derivation can be transformed into a pseudo-canonical derivation.

We need two preliminary lemmas.

**Lemma D.13.** Suppose $D$ is pseudo-canonical and ends as follows:

$$ \frac{\frac{\{\Gamma \vdash^{X \cup \{a\}} t : \beta_i \wedge e_i \to s\}_{i=1,\dots,n}}{\Gamma \vdash^{X \cup \{a\}} t : \beta \to s}}{\beta \vdash^{X \cup \{a\}} \bigvee_i \beta_i \wedge e_i} \quad (\vee) $$

where $\mathrm{FN}(\beta_i) \subseteq X$ and $\mathrm{FN}(e_i) \subseteq \{a\}$. Then there exists literals $c_{ij}$ with free names in $X$ such that

(i) if $i \neq i'$, then for all $j, j'$ either $c_{ij} \equiv c_{i'j'}$ or $c_{ij} \wedge c_{i'j'} \vdash \bot$;

(ii) $\beta_i \equiv \bigvee_j c_{ij}$, and more generally $\bigvee_{i,j} c_{ij} \equiv \bigvee_{i=1}^n \beta_i$.

Moreover, $D$ can be turned into a pseudo-canonical derivation $D'$ ending as follows:

$$ \frac{\frac{\{\Gamma \vdash^{X \cup \{a\}} t : c_{ij} \wedge e_i \to s\}_{i,j}}{\Gamma \vdash^{X \cup \{a\}} t : \beta \to s}}{\beta \vdash^{X \cup \{a\}} \bigvee_{i,j} c_{ij} \wedge e_i} \quad (\vee) $$

*Proof.* For any of the conjunction of literals $\beta_i$, let $W_i \subseteq \mathbb{N} \times \mathbb{N}$ contain all pairs $(j, b)$ such that at least one of the literals $x_b^j, \neg x_b^j$ occurs in $\bigvee_i \beta_i$ but neither of them occurs in $\beta_i$. For any such $\beta_i$, let $c_{i1}, \dots, c_{i2^#w_i}$ be the conjunctions of literals obtained by adding to $\beta_i$ all possible consistent conjunctions of literals chosen from $W_i$ (i.e. all possible choices between $x_b^j$ and $\neg x_b^j$, for $(j, b) \in W_i$). It is clear that $\beta_i \equiv \bigvee_j c_{ij}$ and that all $c_{ij}$ are disjoint, so ii. holds.

Moreover, let $i \neq i'$ and suppose $c_{ij} = \beta_i \wedge d$ and $c_{i'j'} = \beta_j \wedge e$ are not equivalent; since $c_{ij}$ and $c_{i'j'}$ are conjunctions of literals, and each of them contains either $x_b^j$ or $\neg x_b^j$ for $(j, b) \in \bigcup_i W_i$, the only possibility is that for some pair $(j, b)$, $c_{ij}$ contains either $x_b^j$ or $\neg x_b^j$ and $c_{i'j'}$ contains its negation, so $c_{ij} \wedge c_{i'j'} \vdash \bot$. Hence $i$ also holds.

Finally, the pseudo-canonical derivation $D'$ is obtained as follows: for any canonical sub-derivation $D_i$ of $D$ of conclusion $\Gamma \vdash^X t : \beta_i \wedge e_i \to s$ (whose conclusion contains the Boolean formula $\beta_i$) and for each choice of $j$, define a sub-derivation $D_{ij}$ of conclusion $\Gamma \vdash^X t : c_{ij} \wedge e_i \to s$ by replacing each Boolean formula $f$ occurring in $D_i$ by $f \wedge d$, where $c_{ij} = \beta_i \wedge d$. Since $d$ is a conjunction of literals, one can check by induction on $D_i$ that $D_{ij}$ is also canonical. This is immediate for all rules
except for the (∨)-rule. However, since $D_i$ is canonical, (∨)-rules occur in $D_i$ only in $\forall\mu$-patterns, and one can check that one obtains then a $\forall\mu$-pattern by replacing each Boolean formula $\alpha$ by $\alpha \wedge d$.

We finally obtain $D'$ as follows:

$$ \frac{\left\{ \Gamma \vdash^{X \cup \{a\}} t : c_{ij} \wedge e_i \to s \right\}_{i,j} \qquad b \models \bigvee_{i,j} c_{ij} \wedge e_i}{\Gamma \vdash^{X \cup \{a\}} t : b \to s} \qquad (\forall) $$

□

**Lemma D.14.** If $D$ is a derivation ending with a rule whose premises are conclusions of pseudo-canonical derivations, then $D$ can be turned into a pseudo-canonical derivation $D'$.

*Proof.* We consider all possible rules:

* if $D$ is as follows:

$$ \frac{\left\{ \Gamma \vdash^{X \cup \{a\}} t : c_j \to s \right\}_j \qquad b \models \bigvee_i c_j}{\Gamma \vdash^{X \cup \{a\}} t : b \to s \qquad (\oplus l)} \qquad (\forall) $$

then $D'$ is as follows:

$$ \frac{\left\{ \begin{array}{l} D_j \\ \Gamma \vdash^{X \cup \{a\}} t : c_j \to s \\ \Gamma \vdash^{X \cup \{a\}} t : \bigoplus_a^i u : x_a^i \wedge b \to s \end{array} \right\}_j \qquad x_a^i \wedge b \models \bigvee_j x_a^i \wedge c_j}{\Gamma \vdash^{X \cup \{a\}} t : \bigoplus_a^i u : x_a^i \wedge b \to s} \qquad (\forall) $$

The symmetric rule for $\bigoplus_a^i$ is treated similarly.

* If $D$ is as follows:

$$ \frac{\left\{ \begin{array}{l} D_j \\ \Gamma, x : \mathfrak{M} \vdash^X t : c_j \to C^q \sigma \end{array} \right\}_j \qquad b \models \bigvee_j c_j}{\frac{\Gamma, x : \mathfrak{M} \vdash^X t : b \to C^q \sigma}{\Gamma \vdash^X \lambda x.t : b \to C^q (\mathfrak{M} \Rightarrow \sigma)}} \qquad (\forall) \qquad (\lambda) $$

then $D'$ is as follows:

$$ \frac{\left\{ \begin{array}{l} D_j \\ \Gamma, x : \mathfrak{M} \vdash^X t : c_j \to C^q \sigma \\ \Gamma \vdash^X \lambda x.t : c_j \to C^q (\mathfrak{M} \Rightarrow \sigma) \end{array} \right\}_j \qquad b \models \bigvee_j c_j}{\Gamma \vdash^X \lambda x.t : b \to C^q (\mathfrak{M} \Rightarrow \sigma)} \qquad (\forall) $$

* if $D$ is as follows:

$$ \frac{\left\{ \begin{array}{l} D_j \\ \Gamma \vdash^X t : c_j \to C^q (\mathfrak{M} \Rightarrow \sigma) \end{array} \right\}_j \qquad c \models \bigvee_j c_j}{\Gamma \vdash^X t : c \to C^q (\mathfrak{M} \Rightarrow \sigma)} \qquad (\forall) \qquad \left\{ \begin{array}{l} E_l \\ \Gamma \vdash^X u : d_l \to s_l \end{array} \right\}_l \qquad b \models c \wedge (\wedge_l d_l) \qquad (@_n) $$

where $\mathfrak{M} = [s_1, \dots, s_n]$ and each derivation $E_l$ is of the form

$$ \frac{\left\{ \begin{array}{l} E_{lk} \\ \Gamma \vdash^X t : e_{lk} \to s_l \end{array} \right\}_k \qquad d_l \models \bigvee_k e_{lk}}{\Gamma \vdash^X t : d_l \to s_l} \qquad (\forall) $$

Then $D'$ is as follows:
$$ \frac{\left\{ \begin{array}{c} D_j \\ \Gamma \vdash^X t : \mathfrak{c}_j \to \mathsf{C}^q(\mathfrak{R} \Rightarrow \sigma) \\ \Gamma \vdash^X u : \mathfrak{e}_{lg(l)} \to \mathfrak{s}_l \end{array} \right\} \mathfrak{b}_{jg} \models \mathfrak{c}_j \wedge (\bigwedge_l \mathfrak{e}_{lg(l)}) \\ \left. \begin{array}{c} (@\cap) \\ \Gamma \vdash^X tu : \mathfrak{b}_{jg} \to \mathsf{C}^q\sigma \end{array} \right\} \mathfrak{b} \models \bigvee_{j,g} \mathfrak{b}_{jg} \qquad (\vee) $$

where $\mathfrak{b}_{jg} = \mathfrak{c}_j \wedge (\bigwedge_l \mathfrak{e}_{lg(l)})$ and $g$ ranges over all possible choice functions associating each $l$ with a suitable value $k$ such that $\mathfrak{e}_{lk}$ exists, using the fact that

$$ \mathfrak{b} \models \mathfrak{c} \wedge (\bigwedge_l d_l) \equiv (\bigvee_j \mathfrak{c}_j) \wedge (\bigwedge_l \bigvee_k \mathfrak{e}_{lk}) \equiv \bigvee_j (\mathfrak{c}_j \wedge (\bigwedge_l \bigvee_k \mathfrak{e}_{lk})) \equiv \bigvee_{jg} \mathfrak{c}_j \wedge (\bigwedge_l \mathfrak{e}_{lg(l)}) $$

• if D is as follows:

$$ \frac{\left\{ \begin{array}{c} D_{ij} \\ \Gamma \vdash^{X \cup \{a\}} t : d_{ij} \to \mathsf{C}^{q_i} \sigma \end{array} \right\}_j \quad \mathfrak{b}' \wedge \mathfrak{c}_i \models \bigvee_j d_{ij} \\ \left. \begin{array}{c} (\vee) \\ \Gamma \vdash^{X \cup \{a\}} t : \mathfrak{b}' \wedge \mathfrak{c}_i \to \mathsf{C}^{q_i} \sigma \end{array} \right\}_i \quad \mu(\mathfrak{c}_i) \geq s_i \quad \mathfrak{b} \models \mathfrak{b}' \\ \Gamma \vdash^X \mathrm{va.t} : \mathfrak{b} \to \mathsf{C}^{\Sigma_i q_i s_i} \sigma \qquad (\mu) $$

where $\mathrm{FN}(\mathfrak{b}, \mathfrak{b}') \subseteq X$ and $\mathrm{FN}(\mathfrak{c}_i) \subseteq \{a\}$, then, since the $D_{ij}$ are canonical, each $d_{ij}$ is a conjunction of literals and can thus be written as $\mathfrak{e}_{ij} \wedge \mathfrak{f}_{ij}$, where $\mathrm{FN}(\mathfrak{e}_{ij}) \subseteq X$ and $\mathrm{FN}(\mathfrak{f}_{ij}) \subseteq \{a\}$.

Observe that we can suppose w.l.o.g. that none of either the $\mathfrak{e}_{ij}$ or the $\mathfrak{f}_{ij}$ is equivalent to $\perp$. Moreover, we can also suppose w.l.o.g. that $\mathfrak{b}$ and $\mathfrak{b}'$ coincide and are satisfiable.

Now, from $\mathfrak{b} \wedge \mathfrak{c}_i \models \bigvee_j \mathfrak{e}_{ij} \wedge \mathfrak{f}_{ij}$ (using the fact that the $\mathfrak{c}_i$ are satisfiable) we deduce by Lemma D.5 that $\mathfrak{b} \models \bigvee_j \mathfrak{e}_{ij}$ and $\mathfrak{c}_i \models \bigvee_j \mathfrak{f}_{ij}$.

For each $i$, by applying Lemma D.13 to the family $(\mathfrak{e}_{ij})_j$, we obtain a family $\mathfrak{e}_{ijk}$ of conjunctions of literals, all satisfiable, with $\mathrm{FN}(\mathfrak{e}_{ijk}) \subseteq X$, and such that $\mathfrak{e}_{ij} \equiv \bigvee_k \mathfrak{e}_{ijk}$, and for $j \neq j'$, either $\mathfrak{e}_{ijk} \equiv \mathfrak{e}_{ij'k'}$ or $\mathfrak{e}_{ijk} \wedge \mathfrak{e}_{ij'k'} \models \perp$. Moreover, we also deduce the existence of a family $D_{ijk}^{\dagger}$ of canonical derivations of conclusion $\Gamma \vdash^{X \cup \{a\}} t : \mathfrak{e}_{ijk} \wedge \mathfrak{f}_{ij} \to s$.

For each $i, j, k$, let $U_{jk}^i$ be the set of pairs $(j', k')$ such that $\mathfrak{e}_{ij'k'} \equiv \mathfrak{e}_{ijk}$. Observe that for any pair $(j'', k'') \notin U_{jk}^i$, $\mathfrak{e}_{ijk} \wedge \mathfrak{e}_{ij'k''} \models \perp$.

Let $\approx^i$ be the equivalence relation on pairs $(j, k)$ defined by $(j, k) \approx^i (j', k')$ iff $\mathfrak{e}_{ijk} \equiv \mathfrak{e}_{ij'k'}$ (i.e. iff $(j', k') \in U_{jk}^i$), and let $W^i$ contain a chosen representative of $[(j, k)]_{\approx^i}$ for each equivalence class. Then we have that

$$ \bigvee_j \mathfrak{e}_{ij} \wedge \mathfrak{f}_{ij} \equiv \bigvee_{jk} \mathfrak{e}_{ijk} \wedge \mathfrak{f}_{ij} \equiv \bigvee_{(j,k) \in W^i} \mathfrak{e}_{ijk} \wedge \left( \bigvee_{j'k' \in U_{jk}^i} \mathfrak{f}_{ij'} \right) \qquad (2) $$

Let $\tilde{\mathfrak{f}}_{ijk} = \bigvee_{j'k' \in U_{jk}^i} \mathfrak{f}_{ij'}$. Let $\mathfrak{b} \equiv \bigvee_u \mathfrak{b}_u$, where the $\mathfrak{b}_u$ are pairwise disjoint conjunctions of literals, all being satisfiable. From $\mathfrak{b} \wedge \mathfrak{c}_i \models \bigvee_j d_{ij} \equiv \bigvee_{(j,k) \in W^i} \mathfrak{e}_{ijk} \wedge \tilde{\mathfrak{f}}_{ijk}$ we deduce by Lemma D.5 and the satisfiability of $\mathfrak{c}_i$ that $\mathfrak{b} \models \bigvee_{(j,k) \in W^i} \mathfrak{e}_{ijk}$; since the $\mathfrak{e}_{ijk}$, with $(j, k)$ varying in $W^i$, are pairwise disjoint, this implies the existence of functions $J, K$ such that $\mathfrak{b}_u \models \mathfrak{e}_{iJ(u)K(u)}$, and thus a fortiori such that $\mathfrak{b}_u \wedge \mathfrak{c}_i \models \mathfrak{e}_{iJ(u)K(u)} \wedge \tilde{\mathfrak{f}}_{iJ(u)K(u)}$. Since the $\mathfrak{b}_u$ are satisfiable, by Lemma D.5, this implies $\mathfrak{c}_i \models \tilde{\mathfrak{f}}_{iJ(u)K(u)}$.

For each $u$, we can now construct a derivation $D_u^*$ of $\Gamma \vdash^X \mathrm{va.t} : \mathfrak{e}_{iJ(u)K(u)} \to \mathsf{C}^{\Sigma_i q_i s_i} \sigma$ as shown below:

$$ \frac{\left\{ \begin{array}{c} D_{ij'k'}^{\ddagger} \\ \Gamma \vdash^{X \cup \{a\}} t : \mathfrak{b}_u \wedge \mathfrak{f}_{ij'} \to \mathsf{C}^{q_i} \sigma \\ \Gamma \vdash^{X \cup \{a\}} t : \mathfrak{b}_u \wedge \mathfrak{c}_i \to \mathsf{C}^{q_i} \sigma \end{array} \right\}_i \quad \mathfrak{b}_u \wedge \mathfrak{c}_i \models \bigvee_{j'k' \in U_{(u)K(u)}} \mathfrak{b}_{j'k'} \wedge \mathfrak{b}_u \wedge \mathfrak{f}_{ij'} \\ \Gamma \vdash^X \mathrm{va.t} : \mathfrak{b}_u \to \mathsf{C}^{\Sigma_i q_i s_i} \sigma \qquad (\mu) $$

where $D_{ij'k'}^{\ddagger}$ is obtained from $D_{ij'k'}$ by replacing everywhere $\mathfrak{e}_{ij'k'}$ by $\mathfrak{b}_u$, using the fact that $\mathfrak{b}_u \models \mathfrak{e}_{iJ(u)K(u)} \equiv \mathfrak{e}_{ij'k'}$. Observe that the one above is a $\bigvee\mu$-pattern, and thus $D_u^*$ is canonical.

We can now conclude as follows:

$$ \frac{\left\{ \begin{array}{c} D_u^* \\ \Gamma \vdash^X \mathrm{va.t} : \mathfrak{b}_u \to \mathsf{C}^{\Sigma_i q_i s_i} \sigma \end{array} \right\}_u \quad \mathfrak{b} \models \bigvee_u \mathfrak{b}_u \\ \Gamma \vdash^X \mathrm{va.t} : \mathfrak{b} \to \mathsf{C}^{\Sigma_i q_i s_i} \sigma \qquad (\vee) $$
☐

We can now prove Theorem D.12.

*Proof of Theorem D.12.* First, for any axiom

$$ \frac{\mathfrak{s}_i \le t \quad \mathrm{FN}(\mathfrak{b}) \subseteq X}{\Gamma, x : [\mathfrak{s}_1, \dots, \mathfrak{s}_n] \vdash^X x : \mathfrak{b} \to t} \quad (\mathrm{id}_\le) $$

transform $\mathfrak{b}$ into an equivalent disjunctive normal form $\bigvee_j \mathfrak{b}_j$ (with the $\mathfrak{b}_j$ conjunctions of literals), and replace the axiom by the derivation below

$$ \frac{\left\{ \frac{\mathfrak{s}_i \le t \quad \mathrm{FN}(\mathfrak{b}) \subseteq X}{\Gamma, x : [\mathfrak{s}_1, \dots, \mathfrak{s}_n] \vdash^X x : \mathfrak{b} \to t} \right\}_j \quad \mathfrak{b} \models^X \bigvee_j \mathfrak{b}_j}{\Gamma, x : [\mathfrak{s}_1, \dots, \mathfrak{s}_n] \vdash^X x : \mathfrak{b} \to t} \quad (\forall) $$

Now, starting from the axioms, for each rule occurring in the construction of the derivation, use Lemma D.14 to progressively permute $(\forall)$-rules downwards, hence turning the derivation into a pseudo-canonical one. ☐

Using Theorem D.12 we can finally prove the subject $\beta$-expansion property. We will make use of the following property (which is an easy consequence of Lemma D.6 and Lemma D.3):

**Lemma D.15.** If $\Gamma, \Delta \vdash^{XUY} t : \mathfrak{b} \to s$ is derivable, where $FV(t) \subseteq \Gamma$ and $FN(t) \subseteq X$, then there exists a Boolean formula $\mathfrak{b}'$ with $FN(\mathfrak{b}') \subseteq X$ such that $\mathfrak{b} \models \mathfrak{b}'$ and $\Gamma \vdash^X t : \mathfrak{b}' \to s$ is derivable.

**Proposition D.16** (subject $\beta$-expansion). If $\Gamma \vdash^X t[u/x] : \mathfrak{b} \to s$ is derivable then $\Gamma \vdash^X (\lambda x.t)u : \mathfrak{b} \to s$ is also derivable.

*Proof.* A typing derivation of $\Gamma \vdash^X t[u/x] : \mathfrak{b} \to s$ can be depicted as follows:

$$ \begin{array}{c} D_1 \\ \Gamma, \Delta_1 \vdash^{X \cup Y_1} u : \ell_1 \to \mathfrak{s}_1 \\ \multicolumn{2}{c}{\vdots} \\ D \\ \Gamma \vdash^X t[u/x] : \mathfrak{b} \to s \end{array} \quad \begin{array}{c} D_N \\ \Gamma, \Delta_N \vdash^{X \cup Y_N} u : \ell_N \to \mathfrak{s}_N \end{array} $$

Observe that neither the variables in $\Delta_i$ nor the names in $Y_i$ can occur in $u$. Hence using Lemma D.15 we obtain derivations $D_i^*$ of $\Gamma \vdash^X u : d_i \to \mathfrak{s}_i$, with $\ell_i \models d_i$.

Moreover, from $D$ we can deduce a derivation $D^*$ of $\Gamma, x : [\mathfrak{s}_1, \dots, \mathfrak{s}_N] \vdash^X t : \mathfrak{b}' \to s$, where each of the $D_i$ is replaced by an axiom

$$ \frac{\frac{\mathfrak{s}_i \le \mathfrak{s}_i \quad \mathrm{FN}(d_i) \subseteq X}{\Gamma, \Delta_i, x : [\mathfrak{s}_1, \dots, \mathfrak{s}_N] \vdash^X x : d_i \to \mathfrak{s}_i} \quad (\mathrm{id}_\le)}{\mathfrak{b}' \models \bigvee_i c_i} $$

and $\mathfrak{b}'$ is such that $\mathfrak{b} \models \mathfrak{b}'$.

Using Theorem D.12 we can turn $D^*$ into a pseudo-canonical derivation $D^{*\dagger}$, which is thus of the form

$$ D^{*\dagger} = \frac{\left\{ \frac{E_l}{\Gamma, x : [\mathfrak{s}_1, \dots, \mathfrak{s}_N] \vdash^X t : c_l \to s} \right\}_l \quad \mathfrak{b}' \models \bigvee_l c_l}{\Gamma, x : [\mathfrak{s}_1, \dots, \mathfrak{s}_N] \vdash^X t : \mathfrak{b}' \to s} \quad (\forall) $$

where each $E_l$ is canonical and contains all axioms of the form

$$ \frac{\frac{\mathfrak{s}_i \le \mathfrak{s}_i \quad \mathrm{FN}(d_{ig_l(i)}) \subseteq X}{\Gamma, \Delta_i, x : [\mathfrak{s}_1, \dots, \mathfrak{s}_N] \vdash^X x : d_{ig_l(i)} \to \mathfrak{s}_i} \quad (\mathrm{id}_\le)}{\mathfrak{b}' \models \bigvee_l c_l} $$

where $\bigvee_k d_{ik} \equiv d_i$ is a disjunctive normal form and $g_l$ is some choice function choosing one value $k$ for each $i$.

Since $d_{ik} \models \bigvee_k d_{ik} \equiv d_i$ holds we deduce by Lemma C.3 the existence of derivations $D_{ik}$ of $\Gamma \vdash^X u : d_{ik} \to \mathfrak{s}_i$.

Moreover, since the $E_l$ are canonical, by Lemma D.11 we deduce that $c_l \models \bigwedge_i d_{ig_l(i)}$.

Using $\mathfrak{b} \models \mathfrak{b}'$ and $\mathfrak{b}' \models \bigvee_l c_l$, we can thus obtain a derivation of $\Gamma \vdash^X (\lambda x.t)u : \mathfrak{b}' \to s$ as follows (where $\mathfrak{M} = [\mathfrak{s}_1, \dots, \mathfrak{s}_N]$ and $s = C^q\sigma$):
$$
\frac{
  \left(
    \begin{array}{@{}l@{}}
      E_l \\
      \Gamma, x : \mathfrak{M} \vdash^X t : c_l \to s \\
      \Gamma \vdash^X \lambda x.t : c_l \to C^q(\mathfrak{M} \Rightarrow \sigma)
    \end{array}
  \right)
  \quad
  \left\{
    \begin{array}{@{}l@{}}
      D_{ig_l(i)} \\
      \Gamma \vdash^X u : d_{ig_l(i)} \to s_i
    \end{array}
  \right\}_i
  \quad
c_l \vdash \bigwedge_i d_{ig_l(i)}
}
{
  \Gamma \vdash^X (\lambda x.t) u : c_l \to s
}
\quad
l
\quad
\begin{array}{@{}l@{}}
  \beta \vdash \bigvee_l c_l \\
  \Gamma \vdash^X (\lambda x.t) u : \beta \to s
\end{array}
\qquad (\lor)
$$

□

**D.2.2 Subject Permutative Expansion.** The subject expansion property with respect to permutative reduction can be established by a direct inspection of permutative rules.

**Proposition D.17.** If $\Gamma \vdash^X t : \beta \to s$ and $u \to_p t$, then $\Gamma \vdash^X u : \beta \to s$.

*Proof.* As in the proof of Proposition C.1, if the typing derivation *D* of *t* ends by a (∨)-rule, it suffices to establish the property for the immediate sub-derivations of *D* and then apply an instance of (∨)-rule to the resulting derivations. So we will always suppose that the typing derivation of *t* does not end by a (∨)-rule.

($t \oplus_a^i t \to_p t$) From $\Gamma \vdash^{X \cup \{a\}} t : \beta \to s$ we deduce

$$
\frac{
  \frac{
    \frac{
      \Gamma \vdash^{X \cup \{a\}} t : \beta \to s
    }{
      \Gamma \vdash^{X \cup \{a\}} t \oplus_a^i t : x_a^i \wedge \beta \to s
    }
  \quad
  (\oplus l)
}
{
  \Gamma \vdash^{X \cup \{a\}} t \oplus_a^i t : \neg x_a^i \wedge \beta \to s
}
\quad
(\oplus r)
}
{
  \beta \vdash (x_a^i \wedge \beta) \lor (\neg x_a^i \wedge \beta)
}
\quad
(\lor)
$$

($((t \oplus_a^i u) \oplus_a^i v \to_p t \oplus_a^i v)$) There are two possible sub-cases:

1. the type derivation is as follows:

$$
\frac{
  \frac{
    \Gamma \vdash^{X \cup \{a\}} t : \beta' \to s \qquad \beta' \vdash x_a^i \wedge \beta'
  }{
    \Gamma \vdash^{X \cup \{a\}} t \oplus_a^i v : \beta \to s
  }
  (\oplus l)
}
{
  \Gamma \vdash^{X \cup \{a\}} t \oplus_a^i v : \beta' \to s
}
$$

Then we deduce

$$
\frac{
  \frac{
    \frac{
      \Gamma \vdash^{X \cup \{a\}} t : \beta' \to s \qquad \beta' \vdash x_a^i \wedge \beta'
    }{
      \Gamma \vdash^{X \cup \{a\}} t \oplus_a^i u : \beta \to s
    }
  \quad
  (\oplus l)
}
{
  \Gamma \vdash^{X \cup \{a\}} (t \oplus_a^i u) \oplus_a^i v : \beta \to s
}
\quad
(\oplus l)
$$

2. the type derivation is as follows:

$$
\frac{
  \frac{
    \Gamma \vdash^{X \cup \{a\}} v : \beta' \to s \qquad \beta' \vdash \neg x_a^i \wedge \beta'
  }{
    \Gamma \vdash^{X \cup \{a\}} t \oplus_a^i v : \beta \to s
  }
  (\oplus l)
}
{
  \Gamma \vdash^{X \cup \{a\}} v : \beta' \to s
}
$$

Then we deduce

$$
\frac{
  \frac{
    \Gamma \vdash^{X \cup \{a\}} v : \beta' \to s \qquad \beta' \vdash \neg x_a^i \wedge \beta'
  }{
    \Gamma \vdash^{X \cup \{a\}} (t \oplus_a^i u) \oplus_a^i v : \beta \to s
  }
  (\oplus l)
}
{
  \Gamma \vdash^{X \cup \{a\}} v : \beta' \to s
}
$$

($t \oplus_a^i (u \oplus_a^i v) \to_p t \oplus_a^i v$) Similar to the case above.

($\lambda x.(t \oplus_a^i u) \to_p (\lambda x.t) \oplus_a^i (\lambda x.u)$) There are two possible sub-cases, treated similarly. We only consider the first one:

1.

$$
\frac{
  \frac{
    \Gamma, x : \mathfrak{M} \vdash^X t : \beta' \to C^q \sigma
  }{
    \Gamma \vdash^X \lambda x.t : \beta' \to C^q(\mathfrak{M} \Rightarrow \sigma)
  }
  (\lambda)
  \quad
  \begin{array}{@{}l@{}}
    \beta' \vdash x_a^i \wedge \beta'
  \end{array}
}{
  \Gamma \vdash^X (\lambda x.t) \oplus_a^i (\lambda x.u) : \beta \to C^q(\mathfrak{M} \Rightarrow \sigma)
}
(\oplus l)
$$

Then we deduce

$$
\frac{
  \frac{
    \Gamma, x : \mathfrak{M} \vdash^X t : \beta' \to C^q \sigma \qquad \beta' \vdash x_a^i \wedge \beta'
  }{
    \Gamma, x : \mathfrak{M} \vdash^X t \oplus_a^i u : \beta \to C^q \sigma
  }
  (\oplus l)
}{
  \Gamma \vdash^X \lambda x.(t \oplus_a^i u) : \beta \to C^q(\mathfrak{M} \Rightarrow \sigma)
}
(\lambda)
$$

($((t \oplus_a^i u)v \to_p (tv) \oplus_a^i (uv))$) There are two possible sub-cases, treated similarly. We only consider the first one (with $\mathfrak{M} = [\mathfrak{s}_1, \dots, \mathfrak{s}_n]$:
1.

$$ \frac{\Gamma \vdash^X t : \mathfrak{b}'' \to C^q(\mathfrak{M} \Rightarrow \sigma) \quad \{\Gamma \vdash^X v : c_i \to s_i\}_i \quad \mathfrak{b}' \models \mathfrak{b}'' \wedge (\bigwedge_i c_i) \quad (@_\cap)}{\Gamma \vdash^X tv : \mathfrak{b}' \to C^q\sigma} \quad \mathfrak{b} \models x_a^i \wedge \mathfrak{b}' \quad (\oplus l) $$

Then we deduce

$$ \frac{\Gamma \vdash^X t : \mathfrak{b}'' \to C^q(\mathfrak{M} \Rightarrow \sigma) \quad x_a^i \wedge \mathfrak{b}'' \models x_a^i \wedge \mathfrak{b}'' \quad (\oplus l)}{\Gamma \vdash^X t \oplus_a^i u : x_a^i \wedge \mathfrak{b}'' \to C^q(\mathfrak{M} \Rightarrow \sigma) \quad \{\Gamma \vdash^X v : c_i \to s_i\}_i \quad \mathfrak{b}' \models (x_a^i \wedge \mathfrak{b}'' ) \wedge (\bigwedge_i c_i) \quad (@_\cap)} \quad \Gamma \vdash^X (t \oplus_a^i u)v : \mathfrak{b}' \to C^q\sigma $$

$(t(u \oplus_a^i v) \to_p (tu) \oplus_a^i (tv))$ There are two sub-cases, treated similarly. We only consider the first one:

1.

$$ \frac{\Gamma \vdash^X t : \mathfrak{b}'' \to C^q(\mathfrak{M} \Rightarrow \sigma) \quad \{\Gamma \vdash^X u : c_i \to s_i\}_i \quad \mathfrak{b}' \models \mathfrak{b}'' \wedge (\bigwedge_i c_i) \quad (@_\cap)}{\Gamma \vdash^X tu : \mathfrak{b}' \to C^q\sigma} \quad \mathfrak{b} \models x_a^i \wedge \mathfrak{b}' \quad (\oplus l) $$

Then we deduce that

$$ \frac{\Gamma \vdash^X t : \mathfrak{b}'' \to C^q(\mathfrak{M} \Rightarrow \sigma) \quad \left\{ \frac{\Gamma \vdash^X u : c_i \to s_i \quad x_a^i \wedge c_i \models x_a^i \wedge c_i}{\Gamma \vdash^X u \oplus_a^i v : x_a^i \wedge c_i \to s_i} \quad (\oplus l) \right\}_i \quad \mathfrak{b} \models \mathfrak{b}'' \wedge (\bigwedge_i (x_a^i \wedge c_i)) \quad (@_\cap)}{\Gamma \vdash^X t(u \oplus_a^i v) : \mathfrak{b}' \to C^q\sigma} $$

(((t \oplus_a^i u) \oplus_b^j v \to_p (t \oplus_b^j v) \oplus_a^i (u \oplus_b^j v)) We suppose here $a \neq b$ or $i < j$. There are four sub-cases, all treated similarly. We only consider the first one:

1.

$$ \frac{\Gamma \vdash^X t : \mathfrak{b}'' \to s \quad \mathfrak{b}' \models x_b^j \wedge \mathfrak{b}''}{\Gamma \vdash^X t \oplus_b^j v : \mathfrak{b}' \to s \quad \mathfrak{b} \models x_a^i \wedge \mathfrak{b}'} \quad (\oplus l) $$

Then we deduce

$$ \frac{\Gamma \vdash^X t : \mathfrak{b}'' \to s \quad \mathfrak{b} \models x_a^i \wedge \mathfrak{b}''}{\Gamma \vdash^X t \oplus_a^i u : \mathfrak{b}' \to s \quad \mathfrak{b} \models x_b^j \wedge \mathfrak{b}'} \quad (\oplus l) $$

$(t \oplus_b^j (u \oplus_a^i v) \to_p (t \oplus_b^j u) \oplus_a^i (t \oplus_b^j v))$ Similar to the case above.

$(vb.(t \oplus_a^i u) \to_p (vb.t) \oplus_a^i (vb.u))$ We suppose $a \neq b$. There are two sub-cases, treated similarly. We only consider the first one:

1.

$$ \frac{\{\Gamma \vdash^{X \cup \{a,b\}} t : \mathfrak{b}'' \wedge c_i \to C^{q_i} \sigma\}_i \quad \mu(c_i) \geq s_i \quad \mathfrak{b}' \models \mathfrak{b}''}{\Gamma \vdash^{X \cup \{a\}} vb.t : \mathfrak{b}' \to C^{\Sigma_i q_i s_i} \sigma} \quad (\mu_{\Sigma}) $$

From $\mathfrak{b} \models \mathfrak{b}''$ we deduce by Lemma C.3 the existence of derivations of $\Gamma \vdash^{X \cup \{a\}} t : \mathfrak{b} \wedge c_i \to C^{q_i} \sigma$. Then we can construct the following type derivation for $u$:

$$ \frac{\left\{ \frac{\Gamma \vdash^{X \cup \{a,b\}} t : \mathfrak{b} \wedge c_i \to C^{q_i} \sigma}{\Gamma \vdash^{X \cup \{a,b\}} t \oplus_a^i u : \mathfrak{b} \wedge c_i \to C^{q_i} \sigma} \right\}_i \quad \mu(c_i) \geq s_i}{\Gamma \vdash^{X \cup \{a\}} vb.t \oplus_a^i u : \mathfrak{b} \to C^{\Sigma_i q_i s_i} \sigma} \quad (\mu_{\Sigma}) $$

$(va.t \to_p t)$ We can suppose that $a \notin \text{FN}(\mathfrak{b})$, so from $\Gamma \vdash^X t : \mathfrak{b} \to s$ and $\mathfrak{b} \wedge \top \models \mathfrak{b}$ we deduce $\Gamma \vdash^{X \cup \{a\}} t : \mathfrak{b} \wedge \top \to s$ and since $\mu(\top) \geq 1$, $\Gamma \vdash^X va.t : \mathfrak{b} \to s$, since $s = C^q\sigma = C^{q-1}\sigma$.
$$ (\lambda x.v a.t \dashv_p v a.\lambda x.t) $$

$$ \frac{\left\{ \frac{\Gamma, x : \mathfrak{M} \vdash^{X \cup \{a\}} t : b' \wedge c_i \rightarrow C^{q_i} \sigma}{\Gamma \vdash^{X \cup \{a\}} \lambda x.t : b' \wedge c_i \rightarrow C^{q_i}(\mathfrak{M} \Rightarrow \sigma)} \right\}_i}{\Gamma \vdash^X v a.\lambda x.t : b \rightarrow C^{\Sigma_i q_i s_i}(\mathfrak{M} \Rightarrow \sigma)} (\mu_{\Sigma}) $$

from which we deduce

$$ \frac{\{\Gamma, x : \mathfrak{M} \vdash^{X \cup \{a\}} t : b' \wedge c_i \rightarrow C^{q_i} \sigma\}_i \quad \mu(c_i) \geq s_i \quad b \vdash b' \quad (\mu_{\Sigma})}{\frac{\Gamma, x : \mathfrak{M} \vdash^X v a.t : b \rightarrow C^{\Sigma_i q_i s_i} \sigma}{\Gamma \vdash^X \lambda x.v a.t : b \rightarrow C^{\Sigma_i q_i s_i}(\mathfrak{M} \Rightarrow \sigma)} (\lambda)} $$

((va.t)u \dashv_p v a.(tu)) We have

$$ \frac{\left\{ \frac{\Gamma \vdash^{X \cup \{a\}} t : c_i \rightarrow C^{q_i}(\mathfrak{M} \Rightarrow \sigma) \quad \{\Gamma \vdash^{X \cup \{a\}} u : d_{ij} \rightarrow t_{ij}\}_j \quad b' \wedge e_i \vdash c_i \wedge \bigwedge_j d_{ij}}{(\bigwedge_i)} \right\}_i}{\Gamma \vdash^{X \cup \{a\}} tu : b' \wedge e_i \rightarrow C^{q_i} \sigma} (\mu_{\Sigma}) $$

where $\mathfrak{M}_i = [t_{i1}, \dots, t_{ip_i}]$. Let $\mathfrak{M}$ be the concatenation of $\mathfrak{M}_1, \dots, \mathfrak{M}_{k+1}$. Since $\mathfrak{M} \le \mathfrak{M}_i$, we have $C^q(\mathfrak{M}_i \Rightarrow \sigma) \le C^q(\mathfrak{M} \Rightarrow \sigma)$, so from the derivations of $\Gamma \vdash^{X \cup \{a\}} t : c_i \rightarrow C^{q_i}(\mathfrak{M}_i \Rightarrow \sigma)$, using Lemma D.4 we deduce derivations of $\Gamma \vdash^{X \cup \{a\}} t : c_i \rightarrow C^q(\mathfrak{M} \Rightarrow \sigma)$. Moreover, from $b \wedge e_i \vdash c_i$, using Lemma D.3, we deduce the existence of derivations of $\Gamma \vdash^{X \cup \{a\}} t : b \wedge e_i \rightarrow C^q(\mathfrak{M} \Rightarrow \sigma)$, and from $b \wedge e_i \vdash \bigwedge_j d_{ij}$, since $\mathrm{FN}(e_i) \cap \mathrm{FN}(d_{ij}) = \emptyset$, we deduce $b \vdash \bigwedge_j d_{ij}$.
We can thus construct a type derivation for $(va.t)u$ as follows:

$$ \frac{\{\Gamma \vdash^{X \cup \{a\}} t : b \wedge e_i \rightarrow C^q(\mathfrak{M} \Rightarrow \sigma)\}_i \quad \mu(e_i) \geq s_i}{\Gamma \vdash^X v a.t : b \rightarrow C^{\Sigma_i q_i s_i}(\mathfrak{M} \Rightarrow \sigma)} (\mu_{\Sigma}) $$

Observe that this is the unique case in the proof in which we use intersection types in an essential way.

□

## D.3 Completeness.

### D.3.1 Deterministic Completeness. The goal of this subsection is to establish Proposition 6.5.

**Proposition 6.5 (Deterministic Completeness).** For any closed term $t$,

(i.) $t$ is head-normalizable iff $\vdash_{\neg\neg} t : \top \rightarrow C^1\mathfrak{h}$n;

(ii.) $t$ is normalizable iff $\vdash_{\neg\neg} t : \top \rightarrow C^1\mathfrak{n}$.

(iii.) $t$ is strongly normalizable iff $\vdash_{\neg\neg} t : \top \rightarrow C^1\mathfrak{n}$ and all types in the derivation are safe.

We need a few preliminary lemmas:

**Lemma D.18.** For any closed term $t$:

(i.) if $t$ is a HNV, then $\vdash_{\neg\neg} t : \top \rightarrow C^1\sigma$ holds for some type;

(ii.) if $t$ is a HNV and is $\dashv$-normal, then $\vdash_{\neg\neg} t : \top \rightarrow C^1\sigma$ holds for some safe type.

*Proof.* If $t = \lambda x_1 \dots x_n x_i u_1 \dots u_p$, then we can let $\sigma = s_1 \Rightarrow \dots \Rightarrow s_n \Rightarrow o$, where for $j \ne i$, $s_j = []$, and $s_i = C^1[C^1[] \Rightarrow \dots \Rightarrow C^1[] \Rightarrow o]$. The second claim is proved by induction on normal forms, using a similar construction. □

**Lemma D.19.** If $\Gamma \vdash_{\neg\neg} t[u/x] : b \rightarrow s$ is derivable without using $[]$, and $t$ contains at least one occurrence of $x$, then there exists $\mathfrak{M} \ne []$ such that $\Gamma, x : \mathfrak{M} \vdash_{\neg\neg} t : b \rightarrow s$ and $\Gamma \vdash_{\neg\neg} u : b \rightarrow \mathfrak{M}$ are derivable without using $[]$.

*Proof.* It suffices to look at the proof of Proposition D.16, and observe that (1) since $u$ occurs at least once in $t$, $\mathfrak{M}$ cannot be $[]$, and (2) since the original derivation has no occurrence of $(\vee)$, it must be canonical, and thus to construct the derivation of $\Gamma \vdash (\lambda x.t)u : b \rightarrow s$ we do not need to make use of any application of $(\vee)$. □

Using Lemma D.18 together with the subject expansion property we can prove this first half of Proposition 6.5. The second half comes from Corollary E.16.
**Proof of Proposition 6.5.** For (i.), if $t$ is head normalizable, with head-normal form $u$, then by Lemma B.8 the tree $RBT(t) = RBT(u)$ is finite and its leaves are HNV $u_1, \dots, u_N$. By Lemma D.18 we can deduce $\vdash u_i : \mathbf{T} \to \mathbb{C}^1\text{hn}$; we can then climb up $RBT(t)$ using the rules $(\oplus l)$, $(\oplus r)$ and $(\mu_S)$, hence proving $\vdash u : \mathbf{T} \to \mathbb{C}^1\text{hn}$, and finally $\vdash t : \mathbf{T} \to \mathbb{C}^1\text{hn}$ by subject expansion. The converse direction follows from Corollary E.16 (i.).

The argument for (ii.) is similar.

For (iii.), let $t$ be strongly normalizable, we argue by induction on the maximum length $N$ of a reduction of $t$. If $N = 0$, then $t$ is in normal form, so by an argument similar to (i.) we can deduce $\vdash_y t : \mathbf{T} \to \mathbb{C}^1\text{n}$. If $N > 0$ and $t \to u$, then by IH $\vdash_y u : \mathbf{T} \to \mathbb{C}^1\text{n}$ holds with a $\llbracket \cdot \rrbracket$-free derivation, and $t = C[(\lambda x.t')t'']$, $u = C[t'[t''/x]]$. If $x$ occurs in $t'$, then we deduce from Lemma D.19 that $\vdash_y t : \mathbf{T} \to \mathbb{C}^1\text{n}$ holds with a $\llbracket \cdot \rrbracket$-derivation. Otherwise, since $t''$ must be strong normalizable, by IH $\vdash_y t'' : \mathbf{T} \to \mathbb{C}^1\text{n}$, and we deduce, again by IH, that $\lambda x.t'$ can be typed by declaring $x : \mathbb{C}^1\text{n}$. We can then conclude $\vdash_y t : \mathbf{T} \to \mathbb{C}^1\text{n}$ also in this case.

The converse claim follows from Corollary E.16 (iii.) □

**D.3.2 Probabilistic Completeness.** The goal of this subsection is to establish the completeness part of Theorem 6.6:

**Theorem 6.6 (Probabilistic Completeness).** For any closed term $t$,

$$ \text{HNV}_{\leftarrow}(t) = \sup\{q \mid \vdash t : \mathbf{T} \to \mathbb{C}^q\text{hn}\} $$

$$ \text{NF}_{\leftarrow}(t) = \sup\{q \mid \vdash t : \mathbf{T} \to \mathbb{C}^q\text{n}\} $$

More precisely, we will show the $\leq$-part of the equations above, while soundness (i.e. the $\geq$-part of the equations above) will follow from Theorem 6.1 and Theorem 6.3, proved in the next section.

First, we need to study the structure of the trees $RBT(t)$ (see Subsection B.1) further.

**Definition D.20.** A *randomized multi-context C* is a term constructed from the grammar below

$$ C ::= \llbracket i \rrbracket (i \in \mathbb{N}) \mid C \oplus_a^i C \mid va.C $$

where for each two occurrences $\llbracket \cdot \rrbracket_i$ and $\llbracket \cdot \rrbracket_j$, $i \neq j$. The rank $r(C)$ is the maximum $k$ such that $\llbracket \cdot \rrbracket_k$ occurs in $C$.

For any randomized multi-context $C$, we let $C^{-\nu}$ be the randomized multi-context obtained by deleting all occurrences of $\nu$-binders.

If $C$ is a randomized multi-context of rank $k$, for all terms $t_1, \dots, t_k$, we let $C[t_1, \dots, t_k]$ indicate the term obtained by replacing each hole $\llbracket \cdot \rrbracket_i$ in $C$ by $t_i$.

An *initial segment T* of $RBT(t)$, noted $T \sqsubseteq RBT(t)$ is any sub-tree of $RBT(t)$ which contains its root.

Observe that a finite initial segment $T \sqsubseteq RBT(t)$ is the same thing as a term of the form $C_T[u_1, \dots, u_k]$ for some randomized multi-context $C_T$.

**Lemma D.21.** For any term $t$ and HNF $u_1, \dots, u_k$, if there exist randomized paths from $t$ to $u_1, \dots, u_k$, then there exists $N \in \mathbb{N}$, a randomized multi-context $C$ of rank $N+k$ and terms $t_1, \dots, t_N$ such that $t \to_p^* C[u_1, \dots, u_k, t_1, \dots, t_N]$ and $RBT(C[u_1, \dots, u_k, t_1, \dots, t_N]) \sqsubseteq RBT(t)$.

**Proof.** We argue by induction on the maximum length $K$ of the randomized paths considered. If $K = 0$, $k = 1$ and $t = u$, so we just let $N = 0$ and $C[\cdot] = [\cdot]$.

If $K \geq 1$, then in a finite number of reduction steps we get $t \to_p^* va.T$, where $T$ is a $(\mathcal{T}, a)$-tree such that for each $i = 1, \dots, k$, there exists $v_i \in \text{supp}(T)$ with a randomized path from $v_i$ to $u_i$ of length $\leq K - 1$; observe that we can write $T$ as $\mathcal{D}[v_1, \dots, v_q]$ for some randomized multi-context $C$.

For any $j = 1, \dots, q$, let $I_j$ be the set of values $i \leq k$ such that there is a randomized path from $v_j$ to $u_i$. The $I_j$ are disjoint sets with $\cup_j I_j = \{1, \dots, k\}$. By the I.H. we then deduce that there exist randomized multicontexts $C_j$ or rank $N_j + |I_j|$ and terms $w_{j1}, \dots, w_{jN_j}$ such that $v_j \to_p^* C[u_{i_1}, \dots, u_{i_{M_j}}, w_{j1}, \dots, w_{jN_j}]$, where $I_j = \{i_1, \dots, i_{M_j}\}$. We now have that

$$ t \to_p^* va.T = va.C[v_1, \dots, v_q] \to_p^* va.D[C_1[\vec{u}, \vec{w}], \dots, C_q[\vec{u}, \vec{w}]] $$

$$ \text{so we can let } N = \sum_j N_j, \quad C = va.D[C_1, \dots, C_q] \text{ and } t_1, \dots, t_N = w_{11}, \dots, w_{qM_q}. \quad \square $$

**Lemma D.22.** For any randomized multi-context $C$ with $n$ bound names $a_1, \dots, a_n$,

$$ va_1 \dots va_n \cdot C^{-\nu} \to_p^* C \quad (3) $$
*Proof.* We will prove the following fact: for all terms $vb.t, t_1, \dots, t_k$, it $C$ has no $v$-binders, then

$$vb.C[t_1, t_2, \dots, t_k, t] \stackrel{\to_p^*}{\to} C[t_1, \dots, t_k, vb.t] \quad (4)$$

From this fact we can deduce the main claim as follows: let $b$ be a bound variable in $C$ whose binder $v$ has no other binder in its scope; then $C$ splits as $C[t_0, t_1, \dots, t_k] = E[t_{i_1}, \dots, t_{i_p}, vb.D[t_{j_1}, \dots, t_{j_q}]]$, where $I = \{i_1, \dots, i_p\}, J = \{j_1, \dots, j_q\} \subseteq \{1, \dots, k+1\}$ satisfy $I \cap J = \emptyset$ and $p+q = r(C)$ (we are here supposing that $r(C) \ge 1$, because otherwise the claim is trivial).

Then, by (4) we deduce that $vb.E^{-v}[t_{i_1}, \dots, t_{i_p}, D[t_{j_1}, \dots, t_{j_q}]] \stackrel{\to_p}{\to} E^{-v}[t_{i_1}, \dots, t_{i_p}, vb.D[t_{j_1}, \dots, t_{j_q}]]$; by arguing in this way on all binders $v$ we finally obtain (3).

We prove (4) by induction on the construction of $C$:

* if $C = []_i$, then the claim trivially holds;

* if $C = C_1 \oplus_a^j C_2$, then $[]_{k+1}$ occurs in either $C_1$ or $C_2$, and not both; let us say $[]_{k+1}$ occurs in $C_1$; we then have that

$$ \begin{align*} 
vb.C[t_1, \dots, t_k, t] &= vb.C_1[t_{i_1}, \dots, t_{i_p}, t] \oplus_a^j C_2[t_{j_1}, \dots, t_{j_q}] \\ 
&\stackrel{\to_p}{\to} (vb.C_1[t_{i_1}, \dots, t_{i_p}, t]) \oplus_a^i (vb.C_2[t_{j_1}, \dots, t_{j_q}]) \\ 
&\stackrel{\to_p}{\to} (vb.C_1[t_{i_1}, \dots, t_{i_p}, t]) \oplus_a^i C_2[t_{j_1}, \dots, t_{j_q}] \\ 
&\stackrel{\text{I.H.}}{\to} \stackrel{\to_p^*}{C_1[t_{i_1}, \dots, t_{i_p}, vb.t]} \oplus_a^i C_2[t_{j_1}, \dots, t_{j_q}] = C[t_1, \dots, t_k, vb.t] 
\end{align*} $$

□

Still one technical lemmas before proceeding to the proof of Theorem 6.6.

**Lemma D.23.** Let $N, K \ge 1, X = \{a_1, \dots, a_K\}$ be distinct names, and for all $i \in N$ and $j \in K$, $b_{ij}$ be a conjunction of literals of name $a_j$ such that for all $i \ne i'$:

a. for all $k \le K$, if $\bigwedge_{j=1}^k b_{ij} \ne \bigwedge_{j=1}^k b_{i'j}$, then $(\bigwedge_{j=1}^k b_{ij}) \wedge (\bigwedge_{j=1}^k b_{i'j}) \models \perp$;

b. $(\bigwedge_{j=1}^K b_{ij}) \wedge (\bigwedge_{j=1}^K b_{i'j}) \models \perp$.

Suppose $\Gamma \vdash^{X,q_i} t : c \wedge (\bigwedge_{j=1}^K b_{ij}) \rightarrow \sigma$ is derivable for all $i \in \{1, \dots, N\}$. Then there exists a derivation of $\Gamma \vdash^\emptyset va_1 \dots va_K.t : c \rightarrow C^r \sigma$, where $r = \sum_{i=1}^N (q_i \cdot \prod_{j=1}^K \mu(b_{ij}))$.

*Proof.* We argue by induction on $K$. If $K=1$ then $i \ne i'$ implies $b_i \wedge b_{i'} \models \perp$, so we can conclude as follows:

$$ \frac{\left\{ \begin{array}{l} D_i \\ \Gamma \vdash^{\{a\}} t : c \wedge b_i \rightarrow C^{q_i} \sigma \end{array} \right\}_{i=1,\dots,N} (\mu_{\Sigma})}{\Gamma \vdash^{\emptyset} va.t : c \rightarrow C^{\sum_{i=1}^N q_i \cdot \mu(b_i)} \sigma} $$

If $K > 1$, then for all $i, i' \in \{1, \dots, N\}$, let $i \sim i'$ if $b_{iK} \wedge b_{i'K} \models \perp$ and for all $j \in \{1, \dots, K-1\}$, $b_{ij} \equiv b_{i'j}$. Let $Cl(N_\sim)$ indicate the set of cliques of the relation $\sim$, and for each $U \in Cl(N_\sim)$, fix some $i_U \in U$. Then we claim that the following equation holds:

$$ \sum_{i=1}^{N} q_i \cdot \prod_{j=1}^{K} \mu(b_{ij}) = \sum_{U \in Cl_{N_\sim}} \left( \prod_{j=1}^{K-1} \mu(b_{ij}) \right) \cdot \left( \sum_{i \in U} q_i \cdot \mu(b_{iK}) \right) \quad (5) $$

Indeed we can compute

$$ \begin{align*} 
\sum_{i=1}^{N} \left( q_i \cdot \prod_{j=1}^{K} \mu(b_{ij}) \right) &= \sum_{U \in Cl_{N_\sim}} \sum_{i \in U} \left( q_i \cdot \prod_{j=1}^{K} \mu(b_{ij}) \right) \\ 
&= \sum_{U \in Cl_{N_\sim}} \sum_{i \in U} \left( \prod_{j=1}^{K-1} \mu(b_{ij}) \right) \cdot \left( q_i \cdot \mu(b_{iK}) \right) \\ 
&= \sum_{U \in Cl_{N_\sim}} \left( \prod_{j=1}^{K-1} \mu(b_{ij}) \right) \cdot \left( \sum_{i \in U} q_i \cdot \mu(b_{iK}) \right) 
\end{align*} $$

Let us now show how to construct, for all $U \in Cl_{N_\sim}$, a derivation $D_U$ of $\Gamma \vdash^{\{a_1, \dots, a_{K-1}\}} va_{K,t} : c \wedge (\prod_{j=1}^{K-1} b_{ij}) \rightarrow C^{q_U} \sigma$, where $q_U = \sum_{i \in U} q_i \cdot \mu(b_{iK})$:
$$
D_U = \frac{\left\{ \Gamma \vdash^X t : c \wedge \left( \bigwedge_{j=1}^{K-1} \mathfrak{b}_{i_U j} \right) \wedge \mathfrak{b}_{i_U K} \to \mathsf{C}^{q_i} \sigma \right\}_{j \in U}}{\Gamma \vdash^{X-\{a_K\}} va_K.t : c \wedge \left( \bigwedge_{j=1}^{K-1} \mathfrak{b}_{i_U j} \right) \to \mathsf{C}^{q_U} \sigma} (\mu_\Sigma)
$$

Let $d_U = \bigwedge_{j=1}^{K-1} \mathfrak{b}_{i_U j}$, $t' = va_K.t$ and observe that we now have derivations $D_U$ of $\Gamma \vdash \{a_1, \dots, a_{K-1}\}, q_U$ $t' : c \wedge d_U \to \sigma$, where for all $U \neq V$, $d_U \wedge d_V \vdash \perp$. Moreover, for all $U \neq V$, from $d_U \neq d_V$ we deduce by condition (a.) that $d_U \wedge d_V \vdash \perp$; finally condition (b.) for the $d_U$ follows immediately from condition (b.) for the $\bigwedge_{j=1}^K \mathfrak{b}_{ij}$.

Hence, by applying the induction hypothesis, we deduce the existence of a derivation of $\Gamma \vdash^\emptyset v X.t : c \to \mathsf{C}^q \sigma$, where

$$
\begin{align*}
q &= \sum_{U \in \mathrm{Cl}_{N_{\sim}}} q_U \cdot \mu(d_U)) = \sum_{U \in \mathrm{Cl}_{N_{\sim}}} \left( q_U \cdot \prod_{j=1}^{K-1} \mu(\mathfrak{b}_{i_U j}) \right) \\
&= \sum_{U \in \mathrm{Cl}_{N_{\sim}}} \left( \sum_{i \in U} q_i \cdot \mu(\mathfrak{b}_{iK}) \right) \cdot \left( \prod_{j=1}^{K-1} \mu(\mathfrak{b}_{iU j}) \right) \\
&\stackrel{(5)}{=} \sum_{i=1}^{N} \left( q_i \cdot \prod_{j=1}^{K} \mu(\mathfrak{b}_{ij}) \right)
\end{align*}
$$

so we are done.

□

The technical lemma just proved can be used to establish Proposition D.24, i.e. the admissibility of the generalized counting rule $(\mu^*)$.

**Proposition D.24.** The following generalized counting rule is derivable in Cλ,∩:

$$
\frac{\Gamma \vdash \{a_1, \dots, a_K\} \quad t : \mathfrak{b} \quad \rightarrow \quad \mathsf{C}^q \sigma}{\Gamma \vdash^\emptyset va_1 \dots va_K.t : \mathsf{T} \quad \rightarrow \quad \mathsf{C}^{q \cdot \mu(\mathfrak{b})} \sigma} (\mu^*)
$$

Proof. First, let us transform $\mathfrak{b}$ into a disjunctive normal form of the form $\bigvee_{i=1}^N \bigwedge_{j=1}^K e_{ij}$, where each $e_{ij}$ is a conjunction of literals of name $a_j$. Now, as it was done in the proof of Lemma D.13, the $e_{ij}$ can be turned into conjunctions of literals $e_{ij}$, with $i \le N'$, for some $N' \ge N$, and $j \le K$, where for all $i \ne i'$ and $j, j'$, either $e_{ij} = e_{i'j'}$ or $e_{ij} \wedge e_{i'j'} \vdash \perp$, and $\bigvee_{i=1}^{N'} \bigwedge_{j=1}^K e_{ij} \equiv \bigvee_{i=1}^N \bigwedge_{j=1}^K e_{ij}$.

Observe that the $e_{ij}$ now satisfy conditions (a.) and (b.) of Lemma D.23. Moreover, by letting $\ell_i = \bigwedge_{j=1}^K e_{ij}$, from $\ell_i \vdash \mathfrak{b}$ we deduce that for all $i = 1, \dots, N'$, $\Gamma \vdash \{a_1, \dots, a_K\}, q \ t : \ell_i \to \sigma$ is derivable. Hence, by applying the Lemma, we can conclude that $\Gamma \vdash^\emptyset, va_1, \dots, va_K.t : \mathsf{T} \to \sigma$, where $r = \sum_{i=1}^{N'} q_i \cdot \mu(\ell_i) = q \cdot \sum_{i=1}^{N'} \mu(\ell_i) = q \cdot \mu(\mathfrak{b})$. $\square$

□

We can finally turn to the proof of the completeness part Theorem 6.6.

**Proposition D.25.** For any closed term $t$,

$$
\mathrm{HNV}_{\to}(t) \leq \sup\{q \mid \vdash t : \mathsf{T} \to \mathsf{C}^q \mathrm{hn}\}
$$

$$
\mathrm{NF}_{\to}(t) \leq \sup\{q \mid \vdash t : \mathsf{T} \to \mathsf{C}^q \mathrm{n}\}
$$

*Proof.* First observe that (with the notations from Subsection B.1)

$$
\mathrm{HNV}_{\to}(t) = \sup \left\{ \sum_{\pi: v \to w \in \mathrm{HNV}} \mu(\mathfrak{b}_{\pi}^v) \mid t \to_h^* v \right\} \\
= \sup \left\{ \sum_{i=1}^N \mu(\mathfrak{b}_{\pi_i}^u) \mid N \in \mathbb{N}, u_1, \dots, u_N \in \mathrm{HNV}, \pi_1 : v \mapsto u_1, \dots, \pi_N : t \mapsto u_N, t \to_h^* v \right\}
$$

so it is enough to show that for any $n \in \mathbb{N}$, term $v$ such that $t \to_h^* v$ and terms $u_1, \dots, u_n \in \mathrm{HNV}$ together with randomized paths $\pi_i : v \mapsto u_i$, we can prove that $\vdash t : \mathsf{T} \to \mathsf{C}^q \mathrm{hn}$ is derivable, with $q = \sum_{i=1}^n \mu(\mathfrak{b}_{\pi_i})$. Notice that, by subject expansion, it suffices to show $\vdash t : \mathsf{T} \to \mathsf{C}^q \mathrm{hn}$.

Let $\pi_1 : v \mapsto u_1, \dots, \pi_k : t \mapsto u_k$ be randomized paths, with $u_1, \dots, u_n \in \mathrm{HNV}$. By Lemma D.21 there exists $N$, terms $v_1, \dots, v_N$ and a randomized multi-context $\mathcal{C}$ of rank $k+N$ such that $v \to_p^* \mathcal{C}[u_1, \dots, u_k, v_1, \dots, v_N]$. Moreover, by Lemma D.22 there exists a permutative reduction $va_1 \dots va_K \cdot \mathcal{C}^{-\nu}[u_1, \dots, u_k, v_1, \dots, v_N] \to_p^* \mathcal{C}[u_1, \dots, u_k, v_1, \dots, v_N]$.
Let $v^*$ be the term $C^{-\nu}[u_1, \dots, u_k, v_1, \dots, v_N]$. For each HNV $u_i$, by Lemma D.18, we have that $\vdash u_i : \mathbf{T} \to C^1\mathbf{hn}$, so in particular $\vdash \{a_1, \dots, a_K\},^1 u_i : \mathbf{T} \to C^1\mathbf{hn}$ is derivable; using this fact one can construct by induction on C derivations $D_i$ of $\vdash \{a_1, \dots, a_K\} v^* : \mathfrak{b}_{\pi_i} \to C^1\mathbf{hn}$ (using the fact that $RBT(C[u_1, \dots, u_k, v_1, \dots, v_N]) \sqsubseteq RBT(t)$):

* if $C^{-\nu} = []_i$, then $k = 1$, $u^* = u$, and $\mathfrak{b}_{\pi_1} = \mathbf{T}$; then by the hypothesis we have $\vdash v^* : \mathbf{T} \to C^1\mathbf{hn}$;

* if $C^{-\nu} = C_1 \oplus_a^l C_2$, then $u^* = C_1[u_{i_1}, \dots, u_{i_p}, v_{i'_1}, \dots, v_{i'_s}] \oplus_a^l C_2[u_{j_1}, \dots, u_{j_q}, v_{j'_1}, \dots, v_{j'_s}]$, where $p+q=k$, $r+s=N$ and $I \cap J = \{i_1, \dots, i_p\} \cap \{j_1, \dots, j_q\} = \emptyset$, $I' \cap J' = \{i'_1, \dots, i'_r\} \cap \{j'_1, \dots, j'_s\} = \emptyset$. Moreover, we have that for all $m \in I$, $\mathfrak{b}_{\pi_l} = x_a^l \wedge \mathfrak{b}_{\pi'_m}$, where $\pi'_m$ is the path of $u_m$ in $C_1$; similarly, for all $m \in J$, $\mathfrak{b}_{\pi_m} = \neg x_a^l \wedge \mathfrak{b}_{\pi'_m}$, where $\pi'_m$ is the path of $u_l$ in $C_2$.

By the induction hypothesis we then have derivations of $\vdash \{a_1, \dots, a_K\} C_1[u_{i_1}, \dots, u_{i_p}, v_{i'_1}, \dots, v_{i'_s}] : \mathfrak{b}_{\pi'_m} \to C^1\mathbf{hn}$ and $\vdash \{a_1, \dots, a_K\} C_2[u_{j_1}, \dots, u_{j_q}, v_{j'_1}, \dots, v_{j'_s}] : \mathfrak{b}_{\pi'_m} \to C^1\mathbf{hn}$. Since $\mathfrak{b}_{\pi_i}$ is either $x_a^l \wedge \mathfrak{b}_{\pi'_i}$ or $\neg x_a^l \wedge \mathfrak{b}_{\pi'_i}$, on $i$, we obtain then in any case a derivation of $\vdash \{a_1, \dots, a_K\} v^* : \mathfrak{b}_{\pi_l} \to C^1\mathbf{hn}$ using either the $(\oplus l)$- or the $(\oplus r)$-rule.

Using the derivations $D_i$ we thus obtain a derivation of $\vdash^0 v a_1 \dots v a_K v^* : \mathbf{T} \to C^{\sum_i \mu(\mathfrak{b}_{\pi_i})}\mathbf{hn}$ by applying the derivable rule $(\mu^*)$ (Corollary D.24) as shown below:

$$ \frac{\left\{ \begin{array}{c} D_i \\ \vdash \{a_1, \dots, a_K\} v^* : \mathfrak{b}_{\pi_i} \to C^1\mathbf{hn} \end{array} \right\}_{i=1,\dots,k} \quad \begin{array}{c} \bigvee_i \mathfrak{b}_{\pi_i} \vdash \bigvee_i \mathfrak{b}_{\pi_i} \\ \vdash \{a_1, \dots, a_K\} v^* : \bigvee_i \mathfrak{b}_{\pi_i} \to C^1\mathbf{hn} \\ \vdash^0 v a_1 \dots v a_K v^* : \mathbf{T} \to C^{\mu(\bigvee_i \mathfrak{b}_{\pi_i})}\mathbf{hn} \end{array} \quad (\mathbf{V}) \quad (\mu^*) $$

Since $\mu(\bigvee_i \mathfrak{b}_{\pi_i}) = \sum_i \mu(\mathfrak{b}_{\pi_i})$, using subject reduction and subject expansion we can finally deduce $\vdash^0 v : \mathbf{T} \to C^{\sum_i \mu(\mathfrak{b}_{\pi_i})}\mathbf{hn}$. For the case of $NF_{\to}(t)$, we establish the result first for $NF(t)$, arguing by induction on normal forms with an argument similar to the one above, exploiting the fact that if $q_i = \sup S_i$, then $\prod_{i=1}^k q_i = \sup\{\prod_{i=1}^k s_i \mid s_i \in S_i\}$. $\square$

# E Normalization Results

In this section we establish a few normalization results for $C\lambda_{\leftarrow}^{}$ and $C\lambda_{\to, \emptyset}$. All results are based on some variant of the standard reducibility predicates technique.

First, we prove Theorem 5.3 by adapting a result from [16] to the language $\Lambda_{\text{PE}}^{}$. We then turn to probabilistic normalization. In Subsection E.2 we develop a theory of reducibility candidates for probabilistic head normal forms and probabilistic normal forms for $\Lambda_{\text{PE}}$ and for a general family of types which comprises both those of $C\lambda_{\leftarrow}^{}$ an $C\lambda_{\to, \emptyset}$. This will allows us to establish the normalization theorem for $C\lambda_{\to, \emptyset}$, but will also provide most of the steps needed to establish the normalization theorem for $C\lambda_{\leftarrow}^{}$. In Subsection E.3 we discuss reducibility candidates for $\Lambda_{\text{PE}}^{}$, by adapting most of results from the previous subsection, and we complete the proof of Theorem 6.1.

## E.1 Deterministic Normalization.

**E.1.1 Deterministic Normalization of $C\lambda_{\leftarrow}^{}$**. In this section we adapt the proof of [[16], Theorem 1] to $C\lambda_{\leftarrow}^{}$, in order to prove Theorem 5.3:

**Theorem 5.3 (Deterministic Normalization).** In both $C\lambda_{\to}$ and $C\lambda_{\leftarrow}^{}$, if $\Gamma \vdash \neg \neg t : \mathfrak{b} \to s$, then $t$ is strongly normalizable.

We introduce a simply typed $\lambda$-calculus $\lambda_{\leftarrow}^{}$ for $\Lambda_{\text{PE}}^{}$ and we show that typable terms are strongly normalizable under $\to^{}$. Simple types are defined by the grammar below

$$ \sigma ::= o \mid \sigma \Rightarrow \sigma $$

A judgement of $\lambda_{\leftarrow}^{}$ is of the form $\Gamma \vdash^\theta t : \sigma$, where $\theta$ is a list of names and $FN(t) \subseteq \theta$ (observe that we consider here lists and not sets). The rules of $\lambda_{\leftarrow}^{}$ are illustrated in Fig. 16.

The following is easily established by inspecting all reduction rules:

**Proposition E.1 (subject reduction).** If $\Gamma \vdash^\theta t : \sigma$ and $t \to^{} \emptyset$ $u$, then $\Gamma \vdash^\theta u : \sigma$.

For any type $s$ of $C\lambda_{\leftarrow}^{}$, let us define the corresponding simple type $|s|$ by letting $|o| = o$, $|s \Rightarrow \sigma| = |s| \Rightarrow |\sigma|$ and $|C^q s| = |s|$. The following is easily checked by induction:

**Proposition E.2.** If $\Gamma \vdash^X \neg \neg t : \mathfrak{b} \to s$ holds $C\lambda_{\leftarrow}^{}$, then $|\Gamma| \vdash^\theta t : |s|$ is derivable in $\lambda_{\leftarrow}^{}$, for any suitable $\theta$.
$$ \overline{\Gamma, x : \sigma \vdash^\theta x : \sigma} $$

$$ \frac{\Gamma, x : \sigma \vdash^\theta t : \tau}{\Gamma \vdash^\theta \lambda x.t : \sigma \Rightarrow \tau} $$

$$ \frac{\Gamma \vdash^\theta t : \sigma \Rightarrow \tau}{\Gamma \vdash^\theta tu : \tau} $$

$$ \frac{\Gamma \vdash^\theta t : \sigma \qquad \Gamma \vdash^\theta u : \sigma \qquad a \in \theta}{\Gamma \vdash^\theta t \oplus_a^i u : \sigma} $$

$$ \frac{\Gamma \vdash^\theta t : \sigma}{\Gamma \vdash^{\theta-\{a\}} va.t : \sigma} $$

$$ \frac{\Gamma \vdash^\theta t : \sigma \Rightarrow \tau}{\Gamma \vdash^\theta \{t\}u : \tau} $$

<caption>**Figure 16.** Typing rules for the simply typed $\lambda$-calculus $\lambda_{\to}^{\{\}}$.</caption>

Let $\Lambda_{\oplus, v, \{\}}^{\{\}}$ indicate the sets of $\lambda$-terms of $\Lambda_{\text{PE}}^{\{\}}$, and for all finite set of names $X$, let $\Lambda_{\oplus, v, \{\}}^{X}$ indicate the $\lambda$-terms with free names in $X$.

For any term $t$ with $\text{FN}(t) \subseteq \theta = a_1 \dots a_k$, we let $v^\theta t$ indicate the name-closed term $va_1 \dots va_k.t$. For any list of names $\theta$, let $\text{SN}^\theta = \{t \in \Lambda_{\oplus, v, \{\}}^X \mid v^\theta t$ is strongly normalizing$\}$, and for any $t \in \text{SN}^\theta$, let $\text{sn}^\theta(t)$ be the maximum length of a reduction of $v^\theta t$.

We let a $\{\}$-redex be a redex for any of the tree reductions rules $(\{\}\nu)-(\{\}\oplus_2)$.

**Lemma E.3.** (i.) if $tv_1 \dots v_n \in \text{SN}^\theta$, $utv_1 \dots v_n \in \text{SN}^\theta$, and a occurs in $\theta$; then $(t \oplus_a^i u)v_1 \dots v_n \in \text{SN}^\theta$;

(ii.) if $tv_1 \dots v_n \in \text{SN}^{a, \theta}$, where $\text{FN}(v_i) \subseteq X$, then $(va.t)v_1 \dots v_n \in \text{SN}^\theta$;

(iii.) if $v_i \in \text{SN}^\theta$, then $xv_1 \dots v_n \in \text{SN}^\theta$;

(iv.) if $(t[u/x])v_1 \dots v_n \in \text{SN}^\theta$ and $u \in \text{SN}^\theta$, then $(\lambda x.t)uv_1 \dots v_n \in \text{SN}^\theta$;

*Proof.* (i.) Same argument as [[16], Lemma 24], observing that a $\{\}$-redex in $(t \oplus_a^i u)v_1 \dots v_n$ can only occur inside one of $t, u, v_1, \dots, v_n$.

(ii.) Same argument as [[16], Lemma 25], again observing that a $\{\}$-redex in $(va.t)v_1 \dots v_n$ can only occur inside one of $t, u, v_1, \dots, v_n$.

(iii.) Immediate.

(iv.) Same argument as [[16], Lemma 27], again observing that a $\{\}$-redex in $(\lambda x.t)uv_1 \dots v_n$ can only occur inside one of $t, u, v_1, \dots, v_n$.

□

**Lemma E.4.** Let $t^\bullet$ be obtained from $t$ by deleting a finite number of $v$-binders $va_1, \dots, va_k$. If $t \in \text{SN}^\theta$, then $t^\bullet \in \text{SN}^{\theta'}$, for any suitable $\theta'$.

*Proof.* We argue by induction on $|t| + \text{sn}^\theta(t)$:

* if $t = x$ or $t = y$, the claim is immediate;

* if $t = \lambda y.t'$, the claim follows by IH;

* if $t = t_1 t_2$, then $t^\bullet = t_1^\bullet t_2^\bullet$; let us consider all possible reductions of $t^\bullet$:

* a reduction of either $t_1^\bullet$ or $t_2^\bullet$, in which case we apply the IH;

* a reduction $(\lambda y.u^\bullet)t_2^\bullet \to^\beta u^\bullet[t_2^\bullet/y]$, where $t_1 = \lambda y.u$, in which case we also apply the IH;

* a reduction of the form $u^\bullet t_2^\bullet \to^\{\} v^\bullet$, where $t_1 = va.u$, then $t_1 t_2 \to^{\to_{p\{\}}}(va.ut_2)$, so we can apply the IH to $ut_2$.

* if $t = \{t_1\}t_2$, then $t^\bullet = \{t_1^\bullet\}t_2^\bullet$; then a reduction is either a reduction of either $t_1^\bullet$ or $t_2^\bullet$, in which case we apply the IH, either a $(\{\}\oplus_1)$, $(\{\}\oplus_2)$-reduction, in which case we also apply the IH, or a reduction of the form $\{t_1^\bullet\}va.u^\bullet \to^{\to_{p\{\}}}(va.t_1^\bullet u^\bullet)$, where $t_2 = va.u$, in which case we also have $\{t_1\}t_2 \to^{\to_{p\{\}}}(va.t_1u)$, so we can apply the IH.

* if $t = t_1 \oplus_a^i t_2$, then a reduction of $t^\bullet$ is either a reduction of $t_1^\bullet$ or $t_2^\bullet$, in which case we apply the IH, or a reduction of the form $t_1^\bullet \oplus_a^i (u^\bullet \oplus_b^j v^\bullet) \to^{\to_{p\{\}}}(t_1^\bullet \oplus_a^i u^\bullet) \oplus_b^j (t_1^\bullet \oplus_a^i v^\bullet)$, where $t_2 = v \oplus_a^i w$, in which case $t \to^{\to_{p\{\}}}(t_1 \oplus_a^i u) \oplus_b^j (t_2 \oplus_a^i v)$, so we can apply the IH;

* if $t = vb.u$, then if $t^\bullet = u^\bullet$, we can argue by the IH; if $t^\bullet = vb.u^\bullet$, then a reduction of $t^\bullet$ is either a reduction of $u^\bullet$, in which case we can apply the IH, or a permutation $vb.u_1^\bullet \oplus_a^i u_2^\bullet \to^{\to_{p\{\}}}(vb.u_1^\bullet) \oplus_a^i (vb.u_2^\bullet)$, where $u = u_1 \oplus_a^i u_2$, in which case $t \to^{\to_{p\{\}}}(vb.u_1) \oplus_a^i (vb.u_2)$ so we can apply the IH.

□

**Lemma E.5.** (i.) If $(va.tu)v_1 \dots v_n \in \text{SN}^\theta$, then $\{t\}(va.u)v_1 \dots v_n \in \text{SN}^\theta$.

(ii.) If $t[va.u/x]v_1 \dots v_n \in \text{SN}^\theta$, then $t[u/x]v_1 \dots v_n \in \text{SN}^{\theta'}$, for any suitable $\theta'$.

(iii.) If $(tu)v_1 \dots v_n \in \text{SN}^\theta$, then $(\{t\}u)v_1 \dots v_n \in \text{SN}^\theta$.
**Proof.** (i.) We argue by induction on $|t| + \text{sn}^\theta(t) + \text{sn}^\theta(v) + \sum_i \text{sn}^\theta(v_i)$.

A reduction of $\{t\}(va.u)v_1 \dots v_n$ can only be a reduction in either of $t, u, v_1, \dots, v_n$, a reduction of the form $\{t_1 \oplus_a^i t_2\}(va.u)v_1 \dots v_n \to_{p\{}}$ ($\{t_1\}(va.u)v_1 \dots v_n \oplus_a^i (\{t_1\}(va.u)v_1 \dots v_n)$, or a reduction $\{t\}(va.u)v_1 \dots v_n \to_{p\{}}$ ($va.tu)v_1 \dots v_n$. In the first case we can use the IH; in the second case by the IH we deduce $(\{t_i\}(va.u)v_1 \dots v_n) \in \text{SN}^\theta$ and we can conclude by Lemma E.3 (i.). In the third case we conclude by the hypothesis.

(ii.) Immediate application of Lemma E.4.

(iii.) We argue by induction on $n + |t| + |u| + \text{sn}^\theta(t) + \text{sn}^\theta(u) + \sum_i \text{sn}^\theta(v_i)$.

A reduction of $(\{t\}u)v_1 \dots v_n$ is of one of the following forms:

* a reduction of $t$ or of $u, v_1, \dots, v_n$ in which case we argue by the IH;

* a reduction of the form $((\{t\}va.u')v_1 \dots v_n \to_{p\{}}) (va.tu')v_1 \dots v_n$, where $u = va.u'$; then by Lemma E.4, from $(tu)v_1 \dots v_n \in \text{SN}^\theta$ we deduce $(tu')v_1 \dots v_n \in \text{SN}^{X \cup \{a\}}$, and by Lemma E.3 (ii.), $(va.tu')v_1 \dots v_n \in \text{SN}^\theta$;

* a reduction of the form $((\{t_1\} \oplus_a^i t_2\}u)v_1 \dots v_n \to_{p\{}}$ $((\{t_1\}u) \oplus_a^i (\{t_2\}u))v_1 \dots v_n$, where $t = t_1 \oplus_a^i t_2$; then by IH $(\{t_i\}u)v_1 \dots v_n \in \text{SN}^\theta$, so we conclude $((\{t_1\}u) \oplus_a^i (\{t_2\}u))v_1 \dots v_n$ by Lemma E.3 (i.).

* a reduction of the form $((\{t\}(u_1 \oplus_a^i u_2))v_1 \dots v_n \to_{p\{}}) ((\{t\}u_1) \oplus_a^i (\{t\}u_2))v_1 \dots v_n$; then by IH $(\{t\}u_i)v_1 \dots v_n \in \text{SN}^\theta$, so we conclude $((\{t\}u_1) \oplus_a^i (\{t\}u_2))v_1 \dots v_n$ by Lemma E.3 (i.).

* a reduction of the form $((\{t\}u)v_1 \dots v_k)(v_{k+1}^{\oplus_a^i} v_{k+1}^{\oplus_a^i} v_{k+2} \dots v_n \to_{p\{}}) ((\{t\}u)v_1 \dots v_k v_{k+1}^{\oplus_a^i}) \oplus_a^i ((\{t\}u)v_1 \dots v_k v_{k+1}^{\oplus_a^i}) v_{k+2} \dots v_n$; then by IH $(\{t\}u)v_1 \dots v_k v_{k+1}^{\oplus_a^i} \in \text{SN}^\theta$, $(\{t\}u)v_1 \dots v_k v_{k+1}^{\oplus_a^i} \in \text{SN}^\theta$, and by Lemma E.3 (i.) we conclude $((\{t\}u)v_1 \dots v_k v_{k+1}^{\oplus_a^i}) \oplus_a^i ((\{t\}u)v_1 \dots v_k v_{k+1}^{\oplus_a^i}) v_{k+2} \dots v_n \in \text{SN}^\theta$.

□

The family of reducibility predicates $\text{Red}_\sigma^\theta$ of $\lambda_{\{\}}^\to$ is defined as follows:

$$ \text{Red}_\sigma^\theta := \text{SN}^\theta \\ \text{Red}_{\sigma \to \tau}^\theta := \{t \in \Lambda_{\oplus, v, \{\}}^X \mid \forall u \in \text{Red}_\sigma^\theta, tu \in \text{Red}_\tau^\theta\} $$

**Lemma E.6.** 1. If $t \in \text{Red}_\sigma^\theta$, then $t \in \text{SN}^\theta$;

2. if $\Gamma \vdash xu_1 \dots u_n$ and $u_1, \dots, u_n \in \text{SN}^\theta$, then $xu_1 \dots u_n \in \text{Red}_\sigma^\theta$;

3. If $t[u/x]v_1 \dots v_n \in \text{Red}_\sigma^\theta$, and $u \in \text{SN}^\theta$, then $(\lambda x.t)uv_1 \dots v_n \in \text{Red}_\sigma^\theta$;

4. if $tv_1 \dots v_n \in \text{Red}_\sigma^\theta$ and $uv_1 \dots v_n \in \text{Red}_\sigma^\theta$, and $a \in \theta$, then $(t \oplus_a^i u)v_1 \dots v_n \in \text{Red}_\sigma^\theta$

5. if $tv_1 \dots v_n \in \text{Red}_\sigma^{a \to \theta}$ and $\text{FN}(v_i) \subseteq X$, then $(va.t)v_1 \dots v_n \in \text{Red}_\sigma^\theta$.

**Proof.** The proof is similar to the proof of [[16], Lemma 28].

**Lemma E.7.** If $t \in \text{Red}_{\sigma \to \tau}^\theta$ and $u \in \text{Red}_\sigma^\theta$, then $\{t\}u \in \text{Red}_\tau^\theta$.

**Proof.** Let $\tau = \sigma_1 \Rightarrow \dots \Rightarrow \sigma_n \Rightarrow o$ and let $v_1 \in \text{Red}_{\sigma_1}^\theta, \dots, v_n \in \text{Red}_{\sigma_n}^\theta$. Then $(tu)v_1 \dots v_n \in \text{SN}^\theta$ which, by Lemma E.5, implies $\{t\}uv_1 \dots v_n \in \text{SN}^\theta$, from which we conclude $\{t\}u \in \text{NRed}_\tau^X$.

**Proposition E.8.** If $\Gamma \vdash^\theta t : \sigma$ is derivable in $\lambda_{\{\}}^\to$, where $\Gamma = \{x_1 : \sigma_1, \dots, x_n : \sigma_n\}$, then for all $u_i \in \text{Red}_{\sigma_i}^\theta$, $t[u_1/x_1, \dots, u_n/x_n] \in \text{Red}_\sigma^\theta$.

**Proof.** The argument is by induction on $t$. All inductive cases are treated as in the proof of [[16], Proposition 29], using the lemmas proved above; the only new case is the one below:

* if $t$ is $\{t_1\}t_2$ then the last rule is

$$ \frac{\Gamma \vdash^\theta t_1 : \sigma \Rightarrow \tau \qquad \Gamma \vdash^\theta t_2 : \sigma}{\Gamma \vdash^\theta t : \tau} $$

then by IH for all $u_i \in \text{Red}_{\sigma_i}^X$, $t_1[u_1/x_1, \dots, u_n/x_n] \in \text{Red}_{\sigma \to \tau}^\theta$ and $t_2[u_1/x_1, \dots, u_n/x_n] \in \text{Red}_\sigma$, so by Lemma E.7 $t[u_1/x_1, \dots, u_n/x_n] = \{t_1[u_1/x_1, \dots, u_n/x_n]\}(t_2[u_1/x_1, \dots, u_n/x_n]) \in \text{Red}_\tau^\theta$.

□

**Theorem E.9.** If $\Gamma \vdash^\theta t : \sigma$ is derivable in $\lambda_{\{\}}^\to$, then $t \in \text{SN}^\theta$.

From this, using Proposition E.2 we immediately deduce:

**Corollary E.10.** If $\Gamma \vdash^X t : \emptyset \Rightarrow \sigma$ is derivable in $\lambda_{\{\}}^\to$ with no 0-ary instance of the $(\forall)$-rule, then $t \in \text{SN}^\theta$, for any suitable $\theta$.
$$ \frac{\Gamma \vdash^\theta t : \sigma}{\Gamma \vdash^\theta t : \mathit{hn}} \qquad \frac{\Gamma \vdash^\theta t : \sigma}{\Gamma \vdash^\theta t : \mathit{n}} (\sigma \{ \emptyset, \mathit{hn} \}-\mathit{free}) $$

$$ \frac{\mathrm{FV}(t) \subseteq \Gamma}{\Gamma \vdash^\theta t : \emptyset} \qquad \frac{\Gamma \vdash^\theta t : \sigma \qquad \Gamma \vdash^\theta t : \tau}{\Gamma \vdash^\theta t : \sigma \wedge \tau} $$

<caption>**Figure 17.** Typing rules for the simply typed $\lambda$-calculus $\lambda_{\rightarrow, \infty}$.</caption>

**E.1.2 Deterministic Normalization of** $C\lambda_{\rightarrow, \infty}$. We now adapt the proof of [[16], Theorem 1] to $C\lambda_{\rightarrow, \infty}$.

For this we consider an intersection type system $\lambda_{\rightarrow, \infty}$ for $\Lambda_{\mathit{PE}}$ with the following types

$$ \sigma ::= [] | o | \mathit{hn} | n | \sigma \Rightarrow \sigma | \sigma \wedge \sigma $$

The rules of $\lambda_{\rightarrow, \infty}$ include all those of $\lambda_{\rightarrow}^{}$ except the one for $\emptyset$, together with the rules in Fig. 17.

For any type $s$ of $C\lambda_{\rightarrow, \infty}$, we define the corresponding type $|s|$ of $\lambda_{\rightarrow, \infty}$ by $|\sigma| = \sigma$, for $\sigma \in \{\mathit{hn}, \mathit{n}\}$, $|\mathfrak{M} \Rightarrow \sigma| = |\mathfrak{M}| \Rightarrow |\sigma|$, where $|[]| = []$, $|\{s_1, \dots, s_{n+1}\}| = |s_1| \wedge \dots \wedge |s_{n+1}|$, and $|C^q\sigma| = |\sigma|$.

The following is easily checked by induction:

**Proposition E.11.** If $\Gamma \vdash^X \mathit{t} : \mathfrak{b} \Rightarrow s$ is derivable in $C\lambda_{\rightarrow, \infty}$, then $|\Gamma| \vdash^\theta t : |s|$ is derivable in $\lambda_{\rightarrow, \infty}$, for any suitable $\theta$.

Let $\Lambda_{\oplus, \nu}$ indicate the sets of $\lambda$-terms of $\Lambda_{\mathit{PE}}$, and for all finite set of names $X$, let $\Lambda_{\oplus, \nu}^X$ indicate the $\lambda$-terms with free names in $X$. For any finite list of names $\theta$ contained in $X$, we let

$$ \mathrm{HN}^{\theta} := \{t \in \Lambda_{\oplus, \nu}^{X} | v^{\theta}t \text{ is head-normalizing}\} $$

$$ \mathrm{NN}^{\theta} := \{t \in \Lambda_{\oplus, \nu}^{X} | v^{\theta}t \text{ is normalizing}\} $$

$$ \mathrm{SN}^{\theta} := \{t \in \Lambda_{\oplus, \nu}^{X} | v^{\theta}t \text{ is strongly normalizing}\} $$

We define two families of reducibility predicates $\mathrm{NNRed}_{\sigma}^{\theta}$, $\mathrm{HNRed}_{\sigma}^{\theta} \subseteq \Lambda_{\oplus, \nu}^X$ as follows:

$$ \mathrm{HNRed}_{\emptyset}^{\theta} := \Lambda_{\oplus, \nu}^{X} $$

$$ \mathrm{NNRed}_{\emptyset}^{\theta} := \mathrm{NNRed}_{\mathit{hn}} = \Lambda_{\oplus, \nu}^{X} $$

$$ \mathrm{HNRed}_{o}^{\theta} := \mathrm{HNRed}_{\mathit{hn}}^{\theta} = \mathrm{HNRed}_{\mathit{hn}}^{\theta} = \mathrm{HN}^{\theta} $$

$$ \mathrm{NNRed}_{o}^{\theta} := \mathrm{NNRed}_{\mathit{n}}^{\theta} = \mathfrak{N}^{\theta} $$

$$ \mathrm{HNRed}_{\sigma \rightarrow \tau}^{\theta} := \{t \in \Lambda_{\oplus, \nu}^{X} | \forall u \in \mathrm{HNRed}_{\sigma}^{\theta}, \mathrm{tu} \in \mathrm{HNRed}_{\tau}^{\theta}\} $$

$$ \mathrm{NNRed}_{\sigma \rightarrow \tau}^{\theta} := \{t \in \Lambda_{\oplus, \nu}^{X} | \forall u \in \mathrm{NNRed}_{\sigma}^{\theta}, \mathrm{tu} \in \mathrm{NNRed}_{\tau}^{\theta}\} $$

$$ \mathrm{HNRed}_{\sigma \wedge \tau}^{\theta} := \mathrm{HNRed}_{\sigma}^{\theta} \cap \mathrm{HNRed}_{\tau}^{\theta} $$

$$ \mathrm{NNRed}_{\sigma \wedge \tau}^{\theta} := \mathrm{NNRed}_{\sigma}^{\theta} \cap \mathrm{NNRed}_{\tau}^{\theta} $$

Moreover, we define a third family of reducibility predicates $\mathrm{SNRed}_{\sigma}^{\theta} \subseteq \Lambda_{\oplus, \nu}^X$, indexed on all $\{\emptyset, \mathit{hn}\}$-free types as follows:

$$ \mathrm{SNRed}_{o}^{\theta} = \mathrm{SNRed}_{n}^{\theta} = \mathrm{SN}^{\theta} $$

$$ \mathrm{SNRed}_{\sigma \rightarrow \tau}^{\theta} := \{t \in \Lambda_{\oplus, \nu}^{X} | \forall u \in \mathrm{NNRed}_{\sigma}^{\theta}, \mathrm{tu} \in \mathrm{NNRed}_{\tau}^{\theta}\} $$

$$ \mathrm{SNRed}_{\sigma \wedge \tau}^{\theta} := \mathrm{NNRed}_{\sigma}^{\theta} \cap \mathrm{NNRed}_{\tau}^{\theta} $$

**Definition E.12** (non-trivial types). The set of non-trivial types is defined by induction as follows:

* o, hn, n are non-trivial;

* if $\tau$ is non-trivial, $\sigma \Rightarrow \tau$ is non-trivial;

* if either $\sigma$ or $\tau$ are non-trivial, $\sigma \wedge \tau$ is non-trivial.

**Lemma E.13.** For any type $\sigma$,

(i.) if $\sigma$ is non-trivial then $\mathrm{HNRed}_{\sigma}^{\theta} \subseteq \mathrm{HN}^{\theta}$;

(ii.) if $\sigma$ is $\{\emptyset, \mathit{hn}\}$-free, then $\mathrm{NNRed}_{\sigma}^{\theta} \subseteq \mathrm{NN}^{\theta}$;

(iii.) if $\sigma$ is $\{\emptyset, \mathit{hn}\}$-free, then $\mathrm{SNRed}_{\sigma}^{\theta} \subseteq \mathrm{SN}^{\theta}$.

*Proof.* (i.) is proved in a standard way by induction on all types $\sigma$, also proving at each step that for any term $t$ of the form $xt_1 \dots t_n, t \in \mathrm{HNRed}_{\sigma}^{\theta}$.

(ii.) is proved in a standard way by induction on all types $\sigma$, also proving at each step that for any term $t$ of the form $xt_1 \dots t_n$, where $t_1, \dots, t_n \in \mathrm{NN}^{\theta}$, $t \in \mathrm{NNRed}_{\sigma}^{\theta}$.

(iii.) is proved in a standard way by induction on all $\{\emptyset, \mathit{hn}\}$-free types $\sigma$, also proving at each step that for any term $t$ of the form $xt_1 \dots t_n$, where $t_1, \dots, t_n \in \mathrm{SN}^{\theta}$, $t \in \mathrm{SNRed}_{\sigma}^{\theta}$.
☐

**Proposition E.14.** If $\Gamma \vdash^\theta t : \sigma$ is derivable in $\lambda_{\rightarrow, \cap}$, where $\Gamma = \{x_1 : \sigma_1, \dots, x_n : \sigma_n\}$, and $\text{FN}(t) \subseteq X$, then

(i.) for all $u_i \in \text{HNRed}_{\sigma_i}^{\theta}$, $t[u_1/x_1, \dots, u_n/x_n] \in \text{HNRed}_{\sigma}$;

(ii.) for all $u_i \in \text{NNRed}_{\sigma_i}^{\theta}$, $t[u_1/x_1, \dots, u_n/x_n] \in \text{NNRed}_{\sigma}$;

(iii.) if the types [] and hn never occurs in the derivation, then for all $u_i \in \text{SNRed}_{\sigma_i}^{\theta}$, $t[u_1/x_1, \dots, u_n/x_n] \in \text{SNRed}_{\sigma}$;

*Proof.* Both arguments are by induction on the typing derivation of $t$. All inductive cases are treated as in the proof of [[16], Proposition 29], except for those below (we consider here only case (ii.)):

* if the last rule is

$$ \frac{\Gamma \vdash^\theta t : \sigma}{\Gamma \vdash^\theta t : \text{hn}} $$

then for all $u_i \in \text{NNRed}_{\sigma_i}^{\theta}$, $t[u_1/x_1, \dots, u_n/x_n] \in \Lambda_{\oplus, \nu}^{X} = \text{NNRed}_{\text{hn}}^{\theta}$.

* if the last rule is

$$ \frac{\Gamma \vdash^\theta t : \sigma}{\Gamma \vdash^\theta t : \text{n}} $$

where $\sigma$ is {[]}, hn}-free, then for all $u_i \in \text{NNRed}_{\sigma_i}^{\theta}$, $t[u_1/x_1, \dots, u_n/x_n] \in \text{NNRed}_{\sigma}^{\theta}$, and by Lemma E.13 $\text{NNRed}_{\sigma}^{\theta} \subseteq \text{NN}^{\theta} = \text{NNRed}_{\text{n}}^{\theta}$, so $t[u_1/x_1, \dots, u_n/x_n] \in \text{NNRed}_{\text{n}}^{\theta}$.

* if the last rule is

$$ \frac{\text{FN}(t) \subseteq X}{\Gamma \vdash^\theta t : []} $$

then for all $u_i \in \text{NNRed}_{\sigma_i}^{\theta}$, $t[u_1/x_1, \dots, u_n/x_n] \in \Lambda_{\oplus, \nu}^{X} = \text{NNRed}_{\text{[]}}^{\theta}$.

* if the last rule is

$$ \frac{\Gamma \vdash^\theta t : \sigma \quad \Gamma \vdash^\theta t : \tau}{\Gamma \vdash^\theta t : \sigma \wedge \tau} $$

then for all $u_i \in \text{NNRed}_{\sigma_i}^{\theta}$, by IH $t[u_1/x_1, \dots, u_n/x_n] \in \text{NNRed}_{\sigma}^{\theta}$ and $t[u_1/x_1, \dots, u_n/x_n] \in \text{NNRed}_{\tau}^{\theta}$, whence $t[u_1/x_1, \dots, u_n/x_n] \in \text{NNRed}_{\sigma}^{\theta} \cap \text{NNRed}_{\tau}^{\theta} = \text{NNRed}_{\sigma \wedge \tau}^{\theta}$.

☐

**Proposition E.15.** If $\Gamma \vdash^\theta t : \sigma$ is derivable in $\lambda_{\rightarrow, \cap}$, then:

(i.) if [] is non-trivial, then $v^\theta t$ is head-normalizable;

(ii.) if $\Gamma$ and $\sigma$ are {[]}, hn}-free, then $v^\theta t$ is normalizable;

(iii.) if [] and hn never occur in the derivation, then $v^\theta t$ is strongly normalizable.

Using Proposition E.11

**Corollary E.16.** If $\Gamma \vdash_{\neg \vee}^X t : \delta \rightarrow s$ in $C\lambda_{\rightarrow, \cap}$, then for all suitable $\theta$:

(i.) $v^\theta t$ is head-normalizable;

(ii.) if $\Gamma$ and $\sigma$ are {[]}, hn}-free, then $v^\theta t$ is normalizable;

(iii.) if [] and hn never occur in the derivation, then $v^\theta t$ is strongly normalizable.

## E.2 Probabilistic Reducibility Candidates for $\Lambda_{\text{PE}}$.

In this subsection and the following one we work with a general class of types which comprises both those of $C\lambda_{\rightarrow, \cap}^{}$ and those of $C\lambda_{\rightarrow, \cap}$. These types are defined by the grammar below:

$$ \sigma ::= [] | o | hn | n | \sigma \Rightarrow \sigma | \sigma \wedge \sigma | C^q\sigma $$

It is clear that any type of $C\lambda_{\rightarrow, \cap}^{}$ is a type of the grammar above. For the types of $C\lambda_{\rightarrow, \cap}$ it suffices to see $\mathcal{M} = [s_1, \dots, s_n]$ as $(\dots (s_1 \wedge s_2) \wedge \dots \wedge s_{n-1}) \wedge s_n$, where $n > 0$, and as [] otherwise.

For any type $\sigma$, we let the positive real $[\sigma] \in [0, 1]$ be defined by $[[]] = 0$, $[o] = [hn] = [n] = 1$, $[\sigma \Rightarrow \tau] = [\sigma] \cdot [\tau]$, $[\sigma \wedge \tau] = \max\{[\sigma], [\tau]\}$, and $[C^q\sigma] = q \cdot [\sigma]$.

One can check that for all type $\sigma$ coming from either $C\lambda_{\rightarrow, \cap}^{}$ or $C\lambda_{\rightarrow, \cap}^{}$, $[\sigma] > 0$.

Let us establish a few preliminary lemmas.

**Lemma E.17.** For all $t \in \mathcal{T}$ and variables $x, y$, with $y$ not occurring in $t$,

(i.) $\text{HNV}(t) = \text{HNV}(t[y/x])$;

(ii.) $\text{NF}(t) = \text{NF}(t[y/x])$.
*Proof.* We only prove case (ii.), the other one being proved in a similar way. Observe that if $t$ is not a strong head normal form and $\mathcal{D}_t(u) > 0$, it must be that $u$ is of size strictly smaller that $t$. So we can argue by induction on $t$:

* if $t = \lambda \vec{x}.zt_1...t_n$, then $\mathrm{NF}(t) = \prod_i \mathrm{NF}(t_i) \stackrel{\mathrm{[I.H.]}}{=} \prod_i \mathrm{NF}(t_i[y/x]) = \mathrm{NF}(t[y/x]);$

* otherwise, since $\mathcal{D}_t(u) = \mathcal{D}_{t[y/x]}(u[y/x])$, we have that $\mathrm{NF}(t) = \sum_{u \in \mathrm{HNV}} \mathcal{D}_t(u) \cdot \mathrm{NF}(u) = \sum_{u \in \mathrm{HNV}} \mathcal{D}_{t[y/x]}(u[y/x]) \cdot \mathrm{NF}(u) \stackrel{\mathrm{[I.H.]}}{=} \sum_{u \in \mathrm{HNV}} \mathcal{D}_{t[y/x]}(u[y/x]) \cdot \mathrm{NF}(u) = \sum_{u \in \mathrm{HNV}} \mathcal{D}_{t[y/x]}(u) \cdot \mathrm{NF}(u) = \mathrm{NF}(t[y/x])$.

**Lemma E.18.** For any name-closed term $t$,

(i.) $\mathrm{HNV}(t) = \mathrm{HNV}(\lambda y.t)$;

(ii.) $\mathrm{NF}(t) = \mathrm{NF}(\lambda y.t)$.

*Proof.* We only prove case (ii.), the other one being proved in a similar way. We argue by induction on $t$:

* if $t \stackrel{\cdot}{\to}_{p\{\}}^* \lambda \vec{x}.zt_1...t_n$, then $\lambda y.t \stackrel{\cdot}{\to}_{p\{\}}^* \lambda y \lambda \vec{x}.zt_1...t_n$, so by definition $\mathrm{NF}(t) = \prod_i \mathrm{NF}(t_i) = \mathrm{NF}(\lambda y.t)$;

* otherwise, if $t \stackrel{\cdot}{\to}_{p\{\}}^* va.t'$, then $\lambda y.t \stackrel{\cdot}{\to}_{p\{\}}^* va.t^{\lambda y}$, and one can show by induction on a $\to_p$-reduction path that $\mathcal{D}_{t'}(u) = \mathcal{D}_{t^{\lambda y}}(\lambda y.u)$. So we have that $\mathrm{NF}(t) = \sum_{u \in \mathrm{HNV}} \mathcal{D}_{t'}(u) \cdot \mathrm{NF}(u) = \sum_{u \in \mathrm{HNV}} \mathcal{D}_{t^{\lambda y}}(\lambda y.u) \cdot \mathrm{NF}(u) \stackrel{\mathrm{[I.H.]}}{=} \sum_{u \in \mathrm{HNV}} \mathcal{D}_{t^{\lambda y}}(\lambda y.u) \cdot \mathrm{NF}(\lambda y.u) = \sum_{u \in \mathrm{HNV}} \mathcal{D}_{t^{\lambda y}}(u) \cdot \mathrm{NF}(u) = \mathrm{NF}(\lambda y.t)$.

**Lemma E.19.** For any name-closed term $t$,

(i.) $\mathrm{HNV}(t) \geq \mathrm{HNV}(tx)$;

(ii.) $\mathrm{NF}(t) \geq \mathrm{NF}(tx)$.

*Proof.* We only prove case (ii.), the other one being proved in a similar way. Suppose $tx \to^* u$ and $\mathrm{NF}(u) \geq q$. We will show that $\mathrm{NF}(t) \geq q$. Two cases arise:

* $u = u'x$ where $t \to^* u'$. Then $u'$ cannot start with either $v$ (otherwise it would not be a PNF, since $(va.v)x \to_{p\{\}} va.vx)$, $\oplus$ (since $(v_1 \oplus_a^i v_2)x \to_{p\{\}} (v_1x) \oplus_a^i (v_2x)$), or $\lambda$ (since $(\lambda y.v)x$ is a $\beta$-redex, which would imply $\mathrm{NF}(u) = 0$). Hence $u'$ is of the form $yu_1...u_n$, and thus $\mathrm{NF}(u) = \mathrm{NF}(u') \geq q$, which implies $\mathrm{NF}(t) \geq q$.

* $tx \stackrel{\cdot}{\to}_{\{\}}^* (\lambda y.t')x$, and $t'[y \mapsto x] \stackrel{\cdot}{\to}_{\{\}}^* u$. Then $t$ reduces to the PNF $\lambda y.u[x \mapsto y]$, and we can conclude by Lemma E.17 and Lemma E.18.

In the following, we will sometimes write $t \in \mathrm{HNV}_{\to}^r$ (resp. $t \in \mathrm{NF}_{\to}^r$) for $\mathrm{HNV}_{\to}(t) \geq r$ (resp. $\mathrm{NF}_{\to}(t) \geq r$).

We will define two different classes of *reducibility predicates*, one related to probabilistic head normal forms and the other related to probabilistic normal forms. For any type $\sigma$, finite set $X$ of names, $r \in [0, 1]$, and $S \subseteq (2^N)^X$, we define the sets $\mathrm{HRed}_{\sigma}^{X,r}(S)$, $\mathrm{NRed}_{\sigma}^{X,r}(S) \subseteq \Lambda_{\oplus, \nu}^X$ by induction as follows:

$$ \mathrm{HRed}_{\llbracket}^{X,r}(S) = \Lambda_{\oplus, \nu}^{X} $$

$$ \mathrm{HRed}_{\sigma}^{X,r}(S) = \mathrm{HRed}_{\mathrm{hn}}^{X,r}(S) = \mathrm{HRed}_{\mathrm{n}}^{X,r}(S) = \{t \in \Lambda_{\oplus, \nu}^{X} \mid \forall \omega \in S \ \pi_{\omega}^{\omega}(t) \in \mathrm{HNV}_{\to}^{r}\} $$

$$ \mathrm{HRed}_{\sigma \to \tau}^{X,r}(S) = \{t \in \Lambda_{\oplus, \nu}^{X} \mid \forall S' \subseteq S, \forall s \in (0, 1], \forall u \in \mathrm{HRed}_{\sigma}^{X,1}(S'), \mathrm{tu} \in \mathrm{HRed}_{\tau}^{X,r}(S')\} $$

$$ \mathrm{HRed}_{\sigma \wedge \tau}^{X,r}(S) = \mathrm{HRed}_{\sigma}^{X,r}(S) \cap \mathrm{HRed}_{\tau}^{X,r}(S) $$

$$ \mathrm{HRed}_{Cq\sigma}^{X,r}(S) = \mathrm{HRed}_{\sigma}^{X,qr}(S) $$

$$ \mathrm{NRed}_{\llbracket}^{X,r}(S) = \mathrm{NRed}_{\mathrm{hn}}^{X,r}(S) = \Lambda_{\oplus, \nu}^{X} $$

$$ \mathrm{NRed}_{\sigma}^{X,r}(S) = \mathrm{NRed}_{\mathrm{n}}^{X,r}(S) = \{t \in \Lambda_{\oplus, \nu}^{X} \mid \forall \omega \in S \ \pi_{\omega}^{\omega}(t) \in \mathrm{NF}_{\to}^{r}\} $$

$$ \mathrm{NRed}_{\sigma \to \tau}^{X,r}(S) = \{t \in \Lambda_{\oplus, \nu}^{X} \mid \forall S' \subseteq S, \forall s \in (0, 1], \forall u \in \mathrm{NRed}_{\sigma}^{X,1}(S'), \mathrm{tu} \in \mathrm{NRed}_{\tau}^{X,r}(S')\} $$

$$ \mathrm{NRed}_{\sigma \wedge \tau}^{X,r}(S) = \mathrm{NRed}_{\sigma}^{X,r}(S) \cap \mathrm{NRed}_{\tau}^{X,r}(S) $$

$$ \mathrm{NRed}_{Cq\sigma}^{X,r}(S) = \mathrm{NRed}_{\sigma}^{X,qr}(S) $$

We will now establish a few properties of the families $\mathrm{HRed}_{\sigma}^{X,r}(S)$ and $\mathrm{NRed}_{\sigma}^{X,r}(S)$. Since the proofs for the two cases are similar, we will provide details only for the second case.
**Lemma E.20.** For any type $\sigma$ and $q, r \in [0, 1]$, if $q \ge r$, then

(i.) $\mathrm{HRed}_{\sigma}^{q}(S) \subseteq \mathrm{HRed}_{\sigma}^{r}(S)$.

(ii.) $\mathrm{NRed}_{\sigma}^{q}(S) \subseteq \mathrm{NRed}_{\sigma}^{r}(S)$.

*Proof.* We only prove case (ii.), the other one being proved in a similar way. By induction on $\sigma$:

* if $\sigma \in \{\emptyset, \mathbb{h}\}$, the claim is immediate;

* if $\sigma \in \{o, n\}$, then $t \in \mathrm{NRed}_{\sigma}^{q}(S)$ iff for all $\omega \in S$, $\pi_{X}^{\omega}(t) \in \mathrm{NF}_{\to}^{q} \subseteq \mathrm{NF}_{\to}^{r}$, so $t \in \mathrm{NRed}_{\sigma}^{r}(S)$;

* if $\sigma = (\tau \Rightarrow \rho)$ and $t \in \mathrm{NRed}_{\tau}^{X,q}(S)$ then for all $S' \subseteq S$, $u \in \mathrm{NRed}_{\tau}^{X,1}(S')$, $tu \in \mathrm{NRed}_{\rho}^{q}(S') \subseteq \mathrm{NRed}_{\rho}^{r}(S')$; hence we can conclude $t \in \mathrm{NRed}_{\sigma}^{r}(S)$;

* if $\sigma = \tau \wedge \rho$ and $t \in \mathrm{NRed}_{\sigma}^{X,q}(S)$, then by IH $t \in \mathrm{NRed}_{\tau}^{X,r}(S)$ and $t \in \mathrm{NRed}_{\rho}^{X,r}(S)$, so $t \in \mathrm{NRed}_{\sigma}^{X,r}(S)$;

* if $\sigma = C^s\tau$, then $\mathrm{NRed}_{\sigma}^{X,q}(S) = \mathrm{NRed}_{\tau}^{X,sq}(S) \stackrel{\text{[I.H.]}}{\subseteq} \mathrm{NRed}_{\tau}^{X,sr}(S) = \mathrm{NRed}_{\sigma}^{X,r}(S)$.

□

**Lemma E.21.** (i.) $\mathrm{HRed}_{\sigma}^{X,r}(\emptyset) = \{t \in \Lambda_{\oplus, v} | \mathrm{FN}(t) \subseteq X\}$;

(ii.) $\mathrm{NRed}_{\sigma}^{X,r}(\emptyset) = \{t \in \Lambda_{\oplus, v} | \mathrm{FN}(t) \subseteq X\}$.

*Proof.* We only prove (ii.) as (i.) is proved similarly. Let $\Lambda_{\oplus, v}^{X} = \{t \in \Lambda_{\oplus, v} | \mathrm{FN}(t) \subseteq X\}$. Observe that the inclusion $\mathrm{NRed}_{\sigma}^{X,r}(\emptyset) \subseteq \Lambda_{\oplus, v}^{X}$ is immediate. For the converse direction, we argue by induction on $\sigma$:

* if $\sigma \in \{\emptyset, \mathbb{h}\}$, the claim is immediate;

* If $\sigma \in \{o, n\}$, then trivially for all $\omega \in \emptyset$ and $t \in \Lambda_{\oplus, v}^{X}$, $\pi_{X}^{\omega}(t) \in \mathrm{NF}_{\to}^{r}$, so $\Lambda_{\oplus, v}^{X} \subseteq \mathrm{NRed}_{\sigma}^{X,r}(\emptyset)$.

* if $\sigma = \tau \Rightarrow \rho$, then for all $t \in \Lambda_{\oplus, v}^{X}$, and $u \in \mathrm{NRed}_{\tau}^{X,1}(\emptyset)$, $tu \in \Lambda_{\oplus, v}^{X}$, so by IH $tu \in \mathrm{NRed}_{\rho}^{X,r}(\emptyset)$. We can thus conclude that $t \in \mathrm{NRed}_{\sigma}^{X,r}(\emptyset)$.

* if $\sigma = \tau \wedge \rho$, then for all $t \in \Lambda_{\oplus, v}^{X}$, by IH $t \in \mathrm{NRed}_{\tau}^{X,r}(\emptyset)$ and $t \in \mathrm{NRed}_{\rho}^{X,r}(\emptyset)$, so $t \in \mathrm{NRed}_{\sigma}^{X,r}(\emptyset)$.

* If $\sigma = C^q\tau$, then by the I.H. $\Lambda_{\oplus, v}^{X} \subseteq \mathrm{NRed}_{\tau}^{X,qr}(\emptyset) = \mathrm{NRed}_{\sigma}^{X,q}(\emptyset)$.

□

**Lemma E.22.** (i.) $t \in \mathrm{HRed}_{\sigma}^{X,r}(S)$ iff for all $\omega \in S$, $\pi_{X}^{\omega}(t) \in \mathrm{HRed}_{\sigma}^{0,r}$;

(ii.) $t \in \mathrm{NRed}_{\sigma}^{X,r}(S)$ iff for all $\omega \in S$, $\pi_{X}^{\omega}(t) \in \mathrm{NRed}_{\sigma}^{0,r}$.

*Proof.* We only prove (ii.) as (i.) is proved similarly. We argue by induction on $\sigma$:

* if $\sigma \in \{\emptyset, \mathbb{h}\}$, the claim is immediate;

* If $\sigma \in \{o, n\}$, the claim follows from the definition.

* If $\sigma = \tau \Rightarrow \rho$, suppose $t \in \mathrm{NRed}_{\sigma}^{X,r}(S)$, let $\omega \in S$ and $u \in \mathrm{NRed}_{\sigma}^{0,1}$. Then $u$ is name-closed hence for all $g \in S$, $\pi^{g}(u) = u$, which by the IH, implies $u \in \mathrm{NRed}_{\rho}^{X,r}(S)$; we deduce then that $tu \in \mathrm{NRed}_{\rho}^{X,r}(S)$, so by IH $\pi_{X}^{\omega}(tu) = \pi_{X}^{\omega}(t)u \in \mathrm{NRed}_{\rho}^{0,r}$. By a similar argument we can show that for all $v \in \mathrm{NRed}_{\sigma}^{0,s}$, $\pi_{X}^{\omega}(\{t\}v) = \{\pi_{X}^{\omega}(t)\}v \in \mathrm{NRed}_{\rho}^{0,rs}$. We can thus conclude that $\pi_{X}^{\omega}(t) \in \mathrm{NRed}_{\sigma}^{0,r}$.

Conversely, suppose that for all $\omega \in S$, $\pi_{X}^{\omega}(t) \in \mathrm{NRed}_{\sigma}^{0,r}$, let $S' \subseteq S$ and $u \in \mathrm{NRed}_{\tau}^{X,1}(S')$; if $\omega \in S'$, then by IH $\pi_{X}^{\omega}(u) \in \mathrm{NRed}_{\tau}^{0,1}$, so $\pi_{X}^{\omega}(tu) = \pi_{X}^{\omega}(t)\pi_{X}^{\omega}(u) \in \mathrm{NRed}_{\rho}^{0,r}$; We have thus proved that for all $\omega \in S'$, $\pi_{X}^{\omega}(tu) \in \mathrm{NRed}_{\rho}^{0,r}$, which by IH implies that $tu \in \mathrm{NRed}_{\rho}^{X,r}(S')$ We conclude then that $t \in \mathrm{NRed}_{\sigma}^{X,r}(S)$.

* if $\sigma = \tau \wedge \rho$ then $t \in \mathrm{NRed}_{\sigma}^{X,r}(S)$ iff $t \in \mathrm{NRed}_{\tau}^{X,r}(S)$ and $t \in \mathrm{NRed}_{\rho}^{X,r}(S)$ iff (by the IH) for all $\omega \in S$, $\pi_{X}^{\omega}(t) \in \mathrm{NRed}_{\tau}^{X,r}(\emptyset)$ and $\pi_{X}^{\omega}(t) \in \mathrm{NRed}_{\rho}^{X,r}(\emptyset)$, iff for all $\omega \in S$, $\pi_{X}^{\omega}(t) \in \mathrm{NRed}_{\sigma}^{X,r}(\emptyset)$.

* If $\sigma = C^q\tau$, then $t \in \mathrm{NRed}_{\sigma}^{X,r}(S)$ iff $t \in \mathrm{NRed}_{\tau}^{X, rq}(S) \text{ iff } \forall \omega \in S \pi_{X}^{\omega}(t) \in \mathrm{NRed}_{\tau}^{X, rq} \text{ iff } \forall \omega \in S \pi_{X}^{\omega}(t) \in \mathrm{NRed}_{\sigma}^{X,r}$.

□

**Lemma E.23.** (i.) If $t \in \mathrm{HRed}_{\sigma}^{X,r}(S)$ and $t' \to_{\mathrm{p}} t$, then $t' \in \mathrm{HRed}_{\sigma}^{X,r}(S)$.

(ii.) If $t \in \mathrm{NRed}_{\sigma}^{X,r}(S)$ and $t' \to_{\mathrm{p}} t$, then $t' \in \mathrm{NRed}_{\sigma}^{X,r}(S)$.

*Proof.* By induction on $\sigma$.

□

**Lemma E.24.** For all terms $t, u_1, \dots, u_n$ with $\mathrm{FN}(t) \subseteq X \cup \{a\}$, $\mathrm{FN}(u_1), \dots, \mathrm{FN}(u_n) \subseteq X$, and measurable sets $S_1, \dots, S_{k+1} \subseteq (2^N)^{X \cup \{a\}}$ and $S' \subseteq (2^N)^X$, if

1. the $S_i$ are pairwise disjoint;

2. for all $\omega \in S_i$, $\pi_X^\omega(tu_1 \dots u_n) \in \mathrm{HNV}_{\to}^{r_i}$ (resp. $\pi_X^\omega(tu_1 \dots u_n) \in \mathrm{NF}_{\to}^{r_i}$);
3. for all $\omega \in S'$, $\mu(\Pi^\omega(S_i)) \ge s_i$;

then for all $\omega \in S'$, $\pi_X^\omega((va.t)u_1...u_n) \in \text{HNV}_{\to}^{\sum_{i=1}^{k+1} r_i s_i}$ (resp. $\pi_X^\omega((va.t)u_1...u_n) \in \text{NF}_{\to}^{\sum_{i=1}^{k+1} r_i s_i}$).

*Proof.* We only prove the claim in the case of $\text{NF}_{\to}$, the other case being proved similarly. Let us first consider the case where $n=0$. Let $\omega \in S'$. Since any term reduces to a (unique) PNF, we can suppose w.l.o.g. that the name-closed term $\pi_X^\omegava.t) = va.t^*$ is in PNF. Then by Corollary B.5 $t^*$ is a $(\mathcal{T}, a)$-tree of level $I_a(t^*)$. Observe that for all $\omega' \in (2^{\mathbb{N}})^{\{a\}}$, $\pi_{\{a\}}^{\omega'}(t^*) = \pi_{\{a\}}^{\omega'}(\pi_X^\omega(t)) = \pi_{X \cup \{a\}}^{\omega+\omega'}(t)$.

If $N$ is the cardinality of $\text{Supp}(t^*)$, by 3. and the fact that $s_i > 0$ we deduce that for all $i=1, \dots, k+1$ there exists a finite number $K_i$ of elements $w_{i1}, \dots, w_{iK_i}$ of $\text{Supp}(t^*)$ such that $\pi_{\{a\}}^{\omega_{ij}}(t^*) = w_{ij} \in \text{NF}_{\to}^{r_i}$ for some $\omega_{ij} \in (2^{\mathbb{N}})^{\{a\}}$ such that $\omega+\omega_{ij} \in S_i$, and using 3. we deduce that

$$ \sum_{w \in \text{NF}_{\to}^{r_i}} \mu\{\omega \mid \pi_{\{a\}}^{\omega}(t^*) = w\} \ge \sum_{j=1}^{K_i} \mu\{\omega \mid \pi_{\{a\}}^{\omega}(t^*) = w_{ij}\} \ge s_i $$

Now, by reducing, for all $i \le k+1$, each such term $w_{ij}$ inside $va.t$, to some PNF $w'_{ij} \in \text{NF}^{r_i}$, we obtain a new PNF $va.t^\#$ and we can compute (using the fact that $\sum_{u \in \text{HNV}} \mathcal{D}_{w'_{ij}}(u) \cdot \text{NF}(u) \ge r_i$):

$$
\begin{align*}
\text{NF}(va.t^\#) &= \sum_{u \in \text{HNV}} \mathcal{D}_{va.t^\#}(u) \cdot \text{NF}(u) \\
&= \sum_{u \in \text{HNV}} \left( \sum_{t' \in \text{Supp}(t^\#)} \mathcal{D}_{t'}(u) \cdot \mu\{\omega \mid \pi_{\{a\}}^{\omega}(t^\#) = t'\} \right) \cdot \text{NF}(u) \\
&= \sum_{u \in \text{HNV}} \left( \sum_{t' \in \text{Supp}(t^\#)} \mathcal{D}_{t'}(u) \cdot \text{NF}(u) \cdot \mu\{\omega \mid \pi_{\{a\}}^{\omega}(t^\#) = t'\} \right) \\
&= \sum_{t' \in \text{Supp}(t^\#)} \left( \sum_{u \in \text{HNV}} \mathcal{D}_{t'}(u) \cdot \text{NF}(u) \cdot \mu\{\omega \mid \pi_{\{a\}}^{\omega}(t^\#) = t'\} \right) \\
&= \sum_{t' \in \text{Supp}(t^\#)} \left( \sum_{u \in \text{HNV}} \mathcal{D}_{t'}(u) \cdot \text{NF}(u) \right) \cdot \mu\{\omega \mid \pi_{\{a\}}^{\omega}(t^\#) = t'\} \\
&\ge \sum_{i=1}^{k+1} \sum_{j=1}^{K_i} \left( \sum_{u \in \text{HNV}} \mathcal{D}_{w'_{ij}}(u) \cdot \text{NF}(u) \right) \cdot \mu\{\omega \mid \pi_{\{a\}}^{\omega}(t^\#) = w'_{ij}\} \\
&\ge \sum_{i=1}^{k+1} \sum_{j=1}^{K_i} r_i \cdot \mu\{\omega \mid \pi_{\{a\}}^{\omega}(t^\#) = w'_{ij}\} \\
&= \sum_{i=1}^{k+1} r_i \cdot \left( \sum_{j=1}^{K_i} \mu\{\omega \mid \pi_{\{a\}}^{\omega}(t^\#) = w'_{ij}\} \right) \\
&= \sum_{i=1}^{k+1} r_i \cdot \left( \sum_{j=1}^{K_i} \mu\{\omega \mid \pi_{\{a\}}^{\omega}(t^*) = w'_{ij}\} \right) \\
&\ge \sum_{i=1}^{k+1} r_i \cdot s_i
\end{align*}
$$

Now, from $va.t \xrightarrow{\{\}} va.t^\# \in \text{NF}^{\sum_i r_i s_i}$, we conclude $va.t \in \text{NF}_{\to}^{\sum_i r_i s_i}$.

For the case in which $n > 0$, we argue as follows: from the hypotheses we deduce by the first point that $va.(tu_1u_2...u_n) \in \text{NF}_{\to}^{\sum_i r_i s_i}$. We can then conclude by observing that $(va.t)u_1u_2...u_n \xrightarrow{p\{\}} va.(tu_1u_2...u_n)$. $\square$

**Lemma E.25.** For all types $\sigma$, terms $t, u_1, \dots, u_n$ with $\text{FN}(t) \subseteq X \cup \{a\}$, $\text{FN}(u_i) \subseteq X$, and measurable sets $S_1, \dots, S_{k+1} \subseteq (2^{\mathbb{N}})^{X \cup \{a\}}$ and $S' \subseteq (2^{\mathbb{N}})^X$, if

1. the $S_i$ are pairwise disjoint;

2. $tu_1...u_n \in \text{HRed}_{\sigma}^{X \cup \{a\}, r_i}(S_i)$ (resp. $tu_1...u_n \in \text{NRed}_{\sigma}^{X \cup \{a\}, r_i}(S_i)$), for all $i=1, \dots, k+1$;

3. for all $\omega \in S'$, $\mu(\Pi^\omega(S_i)) \ge s_i$;

then $(va.t)u_1...u_n \in \text{HRed}_{\sigma}^{X, \sum_{i=1}^{k+1} r_i s_i}(S')$ (resp. $(va.t)u_1...u_n \in \text{NRed}_{\sigma}^{X, \sum_{i=1}^{k+1} r_i s_i}(S')$).
*Proof.* We only prove the claim for NRed$_{\sigma}$, the other case being proved similarly. We argue by induction on $\sigma$:

* if $\sigma \in \{[\cdot], hn\}$, the claim is immediate;

* if $\sigma \in \{o, n\}$, then the claim follows from Lemma E.24.

* if $\sigma = \tau \Rightarrow \rho$, then let $S'' \subseteq S'$ and $u \in \text{NRed}_{\tau}^{X,1}(S'')$. For all $i$, since $s_i > 0$ for all $\omega \in S'' \subseteq S'$ there exists at least one $\omega' \in (2^{\mathbb{N}})^{\{a\}}$, such that $\omega + \omega' \in S_i$. Let $T_i = \{\omega + \omega' \in S_i | \omega \in S''\}$. The $T_i$ are pairwise disjoint and measurable, since they are counter-images of a measurable set through a measurable function (the projection function from $(2^{\mathbb{N}})^{X \cup \{a\}}$ to $(2^{\mathbb{N}})^X$).

We have that $u \in \text{NRed}_{\tau}^{X,1}(T_i)$, for all $i = 1, \dots, k+1$: for all $\omega + \omega' \in S''$, $\pi_{X \cup \{a\}}^{\omega+\omega'}(u) = \pi_X^{\omega}(u) \in \text{NRed}_{\tau}^{\emptyset,1}$, so by Lemma E.22, $u \in \text{NRed}_{\tau}^{X,1}(T_i)$. Since $T_i \subseteq S_i$, using the hypothesis 2. we deduce that $tu_1 \dots u_n u \in \text{NRed}_{\rho}^{X, r_i}(T_i)$; moreover, for all $\omega \in S''$, $\mu(\Pi^{\omega}(T_i)) = \mu(\Pi^{\omega}(S_i)) \ge s_i$. So, by the induction hypothesis $(va.t)u_1 \dots u_n u \in \text{NRed}_{\rho}^{X, \Sigma_i r_i s_i}(S'') = \text{NRed}_{\rho}^{X, \Sigma_i r_i s_i}(S'')$. We can thus conclude that $(va.t)u_1 \dots u_n \in \text{NRed}_{\sigma}^{X, \Sigma_i r_i s_i}(S')$.

* $\sigma = \tau \wedge \rho$, then from the hypotheses by IH we deduce $(va.t)u_1 \dots u_n \in \text{NRed}_{\tau}^{X, \Sigma r_i s_i}(S')$ and $(va.t)u_1 \dots u_n \in \text{NRed}_{\rho}^{X, \Sigma r_i s_i}(S')$, and thus $(va.t)u_1 \dots u_n \in \text{NRed}_{\sigma}^{X, \Sigma r_i s_i}(S')$.

* if $\sigma = C^q \tau$, the claim follows from the induction hypothesis.

**Lemma E.26.** (i.) $t[u/x]u_1 \dots u_n \in \text{HRed}_{\sigma}^{X,r}(S) \Rightarrow (\lambda x.t)uu_1 \dots u_n \in \text{HRed}_{\sigma}^{X,r}(S)$.

(ii.) $t[u/x]u_1 \dots u_n \in \text{NRed}_{\sigma}^{X,r}(S) \Rightarrow (\lambda x.t)uu_1 \dots u_n \in \text{NRed}_{\sigma}^{X,r}(S)$.

*Proof.* We only prove claim (ii.) as claim (i.) is proved similarly. By induction on $\sigma$:

* if $\sigma \in \{[\cdot], hn\}$, the claim is immediate;

* If $\sigma \in \{o, n\}$, then if $t[u/x]u_1 \dots u_n \in \text{NRed}_{\sigma}^{X,r}(S)$, then for all $\omega \in S$, $\pi_X^{\omega}(t[u/x]u_1 \dots u_n) = \pi_X^{\omega}(t)[\pi_X^{\omega}(u)/x]\pi_X^{\omega}(u_1) \dots \pi_X^{\omega}(u_n) \in \text{NRed}_{\tau}^{r}$. Since the reduction tree of $\pi_X^{\omega}(t'')$, where $t'' = (\lambda x.t)uu_1 \dots u_n$, is contained in that of $\pi_X^{\omega}(t[u/x]u_1 \dots u_n)$, we deduce $\pi_X^{\omega}(t'') \in \text{NF}^r$, and we conclude that $t'' \in \text{NRed}_{\sigma}^{X,r}(S)$.

* If $\sigma = \tau \Rightarrow \rho$, then let $S' \subseteq S$ and $v \in \text{NRed}_{\tau}^{X,1}(S')$; then $t[u/x]u_1 \dots u_n v \in \text{NRed}_{\rho}^{X,r}(S')$ so by IH $(\lambda x.t)uu_1 \dots u_n v \in \text{NRed}_{\rho}^{X,r}(S')$. This proves in particular that $(\lambda x.t)uu_1 \dots u_n \in \text{NRed}_{\sigma}^{X,r}(S)$.

* If $\sigma = \tau \wedge \rho$ and $t[u/x]u_1 \dots u_n \in \text{NRed}_{\sigma}^{X,r}(S)$, then $t[u/x]u_1 \dots u_n \in \text{NRed}_{\tau}^{X,r}(S)$ and $t[u/x]u_1 \dots u_n \in \text{NRed}_{\tau}^{X,r}(S)$, so by IH $(\lambda x.t)uu_1 \dots u_n \in \text{NRed}_{\tau}^{X,r}(S)$ and $(\lambda x.t)uu_1 \dots u_n \in \text{NRed}_{\rho}^{X,r}(S)$, which implies $(\lambda x.t)uu_1 \dots u_n \in \text{NRed}_{\sigma}^{X,r}(S)$.

* If $\sigma = C^q \tau$, then if $t[u/x]u_1 \dots u_n \in \text{NRed}_{\sigma}^{X,r}(S) = \text{NRed}_{\tau}^{X,rq}(S)$, then by I.H. $(\lambda x.t)uu_1 \dots u_n \in \text{NRed}_{\tau}^{X,rq}(S) = \text{NRed}_{\sigma}^{X,r}(S)$.

**Lemma E.27.** For all $t$ such that $\text{FN}(t) \subseteq X$ and measurable sets $S, S' \subseteq (2^{\mathbb{N}})^X$,

(i.) If for all $S'' \subseteq S'$ and $u \in \text{HRed}_{\sigma}^{X,s}(S'')$, $t[u/x] \in \text{NRed}_{\tau}^{X,rs}(S \cap S'')$, then $\lambda x.t \in \text{NRed}_{\sigma \Rightarrow \tau}^{X,r}(S \cap S')$.

(ii.) If for all $S'' \subseteq S'$ and $u \in \text{NRed}_{\sigma}^{X,s}(S'')$, $t[u/x] \in \text{NRed}_{\tau}^{X,rs}(S \cap S'')$, then $\lambda x.t \in \text{NRed}_{\sigma \Rightarrow \tau}^{X,r}(S \cap S')$.

*Proof.* As usual, we only prove claim (ii.). Let $T \subseteq S \cap S'$ and $u \in \text{NRed}_{\sigma}^{X,s}(T)$. Then, by hypothesis, $t[u/x] \in \text{NRed}_{\tau}^{X,rs}(S \cap T) = \text{NRed}_{\tau}^{X,rs}(S \cap S')$ and we conclude by Lemma E.26 that $(\lambda x.t)u \in \text{NRed}_{\tau}^{X,rs}(S \cap S')$. This proves that $\lambda x.t \in \text{NRed}_{\sigma \Rightarrow \tau}^{X,r}(S \cap S')$.

**Lemma E.28.** For any two types $s$, $t$ of $C\lambda_{\rightarrow, \cap}$, if $s \le t$, then for all $S \subseteq (2^{\mathbb{N}})^X$,

(i.) $\text{HRed}_{\sigma}^{X,r}(S) \subseteq \text{HRed}_{\tau}^{X,r}(S)$;

(ii.) $\text{NRed}_{\sigma}^{X,r}(S) \subseteq \text{NRed}_{\tau}^{X,r}(S)$.

*Proof.* As usual, we only prove claim (ii.). We argue by induction on $s$:

* if $s \in \{[\cdot], o, hn, n\}$, then it must be $s = t$, so the claim is immediate.

* If $s = [\mathfrak{R}_1, \dots, \mathfrak{R}_n] \Rightarrow s'$, then $t = [\mathfrak{R}_1, \dots, \mathfrak{R}_m] \Rightarrow t'$, where $s' \le t'$, and $s_i \ge t_{f(i)}$ holds for some injective function $f: \{1, \dots, n\} \to \{1, \dots, m\}$. By the I.H. we have then that $\text{NRed}_{s'}^{X,r}(S) \subseteq \text{NRed}_{t'}^{X,r}(S)$ and $\text{NRed}_{t_{f(i)}}^{X,1}(S') \subseteq \text{NRed}_{s_i}^{X,1}(S')$; by the definition of $\text{NRed}_{s'}^{X,r}(S)$ this implies then $\text{NRed}_{s'}^{X,r}(S) \subseteq \text{NRed}_{t'}^{X,r}(S)$.

* if $s = C^q s'$, then it must be $t = C^s t'$, with $s' \le t'$ and $q \ge s$; then by IH and Lemma E.20 we have $\text{NRed}_{s'}^{X,r}(S) = \text{NRed}_{s'}^{X,qr}(S) \subseteq \text{NRed}_{s'}^{X,sr}(S) \subseteq \text{NRed}_{t'}^{X,sr}(S) = \text{NRed}_{t'}^{X,r}(S)$.

We now show how the two families of reducibility candidates differ on the kind of normalization properties they warrant. Let us introduce a (first) notion of *neutral term* for $\Lambda_{\text{PE}}$:
**Definition E.29** (neutral terms, version 1). For any measurable set $S \subseteq (2^N)^X$, the set Neut($S$) is defined by induction as follows:

* for any variable $x$, $x \in \text{Neut}(S)$;

* if $t \in \text{Neut}(S)$ then for all $u \in \Lambda_{\oplus, \nu}^X$, $tu \in \text{Neut}(S)$.

It is easily checked that for all $t \in \text{Neut}(S)$ and $\omega \in S$, $\text{HNV}(\pi_X^\omega(t)) = 1$.

Probabilistic neutral terms can be used to show that reducible terms reduce to a probabilistic head normal form.

**Definition E.30** (non-trivial type). The set of *non-trivial types* is defined by induction as follows:

* $o, hn, n$ are non-trivial;

* if $\tau$ is non-trivial, $\sigma \Rightarrow \tau$ is non-trivial;

* if either $\sigma$ or $\tau$ are non-trivial, $\sigma \wedge \tau$ is non-trivial;

* if $\sigma$ is non-trivial, $C^q\sigma$ is non-trivial.

**Lemma E.31.** For any type $\sigma$:

1. if $\sigma$ is non-trivial and $t \in \text{HRed}_{\sigma}^{X,r}(S)$ and $\omega \in S$, then $\pi_X^{\omega}(t) \in \text{HNV}_{\to}^{[\sigma]\cdot r}$;

2. $\text{Neut}(S) \subseteq \text{HRed}_{\sigma}^{X,1}(S)$.

*Proof.* We argue by induction on $\sigma$:

* if $\sigma = []$, then both claims are immediate;

* if $\sigma \in \{o, hn, n\}$ then by definition $t \in \text{HRed}_{\sigma}^{X,r}(S)$ iff for any $\omega \in S$, $\pi_X^{\omega}(t) \in \text{HNV}_{\to}^r = \text{HNV}_{\to}^{[\sigma]\cdot r}$. Moreover, if $t \in \text{Neut}(S)$, then $\text{HNV}(t) = 1$, so $t \in \text{HRed}_{\sigma}^{X,1}(S)$.

* if $\sigma = \tau \Rightarrow \rho$ and $t \in \text{HRed}_{\sigma}^{X,r}(S)$, then by IH $x \in \text{HRed}_{\tau}^{X,1}(S)$, hence $tx \in \text{HRed}_{\tau}^{X,r}(S)$, and again by IH for all $\omega \in S$ $\pi_X^{\omega}(tx) = \pi_X^{\omega}(t)x \in \text{HNV}_{\to}^{[\tau]\cdot r} = \text{HNV}_{\to}^{[\sigma]\cdot r}$, and thus $\pi_X^{\omega}(t) \in \text{HNV}_{\to}^{[\sigma]\cdot r}$.

Moreover, if $t \in \text{Neut}(S)$, let $S' \subseteq S$ and $u \in \text{HRed}_{\tau}^{X,1}(S)$, then by IH for all $\omega \in S'$, $\pi^{\omega}(u) \in \text{HNV}_{\to}^{[\tau]}$ and thus $tu \in \text{Neut}(S')$, so by IH $tu \in \text{HRed}_{\rho}^{X,1}(S') \subseteq \text{HRed}_{\rho}^{X,r}(S')$; we can thus conclude that $t \in \text{HRed}_{\sigma}^{X,1}(S)$.

* if $\sigma = \tau \wedge \rho$ and $t \in \text{HRed}_{\sigma}^{X,r}(S)$, then $t \in \text{HRed}_{\tau}^{X,r}(S)$ and $t \in \text{HRed}_{\rho}^{X,r}(S)$, so by IH for all $\omega \in S$, $\pi_X^{\omega}(t) \in \text{HNV}_{\to}^{[\tau]\cdot r}$ and $\pi_X^{\omega}(t) \in \text{HNV}_{\to}^{[\rho]\cdot r}$; hence we deduce that for all $\omega \in S$ $\pi_X^{\omega}(t) \in \text{HNV}_{\to}^{\max\{[\tau],[\rho]\}\cdot r} = \text{HNV}_{\to}^{[\sigma]\cdot r}$.

Moreover, if $t \in \text{Neut}(S)$, then by IH $t \in \text{HRed}_{\sigma}^{X,1}(S)$ and $t \in \text{HRed}_{\rho}^{X,1}(S)$, so $t \in \text{HRed}_{\sigma}^{X,1}(S)$.

* if $\sigma = C^s\tau$ and $t \in \text{HRed}_{\sigma}^{X,q}(S) = \text{HRed}_{\tau}^{X,qS}(S)$, then by IH for all $\omega \in S$, $\pi_X^{\omega}(t) \in \text{HNV}_{\to}^{[\tau]qS} = \text{HNV}_{\to}^{[\sigma]q}$. Moreover, if $t \in \text{Neut}(S)$, then by IH $t \in \text{HRed}_{\tau}^{X,1}(S) \subseteq \text{HRed}_{\tau}^{X,s}(S) = \text{HRed}_{\sigma}^{X,1}(S)$.

□

To establish a result like Lemma E.31 for the family $\text{NRed}_{\sigma}^{X,r}(S)$, as discussed in Section 6, we need to restrict to balanced types. For our general class of types, these are defined as follows:

**Definition E.32.** The set $\text{Bal}$ of balanced types is defined inductively as follows:

* $C^{\bar{q}}\sigma$, for $\sigma \in \{o, hn, n\}$;

* if $\sigma, \tau \in \text{Bal}, \sigma \wedge \tau \in \text{Bal}$;

* if $\sigma_1, \dots, \sigma_n \in \text{Bal}$ and $\prod_{i=1}^k q_i \le \prod_{j=1}^n [\sigma_j]$, then $C^{q_1} \dots C^{q_n} (\sigma_1 \Rightarrow \dots \Rightarrow \sigma_n \Rightarrow o) \in \text{Bal}$.

For instance, the type $C^{\frac{1}{2}}(C^{\frac{1}{2}}o \Rightarrow o)$ is balanced, while $C^1(C^{\frac{1}{2}}o \Rightarrow o)$ is not.

One can check that any balanced type is also non-trivial.

To study normalization for balanced types we need a more refined notion of neutral term.

**Definition E.33** (neutral terms, version 2). For any $q \in (0, 1]$, and measurable set $S$, the set $\text{Neut}^q(S)$ is defined by induction as follows:

* for any variable $x$, $x \in \text{Neut}^q(S)$;

* if $t \in \text{Neut}^q(S)$ and for all $\omega \in S$, $\text{NF}_{\to}(\pi_X^\omega(u)) \ge s$, then $tu \in \text{Neut}^{qs}(S)$.

It is easily checked that for all $t \in \text{Neut}^q(S)$ and $\omega \in S$, $\text{NF}_{\to}(\pi_X^\omega(t)) \ge q$.

**Lemma E.34.** For any balanced and $\{[]$, $hn\}$-free type $\sigma$:

1. if $t \in \text{NRed}_{\sigma}^{X,r}(S)$ and $\omega \in S$, then $\pi_X^{\omega}(S) \in \text{NF}_{\to}^{[\sigma]\cdot r}$;

2. $\text{Neut}^q(S) \subseteq \text{NRed}_{\sigma}^{X,q}(S)$.

*Proof.* We argue by induction on $s$:
• if $\sigma = C^{q_1} \dots C^{q_k} \tau$, with $\tau \in \{0, n\}$, then by definition $t \in \text{NRed}_{\sigma}^{X,r}(S)$ iff for all $\omega \in S$, $\pi_X^{\omega}(t) \in \text{NF}_{\to}^{q_1 \dots q_k r} = \text{NF}^{[o] \cdot r}$. Moreover if $t \in \text{Neut}^q(S)$, then for all $\omega \in S$, $\text{NF}_{\to}(\pi_X^{\omega}(t)) \ge q$, hence $t \in \text{NRed}_o^{X,q}(S) \subseteq \text{NRed}_{\sigma}^{X,q[\sigma]}(S)$.

• if $\sigma = \tau \wedge \rho$, then we can argue as in the corresponding point in the proof of Lemma E.31.

• if $\sigma = C^{q_1} \dots C^{q_k}(\sigma_1 \Rightarrow \dots \Rightarrow \sigma_n \Rightarrow o)$, where $\prod_i q_i \le \prod_j [\sigma_j]$, and $t \in \text{NRed}_{\sigma}^{X,r}(S)$, then by IH $x_j \in \text{Neut}^1(S) \subseteq \text{NRed}_{\sigma_i}^{X,1}(S)$, and thus $tx_1 \dots x_n \in \text{NRed}_o^{rq_1 \dots q_k}(S)$, so for all $\omega \in S$, $\pi_X^{\omega}(tx_1 \dots x_n) = \pi_X^{\omega}(t)x_1 \dots x_n \in \text{NF}_{\to}^{rq_1 \dots q_k} \subseteq \text{NF}_{\to}^{rq_1 \dots q_n \prod_j [\sigma_j]} = \text{NF}_{\to}^{[\sigma]r}$. We deduce then $\pi_X^{\omega}(t) \in \text{NF}_{\to}^{[\sigma]r}$ by applying Lemma E.19 a finite number of times.
Moreover, if $t \in \text{Neut}^q(S)$, $S' \subseteq S$, $\omega \in S'$, and $u_j \in \text{NRed}_{\sigma_j}^{X,1}(S')$, then by the IH for all $\omega \in S'$, $\pi_X^{\omega}(u_j) \in \text{NF}_{\to}^{[\sigma_j]}$, so $tu_1 \dots u_n \in \text{Neut}^q \prod_k [\sigma_j] (S') \subseteq \text{Neut}^{qq_1 \dots q_k}(S')$; by the IH it follows then $tu_1 \dots u_n \in \text{NRed}_o^{X,q_1 \dots q_k s}(S')$. We can thus conclude $t \in \text{NRed}_{\sigma}^{X,q_1 \dots q_k}(S) = \text{NRed}_{\sigma}^{X,q}(S)$.
□

The last ingredient of our reducibility argument is the following:

**Proposition E.35.** If $\Gamma \vdash^X t : \mathfrak{b} \mapsto s$ is derivable in $C\lambda_{\to, \cap}$, where $\Gamma = \{x_1 : \mathfrak{M}_1, \dots, x_m : \mathfrak{M}_n\}$, then for all $S \subseteq [[\mathfrak{b}]_X$, the following two claims hold:

(i.) for all $u_i \in \text{NRed}_{\mathfrak{M}_i}^{X,1}(S)$, $t[u_1/x_1, \dots, u_m/x_m] \in \text{NRed}_s^{X,1}(S)$;

(ii.) for all $u_i \in \text{NRed}_{\mathfrak{M}_i}^{X,1}(S)$, $t[u_1/x_1, \dots, u_m/x_m] \in \text{NRed}_s^{X,1}(S)$.

*Proof.* We only prove claim (ii.). The argument is by induction on a type derivation of t:

• if $t = x$ and the last rule is

$$ \frac{s_i \le t \quad \text{FN}(\mathfrak{b}) \subseteq X}{\Gamma, x : [s_1, \dots, s_n] \vdash^X x : \mathfrak{b} \to t} \quad (\text{id}_\cap) $$

Then for all $S \subseteq [[\mathfrak{b}]_X$, and for all $u_1 \in \text{NRed}_{\mathfrak{M}_1}^{X,1}(S), \dots, u_n \in \text{NRed}_{\mathfrak{M}_n}^{X,1}(S)$, and $u \in \text{NRed}_{\mathfrak{M}_i}^{X,1}(S)$, using Lemma E.28 we deduce $u \in \text{NRed}_{s_i}^{X,1}(S) \subseteq \text{NRed}_t^{X,1}(S)$, whence $t[u_1/x_1, \dots, u_n/x_n, u/x] = u \in \text{NRed}_t^{X,1}([[\mathfrak{b}]_X \cap S) = \text{NRed}_s^{X,1}(S)$.

• if the last rule is

$$ \frac{\{\Gamma \vdash^X t : \mathfrak{b} \to s\}_{j=1,\dots,k} \quad \mathfrak{b} \models^X \bigvee_j \mathfrak{b}_j}{\Gamma \vdash^X t : \mathfrak{b} \to s} \quad (\vee) $$

then by IH, for all $j = 1, \dots, k$, $S \subseteq [[\mathfrak{b}]_X$, for all $u_1 \in \text{NRed}_{\mathfrak{M}_1}^{X,1}(S), \dots, u_n \in \text{NRed}_{\mathfrak{M}_n}^{X,1}(S)$ and for all $\omega \in S$, $\pi_X^{\omega}(t[u_1/x_1, \dots, u_n/x_n]) \in \text{NRed}_{\rho}^{\emptyset, 1}$.

If $k = 0$, then $\mathfrak{b} \vdash \bigvee_j \mathfrak{b}_j = \perp$, so the claim trivially holds. Let then $k > 0$. Let $S \subseteq [[\mathfrak{b}]_X \subseteq [[\bigvee_j \mathfrak{b}_j]]_X = \bigcup_i [[\mathfrak{b}_j]]_X$ and $\omega \in S$. Then $f \in [[\mathfrak{b}]_X$, for some $j \le k$. Then first observe that from $u_i \in \text{NRed}_{\mathfrak{M}_i}^{X,q_i}(S)$ it follows in particular that $u_i \in \text{NRed}_{\mathfrak{M}_i}^{X,1}(S \cap [[\mathfrak{b}]_X])$: for all $\omega \in S \cap [[\mathfrak{b}]_X$, since $\omega \in S$, $\pi_X^{\omega}(u_i) \in \text{NRed}_{\mathfrak{M}_i}^{\emptyset, 1}$, so by Lemma E.22 we conclude that $u_i \in \text{NRed}_{\mathfrak{M}_i}^{X,1}(S \cap [[\mathfrak{b}]_X])$. Hence we deduce that $\pi_X^{\omega}(t[u_1/x_1, \dots, u_n/x_n]) \in \text{NRed}_s^{\emptyset, q_1 \dots q_n}$, and again by Lemma E.22 we conclude $t[u_1/x_1, \dots, u_n/x_n] \in \text{NRed}_s^{X,1}(S)$.

• if $t = t_1 \oplus_a^i t_2$, and the last rule is

$$ \frac{\Gamma \vdash^X t_1 : \mathfrak{b} \to s \quad c \models (\neg x_a^i \wedge \mathfrak{b})}{\Gamma \vdash^X t_1 \oplus_a^i t_2 : c \to s} \quad (\oplus l) $$

By IH and Lemma E.22, for all $S \subseteq [[\mathfrak{b}]_X$, $\omega \in S$, $u_1 \in \text{NRed}_{\mathfrak{M}_1}^{X,1}(S), \dots, u_n \in \text{NRed}_{\mathfrak{M}_n}^{X,1}(S)$, $\pi_X^{\omega}(t_1[u_1/x_1, \dots, u_n/x_n]) \in \text{NRed}_s^{\emptyset, 1}$. Let now $S \subseteq [[c]_X \subseteq [[x_a^i]_X \wedge [[\mathfrak{b}]_X]$ and $u_1 \in \text{NRed}_{\mathfrak{M}_1}^{X,1}(S), \dots, u_n \in \text{NRed}_{\mathfrak{M}_n}^{X,1}(S)$. If now $\omega \in S \subseteq [[c]_{X \cup \{a\}})$, then $\omega(a)(i) = 0$ so in particular $\pi_X^{\omega}(t[u_1/x_1, \dots, u_n/x_n]) = \pi_X^{\omega}(t_1[u_1/x_1, \dots, u_n/x_n]) \in \text{NRed}_s^{\emptyset, 1}$. Hence, using Lemma E.22 we conclude that $t[u_1/x_1, \dots, u_n/x_n] \in \text{NRed}_s^{X,1}(S)$.

• if $t = t_1 \oplus_a^i t_2$, and the last rule is

$$ \frac{\Gamma \vdash^X t_2 : \mathfrak{b} \to s \quad c \models (\neg x_a^i \wedge \mathfrak{b})}{\Gamma \vdash^X t_1 \oplus_a^i t_2 : c \to s} \quad (\oplus r) $$

then we can argue similarly to the previous case.

• if the last rule is

$$ \frac{\Gamma \vdash^X t : \mathfrak{b} \to C^q \sigma}{\Gamma \vdash^X t : \mathfrak{b} \to C^q \text{hn}} \quad (\text{hn}) $$
then by IH for all $S \subseteq [[\mathfrak{b}]_X$, for all $u_1 \in \text{NRed}_{\mathfrak{M}_1}^{X,1}(S), \dots, u_n \in \text{NRed}_{\mathfrak{M}_n}^{X,1}(S)$, $\pi_X^\omega(t[u_1/x_1, \dots, t_n/x_n]) \in \text{NRed}_\sigma^{\theta,q}$, so by Lemma E.31, HNV$(\pi_X^\omega(t[u_1/x_1, \dots, t_n/x_n])) \ge q \cdot [\sigma] = q$, which implies $t[u_1/x_1, \dots, t_n/x_n] \in \text{NRed}_{\text{hn}}^{X,q}(S)$.

* if the last rule is

$$ \frac{\Gamma \vdash^X t : \mathfrak{b} \to C^q \sigma \quad \sigma \text{ safe}}{\Gamma \vdash^X t : \mathfrak{b} \to C^q \mathfrak{n}} (n) $$

then $\sigma$ is $\{[\cdot], \text{hn}\}$-free and balanced; by IH for all $S \subseteq [[\mathfrak{b}]_X$, for all $u_1 \in \text{NRed}_{\mathfrak{M}_1}^{X,1}(S), \dots, u_n \in \text{NRed}_{\mathfrak{M}_n}^{X,1}(S)$, $\pi_X^\omega(t[u_1/x_1, \dots, t_n/x_n]) \in \text{NRed}_\sigma^{\theta,q}$; furthermore, by Lemma E.34, $\text{NF}_{\to}(\pi_X^\omega(t[u_1/x_1, \dots, t_n/x_n])) \ge q \cdot [\sigma] = q$, which implies $t[u_1/x_1, \dots, t_n/x_n] \in \text{NRed}_n^{X,q}(S)$.

* if $t = \lambda x.u$ and the last rule is

$$ \frac{\Gamma, x : \mathfrak{M} \vdash^X u : \mathfrak{b} \to C^\bar{s} \tau}{\Gamma \vdash^X \lambda x.u : \mathfrak{b} \to C^\bar{s}(\mathfrak{M} \Rightarrow \tau)} (\lambda) $$

where $\bar{s} = s_1, \dots, s_l$; then, by IH, for all $S \subseteq [[\mathfrak{b}]_X$, for all $u_1 \in \text{NRed}_{\mathfrak{M}_1}^{X,1}(S), \dots, u_n \in \text{NRed}_{\mathfrak{M}_n}^{X,1}(S)$, and $v \in \text{NRed}_{\mathfrak{M}}^{X,1}(S)$, $u[u_1/x_1, \dots, u_n/x_n, v/x] \in \text{NRed}_{C^\bar{s} \tau}^{X,1}(S) = \text{NRed}_\tau^{X,s_1 \dots s_k}(S)$. In particular, for all choice of $u_1, \dots, u_n$ and variable $y$ not occurring free in $u_1, \dots, u_n$, by letting $t' = u[u_1/x_1, \dots, u_n/x_n, y/x]$, we have that for all $v \in \text{NRed}_{\mathfrak{M}}^{X,1}(S \cap [[\mathfrak{b}]_X)$, $t'[v/y] = u[u_1/x_1, \dots, u_n/x_n, v/x] \in \text{NRed}_\tau^{X,s_1 \dots s_k}(S)$. By Lemma E.27, then, we can conclude that $\lambda y.t' = (\lambda y.t[y/x])[u_1/x_1, \dots, u_n/x_n] = (\lambda x.t)[u_1/x_1, \dots, u_n/x_n] \in \text{NRed}_{\mathfrak{M} \Rightarrow \sigma}^{X,s_1 \dots s_k}(S) = \text{NRed}_{C^\bar{s}(\mathfrak{M} \Rightarrow \sigma)}^{X,1}(S)$.

* $t = uv$ and the last rule is

$$ \frac{\Gamma \vdash^X u : c \to C^\bar{s}(\mathfrak{M} \Rightarrow \sigma) \qquad \{\Gamma \vdash^X v : d_i \to s_i\}_i \qquad \mathfrak{b} \models c \wedge (\bigwedge_i d_i)}{\Gamma \vdash^X uv : \mathfrak{b} \to C^\bar{s} \sigma} (@) $$

where $\bar{s} = s_1, \dots, s_k$ and $\mathcal{M} = [s_1, \dots, s_n]$, then by IH for all $S \subseteq [[\mathfrak{b}]_X \subseteq [[c]]_X \cap \bigcap_i [d_i]]_X$ and $u_1 \in \text{NRed}_{\mathfrak{M}_1}^{X,1}(S), \dots, u_n \in \text{NRed}_{\mathfrak{M}_n}^{X,1}(S)$, $u[u_1/x, \dots, u_n/x] \in \text{NRed}_{\mathfrak{M} \Rightarrow \sigma}^{X,s_1 \dots s_k}(S)$ and $v[u_1/x, \dots, u_n/x] \in \bigcap_i \text{NRed}_{s_i}^{X,1}(S) = \text{NRed}_{\mathfrak{M}}^{X,1}(S)$ (where, if $n=0$, $v[u_1/x, \dots, u_n/x] \in \text{NRed}_{\mathfrak{M}}^{X,1}(S)$ does not follow from the induction hypothesis but from the fact that $\text{NRed}_{[\cdot]}^{X,1}(S) = \Lambda_{\oplus, \nu}^X$) so we deduce $u[u_1/x, \dots, u_n/x]v[u_1/x, \dots, u_n/x] = (uv)[u_1/x, \dots, u_n/x] \in \text{NRed}_\sigma^{X,s_1 \dots s_k}(S) = \text{NRed}_{C^\bar{s} \sigma}^{X,1}(S)$.

* If $t = va.u$ and the last rule is

$$ \frac{\{\Gamma \vdash^{X \cup \{a\}} u : c \wedge d_i \to C^{q_j} \sigma\}_{j=1,\dots,n+1} \quad \vdash \mu(d_j) \ge r_j \quad \mathfrak{b} \models c}{\Gamma \vdash^X va.u : \mathfrak{b} \to C^{\Sigma_j r_j q_j} \sigma} (\mu) $$

where $a \notin \text{FV}(\Gamma) \cup \text{FV}(c)$, then let $S \subseteq [[\mathfrak{b}]_X \subseteq [[c]]_X$ and $u_1 \in \text{NRed}_{\mathfrak{M}_1}^{X,1}(S), \dots, u_n \in \text{NRed}_{\mathfrak{M}_n}^{X,1}(S)$. Let $T = \{\omega + \omega' | \omega \in S\} \subseteq (2^N)^{X \cup \{a\}}$, which is measurable since counter-image of a measurable set through the projection function; then since $\text{FN}(u_i) \subseteq X$, we deduce using Lemma E.22 that $u_i \in \text{NRed}_{\mathfrak{M}_i}^{X \cup \{a\},1}(T \cap [[d_j]]_{X \cup \{a\}})$. By IH and the hypothesis we deduce then that

* the sets $[[d_j]]_{X \cup \{a\}}$ are pairwise disjoint;

* $u[u_1/x_1, \dots, u_n/x_n] \in \text{NRed}_s^{X \cup \{a\},1}(T \cap [[d_j]]_{X \cup \{a\}})$;

* for all $\omega \in S$, $\mu(\Pi^\omega(T \cap [[d_j]]_{X \cup \{a\}})) \ge r_j$;

Hence, by Lemma E.25 we conclude that $va.u[u_1/x_1, \dots, u_n/x_n] = (va.u)[u_1/x_1, \dots, u_n/x_n] \in \text{NRed}_s^{X, \Sigma_j r_j q_j}(S) = \text{NRed}_{C^{\Sigma_j r_j q_j}}^{X,1}(S)$. $\square$

From Proposition E.35 (i.) and Lemma E.31, by observing that any type of $C\lambda_{\to, \cap}$ is non-trivial, we deduce the following, which generalizes the first part of Theorem 6.1.

**Theorem E.36.** If $\Gamma \vdash t : \mathfrak{b} \to C^q \sigma$ holds in $C\lambda_{\to, \cap}$, then for all $\omega \in [[\mathfrak{b}]_X$, HNV$_{\to}(\pi_X^\omega(t)) \ge q$.

From Proposition E.35 (i.) and Lemma E.34 we similarly deduce a generalization of Theorem 6.3:

**Theorem E.37.** If $\Gamma \vdash^X t : \mathfrak{b} \to C^q \sigma$ holds in $C\lambda_{\to, \cap}$, where $\Gamma$ and $s$ are formed of balanced types, then for all $\omega \in [[\mathfrak{b}]_X$, $\text{NF}_{\to}(\pi_X^\omega(t)) \ge q$.

From the two results above we can finally deduce the soundness part of Theorem 6.6:

**Corollary E.38.** For any closed term $t$,

$$ \text{HNV}_{\to}(t) \ge \sup\{q \mid \vdash t : \mathfrak{t} \to C^q \mathfrak{h} n\} $$

$$ \text{NF}_{\to}(t) \ge \sup\{q \mid \vdash t : \mathfrak{t} \to C^q \mathfrak{n}\} $$
### E.3 Probabilistic Reducibility Candidates for $\Lambda_{\text{PE}}^{\{\}}$.

We now show how to adapt the family of reducibility candidates $H\text{Red}_{\sigma}^{X,1}(S)$ to $\Lambda_{\text{PE}}^{\{\}}$, in order to prove the second part of Theorem 6.1. We will still work with the general family of types from the previous section (hence suggesting that intersection types could be added to $C\lambda_{\to}^{\{\}}$, too).

For any $t \in \mathcal{T}$, let $\mathcal{D}_t^1: \mathcal{T} \to [0, 1]$ be $\delta_t$ if $t \in \text{HNV}$, and if $t = \text{va.t'}$, let

$$ \mathcal{D}_t^1(u) = \mu\{\omega \in 2^{\mathbb{N}} | \pi_{\{a\}}^{\omega}(t') = u\} $$

By recalling the definition of head-reduction in $\Lambda_{\text{PE}}^{\{\}}$ from Subsection B.2, one can easily check the following useful properties:

**Lemma E.39.** (i.) If $t \to_{\{\}}^* u$, then $\pi_X^\omega(t) \to_{\{\}}^* \pi_X^\omega(u)$.

(ii.) If $t \to_{\{\}}^* u$, then $\text{HNV}(t) \ge \text{HNV}(u)$.

**Lemma E.40.** For all $t, u, w \in \mathcal{T}$, $\mathcal{D}_t^1(u) = \mathcal{D}_{tw}^1(uw)$.

*Proof.* If $t$ is a HNV, $tw$ is a pseudo-value, so $\mathcal{D}_t^1 = \delta_t$ and $\mathcal{D}_{tw}^1 = \delta_{tw}$, which implies $\mathcal{D}_t^1(u) = 1$ iff $t = u$ iff $tw = uw$ iff $\mathcal{D}_{tw}^1 = tw$. If $t = \text{va.t'}$, since we can suppose $a \notin \text{FN}(w)$, from $\pi_{\{a\}}^{\omega}(t'w) = \pi_{\{a\}}^{\omega}(t')w$ we deduce $\{\omega | \pi_{\{a\}}^{\omega}(t'w) = uw\} = \{\omega | \pi_{\{a\}}^{\omega}(t') = u\}$, from which the claim follows. $\square$

The following is a simple consequence of Lemma E.39:

**Lemma E.41.** Let $W$ be a set of terms such that $t \in W$ and $u \to_{\{\}}^* u$ implies $u \in W$; then for any $t, u \in \mathcal{T}$, if $t \to_{\{\}}^* u$, then $\sum_{w \in W} \mathcal{D}_t^1(w) \ge \sum_{w \in W} \mathcal{D}_u^1(w)$.

To adapt reducibility predicates to $\Lambda_{\text{PE}}^{\{\}}$, we need to adapt the definition of reducibility for counting quantified types. We define yet a new family of reducibility predicates $H^*\text{Red}_{\sigma}^{X,r}(S) \subseteq \Lambda_{\oplus, v, \{\}}^X$ as follows:

$$ H^*\text{Red}_{\oplus, v, \{\}}^{X,r}(S) = \Lambda_{\oplus, v, \{\}}^X $$

$$ H^*\text{Red}_{\sigma}^{X,r}(S) = H^*\text{Red}_{\text{hn}}^{X,r}(S) = H^*\text{Red}_{\text{n}}^{X,r}(S) = \{t \mid \forall \omega \in S \ \text{HNV}_{\to}(\pi_X^\omega(t)) \ge r\} $$

$$ H^*\text{Red}_{\sigma \to \tau}^{X,r}(S) = \{t \mid \forall S' \subseteq S, \forall u \in \text{HRed}_{\sigma}^{X,1}(S'), \text{tu} \in \text{HRed}_{\tau}^{X,r}(S')\} $$

$$ H^*\text{Red}_{\sigma \wedge \tau}^{X,r}(S) = H^*\text{Red}_{\sigma}^{X,r}(S) \cap H^*\text{Red}_{\tau}^{X,r}(S) $$

$$ H^*\text{Red}_{Cq\sigma}^{X,r}(S) = \left\{ t \mid \forall \omega \in S \sum_{u \in H^*\text{Red}_{\sigma}^{\emptyset, r}} \mathcal{D}_{\pi_X^\omega(t)}^1(u) \ge q \right\} $$

Most properties of $H^*\text{Red}_\sigma$ are proved as in the corresponding cases of $H\text{Red}_\sigma$. We here only consider the cases in which the proofs are different.

**Lemma E.42.** If $t \in H^*\text{Red}_{\sigma}^{X,r}(S)$ and $u \to_{\{\}}^* u$, then $u \in H^*\text{Red}_{\sigma}^{X,r}(S)$.

*Proof.* We argue by induction on $\sigma$:

* if $\sigma \in \{o, hn, n\}$, then $t \in H^*\text{Red}_{\sigma}^{X,r}(S)$ iff for all $\omega \in S$, $\text{HNV}_{\to}(\pi_X^\omega(t)) \ge r$; the claim then follows from Lemma E.39 (i).

* if $\sigma = \tau \Rightarrow \rho$ and $t \in H^*\text{Red}_{\sigma}^{X,r}(S)$, then for all $S' \subseteq S$ and $v \in H^*\text{Red}_{\tau}^{X,1}(S')$, $tv \in H^*\text{Red}_{\rho}^{X,r}(S')$; since $uv \to_{\{\}}^* tv$, by IH we deduce then $uv \in H^*\text{Red}_{\sigma}^{X,r}(S')$; we can thus conclude $v \in H^*\text{Red}_{\sigma}^{X,r}(S)$;

* if $\sigma = \tau \wedge \rho$, and $t \in H^*\text{Red}_{\sigma}^{X,r}(S)$, then by IH $u \in H^*\text{Red}_{\tau}^{X,r}(S)$ and $u \in H^*\text{Red}_{\rho}^{X,r}(S)$, so $u \in H^*\text{Red}_{\sigma}^{X,r}(S)$.

* if $\sigma = C^q\tau$ and $t \in H^*\text{Red}_{\sigma}^{X,r}(S)$, then $\sum_{v \in H^*\text{Red}_{\tau}^{X,r}(S)} \mathcal{D}_{\pi_X^\omega(t)}^1(v) \ge q$, and we can conclude $\sum_{v \in H^*\text{Red}_{\tau}^{X,r}(S)} \mathcal{D}_{\pi_X^\omega(u)}^1(v) \ge q$ from the IH and Lemma E.41 (i). $\square$

Using Lemma E.24 (i.), whose proof is adapted without difficulties to $\Lambda_{\text{PE}}^{\{\}}$, Lemma E.25 is adapted as follows:

**Lemma E.43.** For all types $\sigma$, terms $t, u_1, \dots, u_n$ with $\text{FN}(t) \subseteq X \cup \{a\}$, $\text{FN}(u_i) \subseteq X$, and measurable set $S \subseteq (2^{\mathbb{N}})^{X \cup \{a\}}$ and $S' \subseteq (2^{\mathbb{N}})^X$, if

$$ 1. \quad tu_1 \dots u_n \in H^*\text{Red}_{\sigma}^{X \cup \{a\}, r}(S); $$
2. for all $\omega \in S'$, $\mu(\Pi^\omega(S)) \ge s$;
then (va.t)$u_1 \dots u_n \in H^*\mathrm{Red}_{C^s\sigma}^{X,r}(S')$.

The following adaptation of Lemma E.26 immediately follows from Lemma E.42:

**Lemma E.44.** $t[u/x]u_1 \dots u_n \in H^*\mathrm{Red}_\sigma^{X,r}(S) \Rightarrow (\lambda x.t)uu_1 \dots u_n \in H^*\mathrm{Red}_\sigma^{X,r}(S)$.

**Lemma E.45.** For all types $\sigma$ and $\tau$, $H^*\mathrm{Red}_{C^{q_1 \dots C^{q_k}(\sigma \Rightarrow \tau)}}^{X,r}(S) \subseteq H^*\mathrm{Red}_{\sigma \Rightarrow C^{q_1 \dots C^{q_k} \tau}}^{X,r}(S)$.

*Proof.* For any $j \le k$, let $U_j := H^*\mathrm{Red}_{C^{q_{k-j+1} \dots C^{q_k}(\sigma \Rightarrow \tau)}}^{X,r}(S)$ and $V_j := H^*\mathrm{Red}_{\sigma \Rightarrow C^{q_{k-j+1} \dots C^{q_k} \tau}}^{X,r}(S)$.

We argue, by induction on $j \le k$, that $U_j \subseteq V_j$. If $j = 0$ then $U_j = \sigma \Rightarrow \tau = V_j$.

Let then $j > 0$ and $\omega \in S$. Suppose $t \in U_j$ and let $w \in H^*\mathrm{Red}_\sigma^{X,1}(S)$.

By IH we have $U_{j-1} \subseteq V_{j-1}$, from which we deduce $q_1 \le \sum_{u \in U_{j-1}} \mathcal{D}_{\pi_X^\omega(t)}^1(u) \le \sum_{u \in V_{j-1}} \mathcal{D}_{\pi_X^\omega(t)}^1(u)$.

$$ [\text{Lemma E.40}] \quad = \sum_{u \in V_{j-1}} \mathcal{D}_{\pi_X^\omega(t)}^1(\pi_X^\omega(w)) (u\pi_X^\omega(w)) = \sum_{u \in V_{j-1}} \mathcal{D}_{\pi_X^\omega(tw)}^1(u\pi_X^\omega(w)) \quad \text{which implies } t \in V_j. \quad \square $$

We call a term $t$ v-safe if $t$ never reduces to a term of the form $va.t'$.

**Definition E.46** (neutral terms for $\Lambda_{\mathrm{PE}}^{\{j\}}$). For any measurable set $S \subseteq (2^N)^X$, the set $\mathrm{Neut}_{\{j\}}(S)$ is defined by induction as follows:

* for any variable $x$, $x \in \mathrm{Neut}_{\{j\}}(S)$;

* if $t \in \mathrm{Neut}_{\{j\}}(S)$ and for all $\omega \in S$, $\pi_X^\omega(u)$ is v-safe and $\mathrm{HNV}_{\to}(u) = 1$, $\{t\}u \in \mathrm{Neut}_{\{j\}}(S)$.

* if $t \in \mathrm{Neut}_{\{j\}}(S)$, then for all $u \in \Lambda_{\oplus, v, \{j\}}^X$, $tu \in \mathrm{Neut}_{\{j\}}(S)$.

It is easily checked that for all $t \in \mathrm{Neut}_{\{j\}}(S)$ and $\omega \in S$, $\mathrm{HNV}(\pi_X^\omega(t)) = 1$.

**Lemma E.47.** For any type $\sigma$,
(i.) if $\sigma$ is non-trivial, then $t \in H^*\mathrm{Red}_\sigma^{X,r}(S)$ and $\omega \in S$, then $\mathrm{HNV}(\pi_X^\omega(t)) \ge [\sigma] \cdot r$;
(ii.) $\mathrm{Neut}_{\{j\}}(S) \subseteq H^*\mathrm{Red}_\sigma^{X,1}(S)$.

*Proof.* By induction on $\sigma$:

* if $\sigma = []$, both claims are immediate.

* if $\sigma \in \{o, hn, n\}$, claim (i.) holds by definition, and claim (ii.) follows from the fact that for all $t \in \mathrm{Neut}_{\{j\}}(S)$ and for all $\omega \in S$, $\mathrm{HNV}(\pi_X^\omega(t)) = 1$, so $t \in H^*\mathrm{Red}_\sigma^{X,1}(S)$.

* if $\sigma = \tau \Rightarrow \rho$ and $t \in H^*\mathrm{Red}_\sigma^{X,r}(S)$, then, since by IH $x \in H^*\mathrm{Red}_\tau^{X,1}(S)$, $tx \in H^*\mathrm{Red}_\tau^{X,1}(S)$, hence for all $\omega \in S$, $\mathrm{HNV}(\pi_X^\omega(t)) \ge \mathrm{HNV}(\pi_X^\omega(tx)) \ge [\rho] \cdot r = [\sigma] \cdot r$.
Moreover, if $t \in \mathrm{Neut}_{\{j\}}(S)$, then for all $S' \subseteq S$, $u \in H^*\mathrm{Red}_\tau^{X,1}(S')$ and $\omega \in S'$, $tu \in \mathrm{Neut}_{\{j\}}(S)$, so by IH $tu \in H^*\mathrm{Red}_\rho^{X,r}(S')$, and we conclude then $t \in H^*\mathrm{Red}_\sigma^{X,r}(S)$.

* if $\sigma = \tau \wedge \rho$ and $t \in H^*\mathrm{Red}_\sigma^{X,r}(S)$, then $t \in H^*\mathrm{Red}_\tau^{X,r}(S)$ and $t \in H^*\mathrm{Red}_\rho^{X,r}(S)$, so by IH for all $\omega \in S$, $\mathrm{HNV}(\pi_X^\omega(t)) \ge \max\{r \cdot [\tau], r \cdot [\rho]\} = r \cdot \max\{[\tau], [\rho]\} = r \cdot [\sigma]$.
Moreover, it $t \in \mathrm{Neut}_{\{j\}}(S)$, by IH $t \in H^*\mathrm{Red}_\tau^{X,1}(S)$ and $t \in H^*\mathrm{Red}_\rho^{X,1}(S)$, whence $t \in H^*\mathrm{Red}_\sigma^{X,1}(S)$.

* if $\sigma = C^q\tau$, and $t \in H^*\mathrm{Red}_{C^{q\tau}}^{X,r}(S)$, let $\omega \in S$; then we consider two cases:

* if $\pi_X^\omega(t)$ (that we can suppose being in $\mathcal{T}$) is a pseudo-value, then $\sum_{w \in H^*\mathrm{Red}_\tau^{X,r}} \mathcal{D}_t^1(w) \ge q > 0$ implies $\pi_X^\omega(t) \in H^*\mathrm{Red}_\tau^{X,r}$, so by IH we deduce $\mathrm{HNV}(\pi_X^\omega(t)) \ge r \cdot [\tau] \ge r \cdot q \cdot [\tau] = r \cdot [\sigma]$.

* if $\pi_X^\omega(t) = va.t'$, then $\sum_{w \in H^*\mathrm{Red}_\tau^{X,r}} \mathcal{D}_t^1(w) \ge q > 0$ implies, by IH, that $\mu(\{\omega' \in 2^N | \pi^\omega(t') \in H^*\mathrm{Red}_\tau^{0,r}\}) \ge \mu(\{\omega' \in 2^N | \mathrm{HNV}(\pi^\omega(t)) \ge [\tau]r\}) \ge q$, and this implies $\mathrm{HNV}(\pi_X^\omega(t)) \ge q \cdot r \cdot [\tau] = r \cdot [\sigma]$.

Moreover, if $t \in \mathrm{Neut}_{\{j\}}(S)$, then for all $\omega \in S$, $\mathcal{D}_{\pi_X^\omega(t)}^1 = \delta_{\pi_X^\omega(t)}$, and since by the IH $t \in H^*\mathrm{Red}_\tau^{X,r}(S)$, we deduce $\sum_{u \in H^*\mathrm{Red}_\tau^{X,r}} \mathcal{D}_{\pi_X^\omega(t)}^1(u) = \delta_{\pi_X^\omega(t)}(\pi_X^\omega(t)) = 1 \ge q$, so $t \in H^*\mathrm{Red}_{C^{q\tau}}^{X,r}(S)$.

**Lemma E.48.** For any non-trivial type $\sigma$, and term $t$ name-closed and v-safe, if $t \in H^*\mathrm{Red}_\sigma^{0,r}$, then $\mathrm{HNV}_{\to}(t) = 1$.

*Proof.* By induction on $\sigma$:

* if $\sigma \in \{o, hn, n\}$, from $t \in H^*\mathrm{Red}_\sigma^{0,r}$ we deduce $\mathrm{HNV}_{\to}(t) \ge r > 0$, and since for all $u$ such that $t \to_{\{j\}h}^* u$, $\mathcal{D}_u = \delta_u$, we deduce that $\sup\{\mathrm{HNV}(u) | t \to_{\{j\}h}^* u\} = \sup\{\sum_{v \in \mathrm{HNV}_{\{j\}}(S)} \delta_v(v) | t \to_{\{j\}h}^* u\} > 0$, this implies that $t$ reduces to a HNV, whence $\mathrm{HNV}_{\to}(t) = 1$.
* if $\sigma = \tau \Rightarrow \rho$ and $t \in H^*\text{Red}_{\sigma}^{0,r}$ then since by Lemma E.47 $x \in H^*\text{Red}_{\tau}^{0,1}$, $tx \in H^*\text{Red}_{\rho}^{0,r}$; suppose $tx \to_{\{h\}}^* va.t'$; then since $t$ is $v$-safe, the only possibility is that $t \to_{\{h\}}^* (\lambda x.u)$ and $u \to_{\{h\}}^* va.t'$; but then $t \to_{\{h\}}^* \lambda x.va.t' \to_{\{h\}}^* va.\lambda x.t'$, against the hypothesis. We conclude that also $tx$ must be $v$-safe, so by IH $\text{HNV}_{\to}(tx) = 1$, whence $\text{HNV}_{\to}(t) = 1$.

* if $\sigma = \tau \wedge \rho$ and $t \in H^*\text{Red}_{\sigma}^{0,r}$, then $t \in H^*\text{Red}_{\tau}^{0,r}$, so by IH, $\text{HNV}_{\to}(t) = 1$.

* if $\sigma = C^s\tau$ and $t \in H^*\text{Red}_{\sigma}^{0,r}$, then since $\mathcal{D}_t = \delta_t$, from $\sum_{w \in H^*\text{Red}_{\tau}^{0,r}} \delta_t(w) \ge s > 0$, it follows that $t \in H^*\text{Red}_{\tau}^{0,r}$, so by IH $\text{HNV}_{\to}(t) = 1$.

**Lemma E.49.** If $t \in H^*\text{Red}_{\sigma \to \tau}^{X,q}(S)$ and $u \in H^*\text{Red}_{C^s\sigma}^{X,1}(S)$, where $\sigma$ is non-trivial, then $\{t\}u \in H^*\text{Red}_{C^s\tau}^{X,q}(S)$.

*Proof.* Let $\omega \in S$. We distinguish two cases:

* $\pi_X^\omega(u) \to_{\{h\}}^* va.u'$; then, letting $W_\sigma := H^*\text{Red}_\sigma^{X,1}(S)$ and $W_\tau := H^*\text{Red}_\tau^{X,q}(S)$, we have that $\sum_{w \in W} \mathcal{D}_{\pi_X^\omega va.t'}^1(w) = \sum_{w \in W} \mu(\{\omega' | \pi_{X \cup \{a\}}^{\omega+\omega'}(tu') = w\}) = \mu(\{\omega' | \pi_{X \cup \{a\}}^{\omega+\omega'}(tu') \in W\}) = \mu(\{\omega' | t\pi_{X \cup \{a\}}^{\omega+\omega'}(u') \in W\}) \ge \mu(\{\omega' | \pi_{X \cup \{a\}}^{\omega+\omega'}(u') \in U\}) = \sum_{w \in U} \mathcal{D}_{va.u}^1(w) \ge s$, which proves that $va.tu' \in W_\tau$. Since $\{t\}u \to_{\{h\}}^* va.tu'$, we conclude then $\{t\}u \in W_\tau$ from Lemma E.42.

* $\pi_X^\omega(u)$ is $v$-safe; then from $\pi_X^\omega(u) \in H^*\text{Red}_\sigma^{0,q}$ we deduce, by Lemma E.48, that $\text{HNV}_{\to}(\pi_X^\omega(u)) = 1$. We deduce then that $\{t\}u \in \text{Neut}_{\{\}}(S)$, and by Lemma E.47 we conclude $\{t\}u \in H^*\text{Red}_{C^s\sigma}^{X,q}(S)$.

**Proposition E.50.** If $\Gamma \vdash^X t : \mathfrak{b} \mapsto \mathfrak{s}$ is derivable in $C\lambda_{\to}^{\{\}}$, where $\Gamma = \{x_1 : s_1, \dots, x_m : s_m\}$, then for all $S \subseteq [\mathfrak{b}]_X$, for all $u_i \in H^*\text{Red}_{s_i}^{X,1}(S)$, $t[u_1/x_1, \dots, u_m/x_m] \in H^*\text{Red}_S^{X,1}(S)$.

*Proof.* We can argue as in the proof of Proposition E.35, with the following two new cases:

* if $t = \{t_1\}_{t_2}$ and the last rule is

$$ \frac{\Gamma \vdash^X t_1 : c \mapsto C^{\bar{q}}(s \Rightarrow \sigma) \qquad \Gamma \vdash^X t_2 : d \mapsto C^s \mathfrak{b} \qquad \mathfrak{b} \models c \wedge d}{\Gamma \vdash^X t : \mathfrak{b} \mapsto C^s C^{\bar{q}} \sigma} (\{\}) $$

then by IH for all $u_i \in H^*\text{Red}_{s_i}^{X,1}(S)$, $t_1[u_1/x_1, \dots, u_n/x_n] \in H^*\text{Red}_{C^{\bar{q}}(s \Rightarrow \sigma)}^{X,1}(S)$ and $t_2[u_1/x_1, \dots, u_n/x_n] \in H^*\text{Red}_{C^s S}^{X,1}(S)$; then by Lemma E.45 and Lemma E.49 (observing that $\mathfrak{s}$ is non-trivial) we deduce $(\{t_1\}_{t_2})[u_1/x_1, \dots, u_n/x_n] = \{t_1[u_1/x_1, \dots, u_n/x_n]\}(t_2[u_1/x_1, \dots, u_n/x_n]) \in H^*\text{Red}_{C^{\bar{q}}\sigma}^{X,1}(S)$.

* If $t = va.u$ and the last rule is

$$ \frac{\Gamma \vdash^{X \cup \{a\}} u : c \wedge d \mapsto C^{q_j} \sigma \qquad \vdash \mu(d) \ge r \qquad \mathfrak{b} \models c}{\Gamma \vdash^X va.u : \mathfrak{b} \mapsto C^r \sigma} (\mu) $$

where $a \notin \text{FV}(\Gamma) \cup \text{FV}(c)$, then let $S \subseteq [\mathfrak{b}]_X \subseteq [c]_X$ and $u_1 \in H^*\text{Red}_{s_1}^{X,1}(S), \dots, u_n \in H^*\text{Red}_{s_n}^{X,1}(S)$. Let $T = \{g+f \mid \omega \in S\} \subseteq (2^N)^{X \cup \{a\}}$, which is measurable since counter-image of a measurable set through the projection function; then since $\text{FN}(u_i) \subseteq X$, we deduce using Lemma E.22 that $u_i \in H^*\text{Red}_{s_i}^{X \cup \{a\},1}(T \cap [d_j]_{X \cup \{a\}})$. By IH and the hypothesis we deduce then that

* $u[u_1/x_1, \dots, u_n/x_n] \in H^*\text{Red}_S^{X \cup \{a\},1}(T \cap [d_j]_{X \cup \{a\}})$;

* for all $\omega \in S$, $\mu(\Pi^\omega(T \cap [d_j]_{X \cup \{a\}})) \ge r$;

Hence, by Lemma E.43 we conclude that $va.u[u_1/x_1, \dots, u_n/x_n] = (va.u)[u_1/x_1, \dots, u_n/x_n] \in H^*\text{Red}_S^{X, \sum_j r_j q_j}(S) = H^*\text{Red}_{C^r S}^{X,1}(S)$. □

We can now deduce Theorem 6.1 from Proposition E.50 as in the case of $C\lambda_{\to, \cap}$.

**Theorem E.51.** If $\Gamma \vdash^X t : \mathfrak{b} \mapsto \mathfrak{s}$, then for all $\omega \in [\mathfrak{b}]$, $\text{HNV}_{\to}(\pi_X^\omega(t)) \ge \lceil \sigma \rceil$.