(NOTE-LIB "nqthm-boot")

(DEFINE (^BM^LOGICALP X) (^BM^OR (EQUAL X (^BM^TRUE)) (EQUAL X (^BM^FALSE))))

(DEFINE (^BM^EXPT I J)
 (IF (^BM^ZEROP J)
     (^INT (^BM^CONS (^1) (^BM^ZERO)))
     (^BM^TIMES I (^BM^EXPT I (^BM^SUB1 J)))))

(DEFINE (^BM^ZNUMBERP X) (^BM^OR (^BM^NEGATIVEP X) (^BM^NUMBERP X)))

(DEFINE (^BM^ZZERO) (^BM^ZERO))

(DEFINE (^BM^ZPLUS X Y)
 (IF (^BM^NEGATIVEP X)
     (IF (^BM^NEGATIVEP Y)
         (^BM^MINUS (^BM^PLUS (^BM^NEGATIVE-GUTS X) (^BM^NEGATIVE-GUTS Y)))
         (IF (^BM^LESSP Y (^BM^NEGATIVE-GUTS X))
             (^BM^MINUS (^BM^DIFFERENCE (^BM^NEGATIVE-GUTS X) Y))
             (^BM^DIFFERENCE Y (^BM^NEGATIVE-GUTS X))))
     (IF (^BM^NEGATIVEP Y)
         (IF (^BM^LESSP X (^BM^NEGATIVE-GUTS Y))
             (^BM^MINUS (^BM^DIFFERENCE (^BM^NEGATIVE-GUTS Y) X))
             (^BM^DIFFERENCE X (^BM^NEGATIVE-GUTS Y)))
         (^BM^PLUS X Y))))

(DEFINE (^BM^ZDIFFERENCE X Y)
 (IF (^BM^NEGATIVEP X)
     (IF (^BM^NEGATIVEP Y)
         (IF (^BM^LESSP (^BM^NEGATIVE-GUTS Y) (^BM^NEGATIVE-GUTS X))
             (^BM^MINUS
              (^BM^DIFFERENCE (^BM^NEGATIVE-GUTS X) (^BM^NEGATIVE-GUTS Y)))
             (^BM^DIFFERENCE (^BM^NEGATIVE-GUTS Y) (^BM^NEGATIVE-GUTS X)))
         (^BM^MINUS (^BM^PLUS (^BM^NEGATIVE-GUTS X) Y)))
     (IF (^BM^NEGATIVEP Y)
         (^BM^PLUS X (^BM^NEGATIVE-GUTS Y))
         (IF (^BM^LESSP X Y)
             (^BM^MINUS (^BM^DIFFERENCE Y X))
             (^BM^DIFFERENCE X Y)))))

(DEFINE (^BM^ZTIMES X Y)
 (IF (^BM^NEGATIVEP X)
     (IF (^BM^NEGATIVEP Y)
         (^BM^TIMES (^BM^NEGATIVE-GUTS X) (^BM^NEGATIVE-GUTS Y))
         (^BM^MINUS (^BM^TIMES (^BM^NEGATIVE-GUTS X) Y)))
     (IF (^BM^NEGATIVEP Y)
         (^BM^MINUS (^BM^TIMES X (^BM^NEGATIVE-GUTS Y)))
         (^BM^TIMES X Y))))

(DEFINE (^BM^ZQUOTIENT X Y)
 (IF (^BM^NEGATIVEP X)
     (IF (^BM^NEGATIVEP Y)
         (^BM^QUOTIENT (^BM^NEGATIVE-GUTS X) (^BM^NEGATIVE-GUTS Y))
         (^BM^MINUS (^BM^QUOTIENT (^BM^NEGATIVE-GUTS X) Y)))
     (IF (^BM^NEGATIVEP Y)
         (^BM^MINUS (^BM^QUOTIENT X (^BM^NEGATIVE-GUTS Y)))
         (^BM^QUOTIENT X Y))))

(DEFINE (^BM^ZEXPTZ I J)
 (IF (^BM^ZEROP J)
     (^INT (^BM^CONS (^1) (^BM^ZERO)))
     (^BM^ZTIMES I (^BM^ZEXPTZ I (^BM^SUB1 J)))))

(DEFINE (^BM^ZNORMALIZE X)
 (IF (^BM^NEGATIVEP X)
     (IF (EQUAL (^BM^NEGATIVE-GUTS X) (^INT (^BM^ZERO))) (^INT (^BM^ZERO)) X)
     (^BM^FIX X)))

(DEFINE (^BM^ZEQP X Y) (EQUAL (^BM^ZNORMALIZE X) (^BM^ZNORMALIZE Y)))

(DEFINE (^BM^ZNEQP X Y) (^BM^NOT (^BM^ZEQP X Y)))

(DEFINE (^BM^ZLESSP X Y)
 (IF (^BM^NEGATIVEP X)
     (IF (^BM^NEGATIVEP Y)
         (^BM^LESSP (^BM^NEGATIVE-GUTS Y) (^BM^NEGATIVE-GUTS X))
         (^BM^NOT
          (^BM^AND (EQUAL (^BM^NEGATIVE-GUTS X) (^INT (^BM^ZERO)))
           (^BM^ZEROP Y))))
     (IF (^BM^NEGATIVEP Y) (^BM^FALSE) (^BM^LESSP X Y))))

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

(DEFINE (^BM^ZGREATERP X Y) (^BM^ZLESSP Y X))

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

(DEFINE (^BM^GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER)
 (^BM^MINUS (^INT (^BM^CONS (^2) (^BM^CONS (^0) (^BM^CONS (^1) (^BM^ZERO)))))))

(DEFINE (^BM^LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
 (^INT (^BM^CONS (^2) (^BM^CONS (^0) (^BM^CONS (^1) (^BM^ZERO))))))

(LEMMA
 (^BM^AND (^BM^NUMBERP (^BM^LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
  (^BM^AND (^BM^NEGATIVEP (^BM^GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
   (^BM^AND
    (^BM^LESSP
     (^INT (^BM^CONS (^2) (^BM^CONS (^0) (^BM^CONS (^0) (^BM^ZERO)))))
     (^BM^NEGATIVE-GUTS (^BM^GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER)))
    (^BM^LESSP
     (^INT (^BM^CONS (^2) (^BM^CONS (^0) (^BM^CONS (^0) (^BM^ZERO)))))
     (^BM^LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))))))

(DEFINE (^BM^EXPRESSIBLE-ZNUMBERP X)
 (^BM^AND (^BM^ZLESSP (^BM^GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER) X)
  (^BM^ZLESSP X (^BM^LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))))

(DEFINE (^BM^IABS I) (IF (^BM^NEGATIVEP I) (^BM^NEGATIVE-GUTS I) (^BM^FIX I)))

(DEFINE (^BM^MOD X Y) (^BM^ZDIFFERENCE X (^BM^ZTIMES Y (^BM^ZQUOTIENT X Y))))

(DEFINE (^BM^MAX0 I J) (IF (^BM^ZLESSP I J) J I))

(DEFINE (^BM^MIN0 I J) (IF (^BM^ZLESSP I J) I J))

(DEFINE (^BM^ISIGN I J)
 (IF (^BM^NEGATIVEP J)
     (^BM^ZTIMES (^BM^MINUS (^INT (^BM^CONS (^1) (^BM^ZERO)))) (^BM^IABS I))
     (^BM^IABS I)))

(DEFINE (^BM^IDIM I J) (^BM^ZDIFFERENCE I (^BM^MIN0 I J)))

(DEFINE (^BM^FORTRAN-UNDEFINED X)
 (IF (CONSP X)
     (IF (EQUAL (CAR X) '^BM^FORTRAN-UNDEF)
         (IF (CONSP (CDR X))
             (IF (^BM^NOT 'FALSE) (EQUAL (CDR (CDR X)) 'NIL) 'FALSE)
             'FALSE)
         'FALSE)
     'FALSE))

(DEFINE (^BM^FORTRAN-UNDEF T1605)
 (CONS '^BM^FORTRAN-UNDEF (CONS (IF (^BM^NOT 'FALSE) T1605 (^BM^ZERO)) 'NIL)))

(DEFINE (^BM^FORTRAN-UNDEF-GUTS X)
 (IF (^BM^FORTRAN-UNDEFINED X) (CAR (CDR X)) (^BM^ZERO)))

(DEFINE (^BM^DEFINEDP X) (^BM^NOT (^BM^FORTRAN-UNDEFINED X)))

(DEFINE (^BM^ELT1 A I) (CONS 'ELT1 (CONS A (CONS I 'NIL))))

(DEFINE (^BM^ELT2 A I J) (CONS 'ELT2 (CONS A (CONS I (CONS J 'NIL)))))

(DEFINE (^BM^ELT3 A I J K)
 (CONS 'ELT3 (CONS A (CONS I (CONS J (CONS K 'NIL))))))

(DEFINE (^BM^LEX L1 L2)
 (IF (^BM^OR (^BM^NLISTP L1) (^BM^NLISTP L2))
     (^BM^FALSE)
     (^BM^OR (^BM^LESSP (^BM^CAR L1) (^BM^CAR L2))
      (^BM^AND (EQUAL (^BM^CAR L1) (^BM^CAR L2))
       (^BM^LEX (^BM^CDR L1) (^BM^CDR L2))))))

(DEFINE (^BM^RNUMBERP X) (CONS 'RNUMBERP (CONS X 'NIL)))

(DEFINE (^BM^DNUMBERP X) (CONS 'DNUMBERP (CONS X 'NIL)))

(DEFINE (^BM^CNUMBERP X) (CONS 'CNUMBERP (CONS X 'NIL)))

(DEFINE (^BM^RZERO) (CONS 'RZERO 'NIL))

(DEFINE (^BM^DZERO) (CONS 'DZERO 'NIL))

(DEFINE (^BM^CZERO) (CONS 'CZERO 'NIL))

(DEFINE (^BM^EXPRESSIBLE-RNUMBERP X) (CONS 'EXPRESSIBLE-RNUMBERP (CONS X 'NIL)))

(DEFINE (^BM^EXPRESSIBLE-DNUMBERP X) (CONS 'EXPRESSIBLE-DNUMBERP (CONS X 'NIL)))

(DEFINE (^BM^EXPRESSIBLE-CNUMBERP X) (CONS 'EXPRESSIBLE-CNUMBERP (CONS X 'NIL)))

(DEFINE (^BM^RPLUS X Y) (CONS 'RPLUS (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^RTIMES X Y) (CONS 'RTIMES (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^RDIFFERENCE X Y) (CONS 'RDIFFERENCE (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^RQUOTIENT X Y) (CONS 'RQUOTIENT (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^RLESSP X Y) (CONS 'RLESSP (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^RLESSEQP X Y) (CONS 'RLESSEQP (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^REQP X Y) (CONS 'REQP (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^RNEQP X Y) (CONS 'RNEQP (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^RGREATEREQP X Y) (CONS 'RGREATEREQP (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^RGREATERP X Y) (CONS 'RGREATERP (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^DPLUS X Y) (CONS 'DPLUS (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^DTIMES X Y) (CONS 'DTIMES (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^DDIFFERENCE X Y) (CONS 'DDIFFERENCE (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^DQUOTIENT X Y) (CONS 'DQUOTIENT (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^DLESSP X Y) (CONS 'DLESSP (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^DLESSEQP X Y) (CONS 'DLESSEQP (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^DEQP X Y) (CONS 'DEQP (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^DNEQP X Y) (CONS 'DNEQP (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^DGREATEREQP X Y) (CONS 'DGREATEREQP (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^DGREATERP X Y) (CONS 'DGREATERP (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^CPLUS X Y) (CONS 'CPLUS (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^CTIMES X Y) (CONS 'CTIMES (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^CDIFFERENCE X Y) (CONS 'CDIFFERENCE (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^CQUOTIENT X Y) (CONS 'CQUOTIENT (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^CEQP X Y) (CONS 'CEQP (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^CNEQP X Y) (CONS 'CNEQP (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^REXPTZ X Y) (CONS 'REXPTZ (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^DEXPTZ X Y) (CONS 'DEXPTZ (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^CEXPTZ X Y) (CONS 'CEXPTZ (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^REXPTR X Y) (CONS 'REXPTR (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^REXPTD X Y) (CONS 'REXPTD (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^DEXPTR X Y) (CONS 'DEXPTR (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^DEXPTD X Y) (CONS 'DEXPTD (CONS X (CONS Y 'NIL))))

(DEFINE (^BM^ABS I) (CONS 'ABS (CONS I 'NIL)))

(DEFINE (^BM^DABS I) (CONS 'DABS (CONS I 'NIL)))

(DEFINE (^BM^AINT I) (CONS 'AINT (CONS I 'NIL)))

(DEFINE (^BM^INT I) (CONS 'INT (CONS I 'NIL)))

(DEFINE (^BM^IDINT I) (CONS 'IDINT (CONS I 'NIL)))

(DEFINE (^BM^AMOD I J) (CONS 'AMOD (CONS I (CONS J 'NIL))))

(DEFINE (^BM^AMAX0 I J) (CONS 'AMAX0 (CONS I (CONS J 'NIL))))

(DEFINE (^BM^AMAX1 I J) (CONS 'AMAX1 (CONS I (CONS J 'NIL))))

(DEFINE (^BM^MAX1 I J) (CONS 'MAX1 (CONS I (CONS J 'NIL))))

(DEFINE (^BM^DMAX1 I J) (CONS 'DMAX1 (CONS I (CONS J 'NIL))))

(DEFINE (^BM^AMIN0 I J) (CONS 'AMIN0 (CONS I (CONS J 'NIL))))

(DEFINE (^BM^AMIN1 I J) (CONS 'AMIN1 (CONS I (CONS J 'NIL))))

(DEFINE (^BM^MIN1 I J) (CONS 'MIN1 (CONS I (CONS J 'NIL))))

(DEFINE (^BM^DMIN1 I J) (CONS 'DMIN1 (CONS I (CONS J 'NIL))))

(DEFINE (^BM^FLOAT I) (CONS 'FLOAT (CONS I 'NIL)))

(DEFINE (^BM^IFIX I) (CONS 'IFIX (CONS I 'NIL)))

(DEFINE (^BM^SIGN I J) (CONS 'SIGN (CONS I (CONS J 'NIL))))

(DEFINE (^BM^DSIGN I J) (CONS 'DSIGN (CONS I (CONS J 'NIL))))

(DEFINE (^BM^DIM I J) (CONS 'DIM (CONS I (CONS J 'NIL))))

(DEFINE (^BM^SNGL I) (CONS 'SNGL (CONS I 'NIL)))

(DEFINE (^BM^REAL I) (CONS 'REAL (CONS I 'NIL)))

(DEFINE (^BM^AIMAG I) (CONS 'AIMAG (CONS I 'NIL)))

(DEFINE (^BM^DBLE I) (CONS 'DBLE (CONS I 'NIL)))

(DEFINE (^BM^CMPLX I J) (CONS 'CMPLX (CONS I (CONS J 'NIL))))

(DEFINE (^BM^CONJG I) (CONS 'CONJG (CONS I 'NIL)))

(DEFINE (^BM^EXP I) (CONS 'EXP (CONS I 'NIL)))

(DEFINE (^BM^DEXP I) (CONS 'DEXP (CONS I 'NIL)))

(DEFINE (^BM^CEXP I) (CONS 'CEXP (CONS I 'NIL)))

(DEFINE (^BM^ALOG I) (CONS 'ALOG (CONS I 'NIL)))

(DEFINE (^BM^DLOG I) (CONS 'DLOG (CONS I 'NIL)))

(DEFINE (^BM^CLOG I) (CONS 'CLOG (CONS I 'NIL)))

(DEFINE (^BM^ALOG10 I) (CONS 'ALOG10 (CONS I 'NIL)))

(DEFINE (^BM^DLOG10 I) (CONS 'DLOG10 (CONS I 'NIL)))

(DEFINE (^BM^SIN I) (CONS 'SIN (CONS I 'NIL)))

(DEFINE (^BM^DSIN I) (CONS 'DSIN (CONS I 'NIL)))

(DEFINE (^BM^CSIN I) (CONS 'CSIN (CONS I 'NIL)))

(DEFINE (^BM^COS I) (CONS 'COS (CONS I 'NIL)))

(DEFINE (^BM^DCOS I) (CONS 'DCOS (CONS I 'NIL)))

(DEFINE (^BM^CCOS I) (CONS 'CCOS (CONS I 'NIL)))

(DEFINE (^BM^TANH I) (CONS 'TANH (CONS I 'NIL)))

(DEFINE (^BM^SQRT I) (CONS 'SQRT (CONS I 'NIL)))

(DEFINE (^BM^DSQRT I) (CONS 'DSQRT (CONS I 'NIL)))

(DEFINE (^BM^CSQRT I) (CONS 'CSQRT (CONS I 'NIL)))

(DEFINE (^BM^ATAN I) (CONS 'ATAN (CONS I 'NIL)))

(DEFINE (^BM^DATAN I) (CONS 'DATAN (CONS I 'NIL)))

(DEFINE (^BM^ATAN2 I J) (CONS 'ATAN2 (CONS I (CONS J 'NIL))))

(DEFINE (^BM^DATAN2 I J) (CONS 'DATAN2 (CONS I (CONS J 'NIL))))

(DEFINE (^BM^DMOD I J) (CONS 'DMOD (CONS I (CONS J 'NIL))))

(DEFINE (^BM^CABS I) (CONS 'CABS (CONS I 'NIL)))

(DEFINE (^BM^ALMOST-EQUAL1 A1 A2 U V I E)
 (IF (^BM^OR (^BM^ZEROP V) (^BM^LESSP V U))
     (^BM^TRUE)
     (^BM^AND
      (IF (EQUAL V I)
          (EQUAL (^BM^ELT1 A2 V) E)
          (EQUAL (^BM^ELT1 A2 V) (^BM^ELT1 A1 V)))
      (^BM^ALMOST-EQUAL1 A1 A2 U (^BM^SUB1 V) I E))))

(LEMMA (EQUAL (^BM^PLUS X (^INT (^BM^ZERO))) (^BM^FIX X)))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^NUMBERP Y)) (EQUAL (^BM^PLUS X Y) (^BM^FIX X))))

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

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

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

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

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

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^NUMBERP Y))
  (EQUAL (^BM^TIMES X Y) (^INT (^BM^ZERO)))))

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

(LEMMA
 (EQUAL (^BM^TIMES X (^BM^ADD1 Y))
        (IF (^BM^NUMBERP Y) (^BM^PLUS X (^BM^TIMES X Y)) (^BM^FIX X))))

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

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

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

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

(LEMMA
 (EQUAL (EQUAL (^BM^LESSP X Y) Z)
        (IF (^BM^LESSP X Y) (EQUAL (^BM^TRUE) Z) (EQUAL (^BM^FALSE) Z))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (EQUAL (^BM^ELT1 A2 J) W))
   (^BM^AND (EQUAL W (IF (EQUAL J I) E (^BM^ELT1 A1 J)))
    (^BM^AND (^BM^NOT (^BM^ZEROP U))
     (^BM^AND (^BM^NOT (^BM^LESSP J U)) (^BM^NOT (^BM^LESSP V J))))))
  (^BM^NOT (^BM^ALMOST-EQUAL1 A1 A2 U V I E))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (EQUAL (^BM^ELT1 A2 J) W))
   (^BM^AND (EQUAL W (IF (EQUAL J I) E (^BM^ELT1 A1 J)))
    (^BM^AND (^BM^NOT (^BM^ZEROP U))
     (^BM^AND (^BM^LEQ U J)
      (^BM^AND (^BM^LEQ J V)
       (^BM^AND (^BM^NOT (^BM^ZEROP V))
        (^BM^AND (^BM^NOT (^BM^LESSP V U))
         (^BM^AND (^BM^NOT (EQUAL V I))
          (EQUAL (^BM^ELT1 A2 V) (^BM^ELT1 A1 V))))))))))
  (^BM^NOT (^BM^ALMOST-EQUAL1 A1 A2 U (^BM^SUB1 V) I E))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^ALMOST-EQUAL1 A1 A2 U V I E)
   (^BM^AND (^BM^NOT (^BM^ZEROP U))
    (^BM^AND (^BM^NOT (^BM^LESSP X U)) (^BM^NOT (^BM^LESSP V Y)))))
  (^BM^ALMOST-EQUAL1 A1 A2 X Y I E)))