deletions | additions       diff --git a/4b1.tex b/4b1.tex  index 4955d7b..c53dc21 100644  --- a/4b1.tex  +++ b/4b1.tex 
...
We are proving that: $Q \to \wp{S_1}{I}$, where $S_1$ is the statement before the loop.  \begin{equation}  \begin{split}  & Q &\to \wp{S}{I}\\ \wp{S_1}{I}\\  \iff & Q &\to \wp{S}{I}\\ \wp{res, i := res * i, i + 1}{(i \leq n + 1) \a (res = (i - 1)!)}\\  \rule{1} \iff & Q &\to \wp{res, i := res * i, i + 1}{(i \leq n + 1) \a (res = (i - 1)!)}\\  \iff & Q &\to (2 \leq n + 1) \a (1 = 1!)}\\  \iff & n > 0 &\to 2 \leq n + 1}\\  \end{split}  \end{equation}