deletions | additions       diff --git a/3b5.tex b/3b5.tex  index 01bfa36..2b827f5 100644  --- a/3b5.tex  +++ b/3b5.tex 
...
\begin{split}  & I \a B &\to& \wp{V_1 := V; S}{V < V_1}\\  \rule{2} \iff & I \a B &\to& \wp{V_1 := n}{\wp{res := res + m}{\wp{n := n - 1}{n < V_1}}}\\  \rule{1} \iff & I \a B &\to& \wp{V_1 := V}{\wp{res n}{\wp{res  := res + m}{n< n  - 1}}\\ 1 < V_1}}\\  \rule{1} \iff & I \a B &\to& \wp{V_1 := V}{n n}{n - 1  < V_1}\\  \rule{1} \iff & I \a B &\to&  n - 1}\\ 1 < n\\  \end{split}  \end{equation}