deletions | additions       diff --git a/4b5.tex b/4b5.tex  index aa418e5..96026b1 100644  --- a/4b5.tex  +++ b/4b5.tex 
...
\begin{equation}  \begin{split}  &I \a B \to  \wp{V_1 := V; S}{V < V_1}\\ \rule{2} \iff & \wp{V_{1}:=n-1}{\wp{res:=res*i}{\wp{i:=i+1}{n-i \lt V_{1}}}} \\  \rule{1} \iff & \wp{V_{1}:=n-1}{wp{res:=res*i}{n-i-1 \lt V_{1}}} \\  \rule{1} \iff & \wp{V_{1}:=n-1}{n-i-1 \lt V_{1}} \\  \rule{1} \iff & n-i-1 \lt n-i \\  \end{split}  \end{equation}  It This  is trivially true since $\forall n \in \mathbb{Z} : n - 1 < n = \T$.  It is easy to see true, meaning  that the variant decreases. \begin{equation}  \begin{split}  & I \a B \to (n-i-1 \lt n-i)  \end{split}  \end{equation}  always will be true.