Small part of loop invariant i'm not getting

Question

Show that $y = \frac{1}{2} \cdot z \cdot (z + 1)$ is a loop invariant for the following WHILE loop:

y := 0; z := 0 WHILE $\neg$(z = x) DO z := z + 1; y := y + z

In other words, proof that
$\{y = \frac{1}{2} \cdot z \cdot (z + 1)\}$
z := z + 1;
y := y + z
$ \{y = \frac{1}{2} \cdot z \cdot (z + 1)\}$

Used for this are the Hoare axioms:

H1 {[$t$\x]$\varphi$} x := $t$ {$\varphi$}, provided that $t$ is free for $x$ in $\varphi$
H2 from {$\varphi$} $\pi_1$ {$\psi$} and {$\psi$} $\pi_2$ {$\chi$} follows {$\varphi$} ($\pi_1;\pi_2$) {$\chi$}
H3 from {$\varphi \wedge \epsilon$} $\pi_1$ {$\psi$} and {$\varphi \wedge \neg \epsilon$} $\pi_2$ {$\psi$} follows {$\varphi$} IF $\epsilon$ THEN $\pi_1$ ELSE $\pi_2$ {$\psi$}
H4 from {$\varphi \wedge \epsilon$} $\pi$ {$\varphi$} follows {$\varphi$} WHILE $\epsilon$ DO $\pi$ {$\neg \epsilon \wedge \varphi$}
H5 if $\varphi \rightarrow \varphi`$ and $\psi \rightarrow \psi`$ are true in M = (D, I), then: from {$\varphi`$} $\pi$ {$\psi`$} follows {$\varphi$} $\pi$ {$\psi$}

1 {$y + z = \frac{1}{2} \cdot z \cdot (z + 1)$}  y := y + z  {$y = \frac{1}{2} \cdot z \cdot (z + 1)$}   H1

2 {$y + (z + 1) = \frac{1}{2} \cdot (z + 1) \cdot ((z + 1) + 1)$}  z := z + 1   {$y + z = \frac{1}{2} \cdot z \cdot (z + 1)$}   H1

3 {$y + (z + 1) = \frac{1}{2} \cdot (z + 1) \cdot (z + 2)$}
    z := z + 1
   {$y + z = \frac{1}{2} \cdot z \cdot (z + 1)$}   H5, 2

4 {$y + (z + 1) = \frac{1}{2} \cdot (z + 1) \cdot (z + 2)$}
    z := z + 1; y := y + z
    {$y = \frac{1}{2} \cdot z \cdot (z + 1)$}   H2, 3, 1

5 {$y = \frac{1}{2} \cdot z \cdot (z + 1)$}
   z := z + 1; y := y + z
   {$y = \frac{1}{2} \cdot z \cdot (z + 1)$}   H5, 4*

*This application of H5 is correct because: $y + (z + 1)$
$= \frac{1}{2} \cdot (z + 1) \cdot (z + 2)$
$= \frac{1}{2} \cdot z \cdot (z + 1) + \frac{1}{2} \cdot 2 \cdot (z + 1)$
$= \frac{1}{2} \cdot z \cdot (z + 1) + (z + 1)$

So the precondition in stap 3 is equivalent with $y = \frac{1}{2} \cdot z \cdot (z + 1)$.

It's this last part I'm not getting at all; how is the precondition {$y + (z + 1) = \frac{1}{2} \cdot (z + 1) \cdot (z + 2)$} equivalent with $y = \frac{1}{2} \cdot z \cdot (z + 1)$? What happens in this here equation that shows us that this is correct?

$y + (z + 1)$
$= \frac{1}{2} \cdot (z + 1) \cdot (z + 2)$
$= \frac{1}{2} \cdot z \cdot (z + 1) + \frac{1}{2} \cdot 2 \cdot (z + 1)$
$= \frac{1}{2} \cdot z \cdot (z + 1) + (z + 1)$

Answer 1

I'm not sure to understand your question ...

If we have :

$y = \frac{1}{2} \cdot z \cdot (z + 1)$

then, adding $(z+1)$ to both sides, we get :

$y +(z + 1) = \frac{1}{2} \cdot z \cdot (z + 1) + (z+1) = \frac{1}{2}[ z \cdot (z + 1) + 2 \cdot (z+1)] = \frac{1}{2}[ (z + 2) \cdot (z+1)] $;

it's all ...

In your calculation you have :

$y + (z + 1)$
$= \frac{1}{2} \cdot (z + 1) \cdot (z + 2)$
$= \frac{1}{2} \cdot z \cdot (z + 1) + \frac{1}{2} \cdot 2 \cdot (z + 1)$
$= \frac{1}{2} \cdot z \cdot (z + 1) + (z + 1)$

and it's the same thing.

Having derived that :

$y + (z + 1) = \frac{1}{2} \cdot z \cdot (z + 1) + (z + 1)$

you "cancel" $(z+1)$ form both "sides" to get :

$y = \frac{1}{2} \cdot z \cdot (z + 1)$.