A supplement to EWD1002

A supplement to EWD1002

For an $p$ with a natural argument, "the $p.i$ form a weakening sequence" means

$\left( {84}\right)$ $\left( {\underline{A}i,j : 0 \leq i < j : \left\lbrack {{f}{i} \Rightarrow {f}{j}}\right\rbrack }\right)$

For a weakening sequence that is non-empty -i.e. such that $i = 0$ is included in the range - we have (not surprisingly)

$$ [ (\underset {-} {A} i: f. i) \equiv f. 0 ] $$

Proof We observe for any non-empty weakening sequence $\mathcal{P}$

$$ \begin{array}{l} (\underline {{A}} i: \underline {{P}}. i) \ = {i: i = 0; i = 0 \mathrm {i n} r a n g e } \ = {\mathrm {r a n g e n o n - e m p l y} } (\underline {{A}} i: f. 0 \land f. i) \ \begin{array}{r l} {=} & {{(8 4) \mathrm {w i t h} i := 0, \mathrm {w h i c h i s i n r a n g e ; p r e d . c a l c . :}} \ & {(\underline {{A}} j: [ f. 0 \land f. j \equiv f. 0 ]) }} \end{array} \ (\underline {{A}} i: \rho_ {0} ^ {\prime}) \ = {r a n g e n o n - e m p l y } \ \end{array} $$

(End of Proof.)

Austn, 23 March 1987

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