\RequirePackage{amssymb,amsmath,stmaryrd,alltt,color}

\def\A#1{\mathcal{A}\left\llbracket#1\right\rrbracket}
\def\B#1{\mathcal{B}\left\llbracket#1\right\rrbracket}
\def\N#1{\mathcal{N}\left\llbracket#1\right\rrbracket}
\def\s{s\;}

\def\x{\mathtt{x}}
\def\y{\mathtt{y}}

\def\tt{\mathbf{tt}}
\def\ff{\mathbf{ff}}

\def\AND{\mathtt{\;\&\&\;}}
\def\OR{\mathtt{\;||\;}}

\newcommand{\sdowhile}[2]{\mbox{\texttt{do~}}#1\mbox{\texttt{~while~}}#2}
\def\ruleif#1{\using{\enspace\text{if }#1}}
\def\axif#1{\enspace\text{if }#1}

% Engelbert Hubbers, Annotated Programs
\input{sl1defs}
\newcommand{\pass}[2]{\left[#1\mapsto\calA{#2}\right]}
\newcommand{\smaller}[1]{{\small\textcolor{red}{#1}}}
\renewcommand{\allttsup}[1]{\begin{math}^{\textcolor{red}{#1}}\end{math}}
%\renewcommand{\allttsub}[1]{\begin{math}_{\textcolor{red}{#1}}\end{math}}
\renewcommand{\psqan}[5]{\{#1\}^{\textcolor{red}{#4}}\espace #2 \espace \{#3\}^{\textcolor{red}{#5}}}

\newcommand{\transl}[2]{\langle #1, #2\rangle}
\newcommand{\sfor}[4]{\mbox{\texttt{for~}}\sass#1#2\mbox{\texttt{~to~}}#3\mbox{\texttt{~do~}}#4}
\newcommand{\sassert}[2]{\mbox{\texttt{assert~}}#1\mbox{\texttt{~before~}}#2}
\newcommand{\sabort}{\mbox{\texttt{abort}}}

\def\rcompsos#1{[\mbox{comp}_{\mbox{\footnotesize{sos}}}^{#1}]}
\def\rasssos{[\mbox{ass}_{\mbox{\footnotesize{sos}}}]}
\def\rskipsos{[\mbox{skip}_{\mbox{\footnotesize{sos}}}]}
\def\rifsos#1{[\mbox{if}_{\mbox{\footnotesize{sos}}}^{\mbox{\footnotesize{#1}}}]}
\def\rwhilesos{[\mbox{while}_{\mbox{\footnotesize{sos}}}]}

\def\rassert{[\mbox{assert}_{\mbox{\footnotesize{sos}}}]}