Mazdak Farrokhzad edited Rules.tex  over 9 years ago

Commit id: b760c9206747f0c4d32716f528c222ec296d1c21

deletions | additions      

       

\newcommand{\else}[1]{else \ \{ #1 \}}  \newcommand{\ie}[3]{\if{#1}{#2} \ \else{#3}}  \newcommand{\a}[0]{\ \land \ }  \newcommand{\mtt}[1]{\mathttt{#1}}  \newcommand{\mbb}[1]{\mathbf{#1}}  \newcommand{\T}[0]{\mbb{\top}}  \newcommand{\F}[0]{\mbb{\bot}} 

\begin{split}  \wp{x :=e}{R} &= R[x \mapsto e]\\  \wp{S1; S2}{R} &= \wp{S1}{\wp{S2}{R}}\\  \wp{\mbb{assert \wp{\mtt{assert  }B}{R} &= B \a R\\ \end{split}  \end{equation}