\tr_{\b}^+ N^{\diamond}$.

3.  If $M \tr_{\b\m}^* N$, then $M^{\diamond} \tr_{\b}^* N^{\diamond}$ and $lg(M^{\diamond} \tr_{\b}^* N^{\diamond})
    \geq lg(M \tr_{\b\m}^* N)$.

By induction on $M$. (1) is immediate. (2) is as follows.

$(\mu \a^{\neg(A \f B)}.M \; N) \tr_{\m} \mu \a^{\neg
B}.M[(\a^{\neg(A \f B)} \; L) := (\a^{\neg B} \; (L \; N))]$ is translated by\
$\{(\mu \a.M \; N)\}^{\diamond} = (T_{A \f B} \;\; \l
x_{\a}.M^{\diamond} \; N^{\circ}) \ \tr_{\b}^+ (T_B \; \l
u.M^{\diamond}[x_{\a} := \l v. (u \; (v \; N^{\diamond}))] = (T_B \;
\l x_{\a}.M^{\diamond}[x_{\a} := \l v. (x_{\a} \; (v \;
N^{\diamond}))] \ \tr_{\beta}^* (T_B \; \l x_{\a}.\{M[(\a \; L) := (\a
\; (L \; N))]\}^{\diamond}) = \{\m \a.M[(\a \; L) := (\a \; (L \;
N))]\}^{\diamond}$.

\(3) follows immediately from (1) and (2).

\[sn1-&gt;sn2\] Let $M \in {\cal M}'$. If $M^{\diamond} \in SN_{\b}$, then $M \in
SN_{\b\m}$.

Let $n=\eta_{\b}(M^{\diamond})+1$. If $M \not \in SN_{\b\m}$, there is $N$ such that $M \tr_{\b\m}^* N$ and $lg(M \tr_{\b\m}^*
N) \geq n$. Thus, by lemma \[simulation1\], $M^{\diamond}
\tr_{\b}^* N^{\diamond}$ and $lg(M^{\diamond} \tr_{\b}^*
N^{\diamond}) \geq lg(M \tr_{\b\m}^* N) \geq
\eta_{\b}(M^{\diamond})+1$. This contradicts the definition of $\eta_{\b}(M^{\diamond})$.

\[coding1\] If $\G \v_{{\cal S}^{\m}} M : A$, then $\G^{\diamond} \v_{{\cal S}^c}
M^{\diamond} : A$ where 