diff --git a/Paper.tex b/Paper.tex
index fbb0dc5a..69550e16 100644
--- a/Paper.tex
+++ b/Paper.tex
@@ -1414,14 +1414,9 @@ \section{Precompiled Contracts}\label{app:precompiled}
 \Xi_{\mathtt{ADD}} &\equiv& \Xi_{\mathtt{PRE}} \quad \text{except:}\\
 \Xi_{\mathtt{ADD}}(\boldsymbol{\sigma}, g, I) &\equiv& (\varnothing, 0, A^0, ()) \quad \text{if} \quad |I_\mathbf{d}| - 32 <  I_\mathbf{d}[0..31] \\
 g_r &=& G_{addsubbase} + G_{arithword} \Big\lceil \dfrac{|I_\mathbf{d}|}{32} \Big\rceil \\
-\mathbf{o} &=& (X + Y) \in \mathbb{B}_\ell \\
+\mathbf{o} &=& \mathtt{\tiny BE}(X + Y) \\
 X &=& I_\mathbf{d}[32..(32 + I_\mathbf{d}[0..31] - 1)] \\
-Y &=& I_\mathbf{d}[(32 + I_\mathbf{d}[0..31])..(|I_\mathbf{d}| - 1)] \\
-\ell &=&
-\begin{cases}
-0 &\text{if}\, X = Y = 0 \\
-\lfloor \log_8(X + Y) \rfloor + 1 & \text{otherwise}
-\end{cases}
+Y &=& I_\mathbf{d}[(32 + I_\mathbf{d}[0..31])..(|I_\mathbf{d}| - 1)]
 \end{eqnarray}
 
 The sixth contract performs arbitrary-precision subtraction on non-negative integers.  This is similar to the addition.  The subtraction contract halts exceptionally if the result would be negative.
@@ -1431,14 +1426,9 @@ \section{Precompiled Contracts}\label{app:precompiled}
 \Xi_{\mathtt{SUB}}(\boldsymbol{\sigma}, g, I) &\equiv& (\varnothing, 0, A^0, ()) \quad \text{if} \quad |I_\mathbf{d}| - 32 <  I_\mathbf{d}[0..31] \\
 \Xi_{\mathtt{SUB}}(\boldsymbol{\sigma}, g, I) &\equiv& (\varnothing, 0, A^0, ()) \quad \text{if} \quad X < Y \\
 g_r &=& G_{addsubbase} + G_{arithword} \Big\lceil \dfrac{|I_\mathbf{d}|}{32} \Big\rceil \\
-\mathbf{o} &=& (X - Y) \in \mathbb{B}_\ell \\
+\mathbf{o} &=& \mathtt{\tiny BE}(X - Y) \\
 X &=& I_\mathbf{d}[32..(32 + I_\mathbf{d}[0..31] - 1)] \\
-Y &=& I_\mathbf{d}[(32 + I_\mathbf{d}[0..31])..(|I_\mathbf{d}| - 1)] \\
-\ell &=&
-\begin{cases}
-0 &\text{if}\ X = Y \\
-\lfloor \log_8(X - Y) \rfloor + 1 & \text{otherwise}
-\end{cases}
+Y &=& I_\mathbf{d}[(32 + I_\mathbf{d}[0..31])..(|I_\mathbf{d}| - 1)]
 \end{eqnarray}
 
 The seventh contract performs arbitrary-precision multiplication on non-negative integers.  The input format is the same as that of the addition contract.
@@ -1447,16 +1437,11 @@ \section{Precompiled Contracts}\label{app:precompiled}
 \Xi_{\mathtt{MUL}} &\equiv& \Xi_{\mathtt{PRE}} \quad \text{except:}\\
 \Xi_{\mathtt{MUL}}(\boldsymbol{\sigma}, g, I) &\equiv& (\varnothing, 0, A^0, ()) \quad \text{if} \quad |I_\mathbf{d}| - 32 <  I_\mathbf{d}[0..31] \\
 g_r &=& G_{muldivbase} + G_{arithword} \Big\lceil \dfrac{|I_\mathbf{d}|}{32} \Big\rceil + \ell_X \ell_Y / G_{quaddivisor} \\
-\mathbf{o} &=& (X \times Y) \in \mathbb{B}_\ell \\
+\mathbf{o} &=& \mathtt{\tiny BE}(X \times Y) \\
 X &=& I_\mathbf{d}[32..(32 + I_\mathbf{d}[0..31] - 1)] \\
 \ell_X &=& I_\mathbf{d}[0..31] \\
 Y &=& I_\mathbf{d}[(32 + I_\mathbf{d}[0..31])..(|I_\mathbf{d}| - 1)] \\
-\ell_Y &=& |I_\mathbf{d}| - 32 - \ell_X \\
-\ell &=&
-\begin{cases}
-0 &\text{if}\ X = 0 \ \vee\  Y = 0 \\
-\lfloor \log_8(X \times Y) \rfloor + 1 & \text{otherwise}
-\end{cases}
+\ell_Y &=& |I_\mathbf{d}| - 32 - \ell_X
 \end{eqnarray}
 
 The eigth contract performs arbitrary-precision division on non-negative integers.  The definition is similar to that of the multiplication contract.
@@ -1468,17 +1453,12 @@ \section{Precompiled Contracts}\label{app:precompiled}
 \mathbf{o} &=&
 \begin{cases}
  () & \text{if} \  Y = 0 \\
- \Big\lfloor \dfrac X Y \Big\rfloor \in \mathbb{B}_\ell & \text{otherwise}
+ \mathtt{\tiny BE}\Big(\big\lfloor \dfrac X Y \big\rfloor\Big) & \text{otherwise}
 \end{cases} \\
 X &=& I_\mathbf{d}[32..(32 + I_\mathbf{d}[0..31] - 1)] \\
 \ell_X &=& I_\mathbf{d}[0..31] \\
 Y &=& I_\mathbf{d}[(32 + I_\mathbf{d}[0..31])..(|I_\mathbf{d}| - 1)] \\
-\ell_Y &=& |I_\mathbf{d}| - 32 - \ell_X \\
-\ell &=&
-\begin{cases}
-0 &\text{if}\ Y = 0 \ \vee \ \Big\lfloor \dfrac X Y \Big\rfloor = 0 \\
-\lfloor \log_8(\Big\lfloor \dfrac X Y \Big\rfloor) \rfloor + 1 & \text{otherwise}
-\end{cases}
+\ell_Y &=& |I_\mathbf{d}| - 32 - \ell_X
 \end{eqnarray}
 
 The ninth contract performs arbitrary-precision exponentiation under modulo.  Here, $0 ^ 0$ is taken to be one.
@@ -1494,12 +1474,7 @@ \section{Precompiled Contracts}\label{app:precompiled}
 \mathbf{o} &=&
 \begin{cases}
  () & \text{if} \  M = 0 \\
- B ^ E \bmod M \in \mathbb{B}_\ell & \text{otherwise}
-\end{cases} \\
-\ell &=&
-\begin{cases}
-0 &\text{if}\ M = 0 \quad \vee \quad {B ^ E} \bmod M = 0 \\
-\lfloor \log_8(B ^ E \bmod M) \rfloor + 1 & \text{otherwise}
+ \mathtt{\tiny BE}(B ^ E \bmod M) & \text{otherwise}
 \end{cases}
 \end{eqnarray}