From 55923d3295959c1c8886d5ec01ac29cc9997ec9c Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 5 Jul 2018 10:04:45 -0400
Subject: [PATCH] typo, longify some proofs
---
paper/gtt.tex | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index fb51fe2..0b1d82a 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -7118,7 +7118,7 @@ limit is a consequence.
\omega {\u B} S_3$, then $S_1 \itylr i {\u B} S_3$
\end{enumerate}
\end{lemma}
-\begin{proof}
+\begin{longproof}
Proof is by mutual lexicographic induction on the pair $(i, A)$ or
$(i, \u B)$. All cases are straightforward uses of the inductive
hypotheses except the shifts $U, \u F$.
@@ -7145,7 +7145,7 @@ limit is a consequence.
\[ S_1[\ret V_1] \ix\apreorder j \result(S_2[\ret V_2]) \]
which holds by assumption.
\end{enumerate}
-\end{proof}
+\end{longproof}
\begin{lemma}{Logical Relation is Quantitatively Transitive (Open Terms)}
\begin{enumerate}
@@ -7162,7 +7162,7 @@ limit is a consequence.
$\Gamma\pipe \bullet : \u B \vDash S_1 \ilr i S_3 \in \u B'$.
\end{enumerate}
\end{lemma}
-\begin{proof}
+\begin{longproof}
\begin{enumerate}
\item By induction on the length of the context, follows from closed value case.
\item Assume $\gamma_1 \itylr i \Gamma \gamma_2$ and $S_1 \itylr i {\u B} S_2$.
@@ -7181,7 +7181,7 @@ limit is a consequence.
\omega A V_3[\gamma_2]$ so the result holds by the closed case.
\item Stack case is essentially the same as the value case.
\end{enumerate}
-\end{proof}
+\end{longproof}
\begin{corollary}{Logical Relation is Transitive in the Limit}
\begin{enumerate}
@@ -7488,7 +7488,7 @@ following theorem that says our logical relation is a model of CBPV.
following hold:
\begin{mathpar}
\Gamma \pipe \Delta \vDash E \ix\precltdyn i E' \in \u B\and
- \Gamma \pipe \Delta \vDash E' \ix\ltdynsucc i E \in \u B
+ \Gamma \pipe \Delta \vDash E' \ix{\mathrel{\preceq\gtdyn}} i E \in \u B
\end{mathpar}
\end{lemma}
--
GitLab