%\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}
\newcommand{\all}{\forall}
\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{\vN}{\vec{N}}
\newcommand{\vM}{\vec{M}}

\newcommand{\sqless}{\sqsubseteq}
\newcommand{\mdots}{, \dots ,}
% \newcommand{\suchthat}{\mid}
\newcommand{\prv}{\vd}
\newcommand{\nq}{\neq}
 \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{\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{\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}}


% \newtheorem{Example}{Example}[section]
% \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{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}

\newcommand{\RImp}{\stackrel{\mbox{\tiny  1}}{\Imp}}
\newcommand{\rapp}{^{\ \#}}
\newcommand{\zapp}{\circ}
 \newcommand{\TImp}{\stackrel{\mbox{\tiny  u}}{\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}
% \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^{\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}


