(NOTE-LIB "nqthm-boot")

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

(DEFINE (^BM^P M N)
 (IF (^BM^ZEROP M)
     (^BM^ADD1 N)
     (IF (^BM^ZEROP N)
         (^BM^P (^BM^SUB1 M) (^INT (^BM^CONS (^1) (^BM^ZERO))))
         (^BM^P (^BM^SUB1 M) (^BM^P M (^BM^SUB1 N))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP M))
   (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) N))
  (EQUAL (^BM^A M N A) (^BM^A (^BM^SUB1 M) (^BM^A M (^BM^SUB1 N) A) A))))

(LEMMA
 (EQUAL (^BM^A M (^INT (^BM^CONS (^2) (^BM^ZERO)))
         (^INT (^BM^CONS (^2) (^BM^ZERO))))
        (^INT (^BM^CONS (^4) (^BM^ZERO)))))

(LEMMA
 (EQUAL (^BM^PLUS (^INT (^BM^CONS (^2) (^BM^ZERO))) X) (^BM^ADD1 (^BM^ADD1 X))))

(LEMMA
 (^BM^AND (EQUAL (^BM^P (^INT (^BM^ZERO)) N) (^BM^ADD1 N))
  (^BM^IMPLIES (^BM^LESSP (^INT (^BM^ZERO)) M)
   (EQUAL (^BM^PLUS (^INT (^BM^CONS (^3) (^BM^ZERO))) (^BM^P M N))
          (^BM^A (^BM^SUB1 M) (^BM^ADD1 (^BM^ADD1 (^BM^ADD1 N)))
           (^INT (^BM^CONS (^2) (^BM^ZERO))))))))