%\usepackage{amstex}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{eepic}


%%%%%%%%% INFERENCE RULES

\newlength{\rulevgap}
\setlength{\rulevgap}{0.05in}
\newlength{\ruleheight}
\newlength{\ruledepth}
\newsavebox{\rulebox}
\newlength{\GapLength}
\newcommand{\gap}[1]{\settowidth{\GapLength}{#1} \hspace*{\GapLength}}
\newcommand{\dotstep}[2]{\begin{tabular}[b]{@{}c@{}}
                         #1\\$\vdots$\\#2
                         \end{tabular}}
\newlength{\fracwid}
\newcommand{\dotfrac}[2]{\settowidth{\fracwid}{$\frac{#1}{#2}$}
                         \addtolength{\fracwid}{0.1in}
                         \begin{tabular}[b]{@{}c@{}}
                         $#1$\\
                         \parbox[c][0.02in][t]{\fracwid}{\dotfill} \\
                         $#2$\\
                         \end{tabular}}
\newcommand{\Rule}[2]{\savebox{\rulebox}[\width][b]                         %
                              {\( \frac{\raisebox{0in} {\( #1 \)}}       %
                                       {\raisebox{-0.03in}{\( #2 \)}} \)}   %
                      \settoheight{\ruleheight}{\usebox{\rulebox}}          %
                      \addtolength{\ruleheight}{\rulevgap}                  %
                      \settodepth{\ruledepth}{\usebox{\rulebox}}            %
                      \addtolength{\ruledepth}{\rulevgap}                   %
                      \raisebox{0in}[\ruleheight][\ruledepth]               %
                               {\usebox{\rulebox}}}
\newcommand{\Case}[2]{\savebox{\rulebox}[\width][b]                         %
                              {\( \dotfrac{\raisebox{0in} {\( #1 \)}}       %
                                       {\raisebox{-0.03in}{\( #2 \)}} \)}   %
                      \settoheight{\ruleheight}{\usebox{\rulebox}}          %
                      \addtolength{\ruleheight}{\rulevgap}                  %
                      \settodepth{\ruledepth}{\usebox{\rulebox}}            %
                      \addtolength{\ruledepth}{\rulevgap}                   %
                      \raisebox{0in}[\ruleheight][\ruledepth]               %
                               {\usebox{\rulebox}}}
\newcommand{\Axiom}[1]{\savebox{\rulebox}[\width][b]                        %
                               {$\frac{}{\raisebox{-0.03in}{$#1$}}$}        %
                      \settoheight{\ruleheight}{\usebox{\rulebox}}          %
                      \addtolength{\ruleheight}{\rulevgap}                  %
                      \settodepth{\ruledepth}{\usebox{\rulebox}}            %
                      \addtolength{\ruledepth}{\rulevgap}                   %
                      \raisebox{0in}[\ruleheight][\ruledepth]               %
                               {\usebox{\rulebox}}}
\newcommand{\RuleSide}[3]{\gap{$#2$} \hspace*{0.1in}               %
                            \Rule{#1}{#3}                          %
                          \hspace*{0.1in}$#2$}
\newcommand{\AxiomSide}[2]{\gap{$#1$} \hspace*{0.1in}              %
                             \Axiom{#2}                            %
                           \hspace*{0.1in}$#1$}
\newcommand{\RULE}[1]{\textbf{#1}}
\newcommand{\hg}{\hspace{0.2in}}

\newcommand{\ProofState}
                      [2]{\parbox{10cm}{\AR{\hg\AR{#1}\\\Axiom{\hg#2\hg}}}}

%%%%%%%%%%%% TRISTUFF

\newcommand{\btr}{
\setlength{\unitlength}{0.0005in}
\begin{picture}(69,180)(0,12)
\blacken\path(57,192)(57,12)(12,102)
	(57,192)(57,192)
\path(57,192)(57,12)(12,102)
	(57,192)(57,192)
\end{picture}
}

\newcommand{\btl}{
\setlength{\unitlength}{0.0005in}
\begin{picture}(69,180)(0,12)
\blacken\path(12,192)(12,12)(57,102)
	(12,192)(12,192)
\path(12,192)(12,12)(57,102)
	(12,192)(12,192)
\end{picture}
}

\newcommand{\wtr}{
\setlength{\unitlength}{0.0005in}
\begin{picture}(69,180)(0,12)
%\blacken\path(57,192)(57,12)(12,102)
%	(57,192)(57,192)
\path(57,192)(57,12)(12,102)
	(57,192)(57,192)
\end{picture}
}

\newcommand{\wtl}{
\setlength{\unitlength}{0.0005in}
\begin{picture}(69,180)(0,12)
%\blacken\path(12,192)(12,12)(57,102)
%	(12,192)(12,192)
\path(12,192)(12,12)(57,102)
	(12,192)(12,192)
\end{picture}
}



%%%%%%%%%%%% FONTS

\newcommand{\TC}[1]{\mathsf{#1}}
\newcommand{\DC}[1]{\mathsf{#1}}
\newcommand{\VV}[1]{\mathit{#1}}
\newcommand{\FN}[1]{\mathbf{#1}}
\newcommand{\HFN}[1]{\mathtt{#1}}
\newcommand{\RW}[1]{\underline{\textrm{#1}}}
\newcommand{\MO}[1]{\mbox{\textsc{#1}}}

\newcommand{\HF}[1]{\mathtt{#1}}

\newcommand{\MV}[1]{\nhole\mathit{#1}}
\newcommand{\Lang}[1]{\mathsf{#1}}
\newcommand{\Name}[1]{\mathit{#1}}

\newcommand{\demph}[1]{\textbf{#1}}
\newcommand{\remph}[1]{\emph{#1}}

%%%% Keywords for meta operations
\newcommand{\IF}{\;\RW{if}\;\;}
\newcommand{\THEN}{\RW{then}}
\newcommand{\ELSE}{\RW{else}}
\newcommand{\AND}{\RW{and}}
\newcommand{\Otherwise}{\RW{otherwise}}
\newcommand{\Do}{\RW{do}}
\newcommand{\Return}{\RW{return}}

\newcommand{\CASE}{\RW{case}}
\newcommand{\LET}{\RW{let}}
\newcommand{\IN}{\RW{in}}
\newcommand{\of}{\RW{of}}

\newcommand{\CLASS}{\mathtt{class}}
\newcommand{\INSTANCE}{\mathtt{instance}}

%%%%%%%%%%%% GROUPING

\newcommand{\G}{
\setlength{\unitlength}{1pt}
\begin{picture}(4,10)(0,0)
\path(2,10)(2,-10)
\end{picture}
}

\newcommand{\E}{
\setlength{\unitlength}{1pt}
\begin{picture}(4,10)(0,0)
\path(2,10)(2,-2)(4,-2)
\end{picture}
}

%\newcommand{\C}{
%\setlength{\unitlength}{1pt}
%\begin{picture}(4,10)(0,0)
%\path(4,8)(2,8)(2,-2)(4,-2)
%\end{picture}
%}

\newcommand{\M}{
\setlength{\unitlength}{1pt}
\begin{picture}(4,10)(0,0)
\path(2,10)(2,-2)(6,-2)
\end{picture}
}

\newcommand{\F}{
\setlength{\unitlength}{1pt}
\begin{picture}(4,10)(0,0)
\path(4,8)(2,8)(2,-6)
\end{picture}
}

\newcommand{\K}{
\setlength{\unitlength}{1pt}
\begin{picture}(4,10)(0,0)
\path(0,8)(4,8)
\end{picture}
}

\newcommand{\J}{
\setlength{\unitlength}{1pt}
\begin{picture}(4,10)(0,0)
\path(0,-2)(4,-2)
\end{picture}
}

\newcommand{\W}{
\setlength{\unitlength}{1pt}
\begin{picture}(4,10)(0,0)
\end{picture}
}



%%%%%%%%%%%% GUBBINS

\newcommand{\mathskip}{\medskip}

\newcommand{\fbx}[1]{\fbox{$#1$}}
\newcommand{\stk}[1]{\begin{array}{c}#1\end{array}}
%\newcommand{\DM}[1]{\hg\mbox{$#1$}}
\newcommand{\DM}[1]{\mathskip\par\(#1\)\mathskip}
\newcommand{\mbx}[1]{\mathskip\par\noindent\(#1\)\mathskip}
\newcommand{\AR}[1]{\begin{array}[t]{@{}l}#1\end{array}}
\newcommand{\ARt}[1]{\begin{array}[t]{@{}l@{}cl}#1\end{array}}
\newcommand{\ARc}[1]{\begin{array}{@{}l}#1\end{array}}
\newcommand{\ARd}[1]{\begin{array}[t]{cl}#1\end{array}}
\newcommand{\EA}[1]{\begin{array}[t]{r@{}c@{}l}#1\end{array}}
\newcommand{\A}{@{\:}c}
%\newcommand{\R}{@{\:}r}
\newcommand{\CA}{c}
\newcommand{\LA}{l}
\newcommand{\PAc}[2]{\begin{array}{l#1@{}r@{}l}#2\end{array}}
\newcommand{\PA}[2]{\begin{array}[t]{l@{\:}l#1@{}r@{\:}l}#2\end{array}}
\newcommand{\DTREE}[3]{\begin{array}[t]{l#1@{}r@{\:}l#2}#3\end{array}}
\newcommand{\IDTREE}[2]{%
  \begin{array}[t]{l@{\:}c@{\:}l@{\:}r@{\:}l#1}#2\end{array}}
\newcommand{\IA}[2]
   {\begin{array}[t]{l@{\:}r@{\:}c@{\:}l@{\:}#1@{\:}r@{\:}l}#2\end{array}}
\newcommand{\IAc}[2]
   {\begin{array}[c]{r@{\:}c@{\:}l@{\:}#1@{}r@{}l}#2\end{array}}
\newcommand{\CS}[1]{\left\lfloor\begin{array}{@{}l}#1\end{array}\right.}
\newcommand{\BY}[3]{\multicolumn{2}{l}{\;\RW{by}\; #1} \\ %
    \multicolumn{#2}{l}{\CS{#3}} }
\newcommand{\WITH}[3]{\multicolumn{2}{l}{\;\RW{with}\; #1} \\ %
    \multicolumn{#2}{l}{\CS{#3}} }
\newcommand{\WithBy}{\RW{with-by}}
\newcommand{\Wb}[1]{\WithBy& #1}
\newcommand{\By}[1]{\multicolumn{2}{l}{\Leftarrow #1}}
\newcommand{\andby}{\Leftarrow}
\newcommand{\MyWith}[1]{\multicolumn{2}{l}{|\;#1}}
\newcommand{\Byr}[1]{\;\RW{by}\; #1}

\renewcommand{\Bar}{|}
\newcommand{\Bart}{\settowidth{\GapLength}{$\Bar$}%
                   \raisebox{6pt}[0pt][0pt]{$\Bar$}%
                   \hspace*{-1\GapLength}%
                   \Bar}
\newcommand{\With}[1]{\Bar & #1}
\newcommand{\Witt}[1]{\Bart & #1}

\newcommand{\B}{@{\:}r@{\:}c}
\newcommand{\Ret}[1]{\multicolumn{2}{l}{\cq #1}}
\newcommand{\MRet}[2]{\multicolumn{#1}{l}{\cq #2}}
\newcommand{\HRet}[1]{\multicolumn{2}{l}{\hq #1}}
\newcommand{\MHRet}[2]{\multicolumn{#1}{l}{\hq #2}}
\newcommand{\IRet}[1]{\multicolumn{2}{l}{\iq #1}}
\newcommand{\IMRet}[2]{\multicolumn{#1}{l}{\iq #2}}
\newcommand{\MoRet}[1]{\multicolumn{2}{l}{\mq #1}}
\newcommand{\MMoRet}[2]{\multicolumn{#1}{l}{\mq #2}}
\newcommand{\Data}{\RW{data}}
\newcommand{\Where}{\RW{where}}
\newcommand{\Let}{\RW{let}}
\newcommand{\Fact}{\RW{fact}}
\newcommand{\Rec}[1]{#1\textbf{-Rec}}
\newcommand{\Memo}[1]{#1\textbf{-Memo}}
\newcommand{\Elim}[1]{#1\textbf{-Elim}}
\newcommand{\Cases}[1]{#1\textbf{-Case}}
\newcommand{\View}[1]{#1\textbf{-View}}
\newcommand{\As}[2]{#1 \:\RW{as}\: #2}
\newcommand{\nhole}{\Box}
\newcommand{\turq}{\:\vdash_?\:}
\renewcommand{\split}{\;\lhd\;}
\newcommand{\CType}[2]{\{#1 \split\; #2\}}
\newcommand{\CC}[2]{(#1)\:#2}
\newcommand{\UP}[2]{#1 | \{#2\}}
\newcommand{\Ured}{\:\Downarrow\:}
\newcommand{\gdd}{\prec}
\newcommand{\HC}[1]{\left<#1\right>}
\newcommand{\HT}[2]{\left<#1 \hab #2\right>}

\newcommand{\view}{\RW{view}}
\newcommand{\ecase}{\RW{case}}
\newcommand{\rec}{\RW{rec}}

\newcommand{\If}{\mathsf{if}}
\newcommand{\Then}{\mathsf{then}}
\newcommand{\Else}{\mathsf{else}}
\newcommand{\elim}{\RW{elim}}

\newcommand{\Payload}{\mathsf{type}}
\newcommand{\Any}{\mathsf{Some}}

\newcommand{\lbl}[2]{\langle #1 \Hab #2 \rangle}
\newcommand{\call}[2]{\RW{call}\:\langle#1\rangle\:#2}
\newcommand{\return}[1]{\RW{return}\:#1}

\newcommand{\Remark}[1]{\noindent\textbf{Remark:} #1}

\newcommand{\DBOX}[2]{\fbox{\parbox{#1}{\textbf{Definition:}#2}}}

\newcommand{\FIG}[3]{\begin{figure}[h]\DM{#1}\caption{#2}\label{#3}\end{figure}}
\newcommand{\FFIG}[3]{\begin{figure}[h]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}
\newcommand{\FFIGTC}[3]{\begin{figure*}[t]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure*}}
\newcommand{\VFIG}[3]{\begin{figure}[h]\begin{boxedverbatim}#1\end{boxedverbatim}\caption{#2}\label{#3}\end{figure}}
\newcommand{\PFIG}[3]{\begin{figure}[p]\begin{center}\fbox{\DM{#1}}\end{center}\caption{#2}\label{#3}\end{figure}}
\newcommand{\CFIG}[3]{\begin{figure}[h]\begin{center}\DM{#1}\end{center}\caption{#2}\label{#3}\end{figure}}

\newcommand{\TFIG}[4]{\begin{figure}[h]\begin{center}\begin{tabular}{#1}#2\end{tabular}\end{center}\caption{#3}\label{#4}\end{figure}}
\newcommand{\TFIGTC}[4]{\begin{figure*}[t]\begin{center}\begin{tabular}{#1}#2\end{tabular}\end{center}\caption{#3}\label{#4}\end{figure*}}

\newcommand{\RESFIG}[3]{
\TFIG{|l|c|c|c|c|c|c|c|c|}{
\hline
    & \multicolumn{4}{c|}{\Naive{} compilation} &
          \multicolumn{4}{|c|}{Optimised compilation} \\
\cline{2-9}
\raisebox{1.5ex}[0pt]{Program} & Instrs & Thunks & Cells &
Accesses & Instructions & Thunks & Cells & Accesses \\
%\raisebox{1.5ex}[0pt]{Program} & I & T & C & M & I & T & C & M \\
\hline
#1
\hline
}{#2}{#3}}

\newcommand{\NEWRESFIG}[3]{
\TFIG{|l|l|c|c|c|c|}{
\hline
%    & \multicolumn{4}{c|}{\Naive{} compilation} &
%          \multicolumn{4}{|c|}{Optimised compilation} \\
%\cline{2-9}
Program & Version & Instructions & Thunks & Memory Accesses & Cells \\
%\raisebox{1.5ex}[0pt]{Program} & I & T & C & M & I & T & C & M \\
\hline
#1
}{#2}{#3}}

\newcommand{\NEWRESFIGTC}[3]{
\TFIGTC{|l|l|c|c|c|c|}{
\hline
%    & \multicolumn{4}{c|}{\Naive{} compilation} &
%          \multicolumn{4}{|c|}{Optimised compilation} \\
%\cline{2-9}
Program & Version & Instructions & Thunks & Memory Accesses & Cells \\
%\raisebox{1.5ex}[0pt]{Program} & I & T & C & M & I & T & C & M \\
\hline
#1
}{#2}{#3}}

\newcommand{\RESLINE}[9]{
& \Naive{} & #2 & #3 & #5 & #4 \\
#1
& Optimised & #6 & #7 & #9 & #8 \\
}
\newcommand{\RESCHANGE}[4]{
& Change & \textbf{#1} & \textbf{#2} & \textbf{#4} & \textbf{#3} \\
\hline
}
\newcommand{\RESCHANGEa}[5]{
#5 & Change & \textbf{#1} & \textbf{#2} & \textbf{#4} & \textbf{#3} \\
\hline
}

%%%%%%%%%%%% PUNCTUATION

\newcommand{\pad}[2]{#1#2#1}

\newcommand{\hab}{\pad{\,}{:}}
\newcommand{\Hab}{\pad{\;}{:}}
\newcommand{\HHab}{\pad{\;}{::}}

%%%%%%%%%%%% TYPE

\newcommand{\Type}{\star}


%%%%%%%%%%%%% ARROWS

\newcommand{\To}{\pad{\:}{\rightarrow}}
%\newcommand{\car}{\vartriangleright}

%%%%%%%%%%%%% QUANTIFIERS

\newcommand{\lam}[2]{\lambda#1\pad{\!}{:}#2}
\newcommand{\fbind}[3]{(#1\Hab#2)\to#3}
\newcommand{\all}[2]{\forall#1\pad{\!}{:}#2}
\newcommand{\hole}[2]{?#1\pad{\!}{:}#2}
\newcommand{\guess}[3]{?#1\pad{\!}{:}#2\approx#3}
\newcommand{\remlam}[2]{\lambda\{#1\pad{\!}{:}#2\}}
\newcommand{\remall}[2]{\forall\{#1\pad{\!}{:}#2\}}
\newcommand{\allpi}[2]{\Pi#1\pad{\!}{:}#2}
\newcommand{\ali}[2]{\forall#1|#2}
\newcommand{\exi}[2]{\exists#1\pad{\!}{:}#2}
\newcommand{\wit}[2]{\ang{#1,#2}}
\newcommand{\X}{\times}
\newcommand{\sig}[2]{\Sigma#1\pad{\!}{:}#2}

\newcommand{\SC}{.\:}

\newcommand{\letbind}[3]{\mathsf{let}\:#1{:}#2\:=\:#3\:\mathsf{in}}
\newcommand{\ifthen}[3]{\mathsf{if}\:#1\:\mathsf{then}\:#2\:\mathsf{else}\:#3}

%%%%%%%%%%%%% EQUALITIES

\newcommand{\cq}{\pad{\:}{\mapsto}}
\newcommand{\xq}{\pad{}{\doteq}}
\newcommand{\pq}{\pad{\:}{=}}
\newcommand{\dq}{\pad{\:}{:=}}
\newcommand{\iq}{\pad{\:}{\leadsto}}
\newcommand{\mq}{\Longrightarrow}
\newcommand{\retq}{\Rightarrow}
\newcommand{\hq}{\pad{\:}{=}}
\newcommand{\defq}{\mapsto}

\newcommand{\refl}{\TC{refl}}




%%%%%%%%%%%%% CATSTUFF

\newlength{\Lwibrs}
\newlength{\Lwobrs}
\newsavebox{\Bwibrs}
\newsavebox{\Bwobrs}
\newcommand{\Db}[5]{%
  \savebox{\Bwobrs}[\width][b]{$#5$}%
  \savebox{\Bwibrs}[\width][b]{$\left#2\usebox{\Bwobrs}\right#3$}%
  \settowidth{\Lwobrs}{\usebox{\Bwobrs}}%
  \settowidth{\Lwibrs}{\usebox{\Bwibrs}}%
  \addtolength{\Lwibrs}{-\Lwobrs}%
  \left#1\pad{\hspace*{-0.25\Lwibrs}}{\usebox{\Bwibrs}}\right#4}
\newcommand{\LDb}[3]{%
  \savebox{\Bwobrs}[\width][b]{$#3$}%
  \savebox{\Bwibrs}[\width][b]{$\left#2\usebox{\Bwobrs}\right.$}%
  \settowidth{\Lwobrs}{\usebox{\Bwobrs}}%
  \settowidth{\Lwibrs}{\usebox{\Bwibrs}}%
  \addtolength{\Lwibrs}{-\Lwobrs}%
  \left#1\hspace*{-0.4\Lwibrs}\usebox{\Bwibrs}\right.}
\newcommand{\RDb}[3]{%
  \savebox{\Bwobrs}[\width][b]{$#3$}%
  \savebox{\Bwibrs}[\width][b]{$\left.\usebox{\Bwobrs}\right#1$}%
  \settowidth{\Lwobrs}{\usebox{\Bwobrs}}%
  \settowidth{\Lwibrs}{\usebox{\Bwibrs}}%
  \addtolength{\Lwibrs}{-\Lwobrs}%
  \left.\usebox{\Bwibrs}\hspace*{-0.4\Lwibrs}\right#2}
\newcommand{\Sc}{\Db{[}{[}{]}{]}}
\newcommand{\Mo}{\Db{|}{>}{<}{|}}
\newcommand{\MoL}{\LDb{|}{>}}
\newcommand{\MoR}{\RDb{<}{|}}

\newcommand{\car}{\mbox{$-\!\triangleright$}}
\newcommand{\io}[1]{\iota_{#1}}
\newcommand{\cc}{\diamond}


%%%%%%%%%%%%% FNS

\newcommand{\Wk}{\Uparrow}

%%%%%%%%%%%%% Transformation

\newcommand{\Transform}[3]{\textsc{Trans}\:_{\Name{#1}}
   \interp{#2}\:\mq\:#3}
%\:[\:#2\:\Longrightarrow\:#3\:]}
\newcommand{\Morphism}[2]{\textsc{Morphism}\:#1\:\Longrightarrow\:#2}
\newcommand{\MI}[1]{\begin{array}{ll} #1 \end{array}\\}
\newcommand{\MorphItem}[2]{& #1 \:\Longrightarrow\: #2}

%%%%%%%%%%%%% Stuff

% Motive and methods

\newcommand{\motive}{\vP}
\newcommand{\meth}[1]{\vm_{#1}}

% Tuples
\newcommand{\tuple}[1]{\langle#1\rangle}
\newcommand{\Tuple}[1]{\mathsf{Tuple}}
\newcommand{\proj}{\mathsf{proj}}
\newcommand{\app}{\mathrm{+\!+}}

% Commenting out
\newcommand{\ig}[1]{[#1]}
\newcommand{\rem}[1]{\{\!#1\!\}}
\newcommand{\igc}[1]{[#1]}
\newcommand{\remc}[1]{\{\!#1\!\}}


\newcommand{\ind}{\hspace*{0.1cm}}

% Content free type
\newcommand{\CF}{\TC{CF}}
\newcommand{\cf}{\DC{cf}}

% Error token
\newcommand{\error}{\DC{error}}
\newcommand{\fail}{\perp}

% Constructor stripping
\newcommand{\conarg}[2]{#1!#2}

\newcommand{\Vect}{\TC{Vect}}
\newcommand{\VectM}{\TC{Vect^-}}
\newcommand{\Vnil}{\DC{\epsilon}}
\newcommand{\Vcons}{\DC{::}}

\newcommand{\Vsnoc}{\DC{::}}

\newcommand{\VnilM}{\DC{\epsilon^-}}
\newcommand{\VconsM}{\DC{::^-}}

\newcommand{\Vnilcase}{\VV{vNilCase}}
\newcommand{\Vconscase}{\VV{vConsCase}}

\newcommand{\DSigma}{\TC{Sigma}}
\newcommand{\Exists}{\DC{Exists}}

\newcommand{\ListPair}[2]{\sig{#1}{\List\:\vA}.#2 = \FN{length}\:#1}
\newcommand{\lpNilDef}{\lpNil{\FN{refl}\:\Z}}
\newcommand{\lpNil}[1]{(\nil\:\vA,#1)}
\newcommand{\lpConsDef}[3]{\lpCons{#1}{(\FN{fst\:#2})}{\FN{resp}\:(\FN{snd}\:#2)}}
\newcommand{\lpCons}[3]{(\cons\:#1\:#2,#3)}
\newcommand{\lp}[2]{(#1, #2)}

\newcommand{\VnilTop}{\DC{vNil}^\ast}
\newcommand{\VconsTop}{\DC{vCons}^\ast}

\newcommand{\VnilBot}{\DC{\epsilon}^-}
\newcommand{\VconsBot}{\DC{::}^-}

\newcommand{\VectTop}{\TC{Vect}^\ast}
\newcommand{\VectBot}{\TC{Vect}^-}

\newcommand{\VectDrop}{\FN{vectDropIdx}}
\newcommand{\VectRebuild}{\FN{vectRebuild}}

\newcommand{\Prop}{\TC{Prop}}
\newcommand{\Set}{\TC{Set}}
\newcommand{\CoqType}{\TC{Type}}

\newcommand{\List}{\TC{List}}
\newcommand{\nil}{\DC{nil}}
\newcommand{\cons}{\DC{cons}}

\newcommand{\Zip}{\TC{Tsil}}
\newcommand{\zip}{\FN{tsil}}
\newcommand{\zipcons}{\FN{tsilcons}}
\newcommand{\snoc}{\DC{Snoc}}
\newcommand{\lin}{\DC{Empty}}

\newcommand{\BigInt}{\TC{BigInt}}
\newcommand{\False}{\TC{False}}
\newcommand{\Unit}{\TC{True}}
\newcommand{\UnitI}{\DC{()}}

\newcommand{\genType}{\TC{X}}
\newcommand{\genIndicesDec}{\tb\Hab\tB}
\newcommand{\genIndices}{\tb}
\newcommand{\genConArgsDec}[1]{\vec{\VV{a_#1}}\Hab\vec{\VV{A_#1}}}
\newcommand{\genConArgs}[1]{\vec{\VV{a_#1}}}
\newcommand{\genConIndicesDec}[1]{\vec{\VV{b_#1}}\Hab\vec{\VV{B_#1}}}
\newcommand{\genConIndices}[1]{\vec{\VV{b_#1}}}
\newcommand{\genCon}[1]{\DC{x}_#1}

\newcommand{\genTypeTop}{\TC{X^\ast}}
\newcommand{\genTypeBot}{\TC{X^-}}

\newcommand{\genTypeDrop}{\FN{XDropIdx}}
\newcommand{\genTypeRebuild}{\FN{XRebuild}}

\newcommand{\HTerm}{\texttt{Term}}
\newcommand{\Term}{\TC{Term}}
\newcommand{\Var}{\DC{var}}
\newcommand{\Lam}{\DC{lam}}
\newcommand{\App}{\DC{app}}
\newcommand{\TermM}{\TC{Term^-}}
\newcommand{\VarM}{\DC{var^-}}
\newcommand{\LamM}{\DC{lam^-}}
\newcommand{\AppM}{\DC{app^-}}
\newcommand{\Env}{\TC{Env}}
\newcommand{\SType}{\TC{STy}}
\newcommand{\farrow}{\Rightarrow}
\newcommand{\lookup}{\FN{lookup}}

\newcommand{\source}{\Lang{TT}}
\newcommand{\target}{\Lang{ExTT}}
\newcommand{\runtime}{\Lang{RunTT}}

\newcommand{\lt}{\TC{<}}
\newcommand{\ltO}{\DC{ltO}}
\newcommand{\ltS}{\DC{ltS}}

\newcommand{\interp}[1]{\llbracket #1 \rrbracket}
\newcommand{\inferrable}[2]{\FN{inferrable}(#1,#2)}
\newcommand{\mkPat}{\FN{mkPat}}

\newcommand{\FinM}{\TC{Fin^-}}
\newcommand{\fzM}{\DC{f0^-}}
\newcommand{\fsM}{\DC{fs^-}}

\newcommand{\concat}{\mathrm{++}}

%\newcommand{\bottom}{\perp}

% Reductions

\newcommand{\reduces}{\rhd}
\newcommand{\translation}{\Rightarrow}
%\newcommand{\reducesn}[1]{\reduces\hspace*{-0.15cm}_{#1}}
%\newcommand{\reducesto}{\reduces\hspace*{-0.15cm}^{*}}
\newcommand{\reducesn}[1]{\reduces_{#1}}
\newcommand{\reducesto}{\reduces^{*}}

% Equality

\newcommand{\Refl}{\DC{refl}}
\newcommand{\leZ}{\DC{O_{\le}}}
\newcommand{\leS}{\DC{S_{\le}}}

% Random elimination things

\newcommand{\lte}{\TC{\leq}}
\newcommand{\lten}{\DC{leN}}
\newcommand{\lteO}{\DC{leO}}
\newcommand{\lteS}{\DC{leS}}

\newcommand{\ltelim}{\Elim{\lt}}
\newcommand{\leelim}{\Elim{\lte}}

\newcommand{\dD}{\TC{D}}
\newcommand{\delim}{\Elim{\TC{D}}}
\newcommand{\drec}{\Rec{\TC{D}}}
\newcommand{\dcase}{\Cases{\TC{D}}}
\newcommand{\dview}{\View{\TC{D}}}
\newcommand{\dmemo}{\Memo{\TC{D}}}
\newcommand{\natrec}{\Rec{\Nat}}
\newcommand{\natmemo}{\Memo{\Nat}}
\newcommand{\natmemogen}{\Nat\textbf{-MemoGen}}
\newcommand{\natelim}{\Elim{\Nat}}
\newcommand{\boolcase}{\Cases{\Bool}}
\newcommand{\vectrec}{\Rec{\Vect}}
\newcommand{\vectelim}{\Elim{\Vect}}
\newcommand{\listrec}{\Rec{\List}}
\newcommand{\listelim}{\Elim{\List}}
\newcommand{\finrec}{\Rec{\Fin}}
\newcommand{\finelim}{\Elim{\Fin}}
\newcommand{\natcase}{\Cases{\Nat}}
\newcommand{\vectcase}{\Cases{\Vect}}
\newcommand{\natdoublerec}{\Nat\textbf{-double-elim}}
\newcommand{\eqelim}{=\textbf{-elim}}
\newcommand{\falsecase}{\Cases{\False}}

% Code
\newcommand{\Haskell}[1]{\begin{quotation}\begin{verbatim}#1\end{verbatim}\end{quotation}}

% Quicksort

\newcommand{\QSView}{\TC{QuickSort}}
\newcommand{\qsempty}{\DC{empty}}
\newcommand{\partition}{\DC{partition}}
\newcommand{\qsview}{\FN{mkQuickSort}}

% More gubbins

\newcommand{\converts}{\simeq}
\newcommand{\cumul}{\preceq}
\newcommand{\whnf}{\Downarrow}
\newcommand{\elem}{\in}
\newcommand{\proves}{\vdash}
\newcommand{\biimplies}{\Longleftrightarrow}

\newcommand{\lc}{\lambda_{\mathsf{AC}}}
\newcommand{\zed}{\mathbb{Z}}

% Haskell keywords

\newcommand{\hdata}{\mathtt{data}}
\newcommand{\newtype}{\mathtt{newtype}}
%\newcommand{\htype}{\mathtt{type}}

\newcommand{\HTC}[1]{\mathtt{#1}}
\newcommand{\HDC}[1]{\mathtt{#1}}

% Nobby

\newcommand{\Value}{\HTC{Value}}
\newcommand{\VGamma}{\HTC{Env}}
\newcommand{\Ctxt}{\HTC{Ctxt}}
\newcommand{\Defs}{\HTC{Defs}}
\newcommand{\ECtxt}{\HTC{ECtxt}}
\newcommand{\TCtxt}{\HTC{TCtxt}}
\newcommand{\VG}{\HDC{Env}}
\newcommand{\Model}{\HTC{Model}}
\newcommand{\Const}{\HTC{Const}}
\newcommand{\Normal}{\HTC{Normal}}
\newcommand{\Scope}{\HTC{Scope}}
\newcommand{\Kripke}{\HTC{Kripke}}
\newcommand{\Weakening}{\HTC{Weakening}}
\newcommand{\Ready}{\HTC{Ready}}
\newcommand{\Blocked}{\HTC{Blocked}}
\newcommand{\Spine}{\HTC{Spine}}

\newcommand{\BV}{\HDC{BV}}
\newcommand{\BCon}{\HDC{BCon}}
\newcommand{\BTyCon}{\HDC{BTyCon}}
\newcommand{\RCon}{\HDC{RCon}}
\newcommand{\RTyCon}{\HDC{RTyCon}}
\newcommand{\BElim}{\HDC{BElim}}
\newcommand{\DV}{\HDC{V}}
\newcommand{\DP}{\HDC{P}}

\newcommand{\MR}{\HDC{R}}
\newcommand{\MB}{\HDC{B}}
\newcommand{\DSc}{\HDC{Sc}}
\newcommand{\DKr}{\HDC{Kr}}
\newcommand{\DWk}{\HDC{Wk}}
\newcommand{\DSnoc}{\HDC{;}}
\newcommand{\DType}{\HDC{Type}}
\newcommand{\DName}{\HDC{Name}}
\newcommand{\DInt}{\HDC{Int}}
\newcommand{\DString}{\HDC{String}}
\newcommand{\DElim}{\HDC{Elim}}
\newcommand{\Empty}{\HDC{\emptyset}}

\newcommand{\ConCode}{\HTC{ConCode}}
\newcommand{\ElimRule}{\HTC{ElimRule}}

\newcommand{\DConst}{\HDC{Const}}
\newcommand{\DCon}{\HDC{Con}}
\newcommand{\DTyCon}{\HDC{TyCon}}
\newcommand{\RConst}{\HDC{RConst}}
\newcommand{\RLam}{\HDC{RLam}}
\newcommand{\RPi}{\HDC{RPi}}
\newcommand{\DLam}{\HDC{Lam}}
\newcommand{\DLet}{\HDC{Let}}
\newcommand{\DPi}{\HDC{Pi}}
\newcommand{\DApp}{\HDC{App}}

\newcommand{\TMaybe}{\HTC{Maybe}}
\newcommand{\DNothing}{\HDC{Nothing}}
\newcommand{\DJust}{\HDC{Just}}


% G-machine and heap

\newcommand{\PUSH}{\mathsf{PUSH}}
\newcommand{\PUSHNAME}{\mathsf{PUSHNAME}}
\newcommand{\POP}{\mathsf{DISCARD}}
\newcommand{\PUSHFUN}{\mathsf{PUSHFUN}}
\newcommand{\APPLY}{\mathsf{MKAP}}
\newcommand{\EVAL}{\mathsf{EVAL}}
\newcommand{\GCON}{\mathsf{MKCON}}
\newcommand{\GTUP}{\mathsf{MKTUP}}
\newcommand{\GTYPE}{\mathsf{MKTYPE}}
\newcommand{\UPDATE}{\mathsf{UPDATE}}
\newcommand{\RET}{\mathsf{RET}}
\newcommand{\UNWIND}{\mathsf{UNWIND}}
\newcommand{\CASEJUMP}{\mathsf{CASEJUMP}}
\newcommand{\LABEL}{\mathsf{LABEL}}
\newcommand{\MOVE}{\mathsf{MOVE}}
\newcommand{\JUMP}{\mathsf{JUMP}}
\newcommand{\SPLIT}{\mathsf{SPLIT}}
\newcommand{\SQUEEZE}{\mathsf{SQUEEZE}}
\newcommand{\JFUN}{\mathsf{JFUN}}
\newcommand{\PROJ}{\mathsf{PROJ}}
\newcommand{\ERROR}{\mathsf{ERROR}}
\newcommand{\SLIDE}{\mathsf{SLIDE}}
\newcommand{\ALLOC}{\mathsf{ALLOC}}

\newcommand{\PUSHBIG}{\mathsf{PUSHBIG}}
\newcommand{\PUSHBASIC}{\mathsf{PUSHBASIC}}
\newcommand{\PUSHINT}{\mathsf{PUSHINT}}
\newcommand{\PUSHBOOL}{\mathsf{PUSHBOOL}}
\newcommand{\GET}{\mathsf{GET}}
\newcommand{\MKINT}{\mathsf{MKINT}}
\newcommand{\MKBOOL}{\mathsf{MKBOOL}}
\newcommand{\ADD}{\mathsf{ADD}}
\newcommand{\SUB}{\mathsf{SUB}}
\newcommand{\MULT}{\mathsf{MULT}}
\newcommand{\LT}{\mathsf{LT}}
\newcommand{\EQ}{\mathsf{EQ}}
\newcommand{\GT}{\mathsf{GT}}
\newcommand{\JTRUE}{\mathsf{JTRUE}}

\newcommand{\APP}{\mathsf{APP}}
\newcommand{\FUN}{\mathsf{FUN}}
\newcommand{\CON}{\mathsf{CON}}
\newcommand{\TYCON}{\mathsf{TYCON}}
\newcommand{\TUP}{\mathsf{TUP}}
\newcommand{\TYPE}{\mathsf{TYPE}}
\newcommand{\INT}{\mathsf{INT}}
\newcommand{\BIGINT}{\mathsf{BIGINT}}
\newcommand{\BOOL}{\mathsf{BOOL}}
\newcommand{\HOLE}{\mathsf{HOLE}}

% G machine translation scheme

\newcommand{\sinterp}[1]{\mathcal{S}\interp{#1}}
\newcommand{\sinterpm}[1]{\mathcal{S}\AR{\interp{#1}}}
\newcommand{\einterp}[3]{\mathcal{E}\interp{#1}\:#2\:#3}
\newcommand{\cinterp}[3]{\mathcal{C}\interp{#1}\:#2\:#3}
\newcommand{\binterp}[3]{\mathcal{B}\interp{#1}\:#2\:#3}
\newcommand{\rinterp}[3]{\mathcal{R}\interp{#1}\:#2\:#3}
\newcommand{\iinterp}[3]{\mathcal{I}\interp{#1}\:#2\:#3}
\newcommand{\len}[1]{\MO{length}(#1)}

\newcommand{\casecomp}[2]{\mathcal{I}(#1,\left\{\ARc{#2}\right\})}
\newcommand{\casecompA}[3]{\mathcal{I}(#1,\left\{\ARc{#2}\right\}[#3])}
\newcommand{\ischeme}{\mathcal{I}}

% tail call markup

\newcommand{\tailcall}{\mathsf{tail}}

% Trees

\newcommand{\Tree}{\TC{Tree}}
\newcommand{\Leaf}{\DC{Leaf}}
\newcommand{\Node}{\DC{Node}}
\newcommand{\treecase}{\Cases{\Tree}}

% Languages

\newcommand{\Coq}{\textsc{Coq}}
\newcommand{\Lego}{\textsc{Lego}}
\newcommand{\Oleg}{\textsc{Oleg}}
\newcommand{\Alf}{\textsc{Alf}}
\newcommand{\Epigram}{\textsc{Epigram}}
\newcommand{\SystemF}{System $\mathcal{F}$}
\newcommand{\Iswim}{\textsc{Iswim}}
\newcommand{\Cynthia}{\textit{C$^Y$\hspace*{-0.1cm}NTHIA}}

% Accessibility

\newcommand{\Acc}{\TC{Acc}}
\newcommand{\acc}{\DC{acc}}
\newcommand{\qsAcc}{\TC{qsAcc}}
\newcommand{\qsNil}{\DC{qsNil}}
\newcommand{\qsCons}{\DC{qsCons}}
\newcommand{\allQsAcc}{\FN{allQsAcc}}

% Lazy shortcuts

\newcommand{\naive}{na\"{\i}ve}
\newcommand{\Naive}{Na\"{\i}ve}

% Conor's bits

\newcommand{\remem}[1]{\left|#1\right|}
\newcommand{\idsb}{\MO{id}}
\newcommand{\ang}[1]{\langle#1\rangle}

\newcommand{\vePm}[1]{\vP #1 \vm_{\Vnil} #1 \vm_{\Vcons}}%
\newcommand{\vcrhs}{\vm_{\Vcons}\:\vk\:\va\:\vv\:%
                     (\vectelim\:\vA\:\vk\:\vv\:\vePm{\:})}%

\newcommand{\igV}[2]{#1^{\ig{#2}}}
\newcommand{\remV}[2]{#1^{\rem{#2}}}

\newcommand{\FIXME}[1]{[\textbf{FIXME}: #1]}
%\newcommand{\FIXME}[1]{\wibble}

% More gubbins

\newcommand{\Between}{\TC{between}}
\newcommand{\bZ}{\DC{bO}}
\newcommand{\bZZS}{\DC{bOOs}}
\newcommand{\bZSS}{\DC{b0ss}}
\newcommand{\bSSS}{\DC{bsss}}
\newcommand{\betelim}{\Elim{\Between}}
\newcommand{\betrhs}[1]{\motive#1\meth{\bZ}#1\meth{\bZZS}#1\meth{\bZSS}#1\meth{\bSSS}}


\newcommand{\valenv}{\TC{ValEnv}}
\newcommand{\vempty}{\DC{empty}}
\newcommand{\vextend}{\DC{extend}}

\newcommand{\EpiVal}{\TC{Epigram}}
\newcommand{\unsafeCoerce}{\HF{unsafeCoerce\mbox{\texttt{\#}}}}

\newcommand{\qq}{\mbox{\texttt{"}}}
\newcommand{\impossible}{\RW{Impossible}}

\newcommand{\Real}{\mathbb{R}}

\newcommand{\DoubleRec}{\TC{DoubleElim}}
\newcommand{\DoubleOn}{\DC{Double_{\Z\vn}}}
\newcommand{\DoubleSO}{\DC{Double_{\suc\Z}}}
\newcommand{\DoubleSS}{\DC{Double_{\suc\suc}}}

\newcommand{\doublerec}{\textbf{double-elim}}

\newcommand{\set}{\TC{DList}}
\newcommand{\setuser}{\TC{DListTop}}
\newcommand{\setempty}{\emptyset}
\newcommand{\setinsert}{\DC{insert}}


%%%% Type systems

\newcommand{\stlc}{\lambda\hspace*{-0.15cm}\to}
\newcommand{\plc}{\lambda2}
\newcommand{\dlc}{\lambda{}P}

\newcommand{\EC}{\mathcal{E}}

%%%% reductions

\newcommand{\betared}{\iq\hspace*{-0.15cm}_{\beta}}
\newcommand{\deltared}{\iq\hspace*{-0.15cm}_{\delta}}
\newcommand{\gammared}{\iq\hspace*{-0.15cm}_{\gamma}}
\newcommand{\etared}{\iq\hspace*{-0.15cm}_{\eta}}
\newcommand{\iotared}{\iq\hspace*{-0.15cm}_{\iota}}
\newcommand{\rhored}{\iq\hspace*{-0.15cm}_{\rho}}

%%%% ExTT rules

\newcommand{\exconverts}{\stackrel{\mathsf{Ex}}{\converts}}
\newcommand{\excumul}{\stackrel{\mathsf{Ex}}{\cumul}}
\newcommand{\exequiv}{\stackrel{\mathsf{Ex}}{\equiv}}
\newcommand{\exreduces}{\stackrel{\mathsf{Ex}}\reduces}
\newcommand{\exreducesto}{\stackrel{\mathsf{Ex}}{\reducesto}}
\newcommand{\exreducesn}[1]{\exreduces_{#1}}

\newcommand{\ttequiv}{\stackrel{\mathsf{TT}}{\equiv}}
\newcommand{\ttreduces}{\stackrel{\mathsf{TT}}\reduces}
\newcommand{\ttreducesn}[1]{\ttreduces_{#1}}

%%% Type synthesis

\newcommand{\hastype}{\Longrightarrow}
\newcommand{\whnfs}{\twoheadrightarrow}
\newcommand{\conv}{\converts}

\newcommand{\exhastype}{\stackrel{\mathsf{Ex}}{\hastype}}
\newcommand{\exwhnfs}{\stackrel{\mathsf{Ex}}{\whnfs}}
\newcommand{\exconv}{\stackrel{\mathsf{Ex}}{\conv}}
\newcommand{\exproves}{\stackrel{\mathsf{Ex}}{\proves}}

\newcommand{\tthastype}{\stackrel{\mathsf{TT}}{\hastype}}
\newcommand{\ttwhnfs}{\stackrel{\mathsf{TT}}{\whnfs}}
\newcommand{\ttconv}{\stackrel{\mathsf{TT}}{\conv}}
\newcommand{\ttproves}{\stackrel{\mathsf{TT}}{\proves}}

%%% Lightning

\newcommand{\light}[1]{\lightning^{#1}}
\newcommand{\LHab}[1]{\pad{\;}{:^{#1}}}
\newcommand{\llam}[3]{\lambda#1\pad{\!}{:}^{#2}#3}
\newcommand{\lall}[3]{\forall#1\pad{\!}{:}^{#2}#3}
\newcommand{\lapp}[3]{#1(#2)^{#3}}
\newcommand{\larg}[2]{(#1)^{#2}}

\newcommand{\RName}[1]{\hspace*{0.1in}\mathsf{#1}}