(NOTE-LIB "nqthm-boot")

(DEFINE (^BM^P X) X)

(DEFINE (^BM^Q X) X)

(DEFINE (^BM^R X) X)

(LEMMA (^BM^TRUE))

(DEFINE (^BM^H X Y) (^BM^PLUS X Y))

(LEMMA (EQUAL (^BM^H X (^BM^H Y Z)) (^BM^H Y (^BM^H X Z))))

(DEFINE (^BM^PR-H L Z)
 (IF (^BM^NLISTP L) Z (^BM^H (^BM^CAR L) (^BM^PR-H (^BM^CDR L) Z))))

(DEFINE (^BM^AC-H L Z)
 (IF (^BM^NLISTP L) Z (^BM^AC-H (^BM^CDR L) (^BM^H (^BM^CAR L) Z))))

(LEMMA (EQUAL (^BM^AC-H L Z) (^BM^PR-H L Z)))

(DEFINE (^BM^PR-TIMES L Z)
 (IF (^BM^NLISTP L) Z (^BM^TIMES (^BM^CAR L) (^BM^PR-TIMES (^BM^CDR L) Z))))

(DEFINE (^BM^AC-TIMES L Z)
 (IF (^BM^NLISTP L) Z (^BM^AC-TIMES (^BM^CDR L) (^BM^TIMES (^BM^CAR L) Z))))

(DEFINE (^BM^LT X Y) (^BM^FALSE))

(LEMMA (^BM^IMPLIES (^BM^LT Z V) (^BM^NOT (^BM^LT V Z))))

(DEFINE (^BM^ORDERED-LT L)
 (IF (^BM^LISTP L)
     (IF (^BM^LISTP (^BM^CDR L))
         (IF (^BM^LT (^BM^CAR (^BM^CDR L)) (^BM^CAR L))
             (^BM^FALSE)
             (^BM^ORDERED-LT (^BM^CDR L)))
         (^BM^TRUE))
     (^BM^TRUE)))

(DEFINE (^BM^ADDTOLIST-LT X L)
 (IF (^BM^LISTP L)
     (IF (^BM^LT X (^BM^CAR L))
         (^BM^CONS X L)
         (^BM^CONS (^BM^CAR L) (^BM^ADDTOLIST-LT X (^BM^CDR L))))
     (^BM^CONS X (^NIL))))

(DEFINE (^BM^SORT-LT L)
 (IF (^BM^LISTP L)
     (^BM^ADDTOLIST-LT (^BM^CAR L) (^BM^SORT-LT (^BM^CDR L)))
     (^NIL)))

(LEMMA (^BM^ORDERED-LT (^BM^SORT-LT L)))

(DEFINE (^BM^ORDERED-LESSP L)
 (IF (^BM^LISTP L)
     (IF (^BM^LISTP (^BM^CDR L))
         (IF (^BM^LESSP (^BM^CAR (^BM^CDR L)) (^BM^CAR L))
             (^BM^FALSE)
             (^BM^ORDERED-LESSP (^BM^CDR L)))
         (^BM^TRUE))
     (^BM^TRUE)))

(DEFINE (^BM^ADDTOLIST-LESSP X L)
 (IF (^BM^LISTP L)
     (IF (^BM^LESSP X (^BM^CAR L))
         (^BM^CONS X L)
         (^BM^CONS (^BM^CAR L) (^BM^ADDTOLIST-LESSP X (^BM^CDR L))))
     (^BM^CONS X (^NIL))))

(DEFINE (^BM^SORT-LESSP L)
 (IF (^BM^LISTP L)
     (^BM^ADDTOLIST-LESSP (^BM^CAR L) (^BM^SORT-LESSP (^BM^CDR L)))
     (^NIL)))

(DEFINE (^BM^FN T76) (^BM^ADD1 T76))

(LEMMA (^BM^TRUE))

(DEFINE (^BM^MAP-FN X)
 (IF (^BM^NLISTP X)
     (^NIL)
     (^BM^CONS (^BM^FN (^BM^CAR X)) (^BM^MAP-FN (^BM^CDR X)))))

(LEMMA
 (EQUAL (^BM^MAP-FN (^BM^APPEND U V))
        (^BM^APPEND (^BM^MAP-FN U) (^BM^MAP-FN V))))

(DEFINE (^BM^MAP-PLUS-Y X Y)
 (IF (^BM^NLISTP X)
     (^NIL)
     (^BM^CONS (^BM^PLUS (^BM^CAR X) Y) (^BM^MAP-PLUS-Y (^BM^CDR X) Y))))

(DEFINE (^BM^TRUE-REC X)
 (IF (^BM^NLISTP X) (^BM^TRUE) (^BM^TRUE-REC (^BM^CDR X))))

(LEMMA (^BM^TRUE-REC X))

(DEFINE (^BM^APP X Y)
 (IF (^BM^NLISTP X) Y (^BM^CONS (^BM^CAR X) (^BM^APP (^BM^CDR X) Y))))

(DEFINE (^BM^ALL-X-P-X) (^BM^FALSE))

(LEMMA (^BM^IMPLIES (^BM^ALL-X-P-X) (^BM^P X)))

(DEFINE (^BM^ALL-X-NOT-P-X) (^BM^FALSE))

(LEMMA (^BM^IMPLIES (^BM^ALL-X-NOT-P-X) (^BM^NOT (^BM^P X))))

(LEMMA (^BM^IMPLIES (^BM^P X) (^BM^NOT (^BM^ALL-X-NOT-P-X))))

(DEFINE (^BM^SOME-X-P-X) (^BM^NOT (^BM^ALL-X-NOT-P-X)))

(LEMMA (^BM^IMPLIES (^BM^ALL-X-P-X) (^BM^SOME-X-P-X)))

(DEFINE (^BM^EVEN X)
 (IF (^BM^ZEROP X)
     (^BM^TRUE)
     (IF (EQUAL X (^INT (^BM^CONS (^1) (^BM^ZERO))))
         (^BM^FALSE)
         (^BM^NOT (^BM^EVEN (^BM^SUB1 X))))))

(DEFINE (^BM^FAIR X) (^BM^EVEN X))

(DEFINE (^BM^FAIR-TRUE-WITNESS X) (IF (^BM^EVEN X) X (^BM^ADD1 X)))

(DEFINE (^BM^FAIR-FALSE-WITNESS X) (IF (^BM^EVEN X) (^BM^ADD1 X) X))

(LEMMA
 (^BM^AND (^BM^FAIR (^BM^FAIR-TRUE-WITNESS N))
  (^BM^AND (^BM^NOT (^BM^FAIR (^BM^FAIR-FALSE-WITNESS N)))
   (^BM^AND (^BM^NOT (^BM^LESSP (^BM^FAIR-TRUE-WITNESS N) N))
    (^BM^NOT (^BM^LESSP (^BM^FAIR-FALSE-WITNESS N) N))))))

(DEFINE (^BM^NUM T76) (^BM^ADD1 T76))

(LEMMA (^BM^NUMBERP (^BM^NUM X)))

(DEFINE (^BM^INTERP X) (IF (^BM^NOT (^BM^ZEROP X)) (^BM^TIMES X X) (^BM^NUM X)))

(LEMMA (^BM^NUMBERP (^BM^INTERP X)))

(DEFINE (^BM^INTERP2 X)
 (IF (^BM^NOT (^BM^ZEROP X)) (^BM^TIMES X X) (^BM^PLUS X X)))

(DEFINE (^BM^P-ALIAS X) (^BM^P X))

(LEMMA (^BM^EVEN (^BM^P-ALIAS X)))

(LEMMA (^BM^EVEN (^BM^P X)))

(DEFINE (^BM^PP) (^INT (^BM^ZERO)))

(LEMMA (^BM^IMPLIES (EQUAL Y (^INT (^BM^ZERO))) (EQUAL (^BM^PP) Y)))

(LEMMA (EQUAL (^INT (^BM^ZERO)) (^BM^PP)))

(DEFINE (^BM^FN2 X Y) (^BM^PLUS X Y))

(LEMMA (EQUAL (^BM^FN2 X Y) (^BM^FN2 Y X)))

(DEFINE (^BM^FOLDR-FN LST R)
 (IF (^BM^LISTP LST) (^BM^FN2 (^BM^CAR LST) (^BM^FOLDR-FN (^BM^CDR LST) R)) R))

(DEFINE (^BM^FOLDL-FN LST R)
 (IF (^BM^LISTP LST) (^BM^FOLDL-FN (^BM^CDR LST) (^BM^FN2 R (^BM^CAR LST))) R))

(DEFINE (^BM^REVERSE X)
 (IF (^BM^LISTP X)
     (^BM^APPEND (^BM^REVERSE (^BM^CDR X)) (^BM^CONS (^BM^CAR X) (^NIL)))
     (^NIL)))

(LEMMA (EQUAL (^BM^FOLDR-FN LST R) (^BM^FOLDL-FN (^BM^REVERSE LST) R)))

(LEMMA (EQUAL (^BM^TIMES X (^BM^ADD1 Y)) (^BM^PLUS X (^BM^TIMES X Y))))

(LEMMA (EQUAL (^BM^TIMES X Y) (^BM^TIMES Y X)))

(DEFINE (^BM^FOLDR-TIMES LST R)
 (IF (^BM^LISTP LST)
     (^BM^TIMES (^BM^CAR LST) (^BM^FOLDR-TIMES (^BM^CDR LST) R))
     R))

(DEFINE (^BM^FOLDL-TIMES LST R)
 (IF (^BM^LISTP LST)
     (^BM^FOLDL-TIMES (^BM^CDR LST) (^BM^TIMES R (^BM^CAR LST)))
     R))