EWD756

---

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))

Theorem 2 now follows by the standard inference rule. Note that for 1) and for 2) we need Theorem 0. (In EWD755 I failed to mention this.)

*              *
*

The above I regard as a different (and preferable) presentation of the same proof as in EWD755. The following alternative proof of theorem 0 from EWD755 I consider (perhaps somewhat arbitrarily) different.

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 10-Nov-2015 .