Assignment Statements

To prove

$\{p\}\; x\; :=\; E\; \{q\}$

$p$ $=>$ $q$_E^x

To prove

$\{p\}\; x\; :=\; e$₀ if $b$₀ ~ ...~ $e$_n if $b$_n $\{q\}$

it suffices to prove

$\{p$ and $b$₀} x := e₀ {q}
...
$\{p$ and $b$_n} x := e_n {q}
$p$ and (not $b$₀ and ... and not $b$_n) $=>$ $\{q\}$