Let `r` be a left-founded relation, i.e. let

(0) 〈 ∀`x` :: [`x` ⇒ `r` ; `x`] ⇒ [ `x` ⇒ false ] 〉 ;

an appeal to what is called "mathematical induction" means that a proof obligation of the form

(1) [ `x` ⇒ false ]

is replaced by the formally weaker obligation

(2) [`x` ⇒ `r` ; `x`] or [ `x` ∧ ¬ ( `r` ; `x` ) ⇒ false ] .

Proving (2) by mathematical induction leads to the (subsequently simplified) obligation

(3) [ `x` ∧ ¬ ( `r` ; `x` ) ⇒ `r`; ( `x` ∧ ¬ ( `r` ; `x` ))]

≡ {shunting}

[`x` ⇒ `r` ; `x` ∨ `r` ; ( `x` ∧ ¬ ( `r` ; `x` ))]

≡ { ; monotonic in 2nd argument}

[`x` ⇒ `r` ; `x`]

i.e. (2)! The decision to prove by mathematical induction is idempotent. With thanks to the ETAC.

Nuenen, 17 December 1996

prof.dr. Edsger W.Dijkstra

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712-1188, USA