\newtheorem{mtheorem}{Theorem}

\newcommand{\titleslide}[1]{\frametitle{} \vfill 
\centerline{\usebeamercolor[fg]{frametitle}\huge #1} 
\vfill}

\newcommand{\wiki}[1]{\href{https://en.wikipedia.org/wiki/#1}{{\small \rm \textbf(W)} {#1}}}

\newcommand{\mnl}{\\[2ex]}

\newcommand{\extradetail}{\footnotesize} % to be used within { ... }

\newcommand{\QA}[2]{\noindent\question: {#1}{\tiny\ \\[-0.5ex]\answer: {#2}}}

\newcommand{\aut}[1]{\textsf{#1}} % style for an automatically added part
\newcommand{\autosuffix}[2]{#1\aut{#2}} % automatically generated suffix
\newcommand{\listof}[1]{#1} % list of things

\newcommand{\claim}[1]{\noindent #1.\\}

\newcommand{\bunder}[1]{\underline{\textbf{#1}}}

\newcommand{\letd}[3]{\{val\ {#1}={#2};\, {#3}\}}

\newcommand{\semic}[2]{{#1} \mathop{\mathbf{;}} {#2}}
\newcommand{\ifstar}[2]{\mathbf{if(*)}\ {#1}\ \mathbf{else}\ {#2}}
\newcommand{\ifcond}[3]{\mathbf{if}\,({#1})\ {#2}\ \mathbf{else}\ {#3}}
\newcommand{\ifcondskip}[2]{\mathbf{if}\,({#1})\ {#2}}

\newcommand{\choiceop}{\mathop{\, \setlength{\fboxsep}{0.05em}\framebox[0.3em]{\phantom{i}}}\,}
\newcommand{\ndchoice}[2]{{#1} \choiceop {#2}}

\newcommand{\tr}[1]{\llbracket{#1}\rrbracket}

\newcommand{\pset}[1]{\tilde{#1}}

\newcommand{\eqq}{=^{\mbox{\scriptsize ?}}}

\newcommand{\amyrli}{\mbox{Amyli}}
\newcommand{\ZZ}{\mathbb{Z}}

\newcommand{\interp}[2]{\llbracket {#1} \rrbracket_{#2}}
\newcommand{\lstred}[1]{{\alert{\texttt{#1}}}}

\newcommand{\Formulas}{{\cal F}}
\newcommand{\Axioms}{\textsf{Ax}}
\newcommand{\Infer}{\textsf{Infer}}
\newcommand{\Conc}[1]{\textsf{Conc}({#1})}
\newcommand{\MP}{\textsf{MP}}
\newcommand{\InferDec}{\textsf{Infer}_D}
\newcommand{\BB}{\textbf{Bool}}

% LTL
\newcommand{\LTLop}[1]{\mathop{\mathbf{#1}}}
\newcommand{\Tnext}{\LTLop{next}}
\newcommand{\Tprev}{\LTLop{prev}}
\newcommand{\Tuntil}{\LTLop{until}}
\newcommand{\Tsince}{\LTLop{since}}

\newcommand{\Teventually}{\LTLop{eventually}}
\newcommand{\Tglobally}{\LTLop{globally}}


\newcommand{\ite}[3]{{#1} \mathop{\mathbf{?}} {#2} \mathop{\mathbf{:}} {#3}}
\newcommand{\globi}[1]{{gl}({#1})}
\newcommand{\loci}[1]{{loc}({#1})}
\newcommand{\postsh}{{post}^{\#}}

\newcommand{\Nat}{\mathbb{N}}
\newcommand{\eqcl}[1]{{#1}_{/{\sim}}}