A sequel to EWD859 (with C.S.Scholten)

by C.S. Schohen and Edsger W. Dgkstra.

A notational comment

The formulation of (13) and (14) in Theorem 0 of EWD85g is in terms of two functions $p$ and $q$ ; the first one is predicate-valued, the value of the second one is an m-tuple of predicates, and both are defined on two arguments, viz. a predicate and an m-tuple of predicates. In retrospect this was a mistake. In the sequel we shall replace them by a single function, pq say, of which both value and argument are a pair (predicate, m-tuple of predicates). In the new notation, (13) and (14) become

\begin{array}{l} (X, Y): ([ r Y \equiv R ] \wedge \ (A U, V: (U, V) \underline {{s u b}} (X, Y): \ [ (r U, r s V) \equiv p q (r V, r s U) ]) \ \end{array}

h: (\underline {{A R}}:: (\underline {{E Z}}:: [ (h R, Z) \equiv p q (R, h Z) ])))

We thus achieve several simplifications. There is the notational advantage that the arguments need not be repeated once for $p$ and once for $q - j$ ; there is the conceptual simplification that, pg being defined on a single argument, it suffices to require for pg just monotonicity.

(End of notational comment.)

Formulation and proof of lemma 0, EWD85g-4, can be improved as follows.

Lemma 0. Let $X$ and $Y$ range over predicate structures of given shapes; let $b$ be a boolean function such that $b \times Y$ is defined for all ${X,Y}$ . Consider the equa-

fions

(x, y): b \times r \tag {2}

and

X: (\underline {{E}} Y; b \times Y) ; (3)

then there exists a (many to one) correspondence between the solutions of (2) and those of (3) such that a solution of (3) is the $X$ -component of all corresponding solutions of (2).

Proof. For all $X$ we observe

\begin{array}{l} (E Y: (X, Y) i s a s o l u t i o n o f (2)) \ = {(2) } \ (E Y: b X Y) \ = {(3) } \ X i s a s o l u t i o n o f (3). \ \end{array}

(E n d o f P r o o f.)

Corollary 0. If (2) has an extreme solution $\overline{\left( {{X}{e},{Y}{e}}\right) }$ , ${X}_{e}$ is (3)'s extreme solution of the

same kind.

(\mathrm {P r o o f o m i t t e d .})

Re Lemma1, EWD85g-5, we remark that the corresponding lemma for weakest solutions is also valid; the proof is best conducted via the conjuge and is left to the reader.

Similarly, from Theorem 0, EWD85g-10, the corresponding theorem for weakest solutions can be derived. Since this requires a bit more care, we now show how this can be done.

The weakest solution of (0) would be the negation of the strongest solution of (0) with $\left( {X,Y}\right)$ replaced by $\left( {{7x},7y}\right)$ ,i.e.

\begin{array}{l} (X, Y): ([ r (Y) \equiv R ] \wedge \ (\underline {{A}} U, V: (U, V) \mathrm {s u b} (\gamma X, \gamma Y): \ [ (r U, r s \overline {{V}}) \equiv p q (r V, r s U) ]) \ \end{array}

To begin with, we replace the dummies $U,V$ by

\begin{array}{l} (X, Y): ([ r (Y) \equiv R ] \wedge \ (A U, V: (7 U, 7 V) \underline {{\operatorname {s u b}}} (7 X, 7 Y); \ [ (r (¬ U), r s (¬ V)) \equiv p q (r (¬ V), r s (¬ U)) ] ]) \ \end{array}

With $r, rs$ , and structure forming commuting with negation and in view of the definition of the conjugate, this yields

\begin{array}{l} (X, Y): ([ r, Y \equiv r R ] \wedge \ (A U, V: (U, V) \operatorname {s u b} (X, Y): \ [ (r U, r s V) \equiv p q ^ {*} (r V, r s U) ]) \ \end{array}

Since ${p}^{q}$ is monotonic,we deduce on account of Theorem 0,that (4) has a strongest solution, and ,hence (0) has a weakest one.

Let us define $\tilde{g}$ by denoting the root of the X-component of the strongest solution of (4) by $\tilde{g}\left( {iR}\right)$ .

with ${\widetilde{g}}^{ * }R$ short for $¬ {\widetilde{g}}\left( {rR}\right)$ our first conclusion is that

[ \tilde {g} ^ {*} R \equiv (\mathrm {t h e r o o t o f t h e} X \mathrm {- c o m p o n e n t o f t h e w e a k e s t}

Our second conclusion from the definition of $\tilde{g}$ (4) and Theorem 0 is, that $\tilde{g}$ is the strongest solution of

h: (\underline {{A}} R:: (\underline {{E}} Z:: [ (h R, Z) \equiv p q ^ {*} (R, h Z) ]) ;

this is equivalent to the conclusion that $\widetilde{g}^{*}$ is the weakest solution of

h: (\underline {{A}} R:: (\underline {{E}} Z:: [ (h ^ {} R, Z) \equiv p q ^ {} (R, h ^ {*} Z) ])

Negating the dummies, we derive

h: (\underline {{A R}}: (\underline {{E Z}}: [ (h ^ {} (I R), I Z) \equiv p q ^ {} (I R, h ^ {*} (I Z)) ])

and, by applying the definition of the conjugate

h: (\underline {{A}} R:: (\underline {{E}} Z:: [ (h R, Z) \equiv p q (R, h Z) ])

i.e. $\tilde{g}^{*}$ is the weakest solution of (1). And this concludes our demonstration that Theorem 0 holds for weakest solutions as well. (The above book-keeping is more elaborate than we had hoped.)

We shall define, for a recursively defined procedure REC, the predicate transformer wlp (REC,) as the weakest solution of an equation of type (1) and the predicate transformer wp (REC,) as the

shrounge solution of a very similar (possibly iden- tical) equation. The ultimate goal of this note will be to prove at least

(i) that $wp(Rec,?)$ satisfies the Law of the Ex- cluded Miracle (ii) that wlp(REC,?) is universally conjunctive (iii) that $\left\lbrack {{wp}\left( {\operatorname{REC},R}\right) \equiv {w1p}\left( {\operatorname{REC},R}\right) ∧ {wp}\left( {\operatorname{REC},\text{true}}\right) }\right\rbrack$ .

To this end we have to establish first the relevant conjunctivity properties, etc. for functions pg -in

(1) $-$ as derived from the body of REC.

For the time being, we consider the body in isolation, i.e. we temporarily ignore that later the body will be used for a recursive definition. In other words, we consider a body $D$ , built by means of concatenation and the alternative construct from known statements and one "parameter statement" denoted by REC.

of the known statements $S$ we use

(i) $\left\lbrack {{wp}\left( {S,{false}}\right) \equiv {false}}\right\rbrack$ (ii) $w \mid p\left( {S,?}\right)$ is universally conjunctive. (iii) $\left\lbrack {{w}{p}\left( {S,R}\right) \equiv {w}{p}\left( {S,R}\right) }{\Lambda }\right\rbrack {w}{p}\left( {S,{true}}\right) \rbrack$ for all $R$ .

The parameter statement REC enters the game via two predicate transformers, h and Ih respectively. They will be used to play the roles of wp(REC,?) and wlp(REC,?) respectively; here h and Ih will be independent parameters for which assumptions (i),(ii), and (iii) will not be made.

Lemma 1. Let $D$ be a statement, built by concatenation and the alternative construct from known statements and a statement REC for which $h$ and $lh$ play the role of $wp(REC, ?)$ and $wlp(REC, ?)$ respectively. Then two known functions, $pq$ and $lpq$ , of which both value and argument are a pair (predicate, m-tuple of predicates), a predicate $P$ , and an m-tuple of predicates $Q$ can be defined that have the following properties

(i) [pq false = false] (Note that argument, value, and quantification refer to a pair (predicate, m-tuple of predicates).) (ii) If $p$ is universally conjunctive (iii) $\left\lbrack {{pq}\left( {X,Y}\right) \equiv \left| {{pq}\left( {X,Y}\right) ∧ \left( {P,Q}\right) }\right| }\right.$ for all(x,y) (iv) ${wp}\left( {D,R}\right)$ is for all $R$ the solution of

U: (\underline {{E}} Z:: [ (U, Z) \equiv p q (R, h Z) ])

(v) $w|p\left( {D,R}\right)$ is for all $R$ the solution of

U: (\underline {{E}} Z:: [ (U, Z) \equiv 1 _ {p q} (R, I _ {h} Z) ])

(In (iv) and (v), the existing $Z$ is also unique, but this will not be proved.)

Proof. The proof is by induction over the grammar of $D$ . For the base we take ship for $D$ ; for the induction step it suffices to consider for $D$ the forms ${S}{i}{D}^{\prime }, {REC}{i}{D}^{\prime },$ and

D = - s k i p

In this case we have $[wp(D,R) \equiv R]$ and $[wlp(D,R) \equiv R]$ . With the unique o-tuple, $wp(D,R)$ and $wlp(D,R)$ are the solution of

U: (E Z:: [ (U, Z) \equiv (R, 0. t u p l e) ])

consequently it suffices to define, with $m = 0$

\begin{array}{l} [ p q (X, Y) \equiv (X, 0 - t h u p l e) ] \ f o r a l l X, Y ≥) \ [ l p q (X, Y) \equiv (X, 0 - t u p l e) ] \ f o r a l l X, Y *) \ [ (P, Q) \equiv (\mathrm {t r u e}, 0 - h u p l e) ] \ \end{array}

*) $X,Y$ have to be taken from the appropriate range, i.e. $X$ is any predicate and $Y$ "any" 0-tuple of predicates.

The verification of (i) through (v) is left to the reader.

For each of the three cases of the induction step we need the following lemma, that we therefore formulate and prove first.

Lemma 2. Consider the conditions on $V$ and $U$

(E Z: [ Y \equiv f Z ] \wedge [ Z \equiv g Z ]) (5)

(E Z: [ U \equiv k (f Z) ] \wedge [ Z \equiv g Z ]) . (6)

then we have

\begin{array}{l} (U s a t i s f i e s (6)) \equiv \ (E V: [ U \equiv k V ] ∧ (V s a t i s f i e s (5))) \ \end{array}

Proof. (E V: [U E k V ] A (V satis fies (5)))

(U satisfies (G)) (End of Proof of Lemma 2)

\begin{array}{l} = {(s) } \ (E V: [ U \equiv k V ] \wedge (E Z: [ V \equiv f Z ] \wedge [ Z \equiv g Z ])) \ = {\mathrm {p r e d . c a l c .} } \ (E Z: (E V: [ U = k V ] \wedge [ V = f Z ] \wedge [ Z = g Z ]) \ = {\mathrm {p r e d . c a l c} } \ (E Z: [ U \equiv k (f Z) ] \wedge [ Z \equiv g Z ]) \ = {(6) } \ \end{array}

Corollary 1. If ${V}{u}$ is the only solution of (5), $k{v}{u}$ is the only solution of (6).

D = S _ {2} D ^ {\prime}

true

\begin{array}{l} = {\mathrm {d e f i n i l i o n} o p; } \ [ w p (D, R) \equiv w p (S, w p (D ^ {\prime}, R)) ] \ = {\mathrm {i n d u c t i o n h y p o t h e s i s (I V)} } \ [ w p (D, R) \equiv w p (S, t h e s o l u t i o n o f \ U: (\underline {{E}} Z:: [ (U, Z) \equiv p q ^ {\prime} (R, h Z) ]) ]) ] \ ⇒ {\mathrm {C o r o l l a r y} i } \ [ w p (D, R) \equiv (\mathrm {t h e s o l u t i o n o f} \ U: (\underline {{E}} Z:: [ U \equiv w p (S, p ^ {\prime} (R, h Z)) ] \wedge [ Z \equiv q ^ {\prime} (R, h Z) ]) ] \ \end{array}

Hence we define ${pq}$ by

[ p q (X, Y) \equiv (w p (S, p ^ {\prime} (X, Y)), q ^ {\prime} (X, Y)) ]

thus catering for (iv). We cater for (v) by the similar definition of 1pq :

[ l _ {p q} (X, Y) \equiv (w | _ {p} (S, l _ {p} ^ {\prime} (X, Y)), l _ {q} ^ {\prime} (X, Y)) ]

Furthermore we observe

[ p (X, Y) \equiv w _ {p} (S, p ^ {\prime} (X, Y)) ]

$= {$ induction hypothesis(iii) $}$

[ p (X, Y) \equiv w p (S, l _ {p ^ {\prime}} (X, Y) \wedge P ^ {\prime}) ]

$= {$ properties of ${wp}\left( {{S}{1},?}\right)$ and ${wlp}\left( {{S}{2},?}\right) }$

[ p (X, Y) \equiv w | _ {p} (S, l _ {p} ^ {\prime} (X, Y)) \wedge w _ {p} (S, P ^ {\prime}) ]

Combining the above, we can cater for (iii) by defining $\left( {P,Q}\right)$ by

[ (P, Q) \equiv (w p (S ^ {\prime}, P ^ {\prime}), Q ^ {\prime}) ]

The verification of (i) and (ii) is left to the reader.

D = R E C _ {2} D ^ {\prime}

f r u e

= {\mathrm {d e f i n i t i o n o f}; \mathrm {a n d o f} h }

[ w p (D, R) \equiv h w p (D ^ {\prime}, R) ]

= {\mathrm {i n d u c t i o n h y p o t h e s i s (i v)} }

[ w p (D, R) \equiv h (\mathrm {t h e s o l u t i o n o f}

U: (\underline {{E}} Z:: [ (U, Z) \equiv p q ^ {\prime} (R, h Z) ]) ]

⇒ {\mathrm {C o r o l a r y} 1 }

[ w p (D, R) \equiv (\mathrm {t h e s o l u t i o n o f}

U: (\underline {{E}} Z:: [ U \equiv h (p ^ {\prime} (R, h Z)) ] \wedge [ Z \equiv q ^ {\prime} (R, h Z) ]) ])

$= {$ pred.ca,c.; this transformation is necessary, since

$U$ should be expressed as a known function of $P\left( {R,hZ}\right)$ ;

to this end we extend $z$ with the predicate $\widetilde{z}$ to $(\widetilde{z},2) }$

\begin{array}{l} [ w p (D, R) \equiv (\mathrm {t h e s o l u t i o n o f} \ U: (\underline {{E}} \tilde {Z}, Z:: [ U \equiv h \tilde {Z} ] \wedge [ (\tilde {Z}, Z) \equiv p q ^ {\prime} (R, h Z) ]) ] \ \end{array}

Hence we cater for (iv) by defining ${pq}$ by

[ p q (X, (\tilde {Y}, Y)) \equiv (\tilde {Y}, p q ^ {\prime} (X, Y)) ]

We cater for (v) by the similar definition of |pq

[ l p q (X, (\tilde {Y}, Y)) \equiv (\tilde {Y}, l p q ^ {\prime} (X, Y)) ] .

In view of induction hypothesis (iii) we canter for (iii) by defining $\left( {P,Q}\right)$ by

[ (P, Q) \equiv (\mathrm {t r u e}, (P ^ {\prime}, Q ^ {\prime})) ]

Verification of (i) and (ii) is left to the reader. Note that in this case the value of $m$ has been increased by 1 .

\begin{array}{l} D = \mathrm {i f} B O \rightarrow D O ^ {\prime} ∥ B _ {1} \rightarrow D _ {1} ^ {\prime} \ t r u e \ = {\mathrm {d e f i n i t i o n o f} i \mathrm {f l a m b d a} {i } \ [ w p (D, R) \equiv (\underline {{A}} i: B B \wedge (¬ B i \vee w p (D i ^ {\prime}, R))) ] \ = {\mathrm {i n d u c t i o n h y p o t h e s i s (i v)} } \ [ w p (D, R) \equiv (\underline {{A}} i: B B \wedge G B i \vee (\mathrm {t h e s o l u t i o n o f} \ U: (\underline {{E}} Z:: [ (U, Z) \equiv p q i ^ {\prime} (R, h Z) ])))) ] \ ⇒ {\mathrm {C o r o l l a r y} } \ [ w p (D, R) \equiv (\bar {A} i: i t h e s o l u t i o n o f \ U: (\underline {{E}} Z:: [ U \equiv \mathcal {B} B \wedge (¬ B i \vee p i ^ {\prime} (R, h Z)) ] \wedge [ Z \equiv q i ^ {\prime} (R, h Z) ]) ]) \ = {\mathrm {p r e d . c a l c .} } \ \end{array}

\begin{array}{l} [ w p (D, R) \equiv (\mathrm {t h e s o l u t i o n o f} U: (\underline {{E}} 2 0, 2 1:: \ [ U \equiv B B \wedge (¬ B o v p 0 ^ {\prime} (R, h Z _ {0})) \wedge (¬ B 1 v p i ^ {\prime} (R, h Z _ {1})) ] \ ∧ [ (z _ {0}, z _ {1}) \equiv (q _ {0} ^ {\prime} (R, h Z _ {0}), q _ {1} ^ {\prime} (R, h Z _ {1})) ]) ]) ] \ \end{array}

Hence we cater for (iv) by defining ${pq}$ by

\begin{array}{l} [ p q (X, (Y _ {0}, Y _ {1})) \equiv (\mathcal {B} B \wedge (¬ B o v p o ^ {\prime} (X, Y _ {0})) \wedge (¬ B _ {1} \vee p i ^ {\prime} (X, Y _ {2})), \ (q _ {0} ^ {\prime} (X, Y _ {0}), q _ {1} ^ {\prime} (X, Y _ {1}))) ] \ \end{array}

Similarly we can for (v) by defining ${lpq}$ by

\begin{array}{l} [ l p q (X, (Y _ {0}, Y _ {1})) \equiv ((¬ B 0 \vee l p o ^ {\prime} (X, Y _ {0})) \wedge (¬ B 1 \vee l p r ^ {\prime} (X, Y _ {1})), \ (| q 0 ^ {\prime} (X, Y _ {0}), | q 1 ^ {\prime} (X, Y _ {1})) ] \ \end{array}

Again we can cater for (iii), this time by defining

(C, Q) b _ {y}

[ (P, Q) \equiv (B B \wedge (¬ B 0 \vee P _ {0} ^ {\prime}) \wedge (¬ B _ {1} \vee P _ {1} ^ {\prime}), (Q _ {0} ^ {\prime}, Q _ {1} ^ {\prime})) ].

Verification of (i) and (ii) is again left to the

reader. Note that the new $m$ is ${mo} + {m1}$ . In

view of the base and the three forms of the step, m equals the number of calls of REC in the body.

(End of Proof of Lemma 1.)

After the above explorations of the body D and its associated functions ${pg}$ and lpg -as defined in the proof of lemma 1 - we are now ready to explore the recursive definition

R E C = D

In view of Lemma 1 (iv) we now define $\omega \left( {\operatorname{REC},?}\right)$

as the strongest solution of (1), and, in view of Lemma 1 (v), wlp(REC,?) as the weakest solution of

\ln : (\underline {{A R}}: (\underline {{E Z}}: [ (\ln R, Z) \equiv 1 p q (R, \ln Z) ]) . (1 ^ {\prime})

According to Theorem 0, EWD85g, w p (REC, R) is the root of the X-component of the strongest solution of (o), and - see EWD860-2- wlp (REC, R) is the root of the X-component of the weakest solution of the corresponding

\begin{array}{l} (X, Y): ([ r Y \equiv R ] \wedge \ (\underline {{A}} U, V: (U, V) \underline {{\operatorname {s u b}}} (X, Y): \ [ (r U, r s \overline {{V}}) \equiv l p q (r V, r s U) ]) \ \end{array}

Note that Theorem 0 is applicable since from Lemma 1, (ii) and (iii), it follows that $\mathbf{lpq}$ and hence $\mathbf{pg}$ are monotonic.

Since we would like to apply the results of EWD849a "Junctivity of extreme solutions", we shall rewrite (o) and (o') in the forms

(X, Y): [ f (R, X, Y) \equiv (X, Y) ] (7)

(X, Y): [ (X, Y) \equiv I _ {f} (R, X, Y) ] (8)

respectively. The possibility of such a rewriting has been argued on EWD 85g-11 . The relevant properties of these functions are given by

Lemma 3. The functions $\rho$ -from (7)-, If $- {f}_{\text{rom}}\left( 8\right) -$ satisfy

(i) $\left\lbrack {f\text{false} \equiv \text{false}}\right\rbrack$ (Note that the argument

refers to a triple (predicate, pair of m-trees of predicates) and that the value and the quantification refer to a pair of m-trees of predicates.)

(ii) If is universally conjunctive (iii) a pair $(PP,QQ)$ of m-trees of predicates exists such that

[ f (X, Y) \equiv 1 _ {f} (X, Y) \wedge (\mathcal {P P}, \mathcal {Q Q}) ]

Proof.

From (0) and (7) we deduce that $f$ is defined by $\left\lbrack {\left( {\widetilde{X},\widetilde{Y}}\right) \equiv f\left( {R,X,Y}\right) }\right\rbrack = \left( {\text{for all}\widetilde{X},\widetilde{Y},X,Y}\right) \left( g\right)$

\begin{array}{l} [ r \tilde {Y} \equiv R ] \wedge \ (\underline {{A}} \tilde {U}, \tilde {V}, U, V: (\tilde {U}, \tilde {V}, U, V) _ {\mathrm {s u b}} (\tilde {X}, \tilde {Y}, X, Y): \ [ (r \tilde {U}, r s \tilde {V}) \equiv p q (r V, r s U) ]) \ \end{array}

From (0') and (8) we deduce that If is de-

\begin{array}{l} [ (\tilde {X}, \tilde {Y}) \equiv 1 / (R, X, Y) ] = (\mathrm {f o r a l l} \tilde {X}, \tilde {Y}, X, Y) (1 0) \ [ r \tilde {Y} \equiv R ] \wedge \ (\tilde {A} \tilde {U}, \tilde {V}, U, V: (\tilde {U}, \tilde {V}, U, V) _ {\mathrm {s u b}} (\tilde {X}, \tilde {Y}, X, Y); \ [ (r \tilde {U}, r s \tilde {V}) \equiv | p q (\overline {{r V}}, r s U) ] \ \end{array}

The above can be verified by observing that the equation (7) with $f$ defined by (9) yields (0).

(i) By (g), $f\left( x\right)$ is the solution of

(\tilde {X}, \tilde {Y}): ([ r \tilde {Y} \equiv \dot {f a l s e} ] ∧

(A) $\tilde{U},\tilde{V},U,V : \left( {\tilde{U},\tilde{V},U,V}\right)$ sub $\left( {\tilde{X},\tilde{Y},\text{false, false}}\right) :$

[ (r \tilde {U}, r s \tilde {V}) \equiv p q (r V, r s U) ])

Since all subtrees of false have that same value, this equation is, on account of Lemma 1,(i), equiv- valent to the equation

$\left( {\tilde{X},\tilde{Y}}\right) : \left\lbrack {\left\lbrack {r\tilde{Y} = \text{ false }}\right\rbrack ∧ }\right.$

(A \tilde {U}, \tilde {V}: (\tilde {U}, \tilde {V}) _ {\mathrm {s u b}} (\tilde {X}, \tilde {Y}):

[ (r \tilde {U}, r s \tilde {V}) \equiv f a l s e ])

which has false as its only solution.

(ii) By (10), all elements of $\left( {\tilde{X},\tilde{Y}}\right)$ are defined as universally conjunctive functions of $\left( {R,X,Y}\right)$ : For r Y this is obvious,for the remaining elements we rely on Lemma 1,(ii). Hence If is universal by conjunctive. (iii) With $P$ and $Q$ as they occur in Lemma 1, with the pair $(PP,QQ)$ of $m$ -trees of predicates defined by

\begin{array}{l} (\underline {{A}} \tilde {U}: \tilde {U} \underline {{\mathrm {s u b}}} P P: [ r \tilde {U} \equiv P ]) - i. e. \mathrm {t h e} m - f r e e \ w i t h a l l i t s e l e m e n t s e q u a l t o P - \ \end{array}

[ r Q Q \equiv \mathrm {f r u e} ] \wedge (\underline {{A}} \tilde {V}: \tilde {V} \underline {{\mathrm {s u b}}} Q Q: [ r s \tilde {V} \equiv Q ])

the conclusion follows from (g), (10), and Lemma 1,

(iii) (End of Proof.)

Theorem 0.

(i) [wp(REC,falsc) = falsose] (ii) $w{lp}\left( {{REC},?}\right)$ is universally conjunctive (iii) $\left\lbrack {{w}{p}\left( {{REC},R}\right) \equiv {w}{p}\left( {{REC},R}\right) ∧ {w}_{p}\left( {{REC},\text{true}}\right) }\right\rbrack$

Proof. (i) ( {wp}\left( {{RE}{C}_{1} ) false }\right) ) is by (7) the root of

the strongest solution of $\left( {X,Y}\right) : \left\lbrack {f\left( {\text{false},X,Y}\right) \equiv \left( {X,Y}\right) }\right\rbrack$ . By Lemma 3,(i),this solution is false

(ii) Since - Lemma 3, (ii) - If is universally conjunctive, the weakest solution of (8) - EWD849a, Theorem 2 - is a universally conjunctive function of $R$ ,hence so is the root of its $X$ -component. (iii) Consider, with 2 standing for a pair of m-trees of predicates, the equation

(X, Y): [ (X, Y) \equiv 1 \vert f (R, X, Y) ∧ Z ] . (1 1)

By lemma 3 (iii), (11) becomes (7) with $(PP, \mathbb{Q} \mathbb{Q})$ for $Z$ ; if we substitute true for $Z$ , (11) becomes (8). The right-hand side of (11) is universally conjunctive - lemma 3, (ii) - in the quadruple $(R, X, Y, Z)$ .

Let $G(R, Z)$ be the strongest solution of (11) and let $H(R, Z)$ be its weakest solution. The right-hand side of (11) being conjunctive, we have - EwD 84ga, Theorem 4 -

[ G (R, Z) \equiv H (R, \mathbf {t r u e}) \wedge G (\mathbf {t r u e}, Z) ]

With the special choice of (PP,QQ) for Z and confining our attention to the roots of the X-components, the conclusion (iii) follows. (End of Proof.)

Remark. Along the lines of the proof of Lemma 1, it can be shown that pq is or-continuous in

case non-determinacy is bounded. Along lines of the proof of Lemma 3 it can be proven that then the corresponding $f$ is or- continuous. From Theorem ${2}^{ * }$ of EWD84ga-16 then follows that ${wp}\left( {{RE}{C}_{,}?}\right)$ is or-continuous as well. (End of Remark.)

3 December 1983

s. C.S. Scholten cientific Adviser hilips Research Laboratories 600 JA EINDHOVEN ne Netherlands

proo. dr. Edsger W. Dgksra Burroughs Research Fellow Plataansstraat 5 5671 AL Nuenen The Netherlands