(NOTE-LIB "proveall")



(DEFINE (^BM^BC N M)
 (IF (^BM^ZEROP M)
     (^INT (^BM^CONS (^1) (^BM^ZERO)))
     (IF (^BM^LESSP N M)
         (^INT (^BM^ZERO))
         (^BM^PLUS (^BM^BC (^BM^SUB1 N) M)
          (^BM^BC (^BM^SUB1 N) (^BM^SUB1 M))))))



(LEMMA
 (EQUAL (^BM^FOR X (^BM^APPEND A B) TEST
         (^BM^PACK (^BM^CONS ^S (^BM^CONS ^U (^BM^CONS ^M (^BM^ZERO))))) BODY
         ALIST)
        (^BM^PLUS
         (^BM^FOR X A TEST
          (^BM^PACK (^BM^CONS ^S (^BM^CONS ^U (^BM^CONS ^M (^BM^ZERO))))) BODY
          ALIST)
         (^BM^FOR X B TEST
          (^BM^PACK (^BM^CONS ^S (^BM^CONS ^U (^BM^CONS ^M (^BM^ZERO))))) BODY
          ALIST))))



(LEMMA (EQUAL (^BM^BC X (^BM^ADD1 X)) (^INT (^BM^ZERO))))



(LEMMA (EQUAL (^BM^BC X X) (^INT (^BM^CONS (^1) (^BM^ZERO)))))



(LEMMA
 (EQUAL (^BM^FROM-TO (^INT (^BM^ZERO)) B)
        (^BM^CONS (^INT (^BM^ZERO))
         (^BM^FROM-TO (^INT (^BM^CONS (^1) (^BM^ZERO))) B))))



(LEMMA
 (EQUAL (^BM^MEMBER I (^BM^FROM-TO A B))
        (^BM^AND (^BM^NUMBERP I)
         (^BM^AND (^BM^NOT (^BM^LESSP I A)) (^BM^NOT (^BM^LESSP B I))))))



(LEMMA
 (EQUAL (^BM^FOR I RANGE TEST
         (^BM^PACK (^BM^CONS ^S (^BM^CONS ^U (^BM^CONS ^M (^BM^ZERO)))))
         (^BM^CONS
          (^BM^PACK
           (^BM^CONS ^P (^BM^CONS ^L (^BM^CONS ^U (^BM^CONS ^S (^BM^ZERO))))))
          (^BM^CONS A (^BM^CONS B (^NIL))))
         ALIST)
        (^BM^PLUS
         (^BM^FOR I RANGE TEST
          (^BM^PACK (^BM^CONS ^S (^BM^CONS ^U (^BM^CONS ^M (^BM^ZERO))))) A
          ALIST)
         (^BM^FOR I RANGE TEST
          (^BM^PACK (^BM^CONS ^S (^BM^CONS ^U (^BM^CONS ^M (^BM^ZERO))))) B
          ALIST))))



(LEMMA
 (EQUAL (^BM^TIMES (^BM^PLUS A B) C)
        (^BM^PLUS (^BM^TIMES A C) (^BM^TIMES B C))))



(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP I)) (^BM^NOT (^BM^LESSP X I)))
  (EQUAL (^BM^DIFFERENCE X (^BM^SUB1 I)) (^BM^ADD1 (^BM^DIFFERENCE X I)))))



(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^NLISTP ONE) (^BM^NOT (EQUAL ONE VAR)))
  (EQUAL (^BM^FOR VAR RANGE CONDITION
          (^BM^PACK (^BM^CONS ^S (^BM^CONS ^U (^BM^CONS ^M (^BM^ZERO)))))
          (^BM^CONS
           (^BM^PACK
            (^BM^CONS ^T
             (^BM^CONS ^I
              (^BM^CONS ^M (^BM^CONS ^E (^BM^CONS ^S (^BM^ZERO)))))))
           (^BM^CONS ONE (^BM^CONS TWO (^NIL))))
          ALIST)
         (^BM^TIMES (^BM^EVAL$ (^BM^TRUE) ONE ALIST)
          (^BM^FOR VAR RANGE CONDITION
           (^BM^PACK (^BM^CONS ^S (^BM^CONS ^U (^BM^CONS ^M (^BM^ZERO))))) TWO
           ALIST)))))



(LEMMA (EQUAL (^BM^LESSP I (^INT (^BM^CONS (^1) (^BM^ZERO)))) (^BM^ZEROP I)))



(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP I))
  (EQUAL (^BM^LESSP X (^BM^SUB1 I))
         (^BM^AND (^BM^LESSP X I) (^BM^NOT (EQUAL (^BM^FIX X) (^BM^SUB1 I)))))))



(LEMMA
 (EQUAL (^BM^FOR I L COND
         (^BM^PACK (^BM^CONS ^S (^BM^CONS ^U (^BM^CONS ^M (^BM^ZERO)))))
         (^BM^CONS
          (^BM^PACK
           (^BM^CONS ^Q
            (^BM^CONS ^U
             (^BM^CONS ^O (^BM^CONS ^T (^BM^CONS ^E (^BM^ZERO)))))))
          (^BM^CONS (^INT (^BM^ZERO))
           (^BM^PACK (^BM^CONS ^N (^BM^CONS ^I (^BM^CONS ^L (^BM^ZERO)))))))
         ALIST)
        (^INT (^BM^ZERO))))



(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP N))
  (EQUAL (^BM^FOR I IN (^BM^FROM-TO (^INT (^BM^CONS (^1) (^BM^ZERO))) N) SUM
          (^BM^TIMES (^BM^EXP A I)
           (^BM^TIMES (^BM^BC X (^BM^SUB1 I))
            (^BM^EXP B (^BM^DIFFERENCE X I)))))
         (^BM^FOR I IN (^BM^FROM-TO (^INT (^BM^ZERO)) (^BM^SUB1 N)) SUM
          (^BM^TIMES (^BM^EXP A (^BM^ADD1 I))
           (^BM^TIMES (^BM^BC X I)
            (^BM^EXP B (^BM^DIFFERENCE X (^BM^ADD1 I)))))))))



(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP X)
   (^BM^AND (^BM^NOT (EQUAL X (^INT (^BM^ZERO))))
    (^BM^AND (^BM^NOT (EQUAL (^INT (^BM^CONS (^1) (^BM^ZERO))) X))
     (^BM^NOT (EQUAL (^BM^SUB1 X) (^INT (^BM^ZERO)))))))
  (EQUAL (^BM^TIMES A
          (^BM^FOR I IN
           (^BM^FROM-TO (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^SUB1 X)) SUM
           (^BM^TIMES (^BM^BC X I)
            (^BM^TIMES (^BM^EXP A I) (^BM^EXP B (^BM^DIFFERENCE X I))))))
         (^BM^TIMES A
          (^BM^TIMES B
           (^BM^FOR I IN
            (^BM^FROM-TO (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^SUB1 X)) SUM
            (^BM^TIMES (^BM^BC X I)
             (^BM^TIMES (^BM^EXP A I)
              (^BM^EXP B (^BM^DIFFERENCE (^BM^SUB1 X) I))))))))))



(LEMMA
 (EQUAL (^BM^EXP (^BM^PLUS A B) N)
        (^BM^FOR I IN (^BM^FROM-TO (^INT (^BM^ZERO)) N) SUM
         (^BM^TIMES (^BM^BC N I)
          (^BM^TIMES (^BM^EXP A I) (^BM^EXP B (^BM^DIFFERENCE N I)))))))