deletions | additions       diff --git a/Ex3.b.tex b/Ex3.b.tex  index 5f8ea70..7df7350 100644  --- a/Ex3.b.tex  +++ b/Ex3.b.tex 
...
\subsection{I holds immediately before loop}  We are proving that: $Q \to \wp{S}{I}$. \wp{S_1}{I}$, where $S_1$ is the statement before the loop.  \begin{equation}  \begin{split}  S_1 &= S_{11}; S_{12}\\  \end{split}  \end{equation}