__For the record: ETAC and the couples __

ETAC learned the following problem from JLA van de Snepscheut (who probably heard it from J Misra). Of a finite number of couples we are told the following two things:

(i) | the oldest man is as old as the oldest woman |

(ii) | if two couples swap wives, the youngest of the one new couple is as young as the youngest of the other new couple. |

Show that in each couple, man and woman have the same age.

The ETAC came with the following solution. Let dummies `x`, `y` range over the couples; let the ages of man and woman of couple `x` be denoted by `m`.`x` and `f`.`x` respectively. Our proof obligation is then

(0) (__A__`x` :: `m`.`x` = `f`.`x`)

while we have been given

(1) (↑`y` :: `m`.`y`) = (↑`y` :: `f`.`y`) and

(2) (__A__`x`, `y` :: `m`.`x`↓`f`.`y` = `f`.`x`↓`m`.`y`)

Note that (ii) states (2) with the range `x`≠`y`, but that the range can be extended to include `x`=`y`.

We observe for any `x
`

`m`.`x` = `f`.`x`

= { ↑↓ calculus: `p` ≤ `p`↑`q` and `a` ≤ `b` ≡ `a` = `a`↓`b`}

`m`.`x`↓(↑`y` :: `m`.`y`) = `f`.`x`↓(↑`y` :: `f`.`y`)

= {(1)}

`m`.`x`↓(↑`y` :: `f`.`y`) = `f`.`x`↓(↑`y` :: `m`.`y`)

= {↑↓ calculus: ↓ distributes over ↑}

(↑`y` :: `m`.`x`↓`f`.`y`) = (↑`y` :: `f`.`x`↓`m`.`y`)

= {(2)}

true ,

and thus (0) has been proved.

The first step is *not* surprising: in order to use (1) and (2), ↑ and ↓ *have* to be introduced into the calculation.

Nuenen, 29 June 1991

prof.dr. Edsger W.Dijkstra,

Department of Computer Sciences,

The University of Texas at Austin,

Austin, TX 78712–1188

USA

Transcribed by Guy Haworth

Revised