Dedicated to the Tuesday Afternoon Club to C.A.R. Hoare at the occasion of his being elected Fellow of the Royal Society.

**Lemma 0.** For any statement `S` and
any constant predicate `C`

wp(`S`, `C`) = wp(`S`,
`T`) ∧ `C` .

**Proof.** By substituting for `C` the
two constant predicates `T` and `F`, respectively. (End of
Proof.)

**Lemma 1.** For any statement `S`,
any predicate `R`, and any constant predicate `C`

wp(`S`, `R` ∨ `C`) =
wp(`S`, `R`) ∨ wp(`S`,
`C`) .

**Proof.** By substituting for `C` the
two constant predicates `T` and `F`, respectively. (End of
Proof.)

In the following, `P` is a predicate in `x` and by definition
`P`′ = `P`_{x′}^{x} ; variables `x` and
`x`′ range over the same non-empty domain.

**Lemma 2.** For any predicate `P` in
`x` we have for all `x`

`P` = (A`x`′ ::
`x` ≠ `x`′ ∨
`P`′) .

**Proof.** `P` = (A`x`′ :: `P`) = (A`x`′ : `x`′ =
`x` : `P`′) = (A`x`′ :: `x` ≠
`x`′ ∨ `P`′). (End of Proof.)

**Theorem.** For any statement `S`
with state space `x` and any predicate `P` we have

wp(`S`, `P`) = wp(`S`,
`T`) ∧ (A`x`′ ::
wp(`S`, `x` ≠ `x`′)
∨ `P`′) .

**Proof.** wp(`S`,
`P`)

= { Lemma 2 }

wp(`S`, (A`x`′ :: `x` ≠
`x`′ ∨ `P`′))

= { distributivity of wp over universal quantification }

(A`x`′ ::
wp(`S`, `x` ≠ `x`′
∨ `P`′))

= { Lemma 1 }

(A`x`′ ::
wp(`S`, `x` ≠ `x`′)
∨ wp(`S`, `P`′))

= { Lemma 0 }

(A`x`′ ::
wp(`S`, `x` ≠ `x`′)
∨ wp(`S`, `T`) ∧
`P`′)

= { wp(`S`, `R`) ⇒
wp(`S`, `T`) }

wp(`S`, `T`) ∧ (A`x`′ :: wp(`S`,
`x` ≠ `x`′) ∨
`P`′) .

(End of Proof.)

Hence, the predicate transformer wp(`S`, ?) is fully
characterized by the two predicates wp(`S`, `T`)
and wp(`S`, `x` ≠
`x`′) .

20 April 1982