\usepackage{prooftree}

\newenvironment{while}{\medskip\noindent}{\medskip}

\def\whskip{\texttt{skip}}
\def\whass#1#2{\texttt{#1 := #2}}
\def\whcomp#1#2{#1\texttt{;} #2}
\def\whif#1#2#3{\texttt{if~}#1\texttt{~then~}#2\texttt{~else~}#3}
\def\whwhile#1#2{\texttt{while~}#1\texttt{~do~}#2}

\def\whnot#1{\texttt{$\lnot$#1}}
\def\whnotp#1{\texttt{$\lnot$}(#1)}
\def\whle#1#2{\texttt{#1$\le$#2}}

\def\axjustifies{\thickness0em\justifies}
\def\trans#1#2#3{\left\langle#1,#2\right\rangle\rightarrow#3}

\def\smbox#1{\mbox{\footnotesize{#1}}}
\def\rcompns{[\mbox{comp}_{\smbox{ns}}]}
\def\rassns{[\mbox{ass}_{\smbox{ns}}]}
\def\rifttns{[\mbox{if}^{\smbox{tt}}_{\smbox{ns}}]}