EWD249 - 11

After the N-th execution of the repeated statement relations (7a) and (7b) are satisfied for n = N. For the N+1st execution to take place, the necessary and sufficient condition is the truth of

                non prop(d)

which, thanks to (7a) for n = N (i.e. d = d_N) means

                non prop(d_N)

leading to condition (7b) being satisfied for n = N + 1. Furthermore, d = d_N and

(2b) leads to        f(d) = d_N+1

so that the net effect of the N+1st execution of the repeated statement

                "d := f(d)"

established the relation

                d = d_N+1

i.e. relation (7a) for N = N + 1 and thus the induction step (7) has been proved.

Now we shall show that the repetition terminates after the k-th execution of the repeated statement. The n-th execution cannot take place for n > k for (on account of 7b) this would imply

                non prop(d_k)

thereby violating (4). When the repetition terminates after the n-th execution of the repeated statement, the necessary and sufficient condition for termination,

viz.            non (non prop(d))

becomes, thanks to (7a)

                prop(d_n)   .                                    (8)

This excludes termination for n < k, as this would violate (5). As a result the repetition will terminate with n = k, so that (3) follows from (7a), (4) follows from (8) and (5) follows from (7b). Which terminates our proof.

Before turning our attention away from this example illustrating the use of mathematical induction as a pattern of reasoning, I should like to add some remarks, because I have the uneasy feeling that by now some of my readers -in particular experienced and competent programmers- will be terribly irritated, viz. those