Mazdak Farrokhzad edited Ex 1.tex  over 9 years ago

Commit id: 4efd034199122a313a7770f98e931f68eaa76e52

deletions | additions      

       

\newcommand{\empty}{\varnothing}  \newcommand{\wp}[2]{wp(#1, #2)}  \newcommand{\if}[2]{if(#1) \{ #2 \}}  \newcommand{\else}[2]{else(#1) \newcommand{\else}[1]{else  \{ #2 #1  \}} \newcommand{\ie}[3]{\if{#1}{#2} \else{#3}}  Given:  \begin{equation} 

\begin{equation}  \begin{split}  \wp{if(x \wp{\ie{x  < 0) \{ y 0}{y  := -x \} else \{ -x}{  y := x }, R ) }}{R}  & \iff \\ (x < 0 \to wp( y:= -x, R )) \land (0 \leq x \to wp( y:= x, R )  \end{split}  \end{equation}