deletions | additions       diff --git a/Ex3b2.tex b/Ex3b2.tex  index 235a85f..141d3b6 100644  --- a/Ex3b2.tex  +++ b/Ex3b2.tex 
...
\subsection{I holds after each execution of the loop}  I \and B \impl \wp{S}{I}  \wp{S}{I} \Leftrightarrow   \wp{res:=m+res}{\wp{n:=n-1}{I}} \Leftrightarrow  \wp{res:=m+res}{res+(n-1)m = n_{0}m_{0}}