Proof Two

Proof.

$$\langle \alpha[E/x] \rangle \; x := E \; \langle \alpha \rangle$$

Suppose the state variables are $x_1,x_2,\dots,x_n$. Suppose that the assignment has the form $x_1 := E(x_1,x_2,\dots,x_n)$, with no loss of generality.

Define $\beta(x_1,x_2,\dots,x_n) = \alpha(E(x_1,\dots,x_n),x_2,\dots,x_n)$, a test. Then let $(a_1,a_2,\dots,a_n)$ be a state vector for input.

Following the application of the assignment, the output is

$$E(a_1,a_2,\dots,a_n),a_2,\dots,a_n) = (b_1,a_2,\dots,a_n)$$

Clearly then, $\beta(a_1,a_2,\dots,a_n) = \alpha(b_1,a_2,\dots,a_n)$. So $(a_1,a_2,\dots,a_n)$ satisfies $\beta = \alpha[E/x]$ if and only if $(b_1,a_2,\dots,a_n)$ satisfies $\alpha$

So $\alpha[E/x_1]$ counts as True every possible input to the assignment that gives an output satisfying $\alpha$. So $\beta = \alpha[E/x_1]$ is the most general possible precondition making the tripple correct. $\qedsymbol$