% generated by Ott 0.10.14 from: ../tests/leroy-jfp96.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{
 $ \ottmv{name} ,\, \ottmv{t} ,\, \ottmv{x} ,\, \ottmv{v} $ &  \\
 $ \ottmv{stamp} ,\, \ottmv{i} $ &  \\
 $ \ottmv{m} $ &  \\
}}

\newcommand{\ottident}{
\ottrulehead{\ottnt{ident}  ,\ t_i  ,\ x_i  ,\ v_i}{::=}{}\\ 
\ottprodline{|}{ \ottmv{name} _ \ottmv{i} }{}{}{}{}}

\newcommand{\otts}{
\ottrulehead{\ottnt{s}}{::=}{\ottcom{Module expressions}}\\ 
\ottprodline{|}{\ottnt{p}}{}{}{}{\ottcom{access to a structure}}\\ 
\ottprodline{|}{\ottkw{struct} \, \ottnt{d} \, \ottkw{end}}{}{}{}{\ottcom{structure construction}}\\ 
\ottprodline{|}{\ottkw{functor} \, ( \, x_i \, : \, \ottnt{S} \, ) \, \ottnt{s}}{}{\textsf{bind}\; x_i\; \textsf{in}\; \ottnt{s}}{}{\ottcom{functor abstraction}}\\ 
\ottprodline{|}{\ottnt{s} \, ( \, \ottnt{p} \, )}{}{}{}{\ottcom{functor application}}\\ 
\ottprodline{|}{\ottnt{s} \, \ottkw{:>} \, \ottnt{S}}{}{}{}{\ottcom{signature ascription}}\\ 
\ottprodline{|}{\ottnt{s} \, \ottkw{\{} \, x_i \, \leftarrow \, \ottnt{p} \, \ottkw{\}}} {\textsf{M}}{}{}{\ottcom{substitution}}\\ 
\ottprodline{|}{\ottnt{s} \, \ottkw{\{} \, \ottnt{d} \, \leftarrow \, \ottnt{p} \, \ottkw{\}}} {\textsf{M}}{}{}{}\\ 
\ottprodline{|}{\ottnt{s} \, / \, \ottnt{p}} {\textsf{M}}{}{}{}\\ 
\ottprodline{|}{( \, \ottnt{s} \, )} {\textsf{M}}{}{}{}}

\newcommand{\ottd}{
\ottrulehead{\ottnt{d}}{::=}{\ottcom{Structure bodies}}\\ 
\ottprodline{|}{ \epsilon }{}{}{}{}\\ 
\ottprodline{|}{\ottnt{c} \, ; \, \ottnt{d}}{}{\textsf{bind}\; \textrm{cbinders}(\ottnt{c})\; \textsf{in}\; \ottnt{d}}{}{}\\ 
\ottprodline{|}{\ottnt{d_{{\mathrm{1}}}} \, ; \, \ottnt{c} \, ; \, \ottnt{d_{{\mathrm{2}}}}} {\textsf{M}}{}{}{}\\ 
\ottprodline{|}{\ottnt{d} \, \ottkw{\{} \, x_i \, \leftarrow \, \ottnt{p} \, \ottkw{\}}} {\textsf{M}}{}{}{\ottcom{substitution}}\\ 
\ottprodline{|}{\ottnt{d} \, / \, \ottnt{p}} {\textsf{M}}{}{}{}\\ 
\ottprodline{|}{( \, \ottnt{d} \, )} {\textsf{M}}{}{}{}}

\newcommand{\ottc}{
\ottrulehead{\ottnt{c}}{::=}{\ottcom{Definitions}}\\ 
\ottprodline{|}{\ottkw{type} \, t_i \, = \, \ottnt{T}}{}{\textrm{cbinders}=t_i}{}{\ottcom{type binding (non generative)}}\\ 
\ottprodline{|}{\ottkw{datatype} \, t_i}{}{\textrm{cbinders}=t_i}{}{\ottcom{type creation (generative)}}\\ 
\ottprodline{|}{\ottkw{structure} \, x_i \, = \, \ottnt{s}}{}{\textrm{cbinders}=x_i}{}{\ottcom{structure binding}}\\ 
\ottprodline{|}{\ottkw{val} \, v_i \, = \, \ottnt{M}}{}{\textrm{cbinders}=v_i}{}{\ottcom{value binding}}\\ 
\ottprodline{|}{\ottnt{c} \, / \, \ottnt{p}} {\textsf{M}}{}{}{}\\ 
\ottprodline{|}{( \, \ottnt{c} \, )} {\textsf{M}}{}{}{}}

\newcommand{\ottS}{
\ottrulehead{\ottnt{S}}{::=}{\ottcom{Signature expressions}}\\ 
\ottprodline{|}{\ottkw{sig} \, \ottnt{D} \, \ottkw{end}}{}{}{}{\ottcom{simple signature}}\\ 
\ottprodline{|}{\ottkw{functor} \, ( \, x_i \, : \, \ottnt{S_{{\mathrm{1}}}} \, ) \, \ottnt{S_{{\mathrm{2}}}}}{}{\textsf{bind}\; x_i\; \textsf{in}\; \ottnt{S_{{\mathrm{2}}}}}{}{\ottcom{functor signature}}\\ 
\ottprodline{|}{\ottnt{S} \, / \, \ottnt{p}} {\textsf{M}}{}{}{\ottcom{strengthening}}\\ 
\ottprodline{|}{\ottnt{S} \, \ottkw{\{} \, x_i \, \leftarrow \, \ottnt{p} \, \ottkw{\}}} {\textsf{M}}{}{}{\ottcom{substitution}}\\ 
\ottprodline{|}{ \ottnt{S} \{n_i \leftarrow  \ottnt{p} .n | n_i \in BV( \ottnt{D} )\} } {\textsf{M}}{}{}{\ottcom{substitution}}\\ 
\ottprodline{|}{( \, \ottnt{S} \, )} {\textsf{M}}{}{}{}}

\newcommand{\ottD}{
\ottrulehead{\ottnt{D}}{::=}{\ottcom{Signature bodies}}\\ 
\ottprodline{|}{ \epsilon }{}{}{}{}\\ 
\ottprodline{|}{\ottnt{C} \, ; \, \ottnt{D}}{}{\textsf{bind}\; \textrm{Cbinders}(\ottnt{C})\; \textsf{in}\; \ottnt{D}}{}{}\\ 
\ottprodline{|}{\ottnt{D_{{\mathrm{1}}}} \, ; \, \ottnt{C} \, ; \, \ottnt{D_{{\mathrm{2}}}}} {\textsf{M}}{}{}{}\\ 
\ottprodline{|}{\ottnt{D} \, / \, \ottnt{p}} {\textsf{M}}{}{}{\ottcom{strengthening}}\\ 
\ottprodline{|}{( \, \ottnt{D} \, )} {\textsf{M}}{}{}{}}

\newcommand{\ottC}{
\ottrulehead{\ottnt{C}}{::=}{\ottcom{Specifications}}\\ 
\ottprodline{|}{\ottkw{type} \, t_i}{}{\textrm{Cbinders}=t_i}{}{\ottcom{opaque type specification}}\\ 
\ottprodline{|}{\ottkw{type} \, t_i \, = \, \ottnt{T}}{}{\textrm{Cbinders}=t_i}{}{\ottcom{manifest type specification}}\\ 
\ottprodline{|}{\ottkw{structure} \, x_i \, : \, \ottnt{S}}{}{\textrm{Cbinders}=x_i}{}{\ottcom{structure specification}}\\ 
\ottprodline{|}{\ottkw{val} \, v_i \, : \, \ottnt{T}}{}{\textrm{Cbinders}=v_i}{}{\ottcom{value specification}}\\ 
\ottprodline{|}{\ottnt{C} \, / \, \ottnt{p}} {\textsf{M}}{}{}{\ottcom{strengthening}}\\ 
\ottprodline{|}{( \, \ottnt{C} \, )} {\textsf{M}}{}{}{}}

\newcommand{\ottT}{
\ottrulehead{\ottnt{T}}{::=}{\ottcom{Types}}\\ 
\ottprodline{|}{t_i}{}{}{}{\ottcom{lexical type reference}}\\ 
\ottprodline{|}{\ottnt{p} \, . \, \ottmv{t}}{}{}{}{\ottcom{structure-based type reference}}\\ 
\ottprodline{|}{\ottnt{T_{{\mathrm{1}}}} \, \rightarrow \, \ottnt{T_{{\mathrm{2}}}}}{}{}{}{\ottcom{function type}}\\ 
\ottprodline{|}{ \ottnt{T} \{n_i \leftarrow  \ottnt{p} .n | n_i \in BV( \ottnt{D} )\} } {\textsf{M}}{}{}{\ottcom{substitution}}\\ 
\ottprodline{|}{( \, \ottnt{T} \, )} {\textsf{M}}{}{}{}}

\newcommand{\ottp}{
\ottrulehead{\ottnt{p}}{::=}{\ottcom{Structure paths}}\\ 
\ottprodline{|}{x_i}{}{}{}{\ottcom{lexical structure reference}}\\ 
\ottprodline{|}{\ottnt{p} \, . \, \ottmv{x}}{}{}{}{\ottcom{structure-based structure reference}}}

\newcommand{\ottE}{
\ottrulehead{\ottnt{E}}{::=}{\ottcom{Typing contexts}}\\ 
\ottprodline{|}{}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{E} \, ; \, \ottnt{C}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{E_{{\mathrm{1}}}} \, ; \, \ottnt{C} \, ; \, \ottnt{E_{{\mathrm{2}}}}} {\textsf{M}}{}{}{}\\ 
\ottprodline{|}{\ottnt{E} \, ; \, \ottkw{rev} \, \ottnt{D}} {\textsf{M}}{}{}{}}

\newcommand{\ottM}{
\ottrulehead{\ottnt{M}}{::=}{\ottcom{Terms}}\\ 
\ottprodline{|}{v_i}{}{}{}{\ottcom{Lexical term reference}}\\ 
\ottprodline{|}{\ottnt{p} \, . \, \ottmv{v}}{}{}{}{\ottcom{Structure-based term reference}}\\ 
\ottprodline{|}{\lambda \, v_i \, : \, \ottnt{T} \, . \, \ottnt{M}}{}{\textsf{bind}\; v_i\; \textsf{in}\; \ottnt{M}}{}{\ottcom{Function expression}}\\ 
\ottprodline{|}{\ottnt{M_{{\mathrm{1}}}} \, \ottnt{M_{{\mathrm{2}}}}}{}{}{}{\ottcom{Function application}}\\ 
\ottprodline{|}{\ottkw{let} \, \ottnt{d} \, \ottkw{in} \, \ottnt{M}}{}{}{}{\ottcom{Lexical binding}}\\ 
\ottprodline{|}{\ottnt{M} \, \ottkw{\{} \, v_i \, \leftarrow \, \ottnt{V} \, \ottkw{\}}} {\textsf{M}}{}{}{\ottcom{substitution}}\\ 
\ottprodline{|}{ \ottnt{M} \{n_i \leftarrow  \ottnt{p} .n | n_i \in BV( \ottnt{d} )\} } {\textsf{M}}{}{}{\ottcom{substitution}}\\ 
\ottprodline{|}{( \, \ottnt{M} \, )} {\textsf{M}}{}{}{}}

\newcommand{\ottV}{
\ottrulehead{\ottnt{V}}{::=}{\ottcom{Values}}\\ 
\ottprodline{|}{\lambda \, v_i \, : \, \ottnt{T} \, . \, \ottnt{M}}{}{}{}{}}

\newcommand{\ottcV}{
\ottrulehead{\ottnt{cV}}{::=}{\ottcom{Definition values}}\\ 
\ottprodline{|}{\ottkw{type} \, t_i \, = \, \ottnt{T}}{}{}{}{}\\ 
\ottprodline{|}{\ottkw{datatype} \, t_i}{}{}{}{}\\ 
\ottprodline{|}{\ottkw{structure} \, x_i \, = \, \ottnt{sV}}{}{}{}{}\\ 
\ottprodline{|}{\ottkw{val} \, v_i \, = \, \ottnt{V}}{}{}{}{}}

\newcommand{\ottsV}{
\ottrulehead{\ottnt{sV}}{::=}{\ottcom{Module values}}\\ 
\ottprodline{|}{\ottkw{struct} \, \ottnt{dV} \, \ottkw{end}}{}{}{}{}\\ 
\ottprodline{|}{\ottkw{functor} \, ( \, x_i \, : \, \ottnt{S} \, ) \, \ottnt{s}}{}{}{}{}}

\newcommand{\ottdV}{
\ottrulehead{\ottnt{dV}}{::=}{\ottcom{Structure body values}}\\ 
\ottprodline{|}{ \epsilon }{}{}{}{}\\ 
\ottprodline{|}{\ottnt{cV} \, ; \, \ottnt{dV}}{}{}{}{}}

\newcommand{\ottdelta}{
\ottrulehead{\Delta}{::=}{\ottcom{Value environments}}\\ 
\ottprodline{|}{}{}{}{}{}\\ 
\ottprodline{|}{\Delta \, ; \, \ottnt{c}}{}{}{}{}\\ 
\ottprodline{|}{\Delta_{{\mathrm{1}}} \, ; \, \ottnt{c} \, ; \, \Delta_{{\mathrm{2}}}} {\textsf{M}}{}{}{}\\ 
\ottprodline{|}{\Delta \, ; \, \ottkw{rev} \, \ottnt{d}} {\textsf{M}}{}{}{}}

\newcommand{\ottterminals}{
\ottrulehead{\ottnt{terminals}}{::=}{}\\ 
\ottprodline{|}{ \rightarrow }{}{}{}{}\\ 
\ottprodline{|}{ \vdash }{}{}{}{}\\ 
\ottprodline{|}{ \approx }{}{}{}{}\\ 
\ottprodline{|}{ \leftarrow }{}{}{}{}\\ 
\ottprodline{|}{ \mapsto }{}{}{}{}\\ 
\ottprodline{|}{ \lambda }{}{}{}{}\\ 
\ottprodline{|}{ \leadsto }{}{}{}{}}

\newcommand{\ottformula}{
\ottrulehead{\ottnt{formula}}{::=}{}\\ 
\ottprodline{|}{\ottnt{judgement}}{}{}{}{}\\ 
\ottprodline{|}{ x_i \not\in BV( \ottnt{E} ) }{}{}{}{}}

\newcommand{\ottpathE}{
\ottrulehead{\ottnt{pathE}}{::=}{}\\ 
\ottprodline{|}{\ottnt{E} \, \vdash \, \ottnt{p} \, \mapsto \, \ottnt{S}}{}{}{}{}}

\newcommand{\ottWFtype}{
\ottrulehead{\ottnt{WFtype}}{::=}{}\\ 
\ottprodline{|}{\ottnt{E} \, \vdash \, \ottnt{T} \, \ottkw{type}}{}{}{}{}}

\newcommand{\ottWFsig}{
\ottrulehead{\ottnt{WFsig}}{::=}{}\\ 
\ottprodline{|}{\ottnt{E} \, \vdash \, \ottnt{D} \, \ottkw{decl}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{E} \, \vdash \, \ottnt{S} \, \ottkw{signature}}{}{}{}{}}

\newcommand{\otteq}{
\ottrulehead{\ottnt{eq}}{::=}{}\\ 
\ottprodline{|}{\ottnt{E} \, \vdash \, \ottnt{T} \, \approx \, \ottnt{T'}}{}{}{}{}}

\newcommand{\ottsub}{
\ottrulehead{\ottnt{sub}}{::=}{}\\ 
\ottprodline{|}{\ottnt{E} \, \vdash \, \ottnt{S} \, \ottkw{<:} \, \ottnt{S'}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{E} \, \vdash \, \ottnt{D} \, \ottkw{<:} \, \ottnt{D'}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{E} \, \vdash \, \ottnt{C} \, \ottkw{<:} \, \ottnt{C'}}{}{}{}{}}

\newcommand{\otttyp}{
\ottrulehead{\ottnt{typ}}{::=}{}\\ 
\ottprodline{|}{\ottnt{E} \, \vdash \, \ottnt{s} \, : \, \ottnt{S}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{E} \, \vdash \, \ottnt{c} \, : \, \ottnt{C}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{E} \, \vdash \, \ottnt{d} \, : \, \ottnt{D}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{E} \, \vdash \, \ottnt{M} \, : \, \ottnt{T}}{}{}{}{}}

\newcommand{\ottpathDelta}{
\ottrulehead{\ottnt{pathDelta}}{::=}{}\\ 
\ottprodline{|}{\Delta \, \vdash \, \ottnt{p} \, \mapsto \, \ottnt{s}}{}{}{}{}}

\newcommand{\ottreduce}{
\ottrulehead{\ottnt{reduce}}{::=}{}\\ 
\ottprodline{|}{\Delta \, \vdash \, \ottnt{M} \, \leadsto \, \ottnt{M'}}{}{}{}{}\\ 
\ottprodline{|}{\Delta \, \vdash \, \ottnt{c} \, \leadsto \, \ottnt{c'}}{}{}{}{}\\ 
\ottprodline{|}{\Delta \, \vdash \, \ottnt{d} \, \leadsto \, \ottnt{d'}}{}{}{}{}\\ 
\ottprodline{|}{\Delta \, \vdash \, \ottnt{s} \, \leadsto \, \ottnt{s'}}{}{}{}{}}

\newcommand{\ottdeltaE}{
\ottrulehead{\ottnt{deltaE}}{::=}{}\\ 
\ottprodline{|}{\vdash \, \Delta \, : \, \ottnt{E}}{}{}{}{}}

\newcommand{\ottjudgement}{
\ottrulehead{\ottnt{judgement}}{::=}{}\\ 
\ottprodline{|}{\ottnt{pathE}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{WFtype}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{WFsig}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{eq}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{sub}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{typ}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{pathDelta}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{reduce}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{deltaE}}{}{}{}{}}

\newcommand{\ottuserXXsyntax}{
\ottrulehead{\ottnt{user\_syntax}}{::=}{}\\ 
\ottprodline{|}{\ottmv{name}}{}{}{}{}\\ 
\ottprodline{|}{\ottmv{stamp}}{}{}{}{}\\ 
\ottprodline{|}{\ottmv{m}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{ident}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{s}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{d}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{c}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{S}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{D}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{C}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{T}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{p}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{E}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{M}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{V}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{cV}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{sV}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{dV}}{}{}{}{}\\ 
\ottprodline{|}{\Delta}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{terminals}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{formula}}{}{}{}{}}

\newcommand{\ottgrammar}{\ottgrammartabular{
\ottident\ottinterrule
\otts\ottinterrule
\ottd\ottinterrule
\ottc\ottinterrule
\ottS\ottinterrule
\ottD\ottinterrule
\ottC\ottinterrule
\ottT\ottinterrule
\ottp\ottinterrule
\ottE\ottinterrule
\ottM\ottinterrule
\ottV\ottinterrule
\ottcV\ottinterrule
\ottsV\ottinterrule
\ottdV\ottinterrule
\ottdelta\ottinterrule
\ottterminals\ottinterrule
\ottformula\ottinterrule
\ottpathE\ottinterrule
\ottWFtype\ottinterrule
\ottWFsig\ottinterrule
\otteq\ottinterrule
\ottsub\ottinterrule
\otttyp\ottinterrule
\ottpathDelta\ottinterrule
\ottreduce\ottinterrule
\ottdeltaE\ottinterrule
\ottjudgement\ottinterrule
\ottuserXXsyntax\ottafterlastrule
}}

% defnss
% defns pathE
% defn pathE
\newcommand{\ottdrulepathEOne}[1]{\ottdrule[#1]{%
}{
\ottnt{E_{{\mathrm{1}}}} \, ; \, \ottkw{structure} \, x_i \, : \, \ottnt{S} \, ; \, \ottnt{E_{{\mathrm{2}}}} \, \vdash \, x_i \, \mapsto \, \ottnt{S} \, / \, x_i}{
{\ottdrulename{pathE1}}{}
}}


\newcommand{\ottdrulepathETwo}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{p} \, \mapsto \, \ottkw{sig} \, \ottnt{D_{{\mathrm{1}}}} \, ; \, \ottkw{structure} \,  \ottmv{x} _ \ottmv{i}  \, : \, \ottnt{S} \, ; \, \ottnt{D_{{\mathrm{2}}}} \, \ottkw{end}}%
}{
\ottnt{E} \, \vdash \, \ottnt{p} \, . \, \ottmv{x} \, \mapsto \,  \ottnt{S} \{n_i \leftarrow  \ottnt{p} .n | n_i \in BV( \ottnt{D_{{\mathrm{1}}}} )\} }{
{\ottdrulename{pathE2}}{}
}}

\newcommand{\ottdefnpathE}[1]{\begin{ottdefnblock}[#1]{$\ottnt{E} \, \vdash \, \ottnt{p} \, \mapsto \, \ottnt{S}$}{}
\ottusedrule{\ottdrulepathEOne{}}
\ottusedrule{\ottdrulepathETwo{}}
\end{ottdefnblock}}


\newcommand{\ottdefnspathE}{
\ottdefnpathE{}}


% defns WFtype
% defn WFtype
\newcommand{\ottdruleWFtypeOne}[1]{\ottdrule[#1]{%
}{
\ottnt{E_{{\mathrm{1}}}} \, ; \, \ottkw{type} \, t_i \, ; \, \ottnt{E_{{\mathrm{2}}}} \, \vdash \, t_i \, \ottkw{type}}{
{\ottdrulename{WFtype1}}{}
}}


\newcommand{\ottdruleWFtypeTwo}[1]{\ottdrule[#1]{%
}{
\ottnt{E_{{\mathrm{1}}}} \, ; \, \ottkw{type} \, t_i \, = \, \ottnt{T} \, ; \, \ottnt{E_{{\mathrm{2}}}} \, \vdash \, t_i \, \ottkw{type}}{
{\ottdrulename{WFtype2}}{}
}}


\newcommand{\ottdruleWFtypeThree}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{p} \, \mapsto \, \ottkw{sig} \, \ottnt{D_{{\mathrm{1}}}} \, ; \, \ottkw{type} \,  \ottmv{t} _ \ottmv{i}  \, ; \, \ottnt{D_{{\mathrm{2}}}} \, \ottkw{end}}%
}{
\ottnt{E} \, \vdash \, \ottnt{p} \, . \, \ottmv{t} \, \ottkw{type}}{
{\ottdrulename{WFtype3}}{}
}}


\newcommand{\ottdruleWFtypeFour}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{p} \, \mapsto \, \ottkw{sig} \, \ottnt{D_{{\mathrm{1}}}} \, ; \, \ottkw{type} \,  \ottmv{t} _ \ottmv{i}  \, = \, \ottnt{T} \, ; \, \ottnt{D_{{\mathrm{2}}}} \, \ottkw{end}}%
}{
\ottnt{E} \, \vdash \, \ottnt{p} \, . \, \ottmv{t} \, \ottkw{type}}{
{\ottdrulename{WFtype4}}{}
}}


\newcommand{\ottdruleWFtypeFive}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{T_{{\mathrm{1}}}} \, \ottkw{type}}%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{T_{{\mathrm{2}}}} \, \ottkw{type}}%
}{
\ottnt{E} \, \vdash \, ( \, \ottnt{T_{{\mathrm{1}}}} \, \rightarrow \, \ottnt{T_{{\mathrm{2}}}} \, ) \, \ottkw{type}}{
{\ottdrulename{WFtype5}}{}
}}

\newcommand{\ottdefnWFtype}[1]{\begin{ottdefnblock}[#1]{$\ottnt{E} \, \vdash \, \ottnt{T} \, \ottkw{type}$}{}
\ottusedrule{\ottdruleWFtypeOne{}}
\ottusedrule{\ottdruleWFtypeTwo{}}
\ottusedrule{\ottdruleWFtypeThree{}}
\ottusedrule{\ottdruleWFtypeFour{}}
\ottusedrule{\ottdruleWFtypeFive{}}
\end{ottdefnblock}}


\newcommand{\ottdefnsWFtype}{
\ottdefnWFtype{}}


% defns WFsig
% defn WFdecl
\newcommand{\ottdruleWFdeclOne}[1]{\ottdrule[#1]{%
}{
\ottnt{E} \, \vdash \,  \epsilon  \, \ottkw{decl}}{
{\ottdrulename{WFdecl1}}{}
}}


\newcommand{\ottdruleWFdeclTwo}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{T} \, \ottkw{type}}%
\ottpremise{\ottnt{E} \, ; \, \ottkw{type} \, t_i \, = \, \ottnt{T} \, \vdash \, \ottnt{D} \, \ottkw{decl}}%
}{
\ottnt{E} \, \vdash \, ( \, \ottkw{type} \, t_i \, = \, \ottnt{T} \, ; \, \ottnt{D} \, ) \, \ottkw{decl}}{
{\ottdrulename{WFdecl2}}{}
}}


\newcommand{\ottdruleWFdeclThree}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, ; \, \ottkw{type} \, t_i \, \vdash \, \ottnt{D} \, \ottkw{decl}}%
}{
\ottnt{E} \, \vdash \, ( \, \ottkw{type} \, t_i \, ; \, \ottnt{D} \, ) \, \ottkw{decl}}{
{\ottdrulename{WFdecl3}}{}
}}


\newcommand{\ottdruleWFdeclFour}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{S} \, \ottkw{signature}}%
\ottpremise{\ottnt{E} \, ; \, \ottkw{structure} \, x_i \, : \, \ottnt{S} \, \vdash \, \ottnt{D} \, \ottkw{decl}}%
}{
\ottnt{E} \, \vdash \, ( \, \ottkw{structure} \, x_i \, : \, \ottnt{S} \, ; \, \ottnt{D} \, ) \, \ottkw{decl}}{
{\ottdrulename{WFdecl4}}{}
}}


\newcommand{\ottdruleWFdeclFive}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{T} \, \ottkw{type}}%
\ottpremise{\ottnt{E} \, ; \, \ottkw{val} \, v_i \, : \, \ottnt{T} \, \vdash \, \ottnt{D} \, \ottkw{decl}}%
}{
\ottnt{E} \, \vdash \, ( \, \ottkw{val} \, v_i \, : \, \ottnt{T} \, ; \, \ottnt{D} \, ) \, \ottkw{decl}}{
{\ottdrulename{WFdecl5}}{}
}}

\newcommand{\ottdefnWFdecl}[1]{\begin{ottdefnblock}[#1]{$\ottnt{E} \, \vdash \, \ottnt{D} \, \ottkw{decl}$}{}
\ottusedrule{\ottdruleWFdeclOne{}}
\ottusedrule{\ottdruleWFdeclTwo{}}
\ottusedrule{\ottdruleWFdeclThree{}}
\ottusedrule{\ottdruleWFdeclFour{}}
\ottusedrule{\ottdruleWFdeclFive{}}
\end{ottdefnblock}}


% defn WFsig
\newcommand{\ottdruleWFsigOne}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{D} \, \ottkw{decl}}%
}{
\ottnt{E} \, \vdash \, ( \, \ottkw{sig} \, \ottnt{D} \, \ottkw{end} \, ) \, \ottkw{signature}}{
{\ottdrulename{WFsig1}}{}
}}


\newcommand{\ottdruleWFsigTwo}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{S_{{\mathrm{1}}}} \, \ottkw{signature}}%
\ottpremise{\ottnt{E} \, ; \, \ottkw{structure} \, x_i \, : \, \ottnt{S_{{\mathrm{1}}}} \, \vdash \, \ottnt{S_{{\mathrm{2}}}} \, \ottkw{signature}}%
}{
\ottnt{E} \, \vdash \, ( \, \ottkw{functor} \, ( \, x_i \, : \, \ottnt{S_{{\mathrm{1}}}} \, ) \, \ottnt{S_{{\mathrm{2}}}} \, ) \, \ottkw{signature}}{
{\ottdrulename{WFsig2}}{}
}}

\newcommand{\ottdefnWFsig}[1]{\begin{ottdefnblock}[#1]{$\ottnt{E} \, \vdash \, \ottnt{S} \, \ottkw{signature}$}{}
\ottusedrule{\ottdruleWFsigOne{}}
\ottusedrule{\ottdruleWFsigTwo{}}
\end{ottdefnblock}}


\newcommand{\ottdefnsWFsig}{
\ottdefnWFdecl{}
\ottdefnWFsig{}}


% defns eq
% defn eqT
\newcommand{\ottdruleeqTOne}[1]{\ottdrule[#1]{%
}{
\ottnt{E_{{\mathrm{1}}}} \, ; \, \ottkw{type} \, t_i \, = \, \ottnt{T} \, ; \, \ottnt{E_{{\mathrm{2}}}} \, \vdash \, t_i \, \approx \, \ottnt{T}}{
{\ottdrulename{eqT1}}{}
}}


\newcommand{\ottdruleeqTTwo}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{p} \, \mapsto \, \ottkw{sig} \, \ottnt{D_{{\mathrm{1}}}} \, ; \, \ottkw{type} \,  \ottmv{t} _ \ottmv{i}  \, = \, \ottnt{T} \, ; \, \ottnt{D_{{\mathrm{2}}}} \, \ottkw{end}}%
}{
\ottnt{E} \, \vdash \, \ottnt{p} \, . \, \ottmv{t} \, \approx \,  \ottnt{T} \{n_i \leftarrow  \ottnt{p} .n | n_i \in BV( \ottnt{D_{{\mathrm{1}}}} )\} }{
{\ottdrulename{eqT2}}{}
}}


\newcommand{\ottdruleeqTThree}[1]{\ottdrule[#1]{%
}{
\ottnt{E} \, \vdash \, \ottnt{T} \, \approx \, \ottnt{T}}{
{\ottdrulename{eqT3}}{}
}}


\newcommand{\ottdruleeqTFour}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{T_{{\mathrm{2}}}} \, \approx \, \ottnt{T_{{\mathrm{1}}}}}%
}{
\ottnt{E} \, \vdash \, \ottnt{T_{{\mathrm{1}}}} \, \approx \, \ottnt{T_{{\mathrm{2}}}}}{
{\ottdrulename{eqT4}}{}
}}


\newcommand{\ottdruleeqTFive}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{T_{{\mathrm{1}}}} \, \approx \, \ottnt{T_{{\mathrm{2}}}}}%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{T_{{\mathrm{2}}}} \, \approx \, \ottnt{T_{{\mathrm{3}}}}}%
}{
\ottnt{E} \, \vdash \, \ottnt{T_{{\mathrm{1}}}} \, \approx \, \ottnt{T_{{\mathrm{3}}}}}{
{\ottdrulename{eqT5}}{}
}}


\newcommand{\ottdruleeqTSix}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{T_{{\mathrm{1}}}} \, \approx \, \ottnt{T_{{\mathrm{3}}}}}%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{T_{{\mathrm{2}}}} \, \approx \, \ottnt{T_{{\mathrm{4}}}}}%
}{
\ottnt{E} \, \vdash \, ( \, \ottnt{T_{{\mathrm{1}}}} \, \rightarrow \, \ottnt{T_{{\mathrm{2}}}} \, ) \, \approx \, ( \, \ottnt{T_{{\mathrm{3}}}} \, \rightarrow \, \ottnt{T_{{\mathrm{4}}}} \, )}{
{\ottdrulename{eqT6}}{}
}}

\newcommand{\ottdefneqT}[1]{\begin{ottdefnblock}[#1]{$\ottnt{E} \, \vdash \, \ottnt{T} \, \approx \, \ottnt{T'}$}{}
\ottusedrule{\ottdruleeqTOne{}}
\ottusedrule{\ottdruleeqTTwo{}}
\ottusedrule{\ottdruleeqTThree{}}
\ottusedrule{\ottdruleeqTFour{}}
\ottusedrule{\ottdruleeqTFive{}}
\ottusedrule{\ottdruleeqTSix{}}
\end{ottdefnblock}}


\newcommand{\ottdefnseq}{
\ottdefneqT{}}


% defns sub
% defn subS
\newcommand{\ottdrulesubSOne}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{S_{{\mathrm{2}}}} \, \ottkw{<:} \, \ottnt{S_{{\mathrm{1}}}}}%
\ottpremise{\ottnt{E} \, ; \, \ottkw{structure} \, x_i \, : \, \ottnt{S_{{\mathrm{2}}}} \, \vdash \, \ottnt{S'_{{\mathrm{1}}}} \, \ottkw{<:} \, \ottnt{S'_{{\mathrm{2}}}}}%
}{
\ottnt{E} \, \vdash \, \ottkw{functor} \, ( \, x_i \, : \, \ottnt{S_{{\mathrm{1}}}} \, ) \, \ottnt{S'_{{\mathrm{1}}}} \, \ottkw{<:} \, \ottkw{functor} \, ( \, x_i \, : \, \ottnt{S_{{\mathrm{2}}}} \, ) \, \ottnt{S'_{{\mathrm{2}}}}}{
{\ottdrulename{subS1}}{}
}}


\newcommand{\ottdrulesubSTwo}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{D} \, \ottkw{<:} \, \ottnt{D'}}%
}{
\ottnt{E} \, \vdash \, \ottkw{sig} \, \ottnt{D} \, \ottkw{end} \, \ottkw{<:} \, \ottkw{sig} \, \ottnt{D'} \, \ottkw{end}}{
{\ottdrulename{subS2}}{}
}}

\newcommand{\ottdefnsubS}[1]{\begin{ottdefnblock}[#1]{$\ottnt{E} \, \vdash \, \ottnt{S} \, \ottkw{<:} \, \ottnt{S'}$}{}
\ottusedrule{\ottdrulesubSOne{}}
\ottusedrule{\ottdrulesubSTwo{}}
\end{ottdefnblock}}


% defn subD
\newcommand{\ottdrulesubDOne}[1]{\ottdrule[#1]{%
}{
\ottnt{E} \, \vdash \,  \epsilon  \, \ottkw{<:} \,  \epsilon }{
{\ottdrulename{subD1}}{}
}}


\newcommand{\ottdrulesubDTwo}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{C} \, \ottkw{<:} \, \ottnt{C'}}%
\ottpremise{\ottnt{E} \, ; \, \ottnt{C} \, \vdash \, \ottnt{D} \, \ottkw{<:} \, \ottnt{D'}}%
}{
\ottnt{E} \, \vdash \, \ottnt{C} \, ; \, \ottnt{D} \, \ottkw{<:} \, \ottnt{C'} \, ; \, \ottnt{D'}}{
{\ottdrulename{subD2}}{}
}}


\newcommand{\ottdrulesubDThree}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, ; \, \ottnt{C} \, \vdash \, \ottnt{D} \, \ottkw{<:} \, \ottnt{D'}}%
}{
\ottnt{E} \, \vdash \, \ottnt{C} \, ; \, \ottnt{D} \, \ottkw{<:} \, \ottnt{D'}}{
{\ottdrulename{subD3}}{}
}}

\newcommand{\ottdefnsubD}[1]{\begin{ottdefnblock}[#1]{$\ottnt{E} \, \vdash \, \ottnt{D} \, \ottkw{<:} \, \ottnt{D'}$}{}
\ottusedrule{\ottdrulesubDOne{}}
\ottusedrule{\ottdrulesubDTwo{}}
\ottusedrule{\ottdrulesubDThree{}}
\end{ottdefnblock}}


% defn subC
\newcommand{\ottdrulesubCOne}[1]{\ottdrule[#1]{%
}{
\ottnt{E} \, \vdash \, ( \, \ottkw{type} \, t_i \, ) \, \ottkw{<:} \, ( \, \ottkw{type} \, t_i \, )}{
{\ottdrulename{subC1}}{}
}}


\newcommand{\ottdrulesubCTwo}[1]{\ottdrule[#1]{%
}{
\ottnt{E} \, \vdash \, ( \, \ottkw{type} \, t_i \, = \, \ottnt{T} \, ) \, \ottkw{<:} \, ( \, \ottkw{type} \, t_i \, )}{
{\ottdrulename{subC2}}{}
}}


\newcommand{\ottdrulesubCFour}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{T_{{\mathrm{1}}}} \, \approx \, \ottnt{T_{{\mathrm{2}}}}}%
}{
\ottnt{E} \, \vdash \, ( \, \ottkw{type} \, t_i \, = \, \ottnt{T_{{\mathrm{1}}}} \, ) \, \ottkw{<:} \, ( \, \ottkw{type} \, t_i \, = \, \ottnt{T_{{\mathrm{2}}}} \, )}{
{\ottdrulename{subC4}}{}
}}


\newcommand{\ottdrulesubCFive}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{S_{{\mathrm{1}}}} \, \ottkw{<:} \, \ottnt{S_{{\mathrm{2}}}}}%
}{
\ottnt{E} \, \vdash \, ( \, \ottkw{structure} \, x_i \, : \, \ottnt{S_{{\mathrm{1}}}} \, ) \, \ottkw{<:} \, ( \, \ottkw{structure} \, x_i \, : \, \ottnt{S_{{\mathrm{2}}}} \, )}{
{\ottdrulename{subC5}}{}
}}


\newcommand{\ottdrulesubCSix}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{T_{{\mathrm{1}}}} \, \approx \, \ottnt{T_{{\mathrm{2}}}}}%
}{
\ottnt{E} \, \vdash \, ( \, \ottkw{val} \, v_i \, : \, \ottnt{T_{{\mathrm{1}}}} \, ) \, \ottkw{<:} \, ( \, \ottkw{val} \, v_i \, : \, \ottnt{T_{{\mathrm{2}}}} \, )}{
{\ottdrulename{subC6}}{}
}}

\newcommand{\ottdefnsubC}[1]{\begin{ottdefnblock}[#1]{$\ottnt{E} \, \vdash \, \ottnt{C} \, \ottkw{<:} \, \ottnt{C'}$}{}
\ottusedrule{\ottdrulesubCOne{}}
\ottusedrule{\ottdrulesubCTwo{}}
\ottusedrule{\ottdrulesubCFour{}}
\ottusedrule{\ottdrulesubCFive{}}
\ottusedrule{\ottdrulesubCSix{}}
\end{ottdefnblock}}


\newcommand{\ottdefnssub}{
\ottdefnsubS{}
\ottdefnsubD{}
\ottdefnsubC{}}


% defns typ
% defn type_s
\newcommand{\ottdruletypeXXsOne}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{p} \, \mapsto \, \ottnt{S}}%
}{
\ottnt{E} \, \vdash \, \ottnt{p} \, : \, \ottnt{S}}{
{\ottdrulename{type\_s1}}{}
}}


\newcommand{\ottdruletypeXXsTwo}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{S} \, \ottkw{signature}}%
\ottpremise{ x_i \not\in BV( \ottnt{E} ) }%
\ottpremise{\ottnt{E} \, ; \, \ottkw{structure} \, x_i \, : \, \ottnt{S} \, \vdash \, \ottnt{s} \, : \, \ottnt{S'}}%
}{
\ottnt{E} \, \vdash \, \ottkw{functor} \, ( \, x_i \, : \, \ottnt{S} \, ) \, \ottnt{s} \, : \, \ottkw{functor} \, ( \, x_i \, : \, \ottnt{S} \, ) \, \ottnt{S'}}{
{\ottdrulename{type\_s2}}{}
}}


\newcommand{\ottdruletypeXXsThree}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{s} \, : \, \ottkw{functor} \, ( \, x_i \, : \, \ottnt{S'} \, ) \, \ottnt{S}}%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{p} \, \mapsto \, \ottnt{S''}}%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{S''} \, \ottkw{<:} \, \ottnt{S'}}%
}{
\ottnt{E} \, \vdash \, \ottnt{s} \, ( \, \ottnt{p} \, ) \, : \, \ottnt{S} \, \ottkw{\{} \, x_i \, \leftarrow \, \ottnt{p} \, \ottkw{\}}}{
{\ottdrulename{type\_s3}}{}
}}


\newcommand{\ottdruletypeXXsFour}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{d} \, : \, \ottnt{D}}%
}{
\ottnt{E} \, \vdash \, \ottkw{struct} \, \ottnt{d} \, \ottkw{end} \, : \, \ottkw{sig} \, \ottnt{D} \, \ottkw{end}}{
{\ottdrulename{type\_s4}}{}
}}


\newcommand{\ottdruletypeXXsFive}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{S_{{\mathrm{1}}}} \, \ottkw{signature}}%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{s} \, : \, \ottnt{S_{{\mathrm{2}}}}}%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{S_{{\mathrm{2}}}} \, \ottkw{<:} \, \ottnt{S_{{\mathrm{1}}}}}%
}{
\ottnt{E} \, \vdash \, \ottnt{s} \, \ottkw{:>} \, \ottnt{S_{{\mathrm{1}}}} \, : \, \ottnt{S_{{\mathrm{1}}}}}{
{\ottdrulename{type\_s5}}{}
}}

\newcommand{\ottdefntypeXXs}[1]{\begin{ottdefnblock}[#1]{$\ottnt{E} \, \vdash \, \ottnt{s} \, : \, \ottnt{S}$}{}
\ottusedrule{\ottdruletypeXXsOne{}}
\ottusedrule{\ottdruletypeXXsTwo{}}
\ottusedrule{\ottdruletypeXXsThree{}}
\ottusedrule{\ottdruletypeXXsFour{}}
\ottusedrule{\ottdruletypeXXsFive{}}
\end{ottdefnblock}}


% defn type_c
\newcommand{\ottdruletypeXXcOne}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{T} \, \ottkw{type}}%
\ottpremise{ t_i \not\in BV( \ottnt{E} ) }%
}{
\ottnt{E} \, \vdash \, \ottkw{type} \, t_i \, = \, \ottnt{T} \, : \, \ottkw{type} \, t_i \, = \, \ottnt{T}}{
{\ottdrulename{type\_c1}}{}
}}


\newcommand{\ottdruletypeXXcTwo}[1]{\ottdrule[#1]{%
\ottpremise{ t_i \not\in BV( \ottnt{E} ) }%
}{
\ottnt{E} \, \vdash \, \ottkw{datatype} \, t_i \, : \, \ottkw{type} \, t_i}{
{\ottdrulename{type\_c2}}{}
}}


\newcommand{\ottdruletypeXXcThree}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{s} \, : \, \ottnt{S}}%
\ottpremise{ x_i \not\in BV( \ottnt{E} ) }%
}{
\ottnt{E} \, \vdash \, \ottkw{structure} \, x_i \, = \, \ottnt{s} \, : \, \ottkw{structure} \, x_i \, : \, \ottnt{S}}{
{\ottdrulename{type\_c3}}{}
}}


\newcommand{\ottdruletypeXXcFour}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{M} \, : \, \ottnt{T}}%
\ottpremise{ v_i \not\in BV( \ottnt{E} ) }%
}{
\ottnt{E} \, \vdash \, \ottkw{val} \, v_i \, = \, \ottnt{M} \, : \, \ottkw{val} \, v_i \, : \, \ottnt{T}}{
{\ottdrulename{type\_c4}}{}
}}

\newcommand{\ottdefntypeXXc}[1]{\begin{ottdefnblock}[#1]{$\ottnt{E} \, \vdash \, \ottnt{c} \, : \, \ottnt{C}$}{}
\ottusedrule{\ottdruletypeXXcOne{}}
\ottusedrule{\ottdruletypeXXcTwo{}}
\ottusedrule{\ottdruletypeXXcThree{}}
\ottusedrule{\ottdruletypeXXcFour{}}
\end{ottdefnblock}}


% defn type_d
\newcommand{\ottdruletypeXXdOne}[1]{\ottdrule[#1]{%
}{
\ottnt{E} \, \vdash \,  \epsilon  \, : \,  \epsilon }{
{\ottdrulename{type\_d1}}{}
}}


\newcommand{\ottdruletypeXXdTwo}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{c} \, : \, \ottnt{C}}%
\ottpremise{\ottnt{E} \, ; \, \ottnt{C} \, \vdash \, \ottnt{d} \, : \, \ottnt{D}}%
}{
\ottnt{E} \, \vdash \, \ottnt{c} \, ; \, \ottnt{d} \, : \, \ottnt{C} \, ; \, \ottnt{D}}{
{\ottdrulename{type\_d2}}{}
}}

\newcommand{\ottdefntypeXXd}[1]{\begin{ottdefnblock}[#1]{$\ottnt{E} \, \vdash \, \ottnt{d} \, : \, \ottnt{D}$}{}
\ottusedrule{\ottdruletypeXXdOne{}}
\ottusedrule{\ottdruletypeXXdTwo{}}
\end{ottdefnblock}}


% defn typeM
\newcommand{\ottdruletypeMOne}[1]{\ottdrule[#1]{%
}{
\ottnt{E_{{\mathrm{1}}}} \, ; \, \ottkw{val} \, v_i \, : \, \ottnt{T} \, ; \, \ottnt{E_{{\mathrm{2}}}} \, \vdash \, v_i \, : \, \ottnt{T}}{
{\ottdrulename{typeM1}}{}
}}


\newcommand{\ottdruletypeMTwo}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{p} \, \mapsto \, \ottkw{sig} \, \ottnt{D_{{\mathrm{1}}}} \, ; \, \ottkw{val} \,  \ottmv{v} _ \ottmv{i}  \, : \, \ottnt{T} \, ; \, \ottnt{D_{{\mathrm{2}}}} \, \ottkw{end}}%
}{
\ottnt{E} \, \vdash \, \ottnt{p} \, . \, \ottmv{v} \, : \,  \ottnt{T} \{n_i \leftarrow  \ottnt{p} .n | n_i \in BV( \ottnt{D_{{\mathrm{1}}}} )\} }{
{\ottdrulename{typeM2}}{}
}}


\newcommand{\ottdruletypeMThree}[1]{\ottdrule[#1]{%
\ottpremise{ v_i \not\in BV( \ottnt{E} ) }%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{T_{{\mathrm{1}}}} \, \ottkw{type}}%
\ottpremise{\ottnt{E} \, ; \, \ottkw{val} \, v_i \, : \, \ottnt{T_{{\mathrm{1}}}} \, \vdash \, \ottnt{M} \, : \, \ottnt{T_{{\mathrm{2}}}}}%
}{
\ottnt{E} \, \vdash \, \lambda \, v_i \, : \, \ottnt{T_{{\mathrm{1}}}} \, . \, \ottnt{M} \, : \, \ottnt{T_{{\mathrm{1}}}} \, \rightarrow \, \ottnt{T_{{\mathrm{2}}}}}{
{\ottdrulename{typeM3}}{}
}}


\newcommand{\ottdruletypeMFour}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{M_{{\mathrm{1}}}} \, : \, \ottnt{T_{{\mathrm{1}}}} \, \rightarrow \, \ottnt{T_{{\mathrm{2}}}}}%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{M_{{\mathrm{2}}}} \, : \, \ottnt{T_{{\mathrm{1}}}}}%
}{
\ottnt{E} \, \vdash \, \ottnt{M_{{\mathrm{1}}}} \, \ottnt{M_{{\mathrm{2}}}} \, : \, \ottnt{T_{{\mathrm{2}}}}}{
{\ottdrulename{typeM4}}{}
}}


\newcommand{\ottdruletypeMFive}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{d} \, : \, \ottnt{D}}%
\ottpremise{\ottnt{E} \, ; \, \ottkw{rev} \, \ottnt{D} \, \vdash \, \ottnt{M} \, : \, \ottnt{T_{{\mathrm{1}}}}}%
\ottpremise{\ottnt{E} \, ; \, \ottkw{rev} \, \ottnt{D} \, \vdash \, \ottnt{T_{{\mathrm{1}}}} \, \approx \, \ottnt{T_{{\mathrm{2}}}}}%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{T_{{\mathrm{2}}}} \, \ottkw{type}}%
}{
\ottnt{E} \, \vdash \, \ottkw{let} \, \ottnt{d} \, \ottkw{in} \, \ottnt{M} \, : \, \ottnt{T_{{\mathrm{2}}}}}{
{\ottdrulename{typeM5}}{}
}}

\newcommand{\ottdefntypeM}[1]{\begin{ottdefnblock}[#1]{$\ottnt{E} \, \vdash \, \ottnt{M} \, : \, \ottnt{T}$}{}
\ottusedrule{\ottdruletypeMOne{}}
\ottusedrule{\ottdruletypeMTwo{}}
\ottusedrule{\ottdruletypeMThree{}}
\ottusedrule{\ottdruletypeMFour{}}
\ottusedrule{\ottdruletypeMFive{}}
\end{ottdefnblock}}


\newcommand{\ottdefnstyp}{
\ottdefntypeXXs{}
\ottdefntypeXXc{}
\ottdefntypeXXd{}
\ottdefntypeM{}}


% defns pathDelta
% defn pathDelta
\newcommand{\ottdrulepathDeltaOne}[1]{\ottdrule[#1]{%
}{
\Delta_{{\mathrm{1}}} \, ; \, \ottkw{structure} \, x_i \, = \, \ottnt{s} \, ; \, \Delta_{{\mathrm{2}}} \, \vdash \, x_i \, \mapsto \, \ottnt{s} \, / \, x_i}{
{\ottdrulename{pathDelta1}}{}
}}


\newcommand{\ottdrulepathDeltaTwo}[1]{\ottdrule[#1]{%
\ottpremise{\Delta \, \vdash \, \ottnt{p} \, \mapsto \, \ottkw{struct} \, \ottnt{d_{{\mathrm{1}}}} \, ; \, \ottkw{structure} \,  \ottmv{x} _ \ottmv{i}  \, = \, \ottnt{s} \, ; \, \ottnt{d_{{\mathrm{2}}}} \, \ottkw{end}}%
}{
\Delta \, \vdash \, \ottnt{p} \, . \, \ottmv{x} \, \mapsto \, \ottnt{s} \, \ottkw{\{} \, \ottnt{d_{{\mathrm{1}}}} \, \leftarrow \, \ottnt{p} \, \ottkw{\}}}{
{\ottdrulename{pathDelta2}}{}
}}

\newcommand{\ottdefnpathDelta}[1]{\begin{ottdefnblock}[#1]{$\Delta \, \vdash \, \ottnt{p} \, \mapsto \, \ottnt{s}$}{}
\ottusedrule{\ottdrulepathDeltaOne{}}
\ottusedrule{\ottdrulepathDeltaTwo{}}
\end{ottdefnblock}}


\newcommand{\ottdefnspathDelta}{
\ottdefnpathDelta{}}


% defns reduce
% defn redM
\newcommand{\ottdruleredMvar}[1]{\ottdrule[#1]{%
}{
\Delta_{{\mathrm{1}}} \, ; \, \ottkw{val} \, v_i \, = \, \ottnt{V} \, ; \, \Delta_{{\mathrm{2}}} \, \vdash \, v_i \, \leadsto \, \ottnt{V}}{
{\ottdrulename{redMvar}}{}
}}


\newcommand{\ottdruleredMpath}[1]{\ottdrule[#1]{%
\ottpremise{\Delta \, \vdash \, \ottnt{p} \, \mapsto \, \ottkw{struct} \, \ottnt{dV_{{\mathrm{1}}}} \, ; \, \ottkw{val} \,  \ottmv{v} _ \ottmv{i}  \, = \, \ottnt{V} \, ; \, \ottnt{dV_{{\mathrm{2}}}} \, \ottkw{end}}%
}{
\Delta \, \vdash \, \ottnt{p} \, . \, \ottmv{v} \, \leadsto \,  \ottnt{V} \{n_i \leftarrow  \ottnt{p} .n | n_i \in BV( \ottnt{dV_{{\mathrm{1}}}} )\} }{
{\ottdrulename{redMpath}}{}
}}


\newcommand{\ottdruleredMapp}[1]{\ottdrule[#1]{%
}{
\Delta \, \vdash \, ( \, \lambda \, v_i \, : \, \ottnt{T} \, . \, \ottnt{M} \, ) \, \ottnt{V} \, \leadsto \, \ottnt{M} \, \ottkw{\{} \, v_i \, \leftarrow \, \ottnt{V} \, \ottkw{\}}}{
{\ottdrulename{redMapp}}{}
}}


\newcommand{\ottdruleredMlet}[1]{\ottdrule[#1]{%
}{
\Delta \, \vdash \, \ottkw{let} \, \ottnt{dV} \, \ottkw{in} \, ( \, \lambda \, v_i \, : \, \ottnt{T} \, . \, \ottnt{M} \, ) \, \leadsto \, \lambda \, v_i \, : \, \ottnt{T} \, . \, \ottkw{let} \, \ottnt{dV} \, \ottkw{in} \, \ottnt{M}}{
{\ottdrulename{redMlet}}{}
}}


\newcommand{\ottdruleredMappXXctxtOne}[1]{\ottdrule[#1]{%
\ottpremise{\Delta \, \vdash \, \ottnt{M_{{\mathrm{1}}}} \, \leadsto \, \ottnt{M_{{\mathrm{3}}}}}%
}{
\Delta \, \vdash \, \ottnt{M_{{\mathrm{1}}}} \, \ottnt{M_{{\mathrm{2}}}} \, \leadsto \, \ottnt{M_{{\mathrm{3}}}} \, \ottnt{M_{{\mathrm{2}}}}}{
{\ottdrulename{redMapp\_ctxt1}}{}
}}


\newcommand{\ottdruleredMappXXctxtTwo}[1]{\ottdrule[#1]{%
\ottpremise{\Delta \, \vdash \, \ottnt{M_{{\mathrm{1}}}} \, \leadsto \, \ottnt{M_{{\mathrm{2}}}}}%
}{
\Delta \, \vdash \, \ottnt{V} \, \ottnt{M_{{\mathrm{1}}}} \, \leadsto \, \ottnt{V} \, \ottnt{M_{{\mathrm{2}}}}}{
{\ottdrulename{redMapp\_ctxt2}}{}
}}


\newcommand{\ottdruleredMletXXctxtOne}[1]{\ottdrule[#1]{%
\ottpremise{\Delta \, \vdash \, \ottnt{d_{{\mathrm{1}}}} \, \leadsto \, \ottnt{d_{{\mathrm{2}}}}}%
}{
\Delta \, \vdash \, \ottkw{let} \, \ottnt{d_{{\mathrm{1}}}} \, \ottkw{in} \, \ottnt{M} \, \leadsto \, \ottkw{let} \, \ottnt{d_{{\mathrm{2}}}} \, \ottkw{in} \, \ottnt{M}}{
{\ottdrulename{redMlet\_ctxt1}}{}
}}


\newcommand{\ottdruleredMletXXctxtTwo}[1]{\ottdrule[#1]{%
\ottpremise{\Delta \, ; \, \ottkw{rev} \, \ottnt{dV} \, \vdash \, \ottnt{M_{{\mathrm{1}}}} \, \leadsto \, \ottnt{M_{{\mathrm{2}}}}}%
}{
\Delta \, \vdash \, \ottkw{let} \, \ottnt{dV} \, \ottkw{in} \, \ottnt{M_{{\mathrm{1}}}} \, \leadsto \, \ottkw{let} \, \ottnt{dV} \, \ottkw{in} \, \ottnt{M_{{\mathrm{2}}}}}{
{\ottdrulename{redMlet\_ctxt2}}{}
}}

\newcommand{\ottdefnredM}[1]{\begin{ottdefnblock}[#1]{$\Delta \, \vdash \, \ottnt{M} \, \leadsto \, \ottnt{M'}$}{}
\ottusedrule{\ottdruleredMvar{}}
\ottusedrule{\ottdruleredMpath{}}
\ottusedrule{\ottdruleredMapp{}}
\ottusedrule{\ottdruleredMlet{}}
\ottusedrule{\ottdruleredMappXXctxtOne{}}
\ottusedrule{\ottdruleredMappXXctxtTwo{}}
\ottusedrule{\ottdruleredMletXXctxtOne{}}
\ottusedrule{\ottdruleredMletXXctxtTwo{}}
\end{ottdefnblock}}


% defn red_c
\newcommand{\ottdrulerecXXcXXstrXXctxt}[1]{\ottdrule[#1]{%
\ottpremise{\Delta \, \vdash \, \ottnt{s_{{\mathrm{1}}}} \, \leadsto \, \ottnt{s_{{\mathrm{2}}}}}%
}{
\Delta \, \vdash \, \ottkw{structure} \, x_i \, = \, \ottnt{s_{{\mathrm{1}}}} \, \leadsto \, \ottkw{structure} \, x_i \, = \, \ottnt{s_{{\mathrm{2}}}}}{
{\ottdrulename{rec\_c\_str\_ctxt}}{}
}}


\newcommand{\ottdrulerecXXcXXvalXXctxt}[1]{\ottdrule[#1]{%
\ottpremise{\Delta \, \vdash \, \ottnt{M_{{\mathrm{1}}}} \, \leadsto \, \ottnt{M_{{\mathrm{2}}}}}%
}{
\Delta \, \vdash \, \ottkw{val} \, v_i \, = \, \ottnt{M_{{\mathrm{1}}}} \, \leadsto \, \ottkw{val} \, v_i \, = \, \ottnt{M_{{\mathrm{2}}}}}{
{\ottdrulename{rec\_c\_val\_ctxt}}{}
}}

\newcommand{\ottdefnredXXc}[1]{\begin{ottdefnblock}[#1]{$\Delta \, \vdash \, \ottnt{c} \, \leadsto \, \ottnt{c'}$}{}
\ottusedrule{\ottdrulerecXXcXXstrXXctxt{}}
\ottusedrule{\ottdrulerecXXcXXvalXXctxt{}}
\end{ottdefnblock}}


% defn red_d
\newcommand{\ottdruleredXXdXXdXXctxtOne}[1]{\ottdrule[#1]{%
\ottpremise{\Delta \, \vdash \, \ottnt{c_{{\mathrm{1}}}} \, \leadsto \, \ottnt{c_{{\mathrm{2}}}}}%
}{
\Delta \, \vdash \, \ottnt{c_{{\mathrm{1}}}} \, ; \, \ottnt{d} \, \leadsto \, \ottnt{c_{{\mathrm{2}}}} \, ; \, \ottnt{d}}{
{\ottdrulename{red\_d\_d\_ctxt1}}{}
}}


\newcommand{\ottdruleredXXdXXdXXctxtTwo}[1]{\ottdrule[#1]{%
\ottpremise{\Delta \, ; \, \ottnt{cV} \, \vdash \, \ottnt{d_{{\mathrm{1}}}} \, \leadsto \, \ottnt{d_{{\mathrm{2}}}}}%
}{
\Delta \, \vdash \, \ottnt{cV} \, ; \, \ottnt{d_{{\mathrm{1}}}} \, \leadsto \, \ottnt{cV} \, ; \, \ottnt{d_{{\mathrm{2}}}}}{
{\ottdrulename{red\_d\_d\_ctxt2}}{}
}}

\newcommand{\ottdefnredXXd}[1]{\begin{ottdefnblock}[#1]{$\Delta \, \vdash \, \ottnt{d} \, \leadsto \, \ottnt{d'}$}{}
\ottusedrule{\ottdruleredXXdXXdXXctxtOne{}}
\ottusedrule{\ottdruleredXXdXXdXXctxtTwo{}}
\end{ottdefnblock}}


% defn red_s
\newcommand{\ottdruleredXXsXXpath}[1]{\ottdrule[#1]{%
\ottpremise{\Delta \, \vdash \, \ottnt{p} \, \mapsto \, \ottnt{sV}}%
}{
\Delta \, \vdash \, \ottnt{p} \, \leadsto \, \ottnt{sV}}{
{\ottdrulename{red\_s\_path}}{}
}}


\newcommand{\ottdruleredXXsXXftorapp}[1]{\ottdrule[#1]{%
}{
\Delta \, \vdash \, ( \, \ottkw{functor} \, ( \, x_i \, : \, \ottnt{S} \, ) \, \ottnt{s} \, ) \, ( \, \ottnt{p} \, ) \, \leadsto \, \ottnt{s} \, \ottkw{\{} \, x_i \, \leftarrow \, \ottnt{p} \, \ottkw{\}}}{
{\ottdrulename{red\_s\_ftorapp}}{}
}}


\newcommand{\ottdruleredXXsXXseal}[1]{\ottdrule[#1]{%
}{
\Delta \, \vdash \, \ottnt{s} \, \ottkw{:>} \, \ottnt{S} \, \leadsto \, \ottnt{s}}{
{\ottdrulename{red\_s\_seal}}{}
}}


\newcommand{\ottdruleredXXsXXstrXXctxt}[1]{\ottdrule[#1]{%
\ottpremise{\Delta \, \vdash \, \ottnt{d_{{\mathrm{1}}}} \, \leadsto \, \ottnt{d_{{\mathrm{2}}}}}%
}{
\Delta \, \vdash \, \ottkw{struct} \, \ottnt{d_{{\mathrm{1}}}} \, \ottkw{end} \, \leadsto \, \ottkw{struct} \, \ottnt{d_{{\mathrm{2}}}} \, \ottkw{end}}{
{\ottdrulename{red\_s\_str\_ctxt}}{}
}}


\newcommand{\ottdruleredXXsXXftorappXXctxt}[1]{\ottdrule[#1]{%
\ottpremise{\Delta \, \vdash \, \ottnt{s_{{\mathrm{1}}}} \, \leadsto \, \ottnt{s_{{\mathrm{2}}}}}%
}{
\Delta \, \vdash \, \ottnt{s_{{\mathrm{1}}}} \, ( \, \ottnt{p} \, ) \, \leadsto \, \ottnt{s_{{\mathrm{2}}}} \, ( \, \ottnt{p} \, )}{
{\ottdrulename{red\_s\_ftorapp\_ctxt}}{}
}}

\newcommand{\ottdefnredXXs}[1]{\begin{ottdefnblock}[#1]{$\Delta \, \vdash \, \ottnt{s} \, \leadsto \, \ottnt{s'}$}{}
\ottusedrule{\ottdruleredXXsXXpath{}}
\ottusedrule{\ottdruleredXXsXXftorapp{}}
\ottusedrule{\ottdruleredXXsXXseal{}}
\ottusedrule{\ottdruleredXXsXXstrXXctxt{}}
\ottusedrule{\ottdruleredXXsXXftorappXXctxt{}}
\end{ottdefnblock}}


\newcommand{\ottdefnsreduce}{
\ottdefnredM{}
\ottdefnredXXc{}
\ottdefnredXXd{}
\ottdefnredXXs{}}


% defns deltaE
% defn deltaE
\newcommand{\ottdruledeltaEOne}[1]{\ottdrule[#1]{%
}{
\vdash \,  \, : \, }{
{\ottdrulename{deltaE1}}{}
}}


\newcommand{\ottdruledeltaETwo}[1]{\ottdrule[#1]{%
\ottpremise{\vdash \, \Delta \, : \, \ottnt{E}}%
\ottpremise{\ottnt{E} \, \vdash \, \ottnt{cV} \, : \, \ottnt{C}}%
}{
\vdash \, \Delta \, ; \, \ottnt{cV} \, : \, \ottnt{E} \, ; \, \ottnt{C}}{
{\ottdrulename{deltaE2}}{}
}}

\newcommand{\ottdefndeltaE}[1]{\begin{ottdefnblock}[#1]{$\vdash \, \Delta \, : \, \ottnt{E}$}{}
\ottusedrule{\ottdruledeltaEOne{}}
\ottusedrule{\ottdruledeltaETwo{}}
\end{ottdefnblock}}


\newcommand{\ottdefnsdeltaE}{
\ottdefndeltaE{}}

\newcommand{\ottdefnss}{
\ottdefnspathE
\ottdefnsWFtype
\ottdefnsWFsig
\ottdefnseq
\ottdefnssub
\ottdefnstyp
\ottdefnspathDelta
\ottdefnsreduce
\ottdefnsdeltaE}

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

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