(NOTE-LIB "nqthm-boot")

(DEFINE (^BM^RT X)
 (IF (^BM^ZEROP X)
     (^INT (^BM^ZERO))
     (IF (EQUAL (^BM^TIMES (^BM^ADD1 (^BM^RT (^BM^SUB1 X)))
                 (^BM^ADD1 (^BM^RT (^BM^SUB1 X))))
                X)
         (^BM^ADD1 (^BM^RT (^BM^SUB1 X)))
         (^BM^RT (^BM^SUB1 X)))))

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

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

(LEMMA (EQUAL (EQUAL (^BM^TIMES X X) (^INT (^BM^ZERO))) (^BM^ZEROP X)))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^LESSP B A))
  (^BM^NOT (^BM^LESSP (^BM^TIMES B B) (^BM^TIMES A A)))))

(LEMMA
 (^BM^AND (^BM^NOT (^BM^LESSP Y (^BM^TIMES (^BM^RT Y) (^BM^RT Y))))
  (^BM^LESSP Y
   (^BM^ADD1
    (^BM^PLUS (^BM^RT Y)
     (^BM^PLUS (^BM^RT Y) (^BM^TIMES (^BM^RT Y) (^BM^RT Y))))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP A)
   (^BM^AND (^BM^LEQ (^BM^TIMES A A) Y)
    (^BM^LESSP Y (^BM^TIMES (^BM^ADD1 A) (^BM^ADD1 A)))))
  (EQUAL A (^BM^RT Y))))

(LEMMA
 (EQUAL (^BM^RT (^BM^PLUS U (^BM^TIMES (^BM^PLUS U V) (^BM^PLUS U V))))
        (^BM^PLUS U V)))

(DEFINE (^BM^NCAR X) (^BM^DIFFERENCE X (^BM^TIMES (^BM^RT X) (^BM^RT X))))

(DEFINE (^BM^NCDR X) (^BM^DIFFERENCE (^BM^RT X) (^BM^NCAR X)))

(DEFINE (^BM^NCONS I J) (^BM^PLUS I (^BM^TIMES (^BM^PLUS I J) (^BM^PLUS I J))))

(LEMMA (^BM^IMPLIES (^BM^NUMBERP I) (EQUAL (^BM^NCAR (^BM^NCONS I J)) I)))

(LEMMA (^BM^IMPLIES (^BM^NUMBERP J) (EQUAL (^BM^NCDR (^BM^NCONS I J)) J)))

(DEFINE (^BM^NCADR X) (^BM^NCAR (^BM^NCDR X)))

(DEFINE (^BM^NCADDR X) (^BM^NCAR (^BM^NCDR (^BM^NCDR X))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP X))
   (^BM^NOT (EQUAL X (^INT (^BM^CONS (^1) (^BM^ZERO))))))
  (^BM^LESSP (^BM^RT X) X)))

(LEMMA (^BM^NOT (^BM^LESSP X (^BM^RT X))))

(LEMMA
 (^BM^IMPLIES (^BM^LESSP X Y) (EQUAL (^BM^DIFFERENCE X Y) (^INT (^BM^ZERO)))))

(LEMMA
 (EQUAL (^BM^LESSP (^BM^DIFFERENCE A B) C)
        (IF (^BM^LESSP A B)
            (^BM^LESSP (^INT (^BM^ZERO)) C)
            (^BM^LESSP A (^BM^PLUS B C)))))

(LEMMA (^BM^NOT (^BM^LESSP X (^BM^NCAR X))))

(LEMMA (EQUAL (^BM^LESSP X (^BM^DIFFERENCE (^BM^RT X) D)) (^BM^FALSE)))

(LEMMA (^BM^NOT (^BM^LESSP X (^BM^NCDR X))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP FN)
   (^BM^AND (^BM^NOT (EQUAL (^BM^NCAR FN) (^INT (^BM^ZERO))))
    (^BM^NOT (EQUAL (^BM^NCAR FN) (^INT (^BM^CONS (^1) (^BM^ZERO)))))))
  (^BM^LESSP (^BM^NCDR FN) FN)))

(DEFINE (^BM^PR-APPLY FN ARG)
 (IF (^BM^NOT (^BM^NUMBERP FN))
     (^INT (^BM^ZERO))
     (IF (EQUAL (^BM^NCAR FN) (^INT (^BM^ZERO)))
         (^INT (^BM^ZERO))
         (IF (EQUAL (^BM^NCAR FN) (^INT (^BM^CONS (^1) (^BM^ZERO))))
             ARG
             (IF (EQUAL (^BM^NCAR FN) (^INT (^BM^CONS (^2) (^BM^ZERO))))
                 (^BM^ADD1 ARG)
                 (IF (EQUAL (^BM^NCAR FN) (^INT (^BM^CONS (^3) (^BM^ZERO))))
                     (^BM^RT ARG)
                     (IF (EQUAL (^BM^NCAR FN)
                                (^INT (^BM^CONS (^4) (^BM^ZERO))))
                         (IF (^BM^ZEROP ARG)
                             (^INT (^BM^ZERO))
                             (^BM^PR-APPLY (^BM^NCDR FN)
                              (^BM^PR-APPLY FN (^BM^SUB1 ARG))))
                         (IF (EQUAL (^BM^NCAR FN)
                                    (^INT (^BM^CONS (^5) (^BM^ZERO))))
                             (^BM^PLUS (^BM^PR-APPLY (^BM^NCADR FN) ARG)
                              (^BM^PR-APPLY (^BM^NCADDR FN) ARG))
                             (IF (EQUAL (^BM^NCAR FN)
                                        (^INT (^BM^CONS (^6) (^BM^ZERO))))
                                 (^BM^DIFFERENCE
                                  (^BM^PR-APPLY (^BM^NCADR FN) ARG)
                                  (^BM^PR-APPLY (^BM^NCADDR FN) ARG))
                                 (IF (EQUAL (^BM^NCAR FN)
                                            (^INT (^BM^CONS (^7) (^BM^ZERO))))
                                     (^BM^TIMES
                                      (^BM^PR-APPLY (^BM^NCADR FN) ARG)
                                      (^BM^PR-APPLY (^BM^NCADDR FN) ARG))
                                     (IF (EQUAL
                                          (^BM^NCAR FN)
                                          (^INT (^BM^CONS (^8) (^BM^ZERO))))
                                         (^BM^PR-APPLY
                                          (^BM^NCADR FN)
                                          (^BM^PR-APPLY (^BM^NCADDR FN) ARG))
                                         (^INT (^BM^ZERO)))))))))))))

(DEFINE (^BM^NON-PR-FN X) (^BM^ADD1 (^BM^PR-APPLY X X)))

(DEFINE (^BM^COUNTER-EXAMPLE-FOR X) (^BM^FIX X))

(LEMMA
 (^BM^NOT
  (EQUAL (^BM^NON-PR-FN (^BM^COUNTER-EXAMPLE-FOR FN))
         (^BM^PR-APPLY FN (^BM^COUNTER-EXAMPLE-FOR FN)))))

(LEMMA (^BM^NUMBERP (^BM^COUNTER-EXAMPLE-FOR X)))

(DEFINE (^BM^MAX2 FN I)
 (IF (^BM^ZEROP I)
     (^BM^PR-APPLY FN I)
     (^BM^MAX (^BM^PR-APPLY FN I) (^BM^MAX2 FN (^BM^SUB1 I)))))

(DEFINE (^BM^MAX1 FN I)
 (IF (^BM^ZEROP FN)
     (^BM^MAX2 FN I)
     (^BM^MAX (^BM^MAX2 FN I) (^BM^MAX1 (^BM^SUB1 FN) I))))

(LEMMA (^BM^NOT (^BM^LESSP (^BM^MAX2 I J) (^BM^PR-APPLY I J))))

(DEFINE (^BM^EXCEED J) (^BM^ADD1 (^BM^MAX1 J J)))

(DEFINE (^BM^EXCEED-AT I) I)

(LEMMA
 (^BM^IMPLIES (^BM^NUMBERP FN)
  (^BM^NOT (^BM^LESSP (^BM^MAX1 (^BM^PLUS J FN) I) (^BM^PR-APPLY FN I)))))

(LEMMA
 (^BM^IMPLIES (^BM^NUMBERP FN)
  (^BM^NOT
   (^BM^LESSP (^BM^MAX1 (^BM^PLUS J FN) (^BM^PLUS J FN))
    (^BM^PR-APPLY FN (^BM^PLUS J FN))))))

(LEMMA
 (^BM^IMPLIES (^BM^NUMBERP FN)
  (^BM^LESSP (^BM^PR-APPLY FN (^BM^PLUS J (^BM^EXCEED-AT FN)))
   (^BM^EXCEED (^BM^PLUS J (^BM^EXCEED-AT FN))))))