#|
Copyright (C) 1994 by John Cowles.  All Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
John Cowles PROVIDES 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 John Cowles 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.

;            Sums of the Fibonacci Numbers
;                 by John R. Cowles
;                    Computer Science Department
;                    University of Wyoming
;                    Laramie, Wyoming 82071

; This file naturally belongs over in the cowles subdirectory
; rather than in the basic subdirectory, but we put it here because
; it depends upon proveall, proveall is long, and we choose not
; to put operating system/directory syntax information into these files.
; This event list contains several interesting theorems
; about the Fibonacci numbers such as

; The SUM, from k=0 to k=n, of fib( k ) = fib( n+2 ) - 1.
;
; The SUM, from k=0 to k=n, of fib( 2*k+1 ) = fib( 2*n+2 ).
; Here fib( i ) is the ith Fibonacci number.

Definition: fib (n) = if n ≃ 0 then 0

elseif n = 1 then 1

else fib (n − 1) + fib ((n − 1) − 1) endif

Definition: nbr-calls-fib (n) = if n ≃ 0 then 1

elseif n = 1 then 1

else 1 + (nbr-calls-fib (n − 1) + nbr-calls-fib ((n − 1) − 1)) endif

Definition: nbr-plus-fib (n) = if n ≃ 0 then 0

elseif n = 1 then 0

else 1 + (nbr-plus-fib (n − 1) + nbr-plus-fib ((n − 1) − 1)) endif

Theorem: nbr-calls-fib&fib (1 + nbr-calls-fib (n)) = (2 ∗ fib (1 + n))

Theorem: nbr-calls-fib=fib nbr-calls-fib (n) = ((2 ∗ fib (1 + n)) − 1)

Theorem: nbr-plus-fib&fib (1 + nbr-plus-fib (n)) = fib (1 + n)

Theorem: nbr-plus-fib=fib nbr-plus-fib (n) = (fib (1 + n) − 1)

Definition: sum-fib<k> (n) = if n ≃ 0 then 0

else sum-fib<k> (n − 1) + fib (n) endif

Theorem: sum-fib<k>&fib (1 + sum-fib<k> (n)) = fib (1 + (1 + n))

Theorem: sum-fib<k>=fib sum-fib<k> (n) = (fib (1 + (1 + n)) − 1)

Theorem: sum-fib<k>=nbr-plus-fib sum-fib<k> (n) = nbr-plus-fib (1 + n)

Definition: sum-fib<2k> (n) = if n ≃ 0 then 0

else sum-fib<2k> (n − 1) + fib (2 ∗ n) endif

Theorem: sum-fib<2k>&fib (1 + sum-fib<2k> (n)) = fib (1 + (2 ∗ n))

Theorem: sum-fib<2k>=fib sum-fib<2k> (n) = (fib (1 + (2 ∗ n)) − 1)

Definition: sum-fib<2k+1> (n) = if n ≃ 0 then 1

else sum-fib<2k+1> (n − 1) + fib (1 + (2 ∗ n)) endif

Theorem: sum-fib<2k+1>=fib sum-fib<2k+1> (n) = fib (1 + (1 + (2 ∗ n)))

Definition: sum-fib<3k> (n) = if n ≃ 0 then 0

else sum-fib<3k> (n − 1) + fib (3 ∗ n) endif

Theorem: sum-fib<3k>&fib (1 + (2 ∗ sum-fib<3k> (n))) = fib (1 + (1 + (3 ∗ n)))

Theorem: sum-fib<3k>&fib-1 (2 ∗ sum-fib<3k> (n)) = (fib (1 + (1 + (3 ∗ n))) − 1)

Theorem: sum-fib<3k>=fib sum-fib<3k> (n) = ((fib (1 + (1 + (3 ∗ n))) − 1) ÷ 2)

Definition: sum-fib<3k+1> (n) = if n ≃ 0 then 1

else sum-fib<3k+1> (n − 1) + fib (1 + (3 ∗ n)) endif

Theorem: sum-fib<3k+1>&fib (2 ∗ sum-fib<3k+1> (n)) = fib (1 + (1 + (1 + (3 ∗ n))))

Theorem: sum-fib<3k+1>=fib sum-fib<3k+1> (n) = (fib (1 + (1 + (1 + (3 ∗ n)))) ÷ 2)

Definition: sum-fib<3k+2> (n) = if n ≃ 0 then 1

else sum-fib<3k+2> (n − 1) + fib (1 + (1 + (3 ∗ n))) endif

Theorem: sum-fib<3k+2>&fib (1 + (2 ∗ sum-fib<3k+2> (n))) = fib (1 + (1 + (1 + (1 + (3 ∗ n)))))

Theorem: sum-fib<3k+2>&fib-1 (2 ∗ sum-fib<3k+2> (n)) = (fib (1 + (1 + (1 + (1 + (3 ∗ n))))) − 1)

Theorem: sum-fib<3k+2>=fib sum-fib<3k+2> (n) = ((fib (1 + (1 + (1 + (1 + (3 ∗ n))))) − 1) ÷ 2)

Theorem: fib<2n+1>=fib<n>&fib<2n+2>=fib<n> (fib (1 + (2 ∗ n)) = ((fib (n) ∗ fib (n)) + (fib (1 + n) ∗ fib (1 + n)))) ∧ (fib (1 + (1 + (2 ∗ n)))

= ((fib (n) ∗ fib (1 + n)) + (fib (1 + n) ∗ fib (1 + (1 + n)))))

Theorem: fib<2n+1>=fib<n> fib (1 + (2 ∗ n)) = ((fib (n) ∗ fib (n)) + (fib (1 + n) ∗ fib (1 + n)))

Theorem: fib<2n+2>=fib<n> fib (1 + (1 + (2 ∗ n))) = ((fib (n) ∗ fib (1 + n)) + (fib (1 + n) ∗ fib (1 + (1 + n))))

Definition: sum-fib<4k> (n) = if n ≃ 0 then 0

else sum-fib<4k> (n − 1) + fib (4 ∗ n) endif

Definition: sum-fib<4k+1> (n) = if n ≃ 0 then 1

else sum-fib<4k+1> (n − 1) + fib (1 + (4 ∗ n)) endif

Definition: sum-fib<4k+2> (n) = if n ≃ 0 then 1

else sum-fib<4k+2> (n − 1) + fib (1 + (1 + (4 ∗ n))) endif

Definition: sum-fib<4k+3> (n) = if n ≃ 0 then 2

else sum-fib<4k+3> (n − 1) + fib (1 + (1 + (1 + (4 ∗ n)))) endif Theorem: times-4=times-2-2 (4 ∗ n) = (2 ∗ 2 ∗ n)

Theorem: fib<4n+1>=fib<2n> fib (1 + (4 ∗ n)) = ((fib (2 ∗ n) ∗ fib (2 ∗ n))

+ (fib (1 + (2 ∗ n)) ∗ fib (1 + (2 ∗ n))))

Theorem: sum-fib<4k+1>=fib<2n> sum-fib<4k+1> (n) = (fib (1 + (2 ∗ n)) ∗ fib (1 + (1 + (2 ∗ n))))

Theorem: fib<4n+2>=fib<2n> fib (1 + (1 + (4 ∗ n))) = ((fib (2 ∗ n) ∗ fib (1 + (2 ∗ n)))

+ (fib (1 + (2 ∗ n)) ∗ fib (1 + (1 + (2 ∗ n)))))

Theorem: sum-fib<4k+2>=fib<2n> sum-fib<4k+2> (n) = (fib (1 + (1 + (2 ∗ n))) ∗ fib (1 + (1 + (2 ∗ n))))

Theorem: fib<4n+3>=fib<2n> fib (1 + (1 + (1 + (4 ∗ n)))) = ((fib (1 + (2 ∗ n)) ∗ fib (1 + (2 ∗ n)))

+ (fib (1 + (1 + (2 ∗ n))) ∗ fib (1 + (1 + (2 ∗ n)))))

Theorem: sum-fib<4k+3>=fib<2n> sum-fib<4k+3> (n) = (fib (1 + (1 + (1 + (2 ∗ n)))) ∗ fib (1 + (1 + (2 ∗ n))))

Theorem: fib<2n>=fib<n> (0 < n) → (fib (2 ∗ n)

= ((fib (n − 1) ∗ fib (n)) + (fib (n) ∗ fib (1 + n))))

Theorem: fib<4n>=fib<2n> (0 < n) → (fib (4 ∗ n)

= ((fib ((2 ∗ n) − 1) ∗ fib (2 ∗ n))

+ (fib (2 ∗ n) ∗ fib (1 + (2 ∗ n)))))

Theorem: sum-fib<4k>=fib<2n> sum-fib<4k> (n) = (fib (2 ∗ n) ∗ fib (1 + (1 + (2 ∗ n))))

Index

fib, 2–5 fib<2n>=fib<n>, 5 fib<2n+1>=fib<n>, 4 fib<2n+1>=fib<n>&fib<

2n+2>=fib<n>, 4 fib<2n+2>=fib<n>, 4 fib<4n>=fib<2n>, 5 fib<4n+1>=fib<2n>, 5 fib<4n+2>=fib<2n>, 5 fib<4n+3>=fib<2n>, 5

nbr-calls-fib, 2 nbr-calls-fib=fib, 2 nbr-calls-fib&fib, 2 nbr-plus-fib, 2, 3 nbr-plus-fib=fib, 2 nbr-plus-fib&fib, 2

sum-fib<2k>, 3 sum-fib<2k>=fib, 3 sum-fib<2k>&fib, 3 sum-fib<2k+1>, 3 sum-fib<2k+1>=fib, 3 sum-fib<3k>, 3 sum-fib<3k>=fib, 3 sum-fib<3k>&fib, 3 sum-fib<3k>&fib-1, 3 sum-fib<3k+1>, 3 sum-fib<3k+1>=fib, 3 sum-fib<3k+1>&fib, 3 sum-fib<3k+2>, 4 sum-fib<3k+2>=fib, 4 sum-fib<3k+2>&fib, 4 sum-fib<3k+2>&fib-1, 4 sum-fib<4k>, 4, 5 sum-fib<4k>=fib<2n>, 5 sum-fib<4k+1>, 4, 5 sum-fib<4k+1>=fib<2n>, 5 sum-fib<4k+2>, 4, 5 sum-fib<4k+2>=fib<2n>, 5 sum-fib<4k+3>, 4, 5 sum-fib<4k+3>=fib<2n>, 5 sum-fib<k>, 2, 3 sum-fib<k>=fib, 2 sum-fib<k>=nbr-plus-fib, 3 sum-fib<k>&fib, 2

times-4=times-2-2, 5