\ProvidesPackage{BAN2}


\RequirePackage{amsmath}
\RequirePackage{amssymb}
\RequirePackage{latexsym}
\RequirePackage{stmaryrd}
\RequirePackage[mathscr]{euscript}

\def\leftrightarrowfill@{\arrowfill@\leftarrow\relbar\rightarrow}
\newcommand{\xleftrightarrow}[2][]{\ext@arrow 3059\leftrightarrowfill@{#1}{#2}}

\newcommand{\leftsuperscript}[3][{}]{\left.{\vphantom{#3}}^{#2\!}_{#1}#3\right.}
\newcommand{\transpose}[1]{\leftsuperscript{t}{#1}}

\newcommand{\placeholder}{\bullet}

\newcommand{\logicand}{\wedge}
\newcommand{\logicor}{\vee}

\newcommand{\inverse}[1]{{#1}^{-1}}

\newcommand{\bbZ}{\mathbb{Z}}
\newcommand{\bbN}{\mathbb{N}}
\newcommand{\bbR}{\mathbb{R}}

\newcommand{\cpob}{\mathscr{T}}
\newcommand{\cabstractions}{\mathscr{A}}

\newcommand{\solutions}[1]{\mathscr{S}(#1)}

\newcommand{\semantics}[1]{\left\llbracket\texttt{#1}\right\rrbracket}
\newcommand{\tifthenelse}[3]{%
  \textrm{if~}{#1}\textrm{~then~}{#2}\textrm{~else~}{#3}}
\newcommand{\abstr}[1]{#1^\sharp}
\newcommand{\concr}[1]{#1^\flat}
\newcommand{\proba}[1]{#1_p}
\newcommand{\closed}[1]{\mathcal{C}(#1)}

\newcommand{\lam}[1]{\lambda{#1}.}

\newcommand{\lfp}{\operatorname{lfp}}
\newcommand{\gfp}{\operatorname{gfp}}
\newcommand{\compl}[1]{{{#1}^C}}
\newcommand{\parts}[1]{\mathscr{P}(#1)}

%\newcommand{\integr}[2][]{\smallint_{#1}\,\mathrm{d}#2} 
\newcommand{\measures}[1]{\mathscr{M}_+(#1)}
\newcommand{\pmeasures}[1]{\mathscr{M}_{\leq 1}(#1)}
\newcommand{\mprod}[3][]{{{#2}\otimes^{#1}{#3}}}
\newcommand{\fmeasurables}[2]{M(#1,#2)}

\newcommand{\sothat}{\mid}
\newenvironment{fundef}[1]%
  {#1:\left|\begin{array}{l@{\,}c@{\,}l}}%
  {\end{array}\right.}

\newcommand{\expect}[1]{\mathbf{E}#1}
%\newcommand{\pr}[1]{\textrm{Pr}\left(#1\right)}

\newcommand{\restrict}[2]{#1_{|#2}}

\newcommand{\quot}[2]{\raisebox{1ex}{$#1$}\!\diagup\!\raisebox{-1ex}{$#2$}}

\newcommand{\dm}{\,\mathrm{d}}



\newlength{\symlen}
\newlength{\barlen}

\newcommand{\overstrike}[2]{\mbox{\settowidth{\symlen}{$#1$}%
        $#1$\hspace{-\symlen}$#2$}}

\settowidth{\barlen}{$|$}
\newcommand{\vbarred}[1]{\,\overstrike{\hspace{-0.25 \barlen}|}{#1}\,}

\newcommand{\sees}[2]{#1 \triangleleft #2}
\newcommand{\said}[2]{#1 \vbarred{\sim} #2}

\newcommand{\believes}[2]{#1 \vbarred{\equiv} #2}
\newcommand{\istold}[2]{#1 \triangleleft #2}
\newcommand{\possesses}[2]{#1 \ni #2}
\newcommand{\onceconveyed}[2]{#1 \vbarred{\sim} #2}

\newcommand{\fresh}[1]{\sharp(#1)}
\newcommand{\recognizable}[1]{\phi(#1)}
\newcommand{\inv}[2]{(#2={#1}^{-1})}
\newcommand{\sharedkey}[3]{#1\xleftrightarrow{#3}#2}
\newcommand{\sharedsecret}[3]{#1\xleftrightarrow{#3}#2}
\newcommand{\publickey}[2]{\stackrel{+#1}{\mapsto}#2}
\newcommand{\pluskey}[1]{+#1}
\newcommand{\minuskey}[1]{-#1}

\newcommand{\secret}[3]{#1\stackrel{#3}{\rightleftharpoons}#2}

\newcommand{\encrypt}[2]{\left\{#1\right\}_{#2}}
\newcommand{\decrypt}[2]{\left\{#1\right\}^{-1}_{#2}}
\newcommand{\encryptrev}[2]{\left\{#1\right\}_{#2^{-1}}}
\newcommand{\combine}[2]{\left\langle#1\right\rangle_{#2}}
\newcommand{\pair}[2]{(#1,#2)}

\newcommand{\jurisdiction}[2]{#1 \Mapsto #2}
\newcommand{\honestandcompetent}[1]{\jurisdiction{#1}{\believes{#1}{\star}}}
\newcommand{\leadingto}[2]{\left(#1 {\leadsto} #2\right)}
\newcommand{\noh}[1]{\star #1}

\newcommand{\applyi}[2]{#1\left(#2\right)}
\newcommand{\applyii}[3]{#1\left(#2,#3\right)}

\newcommand{\rulesep}{\hspace{1.1em}}
