(NOTE-LIB "nqthm-boot")

(DEFINE (^BM^ZNP X)
 (IF (CONSP X)
     (IF (EQUAL (CAR X) '^BM^ZN)
         (IF (CONSP (CDR X))
             (IF (^BM^NUMBERP (CAR (CDR X)))
                 (IF (CONSP (CDR (CDR X)))
                     (IF (^BM^NUMBERP (CAR (CDR (CDR X))))
                         (EQUAL (CDR (CDR (CDR X))) 'NIL)
                         'FALSE)
                     'FALSE)
                 'FALSE)
             'FALSE)
         'FALSE)
     'FALSE))

(DEFINE (^BM^ZN T1601 T1602)
 (CONS '^BM^ZN
       (CONS (IF (^BM^NUMBERP T1601) T1601 (^BM^ZERO))
             (CONS (IF (^BM^NUMBERP T1602) T1602 (^BM^ZERO)) 'NIL))))

(DEFINE (^BM^POS X) (IF (^BM^ZNP X) (CAR (CDR X)) (^BM^ZERO)))

(DEFINE (^BM^NEG X) (IF (^BM^ZNP X) (CAR (CDR (CDR X))) (^BM^ZERO)))

(DEFINE (^BM^ZLESSP X Y)
 (^BM^LESSP (^BM^PLUS (^BM^POS X) (^BM^NEG Y))
  (^BM^PLUS (^BM^NEG X) (^BM^POS Y))))

(DEFINE (^BM^ZLESSEQP X Y) (^BM^NOT (^BM^ZLESSP Y X)))

(DEFINE (^BM^ZMAX X Y) (IF (^BM^ZLESSP X Y) Y X))

(DEFINE (^BM^ZMIN X Y) (IF (^BM^ZLESSP X Y) X Y))

(DEFINE (^BM^ZSUB1 X) (^BM^ZN (^BM^POS X) (^BM^ADD1 (^BM^NEG X))))

(DEFINE (^BM^PZDIFFERENCE X Y)
 (^BM^DIFFERENCE (^BM^PLUS (^BM^POS X) (^BM^NEG Y))
  (^BM^PLUS (^BM^NEG X) (^BM^POS Y))))

(DEFINE (^BM^M1 X Y Z)
 (IF (^BM^ZLESSEQP X Y) (^INT (^BM^ZERO)) (^INT (^BM^CONS (^1) (^BM^ZERO)))))

(DEFINE (^BM^M2 X Y Z)
 (^BM^PZDIFFERENCE (^BM^ZMAX X (^BM^ZMAX Y Z)) (^BM^ZMIN X (^BM^ZMIN Y Z))))

(DEFINE (^BM^M3 X Y Z) (^BM^PZDIFFERENCE X (^BM^ZMIN X (^BM^ZMIN Y Z))))

(DEFINE (^BM^TAK0 X Y Z) (IF (^BM^ZLESSEQP X Y) Y (IF (^BM^ZLESSEQP Y Z) Z X)))

(DEFINE (^BM^M X Y Z)
 (^BM^CONS (^BM^M1 X Y Z)
  (^BM^CONS (^BM^M2 X Y Z) (^BM^CONS (^BM^M3 X Y Z) (^NIL)))))

(LEMMA
 (EQUAL (^BM^TAK0 X Y Z)
        (IF (^BM^ZLESSEQP X Y)
            Y
            (^BM^TAK0 (^BM^TAK0 (^BM^ZSUB1 X) Y Z) (^BM^TAK0 (^BM^ZSUB1 Y) Z X)
             (^BM^TAK0 (^BM^ZSUB1 Z) X Y)))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZLESSEQP X Y))
  (^BM^NOT
   (^BM^LESSP (^BM^M1 X Y Z)
    (^BM^M1 (^BM^TAK0 (^BM^ZSUB1 X) Y Z) (^BM^TAK0 (^BM^ZSUB1 Y) Z X)
     (^BM^TAK0 (^BM^ZSUB1 Z) X Y))))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZLESSEQP X Y))
  (^BM^NOT (^BM^LESSP (^BM^M1 X Y Z) (^BM^M1 (^BM^ZSUB1 X) Y Z)))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZLESSEQP X Y))
  (^BM^NOT (^BM^LESSP (^BM^M1 X Y Z) (^BM^M1 (^BM^ZSUB1 Y) Z X)))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZLESSEQP X Y))
  (^BM^NOT (^BM^LESSP (^BM^M1 X Y Z) (^BM^M1 (^BM^ZSUB1 Z) X Y)))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZLESSEQP X Y))
  (^BM^NOT
   (^BM^LESSP (^BM^M2 X Y Z)
    (^BM^M2 (^BM^TAK0 (^BM^ZSUB1 X) Y Z) (^BM^TAK0 (^BM^ZSUB1 Y) Z X)
     (^BM^TAK0 (^BM^ZSUB1 Z) X Y))))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZLESSEQP X Y))
  (^BM^NOT (^BM^LESSP (^BM^M2 X Y Z) (^BM^M2 (^BM^ZSUB1 X) Y Z)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZLESSEQP X Y))
   (EQUAL (^BM^M1 (^BM^ZSUB1 Y) Z X) (^BM^M1 X Y Z)))
  (^BM^NOT (^BM^LESSP (^BM^M2 X Y Z) (^BM^M2 (^BM^ZSUB1 Y) Z X)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZLESSEQP X Y))
   (EQUAL (^BM^M1 (^BM^ZSUB1 Z) X Y) (^BM^M1 X Y Z)))
  (^BM^NOT (^BM^LESSP (^BM^M2 X Y Z) (^BM^M2 (^BM^ZSUB1 Z) X Y)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZLESSEQP X Y))
   (EQUAL (^BM^M1 (^BM^TAK0 (^BM^ZSUB1 X) Y Z) (^BM^TAK0 (^BM^ZSUB1 Y) Z X)
           (^BM^TAK0 (^BM^ZSUB1 Z) X Y))
          (^BM^M1 X Y Z)))
  (^BM^LESSP
   (^BM^M3 (^BM^TAK0 (^BM^ZSUB1 X) Y Z) (^BM^TAK0 (^BM^ZSUB1 Y) Z X)
    (^BM^TAK0 (^BM^ZSUB1 Z) X Y))
   (^BM^M3 X Y Z))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZLESSEQP X Y))
   (EQUAL (^BM^M1 (^BM^ZSUB1 X) Y Z) (^BM^M1 X Y Z)))
  (^BM^LESSP (^BM^M3 (^BM^ZSUB1 X) Y Z) (^BM^M3 X Y Z))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZLESSEQP X Y))
   (EQUAL (^BM^M1 (^BM^ZSUB1 Y) Z X) (^BM^M1 X Y Z)))
  (^BM^LESSP (^BM^M3 (^BM^ZSUB1 Y) Z X) (^BM^M3 X Y Z))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZLESSEQP X Y))
   (EQUAL (^BM^M1 (^BM^ZSUB1 Z) X Y) (^BM^M1 X Y Z)))
  (^BM^LESSP (^BM^M2 (^BM^ZSUB1 Z) X Y) (^BM^M2 X Y Z))))

(DEFINE (^BM^MAKE-ORDINAL3 X)
 (^BM^CONS (^BM^CONS (^BM^ADD1 (^BM^CAR X)) (^INT (^BM^ZERO)))
  (^BM^CONS (^BM^ADD1 (^BM^CAR (^BM^CDR X)))
   (^BM^FIX (^BM^CAR (^BM^CDR (^BM^CDR X)))))))

(LEMMA (^BM^ORDINALP (^BM^MAKE-ORDINAL3 X)))

(DEFINE (^BM^LEX3 X Y)
 (^BM^ORD-LESSP (^BM^MAKE-ORDINAL3 X) (^BM^MAKE-ORDINAL3 Y)))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZLESSEQP X Y))
  (^BM^LEX3 (^BM^M (^BM^ZSUB1 X) Y Z) (^BM^M X Y Z))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZLESSEQP X Y))
  (^BM^LEX3 (^BM^M (^BM^ZSUB1 Y) Z X) (^BM^M X Y Z))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZLESSEQP X Y))
  (^BM^LEX3 (^BM^M (^BM^ZSUB1 Z) X Y) (^BM^M X Y Z))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZLESSEQP X Y))
  (^BM^LEX3
   (^BM^M (^BM^TAK0 (^BM^ZSUB1 X) Y Z) (^BM^TAK0 (^BM^ZSUB1 Y) Z X)
    (^BM^TAK0 (^BM^ZSUB1 Z) X Y))
   (^BM^M X Y Z))))