(NOTE-LIB "proveall")

(DEFINE (^BM^FIB N)
 (IF (^BM^ZEROP N)
     (^INT (^BM^ZERO))
     (IF (EQUAL N (^INT (^BM^CONS (^1) (^BM^ZERO))))
         (^INT (^BM^CONS (^1) (^BM^ZERO)))
         (^BM^PLUS (^BM^FIB (^BM^SUB1 N)) (^BM^FIB (^BM^SUB1 (^BM^SUB1 N)))))))

(DEFINE (^BM^NBR-CALLS-FIB N)
 (IF (^BM^ZEROP N)
     (^INT (^BM^CONS (^1) (^BM^ZERO)))
     (IF (EQUAL N (^INT (^BM^CONS (^1) (^BM^ZERO))))
         (^INT (^BM^CONS (^1) (^BM^ZERO)))
         (^BM^ADD1
          (^BM^PLUS (^BM^NBR-CALLS-FIB (^BM^SUB1 N))
           (^BM^NBR-CALLS-FIB (^BM^SUB1 (^BM^SUB1 N))))))))

(DEFINE (^BM^NBR-PLUS-FIB N)
 (IF (^BM^ZEROP N)
     (^INT (^BM^ZERO))
     (IF (EQUAL N (^INT (^BM^CONS (^1) (^BM^ZERO))))
         (^INT (^BM^ZERO))
         (^BM^ADD1
          (^BM^PLUS (^BM^NBR-PLUS-FIB (^BM^SUB1 N))
           (^BM^NBR-PLUS-FIB (^BM^SUB1 (^BM^SUB1 N))))))))

(LEMMA
 (EQUAL (^BM^ADD1 (^BM^NBR-CALLS-FIB N))
        (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^FIB (^BM^ADD1 N)))))

(LEMMA
 (EQUAL (^BM^NBR-CALLS-FIB N)
        (^BM^SUB1
         (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^FIB (^BM^ADD1 N))))))

(LEMMA (EQUAL (^BM^ADD1 (^BM^NBR-PLUS-FIB N)) (^BM^FIB (^BM^ADD1 N))))

(LEMMA (EQUAL (^BM^NBR-PLUS-FIB N) (^BM^SUB1 (^BM^FIB (^BM^ADD1 N)))))

(DEFINE (^BM^SUM-FIB<K> N)
 (IF (^BM^ZEROP N)
     (^INT (^BM^ZERO))
     (^BM^PLUS (^BM^SUM-FIB<K> (^BM^SUB1 N)) (^BM^FIB N))))

(LEMMA (EQUAL (^BM^ADD1 (^BM^SUM-FIB<K> N)) (^BM^FIB (^BM^ADD1 (^BM^ADD1 N)))))

(LEMMA (EQUAL (^BM^SUM-FIB<K> N) (^BM^SUB1 (^BM^FIB (^BM^ADD1 (^BM^ADD1 N))))))

(LEMMA (EQUAL (^BM^SUM-FIB<K> N) (^BM^NBR-PLUS-FIB (^BM^ADD1 N))))

(DEFINE (^BM^SUM-FIB<2K> N)
 (IF (^BM^ZEROP N)
     (^INT (^BM^ZERO))
     (^BM^PLUS (^BM^SUM-FIB<2K> (^BM^SUB1 N))
      (^BM^FIB (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N)))))

(LEMMA
 (EQUAL (^BM^ADD1 (^BM^SUM-FIB<2K> N))
        (^BM^FIB (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N)))))

(LEMMA
 (EQUAL (^BM^SUM-FIB<2K> N)
        (^BM^SUB1
         (^BM^FIB (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))))))

(DEFINE (^BM^SUM-FIB<2K+1> N)
 (IF (^BM^ZEROP N)
     (^INT (^BM^CONS (^1) (^BM^ZERO)))
     (^BM^PLUS (^BM^SUM-FIB<2K+1> (^BM^SUB1 N))
      (^BM^FIB (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))))))

(LEMMA
 (EQUAL (^BM^SUM-FIB<2K+1> N)
        (^BM^FIB
         (^BM^ADD1
          (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))))))

(DEFINE (^BM^SUM-FIB<3K> N)
 (IF (^BM^ZEROP N)
     (^INT (^BM^ZERO))
     (^BM^PLUS (^BM^SUM-FIB<3K> (^BM^SUB1 N))
      (^BM^FIB (^BM^TIMES (^INT (^BM^CONS (^3) (^BM^ZERO))) N)))))

(LEMMA
 (EQUAL (^BM^ADD1
         (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^SUM-FIB<3K> N)))
        (^BM^FIB
         (^BM^ADD1
          (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^3) (^BM^ZERO))) N))))))

(LEMMA
 (EQUAL (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^SUM-FIB<3K> N))
        (^BM^SUB1
         (^BM^FIB
          (^BM^ADD1
           (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^3) (^BM^ZERO))) N)))))))

(LEMMA
 (EQUAL (^BM^SUM-FIB<3K> N)
        (^BM^QUOTIENT
         (^BM^SUB1
          (^BM^FIB
           (^BM^ADD1
            (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^3) (^BM^ZERO))) N)))))
         (^INT (^BM^CONS (^2) (^BM^ZERO))))))

(DEFINE (^BM^SUM-FIB<3K+1> N)
 (IF (^BM^ZEROP N)
     (^INT (^BM^CONS (^1) (^BM^ZERO)))
     (^BM^PLUS (^BM^SUM-FIB<3K+1> (^BM^SUB1 N))
      (^BM^FIB (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^3) (^BM^ZERO))) N))))))

(LEMMA
 (EQUAL (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^SUM-FIB<3K+1> N))
        (^BM^FIB
         (^BM^ADD1
          (^BM^ADD1
           (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^3) (^BM^ZERO))) N)))))))

(LEMMA
 (EQUAL (^BM^SUM-FIB<3K+1> N)
        (^BM^QUOTIENT
         (^BM^FIB
          (^BM^ADD1
           (^BM^ADD1
            (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^3) (^BM^ZERO))) N)))))
         (^INT (^BM^CONS (^2) (^BM^ZERO))))))

(DEFINE (^BM^SUM-FIB<3K+2> N)
 (IF (^BM^ZEROP N)
     (^INT (^BM^CONS (^1) (^BM^ZERO)))
     (^BM^PLUS (^BM^SUM-FIB<3K+2> (^BM^SUB1 N))
      (^BM^FIB
       (^BM^ADD1 (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^3) (^BM^ZERO))) N)))))))

(LEMMA
 (EQUAL (^BM^ADD1
         (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^SUM-FIB<3K+2> N)))
        (^BM^FIB
         (^BM^ADD1
          (^BM^ADD1
           (^BM^ADD1
            (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^3) (^BM^ZERO))) N))))))))

(LEMMA
 (EQUAL (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^SUM-FIB<3K+2> N))
        (^BM^SUB1
         (^BM^FIB
          (^BM^ADD1
           (^BM^ADD1
            (^BM^ADD1
             (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^3) (^BM^ZERO))) N)))))))))

(LEMMA
 (EQUAL (^BM^SUM-FIB<3K+2> N)
        (^BM^QUOTIENT
         (^BM^SUB1
          (^BM^FIB
           (^BM^ADD1
            (^BM^ADD1
             (^BM^ADD1
              (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^3) (^BM^ZERO))) N)))))))
         (^INT (^BM^CONS (^2) (^BM^ZERO))))))

(LEMMA
 (^BM^AND
  (EQUAL (^BM^FIB (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N)))
         (^BM^PLUS (^BM^TIMES (^BM^FIB N) (^BM^FIB N))
          (^BM^TIMES (^BM^FIB (^BM^ADD1 N)) (^BM^FIB (^BM^ADD1 N)))))
  (EQUAL (^BM^FIB
          (^BM^ADD1
           (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))))
         (^BM^PLUS (^BM^TIMES (^BM^FIB N) (^BM^FIB (^BM^ADD1 N)))
          (^BM^TIMES (^BM^FIB (^BM^ADD1 N))
           (^BM^FIB (^BM^ADD1 (^BM^ADD1 N))))))))

(LEMMA
 (EQUAL (^BM^FIB (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N)))
        (^BM^PLUS (^BM^TIMES (^BM^FIB N) (^BM^FIB N))
         (^BM^TIMES (^BM^FIB (^BM^ADD1 N)) (^BM^FIB (^BM^ADD1 N))))))

(LEMMA
 (EQUAL (^BM^FIB
         (^BM^ADD1 (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))))
        (^BM^PLUS (^BM^TIMES (^BM^FIB N) (^BM^FIB (^BM^ADD1 N)))
         (^BM^TIMES (^BM^FIB (^BM^ADD1 N)) (^BM^FIB (^BM^ADD1 (^BM^ADD1 N)))))))

(DEFINE (^BM^SUM-FIB<4K> N)
 (IF (^BM^ZEROP N)
     (^INT (^BM^ZERO))
     (^BM^PLUS (^BM^SUM-FIB<4K> (^BM^SUB1 N))
      (^BM^FIB (^BM^TIMES (^INT (^BM^CONS (^4) (^BM^ZERO))) N)))))

(DEFINE (^BM^SUM-FIB<4K+1> N)
 (IF (^BM^ZEROP N)
     (^INT (^BM^CONS (^1) (^BM^ZERO)))
     (^BM^PLUS (^BM^SUM-FIB<4K+1> (^BM^SUB1 N))
      (^BM^FIB (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^4) (^BM^ZERO))) N))))))

(DEFINE (^BM^SUM-FIB<4K+2> N)
 (IF (^BM^ZEROP N)
     (^INT (^BM^CONS (^1) (^BM^ZERO)))
     (^BM^PLUS (^BM^SUM-FIB<4K+2> (^BM^SUB1 N))
      (^BM^FIB
       (^BM^ADD1 (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^4) (^BM^ZERO))) N)))))))

(DEFINE (^BM^SUM-FIB<4K+3> N)
 (IF (^BM^ZEROP N)
     (^INT (^BM^CONS (^2) (^BM^ZERO)))
     (^BM^PLUS (^BM^SUM-FIB<4K+3> (^BM^SUB1 N))
      (^BM^FIB
       (^BM^ADD1
        (^BM^ADD1
         (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^4) (^BM^ZERO))) N))))))))

(LEMMA
 (EQUAL (^BM^TIMES (^INT (^BM^CONS (^4) (^BM^ZERO))) N)
        (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO)))
         (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))))

(LEMMA
 (EQUAL (^BM^FIB (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^4) (^BM^ZERO))) N)))
        (^BM^PLUS
         (^BM^TIMES (^BM^FIB (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))
          (^BM^FIB (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N)))
         (^BM^TIMES
          (^BM^FIB (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N)))
          (^BM^FIB
           (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N)))))))

(LEMMA
 (EQUAL (^BM^SUM-FIB<4K+1> N)
        (^BM^TIMES
         (^BM^FIB (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N)))
         (^BM^FIB
          (^BM^ADD1
           (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N)))))))

(LEMMA
 (EQUAL (^BM^FIB
         (^BM^ADD1 (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^4) (^BM^ZERO))) N))))
        (^BM^PLUS
         (^BM^TIMES (^BM^FIB (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))
          (^BM^FIB (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))))
         (^BM^TIMES
          (^BM^FIB (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N)))
          (^BM^FIB
           (^BM^ADD1
            (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))))))))

(LEMMA
 (EQUAL (^BM^SUM-FIB<4K+2> N)
        (^BM^TIMES
         (^BM^FIB
          (^BM^ADD1
           (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))))
         (^BM^FIB
          (^BM^ADD1
           (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N)))))))

(LEMMA
 (EQUAL (^BM^FIB
         (^BM^ADD1
          (^BM^ADD1
           (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^4) (^BM^ZERO))) N)))))
        (^BM^PLUS
         (^BM^TIMES
          (^BM^FIB (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N)))
          (^BM^FIB (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))))
         (^BM^TIMES
          (^BM^FIB
           (^BM^ADD1
            (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))))
          (^BM^FIB
           (^BM^ADD1
            (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))))))))

(LEMMA
 (EQUAL (^BM^SUM-FIB<4K+3> N)
        (^BM^TIMES
         (^BM^FIB
          (^BM^ADD1
           (^BM^ADD1
            (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N)))))
         (^BM^FIB
          (^BM^ADD1
           (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N)))))))

(LEMMA
 (^BM^IMPLIES (^BM^LESSP (^INT (^BM^ZERO)) N)
  (EQUAL (^BM^FIB (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))
         (^BM^PLUS (^BM^TIMES (^BM^FIB (^BM^SUB1 N)) (^BM^FIB N))
          (^BM^TIMES (^BM^FIB N) (^BM^FIB (^BM^ADD1 N)))))))

(LEMMA
 (^BM^IMPLIES (^BM^LESSP (^INT (^BM^ZERO)) N)
  (EQUAL (^BM^FIB (^BM^TIMES (^INT (^BM^CONS (^4) (^BM^ZERO))) N))
         (^BM^PLUS
          (^BM^TIMES
           (^BM^FIB (^BM^SUB1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N)))
           (^BM^FIB (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N)))
          (^BM^TIMES (^BM^FIB (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))
           (^BM^FIB
            (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))))))))

(LEMMA
 (EQUAL (^BM^SUM-FIB<4K> N)
        (^BM^TIMES (^BM^FIB (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N))
         (^BM^FIB
          (^BM^ADD1
           (^BM^ADD1 (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) N)))))))