Correction and extension of EWD932b

Correction and extension of EWD932 b

EWD932 b refers to "drawn arrows"; I should have written "solid arrows". More seriously, I mentioned Lemma 4 as "special consequence" of the preceding lemmata. Well, if isn't.

Lemma 4

Proof 4 The precondition corresponding to the solid arrows is equivalent to $(a \max b) \leq (A \min B)$ , which is maintained by the ord operations because they leave the values of $a \max b$ and $A \min B$ unchanged (max and min being symmetric operators). (End of Proof 4.)

Besides the above blemishes EWD932 b suffers from a severe omission in that it leaves open how to use the Lemmata in order to show that some graph represents a theorem. The following should remedy this omission.

Theorem Consider a directed graph with solid and dotted arrows such that no two dotted arrows have an end-point in common. Let there exist a set of subgraphs such that

(i) each solid arrow, together with any dotted arrows with which it has an endpoint in common, occurs in at least one of the subgraphs, and (ii) each subgraph is a theorem (in the sense of EWD932 b).

Then the whole graph represents a theorem (in that same sense.)

Proof The dotted arrows of the graph being without common end-points, the corresponding ord operations may be performed in any (partial) order.

Consider an arbitrary solid arrow and perform first the ord operations of thea subgraph in which that solid arrow occurs together with its (at most two) adjacent dotted arrows; perform subsequently the remaining ord operations.

In view of the opening remark of this proof, the nett result will be as if all ord operations from the graph had been executed concurrently. In the above sequenced execution, the solid arrow is maintained by the first step because the subgraph in question is a theorem, and it is maintained by the second step because its end-points are not involved in the latter's ord operations.

An arbitrary solid arrow being maintained, all solid arrows are maintained, and hence the graph represents a theorem. (End of Proof.)

Note The trap not to fall into is to "convince" oneself that the ord operations are harmless in the following way:

consider

The solid horizontal arrows are safe on account of Lemma 2:

And on account of lemma 3: $\overrightarrow{7} \& \overrightarrow{1}$ neither the one and operation nor the other destroys

EWD937-2

the solid diagonal, hence Quod non, e.g.

is a theorem.

yields

。

6 10

with $6 > 4$ . (End of Note.)

In view of the way in which the theorem has been formulated we can now use (instead of Lemma 0)

Lemma 0a:

Are the lemmata of EWD932 b independent? No, besides Lemma 5 , which followed from Lemmata 3a and 3b , Lemma 1c follows from Lemmata 1a and 1b. But are they complete, or do there exist graphs representing correct theorems, for whose proof we would need more lemmata? (I am endebleed to M.G.Gauda For raising this question.) Currently I have no idea how to settle this question.

Austin, 20 September 1985

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