Proof Two

Proof.

$\displaystyle \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

$\displaystyle 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$