diff --git a/paper/gtt.tex b/paper/gtt.tex
index 2d5850ea193a403b8c0fb4bb4b6e41937597670f..72b00d9ea62a7a8b630ac589eda3a80de374ca78 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1958,80 +1958,6 @@ Our pass is almost exactly the same as the one given in the CBPV
 monograph (TODO cite), and so we relegate the details to the extended
 version/appendix.
 
-\subsection{Call-by-push-value operational semantics}
-
-We present the operational semantics for our CBPV in figure TODO ref.
-%
-It is morally the same as one given in the CBPV monograph (TODO:
-cite), but there are two differences.
-%
-First, we present it in a Hieb-Felleisen style, rather than a stack
-machine style, which is merely cosmetic.
-%
-Second, for the purposes of the logical relation, the step relation is
-\emph{quantitative}: we count the steps that unroll an recursive or
-corecursive type.
-
-\begin{figure}
-  \begin{mathpar}
-    S[\err] \stepzero \err\\
-    S[\caseofXthenYelseZ{\inl V}{x_1. M_1}{x_2. M_2}] \stepzero S[M_1[V/x_1]]\\
-    S[\caseofXthenYelseZ{\inr V}{x_1. M_1}{x_2. M_2}] \stepzero S[M_2[V/x_2]]\\
-    S[\pmpairWtoXYinZ{(V_1,V_2)}{x_1}{x_2}{M} \stepzero S[M[V_1/x_1,V_2/x_2]]]\\
-    S[\pmmuXtoYinZ{\rollty A V}{x}{M}] \stepone S[M[V/x]]\\
-    S[\force\thunk M] \stepzero S[M]\\
-    S[\letXbeYinZ V x M] \stepzero S[M[V/x]]\\
-    S[\bindXtoYinZ {\ret V} x M] \stepzero S[M[V/x]]\\
-    S[(\lambda x:A. M)\,V] \stepzero S[M[V/x]]\\
-    S[\pi \pair{M}{M'}] \stepzero S[M]\\
-    S[\pi' \pair{M}{M'}] \stepzero S[M']\\
-    S[\unroll \rollty{\u B} M] \stepone S[M]\\
-
-    \inferrule
-    {}
-    {M \bigstepsin 0 M}
-
-    \inferrule
-    {M_1 \stepsin{i} M_2 \and M_2 \bigstepsin j M_3}
-    {M_1 \bigstepsin {i+j} M_3}
-  \end{mathpar}
-  \caption{CBPV Operational Semantics}
-\end{figure}
-
-\begin{lemma}{Reduction is Deterministic}
-  If $M \step M_1$ and $M \step M_2$, then $M_1 = M_2$.
-\end{lemma}
-
-\begin{lemma}{Subject Reduction}
-  If $\cdot \vdash M : \u F A$ and $M \step M'$ then $\cdot \vdash M'
-  : \u F A$.
-\end{lemma}
-
-\begin{lemma}{Progress}
-  If $\cdot \vdash M : \u F A$ then one of the following holds:
-  \begin{enumerate}
-  \item $M = \err$
-  \item $M = \ret V$ for $\cdot \vdash V : A$
-  \item there exists $M'$ with $M \step M'$
-  \end{enumerate}
-\end{lemma}
-
-\begin{corollary}{Possible Results of Computation}
-  For any $\cdot \vdash M : \u F 2$, one of the following is true
-  \begin{enumerate}
-  \item $M \Uparrow$
-  \item $M \Downarrow \err$
-  \item $M \Downarrow \ret \tru$
-  \item $M \Downarrow \ret \fls$
-  \end{enumerate}
-\end{corollary}
-
-\begin{definition}{Results}
-  Define the set of possible results of a boolean returning
-  computation to be the set $\{ \diverge, \err, \ret \tru, \ret \fls
-  \}$. We denote a result by $R$.
-\end{definition}
-
 \subsection{Call-by-push-value Inequational Theory}
 
 Next, we give the inequational theory for our CBPV language.
@@ -2301,6 +2227,80 @@ Next, we give the inequational theory for our CBPV language.
   \caption{Call-by-push-value logical and error rules}
 \end{figure}
 
+\subsection{Call-by-push-value operational semantics}
+
+We present the operational semantics for our CBPV in figure TODO ref.
+%
+It is morally the same as one given in the CBPV monograph (TODO:
+cite), but there are two differences.
+%
+First, we present it in a Hieb-Felleisen style, rather than a stack
+machine style, which is merely cosmetic.
+%
+Second, for the purposes of the logical relation, the step relation is
+\emph{quantitative}: we count the steps that unroll an recursive or
+corecursive type.
+
+\begin{figure}
+  \begin{mathpar}
+    S[\err] \stepzero \err\\
+    S[\caseofXthenYelseZ{\inl V}{x_1. M_1}{x_2. M_2}] \stepzero S[M_1[V/x_1]]\\
+    S[\caseofXthenYelseZ{\inr V}{x_1. M_1}{x_2. M_2}] \stepzero S[M_2[V/x_2]]\\
+    S[\pmpairWtoXYinZ{(V_1,V_2)}{x_1}{x_2}{M} \stepzero S[M[V_1/x_1,V_2/x_2]]]\\
+    S[\pmmuXtoYinZ{\rollty A V}{x}{M}] \stepone S[M[V/x]]\\
+    S[\force\thunk M] \stepzero S[M]\\
+    S[\letXbeYinZ V x M] \stepzero S[M[V/x]]\\
+    S[\bindXtoYinZ {\ret V} x M] \stepzero S[M[V/x]]\\
+    S[(\lambda x:A. M)\,V] \stepzero S[M[V/x]]\\
+    S[\pi \pair{M}{M'}] \stepzero S[M]\\
+    S[\pi' \pair{M}{M'}] \stepzero S[M']\\
+    S[\unroll \rollty{\u B} M] \stepone S[M]\\
+
+    \inferrule
+    {}
+    {M \bigstepsin 0 M}
+
+    \inferrule
+    {M_1 \stepsin{i} M_2 \and M_2 \bigstepsin j M_3}
+    {M_1 \bigstepsin {i+j} M_3}
+  \end{mathpar}
+  \caption{CBPV Operational Semantics}
+\end{figure}
+
+\begin{lemma}{Reduction is Deterministic}
+  If $M \step M_1$ and $M \step M_2$, then $M_1 = M_2$.
+\end{lemma}
+
+\begin{lemma}{Subject Reduction}
+  If $\cdot \vdash M : \u F A$ and $M \step M'$ then $\cdot \vdash M'
+  : \u F A$.
+\end{lemma}
+
+\begin{lemma}{Progress}
+  If $\cdot \vdash M : \u F A$ then one of the following holds:
+  \begin{enumerate}
+  \item $M = \err$
+  \item $M = \ret V$ for $\cdot \vdash V : A$
+  \item there exists $M'$ with $M \step M'$
+  \end{enumerate}
+\end{lemma}
+
+\begin{corollary}{Possible Results of Computation}
+  For any $\cdot \vdash M : \u F 2$, one of the following is true
+  \begin{enumerate}
+  \item $M \Uparrow$
+  \item $M \Downarrow \err$
+  \item $M \Downarrow \ret \tru$
+  \item $M \Downarrow \ret \fls$
+  \end{enumerate}
+\end{corollary}
+
+\begin{definition}{Results}
+  Define the set of possible results of a boolean returning
+  computation to be the set $\{ \diverge, \err, \ret \tru, \ret \fls
+  \}$. We denote a result by $R$.
+\end{definition}
+
 \subsection{Graduality Logical Relation}
 
 In this section, we establish an operational interpretation of the