\documentclass[10pt]{article}
\usepackage{dkdefs,kleene,ags,amssymb}
\usepackage{proof}

\newcommand{\RExpPB}{\ensuremath{\mathsf{RExp}_{\mathsf{P,B}}}}
\newcommand\Rel[1]{\ensuremath{\mathsf{Rel}_{#1}}}
\newcommand\Tr[1]{\ensuremath{\mathsf{Tr}_{#1}}}
\newcommand\Traces[1]{\ensuremath{\mathsf{Traces}_{#1}}}
\newcommand\BoolB{\ensuremath{\mathsf{Bool}_\Bool}}
\newcommand\Atoms{\ensuremath{\mathsf{Atoms}_\Bool}}
\newcommand\Ext[1]{\ensuremath{\mathsf{Ext}(#1)}}
\renewcommand\GddStr{\Traces G}
\newcommand\N[2]{N_{#1}(#2)}
\newcommand\rewrite{\rhd}
\newcommand\KATML{\ensuremath{\mathsf{KAT\hyphen ML}}}
\newcommand\textbsf[1]{\textsf{\textsf{#1}}}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollarj}[theorem]{Corollarj}
\newtheorem{definition}{Definition}