[14] D. Baelde, S. Delaune, C. Jacomme, A. Koutsos, and S. Moreau, "An interactive prover for protocol verification in the computational model," in *SP*. IEEE, 2021, pp. 537–554.

[15] D. Baelde, S. Delaune, A. Koutsos, and S. Moreau, "Cracking the stateful nut: Computational proofs of stateful security protocols using the squirrel proof assistant," in *CSF*. IEEE, 2022, pp. 289–304.

[16] C. Cremers, C. Fontaine, and C. Jacomme, "A logic and an interactive prover for the computational post-quantum security of protocols," in *SP*. IEEE, 2022, pp. 125–141.

[17] D. Baelde, A. Koutsos, and J. Lallemand, "A higher-order indistinguishability logic for cryptographic reasoning," in *LICS*, 2023, pp. 1–13.

[18] M. Arapinis, L. I. Mancini, E. Ritter, and M. D. Ryan, "Analysis of privacy in mobile telephony systems," *Int. J. Inf. Sec.*, vol. 16, no. 5, pp. 491–523, 2017.

[19] M. Bellare, "Practice-oriented provable security," in *Lectures on Data Security*, ser. Lecture Notes in Computer Science, vol. 1561. Springer, 1998, pp. 1–15.

[20] M. Fischlin and A. Mittelbach, "An overview of the hybrid argument," *IACR Cryptol. ePrint Arch.*, p. 88, 2021.

[21] M. Bellare, A. Boldyreva, and S. Micali, "Public-key encryption in a multi-user setting: Security proofs and improvements," in *EUROCRYPT*, ser. Lecture Notes in Computer Science, vol. 1807. Springer, 2000, pp. 259–274.

[22] H. Comon and A. Koutsos, "Formal computational unlinkability proofs of RFID protocols," in *CSF*. IEEE Computer Society, 2017, pp. 100–114.

[23] A. Koutsos, "The 5G-AKA authentication protocol privacy," in *EuroS&P*. IEEE, 2019, pp. 464–479.

# APPENDIX A
## SEMANTICS OF PREDICATES

We give here the full definitions of the predicates described in Section II and in rules of Section III.

a) **Bounded length:** For $u$ an order-1 term of type $\tau_0 \to \tau_1$, $l$ a term of type $\overline{\text{int}} \to \overline{\text{int}}$, the predicate $\text{blen}_l(u)$ holds if, for any $\eta$ and $a \in [\tau_0]_M^\eta$ of length $n_a \in \mathbb{N}$, and for every $\rho \in \mathbb{T}_{M,\eta}$, we have $|[u]_M^{\eta,\rho}(a)| \le \inf_{\rho} |[l]_M^{\eta,\rho}(n_a)$. The definition extends naturally to order-1 terms with more than one argument.

b) **Adversarial computability:** Let $u$ be a term of type $\vec{\tau}_1 \to \vec{\tau}_0 \to \tau$ with $\vec{\tau}_1$ are types of order 1, $\vec{\tau}_0$ and $\tau$ have order 1. Let $t$ be a term of type $(\overline{\text{int}} \to \overline{\text{int}})^n \to \overline{\text{int}}^m \to \overline{\text{int}}$, and $\vec{o}$ of type $\overline{\text{int}}^n$, with $n = |\vec{\tau}_1|$ and $m = |\vec{\tau}_0|$. The predicate $\text{adv}_{t,\vec{o}}(u)$ holds if there exists a Turing machine $A$ with $n$ oracles and $m$ inputs such that, for all

* $\eta \in \mathbb{N}$ and $\rho \in \mathbb{T}_{M,\eta}$,

* $\vec{f} \in [\vec{\tau}_1]_M^{\eta,\rho}$ and $\vec{l}$ such that

$|f_i(x)| \le l_i(|x|)$ for all $i$ and $x$,

* $\vec{w} \in [\vec{\tau}_0]_M^{\eta,\rho}$ and $\vec{s}$ such that $w_i = |s_i|$ for all $i$,

we have:

$$ \begin{align*} [u]_M^{\eta,\rho}(\vec{f}, \vec{w}) &= A^f(1^{\eta}, \vec{w}, \rho_a) \\ \text{time}_A(1^{\eta}, \vec{w}, \vec{f}) &\le \inf_{\rho} \left\| [t \vec{l} \vec{s}]_M^{\eta,\rho} \right\| \\ \text{calls}_A^{\eta} &\le \inf_{\rho} \left\| \vec{o}_M^{\eta,\rho} \right\| \end{align*} $$

c) **Well-foundedness:** Let $\tau$ be a type and $<_{\tau}$ be a symbol of type $\tau \to \tau \to \text{bool}$. We let $\text{well-founded}_{\tau}(<_{\tau})$ be the following global formula, which checks if type $\tau$, ordered by $<_{\tau}$, is well-founded:

$$ \text{well-founded}_{\tau}(<_{\tau}) \stackrel{\text{def}}{=} [\forall (l: \text{nat} \to \tau). \neg(\forall i, j. i < j \to l j <_{\tau} l i)]_0 $$

where nat and $<$: nat $\to$ nat $\to$ bool are always interpreted as, resp., the set of natural numbers and the standard order over natural numbers.

# APPENDIX B
## PROOF SYSTEM

### A. Permutation Rule

Let $u_l^1, \dots, u_l^n$ and $u_r^1, \dots, u_r^n$ be two sequences of terms of the same length, whose types are compatible. Let $\pi$ be a permutation of $\{1, \dots, n\}$. Then we can permute terms in an equivalence formula with the permutation rule:

$$ G_{\varepsilon}.E:\text{PERM} \\ \mathbb{E}; \Theta \vdash u_l^{\pi(1)}, \dots, u_l^{\pi(n)} \sim_{\pi(\varepsilon)} u_r^{\pi(1)}, \dots, u_r^{\pi(n)} \\ \mathbb{E}; \Theta \vdash u_l^1, \dots, u_l^n \sim_{\varepsilon} u_r^1, \dots, u_r^n, $$

where $\pi(\varepsilon)$ permutes oracle calls in $\varepsilon$ according to $\pi$, and is defined by:

$$ \pi(\varepsilon) \stackrel{\text{def}}{=} \lambda t, o_1, \dots, o_r. \varepsilon \ t o_{\pi'(1)} \dots o_{\pi'(r)} $$

where, if we let $r$ be the number of terms of order 1 in $u_1^1, \dots, u_l^n$, then $\pi'$ is the permutation of $\{1, \dots, r\}$ defined by:

$$ \pi'(i) \stackrel{\text{def}}{=} \left| \left\{ j \mid \pi(j) \le \pi(i) \text{ and } \pi(u_l^j) \text{ is of order 1} \right\} \right|. $$

### B. Bi-Deduction

The bi-deduction rule shown in Section III-B is a generalization of several reductionistic rules of our proof system. More precisely, this rule captures the Function Applications rules $G_{\varepsilon}.E:\text{FA-APP}$, $G_{\varepsilon}.E:\text{FA-FUN}$ and $G_{\varepsilon}.E:\text{FA-BASE}$, as well as the weakening rule $G_{\varepsilon}.E:\text{WEAK}$.

We now present our full bi-deduction rule, which generalizes the rule presented in the body of this paper in several ways:

* we provide additional fresh names to the contexts;

* we allow for an arbitrary number of contexts instead of a single context.

These two extensions make our bi-deduction rule general enough to subsume more standard CCSA rules: adding names captures the $G_{\varepsilon}.E:\text{FA-NAMES}$ rule capabilities, while having many contexts captures the duplication rules $G_{\varepsilon}.E:\text{DUP-BASE}$ and Ge.Equiv.Dup-Fun, as well as $G_{\varepsilon}.E:\text{PERM}$. The rules subsumed by the generalized bi-deduction rule are clearly marked in Fig. 11.

a) **Generalized bi-deduction:** We now describe our first generalization of the bi-deduction rule. Let $\mathbb{E}$ be an environment such that any declared symbols $x$ in $\mathbb{E}$ is only used in eta-long form and is such that $\mathbb{E}; \Theta \vdash \text{adv}_{+\infty}(x)$ is valid, and let $\Theta$ be a set of global hypotheses.

Let $\vec{u} \stackrel{\text{def}}{=} u_1, \dots, u_m$ and $\vec{v} \stackrel{\text{def}}{=} v_1, \dots, v_m$ be two sequences of terms of the same length such that, for every $i$, terms $u_i$ and $v_i$ have the same types. Let $\vec{l} \stackrel{\text{def}}{=} l_1, \dots, l_m$ be a sequence of length terms for $\vec{u}$ and $\vec{v}$:

* we assume that the types of $\vec{l}$ are compatible with $\vec{u}$ and $\vec{v}$, i.e. $l_i$ has type $\overline{\text{int}}$ if $u_i$ and $v_i$ are of order 0, and has type $\overline{\text{int}} \to \overline{\text{int}}$ if $u_i$ and $v_i$ are of order 1;
• we will require blen<sub>i</sub>(u<sub>i</sub>) ̃ blen<sub>i</sub>(v<sub>i</sub>) for every i.

Similarly, let $\tilde{w}_0$ and $\tilde{w}_1$ be two sequences of terms of the
same length with compatible types, and let $\tilde{l^w}$ be a sequence
of length terms for $\tilde{w}_0$ and $\tilde{w}_1$.

Let $C_1, \dots, C_n$ be sequences of terms representing the
contexts that are to be simulated by the adversary. To account
for the cost aspects of the rule, we consider, for every $i \le n$:

• a term $t_i$ representing the execution time of $C_i$;

• a sequence of terms $\vec{o}_i$ representing the number of calls that $C_i$ makes to its arguments of order 1.

We will require that $adv_{t_i, \vec{o}_i}(C_i)$ holds for every $i \le n$, and
that the terms $C_1, \dots, C_n$ are *without names*.

Let $\vec{n} \stackrel{\text{def}}{=} n_1, \dots, n_p$ a sequence of names that are to be
provided to $C_1, \dots, C_n$. We require that:

• names in $\vec{n}$ are fresh, i.e. we require that no name in $\vec{n}$ appears in $\tilde{w}_0, \tilde{w}_1, \tilde{u}, \tilde{v}, C_1, \dots, C_n$, and $\Theta$;

• names in $\vec{n}$ do not appear in $\mathbb{E}$, except in their declarations;

• we are provided, for every $i \le p$, with a term $t_j^n$ upper-
bounding the time needed by $n_j$ to do a single sampling
in any model;

• we are given a sequence of length terms $\vec{l}^n = l_1^n, \dots, l_p^n$ for $\vec{n}$, where we will require that $\text{blen}_{l_i^n}(n_i)$ holds for every $i \le p$.

We let $j_i, \dots, j_q$ be such that

$$
(C_{j_1} \tilde{w}_0 \tilde{u} \tilde{n}), \dots, (C_{j_q} \tilde{w}_0 \tilde{u} \tilde{n})
$$

is the sub-sequence, in the same order, of terms of order 1 in
$(C_1 \tilde{w}_0 \tilde{u} \tilde{n}), \dots, (C_n \tilde{w}_0 \tilde{u} \tilde{n})$. Furthermore, for every context
$C_i$, we decompose $\tilde{o}_i$ into $\tilde{o}_i^a$, $\tilde{o}_i^n$ where: $\tilde{o}_i^a$ bounds the number
of calls from $C_i$ to each order-1 argument in $\tilde{w}_0, \tilde{u}$ (or $\tilde{w}_1, \tilde{v}$);
$\tilde{o}_i^n$ is of length $p$ and bounds the number of calls from $C_i$ to
each name symbol in $\tilde{n}$.

Then, we have the rule:

G<sub>ε</sub> : E : BI-DEDUCE

$$
\mathbb{E}; \Theta \vdash \tilde{w}_0, \tilde{u} \sim_{\varepsilon} \tilde{w}_1, \tilde{v} \qquad \mathbb{E}; \Theta \vdash \tilde{\Lambda}_{i \le n} \mathrm{adv}_{t_i, \tilde{o}_i}(C_i)
$$

$$
\mathbb{E}; \Theta \vdash \text{blen}_{\vec{l}^w}(\tilde{w}_0) \wedge \text{blen}_{\vec{l}^w}(\tilde{w}_1)
$$

$$
\mathbb{E}; \Theta \vdash \text{blen}_{\vec{l}^w}(\tilde{u}) \wedge \text{blen}_{\vec{l}^w}(\tilde{v}) \qquad \mathbb{E}; \Theta \vdash \text{blen}_{\vec{l}^n}(\vec{n})
$$

$$
\mathbb{E}; \Theta \vdash \tilde{w}_0, (C_1, \dots, C_n) \quad \tilde{w}_0 \quad \tilde{u} \quad \tilde{n} \quad \sim_{\varepsilon'} \tilde{w}_1, (C_1, \dots, C_n) \quad \tilde{w}_1 \quad \tilde{v} \quad \tilde{n}
$$

where $(C_1, \dots, C_n) \tilde{w}_0 \tilde{u} \tilde{n}$ denotes the sequence terms

$$
C_1 \tilde{w}_0 \tilde{u} \tilde{n}, \dots, C_n \tilde{w}_0 \tilde{u} \tilde{n},
$$

and $\varepsilon'$ is the advantage bound term:

$\lambda t, a_1, \dots, a_q.$

$$
\varepsilon \left( t + t_{\text{oracle}} + \sum_{i \le n} \text{cpt}_i \cdot t_i \, \vec{l^w} \, \vec{l^h} \right) \left( \sum_{i \le n} \text{cpt}_i \cdot \vec{o}_i^a \right) \quad (8)
$$

where $t_{\text{oracle}}$ is the time needed to compute all random
samplings for names $\vec{n}$ defined by:

$$
t_{\text{oracle}} \stackrel{\text{def}}{=} \sum_{i \le n, j \le p} t_j^n \cdot \vec{o}_i^n[j]
$$

and where, for every $i \le n$, the term $cpt_i$ represents the number
of times we need to simulate $C_i$, and is defined as:

$$
\text{cpt}_i \stackrel{\text{def}}{=} \begin{cases} 1 & \text{if } (C_i \tilde{u} \tilde{n}) \text{ is of order } 0 \\ a_r & \text{if } (C_i \tilde{u} \tilde{n}) \text{ is of order } 1, \text{ where } r \text{ is s.t. } j_r = i. \end{cases}
$$

C. The Computability Predicate $\mathbb{E}; \Theta; \vec{a} \vdash_{t, \vec{o}}^c u$

For $u$ a term of order at most 2, the computability predicate
$\mathbb{E}; \Theta; \vec{a} \vdash_{t, \vec{o}}^c u$ represents the fact that $\llbracket u \rrbracket_{\mathbb{M}}^{\eta, \rho}$ can be simulated
from $\vec{a}$, in time $t$ and calling its first order arguments at most
$\vec{o}$ times (where $t$ and $\vec{o}$ are well-type in $\mathbb{E}$). It is an extension
of the $\vdash_{pptm}$ predicate from [17]. Practically this predicate is
similar to $adv_{t, \vec{o}}(u)$ with two major differences:

• we allow for simulation of names, that is the distribution of the simulation should be equal to the distribution of $\llbracket u \rrbracket_{\mathbb{M}}^{\eta, \rho}$, as opposed to $adv()$ where we require equality for every $\rho$;

• we fix the evaluation strategy for the simulation, i.e. the simulation evaluates $u$ in a standard way, as opposed to $adv()$ where we only require that a simulator exists.

In order to be able to provide a proof system that allows
for simulating quantifiers, we need a new predicates. For any
type $\tau$ of order 0, we consider an additional global predicate
enum<sub>τ</sub>(t<sub>e</sub>), which is satisfied in a model $\mathbb{M}$ iff. there exists
a machine $\mathcal{M} \in$ PPTM such that, for any $\eta$, $\mathcal{M}$ enumerates
all elements of type $\tau$ in time at most inf<sub>ρ</sub>($\llbracket t_e \rrbracket_{\mathbb{M}}^{\eta, \rho}$). By
enumerating, we mean that there exists a particular working
tape T of $\mathcal{M}$ such that, during an execution of $\mathcal{M}$, the tape T
will successively contains all values of type $\tau$, where $\mathcal{M}$ enters
a special state each time it emits a value of type $\tau$ on tape T
(and $\mathcal{M}$ enter this state only when it emits such a value).

We provide a proof system for $\mathbb{E}; \Theta; \vec{a} \vdash_{t, \vec{o}}^c u$ in 6.

D. Generalized Subterms and Freshness Conditions

To recall the definition of the $\phi_{\text{fresh}}^n(u)$ (This condition can
be any formula that imply the freshness of $n$ $i$ in $u$, meaning
that the sampling of $n$ $i$ isn't necessary to compute $u$), we
first recall the notion of generalize subterms $ST_{\mathbb{E}}(u)$ in Fig. 8,
that represent all subterm $v$ necessary to compute a given term
$u$ in a given environment $\mathbb{E}$ with the conditions $\psi$ require to
have to compute $v$ and the variables $\vec{\alpha}$ bound in $u$ that can
be found in $v$. The formal definition of $\phi_{\text{fresh}}^{n,v}(C(n\,v))$ is any
well-typed formula in $\mathbb{E}$ such as for all model $\mathcal{M}$ of $\Theta$, and
for all $\eta \in \mathbb{N}, \rho \in \mathbb{T}_{\mathcal{M},\eta}$:

$$
\llbracket \phi_{\text{fresh}}^{n,v}(\vec{u}) \rrbracket_{\mathbb{M}}^{\eta, \rho} = 1 \text{ implies}
$$

$$
\llbracket \forall \vec{\alpha}. \psi \Rightarrow v \neq v_0 \rrbracket_{\mathbb{M}}^{\eta, \rho} = 1
$$

$$
\text{for every } (\vec{\alpha}, \psi, n, v_0) \in \mathcal{S}T_{\mathbb{E}}(\vec{u})
$$

We recall the definition given for $\phi_{\text{key}}()$ and $\phi_{\text{rand}}()$ in [17],
starting by some extra cases to add to the generalized subterms:

$$
ST_{\mathbb{E},k,i_k}^{\text{cca}}(\text{pk}(k \, i_0)) \stackrel{\text{def}}{=} \{(\varepsilon, \top, \text{pk}(k \, i_0))\}
$$

$$
\cup ST_{\mathbb{E},k,i_k}^{\text{cca}}(i_0) \cup [i_0 \neq i_k]ST_{\mathbb{E},k,i_k}^{\text{cca}}(k \, i_0)
$$

and

$$
ST_{\mathbb{E},k,i_k}^{\text{cca}} (\text{adec } u (k i_k))
$$

$$
\stackrel{\text{def}}{=} \{(\varepsilon, \top, \text{adec } u (k i_k)), (\varepsilon, \top, \text{adec})\}
$$

$$
\cup ST_{\mathbb{E},k,i_k}^{\text{cca}}(u) \cup ST_{\mathbb{E},k,i_k}^{\text{cca}}(i_0) \cup [i_0 \neq i_k]ST_{\mathbb{E},k,i_k}^{\text{cca}}(k \, i_0)
$$

Those represent the added capacity of the adversary given the
oracles of the CCA1 game. And then, we can define $\phi_{\text{key}}()$ and
* we will require $\text{blen}_{i}(u_{i}) \tilde{\Lambda} \text{blen}_{i}(v_{i})$ for every $i$.

Similarly, let $\tilde{w}_{0}$ and $\tilde{w}_{1}$ be two sequences of terms of the same length with compatible types, and let $\tilde{l}^{\tilde{w}}$ be a sequence of length terms for $\tilde{w}_{0}$ and $\tilde{w}_{1}$.

Let $C_{1}, \dots, C_{n}$ be sequences of terms representing the contexts that are to be simulated by the adversary. To account for the cost aspects of the rule, we consider, for every $i \le n$:

* a term $t_{i}$ representing the execution time of $C_{i}$;

* a sequence of terms $\tilde{o}_{i}$ representing the number of calls that $C_{i}$ makes to its arguments of order 1.

We will require that $\text{adv}_{t_{i}, \tilde{o}_{i}}(C_{i})$ holds for every $i \le n$, and that the terms $C_{1}, \dots, C_{n}$ are without names.

Let $\tilde{n} \stackrel{\text{def}}{=} n_{1}, \dots, n_{p}$ a sequence of names that are to be provided to $C_{1}, \dots, C_{n}$. We require that:

* names in $\tilde{n}$ are fresh, i.e. we require that no name in $\tilde{n}$ appears in $\tilde{w}_{0}, \tilde{w}_{1}, \tilde{u}, \tilde{v}, C_{1}, \dots, C_{n}$, and $\Theta$;

* names in $\tilde{n}$ do not appear in $\mathbb{E}$, except in their declarations;

* we are provided, for every $i \le p$, with a term $t_{j}^{n}$ upper-bounding the time needed by $n_{j}$ to do a single sampling in any model;

* we are given a sequence of length terms $\tilde{l}^{\tilde{n}} = l_{1}^{n}, \dots, l_{p}^{n}$ for $\tilde{n}$, where we will require that $\text{blen}_{l_{i}^{n}}(n_{i})$ holds for every $i \le p$.

We let $j_{i}, \dots, j_{q}$ be such that

$$ (C_{j_1} \tilde{w}_0 \tilde{u} \tilde{n}), \dots, (C_{j_q} \tilde{w}_0 \tilde{u} \tilde{n}) $$

is the sub-sequence, in the same order, of terms of order 1 in $(C_{1} \tilde{w}_{0} \tilde{u} \tilde{n}), \dots, (C_{n} \tilde{w}_{0} \tilde{u} \tilde{n})$. Furthermore, for every context $C_{i}$, we decompose $\tilde{o}_{i}$ into $\tilde{o}_{i}^{a}$, $\tilde{o}_{i}^{n}$ where: $\tilde{o}_{i}^{a}$ bounds the number of calls from $C_{i}$ to each order-1 argument in $\tilde{w}_{0}, \tilde{u}$ (or $\tilde{w}_{1}, \tilde{v}$); $\tilde{o}_{i}^{n}$ is of length $p$ and bounds the number of calls from $C_{i}$ to each name symbol in $\tilde{n}$.

Then, we have the rule:

**G<sub>ε</sub>.E:BI-DEDUCE**

$$ \mathbb{E}; \Theta \vdash \tilde{w}_{0}, \tilde{u} \sim_{\varepsilon} \tilde{w}_{1}, \tilde{v} \qquad \mathbb{E}; \Theta \vdash \tilde{\Lambda}_{i \le n} \text{adv}_{t_i, \tilde{o}_i}(C_i) $$

$$ \mathbb{E}; \Theta \vdash \text{blen}_{\tilde{u}^{\tilde{w}}}(\tilde{w}_{0}) \tilde{\Lambda} \text{blen}_{\tilde{u}^{\tilde{w}}}(\tilde{w}_{1}) $$

$$ \mathbb{E}; \Theta \vdash \text{blen}_{\tilde{r}^{-}}(\tilde{u}) \tilde{\Lambda} \text{blen}_{\tilde{r}^{-}}(\tilde{v}) \qquad \mathbb{E}; \Theta \vdash \text{blen}_{\tilde{n}^{-}}(\tilde{n}) $$

$$ \mathbb{E}; \Theta \vdash \tilde{w}_{0}, (C_{1}, \dots, C_{n}) \tilde{w}_{0} \tilde{u} \tilde{n} \sim_{\varepsilon'} \tilde{w}_{1}, (C_{1}, \dots, C_{n}) \tilde{w}_{1} \tilde{v} \tilde{n} $$

where $(C_{1}, \dots, C_{n}) \tilde{w}_{0} \tilde{u} \tilde{n}$ denotes the sequence terms

$$ C_1 \tilde{w}_0 \tilde{u} \tilde{n}, \dots, C_n \tilde{w}_0 \tilde{u} \tilde{n}, $$

and $\varepsilon'$ is the advantage bound term:

$$ \lambda t, a_1, \dots, a_q. $$

$$ \varepsilon \left( t + t_{\text{oracle}} + \sum_{i \le n} \text{cpt}_i \cdot t_i \, \tilde{l}^{\tilde{w}} \, \tilde{l}^{\tilde{r}^{-}} \right) \left( \sum_{i \le n} \text{cpt}_i \cdot \tilde{o}_i^a \right) \quad (8) $$

where $t_{\text{oracle}}$ is the time needed to compute all random samplings for names $\tilde{n}$ defined by:

$$ t_{\text{oracle}} \stackrel{\text{def}}{=} \sum_{i \le n, j \le p} t_j^n \cdot \tilde{o}_i^n[j] $$

and where, for every $i \le n$, the term $\text{cpt}_{i}$ represents the number of times we need to simulate $C_{i}$, and is defined as:

$$ \text{cpt}_i \stackrel{\text{def}}{=} \begin{cases} 1 & \text{if } (C_i \tilde{u} \tilde{n}) \text{ is of order } 0 \\ a_r & \text{if } (C_i \tilde{u} \tilde{n}) \text{ is of order } 1, \text{ where } r \text{ is s.t. } j_r = i. \end{cases} $$

**C. The Computability Predicate $\mathbb{E}; \Theta; \tilde{a} \vdash_{t, \tilde{o}}^{c} u$**

For $u$ a term of order at most 2, the computability predicate $\mathbb{E}; \Theta; \tilde{a} \vdash_{t, \tilde{o}}^{c} u$ represents the fact that $\llbracket u \rrbracket_{\mathbb{M}}^{\eta, \rho}$ can be simulated from $\tilde{a}$, in time $t$ and calling its first order arguments at most $\tilde{o}$ times (where $t$ and $\tilde{o}$ are well-type in $\mathbb{E}$). It is an extension of the $\vdash_{pptm}$ predicate from [17]. Practically this predicate is similar to $\text{adv}_{t, \tilde{o}}(u)$ with two major differences:

* we allow for simulation of names, that is the distribution of the simulation should be equal to the distribution of $\llbracket u \rrbracket_{\mathbb{M}}^{\eta, \rho}$, as opposed to $\text{adv}()$ where we require equality for every $\rho$;

* we fix the evaluation strategy for the simulation, i.e. the simulation evaluates $u$ in a standard way, as opposed to $\text{adv}()$ where we only require that a simulator exists.

In order to be able to provide a proof system that allows for simulating quantifiers, we need a new predicates. For any type $\tau$ of order 0, we consider an additional global predicate $\text{enum}_{\tau}(t_{e})$, which is satisfied in a model $\mathbb{M}$ iff. there exists a machine $\mathcal{M} \in \text{PPTM}$ such that, for any $\eta$, $\mathcal{M}$ enumerates all elements of type $\tau$ in time at most $\text{inf}_{\rho}(\llbracket t_{e} \rrbracket_{\mathbb{M}}^{\eta, \rho})$. By enumerating, we mean that there exists a particular working tape $\mathcal{T}$ of $\mathcal{M}$ such that, during an execution of $\mathcal{M}$, the tape $\mathcal{T}$ will successively contains all values of type $\tau$, where $\mathcal{M}$ enters a special state each time it emits a value of type $\tau$ on tape $\mathcal{T}$ (and $\mathcal{M}$ enter this state only when it emits such a value).

We provide a proof system for $\mathbb{E}; \Theta; \tilde{a} \vdash_{t, \tilde{o}}^{c} u$ in 6.

**D. Generalized Subterms and Freshness Conditions**

To recall the definition of the $\phi_{\text{fresh}}^{n}(u)$ (This condition can be any formula that imply the freshness of $n$ $i$ in $u$, meaning that the sampling of $n$ $i$ isn't necessary to compute $u$), we first recall the notion of generalize subterms $ST_{\mathbb{E}}(u)$ in Fig. 8, that represent all subterm $v$ necessary to compute a given term $u$ in a given environment $\mathbb{E}$ with the conditions $\psi$ require to have to compute $v$ and the variables $\vec{\alpha}$ bound in $u$ that can be found in $v$. The formal definition of $\phi_{\text{fresh}}^{n,v}(C(n \, v))$ is any well-typed formula in $\mathbb{E}$ such as for all model $\mathcal{M}$ of $\Theta$, and for all $\eta \in \mathbb{N}, \rho \in \mathbb{T}_{\mathcal{M}, \eta}$:

$$ \llbracket \phi_{\text{fresh}}^{n,v}(\tilde{u}) \rrbracket_{\mathbb{M}}^{\eta, \rho} = 1 \text{ implies} $$

$$ \llbracket \forall \vec{\alpha}. \psi \Rightarrow v \neq v_0 \rrbracket_{\mathbb{M}}^{\eta, \rho} = 1 $$

for every $(\vec{\alpha}, \psi, n, v_{0}) \in \mathcal{S}T_{\mathbb{E}}(\tilde{u})$

We recall the definition given for $\phi_{\text{key}}()$ and $\phi_{\text{rand}}()$ in [17], starting by some extra cases to add to the generalized subterms:

$$ ST_{\mathbb{E},k,i_k}^{\text{cca}}(\text{pk}(k \, i_0)) \stackrel{\text{def}}{=} \{(\varepsilon, \top, \text{pk}(k \, i_0))\} $$

$$ \cup ST_{\mathbb{E},k,i_k}^{\text{cca}}(i_0) \cup [i_0 \neq i_k]ST_{\mathbb{E},k,i_k}^{\text{cca}}(k \, i_0) $$

and

$$ ST_{\mathbb{E},k,i_k}^{\text{cca}}(\text{adec } u \, (k \, i_k)) $$

$$ \stackrel{\text{def}}{=} \{(\varepsilon, \top, \text{adec } u \, (k \, i_k)), (\varepsilon, \top, \text{adec})\} $$

$$ \cup ST_{\mathbb{E},k,i_k}^{\text{cca}}(u) \cup ST_{\mathbb{E},k,i_k}^{\text{cca}}(i_0) \cup [i_0 \neq i_k]ST_{\mathbb{E},k,i_k}^{\text{cca}}(k \, i_0) $$

Those represent the added capacity of the adversary given the oracles of the CCA1 game. And then, we can define $\phi_{\text{key}}()$ and
In C. NAME, and t_n and l_n are upper-bounds on, resp., the time needed by n for a single sampling, and the length of a single sampling.

$$
\begin{array}{c}
\textbf{C. INPUT}_0 \\
\tau \text{ of order } 0 \\
\mathbb{E}; \Theta; \bar{\mathbf{a}}, (x : \tau :- l) \vdash_l^c x :- l
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. INPUT}_1 \\
\tau \text{ of order } 1 \\
\mathbb{E}; \Theta; \bar{\mathbf{a}}, (f : \tau :- l, 0) \vdash_0^c f :- l
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. LET} \\
\mathbb{E}; \mathbb{E}; l_v : \overline{\text{int}}; \bar{\mathbf{a}}, (x : \tau :- l_v) \vdash_{t_u, \bar{\sigma}_u}^c u :- l_u \quad \mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_v, \bar{\sigma}_v}^c v :- l_v \quad \tau \text{ of order } 0 \\
\mathbb{E}; \Theta; \bar{\mathbf{a}} \vdash_{t_u+t_v, \bar{\sigma}_u+\bar{\sigma}_v}^c \text{let } (x : \tau) = v \text{ in } u :- l_u
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. APP}_{0} \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_u, \bar{\sigma}}^{c} u :- l_u \quad \mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_v}^{c} v :- l_v \quad \mathbb{E}; \bar{\mathbf{a}} \vdash v : \tau \quad \tau \text{ of order } 0 \quad u \notin \bar{\mathbf{a}} \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_u, l_v+t_v, \bar{\sigma}}^{c} u v :- l_u l_v
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. APP}_{1n} \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}}, (u :- l_u, j) \vdash_{t_v}^c v :- l_v \quad \mathbb{E}, \bar{\mathbf{a}} \vdash v : \tau \quad \tau \text{ of order } 0 \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}}, (u :- l_u, j + 1) \vdash_{t_u, l_v+t_v}^c u v :- l_u l_v
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. APP}_{21i} \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_u, (o_1, \dots, o_n)}^c u :- l_u \quad \mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_v}^c v :- l_v \quad v \notin \bar{\mathbf{a}} \quad \mathbb{E}, \bar{\mathbf{a}} \vdash v : \tau \quad \tau \text{ of order } 1 \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_u, l_v+t_v, (o_2, \dots, o_n)}^c u v :- l_u l_v
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. APP}_{21n} \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_u, (o_1, \dots, o_n)}^c u :- l_u \quad \tau \text{ of order } 1 \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}}, (v : \tau :- l_v, o_1) \vdash_{t_u, l_v+t_v, (o_2, \dots, o_n)}^c u v :- l_u l_v
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. NAME} \\
n \in \mathcal{N} \quad \mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_t^c i :- l \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t+t_n}^c n i :- l_n
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. ADV} \\
\mathbb{E}; \mathbb{E} \vdash \mathit{adv}_{t, \bar{\sigma}}(u) \quad \mathbb{E}; \mathbb{E} \vdash \mathit{blen}_l(u) \\
\mathbb{E}; \mathbb{E}; \emptyset \vdash_{t, \bar{\sigma}}^c u :- l
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. QUANT}_0 \\
Q \in \{\exists; \forall\} \quad \tau \text{ of order } 0 \\
\mathbb{E}; \mathbb{E}; \vdash \mathit{enum}_\tau(t_\epsilon) \quad \mathbb{E}; \mathbb{E}; \vdash \tilde{\forall}(x : \tau). \mathit{blen}_{l_\tau}(x) \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}}, (x : \tau :- l_\tau) \vdash_t^c \phi :- 1 \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_\epsilon+\sum_{x:\tau}(t+l_\tau)}^c Q(x : \tau). \phi :- 1
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. DEF:DELTA} \\
(x : \tau = u) \in \mathbb{E} \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_t^c u :- l \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_t^c x :- l
\end{array}
\qquad
\begin{array}{c}
\textbf{C. LAMBDA}_0 \\
\mathbb{E}, l_x : \overline{\text{int}}; \mathbb{E}; \bar{\mathbf{a}}, (x : \tau :- l_x) \vdash_{t, \bar{\sigma}}^c u :- l \\
\tau \text{ of order } 0 \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{\lambda l_x, t, \bar{\sigma}}^c \lambda x. u :- \lambda l_x. l
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. LAMBDA}_1 \\
\mathbb{E}, l_x : \overline{\text{int}} \to \overline{\text{int}}; \mathbb{E}, \bar{\mathbf{a}}, (x : \tau :- l_x, i) \vdash_{t, \bar{\sigma}}^c u :- l \quad \tau \text{ of order } 1 \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{\lambda l_x, t, (i, \bar{\sigma})}^c \lambda x. u :- \lambda l_x. l
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. HYPSWEAK} \\
\mathbb{E}_0 \text{ well-typed} \quad \mathbb{E}_0 \vdash \mathbb{E}_0 \quad \mathbb{E}_0 \vdash u : \tau \quad \mathbb{E}_0 \vdash \mathbb{E}_0; \bar{\mathbf{a}} \vdash_{t, \bar{\sigma}}^c u \\
\mathbb{E}_0, \mathbb{E}_1; \mathbb{E}_0, \mathbb{E}_1; \bar{\mathbf{a}} \vdash_{t, \bar{\sigma}}^c u
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. INDUCTION} \\
\mathbb{E} = \mathbb{E}_0, (f : \text{bint} \to \tau = \lambda y.b) \quad \tau \text{ of order } 0 \\
\mathbb{E}_{0, l_y} : \overline{\text{int}}; \mathbb{E}; \bar{\mathbf{a}}, (y :- l), (g :- l_f) \vdash_t^c b\{f \mapsto g\} :- l_f l_y \quad l_y \notin \mathit{fv}(t) \quad \mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_u}^c u :- l_u \quad \mathbb{E}; \mathbb{E} \vdash \det(u) \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_u+u.t}^c f u :- l_f l_u
\end{array}
$$

<caption>Figure 6. Rules for the computability predicate $\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_t^c u$.</caption>

$\phi_{\text{rand}}()$. For all model $\mathcal{M}$ of $\Theta$, for all $\eta \in \mathbb{N}$ and $\rho \in \mathbb{T}_{\mathcal{M},\eta}$, we have that:

$$
\begin{array}{l}
\text{if } \left[ \phi_{\text{key}}^{k,i}(u) \right]_{\mathbb{M}}^{\eta,\rho} = 1 \text{ then} \\
\quad \left[ \forall \vec{\alpha}. \psi \Rightarrow i \neq i_0 \right]_{\mathbb{M}}^{\eta,\rho} = 1 \\
\quad \text{for all } (\vec{\alpha}, \psi, k, i_0) \in \mathcal{ST}_{\mathbb{E},k,i}^{\text{cca}}(u)
\end{array}
$$

and

$$
\begin{array}{l}
\text{if } \left[ \phi_{\text{rand}}^{k,i}(u) \right]_{\mathbb{M}}^{\eta,\rho} = 1 \text{ then} \\
\quad \left[ \forall \vec{\alpha}. \psi \Rightarrow i \neq i_0 \right]_{\mathbb{M}}^{\eta,\rho} = 1 \\
\quad \text{for all } (\vec{\alpha}, \psi, r, i_0) \in \mathcal{ST}_{\mathbb{E},k,i}^{\text{cca}}(u).
\end{array}
$$

Finally, the formula $\phi_{\text{dec}}()$ is defined as follows:

$$
\begin{array}{l}
\text{if } \left[ \phi_{\text{dec}}^{k,i}(u) \right]_{\mathbb{M}}^{\eta,\rho} = 1 \text{ then} \\
\quad \left[ \forall \vec{\alpha}. \psi \Rightarrow i \neq i_0 \right]_{\mathbb{M}}^{\eta,\rho} = 1 \\
\quad \text{for all } (\vec{\alpha}, \psi, \text{adec } u (k i_0)) \in \mathcal{ST}_{\mathbb{E},k,i}^{\text{cca}}(u).
\end{array}
$$

APPENDIX C
PROOF TRANSFORMATIONS

A. Admissible Proofs

a) Notation: For any $b, \tilde{u} = u_1, \dots, u_n$ and $\tilde{v} = v_1, \dots, v_n$, we let if $b$ then $\tilde{u}$ else $\tilde{v}$ be the sequence of terms:

if $b$ then $u_1$ else $v_1, \dots$, if $b$ then $u_n$ else $v_n$

b) Restricting the case-study rule: We use a restricted version of the $G_\epsilon$.E:CS rule that can only be used if the
In C. NAME, and t_n and l_n are upper-bounds on, resp., the time needed by n for a single sampling, and the length of a single sampling.

$$
\begin{array}{c}
\textbf{C. INPUT}_0 \\
\tau \text{ of order } 0 \\
\vdots \\
\mathbb{E}; \Theta; \bar{\mathbf{a}}, (x : \tau :- l) \vdash_l^c x :- l
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. INPUT}_1 \\
\tau \text{ of order } 1 \\
\vdots \\
\mathbb{E}; \Theta; \bar{\mathbf{a}}, (f : \tau :- l, 0) \vdash_0^c f :- l
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. LET} \\
\mathbb{E}; \mathbb{E}; l_v : \overline{\text{int}}; \bar{\mathbf{a}}, (x : \tau :- l_v) \vdash_{t_u, \bar{\sigma}_u}^c u :- l_u \quad \mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_v, \bar{\sigma}_v}^c v :- l_v \quad \tau \text{ of order } 0 \\
\mathbb{E}; \Theta; \bar{\mathbf{a}} \vdash_{t_u+t_v, \bar{\sigma}_u+\bar{\sigma}_v}^c \text{let } (x : \tau) = v \text{ in } u :- l_u
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. APP}_{0} \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_u, \bar{\sigma}}^{c} u :- l_u \quad \mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_v}^{c} v :- l_v \quad \mathbb{E}; \bar{\mathbf{a}} \vdash v : \tau \quad \tau \text{ of order } 0 \quad u \notin \bar{\mathbf{a}} \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_u, l_v+t_v, \bar{\sigma}}^{c} u v :- l_u l_v
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. APP}_{1n} \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}}, (u :- l_u, j) \vdash_{t_v}^c v :- l_v \quad \mathbb{E}, \bar{\mathbf{a}} \vdash v : \tau \quad \tau \text{ of order } 0 \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}}, (u :- l_u, j + 1) \vdash_{t_u, l_v+t_v}^c u v :- l_u l_v
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. APP}_{21i} \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_u, (o_1, \dots, o_n)}^c u :- l_u \quad \mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_v}^c v :- l_v \quad v \notin \bar{\mathbf{a}} \quad \mathbb{E}, \bar{\mathbf{a}} \vdash v : \tau \quad \tau \text{ of order } 1 \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_u, l_v+t_v, (o_2, \dots, o_n)}^c u v :- l_u l_v
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. APP}_{21n} \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_u, (o_1, \dots, o_n)}^c u :- l_u \quad \tau \text{ of order } 1 \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}}, (v : \tau :- l_v, o_1) \vdash_{t_u, l_v+t_v, (o_2, \dots, o_n)}^c u v :- l_u l_v
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. NAME} \\
n \in \mathcal{N} \quad \mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_t^c i :- l \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t+t_n}^c n i :- l_n
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. ADV} \\
\mathbb{E}; \mathbb{E} \vdash \mathit{adv}_{t, \bar{\sigma}}(u) \quad \mathbb{E}; \mathbb{E} \vdash \mathit{blen}_l(u) \\
\mathbb{E}; \mathbb{E}; \emptyset \vdash_{t, \bar{\sigma}}^c u :- l
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. QUANT}_0 \\
Q \in \{\exists; \forall\} \quad \tau \text{ of order } 0 \\
\mathbb{E}; \mathbb{E}; \vdash \mathit{enum}_\tau(t_\epsilon) \quad \mathbb{E}; \mathbb{E}; \vdash \tilde{\forall}(x : \tau). \mathit{blen}_{l_\tau}(x) \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}}, (x : \tau :- l_\tau) \vdash_t^c \phi :- 1 \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_\epsilon+\sum_{x:\tau}(t+l_\tau)}^c Q(x : \tau). \phi :- 1
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. DEF: DELTA} \\
(x : \tau = u) \in \mathbb{E} \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_t^c u :- l \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_t^c x :- l
\end{array}
\quad
\begin{array}{c}
\textbf{C. LAMBDA}_0 \\
\mathbb{E}, l_x : \overline{\text{int}}; \mathbb{E}; \bar{\mathbf{a}}, (x : \tau :- l_x) \vdash_{t, \bar{\sigma}}^c u :- l \\
\tau \text{ of order } 0 \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{\lambda l_x, t, \bar{\sigma}}^c \lambda x. u :- \lambda l_x. l
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. LAMBDA}_1 \\
\mathbb{E}, l_x : \overline{\text{int}} \to \overline{\text{int}}; \mathbb{E}, \bar{\mathbf{a}}, (x : \tau :- l_x, i) \vdash_{t, \bar{\sigma}}^c u :- l \quad \tau \text{ of order } 1 \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{\lambda l_x, t, (i, \bar{\sigma})}^c \lambda x. u :- \lambda l_x. l
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. HYPSWEAK} \\
\mathbb{E}_0 \text{ well-typed} \quad \mathbb{E}_0 \vdash \mathbb{E}_0 \quad \mathbb{E}_0 \vdash u : \tau \quad \mathbb{E}_0 \vdash \mathbb{E}_0; \bar{\mathbf{a}} \vdash_{t, \bar{\sigma}}^c u \\
\mathbb{E}_0, \mathbb{E}_1; \mathbb{E}_0, \mathbb{E}_1; \bar{\mathbf{a}} \vdash_{t, \bar{\sigma}}^c u
\end{array}
$$

$$
\begin{array}{c}
\textbf{C. INDUCTION} \\
\mathbb{E} = \mathbb{E}_0, (f : \text{bint} \to \tau = \lambda y.b) \quad \tau \text{ of order } 0 \\
\mathbb{E}_{0, l_y} : \overline{\text{int}}; \mathbb{E}; \bar{\mathbf{a}}, (y :- l), (g :- l_f) \vdash_t^c b\{f \mapsto g\} :- l_f l_y \quad l_y \notin \mathit{fv}(t) \quad \mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_u}^c u :- l_u \quad \mathbb{E}; \mathbb{E} \vdash \mathit{det}(u) \\
\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_{t_u+u.t}^c f u :- l_f l_u
\end{array}
$$

<caption>Figure 6. Rules for the computability predicate $\mathbb{E}; \mathbb{E}; \bar{\mathbf{a}} \vdash_t^c u$.</caption>

$\phi_{\text{rand}}()$. For all model $\mathcal{M}$ of $\Theta$, for all $\eta \in \mathbb{N}$ and $\rho \in \mathbb{T}_{\mathcal{M},\eta}$, we have that:

$$
\begin{array}{l}
\text{if } \llbracket \phi_{\text{key}}^{k,i}(u) \rrbracket_{\mathbb{M}}^{\eta,\rho} = 1 \text{ then} \\
\phantom{\text{if } } \llbracket \forall \vec{\alpha}. \psi \implies i \neq i_0 \rrbracket_{\mathbb{M}}^{\eta,\rho} = 1 \\
\text{for all } (\vec{\alpha}, \psi, k \ i_0) \in \mathcal{S} \mathcal{T}_{\mathbb{E},k,i}^{\text{cca}}(u)
\end{array}
$$

and

$$
\begin{array}{l}
\text{if } \llbracket \phi_{\text{rand}}^{k,i}(u) \rrbracket_{\mathbb{M}}^{\eta,\rho} = 1 \text{ then} \\
\phantom{\text{if } } \llbracket \forall \vec{\alpha}. \psi \implies i \neq i_0 \rrbracket_{\mathbb{M}}^{\eta,\rho} = 1 \\
\text{for all } (\vec{\alpha}, \psi, r \ i_0) \in \mathcal{S} \mathcal{T}_{\mathbb{E},k,i}^{\text{cca}}(u).
\end{array}
$$

Finally, the formula $\phi_{\text{dec}}()$ is defined as follows:

$$
\begin{array}{l}
\text{if } \llbracket \phi_{\text{dec}}^{k,i}(u) \rrbracket_{\mathbb{M}}^{\eta,\rho} = 1 \text{ then} \\
\phantom{\text{if } } \llbracket \forall \vec{\alpha}. \psi \implies i \neq i_0 \rrbracket_{\mathbb{M}}^{\eta,\rho} = 1 \\
\text{for all } (\vec{\alpha}, \psi, \text{adec } u (k \ i_0)) \in \mathcal{S} \mathcal{T}_{\mathbb{E},k,i}^{\text{cca}}(u).
\end{array}
$$

APPENDIX C
PROOF TRANSFORMATIONS

A. Admissible Proofs

a) Notation: For any $b, \tilde{u} = u_1, \dots, u_n$ and $\tilde{v} = v_1, \dots, v_n$, we let if $b$ then $\tilde{u}$ else $\tilde{v}$ be the sequence of terms:

if $b$ then $u_1$ else $v_1, \dots$, if $b$ then $u_n$ else $v_n$

b) Restricting the case-study rule: We use a restricted version of the $G_\epsilon$.E:CS rule that can only be used if the
## Mixed judgements rules.

$$ \begin{array}{rcl} \mathcal{L}_{\varepsilon}.BYGLOB & & \\ \mathbb{E}; \Theta \vdash [\psi]_{\varepsilon} & & \\ \mathbb{E}; \Theta; \emptyset \vdash_{\varepsilon} \psi & & \end{array} $$

$$ \begin{array}{rcl} \mathcal{G}_{\varepsilon}.BYLOC & & \\ \mathbb{E}; \Theta; \emptyset \vdash_{\varepsilon} \psi & & \\ \mathbb{E}; \Theta \vdash [\psi]_{\varepsilon} & & \end{array} $$

$$ \begin{array}{rcl} \mathcal{L}_{\varepsilon}.LOCALISE & & \\ \mathbb{E}; \Theta; \Gamma, \phi \vdash_{\varepsilon_0} \psi & & \\ \mathbb{E}; \Theta; [\phi]_{\varepsilon_1} ; \Gamma \vdash_{\varepsilon_0+\varepsilon_1} \psi & & \end{array} $$

$$ \begin{array}{rcl} \mathcal{L}_{\varepsilon}.REWRITE-EQUIV & & \\ \mathbb{E}; \Theta; \Gamma_1 \vdash_{\varepsilon_1} \psi_1 & \mathbb{E}; \Theta \vdash (\Gamma_0 \Rightarrow \psi_0) & \sim_{\varepsilon_0} (\Gamma_1 \Rightarrow \psi_1) \\ \mathbb{E}; \Theta; \Gamma_0 \vdash_{\varepsilon_1+\varepsilon_0(1)} \psi_0 & & \end{array} $$

<caption>Figure 7. Mixed judgements rules.</caption>

$$ \begin{array}{l@{\qquad}l} \mathcal{S}\mathcal{T}_{\mathbb{E}}(x) & \stackrel{\text{def}}{=} \{ (\varepsilon, \top, x) \} & \text{(when } x : \tau) \in \mathbb{E} \text{ or } x \notin \mathbb{E} \\ \mathcal{S}\mathcal{T}_{\mathbb{E}}(x) & \stackrel{\text{def}}{=} \mathcal{S}\mathcal{T}_{\mathbb{E}}(u) & \text{(when } x : \tau = u) \in \mathbb{E} \\ \mathcal{S}\mathcal{T}_{\mathbb{E}}(u \ u') & \stackrel{\text{def}}{=} \left\{ \begin{array}{@{}l@{}} \mathcal{S}\mathcal{T}_{\mathbb{E}}(u_0\{y \mapsto u'\}) \\ \phantom{\mathcal{S}\mathcal{T}_{\mathbb{E}}(u_0\{}} \{ (\varepsilon, \top, (u \ u')) \} \cup \mathcal{S}\mathcal{T}_{\mathbb{E}}(u) \cup \mathcal{S}\mathcal{T}_{\mathbb{E}}(u') \end{array} \right. & \begin{array}{@{}l@{}} \text{(when } u \equiv x \text{ and } (x : \tau = \lambda y.u_0) \in \mathbb{E} \\ \text{(otherwise)} \end{array} \\ \mathcal{S}\mathcal{T}_{\mathbb{E}}(\lambda(x : \tau).u) & \stackrel{\text{def}}{=} \{ (\varepsilon, \top, \lambda(x : \tau).u) \} \cup (x : \tau) \cdot \mathcal{S}\mathcal{T}_{\mathbb{E}}(u) & \text{(where } x \text{ is fresh)} \\ \mathcal{S}\mathcal{T}_{\mathbb{E}}(\text{if } \phi \text{ then } u_1 \text{ else } u_0) & \stackrel{\text{def}}{=} \{ (\varepsilon, \top, \text{if } \phi \text{ then } u_1 \text{ else } u_0) \} \cup \mathcal{S}\mathcal{T}_{\mathbb{E}}(\phi) \cup [\phi] \cdot \mathcal{S}\mathcal{T}_{\mathbb{E}}(u_1) \cup [\neg \phi] \cdot \mathcal{S}\mathcal{T}_{\mathbb{E}}(u_0) \\ \mathcal{S}\mathcal{T}_{\mathbb{E}}(\text{let } (x : \tau) = u_0 \text{ in } u_1) & \stackrel{\text{def}}{=} \{ (\varepsilon, \top, \text{let } (x : \tau) = u_0 \text{ in } u_1) \} \cup \mathcal{S}\mathcal{T}_{\mathbb{E}}(u_0) \cup (x : \tau) \cdot [x = u_0] \cdot \mathcal{S}\mathcal{T}_{\mathbb{E}}(u_1) \end{array} $$

Where $[\phi]S \stackrel{\text{def}}{=} \{(\vec{\alpha}, \psi \wedge \phi, u) \mid (\vec{\alpha}, \psi, u) \in S\}$ and $(x : \tau).S \stackrel{\text{def}}{=} \{(\vec{\alpha}, x : \tau), \psi, u \mid (\vec{\alpha}, \psi, u) \in S\}$

<caption>Figure 8. Generalised subterms.</caption>

branching condition is bi-deducible from the unmodified part of the equivalence:

$$ \begin{array}{rcl} \mathcal{G}_{\varepsilon}.E:CS_{\mathbb{R}} & & \\ \mathbb{E}; \Theta \vdash \vec{u}_l, \vec{v}_l \sim_{\varepsilon_1} \vec{u}_r, \vec{v}_r & \mathbb{E}; \Theta \vdash \vec{u}_l, \vec{w}_l \sim_{\varepsilon_2} \vec{u}_r, \vec{w}_r & \\ \mathbb{E}; \Theta \vdash \mathrm{adv}_{l,\vec{o}}(C) & \mathbb{E}; \Theta \vdash \mathrm{blen}_{l}(\vec{u}_l) \tilde{\Lambda} \mathrm{blen}_{l}(\vec{u}_r) & \\ \mathbb{E}; \Theta \vdash & \vec{u}_l, & \begin{array}{l} \text{if } C \ \vec{u}_l \text{ then } \vec{v}_l \text{ else } \vec{w}_l \\ \sim_{\varepsilon'} \vec{u}_r, & \text{if } C \ \vec{u}_r \text{ then } \vec{v}_r \text{ else } \vec{w}_r \end{array} \end{array} $$

where C is a context without names and the bound $\varepsilon'$ is:

$$ \varepsilon' \stackrel{\text{def}}{=} \lambda t, \vec{a}. \varepsilon_1 (t + t_C \vec{l}) (\vec{a} + \vec{o}) + \varepsilon_2 (t + t_C \vec{l}) (\vec{a} + \vec{o}) + 1 $$

c) $(\vec{u}; \vec{v})$-admissible proofs: Let $\vec{u}$ and $\vec{v}$ be two same-length sequence of terms with compatible types. We define the set of proofs that are $(\vec{u}; \vec{v})$-admissible by induction:

* If
$$ \frac{\Pi}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_0, \vec{u}_1 \sim_{\varepsilon} \vec{v}, \vec{v}_0, \vec{v}_1} $$

is $(\vec{u}, \vec{u}_0; \vec{v}, \vec{v}_0)$-admissible then it is also $(\vec{u}; \vec{v})$-admissible.

* If L is a leaf rule then
$$ \frac{\Pi}{\mathbb{E}; \Theta \vdash \vec{u} \sim_{\varepsilon} \vec{v}} \text{ L is} $$

* If
$$ \frac{\Pi}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_0 \sim_{\varepsilon} \vec{v}, \vec{v}_0} \text{ is } (\vec{u}; \vec{v})\text{-admissible then} \\ \frac{\Pi}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_0 \sim_{\varepsilon} \vec{v}, \vec{v}_0} \dots \\ \frac{\Pi}{\mathbb{E}; \Theta \vdash \vec{u}, (C_1, \dots, C_n) \vec{u} \ \vec{u}_0 \ \vec{n}} \text{ G}_{\varepsilon}.E:BI-DEDUCE} \\ \sim_{\varepsilon'} \vec{v}, (C_1, \dots, C_n) \vec{v} \ \vec{v}_0 \ \vec{n} $$

is $(\vec{u}; \vec{v})$-admissible. Note that the immutable components of the proof $\vec{u}$ and $\vec{v}$ must be exactly the part of the conclusion that is not touched by the bi-deduction rule.

* If
$$ \frac{\Pi_0}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_0 \sim_{\varepsilon} \vec{v}, \vec{v}_0} \text{ and } \frac{\Pi_1}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_1 \sim_{\varepsilon} \vec{v}, \vec{v}_1} \text{ are} \\ (\vec{u}; \vec{v})\text{-admissible then the following application of the} \\ \mathcal{G}_{\varepsilon}.E:CS_{\mathbb{R}} \text{ rule:} $$

$$ \frac{\Pi_0}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_0 \sim_{\varepsilon_0} \vec{v}, \vec{v}_0} \qquad \frac{\Pi_1}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_1 \sim_{\varepsilon_1} \vec{v}, \vec{v}_1} \dots \\ \mathbb{E}; \Theta \vdash \vec{u}, \text{ if } C \ \vec{u} \text{ then } \vec{u}_0 \text{ else } \vec{u}_1 \\ \sim_{\varepsilon'} \vec{u}, \text{ if } C \ \vec{v} \text{ then } \vec{v}_0 \text{ else } \vec{v}_1 $$

is $(\vec{u}; \vec{v})$-admissible, where C is a context without names. Note that the case-study branching conditions $C \vec{u}$ and $C \vec{v}$ must be fully computable from the immutable components $\vec{u}$ and $\vec{v}$.

* If
$$ \frac{\Pi}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_0 \sim_{\varepsilon} \vec{v}, \vec{v}_0} \text{ is } (\vec{u}; \vec{v})\text{-admissible then} \\ \frac{\Pi}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_1 \sim_{\varepsilon'} \vec{v}, \vec{v}_1} \text{ R} $$

is $(\vec{u}; \vec{v})$-admissible, where the auxiliary premises $\Pi_{\mathrm{Aux}}$ of rule R (if there are any) are arbitrary proofs, and $\vec{u}_1$ and $\vec{v}_1$ are arbitrary terms (such that the derivation above is valid).

d) Positions, paths: We define the path to a position in a proof as the set of all prefix positions of this position. Given an admissible proof $\Pi$, we denote Trunk($\Pi$) its trunk, Aux<sub>Proof</sub>($\Pi$) the multi-set of the auxiliary proof of $\Pi$. Also, given a position $p \in$ Trunk($\Pi$), we let Path<sub>Π</sub>(p) the path from the root of $\Pi$ to position p, and $R_{\Pi}(p)$ the rule at position p.
## Mixed judgements rules.

$$ \begin{array}{rcl} \mathcal{L}_{\varepsilon}.BYGLOB & & \\ \mathbb{E}; \Theta \vdash [\psi]_{\varepsilon} & & \\ \mathbb{E}; \Theta; \emptyset \vdash_{\varepsilon} \psi & & \end{array} $$

$$ \begin{array}{rcl} \mathcal{G}_{\varepsilon}.BYLOC & & \\ \mathbb{E}; \Theta; \emptyset \vdash_{\varepsilon} \psi & & \\ \mathbb{E}; \Theta \vdash [\psi]_{\varepsilon} & & \end{array} $$

$$ \begin{array}{rcl} \mathcal{L}_{\varepsilon}.LOCALISE & & \\ \mathbb{E}; \Theta; \Gamma, \phi \vdash_{\varepsilon_0} \psi & & \\ \mathbb{E}; \Theta; [\phi]_{\varepsilon_1} ; \Gamma \vdash_{\varepsilon_0+\varepsilon_1} \psi & & \end{array} $$

$$ \begin{array}{rcl} \mathcal{L}_{\varepsilon}.REWRITE-EQUIV & & \\ \mathbb{E}; \Theta; \Gamma_1 \vdash_{\varepsilon_1} \psi_1 & \mathbb{E}; \Theta \vdash (\Gamma_0 \Rightarrow \psi_0) & \sim_{\varepsilon_0} (\Gamma_1 \Rightarrow \psi_1) \\ \mathbb{E}; \Theta; \Gamma_0 \vdash_{\varepsilon_1+\varepsilon_0(1)} \psi_0 & & \end{array} $$

<caption>Figure 7. Mixed judgements rules.</caption>

$$ \begin{array}{l@{\qquad}l} \mathcal{S}\mathcal{T}_{\mathbb{E}}(x) & \stackrel{\text{def}}{=} \{(\varepsilon, \top, x)\} & \text{(when } x : \tau) \in \mathbb{E} \text{ or } x \notin \mathbb{E}) \\ \mathcal{S}\mathcal{T}_{\mathbb{E}}(x) & \stackrel{\text{def}}{=} \mathcal{S}\mathcal{T}_{\mathbb{E}}(u) & \text{(when } x : \tau = u) \in \mathbb{E}) \\ \mathcal{S}\mathcal{T}_{\mathbb{E}}(u \ u') & \stackrel{\text{def}}{=} \left\{ \begin{array}{@{}l@{}} \mathcal{S}\mathcal{T}_{\mathbb{E}}(u_0\{y \mapsto u'\}) \\ \quad \{(\varepsilon, \top, (u \ u'))\} \cup \mathcal{S}\mathcal{T}_{\mathbb{E}}(u) \cup \mathcal{S}\mathcal{T}_{\mathbb{E}}(u') \end{array} \right. & \begin{array}{@{}l@{}} \text{(when } u \equiv x \text{ and } (x : \tau = \lambda y.u_0) \in \mathbb{E}) \\ \text{(otherwise)} \end{array} \\ \mathcal{S}\mathcal{T}_{\mathbb{E}}(\lambda(x : \tau).u) & \stackrel{\text{def}}{=} \{(\varepsilon, \top, \lambda(x : \tau).u)\} \cup (x : \tau) \cdot \mathcal{S}\mathcal{T}_{\mathbb{E}}(u) & \text{(where } x \text{ is fresh)} \\ \mathcal{S}\mathcal{T}_{\mathbb{E}}(\text{if } \phi \text{ then } u_1 \text{ else } u_0) & \stackrel{\text{def}}{=} \{(\varepsilon, \top, \text{if } \phi \text{ then } u_1 \text{ else } u_0)\} \cup \mathcal{S}\mathcal{T}_{\mathbb{E}}(\phi) \cup [\phi] \cdot \mathcal{S}\mathcal{T}_{\mathbb{E}}(u_1) \cup [\neg \phi] \cdot \mathcal{S}\mathcal{T}_{\mathbb{E}}(u_0) \\ \mathcal{S}\mathcal{T}_{\mathbb{E}}(\text{let } (x : \tau) = u_0 \text{ in } u_1) & \stackrel{\text{def}}{=} \{(\varepsilon, \top, \text{let } (x : \tau) = u_0 \text{ in } u_1)\} \cup \mathcal{S}\mathcal{T}_{\mathbb{E}}(u_0) \cup (x : \tau) \cdot [x = u_0] \cdot \mathcal{S}\mathcal{T}_{\mathbb{E}}(u_1) \end{array} $$

Where $[\phi]S \stackrel{\text{def}}{=} \{(\vec{\alpha}, \psi \wedge \phi, u) \mid (\vec{\alpha}, \psi, u) \in S\}$ and $(x : \tau).S \stackrel{\text{def}}{=} \{(\vec{\alpha}, x : \tau), \psi, u \mid (\vec{\alpha}, \psi, u) \in S\}$

<caption>Figure 8. Generalised subterms.</caption>

branching condition is bi-deducible from the unmodified part of the equivalence:

$$ \begin{array}{rcl} \mathcal{G}_{\varepsilon}.E:CS_{\mathbb{R}} & & \\ \mathbb{E}; \Theta \vdash \vec{u}_l, \vec{v}_l \sim_{\varepsilon_1} \vec{u}_r, \vec{v}_r & \mathbb{E}; \Theta \vdash \vec{u}_l, \vec{w}_l \sim_{\varepsilon_2} \vec{u}_r, \vec{w}_r & \\ \mathbb{E}; \Theta \vdash \mathrm{adv}_{l,\vec{o}}(C) & \mathbb{E}; \Theta \vdash \mathrm{blen}_{l}^{\vec{u}}(\vec{u}_l) \wedge \mathrm{blen}_{l}^{\vec{v}}(\vec{v}_r) & \\ \mathbb{E}; \Theta \vdash & \vec{u}_l, & \begin{array}{l} \text{if } C \ \vec{u}_l \text{ then } \vec{v}_l \text{ else } \vec{w}_l \\ \sim_{\varepsilon'} \vec{u}_r, & \text{if } C \ \vec{u}_r \text{ then } \vec{v}_r \text{ else } \vec{w}_r \end{array} \end{array} $$

where C is a context without names and the bound $\varepsilon'$ is:

$$ \varepsilon' \stackrel{\text{def}}{=} \lambda t, \vec{a}. \varepsilon_1 (t + t_C \vec{l}) (\vec{a} + \vec{o}) + \varepsilon_2 (t + t_C \vec{l}) (\vec{a} + \vec{o}) + 1 $$

c) $(\vec{u}; \vec{v})$-admissible proofs: Let $\vec{u}$ and $\vec{v}$ be two same-length sequence of terms with compatible types. We define the set of proofs that are $(\vec{u}; \vec{v})$-admissible by induction:

* If
$$ \frac{\Pi}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_0, \vec{u}_1 \sim_{\varepsilon} \vec{v}, \vec{v}_0, \vec{v}_1} $$

is $(\vec{u}, \vec{u}_0; \vec{v}, \vec{v}_0)$-admissible then it is also $(\vec{u}; \vec{v})$-admissible.

* If L is a leaf rule then
$$ \frac{\Pi}{\mathbb{E}; \Theta \vdash \vec{u} \sim_{\varepsilon} \vec{v}} \text{ L is} $$

* If
$$ \frac{\Pi}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_0 \sim_{\varepsilon} \vec{v}, \vec{v}_0} \text{ is } (\vec{u}; \vec{v})\text{-admissible then} \\ \frac{\Pi}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_0 \sim_{\varepsilon} \vec{v}, \vec{v}_0} \dots \\ \frac{\Pi}{\mathbb{E}; \Theta \vdash \vec{u}, (C_1, \dots, C_n) \vec{u} \ \vec{u}_0 \ \vec{n}} \text{ G}_{\varepsilon}.E:BI-DEDUCE} \\ \sim_{\varepsilon'} \vec{v}, (C_1, \dots, C_n) \vec{v} \ \vec{v}_0 \ \vec{n} $$

is $(\vec{u}; \vec{v})$-admissible. Note that the immutable components of the proof $\vec{u}$ and $\vec{v}$ must be exactly the part of the conclusion that is not touched by the bi-deduction rule.

* If
$$ \frac{\Pi_0}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_0 \sim_{\varepsilon} \vec{v}, \vec{v}_0} \text{ and } \frac{\Pi_1}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_1 \sim_{\varepsilon} \vec{v}, \vec{v}_1} \text{ are} \\ (\vec{u}; \vec{v})\text{-admissible then the following application of the} \\ \text{G}_{\varepsilon}.E:CS_{\mathbb{R}} \text{ rule:} $$

$$ \frac{\Pi_0}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_0 \sim_{\varepsilon_0} \vec{v}, \vec{v}_0} \qquad \frac{\Pi_1}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_1 \sim_{\varepsilon_1} \vec{v}, \vec{v}_1} \dots \\ \mathbb{E}; \Theta \vdash \vec{u}, \text{ if } C \ \vec{u} \text{ then } \vec{u}_0 \text{ else } \vec{u}_1 \\ \sim_{\varepsilon'} \vec{u}, \text{ if } C \ \vec{v} \text{ then } \vec{v}_0 \text{ else } \vec{v}_1 $$

is $(\vec{u}; \vec{v})$-admissible, where C is a context without names. Note that the case-study branching conditions $C \vec{u}$ and $C \vec{v}$ must be fully computable from the immutable components $\vec{u}$ and $\vec{v}$.

* If
$$ \frac{\Pi}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_0 \sim_{\varepsilon} \vec{v}, \vec{v}_0} \text{ is } (\vec{u}; \vec{v})\text{-admissible then} \\ \frac{\Pi}{\mathbb{E}; \Theta \vdash \vec{u}, \vec{u}_1 \sim_{\varepsilon'} \vec{v}, \vec{v}_1} \text{ R} $$

is $(\vec{u}; \vec{v})$-admissible, where the auxiliary premises $\Pi_{\mathrm{Aux}}$ of rule R (if there are any) are arbitrary proofs, and $\vec{u}_1$ and $\vec{v}_1$ are arbitrary terms (such that the derivation above is valid).

d) Positions, paths: We define the path to a position in a proof as the set of all prefix positions of this position. Given an admissible proof $\Pi$, we denote Trunk($\Pi$) its trunk, Aux<sub>Proof</sub>($\Pi$) the multi-set of the auxiliary proof of $\Pi$. Also, given a position $p \in$ Trunk($\Pi$), we let Path<sub>Π</sub>(p) the path from the root of $\Pi$ to position p, and $R_{\Pi}(p)$ the rule at position p.
## B. Discussion: Rule Restrictions

We quickly discuss why we do not support some rules in our proof-transformation result, and the impact that removing these rules has.

We do not support the transitivity rule because of the completely new terms that appear in the premises, which cannot be linked to the terms in the conclusion. This prevent us from commuting this rule, notably with the bi-deduction rule, as we do not know how to establish the new auxiliary proof obligations appearing after commutation. Removing transitivity has a limited impact on expressivity, as rules that need it already incorporate a (single, controlled) transitivity step. For example, this is the case for cryptographic rules, and explains some differences in presentation between our G<sub>ε</sub>.CCA1 rule and the CCA1 rule of [17].

We believe our result could have been extended to support the upper-bound weakening rules and the left disjunction rules could have been, but at the cost of a more complicated presentation.

## C. Termination of ►AD

We now sketch the proof of Lemma 1.

**Lemma 1.** The relation ►AD terminates on any admissible proof Π. Moreover, if Π is an admissible proof irreducible w.r.t. ►AD then no ascending rule appears below a descending rule on the trunk of Π.

*Proof sketch.* Let Π be a transformable proof.

Given a position *p* in the trunk of Π, we define HW(*p*), CB(*p*), then Value<sub>►AD</sub>(Π) in Fig. 13. We can show that this value strictly decreases (for the lexicographic ordering) for any proof transformation in ►AD. Thus the proof-transformation relation ►AD terminate.

Let Π<sub>T</sub> a proof in normal form for ►AD. Assume by contradiction that there exists a position *p* ∈ Trunk(Π) at which a descending rule is applied, and such as there exists *q* ∈ Path<sub>Π</sub>(*p*) such that the rule applied at *q* is ascending.

We can assume without lost of generality that *q* is the greatest strict prefix of *p*. To conclude, we observe that if *q* is the greatest strict prefix of *p*, then the proof transformation ▷<sub>R<sub>Π</sub>(*q*)</sub> applies. Thus, Π is not in normal form. Contradiction. □

## D. Termination of the Collapse Proof Transformations

We now sketch the proof of Lemma 2 which we omitted from the body.

**Lemma 2.** Let $\vec{u} \sim_{\varepsilon} \vec{v}$ be an equivalence predicate such that $\vec{u} \neq \vec{v}$. Let $\Pi$ be an $(\vec{u}, \vec{v})$-collapsible proof where all occurrences of G. AXIOM in the trunk are on $\vec{u} \sim_{\varepsilon} \vec{v}$. Then, the rewrite relation ►col terminates on Π and yields proofs with at most one application of this axiom rule in the trunk.

*Proof sketch.* First, we can show that Π doesn't contain any G<sub>ε</sub>.E:REFL leaf in it trunk: indeed, if that happens, we can show that $\vec{u} = \vec{v}$ just by looking at all the cases of the rule before it.

We reuse the new numerical quantity Count-CB<sub>Π</sub>(*p*) defined in Fig. 13. Then, we let:

$$A_{R_0}(\Pi) = \sum_{p \in \text{Trunk}(\Pi)} \text{Count-CB}_{\Pi}(p).$$

Notice that:

$$A_{R_0}(\Pi) = \sum_{p \in \text{Trunk}(\Pi) \wedge R_{\Pi}(p) = G_{\varepsilon}.E:\text{REWRITE}_0} \text{Count-CB}_{\Pi}(p)$$

since G<sub>ε</sub>.E:REWRITE<sub>0</sub> is the only ascending rule allowed in a collapsable proof.

We define a new quantity Count-HW<sub>Π</sub><sup>col</sup>(*p*) similarly to Count-HW<sub>Π</sub>(*p*) but for all rules that are not G. WEAK instead of just the ascending rules.

Now, We can define the decreasing quantity for the ►col w.r.t the lexicographic order, as such :

$$ \left( \left| \left\{ \begin{array}{l} p \in \text{Trunk}(\Pi) \mid R_{\Pi}(p) = \begin{array}{l} G_{\varepsilon}.E:CS_{R} \\ \text{or} \\ G_{\varepsilon}.E:BI-DEDUCE \end{array} \end{array} \right\} \right| \right) \times \left| \left\{ p \in \text{Trunk}(\Pi) \mid R_{\Pi}(p) = G.WEAK \right\} \right| $$

Finally, we analyze what are the possible shapes of proofs in normal form w.r.t ►col by case study.

Indeed, we can notice that it cannot have any G. WEAK since it has a transformation with every rule, and all the G<sub>ε</sub>.E:REWRITE<sub>0</sub> are at the bottom since it have a com-mutation with every ascending rule. Therefore, it there is a G<sub>ε</sub>.E:CS Consider the higher such rule (meaning that it doesn't have any G<sub>ε</sub>.E:CS above it), then it cannot have G. AXIOM above it since a proof obligation of G<sub>ε</sub>.E:CS cannot be $\vec{u} \sim \vec{v}$ directly. And it cannot have any other leaf as one of it proofs since it can be transformed. Therefore, both rule directly above the G<sub>ε</sub>.E:CS is a G<sub>ε</sub>.E:BI-DEDUCE, which at it turn cannot have anything above it except a G. AXIOM and therefore collapse. So, there is not any G<sub>ε</sub>.E:CS rule. As this is the only rule with two principal premises, there cannot remain more than one application of the axiom rule. □

## E. Proof Fragment ε/poly<sup>χ<sub>ε</sub>,n</sup><sub>M</sub>

a) Definition of negligibility for ε and of polynomial for *t* and *l*: We define a semantical notion of polynomial-time for the time, oracles calls and length annotations, and a notion of negligibility for the upper-bound annotations. Note that it is given relatively to a formal variable *N* of type bint, used to interpret the number of inductive steps of the proof.

We say that a term ε is a negligible term w.r.t. *N* in a model M, which we write negl<sup>N</sup><sub>M</sub>(ε), if one of the following case holds:

* ε is of type real and for any P ∈ N[η],

$$E_{\rho}(\llbracket \varepsilon \rrbracket_{M}^{\eta, \rho}[N \mapsto P(\eta)]) \in \text{negl}(\eta).$$
## B. Discussion: Rule Restrictions

We quickly discuss why we do not support some rules in our proof-transformation result, and the impact that removing these rules has.

We do not support the transitivity rule because of the completely new terms that appear in the premises, which cannot be linked to the terms in the conclusion. This prevent us from commuting this rule, notably with the bi-deduction rule, as we do not know how to establish the new auxiliary proof obligations appearing after commutation. Removing transitivity has a limited impact on expressivity, as rules that need it already incorporate a (single, controlled) transitivity step. For example, this is the case for cryptographic rules, and explains some differences in presentation between our G<sub>ε</sub>.CCA1 rule and the CCA1 rule of [17].

We believe our result could have been extended to support the upper-bound weakening rules and the left disjunction rules could have been, but at the cost of a more complicated presentation.

## C. Termination of ►AD

We now sketch the proof of Lemma 1.

**Lemma 1.** The relation ►AD terminates on any admissible proof Π. Moreover, if Π is an admissible proof irreducible w.r.t. ►AD then no ascending rule appears below a descending rule on the trunk of Π.

*Proof sketch.* Let Π be a transformable proof.

Given a position *p* in the trunk of Π, we define HW(*p*), CB(*p*), then Value<sub>►AD</sub>(Π) in Fig. 13. We can show that this value strictly decreases (for the lexicographic ordering) for any proof transformation in ►AD. Thus the proof-transformation relation ►AD terminate.

Let Π<sub>T</sub> a proof in normal form for ►AD. Assume by contradiction that there exists a position *p* ∈ Trunk(Π) at which a descending rule is applied, and such as there exists *q* ∈ Path<sub>Π</sub>(*p*) such that the rule applied at *q* is ascending.

We can assume without lost of generality that *q* is the greatest strict prefix of *p*. To conclude, we observe that if *q* is the greatest strict prefix of *p*, then the proof transformation ▷<sub>R<sub>Π</sub>(*q*)</sub> applies. Thus, Π is not in normal form. Contradiction. □

## D. Termination of the Collapse Proof Transformations

We now sketch the proof of Lemma 2 which we omitted from the body.

**Lemma 2.** Let $\vec{u} \sim_{\varepsilon} \vec{v}$ be an equivalence predicate such that $\vec{u} \neq \vec{v}$. Let $\Pi$ be an $(\vec{u}, \vec{v})$-collapsible proof where all occurrences of G. AXIOM in the trunk are on $\vec{u} \sim_{\varepsilon} \vec{v}$. Then, the rewrite relation ►col terminates on Π and yields proofs with at most one application of this axiom rule in the trunk.

*Proof sketch.* First, we can show that Π doesn't contain any G<sub>ε</sub>.E:REFL leaf in it trunk: indeed, if that happens, we can show that $\vec{u} = \vec{v}$ just by looking at all the cases of the rule before it.

We reuse the new numerical quantity Count-CB<sub>Π</sub>(*p*) defined in Fig. 13. Then, we let:

$$A_{R_0}(\Pi) = \sum_{p \in \text{Trunk}(\Pi)} \text{Count-CB}_{\Pi}(p).$$

Notice that:

$$A_{R_0}(\Pi) = \sum_{p \in \text{Trunk}(\Pi) \wedge R_{\Pi}(p) = G_{\varepsilon}.E:\text{REWRITE}_0} \text{Count-CB}_{\Pi}(p)$$

since G<sub>ε</sub>.E:REWRITE<sub>0</sub> is the only ascending rule allowed in a collapsable proof.

We define a new quantity Count-HW<sub>Π</sub><sup>col</sup>(*p*) similarly to Count-HW<sub>Π</sub>(*p*) but for all rules that are not G. WEAK instead of just the ascending rules.

Now, We can define the decreasing quantity for the ►col w.r.t the lexicographic order, as such :

$$ \left( \left| \left\{ \begin{array}{l} p \in \text{Trunk}(\Pi) \mid R_{\Pi}(p) = \\ \qquad \begin{array}{l} G_{\varepsilon}.E:CS_{R} \\ \qquad \text{or} \\ \qquad G_{\varepsilon}.E:BI-DEDUCE \end{array} \end{array} \right\} \right| \\ , A_{R_0}(\Pi), \sum_{p \in \text{Trunk}(\Pi)} \text{Count-HW}_{\Pi}^{\text{col}}(p), \\ \left| \{p \in \text{Trunk}(\Pi) \mid R_{\Pi}(p) = G.\text{WEAK}\} \right| \right) $$

Finally, we analyze what are the possible shapes of proofs in normal form w.r.t ►col by case study.

Indeed, we can notice that it cannot have any G. WEAK since it has a transformation with every rule, and all the G<sub>ε</sub>.E:REWRITE<sub>0</sub> are at the bottom since it have a com-mutation with every ascending rule. Therefore, it there is a G<sub>ε</sub>.E:CS Consider the higher such rule (meaning that it doesn't have any G<sub>ε</sub>.E:CS above it), then it cannot have G. AXIOM above it since a proof obligation of G<sub>ε</sub>.E:CS cannot be $\vec{u} \sim \vec{v}$ directly. And it cannot have any other leaf as one of it proofs since it can be transformed. Therefore, both rule directly above the G<sub>ε</sub>.E:CS is a G<sub>ε</sub>.E:BI-DEDUCE, which at it turn cannot have anything above it except a G. AXIOM and therefore collapse. So, there is not any G<sub>ε</sub>.E:CS rule. As this is the only rule with two principal premises, there cannot remain more than one application of the axiom rule. □

## E. Proof Fragment ε/poly<sup>χ<sub>ε</sub>,n</sup><sub>M</sub>

a) Definition of negligibility for ε and of polynomial for *t* and *l*: We define a semantical notion of polynomial-time for the time, oracles calls and length annotations, and a notion of negligibility for the upper-bound annotations. Note that it is given relatively to a formal variable *N* of type bint, used to interpret the number of inductive steps of the proof.

We say that a term ε is a negligible term w.r.t. *N* in a model M, which we write negl<sup>N</sup><sub>M</sub>(ε), if one of the following case holds:

* ε is of type real and for any P ∈ N[η],

$$E_{\rho}(\llbracket \varepsilon \rrbracket_{M}^{\eta, \rho}[N \mapsto P(\eta)]) \in \text{negl}(\eta).$$
• $\varepsilon$ is of type $\overline{\text{int}}^l \to \overline{\text{real}}$ and for any, $P \in \mathbb{N}[\eta]$, $P_1, \dots, P_l \in \mathbb{Z}[\eta]$

$$E_{\rho}(\llbracket \varepsilon \rrbracket_{\mathbb{M}}^{\eta, \rho}_{N \mapsto P(\eta)} (P_1(\eta), \dots, P_l(\eta))) \in \text{negl}(\eta).$$

We say that a term $u$ is a polynomial term w.r.t. $N$ in a model $\mathbb{M}$, which we write $\text{poly}_{\mathbb{M}}^N(u)$, if one of the following case holds:

• $u$ is of type $\overline{\text{int}}$ and for any $P \in \mathbb{N}[\eta]$,

$$\sup_{\rho}(\llbracket u \rrbracket_{\mathbb{M}}^{\eta, \rho}_{N \mapsto P(\eta)}) \in \mathbb{Z}[\eta].$$

• $u$ is of type $\overline{\text{int}}^l \to \overline{\text{int}}$ and for any $P \in \mathbb{N}[\eta]$, $P_1, \dots, P_l \in \mathbb{Z}[\eta]$,

$$\sup_{\rho}(\llbracket u \rrbracket_{\mathbb{M}}^{\eta, \rho}_{N \mapsto P(\eta)} (P_1(\eta), \dots, P_l(\eta))) \in \mathbb{Z}[\eta].$$

Such a term is called an order one polynomial, and the set of such functions is noted $\mathbb{Z}_1[\eta]$.

• $u$ is of type

$$(\overline{\text{int}}^{k_i} \to \overline{\text{int}})^m \to \overline{\text{int}}^l \to \overline{\text{int}}$$

and for any

$$P \in \mathbb{N}[\eta] \qquad f_1, \dots, f_m \in \mathbb{Z}_1[\eta]$$

$$P_{1,1}, \dots, P_{1,k_1}, \dots, P_{m,1}, \dots, P_{m,k_m} \in \mathbb{Z}[\eta]$$

$$P_1, \dots, P_l \in \mathbb{Z}[\eta],$$

the following quantity is a polynomial in $\mathbb{Z}[\eta]$:

$$\sup_{\rho} \left( \llbracket u \rrbracket_{\mathbb{M}}^{\eta, \rho}_{N \mapsto P(\eta)} \left( \begin{array}{c} f_1(P_{1,1}(\eta), \dots, P_{1,k_1}), \\ \vdots, f_m(P_{m,1}(\eta), \dots, P_{m,k_m}(\eta)), \\ P_1(\eta), \dots, P_l(\eta) \end{array} \right) \right)$$

b) Definition of $\varepsilon/\text{poly}$ :: Let $n$ be a variable of type bint.

We say that a global formula $F$ is poly-secure compatible w.r.t. $n$ and a model $\mathbb{M}$ when all the advantages, time and length terms appearing in its predicates are polynomial or negligible (according to their type) w.r.t $n$ and $\mathbb{M}$.

Similarly, a judgement is poly-secure compatible (w.r.t. $n$ and $\mathbb{M}$) if its conclusion is poly-secure compatible. If we consider a local or a time judgement, we also require that the advantage or time term labeling the judgement are poly-secure compatible.

Let $\varepsilon_x$ be variable of a type compatible with $\vec{u}; \vec{v}$, in the sense that $\vec{u} \sim_{x_\varepsilon} \vec{v}$ is a well-typed predicate. We say that a proof $\Pi$ which is $(\vec{u}; \vec{v})$-admissible proof is $\varepsilon$-linear with polynomial overhead w.r.t. $x_\varepsilon$, $n$ and $\mathbb{M}$, which we write $\varepsilon/\text{poly}_{\mathbb{M}}^{x_\varepsilon, n}$, if all its auxiliary judgements are poly-secure compatible w.r.t. $n$ and $\mathbb{M}$, and if the advantage at the conclusion of $\Pi$ is of the form:

$$\lambda t, \vec{o}. \varepsilon_0 + \sum_i x_\varepsilon (t + t_i) (\vec{o} + \vec{o}_i)$$

where $t$ and $\vec{o}$ do not occur in $t_i$ and $\vec{o}_i$ (for any $i$), and where $x_\varepsilon$ does not occur in $\varepsilon_0$. The crucial point, here, is that the time over-heads $t_i$ and the oracle calls overheads $\vec{o}_i$ do not depend on the execution time of the adversary, tough they can of course depends on the protocol. Without this, it would not

be possible to bound the time in the full inductive proof by a polynomial.

**Remark 3.** If $\Pi$ is $\varepsilon/\text{poly}_{\mathbb{M}}^{x_\varepsilon, n}$, then any transformation of $\Pi$ by the transformation relations $\triangleright_{\text{AD}}$ and $\triangleright_{\text{col}}$ is also $\varepsilon/\text{poly}_{\mathbb{M}}^{x_\varepsilon, n}$. This can be checked by a simple case analysis of all proof transformations.

**Proposition 1.** Let $\Pi$ be a $(\vec{u}; \vec{v})$-admissible proof that only use G. AXIOM as its leafs in it trunk and only on one particular conclusion $u \sim_{x_\varepsilon} v$, where $x_\varepsilon$ is a variable.

The advantage of its conclusion $\varepsilon_{\text{final}}$ is of the form:

$$\varepsilon_{\text{final}} = \lambda t, \vec{o}. \varepsilon_0 + \sum_{i=1}^{k} (x_\varepsilon (t + t_i) (\vec{o} + \vec{o}_i))$$

where $k$ is the number of G. AXIOM in the trunk of $\Pi$.

Furthermore, if $\mathbb{M}$ is such that $\Pi$ is $\varepsilon/\text{poly}_{\mathbb{M}}^{x_\varepsilon, n}$ (for some $n$), then:

$$\forall i, \text{poly}_{\mathbb{M}}^n(t_i) \wedge \text{poly}_{\mathbb{M}}^n(\vec{o}_i)$$

where a vector is polynomial if each of its component is.

Finally, if $\mathbb{M}$ is a model such that $\text{negl}_{\mathbb{M}}^n(\varepsilon_{\text{CCA1}})$ and $\text{negl}_{\mathbb{M}}^n(\varepsilon_{\text{PRF}})$ holds, then $\text{negl}_{\mathbb{M}}^n(\varepsilon_0)$ holds as well.

This can be proven by induction on the inductive definition of admissible proof, by case analysis over all possible rules involved

## F. Obtaining a Polynomial Level of Security

We now recall and prove Lemma 3.

**Lemma 3.** Let $\Pi$ be an $(u n; v n)$-admissible proof proving the inductive premise of the rule above where: the only occurrence of G. AXIOM in the trunk is on the induction hypothesis $u n \sim_{\varepsilon n} v n$; and where the induction hypothesis and $x_\varepsilon$ are only used in the trunk.

Then there exists $\Pi_{\text{poly}}$ proving the inductive case of $\mathbb{N}$-IND with an improved upper-bound $\varepsilon_{\text{ih}}^{\text{negl}}$, i.e. $\Pi_{\text{poly}}$ proves:

$$E'; \Theta, u n \sim_{x_\varepsilon} v n \vdash u n, u' (n+1) \sim_{\varepsilon_{\text{ih}}^{\text{negl}}} v n, v' (n+1)$$

where $\varepsilon_{\text{ih}}^{\text{negl}}$ is such that the final advantage $\varepsilon^{\text{negl}}$, defined from $\varepsilon_{\text{ih}}^{\text{negl}}$ as described in Eq. (7), is such that for any $\mathbb{M}$ where:

• $\Pi$ is in $\varepsilon/\text{poly}_{\mathbb{M}}^{x_\varepsilon, n}$, i.e. (roughly) the advantage terms (resp. time and length terms) appearing in all auxiliary sub-proofs of $\Pi$ are negligible (resp. polynomial) in $\mathbb{M}$, for any number of session $n$ and adversarial time $t$ which are polynomial in $\eta$. See Appendix C-E for a formal definition of $\varepsilon/\text{poly}_{\mathbb{M}}^{x_\varepsilon, n}$.

• The initial advantage bound $\varepsilon_0$ and the cryptographic advantages $\varepsilon_{\text{CCA1}}$ and $\varepsilon_{\text{PRF}}$ must be negligible for adversaries running in time polynomial in $\eta$.

Then the term $\varepsilon^{\text{negl}}$ is a negligible term w.r.t. $n$ and $\mathbb{M}$, i.e. for any polynomials $P_n, P_t \in \mathbb{N}[\eta]$ bounding, resp., the number of sessions and the execution time of the adversary:

$$E_{\rho}(\llbracket \varepsilon^{\text{negl}} n \rrbracket_{\mathbb{M}}^{\eta; \rho} (P_t(\eta)) \in \text{negl}(\eta))$$
• $\varepsilon$ is of type $\overline{\text{int}}^l \to \overline{\text{real}}$ and for any, $P \in \mathbb{N}[\eta]$, $P_1, \dots, P_l \in \mathbb{Z}[\eta]$

$$E_{\rho}(\llbracket \varepsilon \rrbracket_{\mathbb{M}}^{\eta, \rho}_{N \mapsto P(\eta)} (P_1(\eta), \dots, P_l(\eta))) \in \text{negl}(\eta).$$

We say that a term $u$ is a polynomial term w.r.t. $N$ in a model $\mathbb{M}$, which we write $\text{poly}_{\mathbb{M}}^N(u)$, if one of the following case holds:

• $u$ is of type $\overline{\text{int}}$ and for any $P \in \mathbb{N}[\eta]$,

$$\sup_{\rho}(\llbracket u \rrbracket_{\mathbb{M}}^{\eta, \rho}_{N \mapsto P(\eta)}) \in \mathbb{Z}[\eta].$$

• $u$ is of type $\overline{\text{int}}^l \to \overline{\text{int}}$ and for any $P \in \mathbb{N}[\eta]$, $P_1, \dots, P_l \in \mathbb{Z}[\eta]$,

$$\sup_{\rho}(\llbracket u \rrbracket_{\mathbb{M}}^{\eta, \rho}_{N \mapsto P(\eta)} (P_1(\eta), \dots, P_l(\eta))) \in \mathbb{Z}[\eta].$$

Such a term is called an order one polynomial, and the set of such functions is noted $\mathbb{Z}_1[\eta]$.

• $u$ is of type

$$(\overline{\text{int}}^{k_i} \to \overline{\text{int}})^m \to \overline{\text{int}}^l \to \overline{\text{int}}$$

and for any

$$P \in \mathbb{N}[\eta] \qquad f_1, \dots, f_m \in \mathbb{Z}_1[\eta]$$

$$P_{1,1}, \dots, P_{1,k_1}, \dots, P_{m,1}, \dots, P_{m,k_m} \in \mathbb{Z}[\eta]$$

$$P_1, \dots, P_l \in \mathbb{Z}[\eta],$$

the following quantity is a polynomial in $\mathbb{Z}[\eta]$:

$$\sup_{\rho} \left( \llbracket u \rrbracket_{\mathbb{M}}^{\eta, \rho}_{N \mapsto P(\eta)} \left( \begin{array}{c} f_1(P_{1,1}(\eta), \dots, P_{1,k_1}), \\ \vdots, f_m(P_{m,1}(\eta), \dots, P_{m,k_m}(\eta)), \\ P_1(\eta), \dots, P_l(\eta) \end{array} \right) \right)$$

b) Definition of $\varepsilon/\text{poly}$ :: Let $n$ be a variable of type bint.

We say that a global formula $F$ is poly-secure compatible w.r.t. $n$ and a model $\mathbb{M}$ when all the advantages, time and length terms appearing in its predicates are polynomial or negligible (according to their type) w.r.t $n$ and $\mathbb{M}$.

Similarly, a judgement is poly-secure compatible (w.r.t. $n$ and $\mathbb{M}$) if its conclusion is poly-secure compatible. If we consider a local or a time judgement, we also require that the advantage or time term labeling the judgement are poly-secure compatible.

Let $\varepsilon_x$ be variable of a type compatible with $\vec{u}; \vec{v}$, in the sense that $\vec{u} \sim_{x_\varepsilon} \vec{v}$ is a well-typed predicate. We say that a proof $\Pi$ which is $(\vec{u}; \vec{v})$-admissible proof is $\varepsilon$-linear with polynomial overhead w.r.t. $x_\varepsilon$, $n$ and $\mathbb{M}$, which we write $\varepsilon/\text{poly}_{\mathbb{M}}^{x_\varepsilon, n}$, if all its auxiliary judgements are poly-secure compatible w.r.t. $n$ and $\mathbb{M}$, and if the advantage at the conclusion of $\Pi$ is of the form:

$$\lambda t, \vec{o}. \varepsilon_0 + \sum_i x_\varepsilon (t + t_i) (\vec{o} + \vec{o}_i)$$

where $t$ and $\vec{o}$ do not occur in $t_i$ and $\vec{o}_i$ (for any $i$), and where $x_\varepsilon$ does not occur in $\varepsilon_0$. The crucial point, here, is that the time over-heads $t_i$ and the oracle calls overheads $\vec{o}_i$ do not depend on the execution time of the adversary, tough they can of course depends on the protocol. Without this, it would not

be possible to bound the time in the full inductive proof by a polynomial.

**Remark 3.** If $\Pi$ is $\varepsilon/\text{poly}_{\mathbb{M}}^{x_\varepsilon, n}$, then any transformation of $\Pi$ by the transformation relations $\bullet_{\text{AD}}$ and $\bullet_{\text{col}}$ is also $\varepsilon/\text{poly}_{\mathbb{M}}^{x_\varepsilon, n}$. This can be checked by a simple case analysis of all proof transformations.

**Proposition 1.** Let $\Pi$ be a $(\vec{u}; \vec{v})$-admissible proof that only use G. AXIOM as its leafs in it trunk and only on one particular conclusion $u \sim_{x_\varepsilon} v$, where $x_\varepsilon$ is a variable.

The advantage of its conclusion $\varepsilon_{\text{final}}$ is of the form:

$$\varepsilon_{\text{final}} = \lambda t, \vec{o}. \varepsilon_0 + \sum_{i=1}^{k} (x_\varepsilon (t + t_i) (\vec{o} + \vec{o}_i))$$

where $k$ is the number of G. AXIOM in the trunk of $\Pi$.

Furthermore, if $\mathbb{M}$ is such that $\Pi$ is $\varepsilon/\text{poly}_{\mathbb{M}}^{x_\varepsilon, n}$ (for some $n$), then:

$$\forall i, \text{poly}_{\mathbb{M}}^n(t_i) \wedge \text{poly}_{\mathbb{M}}^n(\vec{o}_i)$$

where a vector is polynomial if each of its component is.

Finally, if $\mathbb{M}$ is a model such that $\text{negl}_{\mathbb{M}}^n(\varepsilon_{\text{CCA1}})$ and $\text{negl}_{\mathbb{M}}^n(\varepsilon_{\text{PRF}})$ holds, then $\text{negl}_{\mathbb{M}}^n(\varepsilon_0)$ holds as well.

This can be proven by induction on the inductive definition of admissible proof, by case analysis over all possible rules involved

## F. Obtaining a Polynomial Level of Security

We now recall and prove Lemma 3.

**Lemma 3.** Let $\Pi$ be an $(u n; v n)$-admissible proof proving the inductive premise of the rule above where: the only occurrence of G. AXIOM in the trunk is on the induction hypothesis $u n \sim_{\varepsilon n} v n$; and where the induction hypothesis and $x_\varepsilon$ are only used in the trunk.

Then there exists $\Pi_{\text{poly}}$ proving the inductive case of $\mathbb{N}$-IND with an improved upper-bound $\varepsilon_{\text{ih}}^{\text{negl}}$, i.e. $\Pi_{\text{poly}}$ proves:

$$E' ; \Theta, u n \sim_{x_\varepsilon} v n \vdash u n, u' (n+1) \sim_{\varepsilon_{\text{ih}}^{\text{negl}}} v n, v' (n+1)$$

where $\varepsilon_{\text{ih}}^{\text{negl}}$ is such that the final advantage $\varepsilon^{\text{negl}}$, defined from $\varepsilon_{\text{ih}}^{\text{negl}}$ as described in Eq. (7), is such that for any $\mathbb{M}$ where:

• $\Pi$ is in $\varepsilon/\text{poly}_{\mathbb{M}}^{x_\varepsilon, n}$, i.e. (roughly) the advantage terms (resp. time and length terms) appearing in all auxiliary sub-proofs of $\Pi$ are negligible (resp. polynomial) in $\mathbb{M}$, for any number of session $n$ and adversarial time $t$ which are polynomial in $\eta$. See Appendix C-E for a formal definition of $\varepsilon/\text{poly}_{\mathbb{M}}^{x_\varepsilon, n}$.

• The initial advantage bound $\varepsilon_0$ and the cryptographic advantages $\varepsilon_{\text{CCA1}}$ and $\varepsilon_{\text{PRF}}$ must be negligible for adversaries running in time polynomial in $\eta$.

Then the term $\varepsilon^{\text{negl}}$ is a negligible term w.r.t. $n$ and $\mathbb{M}$, i.e. for any polynomials $P_n, P_t \in \mathbb{N}[\eta]$ bounding, resp., the number of sessions and the execution time of the adversary:

$$E_{\rho}(\llbracket \varepsilon^{\text{negl}} n \rrbracket_{\mathbb{M}}^{\eta; \rho} (P_t(\eta)) \in \text{negl}(\eta))$$
*Proof sketch.* Since Π is a (u n; v n)-admissible proof, we can rewrite it into another (u n; v n)-admissible proof that use the induction hypothesis only once in it trunk (we apply the transformation ▶<sub>AD</sub> until we have a normal form then we apply ▶<sub>col</sub> on the only (u n, v n)-collapse proof at the top of the tree (there is only one since all the descending rules have only one principal premise)).

Therefore, we now have a proof Π' such that:

• Π' is a (u n; v n)-admissible proof

• Π' is a $\varepsilon/\text{poly}_{\mathbb{M}}^{\chi_{\varepsilon},n}$ (since it a transformation of a
  $\varepsilon/\text{poly}_{\mathbb{M}}^{\chi_{\varepsilon},n}$ proof)

• G. AXIOM is the only leaf in the trunk of Π' and it only appear once.

By Proposition 1, we get that the upper-bound derived by Π' is of the form λt$\vec{o}$.x$_{ε}$ (t + t$_{n}$)($\vec{o}$ + $\vec{o}$$_{n}$) + ε$_{n}$.

Finally, we take $\varepsilon_{\text{poly}}$ to be

$$
\lambda n. \text{ if } n = 0 \text{ then } \varepsilon = 0 \text{ else } \lambda t \vec{o} . \varepsilon_{\text{poly}} (t + t_n) (\vec{o} + \vec{o}_n) + \varepsilon_n
$$

which is well-defined since all the terms in it are well-defined
in Π' and it is well-founded. And it is negligable w.r.t n and
M since Π' is ε/poly<sup>x<sub>ε</sub>,n</sup>.

Therefore, we take the proof Π<sub>poly</sub> to be Π' and ε by ε<sub>poly</sub>
to conclude the proof.
□

<figure><img src="image_1.png" /></figure>
*Proof sketch.* Since Π is a (u n; v n)-admissible proof, we can rewrite it into another (u n; v n)-admissible proof that use the induction hypothesis only once in it trunk (we apply the transformation ▶<sub>AD</sub> until we have a normal form then we apply ▶<sub>col</sub> on the only (u n, v n)-collapse proof at the top of the tree (there is only one since all the descending rules have only one principal premise)).

Therefore, we now have a proof Π' such that:

• Π' is a (u n; v n)-admissible proof

• Π' is a $\varepsilon/\text{poly}_{\mathbb{M}}^{\chi_{\varepsilon},n}$ (since it a transformation of a
  $\varepsilon/\text{poly}_{\mathbb{M}}^{\chi_{\varepsilon},n}$ proof)

• G. AXIOM is the only leaf in the trunk of Π' and it only appear once.

By Proposition 1, we get that the upper-bound derived by Π' is of the form $\lambda t \vec{o} . x_\varepsilon (t + t_n)(\vec{o} + \vec{o}_n) + \varepsilon_n$.

Finally, we take $\varepsilon_{\text{poly}}$ to be

$$
\lambda n. \text{ if } n = 0 \text{ then } \varepsilon = 0 \text{ else } \lambda t \vec{o} . \varepsilon_{\text{poly}} (t + t_n) (\vec{o} + \vec{o}_n) + \varepsilon_n
$$

which is well-defined since all the terms in it are well-defined
in Π' and it is well-founded. And it is negligable w.r.t n and
M since Π' is ε/poly<sup>x<sub>ε</sub>,n</sup>.

Therefore, we take the proof Π<sub>poly</sub> to be Π' and ε by ε<sub>poly</sub>
to conclude the proof.
□

<figure><img src="image_2.png" /></figure>
**Global judgements: left rules.**

$$ \frac{\begin{array}{c} \text{G.L-} \tilde{\vee} \\ \text{E; } \Theta, F_0 \{x \mapsto t\} \vdash F_1 \end{array}}{\begin{array}{c} \text{E; } \Theta, \tilde{\vee}(x : \tau) \cdot F_0 \vdash F_1 \end{array}} \text{E} \vdash t : \tau $$

$$ \frac{\begin{array}{c} \text{G.L-} \tilde{\Xi} \\ \text{E; } x : \tau; \Theta, F_0 \vdash F_1 \end{array}}{\begin{array}{c} \text{E; } \Theta, \tilde{\Xi}(x : \tau) \cdot F_0 \vdash F_1 \end{array}} $$

$$ \frac{\begin{array}{c} \text{G.L-} \dashv \\ \text{E; } \Theta \vdash F_0 \end{array}}{\begin{array}{c} \text{E; } \Theta, F_0 \Rightarrow F_1 \end{array}} \text{E; } \Theta, F_1 \vdash F $$

$$ \frac{\begin{array}{c} \text{G.L-} \bar{\Lambda} \\ \text{E; } \Theta, F_0, F_1 \vdash F \end{array}}{\begin{array}{c} \text{E; } \Theta, F_0 \bar{\Lambda} F_1 \vdash F \end{array}} $$

$$ \frac{\begin{array}{c} \text{G.L-} \tilde{\bar{\nu}} \\ \text{E; } \Theta, F_0 \vdash F \end{array}}{\begin{array}{c} \text{E; } \Theta, F_0 \tilde{\nu} F_1 \vdash F \end{array}} $$

$$ \frac{\begin{array}{c} \text{G.L-} \bar{\perp} \\ \text{E; } \Theta, \bar{\perp} \vdash F \end{array}}{\text{E; } \Theta, \bar{\perp} \vdash F} $$

**Global judgements: right rules.**

$$ \frac{\begin{array}{c} \text{G.R-} \tilde{\vee} \\ \text{E; } x : \tau; \Theta \vdash F \end{array}}{\begin{array}{c} \text{E; } \Theta \vdash \tilde{\vee}(x : \tau) \cdot F \end{array}} $$

$$ \frac{\begin{array}{c} \text{G.R-} \tilde{\Xi} \\ \text{E; } \Theta \vdash F \{x \mapsto u\} \end{array}}{\begin{array}{c} \text{E; } \Theta \vdash \tilde{\Xi}(x : \tau) \cdot F \end{array}} $$

$$ \frac{\begin{array}{c} \text{G.R-} \dashv \\ \text{E; } \Theta \vdash F_0 \vdash F_1 \end{array}}{\begin{array}{c} \text{E; } \Theta \vdash F_0 \Rightarrow F_1 \end{array}} $$

$$ \frac{\begin{array}{c} \text{G.R-} \bar{\Lambda} \\ \text{E; } \Theta \vdash F_0 \end{array}}{\begin{array}{c} \text{E; } \Theta \vdash F_0 \bar{\Lambda} F_1 \end{array}} $$

$$ \frac{\begin{array}{c} \text{G.R}_0-\tilde{\vee} \\ \text{E; } \Theta \vdash F_0 \end{array}}{\begin{array}{c} \text{E; } \Theta \vdash F_0 \tilde{\vee} F_1 \end{array}} $$

$$ \frac{\begin{array}{c} \text{G.R}_1-\tilde{\vee} \\ \text{E; } \Theta \vdash F_1 \end{array}}{\begin{array}{c} \text{E; } \Theta \vdash F_0 \tilde{\vee} F_1 \end{array}} $$

$$ \frac{\begin{array}{c} \text{G.R-} \bar{\perp} \\ \text{E; } \Theta \vdash \bar{\perp} \end{array}}{\text{E; } \Theta \vdash \bar{\perp}} $$

**Global judgement: other rules.**

$$ \frac{\begin{array}{c} \text{G.AXIOM} \\ \text{E; } \Theta, F \vdash F \end{array}}{\text{E; } \Theta, F \vdash F} $$

$$ \frac{\begin{array}{c} \text{G.A} \text{.} \text{\textit{ABSURD}} \\ \text{E; } \Theta, F \Rightarrow \bar{\perp} \vdash \bar{\perp} \end{array}}{\text{E; } \Theta \vdash F} $$

$$ \frac{\begin{array}{c} \text{G.CUT} \\ \text{E; } \Theta \vdash F_1 \end{array}}{\text{E; } \Theta \vdash F_0} \text{E; } \Theta, F_1 \vdash F_0 $$

$$ \frac{\begin{array}{c} \text{G.WEAK} \\ \text{E; } \Theta_0 \vdash F \end{array}}{\text{E; } \Theta_0, \Theta_1 \vdash F} $$

$$ \frac{\begin{array}{c} \text{G.DUP} \\ \text{E; } \Theta, F_0, F_0 \vdash F_1 \end{array}}{\text{E; } \Theta, F_0 \vdash F_1} $$

**Global judgement: local and global relations.**

$$ \frac{\begin{array}{c} \text{G}_\epsilon \cdot \text{L-LOC} \Rightarrow \\ \text{E; } \Theta, [\phi]_0 \Rightarrow [\psi]_\epsilon \vdash F \\ \text{E; } \Theta \vdash \text{const}(\phi) \end{array}}{\begin{array}{c} \text{E; } \Theta, [\phi \Rightarrow \psi]_\epsilon \vdash F \end{array}} $$

$$ \frac{\begin{array}{c} \text{G}_\epsilon \cdot \text{L-LOC} \vee \\ \text{E; } \Theta, [\phi]_\epsilon \vdash F \\ \text{E; } \Theta, [\psi]_\epsilon \vdash F \\ \text{E; } \Theta \vdash \text{const}(\phi) \tilde{\vee} \text{ const}(\psi) \end{array}}{\begin{array}{c} \text{E; } \Theta, [\phi \vee \psi]_\epsilon \vdash F \end{array}} $$

$$ \frac{\begin{array}{c} \text{G}_\epsilon \cdot \text{L-} \tilde{\vee} \cdot \forall \\ \text{E; } \Theta, \tilde{\vee}(x : \tau) \cdot [\psi]_\epsilon \vdash F \\ \text{E; } \Theta, [\forall(x : \tau) \cdot \psi]_\epsilon \vdash F \end{array}}{\text{E; } \Theta, [\forall(x : \tau) \cdot \psi]_\epsilon \vdash F} $$

$$ \frac{\begin{array}{c} \text{G}_\epsilon \cdot \text{L-} \forall \cdot \tilde{\vee} \\ \text{E; } \Theta, [\forall(x : \tau) \cdot \psi]_\epsilon \vdash F \\ \text{E; } \Theta, \tilde{\vee}(x : \tau) \cdot [\psi]_\epsilon \vdash F \end{array}}{\text{E; } \Theta, \tilde{\vee}(x : \tau) \cdot [\psi]_\epsilon \vdash F} $$

$$ \frac{\begin{array}{c} \text{G}_\epsilon \cdot \text{L-LOC} \vee \\ \text{E; } \Theta, [\psi\{x \mapsto u\}]_\epsilon \vdash F \end{array}}{\begin{array}{c} \text{E; } \Theta, [\forall(x : \tau) \cdot \psi]_\epsilon \vdash F \end{array}} $$

$$ \frac{\begin{array}{c} \text{G}_\epsilon \cdot \text{L-LOC} \wedge \\ \text{E; } \Theta, [\psi]_\epsilon, [\phi]_\epsilon \vdash F \end{array}}{\begin{array}{c} \text{E; } \Theta, [\psi \wedge \phi]_\epsilon \vdash F \end{array}} $$

$$ \frac{\begin{array}{c} \text{G}_\epsilon \cdot \text{L-LOC} \perp \\ \text{E; } \Theta, [\perp]_0 \vdash F \end{array}}{\text{E; } \Theta, [\perp]_0 \vdash F} $$

**Global judgement: $\epsilon$ weakening rules.**

Weakening rules for other predicates of the logic are similar. We omit them here.

$$ \frac{\begin{array}{c} \text{G}_\epsilon \cdot \text{REACH} \cdot \epsilon \cdot \text{WEAK}_0 \\ \text{E; } \Theta \vdash [\psi]_\epsilon \end{array}}{\begin{array}{c} \text{E; } \Theta \vdash [\epsilon \le \epsilon']_0 \\ \text{E; } \Theta \vdash [\psi]_\epsilon' \end{array}} $$

$$ \frac{\begin{array}{c} \text{G}_\epsilon \cdot \text{REACH} \cdot \epsilon \cdot \text{WEAK} \\ \text{E; } \Theta \vdash [\psi]_{\epsilon+\epsilon_0} \end{array}}{\begin{array}{c} \text{E; } \Theta \vdash [\epsilon_0 \le \epsilon'_0]_{\epsilon_1} \\ \text{E; } \Theta \vdash [\psi]_{\epsilon+\epsilon'_0+\epsilon_1} \end{array}} $$

$$ \frac{\begin{array}{c} \text{G}_\epsilon \cdot \text{E} \cdot \epsilon \cdot \text{WEAK}_0 \\ \text{E; } \Theta \vdash \tilde{u} \sim_\epsilon \tilde{v} \end{array}}{\begin{array}{c} \text{E; } \Theta \vdash [\epsilon \le \epsilon']_0 \\ \text{E; } \Theta \vdash \tilde{u} \sim_{\epsilon'} \tilde{v} \end{array}} $$

$$ \frac{\begin{array}{c} \text{G}_\epsilon \cdot \text{E} \cdot \epsilon \cdot \text{WEAK} \\ \text{E; } \Theta \vdash \tilde{u} \sim_{\epsilon+\epsilon_0} \tilde{v} \end{array}}{\begin{array}{c} \text{E; } \Theta \vdash [\epsilon_0 \le \epsilon'_0]_{\epsilon_1} \\ \text{E; } \Theta \vdash [\epsilon_0 \le 1]_0 \\ \text{E; } \Theta \vdash \tilde{u} \sim_{\epsilon+\epsilon'_0+\epsilon_1} \tilde{v} \end{array}} $$

**Global judgement: rewrite rules.**

Rewriting rules for other predicates of the logic are similar. We omit them here.

$$ \frac{\begin{array}{c} \text{G}_\epsilon \cdot \text{E} \cdot \text{REWRITE}_0 \\ \text{E; } \Theta \vdash \tilde{u}\{s\} \sim_{\epsilon\{s\}} \tilde{v}\{s\} \end{array}}{\begin{array}{c} \text{E; } \Theta \vdash [s = r]_0 \\ \text{E; } \Theta \vdash \tilde{u}\{r\} \sim_{\epsilon\{r\}} \tilde{v}\{r\} \end{array}} $$

$$ \frac{\begin{array}{c} \text{G}_\epsilon \cdot \text{E} \cdot \text{REWRITE} \\ \text{E; } \Theta \vdash \tilde{u}\{s\} \sim_{\epsilon_1\{s\}+\epsilon_0} \tilde{v}\{s\} \\ \text{if } \{s\} \in \text{fv}(\epsilon_1) \text{ then } \text{E; } \Theta \vdash [\epsilon_1\{s\} \le 1]_0 \\ i \stackrel{\text{def}}{=} (\mathbb{1}\{s \in \text{fv}(\tilde{u})\} + \mathbb{1}\{s \in \text{fv}(\tilde{v})\} + \mathbb{1}\{s \in \text{fv}(\epsilon_1)\}) \\ \text{E; } \Theta \vdash \tilde{u}\{r\} \sim_{\epsilon_1\{r\}+\epsilon_0+i \cdot \epsilon_2} \tilde{v}\{r\} \end{array}}{\text{E; } \Theta \vdash \tilde{u}\{r\} \sim_{\epsilon_1\{r\}+\epsilon_0+i \cdot \epsilon_2} \tilde{v}\{r\}} $$

$$ \frac{\begin{array}{c} \text{G}_\epsilon \cdot \text{REACH} \cdot \text{REWRITE}_0 \\ \text{E; } \Theta \vdash [\psi\{s\}]_{\epsilon\{s\}} \end{array}}{\begin{array}{c} \text{E; } \Theta \vdash [s = r]_0 \\ \text{E; } \Theta \vdash [\psi\{r\}]_{\epsilon\{r\}} \end{array}} $$

$$ \frac{\begin{array}{c} \text{G}_\epsilon \cdot \text{REACH} \cdot \text{REWRITE} \\ \text{E; } \Theta \vdash [\psi\{s\}]_{\epsilon_1\{s\}+\epsilon_0} \\ \text{if } \{s\} \in \text{fv}(\epsilon_1) \text{ then } \text{E; } \Theta \vdash [\epsilon_1\{s\} \le 1]_0 \\ i \stackrel{\text{def}}{=} (\mathbb{1}\{s \in \text{fv}(\psi)\} + \mathbb{1}\{s \in \text{fv}(\epsilon_1)\}) \\ \text{E; } \Theta \vdash [\psi\{r\}]_{\epsilon_1\{r\}+\epsilon_0+i \cdot \epsilon_2} \end{array}}{\text{E; } \Theta \vdash [\psi\{r\}]_{\epsilon_1\{r\}+\epsilon_0+i \cdot \epsilon_2} \end{array}} $$

$$ \frac{\begin{array}{c} \text{G}_\epsilon \cdot \text{BLEN} \cdot \text{REWRITE}_0 \\ \text{E; } \Theta \vdash \text{blen}_{l(s)}(\tilde{u}\{s\}) \end{array}}{\begin{array}{c} \text{E; } \Theta \vdash [s = r]_0 \\ \text{E; } \Theta \vdash \text{blen}_{l(s)}(\tilde{u}\{r\}) \end{array}} $$

<caption>Figure 10. Global judgement rules.</caption>
**Global judgements: left rules.**

<figure><img src="image_3.png" /></figure>

**Global judgements: right rules.**

<figure><img src="image_4.png" /></figure>

**Global judgement: other rules.**

<figure><img src="image_5.png" /></figure>

**Global judgement: local and global relations.**

<figure><img src="image_6.png" /></figure>

**Global judgement: $\varepsilon$ weakening rules.**

Weakening rules for other predicates of the logic are similar. We omit them here.

<figure><img src="image_7.png" /></figure>

**Global judgement: rewrite rules.**

Rewriting rules for other predicates of the logic are similar. We omit them here.

<figure><img src="image_8.png" /><figcaption>Figure 10. Global judgement rules.</figcaption></figure>
## Equivalence relation rules.

$$ \begin{array}{c} \text{G}_\varepsilon \cdot \text{E} \cdot \text{REFL} \\ \overline{\text{E}; \Theta \vdash \tilde{u} \sim_0 \tilde{u}} \end{array} $$

$$ \begin{array}{c} \text{G}_\varepsilon \cdot \text{E} \cdot \text{SYM} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_l \sim_\varepsilon \tilde{u}_r} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_r \sim_\varepsilon \tilde{u}_l} \end{array} $$

$$ \begin{array}{c} \text{G}_\varepsilon \cdot \text{E} \cdot \text{TRANS} \\ \overline{\text{E}; \Theta \vdash \tilde{u} \sim_{\varepsilon_0} \tilde{w}} \\ \overline{\text{E}; \Theta \vdash \tilde{u} \sim_{\varepsilon_1} \tilde{v}} \\ \overline{\text{E}; \Theta \vdash \tilde{u} \sim_{\varepsilon_0 + \varepsilon_1} \tilde{v}} \end{array} $$

## Structural rules included in the G<sub>ε</sub>.E:BI-DEDUCE rule.

In all the rules below, $v, v_l, v_r$ are order-0 terms and $f, f_l, f_r$ are order-1 terms.

In G<sub>ε</sub>.E:FA-NAMES, $n_f$ only occurs in its declaration in E, and $t_n$ is an upper-bound on the time needed by $n_f$ for a single sampling.

$$ \begin{array}{c} \text{G}_\varepsilon \cdot \text{E} \cdot \text{FA-BASE} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_l \sim_\varepsilon \tilde{u}_r} \\ \overline{\text{E}; \Theta \vdash \text{adv}_{t_v}(v)} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_l, v \sim_{\varepsilon'} \tilde{u}_r, v} \end{array} $$

where $\varepsilon' \stackrel{\text{def}}{=} \lambda t, \bar{o}. \varepsilon (t + t_v) \bar{o}$

$$ \begin{array}{c} \text{G}_\varepsilon \cdot \text{E} \cdot \text{FA-FUN} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_l \sim_\varepsilon \tilde{u}_r} \\ \overline{\text{E}; \Theta \vdash \text{adv}_{t_f}(f)} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_l, f \sim_{\varepsilon'} \tilde{u}_r, f} \end{array} $$

where $\varepsilon' \stackrel{\text{def}}{=} \lambda t, \bar{o}, o_f. \varepsilon (t + o_f \cdot (t + t_f(t))) \bar{o}$

$$ \begin{array}{c} \text{G}_\varepsilon \cdot \text{E} \cdot \text{FA-APP} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_l, f_l, v_l \sim_\varepsilon \tilde{u}_r, f_r, v_r} \\ \overline{\text{E}; \Theta \vdash \text{blen}_l(v_l) \wedge \text{blen}_l(v_r)} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_l, (f_l v_l) \sim_{\varepsilon'} \tilde{u}_r, (f_r v_r)} \end{array} $$

where $\varepsilon' \stackrel{\text{def}}{=} \lambda t, \bar{o}. \varepsilon (t + l + 1) \bar{o}$

$$ \begin{array}{c} \text{G}_\varepsilon \cdot \text{E} \cdot \text{FA-NAMES} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_l \sim_\varepsilon \tilde{u}_r} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_l, n_f \sim_{\varepsilon'} \tilde{u}_r, n_f} \end{array} $$

where $\varepsilon' \stackrel{\text{def}}{=} \lambda t, \bar{o}, o_n. \varepsilon (t + o_n \cdot t_n) \bar{o}$

$$ \begin{array}{c} \text{G}_\varepsilon \cdot \text{E} \cdot \text{DUP-BASE} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_l, v_l \sim_\varepsilon \tilde{u}_r, v_r} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_l, v_l, v_l \sim_\varepsilon \tilde{u}_r, v_r, v_r} \end{array} $$

$$ \begin{array}{c} \text{G}_\varepsilon \cdot \text{E} \cdot \text{DUP-FUN} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_l, f_l \sim_\varepsilon \tilde{u}_r, f_r} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_l, f_l, f_l \sim_{\varepsilon'} \tilde{u}_r, f_r, f_r} \end{array} $$

where $\varepsilon' \stackrel{\text{def}}{=} \lambda t, \bar{o}, o_1, o_2. \varepsilon t \bar{o} (o_1 + o_2)$

$$ \begin{array}{c} \text{G}_\varepsilon \cdot \text{E} \cdot \text{WEAK} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_l, v_l \sim_\varepsilon \tilde{u}_r, v_r} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_l \sim_\varepsilon \tilde{u}_r} \end{array} $$

$$ \begin{array}{c} \text{G}_\varepsilon \cdot \text{E} \cdot \text{PERM} \\ \overline{\text{E}; \Theta \vdash u_l^{\pi(1)}, \dots, u_l^{\pi(n)} \sim_{\pi(\varepsilon)} u_r^{\pi(1)}, \dots, u_r^{\pi(n)}} \\ \overline{\text{E}; \Theta \vdash u_l^1, \dots, u_l^n \sim_\varepsilon u_r^1, \dots, u_r^n} \end{array} $$

where $\pi$ is a permutation of $\{1, \dots, n\}$ and $\pi(\varepsilon)$ is defined in Appendix B-A

## Reduction rules.

$$ \begin{array}{c} \text{G.}\beta \\ \overline{\text{E}; \Theta \vdash [(\lambda(x : \tau).t) t_1 = t\{x \mapsto t_1\}]_0} \end{array} $$

$$ \begin{array}{c} \text{G.}\delta \\ \overline{\text{E}, x : \tau = t; \Theta \vdash [x = t]_0} \end{array} $$

$$ \begin{array}{c} \text{G.} \text{LET} \\ \overline{\text{E}; \Theta \vdash [\text{let } (x : v) = u \text{ in } = u\{x \mapsto v\}]_0} \end{array} $$

## Induction rules.

$$ \begin{array}{c} \text{L}_\varepsilon \cdot \text{INDUCTION} \\ \overline{\text{E}; \Theta \vdash \text{well-founded}_\tau(<)} \\ \overline{\text{E}; \Theta \vdash \Gamma \vdash_\varepsilon \forall (x : \tau). (\forall (x_1 : \tau). x_1 < x \Rightarrow \psi\{x \mapsto x_1\}) \Rightarrow \psi} \\ \overline{\text{E}; \Theta \vdash \Gamma \vdash_\varepsilon \forall (x : \tau). \psi} \end{array} $$

$$ \begin{array}{c} \text{G}_\varepsilon \cdot \text{INDUCTION} \\ \overline{\text{E}; \Theta \vdash \text{well-founded}_\tau(<)} \\ \overline{\text{E}; \Theta \vdash \tilde{\forall}(x : \tau). (\tilde{\forall}(x_1 : \tau). [x_1 < x]_0 \Rightarrow F\{x \mapsto x_1\}) \Rightarrow F} \\ \overline{\text{E}; \Theta \vdash \tilde{\forall}(x : \tau). F} \end{array} $$

## Case-study and bi-deduction rules.

See Appendix B-B for a description of G<sub>ε</sub>.E:BI-DEDUCE side-conditions, as well as the advantage bound $\varepsilon'$.

$$ \begin{array}{c} \text{G}_\varepsilon \cdot \text{E} \cdot \text{CS} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_l, b_l, v_l \sim_{\varepsilon_1} \tilde{u}_r, b_r, \tilde{v}_r} \\ \overline{\text{E}; \Theta \vdash \tilde{u}_l, \text{if } b_l \text{ then } \tilde{v}_l \text{ else } \tilde{w}_l \sim_{\varepsilon_1 + \varepsilon_2 + 1} \tilde{u}_r, \text{if } b_r \text{ then } \tilde{v}_r \text{ else } \tilde{w}_r} \end{array} $$

$$ \begin{array}{c} \text{G}_\varepsilon \cdot \text{E} \cdot \text{BI-DEDUCE} \\ \overline{\text{E}; \Theta \vdash \tilde{\Lambda}_{i \le n} \text{adv}_{t_i, \bar{o}_i}(C_i)} \\ \overline{\text{E}; \Theta \vdash \text{blen}_{l^w}(\tilde{w}_0) \wedge \text{blen}_{l^w}(\tilde{w}_1)} \\ \overline{\text{E}; \Theta \vdash \text{blen}_l(\tilde{u}) \wedge \text{blen}_l(\tilde{v})} \\ \overline{\text{E}; \Theta \vdash \text{blen}_{l^n}(\tilde{n})} \\ \overline{\text{E}; \Theta \vdash \tilde{w}_0, (C_1, \dots, C_n) \tilde{w}_0 \tilde{u} \tilde{n} \sim_{\varepsilon'} \tilde{w}_1, (C_1, \dots, C_n) \tilde{w}_1 \tilde{v} \tilde{n}} \end{array} $$

<caption>Figure 11. Remaning of the rules rules.</caption>
Equivalence relation rules.

$$
\begin{array}{r@{\quad}l}
\text{G}_\epsilon \cdot \text{E} \cdot \text{REFL} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u} \sim_0 \tilde{u}} &
\end{array}
$$

$$
\begin{array}{r@{\quad}l}
\text{G}_\epsilon \cdot \text{E} \cdot \text{SYM} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l \sim_\epsilon \tilde{u}_r} &
\end{array}
$$

$$
\begin{array}{r@{\quad}l}
\text{G}_\epsilon \cdot \text{E} \cdot \text{TRANS} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u} \sim_{\epsilon_0} \tilde{w}} & \mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{w} \sim_{\epsilon_1} \tilde{v}} \\
\multicolumn{2}{c}{\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u} \sim_{\epsilon_0 + \epsilon_1} \tilde{v}}} \\
\end{array}
$$

Structural rules included in the G<sub>ε</sub>·E:BI-DEDUCE rule.

In all the rules below, $v, v_l, v_r$ are order-0 terms and $f, f_l, f_r$ are order-1 terms.

In G<sub>ε</sub>·E:FA-NAMES, n<sub>f</sub> only occurs in its declaration in E, and t<sub>n</sub> is an upper-bound on the time needed by n<sub>f</sub> for a single sampling.

$$
\begin{array}{r@{\quad}l}
\text{G}_\epsilon \cdot \text{E} \cdot \text{FA-BASE} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l \sim_\epsilon \tilde{u}_r} & \mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \text{adv}_{t_v}(v)} \\
\multicolumn{2}{c}{\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l, v \sim_{\epsilon'} \tilde{u}_r, v}}
\end{array}
$$

$$
\text{where } \epsilon' \stackrel{\text{def}}{=} \lambda t, \bar{o}. \epsilon (t + t_v) \bar{o}
$$

$$
\begin{array}{r@{\quad}l}
\text{G}_\epsilon \cdot \text{E} \cdot \text{FA-FUN} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l \sim_\epsilon \tilde{u}_r} & \mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \text{adv}_{t_f}(f)} \\
\multicolumn{2}{c}{\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l, f \sim_{\epsilon'} \tilde{u}_r, f}}
\end{array}
$$

$$
\text{where } \epsilon' \stackrel{\text{def}}{=} \lambda t, \bar{o}, o_f. \epsilon (t + o_f \cdot (t + t_f(t))) \bar{o}
$$

$$
\begin{array}{r@{\quad}l}
\text{G}_\epsilon \cdot \text{E} \cdot \text{FA-APP} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l, f_l, v_l \sim_\epsilon \tilde{u}_r, f_r, v_r} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \text{blen}_l(v_l) \land \text{blen}_l(v_r)} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l, (f_l v_l) \sim_{\epsilon'} \tilde{u}_r, (f_r v_r)} &
\end{array}
$$

$$
\text{where } \epsilon' \stackrel{\text{def}}{=} \lambda t, \bar{o}, \epsilon (t + l + 1) \bar{o} 1
$$

$$
\begin{array}{r@{\quad}l}
\text{G}_\epsilon \cdot \text{E} \cdot \text{FA-NAMES} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l \sim_\epsilon \tilde{u}_r} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l, n_f \sim_{\epsilon'} \tilde{u}_r, n_f} &
\end{array}
$$

$$
\text{where } \epsilon' \stackrel{\text{def}}{=} \lambda t, \bar{o}, o_n. \epsilon (t + o_n \cdot t_n) \bar{o}
$$

$$
\begin{array}{r@{\quad}l}
\text{G}_\epsilon \cdot \text{E} \cdot \text{DUP-BASE} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l, v_l \sim_\epsilon \tilde{u}_r, v_r} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l, v_l, v_l \sim_\epsilon \tilde{u}_r, v_r, v_r} &
\end{array}
$$

$$
\begin{array}{r@{\quad}l}
\text{G}_\epsilon \cdot \text{E} \cdot \text{DUP-FUN} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l, f_l \sim_\epsilon \tilde{u}_r, f_r} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l, f_l, f_l \sim_{\epsilon'} \tilde{u}_r, f_r, f_r} &
\end{array}
$$

$$
\text{where } \epsilon' \stackrel{\text{def}}{=} \lambda t, \bar{o}, o_1, o_2. \epsilon \ t \ \bar{o} \ (o_1 + o_2)
$$

$$
\begin{array}{r@{\quad}l}
\text{G}_\epsilon \cdot \text{E} \cdot \text{WEAK} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l, v_l \sim_\epsilon \tilde{u}_r, v_r} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l \sim_\epsilon \tilde{u}_r} &
\end{array}
$$

$$
\begin{array}{r@{\quad}l}
\text{G}_\epsilon \cdot \text{E} \cdot \text{PERM} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash u_l^{\pi(1)}, \dots, u_l^{\pi(n)} \sim_{\pi(\epsilon)} u_r^{\pi(1)}, \dots, u_r^{\pi(n)}} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash u_l^1, \dots, u_l^n \sim_\epsilon u_r^1, \dots, u_r^n} &
\end{array}
$$

$$
\text{where } \pi \text{ is a permutation of } \{1, \dots, n\} \\
\text{and } \pi(\epsilon) \text{ is defined in Appendix B-A}
$$

Reduction rules.

$$
\text{G.\beta} \qquad \mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash [(\lambda(x : \tau).t) t_1 = t\{x \mapsto t_1\}]_0}
$$

$$
\text{G.\delta} \qquad \mathrl{\mathop{\text{E}}\nolimits; x : \tau = t; \Theta \vdash [x = t]_0}
$$

$$
\text{G. LET} \qquad \mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash [\text{let } (x : v) = u \text{ in } = u\{x \mapsto v\}]_0}
$$

Induction rules.

$$
\begin{array}{r@{\quad}l}
\text{L}_\epsilon \cdot \text{INDUCTION} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \text{well-founded}_\tau(<)} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \Gamma \vdash \forall (x : \tau).(\forall (x_1 : \tau).x_1 < x \Rightarrow \psi\{x \mapsto x_1\}) \Rightarrow \psi} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \Gamma \vdash \epsilon \forall (x : \tau).\psi} &
\end{array}
$$

$$
\begin{array}{r@{\quad}l}
\text{G}_\epsilon \cdot \text{INDUCTION} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \text{well-founded}_\tau(<)} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{\forall}(x : \tau). (\tilde{\forall}(x_1 : \tau). [x_1 < x]_0 \Rightarrow F\{x \mapsto x_1\}) \Rightarrow F} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{\forall}(x : \tau). F} &
\end{array}
$$

Case-study and bi-deduction rules.

See Appendix B-B for a description of G<sub>ε</sub>·E:BI-DEDUCE side-conditions, as well as the advantage bound ε'.

$$
\begin{array}{r@{\quad}l}
\text{G}_\epsilon \cdot \text{E} \cdot \text{CS} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l, b_l, v_l \sim_{\epsilon_1} \tilde{u}_r, b_r, \tilde{v}_r} & \mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l, b_l, w_l \sim_{\epsilon_2} \tilde{u}_r, b_r, \tilde{w}_r} \\
\multicolumn{2}{c}{\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{u}_l, \text{if } b_l \text{ then } \tilde{v}_l \text{ else } \tilde{w}_l \sim_{\epsilon_1 + \epsilon_2 + 1} \tilde{u}_r, \text{if } b_r \text{ then } \tilde{v}_r \text{ else } \tilde{w}_r}}
\end{array}
$$

$$
\begin{array}{r@{\quad}l}
\text{G}_\epsilon \cdot \text{E} \cdot \text{BI-DEDUCE} & \\
\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{\Lambda}_{i \le n} \text{adv}_{t_i, \tilde{o}_i}(C_i)} & \mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \text{blen}_{l^w}(\tilde{w}_0) \land \text{blen}_{l^w}(\tilde{w}_1)} \mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \text{blen}_l(\tilde{u}) \land \text{blen}_l(\tilde{v})} \mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \text{blen}_{l^n}(\tilde{n})} \\
\multicolumn{2}{c}{\mathrl{\mathop{\text{E}}\nolimits; \Theta \vdash \tilde{w}_0, (C_1, \dots, C_n) \tilde{w}_0 \tilde{u} \tilde{n} \sim_{\epsilon'} \tilde{w}_1, (C_1, \dots, C_n) \tilde{w}_1 \tilde{v} \tilde{n}}} \\
\end{array}
$$

<caption>Figure 11. Remaning of the rules rules.</caption>
**Probabilistic independence rules.**

In the $L_\epsilon$.FRESH, $c_n$ is a bound on the probability that the name $n$ selects any precise value. For simplicity we give the rule for one context, but it can easily be extended to vectors of contexts containing the same name.

$$
\begin{align*}
& \mathbf{G}_{\epsilon}.E:FRESH \\
& \quad \mathbf{E}; \Theta \vdash \left[ \phi_{\text{fresh}}^{n,i}(\vec{u}, C(n_{\text{fresh}}())) \right]_{\epsilon_1} \quad \mathbf{E}; \Theta \vdash \vec{u}, C(n_{\text{fresh}}()) \sim \epsilon_0 \vec{v} \\
& \qquad \qquad \qquad \qquad \mathbf{E}; \Theta \vdash \vec{u}, C(n) \sim \epsilon_0 + \epsilon_1 \vec{v} \\
& \mathbf{L}_{\epsilon}.FRESH \\
& \quad \mathbf{E}; \Theta \vdash \Gamma \vdash_{c_n} n \ i = u \Rightarrow \neg \phi_{\text{fresh}}^{n,i}(u, i)
\end{align*}
$$

**Cryptographic rules.**

For simplicity we give the cryptographic rules for one context, but it can easily be extended to vectors of contexts containing the same encryption or hash. If $\vec{u} = u_1, \dots, u_n$ and $\vec{v} = v_1, \dots, v_n$ are two vectors of the same length, then $\vec{u} \cdot \vec{v} \stackrel{\text{def}}{=} \sum_i u_i \cdot v_i$ denotes the scalar product of $\vec{u}$ and $\vec{v}$. Moreover, $\vec{1} \cdot \vec{u} \stackrel{\text{def}}{=} \sum_i u_i$ is the scalar product of $\vec{u}$ with the sequence $1, \dots, 1$ of $n$ copies of $1$ ($\vec{1}$ is implicitly of length $\vec{u}$).

In the $G_\epsilon$.PRF and $G_\epsilon$.CCA 1 rules, $\vec{a} \stackrel{\text{def}}{=} \vec{a}_0, \vec{a}_1$ where $\vec{a}_0$ is of order 0 and $\vec{a}_1$ of order 1 and $\vec{u} \stackrel{\text{def}}{=} \vec{u}_0, \vec{u}_1$ where $\vec{u}_0$ is of order 0 and $\vec{u}_1$ of order 1.

$$
\begin{align*}
& \mathbf{L}_{\epsilon}.\text{EUF} \\
& \quad \mathbf{E}; \Theta; \emptyset \vdash_{\vec{t}}^c s, m, i \qquad \mathbf{E}; \Theta; \Gamma, \neg (\phi_{\text{key}}^{k,i}(s, m, t) \lor \phi_{\text{sign}}^{k,i}(s, m, t)) \vdash_{\epsilon} \psi \qquad \mathbf{E}; \Theta \vdash \det(i) \\
& \qquad \qquad \qquad \qquad \mathbf{E}; \Theta; \Gamma, \text{verify } s \ m \ (\text{pk } (k \ i)) \vdash_{\epsilon + \epsilon_{\text{EUF}}}(\vec{1} \cdot \vec{t}) \psi \\
& \mathbf{G}_{\epsilon}.\text{PRF} \\
& \quad \mathbf{E}; \Theta; \emptyset \vdash_{\vec{t} \vec{u}_1}^c \vec{u}_1 \qquad \mathbf{E}; \Theta; \emptyset \vdash_{\vec{t} \vec{a}_1}^c \vec{a}_1 \qquad \mathbf{E}; \Theta; \emptyset \vdash_{\vec{t}_0}^c \vec{u}_0, \vec{a}_0, b, m, i \\
& \qquad \qquad \qquad \qquad \mathbf{E}; \Theta; \emptyset \vdash_{\vec{t}_C, \vec{a}_C}^c C \qquad \mathbf{E}; \Theta \vdash \det(i) \\
& \quad \mathbf{E}; \Theta \vdash \text{blen}_{\vec{r}}(\vec{a}) \qquad \mathbf{E}; \Theta \vdash \text{blen}_{l_h}(\text{hash } m \ (k \ i)) \land \text{blen}_{l_h}(n_{\text{fresh}}()) \\
& \quad \mathbf{E}; \Theta; \emptyset \vdash_{\epsilon_{\phi}} \psi_{\text{key}}^{k,i}(\vec{w}, C) \land \psi_{\text{msg}}^{k,i}(\vec{w}, C) \qquad \mathbf{E}; \Theta \vdash \vec{u}, \text{ if } b \text{ then } C \ \vec{a} \ (n_{\text{fresh}}()) \text{ else } u_e \sim_{\epsilon} \vec{v} \\
& \qquad \qquad \qquad \qquad \mathbf{E}; \Theta \vdash \vec{u}, \text{ if } b \text{ then } C \ \vec{a} \ (\text{hash } m \ (k \ i)) \text{ else } u_e \sim_{\epsilon_f} \vec{v}
\end{align*}
$$

where $\vec{w} \stackrel{\text{def}}{=} \vec{u}, \vec{a}, b, m, i$ (note that $u_e$ is not in $\vec{w}$) and:

$$
t'_{C} \stackrel{\text{def}}{=} t_{C} \vec{l}_{h} \quad \text{and} \quad \epsilon_{f} \stackrel{\text{def}}{=} \lambda t, \vec{o}. \epsilon t \vec{o} + \epsilon_{\phi} + \epsilon_{\text{PRF}}(t + t'_{C} + \vec{o} \cdot (\vec{t}_{\vec{u}_1} t) + \vec{o}_{C} \cdot (\vec{t}_{\vec{a}_1} t'_{C}) + \vec{1} \cdot \vec{t}_0)
$$

$$
\begin{align*}
& \mathbf{G}_{\epsilon}.\mathbf{CCA}\mathbf{1} \\
& \quad \mathbf{E}; \Theta; \emptyset \vdash_{\vec{t} \vec{u}_1}^c \vec{u}_1 \qquad \mathbf{E}; \Theta; \emptyset \vdash_{\vec{t} \vec{a}_1}^c \vec{a}_1 \qquad \mathbf{E}; \Theta; \emptyset \vdash_{\vec{t}_0}^c \vec{u}_0, \vec{a}_0, b, m, i_r, i_k \\
& \qquad \qquad \qquad \qquad \mathbf{E}; \Theta; \emptyset \vdash_{\vec{t}_C, \vec{a}_C}^c C \qquad \mathbf{E}; \Theta \vdash \det(i_r) \land \det(i_k) \\
& \quad \mathbf{E}; \Theta \vdash \text{blen}_{\vec{r}}(\vec{a}) \qquad \mathbf{E}; \Theta \vdash \text{blen}_{l_e}(\text{enc } m \ (r \ i_r) \ (\text{pk}(k \ i_k))) \land \text{blen}_{l_e}(\text{enc } (0_{\text{len}}(m)) \ (r \ i_r) \ (\text{pk}(k \ i_k))) \\
& \qquad \qquad \qquad \qquad \mathbf{E}; \Theta; \emptyset \vdash_{\epsilon_{\phi}} \phi_{\text{key}}^{k,i_k}(\vec{w}, C) \land \phi_{\text{rand}}^{r,i_r}(\vec{w}, C) \land \phi_{\text{dec}}^{k,i_k}(C, \vec{u}_1, \vec{a}_1) \\
& \qquad \qquad \qquad \qquad \mathbf{E}; \Theta \vdash \vec{u}, \text{ if } b \text{ then } C \ \vec{a} \ (\text{enc } (0_{\text{len}}(m)) \ (r \ i_r) \ (\text{pk}(k \ i_k))) \text{ else } u_e \sim_{\epsilon} \vec{v} \\
& \qquad \qquad \qquad \qquad \mathbf{E}; \Theta \vdash \vec{u}, \text{ if } b \text{ then } C \ \vec{a} \ (\text{enc } m \ (r \ i_r) \ (\text{pk}(k \ i_k))) \text{ else } u_e \sim_{\epsilon_f} \vec{v}
\end{align*}
$$

where $\vec{w} \stackrel{\text{def}}{=} \vec{u}, \vec{a}, b, m, i_r, i_k$ (note that $u_e$ is not in $\vec{w}$) and:

$$
t'_{C} \stackrel{\text{def}}{=} t_{C} \vec{l}_{e} \quad \text{and} \quad \epsilon_{f} \stackrel{\text{def}}{=} \lambda t, \vec{o}. \epsilon t \vec{o} + \epsilon_{\phi} + \epsilon_{\text{CCA}}(t + t'_{C} + \vec{o} \cdot (\vec{t}_{\vec{u}_1} t) + \vec{o}_{C} \cdot (\vec{t}_{\vec{a}_1} t'_{C}) + \vec{1} \cdot \vec{t}_0)
$$

<caption>Figure 12. Probabilistic independence and cryptographic rules.</caption>
**Probabilistic independence rules.**

In the $L_\epsilon$.FRESH, $c_n$ is a bound on the probability that the name $n$ selects any precise value. For simplicity we give the rule for one context, but it can easily be extended to vectors of contexts containing the same name.

$G_\epsilon$.E:FRESH

$$ \frac{\mathbb{E}; \Theta \vdash [\phi_{\text{fresh}}^{n,i}(\vec{u}, C(n_{\text{fresh}}())) \tilde{\vee} \phi_{\text{fresh}}^{n_{\text{fresh}},0}(\vec{u}, C(n_{\text{fresh}}()))]_{\epsilon_1}}{\mathbb{E}; \Theta \vdash \vec{u}, C(n) \sim_{\epsilon_0+\epsilon_1} \vec{v}} $$

$L_\epsilon$.FRESH

$$ \frac{\mathbb{E}; \Theta; \Gamma \vdash_{c_n} n i = u \Rightarrow \neg \phi_{\text{fresh}}^{n,i}(u, i)}{} $$

**Cryptographic rules.**

For simplicity we give the cryptographic rules for one context, but it can easily be extended to vectors of contexts containing the same encryption or hash. If $\vec{u} = u_1, \dots, u_n$ and $\vec{v} = v_1, \dots, v_n$ are two vectors of the same length, then $\vec{u} \cdot \vec{v} \stackrel{\text{def}}{=} \sum_i u_i \cdot v_i$ denotes the scalar product of $\vec{u}$ and $\vec{v}$. Moreover, $\vec{1} \cdot \vec{u} \stackrel{\text{def}}{=} \sum_i u_i$ is the scalar product of $\vec{u}$ with the sequence $1, \dots, 1$ of $n$ copies of $1$ ($\vec{1}$ is implicitly of length $\vec{u}$).

In the $G_\epsilon$.PRF and $G_\epsilon$.CCA 1 rules, $\vec{a} \stackrel{\text{def}}{=} \vec{a}_0, \vec{a}_1$ where $\vec{a}_0$ is of order 0 and $\vec{a}_1$ of order 1 and $\vec{u} \stackrel{\text{def}}{=} \vec{u}_0, \vec{u}_1$ where $\vec{u}_0$ is of order 0 and $\vec{u}_1$ of order 1.

$L_\epsilon$.EUF

$$ \frac{\mathbb{E}; \Theta; \emptyset \vdash_{\vec{t}}^c s, m, i \qquad \mathbb{E}; \Theta; \Gamma, \neg (\phi_{\text{key}}^{k,i}(s, m, t) \lor \phi_{\text{sign}}^{k,i}(s, m, t)) \vdash_{\epsilon} \psi \qquad \mathbb{E}; \Theta \vdash \det(i)}{\mathbb{E}; \Theta; \Gamma, \text{verify } s m (\text{pk } (k \ i)) \vdash_{\epsilon+\epsilon_{\text{EUF}}}(\vec{1} \cdot \vec{t}) \psi} $$

$G_\epsilon$.PRF

$$ \frac{\mathbb{E}; \Theta; \emptyset \vdash_{\vec{t}}^c \vec{u}_1 \qquad \mathbb{E}; \Theta; \emptyset \vdash_{\vec{t}}^c \vec{a}_1 \qquad \mathbb{E}; \Theta; \emptyset \vdash_{\vec{t}}^c \vec{u}_0, \vec{a}_0, b, m, i \qquad \mathbb{E}; \Theta; \emptyset \vdash_{\vec{t}}^c \vec{u}_0, \vec{a}_0, b, m, i \qquad \mathbb{E}; \Theta \vdash \det(i)}{\mathbb{E}; \Theta \vdash \text{blen}_{\vec{t}}(\vec{a}) \qquad \mathbb{E}; \Theta \vdash \text{blen}_{l_h}(\text{hash } m (k \ i)) \tilde{\wedge} \text{blen}_{l_h}(n_{\text{fresh}}()) \qquad \mathbb{E}; \Theta \vdash_{\epsilon_\phi} \psi_{\text{key}}^{k,i}(\vec{w}, C) \land \psi_{\text{msg}}^{k,i}(\vec{w}, C) \qquad \mathbb{E}; \Theta \vdash \vec{u}, \text{if } b \text{ then } C \vec{a} (n_{\text{fresh}}()) \text{ else } u_e \sim_{\epsilon} \vec{v}}{\mathbb{E}; \Theta \vdash \vec{u}, \text{ if } b \text{ then } C \vec{a} (\text{hash } m (k \ i)) \text{ else } u_e \sim_{\epsilon_f} \vec{v}} $$

where $\vec{w} \stackrel{\text{def}}{=} \vec{u}, \vec{a}, b, m, i$ (note that $u_e$ is not in $\vec{w}$) and:

$$ t'_{C} \stackrel{\text{def}}{=} t_{C} \vec{l}_{h} \quad \text{and} \quad \epsilon_{f} \stackrel{\text{def}}{=} \lambda t, \vec{o}. \epsilon t \vec{o} + \epsilon_{\phi} + \epsilon_{\text{PRF}}(t + t'_{C} + \vec{o} \cdot (\vec{t}_{\vec{u}_1} t) + \vec{o}_{C} \cdot (\vec{t}_{\vec{a}_1} t'_{C}) + \vec{1} \cdot \vec{t}_0) $$

$G_\epsilon$.CCA 1

$$ \frac{\mathbb{E}; \Theta; \emptyset \vdash_{\vec{t}}^c \vec{u}_1 \qquad \mathbb{E}; \Theta; \emptyset \vdash_{\vec{t}}^c \vec{a}_1 \qquad \mathbb{E}; \Theta; \emptyset \vdash_{\vec{t}}^c \vec{u}_0, \vec{a}_0, b, m, i_r, i_k \qquad \mathbb{E}; \Theta; \emptyset \vdash_{t_{C}, \vec{o}_C} C \qquad \mathbb{E}; \Theta \vdash \det(i_r) \tilde{\wedge} \det(i_k)}{\mathbb{E}; \Theta \vdash \text{blen}_{\vec{t}}(\vec{a}) \qquad \mathbb{E}; \Theta \vdash \text{blen}_{l_e}(\text{enc } m (r i_r) (\text{pk}(k i_k))) \tilde{\wedge} \text{blen}_{l_e}(\text{enc } (0_{\text{len}}(m)) (r i_r) (\text{pk}(k i_k))) \qquad \mathbb{E}; \Theta \vdash_{\epsilon_\phi} \phi_{\text{key}}^{k,i_k}(\vec{w}, C) \land \phi_{\text{rand}}^{r,i_r}(\vec{w}, C) \land \phi_{\text{dec}}^{k,i_k}(C, \vec{u}_1, \vec{a}_1) \qquad \mathbb{E}; \Theta \vdash \vec{u}, \text{ if } b \text{ then } C \vec{a} (\text{enc } (0_{\text{len}}(m)) (r i_r) (\text{pk}(k i_k))) \text{ else } u_e \sim_{\epsilon} \vec{v}}{\mathbb{E}; \Theta \vdash \vec{u}, \text{ if } b \text{ then } C \vec{a} (\text{enc } m (r i_r) (\text{pk}(k i_k))) \text{ else } u_e \sim_{\epsilon_f} \vec{v}} $$

where $\vec{w} \stackrel{\text{def}}{=} \vec{u}, \vec{a}, b, m, i_r, i_k$ (note that $u_e$ is not in $\vec{w}$) and:

$$ t'_{C} \stackrel{\text{def}}{=} t_{C} \vec{l}_{e} \quad \text{and} \quad \epsilon_{f} \stackrel{\text{def}}{=} \lambda t, \vec{o}. \epsilon t \vec{o} + \epsilon_{\phi} + \epsilon_{\text{CCA}}(t + t'_{C} + \vec{o} \cdot (\vec{t}_{\vec{u}_1} t) + \vec{o}_{C} \cdot (\vec{t}_{\vec{a}_1} t'_{C}) + \vec{1} \cdot \vec{t}_0) $$

<caption>Figure 12. Probabilistic independence and cryptographic rules.</caption>
Count-CB<sub>Π</sub>(p) is the number of G<sub>ε</sub>.E:CS<sub>R</sub> or G<sub>ε</sub>.E:BI-DEDUCE rules appearing below position p in Π:

$$
\text{Count-CB}_{\Pi}(p) \stackrel{\text{def}}{=} \left\{ \begin{array}{l} \left| \{p_0 \in \text{Path}_{\Pi}(p) \mid R_{\Pi}(p_0) \in \{G_{\epsilon}.E:CS_{R}, G_{\epsilon}.E:BI-DEDUCE\} \right| \\ 0 \end{array} \right| \quad \begin{array}{l} \text{if } R_{\Pi}(p) \text{ is a descending rule} \\ \text{otherwise} \end{array}
$$

Count-HW<sub>Π</sub>(p) is the number of G.WEAK rules appearing below position p in Π:

$$
\text{Count-HW}_{\Pi}(p) \stackrel{\text{def}}{=} \left\{ \begin{array}{l} \left| \{ p_0 \in \text{Path}_{\Pi}(p) \mid R_{\Pi}(p_0) = \text{G. weak} \} \right| \\ 0 \end{array} \right| \quad \begin{array}{l} \text{if } R_{\Pi}(p) \text{ is descending rule} \\ \text{otherwise} \end{array}
$$

We partition Trunc(Π) into the set of positions T<sub>RD</sub> where the G<sub>ε</sub>.E:REWRITE<sub>0</sub> or G.DUP rules are applied, and the
remaining set of position T<sub>A</sub>, i.e.:

$$
T_{RD} \stackrel{\text{def}}{=} \{ p \in \text{Trunc}(\Pi) \mid R_{\Pi}(p) \in \{ \text{G}_{\epsilon}.\text{E:REWRITE}_{0}, \text{G.DUP} \} \}
$$

$$
T_A \stackrel{\text{def}}{=} \{ p \in \text{Trunc}(\Pi) \mid R_{\Pi}(p) \notin \{ \text{G}_{\epsilon}.\text{E:REWRITE}_{0}, \text{G.DUP} \} \}
$$

The value Value<sub>AD</sub>(Π) ∈ N³ of a proof Π is defined as:

$$
\text{Value}_{\bullet_{AD}}(\Pi) \stackrel{\text{def}}{=} \left( \sum_{p \in T_A} \text{Count-CB}_{\Pi}(p), \sum_{p \in T_{RD}} \text{Count-CB}_{\Pi}(p), \sum_{p \in \text{Trunc}(\Pi)} \text{Count-HW}_{\Pi}(p) \right)
$$

Our goal is to obtain proofs where no ascending rule appear below a descending rule of the trunk, i.e. a proof such that
Value<sub>AD</sub>(Π) = (0, 0, 0).

<caption>Figure 13. Definitions of Count-HW<sub>Π</sub>(p), Count-CB<sub>Π</sub>(p) and Value<sub>AD</sub>(Π).</caption>

All occurrences of G.AXIOM are using the same axiom in those collapse rules
Commutation and merge between ascending rules

<figure><img src="image_2.png" /></figure>

Collapse between ascending rules and G<sub>ε</sub>.L-Loc:⊥

<figure><img src="image_3.png" /></figure>

Collapse between ascending rules and G.L-⊥

<figure><img src="image_4.png" /></figure>

Collapse between ascending rules and G.AXIOM

<figure><img src="image_5.png" /></figure>

Legend:

CS : G<sub>ε</sub>.E:CS<sub>R</sub>

B : G<sub>ε</sub>.E:BI-DEDUCE

W : G. WEAK

R : G<sub>ε</sub>.E:REWRITE<sub>0</sub>

⊥ : G.L-⊥

⊥ : G<sub>ε</sub>.L-LOC : ⊥

Ax : G.AXIOM

A : any rule

<caption>Figure 14. Shape of the collapsing proof transformations.</caption>
Count-CB<sub>Π</sub>(p) is the number of G<sub>ε</sub>.E:CS<sub>R</sub> or G<sub>ε</sub>.E:BI-DEDUCE rules appearing below position p in Π:

$$
\text{Count-CB}_{\Pi}(p) \stackrel{\text{def}}{=} \left\{ \begin{array}{l} \left| \{p_0 \in \text{Path}_{\Pi}(p) \mid R_{\Pi}(p_0) \in \{G_{\epsilon}.E:CS_{R}, G_{\epsilon}.E:BI-DEDUCE\} \right| \\ 0 \end{array} \right| \quad \begin{array}{l} \text{if } R_{\Pi}(p) \text{ is a descending rule} \\ \text{otherwise} \end{array}
$$

Count-HW<sub>Π</sub>(p) is the number of G.WEAK rules appearing below position p in Π:

$$
\text{Count-HW}_{\Pi}(p) \stackrel{\text{def}}{=} \left\{ \begin{array}{l} \left| \{ p_0 \in \text{Path}_{\Pi}(p) \mid R_{\Pi}(p_0) = \text{G. weak} \} \right| \\ 0 \end{array} \right| \quad \begin{array}{l} \text{if } R_{\Pi}(p) \text{ is descending rule} \\ \text{otherwise} \end{array}
$$

We partition Trunc(Π) into the set of positions T<sub>RD</sub> where the G<sub>ε</sub>.E:REWRITE<sub>0</sub> or G.DUP rules are applied, and the
remaining set of position T<sub>A</sub>, i.e.:

$$
T_{RD} \stackrel{\text{def}}{=} \{ p \in \text{Trunc}(\Pi) \mid R_{\Pi}(p) \in \{ \text{G}_{\epsilon}.\text{E:REWRITE}_{0}, \text{G.DUP} \} \}
$$

$$
T_A \stackrel{\text{def}}{=} \{ p \in \text{Trunc}(\Pi) \mid R_{\Pi}(p) \notin \{ \text{G}_{\epsilon}.\text{E:REWRITE}_{0}, \text{G.DUP} \} \}
$$

The value Value<sub>AD</sub>(Π) ∈ N<sup>3</sup> of a proof Π is defined as:

$$
\text{Value}_{\bullet_{AD}}(\Pi) \stackrel{\text{def}}{=} \left( \sum_{p \in T_A} \text{Count-CB}_{\Pi}(p), \sum_{p \in T_{RD}} \text{Count-CB}_{\Pi}(p), \sum_{p \in \text{Trunc}(\Pi)} \text{Count-HW}_{\Pi}(p) \right)
$$

Our goal is to obtain proofs where no ascending rule appear below a descending rule of the trunk, i.e. a proof such that
Value<sub>AD</sub>(Π) = (0, 0, 0).

<caption>Figure 13. Definitions of Count-HW<sub>Π</sub>(p), Count-CB<sub>Π</sub>(p) and Value<sub>AD</sub>(Π).</caption>

All occurrences of G.AXIOM are using the same axiom in those collapse rules
Commutation and merge between ascending rules

<figure><img src="image_9.png" /></figure>

Collapse between ascending rules and G<sub>ε</sub>.L-Loc:⊥

<figure><img src="image_10.png" /></figure>

Collapse between ascending rules and G.L-⊥

<figure><img src="image_11.png" /></figure>

Collapse between ascending rules and G.AXIOM

<figure><img src="image_12.png" /></figure>

Legend:

CS : G<sub>ε</sub>.E:CS<sub>R</sub>

B : G<sub>ε</sub>.E:BI-DEDUCE

W : G. WEAK

R : G<sub>ε</sub>.E:REWRITE<sub>0</sub>

⊥ : G.L-⊥

⊥ : G<sub>ε</sub>.L-LOC : ⊥

Ax : G.AXIOM

A : any rule

<caption>Figure 14. Shape of the collapsing proof transformations.</caption>
A. Sketch of the soundness proofs

In this section, we give the key ingredients which are necessary to check the soundness of our proof system. Later on, in
following sections, we will provide complete proofs for most of the rules that do not use the indistinguishability predicate.

a) *Global indistinguishability rules:* We sketch the proof of the rules given in Fig. 11:

• G<sub>ε</sub>.E:REFL and G<sub>ε</sub>.E:SYM. Proofs are trivial.

• G<sub>ε</sub>.E:TRANS. The proof relies on the triangular inequality.

* G<sub>ε</sub>.E:FA-BASE. We present this first (simple) reductionistic rule with more details, to serve as an example proof.
Consider a machine *A* against *û*<sub>*l*</sub>, *v* ~ *û*<sub>*r*</sub>, *v*. By hypothesis, we have a machine *M* computing *v* in time *t*<sub>*v*</sub> with error
probability at most *ε*<sub>*v*</sub>. Then, we build *B* against *û*<sub>*l*</sub> ~ *û*<sub>*r*</sub> as follows: 1) run *M*, which yields *v* (up-to error *ε*<sub>*v*</sub>) on some
tape; 2) then, *B* simulates *A*, using its own input tapes in-place (containing *û*<sub>*l*</sub> or *û*<sub>*r*</sub>) for the first input tapes of *A*, and
*M*'s output tape (which should contain *v*) as the last input tape of *A*; finally, *B* returns *A*'s answer.

B provides fresh working tapes for $\mathcal{M}$ and for $\mathcal{A}$, without re-using tapes, to ensure that $\mathcal{M}$ and $\mathcal{A}$ working tapes are initially empty.

Machine *B* can forward all oracle calls from *A* to its own oracles without any overhead: if *A* want to call oracle *f*<sub>*i*</sub> using
T as output tape, then *B* does exactly the same. Thus, *B* runs in time *t* + *t*<sub>*v*</sub> where *t* is the running time of *A*.

We conclude by observing that its advantage is at most $\mathcal{A}$'s advantage, plus two times the error $\varepsilon_v$ of $\mathcal{M}$, once per side of
the equivalence $\sim$.

* G<sub>ε</sub>.E:FA-FUN. Let *A* be a machine against *û*<sub>*l*</sub>, *f* ~ *û*<sub>*r*</sub>, *f*. By hypothesis, let *M* be a machine running in time *t*<sub>*f*</sub>(|*x*|)
(on input *x*), and such that *M* correctly computes *f*(*x*) on all inputs *x*, with a probability of error at most *ε*<sub>*f*</sub>.

We now build *B* against $\tilde{u}_l \sim \tilde{u}_r$. *B* simulates *A*, using its input tapes as input tapes for *A* (thus incurring no copy overhead), forwarding all oracle calls different from *f* to its own oracles.

At this step, it only remains to simulate a call to oracle *f*. If *A* calls *f* with output tape *T*, then *B* first copies the content *x* of *A*'s oracle input tape to an additional tape *T*<sub>*i*</sub>, and then executes *M* using *T*<sub>*i*</sub> as input tape and *T* as output tape (which is always possible, even if *M*'s input and output tapes are identical, i.e. *T*<sub>*i*</sub> = *T*).

*B* running time is the running time of *A*, plus the cost of simulating calls to *f*. We know that, since *A* runs in time at most *t*, all its oracle calls are on inputs of size at most *t*. Thus, each call to *f* is simulated in time *t* (to copy the input) plus *t*<sub>*f*</sub>(*t*) (to run *M*). Assuming that *A* calls *f* at most *o*<sub>*f*</sub> times, this yields an overall running time of *t* + *o*<sub>*f*</sub>·(*t* + *t*<sub>*f*</sub>(*t*)). Finally, we conclude by observing that, as for the previous rule, we need to pay twice the error *ε*<sub>*f*</sub> of *M*.

* G<sub>ε</sub>.E:FA-APP. Consider a machine *A* against *û*<sub>*l*</sub>, (*f*<sub>*l*</sub> *v*<sub>*l*</sub>) ~ *û*<sub>*r*</sub>, (*f*<sub>*r*</sub> *v*<sub>*r*</sub>). We build a machine *B* against *û*<sub>*l*</sub>, *f*<sub>*l*</sub>, *v*<sub>*l*</sub> ~ *û*<sub>*r*</sub>, *f*<sub>*r*</sub>, *v*<sub>*r*</sub>: on input *û*, *f*, *v* (which is either *û*<sub>*l*</sub>, *f*<sub>*l*</sub>, *v*<sub>*l*</sub> or *û*<sub>*r*</sub>, *f*<sub>*r*</sub>, *v*<sub>*r*</sub>, depending on the side), *B* copies *v* to the oracle input tape; calls oracle *f* on this oracle tape, which yields *f*(*v*) on an additional working tape *T*; and simulates *A*, using the tapes containing *û* as first inputs tapes, and *T* as last input tape.

*B*'s running time is *t* + *l* + 1, decomposed as: *A*'s running time *t*, plus the cost of copying *v* (which is at most *l*), plus a
cost 1 to trigger the special oracle call transition.

* G<sub>ε</sub>.E:FA-NAMES. Adversary *B* against the premise simulates Adversary *A* against the conclusion, except that it samples
values according to the distribution of *n*<sub>*f*</sub> itself.

* G<sub>ε</sub>.E:DUP-BASE. Consider an adversary *A* against *û*<sub>*l*</sub>, *v*<sub>*l*</sub>, *v*<sub>*l*</sub> ~ *û*<sub>*r*</sub>, *v*<sub>*r*</sub>. We build an adversary *B* against *û*<sub>*l*</sub>, *v*<sub>*l*</sub> ~ *û*<sub>*r*</sub>, *v*<sub>*r*</sub>
by simulating *A* using, in place, *B*'s inputs tapes. The missing input tape *T* of *A*, that should contain *v* (which is *v*<sub>*l*</sub> or *v*<sub>*r*</sub>,
depending on the side), is copied on-the-fly, as described next.

Let $T_0$ be *B*'s input tape initially containing *v*. *B* uses an additional working tape for *T*, initially empty, to which it will gradually copy *v* from $T_0$, copying *i*-th bit of *v* to *T* at the *i*-th step of *A*'s simulation. This is possible by simply having two additional heads, one on $T_0$ and the other on *T*, continually advancing to the right, until the head of $T_0$ reaches the end of *v*. As far as *A* is concerned, $T_0$ contains *v* from the beginning, as a bit has always been set before it can reach it. This construction has no running-time overhead, and yields Adversary *B* with the same advantage as *A*.

* G<sub>ε</sub>.E:DUP-FUN. Consider an adversary *A* against *û*<sub>*l*</sub>, *f*<sub>*l*</sub>, *f*<sub>*l*</sub> ~ *û*<sub>*r*</sub>, *f*<sub>*r*</sub>, *f*<sub>*r*</sub>. Adversary *B* against *û*<sub>*l*</sub>, *f*<sub>*l*</sub> ~ *û*<sub>*r*</sub>, *f*<sub>*r*</sub> simply simulates *A* in-place, on the same input tapes, forwarding each call to the first or second oracle *f* to its own version of *f*.

* G<sub>ε</sub>.E:WEAK. The proof is immediate: *B* against the premise simulates *A* against the conclusion, in-place, ignoring the inputs that *A* does not use.

* G<sub>ε</sub>.E:PERM. The proof is also straightforward: *B* against the premise simulates *A* against the conclusion, in-place, permuting input tapes in *A*'s transition table according to π.

* G.β and G.δ are trivially proven as properties of our term semantics.

* G<sub>ε</sub>.E:CS is a standard CCSA rule. E.g. see [13] for a proof.
A. Sketch of the soundness proofs

In this section, we give the key ingredients which are necessary to check the soundness of our proof system. Later on, in
following sections, we will provide complete proofs for most of the rules that do not use the indistinguishability predicate.

a) *Global indistinguishability rules:* We sketch the proof of the rules given in Fig. 11:

• G<sub>ε</sub>.E:REFL and G<sub>ε</sub>.E:SYM. Proofs are trivial.

• G<sub>ε</sub>.E:TRANS. The proof relies on the triangular inequality.

* G<sub>ε</sub>.E:FA-BASE. We present this first (simple) reductionistic rule with more details, to serve as an example proof.
Consider a machine *A* against *û*<sub>*l*</sub>, *v* ~ *û*<sub>*r*</sub>, *v*. By hypothesis, we have a machine *M* computing *v* in time *t*<sub>*v*</sub> with error
probability at most *ε*<sub>*v*</sub>. Then, we build *B* against *û*<sub>*l*</sub> ~ *û*<sub>*r*</sub> as follows: 1) run *M*, which yields *v* (up-to error *ε*<sub>*v*</sub>) on some
tape; 2) then, *B* simulates *A*, using its own input tapes in-place (containing *û*<sub>*l*</sub> or *û*<sub>*r*</sub>) for the first input tapes of *A*, and
*M*'s output tape (which should contain *v*) as the last input tape of *A*; finally, *B* returns *A*'s answer.

B provides fresh working tapes for $\mathcal{M}$ and for $\mathcal{A}$, without re-using tapes, to ensure that $\mathcal{M}$ and $\mathcal{A}$ working tapes are initially empty.

Machine *B* can forward all oracle calls from *A* to its own oracles without any overhead: if *A* want to call oracle *f*<sub>*i*</sub> using
T as output tape, then *B* does exactly the same. Thus, *B* runs in time *t* + *t*<sub>*v*</sub> where *t* is the running time of *A*.

We conclude by observing that its advantage is at most $\mathcal{A}$'s advantage, plus two times the error $\varepsilon_v$ of $\mathcal{M}$, once per side of
the equivalence $\sim$.

* G<sub>ε</sub>.E:FA-FUN. Let *A* be a machine against *û*<sub>*l*</sub>, *f* ~ *û*<sub>*r*</sub>, *f*. By hypothesis, let *M* be a machine running in time *t*<sub>*f*</sub>(|*x*|)
(on input *x*), and such that *M* correctly computes *f*(*x*) on all inputs *x*, with a probability of error at most *ε*<sub>*f*</sub>.

We now build *B* against $\tilde{u}_l \sim \tilde{u}_r$. *B* simulates *A*, using its input tapes as input tapes for *A* (thus incurring no copy overhead), forwarding all oracle calls different from *f* to its own oracles.

At this step, it only remains to simulate a call to oracle *f*. If *A* calls *f* with output tape *T*, then *B* first copies the content
*x* of *A*'s oracle input tape to an additional tape *T*<sub>*i*</sub>, and then executes *M* using *T*<sub>*i*</sub> as input tape and *T* as output tape
(which is always possible, even if *M*'s input and output tapes are identical, i.e. *T*<sub>*i*</sub> = *T*).

*B* running time is the running time of *A*, plus the cost of simulating calls to *f*. We know that, since *A* runs in time at most *t*, all its oracle calls are on inputs of size at most *t*. Thus, each call to *f* is simulated in time *t* (to copy the input) plus *t*<sub>*f*</sub>(*t*) (to run *M*). Assuming that *A* calls *f* at most *o*<sub>*f*</sub> times, this yields an overall running time of *t* + *o*<sub>*f*</sub>·(*t* + *t*<sub>*f*</sub>(*t*)).
Finally, we conclude by observing that, as for the previous rule, we need to pay twice the error *ε*<sub>*f*</sub> of *M*.

* G<sub>ε</sub>.E:FA-APP. Consider a machine *A* against *û*<sub>*l*</sub>, (*f*<sub>*l*</sub> *v*<sub>*l*</sub>) ~ *û*<sub>*r*</sub>, (*f*<sub>*r*</sub> *v*<sub>*r*</sub>). We build a machine *B* against *û*<sub>*l*</sub>, *f*<sub>*l*</sub>, *v*<sub>*l*</sub> ~ *û*<sub>*r*</sub>, *f*<sub>*r*</sub>, *v*<sub>*r*</sub>: on input *û*, *f*, *v* (which is either *û*<sub>*l*</sub>, *f*<sub>*l*</sub>, *v*<sub>*l*</sub> or *û*<sub>*r*</sub>, *f*<sub>*r*</sub>, *v*<sub>*r*</sub>, depending on the side), *B* copies *v* to the oracle input tape; calls oracle *f* on this oracle tape, which yields *f*(*v*) on an additional working tape *T*; and simulates *A*, using the tapes containing *û* as first inputs tapes, and *T* as last input tape.

*B*'s running time is *t* + *l* + 1, decomposed as: *A*'s running time *t*, plus the cost of copying *v* (which is at most *l*), plus a
cost 1 to trigger the special oracle call transition.

* G<sub>ε</sub>.E:FA-NAMES. Adversary *B* against the premise simulates Adversary *A* against the conclusion, except that it samples
values according to the distribution of *n*<sub>*f*</sub> itself.

* G<sub>ε</sub>.E:DUP-BASE. Consider an adversary *A* against *û*<sub>*l*</sub>, *v*<sub>*l*</sub>, *v*<sub>*l*</sub> ~ *û*<sub>*r*</sub>, *v*<sub>*r*</sub>. We build an adversary *B* against *û*<sub>*l*</sub>, *v*<sub>*l*</sub> ~ *û*<sub>*r*</sub>, *v*<sub>*r*</sub>
by simulating *A* using, in place, *B*'s inputs tapes. The missing input tape *T* of *A*, that should contain *v* (which is *v*<sub>*l*</sub> or *v*<sub>*r*</sub>,
depending on the side), is copied on-the-fly, as described next.

Let $T_0$ be *B*'s input tape initially containing *v*. *B* uses an additional working tape for *T*, initially empty, to which it will gradually copy *v* from $T_0$, copying *i*-th bit of *v* to *T* at the *i*-th step of *A*'s simulation. This is possible by simply having two additional heads, one on $T_0$ and the other on *T*, continually advancing to the right, until the head of $T_0$ reaches the end of *v*. As far as *A* is concerned, $T_0$ contains *v* from the beginning, as a bit has always been set before it can reach it. This construction has no running-time overhead, and yields Adversary *B* with the same advantage as *A*.

* G<sub>ε</sub>.E:DUP-FUN. Consider an adversary *A* against *û*<sub>*l*</sub>, *f*<sub>*l*</sub>, *f*<sub>*l*</sub> ~ *û*<sub>*r*</sub>, *f*<sub>*r*</sub>, *f*<sub>*r*</sub>. Adversary *B* against *û*<sub>*l*</sub>, *f*<sub>*l*</sub> ~ *û*<sub>*r*</sub>, *f*<sub>*r*</sub> simply simulates *A* in-place, on the same input tapes, forwarding each call to the first or second oracle *f* to its own version of *f*.

* G<sub>ε</sub>.E:WEAK. The proof is immediate: *B* against the premise simulates *A* against the conclusion, in-place, ignoring the inputs that *A* does not use.

* G<sub>ε</sub>.E:PERM. The proof is also straightforward: *B* against the premise simulates *A* against the conclusion, in-place, permuting input tapes in *A*'s transition table according to π.

* G.β and G.δ are trivially proven as properties of our term semantics.

* G<sub>ε</sub>.E:CS is a standard CCSA rule. E.g. see [13] for a proof.
• G<sub>ε</sub>.E:BI-DEDUCE is proved through a cryptographic reduction simulating the contexts and the sampling of the names, carefully accounting for cost aspects.

• For the two cryptographic rules G<sub>ε</sub>.CCA1 and G<sub>ε</sub>.PRF, we perform a reduction to the cryptographic game. First, we use the φ-condition as an up-to-bad argument in order to ensure that we can compute our terms without needing to compute the key under the cryptographic hypothesis. (see [17, Proposition 8] for more details about this point). Then, we compute the Boolean and the challenge (along with some other stuff that can be computed at the same time). If the Boolean returns 0, we also abort and return 0. Otherwise, we call the challenge oracle with our challenge, and after that we compute the context that uses the return of the oracle (that is why in the CCA1 game, we have the extra condition φ<sub>dec</sub>() in order to ensure that our context can be computed without calling the decryption oracle (since we do not have access to it anymore). Finally, we can call the attacker against our assumption and return the same result.

## B. Auxillary Lemmas

**Proposition 2.** Let $\mathbb{E}$ be a valid environment, $\phi$ a boolean term and $\varepsilon$ a term of type real such that $\mathbb{E} \vdash \forall (x : \tau) . \phi : \mathbf{bool}$. For all model $\mathcal{M}$ of $\mathbb{E}$, we have:

$$ \mathcal{M} : \mathbb{E} \models [\forall (x : \tau) . \phi]_{\varepsilon} \quad \text{iff.} \quad \mathcal{M} : \mathbb{E} \models \tilde{\forall} (x : \tau) . [\phi]_{\varepsilon} $$

*Proof.* The proof is exactly the same than the one of the analogue property in [17, Proposition 2]. Notice that the exact same proof work since $x$ cannot appear in $\varepsilon$ since $[\forall (x : \tau) . \phi]_{\varepsilon}$ is well-typed. □

## C. Local Judgement: Left Local Rules

• L<sub>ε</sub>.L-∀:

Let $\mathcal{M}$ be a model such that $\mathcal{M} : \mathbb{E} \models \Theta$.

Let $\eta \in \mathbb{N}$, $\rho \in \mathbb{T}_{\mathcal{M},\eta}$:

$[\forall (x : \tau) . \phi]_{\mathcal{M}}^{\eta, \rho} = 1$ imply that $[\phi\{x \mapsto t\}]_{\mathcal{M}}^{\eta, \rho} = 1$ since $\mathbb{E} \vdash t : \tau$.

Therefore, since $[\neg((\wedge\Gamma) \wedge \forall (x : \tau) . \phi \Rightarrow \psi)]_{\mathcal{M}}^{\eta, \rho} = [(\wedge\Gamma) \wedge \forall (x : \tau) . \phi \wedge \neg\psi]_{\mathcal{M}}^{\eta, \rho}$ and $[\neg((\wedge\Gamma) \wedge \phi\{x \mapsto t\} \Rightarrow \psi)]_{\mathcal{M}}^{\eta, \rho} = [(\wedge\Gamma) \wedge \phi\{x \mapsto t\} \wedge \neg\psi]_{\mathcal{M}}^{\eta, \rho}$.

So, $[\neg((\wedge\Gamma) \wedge \forall (x : \tau) . \phi \Rightarrow \psi)]_{\mathcal{M}}^{\eta, \rho} = 1$ imply that $[\neg((\wedge\Gamma) \wedge \phi\{x \mapsto t\} \Rightarrow \psi)]_{\mathcal{M}}^{\eta, \rho} = 1$.

Therefore, for every $\eta \in \mathbb{N}$,

$$ \begin{align*} & \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg((\wedge\Gamma) \wedge \forall (x : \tau) . \phi \Rightarrow \psi)) \\ \leq & \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg((\wedge\Gamma) \wedge \phi\{x \mapsto t\} \Rightarrow \psi)) \\ \leq & \mathbb{E}_{\rho}([\varepsilon]_{\mathcal{M}}^{\eta, \rho}), \end{align*} $$

which clearly imply the soundness of the rule L<sub>ε</sub>.L-∀.

• L<sub>ε</sub>.L-∃:

Let $\mathcal{M}$ be a model of $\mathbb{E}$.

We have to show that, assuming:

$$ \mathcal{M} \models \tilde{\forall} (x : \tau) . (\tilde{\lambda}\Theta) \Rightarrow [((\wedge\Gamma) \wedge \phi) \Rightarrow \psi]_{\varepsilon} $$

(This is equivalent to have that the premise of the rule holds for all model that are extension of $\mathcal{M}$ for the new declaration in $\mathbb{E}$, $x : \tau$) We have:

$$ \mathcal{M} \models (\tilde{\lambda}\Theta) \Rightarrow [((\wedge\Gamma) \wedge (\exists (x : \tau) . \phi) \Rightarrow \psi)]_{\varepsilon} $$

In fact, this is even a equivalence Indeed, the last equation holds iff.

$$ \mathcal{M} \models (\tilde{\lambda}\Theta) \Rightarrow [\forall (x : \tau) . ((\wedge\Gamma) \wedge \phi) \Rightarrow \psi)]_{\varepsilon} $$

holds (since $x$ doesn't appear in $\Gamma$ or $\psi$). By **Proposition 2**, that holds iff.

$$ \mathcal{M} \models (\tilde{\lambda}\Theta) \Rightarrow \tilde{\forall} (x : \tau) . [((\wedge\Gamma) \wedge \phi) \Rightarrow \psi)]_{\varepsilon} $$

holds, and that finally if and only if our assumption holds since $x$ doesn't appear in $\Theta$.

• L<sub>ε</sub>.L-⇒:

Let $\mathcal{M}$ be a model such that $\mathcal{M} : \mathbb{E} \models \Theta$.

Let $\eta \in \mathbb{N}$, $\rho \in \mathbb{T}_{\mathcal{M},\eta}$. We have that:

$$ \begin{align*} & [\neg((\wedge\Gamma) \wedge (\phi_0 \Rightarrow \phi_1) \Rightarrow \psi)]_{\mathcal{M}}^{\eta, \rho} \\ = & [((\wedge\Gamma) \wedge \neg\phi_0 \wedge \neg\psi) \vee ((\wedge\Gamma) \wedge \phi_1 \wedge \neg\psi)]_{\mathcal{M}}^{\eta, \rho} \end{align*} $$
* $G_{\varepsilon}.E:BI-DEDUCE$ is proved through a cryptographic reduction simulating the contexts and the sampling of the names, carefully accounting for cost aspects.

* For the two cryptographic rules $G_{\varepsilon}.CCA1$ and $G_{\varepsilon}.PRF$, we perform a reduction to the cryptographic game. First, we use the $\phi$-condition as an up-to-bad argument in order to ensure that we can compute our terms without needing to compute the key under the cryptographic hypothesis. (see [17, Proposition 8] for more details about this point). Then, we compute the Boolean and the challenge (along with some other stuff that can be computed at the same time). If the Boolean returns 0, we also abort and return 0. Otherwise, we call the challenge oracle with our challenge, and after that we compute the context that uses the return of the oracle (that is why in the CCA1 game, we have the extra condition $\phi_{\text{dec}}$) in order to ensure that our context can be computed without calling the decryption oracle (since we do not have access to it anymore). Finally, we can call the attacker against our assumption and return the same result.

## B. Auxillary Lemmas

**Proposition 2.** Let $\mathbb{E}$ be a valid environment, $\phi$ a boolean term and $\varepsilon$ a term of type real such that $\mathbb{E} \vdash \forall (x : \tau).\phi : \text{bool}$. For all model $\mathcal{M}$ of $\mathbb{E}$, we have:

$$ \mathcal{M} : \mathbb{E} \models [\forall (x : \tau).\phi]_{\varepsilon} \quad \text{iff.} \quad \mathcal{M} : \mathbb{E} \models \tilde{\forall} (x : \tau). [\phi]_{\varepsilon} $$

*Proof.* The proof is exactly the same than the one of the analogue property in [17, Proposition 2]. Notice that the exact same proof work since $x$ cannot appear in $\varepsilon$ since $[\forall (x : \tau).\phi]_{\varepsilon}$ is well-typed. $\square$

## C. Local Judgement: Left Local Rules

* $L_{\varepsilon}.L-\forall$:

Let $\mathcal{M}$ be a model such that $\mathcal{M} : \mathbb{E} \models \Theta$.

Let $\eta \in \mathbb{N}$, $\rho \in T_{\mathcal{M},\eta}$:

$[\forall (x : \tau).\phi]_{\mathcal{M}}^{\eta, \rho} = 1$ imply that $[\phi\{x \mapsto t\}]_{\mathcal{M}}^{\eta, \rho} = 1$ since $\mathbb{E} \vdash t : \tau$.

Therefore, since $[\neg((\wedge\Gamma) \wedge \forall (x : \tau).\phi \Rightarrow \psi)]_{\mathcal{M}}^{\eta, \rho} = [((\wedge\Gamma) \wedge \forall (x : \tau).\phi \wedge \neg\psi)]_{\mathcal{M}}^{\eta, \rho}$ and $[\neg((\wedge\Gamma) \wedge \phi\{x \mapsto t\} \Rightarrow \psi)]_{\mathcal{M}}^{\eta, \rho} = [((\wedge\Gamma) \wedge \phi\{x \mapsto t\} \wedge \neg\psi)]_{\mathcal{M}}^{\eta, \rho}$.

So, $[\neg((\wedge\Gamma) \wedge \forall (x : \tau).\phi \Rightarrow \psi)]_{\mathcal{M}}^{\eta, \rho} = 1$ imply that $[\neg((\wedge\Gamma) \wedge \phi\{x \mapsto t\} \Rightarrow \psi)]_{\mathcal{M}}^{\eta, \rho} = 1$.

Therefore, for every $\eta \in \mathbb{N}$,

$$ \begin{align*} & \mathrm{Pr}_{\rho \in T_{\mathcal{M},\eta}} (\neg((\wedge\Gamma) \wedge \forall (x : \tau).\phi \Rightarrow \psi)) \\ & \leq \mathrm{Pr}_{\rho \in T_{\mathcal{M},\eta}} (\neg((\wedge\Gamma) \wedge \phi\{x \mapsto t\} \Rightarrow \psi)) \\ & \leq \mathrm{E}_{\rho}([\varepsilon]_{\mathcal{M}}^{\eta, \rho}), \end{align*} $$

which clearly imply the soundness of the rule $L_{\varepsilon}.L-\forall$.

* $L_{\varepsilon}.L-\exists$:

Let $\mathcal{M}$ be a model of $\mathbb{E}$.

We have to show that, assuming:

$$ \mathcal{M} \models \tilde{\forall} (x : \tau).(\tilde{\lambda}\Theta) \Rightarrow [((\wedge\Gamma) \wedge \phi) \Rightarrow \psi]_{\varepsilon} $$

(This is equivalent to have that the premise of the rule holds for all model that are extension of $\mathcal{M}$ for the new declaration in $\mathbb{E}$, $x : \tau$) We have:

$$ \mathcal{M} \models (\tilde{\lambda}\Theta) \Rightarrow [((\wedge\Gamma) \wedge (\exists (x : \tau).\phi) \Rightarrow \psi)]_{\varepsilon} $$

In fact, this is even a equivalence Indeed, the last equation holds iff.

$$ \mathcal{M} \models (\tilde{\lambda}\Theta) \Rightarrow [\forall (x : \tau).((\wedge\Gamma) \wedge \phi) \Rightarrow \psi)]_{\varepsilon} $$

holds (since $x$ doesn't appear in $\Gamma$ or $\psi$). By **Proposition 2**, that holds iff.

$$ \mathcal{M} \models (\tilde{\lambda}\Theta) \Rightarrow \tilde{\forall} (x : \tau). [((\wedge\Gamma) \wedge \phi) \Rightarrow \psi)]_{\varepsilon} $$

holds, and that finally if and only if our assumption holds since $x$ doesn't appear in $\Theta$.

* $L_{\varepsilon}.L-\Rightarrow$:

Let $\mathcal{M}$ be a model such that $\mathcal{M} : \mathbb{E} \models \Theta$.

Let $\eta \in \mathbb{N}$, $\rho \in T_{\mathcal{M},\eta}$. We have that:

$$ \begin{align*} & [\neg((\wedge\Gamma) \wedge (\phi_0 \Rightarrow \phi_1) \Rightarrow \psi)]_{\mathcal{M}}^{\eta, \rho} \\ & = [((\wedge\Gamma) \wedge \neg\phi_0 \wedge \neg\psi) \vee ((\wedge\Gamma) \wedge \phi_1 \wedge \neg\psi)]_{\mathcal{M}}^{\eta, \rho} \end{align*} $$
is equal to 1 when either $[[\neg((\wedge\Gamma) \Rightarrow \phi_0)]_{\mathfrak{M}}^{\eta,\rho} = [[((\wedge\Gamma) \wedge \neg\phi_0)]_{\mathfrak{M}}^{\eta,\rho}$ is equal to 1 or $[[\neg(((\wedge\Gamma) \wedge \phi_1) \Rightarrow \psi)]_{\mathfrak{M}}^{\eta,\rho} = [[((\wedge\Gamma) \wedge \phi_1 \wedge \neg\psi)]_{\mathfrak{M}}^{\eta,\rho}$ is equal to 1. Therefore, for every $\eta \in \mathbb{N}$:

$$
\begin{align*}
& \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} ( [[\neg((\wedge\Gamma) \wedge (\phi_0 \Rightarrow \phi_1) \Rightarrow \psi)]_{\mathfrak{M}}^{\eta,\rho} ) \\
\leq & \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} ( [[\neg((\wedge\Gamma) \Rightarrow \phi_0)]_{\mathfrak{M}}^{\eta,\rho} ) \\
& + \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} ( [[\neg((\wedge\Gamma) \wedge \phi_1) \Rightarrow \psi)]_{\mathfrak{M}}^{\eta,\rho} ) \\
\leq & \mathrm{E}_{\rho}([[\varepsilon_0]]_{\mathfrak{M}}^{\eta,\rho}) + \mathrm{E}_{\rho}([[\varepsilon_1]]_{\mathfrak{M}}^{\eta,\rho})
\end{align*}
$$

which clearly imply the soundness of the rule $L_{\varepsilon} \cdot L \Rightarrow$.

* $L_{\varepsilon} \cdot L \wedge$: The premise and the conclusion clearly have the exact same semantic.

* $L_{\varepsilon} \cdot L \vee$:

Let $\mathfrak{M}$ be a model such that $\mathfrak{M} : \mathbb{E} \models \Theta$.

Let $\eta \in \mathbb{N}$, $\rho \in \mathbb{T}_{\mathfrak{M},\eta}$. Then:

$$[[\neg((\wedge\Gamma) \wedge (\phi_0 \lor \phi_1)) \Rightarrow \psi]]_{\mathfrak{M}}^{\eta,\rho} = [[((\wedge\Gamma) \wedge \phi_0 \wedge \neg\psi) \lor ((\wedge\Gamma) \wedge \phi_1 \wedge \neg\psi)]_{\mathfrak{M}}^{\eta,\rho}.$$

Therefore, for every $\eta \in \mathbb{N}$:

$$
\begin{align*}
& \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} ( [[\neg((\wedge\Gamma) \wedge (\phi_0 \lor \phi_1)) \Rightarrow \psi)]_{\mathfrak{M}}^{\eta,\rho} ) \\
\leq & \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} ( [[\neg((\wedge\Gamma) \wedge \phi_0) \Rightarrow \psi]]_{\mathfrak{M}}^{\eta,\rho} ) \\
& + \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} ( [[\neg((\wedge\Gamma) \wedge \phi_1) \Rightarrow \psi)]_{\mathfrak{M}}^{\eta,\rho} ) \\
\leq & \mathrm{E}_{\rho}([[\varepsilon_0]]_{\mathfrak{M}}^{\eta,\rho}) + \mathrm{E}_{\rho}([[\varepsilon_1]]_{\mathfrak{M}}^{\eta,\rho})
\end{align*}
$$

which clearly imply the soundness of the rule $L_{\varepsilon} \cdot L \vee$.

* $L_{\varepsilon} \cdot L \perp$:

Let $\mathfrak{M}$ be a model such that $\mathfrak{M} : \mathbb{E} \models \Theta$.

Let $\eta \in \mathbb{N}$, $\rho \in \mathbb{T}_{\mathfrak{M},\eta}$. Then:

$$[[((\wedge\Gamma) \wedge \perp) \Rightarrow \psi]]_{\mathfrak{M}}^{\eta,\rho} = 1.$$

Therefore, for every $\eta \in \mathbb{N}$:

$$\mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} ( \neg [[((\wedge\Gamma) \wedge \perp) \Rightarrow \psi]]_{\mathfrak{M}}^{\eta,\rho} ) \leq 0$$

which clearly imply the soundness of the rule $L_{\varepsilon} \cdot L \perp$.

### D. Local Judgement: Left Global Rules

* $L_{\varepsilon} \cdot L \tilde{\vee}$:

Let $\mathfrak{M}$ be a model such that $\mathfrak{M} : \mathbb{E} \models (\wedge\Theta) \wedge \forall(x : \tau).F$

Then $\mathfrak{M} \models (\wedge\Theta) \wedge F\{x \mapsto t\}$ (since $\mathbb{E} \vdash t : \tau$).

Therefore, $\mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} ( [[\neg((\wedge\Gamma) \Rightarrow \phi)]_{\mathfrak{M}}^{\eta,\rho} ) \leq \mathrm{E}_{\rho}([[\varepsilon]]_{\mathfrak{M}}^{\eta,\rho}) $.

* $L_{\varepsilon} \cdot L \tilde{\wedge}$:

Let $\mathfrak{M}$ be a model of $\mathbb{E}$.

We want to show that:

$$\mathfrak{M} \models (\wedge\Theta \wedge \tilde{\exists}(x : \tau).F) \Rightarrow [(\wedge\Gamma) \Rightarrow \phi]_{\varepsilon},$$

which is equivalent to (since $x$ does not appear in $\Theta$, $\Gamma$ and $\phi$)

$$\mathfrak{M} \models \tilde{\forall}(x : \tau).((\wedge\Theta \wedge F) \Rightarrow [(\wedge\Gamma) \Rightarrow \phi]_{\varepsilon}).$$

That is exactly the premise of the rule $L_{\varepsilon} \cdot L \tilde{\wedge}$.

* $L_{\varepsilon} \cdot L \tilde{\Rightarrow}$:

Let $\mathfrak{M}$ be a model such that $\mathfrak{M} : \mathbb{E} \models \Theta$, $(F_0 \Rightarrow F_1)$.

Then, by the first premise, we have $\mathfrak{M} \models F_0$, then we have $\mathfrak{M} \models F_1$ since $\mathfrak{M} \models F_0 \Rightarrow F_1$.

Therefore, by the second premise, $\mathfrak{M} \models [\wedge\Gamma \Rightarrow \psi]_{\varepsilon}$ which prove the soundness of $L_{\varepsilon} \cdot L \Rightarrow$

* $L_{\varepsilon} \cdot L \tilde{\Lambda}$: The premise and the conclusion clearly have the exact same semantic.

* $L_{\varepsilon} \cdot L \tilde{\vee}$:

Let $\mathfrak{M}$ be a model such that $\mathfrak{M} : \mathbb{E} \models \Theta$, $(F_0 \tilde{\vee} F_1)$.

Then $\mathfrak{M} \models \Theta, F_0$ or $\mathfrak{M} \models \Theta, F_1$.

Therefore, by the premises, $\mathfrak{M} \models [\wedge\Gamma \Rightarrow \psi]_{\varepsilon}$.

* $L_{\varepsilon} \cdot L \tilde{\wedge}$:

Let $\mathfrak{M}$ be a model such that $\mathfrak{M} : \mathbb{E} \models \Theta, \tilde{\wedge}$.

Then, $\mathfrak{M} \models [\wedge\Gamma \Rightarrow \psi]_{\varepsilon}$.
is equal to 1 when either $[\neg((\wedge\Gamma) \Rightarrow \phi_0)]_{\mathfrak{M}}^{\eta, \rho} = [((\wedge\Gamma) \wedge \neg\phi_0)]_{\mathfrak{M}}^{\eta, \rho}$ is equal to 1 or $[\neg(((\wedge\Gamma) \wedge \phi_1) \Rightarrow \psi)]_{\mathfrak{M}}^{\eta, \rho} = [((\wedge\Gamma) \wedge \phi_1 \wedge \neg\psi)]_{\mathfrak{M}}^{\eta, \rho}$ is equal to 1. Therefore, for every $\eta \in \mathbb{N}$:

$$
\begin{align*}
& \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} ( [\neg((\wedge\Gamma) \wedge (\phi_0 \Rightarrow \phi_1) \Rightarrow \psi)]_{\mathfrak{M}}^{\eta,\rho}) \\
\leq & \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} ( [\neg((\wedge\Gamma) \Rightarrow \phi_0)]_{\mathfrak{M}}^{\eta,\rho}) \\
& + \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} ( [\neg(((\wedge\Gamma) \wedge \phi_1) \Rightarrow \psi)]_{\mathfrak{M}}^{\eta,\rho}) \\
\leq & \mathrm{E}_{\rho}([\varepsilon_0]_{\mathfrak{M}}^{\eta,\rho}) + \mathrm{E}_{\rho}([\varepsilon_1]_{\mathfrak{M}}^{\eta,\rho})
\end{align*}
$$

which clearly imply the soundness of the rule $L_{\varepsilon} \cdot L \Rightarrow$.

* $L_{\varepsilon} \cdot L \wedge$: The premise and the conclusion clearly have the exact same semantic.

* $L_{\varepsilon} \cdot L \vee$:

Let $\mathfrak{M}$ be a model such that $\mathfrak{M} : \mathbb{E} \models \Theta$.

Let $\eta \in \mathbb{N}$, $\rho \in \mathbb{T}_{M,\eta}$. Then:

$$ [\neg((\wedge\Gamma) \wedge (\phi_0 \lor \phi_1)) \Rightarrow \psi]_{\mathfrak{M}}^{\eta,\rho} = [((\wedge\Gamma) \wedge \phi_0 \wedge \neg\psi) \lor ((\wedge\Gamma) \wedge \phi_1 \wedge \neg\psi)]_{\mathfrak{M}}^{\eta,\rho}. $$

Therefore, for every $\eta \in \mathbb{N}$:

$$
\begin{align*}
& \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} ( [\neg(((\wedge\Gamma) \wedge (\phi_0 \lor \phi_1)) \Rightarrow \psi)]_{\mathfrak{M}}^{\eta,\rho}) \\
\leq & \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} ( [\neg((\wedge\Gamma) \wedge \phi_0) \Rightarrow \psi]_{\mathfrak{M}}^{\eta,\rho}) \\
& + \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} ( [\neg(((\wedge\Gamma) \wedge \phi_1) \Rightarrow \psi)]_{\mathfrak{M}}^{\eta,\rho}) \\
\leq & \mathrm{E}_{\rho}([\varepsilon_0]_{\mathfrak{M}}^{\eta,\rho}) + \mathrm{E}_{\rho}([\varepsilon_1]_{\mathfrak{M}}^{\eta,\rho})
\end{align*}
$$

which clearly imply the soundness of the rule $L_{\varepsilon} \cdot L \vee$.

* $L_{\varepsilon} \cdot L \perp$:

Let $\mathfrak{M}$ be a model such that $\mathfrak{M} : \mathbb{E} \models \Theta$.

Let $\eta \in \mathbb{N}$, $\rho \in \mathbb{T}_{M,\eta}$. Then:

$$ [((\wedge\Gamma) \wedge \perp \Rightarrow \psi)]_{\mathfrak{M}}^{\eta,\rho} = 1. $$

Therefore, for every $\eta \in \mathbb{N}$:

$$ \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} (\neg [((\wedge\Gamma) \wedge \perp \Rightarrow \psi)]_{\mathfrak{M}}^{\eta,\rho}) \leq 0 $$

which clearly imply the soundness of the rule $L_{\varepsilon} \cdot L \perp$.

## D. Local Judgement: Left Global Rules

* $L_{\varepsilon} \cdot L \tilde{\nabla}$:

Let $\mathfrak{M}$ be a model such that $\mathfrak{M} : \mathbb{E} \models (\wedge\Theta) \wedge \forall(x : \tau).F$

Then $\mathfrak{M} \models (\wedge\Theta) \wedge F\{x \mapsto t\}$ (since $\mathbb{E} \vdash t : \tau$).

Therefore, $\mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} ( [\neg((\wedge\Gamma) \Rightarrow \phi)]_{\mathfrak{M}}^{\eta,\rho}) \leq \mathrm{E}_{\rho}([\varepsilon]_{\mathfrak{M}}^{\eta,\rho})$.

* $L_{\varepsilon} \cdot L \tilde{\Xi}$:

Let $\mathfrak{M}$ be a model of $\mathbb{E}$.

We want to show that:

$$ \mathfrak{M} \models (\wedge\Theta \wedge \tilde{\Xi}(x : \tau).F) \Rightarrow [((\wedge\Gamma) \Rightarrow \phi]_{\varepsilon}, $$

which is equivalent to (since $x$ does not appear in $\Theta$, $\Gamma$ and $\phi$)

$$ \mathfrak{M} \models \tilde{\nabla}(x : \tau).((\wedge\Theta \wedge F) \Rightarrow [((\wedge\Gamma) \Rightarrow \phi]_{\varepsilon}). $$

That is exactly the premise of the rule $L_{\varepsilon} \cdot L \tilde{\Xi}$.

* $L_{\varepsilon} \cdot L \tilde{\Rightarrow}$:

Let $\mathfrak{M}$ be a model such that $\mathfrak{M} : \mathbb{E} \models \Theta$, $(F_0 \Rightarrow F_1)$.

Then, by the first premise, we have $\mathfrak{M} \models F_0$, then we have $\mathfrak{M} \models F_1$ since $\mathfrak{M} \models F_0 \Rightarrow F_1$.

Therefore, by the second premise, $\mathfrak{M} \models [\wedge\Gamma \Rightarrow \psi]_{\varepsilon}$ which prove the soundness of $L_{\varepsilon} \cdot L \Rightarrow$

* $L_{\varepsilon} \cdot L \tilde{\Lambda}$: The premise and the conclusion clearly have the exact same semantic.

* $L_{\varepsilon} \cdot L \tilde{\nabla}$:

Let $\mathfrak{M}$ be a model such that $\mathfrak{M} : \mathbb{E} \models \Theta$, $(F_0 \tilde{\nabla} F_1)$.

Then $\mathfrak{M} \models \Theta, F_0$ or $\mathfrak{M} \models \Theta, F_1$.

Therefore, by the premises, $\mathfrak{M} \models [\wedge\Gamma \Rightarrow \psi]_{\varepsilon}$.

* $L_{\varepsilon} \cdot L \tilde{\perp}$:

Let $\mathfrak{M}$ be a model such that $\mathfrak{M} : \mathbb{E} \models \Theta, \tilde{\perp}$.

Then, $\mathfrak{M} \models [\wedge\Gamma \Rightarrow \psi]_{\varepsilon}$.
E. Local Judgement: Right Rules

• L<sub>ε</sub>.R-∀:

Let M be a model such that M : E ⊧ ˜V(x : τ).(∧Θ) ⇒ [(∧Γ ⇒ φ)]<sub>ε</sub>.

By Proposition 2, M : E ⊧ (∧Θ) ⇒ ˜V(x : τ).[(∧Γ ⇒ φ)]<sub>ε</sub>.

Therefore gives: M : E ⊧ (∧Θ) ⇒ [∀(x : τ).(∧Γ ⇒ φ)]<sub>ε</sub>.

Then (since x doesn't appear in Γ), M : E ⊧ (∧Θ) ⇒ [∧Γ ⇒ ∀(x : ).φ]<sub>ε</sub>.

which is exactly the conclusion

• L<sub>ε</sub>.R-∃:

Let M be a model such that M ⊧ Θ.

Let η ∈ N, ρ ∈ T<sub>M,η</sub>.

Assume that [[¬((∧Γ) ⇒ φ{x ↦→ t})]]<sub>M</sub><sup>η;ρ</sup> = 0.

Then [[∧Γ]]<sub>M</sub><sup>η,ρ</sup> = 0 and [[¬φ{x ↦→ t}]]]<sub>M</sub><sup>η,ρ</sup> = 0.

Therefore, [[¬∃(x : τ).φ]]<sub>M</sub><sup>η,ρ</sup> = 0.

So, [[¬((∧Γ) ⇒ ∃(x : τ).φ)]]]<sub>M</sub><sup>η,ρ</sup> = 0.

Finally, for every η ∈ N:

$$
\begin{align*}
& \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow \exists(x : \tau).\phi)]_{\mathbb{M}}^{\eta, \rho}) \\
\leq & \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow \phi\{x \mapsto t\})]_{\mathbb{M}}^{\eta, \rho}) \\
\leq & \mathrm{E}_{\rho} ( [\varepsilon]_{\mathbb{M}}^{\eta, \rho}).
\end{align*}
$$

• L<sub>ε</sub>.R-⇒:

Let M be a model such that M ⊧ Θ.

Let η ∈ N, ρ ∈ T<sub>M,η</sub>.

$$
[\neg(\wedge\Gamma \Rightarrow (\psi \Rightarrow \phi))]_{\mathbb{M}}^{\eta, \rho} = [\neg(\wedge\Gamma \wedge \psi \Rightarrow \phi)]_{\mathbb{M}}^{\eta, \rho}
$$

F. Local Judgement: Other Rules

• L<sub>ε</sub>.REWRITE:

Let M be a model such that M ⊧ Θ.

Let η ∈ N,

$$
\begin{align*}
& \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow \phi\{t\})]_{\mathbb{M}}^{\eta, \rho}) \\
&= \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow \phi\{t\})]_{\mathbb{M}}^{\eta, \rho} \wedge [\neg((\wedge \Gamma) \Rightarrow s = t)]_{\mathbb{M}}^{\eta, \rho} ) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow \phi\{t\})]_{\mathbb{M}}^{\eta, \rho} \wedge [\neg((\wedge \Gamma) \Rightarrow \neg(s = t))]]_{\mathbb{M}}^{\eta, \rho} ) \\
&= \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow (\phi\{t\} \wedge s = t))]]_{\mathbb{M}}^{\eta, \rho} ) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow (\phi\{t\} \wedge \neg s = t))]]_{\mathbb{M}}^{\eta, \rho} ) \\
&= \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow (\phi\{s\} \wedge s = t))]]_{\mathbb{M}}^{\eta, \rho} ) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow (\phi\{t\} \wedge \neg s = t))]]_{\mathbb{M}}^{\eta, \rho} ) \\
&\leq \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow \phi\{s\})]_{\mathbb{M}}^{\eta, \rho} ) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow \neg s = t)]_{\mathbb{M}}^{\eta, \rho} ) \\
&\leq \mathrm{E}_{\rho} ( [\varepsilon_0]_{\mathbb{M}}^{\eta, \rho} ) + \mathrm{E}_{\rho} ( [\varepsilon_1]_{\mathbb{M}}^{\eta, \rho} )
\end{align*}
$$

• L<sub>ε</sub>.AXIOM:

Let M be a model such that M ⊧ Θ, then Pr<sub>ρ∈T<sub>M,η</sub></sub> ( [¬((∧Γ ∧ φ ⇒ φ))]<sub>M</sub><sup>η,ρ</sup>) ≤ 0.

• L<sub>ε</sub>.ABSURD:

Let M be a model such that M ⊧ Θ, then:

$$
\begin{align*}
& [\neg((\wedge\Gamma) \wedge (\phi \Rightarrow \perp) \Rightarrow \perp)]_{\mathbb{M}}^{\eta, \rho} \\
= & [\neg((\wedge\Gamma) \Rightarrow (\phi \Rightarrow \perp) \Rightarrow \perp)]_{\mathbb{M}}^{\eta, \rho} \\
= & [\neg((\wedge\Gamma) \Rightarrow \neg\phi)]_{\mathbb{M}}^{\eta, \rho} \\
= & [\neg(\wedge\Gamma \Rightarrow \phi)]_{\mathbb{M}}^{\eta, \rho}.
\end{align*}
$$

• L<sub>ε</sub>.CUT-LOC:

Let M be a model such that M ⊧ Θ, then

$$
\begin{align*}
& \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( \neg[\wedge \Gamma \Rightarrow \psi]_{\mathbb{M}}^{\eta, \rho} ) \\
&= \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( \neg([\wedge \Gamma \Rightarrow \psi]_{\mathbb{M}}^{\eta, \rho} \wedge [\wedge \Gamma \Rightarrow \phi]_{\mathbb{M}}^{\eta, \rho}) ) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( \neg([\wedge \Gamma \Rightarrow \psi]_{\mathbb{M}}^{\eta, \rho} \wedge \neg[\wedge \Gamma \Rightarrow \phi]_{\mathbb{M}}^{\eta, \rho}) ) \\
&= \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( \neg([\wedge \Gamma \wedge \phi \Rightarrow \psi]_{\mathbb{M}}^{\eta, \rho} \wedge [\wedge \Gamma \Rightarrow \phi]_{\mathbb{M}}^{\eta, \rho}) ) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( \neg([\wedge \Gamma \Rightarrow \psi]_{\mathbb{M}}^{\eta, \rho} \wedge \neg([\wedge \Gamma \Rightarrow \phi]_{\mathbb{M}}^{\eta, \rho}) ) ) \\
&\leq \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( \neg([\wedge \Gamma \wedge \phi \Rightarrow \psi]_{\mathbb{M}}^{\eta, \rho}) ) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( \neg[\wedge \Gamma \Rightarrow \psi]_{\mathbb{M}}^{\eta, \rho} ) \\
&\leq \mathrm{E}_{\rho} ( [\varepsilon_0]_{\mathbb{M}}^{\eta, \rho} ) + \mathrm{E}_{\rho} ( [\varepsilon_1]_{\mathbb{M}}^{\eta, \rho} )
\end{align*}
$$
E. Local Judgement: Right Rules

• L<sub>ε</sub>.R-∀:

Let M be a model such that M : E ⊧ ˜V(x : τ).(∧Θ) ⇒ [(∧Γ ⇒ φ)]<sub>ε</sub>.

By Proposition 2, M : E ⊧ (∧Θ) ⇒ ˜V(x : τ).[(∧Γ ⇒ φ)]<sub>ε</sub>.

Therefore gives: M : E ⊧ (∧Θ) ⇒ [∀(x : τ).(∧Γ ⇒ φ)]<sub>ε</sub>.

Then (since x doesn't appear in Γ), M : E ⊧ (∧Θ) ⇒ [∧Γ ⇒ ∀(x : ).φ]<sub>ε</sub>.

which is exactly the conclusion

• L<sub>ε</sub>.R-∃:

Let M be a model such that M ⊧ Θ.

Let η ∈ N, ρ ∈ T<sub>M,η</sub>.

Assume that [[¬((∧Γ) ⇒ φ{x ↦→ t})]]<sub>M</sub><sup>η;ρ</sup> = 0.

Then [[∧Γ]]<sub>M</sub><sup>η,ρ</sup> = 0 and [[¬φ{x ↦→ t}]]]<sub>M</sub><sup>η,ρ</sup> = 0.

Therefore, [[¬∃(x : τ).φ]]<sub>M</sub><sup>η,ρ</sup> = 0.

So, [[¬((∧Γ) ⇒ ∃(x : τ).φ)]]]<sub>M</sub><sup>η,ρ</sup> = 0.

Finally, for every η ∈ N:

$$
\begin{align*}
& \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow \exists(x : \tau).\phi)]_{\mathbb{M}}^{\eta, \rho}) \\
\leq & \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow \phi\{x \mapsto t\})]_{\mathbb{M}}^{\eta, \rho}) \\
\leq & \mathrm{E}_{\rho} ( [\varepsilon]_{\mathbb{M}}^{\eta, \rho}).
\end{align*}
$$

• L<sub>ε</sub>.R-⇒:

Let M be a model such that M ⊧ Θ.

Let η ∈ N, ρ ∈ T<sub>M,η</sub>.

$$
[\neg(\wedge\Gamma \Rightarrow (\psi \Rightarrow \phi))]_{\mathbb{M}}^{\eta, \rho} = [\neg(\wedge\Gamma \wedge \psi \Rightarrow \phi)]_{\mathbb{M}}^{\eta, \rho}
$$

F. Local Judgement: Other Rules

• L<sub>ε</sub>.REWRITE:

Let M be a model such that M ⊧ Θ.

Let η ∈ N,

$$
\begin{align*}
& \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow \phi\{t\})]_{\mathbb{M}}^{\eta, \rho}) \\
&= \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow \phi\{t\})]_{\mathbb{M}}^{\eta, \rho} \wedge [\neg((\wedge \Gamma) \Rightarrow s = t)]_{\mathbb{M}}^{\eta, \rho} ) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow \phi\{t\})]_{\mathbb{M}}^{\eta, \rho} \wedge [\neg((\wedge \Gamma) \Rightarrow \neg(s = t))]]_{\mathbb{M}}^{\eta, \rho} ) \\
&= \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow (\phi\{t\} \wedge s = t))]]_{\mathbb{M}}^{\eta, \rho} ) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow (\phi\{t\} \wedge \neg s = t))]]_{\mathbb{M}}^{\eta, \rho} ) \\
&= \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow (\phi\{s\} \wedge s = t))]]_{\mathbb{M}}^{\eta, \rho} ) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow (\phi\{t\} \wedge \neg s = t))]]_{\mathbb{M}}^{\eta, \rho} ) \\
&\leq \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow \phi\{s\})]_{\mathbb{M}}^{\eta, \rho} ) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( [\neg((\wedge \Gamma) \Rightarrow \neg s = t)]_{\mathbb{M}}^{\eta, \rho} ) \\
&\leq \mathrm{E}_{\rho} ( [\varepsilon_0]_{\mathbb{M}}^{\eta, \rho} ) + \mathrm{E}_{\rho} ( [\varepsilon_1]_{\mathbb{M}}^{\eta, \rho} )
\end{align*}
$$

• L<sub>ε</sub>.AXIOM:

Let M be a model such that M ⊧ Θ, then Pr<sub>ρ ∈ T<sub>M,η</sub></sub> ( [¬((∧Γ ∧ φ ⇒ φ))]<sub>M</sub><sup>η,ρ</sup>) ≤ 0.

• L<sub>ε</sub>.ABSURD:

Let M be a model such that M ⊧ Θ, then:

$$
\begin{align*}
& [\neg((\wedge\Gamma) \wedge (\phi \Rightarrow \perp) \Rightarrow \perp)]_{\mathbb{M}}^{\eta, \rho} \\
= & [\neg((\wedge\Gamma) \Rightarrow (\phi \Rightarrow \perp) \Rightarrow \perp)]_{\mathbb{M}}^{\eta, \rho} \\
= & [\neg((\wedge\Gamma) \Rightarrow \neg\phi)]_{\mathbb{M}}^{\eta, \rho} \\
= & [\neg(\wedge\Gamma \Rightarrow \phi)]_{\mathbb{M}}^{\eta, \rho}.
\end{align*}
$$

• L<sub>ε</sub>.CUT-LOC:

Let M be a model such that M ⊧ Θ, then

$$
\begin{align*}
& \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( \neg[\wedge \Gamma \Rightarrow \psi]_{\mathbb{M}}^{\eta, \rho} ) \\
&= \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( \neg([\wedge \Gamma \Rightarrow \psi]_{\mathbb{M}}^{\eta, \rho} \wedge [\wedge \Gamma \Rightarrow \phi]_{\mathbb{M}}^{\eta, \rho}) ) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( \neg([\wedge \Gamma \Rightarrow \psi]_{\mathbb{M}}^{\eta, \rho} \wedge \neg[\wedge \Gamma \Rightarrow \phi]_{\mathbb{M}}^{\eta, \rho}) ) \\
&= \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( \neg([\wedge \Gamma \wedge \phi \Rightarrow \psi]_{\mathbb{M}}^{\eta, \rho} \wedge [\wedge \Gamma \Rightarrow \phi]_{\mathbb{M}}^{\eta, \rho}) ) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( \neg([\wedge \Gamma \Rightarrow \psi]_{\mathbb{M}}^{\eta, \rho} \wedge \neg([\wedge \Gamma \Rightarrow \phi]_{\mathbb{M}}^{\eta, \rho}) ) ) \\
&\leq \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( \neg([\wedge \Gamma \wedge \phi \Rightarrow \psi]_{\mathbb{M}}^{\eta, \rho}) ) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ( \neg[\wedge \Gamma \Rightarrow \psi]_{\mathbb{M}}^{\eta, \rho} ) \\
&\leq \mathrm{E}_{\rho} ( [\varepsilon_0]_{\mathbb{M}}^{\eta, \rho} ) + \mathrm{E}_{\rho} ( [\varepsilon_1]_{\mathbb{M}}^{\eta, \rho} )
\end{align*}
$$
• L<sub>ε</sub>.CUT-GLOB:

Let M be a model such that M |=$\Theta$, then by the first premise, M |=$F$. Therefore $Pr_{\rho \in T_{M,\eta}} (\neg [[\Lambda \Gamma \Rightarrow \psi]]_{M}^{\eta,\rho}) \le E_{\rho}([\varepsilon]_{M}^{\eta,\rho})$

• L<sub>ε</sub>.WEAK:

Let M be a model such that M |=$\Theta_0, \Theta_1$, then M |=$\Theta_0$. Therefore:

$$
\mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\wedge \Gamma_0 \Gamma_1 \Rightarrow \phi]]_{\mathbb{M}}^{\eta, \rho}) \leq \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\wedge \Gamma_0 \Rightarrow \phi]]_{\mathbb{M}}^{\eta, \rho}) \leq E_{\rho}([\varepsilon]_{\mathbb{M}}^{\eta, \rho}).
$$

G. Local Judgement: ε Weakening Rules

• L<sub>ε</sub>.WEAK<sub>0</sub>:

Let M be a model such that M |=$\Theta$, then $Pr_{\rho \in T_{M,\eta}} (\neg [[\varepsilon \le \varepsilon']_{M}^{\eta,\rho}]) \le 0$ by the second premise, and since for every $\eta \in \mathbb{N}$, we have that $T_{M,\eta}$ are finite, and we use the uniform metric, this is equivalent to:

$$
\forall \eta \in \mathbb{N}, \forall \rho \in T_{M,\eta}, [[\varepsilon]_{M}^{\eta,\rho} \leq [[\varepsilon']_{M}^{\eta,\rho}}
$$

Thus:

$$
\mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\wedge \Gamma \Rightarrow \phi]]_{\mathbb{M}}^{\eta, \rho}) \leq \mathrm{E}_{\rho}([\varepsilon]_{\mathbb{M}}^{\eta, \rho}) \leq \mathrm{E}_{\rho}([\varepsilon']_{\mathbb{M}}^{\eta, \rho}).
$$

• L<sub>ε</sub>.WEAK<sub>ε</sub>:

Let M be a model such that M |=$\Theta$, then $\forall \eta \in \mathbb{N}, \forall \rho \in T_{M,\eta}, \varepsilon_0 \le 1$ by the third premise. Then, for every $\eta \in \mathbb{N}$,

$$
\begin{align*}
& \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\wedge \Gamma \Rightarrow \phi]]_{\mathbb{M}}^{\eta, \rho}) \\
\leq & \mathrm{E}_{\rho}([\varepsilon]_{\mathbb{M}}^{\eta, \rho}) + \mathrm{E}_{\rho}([\varepsilon_0]_{\mathbb{M}}^{\eta, \rho}) \\
\leq & \mathrm{E}_{\rho}([\varepsilon]_{\mathbb{M}}^{\eta, \rho}) + \mathrm{E}_{\rho}([\varepsilon_0]_{\mathbb{M}}^{\eta, \rho} 1_{[[\varepsilon_0 \le \varepsilon'_0]]_{\mathbb{M}}^{\eta, \rho}}) + \mathrm{E}_{\rho}([\varepsilon_0]_{\mathbb{M}}^{\eta, \rho} 1_{[[\varepsilon_0 \le \varepsilon'_0]]_{\mathbb{M}}^{\eta, \rho}}) \\
\leq & \mathrm{E}_{\rho}([\varepsilon]_{\mathbb{M}}^{\eta, \rho}) + \mathrm{E}_{\rho}([\varepsilon'_0]_{\mathbb{M}}^{\eta, \rho} 1_{[[\varepsilon_0 \le \varepsilon'_0]]_{\mathbb{M}}^{\eta, \rho}}) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} ([\varepsilon_0 \le \varepsilon'_0]_{\mathbb{M}}^{\eta, \rho}) \\
\leq & \mathrm{E}_{\rho}([\varepsilon]_{\mathbb{M}}^{\eta, \rho}) + \mathrm{E}_{\rho}([\varepsilon'_0]_{\mathbb{M}}^{\eta, \rho}) + \mathrm{E}_{\rho}([\varepsilon_1]_{\mathbb{M}}^{\eta, \rho}) \\
\leq & \mathrm{E}_{\rho}([\varepsilon + \varepsilon'_0 + \varepsilon_1]_{\mathbb{M}}^{\eta, \rho})
\end{align*}
$$

H. Mixed Judgement Rules

• L<sub>ε</sub>.BYGLOB and G<sub>ε</sub>.BYLOC:

The premise and the conclusion have the exact same semantic.

• L<sub>ε</sub>.LOCALISE:

Let M be a model such that M |=$\Theta$, $[\phi]_{\varepsilon_1}$, then $Pr_{\rho \in T_{M,\eta}} (\neg [[\phi]]_{M}^{\eta,\rho}) \le E_{\rho}([\varepsilon_1]_{M}^{\eta,\rho})$ and since, M |=$\Theta$ by the premise,
$Pr_{\rho \in T_{M,\eta}} (\neg [[\Lambda \Gamma \wedge \phi \Rightarrow \psi]]_{M}^{\eta,\rho}) \le E_{\rho}(\varepsilon_0)$.

Therefore,

$$
\begin{align*}
\mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\wedge \Gamma \Rightarrow \psi]]_{\mathbb{M}}^{\eta, \rho}) \\
&= \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\wedge \Gamma \Rightarrow \psi]]_{\mathbb{M}}^{\eta, \rho} \wedge [[\phi]]_{\mathbb{M}}^{\eta, \rho}) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\wedge \Gamma \Rightarrow \psi]]_{\mathbb{M}}^{\eta, \rho} \wedge \neg [[\phi]]_{\mathbb{M}}^{\eta, \rho}) \\
&\le \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\wedge \Gamma \wedge \phi \Rightarrow \psi]]_{\mathbb{M}}^{\eta, \rho}) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\phi]]_{\mathbb{M}}^{\eta, \rho}) \\
&\le E_{\rho}([\varepsilon_0]_{\mathbb{M}}^{\eta, \rho}) + E_{\rho}([\varepsilon_1]_{\mathbb{M}}^{\eta, \rho})
\end{align*}
$$

• L<sub>ε</sub>.REWRITE-EQUIV:

Let M be a model such that M |=$\Theta$. Since the adversary $A_{bool}$, that get a boolean as input, and send back the opposite boolean, is a adversary against the equivalence in the second premise in time 1. Then,

$$
| \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\wedge \Gamma_0 \Rightarrow \phi_0]]_{\mathbb{M}}^{\eta, \rho}) - \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\wedge \Gamma_1 \Rightarrow \phi_1]]_{\mathbb{M}}^{\eta, \rho}) | \leq \mathrm{E}_{\rho}([\varepsilon_0]_{\mathbb{M}}^{\eta, \rho}) (1).
$$

Therefore,

$$
\begin{align*}
& \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\wedge \Gamma_0 \Rightarrow \phi_0]]_{\mathbb{M}}^{\eta, \rho}) \\
&= \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\wedge \Gamma_0 \Rightarrow \phi_0]]_{\mathbb{M}}^{\eta, \rho}) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\wedge \Gamma_1 \Rightarrow \phi_1]]_{\mathbb{M}}^{\eta, \rho}) - \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\wedge \Gamma_1 \Rightarrow \phi_1]]_{\mathbb{M}}^{\eta, \rho}) \\
&\le \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\wedge \Gamma_1 \Rightarrow \phi_1]]_{\mathbb{M}}^{\eta, \rho}) + |\mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\wedge \Gamma_0 \Rightarrow \phi_0]]_{\mathbb{M}}^{\eta, \rho}) - \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [[\wedge \Gamma_1 \Rightarrow \phi_0]]_{\mathbb{M}}^{\eta, \rho})| \\
&\le E_{\rho}([\varepsilon_1]_{\mathbb{M}}^{\eta, \rho}) + E_{\rho}([\varepsilon_0(1)]_{\mathbb{M}}^{\eta, \rho}).
\end{align*}
$$

I. Global Judgement: Left and Right Rules

We omit the proofs of the left and right rules for the global judgements, as they are standard.
• L<sub>ε</sub>.CUT-GLOB:

Let M be a model such that M |=$\Theta$, then by the first premise, M |=$F$. Therefore $\mathrm{Pr}_{\rho \in T_{M,\eta}} (\neg [\wedge \Gamma \Rightarrow \psi]_M^{\eta,\rho}) \leq \mathrm{E}_{\rho}([\varepsilon]_M^{\eta,\rho})$

• L<sub>ε</sub>.WEAK:

Let M be a model such that M |=$\Theta_0, \Theta_1$, then M |=$\Theta_0$. Therefore:

$$
\mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [\wedge \Gamma_0 \Gamma_1 \Rightarrow \phi]_M^{\eta, \rho}) \leq \mathrm{Pr}_{\rho \in \mathbb{T}_{M, \eta}} (\neg [\wedge \Gamma_0 \Rightarrow \phi]_M^{\eta, \rho}) \leq \mathrm{E}_{\rho}([\varepsilon]_M^{\eta, \rho}).
$$

G. Local Judgement: ε Weakening Rules

• L<sub>ε</sub>.WEAK<sub>0</sub>:

Let M be a model such that M |=$\Theta$, then $\mathrm{Pr}_{\rho \in T_{M,\eta}} (\neg [[\varepsilon \leq \varepsilon']_M^{\eta,\rho}]) \leq 0$ by the second premise, and since for every $\eta \in \mathbb{N}$, we have that $T_{M,\eta}$ are finite, and we use the uniform metric, this is equivalent to:

$$
\forall \eta \in \mathbb{N}, \forall \rho \in T_{M, \eta}, [[\varepsilon]_M^{\eta, \rho} \leq [[\varepsilon']_M^{\eta, \rho}}
$$

Thus:

$$
\mathrm{Pr}_{\rho \in T_{M, \eta}} (\neg [\wedge \Gamma \Rightarrow \phi]_M^{\eta, \rho}) \leq \mathrm{E}_{\rho}([\varepsilon]_M^{\eta, \rho}) \leq \mathrm{E}_{\rho}([\varepsilon']_M^{\eta, \rho}).
$$

• L<sub>ε</sub>.WEAK<sub>ε</sub>:

Let M be a model such that M |=$\Theta$, then $\forall \eta \in \mathbb{N}, \forall \rho \in T_{M,\eta}, \varepsilon_0 \le 1$ by the third premise. Then, for every $\eta \in \mathbb{N}$,

$$
\begin{align*}
& \mathrm{Pr}_{\rho \in T_{M, \eta}} (\neg [\wedge \Gamma \Rightarrow \phi]_M^{\eta, \rho}) \\
\leq & \mathrm{E}_{\rho}([\varepsilon]_M^{\eta, \rho}) + \mathrm{E}_{\rho}([\varepsilon_0]_M^{\eta, \rho}) \\
\leq & \mathrm{E}_{\rho}([\varepsilon]_M^{\eta, \rho}) + \mathrm{E}_{\rho}([\varepsilon_0]_M^{\eta, \rho} 1_{[\varepsilon_0 \le \varepsilon'_0]_M^{\eta, \rho}}) + \mathrm{E}_{\rho}([\varepsilon_0]_M^{\eta, \rho} 1_{[\varepsilon_0 \le \varepsilon'_0]_M^{\eta, \rho}}) \\
\leq & \mathrm{E}_{\rho}([\varepsilon]_M^{\eta, \rho}) + \mathrm{E}_{\rho}([\varepsilon'_0]_M^{\eta, \rho} 1_{[\varepsilon_0 \le \varepsilon'_0]_M^{\eta, \rho}}) + \mathrm{Pr}_{\rho \in T_{M, \eta}} ([\varepsilon_0 \le \varepsilon'_0]_M^{\eta, \rho}) \\
\leq & \mathrm{E}_{\rho}([\varepsilon]_M^{\eta, \rho}) + \mathrm{E}_{\rho}([\varepsilon'_0]_M^{\eta, \rho}) + \mathrm{E}_{\rho}([\varepsilon_1]_M^{\eta, \rho}) \\
\leq & \mathrm{E}_{\rho}([\varepsilon + \varepsilon'_0 + \varepsilon_1]_M^{\eta, \rho})
\end{align*}
$$

H. Mixed Judgement Rules

• L<sub>ε</sub>.BYGLOB and G<sub>ε</sub>.BYLOC:

The premise and the conclusion have the exact same semantic.

• L<sub>ε</sub>.LOCALISE:

Let M be a model such that M |=$\Theta$, $[\phi]_{\varepsilon_1}$, then $\mathrm{Pr}_{\rho \in T_{M,\eta}} (\neg [\phi]_M^{\eta,\rho}) \leq \mathrm{E}_{\rho}([\varepsilon_1]_M^{\eta,\rho})$ and since, M |=$\Theta$ by the premise, $\mathrm{Pr}_{\rho \in T_{M,\eta}} (\neg [\wedge \Gamma \wedge \phi \Rightarrow \psi]_M^{\eta,\rho}) \leq \mathrm{E}_{\rho}(\varepsilon_0)$.

Therefore,

$$
\begin{align*}
\mathrm{Pr}_{\rho \in T_{M, \eta}} (\neg [\wedge \Gamma \Rightarrow \psi]_M^{\eta, \rho}) \\
&= \mathrm{Pr}_{\rho \in T_{M, \eta}} (\neg [\wedge \Gamma \Rightarrow \psi]_M^{\eta, \rho} \wedge [\phi]_M^{\eta, \rho}) + \mathrm{Pr}_{\rho \in T_{M, \eta}} (\neg [\wedge \Gamma \Rightarrow \psi]_M^{\eta, \rho} \wedge \neg [\phi]_M^{\eta, \rho}) \\
&\leq \mathrm{Pr}_{\rho \in T_{M, \eta}} (\neg [\wedge \Gamma \wedge \phi \Rightarrow \psi]_M^{\eta, \rho}) + \mathrm{Pr}_{\rho \in T_{M, \eta}} (\neg [\phi]_M^{\eta, \rho}) \\
&\leq \mathrm{E}_{\rho}([\varepsilon_0]_M^{\eta, \rho}) + \mathrm{E}_{\rho}([\varepsilon_1]_M^{\eta, \rho})
\end{align*}
$$

• L<sub>ε</sub>.REWRITE-EQUIV:

Let M be a model such that M |=$\Theta$. Since the adversary $\mathcal{A}_{bool}$, that get a boolean as input, and send back the opposite boolean, is a adversary against the equivalence in the second premise in time 1. Then,

$$
|\mathrm{Pr}_{\rho \in T_{M, \eta}} (\neg [\wedge \Gamma_0 \Rightarrow \phi_0]_M^{\eta, \rho}) - \mathrm{Pr}_{\rho \in T_{M, \eta}} (\neg [\wedge \Gamma_1 \Rightarrow \phi_1]_M^{\eta, \rho})| \leq \mathrm{E}_{\rho}([\varepsilon_0]_M^{\eta, \rho}) (1).
$$

Therefore,

$$
\begin{align*}
& \mathrm{Pr}_{\rho \in T_{M, \eta}} (\neg [\wedge \Gamma_0 \Rightarrow \phi_0]_M^{\eta, \rho}) \\
&= \mathrm{Pr}_{\rho \in T_{M, \eta}} (\neg [\wedge \Gamma_0 \Rightarrow \phi_0]_M^{\eta, \rho}) + \mathrm{Pr}_{\rho \in T_{M, \eta}} (\neg [\wedge \Gamma_1 \Rightarrow \phi_1]_M^{\eta, \rho}) - \mathrm{Pr}_{\rho \in T_{M, \eta}} (\neg [\wedge \Gamma_1 \Rightarrow \phi_1]_M^{\eta, \rho}) \\
&\leq \mathrm{Pr}_{\rho \in T_{M, \eta}} (\neg [\wedge \Gamma_1 \Rightarrow \phi_1]_M^{\eta, \rho}) + |\mathrm{Pr}_{\rho \in T_{M, \eta}} (\neg [\wedge \Gamma_0 \Rightarrow \phi_0]_M^{\eta, \rho}) - \mathrm{Pr}_{\rho \in T_{M, \eta}} (\neg [\wedge \Gamma_1 \Rightarrow \phi_0]_M^{\eta, \rho})| \\
&\leq \mathrm{E}_{\rho}([\varepsilon_1]_M^{\eta, \rho}) + \mathrm{E}_{\rho}([\varepsilon_0(1)]_M^{\eta, \rho}).
\end{align*}
$$

I. Global Judgement: Left and Right Rules

We omit the proofs of the left and right rules for the global judgements, as they are standard.
All those rules could be deduced from the case analysis on boolean rules
$\frac{\text{const}(\phi)}{[\phi]_0 \tilde{\lor} [\neg\phi]_0}$ and the other rules. (As well, as their
right counterpart that we omit.)

• G<sub>ε</sub>.L-LOC: ⇒:

Let $\mathcal{M}$ a model such that $\mathcal{M} \models \Theta$.

By the second premise, there exists $c \in \cap_{\eta \in \mathbb{N}} [[\mathbf{bool}]_{\mathcal{M}}^{\eta} = \{0, 1\}]$ such that $\forall \eta \in \mathbb{N}, \forall \rho \in \mathbb{T}_{\mathcal{M}, \eta}, [[\phi]_{\mathcal{M}}]^{\eta; \rho} = c$ Then,
by case disjonction:

- case c = 0: For every $\eta \in \mathbb{N}$, $\mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\phi]]_{\mathcal{M}}^{\eta, \rho}) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\top) = 1$

Therefore, $\mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\phi]]_{\mathcal{M}}^{\eta, \rho}) \le 0 \Rightarrow \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg) \le \mathrm{E}_{\rho}([\varepsilon]_{\mathcal{M}}^{\eta, \rho})$ holds

i.e $\mathcal{M} \models [\phi]_0 \Rightarrow [\psi]_0$.

And, by the first premise, $\mathcal{M} \models F$.

- case c = 1: We want to show that $\mathcal{M} \models [\phi \Rightarrow \psi]_{\varepsilon} \dashv F$. So assuming that $\mathcal{M} \models [\phi \Rightarrow \psi]_{\varepsilon}$, let's show that $\mathcal{M} \models F$.

For every $\eta \in \mathbb{N}$, we have $\mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\phi \Rightarrow \psi]]_{\mathcal{M}}^{\eta, \rho}) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} ([[\psi]]_{\mathcal{M}}^{\eta, \rho}) \le \mathrm{E}_{\rho}([\varepsilon]_{\mathcal{M}}^{\eta, \rho})$.

Therefore, $\mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\phi]]_{\mathcal{M}}^{\eta, \rho}) \le 0 \Rightarrow \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\psi]]_{\mathcal{M}}^{\eta, \rho}) \le \mathrm{E}_{\rho}([\varepsilon]_{\mathcal{M}}^{\eta, \rho})$ holds

i.e $\mathcal{M} \models [\phi]_0 \Rightarrow [\psi]_{\varepsilon}$.

And, by the first premise, $\mathcal{M} \models F$.

• G<sub>ε</sub>.L-LOC: V:

Let $\mathcal{M}$ a model such that $\mathcal{M} \models \Theta$.

By the third premise, there exists $c \in \cap_{\eta \in \mathbb{N}} [[\mathbf{bool}]_{\mathcal{M}}^{\eta} = \{0, 1\}]$ such that $\forall \eta \in \mathbb{N}, \forall \rho \in \mathbb{T}_{\mathcal{M}, \eta}, [[\phi]]_{\mathcal{M}}^{\eta; \rho} = c$ (by symmetry of $\psi$ and $\phi$ here, we can only consider the case where const$(\phi)$ holds).

We want to show that $\mathcal{M} \models [\phi \lor \psi]_{\varepsilon} \dashv F$. Therefore, we assume $\mathcal{M} \models [\phi \lor \psi]_{\varepsilon}$. Then, by case disjonction:

- case c = 0: For every $\eta \in \mathbb{N}$,

$\mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\mathrm{psi}]]_{\mathcal{M}}^{\eta; \rho}) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg[\phi \land \neg\psi]_{\mathcal{M}}^{\eta; \rho}) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\phi \lor \psi]]_{\mathcal{M}}^{\eta; \rho}) \le \mathrm{E}_{\rho}([\varepsilon]_{\mathcal{M}}^{\eta; \rho})$ holds

i.e $\mathcal{M} \models [\psi]_{\varepsilon}$

And, by the second premise, $\mathcal{M} \models F$

- case c = 1: For every $\eta \in \mathbb{N}$,

Therefore, $\mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\phi]]_{\mathcal{M}}^{\eta, \rho}) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\bot) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg[\phi \land \neg\psi]_{\mathcal{M}}^{\eta, \rho}) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\phi \lor \psi]]_{\mathcal{M}}^{\eta, \rho}) \le \mathrm{E}_{\rho}([\varepsilon]_{\mathcal{M}}^{\eta, \rho})$

holds

i.e $\mathcal{M} \models [\phi]_{ve}$

And, by the first premise, $\mathcal{M} \models F$

• G<sub>ε</sub>.L-Ψ-∀ and G<sub>ε</sub>.L-∀-Ψ:

Direct by Proposition 2

• G<sub>ε</sub>.L-LOC: ∀:

Let $\mathcal{M}$ a model such that $\mathcal{M} \models \Theta$.

We want to prove that $\mathcal{M} \models [\forall (x : \tau) . \psi]_{\varepsilon} \dashv F$.

Then, we can assume $\mathcal{M} \models [\forall (x : \tau) . \psi]_{\varepsilon}$ to prove $\mathcal{M} \models F$

Which imply by Proposition 2, $\mathcal{M} \models \forall (x : \tau) . [\psi]_{\varepsilon}$

Therefore, in particular, $\mathcal{M} \models [\psi]_{\varepsilon} \{x \mapsto u\}$ since $\mathbb{E} \vdash u : \tau$.

And since, $x$ cannot appear in $\varepsilon, \mathcal{M} \models [\psi \{x \mapsto u\}]_{\varepsilon}$

Finally, by the premise, $\mathcal{M} \models F$.

• G<sub>ε</sub>.L-LOC: ∧:

Let $\mathcal{M}$ a model such that $\mathcal{M} \models \Theta$.

We want to prove that $\mathcal{M} \models [\psi \land \phi]_{\varepsilon} \dashv F$.

Then, we can assume $\mathcal{M} \models [\psi \land \phi]_{\varepsilon}$ to prove $\mathcal{M} \models F$

Therefore we have that, for every $\eta \in \mathbb{N}$,

$$
\mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\psi]]_{\mathcal{M}}^{\eta, \rho}) \leq \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg[\neg\psi \lor \neg\phi]_{\mathcal{M}}^{\eta, \rho}) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\psi \land \phi]]_{\mathcal{M}}^{\eta, \rho}) \leq \mathrm{E}_{\rho}([\varepsilon]_{\mathcal{M}}^{\eta, \rho})
$$

and

$$
\mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\phi]]_{\mathcal{M}}^{\eta, \rho}) \leq \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg[\neg\psi \lor \neg\phi]_{\mathcal{M}}^{\eta, \rho}) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\psi \land \phi]]_{\mathcal{M}}^{\eta, \rho}) \leq \mathrm{E}_{\rho}([\varepsilon]_{\mathcal{M}}^{\eta, \rho})
$$

So, $\mathcal{M} \models [\phi]_{\varepsilon}, [\psi]_{\varepsilon}$.

Then, by the premise, $\mathcal{M} \models F$.

• G<sub>ε</sub>.L-LOC: ⊥:

Let $\mathcal{M}$ a model such that $\mathcal{M} \models \Theta$.
All those rules could be deduced from the case analysis on boolean rules
$\frac{\text{const}(\phi)}{[\phi]_0 \tilde{\lor} [\neg\phi]_0}$ and the other rules. (As well, as their
right counterpart that we omit.)

• G<sub>ε</sub>.L-LOC:⇔:

Let $\mathcal{M}$ a model such that $\mathcal{M} \models \Theta$.

By the second premise, there exists $c \in \cap_{\eta \in \mathbb{N}} [[\mathbf{bool}]_{\mathcal{M}}^{\eta} = \{0, 1\}]$ such that $\forall \eta \in \mathbb{N}, \forall \rho \in \mathbb{T}_{\mathcal{M}, \eta}, [[\phi]]_{\mathcal{M}}^{\eta, \rho} = c$ Then,
by case disjonction:

- case c = 0: For every $\eta \in \mathbb{N}$, $\mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\phi]]_{\mathcal{M}}^{\eta, \rho}) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\top) = 1$
Therefore, $\mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\phi]]_{\mathcal{M}}^{\eta, \rho}) \le 0 \Rightarrow \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg) \le \mathrm{E}_{\rho}([\varepsilon]]_{\mathcal{M}}^{\eta, \rho})$ holds
i.e $\mathcal{M} \models [\phi]_0 \Rightarrow [\psi]_0$.
And, by the first premise, $\mathcal{M} \models F$.

- case c = 1: We want to show that $\mathcal{M} \models [\phi \Rightarrow \psi]_{\varepsilon} \Vdash F$. So assuming that $\mathcal{M} \models [\phi \Rightarrow \psi]_{\varepsilon}$, let's show that $\mathcal{M} \models F$. For every $\eta \in \mathbb{N}$, we have $\mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\phi \Rightarrow \psi]]_{\mathcal{M}}^{\eta, \rho}) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} ([[\psi]]_{\mathcal{M}}^{\eta, \rho}) \le \mathrm{E}_{\rho}([\varepsilon]]_{\mathcal{M}}^{\eta, \rho})$. Therefore, $\mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\phi]]_{\mathcal{M}}^{\eta, \rho}) \le 0 \Rightarrow \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\psi]]_{\mathcal{M}}^{\eta, \rho}) \le \mathrm{E}_{\rho}([\varepsilon]]_{\mathcal{M}}^{\eta, \rho})$ holds i.e $\mathcal{M} \models [\phi]_0 \Rightarrow [\psi]_{\varepsilon}$. And, by the first premise, $\mathcal{M} \models F$.

• G<sub>ε</sub>.L-LOC:V:

Let $\mathcal{M}$ a model such that $\mathcal{M} \models \Theta$.

By the third premise, there exists $c \in \cap_{\eta \in \mathbb{N}} [[\mathbf{bool}]_{\mathcal{M}}^{\eta} = \{0, 1\}]$ such that $\forall \eta \in \mathbb{N}, \forall \rho \in \mathbb{T}_{\mathcal{M}, \eta}, [[\phi]]_{\mathcal{M}}^{\eta, \rho} = c$ (by symmetry of $\psi$ and $\phi$ here, we can only consider the case where const($\phi$) holds).

We want to show that $\mathcal{M} \models [\phi \lor \psi]_{\varepsilon} \Vdash F$. Therefore, we assume $\mathcal{M} \models [\phi \lor \psi]_{\varepsilon}$. Then, by case disjonction:

- case c = 0: For every $\eta \in \mathbb{N}$,
  $\mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\mathrm{psi}]]_{\mathcal{M}}^{\eta, \rho}) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (([\neg\phi \land \neg\psi]]_{\mathcal{M}}^{\eta, \rho}) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\phi \lor \psi]]_{\mathcal{M}}^{\eta, \rho}) \le \mathrm{E}_{\rho}([\varepsilon]]_{\mathcal{M}}^{\eta, \rho})$ holds
  i.e $\mathcal{M} \models [\psi]_{\varepsilon}$
  And, by the second premise, $\mathcal{M} \models F$

- case c = 1: For every $\eta \in \mathbb{N}$,
  Therefore, $\mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\phi]]_{\mathcal{M}}^{\eta, \rho}) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\bot) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (([\neg\phi \land \neg\psi]]_{\mathcal{M}}^{\eta, \rho}) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\phi \lor \psi]]_{\mathcal{M}}^{\eta, \rho}) \le \mathrm{E}_{\rho}([\varepsilon]]_{\mathcal{M}}^{\eta, \rho})$ holds
  i.e $\mathcal{M} \models [\phi]_{ve}$
  And, by the first premise, $\mathcal{M} \models F$

• G<sub>ε</sub>.L-Ψ-∀ and G<sub>ε</sub>.L-∀-Ψ:

Direct by Proposition 2

• G<sub>ε</sub>.L-LOC:∀:

Let $\mathcal{M}$ a model such that $\mathcal{M} \models \Theta$.
We want to prove that $\mathcal{M} \models [\forall (x : \tau) . \psi]_{\varepsilon} \Vdash F$.
Then, we can assume $\mathcal{M} \models [\forall (x : \tau) . \psi]_{\varepsilon}$ to prove $\mathcal{M} \models F$
Which imply by Proposition 2, $\mathcal{M} \models \forall (x : \tau) . [\psi]_{\varepsilon}$
Therefore, in particular, $\mathcal{M} \models [\psi]_{\varepsilon} \{x \mapsto u\}$ since $E \vdash u : \tau$.
And since, $x$ cannot appear in $\varepsilon, \mathcal{M} \models [\psi \{x \mapsto u\}]_{\varepsilon}$
Finally, by the premise, $\mathcal{M} \models F$.

• G<sub>ε</sub>.L-LOC:∧:

Let $\mathcal{M}$ a model such that $\mathcal{M} \models \Theta$.
We want to prove that $\mathcal{M} \models [\psi \wedge \phi]_{\varepsilon} \Vdash F$.
Then, we can assume $\mathcal{M} \models [\psi \wedge \phi]_{\varepsilon}$ to prove $\mathcal{M} \models F$
Therefore we have that, for every $\eta \in \mathbb{N}$,

$$
\mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\psi]]_{\mathcal{M}}^{\eta, \rho}) \leq \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (([\neg \psi \lor \neg \phi]]_{\mathcal{M}}^{\eta, \rho}) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\psi \wedge \phi]]_{\mathcal{M}}^{\eta, \rho}) \leq \mathrm{E}_{\rho}([\varepsilon]]_{\mathcal{M}}^{\eta, \rho})
$$

and

$$
\mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\phi]]_{\mathcal{M}}^{\eta, \rho}) \leq \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (([\neg \psi \lor \neg \phi]]_{\mathcal{M}}^{\eta, \rho}) = \mathrm{Pr}_{\rho \in \mathbb{T}_{\mathcal{M}, \eta}} (\neg [[\psi \wedge \phi]]_{\mathcal{M}}^{\eta, \rho}) \leq \mathrm{E}_{\rho}([\varepsilon]]_{\mathcal{M}}^{\eta, \rho})
$$

So, $\mathcal{M} \models [\phi]_{\varepsilon}, [\psi]_{\varepsilon}$.
Then, by the premise, $\mathcal{M} \models F$.

• G<sub>ε</sub>.L-LOC:⊥:

Let $\mathcal{M}$ a model such that $\mathcal{M} \models \Theta$.
For every $\eta \in \mathbb{N}$, we have $\mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} (\neg [\perp]_M^{\eta,\rho}) = \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} (\top) = 1$.
Therefore, $\mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} (\neg [\perp]_M^{\eta,\rho}) \le 0 \Rightarrow \mathbf{F}$ holds. i.e $\mathbf{M} \models [\perp]_0 \Rightarrow \mathbf{F}$.

### K. Global Judgement: $\varepsilon$-Weakening Rules

* **$G_\varepsilon$. REACH:$\varepsilon$-WEAK$_0$:**

This rule can be deduced by some other rules $L_\varepsilon$. BYGLOB, $G_\varepsilon$. BYLOC and $L_\varepsilon$. WEAK$_0$.

* **$G_\varepsilon$. REACH:$\varepsilon$-WEAK$_0$:**

This rule can be deduced by some other rules $L_\varepsilon$. BYGLOB, $G_\varepsilon$. BYLOC and $L_\varepsilon$. WEAK$_\varepsilon$.

* **$G_\varepsilon$.E:$\varepsilon$-WEAK$_0$:**

Let $\mathbf{M}$ be a model such that $\mathbf{M} \models \Theta$.

By the first premise, we have that $\forall \eta \in \mathbb{N}, \forall \rho \in \mathbb{T}_{M,\eta}, \varepsilon \le \varepsilon'$. where $\le$ is the pointwise order on function.

Let $\eta \in \mathbb{N}$, Let $\mathcal{A}$ be a attacker against the game $(\vec{u}, \vec{v})$. we denote $\vec{u} = \vec{u}_0, \vec{u}_1$ for the term of order 0 and 1 in $\vec{u}$. (And we do the same for $\vec{v}$) Then, by the second premise,

$$ \left| \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} \left( \mathcal{A}[\vec{u}_1]_M^{\eta,\rho} (1^{\eta}, [\vec{u}_0]_M^{\eta,\rho}, \rho_a) \right) - \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} \left( \mathcal{A}[\vec{v}_1]_M^{\eta,\rho} (1^{\eta}, [\vec{v}_0]_M^{\eta,\rho}, \rho_a) \right) \right| \le \mathrm{E}_{\rho} (\llbracket \varepsilon \rrbracket_M^{\eta,\rho} (\mathrm{time}_{\mathcal{A}}^{\eta}, \mathrm{calls}_{\mathcal{A}}^{\eta})) $$

Therefore, we have:

$$ \left| \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} \left( \mathcal{A}[\vec{u}_1]_M^{\eta,\rho} (1^{\eta}, [\vec{u}_0]_M^{\eta,\rho}, \rho_a) \right) - \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} \left( \mathcal{A}[\vec{v}_1]_M^{\eta,\rho} (1^{\eta}, [\vec{v}_0]_M^{\eta,\rho}, \rho_a) \right) \right| \le \mathrm{E}_{\rho} (\llbracket \varepsilon' \rrbracket_M^{\eta,\rho} (\mathrm{time}_{\mathcal{A}}^{\eta}, \mathrm{calls}_{\mathcal{A}}^{\eta})). $$

So, $\mathbf{M} \models \vec{u} \sim_{\varepsilon'} \vec{v}$

* **$G_\varepsilon$.E:$\varepsilon$-WEAK$_0$:**

Let $\mathbf{M}$ be a model such that $\mathbf{M} \models \Theta$.

By the third premise, we have that $\forall \eta \in \mathbb{N}, \forall \rho \in \mathbb{T}_{M,\eta}, \varepsilon \le 1'$. where $\le$ is the pointwise order on function.

By the second premise, we have that $\forall \eta \in \mathbb{N}, \forall \rho \text{ Let } \eta \in \mathbb{N}, \text{ Let } \mathcal{A} \text{ be a attacker against the game } (\vec{u}, \vec{v})$. we denote $\vec{u} = \vec{u}_0, \vec{u}_1$ for the term of order 0 and 1 in $\vec{u}$. (And we do the same for $\vec{v}$).

Then, by the first premise,

$$ \left| \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} \left( \mathcal{A}[\vec{u}_1]_M^{\eta,\rho} (1^{\eta}, [\vec{u}_0]_M^{\eta,\rho}, \rho_a) \right) - \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} \left( \mathcal{A}[\vec{v}_1]_M^{\eta,\rho} (1^{\eta}, [\vec{v}_0]_M^{\eta,\rho}, \rho_a) \right) \right| \le \mathrm{E}_{\rho} (\llbracket \varepsilon_0 \rrbracket_M^{\eta,\rho} (\mathrm{time}_{\mathcal{A}}^{\eta}, \mathrm{calls}_{\mathcal{A}}^{\eta})) $$

And we have that:

$$ \begin{align*} & \mathrm{E}_{\rho}(\llbracket \varepsilon_0 \rrbracket_M^{\eta,\rho} (\mathrm{time}_{\mathcal{A}}^{\eta}, \mathrm{calls}_{\mathcal{A}}^{\eta})) \\ &= \mathrm{E}_{\rho}(\llbracket \varepsilon_0 \rrbracket_M^{\eta,\rho} (\mathrm{time}_{\mathcal{A}}^{\eta}, \mathrm{calls}_{\mathcal{A}}^{\eta}) \llbracket \varepsilon_0 \rrbracket_M^{\eta,\rho} \le \llbracket \varepsilon'_0 \rrbracket_M^{\eta,\rho}) + \mathrm{E}_{\rho}(\llbracket \varepsilon_0 \rrbracket_M^{\eta,\rho} (\mathrm{time}_{\mathcal{A}}^{\eta}, \mathrm{calls}_{\mathcal{A}}^{\eta}) \llbracket -\llbracket \varepsilon_0 \rrbracket_M^{\eta,\rho} \le \llbracket \varepsilon'_0 \rrbracket_M^{\eta,\rho}) \\ &\le \mathrm{E}_{\rho}(\llbracket \varepsilon'_0 \rrbracket_M^{\eta,\rho} (\mathrm{time}_{\mathcal{A}}^{\eta}, \mathrm{calls}_{\mathcal{A}}^{\eta}) \llbracket \varepsilon_0 \rrbracket_M^{\eta,\rho} \le \llbracket \varepsilon'_0 \rrbracket_M^{\eta,\rho}) + \mathrm{E}_{\rho}(\llbracket -\llbracket \varepsilon_0 \rrbracket_M^{\eta,\rho} \le \llbracket \varepsilon'_0 \rrbracket_M^{\eta,\rho}) \\ &= \mathrm{E}_{\rho}(\llbracket \varepsilon'_0 \rrbracket_M^{\eta,\rho} (\mathrm{time}_{\mathcal{A}}^{\eta}, \mathrm{calls}_{\mathcal{A}}^{\eta})) + \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} (\neg (\llbracket \varepsilon_0 \le \varepsilon'_0 \rrbracket_M^{\eta,\rho})) \end{align*} $$

Therefore, by the second premise, we have:

$$ \left| \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} \left( \mathcal{A}[\vec{u}_1]_M^{\eta,\rho} (1^{\eta}, [\vec{u}_0]_M^{\eta,\rho}, \rho_a) \right) - \mathrm{Pr}_{\rho \in \mathbb{T}_{M,\eta}} \left( \mathcal{A}[\vec{v}_1]_M^{\eta,\rho} (1^{\eta}, [\vec{v}_0]_M^{\eta,\rho}, \rho_a) \right) \right| \le \mathrm{E}_{\rho} (\llbracket \varepsilon'_0 \rrbracket_M^{\eta,\rho} (\mathrm{time}_{\mathcal{A}}^{\eta}, \mathrm{calls}_{\mathcal{A}}^{\eta})) + \mathrm{E}_{\rho} (\llbracket \varepsilon_1 \rrbracket_M^{\eta,\rho}). $$

So, $\mathbf{M} \models \vec{u} \sim_{\varepsilon'_0 + \varepsilon_1} \vec{v}$.

### L. Induction Rules

* **$G_\varepsilon$.INDUCTION:**

Let $\mathbf{M}$ be a model such that $\mathbf{M} \models \Theta$.

Then by the first premise of the rule, we have that $\mathbf{M} \models \text{well-founded}_\tau(<_\tau)$. So, we have that

$$ \mathbf{M} \models [\forall (l : \mathrm{nat} \to \tau) . \neg (\forall (i, j : \mathrm{nat}) . i < j \to l j <_\tau l i)]_0 $$

Therefore, since the interpretation of $<$ is always $<$, and the one of nat is $\mathbb{N}$,

$$ \forall \eta \in \mathbb{N}, \forall \rho \in \mathbb{T}_{M,\eta}, \forall l \in \mathcal{F}(\mathbb{N}, [\llbracket \tau \rrbracket_M^{\eta,\rho}), \exists i \in [\llbracket \tau \rrbracket_M^{\eta,\rho}, \exists j \in [\llbracket \tau \rrbracket_M^{\eta,\rho}, i < j \wedge \neg (l j [\llbracket \eta, \rho \rrbracket_M \wedge l x) $$

Which exactly mean that for every $\eta$ in $\mathbb{N}$ and every $\rho$ in $\mathbb{T}_{M,\eta}$, $[\llbracket \eta \rrbracket_M^{\eta,\rho}$ is well-founded. Recall that $\mathbb{RV}(\tau)$ is the set of random variables over $\tau$. (i.e $\mathbb{RV}(\tau)$ is equal to $\prod_{\eta \in \mathbb{N}} (\mathbb{T}_{M,\eta} \to [\llbracket \tau \rrbracket_M^{\eta,\rho})$).

Therefore we can define the order $<_{SPW}$ over $\mathbb{RV}(\tau)$ as such: for every $X, Y$ in $\mathbb{RV}(\tau)$, $X <_{SPW} Y$, if and only if, $\forall \eta \in \mathbb{N}, \forall \rho \in \mathbb{T}_{M,\eta}, X_\eta(\rho) [\llbracket \eta \rrbracket_M^{\eta,\rho} Y_\eta(\rho)$. We can notice, that it is in fact a well-founded function when for every $\eta$ in $\mathbb{N}$