Can someone explain the first assignment and implied? We prove bottom to up and I don't follor after the $(1=x+1)$ if-Statement. This is what my book says about the assignment rule:
, if we wish to show that ψ holds in the state after the assignment $x = E$, we must show that $ψ[E/x]$ holds before the assignment.
But how is that the case here?
I'm not sure what book you're using, so I'm gonna stick to the formulation on wikipedia (hope that's Ok :]). There are two things going on in the first four lines of your example, one application of the Consequence rule and one application of the Assignment axiom schema.
Set $$\psi' = (x + 1 - 1 = 0 \to 1 = x + 1) \land (\neg (x + 1 - 1 = 0) \to x + 1 = x + 1)$$ $$\psi = (a - 1 = 0 \to 1 = x + 1) \land (\neg (a - 1 = 0) \to a = x + 1)$$
and notice that
$$\psi' = \psi[x + 1/a].$$
So applying the Assignment axiom schema (the rule you've mentioned) we're allowed to derive
$$\overline{\{\psi'\}\ a = x + 1\ \{\psi\}}$$
that being lines 2-4. The Consequence rule allows us to strengthen the precondition ($\psi'$), since $\psi'$ is valid we have
$$\top \to \psi'$$ $$\psi \to \psi$$
and can derive
$$\frac{\top \to \psi',\ \overline{\{\psi'\}\ a = x + 1\ \{\psi\}},\ \psi \to \psi}{\{\top\}\ a = x + 1\ \{\psi\}}.$$
The remaining lines prove $\{\psi\}\ \texttt{if } ... \texttt{ else } ...\ \{y = x + 1\}$, so applying the Rule of composition you can derive the required result.
