#|
Copyright (C) 1994 by Robert S. Boyer and J Strother Moore.  All Rights
Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Robert S. Boyer and J Strother Moore PROVIDE ABSOLUTELY NO WARRANTY.  THE
EVENT SCRIPT IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS
OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO
THE QUALITY AND PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT
PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR
CORRECTION.
IN NO EVENT WILL Robert S. Boyer or J Strother Moore BE LIABLE TO YOU FOR ANY
DAMAGES, ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR
CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT
(INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE
OR LOSSES SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE
POSSIBILITY OF SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#

Event: Start with the library "proveall" using the compiled version.

Event: For efficiency, compile those definitions not yet compiled.

Definition: bc (n, m) = if m ≃ 0 then 1

elseif n < m then 0

else bc (n − 1, m) + bc (n − 1, m − 1) endif

Event: Disable eval$.

Theorem: for-append-sum for (x,

append (a, b), test,

'sum,

body, alist)

= (for (x, a, test,

'sum,

body, alist)

+ for (x, b, test,

    'sum,

body, alist))

Theorem: bc-x-x1 bc (x, 1 + x) = 0

Theorem: bc-x-x bc (x, x) = 1

Theorem: from-to-opens-at-btm from-to (0, b) = cons (0, from-to (1, b))

Theorem: member-from-to (i ∈ from-to (a, b)) = ((i ∈ N) ∧ (i ≮ a) ∧ (b ≮ i))

Theorem: for-sum-plus for (i,

range, test,

'sum,

list ('plus, a, b), alist)

= (for (i, range, test,

'sum,

a, alist)

+ for (i, range, test,

           'sum,

b, alist))

Theorem: times-plus-distributivity-again ((a + b) ∗ c) = ((a ∗ c) + (b ∗ c))

Theorem: difference-sub1-2 ((i ≄ 0) ∧ (x ≮ i)) → ((x − (i − 1)) = (1 + (x − i)))

Theorem: out-with-the-factors ((one ≃ nil) ∧ (one ≠ var)) → (for (var,

range, condition,

        'sum,

list ('times, one, two), alist)

= (eval$ (true, one, alist)

∗ for (var, range, condition,

                'sum,

two, alist)))

Theorem: lessp-1 (i < 1) = (i ≃ 0)

Theorem: lessp-crock1 (i ≄ 0) → ((x < (i − 1)) = ((x < i) ∧ (fix (x) ≠ (i − 1))))

Theorem: zero-sum for (i,

l, cond,

   'sum,
   ''0,

alist)

= 0

Theorem: shift-indicial-up-crock (n ≄ 0) → (for i in from-to (1, n)

sum exp (a, i) ∗ (bc (x, i − 1) ∗ exp (b, x − i)) endfor = for i in from-to (0, n − 1) sum exp (a, 1 + i)

∗ (bc (x, i) ∗ exp (b, x − (1 + i))) endfor)

Theorem: goal1 ((x ∈ N) ∧ (x ≠ 0) ∧ (1 ≠ x) ∧ ((x − 1) ≠ 0)) → ((a ∗ for i in from-to (1, x − 1)

sum bc (x, i) ∗ (exp (a, i) ∗ exp (b, x − i)) endfor) = (a ∗ (b ∗ for i in from-to (1, x − 1) sum bc (x, i)

∗ (exp (a, i) ∗ exp (b, (x − 1) − i)) endfor)))

Theorem: newton exp (a + b, n) = for i in from-to (0, n)

sum bc (n, i) ∗ exp (a, i) ∗ exp (b, n − i) endfor

Index

bc, 1–4 bc-x-x, 2 bc-x-x1, 2 difference-sub1-2, 3 exp, 3, 4 for-append-sum, 1 for-sum-plus, 2 from-to, 2–4 from-to-opens-at-btm, 2 goal1, 4 lessp-1, 3 lessp-crock1, 3 member-from-to, 2 newton, 4 out-with-the-factors, 3 shift-indicial-up-crock, 3 times-plus-distributivity-again, 3 zero-sum, 3