diff --git a/paper/gtt.tex b/paper/gtt.tex
index 388911f4b331e5295f9889f2e495b52b30116eb3..cafe912577adb78ea63cc84d80fb328b46d8bcb6 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -108,6 +108,7 @@
 %% DEFINITIONS
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+\newcommand{\nats}{\mathbb{N}}
 \newtheorem{principle}{Principle}
 \newcommand{\vtype}{\,\,\text{val type}}
 \newcommand{\ctype}{\,\,\text{comp type}}
@@ -125,11 +126,22 @@
 \newcommand{\ltdynv}{\mathrel{\sqsubseteq_V}}
 \newcommand{\ltdynt}{\mathrel{\sqsubseteq_T}}
 \newcommand{\ltlogty}[2]{\mathrel{\ltdyn^{#1}_{#2}}}
+\newcommand{\pole}{\Bot}
+\newcommand{\ipole}[1]{\mathrel{\pole^{#1}}}
+\newcommand{\logty}[2]{\mathrel{\lesssim^{#1}_{#2,\pole}}}
+\newcommand{\logc}[1]{\mathrel{\pole}^{#1}}
 \newcommand{\ltlogc}[1]{\mathrel{\ltdyn^{#1}_{\vdash}}}
 \newcommand{\ltctx}{\mathrel{\ltdyn^{ctx}}}
 \newcommand{\ltciu}{\mathrel{\ltdyn^{ciu}}}
 \newcommand{\ltlog}{\mathrel{\ltdyn^{log}}}
+
+%% Operational steps
 \newcommand{\step}{\mapsto}
+\newcommand{\stepsin}[1]{\mathrel{\mapsto^{#1}}}
+\newcommand{\stepzero}{\stepsin 0}
+\newcommand{\stepone}{\stepsin 1}
+\newcommand{\bigstepsin}[1]{\mathrel{\Mapsto^{#1}}}
+\newcommand{\bigstepzero}{\bigstepsin{0}}
 
 \newcommand{\pair}[2]{\{ \pi \mapsto {#1} \pipe \pi' \mapsto {#2}\}}
 \newcommand{\tru}{\texttt{true}}
@@ -147,6 +159,7 @@
 \newcommand{\err}{\mho}
 \newcommand{\print}{\text{print}\,\,}
 \newcommand{\roll}{\text{roll}\,\,}
+\newcommand{\rollty}[1]{\text{roll}_{#1}\,\,}
 \newcommand{\unroll}{\text{unroll}\,\,}
 
 \newcommand{\Set}{\text{Set}}
@@ -154,10 +167,14 @@
 \newcommand{\M}{\mathcal{M}}
 \newcommand{\sq}{\square}
 \newcommand{\lett}{\text{let}\,\,}
-\newcommand{\letXbeYinZ}[2]{\lett#1 = #2;}
+\newcommand{\letXbeYinZ}[2]{\lett#2 = #1;}
 \newcommand{\bindXtoYinZ}[2]{\text{bind}\,\,#2 \leftarrow #1;}
 \newcommand{\too}{\text{to}\,\,}
 \newcommand{\case}{\text{case}\,\,}
+\newcommand{\kw}[1]{\text{#1}\,\,}
+\newcommand{\caseofXthenYelseZ}[3]{\case #1 \{ #2 \pipe #3 \}}
+\newcommand{\pmpairWtoXYinZ}[4]{\kw{split} #1 \kw{to} (#2,#3). #4}
+\newcommand{\pmmuXtoYinZ}[4]{\kw{unroll} #1 \kw{to} \roll #2. #3}
 \newcommand{\ret}{\text{ret}\,\,}
 \newcommand{\thunk}{\text{thunk}\,\,}
 \newcommand{\force}{\text{force}\,\,}
@@ -216,8 +233,10 @@
     determines} the behavior of almost all casts of gradual typing.
   %
   This shows that any gradual language that supports both must be
-  equivalent to the lazy system, and any system that differs from it
-  must violate graduality or extensionality (typically the latter).
+  equivalent to the ``wrapping'' semantics, and any system that
+  differs from it must violate graduality or extensionality (typically
+  the latter), extending a previous result for a fragment of
+  call-by-name to full call-by-value and call-by-name.
   %
   On the other hand the structure of the dynamic type itself, which is
   taken for granted to be a sum in previous work, is not uniquely
@@ -483,6 +502,22 @@ call-by-name calculi, we can provide similar uniqueness theorems for
 those systems by restricting GTT to only include the image of those
 embeddings.
 
+Our proof architecture is as follows:
+\begin{tikzcd}
+GTT \arrow[d] \\
+CBPV \arrow[d] \\
+LR \simeq CtxApprox
+\end{tikzcd}
+Our gradual type theory with casts and syntactic theory of term
+dynamism is translated to Call-by-push-value with recursive types and
+an inequational theory.
+%
+In fact, we give multiple translations by varying which dynamic types
+we have in the source and their interpretation in the target.
+%
+We then give a model of the CBPV inequational theory using contextual
+error approximation over the operational semantics of CBPV.
+
 \section{Axiomatic Gradual Type Theory}
 
 \subsection{Call-by-Push-Value, Gradualized}
@@ -662,8 +697,10 @@ interpreted as value types in call-by-push-value.
 
 \section{Theorems in Gradual Type Theory}
 
-From the axiomatics of Gradual Type Theory, we can derive many
-consequences.
+In this section, we derive equational and inequational properties of
+Gradual Type Theory.
+
+\subsection{Basic Structural properties}
 
 \begin{theorem}{Casts (de)composition}
   For any $A \ltdyn A' \ltdyn A''$ and $\u B \ltdyn \ltdyn \u B' \ltdyn \u B''$:
@@ -675,8 +712,65 @@ consequences.
   \end{enumerate}
 \end{theorem}
 
+\subsection{Upcasts are Thunkable, Downcasts are Linear, a posteriori}
+
+While we have shown 
+
+\subsection{Uniqueness Principles for Casts}
+
+From the axiomatics of Gradual Type Theory, we can derive many
+consequences.
+
+
 \section{Contract Translation to Call-by-push-value}
 
+\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[\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}
+
+\subsection{Call-by-push-value Inequational Theory}
+
+Next, we give the inequational theory for our CBPV language.
+%
+
+
+
 \subsection{Cast to Contract Translation}
 
 \subsection{Graduality Logical Relation}
@@ -684,38 +778,63 @@ consequences.
 
 \begin{figure}
   \begin{mathpar}
-    {\ltlogty{i}{A}} \subseteq \{ \cdot \vdash V : A \}^2 \quad\qquad{\ltlogty{i}{\u B}}\subseteq \{ \cdot \pipe \u B \vdash S : \u F (1 + 1) \}^2\quad\qquad {\ltlogc{i}} \subseteq \{ \cdot \vdash M : \u F (1 + 1) \}^2\\
-    M_1 \ltlogc{i} M_2 = (M_1 \step^{< i} \err) \vee (M_1, M_2 \step^{i}) \vee (M_1,M_2 \step^{< i} \ret \tru)\vee (M_1,M_2 \step^{< i} \ret \fls)\\
+    {\logty{i}{A}} \subseteq \{ \cdot \vdash V : A \}^2 \quad\qquad{\logty{i}{\u B}}\subseteq \{ \cdot \pipe \u B \vdash S : \u F (1 + 1) \}^2\quad\qquad {\logc{i}} \subseteq \{ \cdot \vdash M : \u F (1 + 1) \}^2\\
     \begin{array}{rcl}
-      \Gamma \vDash M_1 \ltdyn M_2 \in \u B &=& \forall i \in \mathbb{N}, \gamma_1 \ltlogty i \Gamma \gamma_2, S_1 \ltlogty i {\u B} S_2.~ S_1[M_1[\gamma_1]] \ltlogc i S_2[M_2[\gamma_2]]\\
-      \Gamma \vDash V_1 \ltdyn V_2 \in A &=& \forall i \in \mathbb{N}, \gamma_1 \ltlogty i \Gamma \gamma_2.~ V_1[\gamma_1] \ltlogty i A V_2[\gamma_2]\\
-      \Gamma\pipe \bullet : \u B \vDash S_1 \ltdyn S_2 \in \u B' &=& \forall i \in \mathbb{N}, \gamma_1 \ltlogty i \Gamma \gamma_2, S_1' \ltlogty i {\u B'} S_2'.~ S_1'[S_1[\gamma_1]] \ltlogc i S_2'[S_2[\gamma_2]]\\
+      \Gamma \vDash M_1 \ltdyn M_2 \in \u B &=& \forall i \in \mathbb{N}, \gamma_1 \logty i \Gamma \gamma_2, S_1 \logty i {\u B} S_2.~ S_1[M_1[\gamma_1]] \logc i S_2[M_2[\gamma_2]]\\
+      \Gamma \vDash V_1 \ltdyn V_2 \in A &=& \forall i \in \mathbb{N}, \gamma_1 \logty i \Gamma \gamma_2.~ V_1[\gamma_1] \logty i A V_2[\gamma_2]\\
+      \Gamma\pipe \bullet : \u B \vDash S_1 \ltdyn S_2 \in \u B' &=& \forall i \in \mathbb{N}, \gamma_1 \logty i \Gamma \gamma_2, S_1' \logty i {\u B'} S_2'.~ S_1'[S_1[\gamma_1]] \logc i S_2'[S_2[\gamma_2]]\\
     \end{array}\\
     \begin{array}{rcl}
-      \cdot \ltlogty i {\cdot} \cdot &=& \top\\
-      \gamma_1,x \mapsto V_1 \ltlogty i {\Gamma,x:A} \gamma_2,x\mapsto V_2 &=& \gamma_1 \ltlogty i \Gamma \gamma_2 \wedge V_1 \ltlogty i A V_2\\
-      V_1 \ltlogty i 0 V_2 &=& \bot\\
-      \inl V_1 \ltlogty i {A + A'} \inl V_2 &= & V_1 \ltlogty i A V_2\\
-      \inr V_1 \ltlogty i {A + A'} \inr V_2 &= & V_1 \ltlogty i {A'} V_2 \\
-      () \ltlogty i 1 () &=& \top\\
-      (V_1,V_1') \ltlogty i {A \times A'} (V_2, V_2') &=& V_1 \ltlogty i A V_2 \wedge V_1' \ltlogty i {A'} V_2'\\
+      \cdot \logty i {\cdot} \cdot &=& \top\\
+      \gamma_1,x \mapsto V_1 \logty i {\Gamma,x:A} \gamma_2,x\mapsto V_2 &=& \gamma_1 \logty i \Gamma \gamma_2 \wedge V_1 \logty i A V_2\\
+      V_1 \logty i 0 V_2 &=& \bot\\
+      \inl V_1 \logty i {A + A'} \inl V_2 &= & V_1 \logty i A V_2\\
+      \inr V_1 \logty i {A + A'} \inr V_2 &= & V_1 \logty i {A'} V_2 \\
+      () \logty i 1 () &=& \top\\
+      (V_1,V_1') \logty i {A \times A'} (V_2, V_2') &=& V_1 \logty i A V_2 \wedge V_1' \logty i {A'} V_2'\\
       % Should this be a roll or not?
-      \roll_{\mu X. A} V_1 \ltlogty 0 {\mu X. A} \roll_{\mu X. A} V_2 &=& \top\\
-      \roll_{\mu X. A} V_1 \ltlogty {i+1} {\mu X. A} \roll_{\mu X. A} V_2 &=& V_1 \ltlogty i {A[\mu X.A/X]} V_2\\
-      V_1 \ltlogty i {U \u B} V_2 &=& \forall j \leq i, S_1 \ltlogty j {\u B} S_2.~ S_1[\force V_1] \ltlogc j S_2[\force V_2] \\\\
-
-      S_1[\bullet V_1] \ltlogty i {A \to \u B} S_1[\bullet V_2] & = & V_1 \ltlogty i A V_2 \wedge S_1 \ltlogty {i}{\u B} S_2\\
-      S_1[\pi_1 \bullet] \ltlogty i {\u B \wedge \u B'} S_2[\pi_1 \bullet] &=& S_1 \ltlogty i {\u B} S_2\\
-      S_1[\pi_2 \bullet] \ltlogty i {\u B \wedge \u B'} S_2[\pi_2 \bullet] &=& S_1 \ltlogty i {\u B'} S_2\\
-      S_1 \ltlogty i {\top} S_2 &=& \bot\\
-      S_1[\unroll \bullet] \ltlogty 0 {\nu \u Y. \u B} S_2[\unroll \bullet] &=& \top\\
-      S_1[\unroll \bullet] \ltlogty {i+1} {\nu \u Y. \u B} S_2[\unroll \bullet] &=& S_1 \ltlogty i {\u B[\nu \u Y. \u B/\u Y]} S_2\\
-      S_1 \ltlogty i {\u F A} S_2 & = & \forall j\leq i, V_1 \ltlogty j A V_2.~ S_1[\ret V_1] \ltlogc j S_2[\ret V_2]
+      \rollty {\mu X. A} V_1 \logty 0 {\mu X. A} \rollty {\mu X. A} V_2 &=& \top\\
+      \rollty {\mu X. A} V_1 \logty {i+1} {\mu X. A} \rollty {\mu X. A} V_2 &=& V_1 \logty i {A[\mu X.A/X]} V_2\\
+      V_1 \logty i {U \u B} V_2 &=& \forall j \leq i, S_1 \logty j {\u B} S_2.~ S_1[\force V_1] \logc j S_2[\force V_2] \\\\
+
+      S_1[\bullet V_1] \logty i {A \to \u B} S_1[\bullet V_2] & = & V_1 \logty i A V_2 \wedge S_1 \logty {i}{\u B} S_2\\
+      S_1[\pi_1 \bullet] \logty i {\u B \wedge \u B'} S_2[\pi_1 \bullet] &=& S_1 \logty i {\u B} S_2\\
+      S_1[\pi_2 \bullet] \logty i {\u B \wedge \u B'} S_2[\pi_2 \bullet] &=& S_1 \logty i {\u B'} S_2\\
+      S_1 \logty i {\top} S_2 &=& \bot\\
+      S_1[\unroll \bullet] \logty 0 {\nu \u Y. \u B} S_2[\unroll \bullet] &=& \top\\
+      S_1[\unroll \bullet] \logty {i+1} {\nu \u Y. \u B} S_2[\unroll \bullet] &=& S_1 \logty i {\u B[\nu \u Y. \u B/\u Y]} S_2\\
+      S_1 \logty i {\u F A} S_2 & = & \forall j\leq i, V_1 \logty j A V_2.~ S_1[\ret V_1] \logc j S_2[\ret V_2]
     \end{array}
   \end{mathpar}
   \caption{Observational Error Approximation Logical Relation}
 \end{figure}
 
+\begin{definition}[Pole]
+  A \emph{pole} $\pole$ is a function from natural numbers to sets of
+  closed programs of type $\u F (1 + 1)$ satisfying
+  \begin{enumerate}
+  \item Downward closure: If $M_1 \ipole i M_2$ and $j \leq i$ then $M_1 \ipole j M_2$.
+  \item Step-indexed anti-reduction: If $M_1 \stepsin j M_1'$ and $M_2
+    \step M_2'$ and $M_1' \ipole i M_2'$ then $M_1' \ipole {i+j} M_2'$.
+  \item Step-indexed transitivity: If $M_1 \ipole i M_2$ and $M_2
+    \ipole \omega M_3$ then $M_1 \ipole i M_3$.
+
+    % TODO: might as well make error the least element? not sure
+  \item Error awareness: For all $i \in \nats$, $\err \ipole i \err$.
+  \end{enumerate}
+\end{definition}
+
+\begin{theorem}[Logical Relations Theorem/Fundamental property]
+  For any pole $\pole$, the logical relation generated by it is a
+  congruence, i.e. a model of the congruence rules of CBPV.
+\end{theorem}
+\begin{proof}
+  By induction on the congruence proofs of CBPV.
+  \begin{enumerate}
+  \item 
+  \end{enumerate}
+\end{proof}
+
 \begin{theorem}[LR is Sound for Contextual Error Approximation]
   \begin{enumerate}
   \item If $\Gamma \vDash M_1 \ltdyn M_2 \in \u B$, then  $\Gamma \vDash M_1 \ltctx M_2 \in \u B$.
@@ -971,6 +1090,12 @@ This gives some evidence that the specific choice of connectives of
 CBPV occupies a certain ``sweet spot'' between semantic expressivity
 and amenability to extensions.
 
+\appendix
+
+\section{Call-by-value Gradual Type Theory}
+
+\section{Call-by-name Gradual Type Theory}
+
 \end{document}
 
 %% Local Variables: