November 10, 2000 November 10, 2000

The source for this problem is Donald Knuth, The Art of Computer Programming, Volume 1 Fundamental Algorithms, Third Edition. His Example 2., page 30 begins with a proof that
 nå i = 0 iå j = 0 aiaj = nå i = 0 nå j = i aiaj  .

Its proof is in the vein of the fourth problem on the fourth assignment. It is formulated in the notation of the text as
 (+i | 0 £ i £ n:(+j | 0 £ j £ i : a[i]a[j])) = (+i | 0 £ i £ n:(+j | i £ j £ n : a[i]a[j])) .

 (+i | 0 £ i £ n:(+j | 0 £ j £ i : a[i]a[j]))
 =

 (8.20), j d.n.o.f. in 0 £ i £ n.

 (+i,j | (0 £ i £ n) Ù(0 £ j £ i) : a[i]a[j])
 =

 Axiom, (*x,y | P:Q ) = (*y,x | P:Q )

 (+j,i | (0 £ i £ n) Ù(0 £ j £ i) : a[i]a[j])
 =

á
 Lemma: (0 £ i £ n) Ù(0 £ j £ i) º (0 £ j £ n) Ù(j £ i £ n),
 Leibniz 8.12. Proof of Lemma appears below.

ñ
 (+j,i | (0 £ j £ n) Ù(j £ i £ n) : a[i]a[j])
 =

 (8.20), i d.n.o.f. in 0 £ j £ n.

 (+j | 0 £ j £ n:( +i | j £ i £ n : a[i]a[j]))
 =

 (8.21) applied four times (see below)

 (+i | 0 £ i £ n:( +j | i £ j £ n : a[j]a[i]))
 =

 Arithmetic, a[j]a[i] = a[i]a[j]

 (+i | 0 £ i £ n:( +j | i £ j £ n : a[i]a[j]))
Now for the proof of the Lemma:
 (0 £ i £ n) Ù(0 £ j £ i)
 =

 Notation

 (0 £ i) Ù(i £ n) Ù(0 £ j) Ù(j £ i)
 =

á
 |- (j £ i)Ù(i £ n) Þ (j £ n) by (15.41)(d).
 Apply (3.60) to obtain |- (j £ i)Ù(i £ n) º (j £ i)Ù(i £ n)Ù(j £ n).

ñ
 (0 £ i) Ù(i £ n) Ù(0 £ j) Ù(j £ i)Ù(j £ n)
 =

á
 |- (0 £ j) Ù(j £ i) Þ (0 £ i) by (15.41)(d).
 Apply (3.60) to obtain |- (0 £ i) Ù(0 £ j) Ù(j £ i) º (0 £ j) Ù(j £ i) .

ñ
 (i £ n) Ù(0 £ j) Ù(j £ i)Ù(j £ n)
 =

 (3.36), (3.37)

 (0 £ j) Ù(j £ n) Ù(j £ i) Ù(i £ n)
 =

 Notation

 (0 £ j £ n) Ù(j £ i £ n)
The proof uses (15.41)(d), the transitivity property for £ .

For the step which uses (8.21), choose k and l fresh variables. Then apply (8.21) to rename the dummy i to k and afterwards (8.21) to rename the dummy j to l. As there are no free occurrences of i or j now ``reverse'' by renaming k to j and then l to i. To formalize write down (8.21) in each case and apply Transitivity three times.

We have already discussed (8.13) Axiom, Empty Range. For (8.14) Axiom, One-point rule observe that there is a restriction that there are no free occurrences of the object variable x in the expression E. The following examples show what can happen if one ignores this restriction:

Consider

(+x | x = x2-2x+2:x) = x2-2x +2
and
("| x = x2-x +1: x = 1) º (x2-x+1 = 1)

Show that neither are theorems by finding an interpretation for which each is false.

File translated from TEX by TTH, version 2.60.
On 9 Nov 2000, 21:04.