\documentstyle[makeidx]{article}
\makeindex
%\setlength{\oddsidemargin}{.5in}
%\setlength{\evensidemargin}{.5in}
%\setlength{\textwidth}{5.8in}
\begin{document}
%\setlength{\parindent}{0pt}
%\newcounter{bean}
%\begin{list}{\arabic{bean}.}{\usecounter{bean}\setlength{\leftmargin}{0pt}\setlength{\rightmargin}{0pt}\setlength{\listparindent}{20pt}\setlength{\parsep}{5pt}}
%\item[]

\begin{verbatim}#|

 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.''

|#

\end{verbatim}
\noindent{\sc Event}:   Start with the library {\tt{"proveall"}} using the compiled version.

\addvspace{18pt}

\begin{verbatim};            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.
 
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{fib} \\  
\=\+{\rm{fib}}\,({\it{n\/}})\index{fib} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{n\/}} $=$ {\tt{1}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{fib}}\,({\it{n\/}} $-\;1$)\index{fib} $+$ {\rm{fib}}\,(({\it{n\/}} $-\;1$) $-\;1$)\index{fib}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{nbr-calls-fib} \\  
\=\+{\rm{nbr-calls-fib}}\,({\it{n\/}})\index{nbr-calls-fib} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf elseif }{\it{n\/}} $=$ {\tt{1}}$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }$1\;+$ ({\rm{nbr-calls-fib}}\,({\it{n\/}} $-\;1$)\index{nbr-calls-fib} $+$ {\rm{nbr-calls-fib}}\,(({\it{n\/}} $-\;1$) $-\;1$)\index{nbr-calls-fib})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{nbr-plus-fib} \\  
\=\+{\rm{nbr-plus-fib}}\,({\it{n\/}})\index{nbr-plus-fib} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf elseif }{\it{n\/}} $=$ {\tt{1}}$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }$1\;+$ ({\rm{nbr-plus-fib}}\,({\it{n\/}} $-\;1$)\index{nbr-plus-fib} $+$ {\rm{nbr-plus-fib}}\,(({\it{n\/}} $-\;1$) $-\;1$)\index{nbr-plus-fib})$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nbr-calls-fib\&fib \\ \index{nbr-calls-fib\&fib}
($1\;+$ {\rm{nbr-calls-fib}}\,({\it{n\/}})\index{nbr-calls-fib}) $=$ ({\tt{2}} $*$ {\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nbr-calls-fib=fib \\ \index{nbr-calls-fib=fib}
{\rm{nbr-calls-fib}}\,({\it{n\/}})\index{nbr-calls-fib} $=$ (({\tt{2}} $*$ {\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib}) $-\;1$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  nbr-plus-fib\&fib \\ \index{nbr-plus-fib\&fib}
($1\;+$ {\rm{nbr-plus-fib}}\,({\it{n\/}})\index{nbr-plus-fib}) $=$ {\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib}
\end{tabbing}                

\begin{tabbing}{\sc Theorem}:  nbr-plus-fib=fib \\ \index{nbr-plus-fib=fib}
{\rm{nbr-plus-fib}}\,({\it{n\/}})\index{nbr-plus-fib} $=$ ({\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib} $-\;1$)
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sum-fib$<$k$>$} \\  
\=\+{\rm{sum-fib$<$k$>$}}\,({\it{n\/}})\index{sum-fib$<$k$>$} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{sum-fib$<$k$>$}}\,({\it{n\/}} $-\;1$)\index{sum-fib$<$k$>$} $+$ {\rm{fib}}\,({\it{n\/}})\index{fib}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-fib$<$k$>$\&fib \\ \index{sum-fib$<$k$>$\&fib}
($1\;+$ {\rm{sum-fib$<$k$>$}}\,({\it{n\/}})\index{sum-fib$<$k$>$}) $=$ {\rm{fib}}\,($1\;+$ ($1\;+$ {\it{n\/}}))\index{fib}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-fib$<$k$>$=fib \\ \index{sum-fib$<$k$>$=fib}
{\rm{sum-fib$<$k$>$}}\,({\it{n\/}})\index{sum-fib$<$k$>$} $=$ ({\rm{fib}}\,($1\;+$ ($1\;+$ {\it{n\/}}))\index{fib} $-\;1$)
\end{tabbing} 

\begin{tabbing}{\sc Theorem}:  sum-fib$<$k$>$=nbr-plus-fib \\ \index{sum-fib$<$k$>$=nbr-plus-fib}
{\rm{sum-fib$<$k$>$}}\,({\it{n\/}})\index{sum-fib$<$k$>$} $=$ {\rm{nbr-plus-fib}}\,($1\;+$ {\it{n\/}})\index{nbr-plus-fib}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sum-fib$<$2k$>$} \\  
\=\+{\rm{sum-fib$<$2k$>$}}\,({\it{n\/}})\index{sum-fib$<$2k$>$} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{sum-fib$<$2k$>$}}\,({\it{n\/}} $-\;1$)\index{sum-fib$<$2k$>$} $+$ {\rm{fib}}\,({\tt{2}} $*$ {\it{n\/}})\index{fib}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-fib$<$2k$>$\&fib \\ \index{sum-fib$<$2k$>$\&fib}
($1\;+$ {\rm{sum-fib$<$2k$>$}}\,({\it{n\/}})\index{sum-fib$<$2k$>$}) $=$ {\rm{fib}}\,($1\;+$ ({\tt{2}} $*$ {\it{n\/}}))\index{fib}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-fib$<$2k$>$=fib \\ \index{sum-fib$<$2k$>$=fib}
{\rm{sum-fib$<$2k$>$}}\,({\it{n\/}})\index{sum-fib$<$2k$>$} $=$ ({\rm{fib}}\,($1\;+$ ({\tt{2}} $*$ {\it{n\/}}))\index{fib} $-\;1$)
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sum-fib$<$2k+1$>$} \\  
\=\+{\rm{sum-fib$<$2k+1$>$}}\,({\it{n\/}})\index{sum-fib$<$2k+1$>$} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{sum-fib$<$2k+1$>$}}\,({\it{n\/}} $-\;1$)\index{sum-fib$<$2k+1$>$} $+$ {\rm{fib}}\,($1\;+$ ({\tt{2}} $*$ {\it{n\/}}))\index{fib}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-fib$<$2k+1$>$=fib \\ \index{sum-fib$<$2k+1$>$=fib}
{\rm{sum-fib$<$2k+1$>$}}\,({\it{n\/}})\index{sum-fib$<$2k+1$>$} $=$ {\rm{fib}}\,($1\;+$ ($1\;+$ ({\tt{2}} $*$ {\it{n\/}})))\index{fib}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sum-fib$<$3k$>$} \\  
\=\+{\rm{sum-fib$<$3k$>$}}\,({\it{n\/}})\index{sum-fib$<$3k$>$} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{sum-fib$<$3k$>$}}\,({\it{n\/}} $-\;1$)\index{sum-fib$<$3k$>$} $+$ {\rm{fib}}\,({\tt{3}} $*$ {\it{n\/}})\index{fib}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-fib$<$3k$>$\&fib \\ \index{sum-fib$<$3k$>$\&fib}
($1\;+$ ({\tt{2}} $*$ {\rm{sum-fib$<$3k$>$}}\,({\it{n\/}})\index{sum-fib$<$3k$>$})) $=$ {\rm{fib}}\,($1\;+$ ($1\;+$ ({\tt{3}} $*$ {\it{n\/}})))\index{fib}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-fib$<$3k$>$\&fib-1 \\ \index{sum-fib$<$3k$>$\&fib-1}
({\tt{2}} $*$ {\rm{sum-fib$<$3k$>$}}\,({\it{n\/}})\index{sum-fib$<$3k$>$}) $=$ ({\rm{fib}}\,($1\;+$ ($1\;+$ ({\tt{3}} $*$ {\it{n\/}})))\index{fib} $-\;1$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-fib$<$3k$>$=fib \\ \index{sum-fib$<$3k$>$=fib}
{\rm{sum-fib$<$3k$>$}}\,({\it{n\/}})\index{sum-fib$<$3k$>$} $=$ (({\rm{fib}}\,($1\;+$ ($1\;+$ ({\tt{3}} $*$ {\it{n\/}})))\index{fib} $-\;1$) $\div$ {\tt{2}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sum-fib$<$3k+1$>$} \\  
\=\+{\rm{sum-fib$<$3k+1$>$}}\,({\it{n\/}})\index{sum-fib$<$3k+1$>$} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{sum-fib$<$3k+1$>$}}\,({\it{n\/}} $-\;1$)\index{sum-fib$<$3k+1$>$} $+$ {\rm{fib}}\,($1\;+$ ({\tt{3}} $*$ {\it{n\/}}))\index{fib}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-fib$<$3k+1$>$\&fib \\ \index{sum-fib$<$3k+1$>$\&fib}
({\tt{2}} $*$ {\rm{sum-fib$<$3k+1$>$}}\,({\it{n\/}})\index{sum-fib$<$3k+1$>$}) $=$ {\rm{fib}}\,($1\;+$ ($1\;+$ ($1\;+$ ({\tt{3}} $*$ {\it{n\/}}))))\index{fib}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-fib$<$3k+1$>$=fib \\ \index{sum-fib$<$3k+1$>$=fib}
{\rm{sum-fib$<$3k+1$>$}}\,({\it{n\/}})\index{sum-fib$<$3k+1$>$} $=$ ({\rm{fib}}\,($1\;+$ ($1\;+$ ($1\;+$ ({\tt{3}} $*$ {\it{n\/}}))))\index{fib} $\div$ {\tt{2}})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sum-fib$<$3k+2$>$} \\  
\=\+{\rm{sum-fib$<$3k+2$>$}}\,({\it{n\/}})\index{sum-fib$<$3k+2$>$} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{sum-fib$<$3k+2$>$}}\,({\it{n\/}} $-\;1$)\index{sum-fib$<$3k+2$>$} $+$ {\rm{fib}}\,($1\;+$ ($1\;+$ ({\tt{3}} $*$ {\it{n\/}})))\index{fib}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-fib$<$3k+2$>$\&fib \\ \index{sum-fib$<$3k+2$>$\&fib}
($1\;+$ ({\tt{2}} $*$ {\rm{sum-fib$<$3k+2$>$}}\,({\it{n\/}})\index{sum-fib$<$3k+2$>$})) $=$ {\rm{fib}}\,($1\;+$ ($1\;+$ ($1\;+$ ($1\;+$ ({\tt{3}} $*$ {\it{n\/}})))))\index{fib}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-fib$<$3k+2$>$\&fib-1 \\ \index{sum-fib$<$3k+2$>$\&fib-1}
({\tt{2}} $*$ {\rm{sum-fib$<$3k+2$>$}}\,({\it{n\/}})\index{sum-fib$<$3k+2$>$}) $=$ ({\rm{fib}}\,($1\;+$ ($1\;+$ ($1\;+$ ($1\;+$ ({\tt{3}} $*$ {\it{n\/}})))))\index{fib} $-\;1$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-fib$<$3k+2$>$=fib \\ \index{sum-fib$<$3k+2$>$=fib}
{\rm{sum-fib$<$3k+2$>$}}\,({\it{n\/}})\index{sum-fib$<$3k+2$>$} $=$ (({\rm{fib}}\,($1\;+$ ($1\;+$ ($1\;+$ ($1\;+$ ({\tt{3}} $*$ {\it{n\/}})))))\index{fib} $-\;1$) $\div$ {\tt{2}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fib$<$2n+1$>$=fib$<$n$>$\&fib$<$2n+2$>$=fib$<$n$>$ \\ \index{fib$<$2n+1$>$=fib$<$n$>$\&fib$<$!2n+2$>$=fib$<$n$>$}
\=\+(\=\+{\rm{fib}}\,($1\;+$ ({\tt{2}} $*$ {\it{n\/}}))\index{fib} \\ 
$=$$\;\;\;\;$(({\rm{fib}}\,({\it{n\/}})\index{fib} $*$ {\rm{fib}}\,({\it{n\/}})\index{fib}) $+$ ({\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib} $*$ {\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib})))\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{fib}}\,($1\;+$ ($1\;+$ ({\tt{2}} $*$ {\it{n\/}})))\index{fib} \\ 
$=$$\;\;\;\;$(\=\+({\rm{fib}}\,({\it{n\/}})\index{fib} $*$ {\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib}) \\ 
$+$$\;\;\;\;$({\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib} $*$ {\rm{fib}}\,($1\;+$ ($1\;+$ {\it{n\/}}))\index{fib}))\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fib$<$2n+1$>$=fib$<$n$>$ \\ \index{fib$<$2n+1$>$=fib$<$n$>$}
\=\+{\rm{fib}}\,($1\;+$ ({\tt{2}} $*$ {\it{n\/}}))\index{fib} \\ 
$=$$\;\;\;\;$(({\rm{fib}}\,({\it{n\/}})\index{fib} $*$ {\rm{fib}}\,({\it{n\/}})\index{fib}) $+$ ({\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib} $*$ {\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib}))\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fib$<$2n+2$>$=fib$<$n$>$ \\ \index{fib$<$2n+2$>$=fib$<$n$>$}
\=\+{\rm{fib}}\,($1\;+$ ($1\;+$ ({\tt{2}} $*$ {\it{n\/}})))\index{fib} \\ 
$=$$\;\;\;\;$(({\rm{fib}}\,({\it{n\/}})\index{fib} $*$ {\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib}) $+$ ({\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib} $*$ {\rm{fib}}\,($1\;+$ ($1\;+$ {\it{n\/}}))\index{fib}))\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sum-fib$<$4k$>$} \\  
\=\+{\rm{sum-fib$<$4k$>$}}\,({\it{n\/}})\index{sum-fib$<$4k$>$} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{0}} \\ 
{\bf else }{\rm{sum-fib$<$4k$>$}}\,({\it{n\/}} $-\;1$)\index{sum-fib$<$4k$>$} $+$ {\rm{fib}}\,({\tt{4}} $*$ {\it{n\/}})\index{fib}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sum-fib$<$4k+1$>$} \\  
\=\+{\rm{sum-fib$<$4k+1$>$}}\,({\it{n\/}})\index{sum-fib$<$4k+1$>$} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{sum-fib$<$4k+1$>$}}\,({\it{n\/}} $-\;1$)\index{sum-fib$<$4k+1$>$} $+$ {\rm{fib}}\,($1\;+$ ({\tt{4}} $*$ {\it{n\/}}))\index{fib}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sum-fib$<$4k+2$>$} \\  
\=\+{\rm{sum-fib$<$4k+2$>$}}\,({\it{n\/}})\index{sum-fib$<$4k+2$>$} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{1}} \\ 
{\bf else }{\rm{sum-fib$<$4k+2$>$}}\,({\it{n\/}} $-\;1$)\index{sum-fib$<$4k+2$>$} $+$ {\rm{fib}}\,($1\;+$ ($1\;+$ ({\tt{4}} $*$ {\it{n\/}})))\index{fib}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{sum-fib$<$4k+3$>$} \\  
\=\+{\rm{sum-fib$<$4k+3$>$}}\,({\it{n\/}})\index{sum-fib$<$4k+3$>$} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\it{n\/}} $\simeq {\tt{0}}$$\;\;${\bf then }{\tt{2}} \\ 
{\bf else }{\rm{sum-fib$<$4k+3$>$}}\,({\it{n\/}} $-\;1$)\index{sum-fib$<$4k+3$>$} $+$ {\rm{fib}}\,($1\;+$ ($1\;+$ ($1\;+$ ({\tt{4}} $*$ {\it{n\/}}))))\index{fib}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  times-4=times-2-2 \\ \index{times-4=times-2-2}
({\tt{4}} $*$ {\it{n\/}}) $=$ ({\tt{2}} $*$ {\tt{2}} $*$ {\it{n\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fib$<$4n+1$>$=fib$<$2n$>$ \\ \index{fib$<$4n+1$>$=fib$<$2n$>$}
\=\+{\rm{fib}}\,($1\;+$ ({\tt{4}} $*$ {\it{n\/}}))\index{fib} \\ 
$=$$\;\;\;\;$(\=\+({\rm{fib}}\,({\tt{2}} $*$ {\it{n\/}})\index{fib} $*$ {\rm{fib}}\,({\tt{2}} $*$ {\it{n\/}})\index{fib}) \\ 
$+$$\;\;\;\;$({\rm{fib}}\,($1\;+$ ({\tt{2}} $*$ {\it{n\/}}))\index{fib} $*$ {\rm{fib}}\,($1\;+$ ({\tt{2}} $*$ {\it{n\/}}))\index{fib}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-fib$<$4k+1$>$=fib$<$2n$>$ \\ \index{sum-fib$<$4k+1$>$=fib$<$2n$>$}
{\rm{sum-fib$<$4k+1$>$}}\,({\it{n\/}})\index{sum-fib$<$4k+1$>$} $=$ ({\rm{fib}}\,($1\;+$ ({\tt{2}} $*$ {\it{n\/}}))\index{fib} $*$ {\rm{fib}}\,($1\;+$ ($1\;+$ ({\tt{2}} $*$ {\it{n\/}})))\index{fib})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fib$<$4n+2$>$=fib$<$2n$>$ \\ \index{fib$<$4n+2$>$=fib$<$2n$>$}
\=\+{\rm{fib}}\,($1\;+$ ($1\;+$ ({\tt{4}} $*$ {\it{n\/}})))\index{fib} \\ 
$=$$\;\;\;\;$(\=\+({\rm{fib}}\,({\tt{2}} $*$ {\it{n\/}})\index{fib} $*$ {\rm{fib}}\,($1\;+$ ({\tt{2}} $*$ {\it{n\/}}))\index{fib}) \\ 
$+$$\;\;\;\;$({\rm{fib}}\,($1\;+$ ({\tt{2}} $*$ {\it{n\/}}))\index{fib} $*$ {\rm{fib}}\,($1\;+$ ($1\;+$ ({\tt{2}} $*$ {\it{n\/}})))\index{fib}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-fib$<$4k+2$>$=fib$<$2n$>$ \\ \index{sum-fib$<$4k+2$>$=fib$<$2n$>$}
\=\+{\rm{sum-fib$<$4k+2$>$}}\,({\it{n\/}})\index{sum-fib$<$4k+2$>$} \\ 
$=$$\;\;\;\;$({\rm{fib}}\,($1\;+$ ($1\;+$ ({\tt{2}} $*$ {\it{n\/}})))\index{fib} $*$ {\rm{fib}}\,($1\;+$ ($1\;+$ ({\tt{2}} $*$ {\it{n\/}})))\index{fib})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fib$<$4n+3$>$=fib$<$2n$>$ \\ \index{fib$<$4n+3$>$=fib$<$2n$>$}
\=\+{\rm{fib}}\,($1\;+$ ($1\;+$ ($1\;+$ ({\tt{4}} $*$ {\it{n\/}}))))\index{fib} \\ 
$=$$\;\;\;\;$(\=\+({\rm{fib}}\,($1\;+$ ({\tt{2}} $*$ {\it{n\/}}))\index{fib} $*$ {\rm{fib}}\,($1\;+$ ({\tt{2}} $*$ {\it{n\/}}))\index{fib}) \\ 
$+$$\;\;\;\;$({\rm{fib}}\,($1\;+$ ($1\;+$ ({\tt{2}} $*$ {\it{n\/}})))\index{fib} $*$ {\rm{fib}}\,($1\;+$ ($1\;+$ ({\tt{2}} $*$ {\it{n\/}})))\index{fib}))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-fib$<$4k+3$>$=fib$<$2n$>$ \\ \index{sum-fib$<$4k+3$>$=fib$<$2n$>$}
\=\+{\rm{sum-fib$<$4k+3$>$}}\,({\it{n\/}})\index{sum-fib$<$4k+3$>$} \\ 
$=$$\;\;\;\;$({\rm{fib}}\,($1\;+$ ($1\;+$ ($1\;+$ ({\tt{2}} $*$ {\it{n\/}}))))\index{fib} $*$ {\rm{fib}}\,($1\;+$ ($1\;+$ ({\tt{2}} $*$ {\it{n\/}})))\index{fib})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fib$<$2n$>$=fib$<$n$>$ \\ \index{fib$<$2n$>$=fib$<$n$>$}
\=\+({\tt{0}} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{fib}}\,({\tt{2}} $*$ {\it{n\/}})\index{fib} \\ 
$=$$\;\;\;\;$(({\rm{fib}}\,({\it{n\/}} $-\;1$)\index{fib} $*$ {\rm{fib}}\,({\it{n\/}})\index{fib}) $+$ ({\rm{fib}}\,({\it{n\/}})\index{fib} $*$ {\rm{fib}}\,($1\;+$ {\it{n\/}})\index{fib})))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  fib$<$4n$>$=fib$<$2n$>$ \\ \index{fib$<$4n$>$=fib$<$2n$>$}
\=\+({\tt{0}} $<$ {\it{n\/}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{fib}}\,({\tt{4}} $*$ {\it{n\/}})\index{fib} \\ 
$=$$\;\;\;\;$(\=\+({\rm{fib}}\,(({\tt{2}} $*$ {\it{n\/}}) $-\;1$)\index{fib} $*$ {\rm{fib}}\,({\tt{2}} $*$ {\it{n\/}})\index{fib}) \\ 
$+$$\;\;\;\;$({\rm{fib}}\,({\tt{2}} $*$ {\it{n\/}})\index{fib} $*$ {\rm{fib}}\,($1\;+$ ({\tt{2}} $*$ {\it{n\/}}))\index{fib}))\-)\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  sum-fib$<$4k$>$=fib$<$2n$>$ \\ \index{sum-fib$<$4k$>$=fib$<$2n$>$}
{\rm{sum-fib$<$4k$>$}}\,({\it{n\/}})\index{sum-fib$<$4k$>$} $=$ ({\rm{fib}}\,({\tt{2}} $*$ {\it{n\/}})\index{fib} $*$ {\rm{fib}}\,($1\;+$ ($1\;+$ ({\tt{2}} $*$ {\it{n\/}})))\index{fib})
\end{tabbing}
            



%\end{list}
\printindex
\end{document}
