deletions | additions       diff --git a/4b2.tex b/4b2.tex  index 0bb4536..0376729 100644  --- a/4b2.tex  +++ b/4b2.tex 
...
\begin{equation}  \begin{split}  & I \a B &\to& wp{S}{I}\\  & I \a B &\to& wp{res := res * i; i := i + 1}{I}\\  \rule{2} \iff & \I \a B &\to& wp{res := res * i, \wp{i := i + 1}{I}}\\  \rule{1} \iff & \I \a B &\to& wp{res := res * i, (i + 1 \leq n + 1) \a (res = i!)}\\  \rule{1} \iff & \I \a B &\to& (i + 1 \leq n + 1) \a (res * i = i!)}\\  \end{split}  \end{equation}