deletions | additions       diff --git a/Ex2.tex b/Ex2.tex  new file mode 100644  index 0000000..af9e724  --- /dev/null  +++ b/Ex2.tex 
...
\newcommand{\empty}{\varnothing}  \newcommand{\wp}[2]{wp\left(#1, #2\right)}  \newcommand{\if}[2]{if\left(#1\right) \ \{ #2 \}}  \newcommand{\else}[1]{else \ \{ #1 \}}  \newcommand{\ie}[3]{\if{#1}{#2} \ \else{#3}}  \newcommand{\a}[0]{\ \land \ }  \newcommand{\mtt}[1]{\text{#1}}  \newcommand{\mbb}[1]{\mathbf{#1}}  \newcommand{\T}[0]{\mbb{\top}}  \newcommand{\F}[0]{\mbb{\bot}}  \newcommand{\rule}[1]{\ (\mbb{§#1})}  \section{Ex2}  Given:  \begin{equation}  \begin{split}  Q &= x \neq y\\  R &= big > small  \end{split}  \end{equation}  Then:  \begin{equation}  \begin{split}  & \wp{\ie{x < 0}{y := -x}{ y := x }}{R} \\  \rule{4} \iff & \left(x < 0 \to \wp{y:= -x}{R}\right) \a \left(0 \leq x \to \wp{y:= x}{R}\right)\\  \rule{1} \iff & (x < 0 \to (0 \leq -x \a (0 \leq x \to -x = x) \a (x < 0 \to -x = -x )))\\  \land & (x \leq 0 \to (0 \leq x \a (0 \leq x \to x = x) \a (x < 0 \to x = -x)))\\  \iff & (x < 0 \to -x = -x) \a (0 \leq x \to x = x)\\  \iff & \T\\  \end{split}  \end{equation}  Therefore:  \begin{equation}  \begin{split}Q \implies& \T  \end{split}  \end{equation}  In other words, the post condition holds for all possible pre conditions.