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

\def\xset#1{\ensuremath{\{#1\}}}
\def\xpair#1#2{\ensuremath{<#1,#2>}}

% quantifier
\def\bnd#1#2#3#4{\ensuremath{{#1}{#2}:{#3}:{#4}}}
\def\sumbnd#1#2#3{\bnd{\sum}{#1}{#2}{#3}}
\def\allbnd#1#2#3{\bnd{\forall}{#1}{#2}{#3}}
\def\exbnd#1#2#3{\bnd{\exists}{#1}{#2}{#3}}
\def\minbnd#1#2#3{\bnd{\uparrow}{#1}{#2}{#3}}
\def\maxbnd#1#2#3{\bnd{\downarrow}{#1}{#2}{#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\be{\ensuremath{]\!\!\mid}}
\def\athen{\ensuremath{\rightarrow}}


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

\def\parbnd#1#2#3{\ensuremath{\bb \bnd{\psync}{#1}{#2}{#3}\be}}
\def\parbb#1#2{\ensuremath{\bb\psync\ \tab {#1}:{#2}:}}
\def\pareb{\ensuremath{\untab\be}} 
\def\ifbb{\ensuremath{\text{\bf if }}}
\def\ifeb{\ensuremath{\text{\bf fi}}}
\def\ifbnd#1#2#3{\ensuremath{\text{\bf if }\bnd{\assync}{#1}{#2}{#3}\text{\bf\, fi}}}
\def\ifbb#1#2{\ensuremath{\text{\bf if }\assync \tab {#1}:#2:}}
\def\ifeb{\ensuremath{\untab\text{\bf fi}}} 
\def\dobnd#1#2#3{\ensuremath{\text{\bf do }\bnd{\assync}{#1}{#2}{#3}\text{\bf\, od}}}
\def\dobb#1#2{\ensuremath{\text{\bf do }\assync \tab {#1}:#2:}}
\def\doeb{\ensuremath{\untab\text{\bf od}}} 
\def\barrier#1#2{\ensuremath{({#1}\athen {#2})}}
\def\parmap#1#2{\ensuremath{\text{\bf parmap }{#1}{#2}}}
\def\seqalter#1#2{\ensuremath{#1\leftarrow #2}}


% 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}}



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

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