\newcommand{\lemmas}[2]{{\scriptsize\tt\noindent\parbox[t]{2.4in}{#1}%
\parbox[t]{3.0in}{#2}}}
\newcommand{\sidebyside}[2]{\vspace{4ex}{\tt\noindent\parbox[t]{2.5in}{#1}\hfill
                            \parbox[t]{2.5in}{#2}}}
\newcommand{\cdef}[1]{{\tt\noindent\centerline{\parbox{3.5in}{#1}}}}
\let\endcode=\endnofill
\newcommand{\cspace}{\vspace{.25in}}

\newcommand{\ignore}[1]{}

\newcommand{\caln}{{\mbox{$\cal N$}}}
\newcommand{\calw}{{\mbox{$\cal W$}}}
\newcommand{\calv}{{\mbox{$\cal V$}}}
\newcommand{\calc}{{\mbox{$\cal C$}}}
\newcommand{\calb}{{\mbox{$\cal B$}}}
\newcommand{\cale}{{\mbox{$\cal E$}}}
\newcommand{\cals}{{\mbox{$\cal S$}}}
\newcommand{\call}{{\mbox{$\cal L$}}}
\newcommand{\calm}{{\mbox{$\cal M$}}}
\newcommand{\calo}{{\mbox{$\cal O$}}}
\newcommand{\calp}{{\mbox{$\cal P$}}}
\newcommand{\calf}{{\mbox{$\cal F$}}}
\newcommand{\calg}{{\mbox{$\cal G$}}}
\newcommand{\cala}{{\mbox{$\cal A$}}}
\newcommand{\calt}{{\mbox{$\cal T$}}}
\newcommand{\calr}{{\mbox{$\cal R$}}}

\newcommand{\gb}{{\mbox{$\Gamma_{B}$}}}
\newcommand{\gbe}{{\mbox{$\Gamma_{BE}$}}}
\newcommand{\gbei}{{\mbox{$\Gamma_{BEI}$}}}
\newcommand{\gbeig}{{\mbox{$\Gamma_{BEIG}$}}}


\newcommand{\arrowb}{{\mbox{$\rightarrow_{\cal B}\;$}}}
\newcommand{\arrowe}{{\mbox{$\rightarrow_{\cal E}\;$}}}
\newcommand{\arrowc}{{\mbox{$\rightarrow_{\cal C}\;$}}}
\newcommand{\arrows}{{\mbox{$\rightarrow_{\cal S}\;$}}}
\newcommand{\arrowsf}{{\mbox{$\rightarrow_{\cal S \cal F}\;$}}}
\newcommand{\arrowsa}{{\mbox{$\rightarrow_{\cal S \cal A}\;$}}}
\newcommand{\arrowsfa}{{\mbox{$\rightarrow_{\cal S \cal F \cal A}\;$}}}
\newcommand{\arrowg}{{\mbox{$\rightarrow_{\cal G}\;$}}}
\newcommand{\arrowgf}{{\mbox{$\rightarrow_{\cal G \cal F}\;$}}}
\newcommand{\arrowga}{{\mbox{$\rightarrow_{\cal G \cal A}\;$}}}
\newcommand{\arrowgfa}{{\mbox{$\rightarrow_{\cal G \cal F \cal A}\;$}}}
\newcommand{\genrel}{{\mbox{$\rightharpoonup_{\cal G}\;$}}}



\newcommand{\pair}[2]{{\mbox{$<\!\!{#1},\;{#2}\!\!>$}}}
\newcommand{\triple}[3]{{\mbox{$<\!\!{#1},\;{#2},\;{#3}\!\!>$}}}
\newcommand{\fourtuple}[4]{{\mbox{$<\!\!{#1},\;{#2},\;{#3},\;{#4}\!\!>$}}}
\newcommand{\tuple}[1]{{\mbox{$\langle#1\rangle$}}}

\newcommand{\slink}[2]{{\mbox{$({#1}_1\:{#1}_2\:\ldots\:{#1}_k)={#2}$}}}

\newcommand{\kunion}[2]{\kappa [\mbox{union}({#1}, {#2})]}

\newcommand{\subbox}[1]{_{\mbox{\scriptsize #1}}}
\newcommand{\spb}[1]{^{\mbox{\scriptsize #1}}}

\newcommand{\aux}{\mbox{\it Aux}}
\newcommand{\taux}{\mbox{{\it Aux}$_2$}}

\newcommand{\boxx}{\mbox{\tt X}}

\newcommand{\xvard}[1]{\mbox{$x_{#1}^{\tau_{#1}}$}}
\newcommand{\xtuple}{\mbox{\tt ($x_1^{\tau_1}$ $\ldots$ $x_k^{\tau_k}$)}}
%%\newcommand{\ytuple}{\mbox{\tt ($y_1^{\sigma_1}$ $\ldots$ $y_k^{\sigma_k}$)}}
\newcommand{\extxtuple}{\mbox{\tt (($x_1$ $\tau_1$) ($x_2$ $\tau_2$) $\ldots$ ($x_k$ $\tau_k$))}}
\newcommand{\extytuple}{\mbox{\tt (($y_1$ $\tau_1$) ($y_2$ $\tau_2$) $\ldots$ ($y_k$ $\tau_k$))}}

\newcommand{\xvaru}[1]{\mbox{$x\spb{\tt#1}$}}

\newcommand{\yvard}[1]{\mbox{$y_{#1}^{\tau_{#1}}$}}
\newcommand{\ytuple}{\mbox{\tt ($y_1^{\tau_1}$ $\ldots$ $y_k^{\tau_k}$)}}

\newcommand{\yvaru}[1]{\mbox{$y\spb{\tt#1}$}}

\newcommand{\qed}{\rule{1ex}{1ex}}

\newcommand{\vdashmore}{\mbox{$\vdash$\raisebox{.3ex}{\hspace{-.4ex}$\rightarrow$}}}

\newcommand{\vdashobv}{\hbox{$\vdash$\raisebox{.3ex}{\hspace{-.6ex}$\circ$}}}

\newcommand{\vdashless}{\hbox{$\vdash$\raisebox{.3ex}{\hspace{-.17ex}\rule{.1ex}{.9ex}
\hspace{.15ex}}}}

\def\proves{\,\vdash\,}
\def\mcproves{\,\;\vdashobv\,\;}
\def\mcfproves{\,\;\vdashless\,\;}

\newcommand{\subvdash}[1]{\vdash\!\!_{#1}}
\newcommand{\subvdashbox}[1]{\vdash\!\!\!\!_{\mbox{\scriptsize #1}}}
\newcommand{\subproves}[1]{\,\;\vdash\!\!_{#1}\;\,}
\newcommand{\subprovesbox}[1]{\,\;\vdash\!\!\!\!_{\mbox{\scriptsize #1}}\;\,}
\newcommand{\subvdashobv}[1]{\vdashobv_{\!#1}}
\newcommand{\submcproves}[1]{\,\;\subvdashobv{#1}\,\;}
\newcommand{\subvdashless}[1]{\vdashless_{\!#1}}
\newcommand{\submcfproves}[1]{\,\;\subvdashless{#1}\,\;}

\newcommand{\notvdash}{\hbox{$\not\vdash$}}
\newcommand{\notvdashobv}{\hbox{$\not\vdash$\raisebox{.3ex}{\hspace{-.6ex}$\circ$}}}
\newcommand{\notvdashless}{\hbox{$\not\vdash$\raisebox{.3ex}{\hspace{-.17ex}\rule{.1ex}{.9ex}
\hspace{.15ex}}}}

\def\notproves{\,\;\notvdash\;\,}
\def\notmcproves{\,\;\notvdashobv\,\;}
\def\notmcfproves{\,\;\notvdashless\,\;}

\newcommand{\subnotproves}[1]{\hbox{$\;\,\not\vdash_{#1}\;\,$}}
\newcommand{\subnotmcproves}[1]{\,\;\notvdashobv_{#1}\,\;}
\newcommand{\subnotmcfproves}[1]{\,\;\notvdashless_{#1}\,\;}

\newcommand{\notsubproves}[1]{\hbox{$\;\,\not\vdash_{#1}\;\,$}}
\newcommand{\notsubmcproves}[1]{\,\;\notvdashobv_{#1}\,\;}
\newcommand{\notsubmcfproves}[1]{\,\;\notvdashless_{#1}\,\;}
\newcommand{\notsubvdashbox}[1]{\not\vdash\!\!_{\mbox{\scriptsize #1}}}
\newcommand{\notsubprovesbox}[1]{\,\;\not\vdash\!\!_{\mbox{\scriptsize #1}}\;\,}
\newcommand{\false}{\mbox{{\bf F}}}
\newcommand{\true}{\mbox{{\bf T}}}

%\newcommand{\clink}[3]{#1\!\!
%\raisebox{.5ex}{$\begin{array}{c} #2 \\[-1.7ex] \rightarrow \end{array}$}
%\!\!#3}

\newcommand{\clink}[3]{#1\stackrel{#2}{\rightarrow} #3}

\newcommand{\putup}[2]{\raisebox{.5ex}{$\begin{array}{c} #1 \\[-1.7ex] #2 \end{array}$}}

\def\eqrulev#1#2#3#4#5#6{{
\begin{tabbing}
#1 \hspace{.2in} \= $#2$ \\
		 \> $#3$ \\
		 \> $#4$ \\
		 \> $#5$ \\
		 \> \parbox{1.5in}{\noindent \hrule \mbox{~}} \\
		 \> $#6$
\end{tabbing}}}

\def\eqruleiv#1#2#3#4#5{{
\begin{tabbing}
#1 \hspace{.2in} \= $#2$ \\
		 \> $#3$ \\
		 \> $#4$ \\
		 \> \parbox{1.5in}{\noindent \hrule \mbox{~}} \\
		 \> $#5$
\end{tabbing}}}

\def\eqruleiii#1#2#3#4{{
\begin{tabbing}
#1 \hspace{.2in} \= $#2$ \\ 	\> $#3$ \\ 	\>
\parbox{1.5in}{\noindent \hrule \mbox{~}} \\
		 \> $#4$
\end{tabbing}}}

\def\eqruleii#1#2#3{{
\begin{tabbing}
#1 \hspace{.2in} \= $#2$ \\
		 \> \parbox{1.5in}{\noindent \hrule \mbox{}} \\
		 \> $#3$
\end{tabbing}}}

\def\eqrulei#1#2{{
\begin{tabbing}
#1 \hspace{.2in} \= $#2$ 
\end{tabbing}}}

\newcommand{\shortrulev}[8]{\begin{minipage}[t]{#1}
\begin{tabbing}
#3 \hspace{.1in} \= $#4$ \\
                 \> $#5$ \\
                 \> $#6$ \\
                 \> $#7$ \\[-.5em]
		 \> \parbox{#2}{\noindent \hrule \mbox{}} \\[-.5em]
		 \> $#8$
\end{tabbing}\end{minipage}}

\newcommand{\shortruleiv}[7]{\begin{minipage}[t]{#1}
\begin{tabbing}
#3 \hspace{.1in} \= $#4$ \\
                 \> $#5$ \\
                 \> $#6$ \\[-.5em]
		 \> \parbox{#2}{\noindent \hrule \mbox{}} \\[-.5em]
		 \> $#7$
\end{tabbing}\end{minipage}}

\newcommand{\shortruleiii}[6]{\begin{minipage}[t]{#1}
\begin{tabbing}
#3 \hspace{.1in} \= $#4$ \\
                 \> $#5$ \\[-.5em]
		 \> \parbox{#2}{\noindent \hrule \mbox{}} \\[-.5em]
		 \> $#6$ \\[-.5em]
\end{tabbing}\end{minipage}}

\newcommand{\shortruleii}[5]{\begin{minipage}[t]{#1}
\begin{tabbing}
#3 \hspace{.1in} \= $#4$ \\[-.5em]
		 \> \parbox{#2}{\noindent \hrule \mbox{}} \\[-.5em]
		 \> $#5$ \\[-.5em]
\end{tabbing}\end{minipage}}

\newcommand{\shortrulei}[3]{\begin{minipage}[t]{#1}
\begin{tabbing}
#2 \hspace{.1in} \= $#3$
\end{tabbing}\end{minipage}}


\newcommand{\bitem}{\begin{itemize} \item}

\newcommand{\eitem}{\end{itemize}}

\newcommand{\beginquote}[1]{\begin{quote}
%%\vspace{-1em}
\noindent {\bf #1}}
%\def\endquote{\end{quote}}
\newcommand{\equote}[0]{%%\vspace{-1em}
			\end{quote}}