Predicate transformers (Draft Ch.3)

Predicate transformers (Draft Ch.3)

In this chapter we consider functions from predicates to predicates: with $f$ such a function and $X$ a predicate, $f.X$ is a predicate that, in general, depends on $X$ . The fact that $f$ is a function is aptly captured by

(0) $\left\lbrack {X \equiv Y}\right\rbrack ⇒ \left\lbrack {f \cdot X \equiv f \cdot Y}\right\rbrack$

bearing in mind that we have decided to use $[\ldots \equiv \ldots ]$ to express equality of two predicates. For historical reasons, such functions are called "predicate transformers": in the metaphor under- lying that term, $f$ is viewed as an operator that "transforms" any given X into the corresp- ponding f.x

It so happens that the sequel enjoys an all- pervading symmetry, a symmetry that we would like to exploit for brevity's sake. The symmetry consists in the circumstance that all concepts and lemmata have their duals. But in order to express that symmetry concisely, we need the notion of "the conjugate of a predicate transformer".

The conjugate of a predicate transformer $f$ is a predicate transformer denoted by ${f}^{ * }$ and defined by

(\underline {{A}} X: \mathrm {t r u e}: [ f ^ {*} X \equiv ¬ f (¬ X) ]) , \mathrm {o r}

(1)

[ f ^ {*} X \equiv - f (X) ]

for short.

Note. In (1), the universal quantification over $X$ is "understood" as usual. But it holds for any predicate transformer $f$ : for (1) to define the star *, its universal quantification over $F$ should be understood as well. (End of Note.)

The term "conjugate" is justified by the cir- cumstance that, if one predicate transformer is the conjugate of another, they are each other's conjugates, as follows from the following

Lemma 3.0 $\left\lbrack {{f}^{ * }.X \equiv f.X}\right\rbrack$

Proof 3.0

\begin{array}{l} f ^ {} X \ = {(1) \mathrm {w i t h} p := p ^ {} } \ \lnot p ^ {}. (\lnot X) \ = {(1) \mathrm {w i t h} X := - 7 X } \ 7 7 f. (7 7 X) \ = {\mathrm {N e g a t i o n}, \mathrm {t w i c e} } \ p _ {X} \ \end{array}

(End of Proof 3.0)

For brevily's sake we also need the notion of "the conjugate of a bag of predicates". For a bag $V$ of predicates we obtain its conjugate $V^{*}$ by negating all its predicates. As a result we have

• with $\epsilon$ having a higher binding power than $\equiv -$

(2) $X \in V^{*} \equiv (¬ X) \in V$ (3) ${V}^{ * } = V$

So much for the notion of "the conjugate"

We now define the two important concepts, viz. conjunctivity and disjunctivity, that will occupy us for the remainder of this chapter:

(4) $\left( {f\text{is}\operatorname{conjunctive}\text{over}V}\right) \equiv$

[ f. (\underline {{A}} X: X \in V: \bar {X}) \equiv (\underline {{A}} X: X \in V: f. X) ]

(5) $\left( {p\text{is disjunctive over}V}\right) \equiv$

[ (\underline {{E X}}: X \in V; f. X) \equiv f. (\underline {{E X}}: X \in V; X) ]

In other words: the conjunctivity of $f$ describes the extent to which $f$ distributes over universal quantification, its disjunctivity describes how it distributes over existential quantification.

The notion of the conjugate enables us to formulate the following lemma, which expresses the symmetry alluded to:

Lemma 3.1

$\left( {f\text{is}\operatorname{conjunctive}\text{over}V}\right) \cong \left( {{F}^{ * }\text{is}\operatorname{disjunctive}\text{over}{V}^{ * }}\right)$

Proof 3.1

\begin{array}{l} (f \mathrm {i s c o n j u n c t i v e o v e r} V) \ = {\mathrm {d e p .} (4) } \ [ f. (\underline {{A}} X: X \in V: X) \equiv (\underline {{A}} X: X \in V: f. X) ] \ = {\mathrm {N e g a t i o n} } \ [ ¬ f. (¬ (\underline {{A}} X: X \in V: X)) \equiv ¬ (\underline {{A}} X: X \in V: f. X) ] \ = {\mathrm {d e M o r g a n}, \mathrm {t w i c e} } \ [ ¬ f. (¬ (\exists X: X \in V: ¬ X)) \equiv (\exists X: X \in V: ¬ f. X) ] \ = {\mathrm {T r a n s p o r m i n g t h e d u m m y}, X := ¬ Y } \ [ ¬ f. (¬ (\underline {{E Y}}; G Y) \in V: Y)) \equiv (\underline {{E Y}}; (¬ Y) \in V: ¬ f. (¬ Y)) ] \ = {d e f: (1); (2) } \ [ f ^ {} (E Y: Y \in V ^ {}: Y) \equiv (E Y: Y \in V ^ {}: f ^ {} Y) ] \ = {\mathrm {d e f .} (5) } \ (f ^ {} i s d i s j u n c t i v e o v e r V ^ {}) \ \end{array}

(E n d o f P r o o p 3. 1)

The less restricted V, the stronger the corresp- ponding junctivity property - "junctive" stands for either conjunctive or disjunctive - . We distinguish the following types of junctivity:

\begin{array}{l} \mathrm {u n i v e r s a l l y j u n c t i v e :} \ j u n c t i v e o v e r a l l V \ \mathrm {u n b o u n d e d l y j u n c t i v e :} \ j u n c h i v e o v e r a l l n o n - e m p l y V \ d e n u m e r a b l y j u n c t i v e: \ j u n c t i v e o v e r a l l n o n - e m p t y V w i t h d e n u m e r a b l y \ m a n y d i s t i n c t p r e d i c a t e s \ \begin{array}{l} \mathrm {(f i n i t e l y)} \end{array} j u n c t i v e: \ j u n c t i v e o v e r a l l n o n - e m p l y V w i t h a f i n i t e n u m b e r \ \end{array}

of distinct predicates

…- continuous:

junctive over all non-empty V, the distinct predicates of which can be ordered as monotonic sequence (see Note below)

monotonic:

junctive over all non-empty $V$ , the distinct predicates of which can be ordered as monotonic sequence of finite length.

Note Here we distinguish between "and-continuity" in the case of conjunctivity and "or-continuity" in the case of disjunctivity. (End of Note.)

Above we have introduced 6 "types" of junctivity corresponding to 6 "types" of bags V of predicates. The constraints that characterize those types of bags V have been formulated in terms of

(i) (the cardinality of) the number of (distinct) predicates in $V$ ,and (ii) the question of whether the (distinct) predi-cates can be ordered in a monotonic sequence, i.e. can be numbered such that

(\underline {{A}} i, j: 0 ≤ i ≤ j: [ X. i ⇒ X. j ]) \vee (\underline {{A}} i, j: 0 ≤ i ≤ j: [ X. j ⇒ X. i ]).

Ad (i) we remark that, the (distinct) predicates in $V^$ being in one-to-one correspondence with the (distinct) predicates in $V$ , $V^$ and $V$ satisfy the same constraints of category (i). Ad (ii) we remark that, since

[ X ⇒ Y ] \equiv [ ¬ Y ⇒ ¬ X ],

either both $V^{ * }$ and $V$ ,or neither of them,satisfy the constraint mentioned under (ii). From the above we conclude

Lemma 3.2

(\mathrm {t h e} ^ {\prime \prime}) ^ {\mathrm {t y p e}} o f V) = (\mathrm {t h e} ^ {\prime \prime}) ^ {\mathrm {t y p e}} o P V ^ {*})

and , in combination with Lemma 3.1

Lemma 3.3

(p ^ {\prime} s ^ {\prime \prime} t h y p e ^ {\prime \prime} o f c o n j u n c t i v i t y) = (p ^ {} s ^ {} t h y p e ^ {*} o f d i s j u n c t i v i t y).

Three remarks are in order.

Firstly, universal conjunctivity is a properly different from universal disjunctivity -different in the sense that a given predicate transformer may enjoy the one, but not the other-, unbounded conjunctivity clippers from unbounded disjunctivity, and so down to and-continuity, which clippers from or-continuity; but there is no point in dis- tinguishing between "and-monotonicity" and "or-monotonicity": they are the same property, called "monotonicity" for short, and usually defined by

(6) ( $f$ is monotonic)

(¬ X, Y: [ X ⇒ Y ] ⇒ [ P. X ⇒ P. Y ])

To prove that and-monotonicity and monotonicity as defined by (6) are the same property, we show that the one property follows from the other and vice versa:

\begin{array}{l} \mathrm {a n d - m o n o t o n i c i t y} ⇒ (6) \ [ X ⇒ Y ] \ = {I m p l i c a t i o n } \ [ X ∧ Y \equiv X ] ∧ [ X ⇒ Y ] \ ⇒ {\mathrm {L e i b n i z} } \ [ p. (X ∧ Y) \equiv p. X ] ∧ [ X ⇒ Y ] \ ⇒ {f i s a n d m o n o t o n i c } \ [ F. X \wedge F. Y = F. X ] \ = {\text {I m p l i c a t i o n} } \ [ f. x ⇒ f. y ] \ \end{array}

(6) ⇒ \frac {}{} \mathrm {a n d} - \mathrm {m o n o t o n i c i t y}

Predicates that can be ordered in a monotonic sequence of finite length can be ordered in a weakening sequence of finite length. We do so, and observe for $n ≥ 1$

\begin{array}{l} (\underline {{A}} i, j: 0 ≤ i ≤ j < n: [ X. i ⇒ X. j ]) \ ⇒ {\text {I n s t a n t i a t i o n}: i := 0 } \ (\exists j: 0 ≤ j < n: [ X. 0 ⇒ X. j ]) \ = {p _ {i} \mathrm {i s m o n o t o n i c} } \ (\underline {{\partial}} _ {j}: 0 ≤ j < n: [ X. 0 ⇒ X. j ]) ∧ (\underline {{\partial}} _ {j}: 0 ≤ j < n: [ f. (X. 0) ⇒ f. (X. j) ]) \ \end{array}

\begin{array}{l} = {\mathrm {i n t e r c h a n g e o f q u a n t i f i c a t i o n s} } \ [ (\underset {-} {A} j: 0 ≤ j < n: X. 0 ⇒ X. j) ] \wedge [ (\underset {-} {A} j: 0 ≤ j < n: f. (X. 0) ⇒ f. (X. j)) ] \ = {\text {d i s t r i b u t i o n}; \text {r a n g e o m i t t e d} } \ [ X. 0 ⇒ (\underline {{A}} _ {j}: X. j) ] \wedge [ f. (X. 0) ⇒ (\underline {{A}} _ {j}: f. (X. j)) ] \ = {\mathrm {I n s t a n t i a l i o n}; \mathrm {r e m e m b e r} n ≥ 1 } \ [ X. 0 ⇒ (\underline {{A}} j: X. j) ] \wedge [ f. (X. 0) ⇒ (\underline {{A}} j: f. (X. j)) ] \wedge \ [ (\underline {{A}} j: X. j) ⇒ \bar {X}. 0 ] ∧ [ (\underline {{A}} j: f. (X. j)) ⇒ f. (X. 0) ] \ = {\mathrm {E q u i v a l e n c e} } \ [ X, 0 \equiv (\underline {{A}} j: X, j) ] \wedge [ f. (X, 0) \equiv (\underline {{A}} j: f. (X, j)) ] \ ⇒ {\mathrm {L e i b n i z}, \mathrm {e l i m i n a t i o n} o f X. 0 } \ [ f. (\underline {{\mathrm {但}}} _ {j}: x, j) \equiv (\underline {{\mathrm {但}}} _ {j}: f. (x, j)) ] \ \end{array}

9.e.d.

The proof that or-monotonicity and monotonicity as defined by (6) are the same property is mutatis mutandis the same argument. From now onwards we shall refer to just monotonicity. We mention the consequence of Lemma 3.3 and the fact that there is only one monotonicity

Lemma 3.4 $\left( {p\text{is monotonic}}\right) \equiv \left( {{p}^{ * }\text{is monotonic}}\right)$ .

Secondly, we draw attention to the consequences of the fact that, the less restricted $V$ , the stronger the corresponding junctitivity property. From the definitions we derive directly

Lemma 3.5

$\left( {f\text{is universally junctive}}\right) ⇒ \left( {f\text{is unboundedly junctive}}\right) ;$

$\left( {f\text{is unboundedly junctive}}\right) ⇒ \left( {f\text{is denumerably junctive}}\right) ;$

\begin{array}{r l} & {(p i s d e n u m e r a b l y j u n c t i v e) ⇒} \ & { (p i s (f i n i t e l y) j u n c t i v e) ∧ (p i s \dots - c o n t i n u o u s);} \ & {(p i s (f i n i t e l y) j u n c t i v e) \lor (p i s \dots - c o n t i n u o u s) ⇒} \ & { (p i s m o n o t o n i c)} \end{array}

Thirdly, we draw attention to the fact that and- continuity is most interestingly applied to an infinite strengthening sequence: in that case, $\left( {\underline{\mathbf{A}}j : 0≤ j : X,j}\right)$ can be viewed as the limit of the infinite sequence $X.j\left( {0 ≤ j}\right)$ ,and and-continuity of $f$ then expresses that "the $f$ of the limit equals the limit of the $f$ ’s". In the case of the infinite weakening sequence, $\left\lbrack {\left( {\underline{\mathbf{A}}j : 0 ≤ j : X.j}\right) \equiv X.0}\right\rbrack$ ,i.e. the limit is the first term and monotonicity -implied by continuity - is already enough to guarantee that application of $F$ and universal quantifica-tion commute. Similarly,or-continuity is most interestingly applied to an infinite weakening sequence.

Two further lemmata about monotonicity are worth knowing.

Lemma 3.6

(p i s m o n o t o n i c) \equiv

(\underline {{A}} X, Y: [ X \vee Y ] ⇒ [ P ^ {*} X \vee P. Y ])

Proof 3.6

(f is monotonic)

\begin{array}{l} = {(6) } \ (\underline {{A}} X, Y: \colon [ X ⇒ Y ] ⇒ [ f. X ⇒ f. Y ]) \ = {I m p l i c a t i o n, t w i c e } \ (A X, Y: [ i X \vee Y ] ⇒ [ i f. X \vee f. Y ]) \ = {\mathrm {T r a n s f o r m i n g t h e d u m m y}: x := X } \ (¬ X, Y: [ X \vee Y ] ⇒ [ ¬ f. (X) \vee f. Y ]) \ = {\mathrm {C o n j u g a t e} } \ (\underline {{\underline {{A}}}} X, Y: [ X \vee Y ] ⇒ [ f. X \vee f. Y ]) \ \end{array}

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

Note that in the implication the antecedent is symmetric in $X$ and $Y$ , while the consequent is not.

Lemma 3.7 For monotonic $f$ and any bag $V$ of predicates

[ f. (\underset {X: X \in V: X} {\cap}) ] a n d

[ (\underline {{E}} X: X \in V; f _ {\cdot} ^ {p} X) ⇒ f. (\underline {{E}} X: X \in V; X) ]

Proof 3.7 For brevity's sake the range restriction " $\in V$ " has been omitted.

\begin{array}{l} f r u e \ = {\mathrm {I n s t a n t i a t i o n} } = {\mathrm {I n s t a n t i a t i o n} } \ [ (A Y: (A X: X) ⇒ Y) ] [ (A Y: Y ⇒ (E X: X)) ] \ ⇒ {f \mathrm {i s m o n o t o n i c} } = {f \mathrm {i s m o n o t o n i c} } \ [ (\underline {{A}} Y: \mathcal {P}. (\underline {{A}} X:: X) ⇒ \mathcal {P}. Y) ] [ (\underline {{A}} Y: \mathcal {P}. Y ⇒ \mathcal {P}. (\underline {{E}} X:: X)) ] \ = {\text {I m p l i c a t i o n} } {\text {I m p l i c a t i o n} } \ [ (\underline {{A Y}}: ¬ f. (\underline {{A X}}: x) \vee f. Y) ] [ (\underline {{A Y}}: ¬ f. Y \vee f. (E X: x)) ] \ = {\text {D i s t r i b u t i o n} } = {\text {D i s t r i b u t i o n} } \ \end{array}

\begin{array}{l} [ \pi f _ {0} (\underline {{A}} X:: X) \vee (\underline {{A}} Y:: f. Y) ] [ (\underline {{A}} Y:: \pi f. Y) \vee f. (E X:: X) ] \ = {\mathrm {I m p l i c a t i o n} } = {\mathrm {I m p l i c a t i o n , d e M o r g a n} } \ [ \rho . (\underline {{A X}}: X) ⇒ (\underline {{A Y}}: \rho : Y) ] [ (\underline {{E Y}}: \rho : Y) ⇒ \rho . (\underline {{E X}}: X) ] \ (E n d o f P r o o f 3. 7) \ \end{array}

The two proofs given next to each other are very similar to each other. This is because the assertions proved are each other's dual. We could have proved only the first one and have reformulated that in terms of $p^$ and $V^$ , which would have yielded

[ (\underline {{E X}}: X \in V ^ {}: f ^ {} X) ⇒ f ^ {} (E X: X \in V ^ {}: X) ]

since this holds for any $V$ and $f^*$ is as monotonic as $f$ , the stars may be omitted. In the sequel we shall no longer give two separate proofs, one for an assertion and one for its dual; often we shall not even take the trouble to formulate the dual assertion.

Where no confusion can arise, it is customary to abbreviate "finitely junctive" as just "junctive". We shall use that convention in the formulation of Lemma 3.8, in which, furthermore, the formulation of the dual property has been left to the reader. Lemma 3.8 strengthens Lemma 3.5 in the sense that one of the latter's implications can be replaced by an equivalence.

Lemma 3.8

$\left( {f\text{is denumerably}\text{conjunctive}}\right) \equiv$ $\left( {f\text{is conjunctive}}\right) ∧ \left( {f\text{is and-continuous}}\right)$

Proof 3.8 In view of Lemma 3.5, we only need to prove here that the right-hand side implies the left-hand side.

\begin{array}{l} f. (\underline {{A}} i: 0 ≤ i: X, i) \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ f. (\underline {{A}} j: 0 ≤ j: (\underline {{A}} i: 0 ≤ i ≤ j: X, i)) \ = {f \mathrm {i s a n d - c o n t i n u o u s a n d} (\underline {{A}} i: 0 ≤ i ≤ j: X. i) (0 ≤ j) \mathrm {i s a n o n - e m p l y , s t r e n g t h e n i n g s e q u e n c e} } \ (\underline {{A}} j: 0 ≤ j: p. (\underline {{A}} i: 0 ≤ i ≤ j: X, i)) \ \begin{array}{l} {= {\underline {{f}} \mathrm {i s c o n j u n c t i v e ,} X. i (0 ≤ i ≤ j) \mathrm {i s n o n - e m p l y ,} f _ {\mathrm {i n i t e}} }} \ {(\underline {{A}} j: 0 ≤ j: (\underline {{A}} i: 0 ≤ i ≤ j: f. (X. i)))} \end{array} \ = {\mathrm {p r e d i c a t e c a l c u l u s} } (\underline {{A}} i: 0 ≤ i: f. (X, i)) \ \end{array}

(End of Proof 3.8)

In the remainder of this chapter we shall consider a number of predicate transformers and derive their junctivity properties; we shall also construct predicate transformers from given ones and investigate to what extent the composite predicate transformer inherits junctivity properties from its components. We shall start with the simpler cases and prove them, even if they can be viewed as special cases of more sophisticated theorems to be dealt with later.

To begin with, we draw attention to

Lemma 3.9

[. true $\equiv$ true] for universally conjunctive $f$ ,and [. false $\equiv$ false] for universally disjunctive $f$ .

Proof 3.9 $= {$ universal quantificatior over empty range $}$ $f.\left( {\underline{\underline{A}}X;\text{ false: }X}\right)$ $= { f\left( x\right) \mid x \in L,x ≠ l$ $= {$ again empty range $}$

p. False $= {$ existential quantificatior over emphy range $}$ $f.\left( {E \times : \text{false:}X}\right)$ $= { F\text{ universally disjunctive}}$ $\left( {E \times : \text{ false: }F \cdot X}\right)$ $= {$ again empty range $}$ false

(End of Proof 3.9)

The above is closely connected to the fact that conjunction distributes over universal quantification and disjunction over existential quantification, provided the range is non-empty. This is to prepare the reader for the circumstance that in quite a few cases below, we find universal junctivity excluded.

Lemma 3.10 Let $f$ be given by $\rho_X \equiv [X]$ ; $f$ is universally conjunctive.

Proof 3.10 We have for any $V$

\begin{array}{l} f. (¬ X: X \in V: X) \ = {\mathrm {d e p . o f} \rho } \ [ (\underline {{A}} X: X \in V: X) ] \ = {\mathrm {i n t e r c h a n g e o f q u a n t i f i c a t i o n s ; r a n g e i s a d o m a i n c o n s t a n t} } \ (\bigtriangleup X: X \in V: [ X ]) \ = {\mathrm {d e f . o p} P } \ (\underline {{A}} X: X \in V: P, X) \ \end{array}

(End of Proof 3.10)

Lemma 3.11 Let $f$ be given by $[f.X \equiv X]$ ; $f$ is universally junctive.

Proof 3.11 We have for any $V$

\begin{array}{l} f. (\underline {{A X}}: X \in V: X) \ = {\mathrm {d e f . o p} \rho } \ (A X: X \in V: X) \ = {\mathrm {d e f . o f} p } \ (\underset {\sim} {A} X: X \in V: P. X) \ \end{array}

Having thus established $f$ 's universal conjunctivity, we can conclude $f$ 's universal disjunctivity from the observation that $f$ is its own conjugate.

(End of Proof 3.11)

Lemma 3.12 Let $f$ be given by $[P.X\equiv Y]$

for arbitrary $r$ , $p$ is unboundedly junctive;

for $\left\lbrack {Y \equiv \text{true}}\right\rbrack ,f$ is universally conjunctive,

for $\left\lbrack {Y \equiv \text{false}}\right\rbrack ,f$ is universally disjunctive.

Proof 3.12 Let $Q$ stand for $A$ or $E$ ; we then observe for any non-empty $V$

\begin{array}{l} f. (\underline {{Q}} X: X \in V: X) \ = {d e f. o p f } \ = {V i s n o n e m p l y } \ (Q X: X \in V: Y) \ = {\mathrm {d e f . o p} f } \ (Q X: X \in V: f. X) \ \end{array}

and, hence $f$ ’s denumerable junctivity has been demonstrated. From the fact that

[ \mathrm {t r u e} \equiv (\exists X: X \in V: \mathrm {t r u e}) ] \mathrm {a n d} [ \mathrm {f a l s e} \equiv (\exists X: X \in V: \mathrm {f a l s e}) ]

also hold for empty $V$ ,the rest of the Lemma follows. (For eP, Pato)

(E n d o f P r o o f 3. 1 2)

Lemma 3.13 Let $f$ be given by $[f.X \equiv X \wedge Y]$ ; for arbitrary $Y$ , $f$ is unboundedly conjunctive and universally disjunctive.

Proof 3.13 We observe for non-empty $V$ and any $W$

\begin{array}{l} p. (\underline {{A X}}: X \in V: X) \ = {\mathrm {d e f . o f} p } \ (A X: X \in V: X) \wedge Y \ = {V i s n o n - e m p l y } \ (A X: X \in V: X \wedge Y) \ = {\mathrm {d e f .} o f V } \ (\underset {\sim} {A} X: X \in V: f. X) \ \end{array}

\begin{array}{l} f. (E X: X \in W: X) \ = {\mathrm {d e f . o p} f } \ (E X: X \in W: X) ∧ Y \ = {\mathrm {d i s t r i b u t i o n} } \ (E X: X \in W; X ∧ Y) \ = {\mathrm {d e f . o f} V } \ (E X: X \in W: P. X) \ \end{array}

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

Lemma 3.14 Let $f$ be given by $\left\lbrack {p,X \equiv g\left( {h,X}\right) }\right\rbrack$ ; $f$ enjoys each type of junctivity that $g$ and share . (Note that ${p}^{f} = {goh}.$ )

Proof 3.14 Let $g$ and $h$ be conjunctive over some $V$ .

\begin{array}{l} f. (\underline {{A}} X: X \in V: X) \ = {\mathrm {d e p . o f} p } \ g. (h. (\underline {{\partial}} X: X \in V: X)) \ = {h \mathrm {i s c o n j u n c t i v e o v e r} V } \ g. (\underset {\sim} {A X}: X \in V: h. X) \ = {g \mathrm {i s c o n j u n c t i v e o v e r} V } \Leftarrow \mathrm {t h i s m o d i v a t i o n i s} \ (\underline {{\underline {{\alpha}}}} X: X \in V: g. (h. X)) \ = {\mathrm {d e p . o p} \rho } \ (\underset {\sim} {A} X: X \in V: f. X) \ \end{array}

Having proved Lemma 3.14 for conjunctivity,

we conclude that it holds for disjunctivity as well

on account of Lemma 3.1 and ${\left\lbrack {P}^{ * }X \equiv {g}^{ * }\left( {h}^{ * }.X\right) \right\rbrack }^{!}$

(End of Proof 3.14)

Lemma 3.15 Let for some bag $M$ of predicate trans.

formers $f$ be given by $\left\lbrack {f.x \equiv \left( {\underline{a}g : g \in M : g.}\right) }\right\rbrack$ ;

f enjoys each type of conjunctivity shared by all elements of $M$

Proof 3.15 Let all elements of $M$ be conjunctive over $V$ .

\begin{array}{l} f. (¬ X: X \in V: X) \ = {\mathrm {d e f . o f} p } \ (\underline {{A}} g: g \in M; g. (\underline {{A}} X: X \in V; X)) \ = {g \mathrm {c o n j u n c t i v e} V } \ \end{array}

\begin{array}{l} (\underline {{A}} g: g \in M: (\underline {{A}} X: X \in V: g. X)) \ = {\mathrm {i n t e r c h a n g e o f q u a n t i p a c i t i o n s} } \ (\underline {{A}} X: X \in V: (\underline {{A}} g: g \in M: g. X)) \ = {\mathrm {d e f . o f} p _ {3} \ (\underline {{A}} X: X \in V: f. X) \ \end{array}

(End of Proof 3.15)

So far, we have considered predicate transformers that were predicate-valued functions of one predicatevalued argument. In the sequel we have to deal also with predicate transformers that are functions of several arguments, $f_{\cdot}X.y$ say. We now have two options: either we write $f_{\cdot}X.y$ and continue to consider $f$ a function of two arguments, or write $f.(X,Y)$ , i.e. view $f$ as a function of one argument which is an ordered pair - in general an ordered m-tuple- of predicates.

We prefer the latter view because it allows a conceptual simplification (be it at the price of some notational brinkmanship, about which more in a moment). The simplification consists in dealing with $n$ -tuples of predicates as with predicates by the rule that logical operators have to be applied element-wise, as illustrated for pairs below:

\begin{array}{l} [ (X, Y) ] \equiv [ X ] \wedge [ Y ] \ [ (X, Y) \equiv (X ^ {\prime}, Y ^ {\prime}) \equiv (X \equiv X ^ {\prime}, Y \equiv Y ^ {\prime}) ] \ \end{array}

\begin{array}{l} [ (X, Y) \vee (X ^ {\prime}, Y ^ {\prime}) \equiv (X \vee X ^ {\prime}, Y \vee Y ^ {\prime}) ] \ [ (X, Y) \wedge (X ^ {\prime}, Y ^ {\prime}) \equiv (X \wedge X ^ {\prime}, Y \wedge Y ^ {\prime}) ] \ [ ¬ (X, Y) \equiv (¬ X, ¬ Y) ] \ [ (X, Y) ⇒ (X ^ {\prime}, Y ^ {\prime}) \equiv (X ⇒ X ^ {\prime}, Y ⇒ Y ^ {\prime}) ] \ [ (X, Y) ≠ (X ^ {\prime}, Y ^ {\prime}) = (X ≠ X ^ {\prime}, Y ≠ Y ^ {\prime}) ] \ \end{array}

Remark on the notational brinkmanship. The first of the above formulae, viz

[ (X, Y) ] \equiv [ X ] \wedge [ Y ]

contains at the left-hand side a square-bracket pair that most definitely clippers from those at the right: if those at the right surround predicates, the pair at the left surrounds a predicate pair. But the comma, viewed as tupling operator, is associative, and if X is an n-tuple, and Y is an m-tuple, (X,Y) is an m+n tuple, with the result that the above formula may contain (at closer inspection or: in a sense) three different pairs of square brackets. (And this is why we did not write the right-hand side as [X ∧ Y]: the formula [X] ∧ [Y] ≡ [X ∧ Y] from the previous chapter only holds under the there still tacit assumption that in [X] ∧ [Y], X and Y are surrounded by equal bracket pairs; the ∧, however, does reflect that we are dealing with universal quantifications.) Those that still prefer to interpret predicates as boolean functions on domains should interpret (X,Y) as a boolean

function on a domain that in the jargon is called the discriminated union of the domains belonging to $X$ and $Y$ respectively. (End of Remark on the notational brinkmanship.)

After the above it will not amaze the reader that it took us quite some time before we had gathered enough courage to dare to push the view that n-tuples of predicates are again predicates. At this stage, mentioning a single fruit must suffice. Having proved something for a pair of predicates is often the induction step for proving the same for n-tuples: the n+1-tuple can be parsed as a pair, of which, for instance, the second one is an n-tuple. We therefore take the liberty to formulate and prove for brevity's sake lemmata only for pairs of predicates, under the addition " (Extendible to n-tuples)".

Quantification is also to be understood to take place element-wise, i.e. for $W$ a bag of predicate pairs

(7) $\left[\left(\underline{Q} X, Y: (X, Y) \in W: (X, Y)\right)\right] =$

((\underline {{Q}} X, Y: (X, Y) \in W: X), (\underline {{Q}} X, Y: (X, Y) \in W: Y)) ]

from which we see that if the range is a domain constant and the term is a predicate pair, the quantification again yields a predicate pair, of which (7) gives the individual components.

Having defined quantifications for which the term is a predicate pair, we can now consider the junctivity of a function, whose value is a predicate pair. The main result about such functions is given by

Lemma 3.16 Let for some predicate transformers $g$ and $h$ ,function $f$ be given by $\left\lbrack {f.X = \left( {g.X,h.X}\right) }\right\rbrack ;f$ enjoys each type of junctivty shared by $g$ and $h$ . (Extendible to n-tuples)

Proof 3.16 Let $g$ and $h$ bejunctive over $\mathbf{bag} V$ of predicates and let $Q$ stand for the corresponding quantification symbol; in the following the range, when omitted, is to be understood to be $X \in V$ .

\begin{array}{l} p. (\underline {{Q}} X: X \in V: X) \ = {\mathrm {d e f . o p} P } \ (g. (\underline {{\varnothing}} X:: X), h. (\underline {{\varnothing}} X:: X)) \ = {g a n d h a r e p r o p e r l y j u n c t i v e } \ (\mathrm {Q X}:: g. x), (\mathrm {Q X}:: h. x)) \ = {(7) } \ (Q X: (g. x, h. x)) \ = {\mathrm {d e f . o f} p } \ (\mathrm {Q X}: \dot {X} \in V: f. X) \ \end{array}

(End of Proof 3.16)

The above lemma 3.16 is our first conceptual gain from considering a predicate pair again a predicate. We get the next one by considering a

function , whose argument is a predicate pair. With $\mathrm{v}$ a bag of predicate pairs and Q the appropriate quantification, we can summarize

(4) and (5) for such a function by

(8) ( $f$ is junctive over $W$ )

\begin{array}{l} [ p. (\underset {\sim} {Q} X, Y: (X, Y) \in W: (X, Y)) \equiv \ (Q X, Y: (X, Y) \in W: f. (X, Y)) ] \ \end{array}

We can now formulate and prove

Lemma 3.17 Let $p$ be given by $[p(X,Y) \equiv X]$ ; $p$ is universally junctive. (Extendible to $n$ -tuples.)

Remark 3.17 is the selector function: it treats one of the components of an n-tuple as function of the n-tuple. (End of Remark.)

Proof 3.17 Define for any bag $W$ of predicate pairs and with $Q$ the appropriate quantification the predicates $Xw$ and $Yw$ by

anol

\begin{array}{l} [ X _ {w} \equiv (\underline {{Q}} X, Y; (X, Y) \in W: X) ] \ [ Y _ {W} \equiv (\underline {{Q}} X, Y: (X, Y) \in W: Y) ] \ f. (\underline {{Q}} X, Y: (X, Y) \in W: (X, Y)) \ = {(7) a n d d e p. o f X w a n d Y w } \ f _ {1} (X _ {w}, Y _ {w}) \ = {\mathrm {d e p . o f} P } \ X _ {w} \ = {\mathrm {d e f . o f} X _ {w} } \ \end{array}

\begin{array}{l} (Q X, Y: (X, Y) \in W: X) \ = {\mathrm {d e f . o f} p } \ (Q X, Y: (X, Y) \in W: P _ {1} (X, Y)) \ \end{array}

(End of Proof 3.17)

Simple as it is, Lemma 3.17 is a very basic one. Now we have the tools to prove Lemma 3.18 in a very different style.

Lemma 3.18 Let $f$ be given by $[f_{\cdot}(X,Y)\equiv g_{\cdot}X\wedge h_{\cdot}Y]$ ; $f$ enjoys each type of conjunctivity shared by $g$ and $h$ . (Extendible to $n$ -tuples.)

Proof 3.18 With $p$ and $q$ defined by

we conclude:

from Lemma 3.17, that $p$ and $q$ are universally junctive; hence, from Lemma 3.14, that $\mathfrak{g} \circ \mathfrak{p}$ is as junctive as $\mathfrak{g}$ and $\mathfrak{h} \circ \mathfrak{q}$ is as junctive as $\mathfrak{h}$ ; and hence, from Lemma 3.15, that $f$ given by $[f_{\cdot}(X,Y)\equiv (gop).(X,Y)\wedge (hog).(X,Y)]$ enjoys each conjunctivity property shared by $g$ and $h$ . But thanks to the definition of $p$ and $q$ , this $f$ is the same one as defined in the Lemma. (End of Proof 3.18)

We may wish to view $\beta .\left( {X,Y}\right)$ primarily as function of $X$ ,the first component of the of the argument,treating $Y$ ,i.e. the other component,

as a for the time not very interesting parameter of the function definition. This leads to the notion of "junctivity in a component (of its argument)".

For a bag V of predicates and function $f$ of a pair of predicates and $Q$ the appropriate quantification,we define

(9) $\left( {f\text{is}\operatorname{junctive}\text{over}V\text{in its first component}}\right) \equiv$

(\underline {{A}} Y: [ f _ {\cdot} ((\underline {{Q}} X: X \in V: X), Y) \equiv (\underline {{Q}} X: X \in V: f _ {\cdot} (X, Y)) ])

(The universal quantification over Y reflects our treating it as "not very interesting".) To stress the contrast to "junctivity in a component" as expressed by (9), we may refer to the junctivity as expressed by (8) as "junctivity in the complete argument".

Our next two lemmata connect a function's junctivity in the complete argument with the junctivity in its components.

Lemma 3.19 Let for some $g$ and $Y$ , function $f$ be given by $[f.X \equiv g.(X,Y)]$ ; $f$ is as junctive as $g$ , universal junctivity excepted. (Extendible to $n$ -tuples.)

or

Lemma 3.19 With the exception of universal junctivity, a function is as junctive in its components as it is in its complete argument.

Proof 3.19 We define functions $p$ and $q$ for some $Y$ by $[p.X \equiv X]$ and $[q.X \equiv Y]$ , and conclude:

From Lemma 3.11, that $p$ is universally junctive:

From Lemma 3.12, that $g$ is unboundedly junctive. Hence, with $h$ defined by $[h.x \equiv (p.x,q.x)]$ ,

we conclude from Lemma 3.16 that $h$ is unboundedly junctive, and hence from Lemma 3.14 that

that ${g}^{0}\partial$ is as junctive as $g$ with the ex-

ception of universal junctivity (i.e. the only junctivity definitely not shared by h). But

\begin{array}{l} (g o h). X \ = {\mathrm {d e f . o p f u n c t i o n a l c o m p o s i t i o n} } \ g. (h, x) \ = {\mathrm {d e f . o p} h } \ g. (p. x, q. x) \ = {\mathrm {d e f . o p} p \mathrm {a n d} q } \ g: (X, Y) \ = {\mathrm {d e p . o p} \rho } \ p. x \ \end{array}

(End of Proof 3.19)

Junctivity in the complete argument is thus largely inherited by the junctivity in the components. In the other direction, the inheritance is much weaker, viz. confined to monotonicity and continuity:

Lemma 3.20 Let function $f$ of a predicate pair be monotonic or continuous in both its components; $f$ enjoys the same junctivity in the complete argument. (Extendible to $n$ -tuples.)

Proof 3.20 We shall prove the theorem for monotonicity and and - continuity. Let $(X, i, Y, i)$ (with $0 ≤ i < N$ or $0 ≤ i$ respectively) be a monotonic sequence. Under the assumption of the appropriate conjunctivity of $f$ in both its components we have to show

(10) $\left\lbrack {f \cdot \left( {{A}{i} : \left( {{X}{i},{Y}{i}}\right) }\right) \equiv \left( {{A}{i} : f \cdot \left( {{X}{i},{Y}{i}}\right) }\right) }\right\rbrack$

To this end we observe to start with

\begin{array}{l} f _ {i} \cdot (A _ {i}: (X, i, Y, i)) \ = {(7), i. e. q u a n t i f i c a t i o n c o m p o n e n t - w i s e } \ f _ {i} ((A _ {i}: X, i), (A _ {j}: Y, j)) \ = {f \mathrm {a p p r o p r a t e l y c o n j u n c t i v e i n i t s f i r s t c o m p o n e n t} } \ = {\mathrm {f} _ {\mathrm {a p p r o p r i a t e l y c o n j u n c t i v e i n i t s s e c o n d c o m p o n e n t}} } \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ (\underset {i, j} {\mathrm {A l}, j}: 0 ≤ i ≤ j: f _ {i} (X _ {i}, Y _ {j})) \wedge (\underset {i, j} {\mathrm {A l}, j}: 0 ≤ j ≤ i: f _ {i} (X _ {i}, Y _ {j})) \ = {\mathrm {t r a n s f o r m i n g t h e d u m m y} } \ (\underline {{A}} i, j: 0 ≤ i ≤ j: f. (X _ {i}, Y _ {j})) \wedge (\underline {{A}} i, j: 0 ≤ i ≤ j: f. (X _ {j}, Y _ {i})) \ \end{array}

We shall now consider the first term of this conjunction in two cases:

(i) sequence $\left( {{X}{i},{Y}{i}}\right)$ is weakening

\begin{array}{l} (\underline {{A}} i, j: 0 ≤ i ≤ j: f. (X _ {i}, Y _ {j})) \ = {\mathrm {n e s t i n g t h e q u a n t i f i c a t i o n s} } \ (\underline {{A}} _ {i}: (\overline {{A}} _ {j}: i \le j: P (X _ {i}, Y _ {j})) \ = {Y, j: \mathrm {w e a k e n i n g a n d} f _ {\mathrm {m o n o t o n i c i n}} 2 ^ {\mathrm {n d}} \mathrm {c o m p o n e n t} } \ (\theta_ {i}: f (X _ {i}, Y _ {i})) \ \end{array}

(ii) sequence (X.i,Y.i) is strengthening

\begin{array}{l} (\exists i, j: 0 ≤ i ≤ j: f. (X _ {i}, Y _ {j})) \ = {\mathrm {n e s t i n g t h e q u a n t i f i c a t i o n s} } \ (\underline {{A}} j: (\underline {{A}} i: 0 ≤ i ≤ j: p. (X _ {i}, Y _ {j}))) \ = {X. i: s t r e n g t h e n i n g a n d f m o n o t o n i c i n i t s 1 ^ {s} t c o m p. 3 \ (A _ {j}: f. (X _ {j}, Y _ {j})) \ \end{array}

In either case, the first term is equivalent to (A i : f. (x. i, y. i)); for reasons of symmetry, the same holds for the second term of the conjunction under consideration, and, combining this with our start, we have demonstrated (10).

(End of Proof 3.20)

Lemmata 3.19 and 3.20 have the following corollaries, which, for the ease of retrieval, are included in the series of Lemmata:

Lemma 3.21 For a function $f$ of an n-tuple of predicates

$\left( {p\text{is monotonistic in its complete argument}}\right) \equiv$

$\left( {p\text{is monotonic in all its components}}\right) .$

Lemma 3.22 For a function $f$ of an n-tuple of predicates

$\left( {p\text{is and-continuous in its complete argument}}\right) \equiv$

$\left( {p\text{is and. continuous in all its components}}\right)$

Lemma 3.23 For a function $f$ of an n-huple of predicates

$\left( {p\text{is or - continuous in its complete argument}}\right) \equiv$

$\left( {f\text{is or-continuous in all its components}}\right) .$

Of these three lemmata, the first one is rather do- vious; it is easily demonstrated in isolation. The last two are less obvious, but they give a hint why con- finuity -a rather complicated property to define! - is a significant notion.

We are now in a position to prove something more about the disjunctive properties of a function that is conjunctively defined:

Lemma 3.24 Let for some or-continuous $g$ and $h$ , predicate transformer $\phi$ be given by $[f.x \equiv g.x \wedge h.x]$ ; $f$ is or-continuous. (Extendible to $n$ -tuples.)

Proof 3.24 Let predicate transformers $p$ and $q$ be given by

\begin{array}{l} [ p. (Y _ {0}, Y _ {1}) \equiv Y _ {0} \wedge Y _ {1} ] \qquad a n d \ [ g. x \equiv (g. x, h. x) ] \ \end{array}

From Lemma 3.13 we conclude that $p$ is or-continuous in both its components and, hence, on account of Lemma 3.23, $p$ is or-continuous in its complements.

From Lemma 3.16 and the or-continuity of $g$ and $h$ we conclude that $g$ is or-continuous.

From the two above conclusions and Lemma 3.14 we conclude that $p^{\circ}q$ is or-continuous. Since $p^{\circ}q = p$ , we have proved the Lemma. $\uparrow \rightarrow$ (End of Proof 3.24) $p^{\circ}q$

Lemma 3.25 Let for some or-continuous $g$ and $h$ , function $f$ be given by $[f.(X,Y)\equiv g.X\wedge h.Y]$ ; $f$ is or-continuous in its complete argument.

Proof3.25 With, for some $Y$ , $k$ given by $\left\lbrack {k \cdot X \equiv h \cdot Y}\right\rbrack$ , we deduce from Lemma 3.12, that $k$ is or-continuous; hence,from Lemma 3.24,that $p$ is or-continuous in its first component; $p$ is similarly or-continuous in its second component. From 3.23,it is or- continuous in its complete argument.(End of Proof 3.25)

For a while, we forget all about predicates and square brackets and consider a simple boolean function $f$ of two arguments, more precisely $f_{x,y}$ is a boolean expression in two variables, each of some type. Let $e$ be a function of those same two variables, but such that $e.x.y$ is an expression of the same type as $x$ . We would like to relate $f.(e.x.y).y$ to $f.x.y$ .

We can do that by using the one-point rule twice, via the intermediate result ${f}_{1} \cdot {x}^{\prime } \cdot y$ that no longer depends on x. With Q standing for either A or E ,we derive from the one point rule

f. x ^ {\prime}. y \equiv (\underline {{Q}} x: x = x ^ {\prime}: f. x. y) \qquad \mathrm {f o r a n y} x ^ {\prime}, y

f. (e \cdot x \cdot y). y \equiv (\underline {{Q}} x ^ {\prime}: x ^ {\prime} = e \cdot x \cdot y: f. x ^ {\prime}. y) \mathrm {f o r a n y} x, y

Combining the two we find (for any $x,y$ )

\mathrm {(1 1)} f. (e. x. y). y \equiv (\underline {{Q}} x ^ {\prime}: x ^ {\prime} = e. x. y: (\underline {{Q}} x: x = x ^ {\prime}: f. x. y))

Denoting $\beta \times \gamma$ by $F$ and e.x.y. ${E}_{1}$ ,

we obtain ${F}_{x}$ . $y$ by substituting ${x}^{\prime }$ in $F$ per $x$ ,

similarly by ${F}_{E}^{x}$ ,and (11) expresses the well-

known property of substitution, that for any $x,y$

F _ {E} ^ {x} \equiv (F _ {x ^ {\prime}} ^ {x}) _ {E} ^ {x ^ {\prime}} (\mathrm {w i t h a f r e s h} x ^ {\prime}).

We can now formulate

Lemma 3.25 Substitution is universally junctive in the

sense that for V an arbitrar bag of boolean

expressions in $x$ and $y$ and" E an expression

in $x$ and $y$ ,

(\underline {{Q}} F: F \in V: F) _ {E} ^ {x} \equiv (\underline {{Q}} F: F \in V: F _ {E} ^ {x}) \mathrm {f o r a n y x , y .}

Proof 3.26 Let $v$ be a bag of functions $f$

such that $F \in V$ ,i.e. ${F}_{X.Y} \in V$ ,is equivalent to

p∈v.

\begin{array}{l} (\underline {{Q}} F: F \in V: F) _ {E} ^ {\times} \ = {\mathrm {d e f . o f} F \mathrm {a n d} E \mathrm {a n d} v } \ (\underline {{Q}} f: f \in v: f. x. y) _ {e. x. y} ^ {x} \ = {(1 2) a s d e f i n i t i o n o f s u b s t i h u l i o n } \ (\underset {\sim} {Q} x ^ {\prime}: x ^ {\prime} = e. x. y: (\underset {\sim} {Q} x: x = x ^ {\prime}: (\underset {\sim} {Q} f: f \in v: f. x. y))) \ = {\mathrm {i n t e r c h a n g e o f q u a n t i f i c a t i o n s} } \ (\underline {{Q}} P: P e v: (\underline {{Q}} x ^ {\prime}: x ^ {\prime} = e. x. y: (\underline {{Q}} x: x = x ^ {\prime}: f. x. y))) \ \end{array}

\begin{array}{l} = {(1 1) } \ (\underline {{Q}} P: P \in v: (P, x. y) _ {e. x. y} ^ {x}) \ = {\mathrm {d e f . o f} \overline {{t}} \mathrm {a n d} E \mathrm {a n d} V } \ (\underline {{Q}} F: F \in V: F _ {E} ^ {x}) \ \end{array}

(End of Proof 3.26)

For the sake of completeness we mention

Lemma 3.27 Substitution distributes over the logical connectives.

Proof 3.27 is left to the reader. (Proving it for the negation is fun!)

In our next chapter we shall transform by substitution predicates $X$ into $X_{E}^{x}$ . such that

[ (\underline {{Q}} X: X \in V; X) _ {E} ^ {} \equiv (Q X: X \in V; X _ {E} ^ {}) ]

in which the square brackets have all the properties of universal quantification over $x$ and $y$ ,as mentioned in Lemma 3.26

Comments on the preceding draft of Chap. 3.

When most of this was written I realized that the treatment of continuity could be simplified by considering not a weakening or a strengthening sequence $X_{i}$ (i30), but a monotonic sequence $X_{i}$ with $i$ ranging over all integers. The distinction between strengthening and weakening then becomes miniscule, viz. no more than transforming the dummy,

$i \mathrel{\text{:=}} - i $ In a next version this unification is easily implemented.

I have made more use of the quantifier $\underline{\mathbf{Q}}$ than I had expected; this is an indication that we should do the same in the previous chapter (certainly in the summary of formulae).

In the proof of lemma 3.8 I used

[ (\underline {{A}} i: o s i: X. i) \equiv (\underline {{A}} j: o s j: (\underline {{A}} i: o s i ≤ j: X. i)) ]

just saying "predicate calculus". If that trick is used more often, the formulae of Chapter 2 should include something to that effect.

I hesitated long between.

(i) talking about ${P}_{0}\left( {X,Y}\right)$ ,its junctivity in its total arguments or in the components (of the argument). (ii) talking about f. X. Y , its multiple junctivity and the junctivity in its arguments.

Actually, when I started on EWD908-16 I had opted for (ii), only switching to (i) while I had already already started. I think I have made the correct choice.

The square brackets cost me trouble. What about $[ ( X , Y ) ] \equiv ([ X ] , [ Y ] )$ ? That would have been true component-wise application. (Note: I sometimes referred to "element-wise"; should be changed to "component-wise" in final version.) The point is that in this chapter I want only to touch on predicate structures and the (potentially)

Cartesian structure of the underlying domain. In the final section on substitution I touched on it again. I could not avoid it, because I wanted to be honest and make clear that e.x.y may depend on the remaining variables (captured by $y$ ).

This raises a point I have not made up my mind about. The Tuesday Afternoon has rightly faub focussed its attention on what they referred to as "propositional functions" for which, instead of the general

[ X \equiv Y ] ⇒ [ P, X \equiv P, Y ]

the much stronger

[ (X \equiv Y) ⇒ (f. X \equiv f. Y) ]

holds. At some stage we shall need functions $f$ for which

[ (u = v) ⇒ (f. u = f. v) ]

holds, with - in the standard interpretation - u and v functions on the domain, but of an other type such that $\left( {u = v}\right)$ is not a domain constant but a full-fledged predicate. And,of course,f.v, Fu might be such things too:

$\left\lbrack {\left( {u = v}\right) ⇒ \left( {{f}{1}u = {f}{1}v}\right) }\right\rbrack$

I need a good term for such u and v - the analogue of our predicates , but now with

values from another type (so that we could write u+Y just as we write XnY). I also need a good adjective for the type of function for which (12) holds. The crucial property is that it distributes over the conditional expression

[ f. (i p B \mathrm {t h e n} u \mathrm {e l s e} v) = i p B \mathrm {t h e n} f. u \mathrm {e l s e} p. v ].

I do not know where to put this. Chapter 2 is already rather long, but when we redo it, it might be the appropriate place. We need it in the proof for the repetition, viz. as soon as our variant function enters the picture; the proof uses the one-point rule in that fancy fashion. (See AvG45/EWD901-7:

\begin{array}{l} [ (\underline {{A}} y: t = y: P \wedge y \mathrm {i n} C \wedge y < x ⇒ Q) ] \ = {\mathrm {o n e - p o i n t} \mathrm {r u l e} } \ [ P \wedge + \ln C \wedge + < x ⇒ Q ] ^ {\prime} \ \end{array}

where the domain constants $y$ in $C$ and $y < x$ are transformed in full. Fledged predicates $t$ in $C$ and $f < x!$

Austin, 23 February 1985

prop. dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1188 United States of America