\def\assync{\ensuremath{[\negthinspace]}}
\def\kassync{\untab\untab\assync\ \ }
\def\psync{\ensuremath{\|}}
\def\quant#1{\ensuremath{\langle{#1}\rangle}}
\def\xquant#1#2#3#4{\ensuremath{\langle{#1\ } {#2}:{#3}:{#4}\rangle}}
\def\some{\ensuremath{\eta}}
\def\theone{\ensuremath{\iota}}
\def\diverge{\ensuremath{\Omega}}
\def\forever{\ensuremath{\Box}}
\def\eventually{\ensuremath{\Diamond}}
%\def\leadsto#1#2{\ensuremath{{#1}\maps{#2}}}
\def\sizeof#1{\ensuremath{|{#1}|}}

\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\pccand{\ensuremath{\text{\bf\mbox{ cand }}}}
\def\pcand{\ensuremath{\wedge}}
\def\pcor{\ensuremath{\vee}}
\def\pcimp{\ensuremath{\Rightarrow}}
\def\fp#1{\ensuremath{\mathrm{\bf FP\ }{#1}}}

\def\DEF{\ensuremath{\stackrel{\bigtriangleup}{=}}}
\def\FUNC{\keyword{funct}\ }
\def\PROG{\keyword{program}\ }
\def\ALGO{\keyword{algorithm}\ }
\def\initially{\keyword{initially}\ }
\def\assign{\keyword{assign}\ }
\def\declare{\keyword{declare}\ }
\def\NAT{\keyword{Nat}}
\def\INT{\keyword{Int}}

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

\def\szof#1{\ensuremath{\natural.#1}}

\def\divs{\ensuremath{\mid}}
\def\map{\ensuremath{\longrightarrow}}
\def\uthen{\ensuremath{\longrightarrow}}
\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}}

