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