deletions | additions       diff --git a/Ex3b2.tex b/Ex3b2.tex  index c356819..928c2db 100644  --- a/Ex3b2.tex  +++ b/Ex3b2.tex 
...
\subsection{I holds after each execution of the loop}  \begin{equation}  I \and \a  B \impl \to  \wp{S}{I} \\ \wp{S}{I} \Leftrightarrow \iff  \\ \wp{res:=m+res}{\wp{n:=n-1}{I}} \Leftrightarrow \iff  \\ \wp{res:=m+res}{res+(n-1)m = n_{0}m_{0}}   \end{equation}