% relational operators
\def\lele#1#2#3{\ensuremath{{#1}\le{#2}\le{#3}}}
\def\ltlt#1#2#3{\ensuremath{{#1}\lt{#2}\lt{#3}}}
\def\lelt#1#2#3{\ensuremath{{#1}\le{#2}\lt{#3}}}
\def\ltle#1#2#3{\ensuremath{{#1}\lt{#2}\le{#3}}}

% algorithms

\def\initially{\ensuremath{\text{\bf initially\ }}}
\def\assign{\ensuremath{\text{\bf assign\ }}}
\def\declare{\ensuremath{\text{\bf declare\ }}}
\def\Nat{\ensuremath{\text{\bf Nat}}}
\def\Int{\ensuremath{\text{\bf Int}}}
\def\progis{\ensuremath{\text{\bf is}}}
\def\Var{\ensuremath{\text{\bf Var\ }}}


\def\bb{\ensuremath{\mid\!\![}}
\def\eb{\ensuremath{]\!\!\mid}}
\def\bloop{\ensuremath{\ast\tab\mid\!\![\tab}}
\def\eloop{\ensuremath{\untab]\!\!\mid\untab}}
\def\athen{\ensuremath{\rightarrow}}


% concurrency constructs
\def\assync{\ensuremath{]\negthickspace\negthinspace[}}
\def\kassync{\untab\untab\assync\ \ }
\def\psync{\ensuremath{\|}}

\def\parbb#1#2{\ensuremath{\bb \psync\ \tab {#1}:{#2}:}}
\def\pareb{\ensuremath{\untab\eb}} 
\def\assbb#1#2{\ensuremath{\bb\assync \tab {#1}:#2:}}
\def\asseb{\ensuremath{\untab\eb}} 
\def\ifbb{\ensuremath{\text{\bf if }}}
\def\ifeb{\ensuremath{\text{\bf fi}}}
\def\ifassync{\ensuremath{\ \assync\ }}



% transition relators
\def\CO#1#2{\ensuremath{#1\ {\rm\bf co}\ #2}}
\def\invariant#1{\ensuremath{#1\ {\rm\bf invariant}}}
\def\stable#1{\ensuremath{#1\ {\rm\bf stable}}}
\def\hoare#1#2#3{\ensuremath{\{{#1}\}\ #2\ \{{#3}}}
\def\bound#1{\ensuremath{\{{\rm bound\ }#1}}
\def\progress#1{\ensuremath{\{{\rm progress\ }#1}}
\def\fp#1{\ensuremath{\mathrm{\bf FP\ }{#1}}}
\def\derivedvar{\ensuremath{\text{\bf derived variable }}}

\def\precond#1{\ensuremath{\{{\rm\bf Requires:\ }{#1}\}}}
\def\poscond#1{\ensuremath{\{{\rm\bf Ensures:\ }{#1}\}}}

% functional operators
\def\szof#1{\ensuremath{\# #1}}
\def\app#1#2{\ensuremath{{#1}+\!\!\!+{#2}}}
\def\split#1{\ensuremath{\text{split }#1}}
\def\Seq#1#2#3{\ensuremath{{#1}.{#2}..{#3}}}

% quantifiers
\def\theone{\ensuremath{\iota}}


% environments
\newtheorem{program}{Program}
\newtheorem{algorithm}{Algorithm}
\newtheorem{definition}{Definition}
\newtheorem{note}{Note}
\newtheorem{exercise}{Exercise}
\newtheorem{notation}{Notation}


\newenvironment{bxalgorithm}{
\begin{algorithm}
\ \newline
\vspace*{.2cm}   
\begin{boxedminipage}[t]{6cm}
%\begin{program}
}
{
%\end{program}
\end{boxedminipage}\end{algorithm}}

\def\proofjust#1{\ensuremath{\langle{#1}\rangle}}


\newenvironment{Proof}{\begin{proof}}
{\begin{flushright}$\Box$\end{flushright}\end{proof}}

\def\initially{\keyword{initially}\ }
\def\assign{\keyword{assign}\ }
\def\declare{\keyword{declare}\ }
