% -*- LaTeX -*-
\documentclass{article}
\usepackage{euler,proof,amstext,longtable,fullpage,makeidx}

\makeindex
\begin{document}

\newcommand{\N}[1]{\text{\rm\ttfamily\mdseries{#1}}}
\newcommand{\Head}[1]{\newpage\multicolumn{2}{l}
  {\addtocounter{section}{1}
    \addcontentsline{toc}{section}{\protect\numberline{\thesection} #1}
    \setcounter{subsection}{0}\Large\bfseries\thesection\quad{#1}}}
\newcommand{\Subhead}[1]{\multicolumn{2}{l}
  {\addtocounter{subsection}{1} 
    \addcontentsline{toc}{subsection}{\protect\numberline{\thesubsection} #1}
    \large\bfseries\thesubsection\quad #1}}

\newcommand{\Infer}[2]{\infer{#2}{#1}}
\newcommand{\Step}[3]{\mbox{\infer[\text{#1}]{#2}{#3}}}
\newcommand{\Use}[2]{\mbox{\infer*{#1}{#2}}}
\newcommand{\invert}{\ensuremath{\downarrow}}

\newcommand{\Class}[2]{\fbox{\N{#2} ::= $\cdots$} & \fbox{#1}\index{#1}}
\newcommand{\Def}[3]{\fbox{\N{#2} $\equiv$ {#3}} & \fbox{#1}\index{#1}}
\newcommand{\Syntax}[3]{#3 ::= #2 & \text{(#1)}\index{#1}}
\newcommand{\Scheme}[2]{\fbox{#2} & \fbox{#1}\index{#1}}
\newcommand{\Axiom}[2]{{#2} & \text{(#1)}\index{#1}}
\newcommand{\Rule}[3]{\infer{#3}{#2} & \raisebox{1.5ex}{\text{(#1)}}\index{#1}}
\newcommand{\Thm}[3]{\fbox{\Infer{#2}{#3}} & \fbox{#1}\index{#1}}
\newcommand{\Prooft}[2]{{#2} & \text{(#1)}\index{#1}}
\newcommand{\Proofp}[1]{& \text{(#1)}\index{#1}} 
\newcommand{\Point}[1]{\multicolumn{1}{l}#1}


\newcommand{\zg}[0]{@g@}
\newcommand{\zt}[0]{@t@}
\newcommand{\ze}[0]{@e@}
\newcommand{\zx}[0]{@x@}

\newcommand{\ztunit}[0]{@<>@}
\newcommand{\ztfun}[2]{@#1 -> #2@}

\newcommand{\zunit}[0]{@<>@}
\newcommand{\zvar}[1]{@#1@}
\newcommand{\zfun}[2]{@fun x:#1.#2@}
\newcommand{\zapp}[2]{@#1\ #2@}

\newcommand{\zgn}[0]{@\cdot@}
\newcommand{\zgt}[2]{@#1,x:#2@}

\newcommand{\zmap}[3]{@#1[[#2]] = #3@}
\newcommand{\zsub}[3]{@#1 [#2 / x] = #3@}
\newcommand{\zty}[3]{@#1 |- #2 : #3@}
\newcommand{\zval}[1]{@val\ #1@}
\newcommand{\zev}[2]{@#1 --> #2@}
\newcommand{\zevval}[1]{@evval\ #1@}

\title{Soundness Theorem for Simply-Typed Lambda Calculus \\
  in Abstract Variable Representation}
\author{Stephen Tse}
\date{Aug 1, 2004\footnote{Last update: \today}}
\maketitle

This report is automatically generated by the tool \verb|lf2tex| from
the semantics specification \verb|lambda.elf| (Twelf source) and the
syntactic specification \verb|lambda.tex| (\LaTeX\ source).

  \bigskip
  Some notes about the typesetting used in this report:

  \begin{itemize}
  \item A syntax class is displayed boxed like \fbox{@e@ ::= $\cdots$}
    ({\em terms}).
  \item A syntax entity is displayed unboxed like @e@ ::= @fun x:t. e@
    ({\em functions}).
  \item A judgement form is displayed boxed like \fbox{@g |- e : t@}
    ({\em typings}).
  \item A judgement rule is displayed unboxed like 
    \Infer{@g,x:t1 |- e : t2@}{@g |- fun x:t.e : t1 -> t2@}
    ({\em typing for functions}).
  \item A theorem is displayed boxed like
    \fbox{\Infer{@g |- e1:t@ & @e1 --> e2@}
{@g |- e2 : t@}} ({\em preservations}).

  \item A proof is displayed as a numbered list with the last one of
  the list being the conclusion. (A rule name with downarrow
  ($\downarrow\text{ty-fun}$) means by the inversion of such rule.)
  \end{itemize}

\tableofcontents

\footnotesize
\begin{longtable}{cr}
\csname \@\@input\endcsname lambda.tex2
\end{longtable}

\printindex
\end{document}