<s>[INST] Small part of loop invariant i'm not getting 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)$
 [/INST] 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)$.

</s>