% generated by Ott 0.10.14 from: ../tests/test10.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{\testTendrule}[4][]{{\displaystyle\frac{\begin{array}{l}#2\end{array}}{#3}\quad\testTendrulename{#4}}}
\newcommand{\testTenusedrule}[1]{\[#1\]}
\newcommand{\testTenpremise}[1]{ #1 \\}
\newenvironment{testTendefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]}{}
\newenvironment{testTenfundefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]\begin{displaymath}\begin{array}{l}}{\end{array}\end{displaymath}}
\newcommand{\testTenfunclause}[2]{ #1 \equiv #2 \\}
\newcommand{\testTennt}[1]{\mathit{#1}}
\newcommand{\testTenmv}[1]{\mathit{#1}}
\newcommand{\testTenkw}[1]{\mathbf{#1}}
\newcommand{\testTencom}[1]{\text{#1}}
\newcommand{\testTendrulename}[1]{\textsc{#1}}
\newcommand{\testTencomplu}[5]{\overline{#1}^{\,#2\in #3 #4 #5}}
\newcommand{\testTencompu}[3]{\overline{#1}^{\,#2<#3}}
\newcommand{\testTencomp}[2]{\overline{#1}^{\,#2}}
\newcommand{\testTengrammartabular}[1]{\begin{supertabular}{llcllllll}#1\end{supertabular}}
\newcommand{\testTenmetavartabular}[1]{\begin{supertabular}{ll}#1\end{supertabular}}
\newcommand{\testTenrulehead}[3]{$#1$ & & $#2$ & & & \multicolumn{2}{l}{#3}}
\newcommand{\testTenprodline}[6]{& & $#1$ & $#2$ & $#3 #4$ & $#5$ & $#6$}
\newcommand{\testTeninterrule}{\\[5.0mm]}
\newcommand{\testTenafterlastrule}{\\}
\newcommand{\testTenmetavars}{
\testTenmetavartabular{
 $ \mathit{termvar} ,\, \mathit{x} $ & \multicolumn{1}{l}{\testTencom{term variable}} \\
}}

\newcommand{\testTent}{
\testTenrulehead{\testTennt{t}}{::=}{\testTencom{term}}\\ 
\testTenprodline{|}{\mathit{x}}{}{}{}{\testTencom{variable}}\\ 
\testTenprodline{|}{\lambda \, \mathit{x} \, . \, \testTennt{t}}{}{\textsf{bind}\; \mathit{x}\; \textsf{in}\; \testTennt{t}}{}{\testTencom{lambda}}\\ 
\testTenprodline{|}{\testTennt{t} \, \testTennt{t'}}{}{}{}{\testTencom{app}}}

\newcommand{\testTenv}{
\testTenrulehead{\testTennt{v}}{::=}{\testTencom{value}}\\ 
\testTenprodline{|}{\lambda \, \mathit{x} \, . \, \testTennt{t}}{}{}{}{\testTencom{lambda}}}

\newcommand{\testTengrammar}{\testTengrammartabular{
\testTent\testTeninterrule
\testTenv\testTenafterlastrule
}}

% defnss
% defns Jop
% defn reduce
\newcommand{\testTendruleaxXXapp}[1]{\testTendrule[#1]{%
}{
( \, \lambda \, \mathit{x} \, . \, \testTennt{t_{{\mathrm{12}}}} \, ) \, \testTennt{v_{{\mathrm{2}}}} \, \longrightarrow \, \testTenkw{\{} \, \testTennt{v_{{\mathrm{2}}}} \, / \, \mathit{x} \, \testTenkw{\}} \, \testTennt{t_{{\mathrm{12}}}}}{
{\testTendrulename{ax\_app}}{}
}}


\newcommand{\testTendrulectxXXappXXfun}[1]{\testTendrule[#1]{%
\testTenpremise{\testTennt{t_{{\mathrm{1}}}} \, \longrightarrow \, \testTennt{t'_{{\mathrm{1}}}}}%
}{
\testTennt{t_{{\mathrm{1}}}} \, \testTennt{t} \, \longrightarrow \, \testTennt{t'_{{\mathrm{1}}}} \, \testTennt{t}}{
{\testTendrulename{ctx\_app\_fun}}{}
}}


\newcommand{\testTendrulectxXXappXXarg}[1]{\testTendrule[#1]{%
\testTenpremise{\testTennt{t_{{\mathrm{1}}}} \, \longrightarrow \, \testTennt{t'_{{\mathrm{1}}}}}%
}{
\testTennt{v} \, \testTennt{t_{{\mathrm{1}}}} \, \longrightarrow \, \testTennt{v} \, \testTennt{t'_{{\mathrm{1}}}}}{
{\testTendrulename{ctx\_app\_arg}}{}
}}

\newcommand{\testTendefnreduce}[1]{\begin{testTendefnblock}[#1]{$\testTennt{t_{{\mathrm{1}}}} \, \longrightarrow \, \testTennt{t_{{\mathrm{2}}}}$}{\testTencom{$\testTennt{t_{{\mathrm{1}}}}$ reduces to $\testTennt{t_{{\mathrm{2}}}}$}}
\testTenusedrule{\testTendruleaxXXapp{}}
\testTenusedrule{\testTendrulectxXXappXXfun{}}
\testTenusedrule{\testTendrulectxXXappXXarg{}}
\end{testTendefnblock}}


\newcommand{\testTendefnsJop}{
\testTendefnreduce{}}

\newcommand{\testTendefnss}{
\testTendefnsJop}

\newcommand{\testTenall}{\testTenmetavars\\[0pt]
\testTengrammar\\[5.0mm]
\testTendefnss
}

\testTenall
\begin{verbatim}
Definition rules:        3 good    0 bad
Definition rule clauses: 5 good    0 bad
\end{verbatim}
\end{document}