deletions | additions       diff --git a/Ex3.b.tex b/Ex3.b.tex  index b4a774d..5f8ea70 100644  --- a/Ex3.b.tex  +++ b/Ex3.b.tex 
...
\end{split}  \end{equation}  Then:  \begin{equation}  \begin{split}  & \wp{\ie{x > y}{big, small := x, y}{big, small := y, x}}{R} \\  \rule{4} \iff & (x > y \to \wp{big, small := x, y}{R}) \a (x \leq y \to \wp{big, small := y, x}{R})\\  \rule{1} \iff & (x > y \to x > y) \a (x \leq y \to x < y)\\  \iff & x \leq y \to x < y \\  \end{split}  \end{equation} \subsection{I holds immediately before loop}  We are proving that: $Q \to \wp{S}{I}$.  This is not true for all $x, y \in \mathbb{Z}$, specifically when $x = y$.  Therefore:  \begin{equation}  \begin{split}Q &= x \neq y\\ \begin{split}  \end{split}  \end{equation}