%\newcommand{\Dick}{Dyckhoff}
%\newcommand{\snot}{\sim}
\newcommand{\ex}{\exists}
\newcommand{\all}{\forall}
\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{\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}
\def\vd{\null\mathrel{\vdash}} %Frank's
\def\nprv{\null\mathrel{\not\vdash}} %Frank's
\newcommand{\prv}{\vd}
% \newcommand{\proves}{\vdash}
% \newcommand{\prv}{\proves}
\newcommand{\nq}{\neq}
% \newcommand{\eqd}[2] 
% {#1 =_{def} #2}
% \newcommand{\neqeb}[2]
%  {#1 \not =_{\beta\eta} #2}	%need argument
% \newcommand{\eqeb}[2] 
% {#1 =_{\beta\eta}  #2}
\newcommand{\nebe}{\not =_{\beta\eta}}	% do not need argument
\newcommand{\ebe}{=_{\beta\eta}}

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

\newcommand{\lll}{{$L_{\l}$}}
\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{\cB}{{\cal B}}
\newcommand{\cQ}{{\cal Q}}
\newcommand{\cP}{{\cal P}}
\newcommand{\mnot}{{\rm Not}}
\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{Definition}}
\newcommand{\enef}{\end{Definition}}
\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]
\newtheorem{Definition}{Definition}[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}}
\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}

% New commands from rel.tex
% \newcommand{\RImp}{>\Imp}
\newcommand{\RImp}{\stackrel{1}{\Imp}}
% \newcommand{\rapp}{^{\verb+^+}}
\newcommand{\rapp}{^{\ \#}}
\newcommand{\zapp}{\circ}
% \newcommand{\TImp}{\stackrel{\top}{\Imp}}
\newcommand{\TImp}{\Imp}
\newcommand{\ZImp}{\stackrel{0}{\Imp}}
\newcommand{\prvs}{\prv_{\Sigma}}
% \newcommand{\lom}{\lambda^{\omega}}
\newcommand{\lom}{\lambda}
% \newcommand{\lR}{\lambda^{\rm {small R}}}
\newcommand{\lr}{\lambda^{1}}
\newcommand{\lt}{\lambda^{0}}
\newcommand{\lu}{\lambda^{u}}
\newcommand{\lx}{\lambda x  . \, }
\newcommand{\lc}{\lambda{{\stackrel{l}{\Imp}}}}
\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{\lam}[2]{\lambda {#1}\!:\!{#2}.\,}
\newcommand{\PI}[2]{\Pi {#1}\!:\!{#2}.\,}
% example \PI{x}{A} K  
% End new commands
