%\def\ss{}
\def\pal{{\rm PAL}}
\def\rev #1{{\bf rev}\, #1}
%\def\subst#1#2#3{#1[#2/#3]}
\def\startx{\ensuremath{\mathtt{start}_x}}
\def\acceptx{\ensuremath{\mathtt{accept}_x}}
\def\rejectx{\ensuremath{\mathtt{reject}_x}}
\def\start{\ensuremath{\mathtt{start}}}
\def\accept{\ensuremath{\mathtt{accept}}}
\def\reject{\ensuremath{\mathtt{reject}}}
%\def\acceptx{Y^+}
%\def\rejectx{Y^-}
\def\type{{\bf type}}
\def\ellstar{\ell_{\textstyle *}}
\def\subsneq{\subsetneqq}
\def\AL{{\it ALOGSPACE}}
\def\AP{{\it APTIME}}
\def\PTIME{{\it PTIME}}
\def\AE{{\it AEXPTIME}}
\def\SAV{{\rm SAV}}
\def\EXACTSAV{{\rm EXACTSAV}}
\def\PARSAV{{\rm PARSAV}}
\def\sqeq{\sqsubseteq}
\def\rev#1{{\bf rev}\:#1}
\def\MAZE{{\rm MAZE}}
\def\SAT{{\rm SAT}}
\def\CVP{{\rm CVP}}
\def\RP{{\it RP}}
\def\BPP{{\it BPP}}
\def\checkmate{\m{\sc checkmate}}
\def\force{\m{\sc force}}
\def\boards{\m{\sc boards}}
\def\move{\m{\sc move}}
\def\win{\m{\sc win}}
\def\Prob#1#2{{\rm Pr}_{#1}(\m{#2})}
\def\Pr#1{{\rm Pr}(#1)}
\def\CPr#1#2{{\rm Pr}_{\rm opt}(#1 \mid #2)}
\def\Popt{P_{\rm opt}}
\def\Propt{{\rm Pr}_{\rm opt}}
\def\acc{m_N=1}
\newcommand\powerset[1]{2^{#1}}
\newcommand\lbl[1]{\label{#1}}
\newcommand\Ord{{\bf Ord}}
\def\ms#1{{\m{\scriptsize #1}}}
\def\APSPACE{{\it APSPACE}}
\def\R{R}
\def\ifthengoto#1#2{\textbf{if}\ #1\ \textbf{then goto}\ #2}
\def\goto#1{\textbf{goto}\ #1}

\newlength\alength
\newlength\mylength
\settowidth\alength{$a$}
\def\my#1{\settowidth\mylength{$#1$}\parbox[b]{\mylength}{$#1$}}
\def\fix#1{\parbox[b]{\alength}{$#1$}}

\def\Th#1{{\bf Th}(#1)}
\def\Mod#1{{\bf Mod}(#1)}
\def\ttdet#1{\begin{array}{|cc|}#1&#1'\\a_{k+1}&a_{k+1}'\end{array}}
\def\axok{a_1x_1+\cdots+a_kx_k+b}
\def\ayok{a_1y_1+\cdots+a_ky_k+b}
\def\sign#1{{\bf sign\ }#1}
\def\size#1{\makebox[6pt][l]{$\parallel$}#1\makebox[6pt][r]{$\parallel$}}
\def\next#1{\rho(#1)}
\def\signs{\{-1,0,1\}}
\def\A#1#2{A_{\m{\scriptsize $#2$}}^{#1}}
\def\eq#1#2{\equiv^{#1}_{\m{\scriptsize $#2$}}}
\newcommand{\lapprox}{\raisebox{-.6ex}{$\;\stackrel{{\textstyle <}}{\sim}\;$}}
\newcommand{\EEapprox}{\EE/\!\!\approx}
\newcommand{\DDequiv}{\DD/\!\equiv}
\newcommand{\EEequiv}{\EE/\!\equiv}
\def\PFP#1{\m{\sc pfp}(#1)}
\def\FP#1{\m{\sc fp}(#1)}
\def\PFPx#1#2{\m{\sc pfp}(#1,#2)}
\def\FPx#1#2{\m{\sc fp}(#1,#2)}

\def\QBF{{\rm QBF}}
\def\MULT{\m{\sc mult}}
\def\INTDIV{\m{\sc intdiv}}
\def\DIV{\m{\sc div}}
\def\REM{\m{\sc rem}}
\def\EVEN{\m{\sc even}}
\def\ODD{\m{\sc odd}}
\def\PRIME{\m{\sc prime}}
\def\POWER2{\m{\sc power2}}
\def\BIT{\m{\sc bit}}
\def\ttn{2^{2^n}}
\def\tttn{2^{2^{2^n}}}
\def\ttno{2^{2^{n+1}}}
\def\ttnmo{2^{2^{n-1}}}
\def\tttnmo{2^{2^{2^{n-1}}}}
\def\ThRA{\m{$\Th{\reals,+,\leq}$}}
\def\ThZ{\m{$\Th{\integers,+,\leq}$}}
\def\elln{\ell_n}
\def\sos{{\sf S1S}}
\def\io#1{{\rm IO}(#1)}
\def\succ{{\mathbf{s}\kern1pt}}

\boxlength=\textwidth
\addtolength{\boxlength}{-2cm}
\def\codebox#1{
\makebox[\boxlength][l]{\hspace{1cm}\begin{minipage}{\boxlength}
\begin{tabbing}
\hspace{2ex} \= \hspace{2ex} \= \hspace{2ex} \= \hspace{2ex} \= \hspace{2ex} \= \kill
#1
\end{tabbing}
\end{minipage}}
}

\def\return#1{\m{\bf return\rm (#1)}}
%\def\const{{\bf const}}
%\def\comp{{\bf comp}}
%\def\pair{{\bf pair}}
\newcommand\Comp{\mathsf{comp}}
\newcommand\Const{\mathsf{const}}
\newcommand\Pair{\mathsf{pair}}
\def\HP{{\rm HP}}
\def\MP{{\rm MP}}
\def\EMPTY{{\rm EMPTY}}
\def\TOTAL{{\rm TOTAL}}
\def\ALL{{\rm ALL}}
\def\FIN{{\rm FIN}}
\def\COF{{\rm COF}}
\def\ltT{<_{\rm T}}

\def\NPSPACE{{\it NPSPACE}}
\def\APTIME{{\it APTIME}}
\def\E{{\it EXPTIME}}
\def\NE{{\it NEXPTIME}}
\def\ESPACE{{\it EXPSPACE}}
\def\NESPACE{{\it NEXPSPACE}}
\def\leqm{\leq_{\rm m}}
\def\leqT{\leq_{\rm T}}
\def\equivm{\equiv_{\rm m}}
\def\equivT{\equiv_{\rm T}}
\def\leqlm{\leq^{\rm log}_{\rm m}}
\def\leqpm{\leq^{\rm p}_{\rm m}}
\def\blank{{\llcorner\hspace{-4pt}\lrcorner}}
\def\nsubs{\,\nsubseteq\,}

\def\SigmaP#1{\Sigma^{\mathrm p}_{#1}}
\def\PiP#1{\Pi^{\mathrm p}_{#1}}
\def\DeltaP#1{\Delta^{\mathrm p}_{#1}}
\def\coNL{co-\textit{NLOGSPACE}}

%from kozenau.sty

\makeatletter

\def\division#1{\cleardoublepage      % Starts new page.
   \thispagestyle{empty}     % Page style of chapter page is 'plain'
   \global\@topnum\z@        % Prevents figures from going at top of page.
   \@afterindentfalse        % Suppresses indent in first paragraph. Change
%   \secdef\@chapter\@schapter
{\mbox{\ }\vspace{2in}\huge\bf #1}
\addcontentsline{toc}{chapter}{\protect #1}
}   % to \@afterindenttrue to have indent.

\newcounter{tmp}
\newcounter{lecture}
\setcounter{lecture}0
\newcounter{supplecture}
\setcounter{supplecture}0
\def\thelecture{\arabic{lecture}}
\def\thesupplecture{\Alph{supplecture}}

\def\@lecture#1#2#3#4{
	\clearpage
	\refstepcounter{#3}
	\def\thesection{#4}
	\def\thefigure{\thesection.\@arabic\c@figure}
	{\mbox{}\vspace{12pc}
		\raggedright\section*{#2 \thesection\\[1pc]#1}
		\begin{center}\mbox{}\end{center}}
	\markboth{#2 \thesection}{#1}
	\addcontentsline{toc}{section}{\protect\numberline{\thesection}#1}
	\setcounter{equation}0
	\setcounter{theorem}0
	\setcounter{footnote}0
	\thispagestyle{empty}}
\def\lecture#1{\@lecture{#1}{Lecture}{lecture}{\thelecture}}
\def\supplecture#1{\@lecture{#1}{Supplementary Lecture}{supplecture}{\thesupplecture}}
\def\solutionsname{}
\def\homework{\clearpage
	\setcounter{tmp}{\value{section}}
	\def\thesection{Homework \arabic{section}\solutionsname}
	{\section{}}
%        \markboth{Homework \arabic{section}}{Homework \arabic{section}}
	\def\thesection{\arabic{section}}
	\setcounter{section}{\value{tmp}}
	\refstepcounter{section}
\thispagestyle{headings}
	}
\def\mysection#1{
        \def\thesection{#1}
	{\mbox{}\vspace{12pc}
		\raggedright\section*{\thechapter\\[1pc]\thesection}
		\begin{center}\mbox{}\end{center}}
	\markright{\thesection}
	\addcontentsline{toc}{section}{\protect\numberline{\thesection}}
	\thispagestyle{empty}}

\newlength\glossarywidth
\newcommand\glossaryentry[3]{\settowidth\glossarywidth{#3}\item[]\makebox[22mm][l]{#1}#2\dotfill\makebox[\glossarywidth][r]{#3}}

\newcommand\frA{{\mathfrak A}}
\def\omegack{\omega_1^{\mathrm{ck}}}

\newcommand\THEN{{\bf then}}
\newcommand\ELSE{{\bf else}}
\newcommand\HKA{$H({\rm KA})$}
\newcommand\HKAs{$H({\rm KA}\star)$}
%\newcommand\barnone{\bar{\rule{0mm}{1ex}\hspace{1ex}}} moved to dkdefs.sty
\newcommand{\ldb}{[\![} %% left double brace
\newcommand{\rdb}{]\!]} %% right double brace
\newcommand{\bbfn}{\fam\msyfam}
\newcommand{\term}[1]{{\em #1}}
\newcommand{\GSSB}{{{\rm GS}_{\Sigma,\Bool}}} %% Guarded Strings
\newcommand{\GS}{{\rm GS}} %% Guarded Strings
\newcommand{\G}{G} %% Standard interpretation of GS
\newcommand{\GSB}{{{\cal G}_{\Sigma,\Bool}}} %% Guarded String model
\newcommand{\gsone}{{1_{\GG}}}
\newcommand{\gsdot} {\diamond}
\newcommand{\Union}{\bigcup}
\newcommand{\univ}{\top}
\newcommand{\TSB}{T_{\Sigma,\Bool}}
\newcommand{\RSB}{R_{\Sigma,\Bool}}
\newcommand{\TB}{T_{\Bool}}
\newcommand{\K}{{\cal K}}
\newcommand{\M}{{\cal M}}
\newcommand{\F}{{\cal F}}
\newcommand{\PSB}{{\cal P}_{\Sigma,\Bool}}
\newcommand{\id}{\iota}
\newcommand{\Bool}{{\sf B}}
\newcommand{\KA}{\ensuremath{\mathsf{KA}}}
\newcommand{\KAT}{\ensuremath{\mathsf{KAT}}}
\newcommand{\SKAT}{\ensuremath{\mathsf{SKAT}}}
\newcommand{\ka}{Kleene algebra}
\newcommand{\kat}{Kleene algebra with tests}
\newcommand{\KAS}{\ensuremath{\mathsf{KA}\star}}
\newcommand{\KATS}{\ensuremath{\mathsf{KAT}\star}}
\newcommand{\REL}{\ensuremath{\mathsf{REL}}}
\newcommand\PHL{\ensuremath{\mathsf{PHL}}}
\newcommand\DL{\ensuremath{\mathsf{DL}}}
\newcommand{\PDL}{\ensuremath{\mathsf{PDL}}}
\newcommand\PCA{\m{PCA}}
\newcommand\Diag{\Delta}
\newcommand\RS{R_\Sigma}
\newcommand\FS{\FF_\Sigma}
\newcommand\PPQ{\PP(Q)}
\newcommand{\NFA}{{\em NFA}}
\newcommand\Mat[2]{\ensuremath{\mathrm{Mat}(#1,#2)}}
\renewcommand\matrix[4]{
\left[\begin{array}{c|c}
#1 & #2\\ \hline
#3 & #4
\end{array}\right]
}
\def\aps#1{\alpha_0 p_1 \alpha_1 \cdots \alpha_{#1-1} p_{#1} \alpha_{#1}}
\def\JAs#1{J_{\alpha_0}\star A_{p_1} J_{\alpha_1}\star\cdots J_{\alpha_{#1-1}}\star A_{p_{#1}} J_{\alpha_{#1}}\star}
\def\KBs#1{K_{\alpha_0}\star B_{p_1} K_{\alpha_1}\star\cdots K_{\alpha_{#1-1}}\star B_{p_{#1}} K_{\alpha_{#1}}\star}

\newcommand\unique[3]{U_{#1 #2}(#3)}
\newcommand\pretype[1]{\mathsf{#1}}
\newcommand\tpn[2]{#1\imp #2}
\newcommand\tp[2]{\tpn{\pretype{#1}}{\pretype{#2}}}
\newcommand\umg[1]{{\mathfrak m}_{#1}} 
\newcommand\mg[1]{\umg{\mathfrak #1}}
\newcommand\uMg[2]{\umg{#1}(#2)}
\newcommand\Mg[2]{\mg{#1}(#2)}
\newcommand\frK{{\mathfrak K}}
\newcommand\RExpS{\ensuremath{\mathsf{RExp}_\Sigma}}
\newcommand\RegS{\ensuremath{\mathsf{Reg}_\Sigma}}
\newcommand\SA{\ensuremath{\mathsf{SA}}}
\newcommand\RA{\ensuremath{\mathsf{RA}}}
\newcommand\CS{\ensuremath{\mathsf{CS}}}
\newcommand\BC{\ensuremath{\mathsf{C}}}
\newcommand\BS{\ensuremath{\mathsf{S}}}
\newcommand\BK{\ensuremath{\mathsf{K}}}
\newcommand\BG{\ensuremath{\mathsf{G}}}
\newcommand\BN{\ensuremath{\mathsf{N}}}
\newcommand\BR{\ensuremath{\mathsf{R}}}
\newcommand\supp[1]{\mathsf{supp}\:#1}%
\newcommand\Eq[1]{\cal{E}(#1)}%

\def\Reg#1{\Regname\: #1}
\def\Regname{\ensuremath{\mathsf{Reg}}}
\def\Mon{\ensuremath{\mathsf{Mon}}}
\def\MON{\ensuremath{\mathsf{Mon}}}
\def\powerset#1{2^{#1}}
\def\WF{{\sf WF}}
\def\HTh#1{\HH\: #1}
\def\ETh#1{\EE\: #1}
\def\closure#1{\bar{#1}}
\def\le{\vdash}
\def\re{\dashv}
\def\bracket#1{\,\le\! #1\!\re\,}
\def\ostar{^\circledast}
\def\on{^n}
\def\circled#1{%
\begin{picture}(10,0)(-5,0)%
\put(0,3){\makebox(0,0){#1}}%
\put(0,3){\circle{12}}%
\end{picture}%
}%

\def\theequation{\arabic{equation}}

\newcommand\GF[1]{\mathbb{GF}_{#1}}
\newcommand\acGF[1]{\bar{\mathbb{GF}}_{#1}}
\newcommand\Res{\mathsf{Res}}
\newcommand\primes{\m{\textsc{primes}}}
\newcommand\ord[1]{\mathrm{order}\:#1}

