**A postScript to EWD755.**

While presenting my proof of Theorem 2 in EWD755 I had forgotten my own preaching (in EWD731): with explicitly named predicates a more symmetric presentation is possible. With

C n p = | n is the product of a bag of primes containing p |

D n p = | n is the product of a bag of primes not containing p |

we have (as obviously as before) for
positive integers `p`, `x`, and `y` :

1) | ¬(prime p) ∨ ¬(p|(x.y)) ∨ (C(x.y) p) |

2) | p|x ∨ p|y ∨ (D(x.y) p) |

3) | ¬(C(x.y) p) ∨ ¬(D(x.y) p) ∨ ¬(UPF(x.y)) |

* *

*

Consider, for `n` ≥` 1, the following program
`

if |
n = 1 → bag := ∅ ⫿ n >1 → bag := {n} fi; |

do |
bag contains a composite multiple → |

replace each occurrence of the largest composite multiple c in bag by the multiples x and y, where x.y = c | |

od |

The repetition leaves the product of the numbers in `bag` equal to `n`. On account of (3') from
EWD755 —which is, of
course, again needed— the lowest upper bound for composite multiples in `bag` can be taken as
variant function, and termination is
guaranteed. This proof is more constructive; Euclid would have liked it (if he did not
prove it that way!).

Plantaanstraat 5 | 23 October 1980 |

5671 AL NUENEN | prof. dr. Edsger W. Dijkstra |

The Netherlands | Burroughs Research Fellow |

Transcribed by Martin P.M. van der Burgt

Last revision