% generated by Ott 0.10.14 from: ../tests/test10st.ott
\documentclass[11pt]{article}
\usepackage{amsmath,amssymb}
\usepackage{supertabular}
\usepackage{geometry}
\usepackage{ifthen}
\geometry{%
a4paper,
% letterpaper,
dvips,
twoside,
left=22.5mm, right=22.5mm,
top=20mm,  bottom=30mm,
}
\usepackage{color}
\begin{document}
\newcommand{\ottdrule}[4][]{{\displaystyle\frac{\begin{array}{l}#2\end{array}}{#3}\quad\ottdrulename{#4}}}
\newcommand{\ottusedrule}[1]{\[#1\]}
\newcommand{\ottpremise}[1]{ #1 \\}
\newenvironment{ottdefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]}{}
\newenvironment{ottfundefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]\begin{displaymath}\begin{array}{l}}{\end{array}\end{displaymath}}
\newcommand{\ottfunclause}[2]{ #1 \equiv #2 \\}
\newcommand{\ottnt}[1]{\mathit{#1}}
\newcommand{\ottmv}[1]{\mathit{#1}}
\newcommand{\ottkw}[1]{\mathbf{#1}}
\newcommand{\ottcom}[1]{\text{#1}}
\newcommand{\ottdrulename}[1]{\textsc{#1}}
\newcommand{\ottcomplu}[5]{\overline{#1}^{\,#2\in #3 #4 #5}}
\newcommand{\ottcompu}[3]{\overline{#1}^{\,#2<#3}}
\newcommand{\ottcomp}[2]{\overline{#1}^{\,#2}}
\newcommand{\ottgrammartabular}[1]{\begin{supertabular}{llcllllll}#1\end{supertabular}}
\newcommand{\ottmetavartabular}[1]{\begin{supertabular}{ll}#1\end{supertabular}}
\newcommand{\ottrulehead}[3]{$#1$ & & $#2$ & & & \multicolumn{2}{l}{#3}}
\newcommand{\ottprodline}[6]{& & $#1$ & $#2$ & $#3 #4$ & $#5$ & $#6$}
\newcommand{\ottinterrule}{\\[5.0mm]}
\newcommand{\ottafterlastrule}{\\}
\newcommand{\ottmetavars}{
\ottmetavartabular{
 $ \mathit{termvar} ,\, \mathit{x} $ & \multicolumn{1}{l}{\ottcom{term variable}} \\
 $ \mathit{typvar} ,\, \mathit{X} $ & \multicolumn{1}{l}{\ottcom{type variable}} \\
}}

\newcommand{\ottt}{
\ottrulehead{\ottnt{t}}{::=}{\ottcom{term}}\\ 
\ottprodline{|}{\mathit{x}}{}{}{}{\ottcom{variable}}\\ 
\ottprodline{|}{\lambda \, \mathit{x} \, . \, \ottnt{t}}{}{\textsf{bind}\; \mathit{x}\; \textsf{in}\; \ottnt{t}}{}{\ottcom{abstraction}}\\ 
\ottprodline{|}{\ottnt{t} \, \ottnt{t'}}{}{}{}{\ottcom{application}}\\ 
\ottprodline{|}{( \, \ottnt{t} \, )} {\textsf{S}}{}{}{}\\ 
\ottprodline{|}{\ottkw{\{} \, \ottnt{t} \, / \, \mathit{x} \, \ottkw{\}} \, \ottnt{t'}} {\textsf{M}}{}{}{}}

\newcommand{\ottv}{
\ottrulehead{\ottnt{v}}{::=}{\ottcom{value}}\\ 
\ottprodline{|}{\lambda \, \mathit{x} \, . \, \ottnt{t}}{}{}{}{\ottcom{abstraction}}}

\newcommand{\ottT}{
\ottrulehead{\ottnt{T}}{::=}{\ottcom{type}}\\ 
\ottprodline{|}{\mathit{X}}{}{}{}{\ottcom{variable}}\\ 
\ottprodline{|}{\ottnt{T} \, \rightarrow \, \ottnt{T'}}{}{}{}{\ottcom{function}}\\ 
\ottprodline{|}{( \, \ottnt{T} \, )} {\textsf{S}}{}{}{}}

\newcommand{\ottG}{
\ottrulehead{\Gamma}{::=}{\ottcom{type environment}}\\ 
\ottprodline{|}{\ottkw{empty}}{}{}{}{}\\ 
\ottprodline{|}{\Gamma \, , \, \mathit{x} \, : \, \ottnt{T}}{}{}{}{}}

\newcommand{\ottterminals}{
\ottrulehead{\ottnt{terminals}}{::=}{}\\ 
\ottprodline{|}{ \lambda }{}{}{}{}\\ 
\ottprodline{|}{ \longrightarrow }{}{}{}{}\\ 
\ottprodline{|}{ \rightarrow }{}{}{}{}\\ 
\ottprodline{|}{ \vdash }{}{}{}{}\\ 
\ottprodline{|}{ \in }{}{}{}{}}

\newcommand{\ottformula}{
\ottrulehead{\ottnt{formula}}{::=}{}\\ 
\ottprodline{|}{\ottnt{judgement}}{}{}{}{}\\ 
\ottprodline{|}{\ottkw{not} \, ( \, \ottnt{formula} \, )}{}{}{}{}\\ 
\ottprodline{|}{\mathit{x} \, = \, \mathit{x'}}{}{}{}{}\\ 
\ottprodline{|}{\mathit{x} \, : \, \ottnt{T} \, \in \, \Gamma}{}{}{}{}}

\newcommand{\ottJtype}{
\ottrulehead{\ottnt{Jtype}}{::=}{}\\ 
\ottprodline{|}{\Gamma \, \vdash \, \ottnt{t} \, : \, \ottnt{T}}{}{}{}{}}

\newcommand{\ottJop}{
\ottrulehead{\ottnt{Jop}}{::=}{}\\ 
\ottprodline{|}{\ottnt{t_{{\mathrm{1}}}} \, \longrightarrow \, \ottnt{t_{{\mathrm{2}}}}}{}{}{}{\ottcom{$\ottnt{t_{{\mathrm{1}}}}$ reduces to $\ottnt{t_{{\mathrm{2}}}}$}}}

\newcommand{\ottjudgement}{
\ottrulehead{\ottnt{judgement}}{::=}{}\\ 
\ottprodline{|}{\ottnt{Jtype}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{Jop}}{}{}{}{}}

\newcommand{\ottuserXXsyntax}{
\ottrulehead{\ottnt{user\_syntax}}{::=}{}\\ 
\ottprodline{|}{\mathit{termvar}}{}{}{}{}\\ 
\ottprodline{|}{\mathit{typvar}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{t}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{v}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{T}}{}{}{}{}\\ 
\ottprodline{|}{\Gamma}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{terminals}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{formula}}{}{}{}{}}

\newcommand{\ottgrammar}{\ottgrammartabular{
\ottt\ottinterrule
\ottv\ottinterrule
\ottT\ottinterrule
\ottG\ottinterrule
\ottterminals\ottinterrule
\ottformula\ottinterrule
\ottJtype\ottinterrule
\ottJop\ottinterrule
\ottjudgement\ottinterrule
\ottuserXXsyntax\ottafterlastrule
}}

% defnss
% defns Jtype
% defn GtT
\newcommand{\ottdruleGtTXXvalueXXname}[1]{\ottdrule[#1]{%
\ottpremise{\mathit{x} \, : \, \ottnt{T} \, \in \, \Gamma}%
}{
\Gamma \, \vdash \, \mathit{x} \, : \, \ottnt{T}}{
{\ottdrulename{GtT\_value\_name}}{}
}}


\newcommand{\ottdruleGtTXXapply}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottnt{t} \, : \, \ottnt{T_{{\mathrm{1}}}} \, \rightarrow \, \ottnt{T_{{\mathrm{2}}}}}%
\ottpremise{\Gamma \, \vdash \, \ottnt{t'} \, : \, \ottnt{T_{{\mathrm{1}}}}}%
}{
\Gamma \, \vdash \, \ottnt{t} \, \ottnt{t'} \, : \, \ottnt{T_{{\mathrm{2}}}}}{
{\ottdrulename{GtT\_apply}}{}
}}


\newcommand{\ottdruleGtTXXlambda}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, , \, \mathit{x_{{\mathrm{1}}}} \, : \, \ottnt{T_{{\mathrm{1}}}} \, \vdash \, \ottnt{t} \, : \, \ottnt{T}}%
}{
\Gamma \, \vdash \, \lambda \, \mathit{x_{{\mathrm{1}}}} \, . \, \ottnt{t} \, : \, \ottnt{T_{{\mathrm{1}}}} \, \rightarrow \, \ottnt{T}}{
{\ottdrulename{GtT\_lambda}}{}
}}

\newcommand{\ottdefnGtT}[1]{\begin{ottdefnblock}[#1]{$\Gamma \, \vdash \, \ottnt{t} \, : \, \ottnt{T}$}{}
\ottusedrule{\ottdruleGtTXXvalueXXname{}}
\ottusedrule{\ottdruleGtTXXapply{}}
\ottusedrule{\ottdruleGtTXXlambda{}}
\end{ottdefnblock}}


\newcommand{\ottdefnsJtype}{
\ottdefnGtT{}}


% defns Jop
% defn reduce
\newcommand{\ottdruleaxXXapp}[1]{\ottdrule[#1]{%
}{
( \, \lambda \, \mathit{x} \, . \, \ottnt{t_{{\mathrm{12}}}} \, ) \, \ottnt{v_{{\mathrm{2}}}} \, \longrightarrow \, \ottkw{\{} \, \ottnt{v_{{\mathrm{2}}}} \, / \, \mathit{x} \, \ottkw{\}} \, \ottnt{t_{{\mathrm{12}}}}}{
{\ottdrulename{ax\_app}}{}
}}


\newcommand{\ottdrulectxXXappXXfun}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{t_{{\mathrm{1}}}} \, \longrightarrow \, \ottnt{t'_{{\mathrm{1}}}}}%
}{
\ottnt{t_{{\mathrm{1}}}} \, \ottnt{t} \, \longrightarrow \, \ottnt{t'_{{\mathrm{1}}}} \, \ottnt{t}}{
{\ottdrulename{ctx\_app\_fun}}{}
}}


\newcommand{\ottdrulectxXXappXXarg}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{t_{{\mathrm{1}}}} \, \longrightarrow \, \ottnt{t'_{{\mathrm{1}}}}}%
}{
\ottnt{v} \, \ottnt{t_{{\mathrm{1}}}} \, \longrightarrow \, \ottnt{v} \, \ottnt{t'_{{\mathrm{1}}}}}{
{\ottdrulename{ctx\_app\_arg}}{}
}}

\newcommand{\ottdefnreduce}[1]{\begin{ottdefnblock}[#1]{$\ottnt{t_{{\mathrm{1}}}} \, \longrightarrow \, \ottnt{t_{{\mathrm{2}}}}$}{\ottcom{$\ottnt{t_{{\mathrm{1}}}}$ reduces to $\ottnt{t_{{\mathrm{2}}}}$}}
\ottusedrule{\ottdruleaxXXapp{}}
\ottusedrule{\ottdrulectxXXappXXfun{}}
\ottusedrule{\ottdrulectxXXappXXarg{}}
\end{ottdefnblock}}


\newcommand{\ottdefnsJop}{
\ottdefnreduce{}}

\newcommand{\ottdefnss}{
\ottdefnsJtype
\ottdefnsJop}

\newcommand{\ottall}{\ottmetavars\\[0pt]
\ottgrammar\\[5.0mm]
\ottdefnss
}

\ottall
\begin{verbatim}
Definition rules:        6 good    0 bad
Definition rule clauses: 12 good    0 bad
\end{verbatim}
\end{document}
