\usepackage{latexsym}
\usepackage{amssymb}
%\usepackage{amsmath}

\newcommand{\record}[3]{\{#1 = #2\}^{#3}}

\newlength{\skipline}
\setlength{\skipline}{0.2cm}

% comment brackets
\newcommand\ignore[1]{}

% naturals, integers, reals, etc.
\DeclareSymbolFont{AMSb}{U}{msb}{m}{n}
\DeclareMathSymbol{\N}{\mathbin}{AMSb}{"4E}
\DeclareMathSymbol{\Z}{\mathbin}{AMSb}{"5A}
\DeclareMathSymbol{\R}{\mathbin}{AMSb}{"52}
\DeclareMathSymbol{\Q}{\mathbin}{AMSb}{"51}
\DeclareMathSymbol{\I}{\mathbin}{AMSb}{"49}
\DeclareMathSymbol{\C}{\mathbin}{AMSb}{"43}

% mathtt
\newcommand\ttp{\mbox{{\tt '}}}
\newcommand\tts{\mbox{{\tt *}}}
\newcommand\ttop{\mbox{{\tt (}}}
\newcommand\ttcl{\mbox{{\tt )}}}
\newcommand\ttarrow{\mbox{\tt ->}}

%environments
\newenvironment{mytabbing}
{\begin{center}
 \begin{minipage}{\textwidth}
 \begin{tabbing}}
{\end{tabbing}
 \end{minipage}
 \end{center}}

\newenvironment{frfigure}
{\begin{figure} \hrule \medskip}
{\medskip 
 \hrule
 \end{figure}}

\newenvironment{ffrfigure}
{\begin{frfigure}\bigskip}
{\end{frfigure}}

\newenvironment{numarray}
{\renewcommand\arraystretch{1.5}\begin{array}{c@{\quad\quad\quad\quad}l}}
{\end{array}} 


% tabular proofs
\newlength{\tabproofbox}
\setlength{\tabproofbox}{0.95\textwidth}

\newenvironment{tabproof}
{
\par
\hfill
\begin{minipage}[c]{\tabproofbox}
}
{\end{minipage}\\[\skipline]}

\newlength{\tabproofboxtwo}
\setlength{\tabproofboxtwo}{0.9\textwidth}

\newenvironment{tabproof2}
{
\par
\hfill
\begin{minipage}[c]{\tabproofboxtwo}
}
{\end{minipage}\\[\skipline]}

\newenvironment{tabproof2beg}
{
\par
\hfill
\begin{minipage}[c]{\tabproofboxtwo}
}
{\end{minipage}\\}

\newenvironment{tabproof2comp}
{
\par
\hfill
\begin{minipage}[c]{\tabproofboxtwo}
}
{\end{minipage}\\[\skipline]}

\newlength{\tabproofboxthree}
\setlength{\tabproofboxthree}{0.85\textwidth}

\newenvironment{tabproof3}
{
\par
\hfill
\begin{minipage}[c]{\tabproofboxthree}
}
{\end{minipage}\\[\skipline]}

\newcommand\proofcase{\par\medskip\noindent{\bf Case:}}

\newcommand\outercase[1]
{\par\medskip\noindent
\parbox[t]{\textwidth}{{\bf Case,} #1:}
\par\medskip}

\newcommand\innercase[1]{%\par\medskip
\parbox[t]{\tabproofbox}{{\bf Case,} #1:}
\par\medskip}

\newcommand\innerproof[1]{%\par\medskip
\parbox[t]{\tabproofbox}{{\bf Proof,} #1:}
\par\medskip}

\newcommand\innercaseNoColon[1]{%\par\medskip
\parbox[t]{\tabproofbox}{{\bf Case,} #1}
\par\medskip}

\newcommand\innerinnercase[1]{%\par\medskip
\hfill
\parbox[t]{\tabproofboxtwo}{{\bf Case,} #1:}
\par\medskip}

%programs in tabbing
\newcommand\oftype{:$\!${ }}

% labeled objects
\newcommand\labobj[2]{#1\quad\quad\quad\quad #2}

% wildcard
\newcommand\wildcard{\_\,}

% tupling
\newcommand\nulltuple{\langle\,\rangle}
\newcommand\tuple[2]{\langle \, #1,\,#2\, \rangle}
\newcommand\triple[3]{\langle \, #1,\,#2,\,#3\, \rangle}
\newcommand\tripleNS[3]{\langle  #1,#2,#3 \rangle}
\newcommand\quaple[4]{\langle \, #1,\,#2,\,#3,\,#4\, \rangle}
\newcommand\quintuple[5]{\langle \, #1,\,#2,\,#3,\,#4,\,#5\, \rangle}
\newcommand\sixuple[6]{\langle \, #1,\,#2,\,#3,\,#4,\,#5,\,#6\, \rangle}
\newcommand\sevenuple[7]{\langle \, #1,\,#2,\,#3,\,#4,\,#5,\,#6,\,#7\, \rangle}

% sets
\newcommand{\set}[2]{\{#1\,|\,#2\}}
\newcommand{\singset}[1]{\{#1\}}
\newcommand{\twoset}[2]{\{{#1},{#2}\}}
\newcommand{\threeset}[3]{\{\,{#1},\,{#2},\,{#3}\,\}}
\newcommand{\intervalset}[2]{\{#1,\dots,#2\}}
\newcommand{\twofield}{{\sf I}\!{\sf B}}
\newcommand\depfct[2]{\Pi\,#1.\,#2}
\newcommand\dom[1]{{\const{dom}}(#1)}
\newcommand\toset[1]{\mathit{set}(#1)}
\newcommand\powerset[1]{\mathcal P (#1)}
\newcommand\setvar{\mathcal S}
\newcommand\multiset[1]{\mathcal M (#1)}
\newcommand\twomultiset[1]{\mathcal M^2 (#1)}
\newcommand\finseq[1]{\mathit{FinSeq}(#1)}

% functions
\newcommand\fcnupdt[3]{#1[#2\mapsto #3]}
\newcommand\fcnupdtthree[7]{#1[#2\mapsto #3,\,#4\mapsto #5,\,#6\mapsto #7]}
\newcommand\singfcn[2]{\{#1\mapsto #2\}}
\newcommand\twofcn[4]{\{\,#1\mapsto #2,\;#3\mapsto #4\,\}}
\newcommand\compfcn[2]{#1 \circ #2}
\newcommand\rstrctfcn[2]{#1|_{#2}}

% function application
\newcommand\appit[2]{\mathit{#1}(#2)}

%general purpose functions
\newcommand\abs[1]{|#1|}
\newcommand\abssym{\abs\cdot}
\newcommand\abssig[2]{\abs{#1}_{\Sigma,#2}}

% Norm
\newcommand\norm[1]{\| #1 \|}
\newcommand\normsym{\norm\cdot}

% bnf Operators
\newcommand\gor{\; | \;}

% Term Operators
\newcommand\const[1]{{\mathsf {#1}}}
\newcommand\cond[3]{\const{if}\,#1\,\const{then}\,#2\,\const{else}\,#3}
\newcommand\unop[2]{\const{#1}\,#2}
\newcommand\binop[3]{#2\,\mathit{#1}\,#3}
\newcommand\eq[2]{#1=#2}
\newcommand\lam[2]{\lambda #1.\,#2}
\newcommand\explam[3]{\lam {#1 : #2}{\,#3}}
\newcommand\Lam[2]{\Lambda #1.\,#2}
\newcommand\app[2]{#1\,#2}
\newcommand\letdec[3]{\const{let}\,#1 = #2\,\const{in}\,#3}
\newcommand\tyapp[2]{#1\,[#2]}
\newcommand\fix[2]{\mu #1.#2}
\newcommand\pair[2]{\langle #1, #2 \rangle}
\newcommand\pairsp[2]{\langle #1,\, #2 \rangle}
\newcommand\fst[1]{\unop{fst}{#1}}
\newcommand\snd[1]{\unop{snd}{#1}}
\newcommand\nil{\const{nil}}
\newcommand\conssym{\const{cons}}
\newcommand\cons[2]{\app {\const{cons}}{\pair {#1}{#2}}} %{#1::#2}
\newcommand\uncons[1]{\app \conssym {#1}}
\newcommand\case[4]{\const{case}\,#1\,\const{of}\,\{\,\nil\rightarrow #2 \,
                   |\,\uncons{#3}\rightarrow #4\,\}}
\newcommand\true{\const{true}}
\newcommand\false{\const{false}}
\newcommand\bnot{\const{not}}
\newcommand\bor{\const{or}}
\newcommand\band{\const{and}}
\newcommand\eqtest[1]{{\mathit Eq}_{#1}}
\newcommand\select[2]{\msf{select}(#1,#2)}

% atoms
\newcommand\predsym[1]{\mathit{#1}}
\newcommand\atom[3]{\predsym{#1}\langle{#2}\rangle\langle{#3}\rangle}
\newcommand\atomsp[3]{\predsym{#1}\,\langle{#2}\rangle\,\langle{#3}\rangle}

%divergence
\newcommand\divergence{\Omega}

% Type Operators
\newcommand\tvar{X}
\newcommand\tunit{\const{1}}
\newcommand\tbool{\const{bool}}
\newcommand\tint{\const{int}}
\newcommand\tprop{\const{prop}}
\newcommand\tpropseq{\const{propseq}}
\newcommand\tprod[2]{#1 * #2}
\newcommand\tpred[2]{#1 \times #2}
\newcommand\tfun[2]{#1 \rightarrow #2}
\newcommand\tlist[1]{\const{list}\,#1}
%\newcommand\tforall[2]{\forall\,#1.\,#2}
\newcommand\tdf[3]{\Pi #1 : #2.\,#3}

% Kinds
\newcommand\ktype{\const{type}}
\newcommand\keqtype{\const{eqtype}}
\newcommand\ktyscheme{\const{tyscheme}}
\newcommand\katttyscheme{\const{atyscheme}}
\newcommand\kdecotyscheme{\const{decotyscheme}}
\newcommand\kpredty{\const{predty}}
\newcommand\kkind{\const{kind}}

% Attributes
\newcommand\valatt{\const{val}}
\newcommand\valconatt{\const{valcon}}
\newcommand\absatt[1]{\const{abs}(#1)}
\newcommand\dcrsym{\mathit{dcr}}
\newcommand\dcr[1]{\dcrsym(#1)}

% Aggregates and spines
\newcommand\aggapp[2]{#1 \cdot #2}
%\newcommand\aggexplam[3]{\hat{\lambda} #1 : #2 .\, #3}
%\newcommand\agglam[2]{\hat{\lambda} #1.\, #2}
%\newcommand\aggLam[2]{\hat{\Lambda} #1.\, #2}
%\newcommand\aggpair[2]{\hat{\langle} #1, #2 \hat{\rangle}}
%\newcommand\aggpairsp[2]{\hat{\langle} #1,\, #2 \hat{\rangle}}
\newcommand\spinenil{\nil}
\newcommand\spinecons[2]{#1 :: #2}
\newcommand\tokenfst{\const{fst}}
\newcommand\tokensnd{\const{snd}} 
\newcommand\tokenarrow{\rightarrow}
\newcommand\tokenstar{*}
\newcommand\aggappsp[2]{\aggapp{#1}{\;#2}}
\newcommand\aggtotermsym{\abssym}
\newcommand\aggtoterm[1]{\abs{#1}}
\newcommand\termtoagg[1]{\aggapp {#1} \spinenil}
\newcommand\spineappendsym{{\mathtt @}}
\newcommand\spineappend[2]{#1\, \spineappendsym\,#2}
\newcommand\aggtermsize[1]{\mathit{size}(#1)}
\newcommand\aggexplam[3]{\termtoagg{(\explam {#1}{#2}{#3})}}
\newcommand\agglam[2]{\termtoagg{(\lam {#1}{#2})}}
\newcommand\aggLam[2]{\termtoagg{(\Lam {#1}{#2})}}
\newcommand\aggpair[2]{\termtoagg{\pair {#1}{#2}}}
\newcommand\aggpairsp[2]{\termtoagg{\pair {#1}{#2}}}
\newcommand\tspine[2]{#1 > #2}

% Aggregate decomposition
\newcommand\adsym{\rightarrow_{ad}}
\newcommand\ad[2]{#1 \adsym #2}
\newcommand\adsymtrans{\stackrel{*}\rightarrow_{ad}}
\newcommand\adtrans[2]{#1 \adsymtrans #2}

% Neutral terms
\newcommand\neutralatt{\const{neutral}}
\newcommand\neutral[1]{#1 : \neutralatt}

% Rules
\newcommand\ternrultwoone[4]
  {\frac{\begin{array}{c}
           \begin{array}{cc} {#1} & \quad{#2} \end{array} \\
            {#3}
         \end{array}
        }
        {{#4}}}

\newcommand\ax[1]{\begin{array}{c} \\ \hline {#1} \end{array}}

\newcommand\axside[2]{\begin{array}{c} \\ \hline {#1} \end{array}
                      \quad\mbox{if $#2$}}

\newcommand\unrul[2]{\begin{array}{c} {#1} \\ \hline {#2} \end{array}}

\newcommand\unrulside[3]{\begin{array}{c} {#1} \\ \hline {#2} \end{array}
                         \quad\mbox{if $#3$}}

\newcommand\unrulsidewhere[3]{\begin{array}{c} {#1} \\ \hline {#2} \end{array}
                              \quad\mbox{where $#3$}}

\newcommand\binrul[3]{
 \begin{array}{ccc}
    #1\;  & \;#2 \\ \hline  
    \multicolumn{2}{c}{#3}
 \end{array}
}

\newcommand\binrulside[4]{
 \begin{array}{ccc}
    #1\; & \;#2 \\ \hline  
    \multicolumn{2}{c}{#3}
 \end{array}
 \quad\mbox{if $#4$}
}

\newcommand\ternrul[4]{
 \begin{array}{ccc}
    #1\; & \;#2\; & \;#3 \\ \hline  
    \multicolumn{3}{c}{#4}
 \end{array}
}

% Goal directed rules
\newcommand\backunrul[2]
  {\begin{array}{r@{\hspace{2em}}l}
    \mbox{Current Goal:} & {#1} \\
            & \multicolumn{1}{c}{\downarrow}\\
  \mbox{New Goal:} & {#2}
   \end{array}}

\newcommand\backbinrul[3]
  {\begin{array}{r@{\hspace{2em}}l}
    \mbox{Current Goal:} & {#1} \\
            & \multicolumn{1}{c}{\downarrow}\\
  \mbox{New Goals:} & \left\{ \begin{array}{l} #2 \\ #3 \end{array}\right.
   \end{array}}


% Sequents
\newcommand\seq[2]{#1\,\vdash\,#2}
\newcommand\labseq[3]{#1\,\vdash^{#2}\,#3}
\newcommand\tyseq[3]{\seq {#1}{#2} \, : \, {#3}}
\newcommand\caltyseq[3]{\tyseq {\mathcal #1}{#2}{#3}}
\newcommand\tyseqdbl[4]{\seq {{#1};\,{#2}} {#3} \, : \, {#4}}
\newcommand\labtyseq[4]{\labseq {#1}
                                {#2} 
                                {{#3}\, : \, {#4}}}
\newcommand\callabtyseq[4]{\labtyseq {\mathcal #1}{#2}{#3}{#4}}
\newcommand\labtyseqdbl[5]{\labseq {{#1};\,{#2}} 
                                   {{#3}} 
                                   {{#4}\, : \, {#5}}
                          }
\newcommand\condlabtyseq[5]{\labtyseq {#1;\,#2} {#3} {#4} {#5}}
\newcommand\logseq[6] {\labseq {{#1};\,{#2}} {{#3};{#4};{#5}} {#6}}
\newcommand\cltyseq[2]{#1\,:\,#2}
\newcommand\updtctx[3]{#1,\,#2:#3}
\newcommand\emptyctxdbl{\langle\langle\rangle;\langle\rangle\rangle}
\newcommand\entails[4]{#1;#2 \models^{#3} #4}

% natural semantics
\newcommand\evalto[2]{#1 \Downarrow #2}
\newcommand\notevalto[2]{#1 \not\Downarrow #2}
\newcommand\converges[1]{#1 \Downarrow}
\newcommand\diverges[1]{#1 \Uparrow}


% relations
\newcommand\clrel[4]{#1\;\;\mathcal{#2}\;\;#3\,:\,#4}
\newcommand\clrelext[4]{#1\;\;\mathcal{#2}^o\;\;#3\,:\,#4}
\newcommand\sclrel[4]{#1\,\mathcal{#2}\,#3:#4}
\newcommand\oprel[5]{{#1}\,\vdash\,{#2}\;\;\mathcal{#3}\;\;{#4}\,:\,{#5}}
\newcommand\oprelext[5]{{#1}\,\vdash\,{#2}\;\;\mathcal{#3}^o\;\;{#4}\,:\,{#5}}
\newcommand\opreldbl[6]
   {{#1};\,{#2}\,\vdash\,{#3}\;\;\mathcal{#4}\;\;{#5}\,:\,{#6}}
\newcommand\opreldblext[6]
   {{#1};\,{#2}\,\vdash\,{#3}\;\;\mathcal{#4}^o\;\;{#5}\,:\,{#6}}
\newcommand\opequiv[5]{{#1}\,\vdash^{#2}\,{#3}\equiv{#4}\,:\,{#5}}
\newcommand\termbis[5]{{#1}\,\vdash^{#2}\,{#3}\simeq{#4}\,:\,{#5}}
\newcommand\annrel[6]{#1\,\vdash^{#2}\, #3 \; \mathcal{#4} \; #5\,:\, #6}
\newcommand\annreldbl[7]
  {#1;\,#2\,\vdash^{#3}\, #4 \; \mathcal{#5} \; #6\,:\, #7} 
\newcommand\rawrel[3]{#1 \;\mathcal{#2}\; #3}
\newcommand\rawterrel[4]{#1\,\vdash\, #2\; \mathcal{#3}\; #4}

% observational equality
\newcommand\obsleq[3]{#1\leq^{\mathrm{obs}} #2 : #3}
\newcommand\nobsleq[3]{#1\not\leq^{\mathrm{obs}} #2 : #3}
\newcommand\obseq[3]{#1= ^{\mathrm{obs}} #2 : #3}
\newcommand\nobseq[3]{#1\not= ^{\mathrm{obs}} #2 : #3}
\newcommand\obseqsymbol{= ^{\mathrm{obs}}}
\newcommand\obsleqsymbol{\leq ^{\mathrm{obs}}}

% bisimilarity
\newcommand\simleq{\preceq}
\newcommand\similar[3]{#1\simleq #2 : #3}
\newcommand\similarext[3]{#1\simleq^o #2 : #3}
\newcommand\bisimilar[3]{#1\simeq #2 : #3}
\newcommand\bisimwide[3]{#1\;\;\simeq\;\; #2 \;\; : \;\; #3}
\newcommand\bisimilarext[3]{#1\simeq^o #2 : #3}
\newcommand\opsimilar[4]{#1\vdash #2\simleq^o #3 : #4}
\newcommand\opsimilardbl[5]{#1;\,#2\vdash #3\simleq^o #4 : #5}
\newcommand\opbisimilar[4]{#1\vdash#2\simeq^o #3 : #4}
\newcommand\starsimilar[4]{#1\vdash #2\simleq^* #3 : #4}
\newcommand\clstarsimilar[3]{#1\simleq^* #2 : #3}
\newcommand\starsimilardbl[5]{#1;\,#2\vdash #3\simleq^* #4 : #5}
\newcommand\labbisimilar[4]{#1\vdash^{\Sigma^0}#2\simeq #3 : #4}
\newcommand\expbisimilar[4]{#1\vdash#2\simeq #3 : #4}

% beta equality
\newcommand\betasym{=_{\beta}}
\newcommand\betavalsym{=_{\beta_v}}
\newcommand\etavalsym{=_{\eta_v}}
\newcommand\betaetavalsym{=_{\beta\eta_v}}
\newcommand\opbetaval[4]{#1\vdash#2\betavalsym #3 : #4}
\newcommand\opetaval[4]{#1\vdash#2\etavalsym #3 : #4}
\newcommand\opbetaetaval[4]{#1\vdash#2\betaetavalsym #3 : #4}
\newcommand\bnf[1]{\mathit{NF}(#1)}
\newcommand\betareduces[2]{#1 \stackrel{*}\rightarrow_\beta #2}
\newcommand\betaonereduces[2]{#1 \rightarrow_\beta #2}
\newcommand\betareducessym{\stackrel{*}\rightarrow_\beta}
\newcommand\betaonereducessym{\rightarrow_\beta}
\newcommand\betaeq[2]{#1 =_\beta #2}
\newcommand\bredsym{\rightarrow_\beta}
\newcommand\bred[2]{#1 \bredsym #2}
\newcommand\btredsym{\stackrel{*}\rightarrow_\beta}
\newcommand\btred[2]{#1 \btredsym #2}
\newcommand\bpredsym{\stackrel{\mathtt{+}}\rightarrow_\beta}
\newcommand\bpred[2]{#1 \bpredsym #2}
\newcommand\beqsym{=_\beta}
\newcommand\beq[2]{#1 \beqsym #2}

% beta-pi value equality
\newcommand\bpveqsym{=_{v}}
\newcommand\bpveq[3]{#1\,\vdash\, #2 \bpveqsym #3}
\newcommand\bpveqty[2]{#1 \bpveqsym #2}
\newcommand\bpvredsym{\rightarrow_v}
\newcommand\bpvred[3]{#1\,\vdash\, #2 \bpvredsym #3}
\newcommand\bpvredty[2]{#1 \bpvredsym #2}
\newcommand\bpvtredsym{\stackrel{*}\rightarrow_v}
\newcommand\bpvtred[3]{#1\,\vdash\, #2 \bpvtredsym #3}
\newcommand\bpvtredty[2]{#1 \bpvtredsym #2}
\newcommand\bpvpredsym{\stackrel{\mathtt{+}}\rightarrow_{v}}
\newcommand\bpvpred[3]{#1\,\vdash\, #2 \bpvpredsym #3}
\newcommand\bpvoredsym{\stackrel{{1}}\rightarrow_{v}}
\newcommand\bpvored[3]{#1\,\vdash\, #2 \bpvoredsym #3}
\newcommand\bpvoredty[2]{#1 \bpvoredsym #2}
\newcommand\vnf[2]{\mathit{NF}_{#1}(#2)}

% equality of raw terms indexed by value assertion context
\newcommand\rteq[3]{#1\,\vdash\, #2 = #3}

% beta-pi reduction
\newcommand\bpiredsym{\rightarrow_{\beta\pi}}
\newcommand\bpiredctx[3]{#1\,\vdash\, #2 \bpiredsym #3}
\newcommand\bpired[2]{#1 \bpiredsym #2}
\newcommand\bpitredsym{\stackrel{*}\rightarrow_{\beta\pi}}
%\newcommand\bpvtred[3]{#1\,\vdash\, #2 \bpvtredsym #3}
\newcommand\bpitred[2]{#1 \bpitredsym #2}
\newcommand\bpipredsym{\stackrel{\mathtt{+}}\rightarrow_{\beta\pi}}
\newcommand\bpipred[2]{#1 \bpipredsym #2}
\newcommand\bpioredsym{\stackrel{{1}}\rightarrow_{\beta\pi}}
%\newcommand\bpvored[3]{#1\,\vdash\, #2 \bpvoredsym #3}
\newcommand\bpiored[2]{#1 \bpioredsym #2}

% beta-pi + extensionality
\newcommand\bpvesym{=_{v,\eta,\spng}}  %{=_{v,\eta}}
\newcommand\bpvemsym{=_{v,\eta,\spv}} %{=_{v,\eta,-}}
\newcommand\bpvextfsym{=_{v,\rightarrow}}
\newcommand\bpvextsym{=_{v,\rightarrow,*}}  %{=_{v,\mathit{ext}}}
\newcommand\bpvextmsym{=_{v,\rightarrow,*_v}}  %{=_{v,\mathit{ext},-}}
\newcommand\bpve[4]{#1\,\vdash\, #2 \bpvesym #3 : #4}
\newcommand\bpvem[4]{#1\,\vdash\, #2 \bpvemsym #3 : #4}
\newcommand\bpvextf[4]{#1\,\vdash\, #2 \bpvextfsym #3 : #4}
\newcommand\bpvext[4]{#1\,\vdash\, #2 \bpvextsym #3 : #4}
\newcommand\bpvextm[4]{#1\,\vdash\, #2 \bpvextmsym #3 : #4}

% beta-pi equality
\newcommand\bpi{\beta\pi}
\newcommand\bpisym{=_{\bpi}}
\newcommand\bpieq[2]{#1 \bpisym #2}

% beta-pi equality + extensionality for types
\newcommand\bpiplus{\beta\pi^+}
\newcommand\bpiplussym{=_{\bpiplus}}
\newcommand\bpipluseq[5]{#1\,\vdash^{#2}\, #3 \bpiplussym #4 \, :\, #5}
\newcommand\bplus{\beta^+}
\newcommand\bplussym{=_{\bplus}}
\newcommand\bpluseq[5]{#1\,\vdash^{#2}\, #3 \bplussym #4\, :\, #5}


% rule names
\newcommand\spng{\mathit{SP}}
\newcommand\spv{\mathit{SP}\!_v}
\newcommand\extfunv{\rightarrow\!\mbox{-{\it ext}}_v}
\newcommand\extprod{*\mbox{-{\it ext}}}
\newcommand\extprodv{*\mbox{-{\it ext}}_v}

% critical variable algorithm
\newcommand\cvarsym{\downarrow}
\newcommand\cvar[3]{#1 \cvarsym \pair{#2}{#3}}

% weak normalization
\newcommand\wnlztosym{\downarrow}
\newcommand\wnlzto[2]{#1 \wnlztosym #2}
\newcommand\wnlz[1]{|#1|}
\newcommand\wnlzsym{\wnlz\cdot}
\newcommand\wnf{\mathit{WNF}}

% algorithmic extensional equality
\newcommand\algeqsym{\Longleftrightarrow}
\newcommand\algeqnsym{\longleftrightarrow}
\newcommand\algeq[4]{#1\,\vdash\, #2 \algeqsym #3 : #4}
\newcommand\algeqn[4]{#1\,\vdash\, #2 \algeqnsym #3 : #4}

% logical relation
\newcommand\logrelsym{\equiv}
\newcommand\logrel[4]{#1\,\vdash\, #2 \logrelsym #3 : #4}

% Operations on problem contexts
\newcommand\allpre[2]{\mathcal #1^{\forall,#2}}
\newcommand\allctx[1]{\mathcal{#1}^\forall}
\newcommand\prectx[2]{\mathcal #1^{#2}}
\newcommand\exrsym{\mathit{exr}}
\newcommand\exr[2]{\exrsym(#1,#2)}
\newcommand\calexr[2]{\exr {\mathcal #1} {\mathcal #2}}
%\newcommand\ctxleqsym[1]{\leq_{#1}}
\newcommand\ctxleq[4]{#1 \stackrel{#2}\longrightarrow_{#3} #4}
\newcommand\prbctxprunenc[3]{{#1}[ {#2}\Rightarrow {\mathcal #3}]}
\newcommand\prbctxprunencnc[3]{{#1}[ {#2}\Rightarrow {#3}]}
\newcommand\prbctxprune[3]{\prbctxprunenc{\mathcal #1}{#2}{#3}}
\newcommand\prbctxglue[3]{\mathcal #1 \oplus_{#2} \mathcal #3}
\newcommand\prbctxgluenc[3]{#1 \oplus_{#2} \mathcal #3}

% Unification problems
\newcommand\unifprob[2]{\langle \mathcal #1;\mathit{#2} \rangle}
\newcommand\unifprobdpeq[3]
  {\langle\; \mathcal #1;\; #2 \,=\, #3 \;\rangle}
\newcommand\unifprobdpdpeq[5]
  {\langle\; \mathcal #1;
    \begin{array}[c]{rcl} #2  & = & #3 \\ #4 & = & #5 \end{array} \rangle}
\newcommand\unifprobdsds[3]
  {\langle \mathcal #1;\,\mathit{#2},\mathit{#3} \rangle}
\newcommand\unifprobdsdp[4]
  {\langle \mathcal #1;\,\mathit{#2},\pair{#3}{#4} \rangle}
\newcommand\unifprobdsdpdp[6]
  {\langle \mathcal #1;\,\mathit{#2},\pair{#3}{#4},\pair{#5}{#6} \rangle}
\newcommand\unifprobdsdpnldp[6]
  {\langle \mathcal #1;\,\mathit{#2},
   \begin{array}[t]{l} \pair{#3}{#4}, \\ \pair{#5}{#6}\,\rangle \end{array}}
\newcommand\unifprobccdsdpdp[7]
  {\langle \mathcal #1,{#2};\,\mathit{#3},\pair{#4}{#5},\pair{#6}{#7} \rangle}
\newcommand\unifprobccdsdpnldp[7]
  {\langle \mathcal #1,{#2};\,\mathit{#3},
   \begin{array}[t]{l} \pair{#4}{#5}, \\ \pair{#6}{#7}\,\rangle \end{array}}

% transformations of unification problems
\newcommand\ctxtra[2]{#1\,(#2)}
\newcommand\transapp[2]{\mathcal #1(\mathcal #2)}

% imitation and projection and match
\newcommand\match{\mathit{match}}
\newcommand\matchsym{\stackrel{\!\mathit{match}}{-\!\!\!\longrightarrow}}
\newcommand\imitsym{\downarrow^{\mathit{imit}}}
\newcommand\projsym{\downarrow^{\mathit{proj}}}
\newcommand\imit[3]
  {\unifprob {#1}{#2} \imitsym \mathcal #3}
\newcommand\proj[3]
  {\unifprob {#1}{#2} \projsym \mathcal #3}
\newcommand\matchgensym{\downarrow}
%\newcommand\matchgensym{
%  (\wildcard \vdash^{\Sigma,\mathcal C} \wildcard \downarrow \wildcard)}
\newcommand\matchgen[9]{
   \langle\, #1,\,#2,\,#3,\,#4,\,#5,\,#6,\, #7\,\rangle
   \vdash^{\Sigma,\mathcal C}
    \,#8\, \downarrow #9}
\newcommand\matchgenty[7]{
   \langle\, #1,\,#2,\,#3,\,#5\,\rangle
   \vdash^{\Sigma,\mathcal C}
   \,#4\, \downarrow \langle\, #6,\,#7\,\rangle}
\newcommand\spineimitsym{\downarrow^{\mathit{si}}}
\newcommand\spineimit[6]{
  \quaple {#1}{#2}{#3}{#4} \vdash^{\mathcal C} \,#5\, \spineimitsym
  #6}
\newcommand\spineimitty[5]{ 
  \tuple {#1}{#2} \vdash^{\mathcal C} \,#3\, \spineimitsym \tuple {#4}{#5} }
\newcommand\spineconsym{\downarrow^{\mathit{sc}}}
\newcommand\spinecon[5]{
  #1 \vdash^{\mathcal C} \,#2\, \spineconsym \triple{#3}{#4}{#5} }
%\newcommand\spineconty[4]{ }

% variable pools
\newcommand\poolnil{\nil}
\newcommand\poolcons[2]{#1 :: #2}
\newcommand\poolToSpineSym{\downarrow^{\mathit{poolToSpine}}}
\newcommand\poolToSpine[4]{\pair{#1}{#2} \poolToSpineSym  \pair{#3}{#4}}
\newcommand\typoolToSpine[3]{#1 \poolToSpineSym \pair{#2}{#3}}
\newcommand\tvpsym{\mathit{tbp}}
\newcommand\tvp[1]{\tvpsym(#1)}
\newcommand\raiseVarSym{\downarrow^r}
\newcommand\raiseVar[5]{\tuple {#2}{#3} \vdash\, #1\, \raiseVarSym \tuple {#4}{#5}}
%\newcommand\raiseVarTy[4]{ {#2} \vdash\, #1\, \raiseVarSym \tuple {#3}{#4}}
%\newcommand\raiseVarTyNS[4]{ {#2} \vdash #1 \raiseVarSym \pair {#3}{#4}}
\newcommand\raiseVarNS[5]{\langle {#2},{#3} \rangle \vdash #1 
                             \raiseVarSym \pair {#4}{#5}}
\newcommand\raiseVarAbs[6]{
  \tuple {#2}{#3} \vdash\, #1\, \raiseVarSym  \tuple {#4}{#5 \wedge \absatt{#6}}}
\newcommand\raiseVarAbsNS[6]{
  \langle {#2},{#3} \rangle  \vdash #1 \raiseVarSym 
    \pair {#4}{#5 \wedge \absatt{#6}}}

% Simplification rules
\newcommand\simplsym
  {\stackrel{\!\mathit{simpl}}{-\!\!\!\longrightarrow}}
\newcommand\fail{\mathit{Fail}}
\newcommand\simplcoarse[2]{\mathcal #1\simplsym \mathcal #2}
\newcommand\simpl[4]{\unifprob{#1}{#2} \simplsym \unifprob{#3}{#4}}
\newcommand\simplfailcoarse[1]{\mathcal #1\simplsym \fail}
\newcommand\simplfail[2]{\unifprob{#1}{#2} \simplsym \fail}
\newcommand\dcmp{\mathit{dcmp}}
\newcommand\ill[1]{\mathit{ill}(\mathit{#1})}

% bounded types
\newcommand\rbdsym{\const{rbd}}
\newcommand\rbd[2]{\tyseq {\mathcal #1} {#2} {\rbdsym}}
\newcommand\abdsym{\const{abd}}
\newcommand\abd[3]{\tyseq {\mathcal #1;\,#2} {#3} \abdsym}
\newcommand\abdns[3]{\tyseq {\mathcal #1;#2} {#3} \abdsym}

% Head reduction
\newcommand\hdredsym{\rightarrow_{\mathit{hd}}}
\newcommand\hdred[2]{#1 \hdredsym #2}

% logical operators
\newcommand\iand[2]{#1\land#2}
\newcommand\ior[2]{#1\lor#2}
\newcommand\imp[2]{#1\Rightarrow#2}
\newcommand\equi[2]{#1\Leftrightarrow#2}
%\newcommand\lnot[1]{\neg#1}
\newcommand\expforall[3]{\forall #1:#2.\,#3}
\newcommand\impforall[2]{\forall #1.\,#2}
\newcommand\impforalltpl[2]{\forall #1.\,#2}
\newcommand\specialforall[3]{\forall #1\triangleright#2.\,#3}

% substitution
\newcommand\subst[3]{[#1/#2]#3}
\newcommand\singsubst[2]{[#1/#2]}
\newcommand\simsubst[2]{#1(#2)}

% free variables
\newcommand\ftvsym{\mathsf{ftv}}
\newcommand\ftv[1]{\ftvsym(#1)}
\newcommand\fvsym{\mathsf{fv}}
\newcommand\fv[1]{\fvsym(#1)}
\newcommand\tc[1]{\mathit{tc}(#1)}
\newcommand\vc[1]{\mathit{vc}(#1)}

% math italic
\newcommand\Var{\mathit{Var}}
\newcommand\Term{\mathit{Term}}
\newcommand\TyVar{\mathit{TyVar}}
\newcommand\TyCon{\mathit{TyCon}}
\newcommand\ValCon{\mathit{ValCon}}
\newcommand\TyScheme{\mathit{TyScheme}}
\newcommand\TyFcnScheme{\mathit{TyFcnScheme}}
\newcommand\AttTyScheme{\mathit{AttTyScheme}}
\newcommand\AttTyFcnScheme{\mathit{AttTyFcnScheme}}
\newcommand\ClosedAttTyScheme{\mathit{ClosedAttTyScheme}}
\newcommand\DecoTyScheme{\mathit{DecoTyScheme}}
\newcommand\Val{\mathit{Val}}
\newcommand\Exp{\mathit{Exp}}
\newcommand\type{\mathit{type}}
\newcommand\eval{\mathit{eval}}
\newcommand\Type{\mathit{Ty}}
\newcommand\Eq{\mathit{Eq}}
\newcommand\PartialEq{\mathit{PartialEq}}
\newcommand\Terminates{\mathit{Terminates}}
\newcommand\Reflexive{\mathit{Reflexive}}
\newcommand\Transitive{\mathit{Transitive}}
\newcommand\Linear{\mathit{Linear}}
\newcommand\LinPreorder{\mathit{LinPreorder}}
\newcommand\Sorted{\mathit{Sorted}}
\newcommand\StreamEq{\mathit{StreamEq}}
\newcommand\PreservesAndReflects{\mathit{PreservesAndReflects}}
\newcommand\lfp{\mathit{lfp}}
\newcommand\gfp{\mathit{gfp}}
\newcommand\itrel{\mathit{rel}}
\newcommand\map{\mathit{map}}
\newcommand\Env{\mathit{Env}}
\newcommand\erase{\mathit{erase}}
\newcommand\Subst{\mathit{Subst}}
\newcommand\id{\mathit{id}}


% semantic brackets
\newcommand{\rbr}{{\bf ]\!]}}
\newcommand{\lbr}{{\bf [\![}}
\newcommand\sem[1]{\lbr #1 \rbr}
\newcommand\semplus[2]{\mathcal{#1}\,\sem{#2}}
\newcommand\sempluss[3]{\mathcal{#1}_{#2}\,\sem{#3}}

% definitional equality
\newcommand\defeq{\stackrel{\mathrm{def}}{=}}
\newcommand\defequi{\stackrel{\mathrm{def}}{\Leftrightarrow}}

\ignore{
% theorems, definitions, ...
\newcommand\proof[1]{{\bf Proof.} #1 \hspace*{\fill}$\Box$\vspace{4mm}}
\newcommand\proofidea[1]{%
  {\bf Proof idea.} #1 \hspace*{\fill}$\Box$\vspace{4mm}}
\newcommand\farproof[2]{%
   {\bf Proof of { #1}.} #2\hspace*{\fill}$\Box$\vspace{4mm}}
\newcommand\remark[1]{{\bf Remark.} #1 \vspace{4mm}}}

