diff --git a/paper/gtt.tex b/paper/gtt.tex
index 989fdbf0c40437653b94bd3eedaa946b31d723ff..bf1a4de1eb17b6d8fbef9dd538cd10a34fbd7c7b 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -2657,16 +2657,14 @@ We extend the definition to contexts point-wise.
() \itylr i 1 () &=& \top\\
(V_1,V_1') \itylr i {A \times A'} (V_2, V_2') &=& V_1 \itylr i A V_2 \wedge V_1' \itylr i {A'} V_2'\\
% Should this be a roll or not?
- \rollty {\mu X. A} V_1 \itylr 0 {\mu X. A} \rollty {\mu X. A} V_2 &=& \top\\
- \rollty {\mu X. A} V_1 \itylr {i+1} {\mu X. A} \rollty {\mu X. A} V_2 &=& V_1 \itylr i {A[\mu X.A/X]} V_2\\
+ \rollty {\mu X. A} V_1 \itylr i {\mu X. A} \rollty {\mu X. A} V_2 &=& i = 0 \vee V_1 \itylr {i-1} {A[\mu X.A/X]} V_2\\
V_1 \itylr i {U \u B} V_2 &=& \forall j \leq i, S_1 \itylr j {\u B} S_2.~ S_1[\force V_1] \ix\apreorder j \result(S_2[\force V_2]) \\\\
S_1[\bullet V_1] \itylr i {A \to \u B} S_1[\bullet V_2] & = & V_1 \itylr i A V_2 \wedge S_1 \itylr {i}{\u B} S_2\\
S_1[\pi_1 \bullet] \itylr i {\u B \wedge \u B'} S_2[\pi_1 \bullet] &=& S_1 \itylr i {\u B} S_2\\
S_1[\pi_2 \bullet] \itylr i {\u B \wedge \u B'} S_2[\pi_2 \bullet] &=& S_1 \itylr i {\u B'} S_2\\
S_1 \itylr i {\top} S_2 &=& \bot\\
- S_1[\unroll \bullet] \itylr 0 {\nu \u Y. \u B} S_2[\unroll \bullet] &=& \top\\
- S_1[\unroll \bullet] \itylr {i+1} {\nu \u Y. \u B} S_2[\unroll \bullet] &=& S_1 \itylr i {\u B[\nu \u Y. \u B/\u Y]} S_2\\
+ S_1[\unroll \bullet] \itylr i {\nu \u Y. \u B} S_2[\unroll \bullet] &=& i = 0 \vee S_1 \itylr {i-1} {\u B[\nu \u Y. \u B/\u Y]} S_2\\
S_1 \itylr i {\u F A} S_2 & = & \forall j\leq i, V_1 \itylr j A V_2.~ S_1[\ret V_1] \ix\apreorder j \result(S_2[\ret V_2])
\end{array}
\end{mathpar}
@@ -3161,19 +3159,216 @@ limit is a consequence.
\begin{enumerate}
\item We need to show
\[ S_1[\pmmuXtoYinZ {\rollty{\mu X.A} V[\gamma_1]} x M[\gamma_1]] \ilr i \result(S_2[M[\gamma_2,V[\gamma_2]/x]]) \]
- The left side takes $1$ step so if $i \leq 1$ we are done. Otherwise, we need to show
- \[ S_1[M[\gamma_1,V[\gamma_1]/x]] \ilr {i-1} S_2[M[\gamma_2,V[\gamma_2]/x]] \]
- which follows by anti-reduction because by assumption, we have
- \[ S_1[M[\gamma_1,V[\gamma_1]/x]] \ilr {i} S_2[M[\gamma_2,V[\gamma_2]/x]] \]
- \item The other case is easier, because result is invariant under
- a step.
+ The left side takes $1$ step to $S_1[M[\gamma_1,V[\gamma_1]/x]]$ and we know
+ \[ S_1[M[\gamma_1,V[\gamma_1]/x]] \ilr i \result (S_2[M[\gamma_2,V[\gamma_2]/x]]) \]
+ by assumption and reflexivity, so by anti-reduction we have
+ \[ S_1[\pmmuXtoYinZ {\rollty{\mu X.A} V[\gamma_1]} x M[\gamma_1]] \ilr {i+1} \result(S_2[M[\gamma_2,V[\gamma_2]/x]]) \]
+ so the result follows by downward-closure.
+
+ \item For the other direction we need to show
+ \[ S_1[M[\gamma_1,V[\gamma_1]/x]] \ilr i \result(S_2[\pmmuXtoYinZ {\rollty{\mu X.A} V[\gamma_2]} x M[\gamma_2]]) \]
+ Since results are invariant under steps, this is the same as
+ \[ S_1[M[\gamma_1,V[\gamma_1]/x]] \ilr i \result(S_2[M[\gamma_2,V[\gamma_2/x]]]) \]
+ which follows by reflexivity and assumptions about the stacks
+ and substitutions.
\end{enumerate}
\item $\mu X.A-\eta$:
\begin{enumerate}
\item We need to show for any $\Gamma, x : \mu X. A \vdash M : \u B$,
and appropriate substitutions and stacks,
- \[ S_1[\pmmuXtoYinZ {\rollty{\mu X.A}} {\gamma_1(x)} M] \ilr i \result(S_2[M[\gamma_2]]) \]
- TODO: finish
+ \[ S_1[\pmmuXtoYinZ {\rollty{\mu X.A} {\gamma_1(x)}} {y} M[\rollty{\mu X.A}y/x][\gamma_1]] \ilr i \result(S_2[M[\gamma_2]]) \]
+ By assumption, $\gamma_1(x) \itylr i {\mu X.A} \gamma_2(x)$, so we know
+ \[ \gamma_1(x) = \rollty{\mu X.A} V_1 \]
+ and
+ \[ \gamma_2(x) = \rollty{\mu X.A} V_2 \]
+ so the left side takes a step:
+ \[ S_1[\pmmuXtoYinZ {\rollty{\mu X.A} {\gamma_1(x)}} {y} M[\rollty{\mu X.A}y/x][\gamma_1]] \bigstepsin{1} S_1[M[\rollty{\mu X.A}y/x][\gamma_1][V_1/y]] = S_1[M[\rollty{\mu X.A}V_1/x][\gamma_1]] = S_1[M[\gamma_1]] \]
+ and by refleixivity and assumptions we know
+ \[ S_1[M[\gamma_1]] \ilr {i} \result(S_2[M[\gamma_2]]) \]
+ so by anti-reduction we know
+ \[ S_1[\pmmuXtoYinZ {\rollty{\mu X.A} {\gamma_1(x)}} {y} M[\rollty{\mu X.A}y/x][\gamma_1]] \ilr {i+1} \result(S_2[M[\gamma_2]]) \]
+ so the result follows by downward closure.
+ \item Similarly, to show
+ \[ S_1[M[\gamma_1]] \ilr i \result(S_2[\pmmuXtoYinZ {\rollty{\mu X.A} {\gamma_2(x)}} {y} M[\rollty{\mu X.A}y/x][\gamma_2]]) \]
+ by the same reasoning as above, $\gamma_2(x) = \rollty{\mu X.A}V_2$, so because result is invariant under reduction we need to show
+ \[ S_1[M[\gamma_1]] \ilr i \result(S_2[M[\gamma_2]]) \]
+ which follows by assumption and reflexivity.
+ \end{enumerate}
+ \item $\nu \u Y. \u B-\beta$
+ \begin{enumerate}
+ \item We need to show
+ \[ S_1[\unroll \rollty{\nu \u Y. \u B} M[\gamma_1]] \ix\apreorder i
+ \result(S_2[M[\gamma_2]]) \]
+ By the operational semantics,
+ \[ S_1[\unroll \rollty{\nu \u Y. \u B} M[\gamma_1]] \bigstepsin{1} S_1[M[\gamma_1]] \]
+ and by reflexivity and assumptions
+ \[ S_1[M[\gamma_1]] \ix\apreorder {i} S_2[M[\gamma_2]] \]
+ so the result follows by anti-reduction and downward closure.
+ \item We need to show
+ \[ S_1[M[\gamma_1]] \ix\apreorder i \result(S_2[\unroll \rollty{\nu \u Y. \u B} M[\gamma_2]]) \]
+ By the operational semantics and invariance of result under reduction this is equivalent to
+ \[ S_1[M[\gamma_1]] \ix\apreorder i \result(S_2[M[\gamma_2]]) \]
+ which follows by assumption.
+ \end{enumerate}
+ \item $\nu \u Y. \u B-\eta$
+ \begin{enumerate}
+ \item We need to show
+ \[ S_1[\roll \unroll M[\gamma_1]] \ix\apreorder i \result(S_2[M[\gamma_2]]) \]
+ by assumption, $S_1 \itylr i {\nu \u Y.\u B} S_2$, so
+ \[ S_1 = S_1'[\unroll \bullet] \]
+ and therefore the left side reduces:
+ \begin{align*}
+ S_1[\roll \unroll M[\gamma_1]]
+ &= S_1'[\unroll\roll\unroll M[\gamma_1]]\\
+ &\bigstepsin{1} S_1'[\unroll M[\gamma_1]]\\
+ &= S_1[M[\gamma_1]]
+ \end{align*}
+ and by assumption and reflexivity,
+ \[ S_1[M[\gamma_1]] \ix\apreorder i \result(S_2[M[\gamma_2]]) \]
+ so the result holds by anti-reduction and downward-closure.
+ \item Similarly, we need to show
+ \[ S_1[M[\gamma_1]] \ix\apreorder i \result(S_2[\roll\unroll M[\gamma_2]])\]
+ as above, $S_1 \itylr i {\nu \u Y.\u B} S_2$, so we know
+ \[ S_2 = S_2'[\unroll\bullet] \]
+ so
+ \[ \result(S_2[\roll\unroll M[\gamma_2]]) = \result(S_2[M[\gamma_2]])\]
+ and the result follows by reflexivity, anti-reduction and downard closure.
+ \end{enumerate}
+ \item $0\eta$ Let $\Gamma, x : 0 \vdash M : \u B$.
+ \begin{enumerate}
+ \item We need to show
+ \[ S_1[\absurd \gamma_1(x)] \ix\apreorder i \result(S_2[M[\gamma_2]])\]
+ By assumption $\gamma_1(x) \itylr i 0 \gamma_2(x)$ but this is a contradiction
+ \item Other direction is the same contradiction.
+ \end{enumerate}
+ \item $+\eta$. Let $\Gamma , x:A_1 + A_2 \vdash M : \u B$
+ \begin{enumerate}
+ \item We need to show
+ \[ S_1[\caseofXthenYelseZ {\gamma_1(x)} {x_1. M[\inl x_1/x][\gamma_1]}{x_2. M[\inr x_2/x][\gamma_1]}]
+ \ix\apreorder i \result(S_2[M[\gamma_2]]) \] by assumption
+ $\gamma_1(x) \itylr i {A_1 + A_2} \gamma_2(x)$, so either it's
+ an $\inl$ or $inr$. The cases are symmetric so assume
+ $\gamma_1(x) = \inl V_1$.
+ Then
+ \begin{align*}
+ S_1[\caseofXthenYelseZ {\gamma_1(x)} {x_1. M[\inl x_1/x][\gamma_1]}{x_2. M[\inr x_2/x][\gamma_1]}]
+ &=S_1[\caseofXthenYelseZ {\inl V_1} {x_1. M[\inl x_1/x][\gamma_1]}{x_2. M[\inr x_2/x][\gamma_1]}]\\
+ &\bigstepsin{0} S_1[M[\inl V_1/x][\gamma_1]]\\
+ &= S_1[M[\gamma_1]]
+ \end{align*}
+ and so by anti-reduction it is sufficient to show
+ \[ S_1[M[\gamma_1]] \ix\apreorder i S_2[M[\gamma_2]]\]
+ which follows by reflexivity and assumptions.
+ \item Similarly, We need to show
+ \[
+ \result(S_1[M[\gamma_1]])
+ \ix\apreorder i
+ \result(S_2[\caseofXthenYelseZ {\gamma_2(x)} {x_1. M[\inl x_1/x][\gamma_2]}{x_2. M[\inr x_2/x][\gamma_2]}])
+ \]
+ and by assumption $\gamma_1(x) \itylr i {A_1 + A_2}
+ \gamma_2(x)$, so either it's an $\inl$ or $inr$. The cases are
+ symmetric so assume $\gamma_2(x) = \inl V_2$.
+ Then
+ \[ S_2[\caseofXthenYelseZ {\gamma_2(x)} {x_1. M[\inl x_1/x][\gamma_2]}{x_2. M[\inr x_2/x][\gamma_2]}] \bigstepsin{0}
+ S_2[M[\gamma_2]]
+ \]
+ So the result holds by invariance of result under reduction,
+ reflexivity and assumptions.
+ \end{enumerate}
+ \item $1\eta$ Let $\Gamma, x : 1 \vdash M : \u B$
+ \begin{enumerate}
+ \item We need to show
+ \[ S_1[M[()/x][\gamma_1]] \ix\apreorder i \result(S_2[M[\gamma_2]])\]
+ By assumption $\gamma_1(x) \itylr i 1 \gamma_2(x)$ so $\gamma_1(x) = ()$, so this is equivalent to
+ \[ S_1[M[\gamma_1]] \ix\apreorder i \result(S_2[M[\gamma_2]])\]
+ which follows by reflexivity, assumption.
+ \item Opposite case is similar.
+ \end{enumerate}
+ \item $\times\eta$ Let $\Gamma, x : A_1\times A_2 \vdash M : \u B$
+ \begin{enumerate}
+ \item We need to show
+ \[ S_1[\pmpairWtoXYinZ x {x_1}{y_1} M[(x_1,y_1)/x][\gamma_1]] \ix\apreorder i \result(S_2[M[\gamma_2]]) \]
+ By assumption $\gamma_1(x) \itylr i {A_1\times A_2} \gamma_2(x)$, so $\gamma_1(x) = (V_1,V_2)$, so
+ \begin{align*}
+ S_1[\pmpairWtoXYinZ x {x_1}{y_1} M[(x_1,y_1)/x][\gamma_1]]
+ &= S_1[\pmpairWtoXYinZ {(V_1,V_2)} {x_1}{y_1} M[(x_1,y_1)/x][\gamma_1]]\\
+ &\bigstepsin{0} S_1[M[(V_1,V_2)/x][\gamma_1]]\\
+ &= S_1[M[\gamma_1]]
+ \end{align*}
+ 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 reflexivity, assumption.
+ \item Opposite case is similar.
+ \end{enumerate}
+ \item $U\eta$ Let $\Gamma \vdash V : U \u B$
+ \begin{enumerate}
+ \item We need to show that
+ \[ \thunk\force V[\gamma_1] \itylr i {U \u B} V[\gamma_2] \]
+ So assume $S_1 \itylr j {\u B} S_2$ for some $j\leq i$, then we need to show
+ \[ S_1[\force \thunk\force V[\gamma_1]] \ix\apreorder j \result(S_2[\force V[\gamma_2]])\]
+ The left side takes a step:
+ \[ S_1[\force \thunk\force V[\gamma_1]] \bigstepsin{0} S_1[\force V[\gamma_1]] \]
+ so by anti-reduction it is sufficient to show
+ \[ S_1[\force V[\gamma_1]] \ix\apreorder j \result(S_2[\force V[\gamma_2]]) \]
+ which follows by assumption.
+ \item Opposite case is similar.
+ \end{enumerate}
+ \item $F\eta$
+ \begin{enumerate}
+ \item We need to show that given $S_1 \itylr i {\u F A} S_2$,
+ \[ S_1[\bindXtoYinZ \bullet x \ret x] \itylr i {\u F A} S_2 \]
+ So assume $V_1 \itylr j A V_2$ for some $j\leq i$, then we need to show
+ \[ S_1[\bindXtoYinZ \bullet {\ret V_1} \ret x] \ix\apreorder j \result(S_2[\ret V_2])
+ \]
+ The left side takes a step:
+ \[ S_1[\bindXtoYinZ \bullet {\ret V_1} \ret x] \bigstepsin{0} S_1[\ret V_1]\]
+ so by anti-reduction it is sufficient to show
+ \[ S_1[\ret V_1] \ix\apreorder j \result(S_2[\ret V_2])\]
+ which follows by assumption
+ \item Opposite case is similar.
+ \end{enumerate}
+ \item $\to\eta$ Let $\Gamma \vdash M : A \to \u B$
+ \begin{enumerate}
+ \item We need to show
+ \[ S_1[(\lambda x:A. M[\gamma_1]\, x)] \ix\apreorder i \result(S_2[M[\gamma_2]])
+ \]
+ by assumption that $S_1 \itylr i {A \to \u B} S_2$, we know
+ \[ S_1 = S_1'[\bullet\, V_1]\]
+ so the left side takes a step:
+ \begin{align*}
+ S_1[(\lambda x:A. M[\gamma_1]\, x)]
+ &= S_1'[(\lambda x:A. M[\gamma_1]\, x)\, V_1]\\
+ &\bigstepsin{0} S_1'[M[\gamma_1]\, V_1]\\
+ &= S_1[M[\gamma_1]]
+ \end{align*}
+ 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 reflexivity, assumption.
+ \item Opposite case is similar.
+ \end{enumerate}
+ \item $\with\eta$ Let $\Gamma \vdash M : \u B_1 \with \u B_2$
+ \begin{enumerate}
+ \item We need to show
+ \[ S_1[\pair{\pi M[\gamma_1]}{\pi' M[\gamma_1]}] \ix\apreorder i \result(S_1[M[\gamma_2]]) \]
+ by assumption, $S_1 \itylr i {\u B_1 \with \u B_2} S_2$ so
+ either it starts with a $\pi$ or $\pi'$ so assume that $S_1 =
+ S_1'[\pi \bullet]$ ($\pi'$ case is similar).
+ Then the left side reduces
+ \begin{align*}
+ S_1[\pair{\pi M[\gamma_1]}{\pi' M[\gamma_1]}]
+ &= S_1'[\pi\pair{\pi M[\gamma_1]}{\pi' M[\gamma_1]}]\\
+ &\bigstepsin{0} S_1'[\pi M[\gamma_1]]\\
+ &= S_1[M[\gamma_1]]
+ \end{align*}
+ 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 reflexivity, assumption.
+ \item Opposite case is similar.
+ \end{enumerate}
+ \item $\top\eta$ Let $\Gamma \vdash M : \top$
+ \begin{enumerate}
+ \item In either case, we assume we are given $S_1 \itylr i \top
+ S_2$, but this is a contradiction.
\end{enumerate}
\end{enumerate}
\end{proof}