deletions | additions       diff --git a/Rules.tex b/Rules.tex  index 8308c23..6a8901c 100644  --- a/Rules.tex  +++ b/Rules.tex 
...
\wp{\ie{B}{S1}{S2}}{R} &= B \to \wp{S1}{R} \a \neg B \to \wp{S2}{R} && \rule{4}\\  \wp{\if{B}{S1}}{R} &= B \to \wp{S1}{R} \a \neg B \to R && \rule{5}\\  \end{split}  \end{equation}  Variable names:  \begin{equation}  \begin{split}  Q &: \text{Precondition}\\  R &: \text{Postcondition}\\  I &: \text{Loop invariant}\\  B &: \text{Loop branch condition}\\  V &: \text{Loop variant}\\  S &: \text{Statement inside loop}\\  \end{split}  \end{equation}