\newbox\toc
\global\setbox\toc=\vbox{}

\newcommand{\df}{\mathit{def}}
\newcommand{\addtoc}[1]{
% Append it to the table of contents.
\global\setbox\toc=\vbox{\tiny\unvbox\toc\hbox{\strut\arabic{slide}: #1\strut}}
}
\newcommand{\slidetitle}[1]{
  {\large #1} \addtoc{#1} \vspace{.1cm} \par  
                            \hrule% \vspace{-.5cm}\noindent}
 }

\newlength{\bcpextraheight}
\newlength{\bcpextrawidth}
\setlength{\bcpextraheight}{2.4cm}
\setlength{\bcpextrawidth}{0cm}

\addtolength{\textwidth}{\bcpextrawidth}
\addtolength{\textheight}{\bcpextraheight}
\addtolength{\oddsidemargin}{-.5\bcpextrawidth}
\addtolength{\evensidemargin}{-.5\bcpextrawidth}
\addtolength{\topmargin}{-.5\bcpextraheight}
\newcommand{\oftp}{\mathord{:}}
\newcommand{\hastype}{\mathrel{:}}
\newcommand{\bnfas}{\mathrel{::=}}
\newcommand{\bnfalt}{\mathrel{\mid}}
\newcommand{\arrow}{\mathbin{\rightarrow}}
\newcommand{\fa}{\mathbin{\Rightarrow}} \newcommand{\Fa}{$\fa$\ }
\newcommand{\all}{\mathord{\forall}} \newcommand{\All}{$\all$\ }
\newcommand{\vd}{\null\mathrel{\vdash}}
\def\nprv{\null\mathrel{\not\vdash}} %Frank's
\def\nvd{\null\mathrel{\not\vdash}} %Frank's
% \newcommand{\th}{\null\mathrel{\vdash}}
\newcommand{\goesto}{\Longrightarrow}
\newcommand{\lam}{\lambda}
\newcommand{\evalsto}{\mathrel{\hookrightarrow}}
\newcommand{\ldot}{\mathord{.}}
\newcommand{\ldott}{\mathrel{.}}

% ----------------------------------------------------------------------
% Typesetting deductions.
% ----------------------------------------------------------------------

\newbox\tempa
\newbox\tempb
\newdimen\tempc
\newbox\tempd

\def\mud#1{\hfil $\displaystyle{#1}$\hfil}
\def\rig#1{\hfil $\displaystyle{#1}$}

\def\inruleanhelp#1#2#3{\setbox\tempa=\hbox{$\displaystyle{\mathstrut #2}$}%
                        \setbox\tempd=\hbox{$\; #3$}%
                        \setbox\tempb=\vbox{\halign{##\cr
        \mud{#1}\cr
        \noalign{\vskip\the\lineskip}%
        \noalign{\hrule height 0pt}%
        \rig{\vbox to 0pt{\vss\hbox to 0pt{\copy\tempd \hss}\vss}}\cr
        \noalign{\hrule}%
        \noalign{\vskip\the\lineskip}%
        \mud{\copy\tempa}\cr}}%
                      \tempc=\wd\tempb
                      \advance\tempc by \wd\tempa
                      \divide\tempc by 2 }

\def\inrulean#1#2#3{{\inruleanhelp{#1}{#2}{#3}%
                     \hbox to \wd\tempa{\hss \box\tempb \hss}}}

\def\ian#1#2#3{{\lineskip 4pt\inrulean{#1}{#2}{#3}}}
\def\ibn#1#2#3#4{{\ian{#1\hspace{3em}#2}{#3}{#4}}}

% \def\lowerhalf#1{\hbox{\raise -0.8\baselineskip\hbox{#1}}}

\def\ianc#1#2#3{{\lineskip 4pt\inruleanhelp{#1}{#2}{#3}%
                             \box\tempb\hskip\wd\tempd}}
\def\ibnc#1#2#3#4{{\lineskip 4pt\ianc{#1\quad\qquad #2}{#3}{#4}}}

%\newcommand{\Dick}{Dyckhoff}
%\newcommand{\snot}{\sim}
\def\vd{\null\mathrel{\vdash}} %Frank's
\def\nprv{\null\mathrel{\not\vdash}} %Frank's
\newcommand{\mnot}{{\rm Not}}
\newcommand{\ex}{\exists}
\renewcommand{\ll}{\overline{l}}
\newcommand{\xn}{\overline{x_n}}
\newcommand{\xk}{\overline{x_k}}
\newcommand{\xnk}{\overline{x_{n-k}}}
\newcommand{\ym}{\overline{y_m}}
\newcommand{\yn}{\overline{y_n}}
\newcommand{\Xn}{\overline{X_n}}
\newcommand{\Yn}{\overline{Y_n}}
\newcommand{\Ym}{\overline{Y_m}}
\renewcommand{\wr}{\overline{w_r}}
\newcommand{\Wr}{\overline{W_r}}
\newcommand{\zp}{\overline{z_p}}
\newcommand{\zm}{\overline{z_m}}
\newcommand{\Zp}{\overline{Z_p}}
\newcommand{\tn}{\overline{t_n}}
\newcommand{\tm}{\overline{t_m}}
\newcommand{\sm}{\overline{s_m}}
\newcommand{\un}{\overline{u_n}}
\newcommand{\sN}{\overline{s_n}}
\newcommand{\Am}{\overline{A_m}}
\newcommand{\Bn}{\overline{B_n}}
\newcommand{\Ep}{\overline{E_q}}
\newcommand{\Hk}{\overline{H_k}}
\newcommand{\Mm}{\overline{M_m}}
 \newcommand{\Mn}{\ol{M_{n}}}
\newcommand{\Nn}{\overline{N_n}}
\newcommand{\vx}{\vec{x}}
\newcommand{\vy}{\vec{y}}
\newcommand{\vz}{\vec{z}}
\newcommand{\vw}{\vec{w}}
\newcommand{\vX}{\vec{X}}
\newcommand{\vY}{\vec{Y}}
\newcommand{\vZ}{\vec{Z}}
\newcommand{\vW}{\vec{W}}
\newcommand{\vt}{\vec{t}}
\newcommand{\vs}{\vec{s}}

\newcommand{\sqless}{\sqsubseteq}
\newcommand{\mdots}{, \dots ,}
\newcommand{\suchthat}{\mid}
\newcommand{\prv}{\vd}
\newcommand{\nq}{\neq}
 \newcommand{\eqdef}{\stackrel\mbox{\tiny  def}{=}}
\newcommand{\nebe}{\not =_{\beta\eta}}  % do not need argument
\newcommand{\ebe}{=_{\beta\eta}}

% renewd
%\renewcommand{\frac}{\ianc}
\renewcommand{\l}{\lambda}


\newcommand{\skl}{\mbox{}\\}
\newcommand{\vsk}{\\[2ex]}
\newcommand{\s}{\sigma}
\newcommand{\q}{\theta}
\newcommand{\fo}{first-order }
\newcommand{\ho}{higher-order }
\newcommand{\eg}{e.g.~}
\newcommand{\ie}{{i.e.~}}
\newcommand{\wrt}{{w.r.t.~}}
\newcommand{\lp}{logic programming\/ }
\newcommand{\cN}{{\cal N}}
\newcommand{\cC}{{\cal C}}
\newcommand{\cD}{{\cal D}}
\newcommand{\cE}{{\cal E}}
\newcommand{\cB}{{\cal B}}
\newcommand{\cQ}{{\cal Q}}
\newcommand{\cP}{{\cal P}}
\newcommand{\GG}{\Gamma}
\newcommand{\ap}{\mathrm{ca}}
\newcommand{\ci}{\mathrm{ci}}
\newcommand{\sk}{\mathit{sk}}
\newcommand{\SLD}{{\em SLD\/}}
\newcommand{\SLDNF}{{\em SLDNF\/}}
\newcommand{\NF}{{\em NF\/}}
\newcommand{\nf}{{\em NF\/}}
\newcommand{\ul}{\underline}
\newcommand{\ol}{\overline}
\newcommand{\Or}{\vee}
\newcommand{\BOr}{\bigvee}
\newcommand{\And}{\wedge}
\newcommand{\ANd}{\bigwedge}
\newcommand{\BAnd}{\bigwedge}
\newcommand{\Not}{\neg}
\newcommand{\Imp}{\rightarrow}
\newcommand{\LImp}{\longrightarrow}
\newcommand{\Lmap}{\longmapsto}
\newcommand{\lead}{\leadsto}
\newcommand{\If}{\leftarrow}
\newcommand{\Ift}{:-}
\newcommand{\Bimp}{\leftrightarrow}
\newcommand{\leavebigvspace}{\par 
\addvspace{\bigskipamount}}
\newcommand{\la}{\langle}
\newcommand{\ra}{\rangle}
\newcommand{\beq}{\begin{eqnarray*}}
\newcommand{\eneq}{\end{eqnarray*}}
\newcommand{\bit}{\begin{itemize}}
\newcommand{\enit}{\end{itemize}}
\newcommand{\ben}{\begin{enumerate}}
\newcommand{\enen}{\end{enumerate}}
\newcommand{\bedef}{\begin{Def}}
\newcommand{\enef}{\end{Def}}
\newcommand{\putline}[2]{
{\put(0,0.35){\line(1,0){#1}}
\put(#1.1,0.25){#2}}
}


%\newtheorem{Lemma}{Lemma}[section]
%\newtheorem{Corollary}{Corollary}[section]
%%\newtheorem{Property}{Property}[section]
%%%%%%\newtheorem{Fact}{Fact}[section]
%     %  \newtheorem{Notation}{Notation}[section]
%      % \newtheorem{Observation}{Observation}[section]
%      % \newtheorem{Proposal}{Proposal}[section]
%      % \newtheorem{Remark}{Remark}[section]
%      % \newtheorem{Result}{Result}[section]
%      % \newtheorem{Conjecture}{Conjecture}[section]
%      % \newtheorem{Claim}{Claim}[section]

%% \newcommand{\parray} [1]
%% {\begin{array}{lllll}
%% \[  #1\]
%% % \end{array}}

%% \newenvironment{proof}{\noindent
%% {\bf Proof.} $\;$}{$\phantom{a}$\hfill$\Box$\leavebigvspace}
%% \newenvironment{example}{\leavebigvspace\noindent
%% {\bf Example.} 
%% $\;$}{$\phantom{a}$\hfill$\Diamond$\leavebigvspace}
%% \def\theexample{\arabic{example}}
%% \newtheorem{Example}{Example}

%\newenvironment{Examplen}
%{\begin{Example}%  
%\def\p@example{\theexample} \em}%
%{{$\phantom{a}$\hfill$\Diamond$}\end{Example}}
%\newcommand{\bdef}[1]
%{{\small{\bf Definition \ref{#1}}}}
%\def\thedefinition{\thesection.\arabic{definition}}
%\newtheorem{Definition}{Definition}[section]
%\newenvironment{Def}
%{\begin{Definition}%  
%\def\p@definition{\thedefinition} \em}%
%{\end{Definition}}
%\def\theproperty{\thesection.\arabic{property}}
%\newtheorem{Property}{Property}[section]
%\newenvironment{Pty}
%{\begin{Property}%  
%\def\p@property{\theproperty} \em}%
%{\end{Property}}
%\newcommand{\bpty}[1]
%{{\small{\bf Property \ref{#1}}}}
%\def\theproperty{\thesection.\arabic{property}}
%\newtheorem{Proposition}{Proposition}[section]
%\newenvironment{Ppn}
%{\begin{Proposition}%  
%\def\p@proposition{\theproposition} \em}%
%{\end{Proposition}}
%\newcommand{\bppn}[1]
%{{\small{\bf Proposition \ref{#1}}}}
%\newtheorem{Theorem}{Theorem}
%\mbox{\\tiny   whr}
% New commands from rel.tex
% \newcommand{\RImp}{>\Imp}
\newcommand{\RImp}{\stackrel{\mbox{\tiny  1}}{\Imp}}
% \newcommand{\rapp}{^{\verb+^+}}
\newcommand{\rapp}{^{\ \#}}
\newcommand{\zapp}{\circ}
 \newcommand{\TImp}{\stackrel{\mbox{\tiny  u}}{\Imp}}
%\newcommand{\TImp}{\Imp}
\newcommand{\ZImp}{\stackrel{\mbox{\tiny  $0$}}{\Imp}}
% \newcommand{\red}{\stackrel{\mbox{\tiny whr}}{\longrightarrow}}
\newcommand{\GImp}[1]{\stackrel{\mbox{\tiny  ${#1}$}}{\Imp}}
\renewcommand{\LImp}{\stackrel{\mbox{\tiny  $l$}}{\Imp}}
\newcommand{\prvs}{\prv_{\Sigma}}
\newcommand{\nprvs}{\nprv_{\Sigma}}
% \newcommand{\lom}{\lambda^{\omega}}
\newcommand{\lom}{\lambda}
% \newcommand{\lR}{\lambda^{\rm {small R}}}
\newcommand{\lr}{\lambda^{\mbox{\tiny   1}}}
\newcommand{\lt}{\lambda^{\mbox{\tiny   0}}}
\newcommand{\lu}{\lambda^{\mbox{\tiny   u}}}
\newcommand{\lx}{\lambda x \! . \, }
\newcommand{\PI}[2]{\Pi {#1}\!:\!{#2}.\,}
 \newcommand{\lamb}[2]{\lambda {#1}\!:\!{#2}.\,}
\newcommand{\of}[2]{{#1}\!:\!{#2}}

\newcommand{\lxa}{\lambda x\!:\! A.\,}
% \newcommand{\lc}{\lambda{{\stackrel{l}{\Imp}}}}
 \newcommand{\lc}{\lambda^{\LImp}}
\newcommand{\eset}{\emptyset}
\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
\penalty50\hskip1em\null\nobreak\hfil\squareforqed
\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}
\def\be{\beta\eta}

\newcommand{\vN}{\vec{N}}
\newcommand{\vM}{\vec{M}}

% End new commands
%\newcommand{myslide}[1]{ \begin{slide}{} \slidetitle{#1}}
\newcommand{\twoslide}[2]{ \begin{slide}{} \myslidetitle{#1}{#2}}
\newcommand{\mends}{\vfill\end{slide}}
\renewcommand{\theslide}{\arabic{slide}}
% End new commands
