we prove for every $i \in\mathbb{N}$ the validity of the rule
\[
\inferrule
{\Gamma\pipe\Delta\vDash E_1\ilr i E_1' \in T_1\cdots}
{\Gamma\pipe\Delta\vDash E_c \ilr i E_c' \in T_c}
\]
\begin{enumerate}
\item$\inferrule{}{\Gamma,x : A,\Gamma' \vDash x \ilr i x \in
A}$. Given $\gamma_1\itylr i {\Gamma,x:A,\Gamma'}\gamma_2$,
then by definition $\gamma_1(x)\itylr i A \gamma_2(x)$.
\item$\inferrule{}{\Gamma\vDash\err\itylr\err\in\u B}$ We
need to show $S_1[\err]\ix\apreorder i \result(S_2[\err])$. By
anti-reduction and strictness of stacks, it is sufficient to show
$\err\ilr i \err$. If $i =0$ there is nothing to show,
otherwise, it follows by reflexivity of $\apreorder$.
\item$\inferrule
{\Gamma\vDash V \ilr i V' \in A \and
\Gamma, x : A \vDash M \ilr i M' \in\u B
}
{\Gamma\vDash\letXbeYinZ V x M \ilr i \letXbeYinZ{V'}{x}{M'}\in\u B}$
Each side takes a $0$-cost step, so by anti-reduction, this reduces to
\[ S_1[M[\gamma_1,V/x]]\ix\apreorder i \result(S_2[M'[\gamma_2,V'/x]])\] which follows by the assumption $\Gamma, x : A \vDash M \ilr i M' \in\u B$
\item$\inferrule
{\Gamma\vDash V \ilr i V' \in0}
{\Gamma\vDash\abort V \ilr i \abort V' \in\u B}$.
By assumption, we get $V[\gamma_1]\logty i {0} V'[\gamma_2]$, but this is a contradiction.
\item$\inferrule
{\Gamma\vDash V \ilr i V' \in A_1}
{\Gamma\vDash\inl V \ilr i \inl V' \in A_1+ A_2}$.
Direct from assumption, rule for sums.
\item$\inferrule
{\Gamma\vDash V \ilr i V' \in A_2}
{\Gamma\vDash\inr V \ilr i \inr V' \in A_1+ A_2}$
Direct from assumption, rule for sums.
\item$\inferrule
{\Gamma\vDash V \ilr i V' \in A_1+ A_2\and
\Gamma, x_1 : A_1\vDash M_1\ilr i M_1' \in\u B\and
\Gamma, x_2 : A_2\vDash M_2\ilr i M_2' \in\u B
}
{\Gamma\vDash\caseofXthenYelseZ V {x_1. M_1}{x_2.M_2}\ilr i \caseofXthenYelseZ{V'}{x_1. M_1'}{x_2.M_2'}\in\u B}$
By case analysis of $V[\gamma_1]\ilr i V'[\gamma_2]$.
\begin{enumerate}
\item If $V[\gamma_1]=\inl V_1, V'[\gamma_2]=\inl V_1'$ with
$V_1\itylr i {A_1} V_1'$, then taking $0$ steps, by anti-reduction
the problem reduces to
\[ S_1[M_1[\gamma_1,V_1/x_1]]\ix\apreorder i \result(S_1[M_1[\gamma_1,V_1/x_1]])\]
which follows by assumption.
\item For $\inr{}$, the same argument.
\end{enumerate}
\item$\inferrule
{}
{\Gamma\vDash()\ilr i ()\in1}$ Immediate by unit rule.
\item$\inferrule
{\Gamma\vDash V_1\ilr i V_1' \in A_1\and
\Gamma\vDash V_2\ilr i V_2' \in A_2}
{\Gamma\vDash(V_1,V_2)\ilr i (V_1',V_2')\in A_1\times A_2}$
Immediate by pair rule.
\item$\inferrule
{\Gamma\vDash V \ilr i V' \in A_1\times A_2\and
\Gamma, x : A_1,y : A_2\vDash M \ilr i M' \in\u B
}
{\Gamma\vDash\pmpairWtoXYinZ V x y M \ilr i \pmpairWtoXYinZ{V'}{x}{y}{M'}\in\u B}$
By $V \itylr i {A_1\times A_2} V'$, we know $V[\gamma_1]=
(V_1,V_2)$ and $V'[\gamma_2]=(V_1', V_2')$ with $V_1\itylr i
{A_1} V_1'$ and $V_2\itylr i {A_2} V_2'$.
Then by anti-reduction, the problem reduces to
\[ S_1[M[\gamma_1,V_1/x,V_2/y]]\ix\apreorder i \result(S_1[M'[\gamma_1,V_1'/x,V_2'/y]])\]
which follows by assumption.
\item$\inferrule
{\Gamma\vDash V \ilr i V' \in A[\mu X.A/X]}
{\Gamma\vDash\rollty{\mu X.A} V \ilr i \rollty{\mu X.A} V' \in\mu X.A }$
If $i =0$, we're done. Otherwise $i=j+1$, and our assumption is
that $V[\gamma_1]\itylr{j+1}{A[\mu X.A/X]} V'[\gamma_2]$ and we need to show
that $\roll V[\gamma_1]\itylr{j+1}{\mu X. A}\roll
V'[\gamma_2]$. By definition, we need to show $V[\gamma_1]\itylr
j {A[\mu X.A/X]} V'[\gamma_2]$, which follows by downward-closure.
\item$\inferrule
{\Gamma\vDash V \ilr i V' \in\mu X. A\and
\Gamma, x : A[\mu X. A/X]\vDash M \ilr i M' \in\u B}
{\Gamma\vDash\pmmuXtoYinZ V x M \ilr i \pmmuXtoYinZ{V'}{x}{M'}\in\u B}$
If $i =0$, then by triviality at $0$, we're done.
Otherwise, $V[\gamma_1]\itylr{j+1}{\mu X. A} V'[\gamma_2]$ so
$V[\gamma_1]=\roll V_\mu, V'[\gamma_2]=\roll V_\mu'$ with
$V_\mu\itylr j {A[\mu X.A/X]} V_\mu'$. Then each side takes $1$ step, so by anti-reduction it is sufficient to show
\[ S_1[M[\gamma_1,V_\mu/x]]\ix\apreorder j \result(S_2[M'[\gamma_2,V_\mu'/x]])\] which follows by assumption and downward closure of the stack, value relations.
\item$\inferrule{\Gamma\vDash M \ilr i M' \in\u B}{\Gamma
\vDash\thunk M \ilr i \thunk M' \in U \u B}$. We need to show
$\thunk M[\gamma_1]\itylr i {U \u B}\thunk M'[\gamma_2]$, so let
$S_1\itylr j {\u B} S_2$ for some $j \leq i$, and we need to show
which follows by anti-reduction for $\gamma_1\itylr i {\Gamma}\gamma_2$ and $N \ilr i N'$.
\item$\inferrule
{\Gamma, x: A \vDash M \ilr i M' \in\u B}
{\Gamma\vDash\lambda x : A . M \ilr i \lambda x:A. M' \in A \to\u B}$
We need to show
\[S_1[\lambda x:A. M[\gamma_1]]\ix\apreorder i \result(S_2[\lambda x:A.M'[\gamma_2]]).\]
By $S_1\itylr i {A \to\u B} S_2$, we know $S_1= S_1'[\bullet V_1]$, $S_2= S_2'[\bullet V_2]$ with $S_1' \itylr i {\u B} S_2'$ and $V_1\itylr i {A} V_2$.
Then by anti-reduction it is sufficient to show
\[
S_1'[M[\gamma_1,V_1/x]]\ix\apreorder i \result(S_2'[M'[\gamma_2,V_2/x]])
\]
which follows by $M \ilr i M'$.
\item$\inferrule
{\Gamma\vDash M \ilr i M' \in A \to\u B\and
\Gamma\vDash V \ilr i V' \in A}
{\Gamma\vDash M\,V \ilr i M'\,V' \in\u B }$
We need to show
\[S_1[M[\gamma_1]\,V[\gamma_1]]\ix\apreorder i \result(S_2[M'[\gamma_2]\,V'[\gamma_2]])\] so by $M \ilr i M'$ it is sufficient to show $S_1[\bullet V[\gamma_1]]\itylr i {A \to\u B} S_2[\bullet V'[\gamma_2]]$ which follows by definition and assumption that $V \ilr i V'$.
\item$\inferrule{}{\Gamma\vdash\{\} : \top}$ We assume we are
given $S_1\itylr i {\top} S_2$, but this is a contradiction.
\item$\inferrule
{\Gamma\vDash M_1\ilr i M_1' \in\u B_1\and
\Gamma\vDash M_2\ilr i M_2' \in\u B_2}
{\Gamma\vDash\pair{M_1}{M_2}\ilr i \pair{M_1'}{M_2'}\in\u B_1\with\u B_2}$
We need to show
\[S_1[\pair{M_1[\gamma_1]}{M_2[\gamma_1]}]\ix\apreorder i \result(S_2[\pair{M_1'[\gamma_1]}{M_2'[\gamma_2]}]).\]
We proceed by case analsysis of $S_1\itylr i {\u B_1\with\u B_2} S_2$
\begin{enumerate}
\item In the first possibility $S_1= S_{1}'[\pi\bullet], S_2=
S_2'[\pi\bullet]$ and $S_1' \itylr i {\u B_1} S_2'$.
Then by anti-reduction, it is sufficient to show
\[ S_1'[M_1[\gamma_1]]\ix\apreorder i \result(S_2'[M_1'[\gamma_2]])\]
which follows by $M_1\ilr i M_1'$.
\item Same as previous case.
\end{enumerate}
\item$\inferrule
{\Gamma\vDash M \ilr i M' \in\u B_1\with\u B_2}
{\Gamma\vDash\pi M \ilr i \pi M' \in\u B_1}$
We need to show $S_1[\pi M[\gamma_1]]\ix\apreorder i \result(S_2[\pi
M'[\gamma_2]])$, which follows by $S_1[\pi\bullet]\itylr i {\u
B_1\with\u B_2} S_2[\pi\bullet]$ and $M \ilr i M'$.
\item$\inferrule{\Gamma\vDash M \ilr i M' \in\u B_1\with\u
B_2}{\Gamma\vDash\pi' M \ilr i \pi' M' \in\u B_2}$ Similar
to previous case.
\item$\inferrule
{\Gamma\vDash M \ilr i M' \in\u B[{\nu\u Y. \u B}/\u Y]}
{\Gamma\vDash\rollty{\nu\u Y. \u B} M \ilr i \rollty{\nu\u Y. \u B} M' \in{\nu\u Y. \u B}}$
We need to show that
\[ S_1[\rollty{\nu\u Y. \u B} M[\gamma_1]]
\ix\apreorder i \result(S_2[\rollty{\nu\u Y. \u B} M'[\gamma_2]])\]
If $i =0$, we invoke triviality at $0$.
Otherwise, $i = j +1$ and we know by $S_1\itylr{j+1}{\nu\u Y. \u B} S_2$ that
$S_1= S_1'[\unroll\bullet]$ and $S_2= S_2'[\unroll\bullet]$ with $S_1' \itylr j {\u B[{\nu\u Y. \u B}/\u Y]} S_2'$, so by anti-reduction it is sufficient to show
\[ S_1'[ M[\gamma_1]]\ix\apreorder i \result(S_2'[ M'[\gamma_2]])\]
which follows by $M \ilr i M'$ and downward-closure.
\item$\inferrule
{\Gamma\vDash M \ilr i M' \in{\nu\u Y. \u B}}
{\Gamma\vDash\unroll M \ilr i \unroll M' \in\u B[{\nu\u Y. \u B}/\u Y]}$
We need to show
\[S_1[\unroll M]\ix\apreorder i \result(S_2[\unroll M']),\] which
follows because $S_1[\unroll\bullet]\itylr i {\nu\u Y. \u B}
S_2[\unroll\bullet]$ and $M \ilr i M'$.
\end{enumerate}
\end{proof}
\begin{corollary}{Reflexivity}
For any $\Gamma\vdash M : \u B$, and $i \in\mathbb{N}$,
\[\Gamma\vDash M \ilrof\apreorder i {} M \in\u B.\]
\[\Gamma\vDash M \ilrof\apreorder i M \in\u B.\]
\end{corollary}
As another corollary we have the following \emph{strengthening} of the
...
...
@@ -2681,7 +2927,7 @@ counts unrolling steps.
\end{corollary}
\begin{proof}
By reflexivity, $\cdot\vDash M \ix\apreorder i M \in\u F 2$ and by
definition $\bullet\ilrof\apreorder i {\u F 2}\bullet$, so
definition $\bullet\itylrof\apreorder i {\u F 2}\bullet$, so
unrolling definitions we get $M \ix\apreorder i \result(M)$.
\end{proof}
...
...
@@ -2717,14 +2963,14 @@ the limit as $i \to \infty$.
\end{proof}
\begin{corollary}{LR is Sound wrt Contextual Preorder}
If $\Gamma\vDash M \ilrof\apreorder\omega{}N \in\u B$
If $\Gamma\vDash M \ilrof\apreorder\omega N \in\u B$
then
$\Gamma\vDash M \ctxize\apreorder N \in\u B$.
TODO: value, stack cases
\end{corollary}
\begin{proof}
Let $C$ be a closing context. By congruence, $C[M]\ilrof\apreorder
\omega{}C[N]$, so because the identity stack is related to itself
\omega C[N]$, so because the identity stack is related to itself
we have
\[ C[M]\ix\apreorder\omega\result(C[N])\]
so by the limit lemma, we have
...
...
@@ -2733,8 +2979,8 @@ the limit as $i \to \infty$.
\end{proof}
\begin{corollary}{LR is Sound wrt Contextual Graduality Ordering}
If $\Gamma\vDash M \ilrof\precltdyn\omega{}N \in\u B$
and $\Gamma\vDash N \ilrof\precgtdyn\omega{}M \in\u B$
If $\Gamma\vDash M \ilrof\precltdyn\omega N \in\u B$
and $\Gamma\vDash N \ilrof\precgtdyn\omega M \in\u B$
then
$\Gamma\vDash M \ctxize\ltdyn N \in\u B$.
TODO: value, stack cases
...
...
@@ -2749,16 +2995,39 @@ our LR is \emph{complete} with respect to contextual graduality
\begin{lemma}{Logical Preorder is Complete wrt Contextual Preorder}
For any $\apreorder$, if $\Gamma\vDash M \ctxize\apreorder N \in
\u B$, then $\Gamma\vDash M \ilrof\apreorder\omega{}N \in\u B$.
\u B$, then $\Gamma\vDash M \ilrof\apreorder\omega N \in\u B$.
\end{lemma}
\begin{proof}
Let $S_1\ilrof\apreorder i {\u B} S_2$ and $\gamma_1\ilrof
\apreorder i \Gamma\gamma_2$. We need to show that
\[
S_1[M[\gamma_1]]\ix\apreorder i S_2[N[\gamma_2]]
S_1[M[\gamma_1]]\ix\apreorder i \result(S_2[N[\gamma_2]])
\]
We use \emph{reflexivity} of the relation:
TODO: adapt the old proof of this below
So we need to construct a \emph{context} that when $M$ or $N$ is
plugged into the hole will reduce to the above.
To do this, first, we deconstruct the context
$x_1:A_1,\ldots,x_n:A_n =\Gamma$. Then we define $\cdot\vdash M'
and similarly for $M_2$, so if $S_1\itylr i {\u B} S_2$ then
\[ S_1[M_1[\gamma_1,V_1[\gamma_1]/x]]\ix\apreorder i \result(S_2[M_2[\gamma_2,V_2[\gamma_2]/x]])\]
\end{proof}
\begin{lemma}{Validity of Error Rules}
For any divergence-least preorder $\apreorder$,
\[\Gamma\vDash S[\err]\ilr i \err\in\u B \]
and
\[\Gamma\vDash\err\ilr i S[\err]\in\u B \]
and for any $\Gamma\vdash M : \u B$
\[\err\ilrof\precltdyn i M\]
and
\[ M \ilrof\precltdyn i \err\]
and
\[\err\ilrof\ltdynsucc i M\]
and
\[ M \ilrof\ltdynsucc i \err\]
\end{lemma}
\begin{proof} All are trivial verifications. \end{proof}
\begin{lemma}{$\precltdyn$ and $\ltdynsucc$ are Models of CBPV}
\begin{enumerate}
...
...
@@ -2875,366 +3243,6 @@ limit is a consequence.
Contextual of the 2 => Contextual ltdyn by earlier lemma
\end{proof}
\begin{figure}
\begin{mathpar}
{\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 \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\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'\\
\Gamma, x : A_1,y : A_2\vDash M \logpole M' \in\u B
}
{\Gamma\vDash\pmpairWtoXYinZ V x y M \logpole\pmpairWtoXYinZ{V'}{x}{y}{M'}\in\u B}$
By $V \logty i {A_1\times A_2} V'$, we know $V[\gamma_1]=
(V_1,V_2)$ and $V'[\gamma_2]=(V_1', V_2')$ with $V_1\logty i
{A_1} V_1'$ and $V_2\logty i {A_2} V_2'$.
Then by anti-reduction, the problem reduces to
\[ S_1[M[\gamma_1,V_1/x,V_2/y]]\ipole i S_1[M'[\gamma_1,V_1'/x,V_2'/y]]\]
which follows by assumption.
\item$\inferrule
{\Gamma\vDash V \logpole V' \in A[\mu X.A/X]}
{\Gamma\vDash\rollty{\mu X.A} V \logpole\rollty{\mu X.A} V' \in\mu X.A }$
If $i =0$, we're done. Otherwise $i=j+1$, and our assumption is
that $V[\gamma_1]\logty{j+1} V'[\gamma_2]$ and we need to show
that $\roll V[\gamma_1]\logty{j+1}{\mu X. A}\roll
V'[\gamma_2]$. By definition, we need to show $V[\gamma_1]\logty
j V'[\gamma_2]$, which follows by downward-closure.
\item$\inferrule
{\Gamma\vDash V \logpole V' \in\mu X. A\and
\Gamma, x : A[\mu X. A/X]\vDash M \logpole M' \in\u B}
{\Gamma\vDash\pmmuXtoYinZ V x M \logpole\pmmuXtoYinZ{V'}{x}{M'}\in\u B}$
If $i =0$, then by triviality at $0$, we're done.
Otherwise, $V[\gamma_1]\logty{j+1}{\mu X. A} V'[\gamma_2]$ so
$V[\gamma_1]=\roll V_\mu, V'[\gamma_2]=\roll V_\mu'$ with
$V_\mu\logty j {A[\mu X.A/X]} V_\mu'$. Then each side takes $1$ step, so by anti-reduction it is sufficient to show
\[ S_1[M[\gamma_1,V_\mu/x]]\ipole j S_2[M'[\gamma_2,V_\mu'/x]]\] which follows by assumption and downward closure of the stack, value relations.
\item$\inferrule{\Gamma\vDash M \logpole M' \in\u B}{\Gamma
\vDash\thunk M \logpole\thunk M' \in U \u B}$. We need to show
$M[\gamma_1]\logty i {U \u B} M'[\gamma_2]$, so let $S_1\logty
j {\u B} S_2$. Then by downward-closure $\gamma_1\logty j
{\Gamma}\gamma_2$, so by assumption, $S_1[M_1[\gamma_1]]\ipole
j S_2[M_2[\gamma_2]]$.
\item$\inferrule
{\Gamma\vDash V \logpole V' \in U \u B}
{\Gamma\vDash\force V \logpole\force V' \in\u B}$.
We need to show $S_1[\force V[\gamma_1]]\ipole i S_2[\force
V'[\gamma_2]]$, which follows by the orthogonality definition of
$V[\gamma_1]\logty i {U \u B} V'[\gamma_2]$.
\item$\inferrule
{\Gamma\vDash V \logpole V' \in A}
{\Gamma\vDash\ret V \logpole\ret V' \in\u F A}$
We need to show $S_1[\ret V[\gamma_1]]\ipole i S_2[\ret
V'[\gamma_2]]$, which follows by the orthogonality definition of
$S_1\logty i {\u F A} S_2$.
\item$\inferrule
{\Gamma\vDash M \logpole M' \in\u F A\and
\Gamma, x: A \vDash N \logpole N' \in\u B}
{\Gamma\vDash\bindXtoYinZ M x N \logpole\bindXtoYinZ{M'}{x}{N'}\in\u B}$.
We need to show $\bindXtoYinZ{M[\gamma_1]} x {N[\gamma_2]}\ipole i \bindXtoYinZ{M'[\gamma_2]}{x}{N'[\gamma_2]}$.
By $M \logpole M' \in\u F A$, it is sufficient to show that
\[\bindXtoYinZ\bullet x {N[\gamma_1]}\logty i {\u F A}\bindXtoYinZ\bullet{x}{N'[\gamma_2]}\]
So let $j \leq i$ and $V \logty j A V'$, then we need to show
\[\bindXtoYinZ{\ret V} x {N[\gamma_1]}\logty j {\u F A}\bindXtoYinZ{\ret V'}{x}{N'[\gamma_2]}\]
By anti-reduction, it is sufficient to show
\[ N[\gamma_1,V/x]\ipole j N'[\gamma_2,V'/x]\]
which follows by anti-reduction for $\gamma_1\logty i {\Gamma}\gamma_2$ and $N \logpole N'$.
\item$\inferrule
{\Gamma, x: A \vDash M \logpole M' \in\u B}
{\Gamma\vDash\lambda x : A . M \logpole\lambda x:A. M' \in A \to\u B}$
We need to show $S_1[\lambda x:A. M[\gamma_1]]\ipole i S_2[\lambda x:A.M'[\gamma_2]]$.
By $S_1\logty i {A \to\u B} S_2$, we know $S_1= S_1'[\bullet V_1]$, $S_2= S_2'[\bullet V_2]$ with $S_1' \logty i {\u B} S_2'$ and $V_1\logty i {A} V_2$.
Then by anti-reduction it is sufficient to show
\[
S_1'[M[\gamma_1,V_1/x]]\ipole i S_2'[M'[\gamma_2,V_2/x]]
\]
which follows by $M \logpole M'$.
\item$\inferrule
{\Gamma\vDash M \logpole M' \in A \to\u B\and
\Gamma\vDash V \logpole V' \in A}
{\Gamma\vDash M\,V \logpole M'\,V' \in\u B }$
We need to show $S_1[M[\gamma_1]\,V[\gamma_1]]\ipole i S_2[M'[\gamma_2]\,V'[\gamma_2]]$ so by $M \logpole M'$ it is sufficient to show $S_1[\bullet V[\gamma_1]]\logty i {A \to\u B} S_2[\bullet V'[\gamma_2]]$ which follows by definition and assumption that $V \logpole V'$.
We need to show $S_1[\pair{M_1[\gamma_1]}{M_2[\gamma_1]}]\ipole i S_2[\pair{M_1'[\gamma_1]}{M_2'[\gamma_2]}]$.
We proceed by case analsysis of $S_1\logty i {\u B_1\with\u B_2} S_2$
\begin{enumerate}
\item In the first possibility $S_1= S_{1}'[\pi\bullet], S_2=
S_2'[\pi\bullet]$ and $S_1' \logty i {\u B_1} S_2'$.
Then by anti-reduction, it is sufficient to show
\[ S_1'[M_1[\gamma_1]]\ipole i S_2'[M_1'[\gamma_2]]\]
which follows by $M_1\logpole M_1'$.
\item Same as previous case.
\end{enumerate}
\item$\inferrule
{\Gamma\vDash M \logpole M' \in\u B_1\with\u B_2}
{\Gamma\vDash\pi M \logpole\pi M' \in\u B_1}$
We need to show $S_1[\pi M[\gamma_1]]\ipole i S_2[\pi
M'[\gamma_2]]$, which follows by $S_1[\pi\bullet]\logty i {\u
B_1\with\u B_2} S_2[\pi\bullet]$ and $M \logpole M'$.
\item$\inferrule{\Gamma\vDash M \logpole M' \in\u B_1\with\u
B_2}{\Gamma\vDash\pi' M \logpole\pi' M' \in\u B_2}$ Similar
to previous case.
\item$\inferrule
{\Gamma\vDash M \logpole M' \in\u B[{\nu\u Y. \u B}/\u Y]}
{\Gamma\vDash\rollty{\nu\u Y. \u B} M \logpole\rollty{\nu\u Y. \u B} M' \in{\nu\u Y. \u B}}$
We need to show that
\[ S_1[\rollty{\nu\u Y. \u B} M[\gamma_1]]
\ipole i S_2[\rollty{\nu\u Y. \u B} M'[\gamma_2]]\]
If $i =0$, we invoke triviality at $0$.
Otherwise, $i = j +1$ and we know by $S_1\logty{j+1}{\nu\u Y. \u B} S_2$ that
$S_1= S_1'[\unroll\bullet]$ and $S_2= S_2'[\unroll\bullet]$ with $S_1' \logty j {\u B[{\nu\u Y. \u B}/\u Y]} S_2'$, so by anti-reduction it is sufficient to show
\[ S_1'[ M[\gamma_1]]\ipole i S_2'[ M'[\gamma_2]]\]
which follows by $M \logpole M'$ and downward-closure.
\item$\inferrule
{\Gamma\vDash M \logpole M' \in{\nu\u Y. \u B}}
{\Gamma\vDash\unroll M \logpole\unroll M' \in\u B[{\nu\u Y. \u B}/\u Y]}$
We need to show $S_1[\unroll M]\ipole i S_2[\unroll M']$, which
follows because $S_1[\unroll\bullet]\logty i {\nu\u Y. \u B}
S_2[\unroll\bullet]$ and $M \logpole M'$.
\end{enumerate}
\end{proof}
\begin{corollary}[Reflexivity/Monotonicity]
For any $\Gamma\vdash M : \u B$, $\Gamma\vdash M \logpole M \in\u B$
\end{corollary}
\begin{theorem}[Completeness of Logical wrt Contextual]
For any pole $\pole$, the logical lifting is complete with respect
to the contextual lifting.
\end{theorem}
\begin{proof}
TODO: modify the proof below
\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$.
\item If $\Gamma\vDash V_1\ltdyn V_2\in A$, then $\Gamma\vDash V_1\ltctx V_2\in A$.
\item If $\Gamma\pipe\bullet:\u B \vDash S_1\ltdyn S_2\in\u B'$,
then $\Gamma\pipe\bullet:\u B \vDash S_1\ltctx S_2\in\u B'$.
\end{enumerate}
\end{theorem}
\begin{proof}
Proved in 2 pieces: congruence and adequacy.
\begin{enumerate}
\item (Congruence) By induction on term constructors, we show the
relations are closed under all term, value, stack constructors.
\item (Adequacy) If $\cdot\vDash M_1\ltdyn M_2\in\u F (1+1)$,
then TODO (nothing really to say?)
\end{enumerate}
\end{proof}
\begin{theorem}[Skewed Transitivity]
All of the following are true
\begin{enumerate}
\item If $V_1\ltlogty\omega A V_1'$, $V_2' \ltlogty\omega A V_2$,
and $V_1\ltlogty i A V_2'$ and $V_1' \ltlogty i A V_2$, then $V_1\ltlogty i A V_2$.
\item If $S_1\ltlogty\omega{\u B} S_1'$, $S_2' \ltlogty\omega{\u B} S_2$,
and $S_1\ltlogty i {\u B} S_2'$ and $S_1' \ltlogty i {\u B} S_2$, then $S_1\ltlogty i {\u B} S_2$.
\item If $M_1\ltlogc\omega M_1'$, $M_2' \ltlogc\omega M_2$,
and $M_1\ltlogc i M_2'$ and $M_1' \ltlogc i M_2$, then $M_1\ltlogc i M_2$.
\end{enumerate}
\end{theorem}
\begin{proof}
TODO: the values and stacks by step-indexed induction on types (uses
fundamental property so prove that first). The term one by direct
verification.
\end{proof}
\begin{corollary}[Transitivity in the Limit]
All of the following are true
\begin{enumerate}
\item If $V_1\ltlogty\omega A V_2\ltlogty\omega A V_3$, then $V_1\ltlogty\omega A V_3$.
\item If $S_1\ltlogty\omega{\u B} S_2\ltlogty\omega{\u B} S_3$, then $S_1\ltlogty\omega{\u B} S_3$.
\item If $M_1\ltlogc\omega M_2\ltlogc\omega M_3$, then $M_1\ltlogc\omega M_3$.
\end{enumerate}
\end{corollary}
\begin{proof}
Use the previous with $V_2/S_2/M_2$ as the middle term.
\end{proof}
\begin{theorem}[LR is Complete for Contextual Error Approximation]
If $\Gamma\vDash M_1\ltctx M_2\in\u B$ then $\Gamma\vDash M_1\ltdyn M_2\in\u B$.
\end{theorem}
\begin{proof}
Let $S_1\ltlogty{i}{\u B} S_2$ and $\gamma_1\ltlogty i \Gamma\gamma_2$.
%
Then define $x_1:A_1,\ldots,x_n:A_n =\Gamma$.
%
Then we define \emph{contexts}$C_1,C_2$ that correspond to the
