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 \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 \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 \varepsilon_0 \rrbracket_M^{\eta,\rho} l x]$$

Which exactly mean that for every $\eta$ in $\mathbb{N}$ and every $\rho$ in $\mathbb{T}_{M,\eta}$, $[\llbracket \varepsilon_0 \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 \varepsilon_0 \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}$
and every $\rho$ in $T_{M,\eta}$, $[<]_{M}^{\eta,\rho}$ is also well-founded.

By the second premise, we have that

$$M \models \tilde{\forall}(x : \tau).(\tilde{\forall}(y : \tau).[x <_{\tau} y]_0 \Rightarrow F\{x \mapsto y\}) \Rightarrow F$$

That give,

$$\forall X \in \mathbb{RV}(\tau), (\forall Y \in \mathbb{RV}(\tau).(\forall \eta \in \mathbb{N}, \forall \rho \in T_{M,\eta}, X_{\eta}(\rho) [ [<]_{M}^{\eta,\rho} Y_{\eta}(\rho) ) \Rightarrow [F]_{M} M[x \mapsto Y]) \Rightarrow [F]_{M}$$

which is exactly the induction principle on $\mathbb{RV}(\tau)$ over the well-founded order $<_{SPW}$. Therefore, we have that $\forall X \in \mathbb{RV}(\tau).F$ holds, and this is exactly the conclusion of the rule.

### L_ε.INDUCTION:

Let $M$ be a model such that $M \models \Theta$.

Then by the first premise of the rule, we have that $M \models \text{well-founded}_\tau(<_\tau)$. So, we have that $M \models \det(<_\tau)$. Therefore, there exists $(<_\eta)_{\eta \in \mathbb{N}}$ such that $\forall \eta \in \mathbb{N}, \forall \rho \in T_{M,\eta}, [<_\tau]_{M}^{\eta,\rho} = <_\eta$.

We also have that

$$M \models [\forall (l : \text{nat} \to \tau). \neg (\forall (i, j : \text{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 T_{M,\eta}, \forall l \in \mathcal{F}(\mathbb{N}, [[\tau]]_{M}^{\eta,\rho}), \exists i \in [[\tau]]_{M}^{\eta,\rho}, \exists j \in [[\tau]]_{M}^{\eta,\rho}, i < j \wedge \neg (l j <_\eta l x)$$

Which exactly mean that for every $\eta$ in $\mathbb{N}$, $<_\eta$ is well-founded.

Let $\eta \in \mathbb{N}, \rho \in T_{M,\eta}$ such that $[[\wedge\Gamma]]_{M}^{\eta,\rho} = 1$ and $[[\forall (x : \tau).(\forall (y : \tau).(x <_\tau y) \Rightarrow \psi\{x \mapsto y\}) \Rightarrow \psi]]_{M}^{\eta,\rho} = 1$. Then, we have that $\forall x \in [[\tau]]_{M}^{\eta,\rho}. (\forall y \in [[\tau]]_{M}^{\eta,\rho}. (x <_\eta y) \Rightarrow ([[\psi\{x \mapsto y\}]_{M}^{\eta,\rho} = 1)) \Rightarrow ([[\psi]]_{M}^{\eta,\rho} = 1)$. Which, by induction on $[[\tau]]_{M}^{\eta,\rho}$ over the well-founded order $<_\eta$ give that $\forall x \in [[\tau]]_{M}^{\eta,\rho} \cdot [[\psi]]_{M}^{\eta,\rho} = 1$. Therefore we have that:

$$[[\wedge\Gamma \Rightarrow \forall (x : \tau).(\forall (y : \tau).(x <_\tau y) \Rightarrow \psi\{x \mapsto y\}) \Rightarrow \psi]]_{M}^{\eta,\rho} = 1$$

implies that:

$$[[\wedge\Gamma \Rightarrow \forall (x : \tau).\psi]]_{M}^{\eta,\rho} = 1$$

Which is equivalent to say that:

$$\neg( [[\wedge\Gamma \Rightarrow \forall (x : \tau).\psi]]_{M}^{\eta,\rho} ) = 1$$

which implies that:

$$\neg( [[\wedge\Gamma \Rightarrow \forall (x : \tau).(\forall (y : \tau).(x <_\tau y) \Rightarrow \psi\{x \mapsto y\}) \Rightarrow \psi]]_{M}^{\eta,\rho} ) = 1$$

Which finally give that, for every $\eta$ in $\mathbb{N}$:

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

# APPENDIX E

## PROOF TRANSFORMATIONS: COMMUTATIONS

In this section, we present the detail of ►AD, which is constituted of the commutation of $G_\varepsilon.E:CS_R, G_\varepsilon.E:BI-DEDUCE$ and $G.WEAK$ with:

* $G_\varepsilon.E:REWRITE_0$

* $G_\varepsilon.E:FRESH$

* The cryptographic rules: $G_\varepsilon.PRF, G_\varepsilon.CCA_1$

* the rules in Fig. 10 in section left rules and the section local and global relations (except for $G.L-\tilde{\forall}$ and $G_\varepsilon.L-LOC:\lor$)

* $G.CUT, G.DUP$

We show the commutation in detail of $G_\varepsilon.E:REWRITE_0, G_\varepsilon.E:FRESH$ and $G_\varepsilon.CCA_1$. We don't show it for $G_\varepsilon.PRF$ since it is almost identical to $G_\varepsilon.CCA_1$. Same, the rest of the rules, we show some examples but not all of them since most of them are almost identical or with very little change.

We will use $G.WEAK$ and $G.DUP$ without mention it (except in the commutation of $G.L-\tilde{\Lambda}$ and $G_\varepsilon.E:CS$ as an example). Same with the use rule of the family of rewriting without error, we will not mention the equality we are rewriting for the sake of readability (except in the commutation of $G_\varepsilon.E:REWRITE_0$). We also simplify quite a lot the expression of the upper-bound given by the $G_\varepsilon.E:BI-DEDUCE$ rule in order to make the rules readable (see Appendix B-B for more details)
and every $\rho$ in $T_{M,\eta}$, $[<]_{M}^{\eta,\rho}$ is also well-founded.

By the second premise, we have that

$$M \models \tilde{\forall}(x : \tau).(\tilde{\forall}(y : \tau).[x <_{\tau} y]_0 \Rightarrow F\{x \mapsto y\}) \Rightarrow F$$

That give,

$$\forall X \in \mathbb{RV}(\tau), (\forall Y \in \mathbb{RV}(\tau).(\forall \eta \in \mathbb{N}, \forall \rho \in T_{M,\eta}, X_{\eta}(\rho) [[<]]_{M}^{\eta,\rho} Y_{\eta}(\rho)) \Rightarrow [[F]]_{M} M[x \mapsto Y]) \Rightarrow [[F]]_{M}$$

which is exactly the induction principle on $\mathbb{RV}(\tau)$ over the well-founded order $<_{SPW}$. Therefore, we have that $\forall X \in \mathbb{RV}(\tau).F$ holds, and this is exactly the conclusion of the rule.

### L_ε.INDUCTION:

Let $M$ be a model such that $M \models \Theta$.

Then by the first premise of the rule, we have that $M \models \text{well-founded}_\tau(<_\tau)$. So, we have that $M \models \det(<_\tau)$. Therefore, there exists $(<_\eta)_{\eta \in \mathbb{N}}$ such that $\forall \eta \in \mathbb{N}, \forall \rho \in T_{M,\eta}, [[<_\tau]]_{M}^{\eta,\rho} = <_\eta$.

We also have that

$$M \models [\forall (l : \text{nat} \to \tau). \neg (\forall (i, j : \text{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 T_{M,\eta}, \forall l \in \mathcal{F}(\mathbb{N}, [[\tau]]_{M}^{\eta,\rho}), \exists i \in [[\tau]]_{M}^{\eta,\rho}, \exists j \in [[\tau]]_{M}^{\eta,\rho}, i < j \wedge \neg (l j <_\eta l x)$$

Which exactly mean that for every $\eta$ in $\mathbb{N}$, $<_\eta$ is well-founded.

Let $\eta \in \mathbb{N}, \rho \in T_{M,\eta}$ such that $[[\wedge\Gamma]]_{M}^{\eta,\rho} = 1$ and $[[\forall (x : \tau).(\forall (y : \tau).(x <_\tau y) \Rightarrow \psi\{x \mapsto y\}) \Rightarrow \psi]]_{M}^{\eta,\rho} = 1$. Then, we have that $\forall x \in [[\tau]]_{M}^{\eta,\rho}. (\forall y \in [[\tau]]_{M}^{\eta,\rho}. (x <_\eta y) \Rightarrow ([[\psi\{x \mapsto y\}]_{M}^{\eta,\rho} = 1)) \Rightarrow ([[\psi]]_{M}^{\eta,\rho} = 1)$. Which, by induction on $[[\tau]]_{M}^{\eta,\rho}$ over the well-founded order $<_\eta$ give that $\forall x \in [[\tau]]_{M}^{\eta,\rho} \cdot [[\psi]]_{M}^{\eta,\rho} = 1$. Therefore we have that:

$$[[\wedge\Gamma \Rightarrow \forall (x : \tau).(\forall (y : \tau).(x <_\tau y) \Rightarrow \psi\{x \mapsto y\}) \Rightarrow \psi]]_{M}^{\eta,\rho} = 1$$

implies that:

$$[[\wedge\Gamma \Rightarrow \forall (x : \tau).\psi]]_{M}^{\eta,\rho} = 1$$

Which is equivalent to say that:

$$\neg([[\wedge\Gamma \Rightarrow \forall (x : \tau).\psi]]_{M}^{\eta,\rho}) = 1$$

which implies that:

$$\neg([[\wedge\Gamma \Rightarrow \forall (x : \tau).(\forall (y : \tau).(x <_\tau y) \Rightarrow \psi\{x \mapsto y\}) \Rightarrow \psi]]_{M}^{\eta,\rho}) = 1$$

Which finally give that, for every $\eta$ in $\mathbb{N}$:

$$\Pr_{\rho \in T_{M,\eta}} (\neg(\neg(\wedge\Gamma \Rightarrow \forall (x : \tau).\psi]]_{M}^{\eta,\rho})) \leq \Pr_{\rho \in T_{M,\eta}} (\neg(\neg(\wedge\Gamma \Rightarrow \forall (x : \tau).(\forall (y : \tau).(x <_\tau y) \Rightarrow \psi\{x \mapsto y\}) \Rightarrow \psi]]_{M}^{\eta,\rho})) \\ \leq \mathbb{E}_{\rho}(\varepsilon)$$

# APPENDIX E

## PROOF TRANSFORMATIONS: COMMUTATIONS

In this section, we present the detail of ►AD, which is constituted of the commutation of $G_\varepsilon.E:CS_R, G_\varepsilon.E:BI-DEDUCE$ and $G.WEAK$ with:

* $G_\varepsilon.E:REWRITE_0$

* $G_\varepsilon.E:FRESH$

* The cryptographic rules: $G_\varepsilon.PRF, G_\varepsilon.CCA_1$

* the rules in Fig. 10 in section left rules and the section local and global relations (except for $G.L-\tilde{\forall}$ and $G_\varepsilon.L-LOC:\lor$)

* $G.CUT, G.DUP$

We show the commutation in detail of $G_\varepsilon.E:REWRITE_0, G_\varepsilon.E:FRESH$ and $G_\varepsilon.CCA_1$. We don't show it for $G_\varepsilon.PRF$ since it is almost identical to $G_\varepsilon.CCA_1$. Same, the rest of the rules, we show some examples but not all of them since most of them are almost identical or with very little change.

We will use $G.WEAK$ and $G.DUP$ without mention it (except in the commutation of $G.L-\tilde{\forall}$ and $G_\varepsilon.E:CS$ as an example). Same with the use rule of the family of rewriting without error, we will not mention the equality we are rewriting for the sake of readability (except in the commutation of $G_\varepsilon.E:REWRITE_0$). We also simplify quite a lot the expression of the upper-bound given by the $G_\varepsilon.E:BI-DEDUCE$ rule in order to make the rules readable (see Appendix B-B for more details)
As for the $\blacktriangleright_{col}$, we limit ourself the Fig. 14 since this level of detail is enough to see and be able to complete it. For a bit more detail, in most complicated collapsing rule, the one with G.AXIOM and $G_\epsilon.E:CS_R$. The term at the conclusion is of the form

$$ \bar{u}, \text{ if } b \bar{u} \text{ then } C \bar{u} \bar{n} \text{ else } C' \bar{u} \bar{n}' $$

(and the same thing with $\bar{v}$ on the other side of the equivalence), with the assumption that $b, C$ and $C'$ can be computed by the adversary form $\bar{u}$ in polynomial time. Then we can show that the term

$$ \lambda \bar{x} \bar{y}. \text{ if } b \bar{x} \text{ then } C \bar{x} \bar{y} \text{ else } C' \bar{x} \bar{y} $$

can also be computed by the adversary in polynomial time. Therefore, we can collapse the case-study as shown in the sketch in Fig. 14
As for the $\blacktriangleright_{col}$, we limit ourself the Fig. 14 since this level of detail is enough to see and be able to complete it. For a bit more detail, in most complicated collapsing rule, the one with G.AXIOM and $G_\epsilon.E:CS_R$. The term at the conclusion is of the form

$$ \bar{u}, \text{ if } b \bar{u} \text{ then } C \bar{u} \bar{n} \text{ else } C' \bar{u} \bar{n}' $$

(and the same thing with $\bar{v}$ on the other side of the equivalence), with the assumption that $b$, $C$ and $C'$ can be computed by the adversary form $\bar{u}$ in polynomial time. Then we can show that the term

$$ \lambda \bar{x} \bar{y}. \text{ if } b \bar{x} \text{ then } C \bar{x} \bar{y} \text{ else } C' \bar{x} \bar{y} $$

can also be computed by the adversary in polynomial time. Therefore, we can collapse the case-study as shown in the sketch in Fig. 14
Commutation between G<sub>ε</sub>.E:REWRITE<sub>0</sub> and the ascending rules
With G<sub>ε</sub>.E:CS<sub>R</sub>

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

► CS
REWRITE<sub>0</sub>

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

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

For lisibility reason, we don't show the derivation of ε along the transformation

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

► BI-DUCE
REWRITE<sub>0</sub>

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

With G.WEAK

<figure><img src="image_10.png" /></figure>
Commutation between G<sub>ε</sub>.E:REWRITE<sub>0</sub> and the ascending rules

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

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

► CS
REWRITE<sub>0</sub>

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

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

For lisibility reason, we don't show the derivation of ε along the transformation

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

► BI-DEDUCE
REWRITE<sub>0</sub>

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

With G.WEAK

<figure><img src="image_17.png" /></figure>
## Commutation between G<sub>ε</sub>.E:FRESH and the ascending rules

We omit the commutation with G.WEAK since it is exactly the kind as one with G<sub>ε</sub>.E:REWRITE<sub>0</sub> where the G.WEAK is move upward in all the premises of G<sub>ε</sub>.E:FRESH

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

Since the auxiliary proofs of case-study are not changed by the transformation, we don't write them, same thing for the upper-bound. And we also show the transformation for only one case-study since it is very similar with multiple case-studies.

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

► CS
FRESH

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

Since we can take $b \vec{u}_0 \wedge \phi_{\text{fresh}}^{n,i}(\vec{u}_0, C(n_{\text{fresh}}))$ for $\phi_{\text{fresh}}^{n,i}(\vec{u}_0, b \vec{u}_0 \text{ then } C(n_{\text{fresh}}))$ else $w_0$) (We assume that $n$ $i$ is always require for $w_0$) and $-(b \vec{u}_0) \vee \phi_{\text{fresh}}^{n_{\text{fresh}},i}(\vec{u}_0, C(n_{\text{fresh}}))$ for $\phi_{\text{fresh}}^{n_{\text{fresh}}}(\vec{u}_0, b \vec{u}_0 \text{ then } C(n_{\text{fresh}}))$ else $w_0$) (since $n_{\text{fresh}}$ doesn't appear in $w_0$)

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

Since the upper-bound is not changed by the transformation, we don't write it. And we also show the transformation for only one context since it is very similar with multiple context. The added G<sub>ε</sub>.E:REWRITE<sub>0</sub> are on equality that hold immediately with G.<sub>β</sub>

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

► BI-DEDUCE
FRESH

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

Where the two freshness condition $\phi_{\text{fresh}}$() after transformation can be equal to those right before the transformation since D contains no name and $n_{\text{fresh}}$ cannot appear in $\vec{n}$.
## Commutation between G<sub>ε</sub>.E:FRESH and the ascending rules

We omit the commutation with G.WEAK since it is exactly the kind as one with G<sub>ε</sub>.E:REWRITE<sub>0</sub> where the G.WEAK is move upward in all the premises of G<sub>ε</sub>.E:FRESH

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

Since the auxiliary proofs of case-study are not changed by the transformation, we don't write them, same thing for the upper-bound. And we also show the transformation for only one case-study since it is very similar with multiple case-studies.

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

► CS
FRESH

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

Since we can take $b \vec{u}_0 \wedge \phi_{\text{fresh}}^{n,i}(\vec{u}_0, C(n_{\text{fresh}}))$ for $\phi_{\text{fresh}}^{n,i}(\vec{u}_0, b \vec{u}_0 \text{ then } C(n_{\text{fresh}}))$ else $w_0$) (We assume that $n$ $i$ is always require for $w_0$) and $-(b \vec{u}_0) \vee \phi_{\text{fresh}}^{n, fresh}(\vec{u}_0, C(n_{\text{fresh}}))$ for $\phi_{\text{fresh}}^{n, fresh}(\vec{u}_0, b \vec{u}_0 \text{ then } C(n_{\text{fresh}}))$ else $w_0$) (since $n_{\text{fresh}}$ doesn't appear in $w_0$)

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

Since the upper-bound is not changed by the transformation, we don't write it. And we also show the transformation for only one context since it is very similar with multiple context. The added G<sub>ε</sub>.E:REWRITE<sub>0</sub> are on equality that hold immediately with G.<sub>β</sub>

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

► BI-DEDUCE
FRESH

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

Where the two freshness condition $\phi_{\text{fresh}}$() after transformation can be equal to those right before the transformation since D contains no name and $n_{\text{fresh}}$ cannot appear in $\vec{n}$.
## Commutation between $G_\epsilon$.CCA1 and the ascending rules
With $G_\epsilon$.E:CSR

We omit the auxiliary proof obligation of $G_\epsilon$.E:CSR since there is no difficulty here (note that one of them is to prove that $\text{adv}(b_0)$ which allows to derive the computation of $b_0$ $u_0 \bar{\wedge} b$). We show the commutation with only one case-study, the case with multiple case-study is extremely similar. We also omit the details on the upper-bound. We show a case where $\vec{u}_0$ and $\vec{\alpha}$ are vector of terms of kind 1.

$$ \begin{array}{r@{\;}c@{\;}l@{\quad}l@{\quad}l} & \begin{array}{c} \Pi \\ \mathbb{E}; \Theta; \vec{a} \vdash_c \vec{u}_0, b, i_r, i_k, \vec{a} \\ \Pi_i \end{array} & \begin{array}{c} \Pi_C \\ \mathbb{E}; \Theta; \vec{a} \vdash_c \vec{t}_C, \vec{\sigma}_C C \\ \Pi_\phi \end{array} & \begin{array}{c} \Pi_r \\ \mathbb{E}; \Theta; \emptyset \vdash_{\epsilon_\psi} \phi_{\text{key}}^{k,i_k}(\vec{u}_0, b, i_r, i_k, \vec{a}, C) \wedge \phi_{\text{rand}}^{r,i_r}(\vec{u}_0, b, i_r, i_k, \vec{a}, C) \wedge \phi_{\text{dec}}^{k,i_k}(C) \\ \mathbb{E}; \Theta \vdash \det(i_r) \bar{\wedge} \det(i_k) \end{array} & \begin{array}{c} \Pi_{\text{len}} \\ \mathbb{E}; \Theta \vdash \emptyset \vdash_{\epsilon_r+\epsilon_{\text{CCA}_1}+\epsilon_{\text{aux}}+\epsilon_l} \phi_{\text{key}}^{k,i_k}(\vec{u}_0, b, i_r, i_k, \vec{a}, C) \wedge \phi_{\text{rand}}^{r,i_r}(\vec{u}_0, b, i_r, i_k, \vec{a}, C) \wedge \phi_{\text{dec}}^{k,i_k}(C) \\ \mathbb{E}; \Theta \vdash \vec{u}_0, \text{ if } b \text{ then } C(\vec{a}, \text{enc } (0_{\text{len}}(m)) (r i_r) (\text{pk}(k i_k))) \text{ else } v_0 \sim_{\epsilon_l} \vec{u}_1, v_1 \\ \mathbb{E}; \Theta \vdash \vec{u}_0, \text{ if } b \text{ then } C(\vec{a}, \text{enc } m (r i_r) (\text{pk}(k i_k))) \text{ else } v_0 \sim_{\epsilon_r+\epsilon_{\text{CCA}_1}+\epsilon_{\text{aux}}+\epsilon_l} \vec{u}_1, v_1 \\ \mathbb{E}; \Theta \vdash \vec{u}_0, \text{ if } b_0 \vec{u}_0 \text{ then if } b \text{ then } C(\vec{a}, \text{enc } m (r i_r) (\text{pk}(k i_k))) \text{ else } v_0 \text{ else } v_0 \sim_{\epsilon_r+\epsilon_{\text{CCA}_1}+\epsilon_{\text{aux}}+\epsilon_l} \vec{u}_1, \text{ if } b_0 \vec{u}_1 \text{ then } v_1 \text{ else } w_1 \end{array} & \begin{array}{c} G_\epsilon \cdot \text{CCA1} \\ \mathbb{E}; \Theta \vdash \vec{u}_0, w_0 \sim_{\epsilon_r} \vec{u}_1, w_1 \\ G_\epsilon \cdot \text{E:CSR} \end{array} \\ \multicolumn{4}{c}{\text{► CCA1}} \\ & \begin{array}{c} \Pi_l \\ \mathbb{E}; \Theta \vdash \vec{u}_0, \text{ if } b \text{ then } C(\vec{a}, \text{enc } (0_{\text{len}}(m)) (r i_r) (\text{pk}(k i_k))) \text{ else } v_0 \sim_{\epsilon'_l} \vec{u}_1, v_1 \\ \mathbb{E}; \Theta \vdash \vec{u}_0, \text{ if } b_0 \vec{u}_0 \text{ then if } b \text{ then } C(\vec{a}, \text{enc } (0_{\text{len}}(m)) (r i_r) (\text{pk}(k i_k))) \text{ else } v_0 \text{ else } v_0 \sim_{\epsilon'_r+\epsilon'_l} \vec{u}_1, \text{ if } b_0 \vec{u}_0 \text{ then } v_1 \text{ else } w_1 \\ \mathbb{E}; \Theta \vdash \vec{u}_0, \text{ if } b_0 \vec{u}_0 \wedge b \text{ then } C(\vec{a}, \text{enc } (0_{\text{len}}(m)) (r i_r) (\text{pk}(k i_k))) \text{ else if } b \text{ then } v_0 \text{ else } v_0 \sim_{\epsilon'_r+\epsilon'_l} \vec{u}_1, \text{ if } b_0 \vec{u}_0 \text{ then } v_1 \text{ else } w_1 \end{array} & \begin{array}{c} \Pi_r \\ \mathbb{E}; \Theta \vdash \vec{u}_0, w_0 \sim_{\epsilon'_r} \vec{u}_1, w_1 \\ G_\epsilon \cdot \text{E:CSR} \\ G_\epsilon \cdot \text{E:REWRITE}_0 \end{array} \\ & \begin{array}{c} \Pi'_l \\ \mathbb{E}; \Theta; \vec{a} \vdash_c \vec{u}_0, b_0 \vec{u}_0 \wedge b, i_r, i_k, \vec{a} \\ \Pi_i \end{array} & \begin{array}{c} \Pi_C \\ \mathbb{E}; \Theta; \vec{a} \vdash_c \vec{t}_C, \vec{\sigma}_C C \\ \Pi_\phi \end{array} & \begin{array}{c} \Pi_{\text{len}} \\ \mathbb{E}; \Theta \vdash \emptyset \vdash_{\epsilon_\psi} \phi_{\text{key}}^{k,i_k}(\vec{u}_0, b_0 \vec{u}_0 \wedge b, i_r, i_k, \vec{a}, C) \wedge \phi_{\text{rand}}^{r,i_r}(\vec{u}_0, b_0 \vec{u}_0 \wedge b, i_r, i_k, \vec{a}, C) \wedge \phi_{\text{dec}}^{k,i_k}(C) \\ \mathbb{E}; \Theta \vdash \det(i_r) \bar{\wedge} \det(i_k) \end{array} & \begin{array}{c} \Pi_{\text{len}} \\ \mathbb{E}; \Theta \vdash \vec{u}_0, \text{ if } b_0 \vec{u}_0 \wedge b \text{ then } C(\vec{a}, \text{enc } m (r i_r) (\text{pk}(k i_k))) \text{ else if } b \text{ then } v_0 \text{ else } v_0 \sim_{\epsilon'_r+\epsilon'_l} \vec{u}_1, \text{ if } b_0 \vec{u}_0 \text{ then } v_1 \text{ else } w_1 \\ \mathbb{E}; \Theta \vdash \vec{u}_0, \text{ if } b_0 \vec{u}_0 \text{ then if } b \text{ then } C(\vec{a}, \text{enc } m (r i_r) (\text{pk}(k i_k))) \text{ else } v_0 \text{ else } v_0 \sim_{\epsilon'_r+\epsilon'_l} \vec{u}_1, \text{ if } b_0 \vec{u}_0 \text{ then } v_1 \text{ else } w_1 \end{array} & \begin{array}{c} G_\epsilon \cdot \text{CCA1} \\ G_\epsilon \cdot \text{E:REWRITE}_0 \end{array} \end{array} $$

$$ \begin{array}{r@{\;}c@{\;}l@{\quad}l@{\quad}l} & \begin{array}{c} \Pi_l \\ \mathbb{E}; \Theta \vdash \vec{u}_0, \text{ if } b \text{ then } C(\vec{a}, \text{enc } (0_{\text{len}}(m)) (r i_r) (\text{pk}(k i_k))) \text{ else } v_0 \sim_{\epsilon'_l} \vec{u}_1, v_1 \\ \mathbb{E}; \Theta \vdash \vec{u}_0, \text{ if } b_0 \vec{u}_0 \text{ then if } b \text{ then } C(\vec{a}, \text{enc } (0_{\text{len}}(m)) (r i_r) (\text{pk}(k i_k))) \text{ else } v_0 \text{ else } v_0 \sim_{\epsilon'_r+\epsilon'_l} \vec{u}_1, \text{ if } b_0 \vec{u}_0 \text{ then } v_1 \text{ else } w_1 \\ \mathbb{E}; \Theta \vdash \vec{u}_0, \text{ if } b_0 \vec{u}_0 \wedge b \text{ then } C(\vec{a}, \text{enc } (0_{\text{len}}(m)) (r i_r) (\text{pk}(k i_k))) \text{ else if } b \text{ then } v_0 \text{ else } v_0 \sim_{\epsilon'_r+\epsilon'_l} \vec{u}_1, \text{ if } b_0 \vec{u}_0 \text{ then } v_1 \text{ else } w_1 \end{array} & \begin{array}{c} \Pi_r \\ \mathbb{E}; \Theta \vdash \vec{u}_0, w_0 \sim_{\epsilon'_r} \vec{u}_1, w_1 \\ G_\epsilon \cdot \text{E:CSR} \\ G_\epsilon \cdot \text{E:REWRITE}_0 \end{array} & \begin{array}{c} \Pi_{\text{len}} \\ \mathbb{E}; \Theta \vdash \vec{u}_0, w_0 \sim_{\epsilon'_r+\epsilon'_l} \vec{u}_1, w_1 \\ G_\epsilon \cdot \text{E:CSR} \\ G_\epsilon \cdot \text{E:REWRITE}_0 \end{array} \\ & \begin{array}{c} \Pi'_l \\ \mathbb{E}; \Theta \vdash \emptyset \vdash_{\epsilon_\psi} \phi_{\text{key}}^{k,i_k}(\vec{u}_0, b_0 \vec{u}_0 \wedge b, i_r, i_k, \vec{a}, C) \wedge \phi_{\text{rand}}^{r,i_r}(\vec{u}_0, b_0 \vec{u}_0 \wedge b, i_r, i_k, \vec{a}, C) \wedge \phi_{\text{dec}}^{k,i_k}(C) \\ \mathbb{E}; \Theta \vdash \det(i_r) \bar{\wedge} \det(i_k) \end{array} & \begin{array}{c} \Pi_C \\ \mathbb{E}; \Theta \vdash \vec{a} \vdash_c \vec{t}_C, \vec{\sigma}_C C \\ \Pi_\phi \end{array} & \begin{array}{c} \Pi_{\text{len}} \\ \mathbb{E}; \Theta \vdash \vec{u}_0, \text{ if } b_0 \vec{u}_0 \wedge b \text{ then } C(\vec{a}, \text{enc } (0_{\text{len}}(m)) (r i_r) (\text{pk}(k i_k))) \text{ else if } b \text{ then } v_0 \text{ else } v_0 \sim_{\epsilon'_r+\epsilon'_l} \vec{u}_1, \text{ if } b_0 \vec{u}_0 \text{ then } v_1 \text{ else } w_1 \\ \mathbb{E}; \Theta \vdash \vec{u}_0, \text{ if } b_0 \vec{u}_0 \wedge b \text{ then } C(\vec{a}, \text{enc } m (r i_r) (\text{pk}(k i_k))) \text{ else if } b \text{ then } v_0 \text{ else } v_0 \sim_{\epsilon'_r+\epsilon'_l} \vec{u}_1, \text{ if } b_0 \vec{u}_0 \text{ then } v_1 \text{ else } w_1 \end{array} & \begin{array}{c} G_\epsilon \cdot \text{CCA1} \\ G_\epsilon \cdot \text{E:REWRITE}_0 \end{array} \end{array} $$

The commutation between $G_\epsilon$.CCA1 and $G_\epsilon$.E:BI-DEDUCE is quite similar, the main point is that we can change

$$ D\vec{u} \vec{u}_0 \text{ if } b \text{ then } C(\vec{a}, \text{enc } m (r i_r) (\text{pk}(k i_k))) \text{ else } v_0 \vec{n} $$

(where $D$ is the context for the $G_\epsilon$.E:BI-DEDUCE rule) to

$$ (\lambda\vec{x} \vec{y} \vec{z} h.(D \vec{x} \vec{y} \vec{z} h \vec{n}))\vec{u} \vec{u}_0 \vec{\alpha} \text{ enc } m (r i_r) (\text{pk}(k i_k)) $$

with $G_\epsilon$.E:REWRITE$_0$ and that if we have $\mathbb{E}; \Theta; \vec{a} \vdash_c \vec{t}_C, \vec{\sigma}_C C$ and $\mathbb{E}; \Theta \vdash \text{adv}_{t,\vec{\sigma}}(\cdot)$ with all the annotation being polynomial (see Appendix C-E for a exact definition) then we can deduce that $\mathbb{E}; \Theta; \vec{a} \vdash_c \vec{t}', \vec{\sigma}' \lambda\vec{x} \vec{y} \vec{z} h.(D \vec{x} \vec{y} \vec{z} h \vec{n})$ with $t'$ and $\vec{\sigma}'$ also polynomial. And the $\phi_{\text{key}}(\cdot), \phi_{\text{rand}}(\cdot), \phi_{\text{dec}}(\cdot)$ are still valid for this new context since $D$ is without names and $\vec{n}$ are names that do not appear in the rest of the terms. Therefore, any ooccurences of $k$ or $r$ in this new context can only come from $C$ and are thus already taken care off by the previous conditions.

We omit the commutation with $G$.WEAK since it is similar to every other commutation of $G$.WEAK but with more auxilary proofs.
Commutation between G.L-Ξ and the ascending rules

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

Since the auxillary proofs of case-study are changed by the transformation exactly as the other branch, we don't write them. We also omit the upper-bound And we also show the transformation for only one case-study since it is very similar with multiples case-studies.

$$
\begin{array}{c}
\displaystyle \frac{\Pi_l}{\frac{\mathbb{E}, x : \tau; \Theta, F \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1}{\mathbb{E}; \Theta, \tilde{\Xi}(x : \tau). F \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1}} \quad \text{G.L.-Ξ} \quad \frac{\Pi_r}{\frac{\mathbb{E}; \Theta, \tilde{\Xi}(x : \tau). F \vdash \tilde{u}_0, w_0 \sim \tilde{u}_1, w_1}{\mathbb{E}; \Theta, \tilde{\Xi}(x : \tau). F \vdash \tilde{u}_0, w_0 \sim \tilde{u}_1, w_1}} \quad \text{G<sub>ε</sub>.E:CS<sub>R</sub>} \\
\qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \text{►CS<sub>Ξ</sub>}
\end{array}
$$

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

$$
\begin{array}{c}
\displaystyle \frac{\Pi_l}{\frac{\mathbb{E}, x : \tau; \Theta, F \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1}{\mathbb{E}, x : \tau; \Theta, \tilde{\Xi}(y : \tau). F, F \vdash \tilde{u}_0, \text{ if } b \tilde{u}_0 \text{ then } v_0 \text{ else } w_0 \sim \tilde{u}_1, \text{ if } b \tilde{u}_1 \text{ then } v_1 \text{ else } w_1}} \quad \text{G<sub>ε</sub>.E:CS<sub>R</sub>} \\
\qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \text{G.L.-Ξ} \\
\displaystyle \frac{\Pi_r}{\frac{\mathbb{E}; \Theta, \tilde{\Xi}(x : \tau). F \vdash \tilde{u}_0, w_0 \sim \tilde{u}_1, w_1}{\mathbb{E}; \Theta, \tilde{\Xi}(x : \tau). F \vdash \tilde{u}_0, w_0 \sim \tilde{u}_1, w_1}} \quad \text{G<sub>ε</sub>.E:CS<sub>R</sub>} \\
\qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \text{G.L.-Ξ}
\end{array}
$$

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

$$
\begin{array}{c}
\displaystyle \frac{\Pi}{\frac{\mathbb{E}, (x : \tau); \Theta, F \vdash \tilde{u} \sim_{\varepsilon} \tilde{v}}{\mathbb{E}; \Theta, \tilde{\Xi}(x : \tau). F \vdash \tilde{u} \sim_{\varepsilon} \tilde{v}}} \quad \text{G.L.-Ξ} \quad \frac{\Pi_C}{\frac{\mathbb{E}; \Theta, \tilde{\Xi}(x : \tau). F \vdash \bigwedge_{i \le n} \mathrm{adv}_{t_i, \delta_i}(C_i)}{\mathbb{E}; \Theta, \tilde{\Xi}(x : \tau). F \vdash \tilde{u} \sim_{\varepsilon} \tilde{v}}} \quad \text{G<sub>ε</sub>.E:BI-DEDUCE} \\
\qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \text{G<sub>ε</sub>.E:BI-DEDUCE} \\
\displaystyle \frac{\Pi_w}{\frac{\mathbb{E}; \Theta, \tilde{\Xi}(x : \tau). F \vdash \mathrm{blen}_{l\tilde{w}}(\tilde{w}_0) \wedge \mathrm{blen}_{l\tilde{w}}(\tilde{w}_1)}{\mathbb{E}; \Theta, \tilde{\Xi}(x : \tau). F \vdash \mathrm{blen}_l(\tilde{u}) \wedge \mathrm{blen}_l(\tilde{v})}} \quad \text{G<sub>ε</sub>.E:BI-DEDUCE} \\
\qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \text{G<sub>ε</sub>.E:BI-DEDUCE} \\
\displaystyle \frac{\Pi}{\frac{\mathbb{E}, (x : \tau); \Theta, F \vdash \tilde{u} \sim_{\varepsilon} \tilde{v}}{\mathbb{E}; \Theta, \tilde{\Xi}(x : \tau). F \vdash \tilde{u} \sim_{\varepsilon} \tilde{v}}} \quad \text{G.L.-Ξ} \quad \frac{\Pi_w}{\frac{\mathbb{E}; \Theta, \tilde{\Xi}(x : \tau). F \vdash \mathrm{blen}_{l\tilde{w}}(\tilde{w}_0) \wedge \mathrm{blen}_{l\tilde{w}}(\tilde{w}_1)}{\mathbb{E}; \Theta, \tilde{\Xi}(x : \tau). F \vdash \mathrm{blen}_{l\tilde{n}}(\tilde{n})}} \quad \text{G<sub>ε</sub>.E:BI-DEDUCE} \\
\qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \text{G<sub>ε</sub>.E:BI-DEDUCE} \\
\displaystyle \frac{\Pi}{\frac{\mathbb{E}, (x : \tau); \Theta, \tilde{\Xi}(y : \tau). F, F \vdash \tilde{w}_0, (C_1, \dots, C_n)}{\mathbb{E}; \Theta, \tilde{\Xi}(x : \tau). F \vdash \tilde{w}_0, (C_1, \dots, C_n)} \quad \text{G.L.-Ξ} \quad \frac{\Pi}{\frac{\mathbb{E}, (x : \tau); \Theta, \tilde{\Xi}(x : \tau). F \vdash \tilde{w}_0, (C_1, \dots, C_n)}{\mathbb{E}; \Theta, \tilde{\Xi}(x : \tau). F \vdash \tilde{w}_0, (C_1, \dots, C_n)} \quad \text{G.L.-Ξ}
\end{array}
$$

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

With G.W.EAK

$$
\frac{\Pi}{\frac{\mathbb{E}, (x : \tau); \Theta_0, F \vdash F_0}{\mathbb{E}; \Theta_0, \tilde{\Xi}(x : \tau). F \vdash F_0}} \quad \text{G.L.-Ξ} \quad \frac{\mathbb{E}, (x : \tau); \Theta_0, F \vdash F_0}{\mathbb{E}; (x : \tau); \Theta_0, F, \Theta_1 \vdash F_0} \quad \text{G.W.EAK} \\
\frac{\mathbb{E}; \Theta_0, \tilde{\Xi}(x : \tau). F, \Theta_1 \vdash F_0}{\mathbb{E}; \Theta_0, \tilde{\Xi}(x : \tau). F, \Theta_1 \vdash F_0} \quad \text{G.L.-Ξ}
$$

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

$$
\frac{\Pi}{\frac{\mathbb{E}, (x : \tau); \Theta_0, F \vdash F_0}{\mathbb{E}, (x : \tau); \Theta_0, F, \Theta_1 \vdash F_0}} \quad \text{G.W.EAK} \quad \frac{\mathbb{E}; \Theta_0, \tilde{\Xi}(x : \tau). F, \Theta_1 \vdash F_0}{\mathbb{E}; \Theta_0, \tilde{\Xi}(x : \tau). F, \Theta_1 \vdash F_0} \quad \text{G.L.-Ξ}
$$
Commutation between G.L-Λ̃ and the ascending rules

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

Since the auxillary proofs of case-study are changed by the transformation exactly as the other branch, we don't write them. We also omit the upper-bound And we also show the transformation for only one case-study since it is very similar with multiples case-studies.

$$
\begin{array}{c}
\begin{array}{c}
\Pi_l \\
\begin{array}{c}
\mathbb{E}; \Theta, F_0, F_1 \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1 \\
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1
\end{array}
\end{array}
\end{array}
\quad
\begin{array}{c}
\Pi_r \\
\begin{array}{c}
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \vdash \tilde{u}_0, w_0 \sim \tilde{u}_1, w_1 \\
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \vdash \tilde{u}_0, w_0 \sim \tilde{u}_1, w_1
\end{array}
\end{array}
\quad
\begin{array}{c}
G.L.-\tilde{\Lambda} \\
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \vdash \tilde{u}_0, \text{if } b \tilde{u}_0 \text{ then } v_0 \text{ else } w_0 \sim \tilde{u}_1, \text{if } b \tilde{u}_1 \text{ then } v_1 \text{ else } w_1
\end{array}
\quad
\begin{array}{c}
G_{\epsilon}.E:CS_{R} \\
\blacktriangle_{\tilde{\Lambda}}^{\text{CS}}
\end{array}
\end{array}
$$

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

$$
\begin{array}{c}
\begin{array}{c}
\Pi_l \\
\begin{array}{c}
\mathbb{E}; \Theta, F_0, F_1 \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1 \\
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1, F_0, F_1 \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1
\end{array}
\end{array}
\end{array}
\quad
\begin{array}{c}
\Pi_r \\
\begin{array}{c}
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \vdash \tilde{u}_0, w_0 \sim \tilde{u}_1, w_1 \\
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1, F_0, F_1 \vdash \tilde{u}_0, w_0 \sim \tilde{u}_1, w_1
\end{array}
\end{array}
\quad
\begin{array}{c}
G.W.EAK \\
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1, F_0, F_1 \vdash \tilde{u}_0, \text{if } b \tilde{u}_0 \text{ then } v_0 \text{ else } w_0 \sim \tilde{u}_1, \text{if } b \tilde{u}_1 \text{ then } v_1 \text{ else } w_1
\end{array}
\quad
\begin{array}{c}
G.E.E:CS_{R} \\
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \vdash \tilde{u}_0, \text{if } b \tilde{u}_0 \text{ then } v_0 \text{ else } w_0 \sim \tilde{u}_1, \text{if } b \tilde{u}_1 \text{ then } v_1 \text{ else } w_1
\end{array}
\quad
\begin{array}{c}
G.L.-\tilde{\Lambda} \\
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \vdash \tilde{u}_0, \text{if } b \tilde{u}_0 \text{ then } v_0 \text{ else } w_0 \sim \tilde{u}_1, \text{if } b \tilde{u}_1 \text{ then } v_1 \text{ else } w_1
\end{array}
\quad
\begin{array}{c}
G.DUP
\end{array}
\end{array}
$$

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

$$
\begin{array}{c}
\begin{array}{c}
\Pi \\
\begin{array}{c}
\mathbb{E}; \Theta, F_0, F_1 \vdash \tilde{u} \sim_{\varepsilon} \tilde{v} \\
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \vdash \tilde{u} \sim_{\varepsilon} \tilde{v}
\end{array}
\end{array}
\end{array}
\quad
\begin{array}{c}
\Pi_C \\
\begin{array}{c}
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \vdash \bigwedge_{i \le n} \mathrm{adv}_{t_i, \tilde{\sigma}_i}(C_i)
\end{array}
\end{array}
\quad
\begin{array}{c}
\Pi_w \\
\begin{array}{c}
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \vdash \mathrm{blen}_{l^w}(\tilde{w}_0) \tilde{\Lambda} \mathrm{blen}_{l^w}(\tilde{w}_1)
\end{array}
\end{array}
\quad
\begin{array}{c}
\Pi_a \\
\begin{array}{c}
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \vdash \mathrm{blen}_l(\tilde{u}) \tilde{\Lambda} \mathrm{blen}_l(\tilde{v})
\end{array}
\end{array}
\quad
\begin{array}{c}
\Pi_n \\
\begin{array}{c}
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \vdash \mathrm{blen}_{l^n}(n)
\end{array}
\end{array}
\quad
\begin{array}{c}
G_{\epsilon}.E:BI-DEDUCE \\
\blacktriangle_{\tilde{\Lambda}}^{\text{BI-DEDUCE}}
\end{array}
\end{array}
\quad
\begin{array}{c}
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \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}
\end{array}
$$

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

$$
\begin{array}{c}
\begin{array}{c}
\Pi \\
\begin{array}{c}
\mathbb{E}; \Theta, F_0, F_1 \vdash \tilde{u} \sim_{\varepsilon} \tilde{v}
\end{array}
\end{array}
\end{array}
\quad
\begin{array}{c}
\Pi_C \\
\begin{array}{c}
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \vdash \bigwedge_{i \le n} \mathrm{adv}_{t_i, \tilde{\sigma}_i}(C_i)
\end{array}
\end{array}
\quad
\begin{array}{c}
\Pi_w \\
\begin{array}{c}
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \vdash \mathrm{blen}_{l^w}(\tilde{w}_0) \tilde{\Lambda} \mathrm{blen}_{l^w}(\tilde{w}_1)
\end{array}
\end{array}
\quad
\begin{array}{c}
\Pi_a \\
\begin{array}{c}
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \vdash \mathrm{blen}_l(\tilde{u}) \tilde{\Lambda} \mathrm{blen}_l(\tilde{v})
\end{array}
\end{array}
\quad
\begin{array}{c}
\Pi_n \\
\begin{array}{c}
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \vdash \mathrm{blen}_{l^n}(n)
\end{array}
\end{array}
\quad
\begin{array}{c}
G_{\epsilon}.E:BI-DEDUCE \\
\blacktriangle_{\tilde{\Lambda}}^{\text{BI-DEDUCE}}
\end{array}
\quad
\begin{array}{c}
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1, F_0, F_1 \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} \\
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \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}_0 \tilde{v} \tilde{n}
\end{array}
\end{array}
\quad
\begin{array}{c}
G.L.-\tilde{\Lambda} \\
\mathbb{E}; \Theta, F_0 \tilde{\Lambda} F_1 \vdash \tilde{w}_0, (C_1, \dots, C_n) \tilde{w}_0 \tilde{u} \tilde{n} \sim_{\varepsilon'} (C_1, \dots, C_n) \tilde{w}_0 \tilde{v} \tilde{n}
\end{array}
\end{array}
$$

With G.W.EAK

$$
\begin{array}{c}
\begin{array}{c}
\Pi \\
\begin{array}{c}
\mathbb{E}; \Theta_0, F_0, F_1 \vdash F \\
\mathbb{E}; \Theta_0, F_0 \tilde{\Lambda} F_1 \vdash F
\end{array}
\end{array}
\end{array}
\quad
\begin{array}{c}
G.L.-\tilde{\Lambda} \\
\mathbb{E}; \Theta_0, F_0 \tilde{\Lambda} F_1, \Theta_1 \vdash F
\end{array}
\quad
\begin{array}{c}
\Pi \\
\begin{array}{c}
\mathbb{E}; \Theta_0, F_0, F_1 \vdash F \\
\mathbb{E}; \Theta_0, F_0, F_1, \Theta_1 \vdash F
\end{array}
\end{array}
\quad
\begin{array}{c}
G.W.EAK \\
\mathbb{E}; \Theta_0, F_0 \tilde{\Lambda} F_1, \Theta_1 \vdash F
\end{array}
\quad
\begin{array}{c}
G.L.-\tilde{\Lambda} \\
\blacktriangle_{\tilde{\Lambda}}^{\text{WEAK}}
\end{array}
\end{array}
$$

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

$$
\begin{array}{c}
\begin{array}{c}
\Pi \\
\begin{array}{c}
\mathbb{E}; \Theta_0, F_0, F_1 \vdash F \\
\mathbb{E}; \Theta_0, F_0, F_1, \Theta_1 \vdash F
\end{array}
\end{array}
\end{array}
\quad
\begin{array}{c}
G.W.EAK \\
\mathbb{E}; \Theta_0, F_0 \tilde{\Lambda} F_1, \Theta_1 \vdash F
\end{array}
\quad
\begin{array}{c}
G.L.-\tilde{\Lambda} \\
\blacktriangle_{\tilde{\Lambda}}^{\text{WEAK}}
\end{array}
\end{array}
$$
Commutation between G.L-Λ̃ and the ascending rules

With G_ε.E:CS_R

Since the auxillary proofs of case-study are changed by the transformation exactly as the other branch, we don't write them. We also omit the upper-bound And we also show the transformation for only one case-study since it is very similar with multiples case-studies.

$$ \begin{array}{ccc} \begin{array}{c} \Pi_l \\ \frac{\mathbb{E}; \Theta, F_0, F_1 \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1}{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1 \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1} \end{array} & \text{G.L-Λ̃} & \begin{array}{c} \Pi_r \\ \frac{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1 \vdash \tilde{u}_0, w_0 \sim \tilde{u}_1, w_1}{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1 \vdash \tilde{u}_0, w_0 \sim \tilde{u}_1, w_1} \end{array} \end{array} \quad G_\epsilon.E:CS_R $$

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

$$ \begin{array}{ccc} \begin{array}{c} \Pi_l \\ \frac{\mathbb{E}; \Theta, F_0, F_1 \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1}{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1, F_0, F_1 \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1} \end{array} & \text{G.W.EAK} & \begin{array}{c} \Pi_r \\ \frac{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1 \vdash \tilde{u}_0, w_0 \sim \tilde{u}_1, w_1}{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1, F_0, F_1 \vdash \tilde{u}_0, w_0 \sim \tilde{u}_1, w_1} \end{array} \end{array} \quad G.W.EAK \quad G_\epsilon.E:CS_R $$
$$ \begin{array}{ccc} \begin{array}{c} \Pi_r \\ \frac{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1, F_0, F_1 \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1}{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1, F_0, F_1 \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1} \end{array} & \text{G.W.EAK} & \begin{array}{c} \Pi_l \\ \frac{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1 \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1}{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1 \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1} \end{array} \end{array} \quad G.DUP $$

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

With G_ε.E:BI-DEDUCE

$$ \begin{array}{ccc} \begin{array}{c} \Pi \\ \frac{\mathbb{E}; \Theta, F_0, F_1 \vdash \tilde{u} \sim_{\varepsilon} \tilde{v}}{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1 \vdash \tilde{u} \sim_{\varepsilon} \tilde{v}} \end{array} & \text{G.L-Λ̃} & \begin{array}{c} \Pi_C \\ \frac{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1 \vdash \tilde{\Lambda}_{i \le n} \mathrm{adv}_{t_i, \tilde{\sigma}_i}(C_i)}{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1 \vdash \tilde{\Lambda}_{i \le n} \mathrm{adv}_{t_i, \tilde{\sigma}_i}(C_i)} \end{array} \end{array} \quad G_\epsilon.E:BI-DEDUCE $$

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

$$ \begin{array}{ccc} \begin{array}{c} \Pi \\ \frac{\mathbb{E}; \Theta, F_0, F_1 \vdash \tilde{u} \sim_{\varepsilon} \tilde{v}}{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1 \vdash \tilde{u} \sim_{\varepsilon} \tilde{v}} \end{array} & \text{G.L-Λ̃} & \begin{array}{c} \Pi_C \\ \frac{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1 \vdash \tilde{\Lambda}_{i \le n} \mathrm{adv}_{t_i, \tilde{\sigma}_i}(C_i)}{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1 \vdash \tilde{\Lambda}_{i \le n} \mathrm{adv}_{t_i, \tilde{\sigma}_i}(C_i)} \end{array} \end{array} \quad G_\epsilon.E:BI-DEDUCE $$
$$ \begin{array}{ccc} \begin{array}{c} \Pi_w \\ \frac{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1 \vdash \mathrm{blen}_{l^w}(\tilde{w}_0) \tilde{\Lambda} \mathrm{blen}_{l^w}(\tilde{w}_1)}{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1 \vdash \mathrm{blen}_{l^w}(\tilde{w}_0) \tilde{\Lambda} \mathrm{blen}_{l^w}(\tilde{w}_1)} \end{array} & \text{G.W.EAK} & \begin{array}{c} \Pi_a \\ \frac{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1 \vdash \mathrm{blen}_l(\tilde{u}) \tilde{\Lambda} \mathrm{blen}_l(\tilde{v})}{\mathbb{E}; \Theta, F_0, \tilde{\Lambda} F_1 \vdash \mathrm{blen}_l(\tilde{u}) \tilde{\Lambda} \mathrm{blen}_l(\tilde{v})} \end{array} \end{array} \quad G.L-\tilde{\Lambda} $$

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

With G.W.EAK

$$ \begin{array}{ccc} \begin{array}{c} \Pi \\ \frac{\mathbb{E}; \Theta_0, F_0, F_1 \vdash F}{\mathbb{E}; \Theta_0, F_0, \tilde{\Lambda} F_1 \vdash F} \end{array} & \text{G.L-Λ̃} & \begin{array}{c} \Pi \\ \frac{\mathbb{E}; \Theta_0, F_0, F_1 \vdash F}{\mathbb{E}; \Theta_0, F_0, \tilde{\Lambda} F_1 \vdash F} \end{array} \end{array} \quad G.W.EAK $$

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

$$ \begin{array}{ccc} \begin{array}{c} \Pi \\ \frac{\mathbb{E}; \Theta_0, F_0, F_1 \vdash F}{\mathbb{E}; \Theta_0, F_0, F_1, \Theta_1 \vdash F} \end{array} & \text{G.W.EAK} & \begin{array}{c} \Pi \\ \frac{\mathbb{E}; \Theta_0, F_0, \tilde{\Lambda} F_1, \Theta_1 \vdash F}{\mathbb{E}; \Theta_0, F_0, \tilde{\Lambda} F_1, \Theta_1 \vdash F} \end{array} \end{array} \quad G.L-\tilde{\Lambda} $$
## Commutation between G.CUT and the ascending rules

Since the auxiliary proofs of case-study are changed by the transformation exactly as the other branch, we don't write them. We also omit the upper-bound And we also show the transformation for only one case-study since it is very similar with multiples case-studies.

$$ \begin{array}{ccc} \begin{array}{c} \Pi_c \\ \mathbb{E}; \Theta \vdash F \\ \mathbb{E}; \Theta \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1 \end{array} & \begin{array}{c} \Pi_l \\ \mathbb{E}; \Theta, F \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1 \end{array} & \begin{array}{c} \Pi_r \\ \mathbb{E}; \Theta \vdash \tilde{u}_0, w_0 \sim \tilde{u}_1, w_1 \end{array} \\ \text{G.CUT} & & \text{G.} \varepsilon. \text{E:CS}_R \\ \mathbb{E}; \Theta \vdash \tilde{u}_0, \text{if } b \tilde{u}_0 \text{ then } v_0 \text{ else } w_0 \sim \tilde{u}_1, \text{if } b \tilde{u}_1 \text{ then } v_1 \text{ else } w_1 & & \text{CS.} \varepsilon. \text{E:} \text{CS}_R \end{array} $$

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

$$ \begin{array}{ccc} \begin{array}{c} \Pi_c \\ \mathbb{E}; \Theta \vdash F \end{array} & \begin{array}{c} \Pi_l \\ \mathbb{E}; \Theta, F \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1 \end{array} & \begin{array}{c} \Pi_r \\ \mathbb{E}; \Theta \vdash \tilde{u}_0, w_0 \sim \tilde{u}_1, w_1 \end{array} \\ \text{G.} \varepsilon. \text{E:CS}_R & & \text{G.} \text{CUT} \\ \mathbb{E}; \Theta \vdash \tilde{u}_0, \text{if } b \tilde{u}_0 \text{ then } v_0 \text{ else } w_0 \sim \varepsilon_l + \varepsilon_r, \tilde{u}_1, \text{if } b \tilde{u}_1 \text{ then } v_1 \text{ else } w_1 & & \end{array} $$

## With G.ε.E:BI-DEDUCE

$$ \begin{array}{ccc} \begin{array}{c} \Pi_F \\ \mathbb{E}; \Theta \vdash F \end{array} & \begin{array}{c} \Pi \\ \mathbb{E}; \Theta, F \vdash \tilde{u} \sim \varepsilon \end{array} & \begin{array}{c} \Pi_R \\ \mathbb{E}; \Theta \vdash \tilde{u} \sim \varepsilon \end{array} \\ \text{G.CUT} & & \text{G.} \varepsilon. \text{E:BI-DEDUCE} \\ \mathbb{E}; \Theta \vdash \tilde{u}_0, (C_1, \dots, C_n) \tilde{u}_0 \tilde{u} \tilde{n} \sim \varepsilon' \tilde{w}_1, (C_1, \dots, C_n) \tilde{w}_1 \tilde{v} \tilde{n} & & \end{array} $$

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

$$ \begin{array}{ccc} \begin{array}{c} \Pi_F \\ \mathbb{E}; \Theta \vdash F \end{array} & \begin{array}{c} \Pi \\ \mathbb{E}; \Theta, F \vdash \tilde{u}_0 \sim \tilde{v} \end{array} & \begin{array}{c} \Pi_C \\ \mathbb{E}; \Theta \vdash \tilde{u}_0 \sim \tilde{v} \end{array} \\ \text{G.} \varepsilon. \text{E:BI-DEDUCE} & & \text{G.} \text{CUT} \\ \mathbb{E}; \Theta \vdash \tilde{u}_0, (C_1, \dots, C_n) \tilde{u}_0 \tilde{u} \tilde{n} \sim \varepsilon' \tilde{w}_1, (C_1, \dots, C_n) \tilde{w}_1 \tilde{v} \tilde{n} & & \end{array} $$

## With G.WEAK

$$ \begin{array}{ccc} \begin{array}{c} \Pi_F \\ \mathbb{E}; \Theta \vdash F \\ \mathbb{E}; \Theta_0 \vdash F_0 \end{array} & \begin{array}{c} \Pi \\ \mathbb{E}; \Theta_0, F \vdash F_0 \\ \mathbb{E}; \Theta_0, \Theta_1 \vdash F_0 \end{array} & \begin{array}{c} \Pi \\ \mathbb{E}; \Theta_0, F \vdash F_0 \\ \mathbb{E}; \Theta_0, F, \Theta_1 \vdash F_0 \end{array} \\ \text{G.CUT} & & \text{G.WEAK} \\ \mathbb{E}; \Theta_0, \Theta_1 \vdash F_0 & & \end{array} $$

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

$$ \begin{array}{ccc} \begin{array}{c} \Pi_F \\ \mathbb{E}; \Theta \vdash F \end{array} & \begin{array}{c} \Pi \\ \mathbb{E}; \Theta_0, F \vdash F_0 \\ \mathbb{E}; \Theta_0, F, \Theta_1 \vdash F_0 \end{array} & \begin{array}{c} \Pi \\ \mathbb{E}; \Theta_0, \Theta_1 \vdash F_0 \end{array} \\ \text{G.WEAK} & & \text{G.CUT} \end{array} $$
## Commutation between G.CUT and the ascending rules

Since the auxiliary proofs of case-study are changed by the transformation exactly as the other branch, we don't write them. We also omit the upper-bound And we also show the transformation for only one case-study since it is very similar with multiples case-studies.

$$ \begin{array}{ccc} \begin{array}{c} \Pi_c \\ \mathbb{E}; \Theta \vdash F \\ \mathbb{E}; \Theta \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1 \end{array} & \begin{array}{c} \Pi_l \\ \mathbb{E}; \Theta, F \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1 \end{array} & \begin{array}{c} \Pi_r \\ \mathbb{E}; \Theta \vdash \tilde{u}_0, w_0 \sim \tilde{u}_1, w_1 \end{array} \\ \text{G.CUT} & & \text{G.} \varepsilon. \text{E:CS}_R \\ \mathbb{E}; \Theta \vdash \tilde{u}_0, \text{if } b \tilde{u}_0 \text{ then } v_0 \text{ else } w_0 \sim \tilde{u}_1, \text{if } b \tilde{u}_1 \text{ then } v_1 \text{ else } w_1 & & \text{►} \text{CS CUT} \end{array} $$

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

$$ \begin{array}{ccc} \begin{array}{c} \Pi_c \\ \mathbb{E}; \Theta \vdash F \end{array} & \begin{array}{c} \Pi_l \\ \mathbb{E}; \Theta, F \vdash \tilde{u}_0, v_0 \sim \tilde{u}_1, v_1 \end{array} & \begin{array}{c} \Pi_r \\ \mathbb{E}; \Theta \vdash \tilde{u}_0, w_0 \sim \tilde{u}_1, w_1 \end{array} \\ \text{G.} \varepsilon. \text{E:CS}_R & & \text{G.CUT} \\ \mathbb{E}; \Theta \vdash \tilde{u}_0, \text{if } b \tilde{u}_0 \text{ then } v_0 \text{ else } w_0 \sim \varepsilon_l + \varepsilon_r, \tilde{u}_1, \text{if } b \tilde{u}_1 \text{ then } v_1 \text{ else } w_1 & & \end{array} $$

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

## With G.ε.E:BI-DEDUCE

$$ \begin{array}{ccc} \begin{array}{c} \Pi_F \\ \mathbb{E}; \Theta \vdash F \end{array} & \begin{array}{c} \Pi \\ \mathbb{E}; \Theta, F \vdash \tilde{u} \sim \varepsilon \end{array} & \begin{array}{c} \Pi_r \\ \mathbb{E}; \Theta \vdash \tilde{u} \sim \tilde{v} \end{array} \\ \text{G.CUT} & & \text{G.} \varepsilon. \text{E:BI-DEDUCE} \\ \mathbb{E}; \Theta \vdash \tilde{u}_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} $$

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

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

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

$$ \begin{array}{ccc} \begin{array}{c} \Pi_F \\ \mathbb{E}; \Theta \vdash F \end{array} & \begin{array}{c} \Pi_w \\ \mathbb{E}; \Theta \vdash, \text{blen}_{l\tilde{w}}(\tilde{w}_0) \tilde{\Lambda} \text{blen}_{l\tilde{w}}(\tilde{w}_1) \end{array} & \begin{array}{c} \Pi_a \\ \mathbb{E}; \Theta \vdash, \text{blen}_{l\tilde{w}}(\tilde{w}_1) \tilde{\Lambda} \text{blen}_{l\tilde{w}}(\tilde{w}_1) \end{array} \\ \text{G.} \varepsilon. \text{E:BI-DEDUCE} & & \text{G.CUT} \\ \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} & & \end{array} $$

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

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

## With G.WEAK

$$ \begin{array}{ccc} \begin{array}{c} \Pi_F \\ \mathbb{E}; \Theta \vdash F \\ \mathbb{E}; \Theta_0 \vdash F_0 \end{array} & \begin{array}{c} \Pi \\ \mathbb{E}; \Theta_0, F \vdash F_0 \\ \mathbb{E}; \Theta_0, \Theta_1 \vdash F_0 \end{array} & \begin{array}{c} \Pi_r \\ \mathbb{E}; \Theta_0, F \vdash F_0 \\ \mathbb{E}; \Theta_0, F, \Theta_1 \vdash F_0 \end{array} \\ \text{G.CUT} & & \text{G.WEAK} \\ \mathbb{E}; \Theta_0, \Theta_1 \vdash F_0 & & \end{array} $$

$$ \begin{array}{ccc} \begin{array}{c} \Pi_F \\ \mathbb{E}; \Theta \vdash F \end{array} & \begin{array}{c} \Pi \\ \mathbb{E}; \Theta_0, F \vdash F_0 \\ \mathbb{E}; \Theta_0, F, \Theta_1 \vdash F_0 \end{array} & \begin{array}{c} \Pi_r \\ \mathbb{E}; \Theta_0, \Theta_1 \vdash F_0 \end{array} \\ \text{G.WEAK} & & \text{G.CUT} \end{array} $$

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