A correction of EWD1112

The final observation of EWD1112 for fresh variables $x^{\prime}, y^{\prime}$ from a nontrivial type (i.e. with at least 2 distinct values, so that $[x^{\prime} = y^{\prime}]_{x^{\prime}y^{\prime}} \equiv$ false) should have been as follows:

$$ [ R \wedge \sim R \Rightarrow J ] _ {x x ^ {\prime} y y ^ {\prime}} $$

$= { {d\phi .o\rho j}$ in extended context $}$

$$ [ R \wedge \sim R \Rightarrow x = y \wedge x ^ {\prime} = y ^ {\prime} ] _ {x x ^ {\prime} y y ^ {\prime}} $$

$= { {x}^{\prime }{y}^{\prime }\;f\left( x\right)$

$$ [ R \wedge \sim R \Rightarrow [ x = y \wedge x ^ {\prime} = y ^ {\prime} ] _ {x ^ {\prime} y ^ {\prime}} ] _ {x y} $$

$= {$ type of ${x}^{\prime }{y}^{\prime }\;{non}\;{emph}y}$

$$ [ R \wedge \sim R \Rightarrow x = y \wedge [ x ^ {\prime} = y ^ {\prime} ] _ {x ^ {\prime} y ^ {\prime}} ] _ {x y} $$

$= {$ type of ${x}^{\prime }{y}^{\prime }$ nontrivial $}$

$$ [ R \land \sim R \Rightarrow f a l s e ] $$

and as a constraint on $R$ the last line is more stringent than $[R \land wR \Rightarrow ]$ , i.e. Cartesian extension destroys antisymmetry and turns partial orders into preorders.

Nuenen 16 December 1991

Prof. dr. Edsger W. Dyrkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188, USA