deletions | additions       diff --git a/4b1.tex b/4b1.tex  index fe857b3..4955d7b 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}\\  \iff & Q &\to \wp{S}{I}\\  \end{split}  \end{equation}