\newcommand{\cF}{{\cal F}}
\newcommand{\upt}[3]{{\displaystyle 
{#1}}\atop{{\displaystyle{#2}}\atop{\displaystyle{#3}}}}
\newcommand{\fold}{{\mathit{fold}}}
\newcommand{\foldo}{\fold^{\omega}}

\newcommand{\trad}{\mathit{t}}
\newcommand{\N}{{\bf N }}
\newcommand{\sn}{\sim}
\newcommand{\skl}{\mbox{} & \mbox{}\\}
\newcommand{\ova}[3]{\displaystyle #1\over {\displaystyle{#2 \over #3}}}
\newcommand{\ptuno}[3]{{{\displaystyle {#1}} \over {#2}}{#3}}
\newcommand{\ptdue}[4]{{{\displaystyle {#1}\quad{#2}} \over {#3}}{#4}}
\newcommand{\pttre}[5]{{{\displaystyle {#1}\quad{#2}\quad{#3}} \over 
{#4}}{#5}}
\newcommand{\ptn}[5]{{{\displaystyle 
{#1}\,,\dots,\,{#2}\quad{#3}}\over{#4}}{#5}}

\newcommand{\ft}[3]{\frac{#1}{#2}{{\mbox{\tiny #3}}}}


       \newtheorem{definition}{Definition}
      \newtheorem{example}[definition]{Example}
       \newtheorem{application}[definition]{Application}
       \newtheorem{theorem}[definition]{Theorem}
       \newtheorem{exercise}[definition]{Exercise}
       \newtheorem{lemma}[definition]{Lemma}
       \newtheorem{notation}[definition]{Notation}
       \newtheorem{observation}[definition]{Observation}
       \newtheorem{proposition}[definition]{Proposition}
       \newtheorem{proposal}[definition]{Proposal}
       \newtheorem{remark}[definition]{Remark}
       \newtheorem{result}[definition]{Result}
       \newtheorem{conjecture}[definition]{Conjecture}
       \newtheorem{claim}[definition]{Claim}
       \newtheorem{assumption}[definition]{Assumption}
       \newtheorem{corollary}[definition]{Corollary}
       \makeatletter
       \renewcommand{\@begintheorem}[2]{ % not in italics
         \trivlist\item[\hskip\labelsep{\bf #1\ #2}]}
       \renewcommand{\@opargbegintheorem}[3]{\trivlist
         \item[\hskip \labelsep{\bf #1\ #2\ (#3)}]}
       \makeatother
       \newtheorem{proof}{Proof}
       \renewcommand{\theproof}{}  % no numbers on proofs


%\newcommand{\Dick}{Dyckhoff}
%\newcommand{\sn}{\sim}
\newcommand{\xn}{\overline{x_n}}
\newcommand{\xk}{\overline{x_k}}
\newcommand{\ym}{\overline{y_m}}
\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{\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{\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{\proves}{\vdash}
\newcommand{\prv}{\proves}
\newcommand{\nq}{\neq}
\newcommand{\eqd}[2] 
{#1 =_{def} #2}
\newcommand{\neqeb}[2]
 {#1 \not =_{\eta \beta} #2}	%need argument
\newcommand{\eqeb}[2] 
{#1 =_{\eta \beta} #2}
\renewcommand{\l}{\lambda}
\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{\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{\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}}
}
