deletions | additions       diff --git a/3b5.tex b/3b5.tex  index 970e932..fbe305b 100644  --- a/3b5.tex  +++ b/3b5.tex 
...
\rule{1} \iff & I \a B \to \wp{V_1 := n}{\wp{res := res + m}{n - 1 < V_1}}\\  \rule{1} \iff & I \a B \to \wp{V_1 := n}{n - 1 < V_1}\\  \rule{1} \iff & I \a B \to n - 1 < n\\  \iff & (res + nm = n_0m_0) \a (n \geq 0) \a (0 < n) &\to& \to  n - 1 < n\\ \end{split}  \end{equation}