deletions | additions       diff --git a/Ex3.b.tex b/Ex3.b.tex  index 1e01ca3..ebca41e 100644  --- a/Ex3.b.tex  +++ b/Ex3.b.tex 
...
We are proving that: $Q \to \wp{S_1}{I}$, where $S_1$ is the statement before the loop.  \begin{equation}  \begin{split}  & S_1 &= &=&  S_{11}; S_{12}\\ & S_{11} &= &=&  res := 0\\ & S_{12} &= &=&  \ie{n_0 \geq 0}{n, m := n_0, m_0}{n, m := -n_0, -m_0}\\ & Q &\to &\to&  \wp{S_1}{I}\\ \iff & Q &\to &\to&  \wp{S_{11}; S_{12}}{I}\\ \rule{2} \iff & Q &\to &\to&  \wp{S_{11}}{\wp{S_{12}}{I}}\\ \rule{3} \iff & Q &\to &\to&  \wp{res := 0}{(n_0 > 0 \to \wp{n, m := n_0, m_0}{I}) \a \\ (n_0 \leq 0 \to \wp{n, m := -n_0, -m_0}{I})}\\ \rule{1} \iff & Q &\to &\to&  \wp{res := 0}{(n_0 > 0 \to (res + n_0m_0 = n_0m_0) \a n_0 \geq 0) \a \\ (n_0 \leq 0 \to (res + n_0m_0 = n_0m_0) \a -n_0 \geq 0)}\\ \rule{1} \iff & Q &\to &\to&  (n_0 > 0 \to (n_0m_0 = n_0m_0) \a n_0 \geq 0) \a\\ & & &  (n_0 \leq 0 \to (n_0m_0 = n_0m_0) \a -n_0 \geq 0)\\ \end{split}  \end{equation}