On a formula designed by Henk Doornbos

On a formula designed by Henk Doornbos

We are asked to prove for any $x,y,z$

(0) $\left\lbrack {x;{y}^{ \land }z \Rightarrow {\left( z;{v}{y} \land x\right) }{;}{\left( {v}_{x};{z}^{ \land }y\right) }}\right\rbrack$ .

We don't know beforehand how much of the relational calculus we shall need, but it is almost certain that we shall need the exchange rules

$$ \begin{array}{l} [ x; y \Rightarrow z ] \equiv [ 7 2; \sim y \Rightarrow \sim x ] \ [ x; y \Rightarrow z ] \equiv [ u x; 7 z \Rightarrow 7 y ] \ \end{array} $$

as they embody the axiom connecting the transposition “~” and the composition “;”. In a moment we shall need that composition is monotonic; we may need that composition is universally disjunctive (from which the monotonicity follows).

In (0), it is the consequent that needs to be unravelled, because nothing nice is known about the compositions of conjunc-tions. So we replace the consequent by rjs and since

(1) $\left\lbrack {x;{y}^{ \land }z \Rightarrow r;s}\right\rbrack$

is a monotonic function of $r$ and $s$ ,

Because, in view of the exchange rule, the expressions replaced are quite acceptable as antecedents, we use from EWD1117 that for monotonic

$$ [ f. e x p ] \equiv \langle \forall z: [ e x p \Rightarrow z ]: [ f. z ] \rangle $$

i.e. we propose to prove (0) by showing that for any $r,s, \left( 1\right)$ follows from

$\left\lbrack {z;{v}{y} \land x \Rightarrow r}\right\rbrack$ $\left\lbrack {{\sim }{x};z\; \land y \Rightarrow s}\right\rbrack$

Because 2 occurs fairly isolated in (1) we try to isolate 2 from (2). We observe

(2)

$$ \begin{array}{l} = {\mathrm {d e f i n i t i o n} } \ [ z; \sim y \land x \Rightarrow r ] \land [ \sim x; z \land y \Rightarrow s ] \ = {\mathrm {s h u n t i n p r e p a r a t i o n f o r} e x c h a n g e s } \ [ z; \sim y \Rightarrow \exists x. v ^ {\prime} r ] ^ {\prime} \land [ \sim x; z \Rightarrow \exists y. v s ] \ = {\mathrm {e x c h a n g e r u l e s a n d d e M o r g a m} } \ [ (x \wedge \neg r); y \Rightarrow \neg z ] \wedge [ x; (y \wedge \neg s) \Rightarrow \neg z ] \ = {p r e d i c a t e c a l c u l u s } \ [ (x _ {1} \wedge 7 r); y \vee x; (y \wedge 7 s) \Rightarrow 7 z ] \ \end{array} $$

Using the above rewriting of (2) we observe

(1)

$$ = {\mathrm {d e f i n i t i o n} } $$

$$ \begin{array}{l} [ x; y \land z \Rightarrow r; s ] \ = {\mathrm {s h u n t i n g} } \ [ x; y \Rightarrow r; s \lor 7 2 ] \ \Leftrightarrow {2 } a s r e w r i t t e n \ [ x; y \Rightarrow r; s, v (x \wedge 7 r); y \vee x; (y \wedge 7 s) ] \ = {\mathrm {s e e b e l o w} } \ t r u e \ \end{array} $$

Our final obligation is to weaken $x,y$ to the above disjunction , at the same time introducing r,s, and the conjuncts 7r,1s . We observe to this end

$$ \begin{array}{l} \left. \begin{array}{l} x; y \ {[ y \equiv (y \wedge s) \vee (y \wedge \neg s) ], ^ {\prime}; ^ {\prime} i s d i s j u n c t i v e } \end{array} \right} \ x; (y \wedge s) \vee x; (y \wedge 7 s) \ = {[ x \equiv (x \wedge r) \vee (x \wedge \neg r) ], " ; " i s d i s j u n c t i v e } \ (x \wedge r); (y \wedge s) \vee (x \wedge r); (y \wedge s) \vee x; (y \wedge 1 s) \ \Rightarrow {” _ {j} ^ {\prime \prime} i s m o n o t o n i c } \ r; s \vee (x \wedge 7 r); y \vee x; (y \wedge 7 s) \ \end{array} $$

QED

Remark I met the formula in the form (1) $\Leftarrow$ (2), in which form it was attributed to Henk Doornbos (and called the Grand Dedekind rule).

Austin, 1 December 1991

prof. dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78750-1188, USA