deletions | additions       diff --git a/Ex3b2.tex b/Ex3b2.tex  index 928c2db..4b6a297 100644  --- a/Ex3b2.tex  +++ b/Ex3b2.tex 
...
\newcommand{\rule}[1]{\ (\mbb{§#1})}  \subsection{I holds after each execution of the loop}  We shall prove that $I \a B \to \wp{S}{I}$  \begin{equation}  I \a B \to \begin{split}  &  \wp{S}{I} \\\wp{S}{I}  \iff & \wp{res:=m+res;n:=n-1}{I}  \\ \wp{res:=m+res}{\wp{n:=n-1}{I}} \rule{2}  \iff & \wp{res:=m+res}{\wp{n:=n-1}{I}}  \\ \rule{1} \iff &  \wp{res:=m+res}{res+(n-1)m = n_{0}m_{0}} n_{0}m_{0} \a n \geq 0} \\  \iff & m+res+(n-1)m=n_{0}m_{0} \a n \geq 0 \\  \iff & res+nm=n_{0}m_{0} \a n \geq 0  \end{split}  \end{equation}  We end up with the implication:  \begin{equation}  \begin{split}  (res+nm=n_{0}m_{0} \a n \geq 0 \a 0 \lt n) \to res+nm=n_{0}m_{0} \a n \geq 0  \end{split}  \end{equation} which is trivially true since the right hand side of the implication is a conjunct in  the left hand side of the implication.