start formalizing the lr

paper/gtt.tex

@@ -125,14 +125,11 @@
 \newcommand{\ltdynt}{\mathrel{\sqsubseteq_T}}
 \newcommand{\ltlogty}[2]{\mathrel{\ltdyn^{#1}_{#2}}}
 \newcommand{\ltlogc}[1]{\mathrel{\ltdyn^{#1}_{\vdash}}}
-\newcommand{\ltdynlt}{\mathrel{\sqsubseteq\prec}}
-\newcommand{\ltdyngt}{\mathrel{\sqsubseteq\succ}}
-\newcommand{\ltltlogty}[2]{\mathrel{\ltdynlt^{#1}_{#2}}}
-\newcommand{\ltgtlogty}[2]{\mathrel{\ltdyngt^{#1}_{#2}}}
-\newcommand{\ltltlogc}[1]{\mathrel{\ltdynlt^{#1}_{\vdash}}}
-\newcommand{\ltgtlogc}[1]{\mathrel{\ltdyngt^{#1}_{\vdash}}}
+\newcommand{\step}{\mapsto}
 
 \newcommand{\pair}[2]{\{ \pi \mapsto {#1} \pipe \pi' \mapsto {#2}\}}
+\newcommand{\tru}{\texttt{true}}
+\newcommand{\fls}{\texttt{false}}
 
 \newcommand{\dyn}{{?}}
 \newcommand{\dynv}{{?}}
@@ -146,7 +143,6 @@
 \newcommand{\roll}{\text{roll}\,\,}
 \newcommand{\unroll}{\text{unroll}\,\,}
 
-
 \newcommand{\Set}{\text{Set}}
 \newcommand{\relto}{\to}
 \newcommand{\M}{\mathcal{M}}
@@ -627,9 +623,13 @@ consequences.
 
 \begin{figure}
   \begin{mathpar}
-    {\ltltlogty{i}{A}},{\ltgtlogty{i}{A}} \subseteq \{ \cdot \vdash V : A \}^2\\
-    {\ltltlogty{i}{\u B}},{\ltgtlogty{i}{\u B}} \subseteq \{ \cdot \pipe \u B \vdash S : \u F (1 + 1) \}^2\\
-    {\ltltlogc{i}}, {\ltgtlogc{i}} \subseteq \{ \cdot \vdash M : \u F (1 + 1) \}^2\\\\
+    {\ltlogty{i}{A}} \subseteq \{ \cdot \vdash V : A \}^2\\
+    {\ltlogty{i}{\u B}}\subseteq \{ \cdot \pipe \u B \vdash S : \u F (1 + 1) \}^2\\
+    {\ltlogc{i}} \subseteq \{ \cdot \vdash M : \u F (1 + 1) \}^2\\\\
+
+    \begin{array}{rcl}
+      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)
+    \end{array}
   \end{mathpar}
   \caption{Observational Approximation Logical Relation}
 \end{figure}