**► Lemma 13.** For all $\mathbb{E}$, $l$, $[\mathbb{E}\langle l\rangle] = [\mathbb{E}]\langle[\l]\rangle$.

*Proof.* By induction on $\mathbb{E}$. The ■ case is easy.

We have $[\langle \Box k :: \mathbb{E} \rangle \langle l \rangle] = [\mathbb{E}\langle l k \rangle] \stackrel{\text{ind}}{=} [\mathbb{E}]\langle [l k] \rangle = [\mathbb{E}]\langle [l] \mid k \rangle = (\Box [k] :: [\mathbb{E}])\langle [l] \rangle = [\Box k :: \mathbb{E}]\langle [l] \rangle$. The case $k \Box :: \mathbb{E}$ is similar.

We have $[(\lambda :: \mathbb{E}) \langle l \rangle] = [\mathbb{E} \langle \lambda . l \rangle] \stackrel{\text{ind}}{=} [\mathbb{E}] \langle [\lambda . l] \rangle = [\mathbb{E}] \langle \lambda . [l] (\hat{\otimes} \text{id}) \rangle \stackrel{\text{Lem. 7}}{=} [\mathbb{E}] \langle \lambda . [l] \rangle = (\lambda :: [\mathbb{E}]) \langle [l] \rangle = [\lambda :: \mathbb{E}] \langle [l] \rangle$.

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

**► Lemma 14.** For all $l$ and $h$, $[\l](\uparrow^h) = \langle[\l] \rangle_0^h$.

*Proof.* We prove that for all $i$, $[\l](\uparrow^i \uparrow^h) = \langle[\l] \rangle_i^h$, starting with terms. We proceed by induction: the application case is easy.

If $l = \lambda.t$, then $[\lambda.t](\uparrow^i \uparrow^h) = \lambda.[\l](\uparrow^{i+1} \uparrow^h) \stackrel{\text{ind}}{=} \lambda.\langle[\l] \rangle_{i+1}^h = \langle\lambda.[\l] \rangle_i^h = \langle[\lambda.t] \rangle_i^h$.

Suppose $l = n$. If $n \ge i$, then $[n](\uparrow^i \uparrow^h) \stackrel{\text{Lem. 9}}{=} [n - i](\uparrow^{h+i}) = n + h = \langle[\n] \rangle_i^h$. Otherwise $[n](\uparrow^i \uparrow^h) \stackrel{\text{Lem. 9}}{=} [0](\uparrow^{i-n} \uparrow^h \circ \uparrow^n) = n = \langle[\n] \rangle_i^h$.

The proof then extends easily to configurations by induction.

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

**► Lemma 15.** For all $l$, $k$, and $h$, $[\l](\uparrow^{h+1})\{[k]/h\} = [\l](\uparrow^h)$.

*Proof.* We prove that for all $l$ and $i$, $[\l](\uparrow^i \uparrow^{h+1})\{[k]/h+i\} = [\l](\uparrow^i \uparrow^h)$. Only the index case $n$ is interesting. Suppose $n \ge i$. Then $[n](\uparrow^i \uparrow^{h+1})\{[k]/h+i\} = [n-i](\uparrow^{h+1+i})\{[k]/h+i\} = n+h+1\{[k]/h+i\} = n+h$ and $[n](\uparrow^i \uparrow^h) = [n-i](\uparrow^{h+i}) = n+h$.

If $i > n$, then $[n](\uparrow^i \uparrow^{h+1})\{[k]/h+i\} = [[0](\uparrow^{i-n} \uparrow^{h+1})](\uparrow^n)\{[k]/h+i\} = n\{[k]/h+i\} = n$ and $[n](\uparrow^i \uparrow^h) = [[0](\uparrow^{i-n} \uparrow^h)](\uparrow^n) = n$.

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

**► Lemma 16.** For all $l$, $k$, and $\epsilon$, $[\l](k \cdot \epsilon)] = [\l](\uparrow^\epsilon)\{[k]/0\}$.

*Proof.* We prove that for all $h$, $[\l](\uparrow^h (k \cdot \epsilon)) = [\l](\uparrow^{h+1} \epsilon)\{[k]/h\}$, starting with terms. The interesting case is for a variable $n$, where we distinguish three cases.

Suppose $n < h$. Then

$$ 
\begin{aligned}
[\l](\uparrow^h (k \cdot \epsilon)) &= [[0](\uparrow^{h-n} (k \cdot \epsilon))](\uparrow^n) & \text{by Lemma 9} \\
&= [0](\uparrow^n) = n & \text{by def}
\end{aligned}
$$

and

$$ 
\begin{aligned}
[\l](\uparrow^{h+1} \epsilon)\{[k]/h\} &= [[0](\uparrow^{h+1-n} \epsilon)](\uparrow^n)\{[k]/h\} & \text{by Lemma 9} \\
&= [0](\uparrow^n)\{[k]/h\} = n\{[k]/h\} & \text{by def} \\
&= n & \text{by def}
\end{aligned}
$$

Suppose $n = h$. Then

$$ 
\begin{aligned}
[\l](\uparrow^h (k \cdot \epsilon)) &= [[0](k \cdot \epsilon)](\uparrow^h) & \text{by Lemma 9} \\
&= [k](\uparrow^h) & \text{by def}
\end{aligned}
$$

and

$$ 
\begin{aligned}
[\l](\uparrow^{h+1} \epsilon)\{[k]/h\} &= [[0](\uparrow^\epsilon)](\uparrow^h)\{[k]/h\} & \text{by Lemma 9} \\
&= [0](\uparrow^h)\{[k]/h\} = h\{[k]/h\} & \text{by def} \\
&= \langle[\l] \rangle_0^h & \text{by def}
\end{aligned}
$$
We conclude with Lemma 14.

Suppose $n > h$. Then

$$ 
\begin{aligned}
\llbracket n \rrbracket (\uparrow^h (k \cdot \epsilon)) &= \llbracket \llbracket n - h \rrbracket (k \cdot \epsilon) \rrbracket (\uparrow^h) && \text{by Lemma 9} \\
&= \llbracket \llbracket n - h - 1 \rrbracket (\epsilon) \rrbracket (\uparrow^h) && \text{by def}
\end{aligned}
$$

and

$$ \llbracket n \rrbracket (\uparrow^{h+1} \epsilon) \{ \llbracket k \rrbracket / h \} = \llbracket \llbracket n - h - 1 \rrbracket (\epsilon) \rrbracket (\uparrow^{h+1}) \{ \llbracket k \rrbracket / h \} \quad \text{by Lemma 9} $$

We conclude with Lemma 15.

It concludes the proof on terms, and we extend the proof easily to all configurations by induction. ◀

**Lemma 17.** For all $l, \epsilon$, and $\mathcal{E}$, $\llbracket l \rrbracket (\epsilon \bullet \mathcal{E}) = \llbracket \llbracket l \rrbracket (\epsilon) \rrbracket (\mathcal{E})$.

*Proof.* By case analysis on $\mathcal{E}$, using Lemmas 12 or 8 to conclude. ◀

**Lemma 18.** If $l \xrightarrow{\mathcal{E}, \mathcal{E}}_{\text{ev}} c$, then $\llbracket l \rrbracket (\mathcal{E}) \xrightarrow{\mathcal{E}}_{\text{ev}} \llbracket c \rrbracket$.

$$ \text{If } \epsilon \xrightarrow{\mathcal{E}, n, \mathcal{E}}_{\text{var}} c, \text{ then } \llbracket \llbracket n \rrbracket (\epsilon) \rrbracket (\mathcal{E}) \xrightarrow{\mathcal{E}}_{\text{ev}} \llbracket c \rrbracket. $$

*Proof.* Most cases are straightforward by induction. We detail some for which we need extra results.

env By induction, we get $\llbracket l \rrbracket (\epsilon \bullet \mathcal{E}) \xrightarrow{\mathcal{E}}_{\text{ev}} \llbracket c \rrbracket$, but we want $\llbracket l[\epsilon] \rrbracket (\mathcal{E}) \xrightarrow{\mathcal{E}}_{\text{ev}} \llbracket c \rrbracket$. We get the result by Lemma 12 if $\mathcal{E} = !\phi$, and by Lemma 8 if $\mathcal{E} = *$.

lam In the case $\mathcal{E} = *$, we need Lemma 8 to conclude.

lamβ We want $\llbracket \lambda.l \rrbracket (\epsilon) \xrightarrow{\mathcal{E}}_{\text{ev}} \llbracket \mathcal{E} \langle l[k \cdot \epsilon] \rangle \rrbracket$ (where we might have $\epsilon = \text{id}$), i.e., $\lambda.\llbracket l \rrbracket (\uparrow\epsilon) \xrightarrow{\mathcal{E}}_{\text{ev}} \llbracket \mathcal{E} \langle l[k \cdot \epsilon] \rangle \rrbracket$. We have $\lambda.\llbracket l \rrbracket (\uparrow\epsilon) \xrightarrow{\mathcal{E}}_{\text{ev}} \llbracket \mathcal{E} \langle l \rangle (\uparrow\epsilon) \{ \llbracket k \rrbracket / 0 \} \rangle$. We conclude with Lemmas 13 and 16.

**Lemma 19.** Let $t \xrightarrow{\mathcal{E}}_{\text{ev}} s$. For all $l, \mathcal{E}$ such that $\llbracket l \rrbracket (\mathcal{E}) = t$, for all $\mathcal{E}'$ such that $\llbracket \mathcal{E}' \rrbracket = \mathcal{E}$, there exists $c$ such that $l \xrightarrow{\mathcal{E}', \mathcal{E}}_{\text{ev}} c$ and $\llbracket c \rrbracket = s$.

For all $n, \epsilon, \mathcal{E}$ such that $\llbracket \llbracket n \rrbracket (\epsilon) \rrbracket (\mathcal{E}) = t$, for all $\mathcal{E}'$ such that $\llbracket \mathcal{E}' \rrbracket = \mathcal{E}$, there exists $c$ such that $\epsilon \xrightarrow{\mathcal{E}', n, \mathcal{E}}_{\text{var}} c$ and $\llbracket c \rrbracket = s$.

*Proof.* We define an ordering on couples $(l, \mathcal{E})$ and triples $(n, \epsilon, \mathcal{E})$ as follows.

- $(l, \mathcal{E}) > (k, \mathcal{F})$ if $f_1(l)(f_2(\mathcal{E}) + 1) > f_1(k)(f_2(\mathcal{F}) + 1)$;

- $(l, \mathcal{E}) > (n, \epsilon, \mathcal{F})$ if $f_1(l)(f_2(\mathcal{E}) + 1) > f_2(\epsilon)(f_2(\mathcal{F}) + 1)$;

- $(n, \epsilon, \mathcal{E}) > (l, \mathcal{F})$ if $f_2(\epsilon)(f_2(\mathcal{E}) + 1) > f_1(l)(f_2(\mathcal{F}) + 1)$;

- $(n, \epsilon, \mathcal{E}) > (n, \phi, \mathcal{F})$ if $f_2(\epsilon)(f_2(\mathcal{E}) + 1) > f_2(\phi)(f_2(\mathcal{F}) + 1)$.

where

$$ 
\begin{aligned}
f_1(l[\epsilon]) &\triangleq f_1(l_1)(f_2(\epsilon) + 1) & f_2(\star) &\triangleq 1 \\
f_1(l_1 l_2) &\triangleq f_1(l_1) + f_1(l_2) + 1 & f_2(!\epsilon) &\triangleq f_2(\epsilon) \\
f_1(\lambda.l) &\triangleq 4f_1(l) & f_2(\text{id}) &\triangleq 2 \\
f_1(n) &\triangleq 3 & f_2(\uparrow) &\triangleq 2 \\
& & f_2(l \cdot \epsilon) &\triangleq f_1(l) + f_2(\epsilon) \\
& & f_2(\uparrow\epsilon) &\triangleq 3f_2(\epsilon) \\
& & f_2(\epsilon_1 \circ \epsilon_2) &\triangleq f_2(\epsilon_1)(f_2(\epsilon_2) + 1)
\end{aligned}
$$
We conclude with Lemma 14.

Suppose $n > h$. Then

$$ 
\begin{aligned}
\llbracket n \rrbracket (\uparrow^h (k \cdot \epsilon)) &= \llbracket \llbracket n - h \rrbracket (k \cdot \epsilon) \rrbracket (\uparrow^h) && \text{by Lemma 9} \\
&= \llbracket \llbracket n - h - 1 \rrbracket (\epsilon) \rrbracket (\uparrow^h) && \text{by def}
\end{aligned}
$$

and

$$ \llbracket n \rrbracket (\uparrow^{h+1} \epsilon) \{ \llbracket k \rrbracket / h \} = \llbracket \llbracket n - h - 1 \rrbracket (\epsilon) \rrbracket (\uparrow^{h+1}) \{ \llbracket k \rrbracket / h \} \quad \text{by Lemma 9} $$

We conclude with Lemma 15.

It concludes the proof on terms, and we extend the proof easily to all configurations by induction. ▶

**Lemma 17.** For all $l, \epsilon$, and $\mathcal{E}$, $\llbracket l \rrbracket (\epsilon \bullet \mathcal{E}) = \llbracket \llbracket l \rrbracket (\epsilon) \rrbracket (\mathcal{E})$.

**Proof.** By case analysis on $\mathcal{E}$, using Lemmas 12 or 8 to conclude. ▶

**Lemma 18.** If $l \xrightarrow{\mathcal{E}, \mathcal{E}}_{\text{ev}} c$, then $\llbracket l \rrbracket (\mathcal{E}) \xrightarrow{\mathcal{E}}_{\text{ev}} \llbracket c \rrbracket$.

$$ \text{If } \epsilon \xrightarrow{\mathcal{E}, n, \mathcal{E}}_{\text{var}} c, \text{ then } \llbracket \llbracket n \rrbracket (\epsilon) \rrbracket (\mathcal{E}) \xrightarrow{\mathcal{E}}_{\text{ev}} \llbracket c \rrbracket. $$

**Proof.** Most cases are straightforward by induction. We detail some for which we need extra results.

**env** By induction, we get $\llbracket l \rrbracket (\epsilon \bullet \mathcal{E}) \xrightarrow{\mathcal{E}}_{\text{ev}} \llbracket c \rrbracket$, but we want $\llbracket l[\epsilon] \rrbracket (\mathcal{E}) \xrightarrow{\mathcal{E}}_{\text{ev}} \llbracket c \rrbracket$. We get the result by Lemma 12 if $\mathcal{E} = !\phi$, and by Lemma 8 if $\mathcal{E} = *$.

**lam** In the case $\mathcal{E} = *$, we need Lemma 8 to conclude.

**lamβ** We want $\llbracket \lambda.l \rrbracket (\epsilon) \xrightarrow{\mathcal{E}}_{\text{ev}} \llbracket \mathcal{E} \langle l[k \cdot \epsilon] \rangle \rrbracket$ (where we might have $\epsilon = \text{id}$), i.e., $\lambda.\llbracket l \rrbracket (\uparrow\epsilon) \xrightarrow{\mathcal{E}}_{\text{ev}} \llbracket \mathcal{E} \langle l[k \cdot \epsilon] \rangle \rrbracket$. We have $\lambda.\llbracket l \rrbracket (\uparrow\epsilon) \xrightarrow{\mathcal{E}}_{\text{ev}} \llbracket \mathcal{E} \langle l \rangle (\uparrow\epsilon) \{ \llbracket k \rrbracket / 0 \} \rangle$. We conclude with Lemmas 13 and 16.

**Lemma 19.** Let $t \xrightarrow{\mathcal{E}}_{\text{ev}} s$. For all $l, \mathcal{E}$ such that $\llbracket l \rrbracket (\mathcal{E}) = t$, for all $\mathcal{E}'$ such that $\llbracket \mathcal{E}' \rrbracket = \mathcal{E}$, there exists $c$ such that $l \xrightarrow{\mathcal{E}', \mathcal{E}}_{\text{ev}} c$ and $\llbracket c \rrbracket = s$.

For all $n, \epsilon, \mathcal{E}$ such that $\llbracket \llbracket n \rrbracket (\epsilon) \rrbracket (\mathcal{E}) = t$, for all $\mathcal{E}'$ such that $\llbracket \mathcal{E}' \rrbracket = \mathcal{E}$, there exists $c$ such that $\epsilon \xrightarrow{\mathcal{E}', n, \mathcal{E}}_{\text{var}} c$ and $\llbracket c \rrbracket = s$.

**Proof.** We define an ordering on couples $(l, \mathcal{E})$ and triples $(n, \epsilon, \mathcal{E})$ as follows.

- $(l, \mathcal{E}) > (k, \mathcal{F})$ if $f_1(l)(f_2(\mathcal{E}) + 1) > f_1(k)(f_2(\mathcal{F}) + 1)$;

- $(l, \mathcal{E}) > (n, \epsilon, \mathcal{F})$ if $f_1(l)(f_2(\mathcal{E}) + 1) > f_2(\epsilon)(f_2(\mathcal{F}) + 1)$;

- $(n, \epsilon, \mathcal{E}) > (l, \mathcal{F})$ if $f_2(\epsilon)(f_2(\mathcal{E}) + 1) > f_1(l)(f_2(\mathcal{F}) + 1)$;

- $(n, \epsilon, \mathcal{E}) > (n, \phi, \mathcal{F})$ if $f_2(\epsilon)(f_2(\mathcal{E}) + 1) > f_2(\phi)(f_2(\mathcal{F}) + 1)$.

where

$$ 
\begin{aligned}
f_1(l[\epsilon]) &\triangleq f_1(l_1)(f_2(\epsilon) + 1) & f_2(\star) &\triangleq 1 \\
f_1(l_1 l_2) &\triangleq f_1(l_1) + f_1(l_2) + 1 & f_2(!\epsilon) &\triangleq f_2(\epsilon) \\
f_1(\lambda.l) &\triangleq 4f_1(l) & f_2(\text{id}) &\triangleq 2 \\
f_1(n) &\triangleq 3 & f_2(\uparrow) &\triangleq 2 \\
& & f_2(l \cdot \epsilon) &\triangleq f_1(l) + f_2(\epsilon) \\
& & f_2(\uparrow\epsilon) &\triangleq 3f_2(\epsilon) \\
& & f_2(\epsilon_1 \circ \epsilon_2) &\triangleq f_2(\epsilon_1)(f_2(\epsilon_2) + 1)
\end{aligned}
$$
The sizes have been chosen to be strictly decreasing between the conclusion and the premise of a ZS rule.

We prove the two items simultaneously by induction on <. Let $t \xrightarrow{\mathbb{E}}_{\text{ev}} s$.

Let $l, \mathcal{E}$ such that $[[l]](\mathcal{E}) = t$, and $\mathbb{F}$ such that $[[\mathbb{F}]] = \mathbb{E}$.

If $l = n$, then $\mathcal{E} = !\epsilon$ for some $\epsilon$, because $[[l]](\mathcal{E})$ makes a transition and there is no transition for variable in the substitution world. Because $f_1(n)(f_2(\epsilon) + 1) > f_2(\epsilon)(f_2(\star) + 1)$, we can apply the induction hypothesis on $(n, \epsilon, \star)$, and there exists $c$ such that $\epsilon \xrightarrow{\mathbb{F},n,\mathcal{E}}_{\text{var}} c$ and $[[c]] = s$. We then conclude by applying rule **consZ**.

If $l = l'[c]$, then $t = [[l]](\mathcal{E}) = [[[[l']](\epsilon)]](\mathcal{E}) = [[l']](\epsilon \bullet \mathcal{E})$. Since $f_1(l'[c])(f_2(\mathcal{E}) + 1) = f_1(l')(f_2(\epsilon) + 1)(f_2(\mathcal{E}) + 1) > f_1(l')(f_2(\epsilon)(f_2(\mathcal{E}) + 1) + 1) \ge f_1(l')(f_2(\epsilon \bullet \mathcal{E}) + 1)$, we can apply the induction hypothesis on $(l', \epsilon \bullet \mathcal{E})$: there exists $c$ such that $l' \xrightarrow{\mathbb{F},\epsilon \bullet \mathcal{E}}_{\text{ev}} c$ and $[[c]] = s$; we conclude using rule **env**.

Suppose $l = l_1 l_2$; then $t = [[l_1]](\mathcal{E}) [[l_2]](\mathcal{E})$. There are two possible premises for $t \xrightarrow{\mathbb{E}}_{\text{ev}} s$. Suppose $[[l_1]](\mathcal{E}) \stackrel{\square}{\xrightarrow{[l_2]} (\mathcal{E}) \coloneqq \mathbb{E}}_{\text{ev}} s$. Because $(l_1 l_2, \mathcal{E}) > (l_1, \mathcal{E})$ and $[[\square (l_2[\mathcal{E}])] \coloneqq \mathbb{F}] = \square [[l_2]](\mathcal{E}) \coloneqq \mathbb{E}$, we can apply the induction hypothesis: there exists $c$ such that $l_1 \xrightarrow{\square (l_2[\mathcal{E}]) \coloneqq \mathbb{F}, \mathcal{E}}_{\text{ev}} c$ and $[[c]] = s$. Applying **appl**, we get $l_1 l_2 \xrightarrow{\mathbb{F}, \mathcal{E}}_{\text{ev}} c$, as wished. The other case is treated similarly.

If $l = \lambda.l'$, then $[[\lambda.l']](\mathcal{E}) = \lambda.[[l']](\upharpoonright_{\mathcal{E}} \lambda) = \lambda.t$. We have two possibilities. The inductive case is treated like the application case. Otherwise, the transition $t \xrightarrow{\mathbb{E}}_{\text{ev}} s$ comes from $\lambda.t' \stackrel{\square s' \coloneqq \mathbb{E}'}{\xrightarrow{[s']}}_{\text{ev}} \mathbb{E}\langle t'\{s'/0\} \rangle$ with $t = \lambda.t'$ and $\mathbb{E} = \square s' \coloneqq \mathbb{E}'$. Because $[[\mathbb{F}]] = \mathbb{E}$, there exist $k, \mathbb{F}'$ such that $\mathbb{F} = \square k \coloneqq \mathbb{F}'$, $[[k]] = s'$, and $[[\mathbb{F}]] = \mathbb{E}'$. By **lamβ**, we have $\lambda.l' \stackrel{\square k \coloneqq \mathbb{F}', \mathcal{E}}{\xrightarrow{[k']}}_{\text{ev}} \mathbb{F}'\langle l'[(k \cdot \mathcal{E})] \rangle$. To conclude, we need $[[\mathbb{E}'\langle l'[(k \cdot \mathcal{E})] \rangle]] = \mathbb{E}\langle t'\{s'/0\} \rangle$. By **Lemmas 13 and 16**, $[[\mathbb{E}'\langle l'[(k \cdot \mathcal{E})] \rangle]] = [[\mathbb{E}']\langle l'[(k \cdot \mathcal{E})] \rangle] = [[\mathbb{E}']\langle l'[(k \cdot \mathcal{E})] \rangle/0] = \mathbb{E}\langle t'\{s'/0\} \rangle$, hence the result holds.

Let $n, \epsilon, \mathcal{E}$ such that $[[[n]](\epsilon)](\mathcal{E}) = t$. We proceed by case analysis on $\epsilon$.

If $\epsilon = \text{id}$, then $\mathcal{E} = !\epsilon'$ for some $\epsilon'$, because $t$ cannot be a variable. Because $(n, \text{id}, !\epsilon') > (n, \epsilon', \star)$ and $[[[[n]](\epsilon')](\star) = [[[[n]](\epsilon')](\text{id}) = [[[[n]](\text{id})](!\epsilon') = t$, we can apply the induction hypothesis on $(n, \epsilon', \star)$ to obtain $c$ such that $\epsilon \xrightarrow{\mathbb{E}', n, \star} \text{var} c$ and $[[c]] = s$. We apply rule **id!** to conclude.

Suppose $\epsilon = k \cdot \epsilon'$ and $n = 0$. Because $(0, \epsilon, \mathcal{E}) > (k, \mathcal{E})$ and $[[[[0]](\epsilon)](\mathcal{E}) = [[k]](\mathcal{E}) = t$, we can apply the induction hypothesis on $(k, \mathcal{E})$ to obtain $c$ such that $k \xrightarrow{\mathbb{E}', \mathcal{E}}_{\text{ev}} c$ and $[[c]] = s$. We apply rule **consZ** to conclude.

The remaining cases are similar.

# B Correspondence Between the DAM and the OAM

The main differences between closures in the OAM and DAM machine states is that some environments $l[c]$ in the DAM may be pushed to the leaves in the OAM, and that some variables $n$ may be solved in the OAM but not in the DAM. These discrepancies can be erased by adapting the translation to terms $[\cdot]$ of Figure 3, which pushes all the environments to the leaves and solve all the variables. Closures in OAM states may also have more annotations than in their DAM counterparts, because annotations are erased after $\beta$-reduction in the DAM, but some of these extra annotations may be meaningless.

We adapt the translation of Figure 3 to our current problem. We define two translations $[[l]]_o(\mathcal{E})$ on the OAM side $[[l]]_d(\mathcal{E})$ and the DAM side which go through $l$ to push the envi-
The sizes have been chosen to be strictly decreasing between the conclusion and the premise of a ZS rule.

We prove the two items simultaneously by induction on <. Let $t \xrightarrow{\mathbb{E}}_{\text{ev}} s$.

Let $l, \mathcal{E}$ such that $[[l]](\mathcal{E}) = t$, and $\mathbb{F}$ such that $[[\mathbb{F}]] = \mathbb{E}$.

If $l = n$, then $\mathcal{E} = !\epsilon$ for some $\epsilon$, because $[[l]](\mathcal{E})$ makes a transition and there is no transition for variable in the substitution world. Because $f_1(n)(f_2(\epsilon) + 1) > f_2(\epsilon)(f_2(\star) + 1)$, we can apply the induction hypothesis on $(n, \epsilon, \star)$, and there exists $c$ such that $\epsilon \xrightarrow{\mathbb{F},n,\mathcal{E}}_{\text{var}} c$ and $[[c]] = s$. We then conclude by applying rule **consZ**.

If $l = l'[c]$, then $t = [[l]](\mathcal{E}) = [[[[l']](\epsilon)]](\mathcal{E}) = [[l']](\epsilon \bullet \mathcal{E})$. Since $f_1(l'[c])(f_2(\mathcal{E}) + 1) = f_1(l')(f_2(\epsilon) + 1)(f_2(\mathcal{E}) + 1) > f_1(l')(f_2(\epsilon)(f_2(\mathcal{E}) + 1) + 1) \ge f_1(l')(f_2(\epsilon \bullet \mathcal{E}) + 1)$, we can apply the induction hypothesis on $(l', \epsilon \bullet \mathcal{E})$: there exists $c$ such that $l' \xrightarrow{\mathbb{F},\epsilon \bullet \mathcal{E}}_{\text{ev}} c$ and $[[c]] = s$; we conclude using rule **env**.

Suppose $l = l_1 l_2$; then $t = [[l_1]](\mathcal{E}) [[l_2]](\mathcal{E})$. There are two possible premises for $t \xrightarrow{\mathbb{E}}_{\text{ev}} s$. Suppose $[[l_1]](\mathcal{E}) \stackrel{\square}{\xrightarrow{[l_2]} (\mathcal{E}) \coloneqq \mathbb{E}}_{\text{ev}} s$. Because $(l_1 l_2, \mathcal{E}) > (l_1, \mathcal{E})$ and $[[\square (l_2[\mathcal{E}])] \coloneqq \mathbb{F}] = \square [[l_2]](\mathcal{E}) \coloneqq \mathbb{E}$, we can apply the induction hypothesis: there exists $c$ such that $l_1 \xrightarrow{\square (l_2[\mathcal{E}]) \coloneqq \mathbb{F}, \mathcal{E}}_{\text{ev}} c$ and $[[c]] = s$. Applying **appl**, we get $l_1 l_2 \xrightarrow{\mathbb{F}, \mathcal{E}}_{\text{ev}} c$, as wished. The other case is treated similarly.

If $l = \lambda.l'$, then $[[\lambda.l']](\mathcal{E}) = \lambda.[[l']](\upharpoonright_{\mathcal{E}}) = \lambda.t$. We have two possibilities. The inductive case is treated like the application case. Otherwise, the transition $t \xrightarrow{\mathbb{E}}_{\text{ev}} s$ comes from $\lambda.t' \stackrel{\square s' \coloneqq \mathbb{E}'}{\xrightarrow{[s']}}_{\text{ev}} \mathbb{E}\langle t'\{s'/0\} \rangle$ with $t = \lambda.t'$ and $\mathbb{E} = \square s' \coloneqq \mathbb{E}'$. Because $[[\mathbb{F}]] = \mathbb{E}$, there exist $k, \mathbb{F}'$ such that $\mathbb{F} = \square k \coloneqq \mathbb{F}'$, $[[k]] = s'$, and $[[\mathbb{F}]] = \mathbb{E}'$. By **lamβ**, we have $\lambda.l' \stackrel{\square k \coloneqq \mathbb{F}', \mathcal{E}}{\xrightarrow{[k']}}_{\text{ev}} \mathbb{F}'\langle l'[(k \cdot \mathcal{E})] \rangle$. To conclude, we need $[[\mathbb{E}'\langle l'[(k \cdot \mathcal{E})] \rangle]] = \mathbb{E}\langle t'\{s'/0\} \rangle$. By **Lemmas 13 and 16**, $[[\mathbb{E}'\langle l'[(k \cdot \mathcal{E})] \rangle]] = [[\mathbb{E}']\langle [[l']](\upharpoonright_{\mathcal{E}}) \{[[k]]/0\} \rangle = \mathbb{E}\langle t'\{s'/0\} \rangle$, hence the result holds.

Let $n, \epsilon, \mathcal{E}$ such that $[[[n]](\epsilon)](\mathcal{E}) = t$. We proceed by case analysis on $\epsilon$.

If $\epsilon = \text{id}$, then $\mathcal{E} = !\epsilon'$ for some $\epsilon'$, because $t$ cannot be a variable. Because $(n, \text{id}, !\epsilon') > (n, \epsilon', \star)$ and $[[[[n]](\epsilon')]](\star) = [[[[n]](\epsilon')]](\text{id}) = [[[[n]](\text{id})]](!\epsilon') = t$, we can apply the induction hypothesis on $(n, \epsilon', \star)$ to obtain $c$ such that $\epsilon \xrightarrow{\mathbb{E}', n, \star} \text{var} c$ and $[[c]] = s$. We apply rule **id!** to conclude.

Suppose $\epsilon = k \cdot \epsilon'$ and $n = 0$. Because $(0, \epsilon, \mathcal{E}) > (k, \mathcal{E})$ and $[[[[0]](\epsilon)]](\mathcal{E}) = [[k]](\mathcal{E}) = t$, we can apply the induction hypothesis on $(k, \mathcal{E})$ to obtain $c$ such that $k \xrightarrow{\mathbb{E}', \mathcal{E}}_{\text{ev}} c$ and $[[c]] = s$. We apply rule **consZ** to conclude.

The remaining cases are similar.

# B Correspondence Between the DAM and the OAM

The main differences between closures in the OAM and DAM machine states is that some environments $l[c]$ in the DAM may be pushed to the leaves in the OAM, and that some variables $n$ may be solved in the OAM but not in the DAM. These discrepancies can be erased by adapting the translation to terms $[\cdot]$ of Figure 3, which pushes all the environments to the leaves and solve all the variables. Closures in OAM states may also have more annotations than in their DAM counterparts, because annotations are erased after $\beta$-reduction in the DAM, but some of these extra annotations may be meaningless.

We adapt the translation of Figure 3 to our current problem. We define two translations $[[l]]_o(\mathcal{E})$ on the OAM side $[[l]]_d(\mathcal{E})$ and the DAM side which go through $l$ to push the environment
ronments to the leaves. On the OAM side, it also keeps the meaningful annotations, and discards the others. To do so, we use a translation $[[l]]_o^b(\epsilon)$ where $b \in \{\top, \bot\}$ is a boolean remembering whether the environment $\mathcal{E}$ is $\star$ or not. We define $?\Sigma$ as $\Sigma$ if $\Sigma = \text{ev}$ and $b = \top$, and as $\emptyset$ otherwise.

$$[[l]]_o(\star) \triangleq [[l]]_o^\top(\text{id})$$

$$[[l]]_o(\!\epsilon) \triangleq [[l]]_o^\perp(\epsilon)$$

$$[[l[\epsilon_1]^\Sigma]]_o^b(\epsilon_2) \triangleq [[l]]_o^\perp(\epsilon_1 \circ \epsilon_2) \text{ if } l \neq n$$

$$[[n[\epsilon_1]^\Sigma]]_o^b(\epsilon_2) \triangleq (n, \epsilon_1 \circ \epsilon_2, ?\Sigma)$$

$$[[l_1 @^\Sigma l_2]]_o^b(\epsilon) \triangleq [[l_1]]_o^b(\epsilon) @^{?\Sigma} [[l_2]]_o^b(\epsilon)$$

$$[[\lambda^\Sigma .l]]_o^b(\epsilon) \triangleq \lambda^{?\Sigma} .[[l]]_o^b(\top\epsilon)$$

$$[[n]]_o^b(\epsilon) \triangleq (n, \epsilon, \emptyset)$$

$$[[l]]_d(\star) \triangleq [[l]]_d(\text{id})$$

$$[[l]]_d(\!\epsilon) \triangleq [[l]]_d(\epsilon)$$

$$[[l[\epsilon_1]^\Sigma]]_d(\epsilon_2) \triangleq [[l]]_d(\epsilon_1 \circ \epsilon_2)$$

$$[[l_1 @^\Sigma l_2]]_d(\epsilon) \triangleq [[l_1]]_d(\epsilon) @^\Sigma [[l_2]]_d(\epsilon)$$

$$[[\lambda^\Sigma .l]]_d(\epsilon) \triangleq \lambda^{?\Sigma} .[[l]]_d(\top\epsilon)$$

$$[[n^\Sigma]]_d(\epsilon) \triangleq (n, \epsilon, \Sigma)$$

The two translations produce similar results, denoted $r_o$ and $r_d$, which mirrors the initial annotated term or closure $l$, except the variables are turned into triples $(n, \epsilon, \Sigma)$ containing the variable itself, the environment for it, and its annotation. We recall that variables are not directly annotated in the OAM, but may be annotated when paired with an environment $n[\epsilon]^\Sigma$.

We check that $r_o$ contains more annotations than $r_d$ with the predicate $r_o \triangleright r_d$, defined below. We use two operations $\|(n, \epsilon, \Sigma)\|_o$ and $\|(n, \epsilon, \Sigma)\|_d$ which solves $n$ in $\epsilon$ with the usual steps, the result being a pair $(l, \mathcal{E})$ or a variable $m$. The operation $\|(n, \epsilon, \Sigma)\|_d$ also checks that the annotations of $\epsilon$ correspond to $\Sigma$: $\text{an}(\epsilon) = \text{var}$ iff $\Sigma = \text{ev}$.

$$\frac{r_o^1 \triangleright r_d^1 \quad r_o^2 \triangleright r_d^2 \quad \Sigma \supseteq \Delta}{r_o^1 @^\Sigma r_o^2 \triangleright r_d^1 @^\Delta r_d^2}$$

$$\frac{r_o \triangleright r_d \quad \Sigma \supseteq \Delta}{\lambda^\Sigma .r_o \triangleright \lambda^\Delta .r_d}$$

$$\frac{r_o \neq (n, \epsilon, \Sigma) \quad \|(n, \phi, \Delta)\|_d = (k, \mathcal{F}) \quad r_o \triangleright [[k]]_d(\mathcal{F})}{r_o \triangleright (n, \phi, \Delta)}$$

$$\frac{\|(n, \epsilon, \Sigma)\|_o = \|(n, \phi, \Delta)\|_d = m \quad \Sigma \supseteq \Delta}{(n, \epsilon, \Sigma) \triangleright (n, \phi, \Delta)}$$

$$\frac{\|(n, \epsilon, \Sigma)\|_o = (l, \mathcal{E}) \quad \|(n, \phi, \Delta)\|_d = (k, \mathcal{F}) \quad [[l]]_o(\mathcal{E}) \triangleright [[k]]_d(\mathcal{F}) \quad \Sigma \supseteq \Delta}{(n, \epsilon, \Sigma) \triangleright (n, \phi, \Delta)}$$

We extend the translations $[[\cdot]]_o$ and $[[\cdot]]_d$ and relation $\triangleright$ to contexts frame by frame.

We define an equivalence between machine states. We have $\mathcal{O} \approx \mathcal{D}$ if either:

- $\mathcal{O} = \langle l | \mathbb{E}, \mathcal{E} \rangle_{\text{ev}}, \mathcal{D} = \langle k | \mathbb{F}, \mathcal{F}, \pi \rangle_{\text{ev}}, [[l]]_o(\mathcal{E}) \triangleright [[k]]_d(\mathcal{F}), \text{ and } [[\mathbb{E}]]_o \triangleright [[\mathbb{F}]]_d$;

- $\mathcal{O} = \langle \mathbb{E} | c \rangle_{\text{bev}}, \mathcal{D} = \langle \pi | k, \mathbb{F}, \mathcal{F} \rangle_{\text{bev}}, [[c]]_o(\star) \triangleright [[k]]_d(\mathcal{F}), \text{ and } [[\mathbb{E}]]_o \triangleright [[\mathbb{F}]]_d$;

- $\mathcal{O} = \langle c \rangle_{\text{nf}}, \mathcal{D} = \langle d \rangle_{\text{nf}}, \text{ and } [[c]]_o(\star) \triangleright [[d]]_d(\star)$.

We write $(\mathcal{O}_0, \mathcal{O}_1, \dots, \mathcal{O}_i) \approx (\mathcal{D}_0, \mathcal{D}_1, \dots, \mathcal{D}_i)$ if $\mathcal{O}_0 = \mathcal{I}_t$ and $\mathcal{D}_0 = \mathcal{I}_t$ for the same $t$, $\mathcal{O}_j \to^* \mathcal{O}_{j+1}$ and $\mathcal{D}_j \to^* \mathcal{D}_{j+1}$ for all $0 \le j < i$, $\mathcal{O}_j \approx \mathcal{D}_j$ for all $0 \le j \le i$, and for all switching step $c \to c'$ in the sequence $\mathcal{O}_0 \to^* \mathcal{O}_i$, there exists $\mathcal{O}_j$ such that $\mathcal{O}_j = c'$.

The last condition ensures that all switching steps (where annotations are added) of the OAM are matched by the DAM, adding an annotation at the same position (because
onments to the leaves. On the OAM side, it also keeps the meaningful annotations, and discards the others. To do so, we use a translation $[[l]]_o^b(\epsilon)$ where $b \in \{\top, \bot\}$ is a boolean remembering whether the environment $\mathcal{E}$ is $\star$ or not. We define $?\Sigma$ as $\Sigma$ if $\Sigma = \text{ev}$ and $b = \top$, and as $\emptyset$ otherwise.

$$[[l]]_o(\star) \triangleq [[l]]_o^\top(\text{id})$$

$$[[l]]_o(!\epsilon) \triangleq [[l]]_o^\perp(\epsilon)$$

$$[[l[\epsilon_1]^\Sigma]]_o^b(\epsilon_2) \triangleq [[l]]_o^\perp(\epsilon_1 \circ \epsilon_2) \text{ if } l \neq n$$

$$[[n[\epsilon_1]^\Sigma]]_o^b(\epsilon_2) \triangleq (n, \epsilon_1 \circ \epsilon_2, ?\Sigma)$$

$$[[l_1 @^\Sigma l_2]]_o^b(\epsilon) \triangleq [[l_1]]_o^b(\epsilon) @^{?\Sigma} [[l_2]]_o^b(\epsilon)$$

$$[[\lambda^\Sigma . l]]_o^b(\epsilon) \triangleq \lambda^{?\Sigma} . [[l]]_o^b(\hat{\top}\epsilon)$$

$$[[n]]_o^b(\epsilon) \triangleq (n, \epsilon, \emptyset)$$

$$[[l]]_d(\star) \triangleq [[l]]_d(\text{id})$$

$$[[l]]_d(!\epsilon) \triangleq [[l]]_d(\epsilon)$$

$$[[l[\epsilon_1]^\Sigma]]_d(\epsilon_2) \triangleq [[l]]_d(\epsilon_1 \circ \epsilon_2)$$

$$[[l_1 @^\Sigma l_2]]_d(\epsilon) \triangleq [[l_1]]_d(\epsilon) @^\Sigma [[l_2]]_d(\epsilon)$$

$$[[\lambda^\Sigma . l]]_d(\epsilon) \triangleq \lambda^{?\Sigma} . [[l]]_d(\hat{\top}\epsilon)$$

$$[[n^\Sigma]]_d(\epsilon) \triangleq (n, \epsilon, \Sigma)$$

The two translations produce similar results, denoted $r_o$ and $r_d$, which mirrors the initial annotated term or closure $l$, except the variables are turned into triples $(n, \epsilon, \Sigma)$ containing the variable itself, the environment for it, and its annotation. We recall that variables are not directly annotated in the OAM, but may be annotated when paired with an environment $n[\epsilon]^\Sigma$.

We check that $r_o$ contains more annotations than $r_d$ with the predicate $r_o \triangleright r_d$, defined below. We use two operations $\|(n, \epsilon, \Sigma)\|_o$ and $\|(n, \epsilon, \Sigma)\|_d$ which solves $n$ in $\epsilon$ with the usual steps, the result being a pair $(l, \mathcal{E})$ or a variable $m$. The operation $\|(n, \epsilon, \Sigma)\|_d$ also checks that the annotations of $\epsilon$ correspond to $\Sigma$: $\text{an}(\epsilon) = \text{var}$ iff $\Sigma = \text{ev}$.

$$\frac{r_o^1 \triangleright r_d^1 \quad r_o^2 \triangleright r_d^2 \quad \Sigma \supseteq \Delta}{r_o^1 @^\Sigma r_o^2 \triangleright r_d^1 @^\Delta r_d^2}$$

$$\frac{r_o \triangleright r_d \quad \Sigma \supseteq \Delta}{\lambda^\Sigma . r_o \triangleright \lambda^\Delta . r_d}$$

$$\frac{r_o \neq (n, \epsilon, \Sigma) \quad \|(n, \phi, \Delta)\|_d = (k, \mathcal{F}) \quad r_o \triangleright [[k]]_d(\mathcal{F})}{r_o \triangleright (n, \phi, \Delta)}$$

$$\frac{\|(n, \epsilon, \Sigma)\|_o = \|(n, \phi, \Delta)\|_d = m \quad \Sigma \supseteq \Delta}{(n, \epsilon, \Sigma) \triangleright (n, \phi, \Delta)}$$

$$\frac{\|(n, \epsilon, \Sigma)\|_o = (l, \mathcal{E}) \quad \|(n, \phi, \Delta)\|_d = (k, \mathcal{F}) \quad [[l]]_o(\mathcal{E}) \triangleright [[k]]_d(\mathcal{F}) \quad \Sigma \supseteq \Delta}{(n, \epsilon, \Sigma) \triangleright (n, \phi, \Delta)}$$

We extend the translations $[[\cdot]]_o$ and $[[\cdot]]_d$ and relation $\triangleright$ to contexts frame by frame.

We define an equivalence between machine states. We have $\mathcal{O} \approx \mathcal{D}$ if either:

- $\mathcal{O} = \langle l | \mathbb{E}, \mathcal{E} \rangle_{\text{ev}}, \mathcal{D} = \langle k | \mathbb{F}, \mathcal{F}, \pi \rangle_{\text{ev}}, [[l]]_o^b(\mathcal{E}) \triangleright [[k]]_d(\mathcal{F}), \text{ and } [[\mathcal{E}]]_o \triangleright [[\mathbb{F}]]_d$;

- $\mathcal{O} = \langle \mathbb{E} | c \rangle_{\text{bev}}, \mathcal{D} = \langle \pi | k, \mathbb{F}, \mathcal{F} \rangle_{\text{bev}}, [[c]]_o^b(\star) \triangleright [[k]]_d(\mathcal{F}), \text{ and } [[\mathcal{E}]]_o \triangleright [[\mathbb{F}]]_d$;

- $\mathcal{O} = \langle c \rangle_{\text{nf}}, \mathcal{D} = \langle d \rangle_{\text{nf}}, \text{ and } [[c]]_o^b(\star) \triangleright [[d]]_d(\star)$.

We write $(\mathcal{O}_0, \mathcal{O}_1, \dots, \mathcal{O}_i) \approx (\mathcal{D}_0, \mathcal{D}_1, \dots, \mathcal{D}_i)$ if $\mathcal{O}_0 = \mathcal{I}_t$ and $\mathcal{D}_0 = \mathcal{I}_t$ for the same $t$, $\mathcal{O}_j \to^* \mathcal{O}_{j+1}$ and $\mathcal{D}_j \to^* \mathcal{D}_{j+1}$ for all $0 \le j < i$, $\mathcal{O}_j \approx \mathcal{D}_j$ for all $0 \le j \le i$, and for all switching step $c \to c'$ in the sequence $\mathcal{O}_0 \to^* \mathcal{O}_i$, there exists $\mathcal{O}_j$ such that $\mathcal{O}_j = c'$.

The last condition ensures that all switching steps (where annotations are added) of the OAM are matched by the DAM, adding an annotation at the same position (because
contexts between related states must have the same shape). However, there are switching
steps from the DAM which are not matched by the OAM.

**Lemma 20.** Let $\mathcal{O} \approx \mathcal{D}$ such that $\mathcal{O} = \langle l | \mathbb{E}, \mathcal{E} \rangle_{\text{ev}}$.

If $[[l]]_o(\mathcal{E}) = l_1 @^\emptyset l_2$, there exists $\mathcal{D}'$ such that $\mathcal{D}' = \langle k_1 @^\emptyset k_2 | \mathbb{F}, \mathcal{F}', \pi' \rangle_{\text{ev}}$, $\mathcal{D} \to^* \mathcal{D}'$, and
$\mathcal{O} \approx \mathcal{D}'$;

A similar result holds if $[[l]]_o(\mathcal{E}) = \lambda^\emptyset.l'$ or $[[l]]_o(\mathcal{E}) = (n, \epsilon, \emptyset)$.

**Proof.** Let $\mathcal{D} = \langle k | \mathbb{F}, \mathcal{F}, \pi \rangle_{\text{ev}}$. Assume $[[l]]_o(\mathcal{E}) = l_1 @^\emptyset l_2$. Because $[[l]]_o(\mathcal{E}) \triangleright [[k]](\mathcal{F})$, there exist $k_1$ and $k_2$ such that $[[k]]_d(\mathcal{F}) = k_1 @^\emptyset k_2$. We prove that the derivation exists by induction on the number of steps required to compute $[[k]]_d(\mathcal{F}) = k_1 @^\emptyset k_2$. If that number is 0, then $k$ is an application and the result holds by picking $\mathcal{D}' = \mathcal{D}$.

Otherwise, we distinguish cases based on $k$. If $k = k'[\phi]^\Delta$, then $[[k]]_d(\mathcal{F}) = [[k')]_d(\phi[\mathcal{F}])$, so $[[l]]_o(\mathcal{E}) \triangleright [[k']](\phi[\mathcal{F}])$ holds. The step $\mathcal{D} \to \langle k' | \mathbb{F}, \phi[\mathcal{F}], \pi'' \rangle_{\text{ev}}$ is possible for some $\pi''$, otherwise $k'$ would be annotated, and $k_1 @^\emptyset k_2$ as well. We have $\mathcal{O} \approx \langle k' | \mathbb{F}, \phi[\mathcal{F}], \pi'' \rangle_{\text{ev}}$, and $[[k']]_d(\phi[\mathcal{F}]) = k_1 @^\emptyset k_2$ with one less step, so by induction, there exists $\mathcal{D}'$ as wished such that $\langle k' | \mathbb{F}, \phi[\mathcal{F}], \pi'' \rangle_{\text{ev}} \to^* \mathcal{D}'$, from which we conclude $\mathcal{D} \to^* \mathcal{D}'$.

If $k = m^\Delta$, then $\|(m, \mathcal{F}, \Delta)\|_d = (d, \mathcal{F}'')$ and $[[d]]_d(\mathcal{F}'') = k_1 @^\emptyset k_2$. Therefore $d$ is not annotated, $\Delta$ must be empty, and the environment in $\mathcal{F}''$ is not annotated: the sequence $\mathcal{D} \to^* \langle d | \mathbb{F}, \mathcal{F}'', \pi'' \rangle_{\text{ev}}$ is possible for some $\pi''$. We have $\mathcal{O} \approx \langle d | \mathbb{F}, \mathcal{F}'', \pi'' \rangle_{\text{ev}}$, and by induction, there exists $\mathcal{D}'$ as wished such that $\langle d | \mathbb{F}, \mathcal{F}'', \pi'' \rangle_{\text{ev}} \to^* \mathcal{D}'$. We then conclude $\mathcal{D} \to^* \mathcal{D}'$.

The abstraction and variable cases are similar.

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

**Lemma 21.** Let $\mathcal{O} \approx \mathcal{D}$ such that $\mathcal{O} = \langle \mathbb{E} | c \rangle_{\text{bev}}$.

If $\mathbb{E} = \square l' :: \mathbb{E}'$, there exists $\mathcal{D}'$ such that $\mathcal{D}' = \langle \text{appl} :: \pi' | l_1, \square (l_2[\mathcal{F}']) :: \mathbb{F}', \mathcal{F}' \rangle_{\text{bev}}$, $\mathcal{D} \to^* \mathcal{D}'$, and $\mathcal{O} \approx \mathcal{D}'$;

A similar result holds if $\mathbb{E} = l' \square :: \mathbb{E}'$, $\mathbb{E} = \lambda :: \mathbb{E}'$, or $\mathbb{E} = \blacksquare$.

**Proof.** We detail only the first item, the other cases are similar. Let $\mathcal{D} = \langle \pi | l, \mathbb{F}, \mathcal{F} \rangle_{\text{bev}}$. Because $[[\mathbb{E}]]_o \triangleright [[\mathbb{F}]]_d$, we have $\mathbb{F} = \square (l_2[\mathcal{F}']) :: \mathbb{F}'$ and $\pi$ is of the shape $\pi''++ \text{appl} :: \pi'$. When we apply the rule `appl` in the DAM, the annotation set $\Delta$ must be empty for a valid configuration, so $\Delta = \emptyset$. We proceed by induction on the size of $\pi''$. If $\pi''$ is empty, then pick $\mathcal{D}' = \mathcal{D}$ and the result holds. Otherwise, we distinguish two cases.

Suppose $\pi = \text{env}(\epsilon) :: \pi''''$. Then $\mathcal{D} \to \langle l[\epsilon]^{\Delta'} | \mathbb{F}, \mathcal{F}''', \pi''' \rangle_{\text{ev}} \stackrel{\Delta}{=} \mathcal{D}_1$ with $\mathcal{F} = \epsilon \bullet \mathcal{F}''$. Because $\mathcal{D}$ is a backward configuration, we know $l$ is annotated, and $\mathcal{D}_1$ can only do a switching step $\mathcal{D}_1 \to \langle \pi''' | l[\epsilon]^{\text{ev}}, \mathbb{F}, \mathcal{F}'' \rangle_{\text{bev}} \stackrel{\Delta}{=} \mathcal{D}_2$. We have $[[l[\epsilon]^{\text{ev}}]]_d(\mathcal{F}'') = [[l]]_d(\epsilon \bullet \mathcal{F}'') = [[l]]_d(\mathcal{F})$, hence we have $[[c]]_o(\star) \triangleright [[l[\epsilon]^{\text{ev}}]]_d(\mathcal{F}'')$ and $\mathcal{O} \approx \mathcal{D}_2$. We apply the induction hypothesis to $\mathcal{D}_2$ to conclude.

Suppose $\pi = \text{cons0}(\epsilon) :: \pi''''$. Then $\mathcal{D} \to \langle l \cdot \Delta' \epsilon | \mathbb{F}, 0, \mathcal{F}, \pi''' \rangle_{\text{var}} \stackrel{\Delta}{=} \mathcal{D}_1$. Because $\mathcal{D}$ is a backward configuration, we know $l$ is annotated, and $\mathcal{D}_1$ can only do a switching step $\mathcal{D}_1 \to \langle \pi''' | \epsilon^{+\text{var}}, \mathbb{F}, 0, \mathcal{F} \rangle_{\text{bvar}}$. In fact, there exists a sequence $\mathcal{D}_1 \to^* \langle \pi^{(4)} | n^{\text{ev}}, \mathbb{F}, !\phi \rangle_{\text{bev}} \stackrel{\Delta}{=} \mathcal{D}_2$ which undoes all the `var` steps. Because $\|(n, \phi, \text{ev})\|_d = (l, \mathcal{F})$ and $[[c]]_o(\star) \triangleright [[l]]_d(\mathcal{F})$, we have $[[c]]_o(\star) \triangleright [[n^{\text{ev}}]]_d(!\phi)$ and therefore $\mathcal{O} \approx \mathcal{D}_2$. We apply the induction hypothesis to $\mathcal{D}_2$ to conclude.

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

We write $\|r_o\|$ or $\|r_d\|$ for the forcing of $r_o$ or $r_d$, where the variable triples are solved.
We extend $[\cdot]$ to annotated terms and closures so that it ignores the annotations.

**Lemma 22.** For all $l, \mathcal{E}$, we have $\|[[l]]_o(\mathcal{E})\| = [[l]](\mathcal{E})$ and $\|[[l]]_d(\mathcal{E})\| = [[l]](\mathcal{E})$.
contexts between related states must have the same shape). However, there are switching
steps from the DAM which are not matched by the OAM.

**Lemma 20.** Let $\mathcal{O} \approx \mathcal{D}$ such that $\mathcal{O} = \langle l | \mathbb{E}, \mathcal{E} \rangle_{\mathrm{ev}}$.

■ If $[[l]]_o(\mathcal{E}) = l_1 @^\emptyset l_2$, there exists $\mathcal{D}'$ such that $\mathcal{D}' = \langle k_1 @^\emptyset k_2 | \mathbb{F}, \mathcal{F}', \pi' \rangle_{\mathrm{ev}}$, $\mathcal{D} \to^* \mathcal{D}'$, and $\mathcal{O} \approx \mathcal{D}'$;

■ A similar result holds if $[[l]]_o(\mathcal{E}) = \lambda^\emptyset.l'$ or $[[l]]_o(\mathcal{E}) = (n, \epsilon, \emptyset)$.

**Proof.** Let $\mathcal{D} = \langle k | \mathbb{F}, \mathcal{F}, \pi \rangle_{\mathrm{ev}}$. Assume $[[l]]_o(\mathcal{E}) = l_1 @^\emptyset l_2$. Because $[[l]]_o(\mathcal{E}) \triangleright [[k]](\mathcal{F})$, there exist $k_1$ and $k_2$ such that $[[k]]_d(\mathcal{F}) = k_1 @^\emptyset k_2$. We prove that the derivation exists by induction on the number of steps required to compute $[[k]]_d(\mathcal{F}) = k_1 @^\emptyset k_2$. If that number is 0, then $k$ is an application and the result holds by picking $\mathcal{D}' = \mathcal{D}$.

Otherwise, we distinguish cases based on $k$. If $k = k'[\phi]^\Delta$, then $[[k]]_d(\mathcal{F}) = [[k')]_d(\phi[\mathcal{F}])$, so $[[l]]_o(\mathcal{E}) \triangleright [[k']](\phi[\mathcal{F}])$ holds. The step $\mathcal{D} \to \langle k' | \mathbb{F}, \phi[\mathcal{F}], \pi'' \rangle_{\mathrm{ev}}$ is possible for some $\pi''$, otherwise $k'$ would be annotated, and $k_1 @^\emptyset k_2$ as well. We have $\mathcal{O} \approx \langle k' | \mathbb{F}, \phi[\mathcal{F}], \pi'' \rangle_{\mathrm{ev}}$, and $[[k']]_d(\phi[\mathcal{F}]) = k_1 @^\emptyset k_2$ with one less step, so by induction, there exists $\mathcal{D}'$ as wished such that $\langle k' | \mathbb{F}, \phi[\mathcal{F}], \pi'' \rangle_{\mathrm{ev}} \to^* \mathcal{D}'$, from which we conclude $\mathcal{D} \to^* \mathcal{D}'$.

If $k = m^\Delta$, then $\|(m, \mathcal{F}, \Delta)\|_d = (d, \mathcal{F}'')$ and $[[d]]_d(\mathcal{F}'') = k_1 @^\emptyset k_2$. Therefore $d$ is not annotated, $\Delta$ must be empty, and the environment in $\mathcal{F}''$ is not annotated: the sequence $\mathcal{D} \to^* \langle d | \mathbb{F}, \mathcal{F}'', \pi'' \rangle_{\mathrm{ev}}$ is possible for some $\pi''$. We have $\mathcal{O} \approx \langle d | \mathbb{F}, \mathcal{F}'', \pi'' \rangle_{\mathrm{ev}}$, and by induction, there exists $\mathcal{D}'$ as wished such that $\langle d | \mathbb{F}, \mathcal{F}'', \pi'' \rangle_{\mathrm{ev}} \to^* \mathcal{D}'$. We then conclude $\mathcal{D} \to^* \mathcal{D}'$.

The abstraction and variable cases are similar.

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

**Lemma 21.** Let $\mathcal{O} \approx \mathcal{D}$ such that $\mathcal{O} = \langle \mathbb{E} | c \rangle_{\mathrm{bev}}$.

■ If $\mathbb{E} = \square l' :: \mathbb{E}'$, there exists $\mathcal{D}'$ such that $\mathcal{D}' = \langle \mathrm{appl} :: \pi' | l_1, \square (l_2[\mathcal{F}']) :: \mathbb{F}', \mathcal{F}' \rangle_{\mathrm{bev}}$, $\mathcal{D} \to^* \mathcal{D}'$, and $\mathcal{O} \approx \mathcal{D}'$;

■ A similar result holds if $\mathbb{E} = l' \square :: \mathbb{E}'$, $\mathbb{E} = \lambda :: \mathbb{E}'$, or $\mathbb{E} = \blacksquare$.

**Proof.** We detail only the first item, the other cases are similar. Let $\mathcal{D} = \langle \pi | l, \mathbb{F}, \mathcal{F} \rangle_{\mathrm{bev}}$. Because $[[\mathbb{E}]]_o \triangleright [[\mathbb{F}]]_d$, we have $\mathbb{F} = \square (l_2[\mathcal{F}']) :: \mathbb{F}'$ and $\pi$ is of the shape $\pi''++ \mathrm{appl} :: \pi'$. When we apply the rule $\mathrm{appl}$ in the DAM, the annotation set $\Delta$ must be empty for a valid configuration, so $\Delta = \emptyset$. We proceed by induction on the size of $\pi''$. If $\pi''$ is empty, then pick $\mathcal{D}' = \mathcal{D}$ and the result holds. Otherwise, we distinguish two cases.

Suppose $\pi = \mathrm{env}(\epsilon) :: \pi''''$. Then $\mathcal{D} \to \langle l[\epsilon]^{\Delta'} | \mathbb{F}, \mathcal{F}''', \pi''' \rangle_{\mathrm{ev}} \stackrel{\Delta}{=} \mathcal{D}_1$ with $\mathcal{F} = \epsilon \bullet \mathcal{F}''$. Because $\mathcal{D}$ is a backward configuration, we know $l$ is annotated, and $\mathcal{D}_1$ can only do a switching step $\mathcal{D}_1 \to \langle \pi''' | l[\epsilon]^{\mathrm{ev}}, \mathbb{F}, \mathcal{F}'' \rangle_{\mathrm{bev}} \stackrel{\Delta}{=} \mathcal{D}_2$. We have $[[l[\epsilon]^{\mathrm{ev}}]]_d(\mathcal{F}'') = [[l]]_d(\epsilon \bullet \mathcal{F}'') = [[l]]_d(\mathcal{F})$, hence we have $[[c]]_o(\star) \triangleright [[l[\epsilon]^{\mathrm{ev}}]]_d(\mathcal{F}'')$ and $\mathcal{O} \approx \mathcal{D}_2$. We apply the induction hypothesis to $\mathcal{D}_2$ to conclude.

Suppose $\pi = \mathrm{cons0}(\epsilon) :: \pi''''$. Then $\mathcal{D} \to \langle l \cdot \Delta' \epsilon | \mathbb{F}, 0, \mathcal{F}, \pi''' \rangle_{\mathrm{var}} \stackrel{\Delta}{=} \mathcal{D}_1$. Because $\mathcal{D}$ is a backward configuration, we know $l$ is annotated, and $\mathcal{D}_1$ can only do a switching step $\mathcal{D}_1 \to \langle \pi''' | \epsilon^{+\mathrm{var}}, \mathbb{F}, 0, \mathcal{F} \rangle_{\mathrm{bvar}}$. In fact, there exists a sequence $\mathcal{D}_1 \to^* \langle \pi^{(4)} | n^{\mathrm{ev}}, \mathbb{F}, !\phi \rangle_{\mathrm{bev}} \stackrel{\Delta}{=} \mathcal{D}_2$ which undoes all the $\mathrm{var}$ steps. Because $\|(n, \phi, \mathrm{ev})\|_d = (l, \mathcal{F})$ and $[[c]]_o(\star) \triangleright [[l]]_d(\mathcal{F})$, we have $[[c]]_o(\star) \triangleright [[n^{\mathrm{ev}}]]_d(!\phi)$ and therefore $\mathcal{O} \approx \mathcal{D}_2$. We apply the induction hypothesis to $\mathcal{D}_2$ to conclude.

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

We write $\|r_o\|$ or $\|r_d\|$ for the forcing of $r_o$ or $r_d$, where the variable triples are solved.
We extend $[\cdot]$ to annotated terms and closures so that it ignores the annotations.

**Lemma 22.** For all $l, \mathcal{E}$, we have $\|[[l]]_o(\mathcal{E})\| = [[l]](\mathcal{E})$ and $\|[[l]]_d(\mathcal{E})\| = [[l]](\mathcal{E})$.
**Proof.** The definitions of $[[\cdot]]_o$, $[[\cdot]]_d$, and $[[\cdot]]$ are almost the same if we ignore annotations. ▶

**Lemma 23.** If $[[l]]_o(\mathcal{E}) \triangleright [[k]]_o(\mathcal{F})$, then $[[l]](\mathcal{E}) = [[k]](\mathcal{F})$.

**Proof.** We first prove the result on terms without the $l[\epsilon]^\Sigma$ construct, which is easy by induction on the derivation of $\triangleright$. We then show that $[[\cdot]]_o$ and $[[\cdot]]_d$ also preserves $[[\cdot]]$. ▶

**Lemma 24.** If $r_o \triangleright r_d^1$, $\|r_d^1\| = \|r_d^2\|$, and the annotations of $r_d^1$ and $r_d^2$ are the same, then $r_o \triangleright r_d^2$.

If $r_o^1 \triangleright r_d$, $\|r_o^1\| = \|r_o^2\|$, and the annotations of $r_o^1$ and $r_o^2$ are the same, then $r_o^2 \triangleright r_d$.

**Proof.** By induction on the derivation of the $\triangleright$ judgements. ▶

**Lemma 25.** If $[[l]]_o(\mathcal{E}) \triangleright [[k]]_d(\mathcal{F})$, then $[[l[\mathcal{E}]]_o(\star) \triangleright [[k[\mathcal{F}]]_d(\star)$.

If $r_o \triangleright [[k[\mathcal{F}]]_d(\star)$, then $r_o \triangleright [[k]]_d(\mathcal{F})$.

**Proof.** We have $\|[[l]]_o(\mathcal{E})\| = [[l]](\mathcal{E}) = [[l[\mathcal{E}]]](\star)$ and similarly for $[[k]]_d(\mathcal{F})$, so we can conclude with Lemma 24. ▶

**Lemma 26.** Let $[[\mathcal{E}]]_o \triangleright [[\mathcal{F}]]_d$, $[[l']]_o(\star) \triangleright [[k']]_o(\star)$, and $[[l]]_o(\upharpoonright \mathcal{E}) \triangleright [[k]]_d(\upharpoonright \mathcal{F})$ such that all the annotation sets are empty on the DAM side. Then $\mathbb{E}\langle l[l' \cdot \mathcal{E}]^\theta \rangle \triangleright \mathbb{F}\langle k[k' \cdot \emptyset \mathcal{F}]^\theta \rangle$.

**Proof.** We can prove that for all $l, k, \mathcal{E}, \mathcal{F}, l', k'$, and $n$, $[[l]]_o(\mathcal{E}) \triangleright [[k]]_d(\mathcal{F})$ and $[[l']]_o(\star) \triangleright [[k']_d(\star)$ imply $[[l]]_o(\mathcal{E})\{[[l']_o(\star)/n\} \triangleright [[k]]_d(\mathcal{F})\{[[k']_d(\star)/n\}$. The proof is by induction on the derivation of $[[l]]_o(\mathcal{E}) \triangleright [[k]]_d(\mathcal{F})$. The inductive cases are straightforward, and in the variable case, we either change the variable the same way on both side, or we replace it with related configurations, so the result holds.

So we have $[[l]]_o(\upharpoonright \mathcal{E})\{[[l']_o(\star)/0\} \triangleright [[k]]_d(\upharpoonright \mathcal{F})\{[[k']_o(\star)/0\}$, but then $\|[[l]]_o(\upharpoonright \mathcal{E})\{[[l']_o(\star)/0\}\| = [[l](\upharpoonright \mathcal{E})\{[[l'](\star)/0\} = [[l[l' \cdot \mathcal{E}]]\| \|[[l[l' \cdot \mathcal{E}]]\| \|[[l']^\theta \triangleright k[k' \cdot \emptyset \mathcal{F}]^\theta\| \|[[k']^\theta \triangleright k[k' \cdot \emptyset \mathcal{F}]^\theta\|$, as wished.

**Theorem 27 (OAM implies DAM).** If $(\mathcal{O}_0, \mathcal{O}_1, \dots, \mathcal{O}_i) \approx (\mathcal{D}_0, \mathcal{D}_1, \dots, \mathcal{D}_i)$ and $\mathcal{O}_i \to \mathcal{O}',$ there exist $\mathcal{O}_{i+1}$ and $\mathcal{D}_{i+1}$ such that $\mathcal{O}' \to^* \mathcal{O}_{i+1}$, $\mathcal{D}_i \to^* \mathcal{D}_{i+1}$, and $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$.

**Proof.** We proceed by case analysis on $\mathcal{O}_i \to \mathcal{O}'$.

(O1) We have $\mathcal{O}_i = \langle l_1 \upharpoonright \mathcal{S} l_2 | \mathbb{E}, \mathcal{E} \rangle_{\mathcal{E}} \to \langle l_1 | \square (l_2[\mathcal{E}]) \rangle :: \mathbb{E}, \mathcal{E} \rangle_{\mathcal{E}} = \mathcal{O}'$ with $\mathcal{E}, \upharpoonright l_1$. We pick $\mathcal{O}_{i+1} = \mathcal{O}'$. Because $\mathcal{O}_i$ is valid, $\Sigma$ cannot be a blocking annotation, and we have $[[l_1 \upharpoonright l_2]]_o(\mathcal{E}) = [[l_1]]_o(\mathcal{E}) \upharpoonright \mathcal{E} \{[[l_2]]_o(\mathcal{E})$. By Lemma 20, there exists $\mathcal{D}'$ such that $\mathcal{D}' = \langle k_1 \upharpoonright \mathcal{D} k_2 | \mathbb{F}, \mathcal{F}', \pi' \rangle_{\mathcal{E}}$, $\mathcal{D}_i \to^* \mathcal{D}'$, and $\mathcal{O}_i \approx \mathcal{D}'$. Because $\mathcal{O}_i \approx \mathcal{D}'$, we have in particular $[[l_1]]_o(\mathcal{E}) \triangleright [[k_1]]_d(\mathcal{F}')$ and $[[l_2]]_o(\mathcal{E}) \triangleright [[k_2]]_d(\mathcal{F}')$, and since $\mathcal{E}, \upharpoonright l_1$, there is no blocking annotation in $k_1$. Therefore we have $\mathcal{D}' \to \langle k_1 | \square (k_2[\mathcal{F}']) \rangle :: \mathbb{F}, \mathcal{F}', \pi'' \rangle_{\mathcal{E}} = \mathcal{D}_{i+1}$. From $[[l_2]]_o(\mathcal{E}) \triangleright [[k_2]]_d(\mathcal{F}')$, we deduce $[[l_2[\mathcal{E}]]_o \triangleright [[k_2[\mathcal{F}]]_d]$ by Lemma 25, so we have $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$.

(O2)-(O3) Similar to the case above.

(O4) We have $\mathcal{O}_i = \langle l[\epsilon]^\Sigma | \mathbb{E}, \mathcal{E} \rangle_{\mathcal{E}} \to \langle l | \mathbb{E}, \epsilon \cdot \mathcal{E} \rangle_{\mathcal{E}} = \mathcal{O}'$. We pick $\mathcal{O}_{i+1} = \mathcal{O}'$ and $\mathcal{D}_{i+1} = \mathcal{D}_i$. Because $\mathcal{O}_i \approx \mathcal{D}_i$, we have $[[l[\epsilon]^\Sigma]]_o(\mathcal{E}) \triangleright [[k]]_d(\mathcal{F})$, i.e., $[[l]]_o(\epsilon \cdot \mathcal{E}) \triangleright [[k]]_d(\mathcal{F})$, therefore $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$ holds.
(O5) Because $[[n]]_o(!\epsilon) = (n, \epsilon, \emptyset)$, by Lemma 20, there exists $\mathcal{D}'$ such that $\mathcal{D}' = \langle n^\emptyset | \mathbb{F}, \mathcal{F}', \pi' \rangle_{\text{ev}}$, $\mathcal{D}_i \to^* \mathcal{D}'$, and $\mathcal{O}_i \approx \mathcal{D}'$. In particular, we have $[[n^\emptyset]]_d(\mathcal{F}') = (n, \phi, \emptyset)$ for some $\phi$ with $(n, \epsilon, \emptyset) \triangleright (n, \phi, \emptyset)$. From there, we distinguish three cases.

Suppose $\|(n, \epsilon, \emptyset)\|_o = \|(n, \phi, \emptyset)\|_d = m$. There is a one-to-one correspondence between the equations defining $\|\cdot\|_o$ and $\|\cdot\|_d$ and the var steps of the OAM and the DAM, except for the equations returning a variable, which can be replaced by the switching step of the var mode. On the DAM side, by definition of $\|\cdot\|_d$, we are sure that the environment is not annotated because we start from a variable with no annotation. As a result, we can build sequences $\mathcal{O}_i \to^* \langle \mathbb{E} | n[\epsilon]^{\text{ev}} \rangle_{\text{bev}} \stackrel{\Delta}{=} \mathcal{O}_{i+1}$ and $\mathcal{D}_i \to^* \langle \pi' | n^{\text{ev}}, \mathbb{E}, \mathcal{F}' \rangle_{\text{bev}} \stackrel{\Delta}{=} \mathcal{D}_{i+1}$, and check that we have $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$, as wished.

Suppose $\|(n, \epsilon, \emptyset)\|_o = (l, \mathcal{E})$ with $\mathcal{E}, \text{infun}(\mathbb{F}) \nmid l$. Because $(n, \epsilon, \emptyset) \triangleright (n, \phi, \emptyset)$, there exists $(k, \mathcal{F}'')$ such that $\|(n, \phi, \emptyset)\|_o = (k, \mathcal{F}'')$ and $[[l]]_o(\mathcal{E}) \triangleright [[k]]_d(\mathcal{F}'')$. In particular, $k$ is not annotated. As in the previous subcase, we can build sequences $\mathcal{O}_i \to^* \langle l | \mathbb{E}, \mathcal{E} \rangle_{\text{ev}} \stackrel{\Delta}{=} \mathcal{O}_{i+1}$ and $\mathcal{D}_i \to^* \langle k | \mathbb{F}, \mathcal{F}'', \pi'' \rangle_{\text{ev}} \stackrel{\Delta}{=} \mathcal{D}_{i+1}$ with $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$, as wished.

Suppose $\|(n, \epsilon, \emptyset)\|_o = (l, \mathcal{E})$ with $\mathcal{E}, \text{infun}(\mathbb{F}) \vdash l$, i.e., $\mathcal{E} = \star$. Because $(n, \epsilon, \emptyset) \triangleright (n, \phi, \emptyset)$, there exists $(k, \mathcal{F}'')$ such that $\|(n, \phi, \emptyset)\|_o = (k, \mathcal{F}'')$ and $[[l]]_o(\star) \triangleright [[k]]_d(\mathcal{F}'')$. If $k$ is annotated, we conclude as in the first subcase. Otherwise, there exists $\mathcal{O}_j$ such that the annotation is added to $l$ at that point. By construction of the sequences of machine states, $\mathcal{D}_j = \langle \pi_j | k_j, \mathbb{F}_j, \mathcal{F}_j \rangle_{\text{bev}}$ also adds the annotation. Because the DAM is sound w.r.t. the ZS, $[[k_j]]_o(\star) \triangleright [[k_j]]_d(\mathcal{E}_j)$ is a normal form. We have $[[l]]_o(\star) \triangleright [[k_j]]_d(\mathcal{E}_j)$, which implies $[[l]](\star) = [[k_j]](\mathcal{E}_j)$ by Lemma 23. We also have $[[l]](\star) = [[k]](\mathcal{F}'')$, so $[[k]](\mathcal{F}'')$ is a normal form. Because the DAM is complete w.r.t. the ZS, there exists a sequence $\langle k | \mathbb{F}, \mathcal{F}'', \pi'' \rangle_{\text{ev}} \to^* \langle \pi'' | k^{+\text{ev}}, \mathbb{F}, \mathcal{F}' \rangle_{\text{bev}}$, and then $\langle \pi'' | k^{+\text{ev}}, \mathbb{F}, \mathcal{F}' \rangle_{\text{bev}} \to^* \langle \pi' | n^{\text{ev}}, \mathbb{E}, \mathcal{F}' \rangle_{\text{bev}} \stackrel{\Delta}{=} \mathcal{D}_{i+1}$. We also have $\mathcal{O}_i \to^* \langle \mathbb{E} | n[\epsilon]^{\text{ev}} \rangle_{\text{bev}} \stackrel{\Delta}{=} \mathcal{O}_{i+1}$ with $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$.

(O6) We have $\mathcal{O}_i = \langle \lambda^\Sigma.l | \Box l' :: \mathbb{E}, \mathcal{E} \rangle_{\text{ev}} \to \langle \mathbb{E} | l[l' \cdot \mathcal{E}]^\emptyset \rangle_{\text{rec}} = \mathcal{O}'$. Because $\mathcal{O}_i$ is valid, $\Sigma$ cannot be a blocking annotation, and we have $[[\lambda^\Sigma.l]]_o(\mathcal{E}) = \lambda^\emptyset.[[l]]_o(\upharpoonright \mathcal{E})$. By Lemma 20, there exists $\mathcal{D}'$ such that $\mathcal{D}' = \langle \lambda^\emptyset.k | \mathbb{F}', \mathcal{F}, \pi' \rangle_{\text{ev}}$, $\mathcal{D}_i \to^* \mathcal{D}'$, and $\mathcal{O}_i \approx \mathcal{D}'$. Because $\mathcal{O}_i \approx \mathcal{D}'$, we have in particular $[[l]]_o(\upharpoonright \mathcal{E}) \triangleright [[k]]_d(\upharpoonright \mathcal{F})$, $\mathbb{F}' = \Box k' :: \mathbb{F}, [[l')]_o(\star) \triangleright [[k')]_d(\star)$, and $[[\mathbb{E}]_o \triangleright [[\mathbb{F}]_d$. Then $\mathcal{D}' \to \langle |\mathbb{F}\langle k[k' \cdot \emptyset \mathcal{F}]^\emptyset \rangle| | \Box, \star, \triangle \rangle_{\text{ev}} \stackrel{\Delta}{=} \mathcal{D}'$.

Since $[[\mathbb{E}]_o \triangleright [[\mathbb{F}]_d]$, the contexts are of the same size $a$. Let $\mathcal{O}' \to^* \langle \mathbb{E}_b \langle l[l' \cdot \mathcal{E}]^\emptyset \rangle | \mathbb{E}_{a-b}, \star \rangle_{\text{ev}} \stackrel{\Delta}{=} \mathcal{O}_{i+1}$ be the sequence of $b$ reconstruction steps taken by the OAM. Because $[[\mathbb{E}]_o \triangleright [[\mathbb{F}]_d]$, the contexts have the same shape, and because the annotations have been erased on the DAM side, nothing prevents the DAM to match with $\mathcal{D}' \to^* \langle \mathbb{F}_b \langle k[k' \cdot \emptyset \mathcal{F}]^\emptyset \rangle | \mathbb{F}_{a-b}, \star | \pi'' \rangle_{\text{ev}} \stackrel{\Delta}{=} \mathcal{D}_{i+1}$. Because $[[\mathbb{E}]_o \triangleright [[\mathbb{F}]_d]$ frame by frame, we also have $[[\mathbb{E}_b]_o \triangleright [[\mathbb{F}_b]]_d$ and $[[\mathbb{E}_{a-b}]_o \triangleright [[\mathbb{F}_{a-b}]]_d$. We conclude that $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$ with Lemma 26.

(O7) Similar to the first subcase of (O5).

(O8) The OAM does a switching step because all the subterms are annotated. We sketch the application case, the abstraction one is similar. We have $\langle c_1 | \mathbb{E}, \mathcal{F}' \rangle_{\text{ev}} \to \langle \mathbb{E} | c_1 | \mathbb{E}, c_2 \rangle_{\text{bev}} \stackrel{\Delta}{=} \mathcal{O}_{i+1}$. Because $\mathcal{O}_i$ is valid, $\Sigma$ cannot be a blocking annotation, and we have $[[c_1 | \mathbb{E}, c_2]]_o(\star) = [[c_1]]_o(\star) | \emptyset^\emptyset [[c_2]]_o(\star)$. By Lemma 20, there exists $\mathcal{D}'$ such that $\mathcal{D}' = \langle k_1 | \emptyset^\emptyset k_2 | \mathbb{F}, \mathcal{F}', \pi' \rangle_{\text{ev}}$, $\mathcal{D}_i \to^* \mathcal{D}'$, and $\mathcal{O}_i \approx \mathcal{D}'$. If $k_1$ and $k_2$ are annotated, then the DAM directly does the switching step. Otherwise, we prove as in the third subcase of (O5) that the DAM adds the missing annotations, and then does the switching step to $\mathcal{D}_{i+1}$. We can then prove that $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$.

(O9) We have $\mathcal{O}_i = \langle \Box l :: \mathbb{E} | c \rangle_{\text{bev}} \to \langle c | \emptyset^\emptyset l | \mathbb{E}, \star \rangle_{\text{ev}} = \mathcal{O}'$. We pick $\mathcal{O}_{i+1} = \mathcal{O}'$. By Lemma 21, there exists $\mathcal{D}'$ such that $\mathcal{D}' = \langle \text{appl} :: \pi | l_1, \Box (l_2[\mathcal{F}]) :: \mathbb{F}, \mathcal{F} \rangle_{\text{bev}}$, $\mathcal{D} \to^* \mathcal{D}'$, and $\mathcal{O} \approx \mathcal{D}'$. Then $\mathcal{D}' \to \langle l_1 | \emptyset^\emptyset l_2 | \mathbb{F}, \mathcal{F}, \pi \rangle_{\text{ev}} \stackrel{\Delta}{=} \mathcal{D}_{i+1}$. Because $\mathcal{O} \approx \mathcal{D}'$, we know $[[c]]_o(\star) \triangleright [[l_1]]_d(\mathcal{F})$ and
(O5) Because $[[n]]_o(!\epsilon) = (n, \epsilon, \emptyset)$, by Lemma 20, there exists $\mathcal{D}'$ such that $\mathcal{D}' = \langle n^\emptyset | \mathbb{F}, \mathcal{F}', \pi' \rangle_{\text{ev}}$, $\mathcal{D}_i \to^* \mathcal{D}'$, and $\mathcal{O}_i \approx \mathcal{D}'$. In particular, we have $[[n^\emptyset]]_d(\mathcal{F}') = (n, \phi, \emptyset)$ for some $\phi$ with $(n, \epsilon, \emptyset) \triangleright (n, \phi, \emptyset)$. From there, we distinguish three cases.

Suppose $\|(n, \epsilon, \emptyset)\|_o = \|(n, \phi, \emptyset)\|_d = m$. There is a one-to-one correspondence between the equations defining $\|\cdot\|_o$ and $\|\cdot\|_d$ and the var steps of the OAM and the DAM, except for the equations returning a variable, which can be replaced by the switching step of the var mode. On the DAM side, by definition of $\|\cdot\|_d$, we are sure that the environment is not annotated because we start from a variable with no annotation. As a result, we can build sequences $\mathcal{O}_i \to^* \langle \mathbb{E} | n[\epsilon]^{\text{ev}} \rangle_{\text{bev}} \triangleq \mathcal{O}_{i+1}$ and $\mathcal{D}_i \to^* \langle \pi' | n^{\text{ev}}, \mathbb{E}, \mathcal{F}' \rangle_{\text{bev}} \triangleq \mathcal{D}_{i+1}$, and check that we have $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$, as wished.

Suppose $\|(n, \epsilon, \emptyset)\|_o = (l, \mathcal{E})$ with $\mathcal{E}, \text{infun}(\mathbb{F}) \nmid l$. Because $(n, \epsilon, \emptyset) \triangleright (n, \phi, \emptyset)$, there exists $(k, \mathcal{F}'')$ such that $\|(n, \phi, \emptyset)\|_o = (k, \mathcal{F}'')$ and $[[l]]_o(\mathcal{E}) \triangleright [[k]]_d(\mathcal{F}'')$. In particular, $k$ is not annotated. As in the previous subcase, we can build sequences $\mathcal{O}_i \to^* \langle l | \mathbb{E}, \mathcal{E} \rangle_{\text{ev}} \triangleq \mathcal{O}_{i+1}$ and $\mathcal{D}_i \to^* \langle k | \mathbb{F}, \mathcal{F}'', \pi'' \rangle_{\text{ev}} \triangleq \mathcal{D}_{i+1}$ with $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$, as wished.

Suppose $\|(n, \epsilon, \emptyset)\|_o = (l, \mathcal{E})$ with $\mathcal{E}, \text{infun}(\mathbb{F}) \vdash l$, i.e., $\mathcal{E} = \star$. Because $(n, \epsilon, \emptyset) \triangleright (n, \phi, \emptyset)$, there exists $(k, \mathcal{F}'')$ such that $\|(n, \phi, \emptyset)\|_o = (k, \mathcal{F}'')$ and $[[l]]_o(\star) \triangleright [[k]]_d(\mathcal{F}'')$. If $k$ is annotated, we conclude as in the first subcase. Otherwise, there exists $\mathcal{O}_j$ such that the annotation is added to $l$ at that point. By construction of the sequences of machine states, $\mathcal{D}_j = \langle \pi_j | k_j, \mathbb{F}_j, \mathcal{F}_j \rangle_{\text{bev}}$ also adds the annotation. Because the DAM is sound w.r.t. the ZS, $[[k_j]]_o(\star) \triangleright [[k_j]]_d(\mathcal{E}_j)$ is a normal form. We have $[[l]]_o(\star) \triangleright [[k_j]]_d(\mathcal{E}_j)$, which implies $[[l]](\star) = [[k_j]](\mathcal{E}_j)$ by Lemma 23. We also have $[[l]](\star) = [[k]](\mathcal{F}'')$, so $[[k]](\mathcal{F}'')$ is a normal form. Because the DAM is complete w.r.t. the ZS, there exists a sequence $\langle k | \mathbb{F}, \mathcal{F}'', \pi'' \rangle_{\text{ev}} \to^* \langle \pi'' | k^{+\text{ev}}, \mathbb{F}, \mathcal{F}' \rangle_{\text{bev}}$, and then $\langle \pi'' | k^{+\text{ev}}, \mathbb{F}, \mathcal{F}' \rangle_{\text{bev}} \to^* \langle \pi' | n^{\text{ev}}, \mathbb{E}, \mathcal{F}' \rangle_{\text{bev}} \triangleq \mathcal{D}_{i+1}$. We also have $\mathcal{O}_i \to^* \langle \mathbb{E} | n[\epsilon]^{\text{ev}} \rangle_{\text{bev}} \triangleq \mathcal{O}_{i+1}$ with $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$.

(O6) We have $\mathcal{O}_i = \langle \lambda^\Sigma.l | \Box l' :: \mathbb{E}, \mathcal{E} \rangle_{\text{ev}} \to \langle \mathbb{E} | l[l' \cdot \mathcal{E}]^\emptyset \rangle_{\text{rec}} = \mathcal{O}'$. Because $\mathcal{O}_i$ is valid, $\Sigma$ cannot be a blocking annotation, and we have $[[\lambda^\Sigma.l]]_o(\mathcal{E}) = \lambda^\emptyset.[[l]]_o(\upharpoonright\mathcal{E})$. By Lemma 20, there exists $\mathcal{D}'$ such that $\mathcal{D}' = \langle \lambda^\emptyset.k | \mathbb{F}', \mathcal{F}, \pi' \rangle_{\text{ev}}$, $\mathcal{D}_i \to^* \mathcal{D}'$, and $\mathcal{O}_i \approx \mathcal{D}'$. Because $\mathcal{O}_i \approx \mathcal{D}'$, we have in particular $[[l]]_o(\upharpoonright\mathcal{E}) \triangleright [[k]]_d(\upharpoonright\mathcal{F})$, $\mathbb{F}' = \Box k' :: \mathbb{F}, [[l']](\star) \triangleright [[k']](\star)$, and $[[\mathbb{E}]](\star) \triangleright [[\mathbb{F}]](\star)$. Then $\mathcal{D}' \to \langle \mathbb{F} \langle k[k' \cdot \emptyset] \mathcal{F} \rangle^\emptyset \rangle | \llcorner \star, \star, \Delta \rangle_{\text{ev}} \triangleq \mathcal{D}'$.

Since $[[\mathbb{E}]]_o \triangleright [[\mathbb{F}]](\star)$, the contexts are of the same size $a$. Let $\mathcal{O}' \to^* \langle \mathbb{E}_b \langle l[l' \cdot \mathcal{E}]^\emptyset \rangle | \mathbb{E}_{a-b}, \star \rangle_{\text{ev}} \triangleq \mathcal{O}_{i+1}$ be the sequence of $b$ reconstruction steps taken by the OAM. Because $[[\mathbb{E}]]_o \triangleright [[\mathbb{F}]](\star)$, the contexts have the same shape, and because the annotations have been erased on the DAM side, nothing prevents the DAM to match with $\mathcal{D}' \to^* \langle \mathbb{F}_b \langle k[k' \cdot \emptyset] \mathcal{F} \rangle^\emptyset \rangle | \mathbb{F}_{a-b}, \star | \pi'' \rangle_{\text{ev}} \triangleq \mathcal{D}_{i+1}$. Because $[[\mathbb{E}]]_o \triangleright [[\mathbb{F}]](\star)$ frame by frame, we also have $[[\mathbb{E}_b]]_o \triangleright [[\mathbb{F}_b]]_d$ and $[[\mathbb{E}_{a-b}]]_o \triangleright [[\mathbb{F}_{a-b}]]_d$. We conclude that $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$ with Lemma 26.

(O7) Similar to the first subcase of (O5).

(O8) The OAM does a switching step because all the subterms are annotated. We sketch the application case, the abstraction one is similar. We have $\langle c_1 | \mathbb{E}, \star \rangle_{\text{ev}} \to \langle \mathbb{E} | c_1 | \mathbb{E} \rangle_{\text{bev}} \triangleq \mathcal{O}_{i+1}$. Because $\mathcal{O}_i$ is valid, $\Sigma$ cannot be a blocking annotation, and we have $[[c_1 | \mathbb{E} \rangle_{\text{bev}}(\star)] = [[c_1]]_o(\star) | \mathbb{E}^\emptyset [[c_2]]_o(\star)$. By Lemma 20, there exists $\mathcal{D}'$ such that $\mathcal{D}' = \langle k_1 | \mathbb{E}^\emptyset k_2 | \mathbb{F}, \mathcal{F}', \pi' \rangle_{\text{ev}}$, $\mathcal{D}_i \to^* \mathcal{D}'$, and $\mathcal{O}_i \approx \mathcal{D}'$. If $k_1$ and $k_2$ are annotated, then the DAM directly does the switching step. Otherwise, we prove as in the third subcase of (O5) that the DAM adds the missing annotations, and then does the switching step to $\mathcal{D}_{i+1}$. We can then prove that $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$.

(O9) We have $\mathcal{O}_i = \langle \Box l :: \mathbb{E} | c \rangle_{\text{bev}} \to \langle c | \mathbb{E}^\emptyset l | \mathbb{E}, \star \rangle_{\text{ev}} = \mathcal{O}'$. We pick $\mathcal{O}_{i+1} = \mathcal{O}'$. By Lemma 21, there exists $\mathcal{D}'$ such that $\mathcal{D}' = \langle \text{appl} :: \pi | l_1, \Box (l_2[\mathcal{F}]) :: \mathbb{F}, \mathcal{F} \rangle_{\text{bev}}$, $\mathcal{D} \to^* \mathcal{D}'$, and $\mathcal{O} \approx \mathcal{D}'$. Then $\mathcal{D}' \to \langle l_1 | \mathbb{E}^\emptyset l_2 | \mathbb{F}, \mathcal{F}, \pi \rangle_{\text{ev}} \triangleq \mathcal{D}_{i+1}$. Because $\mathcal{O} \approx \mathcal{D}'$, we know $[[c]]_o(\star) \triangleright [[l_1]]_d(\mathcal{F})$ and
$[[l]_o(\star) \triangleright [[l_2[\mathcal{F}]]_d(\star)],$ which implies $[[l]_o(\star) \triangleright [[l_2]]_d(\mathcal{F})$ by Lemma 25. Therefore we have
$[[c @^\emptyset l]_o(\star) \triangleright [[l_1 @^\emptyset l_2]]_d(\mathcal{F})$ and $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$

(O10)-(O12) Similar to the case above.

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

► **Lemma 28.** Let $\mathcal{O} \approx \mathcal{D}$ such that $\mathcal{D} = \langle k | \mathbb{F}, \mathcal{F}, \pi \rangle_{\text{ev}}$.

■ If $[[k]]_d(\mathcal{F}) = k_1 @^\Delta k_2$, there exists $\mathcal{O}'$ such that $\mathcal{O}' = \langle l_1 @^\Sigma l_2 | \mathbb{F}, \mathcal{E}' \rangle_{\text{ev}}, \mathcal{O} \to^* \mathcal{O}', \text{ and } \mathcal{O}' \approx \mathcal{D}$;

■ A similar result holds if $[[k]]_d(\mathcal{F}) = \lambda^\Delta.l'$, or if $[[l]]_o(\mathcal{E}) = (n, \epsilon, \emptyset)$ and $[[k]]_d(\mathcal{F}) = (n, \phi, \emptyset)$.

**Proof.** Let $\mathcal{O} = \langle l | \mathbb{E}, \mathcal{E} \rangle_{\text{ev}}$. Assume $[[k]]_d(\mathcal{F}) = k_1 @^\Delta k_2$. Because $[[l]]_o(\mathcal{E}) \triangleright [[k]](\mathcal{F})$, there exist $l_1$ and $l_2$ such that $[[l]]_o(\mathcal{E}) = l_1 @^\Sigma l_2$. We prove that the derivation exists by induction on the number of steps required to compute $[[l]]_d(\mathcal{E}) = l_1 @^\Sigma l_2$. If that number is 0, then $l$ is an application and the result holds by picking $\mathcal{O}' = \mathcal{O}$.

Otherwise, the only other case is $l = l'[\epsilon]^\Sigma$; then $[[l]]_o(\mathcal{E}) = [[l']]'(\epsilon[\mathcal{E}])$, so $[[l']]'(\epsilon[\mathcal{E}]) \triangleright [[k]](\mathcal{F})$ holds. The step $\mathcal{O} \to \langle l' | \mathbb{F}, \epsilon[\mathcal{E}] \rangle_{\text{ev}}$ is always possible. We have $\langle l' | \mathbb{E}, \epsilon[\mathcal{E}] \rangle_{\text{ev}} \approx \mathcal{D}$, and $[[l']]'(\epsilon[\mathcal{E}]) = l_1 @^\Sigma l_2$ with one less step, so by induction, there exists $\mathcal{O}'$ as wished such that $\langle l' | \mathbb{E}, \epsilon[\mathcal{E}] \rangle_{\text{ev}} \to^* \mathcal{O}'$, from which we conclude $\mathcal{O} \to^* \mathcal{O}'$.

The abstraction and variable cases are similar.

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

► **Theorem 29 (DAM implies OAM).** If $(\mathcal{O}_0, \mathcal{O}_1 \dots \mathcal{O}_i) \approx (\mathcal{D}_0, \mathcal{D}_1 \dots \mathcal{D}_i)$ and $\mathcal{D}_i \to \mathcal{D}',$ there
exist $\mathcal{O}_{i+1}$ and $\mathcal{D}_{i+1}$ such that $\mathcal{D}' \to^* \mathcal{D}_{i+1}$, $\mathcal{O}_i \to^* \mathcal{O}_{i+1}$, and $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$.

**Proof.** By case analysis on the step $\mathcal{D}_i \to \mathcal{D}'$.

(D1) We have $\mathcal{D}_i = \langle k_1 @^\Sigma k_2 | \mathbb{F}, \mathcal{F}, \pi \rangle_{\text{ev}} \to \langle k_1 | \Box (k_2[\mathcal{F}]) \:: \mathbb{E}, \mathcal{F}, \pi' \rangle_{\text{ev}} = \mathcal{D}'$ with $ev \notin an(k_1)$.
By Lemma 28, there exists $\mathcal{O}'$ such that $\mathcal{O}' = \langle l_1 @^\Sigma l_2 | \mathbb{E}, \mathcal{E}' \rangle_{\text{ev}}, O_i \to^* \mathcal{O}', \text{ and } \mathcal{O}' \approx \mathcal{D}_i$.
Because $\mathcal{O}' \approx \mathcal{D}_i$, we have in particular $[[l_1]]_o(\mathcal{E}) \triangleright [[k_1]]_d(\mathcal{F})$ and $[[l_2]]_o(\mathcal{E}') \triangleright [[k_2]]_d(\mathcal{F})$. We
distinguish two cases.

If $\mathcal{E}', \top / l_1$, we have $\mathcal{O}' \to \langle k_1 | \Box (l_2[\mathcal{E}']) \:: \mathbb{E}, \mathcal{E}' \rangle_{\text{ev}} = \mathcal{O}_{i+1}$, and we pick $\mathcal{D}_{i+1} = \mathcal{D}'$.
From $[[l_2]]_o(\mathcal{E}') \triangleright [[k_2]]_d(\mathcal{F})$, we deduce $[[l_2[\mathcal{E}']]]_o \triangleright [[k_2[\mathcal{F}]]]_d$ by Lemma 25, so we have
$\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$.

Otherwise, there is a blocking annotation on $l_1$. By the same reasoning as in the proof of Theorem 27 (subcase O5), we can prove that the DAM generates an annotation on $k_1$: there exists a sequence $\mathcal{D}' \to^* \langle k_1' @^\Sigma k_2 | \mathbb{F}, \mathcal{F}, \pi \rangle_{\text{ev}} = \mathcal{D}_{I+1}$ such that $ev \in an(k_1')$. In fact, all the subterms of $k_1'$ must be annotated, and it must also be the case of the subterms of $l_1$. By picking $\mathcal{O}_{i+1} = \mathcal{O}',$ we have $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$ as wished.

(D2)-(D3) Similar to the case above.

(D4) We have $\mathcal{D}_i = \langle k[\phi]^\Delta | \mathbb{F}, \mathcal{F} \rangle_{\text{ev}} \to \langle k | \mathbb{F}, \phi \bullet \mathcal{F} \rangle_{\text{ev}} = \mathcal{D}'$. We pick $\mathcal{D}_{I+1} = \mathcal{D}'$ and $\mathcal{O}_{I+1} = \mathcal{O}_i$.
Because $\mathcal{O}_i \approx \mathcal{D}_i$, we have $[[l]]_o(\mathcal{E}) \triangleright [[k[\phi]^\Delta]]_d(\mathcal{F})$, i.e., $[[l]]_o(\mathcal{E}) \triangleright [[k]]_d(\phi \bullet \mathcal{F})$, therefore
$\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$ holds.

(D5) Because $\mathcal{D}_i$ is valid, we have $\mathcal{D}_i = \langle n^\emptyset | \mathbb{E}, !\phi, \pi \rangle_{\text{ev}}$. If $[[l]]_o(\mathcal{E}) \triangleright (n, \phi, \emptyset)$ with $[[l]]_o(\mathcal{E}) \neq (n, \epsilon, \Sigma)$, then $\|(n, \phi, \emptyset)\|_d = (k, \mathcal{F}')$ and $[[l]]_o(\mathcal{E}) \triangleright [[k]]_d(\mathcal{F}')$. By definition of $\|\cdot\|_d$, the environment $\phi$ does not have blocking annotations, and there is a one-to-one corresponding between the definition of $\|\cdot\|_d$ and the var step, so there exists a sequence $\mathcal{D}_i \to^* \langle k, \mathbb{F} | \mathcal{F}' | \pi' \rangle_{\text{ev}} = \mathcal{D}_{i+1}$. By choosing $\mathcal{O}_{i+1} = \mathcal{O}_i$, we have the required result.

If $[[l]]_o(\mathcal{E}) = (n, \epsilon, \text{ev})$, then $l = n[\epsilon]^{\text{ev}}$ and $\mathcal{E} = \star$: we have a valid forward machine state with a blocking annotation, a contradiction. If $[[l]]_o(\mathcal{E}) = (n, \epsilon, \emptyset)$, by Lemma 28, there exists $\mathcal{O}'$ such that $\mathcal{O}' = \langle n | \mathbb{E}, !\epsilon \rangle_{\text{ev}}$, $\mathcal{O}_i \to^* \mathcal{O}'$, and $\mathcal{O}' \approx \mathcal{D}_i$. From there, we distinguish three cases, and we conclude for each of them as in the proof of Theorem 27.
$[[l]_o(\star) \triangleright [[l_2[\mathcal{F}]]_d(\star)],$ which implies $[[l]]_o(\star) \triangleright [[l_2]]_d(\mathcal{F})$ by Lemma 25. Therefore we have
$[[c @^\emptyset l]]_o(\star) \triangleright [[l_1 @^\emptyset l_2]]_d(\mathcal{F})$ and $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$

(O10)-(O12) Similar to the case above.

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

► **Lemma 28.** Let $\mathcal{O} \approx \mathcal{D}$ such that $\mathcal{D} = \langle k | \mathbb{F}, \mathcal{F}, \pi \rangle_{\text{ev}}$.

■ If $[[k]]_d(\mathcal{F}) = k_1 @^\Delta k_2$, there exists $\mathcal{O}'$ such that $\mathcal{O}' = \langle l_1 @^\Sigma l_2 | \mathbb{F}, \mathcal{E}' \rangle_{\text{ev}}, \mathcal{O} \to^* \mathcal{O}', \text{ and } \mathcal{O}' \approx \mathcal{D}$;

■ A similar result holds if $[[k]]_d(\mathcal{F}) = \lambda^\Delta.l'$, or if $[[l]]_o(\mathcal{E}) = (n, \epsilon, \emptyset)$ and $[[k]]_d(\mathcal{F}) = (n, \phi, \emptyset)$.

**Proof.** Let $\mathcal{O} = \langle l | \mathbb{E}, \mathcal{E} \rangle_{\text{ev}}$. Assume $[[k]]_d(\mathcal{F}) = k_1 @^\Delta k_2$. Because $[[l]]_o(\mathcal{E}) \triangleright [[k]](\mathcal{F})$, there exist $l_1$ and $l_2$ such that $[[l]]_o(\mathcal{E}) = l_1 @^\Sigma l_2$. We prove that the derivation exists by induction on the number of steps required to compute $[[l]]_d(\mathcal{E}) = l_1 @^\Sigma l_2$. If that number is 0, then $l$ is an application and the result holds by picking $\mathcal{O}' = \mathcal{O}$.

Otherwise, the only other case is $l = l'[\epsilon]^\Sigma$; then $[[l]]_o(\mathcal{E}) = [[l']]'(\epsilon[\mathcal{E}])$, so $[[l']]'(\epsilon[\mathcal{E}]) \triangleright [[k]](\mathcal{F})$ holds. The step $\mathcal{O} \to \langle l' | \mathbb{F}, \epsilon[\mathcal{E}] \rangle_{\text{ev}}$ is always possible. We have $\langle l' | \mathbb{E}, \epsilon[\mathcal{E}] \rangle_{\text{ev}} \approx \mathcal{D}$, and $[[l']]'(\epsilon[\mathcal{E}]) = l_1 @^\Sigma l_2$ with one less step, so by induction, there exists $\mathcal{O}'$ as wished such that $\langle l' | \mathbb{E}, \epsilon[\mathcal{E}] \rangle_{\text{ev}} \to^* \mathcal{O}'$, from which we conclude $\mathcal{O} \to^* \mathcal{O}'$.

The abstraction and variable cases are similar.

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

► **Theorem 29 (DAM implies OAM).** If $(\mathcal{O}_0, \mathcal{O}_1 \dots \mathcal{O}_i) \approx (\mathcal{D}_0, \mathcal{D}_1 \dots \mathcal{D}_i)$ and $\mathcal{D}_i \to \mathcal{D}',$ there
exist $\mathcal{O}_{i+1}$ and $\mathcal{D}_{i+1}$ such that $\mathcal{D}' \to^* \mathcal{D}_{i+1}$, $\mathcal{O}_i \to^* \mathcal{O}_{i+1}$, and $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$.

**Proof.** By case analysis on the step $\mathcal{D}_i \to \mathcal{D}'$.

(D1) We have $\mathcal{D}_i = \langle k_1 @^\Sigma k_2 | \mathbb{F}, \mathcal{F}, \pi \rangle_{\text{ev}} \to \langle k_1 | \Box (k_2[\mathcal{F}]) \:: \mathbb{E}, \mathcal{F}, \pi' \rangle_{\text{ev}} = \mathcal{D}'$ with $ev \notin an(k_1)$.
By Lemma 28, there exists $\mathcal{O}'$ such that $\mathcal{O}' = \langle l_1 @^\Sigma l_2 | \mathbb{E}, \mathcal{E}' \rangle_{\text{ev}}, O_i \to^* \mathcal{O}', \text{ and } \mathcal{O}' \approx \mathcal{D}_i$.
Because $\mathcal{O}' \approx \mathcal{D}_i$, we have in particular $[[l_1]]_o(\mathcal{E}) \triangleright [[k_1]]_d(\mathcal{F})$ and $[[l_2]]_o(\mathcal{E}') \triangleright [[k_2]]_d(\mathcal{F})$. We
distinguish two cases.

If $\mathcal{E}', \top / l_1$, we have $\mathcal{O}' \to \langle k_1 | \Box (l_2[\mathcal{E}']) \:: \mathbb{E}, \mathcal{E}' \rangle_{\text{ev}} = \mathcal{O}_{i+1}$, and we pick $\mathcal{D}_{i+1} = \mathcal{D}'$.
From $[[l_2]]_o(\mathcal{E}') \triangleright [[k_2]]_d(\mathcal{F})$, we deduce $[[l_2[\mathcal{E}']]]_o \triangleright [[k_2[\mathcal{F}]]]_d$ by Lemma 25, so we have
$\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$.

Otherwise, there is a blocking annotation on $l_1$. By the same reasoning as in the proof of Theorem 27 (subcase O5), we can prove that the DAM generates an annotation on $k_1$: there exists a sequence $\mathcal{D}' \to^* \langle k_1' @^\Sigma k_2 | \mathbb{F}, \mathcal{F}, \pi \rangle_{\text{ev}} = \mathcal{D}_{I+1}$ such that $ev \in an(k_1')$. In fact, all the subterms of $k_1'$ must be annotated, and it must also be the case of the subterms of $l_1$. By picking $\mathcal{O}_{i+1} = \mathcal{O}',$ we have $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$ as wished.

(D2)-(D3) Similar to the case above.

(D4) We have $\mathcal{D}_i = \langle k[\phi]^\Delta | \mathbb{F}, \mathcal{F} \rangle_{\text{ev}} \to \langle k | \mathbb{F}, \phi \bullet \mathcal{F} \rangle_{\text{ev}} = \mathcal{D}'$. We pick $\mathcal{D}_{I+1} = \mathcal{D}'$ and $\mathcal{O}_{I+1} = \mathcal{O}_i$.
Because $\mathcal{O}_i \approx \mathcal{D}_i$, we have $[[l]]_o(\mathcal{E}) \triangleright [[k[\phi]^\Delta]]_d(\mathcal{F})$, i.e., $[[l]]_o(\mathcal{E}) \triangleright [[k]]_d(\phi \bullet \mathcal{F})$, therefore
$\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$ holds.

(D5) Because $\mathcal{D}_i$ is valid, we have $\mathcal{D}_i = \langle n^\emptyset | \mathbb{E}, !\phi, \pi \rangle_{\text{ev}}$. If $[[l]]_o(\mathcal{E}) \triangleright (n, \phi, \emptyset)$ with $[[l]]_o(\mathcal{E}) \neq (n, \epsilon, \Sigma)$, then $\|(n, \phi, \emptyset)\|_d = (k, \mathcal{F}')$ and $[[l]]_o(\mathcal{E}) \triangleright [[k]]_d(\mathcal{F}')$. By definition of $\|\cdot\|_d$, the environment $\phi$ does not have blocking annotations, and there is a one-to-one corresponding between the definition of $\|\cdot\|_d$ and the var step, so there exists a sequence $\mathcal{D}_i \to^* \langle k, \mathbb{F} | \mathcal{F}' | \pi' \rangle_{\text{ev}} = \mathcal{D}_{i+1}$. By choosing $\mathcal{O}_{i+1} = \mathcal{O}_i$, we have the required result.

If $[[l]]_o(\mathcal{E}) = (n, \epsilon, \text{ev})$, then $l = n[\epsilon]^{\text{ev}}$ and $\mathcal{E} = \star$: we have a valid forward machine state with a blocking annotation, a contradiction. If $[[l]]_o(\mathcal{E}) = (n, \epsilon, \emptyset)$, by Lemma 28, there exists $\mathcal{O}'$ such that $\mathcal{O}' = \langle n | \mathbb{E}, !\epsilon \rangle_{\text{ev}}$, $\mathcal{O}_i \to^* \mathcal{O}'$, and $\mathcal{O}' \approx \mathcal{D}_i$. From there, we distinguish three cases, and we conclude for each of them as in the proof of Theorem 27.
(D6) We have $\mathcal{D}_i = \langle \lambda^\Delta.k | \Box k' :: \mathbb{F}, \mathcal{F}, \pi \rangle_{\text{ev}} \to \langle |\mathbb{F}\langle k[k' \cdot \emptyset, \mathcal{F}]^\emptyset \rangle| | \Box, \star, \triangle \rangle_{\text{ev}} = \mathcal{D}'$. By Lemma 28, there exists $\mathcal{O}'$ such that $\mathcal{O}' = \langle \lambda^\Sigma.l | \mathbb{E}', \mathcal{E} \rangle_{\text{ev}}$, $\mathcal{O}_i \to^* \mathcal{O}'$, and $\mathcal{O}' \approx \mathcal{D}_i$. Because $\mathcal{O}' \approx \mathcal{D}_i$, we have in particular $[[l]_o(\upharpoonright \mathcal{E})] \triangleright [[k]_d(\upharpoonright \mathcal{F})$, $\mathbb{E}' = \Box l' :: \mathbb{E}$, $[[l']_o(\star)] \triangleright [[k']_d(\star)$, and $[[\mathbb{E}]_o] \triangleright [[\mathbb{F}]_d$: these relations also hold after erasing on the DAM side. Then we have $\mathcal{O}' \to \langle \mathbb{E} | l[l' \cdot \mathcal{E}]^\emptyset \rangle_{\text{rec}} \to^* \langle \mathbb{E}\langle l[l' \cdot \mathcal{E}]^\emptyset \rangle | \Box, \star \rangle_{\text{ev}} \stackrel{\Delta}{=} \mathcal{O}_{i+1}$, and we pick $\mathcal{D}_{i+1} = \mathcal{D}'$. We conclude that $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$ with Lemma 26.

(D7) In that case, the step $\mathcal{D}_i \to \mathcal{D}'$ is a switching step: the DAM has to backtrack because of the annotations. We pick $\mathcal{D}_{i+1} = \mathcal{D}'$. A possible case is that the DAM cannot do step (D5) because of a var annotation on the environment. However, by definition of $\|\cdot\|_d$, the environment is annotated only if the variable is also annotated, which is in contradiction with the fact that $\mathcal{D}_i$ is valid. Therefore, the DAM backtracks only because of ev annotations, which are also present on the OAM side because $\mathcal{D}_i \approx \mathcal{O}_i$. The OAM also does a switching step $\mathcal{O}_i \to \mathcal{O}_{i+1}$, and we have $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$.

(D10) We have $\mathcal{D} = \langle \text{env}(\phi) :: \pi | k, \mathbb{F}, \phi \bullet \mathcal{F} \rangle_{\text{bev}} \to \langle k[\phi]^\Delta | \mathbb{F}, \mathcal{F}, \pi \rangle_{\text{ev}} = \mathcal{D}'$. Because $\mathcal{D}$ is a backward configuration, we know $k$ is annotated, and $\mathcal{D}'$ can only do a switching step $\mathcal{D}' \to \langle \pi | k[\phi]^{\text{ev}}, \mathbb{F}, \mathcal{F} \rangle_{\text{bev}} \stackrel{\Delta}{=} \mathcal{D}_{i+1}$. We pick $\mathcal{O}_{i+1} = \mathcal{O}_i$. Because $\mathcal{O}_i \approx \mathcal{D}_i$, we have $[[c]_o(\star)] \triangleright [[k]_d(\phi \bullet \mathcal{F})$, i.e., $[[c]_o(\star)] \triangleright [[k[\phi]^{\text{ev}}]_d(\mathcal{F})$. Therefore we have $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$.

(D8) We have $\mathcal{D}_i = \langle \text{appl} :: \pi | l_1, \Box (l_2[\mathcal{F}]) :: \mathbb{F}, \mathcal{F} \rangle_{\text{bev}} \to \langle l_1 @^\emptyset l_2 | \mathbb{F}, \mathcal{F}, \pi \rangle_{\text{ev}} \stackrel{\Delta}{=} \mathcal{D}_{i+1}$. Because $\mathcal{O}_i \approx \mathcal{D}_i$, we must have $\mathcal{O}_i = \langle \Box l :: \mathbb{E} | c \rangle_{\text{bev}} \to \langle c @^\emptyset l | \mathbb{E}, \star \rangle_{\text{ev}} \stackrel{\Delta}{=} \mathcal{O}_{i+1}$, and we know $[[c]_o(\star)] \triangleright [[l_1]_d(\mathcal{F})$ and $[[l]_o(\star)] \triangleright [[l_2[\mathcal{F}]]_d(\star)$. The latter implies $[[l]_o(\star)] \triangleright [[l_2]_d(\mathcal{F})$ by Lemma 25, so we have $[[c @^\emptyset l]_o(\star)] \triangleright [[l_1 @^\emptyset l_2]_d(\mathcal{F})$ and $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$.

(D9)-(D13) Similar to the case above.

<figure><img src="image_13.png" /></figure>
(D6) We have $\mathcal{D}_i = \langle \lambda^\Delta.k | \Box k' :: \mathbb{F}, \mathcal{F}, \pi \rangle_{\text{ev}} \to \langle |\mathbb{F}\langle k[k' \cdot \emptyset, \mathcal{F}]^\emptyset \rangle| | \Box, \star, \triangle \rangle_{\text{ev}} = \mathcal{D}'$. By Lemma 28, there exists $\mathcal{O}'$ such that $\mathcal{O}' = \langle \lambda^\Sigma.l | \mathbb{E}', \mathcal{E} \rangle_{\text{ev}}$, $\mathcal{O}_i \to^* \mathcal{O}'$, and $\mathcal{O}' \approx \mathcal{D}_i$. Because $\mathcal{O}' \approx \mathcal{D}_i$, we have in particular $[[l]_o(\upharpoonright \mathcal{E})] \triangleright [[k]_d(\upharpoonright \mathcal{F})]$, $\mathbb{E}' = \Box l' :: \mathbb{E}$, $[[l']_o(\star)] \triangleright [[k']_d(\star)]$, and $[[\mathbb{E}]_o] \triangleright [[\mathbb{F}]_d]:$ these relations also hold after erasing on the DAM side. Then we have $\mathcal{O}' \to \langle \mathbb{E} | l[l' \cdot \mathcal{E}]^\emptyset \rangle_{\text{rec}} \to^* \langle \mathbb{E}\langle l[l' \cdot \mathcal{E}]^\emptyset \rangle | \Box, \star \rangle_{\text{ev}} \stackrel{\Delta}{=} \mathcal{O}_{i+1}$, and we pick $\mathcal{D}_{i+1} = \mathcal{D}'$. We conclude that $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$ with Lemma 26.

(D7) In that case, the step $\mathcal{D}_i \to \mathcal{D}'$ is a switching step: the DAM has to backtrack because of the annotations. We pick $\mathcal{D}_{i+1} = \mathcal{D}'$. A possible case is that the DAM cannot do step (D5) because of a var annotation on the environment. However, by definition of $\|\cdot\|_d$, the environment is annotated only if the variable is also annotated, which is in contradiction with the fact that $\mathcal{D}_i$ is valid. Therefore, the DAM backtracks only because of ev annotations, which are also present on the OAM side because $\mathcal{D}_i \approx \mathcal{O}_i$. The OAM also does a switching step $\mathcal{O}_i \to \mathcal{O}_{i+1}$, and we have $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$.

(D10) We have $\mathcal{D} = \langle \text{env}(\phi) :: \pi | k, \mathbb{F}, \phi \bullet \mathcal{F} \rangle_{\text{bev}} \to \langle k[\phi]^\Delta | \mathbb{F}, \mathcal{F}, \pi \rangle_{\text{ev}} = \mathcal{D}'$. Because $\mathcal{D}$ is a backward configuration, we know $k$ is annotated, and $\mathcal{D}'$ can only do a switching step $\mathcal{D}' \to \langle \pi | k[\phi]^{\text{ev}}, \mathbb{F}, \mathcal{F} \rangle_{\text{bev}} \stackrel{\Delta}{=} \mathcal{D}_{i+1}$. We pick $\mathcal{O}_{i+1} = \mathcal{O}_i$. Because $\mathcal{O}_i \approx \mathcal{D}_i$, we have $[[c]_o(\star)] \triangleright [[k]_d(\phi \bullet \mathcal{F})]$, i.e., $[[c]_o(\star)] \triangleright [[k[\phi]^{\text{ev}}]_d(\mathcal{F})]$. Therefore we have $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$.

(D8) We have $\mathcal{D}_i = \langle \text{appl} :: \pi | l_1, \Box (l_2[\mathcal{F}]) :: \mathbb{F}, \mathcal{F} \rangle_{\text{bev}} \to \langle l_1 @^\emptyset l_2 | \mathbb{F}, \mathcal{F}, \pi \rangle_{\text{ev}} \stackrel{\Delta}{=} \mathcal{D}_{i+1}$. Because $\mathcal{O}_i \approx \mathcal{D}_i$, we must have $\mathcal{O}_i = \langle \Box l :: \mathbb{E} | c \rangle_{\text{bev}} \to \langle c @^\emptyset l | \mathbb{E}, \star \rangle_{\text{ev}} \stackrel{\Delta}{=} \mathcal{O}_{i+1}$, and we know $[[c]_o(\star)] \triangleright [[l_1]_d(\mathcal{F})]$ and $[[l]_o(\star)] \triangleright [[l_2[\mathcal{F}]]_d(\star)]$. The latter implies $[[l]_o(\star)] \triangleright [[l_2]_d(\mathcal{F})]$ by Lemma 25, so we have $[[c @^\emptyset l]_o(\star)] \triangleright [[l_1 @^\emptyset l_2]_d(\mathcal{F})]$ and $\mathcal{O}_{i+1} \approx \mathcal{D}_{i+1}$.

(D9)-(D13) Similar to the case above.

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