(NOTE-LIB "proveall" T)
Loading ./basic/proveall.lib
Finished loading ./basic/proveall.lib
Loading ./basic/proveall.o
Finished loading ./basic/proveall.o

(#./basic/proveall.lib #./basic/proveall)


(DEFN FIB
      (N)
      (IF (ZEROP N)
          0
          (IF (EQUAL N 1)
              1
              (PLUS (FIB (SUB1 N))
                    (FIB (SUB1 (SUB1 N)))))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call.  Hence, FIB is accepted under the
principle of definition.  Note that (NUMBERP (FIB N)) is a theorem.




[ 0.0 0.0 0.0 ]

FIB


(DEFN NBR-CALLS-FIB
      (N)
      (IF (ZEROP N)
          1
          (IF (EQUAL N 1)
              1
              (ADD1 (PLUS (NBR-CALLS-FIB (SUB1 N))
                          (NBR-CALLS-FIB (SUB1 (SUB1 N))))))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to show that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call.  Hence, NBR-CALLS-FIB is
accepted under the definitional principle.  Note that:
      (NUMBERP (NBR-CALLS-FIB N))
is a theorem.




[ 0.0 0.0 0.0 ]

NBR-CALLS-FIB


(DEFN NBR-PLUS-FIB
      (N)
      (IF (ZEROP N)
          0
          (IF (EQUAL N 1)
              0
              (ADD1 (PLUS (NBR-PLUS-FIB (SUB1 N))
                          (NBR-PLUS-FIB (SUB1 (SUB1 N))))))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to show that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call.  Hence, NBR-PLUS-FIB is
accepted under the definitional principle.  Note that:
      (NUMBERP (NBR-PLUS-FIB N))
is a theorem.




[ 0.0 0.0 0.0 ]

NBR-PLUS-FIB


(PROVE-LEMMA NBR-CALLS-FIB&FIB NIL
             (EQUAL (ADD1 (NBR-CALLS-FIB N))
                    (TIMES 2 (FIB (ADD1 N)))))

This conjecture simplifies, rewriting with TIMES-2, to:

      (EQUAL (ADD1 (NBR-CALLS-FIB N))
             (PLUS (FIB (ADD1 N)) (FIB (ADD1 N)))),

which we will name *1.


     We will appeal to induction.  There is only one plausible induction.  We
will induct according to the following scheme:
      (AND (IMPLIES (ZEROP N) (p N))
           (IMPLIES (AND (NOT (ZEROP N)) (EQUAL N 1))
                    (p N))
           (IMPLIES (AND (NOT (ZEROP N))
                         (NOT (EQUAL N 1))
                         (p (SUB1 (SUB1 N)))
                         (p (SUB1 N)))
                    (p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each induction step of the scheme.  The above induction
scheme produces the following three new goals:

Case 3. (IMPLIES (ZEROP N)
                 (EQUAL (ADD1 (NBR-CALLS-FIB N))
                        (PLUS (FIB (ADD1 N))
                              (FIB (ADD1 N))))).

  This simplifies, rewriting with the lemma SUB1-TYPE-RESTRICTION, and
  unfolding ZEROP, NBR-CALLS-FIB, ADD1, FIB, PLUS, and EQUAL, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP N)) (EQUAL N 1))
                 (EQUAL (ADD1 (NBR-CALLS-FIB N))
                        (PLUS (FIB (ADD1 N))
                              (FIB (ADD1 N))))).

  This simplifies, unfolding the definitions of ZEROP, NBR-CALLS-FIB, ADD1,
  FIB, PLUS, and EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP N))
                      (NOT (EQUAL N 1))
                      (EQUAL (ADD1 (NBR-CALLS-FIB (SUB1 (SUB1 N))))
                             (PLUS (FIB (ADD1 (SUB1 (SUB1 N))))
                                   (FIB (ADD1 (SUB1 (SUB1 N))))))
                      (EQUAL (ADD1 (NBR-CALLS-FIB (SUB1 N)))
                             (PLUS (FIB (ADD1 (SUB1 N)))
                                   (FIB (ADD1 (SUB1 N))))))
                 (EQUAL (ADD1 (NBR-CALLS-FIB N))
                        (PLUS (FIB (ADD1 N))
                              (FIB (ADD1 N))))).

  This simplifies, applying ADD1-SUB1, COMMUTATIVITY2-OF-PLUS,
  ASSOCIATIVITY-OF-PLUS, SUB1-ADD1, ADD1-EQUAL, COMMUTATIVITY-OF-PLUS, and
  PLUS-ADD1, and expanding the functions ZEROP, FIB, NBR-CALLS-FIB, NUMBERP,
  ADD1, PLUS, EQUAL, and SUB1, to two new conjectures:

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL N 0))
                        (NUMBERP N)
                        (NOT (EQUAL N 1))
                        (NOT (EQUAL (SUB1 N) 0))
                        (EQUAL (ADD1 (NBR-CALLS-FIB (SUB1 (SUB1 N))))
                               (PLUS (FIB (SUB1 N)) (FIB (SUB1 N))))
                        (EQUAL (ADD1 (NBR-CALLS-FIB (SUB1 N)))
                               (PLUS (FIB (SUB1 N))
                                     (FIB (SUB1 N))
                                     (FIB (SUB1 (SUB1 N)))
                                     (FIB (SUB1 (SUB1 N))))))
                   (EQUAL (ADD1 (PLUS (NBR-CALLS-FIB (SUB1 N))
                                      (NBR-CALLS-FIB (SUB1 (SUB1 N)))))
                          (PLUS (FIB (SUB1 N))
                                (FIB (SUB1 N))
                                (NBR-CALLS-FIB (SUB1 N))))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL N 0))
                        (NUMBERP N)
                        (NOT (EQUAL N 1))
                        (EQUAL (SUB1 N) 0)
                        (EQUAL (ADD1 (NBR-CALLS-FIB (SUB1 (SUB1 N))))
                               (PLUS (FIB 1) (FIB 1))))
                   (NOT (EQUAL (NBR-CALLS-FIB (SUB1 N)) 1))),

    which again simplifies, using linear arithmetic, to:

          T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

NBR-CALLS-FIB&FIB


(PROVE-LEMMA NBR-CALLS-FIB=FIB NIL
             (EQUAL (NBR-CALLS-FIB N)
                    (SUB1 (TIMES 2 (FIB (ADD1 N)))))
             ((USE (NBR-CALLS-FIB&FIB (N N)))))

This conjecture simplifies, using linear arithmetic, to the conjecture:

      (IMPLIES (AND (EQUAL (TIMES 2 (FIB (ADD1 N))) 0)
                    (EQUAL (ADD1 (NBR-CALLS-FIB N))
                           (TIMES 2 (FIB (ADD1 N)))))
               (EQUAL (NBR-CALLS-FIB N)
                      (SUB1 (TIMES 2 (FIB (ADD1 N)))))).

However this again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

NBR-CALLS-FIB=FIB


(PROVE-LEMMA NBR-PLUS-FIB&FIB NIL
             (EQUAL (ADD1 (NBR-PLUS-FIB N))
                    (FIB (ADD1 N))))


     Name the conjecture *1.


     Perhaps we can prove it by induction.  There is only one plausible
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP N) (p N))
           (IMPLIES (AND (NOT (ZEROP N)) (EQUAL N 1))
                    (p N))
           (IMPLIES (AND (NOT (ZEROP N))
                         (NOT (EQUAL N 1))
                         (p (SUB1 (SUB1 N)))
                         (p (SUB1 N)))
                    (p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each induction step of the scheme.  The above induction
scheme produces the following three new goals:

Case 3. (IMPLIES (ZEROP N)
                 (EQUAL (ADD1 (NBR-PLUS-FIB N))
                        (FIB (ADD1 N)))).

  This simplifies, applying SUB1-TYPE-RESTRICTION, and unfolding the
  definitions of ZEROP, NBR-PLUS-FIB, ADD1, FIB, and EQUAL, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP N)) (EQUAL N 1))
                 (EQUAL (ADD1 (NBR-PLUS-FIB N))
                        (FIB (ADD1 N)))),

  which simplifies, unfolding the definitions of ZEROP, NBR-PLUS-FIB, ADD1,
  FIB, and EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP N))
                      (NOT (EQUAL N 1))
                      (EQUAL (ADD1 (NBR-PLUS-FIB (SUB1 (SUB1 N))))
                             (FIB (ADD1 (SUB1 (SUB1 N)))))
                      (EQUAL (ADD1 (NBR-PLUS-FIB (SUB1 N)))
                             (FIB (ADD1 (SUB1 N)))))
                 (EQUAL (ADD1 (NBR-PLUS-FIB N))
                        (FIB (ADD1 N)))),

  which simplifies, rewriting with ADD1-SUB1, SUB1-ADD1, ADD1-EQUAL, PLUS-ADD1,
  and COMMUTATIVITY-OF-PLUS, and expanding the definitions of ZEROP, FIB,
  NBR-PLUS-FIB, NUMBERP, ADD1, EQUAL, PLUS, and SUB1, to the following two new
  goals:

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL N 0))
                        (NUMBERP N)
                        (NOT (EQUAL N 1))
                        (NOT (EQUAL (SUB1 N) 0))
                        (EQUAL (ADD1 (NBR-PLUS-FIB (SUB1 (SUB1 N))))
                               (FIB (SUB1 N)))
                        (EQUAL (ADD1 (NBR-PLUS-FIB (SUB1 N)))
                               (PLUS (FIB (SUB1 N))
                                     (FIB (SUB1 (SUB1 N))))))
                   (EQUAL (ADD1 (PLUS (NBR-PLUS-FIB (SUB1 N))
                                      (NBR-PLUS-FIB (SUB1 (SUB1 N)))))
                          (PLUS (FIB (SUB1 N))
                                (NBR-PLUS-FIB (SUB1 N))))).

    However this again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL N 0))
                        (NUMBERP N)
                        (NOT (EQUAL N 1))
                        (EQUAL (SUB1 N) 0)
                        (EQUAL (ADD1 (NBR-PLUS-FIB (SUB1 (SUB1 N))))
                               (FIB 1)))
                   (NOT (EQUAL (NBR-PLUS-FIB (SUB1 N)) 0))),

    which again simplifies, using linear arithmetic, to:

          T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

NBR-PLUS-FIB&FIB


(PROVE-LEMMA NBR-PLUS-FIB=FIB
             (REWRITE)
             (EQUAL (NBR-PLUS-FIB N)
                    (SUB1 (FIB (ADD1 N))))
             ((USE (NBR-PLUS-FIB&FIB (N N)))))

This formula simplifies, using linear arithmetic, to:

      (IMPLIES (AND (EQUAL (FIB (ADD1 N)) 0)
                    (EQUAL (ADD1 (NBR-PLUS-FIB N))
                           (FIB (ADD1 N))))
               (EQUAL (NBR-PLUS-FIB N)
                      (SUB1 (FIB (ADD1 N))))).

This again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

NBR-PLUS-FIB=FIB


(DEFN SUM-FIB<K>
      (N)
      (IF (ZEROP N)
          0
          (PLUS (SUM-FIB<K> (SUB1 N)) (FIB N))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call.  Hence, SUM-FIB<K> is accepted under
the definitional principle.  From the definition we can conclude that
(NUMBERP (SUM-FIB<K> N)) is a theorem.




[ 0.0 0.0 0.0 ]

SUM-FIB<K>


(PROVE-LEMMA SUM-FIB<K>&FIB NIL
             (EQUAL (ADD1 (SUM-FIB<K> N))
                    (FIB (ADD1 (ADD1 N)))))

This conjecture simplifies, applying SUB1-ADD1 and ADD1-EQUAL, and unfolding
the functions NUMBERP and FIB, to two new goals:

Case 2. (IMPLIES (NOT (NUMBERP N))
                 (EQUAL (ADD1 (SUM-FIB<K> N))
                        (PLUS (FIB (ADD1 N)) (FIB 0)))),

  which again simplifies, applying SUB1-TYPE-RESTRICTION, and expanding the
  definitions of SUM-FIB<K>, ADD1, FIB, PLUS, and EQUAL, to:

        T.

Case 1. (IMPLIES (NUMBERP N)
                 (EQUAL (ADD1 (SUM-FIB<K> N))
                        (PLUS (FIB (ADD1 N)) (FIB N)))).

  This again simplifies, applying COMMUTATIVITY-OF-PLUS, to:

        (IMPLIES (NUMBERP N)
                 (EQUAL (ADD1 (SUM-FIB<K> N))
                        (PLUS (FIB N) (FIB (ADD1 N))))),

  which we will name *1.


     We will appeal to induction.  There are two plausible inductions.
However, they merge into one likely candidate induction.  We will induct
according to the following scheme:
      (AND (IMPLIES (ZEROP N) (p N))
           (IMPLIES (AND (NOT (ZEROP N)) (EQUAL N 1))
                    (p N))
           (IMPLIES (AND (NOT (ZEROP N))
                         (NOT (EQUAL N 1))
                         (p (SUB1 (SUB1 N)))
                         (p (SUB1 N)))
                    (p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to prove that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme produces three new conjectures:

Case 3. (IMPLIES (AND (ZEROP N) (NUMBERP N))
                 (EQUAL (ADD1 (SUM-FIB<K> N))
                        (PLUS (FIB N) (FIB (ADD1 N))))),

  which simplifies, unfolding the functions ZEROP, NUMBERP, SUM-FIB<K>, ADD1,
  FIB, PLUS, and EQUAL, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP N))
                      (EQUAL N 1)
                      (NUMBERP N))
                 (EQUAL (ADD1 (SUM-FIB<K> N))
                        (PLUS (FIB N) (FIB (ADD1 N))))),

  which simplifies, unfolding ZEROP, NUMBERP, SUM-FIB<K>, ADD1, FIB, PLUS, and
  EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP N))
                      (NOT (EQUAL N 1))
                      (EQUAL (ADD1 (SUM-FIB<K> (SUB1 (SUB1 N))))
                             (PLUS (FIB (SUB1 (SUB1 N)))
                                   (FIB (ADD1 (SUB1 (SUB1 N))))))
                      (EQUAL (ADD1 (SUM-FIB<K> (SUB1 N)))
                             (PLUS (FIB (SUB1 N))
                                   (FIB (ADD1 (SUB1 N)))))
                      (NUMBERP N))
                 (EQUAL (ADD1 (SUM-FIB<K> N))
                        (PLUS (FIB N) (FIB (ADD1 N))))),

  which simplifies, applying ADD1-SUB1, COMMUTATIVITY2-OF-PLUS,
  ASSOCIATIVITY-OF-PLUS, COMMUTATIVITY-OF-PLUS, SUB1-ADD1, ADD1-EQUAL, and
  PLUS-ADD1, and unfolding the definitions of ZEROP, FIB, SUM-FIB<K>, NUMBERP,
  PLUS, ADD1, and EQUAL, to the new goal:

        (IMPLIES (AND (NOT (EQUAL N 0))
                      (NOT (EQUAL N 1))
                      (EQUAL (SUB1 N) 0)
                      (EQUAL (ADD1 (SUM-FIB<K> (SUB1 (SUB1 N))))
                             (PLUS (FIB (SUB1 (SUB1 N))) (FIB 1)))
                      (EQUAL (ADD1 (SUM-FIB<K> (SUB1 N)))
                             (PLUS 1 (FIB (SUB1 N))))
                      (NUMBERP N))
                 (EQUAL (ADD1 (PLUS (FIB (SUB1 N))
                                    (SUM-FIB<K> (SUB1 N))
                                    (FIB (SUB1 (SUB1 N)))))
                        (PLUS (FIB (SUB1 N))
                              (FIB (SUB1 N))
                              (FIB (SUB1 (SUB1 N)))
                              (FIB (SUB1 (SUB1 N)))))),

  which again simplifies, using linear arithmetic, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

SUM-FIB<K>&FIB


(PROVE-LEMMA SUM-FIB<K>=FIB
             (REWRITE)
             (EQUAL (SUM-FIB<K> N)
                    (SUB1 (FIB (ADD1 (ADD1 N)))))
             ((USE (SUM-FIB<K>&FIB (N N)))))

This simplifies, using linear arithmetic, to:

      (IMPLIES (AND (EQUAL (FIB (ADD1 (ADD1 N))) 0)
                    (EQUAL (ADD1 (SUM-FIB<K> N))
                           (FIB (ADD1 (ADD1 N)))))
               (EQUAL (SUM-FIB<K> N)
                      (SUB1 (FIB (ADD1 (ADD1 N)))))).

This again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

SUM-FIB<K>=FIB


(PROVE-LEMMA SUM-FIB<K>=NBR-PLUS-FIB NIL
             (EQUAL (SUM-FIB<K> N)
                    (NBR-PLUS-FIB (ADD1 N))))

This formula can be simplified, using the abbreviations NBR-PLUS-FIB=FIB and
SUM-FIB<K>=FIB, to:

      (EQUAL (SUB1 (FIB (ADD1 (ADD1 N))))
             (SUB1 (FIB (ADD1 (ADD1 N))))),

which simplifies, trivially, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

SUM-FIB<K>=NBR-PLUS-FIB


(DEFN SUM-FIB<2K>
      (N)
      (IF (ZEROP N)
          0
          (PLUS (SUM-FIB<2K> (SUB1 N))
                (FIB (TIMES 2 N)))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call.  Hence, SUM-FIB<2K> is accepted under
the principle of definition.  Note that (NUMBERP (SUM-FIB<2K> N)) is a theorem.




[ 0.0 0.0 0.0 ]

SUM-FIB<2K>


(PROVE-LEMMA SUM-FIB<2K>&FIB NIL
             (EQUAL (ADD1 (SUM-FIB<2K> N))
                    (FIB (ADD1 (TIMES 2 N)))))

This conjecture simplifies, rewriting with TIMES-2, to:

      (EQUAL (ADD1 (SUM-FIB<2K> N))
             (FIB (ADD1 (PLUS N N)))),

which we will name *1.


     We will appeal to induction.  The recursive terms in the conjecture
suggest two inductions.  However, they merge into one likely candidate
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP N) (p N))
           (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
                    (p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each induction step of the scheme.  The above induction
scheme produces the following two new goals:

Case 2. (IMPLIES (ZEROP N)
                 (EQUAL (ADD1 (SUM-FIB<2K> N))
                        (FIB (ADD1 (PLUS N N))))).

  This simplifies, rewriting with the lemma PLUS-RIGHT-ID2, and unfolding
  ZEROP, SUM-FIB<2K>, ADD1, PLUS, FIB, and EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP N))
                      (EQUAL (ADD1 (SUM-FIB<2K> (SUB1 N)))
                             (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))))
                 (EQUAL (ADD1 (SUM-FIB<2K> N))
                        (FIB (ADD1 (PLUS N N))))).

  This simplifies, rewriting with COMMUTATIVITY-OF-PLUS, TIMES-2, SUB1-ADD1,
  ADD1-EQUAL, and PLUS-ADD1, and expanding the definitions of ZEROP,
  SUM-FIB<2K>, PLUS, NUMBERP, and FIB, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

SUM-FIB<2K>&FIB


(PROVE-LEMMA SUM-FIB<2K>=FIB NIL
             (EQUAL (SUM-FIB<2K> N)
                    (SUB1 (FIB (ADD1 (TIMES 2 N)))))
             ((USE (SUM-FIB<2K>&FIB (N N)))))

This conjecture simplifies, using linear arithmetic, to the conjecture:

      (IMPLIES (AND (EQUAL (FIB (ADD1 (TIMES 2 N))) 0)
                    (EQUAL (ADD1 (SUM-FIB<2K> N))
                           (FIB (ADD1 (TIMES 2 N)))))
               (EQUAL (SUM-FIB<2K> N)
                      (SUB1 (FIB (ADD1 (TIMES 2 N)))))).

However this again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

SUM-FIB<2K>=FIB


(DEFN SUM-FIB<2K+1>
      (N)
      (IF (ZEROP N)
          1
          (PLUS (SUM-FIB<2K+1> (SUB1 N))
                (FIB (ADD1 (TIMES 2 N))))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call.  Hence, SUM-FIB<2K+1> is accepted under
the principle of definition.  From the definition we can conclude that:
      (NUMBERP (SUM-FIB<2K+1> N))
is a theorem.




[ 0.0 0.0 0.0 ]

SUM-FIB<2K+1>


(PROVE-LEMMA SUM-FIB<2K+1>=FIB NIL
             (EQUAL (SUM-FIB<2K+1> N)
                    (FIB (ADD1 (ADD1 (TIMES 2 N))))))

This conjecture simplifies, rewriting with TIMES-2, COMMUTATIVITY-OF-PLUS,
SUB1-ADD1, and ADD1-EQUAL, and unfolding NUMBERP and FIB, to:

      (EQUAL (SUM-FIB<2K+1> N)
             (PLUS (FIB (PLUS N N))
                   (FIB (ADD1 (PLUS N N))))),

which we will name *1.


     Perhaps we can prove it by induction.  There are three plausible
inductions.  However, they merge into one likely candidate induction.  We will
induct according to the following scheme:
      (AND (IMPLIES (ZEROP N) (p N))
           (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
                    (p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to prove that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme generates two new goals:

Case 2. (IMPLIES (ZEROP N)
                 (EQUAL (SUM-FIB<2K+1> N)
                        (PLUS (FIB (PLUS N N))
                              (FIB (ADD1 (PLUS N N)))))),

  which simplifies, rewriting with PLUS-RIGHT-ID2, and opening up the
  functions ZEROP, SUM-FIB<2K+1>, PLUS, FIB, ADD1, and EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP N))
                      (EQUAL (SUM-FIB<2K+1> (SUB1 N))
                             (PLUS (FIB (PLUS (SUB1 N) (SUB1 N)))
                                   (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))))
                 (EQUAL (SUM-FIB<2K+1> N)
                        (PLUS (FIB (PLUS N N))
                              (FIB (ADD1 (PLUS N N)))))).

  This simplifies, applying COMMUTATIVITY-OF-PLUS, TIMES-2, SUB1-ADD1, and
  ADD1-EQUAL, and opening up the definitions of ZEROP, SUM-FIB<2K+1>, PLUS,
  NUMBERP, and FIB, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

SUM-FIB<2K+1>=FIB


(DEFN SUM-FIB<3K>
      (N)
      (IF (ZEROP N)
          0
          (PLUS (SUM-FIB<3K> (SUB1 N))
                (FIB (TIMES 3 N)))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call.  Hence, SUM-FIB<3K> is accepted under
the principle of definition.  Note that (NUMBERP (SUM-FIB<3K> N)) is a theorem.




[ 0.0 0.0 0.0 ]

SUM-FIB<3K>


(PROVE-LEMMA SUM-FIB<3K>&FIB NIL
             (EQUAL (ADD1 (TIMES 2 (SUM-FIB<3K> N)))
                    (FIB (ADD1 (ADD1 (TIMES 3 N))))))

This formula simplifies, rewriting with the lemmas TIMES-2,
COMMUTATIVITY-OF-PLUS, SUB1-ADD1, and ADD1-EQUAL, and expanding SUB1, NUMBERP,
EQUAL, TIMES, and FIB, to the new formula:

      (EQUAL (ADD1 (PLUS (SUM-FIB<3K> N)
                         (SUM-FIB<3K> N)))
             (PLUS (FIB (PLUS N N N))
                   (FIB (ADD1 (PLUS N N N))))),

which we will name *1.


     Perhaps we can prove it by induction.  There are six plausible inductions.
However, they merge into one likely candidate induction.  We will induct
according to the following scheme:
      (AND (IMPLIES (ZEROP N) (p N))
           (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
                    (p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to establish that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme produces two new conjectures:

Case 2. (IMPLIES (ZEROP N)
                 (EQUAL (ADD1 (PLUS (SUM-FIB<3K> N)
                                    (SUM-FIB<3K> N)))
                        (PLUS (FIB (PLUS N N N))
                              (FIB (ADD1 (PLUS N N N)))))),

  which simplifies, appealing to the lemmas PLUS-RIGHT-ID2 and
  COMMUTATIVITY-OF-PLUS, and expanding the definitions of ZEROP, SUM-FIB<3K>,
  PLUS, ADD1, FIB, EQUAL, and NUMBERP, to:

        T.

Case 1. (IMPLIES
            (AND (NOT (ZEROP N))
                 (EQUAL (ADD1 (PLUS (SUM-FIB<3K> (SUB1 N))
                                    (SUM-FIB<3K> (SUB1 N))))
                        (PLUS (FIB (PLUS (SUB1 N) (SUB1 N) (SUB1 N)))
                              (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N) (SUB1 N)))))))
            (EQUAL (ADD1 (PLUS (SUM-FIB<3K> N)
                               (SUM-FIB<3K> N)))
                   (PLUS (FIB (PLUS N N N))
                         (FIB (ADD1 (PLUS N N N)))))),

  which simplifies, rewriting with PLUS-ADD1, TIMES-2, COMMUTATIVITY-OF-PLUS,
  SUB1-ADD1, ADD1-EQUAL, ASSOCIATIVITY-OF-PLUS, and COMMUTATIVITY2-OF-PLUS,
  and expanding the definitions of ZEROP, SUM-FIB<3K>, PLUS, SUB1, NUMBERP,
  EQUAL, TIMES, and FIB, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.1 0.0 ]

SUM-FIB<3K>&FIB


(PROVE-LEMMA SUM-FIB<3K>&FIB-1 NIL
             (EQUAL (TIMES 2 (SUM-FIB<3K> N))
                    (SUB1 (FIB (ADD1 (ADD1 (TIMES 3 N))))))
             ((USE (SUM-FIB<3K>&FIB (N N)))))

This conjecture simplifies, using linear arithmetic, to:

      (IMPLIES (AND (EQUAL (FIB (ADD1 (ADD1 (TIMES 3 N))))
                           0)
                    (EQUAL (ADD1 (TIMES 2 (SUM-FIB<3K> N)))
                           (FIB (ADD1 (ADD1 (TIMES 3 N))))))
               (EQUAL (TIMES 2 (SUM-FIB<3K> N))
                      (SUB1 (FIB (ADD1 (ADD1 (TIMES 3 N))))))).

However this again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

SUM-FIB<3K>&FIB-1


(PROVE-LEMMA SUM-FIB<3K>=FIB NIL
             (EQUAL (SUM-FIB<3K> N)
                    (QUOTIENT (SUB1 (FIB (ADD1 (ADD1 (TIMES 3 N)))))
                              2))
             ((USE (SUM-FIB<3K>&FIB-1 (N N)))))

This conjecture simplifies, applying TIMES-2, COMMUTATIVITY-OF-PLUS, SUB1-ADD1,
ADD1-EQUAL, and DIVIDES-IMPLIES-TIMES, and expanding SUB1, NUMBERP, EQUAL,
TIMES, and FIB, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

SUM-FIB<3K>=FIB


(DEFN SUM-FIB<3K+1>
      (N)
      (IF (ZEROP N)
          1
          (PLUS (SUM-FIB<3K+1> (SUB1 N))
                (FIB (ADD1 (TIMES 3 N))))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call.  Hence, SUM-FIB<3K+1> is accepted under
the principle of definition.  From the definition we can conclude that:
      (NUMBERP (SUM-FIB<3K+1> N))
is a theorem.




[ 0.0 0.0 0.0 ]

SUM-FIB<3K+1>


(PROVE-LEMMA SUM-FIB<3K+1>&FIB NIL
             (EQUAL (TIMES 2 (SUM-FIB<3K+1> N))
                    (FIB (ADD1 (ADD1 (ADD1 (TIMES 3 N)))))))

This formula simplifies, rewriting with the lemmas TIMES-2,
COMMUTATIVITY-OF-PLUS, SUB1-ADD1, ADD1-EQUAL, and COMMUTATIVITY2-OF-PLUS, and
expanding SUB1, NUMBERP, EQUAL, TIMES, and FIB, to the new formula:

      (EQUAL (PLUS (SUM-FIB<3K+1> N)
                   (SUM-FIB<3K+1> N))
             (PLUS (FIB (PLUS N N N))
                   (FIB (ADD1 (PLUS N N N)))
                   (FIB (ADD1 (PLUS N N N))))),

which we will name *1.


     Perhaps we can prove it by induction.  There are eight plausible
inductions.  However, they merge into one likely candidate induction.  We will
induct according to the following scheme:
      (AND (IMPLIES (ZEROP N) (p N))
           (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
                    (p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to establish that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme produces two new conjectures:

Case 2. (IMPLIES (ZEROP N)
                 (EQUAL (PLUS (SUM-FIB<3K+1> N)
                              (SUM-FIB<3K+1> N))
                        (PLUS (FIB (PLUS N N N))
                              (FIB (ADD1 (PLUS N N N)))
                              (FIB (ADD1 (PLUS N N N)))))),

  which simplifies, appealing to the lemmas PLUS-RIGHT-ID2 and
  COMMUTATIVITY-OF-PLUS, and expanding the definitions of ZEROP, SUM-FIB<3K+1>,
  PLUS, FIB, ADD1, EQUAL, and NUMBERP, to:

        T.

Case 1. (IMPLIES
            (AND (NOT (ZEROP N))
                 (EQUAL (PLUS (SUM-FIB<3K+1> (SUB1 N))
                              (SUM-FIB<3K+1> (SUB1 N)))
                        (PLUS (FIB (PLUS (SUB1 N) (SUB1 N) (SUB1 N)))
                              (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N) (SUB1 N))))
                              (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N) (SUB1 N)))))))
            (EQUAL (PLUS (SUM-FIB<3K+1> N)
                         (SUM-FIB<3K+1> N))
                   (PLUS (FIB (PLUS N N N))
                         (FIB (ADD1 (PLUS N N N)))
                         (FIB (ADD1 (PLUS N N N)))))),

  which simplifies, rewriting with PLUS-ADD1, TIMES-2, COMMUTATIVITY-OF-PLUS,
  SUB1-ADD1, ADD1-EQUAL, COMMUTATIVITY2-OF-PLUS, and ASSOCIATIVITY-OF-PLUS,
  and expanding the definitions of ZEROP, SUM-FIB<3K+1>, PLUS, SUB1, NUMBERP,
  EQUAL, TIMES, and FIB, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.1 0.0 ]

SUM-FIB<3K+1>&FIB


(PROVE-LEMMA SUM-FIB<3K+1>=FIB NIL
             (EQUAL (SUM-FIB<3K+1> N)
                    (QUOTIENT (FIB (ADD1 (ADD1 (ADD1 (TIMES 3 N)))))
                              2))
             ((USE (SUM-FIB<3K+1>&FIB (N N)))))

This conjecture simplifies, applying TIMES-2, COMMUTATIVITY-OF-PLUS, SUB1-ADD1,
ADD1-EQUAL, COMMUTATIVITY2-OF-PLUS, and DIVIDES-IMPLIES-TIMES, and expanding
SUB1, NUMBERP, EQUAL, TIMES, and FIB, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

SUM-FIB<3K+1>=FIB


(DEFN SUM-FIB<3K+2>
      (N)
      (IF (ZEROP N)
          1
          (PLUS (SUM-FIB<3K+2> (SUB1 N))
                (FIB (ADD1 (ADD1 (TIMES 3 N)))))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to show that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call.  Hence, SUM-FIB<3K+2> is
accepted under the definitional principle.  Observe that:
      (NUMBERP (SUM-FIB<3K+2> N))
is a theorem.




[ 0.0 0.0 0.0 ]

SUM-FIB<3K+2>


(PROVE-LEMMA SUM-FIB<3K+2>&FIB NIL
             (EQUAL (ADD1 (TIMES 2 (SUM-FIB<3K+2> N)))
                    (FIB (ADD1 (ADD1 (ADD1 (ADD1 (TIMES 3 N))))))))

This conjecture simplifies, applying TIMES-2, COMMUTATIVITY-OF-PLUS, SUB1-ADD1,
ADD1-EQUAL, COMMUTATIVITY2-OF-PLUS, and ASSOCIATIVITY-OF-PLUS, and opening up
the definitions of SUB1, NUMBERP, EQUAL, TIMES, and FIB, to:

      (EQUAL (ADD1 (PLUS (SUM-FIB<3K+2> N)
                         (SUM-FIB<3K+2> N)))
             (PLUS (FIB (PLUS N N N))
                   (FIB (PLUS N N N))
                   (FIB (ADD1 (PLUS N N N)))
                   (FIB (ADD1 (PLUS N N N)))
                   (FIB (ADD1 (PLUS N N N))))).

Call the above conjecture *1.


     We will appeal to induction.  12 inductions are suggested by terms in the
conjecture.  However, they merge into one likely candidate induction.  We will
induct according to the following scheme:
      (AND (IMPLIES (ZEROP N) (p N))
           (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
                    (p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT N) decreases according to the well-founded relation
LESSP in each induction step of the scheme.  The above induction scheme
generates the following two new goals:

Case 2. (IMPLIES (ZEROP N)
                 (EQUAL (ADD1 (PLUS (SUM-FIB<3K+2> N)
                                    (SUM-FIB<3K+2> N)))
                        (PLUS (FIB (PLUS N N N))
                              (FIB (PLUS N N N))
                              (FIB (ADD1 (PLUS N N N)))
                              (FIB (ADD1 (PLUS N N N)))
                              (FIB (ADD1 (PLUS N N N)))))).

  This simplifies, rewriting with PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS,
  and unfolding ZEROP, SUM-FIB<3K+2>, PLUS, ADD1, FIB, EQUAL, and NUMBERP, to:

        T.

Case 1. (IMPLIES
            (AND (NOT (ZEROP N))
                 (EQUAL (ADD1 (PLUS (SUM-FIB<3K+2> (SUB1 N))
                                    (SUM-FIB<3K+2> (SUB1 N))))
                        (PLUS (FIB (PLUS (SUB1 N) (SUB1 N) (SUB1 N)))
                              (FIB (PLUS (SUB1 N) (SUB1 N) (SUB1 N)))
                              (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N) (SUB1 N))))
                              (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N) (SUB1 N))))
                              (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N) (SUB1 N)))))))
            (EQUAL (ADD1 (PLUS (SUM-FIB<3K+2> N)
                               (SUM-FIB<3K+2> N)))
                   (PLUS (FIB (PLUS N N N))
                         (FIB (PLUS N N N))
                         (FIB (ADD1 (PLUS N N N)))
                         (FIB (ADD1 (PLUS N N N)))
                         (FIB (ADD1 (PLUS N N N)))))),

  which simplifies, rewriting with the lemmas PLUS-ADD1, TIMES-2,
  COMMUTATIVITY-OF-PLUS, SUB1-ADD1, ADD1-EQUAL, COMMUTATIVITY2-OF-PLUS, and
  ASSOCIATIVITY-OF-PLUS, and opening up the definitions of ZEROP,
  SUM-FIB<3K+2>, PLUS, SUB1, NUMBERP, EQUAL, TIMES, and FIB, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.2 0.0 ]

SUM-FIB<3K+2>&FIB


(PROVE-LEMMA SUM-FIB<3K+2>&FIB-1 NIL
             (EQUAL (TIMES 2 (SUM-FIB<3K+2> N))
                    (SUB1 (FIB (ADD1 (ADD1 (ADD1 (ADD1 (TIMES 3 N))))))))
             ((USE (SUM-FIB<3K+2>&FIB (N N)))))

This simplifies, using linear arithmetic, to:

      (IMPLIES (AND (EQUAL (FIB (ADD1 (ADD1 (ADD1 (ADD1 (TIMES 3 N))))))
                           0)
                    (EQUAL (ADD1 (TIMES 2 (SUM-FIB<3K+2> N)))
                           (FIB (ADD1 (ADD1 (ADD1 (ADD1 (TIMES 3 N))))))))
               (EQUAL (TIMES 2 (SUM-FIB<3K+2> N))
                      (SUB1 (FIB (ADD1 (ADD1 (ADD1 (ADD1 (TIMES 3 N))))))))).

But this again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

SUM-FIB<3K+2>&FIB-1


(PROVE-LEMMA SUM-FIB<3K+2>=FIB NIL
          (EQUAL (SUM-FIB<3K+2> N)
                 (QUOTIENT (SUB1 (FIB (ADD1 (ADD1 (ADD1 (ADD1 (TIMES 3 N)))))))
                           2))
          ((USE (SUM-FIB<3K+2>&FIB-1 (N N)))))

This simplifies, rewriting with TIMES-2, COMMUTATIVITY-OF-PLUS, SUB1-ADD1,
ADD1-EQUAL, COMMUTATIVITY2-OF-PLUS, ASSOCIATIVITY-OF-PLUS, and
DIVIDES-IMPLIES-TIMES, and unfolding the functions SUB1, NUMBERP, EQUAL, TIMES,
and FIB, to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

SUM-FIB<3K+2>=FIB


(PROVE-LEMMA FIB<2N+1>=FIB<N>&FIB<2N+2>=FIB<N> NIL
             (AND (EQUAL (FIB (ADD1 (TIMES 2 N)))
                         (PLUS (TIMES (FIB N) (FIB N))
                               (TIMES (FIB (ADD1 N))
                                      (FIB (ADD1 N)))))
                  (EQUAL (FIB (ADD1 (ADD1 (TIMES 2 N))))
                         (PLUS (TIMES (FIB N) (FIB (ADD1 N)))
                               (TIMES (FIB (ADD1 N))
                                      (FIB (ADD1 (ADD1 N)))))))
             ((INDUCT (SUM-FIB<K> N))))

This formula can be simplified, using the abbreviations ZEROP, NOT, OR, and
AND, to the following two new goals:

Case 2. (IMPLIES (ZEROP N)
                 (AND (EQUAL (FIB (ADD1 (TIMES 2 N)))
                             (PLUS (TIMES (FIB N) (FIB N))
                                   (TIMES (FIB (ADD1 N))
                                          (FIB (ADD1 N)))))
                      (EQUAL (FIB (ADD1 (ADD1 (TIMES 2 N))))
                             (PLUS (TIMES (FIB N) (FIB (ADD1 N)))
                                   (TIMES (FIB (ADD1 N))
                                          (FIB (ADD1 (ADD1 N)))))))).

  This simplifies, appealing to the lemmas PLUS-RIGHT-ID2, TIMES-2, and
  SUB1-TYPE-RESTRICTION, and unfolding ZEROP, TIMES, ADD1, FIB, PLUS, EQUAL,
  and AND, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL N 0))
                      (NUMBERP N)
                      (EQUAL (FIB (ADD1 (TIMES 2 (SUB1 N))))
                             (PLUS (TIMES (FIB (SUB1 N)) (FIB (SUB1 N)))
                                   (TIMES (FIB (ADD1 (SUB1 N)))
                                          (FIB (ADD1 (SUB1 N))))))
                      (EQUAL (FIB (ADD1 (ADD1 (TIMES 2 (SUB1 N)))))
                             (PLUS (TIMES (FIB (SUB1 N))
                                          (FIB (ADD1 (SUB1 N))))
                                   (TIMES (FIB (ADD1 (SUB1 N)))
                                          (FIB (ADD1 (ADD1 (SUB1 N))))))))
                 (AND (EQUAL (FIB (ADD1 (TIMES 2 N)))
                             (PLUS (TIMES (FIB N) (FIB N))
                                   (TIMES (FIB (ADD1 N))
                                          (FIB (ADD1 N)))))
                      (EQUAL (FIB (ADD1 (ADD1 (TIMES 2 N))))
                             (PLUS (TIMES (FIB N) (FIB (ADD1 N)))
                                   (TIMES (FIB (ADD1 N))
                                          (FIB (ADD1 (ADD1 N)))))))).

  This simplifies, applying TIMES-2, ADD1-SUB1, COMMUTATIVITY-OF-PLUS,
  SUB1-ADD1, ADD1-EQUAL, COMMUTATIVITY-OF-TIMES,
  DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, COMMUTATIVITY2-OF-PLUS, and
  ASSOCIATIVITY-OF-PLUS, and expanding the functions NUMBERP, FIB, PLUS, and
  AND, to two new conjectures:

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL N 0))
                        (NUMBERP N)
                        (EQUAL (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))
                               (PLUS (TIMES (FIB N) (FIB N))
                                     (TIMES (FIB (SUB1 N))
                                            (FIB (SUB1 N)))))
                        (EQUAL (PLUS (FIB (PLUS (SUB1 N) (SUB1 N)))
                                     (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                               (PLUS (TIMES (FIB N) (FIB N))
                                     (TIMES (FIB N) (FIB (SUB1 N)))
                                     (TIMES (FIB N) (FIB (SUB1 N))))))
                   (EQUAL (PLUS (FIB (PLUS (SUB1 N) (SUB1 N)))
                                (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))
                                (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                          (PLUS (TIMES (FIB N) (FIB N))
                                (TIMES (FIB N) (FIB N))
                                (TIMES (FIB N) (FIB (SUB1 N)))
                                (TIMES (FIB N) (FIB (SUB1 N)))
                                (TIMES (FIB (SUB1 N))
                                       (FIB (SUB1 N)))))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL N 0))
                        (NUMBERP N)
                        (EQUAL (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))
                               (PLUS (TIMES (FIB N) (FIB N))
                                     (TIMES (FIB (SUB1 N))
                                            (FIB (SUB1 N)))))
                        (EQUAL (PLUS (FIB (PLUS (SUB1 N) (SUB1 N)))
                                     (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                               (PLUS (TIMES (FIB N) (FIB N))
                                     (TIMES (FIB N) (FIB (SUB1 N)))
                                     (TIMES (FIB N) (FIB (SUB1 N))))))
                   (EQUAL (PLUS (FIB (PLUS (SUB1 N) (SUB1 N)))
                                (FIB (PLUS (SUB1 N) (SUB1 N)))
                                (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))
                                (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))
                                (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                          (PLUS (TIMES (FIB N) (FIB N))
                                (TIMES (FIB N) (FIB N))
                                (TIMES (FIB N) (FIB N))
                                (TIMES (FIB N) (FIB (SUB1 N)))
                                (TIMES (FIB N) (FIB (SUB1 N)))
                                (TIMES (FIB N) (FIB (SUB1 N)))
                                (TIMES (FIB N) (FIB (SUB1 N)))
                                (TIMES (FIB (SUB1 N))
                                       (FIB (SUB1 N)))))),

    which again simplifies, using linear arithmetic, to:

          T.

Q.E.D.


[ 0.0 0.1 0.0 ]

FIB<2N+1>=FIB<N>&FIB<2N+2>=FIB<N>


(PROVE-LEMMA FIB<2N+1>=FIB<N> NIL
             (EQUAL (FIB (ADD1 (TIMES 2 N)))
                    (PLUS (TIMES (FIB N) (FIB N))
                          (TIMES (FIB (ADD1 N))
                                 (FIB (ADD1 N)))))
             ((USE (FIB<2N+1>=FIB<N>&FIB<2N+2>=FIB<N> (N N)))))

This conjecture simplifies, trivially, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

FIB<2N+1>=FIB<N>


(PROVE-LEMMA FIB<2N+2>=FIB<N> NIL
             (EQUAL (FIB (ADD1 (ADD1 (TIMES 2 N))))
                    (PLUS (TIMES (FIB N) (FIB (ADD1 N)))
                          (TIMES (FIB (ADD1 N))
                                 (FIB (ADD1 (ADD1 N))))))
             ((USE (FIB<2N+1>=FIB<N>&FIB<2N+2>=FIB<N> (N N)))))

This formula simplifies, trivially, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

FIB<2N+2>=FIB<N>


(DEFN SUM-FIB<4K>
      (N)
      (IF (ZEROP N)
          0
          (PLUS (SUM-FIB<4K> (SUB1 N))
                (FIB (TIMES 4 N)))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call.  Hence, SUM-FIB<4K> is accepted under
the principle of definition.  Note that (NUMBERP (SUM-FIB<4K> N)) is a theorem.




[ 0.0 0.0 0.0 ]

SUM-FIB<4K>


(DEFN SUM-FIB<4K+1>
      (N)
      (IF (ZEROP N)
          1
          (PLUS (SUM-FIB<4K+1> (SUB1 N))
                (FIB (ADD1 (TIMES 4 N))))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call.  Hence, SUM-FIB<4K+1> is accepted under
the principle of definition.  From the definition we can conclude that:
      (NUMBERP (SUM-FIB<4K+1> N))
is a theorem.




[ 0.0 0.0 0.0 ]

SUM-FIB<4K+1>


(DEFN SUM-FIB<4K+2>
      (N)
      (IF (ZEROP N)
          1
          (PLUS (SUM-FIB<4K+2> (SUB1 N))
                (FIB (ADD1 (ADD1 (TIMES 4 N)))))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to show that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call.  Hence, SUM-FIB<4K+2> is
accepted under the definitional principle.  Observe that:
      (NUMBERP (SUM-FIB<4K+2> N))
is a theorem.




[ 0.0 0.0 0.0 ]

SUM-FIB<4K+2>


(DEFN SUM-FIB<4K+3>
      (N)
      (IF (ZEROP N)
          2
          (PLUS (SUM-FIB<4K+3> (SUB1 N))
                (FIB (ADD1 (ADD1 (ADD1 (TIMES 4 N))))))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call.  Hence, SUM-FIB<4K+3> is accepted under
the principle of definition.  Note that (NUMBERP (SUM-FIB<4K+3> N)) is a
theorem.




[ 0.0 0.0 0.0 ]

SUM-FIB<4K+3>


(PROVE-LEMMA TIMES-4=TIMES-2-2
             (REWRITE)
             (EQUAL (TIMES 4 N) (TIMES 2 2 N)))

WARNING:  the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the newly proposed TIMES-4=TIMES-2-2 could!


This simplifies, appealing to the lemmas TIMES-2 and ASSOCIATIVITY-OF-PLUS, to
the conjecture:

      (EQUAL (TIMES 4 N) (PLUS N N N N)).

This again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

TIMES-4=TIMES-2-2


(PROVE-LEMMA FIB<4N+1>=FIB<2N>
             (REWRITE)
             (EQUAL (FIB (ADD1 (TIMES 4 N)))
                    (PLUS (TIMES (FIB (TIMES 2 N))
                                 (FIB (TIMES 2 N)))
                          (TIMES (FIB (ADD1 (TIMES 2 N)))
                                 (FIB (ADD1 (TIMES 2 N))))))
             ((USE (FIB<2N+1>=FIB<N> (N (TIMES 2 N))))))

This formula can be simplified, using the abbreviation TIMES-4=TIMES-2-2, to:

      T,

which simplifies, trivially, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

FIB<4N+1>=FIB<2N>


(PROVE-LEMMA SUM-FIB<4K+1>=FIB<2N> NIL
             (EQUAL (SUM-FIB<4K+1> N)
                    (TIMES (FIB (ADD1 (TIMES 2 N)))
                           (FIB (ADD1 (ADD1 (TIMES 2 N))))))
             ((DISABLE TIMES-4=TIMES-2-2)))

This formula simplifies, rewriting with TIMES-2, COMMUTATIVITY-OF-PLUS,
SUB1-ADD1, ADD1-EQUAL, COMMUTATIVITY-OF-TIMES, and
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and opening up the definitions of NUMBERP
and FIB, to the new goal:

      (EQUAL (SUM-FIB<4K+1> N)
             (PLUS (TIMES (FIB (PLUS N N))
                          (FIB (ADD1 (PLUS N N))))
                   (TIMES (FIB (ADD1 (PLUS N N)))
                          (FIB (ADD1 (PLUS N N)))))),

which we will name *1.


     We will appeal to induction.  There are five plausible inductions.
However, they merge into one likely candidate induction.  We will induct
according to the following scheme:
      (AND (IMPLIES (ZEROP N) (p N))
           (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
                    (p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to establish that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme produces two new conjectures:

Case 2. (IMPLIES (ZEROP N)
                 (EQUAL (SUM-FIB<4K+1> N)
                        (PLUS (TIMES (FIB (PLUS N N))
                                     (FIB (ADD1 (PLUS N N))))
                              (TIMES (FIB (ADD1 (PLUS N N)))
                                     (FIB (ADD1 (PLUS N N))))))),

  which simplifies, rewriting with PLUS-RIGHT-ID2, and expanding the functions
  ZEROP, SUM-FIB<4K+1>, PLUS, FIB, ADD1, TIMES, and EQUAL, to:

        T.

Case 1. (IMPLIES
             (AND (NOT (ZEROP N))
                  (EQUAL (SUM-FIB<4K+1> (SUB1 N))
                         (PLUS (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                      (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                               (TIMES (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))
                                      (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))))))
             (EQUAL (SUM-FIB<4K+1> N)
                    (PLUS (TIMES (FIB (PLUS N N))
                                 (FIB (ADD1 (PLUS N N))))
                          (TIMES (FIB (ADD1 (PLUS N N)))
                                 (FIB (ADD1 (PLUS N N))))))).

  This simplifies, rewriting with the lemmas COMMUTATIVITY-OF-PLUS, TIMES-2,
  SUB1-ADD1, ADD1-EQUAL, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS,
  COMMUTATIVITY-OF-TIMES, COMMUTATIVITY2-OF-PLUS, ASSOCIATIVITY-OF-PLUS, and
  FIB<4N+1>=FIB<2N>, and opening up the functions ZEROP, SUM-FIB<4K+1>, PLUS,
  NUMBERP, and FIB, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.1 0.0 ]

SUM-FIB<4K+1>=FIB<2N>


(PROVE-LEMMA FIB<4N+2>=FIB<2N>
             (REWRITE)
             (EQUAL (FIB (ADD1 (ADD1 (TIMES 4 N))))
                    (PLUS (TIMES (FIB (TIMES 2 N))
                                 (FIB (ADD1 (TIMES 2 N))))
                          (TIMES (FIB (ADD1 (TIMES 2 N)))
                                 (FIB (ADD1 (ADD1 (TIMES 2 N)))))))
             ((USE (FIB<2N+2>=FIB<N> (N (TIMES 2 N))))))

This formula can be simplified, using the abbreviation TIMES-4=TIMES-2-2, to:

      T,

which simplifies, obviously, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

FIB<4N+2>=FIB<2N>


(PROVE-LEMMA SUM-FIB<4K+2>=FIB<2N> NIL
             (EQUAL (SUM-FIB<4K+2> N)
                    (TIMES (FIB (ADD1 (ADD1 (TIMES 2 N))))
                           (FIB (ADD1 (ADD1 (TIMES 2 N))))))
             ((DISABLE TIMES-4=TIMES-2-2)))

This conjecture simplifies, rewriting with the lemmas TIMES-2,
COMMUTATIVITY-OF-PLUS, SUB1-ADD1, ADD1-EQUAL,
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, COMMUTATIVITY-OF-TIMES, and
ASSOCIATIVITY-OF-PLUS, and unfolding the functions NUMBERP and FIB, to:

      (EQUAL (SUM-FIB<4K+2> N)
             (PLUS (TIMES (FIB (PLUS N N))
                          (FIB (PLUS N N)))
                   (TIMES (FIB (PLUS N N))
                          (FIB (ADD1 (PLUS N N))))
                   (TIMES (FIB (PLUS N N))
                          (FIB (ADD1 (PLUS N N))))
                   (TIMES (FIB (ADD1 (PLUS N N)))
                          (FIB (ADD1 (PLUS N N)))))).

Name the above subgoal *1.


     Perhaps we can prove it by induction.  The recursive terms in the
conjecture suggest nine inductions.  However, they merge into one likely
candidate induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP N) (p N))
           (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
                    (p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each induction step of the scheme.  The above induction
scheme produces the following two new formulas:

Case 2. (IMPLIES (ZEROP N)
                 (EQUAL (SUM-FIB<4K+2> N)
                        (PLUS (TIMES (FIB (PLUS N N))
                                     (FIB (PLUS N N)))
                              (TIMES (FIB (PLUS N N))
                                     (FIB (ADD1 (PLUS N N))))
                              (TIMES (FIB (PLUS N N))
                                     (FIB (ADD1 (PLUS N N))))
                              (TIMES (FIB (ADD1 (PLUS N N)))
                                     (FIB (ADD1 (PLUS N N))))))).

  This simplifies, rewriting with the lemma PLUS-RIGHT-ID2, and unfolding
  ZEROP, SUM-FIB<4K+2>, PLUS, FIB, TIMES, ADD1, and EQUAL, to:

        T.

Case 1. (IMPLIES
             (AND (NOT (ZEROP N))
                  (EQUAL (SUM-FIB<4K+2> (SUB1 N))
                         (PLUS (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                      (FIB (PLUS (SUB1 N) (SUB1 N))))
                               (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                      (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                               (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                      (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                               (TIMES (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))
                                      (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))))))
             (EQUAL (SUM-FIB<4K+2> N)
                    (PLUS (TIMES (FIB (PLUS N N))
                                 (FIB (PLUS N N)))
                          (TIMES (FIB (PLUS N N))
                                 (FIB (ADD1 (PLUS N N))))
                          (TIMES (FIB (PLUS N N))
                                 (FIB (ADD1 (PLUS N N))))
                          (TIMES (FIB (ADD1 (PLUS N N)))
                                 (FIB (ADD1 (PLUS N N))))))).

  This simplifies, rewriting with COMMUTATIVITY-OF-PLUS, TIMES-2, SUB1-ADD1,
  ADD1-EQUAL, COMMUTATIVITY2-OF-PLUS, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS,
  COMMUTATIVITY-OF-TIMES, ASSOCIATIVITY-OF-PLUS, and FIB<4N+2>=FIB<2N>, and
  expanding the functions ZEROP, SUM-FIB<4K+2>, PLUS, NUMBERP, and FIB, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.3 0.0 ]

SUM-FIB<4K+2>=FIB<2N>


(PROVE-LEMMA FIB<4N+3>=FIB<2N>
             (REWRITE)
             (EQUAL (FIB (ADD1 (ADD1 (ADD1 (TIMES 4 N)))))
                    (PLUS (TIMES (FIB (ADD1 (TIMES 2 N)))
                                 (FIB (ADD1 (TIMES 2 N))))
                          (TIMES (FIB (ADD1 (ADD1 (TIMES 2 N))))
                                 (FIB (ADD1 (ADD1 (TIMES 2 N)))))))
             ((USE (FIB<2N+1>=FIB<N> (N (ADD1 (TIMES 2 N)))))))

This formula can be simplified, using the abbreviation TIMES-4=TIMES-2-2, to
the new formula:

      (IMPLIES (EQUAL (FIB (ADD1 (TIMES 2 (ADD1 (TIMES 2 N)))))
                      (PLUS (TIMES (FIB (ADD1 (TIMES 2 N)))
                                   (FIB (ADD1 (TIMES 2 N))))
                            (TIMES (FIB (ADD1 (ADD1 (TIMES 2 N))))
                                   (FIB (ADD1 (ADD1 (TIMES 2 N)))))))
               (EQUAL (FIB (ADD1 (ADD1 (ADD1 (TIMES 2 2 N)))))
                      (PLUS (TIMES (FIB (ADD1 (TIMES 2 N)))
                                   (FIB (ADD1 (TIMES 2 N))))
                            (TIMES (FIB (ADD1 (ADD1 (TIMES 2 N))))
                                   (FIB (ADD1 (ADD1 (TIMES 2 N)))))))),

which simplifies, rewriting with TIMES-2, PLUS-ADD1, ASSOCIATIVITY-OF-PLUS,
COMMUTATIVITY-OF-PLUS, SUB1-ADD1, ADD1-EQUAL, COMMUTATIVITY2-OF-PLUS,
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and COMMUTATIVITY-OF-TIMES, and expanding
NUMBERP and FIB, to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

FIB<4N+3>=FIB<2N>


(PROVE-LEMMA SUM-FIB<4K+3>=FIB<2N> NIL
             (EQUAL (SUM-FIB<4K+3> N)
                    (TIMES (FIB (ADD1 (ADD1 (ADD1 (TIMES 2 N)))))
                           (FIB (ADD1 (ADD1 (TIMES 2 N))))))
             ((DISABLE TIMES-4=TIMES-2-2)))

This simplifies, applying TIMES-2, COMMUTATIVITY-OF-PLUS, SUB1-ADD1,
ADD1-EQUAL, COMMUTATIVITY2-OF-PLUS, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS,
COMMUTATIVITY-OF-TIMES, and ASSOCIATIVITY-OF-PLUS, and expanding the
definitions of NUMBERP and FIB, to the new goal:

      (EQUAL (SUM-FIB<4K+3> N)
             (PLUS (TIMES (FIB (PLUS N N))
                          (FIB (PLUS N N)))
                   (TIMES (FIB (PLUS N N))
                          (FIB (ADD1 (PLUS N N))))
                   (TIMES (FIB (PLUS N N))
                          (FIB (ADD1 (PLUS N N))))
                   (TIMES (FIB (PLUS N N))
                          (FIB (ADD1 (PLUS N N))))
                   (TIMES (FIB (ADD1 (PLUS N N)))
                          (FIB (ADD1 (PLUS N N))))
                   (TIMES (FIB (ADD1 (PLUS N N)))
                          (FIB (ADD1 (PLUS N N)))))),

which we will name *1.


     We will appeal to induction.  The recursive terms in the conjecture
suggest 13 inductions.  However, they merge into one likely candidate
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP N) (p N))
           (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
                    (p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT N) decreases according to the well-founded relation
LESSP in each induction step of the scheme.  The above induction scheme
generates the following two new conjectures:

Case 2. (IMPLIES (ZEROP N)
                 (EQUAL (SUM-FIB<4K+3> N)
                        (PLUS (TIMES (FIB (PLUS N N))
                                     (FIB (PLUS N N)))
                              (TIMES (FIB (PLUS N N))
                                     (FIB (ADD1 (PLUS N N))))
                              (TIMES (FIB (PLUS N N))
                                     (FIB (ADD1 (PLUS N N))))
                              (TIMES (FIB (PLUS N N))
                                     (FIB (ADD1 (PLUS N N))))
                              (TIMES (FIB (ADD1 (PLUS N N)))
                                     (FIB (ADD1 (PLUS N N))))
                              (TIMES (FIB (ADD1 (PLUS N N)))
                                     (FIB (ADD1 (PLUS N N))))))).

  This simplifies, rewriting with PLUS-RIGHT-ID2, and opening up ZEROP,
  SUM-FIB<4K+3>, PLUS, FIB, TIMES, ADD1, and EQUAL, to:

        T.

Case 1. (IMPLIES
             (AND (NOT (ZEROP N))
                  (EQUAL (SUM-FIB<4K+3> (SUB1 N))
                         (PLUS (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                      (FIB (PLUS (SUB1 N) (SUB1 N))))
                               (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                      (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                               (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                      (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                               (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                      (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                               (TIMES (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))
                                      (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                               (TIMES (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))
                                      (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))))))
             (EQUAL (SUM-FIB<4K+3> N)
                    (PLUS (TIMES (FIB (PLUS N N))
                                 (FIB (PLUS N N)))
                          (TIMES (FIB (PLUS N N))
                                 (FIB (ADD1 (PLUS N N))))
                          (TIMES (FIB (PLUS N N))
                                 (FIB (ADD1 (PLUS N N))))
                          (TIMES (FIB (PLUS N N))
                                 (FIB (ADD1 (PLUS N N))))
                          (TIMES (FIB (ADD1 (PLUS N N)))
                                 (FIB (ADD1 (PLUS N N))))
                          (TIMES (FIB (ADD1 (PLUS N N)))
                                 (FIB (ADD1 (PLUS N N))))))),

  which simplifies, applying the lemmas COMMUTATIVITY-OF-PLUS, TIMES-2,
  SUB1-ADD1, ADD1-EQUAL, COMMUTATIVITY2-OF-PLUS,
  DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, COMMUTATIVITY-OF-TIMES,
  ASSOCIATIVITY-OF-PLUS, FIB<4N+3>=FIB<2N>, and CORRECTNESS-OF-CANCEL, and
  opening up the definitions of ZEROP, SUM-FIB<4K+3>, PLUS, NUMBERP, and FIB,
  to:

        (IMPLIES
             (AND (NOT (EQUAL N 0))
                  (NUMBERP N)
                  (EQUAL (SUM-FIB<4K+3> (SUB1 N))
                         (PLUS (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                      (FIB (PLUS (SUB1 N) (SUB1 N))))
                               (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                      (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                               (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                      (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                               (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                      (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                               (TIMES (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))
                                      (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                               (TIMES (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))
                                      (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))))))
             (EQUAL (PLUS (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                 (FIB (PLUS (SUB1 N) (SUB1 N))))
                          (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                 (FIB (PLUS (SUB1 N) (SUB1 N))))
                          (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                 (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                          (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                 (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                          (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                 (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                          (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                 (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                          (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                 (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                          (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                 (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                          (TIMES (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))
                                 (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                          (TIMES (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))
                                 (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                          (TIMES (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))
                                 (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N)))))
                          (TIMES (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))
                                 (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))))
                    (PLUS (SUM-FIB<4K+3> (SUB1 N))
                          (SUM-FIB<4K+3> (SUB1 N))))).

  However this again simplifies, using linear arithmetic, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.6 0.0 ]

SUM-FIB<4K+3>=FIB<2N>


(PROVE-LEMMA FIB<2N>=FIB<N> NIL
             (IMPLIES (LESSP 0 N)
                      (EQUAL (FIB (TIMES 2 N))
                             (PLUS (TIMES (FIB (SUB1 N)) (FIB N))
                                   (TIMES (FIB N) (FIB (ADD1 N))))))
             ((USE (FIB<2N+2>=FIB<N> (N (SUB1 N))))))

This conjecture simplifies, appealing to the lemmas TIMES-2,
COMMUTATIVITY-OF-PLUS, SUB1-ADD1, ADD1-EQUAL, ADD1-SUB1,
COMMUTATIVITY-OF-TIMES, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS,
ASSOCIATIVITY-OF-PLUS, and COMMUTATIVITY2-OF-PLUS, and expanding the
definitions of NUMBERP, FIB, LESSP, EQUAL, and PLUS, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

FIB<2N>=FIB<N>


(PROVE-LEMMA FIB<4N>=FIB<2N>
             (REWRITE)
             (IMPLIES (LESSP 0 N)
                      (EQUAL (FIB (TIMES 4 N))
                             (PLUS (TIMES (FIB (SUB1 (TIMES 2 N)))
                                          (FIB (TIMES 2 N)))
                                   (TIMES (FIB (TIMES 2 N))
                                          (FIB (ADD1 (TIMES 2 N)))))))
             ((USE (FIB<2N>=FIB<N> (N (TIMES 2 N))))))

This conjecture can be simplified, using the abbreviations IMPLIES and
TIMES-4=TIMES-2-2, to the formula:

      (IMPLIES (AND (IMPLIES (LESSP 0 (TIMES 2 N))
                             (EQUAL (FIB (TIMES 2 2 N))
                                    (PLUS (TIMES (FIB (SUB1 (TIMES 2 N)))
                                                 (FIB (TIMES 2 N)))
                                          (TIMES (FIB (TIMES 2 N))
                                                 (FIB (ADD1 (TIMES 2 N)))))))
                    (LESSP 0 N))
               (EQUAL (FIB (TIMES 2 2 N))
                      (PLUS (TIMES (FIB (SUB1 (TIMES 2 N)))
                                   (FIB (TIMES 2 N)))
                            (TIMES (FIB (TIMES 2 N))
                                   (FIB (ADD1 (TIMES 2 N))))))).

This simplifies, applying TIMES-2, PLUS-EQUAL-0, ASSOCIATIVITY-OF-PLUS,
COMMUTATIVITY-OF-TIMES, and COMMUTATIVITY-OF-PLUS, and unfolding the functions
EQUAL, LESSP, and IMPLIES, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

FIB<4N>=FIB<2N>


(PROVE-LEMMA SUM-FIB<4K>=FIB<2N> NIL
             (EQUAL (SUM-FIB<4K> N)
                    (TIMES (FIB (TIMES 2 N))
                           (FIB (ADD1 (ADD1 (TIMES 2 N))))))
             ((DISABLE TIMES-4=TIMES-2-2)))

This simplifies, applying TIMES-2, COMMUTATIVITY-OF-PLUS, SUB1-ADD1,
ADD1-EQUAL, and DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and unfolding NUMBERP and
FIB, to the new conjecture:

      (EQUAL (SUM-FIB<4K> N)
             (PLUS (TIMES (FIB (PLUS N N))
                          (FIB (PLUS N N)))
                   (TIMES (FIB (PLUS N N))
                          (FIB (ADD1 (PLUS N N)))))),

which we will name *1.


     Perhaps we can prove it by induction.  There are five plausible
inductions.  However, they merge into one likely candidate induction.  We will
induct according to the following scheme:
      (AND (IMPLIES (ZEROP N) (p N))
           (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
                    (p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT N) decreases according to the well-founded relation
LESSP in each induction step of the scheme.  The above induction scheme
generates the following two new goals:

Case 2. (IMPLIES (ZEROP N)
                 (EQUAL (SUM-FIB<4K> N)
                        (PLUS (TIMES (FIB (PLUS N N))
                                     (FIB (PLUS N N)))
                              (TIMES (FIB (PLUS N N))
                                     (FIB (ADD1 (PLUS N N))))))).

  This simplifies, applying PLUS-RIGHT-ID2, and unfolding the functions ZEROP,
  SUM-FIB<4K>, PLUS, FIB, TIMES, ADD1, and EQUAL, to:

        T.

Case 1. (IMPLIES
             (AND (NOT (ZEROP N))
                  (EQUAL (SUM-FIB<4K> (SUB1 N))
                         (PLUS (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                      (FIB (PLUS (SUB1 N) (SUB1 N))))
                               (TIMES (FIB (PLUS (SUB1 N) (SUB1 N)))
                                      (FIB (ADD1 (PLUS (SUB1 N) (SUB1 N))))))))
             (EQUAL (SUM-FIB<4K> N)
                    (PLUS (TIMES (FIB (PLUS N N))
                                 (FIB (PLUS N N)))
                          (TIMES (FIB (PLUS N N))
                                 (FIB (ADD1 (PLUS N N))))))),

  which simplifies, rewriting with COMMUTATIVITY-OF-PLUS, TIMES-2, SUB1-ADD1,
  ADD1-EQUAL, COMMUTATIVITY-OF-TIMES, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS,
  COMMUTATIVITY2-OF-PLUS, ASSOCIATIVITY-OF-PLUS, and FIB<4N>=FIB<2N>, and
  opening up the functions ZEROP, SUM-FIB<4K>, LESSP, EQUAL, PLUS, NUMBERP,
  and FIB, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.1 0.0 ]

SUM-FIB<4K>=FIB<2N>