(NOTE-LIB "nqthm-boot")

(DEFINE (^BM^RATE-PROXIMITY W R)
 (^BM^AND
  (^BM^NOT
   (^BM^LESSP (^BM^TIMES (^INT (^BM^CONS (^1) (^BM^CONS (^8) (^BM^ZERO)))) W)
    (^BM^TIMES (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) R)))
  (^BM^NOT
   (^BM^LESSP (^BM^TIMES (^INT (^BM^CONS (^1) (^BM^CONS (^9) (^BM^ZERO)))) R)
    (^BM^TIMES (^INT (^BM^CONS (^1) (^BM^CONS (^8) (^BM^ZERO)))) W)))))

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

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

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

(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 Z))
  (EQUAL (^BM^TIMES X Z) (^INT (^BM^ZERO)))))

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

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

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

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

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

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

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

(LEMMA (EQUAL (^BM^DIFFERENCE (^BM^PLUS I X) I) (^BM^FIX X)))

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

(LEMMA (EQUAL (^BM^DIFFERENCE (^BM^PLUS I (^BM^PLUS J X)) J) (^BM^PLUS I X)))

(LEMMA (EQUAL (^BM^LESSP (^BM^REMAINDER X Y) Y) (^BM^NOT (^BM^ZEROP Y))))

(LEMMA
 (^BM^IMPLIES (^BM^NUMBERP X)
  (EQUAL (^BM^PLUS (^BM^REMAINDER X Y) (^BM^TIMES Y (^BM^QUOTIENT X Y))) X)))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP W))
  (EQUAL (^BM^QUOTIENT (^BM^PLUS V (^BM^TIMES W I)) W)
         (^BM^PLUS I (^BM^QUOTIENT V W)))))

(DEFINE (^BM^LEN X)
 (IF (^BM^NLISTP X) (^INT (^BM^ZERO)) (^BM^ADD1 (^BM^LEN (^BM^CDR X)))))

(LEMMA (EQUAL (EQUAL (^BM^LEN X) (^INT (^BM^ZERO))) (^BM^NLISTP X)))

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

(LEMMA (EQUAL (EQUAL (^BM^APP A B) (^BM^APP A C)) (EQUAL B C)))

(LEMMA (EQUAL (^BM^APP (^BM^APP A B) C) (^BM^APP A (^BM^APP B C))))

(LEMMA (EQUAL (^BM^LEN (^BM^APP A B)) (^BM^PLUS (^BM^LEN A) (^BM^LEN B))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP X))
  (EQUAL (^BM^QUOTIENT X X) (^INT (^BM^CONS (^1) (^BM^ZERO))))))

(LEMMA (^BM^NOT (^BM^LESSP N (^BM^TIMES W (^BM^QUOTIENT N W)))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP W)) (^BM^LESSP A B))
  (^BM^LESSP (^BM^TIMES W A) (^BM^TIMES W B))))

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

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^LESSP N (^BM^QUOTIENT (^BM^PLUS R X) W))
   (^BM^AND (^BM^NUMBERP W) (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))))
  (EQUAL (^BM^LESSP (^BM^PLUS TS (^BM^TIMES N W)) (^BM^PLUS R (^BM^PLUS TS X)))
         (^BM^TRUE))))

(LEMMA
 (EQUAL (^BM^DIFFERENCE (^BM^PLUS R (^BM^PLUS TS X)) (^BM^PLUS TS Y))
        (^BM^DIFFERENCE (^BM^PLUS R X) Y)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^LESSP N (^BM^QUOTIENT (^BM^PLUS R X) W))
   (^BM^AND (^BM^NUMBERP X)
    (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
     (^BM^AND (^BM^NUMBERP R)
      (^BM^AND (^BM^NOT (^BM^LESSP (^BM^TIMES N W) (^BM^PLUS R X)))
       (^BM^AND (^BM^NUMBERP N)
        (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
         (^BM^AND (^BM^NUMBERP W) (^BM^LESSP X W)))))))))
  (EQUAL (EQUAL (^BM^QUOTIENT (^BM^PLUS R X) W)
                (^BM^QUOTIENT
                 (^BM^PLUS X
                  (^BM^TIMES R
                   (^BM^QUOTIENT (^BM^DIFFERENCE (^BM^TIMES N W) X) R)))
                 W))
         (^BM^TRUE))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP I))
  (EQUAL (EQUAL (^BM^TIMES I J) (^BM^TIMES I K))
         (EQUAL (^BM^FIX J) (^BM^FIX K)))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP W))
  (EQUAL (EQUAL (^BM^PLUS (^BM^TIMES W X) (^BM^TIMES W Y)) (^BM^TIMES W Z))
         (EQUAL (^BM^PLUS X Y) (^BM^FIX Z)))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^LESSP B C))
  (EQUAL (^BM^DIFFERENCE A (^BM^DIFFERENCE B C))
         (^BM^DIFFERENCE (^BM^PLUS A C) B))))

(LEMMA
 (EQUAL (^BM^DIFFERENCE (^BM^DIFFERENCE A B) C)
        (^BM^DIFFERENCE A (^BM^PLUS B C))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP W))
  (EQUAL (^BM^QUOTIENT (^BM^PLUS V (^BM^PLUS (^BM^TIMES I W) (^BM^TIMES W J)))
          W)
         (^BM^PLUS I (^BM^PLUS J (^BM^QUOTIENT V W))))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^NUMBERP I) (^BM^NOT (^BM^LESSP I J)))
  (EQUAL (^BM^PLUS J (^BM^DIFFERENCE I J)) I)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP W)) (^BM^NOT (^BM^LESSP A (^BM^TIMES W B))))
  (EQUAL (^BM^QUOTIENT (^BM^DIFFERENCE A (^BM^TIMES W B)) W)
         (^BM^DIFFERENCE (^BM^QUOTIENT A W) B))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^LESSP Z1 Y)
   (^BM^AND (^BM^LESSP Z2 Y)
    (^BM^AND (^BM^NOT (EQUAL Y (^INT (^BM^ZERO))))
     (^BM^AND (^BM^NUMBERP Y) (^BM^LESSP X V)))))
  (EQUAL (^BM^LESSP (^BM^PLUS Z1 (^BM^TIMES Y X))
          (^BM^PLUS Z2 (^BM^TIMES V Y)))
         (^BM^TRUE))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^LESSP N (^BM^QUOTIENT (^BM^PLUS R X) W))
   (^BM^AND (^BM^NUMBERP X)
    (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
     (^BM^AND (^BM^NUMBERP R)
      (^BM^AND
       (^BM^NOT
        (^BM^LESSP (^BM^PLUS TS (^BM^TIMES N W)) (^BM^PLUS R (^BM^PLUS TS X))))
       (^BM^AND (^BM^NUMBERP N)
        (^BM^AND (^BM^NUMBERP TS)
         (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
          (^BM^AND (^BM^NUMBERP W)
           (^BM^AND (^BM^NOT (^BM^LESSP (^BM^PLUS TS X) TS))
            (^BM^LESSP (^BM^PLUS TS X) (^BM^PLUS TS W))))))))))))
  (EQUAL (EQUAL (^BM^PLUS R (^BM^PLUS TS X))
                (^BM^PLUS TS
                 (^BM^PLUS X
                  (^BM^TIMES R
                   (^BM^QUOTIENT (^BM^DIFFERENCE (^BM^TIMES N W) X) R)))))
         (^BM^TRUE))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^LESSP X R))
  (^BM^NOT (^BM^LESSP (^BM^TIMES R (^BM^QUOTIENT X R)) R))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP W)) (^BM^NOT (^BM^LESSP A B)))
  (EQUAL (^BM^LESSP (^BM^QUOTIENT A W) (^BM^QUOTIENT B W)) (^BM^FALSE))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP X)
   (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
    (^BM^AND (^BM^NUMBERP R)
     (^BM^AND
      (^BM^NOT
       (^BM^LESSP (^BM^PLUS TS (^BM^TIMES N W)) (^BM^PLUS R (^BM^PLUS TS X))))
      (^BM^AND (^BM^NUMBERP N)
       (^BM^AND (^BM^NUMBERP TS)
        (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
         (^BM^AND (^BM^NUMBERP W)
          (^BM^AND (^BM^NOT (^BM^LESSP (^BM^PLUS TS X) TS))
           (^BM^LESSP (^BM^PLUS TS X) (^BM^PLUS TS W)))))))))))
  (EQUAL (^BM^PLUS (^BM^QUOTIENT (^BM^PLUS R X) W)
          (^BM^QUOTIENT
           (^BM^DIFFERENCE
            (^BM^PLUS X
             (^BM^TIMES R (^BM^QUOTIENT (^BM^DIFFERENCE (^BM^TIMES N W) X) R)))
            (^BM^TIMES W (^BM^QUOTIENT (^BM^PLUS R X) W)))
           W))
         (^BM^QUOTIENT
          (^BM^PLUS X
           (^BM^TIMES R (^BM^QUOTIENT (^BM^DIFFERENCE (^BM^TIMES N W) X) R)))
          W))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP R))
  (^BM^NOT
   (^BM^LESSP (^BM^QUOTIENT (^BM^TIMES N W) R)
    (^BM^QUOTIENT (^BM^DIFFERENCE (^BM^TIMES N W) (^BM^DIFFERENCE TR TS)) R)))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP R))
  (EQUAL (^BM^QUOTIENT (^BM^TIMES N R) R) (^BM^FIX N))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP R))
  (EQUAL (^BM^LESSP (^BM^TIMES A R) (^BM^TIMES B R)) (^BM^LESSP A B))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP R)) (^BM^NOT (^BM^LESSP (^BM^QUOTIENT X R) N)))
  (^BM^NOT (^BM^LESSP X (^BM^TIMES N R)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP R)) (^BM^NOT (^BM^LESSP X (^BM^TIMES N R))))
  (^BM^NOT (^BM^LESSP (^BM^QUOTIENT X R) N))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP R))
  (EQUAL (^BM^LESSP (^BM^QUOTIENT X R) N) (^BM^LESSP X (^BM^TIMES N R)))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP R))
  (EQUAL (^BM^QUOTIENT (^BM^PLUS (^BM^TIMES N R) Z) R)
         (^BM^PLUS N (^BM^QUOTIENT Z R)))))

(LEMMA
 (EQUAL (EQUAL (^BM^TIMES I J) (^INT (^BM^ZERO)))
        (^BM^OR (^BM^ZEROP I) (^BM^ZEROP J))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP R))
   (^BM^AND
    (^BM^NOT
     (^BM^LESSP R
      (^BM^TIMES (^INT (^BM^CONS (^1) (^BM^CONS (^8) (^BM^ZERO)))) DELTA)))
    (^BM^LESSP N (^INT (^BM^CONS (^1) (^BM^CONS (^8) (^BM^ZERO)))))))
  (EQUAL (^BM^LESSP (^BM^TIMES N DELTA) R) (^BM^TRUE))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND
   (^BM^NOT
    (^BM^LESSP
     (^BM^PLUS R
      (^BM^PLUS R
       (^BM^TIMES (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) R)))
     (^BM^PLUS W
      (^BM^TIMES (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) W))))
   (^BM^AND
    (^BM^NOT
     (^BM^LESSP
      (^BM^PLUS W
       (^BM^TIMES (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) W))
      (^BM^TIMES (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) R)))
    (^BM^AND (^BM^NOT (^BM^ZEROP W))
     (^BM^AND (^BM^NOT (^BM^ZEROP R))
      (^BM^AND (^BM^NOT (^BM^ZEROP N))
       (^BM^AND (^BM^LESSP N (^INT (^BM^CONS (^1) (^BM^CONS (^8) (^BM^ZERO)))))
        (^BM^LESSP W R)))))))
  (EQUAL (^BM^PLUS W (^BM^TIMES W (^BM^SUB1 N)))
         (^BM^PLUS (^BM^TIMES (^BM^SUB1 N) (^BM^DIFFERENCE R W))
          (^BM^PLUS
           (^BM^DIFFERENCE W (^BM^TIMES (^BM^SUB1 N) (^BM^DIFFERENCE R W)))
           (^BM^TIMES W (^BM^SUB1 N)))))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP (^BM^PLUS X (^BM^PLUS Z (^BM^TIMES X N)))))
  (EQUAL (^BM^QUOTIENT
          (^BM^PLUS Z
           (^BM^PLUS (^BM^TIMES X N)
            (^BM^PLUS (^BM^TIMES Z N) (^BM^TIMES X (^BM^TIMES N N)))))
          (^BM^PLUS X (^BM^PLUS Z (^BM^TIMES X N))))
         (^BM^PLUS N
          (^BM^QUOTIENT Z (^BM^PLUS X (^BM^PLUS Z (^BM^TIMES N X))))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^LESSP (^BM^PLUS Z (^BM^TIMES X (^BM^SUB1 N)))
   (^BM^PLUS X (^BM^PLUS Z (^BM^TIMES X (^BM^SUB1 N)))))
  (EQUAL (^BM^LESSP Z (^BM^PLUS X (^BM^PLUS Z (^BM^TIMES X (^BM^SUB1 N)))))
         (^BM^TRUE))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^NUMBERP W) (^BM^NOT (^BM^LESSP W R)))
  (EQUAL W (^BM^PLUS R (^BM^DIFFERENCE W R)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP N)
   (^BM^AND (^BM^NOT (^BM^ZEROP W))
    (^BM^AND (^BM^NOT (^BM^ZEROP R))
     (^BM^AND (^BM^RATE-PROXIMITY W R)
      (^BM^AND (^BM^LESSP N (^INT (^BM^CONS (^1) (^BM^CONS (^8) (^BM^ZERO)))))
       (^BM^NOT (^BM^LESSP W R)))))))
  (EQUAL (^BM^QUOTIENT (^BM^TIMES N W) R) N)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP N)
   (^BM^AND (^BM^NOT (^BM^ZEROP W))
    (^BM^AND (^BM^NOT (^BM^ZEROP R))
     (^BM^AND (^BM^RATE-PROXIMITY W R)
      (^BM^AND (^BM^LESSP N (^INT (^BM^CONS (^1) (^BM^CONS (^8) (^BM^ZERO)))))
       (^BM^LESSP W R))))))
  (EQUAL (^BM^QUOTIENT (^BM^TIMES N W) R) (^BM^SUB1 N))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP N)
   (^BM^AND (^BM^NOT (^BM^ZEROP W))
    (^BM^AND (^BM^NOT (^BM^ZEROP R))
     (^BM^AND (^BM^RATE-PROXIMITY W R)
      (^BM^LESSP N (^INT (^BM^CONS (^1) (^BM^CONS (^8) (^BM^ZERO)))))))))
  (EQUAL (^BM^QUOTIENT (^BM^TIMES N W) R) (IF (^BM^LESSP W R) (^BM^SUB1 N) N))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP N)
   (^BM^AND (^BM^NOT (^BM^ZEROP W))
    (^BM^AND (^BM^NOT (^BM^ZEROP R))
     (^BM^AND (^BM^RATE-PROXIMITY W R)
      (^BM^LESSP N (^INT (^BM^CONS (^1) (^BM^CONS (^8) (^BM^ZERO)))))))))
  (^BM^NOT (^BM^LESSP N (^BM^QUOTIENT (^BM^TIMES N W) R)))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP R)) (^BM^NOT (^BM^LESSP W TR-TS)))
  (^BM^NOT
   (^BM^LESSP (^BM^QUOTIENT (^BM^DIFFERENCE (^BM^TIMES N W) TR-TS) R)
    (^BM^QUOTIENT (^BM^TIMES (^BM^SUB1 N) W) R)))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP N)) (^BM^NOT (^BM^LESSP (^BM^TIMES N W) W))))

(LEMMA
 (EQUAL (EQUAL (^BM^PLUS I J) (^BM^PLUS I K)) (EQUAL (^BM^FIX J) (^BM^FIX K))))

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

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^BOOLP X) X)
  (EQUAL (EQUAL (^BM^TRUE) X) (^BM^TRUE))))

(DEFINE (^BM^B-NOT X) (^BM^NOT X))

(DEFINE (^BM^B-XOR X Y) (IF X (^BM^NOT Y) (IF Y (^BM^TRUE) (^BM^FALSE))))

(LEMMA (^BM^AND (^BM^B-XOR X (^BM^B-NOT X)) (^BM^B-XOR (^BM^B-NOT X) X)))

(DEFINE (^BM^SMOOTH PREV-VAL LST)
 (IF (^BM^NLISTP LST)
     (^NIL)
     (IF (^BM^B-XOR PREV-VAL (^BM^CAR LST))
         (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
          (^BM^SMOOTH (^BM^CAR LST) (^BM^CDR LST)))
         (^BM^CONS (^BM^CAR LST) (^BM^SMOOTH (^BM^CAR LST) (^BM^CDR LST))))))

(DEFINE (^BM^RECONCILE-SIGNALS A B)
 (IF (EQUAL A B) A (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))))

(DEFINE (^BM^SIG LST TS TR W)
 (IF (^BM^NLISTP LST)
     (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
     (IF (^BM^LESSP (^BM^PLUS TS W) TR)
         (^BM^RECONCILE-SIGNALS (^BM^CAR LST)
          (^BM^SIG (^BM^CDR LST) (^BM^PLUS TS W) TR W))
         (^BM^CAR LST))))

(DEFINE (^BM^ENDP LST TS TR W)
 (IF (^BM^NLISTP LST)
     (^BM^TRUE)
     (IF (^BM^LESSP (^BM^PLUS TS W) TR)
         (^BM^ENDP (^BM^CDR LST) (^BM^PLUS TS W) TR W)
         (^BM^FALSE))))

(DEFINE (^BM^LST+ LST TS NXTR W)
 (IF (^BM^NLISTP LST)
     LST
     (IF (^BM^LESSP NXTR (^BM^PLUS TS W))
         LST
         (^BM^LST+ (^BM^CDR LST) (^BM^PLUS TS W) NXTR W))))

(DEFINE (^BM^TS+ LST TS NXTR W)
 (IF (^BM^NLISTP LST)
     TS
     (IF (^BM^LESSP NXTR (^BM^PLUS TS W))
         TS
         (^BM^TS+ (^BM^CDR LST) (^BM^PLUS TS W) NXTR W))))

(LEMMA (^BM^NOT (^BM^LESSP (^BM^COUNT LST) (^BM^COUNT (^BM^LST+ LST TS TR W)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ENDP LST TS (^BM^PLUS R TR) W))
   (^BM^AND (^BM^NOT (^BM^ZEROP R))
    (EQUAL (^BM^COUNT LST) (^BM^COUNT (^BM^LST+ LST TS (^BM^PLUS R TR) W)))))
  (EQUAL (^BM^LESSP
          (^BM^DIFFERENCE (^BM^PLUS W (^BM^TS+ LST TS (^BM^PLUS R TR) W))
           (^BM^PLUS R TR))
          (^BM^DIFFERENCE (^BM^PLUS TS W) TR))
         (^BM^TRUE))))

(DEFINE (^BM^WARP LST TS TR W R)
 (IF (^BM^OR (^BM^ZEROP R) (^BM^ENDP LST TS (^BM^PLUS TR R) W))
     (^NIL)
     (^BM^CONS (^BM^SIG LST TS (^BM^PLUS TR R) W)
      (^BM^WARP (^BM^LST+ LST TS (^BM^PLUS TR R) W)
       (^BM^TS+ LST TS (^BM^PLUS TR R) W) (^BM^PLUS TR R) W R))))

(DEFINE (^BM^DET LST ORACLE)
 (IF (^BM^NLISTP LST)
     LST
     (IF (EQUAL (^BM^CAR LST) (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
         (^BM^CONS (IF (^BM^CAR ORACLE) (^BM^TRUE) (^BM^FALSE))
          (^BM^DET (^BM^CDR LST) (^BM^CDR ORACLE)))
         (^BM^CONS (^BM^CAR LST) (^BM^DET (^BM^CDR LST) ORACLE)))))

(DEFINE (^BM^ASYNC LST TS TR W R ORACLE)
 (^BM^DET (^BM^WARP (^BM^SMOOTH (^BM^TRUE) LST) TS TR W R) ORACLE))

(DEFINE (^BM^LISTN N VALUE)
 (IF (^BM^ZEROP N) (^NIL) (^BM^CONS VALUE (^BM^LISTN (^BM^SUB1 N) VALUE))))

(DEFINE (^BM^CSIG PREV-SIGNAL BIT) (IF BIT PREV-SIGNAL (^BM^B-NOT PREV-SIGNAL)))

(DEFINE (^BM^CELL PREV-SIGNAL N1 N2 BIT)
 (^BM^APP (^BM^LISTN N1 (^BM^B-NOT PREV-SIGNAL))
  (^BM^LISTN N2 (^BM^CSIG PREV-SIGNAL BIT))))

(DEFINE (^BM^CELLS PREV-SIGNAL N1 N2 MSG)
 (IF (^BM^NLISTP MSG)
     (^NIL)
     (^BM^APP (^BM^CELL PREV-SIGNAL N1 N2 (^BM^CAR MSG))
      (^BM^CELLS (^BM^CSIG PREV-SIGNAL (^BM^CAR MSG)) N1 N2 (^BM^CDR MSG)))))

(DEFINE (^BM^SEND MSG PAD1 N1 N2 PAD2)
 (^BM^APP (^BM^LISTN PAD1 (^BM^TRUE))
  (^BM^APP (^BM^CELLS (^BM^TRUE) N1 N2 MSG) (^BM^LISTN PAD2 (^BM^TRUE)))))

(DEFINE (^BM^SCAN PREV-SIGNAL LST)
 (IF (^BM^NLISTP LST)
     (^NIL)
     (IF (^BM^B-XOR PREV-SIGNAL (^BM^CAR LST))
         LST
         (^BM^SCAN PREV-SIGNAL (^BM^CDR LST)))))

(DEFINE (^BM^CDRN N LST)
 (IF (^BM^ZEROP N) LST (^BM^CDRN (^BM^SUB1 N) (^BM^CDR LST))))

(DEFINE (^BM^NTH N LST) (^BM^CAR (^BM^CDRN N LST)))

(DEFINE (^BM^RECV-BIT K LST)
 (IF (^BM^B-XOR (^BM^CAR LST) (^BM^NTH K LST)) (^BM^TRUE) (^BM^FALSE)))

(DEFINE (^BM^RECV I FLG K LST)
 (IF (^BM^ZEROP I)
     (^NIL)
     (^BM^CONS (^BM^RECV-BIT K (^BM^SCAN FLG LST))
      (^BM^RECV (^BM^SUB1 I) (^BM^NTH K (^BM^SCAN FLG LST)) K
       (^BM^CDRN K (^BM^SCAN FLG LST))))))

(DEFINE (^BM^BVP X)
 (IF (^BM^NLISTP X)
     (EQUAL X (^NIL))
     (^BM^AND (^BM^BOOLP (^BM^CAR X)) (^BM^BVP (^BM^CDR X)))))

(LEMMA (^BM^NOT (^BM^B-XOR X X)))

(DEFINE (^BM^LST* LST TS TR W R)
 (IF (^BM^OR (^BM^ZEROP R) (^BM^ENDP LST TS (^BM^PLUS TR R) W))
     LST
     (^BM^LST* (^BM^LST+ LST TS (^BM^PLUS TR R) W)
      (^BM^TS+ LST TS (^BM^PLUS TR R) W) (^BM^PLUS TR R) W R)))

(DEFINE (^BM^TS* LST TS TR W R)
 (IF (^BM^OR (^BM^ZEROP R) (^BM^ENDP LST TS (^BM^PLUS TR R) W))
     TS
     (^BM^TS* (^BM^LST+ LST TS (^BM^PLUS TR R) W)
      (^BM^TS+ LST TS (^BM^PLUS TR R) W) (^BM^PLUS TR R) W R)))

(DEFINE (^BM^TR* LST TS TR W R)
 (IF (^BM^OR (^BM^ZEROP R) (^BM^ENDP LST TS (^BM^PLUS TR R) W))
     TR
     (^BM^TR* (^BM^LST+ LST TS (^BM^PLUS TR R) W)
      (^BM^TS+ LST TS (^BM^PLUS TR R) W) (^BM^PLUS TR R) W R)))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^LESSP TR TS)) (^BM^NOT (^BM^ZEROP W)))
  (^BM^NOT (^BM^LESSP TR (^BM^TS+ LST TS TR W)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ENDP LST TS TR W))
   (^BM^AND (^BM^NOT (^BM^LESSP TR TS)) (^BM^NOT (^BM^ZEROP W))))
  (^BM^LESSP TR (^BM^PLUS W (^BM^TS+ LST TS TR W)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ENDP LST1 TS TR+ W)) (^BM^NOT (^BM^ZEROP W)))
  (EQUAL (^BM^LST+ (^BM^APP LST1 LST2) TS TR+ W)
         (^BM^APP (^BM^LST+ LST1 TS TR+ W) LST2))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ENDP LST1 TS TR+ W)) (^BM^NOT (^BM^ZEROP W)))
  (EQUAL (^BM^TS+ (^BM^APP LST1 LST2) TS TR+ W) (^BM^TS+ LST1 TS TR+ W))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ENDP LST1 TS TR+ W)) (^BM^NOT (^BM^ZEROP W)))
  (EQUAL (^BM^SIG (^BM^APP LST1 LST2) TS TR+ W) (^BM^SIG LST1 TS TR+ W))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ENDP LST1 TS TR+ W)) (^BM^NOT (^BM^ZEROP W)))
  (^BM^NOT (^BM^ENDP (^BM^APP LST1 LST2) TS TR+ W))))

(DEFINE (^BM^TARGET X) X)

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
     (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
      (^BM^AND (^BM^NOT (^BM^ZEROP W)) (^BM^NOT (^BM^ZEROP R)))))))
  (EQUAL (^BM^TARGET (^BM^WARP (^BM^APP LST1 LST2) TS TR W R))
         (^BM^APP (^BM^WARP LST1 TS TR W R)
          (^BM^WARP (^BM^APP (^BM^LST* LST1 TS TR W R) LST2)
           (^BM^TS* LST1 TS TR W R) (^BM^TR* LST1 TS TR W R) W R)))))

(DEFINE (^BM^NLST+ N TS TR W)
 (IF (^BM^ZEROP N)
     N
     (IF (^BM^LESSP TR (^BM^PLUS TS W))
         N
         (^BM^NLST+ (^BM^SUB1 N) (^BM^PLUS TS W) TR W))))

(LEMMA
 (EQUAL (^BM^LEN (^BM^LST+ LST TS TR W)) (^BM^NLST+ (^BM^LEN LST) TS TR W)))

(DEFINE (^BM^NTS+ N TS TR W)
 (IF (^BM^ZEROP N)
     TS
     (IF (^BM^LESSP TR (^BM^PLUS TS W))
         TS
         (^BM^NTS+ (^BM^SUB1 N) (^BM^PLUS TS W) TR W))))

(LEMMA (EQUAL (^BM^TS+ LST TS TR W) (^BM^NTS+ (^BM^LEN LST) TS TR W)))

(DEFINE (^BM^NENDP N TS TR W)
 (IF (^BM^ZEROP N)
     (^BM^TRUE)
     (IF (^BM^LESSP (^BM^PLUS TS W) TR)
         (^BM^NENDP (^BM^SUB1 N) (^BM^PLUS TS W) TR W)
         (^BM^FALSE))))

(LEMMA (EQUAL (^BM^ENDP LST TS TR W) (^BM^NENDP (^BM^LEN LST) TS TR W)))

(LEMMA (^BM^NOT (^BM^LESSP N (^BM^NLST+ N TS TR W))))

(LEMMA
 (EQUAL (EQUAL (^BM^NLST+ N TS (^BM^PLUS R TR) W) N)
        (^BM^OR (^BM^ZEROP N) (^BM^LESSP (^BM^PLUS R TR) (^BM^PLUS TS W)))))

(DEFINE (^BM^NLST* N TS TR W R)
 (IF (^BM^OR (^BM^ZEROP R) (^BM^NENDP N TS (^BM^PLUS TR R) W))
     N
     (^BM^NLST* (^BM^NLST+ N TS (^BM^PLUS TR R) W)
      (^BM^NTS+ N TS (^BM^PLUS TR R) W) (^BM^PLUS TR R) W R)))

(LEMMA
 (EQUAL (^BM^LEN (^BM^LST* LST TS TR W R)) (^BM^NLST* (^BM^LEN LST) TS TR W R)))

(DEFINE (^BM^NTS* N TS TR W R)
 (IF (^BM^OR (^BM^ZEROP R) (^BM^NENDP N TS (^BM^PLUS TR R) W))
     TS
     (^BM^NTS* (^BM^NLST+ N TS (^BM^PLUS TR R) W)
      (^BM^NTS+ N TS (^BM^PLUS TR R) W) (^BM^PLUS TR R) W R)))

(LEMMA (EQUAL (^BM^TS* LST TS TR W R) (^BM^NTS* (^BM^LEN LST) TS TR W R)))

(DEFINE (^BM^NTR* N TS TR W R)
 (IF (^BM^OR (^BM^ZEROP R) (^BM^NENDP N TS (^BM^PLUS TR R) W))
     TR
     (^BM^NTR* (^BM^NLST+ N TS (^BM^PLUS TR R) W)
      (^BM^NTS+ N TS (^BM^PLUS TR R) W) (^BM^PLUS TR R) W R)))

(LEMMA (EQUAL (^BM^TR* LST TS TR W R) (^BM^NTR* (^BM^LEN LST) TS TR W R)))

(LEMMA (EQUAL (^BM^LEN (^BM^LISTN N FLG)) (^BM^FIX N)))

(DEFINE (^BM^LASTN N LST)
 (IF (EQUAL N (^BM^LEN LST))
     LST
     (IF (^BM^NLISTP LST) LST (^BM^LASTN N (^BM^CDR LST)))))

(DEFINE (^BM^TAILP X LST)
 (IF (EQUAL X LST)
     (^BM^TRUE)
     (IF (^BM^NLISTP LST) (^BM^FALSE) (^BM^TAILP X (^BM^CDR LST)))))

(LEMMA (^BM^IMPLIES (^BM^AND (^BM^TAILP X Y) (^BM^TAILP Y Z)) (^BM^TAILP X Z)))

(LEMMA (^BM^TAILP (^BM^LST+ LST TS TR W) LST))

(LEMMA (^BM^TAILP (^BM^LST* LST TS TR W R) LST))

(LEMMA
 (EQUAL (^BM^LEN (^BM^LASTN N LST))
        (IF (^BM^LESSP (^BM^LEN LST) N) (^INT (^BM^ZERO)) (^BM^FIX N))))

(LEMMA (^BM^IMPLIES (^BM^TAILP X Y) (EQUAL (^BM^LASTN (^BM^LEN X) Y) X)))

(LEMMA
 (EQUAL (^BM^LASTN (^BM^LEN (^BM^LST* LST TS TR W R)) LST)
        (^BM^LST* LST TS TR W R)))

(DEFINE (^BM^PROPERP X)
 (IF (^BM^NLISTP X) (EQUAL X (^NIL)) (^BM^PROPERP (^BM^CDR X))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^PROPERP LST) (^BM^LESSP (^BM^LEN LST) N))
  (EQUAL (^BM^LASTN N LST) (^NIL))))

(LEMMA (^BM^PROPERP (^BM^LISTN N FLG)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP N) (^BM^AND (^BM^NUMBERP K) (^BM^NOT (^BM^LESSP K N))))
  (EQUAL (^BM^LASTN N (^BM^LISTN K FLG)) (^BM^LISTN N FLG))))

(LEMMA (^BM^NOT (^BM^LESSP N (^BM^NLST* N TS TR W R))))

(LEMMA
 (^BM^IMPLIES (^BM^NUMBERP N)
  (EQUAL (^BM^LST* (^BM^LISTN N FLG) TS TR W R)
         (^BM^LISTN (^BM^NLST* N TS TR W R) FLG))))

(DEFINE (^BM^N* N TS TR W R)
 (IF (^BM^OR (^BM^ZEROP R) (^BM^NENDP N TS (^BM^PLUS TR R) W))
     (^INT (^BM^ZERO))
     (^BM^ADD1
      (^BM^N* (^BM^NLST+ N TS (^BM^PLUS TR R) W)
       (^BM^NTS+ N TS (^BM^PLUS TR R) W) (^BM^PLUS TR R) W R))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^LESSP TR TS)) (^BM^NOT (^BM^ZEROP W)))
  (^BM^NOT (^BM^LESSP TR (^BM^NTS+ N TS TR W)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^NENDP N TS TR W))
   (^BM^AND (^BM^NOT (^BM^LESSP TR TS)) (^BM^NOT (^BM^ZEROP W))))
  (^BM^LESSP TR (^BM^PLUS W (^BM^NTS+ N TS TR W)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP N)
   (^BM^AND (^BM^NOT (^BM^NENDP N TS TR+ W)) (^BM^NOT (^BM^ZEROP W))))
  (EQUAL (^BM^LST+ (^BM^LISTN N FLG) TS TR+ W)
         (^BM^LISTN (^BM^NLST+ N TS TR+ W) FLG))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
   (^BM^AND (^BM^NUMBERP R)
    (^BM^AND (^BM^NOT (^BM^NENDP N TS (^BM^PLUS R TR) W))
     (^BM^AND (^BM^NUMBERP N)
      (^BM^AND (^BM^NUMBERP TS)
       (^BM^AND (^BM^NUMBERP TR)
        (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
         (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
          (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
           (^BM^NUMBERP W))))))))))
  (EQUAL (^BM^SIG (^BM^LISTN N FLG) TS (^BM^PLUS R TR) W) FLG)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP N)
   (^BM^AND (^BM^NUMBERP TS)
    (^BM^AND (^BM^NUMBERP TR)
     (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
      (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
       (^BM^AND (^BM^NOT (^BM^ZEROP W)) (^BM^NOT (^BM^ZEROP R))))))))
  (EQUAL (^BM^WARP (^BM^LISTN N FLG) TS TR W R)
         (^BM^LISTN (^BM^N* N TS TR W R) FLG))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR+) (^BM^NENDP (^BM^LEN PAD) TS TR+ W)))
  (EQUAL (^BM^LST+ (^BM^APP PAD LST) TS TR+ W)
         (^BM^LST+ LST (^BM^PLUS TS (^BM^TIMES (^BM^LEN PAD) W)) TR+ W))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR+)
    (^BM^AND (^BM^NUMBERP K) (^BM^NENDP K TS TR+ W))))
  (EQUAL (^BM^NTS+ (^BM^PLUS N K) TS TR+ W)
         (^BM^NTS+ N (^BM^PLUS TS (^BM^TIMES K W)) TR+ W))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NOT (^BM^ZEROP R))
    (^BM^NENDP (^BM^LEN PAD) TS (^BM^PLUS R TR) W)))
  (EQUAL (^BM^WARP (^BM^APP PAD LST) TS TR W R)
         (IF (^BM^NENDP (^BM^PLUS (^BM^LEN PAD) (^BM^LEN LST)) TS
              (^BM^PLUS R TR) W)
             (^NIL)
             (^BM^CONS (^BM^SIG (^BM^APP PAD LST) TS (^BM^PLUS R TR) W)
              (^BM^WARP
               (^BM^LST+ LST (^BM^PLUS TS (^BM^TIMES (^BM^LEN PAD) W))
                (^BM^PLUS R TR) W)
               (^BM^NTS+ (^BM^LEN LST)
                (^BM^PLUS TS (^BM^TIMES (^BM^LEN PAD) W)) (^BM^PLUS R TR) W)
               (^BM^PLUS R TR) W R))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (^BM^ZEROP R))
     (^BM^AND (^BM^NOT (^BM^ZEROP W))
      (^BM^AND (^BM^NOT (^BM^LESSP TR TS)) (^BM^LESSP TR (^BM^PLUS TS W)))))))
  (^BM^NENDP (^BM^NLST* K TS TR W R) (^BM^NTS* K TS TR W R)
   (^BM^PLUS R (^BM^NTR* K TS TR W R)) W)))

(DEFINE (^BM^NQG K TS TR W R)
 (IF (^BM^LESSP (^BM^PLUS R TR) (^BM^PLUS W (^BM^PLUS TS (^BM^TIMES W K))))
     (IF (^BM^LESSP (^BM^PLUS R (^BM^PLUS R TR))
          (^BM^PLUS W (^BM^PLUS TS (^BM^TIMES W K))))
         (^INT (^BM^CONS (^3) (^BM^ZERO)))
         (^INT (^BM^CONS (^2) (^BM^ZERO))))
     (^INT (^BM^CONS (^1) (^BM^ZERO)))))

(DEFINE (^BM^DWG K TS TR W R)
 (IF (^BM^LESSP (^BM^PLUS R TR) (^BM^PLUS TS (^BM^PLUS W (^BM^TIMES K W))))
     (IF (^BM^LESSP (^BM^PLUS R (^BM^PLUS R TR))
          (^BM^PLUS TS (^BM^PLUS W (^BM^PLUS W (^BM^TIMES K W)))))
         (^INT (^BM^ZERO))
         (^INT (^BM^CONS (^1) (^BM^ZERO))))
     (IF (EQUAL (^BM^PLUS R TR) (^BM^PLUS TS (^BM^PLUS W (^BM^TIMES K W))))
         (^INT (^BM^ZERO))
         (IF (^BM^AND
              (^BM^LESSP (^BM^PLUS TS (^BM^PLUS W (^BM^TIMES K W)))
               (^BM^PLUS R TR))
              (^BM^LESSP (^BM^PLUS R TR)
               (^BM^PLUS TS (^BM^PLUS W (^BM^PLUS W (^BM^TIMES K W))))))
             (^INT (^BM^ZERO))
             (IF (^BM^LESSP (^BM^PLUS R TR)
                  (^BM^PLUS TS (^BM^PLUS W (^BM^PLUS W (^BM^TIMES K W)))))
                 (^INT (^BM^ZERO))
                 (^INT (^BM^CONS (^1) (^BM^ZERO))))))))

(DEFINE (^BM^TSG K TS TR W R)
 (^BM^PLUS TS
  (^BM^PLUS (^BM^TIMES W K) (^BM^PLUS W (^BM^TIMES W (^BM^DWG K TS TR W R))))))

(DEFINE (^BM^TRG K TS TR W R) (^BM^PLUS TR (^BM^TIMES R (^BM^NQG K TS TR W R))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
     (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W)) (^BM^NOT (^BM^ZEROP W))))))
  (^BM^NOT (^BM^LESSP (^BM^NTR* K TS TR W R) (^BM^NTS* K TS TR W R)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
     (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W)) (^BM^NOT (^BM^ZEROP W))))))
  (^BM^LESSP (^BM^NTR* K TS TR W R) (^BM^PLUS W (^BM^NTS* K TS TR W R)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
     (^BM^AND (^BM^NUMBERP W)
      (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
       (^BM^AND (^BM^NUMBERP R)
        (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
         (^BM^AND (^BM^LESSP W (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) R))
          (^BM^AND
           (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W))
           (^BM^LESSP (^INT (^BM^CONS (^2) (^BM^ZERO))) K))))))))))
  (^BM^NOT (^BM^NENDP K TS (^BM^PLUS R TR) W))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NENDP K TS (^BM^PLUS R TR) W)
   (^BM^AND (^BM^NUMBERP TS)
    (^BM^AND (^BM^NUMBERP TR)
     (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
      (^BM^AND (^BM^NUMBERP W)
       (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
        (^BM^AND (^BM^NUMBERP R)
         (^BM^AND (^BM^NOT (^BM^LESSP (^BM^PLUS R TR) TS))
          (^BM^LESSP TR (^BM^PLUS TS W))))))))))
  (^BM^NOT (^BM^LESSP (^BM^PLUS R TR) (^BM^PLUS TS (^BM^TIMES K W))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (^BM^ZEROP W))
     (^BM^AND (^BM^NOT (^BM^ZEROP R))
      (^BM^AND (^BM^NOT (^BM^LESSP TR TS)) (^BM^LESSP TR (^BM^PLUS TS W)))))))
  (^BM^NOT
   (^BM^LESSP (^BM^PLUS R (^BM^NTR* K TS TR W R))
    (^BM^PLUS (^BM^NTS* K TS TR W R) (^BM^TIMES W (^BM^NLST* K TS TR W R)))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
     (^BM^AND (^BM^NUMBERP W)
      (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
       (^BM^AND (^BM^NUMBERP R)
        (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
         (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
          (^BM^AND
           (^BM^LESSP W (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) R))
           (^BM^AND
            (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W))
            (^BM^AND (^BM^LISTP REST)
             (^BM^AND (^BM^LESSP (^BM^PLUS TS (^BM^PLUS W W)) (^BM^PLUS R TR))
              (^BM^AND (^BM^LESSP (^BM^PLUS TS W) (^BM^PLUS R TR))
               (^BM^NOT
                (^BM^LESSP (^BM^PLUS R TR)
                 (^BM^PLUS TS (^BM^PLUS W W)))))))))))))))))
  (EQUAL (^BM^WARP
          (^BM^LST+ REST (^BM^PLUS TS (^BM^PLUS W W)) (^BM^PLUS R TR) W)
          (^BM^NTS+ (^BM^LEN REST) (^BM^PLUS TS (^BM^PLUS W W)) (^BM^PLUS R TR)
           W)
          (^BM^PLUS R TR) W R)
         (^BM^WARP REST (^BM^PLUS TS (^BM^PLUS W W)) (^BM^PLUS R TR) W R))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NUMBERP K)
     (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
      (^BM^AND (^BM^NUMBERP W)
       (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
        (^BM^AND (^BM^NUMBERP R)
         (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
          (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
           (^BM^AND
            (^BM^LESSP W (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) R))
            (^BM^AND
             (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W))
             (^BM^AND (^BM^LISTP REST)
              (^BM^AND (^BM^LISTP (^BM^CDR REST))
               (^BM^AND (EQUAL (^BM^SUB1 (^BM^SUB1 K)) (^INT (^BM^ZERO)))
                (^BM^AND
                 (^BM^LESSP (^BM^PLUS TS (^BM^PLUS W W)) (^BM^PLUS R TR))
                 (^BM^AND (^BM^LESSP (^BM^PLUS TS W) (^BM^PLUS R TR))
                  (^BM^AND
                   (^BM^LESSP (^BM^PLUS R TR)
                    (^BM^PLUS TS (^BM^PLUS W (^BM^TIMES K W))))
                   (^BM^AND
                    (^BM^NOT
                     (^BM^LESSP (^BM^PLUS R (^BM^PLUS R TR))
                      (^BM^PLUS TS (^BM^PLUS W (^BM^TIMES K W)))))
                    (^BM^LESSP (^BM^PLUS R (^BM^PLUS R TR))
                     (^BM^PLUS TS
                      (^BM^PLUS W
                       (^BM^PLUS W (^BM^TIMES K W)))))))))))))))))))))))
  (EQUAL (^BM^WARP (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))) REST)
          (^BM^PLUS TS (^BM^TIMES K W)) (^BM^PLUS R TR) W R)
         (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
          (^BM^WARP REST (^BM^PLUS TS (^BM^PLUS W (^BM^TIMES K W)))
           (^BM^PLUS TR (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) R)) W
           R)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
     (^BM^AND (^BM^NUMBERP W)
      (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
       (^BM^AND (^BM^NUMBERP R)
        (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
         (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
          (^BM^AND
           (^BM^LESSP W (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) R))
           (^BM^AND
            (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W))
            (^BM^AND (^BM^LISTP REST)
             (^BM^AND (^BM^LISTP (^BM^CDR REST))
              (^BM^AND (^BM^LESSP (^BM^PLUS TS W) (^BM^PLUS R TR))
               (^BM^AND
                (^BM^NOT
                 (^BM^LESSP (^BM^PLUS R TR) (^BM^PLUS TS (^BM^PLUS W W))))
                (^BM^LESSP (^BM^PLUS R TR)
                 (^BM^PLUS TS (^BM^PLUS W (^BM^PLUS W W))))))))))))))))))
  (EQUAL (^BM^WARP
          (^BM^CONS FLG1 (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))) REST))
          TS TR W R)
         (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
          (^BM^WARP REST (^BM^PLUS TS (^BM^PLUS W W)) (^BM^PLUS R TR) W R)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
     (^BM^AND (^BM^NUMBERP W)
      (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
       (^BM^AND (^BM^NUMBERP R)
        (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
         (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
          (^BM^AND
           (^BM^LESSP W (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) R))
           (^BM^AND
            (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W))
            (^BM^AND (^BM^LISTP REST)
             (^BM^AND (^BM^LISTP (^BM^CDR REST))
              (^BM^AND (^BM^LESSP (^BM^PLUS TS W) (^BM^PLUS R TR))
               (^BM^AND (^BM^NOT (^BM^LESSP (^BM^PLUS R TR) (^BM^PLUS TS W)))
                (^BM^AND (^BM^NOT (EQUAL (^BM^PLUS R TR) (^BM^PLUS TS W)))
                 (^BM^NOT
                  (^BM^LESSP (^BM^PLUS R TR)
                   (^BM^PLUS TS (^BM^PLUS W W)))))))))))))))))))
  (EQUAL (^BM^WARP (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))) REST) TS TR
          W R)
         (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
          (^BM^WARP (^BM^CDR REST) (^BM^PLUS TS (^BM^PLUS W W)) (^BM^PLUS R TR)
           W R)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
     (^BM^AND (^BM^NUMBERP W)
      (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
       (^BM^AND (^BM^NUMBERP R)
        (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
         (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
          (^BM^AND (^BM^LESSP W (^BM^PLUS R R))
           (^BM^AND
            (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W))
            (^BM^AND (^BM^LISTP REST)
             (^BM^AND (^BM^LISTP (^BM^CDR REST))
              (^BM^AND (^BM^LESSP (^BM^PLUS TS W) (^BM^PLUS R TR))
               (^BM^AND
                (^BM^LESSP (^BM^PLUS R TR) (^BM^PLUS TS (^BM^PLUS W W)))
                (^BM^AND
                 (^BM^NOT
                  (^BM^LESSP (^BM^PLUS R (^BM^PLUS R TR))
                   (^BM^PLUS TS (^BM^PLUS W W))))
                 (^BM^NOT
                  (^BM^LESSP (^BM^PLUS R (^BM^PLUS R TR))
                   (^BM^PLUS TS (^BM^PLUS W (^BM^PLUS W W))))))))))))))))))))
  (EQUAL (^BM^WARP
          (^BM^CONS FLG1 (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))) REST))
          TS TR W R)
         (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
          (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
           (^BM^WARP (^BM^CDR REST) (^BM^PLUS TS (^BM^PLUS W (^BM^PLUS W W)))
            (^BM^PLUS R (^BM^PLUS R TR)) W R))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
     (^BM^AND (^BM^NUMBERP W)
      (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
       (^BM^AND (^BM^NUMBERP R)
        (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
         (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
          (^BM^AND (^BM^LESSP W (^BM^PLUS R R))
           (^BM^AND
            (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W))
            (^BM^AND (^BM^LISTP REST)
             (^BM^AND (^BM^LISTP (^BM^CDR REST))
              (^BM^AND (^BM^LESSP (^BM^PLUS TS W) (^BM^PLUS R TR))
               (^BM^AND
                (^BM^LESSP (^BM^PLUS R TR) (^BM^PLUS TS (^BM^PLUS W W)))
                (^BM^AND
                 (^BM^NOT
                  (^BM^LESSP (^BM^PLUS R (^BM^PLUS R TR))
                   (^BM^PLUS TS (^BM^PLUS W W))))
                 (^BM^LESSP (^BM^PLUS R (^BM^PLUS R TR))
                  (^BM^PLUS TS (^BM^PLUS W (^BM^PLUS W W)))))))))))))))))))
  (EQUAL (^BM^WARP
          (^BM^CONS FLG1 (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))) REST))
          TS TR W R)
         (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
          (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
           (^BM^WARP REST (^BM^PLUS TS (^BM^PLUS W W))
            (^BM^PLUS R (^BM^PLUS R TR)) W R))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
     (^BM^AND (^BM^NUMBERP W)
      (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
       (^BM^AND (^BM^NUMBERP R)
        (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
         (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
          (^BM^AND (^BM^LESSP W (^BM^PLUS R R))
           (^BM^AND
            (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W))
            (^BM^AND (^BM^LISTP REST)
             (^BM^AND (^BM^LISTP (^BM^CDR REST))
              (^BM^AND (^BM^LESSP (^BM^PLUS TS W) (^BM^PLUS R TR))
               (^BM^AND
                (^BM^LESSP (^BM^PLUS R TR) (^BM^PLUS TS (^BM^PLUS W W)))
                (^BM^AND
                 (^BM^LESSP (^BM^PLUS R (^BM^PLUS R TR))
                  (^BM^PLUS TS (^BM^PLUS W W)))
                 (^BM^LESSP (^BM^PLUS R (^BM^PLUS R TR))
                  (^BM^PLUS TS (^BM^PLUS W (^BM^PLUS W W)))))))))))))))))))
  (EQUAL (^BM^WARP
          (^BM^CONS FLG1 (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))) REST))
          TS TR W R)
         (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
          (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
           (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
            (^BM^WARP REST (^BM^PLUS TS (^BM^PLUS W W))
             (^BM^PLUS TR (^BM^TIMES (^INT (^BM^CONS (^3) (^BM^ZERO))) R)) W
             R)))))))

(LEMMA
 (^BM^IMPLIES (^BM^LISTP MSG)
  (^BM^NOT
   (^BM^LESSP
    (^BM^TIMES (^INT (^BM^CONS (^1) (^BM^CONS (^8) (^BM^ZERO)))) (^BM^LEN MSG))
    (^INT (^BM^CONS (^1) (^BM^CONS (^8) (^BM^ZERO))))))))

(LEMMA (EQUAL (^BM^LISTN (^BM^ADD1 N) FLG) (^BM^CONS FLG (^BM^LISTN N FLG))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
     (^BM^AND (^BM^NUMBERP W)
      (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
       (^BM^AND (^BM^NUMBERP R)
        (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
         (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
          (^BM^AND (^BM^LESSP W (^BM^PLUS R R))
           (^BM^AND
            (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W))
            (^BM^AND (^BM^LISTP REST)
             (^BM^AND (^BM^LISTP (^BM^CDR REST))
              (^BM^AND (^BM^NOT (^BM^LESSP (^BM^PLUS R TR) (^BM^PLUS TS W)))
               (^BM^LESSP (^BM^PLUS R TR)
                (^BM^PLUS TS (^BM^PLUS W W))))))))))))))))
  (EQUAL (^BM^WARP (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))) REST) TS TR
          W R)
         (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
          (^BM^WARP REST (^BM^PLUS TS W) (^BM^PLUS R TR) W R)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
     (^BM^AND (^BM^NUMBERP W)
      (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
       (^BM^AND (^BM^NUMBERP R)
        (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
         (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
          (^BM^AND (^BM^LESSP W (^BM^PLUS R R))
           (^BM^AND
            (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W))
            (^BM^AND (^BM^LISTP REST)
             (^BM^AND (^BM^LISTP (^BM^CDR REST))
              (^BM^AND (^BM^LESSP (^BM^PLUS R TR) (^BM^PLUS TS W))
               (^BM^AND
                (^BM^NOT
                 (^BM^LESSP (^BM^PLUS R (^BM^PLUS R TR)) (^BM^PLUS TS W)))
                (^BM^LESSP (^BM^PLUS R (^BM^PLUS R TR))
                 (^BM^PLUS TS (^BM^PLUS W W)))))))))))))))))
  (EQUAL (^BM^WARP (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))) REST) TS TR
          W R)
         (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
          (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
           (^BM^WARP REST (^BM^PLUS TS W) (^BM^PLUS R (^BM^PLUS R TR)) W R))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NUMBERP K)
     (^BM^AND (^BM^NOT (^BM^ZEROP W))
      (^BM^AND (^BM^NOT (^BM^ZEROP R))
       (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
        (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
         (^BM^AND (^BM^LESSP W (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) R))
          (^BM^AND
           (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W))
           (^BM^AND (^BM^LISTP REST)
            (^BM^AND (^BM^LISTP (^BM^CDR REST))
             (^BM^NENDP K TS (^BM^PLUS R TR) W))))))))))))
  (EQUAL (^BM^WARP
          (^BM^APP (^BM^LISTN K FLG1)
           (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))) REST))
          TS TR W R)
         (^BM^APP
          (^BM^LISTN (^BM^NQG K TS TR W R)
           (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
          (^BM^WARP (^BM^CDRN (^BM^DWG K TS TR W R) REST) (^BM^TSG K TS TR W R)
           (^BM^TRG K TS TR W R) W R)))))

(DEFINE (^BM^NQ N TS TR W R)
 (^BM^NQG (^BM^NLST* N TS TR W R) (^BM^NTS* N TS TR W R) (^BM^NTR* N TS TR W R)
  W R))

(DEFINE (^BM^DW N TS TR W R)
 (^BM^DWG (^BM^NLST* N TS TR W R) (^BM^NTS* N TS TR W R) (^BM^NTR* N TS TR W R)
  W R))

(DEFINE (^BM^TS N TS TR W R)
 (^BM^TSG (^BM^NLST* N TS TR W R) (^BM^NTS* N TS TR W R) (^BM^NTR* N TS TR W R)
  W R))

(DEFINE (^BM^TR N TS TR W R)
 (^BM^TRG (^BM^NLST* N TS TR W R) (^BM^NTS* N TS TR W R) (^BM^NTR* N TS TR W R)
  W R))

(LEMMA
 (^BM^IMPLIES (^BM^LESSP (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^LEN X))
  (^BM^AND (^BM^LISTP X) (^BM^LISTP (^BM^CDR X)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (^BM^ZEROP W))
     (^BM^AND (^BM^NOT (^BM^ZEROP R))
      (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
       (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
        (^BM^AND (^BM^LESSP W (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) R))
         (^BM^AND (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W))
          (^BM^AND (^BM^NUMBERP N1)
           (^BM^LESSP (^INT (^BM^CONS (^2) (^BM^ZERO)))
            (^BM^LEN REST)))))))))))
  (EQUAL (^BM^TARGET
          (^BM^WARP
           (^BM^APP (^BM^LISTN N1 FLG1)
            (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))) REST))
           TS TR W R))
         (^BM^APP (^BM^LISTN (^BM^N* N1 TS TR W R) FLG1)
          (^BM^APP
           (^BM^LISTN (^BM^NQ N1 TS TR W R)
            (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
           (^BM^WARP (^BM^CDRN (^BM^DW N1 TS TR W R) REST)
            (^BM^TS N1 TS TR W R) (^BM^TR N1 TS TR W R) W R))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (^BM^ZEROP W))
     (^BM^AND (^BM^NOT (^BM^ZEROP R))
      (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
       (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
        (^BM^AND (^BM^LESSP W (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) R))
         (^BM^AND (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W))
          (^BM^AND (^BM^NUMBERP N1)
           (^BM^LESSP (^INT (^BM^CONS (^2) (^BM^ZERO)))
            (^BM^LEN REST)))))))))))
  (EQUAL (^BM^WARP
          (^BM^APP (^BM^LISTN N1 FLG1)
           (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))) REST))
          TS TR W R)
         (^BM^APP (^BM^LISTN (^BM^N* N1 TS TR W R) FLG1)
          (^BM^APP
           (^BM^LISTN (^BM^NQ N1 TS TR W R)
            (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
           (^BM^WARP (^BM^CDRN (^BM^DW N1 TS TR W R) REST)
            (^BM^TS N1 TS TR W R) (^BM^TR N1 TS TR W R) W R))))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^B-XOR FLG1 FLG2))
  (EQUAL (EQUAL (^BM^SMOOTH FLG2 REST) (^BM^SMOOTH FLG1 REST)) (^BM^TRUE))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^B-XOR FLG1 FLG2))
  (EQUAL (^BM^SMOOTH FLG1 (^BM^APP (^BM^LISTN P1 FLG2) REST))
         (^BM^APP (^BM^LISTN P1 FLG2) (^BM^SMOOTH FLG1 REST)))))

(LEMMA
 (EQUAL (^BM^LISTP (^BM^APP (^BM^LISTN N FLG) REST))
        (^BM^OR (^BM^NOT (^BM^ZEROP N)) (^BM^LISTP REST))))

(LEMMA
 (EQUAL (^BM^LISTP
         (^BM^CELLS FLG (^INT (^BM^CONS (^5) (^BM^ZERO)))
          (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO)))) MSG))
        (^BM^LISTP MSG)))

(LEMMA
 (EQUAL (^BM^CAR (^BM^APP A B)) (IF (^BM^LISTP A) (^BM^CAR A) (^BM^CAR B))))

(LEMMA (EQUAL (^BM^LISTP (^BM^LISTN N FLG)) (^BM^NOT (^BM^ZEROP N))))

(LEMMA
 (^BM^IMPLIES (^BM^LISTP MSG)
  (EQUAL (^BM^CAR
          (^BM^CELLS FLG (^INT (^BM^CONS (^5) (^BM^ZERO)))
           (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO)))) MSG))
         (^BM^B-NOT FLG))))

(LEMMA
 (^BM^IMPLIES (^BM^LISTP MSG)
  (EQUAL (^BM^SMOOTH (^BM^TRUE)
          (^BM^APP (^BM^LISTN P1 (^BM^TRUE))
           (^BM^APP
            (^BM^CELLS (^BM^TRUE) (^INT (^BM^CONS (^5) (^BM^ZERO)))
             (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO)))) MSG)
            (^BM^LISTN P2 (^BM^TRUE)))))
         (^BM^APP (^BM^LISTN P1 (^BM^TRUE))
          (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
           (^BM^SMOOTH (^BM^FALSE)
            (^BM^APP
             (^BM^CDR
              (^BM^CELLS (^BM^TRUE) (^INT (^BM^CONS (^5) (^BM^ZERO)))
               (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO)))) MSG))
             (^BM^LISTN P2 (^BM^TRUE)))))))))

(DEFINE (^BM^ORACLE* LST ORACLE)
 (IF (^BM^NLISTP LST)
     ORACLE
     (IF (EQUAL (^BM^CAR LST) (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
         (^BM^ORACLE* (^BM^CDR LST) (^BM^CDR ORACLE))
         (^BM^ORACLE* (^BM^CDR LST) ORACLE))))

(LEMMA
 (EQUAL (^BM^DET (^BM^APP LST1 LST2) ORACLE)
        (^BM^APP (^BM^DET LST1 ORACLE)
         (^BM^DET LST2 (^BM^ORACLE* LST1 ORACLE)))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (EQUAL FLG (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))))
  (EQUAL (^BM^DET (^BM^LISTN N FLG) ORACLE) (^BM^LISTN N FLG))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (EQUAL FLG (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))))
  (EQUAL (^BM^ORACLE* (^BM^LISTN N FLG) ORACLE) ORACLE)))

(LEMMA (EQUAL (^BM^LEN (^BM^SMOOTH FLG LST)) (^BM^LEN LST)))

(LEMMA
 (EQUAL (^BM^CDR (^BM^APP A B))
        (IF (^BM^LISTP A) (^BM^APP (^BM^CDR A) B) (^BM^CDR B))))

(LEMMA
 (^BM^IMPLIES (^BM^LISTP MSG)
  (^BM^LESSP (^INT (^BM^CONS (^2) (^BM^ZERO)))
   (^BM^LEN
    (^BM^CDR
     (^BM^CELLS (^BM^TRUE) (^INT (^BM^CONS (^5) (^BM^ZERO)))
      (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO)))) MSG))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^BVP MSG)
   (^BM^AND (^BM^LISTP MSG)
    (^BM^AND (^BM^NUMBERP TS)
     (^BM^AND (^BM^NUMBERP TR)
      (^BM^AND (^BM^NOT (^BM^ZEROP W))
       (^BM^AND (^BM^NOT (^BM^ZEROP R))
        (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
         (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
          (^BM^AND (^BM^RATE-PROXIMITY W R) (^BM^NUMBERP P1))))))))))
  (EQUAL (^BM^ASYNC
          (^BM^SEND MSG P1 (^INT (^BM^CONS (^5) (^BM^ZERO)))
           (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO)))) P2)
          TS TR W R ORACLE)
         (^BM^APP (^BM^LISTN (^BM^N* P1 TS TR W R) (^BM^TRUE))
          (^BM^APP
           (^BM^DET
            (^BM^LISTN
             (^BM^NQG (^BM^NLST* P1 TS TR W R) (^BM^NTS* P1 TS TR W R)
              (^BM^NTR* P1 TS TR W R) W R)
             (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
            ORACLE)
           (^BM^DET
            (^BM^WARP
             (^BM^CDRN
              (^BM^DWG (^BM^NLST* P1 TS TR W R) (^BM^NTS* P1 TS TR W R)
               (^BM^NTR* P1 TS TR W R) W R)
              (^BM^SMOOTH (^BM^FALSE)
               (^BM^APP
                (^BM^CDR
                 (^BM^CELLS (^BM^TRUE) (^INT (^BM^CONS (^5) (^BM^ZERO)))
                  (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO)))) MSG))
                (^BM^LISTN P2 (^BM^TRUE)))))
             (^BM^TSG (^BM^NLST* P1 TS TR W R) (^BM^NTS* P1 TS TR W R)
              (^BM^NTR* P1 TS TR W R) W R)
             (^BM^TRG (^BM^NLST* P1 TS TR W R) (^BM^NTS* P1 TS TR W R)
              (^BM^NTR* P1 TS TR W R) W R)
             W R)
            (^BM^ORACLE*
             (^BM^LISTN
              (^BM^NQG (^BM^NLST* P1 TS TR W R) (^BM^NTS* P1 TS TR W R)
               (^BM^NTR* P1 TS TR W R) W R)
              (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
             ORACLE)))))))

(LEMMA
 (EQUAL (^BM^SCAN FLG (^BM^APP (^BM^LISTN N FLG) REST)) (^BM^SCAN FLG REST)))

(LEMMA
 (EQUAL (^BM^RECV N (^BM^TRUE) K (^BM^APP (^BM^LISTN P1 (^BM^TRUE)) REST))
        (^BM^RECV N (^BM^TRUE) K REST)))

(LEMMA
 (^BM^AND (^BM^LESSP (^INT (^BM^ZERO)) (^BM^NQG N TS TR W R))
  (^BM^NOT
   (^BM^LESSP (^INT (^BM^CONS (^3) (^BM^ZERO))) (^BM^NQG N TS TR W R)))))

(LEMMA
 (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) (^BM^DWG N TS TR W R))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NUMBERP N)
     (^BM^AND (^BM^NOT (^BM^ZEROP W))
      (^BM^AND (^BM^NOT (^BM^ZEROP R))
       (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
        (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
         (^BM^AND (^BM^LESSP W (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) R))
          (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W))))))))))
  (^BM^NOT
   (^BM^LESSP
    (^BM^TRG (^BM^NLST* N TS TR W R) (^BM^NTS* N TS TR W R)
     (^BM^NTR* N TS TR W R) W R)
    (^BM^TSG (^BM^NLST* N TS TR W R) (^BM^NTS* N TS TR W R)
     (^BM^NTR* N TS TR W R) W R)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NUMBERP N)
     (^BM^AND (^BM^NOT (^BM^ZEROP W))
      (^BM^AND (^BM^NOT (^BM^ZEROP R))
       (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
        (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
         (^BM^AND (^BM^LESSP W (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) R))
          (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W))))))))))
  (^BM^LESSP
   (^BM^TRG (^BM^NLST* N TS TR W R) (^BM^NTS* N TS TR W R)
    (^BM^NTR* N TS TR W R) W R)
   (^BM^PLUS W
    (^BM^TSG (^BM^NLST* N TS TR W R) (^BM^NTS* N TS TR W R)
     (^BM^NTR* N TS TR W R) W R)))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP N1))
  (EQUAL (^BM^CDR
          (^BM^APP (^BM^CELL FLG1 N1 N2 BIT) (^BM^CELLS FLG2 N1 N2 MSG)))
         (^BM^APP (^BM^CELL FLG1 (^BM^SUB1 N1) N2 BIT)
          (^BM^CELLS FLG2 N1 N2 MSG)))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^B-XOR FLG1 FLG2))
  (EQUAL (^BM^SMOOTH FLG1 (^BM^LISTN N FLG2)) (^BM^LISTN N FLG2))))

(LEMMA
 (^BM^IMPLIES (^BM^B-XOR FLG1 FLG2)
  (^BM^AND (^BM^NOT (^BM^B-XOR FLG1 (^BM^B-NOT FLG2)))
   (^BM^NOT (^BM^B-XOR (^BM^B-NOT FLG2) FLG1)))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP N)) (^BM^B-XOR FLG1 FLG2))
  (EQUAL (^BM^SMOOTH FLG1 (^BM^APP (^BM^LISTN N FLG2) REST))
         (^BM^APP (^BM^SMOOTH FLG1 (^BM^LISTN N FLG2))
          (^BM^SMOOTH FLG2 REST)))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP N1)) (^BM^B-XOR FLG1 FLG2))
  (EQUAL (^BM^SMOOTH FLG1
          (^BM^APP (^BM^CELL FLG2 M1 N1 BIT)
           (^BM^APP (^BM^CELLS (^BM^CSIG FLG2 BIT) M N MSG)
            (^BM^LISTN P2 (^BM^TRUE)))))
         (^BM^APP (^BM^SMOOTH FLG1 (^BM^CELL FLG2 M1 N1 BIT))
          (^BM^SMOOTH (^BM^CSIG FLG2 BIT)
           (^BM^APP (^BM^CELLS (^BM^CSIG FLG2 BIT) M N MSG)
            (^BM^LISTN P2 (^BM^TRUE))))))))

(LEMMA (^BM^IMPLIES (^BM^B-XOR X Y) (^BM^B-XOR Y X)))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP M))
  (^BM^LISTP (^BM^SMOOTH FLG1 (^BM^CELL FLG2 M N BIT)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP M))
   (^BM^AND (^BM^NUMBERP DW)
    (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) DW))))
  (EQUAL (^BM^CDRN DW (^BM^APP (^BM^SMOOTH FLG1 (^BM^CELL FLG2 M N BIT)) REST))
         (^BM^APP (^BM^CDRN DW (^BM^SMOOTH FLG1 (^BM^CELL FLG2 M N BIT)))
          REST))))

(LEMMA
 (EQUAL (^BM^CAR (^BM^LISTN N FLG)) (IF (^BM^ZEROP N) (^INT (^BM^ZERO)) FLG)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (^BM^ZEROP M))
   (^BM^AND (^BM^NUMBERP DW)
    (^BM^AND (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) DW))
     (^BM^B-XOR FLG1 FLG2))))
  (EQUAL (^BM^CDRN DW (^BM^SMOOTH FLG2 (^BM^CELL FLG1 M N (^BM^CAR MSG))))
         (^BM^SMOOTH FLG2
          (^BM^CELL FLG1 (^BM^DIFFERENCE M DW) N (^BM^CAR MSG))))))

(LEMMA (EQUAL (^BM^LEN (^BM^CELL FLG M N BIT)) (^BM^PLUS M N)))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) DW))
  (EQUAL (^BM^ADD1
          (^BM^PLUS (^INT (^BM^CONS (^1) (^BM^CONS (^2) (^BM^ZERO))))
           (^BM^DIFFERENCE (^INT (^BM^CONS (^4) (^BM^ZERO))) DW)))
         (^BM^DIFFERENCE (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO))))
          DW))))

(LEMMA
 (EQUAL (^BM^LST* LST TS TR W R)
        (^BM^LASTN (^BM^NLST* (^BM^LEN LST) TS TR W R) LST)))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^LESSP (^BM^LEN B) N))
  (EQUAL (^BM^LASTN N (^BM^APP A B)) (^BM^LASTN N B))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (^BM^ZEROP W))
     (^BM^AND (^BM^NOT (^BM^ZEROP R))
      (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
       (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
        (^BM^AND (^BM^LESSP W (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) R))
         (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W)))))))))
  (^BM^NOT
   (^BM^LESSP (^INT (^BM^CONS (^2) (^BM^ZERO))) (^BM^NLST* N TS TR W R)))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP N)) (^BM^B-XOR FLG1 FLG2))
  (EQUAL (^BM^SMOOTH FLG1 (^BM^LISTN N FLG2))
         (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
          (^BM^LISTN (^BM^SUB1 N) FLG2)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (^BM^ZEROP W))
     (^BM^AND (^BM^NOT (^BM^ZEROP R))
      (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
       (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
        (^BM^AND (^BM^LESSP W (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) R))
         (^BM^AND (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W))
          (^BM^AND (^BM^NOT (^BM^ZEROP M))
           (^BM^AND (^BM^NUMBERP N)
            (^BM^AND (^BM^LESSP (^INT (^BM^CONS (^2) (^BM^ZERO))) N)
             (^BM^B-XOR FLG1 FLG2))))))))))))
  (EQUAL (^BM^LST* (^BM^SMOOTH FLG2 (^BM^CELL FLG1 M N BIT)) TS TR W R)
         (^BM^LISTN (^BM^NLST* (^BM^PLUS M N) TS TR W R) (^BM^CSIG FLG1 BIT)))))

(LEMMA
 (EQUAL (^BM^CDR (^BM^LISTN N FLG))
        (IF (^BM^ZEROP N) (^INT (^BM^ZERO)) (^BM^LISTN (^BM^SUB1 N) FLG))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^LISTP MSG) (^BM^NOT (^BM^ZEROP M)))
  (EQUAL (^BM^SMOOTH FLG
          (^BM^APP (^BM^CELLS FLG M N MSG) (^BM^LISTN P2 (^BM^TRUE))))
         (^BM^CONS (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))
          (^BM^SMOOTH (^BM^B-NOT FLG)
           (^BM^APP (^BM^CDR (^BM^CELLS FLG M N MSG))
            (^BM^LISTN P2 (^BM^TRUE))))))))

(LEMMA
 (^BM^IMPLIES (^BM^LISTP MSG)
  (^BM^LESSP (^INT (^BM^CONS (^2) (^BM^ZERO)))
   (^BM^LEN
    (^BM^CDR
     (^BM^CELLS FLG (^INT (^BM^CONS (^5) (^BM^ZERO)))
      (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO)))) MSG))))))

(LEMMA (EQUAL (^BM^APP (^BM^LISTN (^INT (^BM^ZERO)) FLG) REST) REST))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^BVP MSG)
   (^BM^AND (^BM^LISTP MSG)
    (^BM^AND (^BM^LISTP (^BM^CDR MSG))
     (^BM^AND (^BM^NUMBERP TS)
      (^BM^AND (^BM^NUMBERP TR)
       (^BM^AND (^BM^NOT (^BM^ZEROP W))
        (^BM^AND (^BM^NOT (^BM^ZEROP R))
         (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
          (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
           (^BM^AND (^BM^RATE-PROXIMITY W R)
            (^BM^AND (^BM^NUMBERP NQ)
             (^BM^AND
              (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^3) (^BM^ZERO))) NQ))
              (^BM^AND (^BM^NUMBERP DW)
               (^BM^AND
                (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) DW))
                (^BM^B-XOR FLG1 FLG2)))))))))))))))
  (EQUAL (^BM^RECV (^BM^LEN MSG) FLG1
          (^INT (^BM^CONS (^1) (^BM^CONS (^0) (^BM^ZERO))))
          (^BM^APP
           (^BM^DET (^BM^LISTN NQ (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
            ORACLE1)
           (^BM^DET
            (^BM^TARGET
             (^BM^WARP
              (^BM^CDRN DW
               (^BM^SMOOTH FLG2
                (^BM^APP
                 (^BM^CDR
                  (^BM^CELLS FLG1 (^INT (^BM^CONS (^5) (^BM^ZERO)))
                   (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO)))) MSG))
                 (^BM^LISTN P2 (^BM^TRUE)))))
              TS TR W R))
            ORACLE2)))
         (^BM^RECV (^BM^LEN MSG) FLG1
          (^INT (^BM^CONS (^1) (^BM^CONS (^0) (^BM^ZERO))))
          (^BM^APP
           (^BM^DET (^BM^LISTN NQ (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
            ORACLE1)
           (^BM^APP
            (^BM^DET
             (^BM^WARP
              (^BM^SMOOTH FLG2
               (^BM^CELL FLG1
                (^BM^DIFFERENCE (^INT (^BM^CONS (^4) (^BM^ZERO))) DW)
                (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO))))
                (^BM^CAR MSG)))
              TS TR W R)
             ORACLE2)
            (^BM^APP
             (^BM^DET
              (^BM^LISTN
               (^BM^NQG
                (^BM^NLST*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                (^BM^NTS*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                (^BM^NTR*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                W R)
               (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
              (^BM^ORACLE*
               (^BM^WARP
                (^BM^SMOOTH FLG2
                 (^BM^CELL FLG1
                  (^BM^DIFFERENCE (^INT (^BM^CONS (^4) (^BM^ZERO))) DW)
                  (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO))))
                  (^BM^CAR MSG)))
                TS TR W R)
               ORACLE2))
             (^BM^DET
              (^BM^WARP
               (^BM^CDRN
                (^BM^DWG
                 (^BM^NLST*
                  (^BM^DIFFERENCE
                   (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                  TS TR W R)
                 (^BM^NTS*
                  (^BM^DIFFERENCE
                   (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                  TS TR W R)
                 (^BM^NTR*
                  (^BM^DIFFERENCE
                   (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                  TS TR W R)
                 W R)
                (^BM^SMOOTH (^BM^B-NOT (^BM^CSIG FLG1 (^BM^CAR MSG)))
                 (^BM^APP
                  (^BM^CDR
                   (^BM^CELLS (^BM^CSIG FLG1 (^BM^CAR MSG))
                    (^INT (^BM^CONS (^5) (^BM^ZERO)))
                    (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO))))
                    (^BM^CDR MSG)))
                  (^BM^LISTN P2 (^BM^TRUE)))))
               (^BM^TSG
                (^BM^NLST*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                (^BM^NTS*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                (^BM^NTR*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                W R)
               (^BM^TRG
                (^BM^NLST*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                (^BM^NTS*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                (^BM^NTR*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                W R)
               W R)
              (^BM^ORACLE*
               (^BM^LISTN
                (^BM^NQG
                 (^BM^NLST*
                  (^BM^DIFFERENCE
                   (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                  TS TR W R)
                 (^BM^NTS*
                  (^BM^DIFFERENCE
                   (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                  TS TR W R)
                 (^BM^NTR*
                  (^BM^DIFFERENCE
                   (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                  TS TR W R)
                 W R)
                (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
               (^BM^ORACLE*
                (^BM^WARP
                 (^BM^SMOOTH FLG2
                  (^BM^CELL FLG1
                   (^BM^DIFFERENCE (^INT (^BM^CONS (^4) (^BM^ZERO))) DW)
                   (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO))))
                   (^BM^CAR MSG)))
                 TS TR W R)
                ORACLE2))))))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^BVP MSG)
   (^BM^AND (^BM^LISTP MSG)
    (^BM^AND (^BM^LISTP (^BM^CDR MSG))
     (^BM^AND (^BM^NUMBERP TS)
      (^BM^AND (^BM^NUMBERP TR)
       (^BM^AND (^BM^NOT (^BM^ZEROP W))
        (^BM^AND (^BM^NOT (^BM^ZEROP R))
         (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
          (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
           (^BM^AND (^BM^RATE-PROXIMITY W R)
            (^BM^AND (^BM^NUMBERP NQ)
             (^BM^AND
              (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^3) (^BM^ZERO))) NQ))
              (^BM^AND (^BM^NUMBERP DW)
               (^BM^AND
                (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) DW))
                (^BM^B-XOR FLG1 FLG2)))))))))))))))
  (EQUAL (^BM^RECV (^BM^LEN MSG) FLG1
          (^INT (^BM^CONS (^1) (^BM^CONS (^0) (^BM^ZERO))))
          (^BM^APP
           (^BM^DET (^BM^LISTN NQ (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
            ORACLE1)
           (^BM^DET
            (^BM^WARP
             (^BM^CDRN DW
              (^BM^SMOOTH FLG2
               (^BM^APP
                (^BM^CDR
                 (^BM^CELLS FLG1 (^INT (^BM^CONS (^5) (^BM^ZERO)))
                  (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO)))) MSG))
                (^BM^LISTN P2 (^BM^TRUE)))))
             TS TR W R)
            ORACLE2)))
         (^BM^RECV (^BM^LEN MSG) FLG1
          (^INT (^BM^CONS (^1) (^BM^CONS (^0) (^BM^ZERO))))
          (^BM^APP
           (^BM^DET (^BM^LISTN NQ (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
            ORACLE1)
           (^BM^APP
            (^BM^DET
             (^BM^WARP
              (^BM^SMOOTH FLG2
               (^BM^CELL FLG1
                (^BM^DIFFERENCE (^INT (^BM^CONS (^4) (^BM^ZERO))) DW)
                (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO))))
                (^BM^CAR MSG)))
              TS TR W R)
             ORACLE2)
            (^BM^APP
             (^BM^DET
              (^BM^LISTN
               (^BM^NQG
                (^BM^NLST*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                (^BM^NTS*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                (^BM^NTR*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                W R)
               (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
              (^BM^ORACLE*
               (^BM^WARP
                (^BM^SMOOTH FLG2
                 (^BM^CELL FLG1
                  (^BM^DIFFERENCE (^INT (^BM^CONS (^4) (^BM^ZERO))) DW)
                  (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO))))
                  (^BM^CAR MSG)))
                TS TR W R)
               ORACLE2))
             (^BM^DET
              (^BM^WARP
               (^BM^CDRN
                (^BM^DWG
                 (^BM^NLST*
                  (^BM^DIFFERENCE
                   (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                  TS TR W R)
                 (^BM^NTS*
                  (^BM^DIFFERENCE
                   (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                  TS TR W R)
                 (^BM^NTR*
                  (^BM^DIFFERENCE
                   (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                  TS TR W R)
                 W R)
                (^BM^SMOOTH (^BM^B-NOT (^BM^CSIG FLG1 (^BM^CAR MSG)))
                 (^BM^APP
                  (^BM^CDR
                   (^BM^CELLS (^BM^CSIG FLG1 (^BM^CAR MSG))
                    (^INT (^BM^CONS (^5) (^BM^ZERO)))
                    (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO))))
                    (^BM^CDR MSG)))
                  (^BM^LISTN P2 (^BM^TRUE)))))
               (^BM^TSG
                (^BM^NLST*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                (^BM^NTS*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                (^BM^NTR*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                W R)
               (^BM^TRG
                (^BM^NLST*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                (^BM^NTS*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                (^BM^NTR*
                 (^BM^DIFFERENCE
                  (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                 TS TR W R)
                W R)
               W R)
              (^BM^ORACLE*
               (^BM^LISTN
                (^BM^NQG
                 (^BM^NLST*
                  (^BM^DIFFERENCE
                   (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                  TS TR W R)
                 (^BM^NTS*
                  (^BM^DIFFERENCE
                   (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                  TS TR W R)
                 (^BM^NTR*
                  (^BM^DIFFERENCE
                   (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
                  TS TR W R)
                 W R)
                (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
               (^BM^ORACLE*
                (^BM^WARP
                 (^BM^SMOOTH FLG2
                  (^BM^CELL FLG1
                   (^BM^DIFFERENCE (^INT (^BM^CONS (^4) (^BM^ZERO))) DW)
                   (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO))))
                   (^BM^CAR MSG)))
                 TS TR W R)
                ORACLE2))))))))))

(DEFINE (^BM^LOOP-IND-HINT NQ ORACLE1 DW FLG2 FLG1 MSG TS TR W R ORACLE2)
 (IF (^BM^NLISTP MSG)
     (^BM^TRUE)
     (IF (^BM^NLISTP (^BM^CDR MSG))
         (^BM^TRUE)
         (^BM^LOOP-IND-HINT
          (^BM^NQG
           (^BM^NLST*
            (^BM^DIFFERENCE (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO))))
             DW)
            TS TR W R)
           (^BM^NTS*
            (^BM^DIFFERENCE (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO))))
             DW)
            TS TR W R)
           (^BM^NTR*
            (^BM^DIFFERENCE (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO))))
             DW)
            TS TR W R)
           W R)
          (^BM^ORACLE*
           (^BM^WARP
            (^BM^SMOOTH FLG2
             (^BM^CELL FLG1
              (^BM^DIFFERENCE (^INT (^BM^CONS (^4) (^BM^ZERO))) DW)
              (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO)))) (^BM^CAR MSG)))
            TS TR W R)
           ORACLE2)
          (^BM^DWG
           (^BM^NLST*
            (^BM^DIFFERENCE (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO))))
             DW)
            TS TR W R)
           (^BM^NTS*
            (^BM^DIFFERENCE (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO))))
             DW)
            TS TR W R)
           (^BM^NTR*
            (^BM^DIFFERENCE (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO))))
             DW)
            TS TR W R)
           W R)
          (^BM^B-NOT (^BM^CSIG FLG1 (^BM^CAR MSG)))
          (^BM^CSIG FLG1 (^BM^CAR MSG)) (^BM^CDR MSG)
          (^BM^TSG
           (^BM^NLST*
            (^BM^DIFFERENCE (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO))))
             DW)
            TS TR W R)
           (^BM^NTS*
            (^BM^DIFFERENCE (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO))))
             DW)
            TS TR W R)
           (^BM^NTR*
            (^BM^DIFFERENCE (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO))))
             DW)
            TS TR W R)
           W R)
          (^BM^TRG
           (^BM^NLST*
            (^BM^DIFFERENCE (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO))))
             DW)
            TS TR W R)
           (^BM^NTS*
            (^BM^DIFFERENCE (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO))))
             DW)
            TS TR W R)
           (^BM^NTR*
            (^BM^DIFFERENCE (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO))))
             DW)
            TS TR W R)
           W R)
          W R
          (^BM^ORACLE*
           (^BM^LISTN
            (^BM^NQG
             (^BM^NLST*
              (^BM^DIFFERENCE (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO))))
               DW)
              TS TR W R)
             (^BM^NTS*
              (^BM^DIFFERENCE (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO))))
               DW)
              TS TR W R)
             (^BM^NTR*
              (^BM^DIFFERENCE (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO))))
               DW)
              TS TR W R)
             W R)
            (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
           (^BM^ORACLE*
            (^BM^WARP
             (^BM^SMOOTH FLG2
              (^BM^CELL FLG1
               (^BM^DIFFERENCE (^INT (^BM^CONS (^4) (^BM^ZERO))) DW)
               (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO))))
               (^BM^CAR MSG)))
             TS TR W R)
            ORACLE2))))))

(LEMMA
 (EQUAL (^BM^APP (^BM^LISTN M FLG) (^BM^LISTN N FLG))
        (^BM^LISTN (^BM^PLUS M N) FLG)))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^LESSP N DW))
  (EQUAL (^BM^CDRN DW (^BM^LISTN N FLG))
         (^BM^LISTN (^BM^DIFFERENCE N DW) FLG))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^BOOLP BIT)
   (^BM^AND (^BM^NUMBERP TS)
    (^BM^AND (^BM^NUMBERP TR)
     (^BM^AND (^BM^NOT (^BM^ZEROP W))
      (^BM^AND (^BM^NOT (^BM^ZEROP R))
       (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
        (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
         (^BM^AND (^BM^RATE-PROXIMITY W R)
          (^BM^AND (^BM^NUMBERP M)
           (^BM^AND (^BM^NUMBERP N)
            (^BM^AND (^BM^LESSP (^INT (^BM^CONS (^3) (^BM^ZERO))) N)
             (^BM^B-XOR FLG1 FLG2))))))))))))
  (EQUAL (^BM^WARP (^BM^SMOOTH FLG2 (^BM^CELL FLG1 M N BIT)) TS TR W R)
         (IF BIT
             (^BM^APP (^BM^LISTN (^BM^N* M TS TR W R) (^BM^B-NOT FLG1))
              (^BM^APP
               (^BM^LISTN
                (^BM^NQG (^BM^NLST* M TS TR W R) (^BM^NTS* M TS TR W R)
                 (^BM^NTR* M TS TR W R) W R)
                (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
               (^BM^LISTN
                (^BM^N*
                 (^BM^DIFFERENCE (^BM^SUB1 N)
                  (^BM^DWG (^BM^NLST* M TS TR W R) (^BM^NTS* M TS TR W R)
                   (^BM^NTR* M TS TR W R) W R))
                 (^BM^TSG (^BM^NLST* M TS TR W R) (^BM^NTS* M TS TR W R)
                  (^BM^NTR* M TS TR W R) W R)
                 (^BM^TRG (^BM^NLST* M TS TR W R) (^BM^NTS* M TS TR W R)
                  (^BM^NTR* M TS TR W R) W R)
                 W R)
                FLG1)))
             (^BM^LISTN (^BM^N* (^BM^PLUS M N) TS TR W R) (^BM^B-NOT FLG1))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR+)
    (^BM^AND (^BM^NOT (^BM^ZEROP W)) (^BM^LESSP TS TR+))))
  (EQUAL (^BM^NENDP N TS TR+ W) (^BM^LESSP (^BM^PLUS TS (^BM^TIMES N W)) TR+))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^NUMBERP N) (^BM^NOT (^BM^ZEROP W)))
  (EQUAL (^BM^NLST+ N TS (^BM^PLUS TS W) W) (^BM^SUB1 N))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP N)
   (^BM^AND (^BM^NUMBERP TS)
    (^BM^AND (^BM^NUMBERP TR+)
     (^BM^AND (^BM^NOT (^BM^ZEROP W)) (^BM^LESSP TS TR+)))))
  (EQUAL (^BM^NLST+ N TS TR+ W)
         (^BM^DIFFERENCE N (^BM^QUOTIENT (^BM^DIFFERENCE TR+ TS) W)))))

(LEMMA (^BM^NOT (^BM^LESSP (^BM^NTS+ N TS TR+ W) TS)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP N)
   (^BM^AND (^BM^NUMBERP TS)
    (^BM^AND (^BM^NUMBERP TR+)
     (^BM^AND (^BM^NOT (^BM^ZEROP W)) (^BM^NOT (^BM^LESSP TR+ TS))))))
  (EQUAL (^BM^NTS+ N TS TR+ W)
         (IF (^BM^LESSP (^BM^PLUS TS (^BM^TIMES N W)) TR+)
             (^BM^PLUS TS (^BM^TIMES N W))
             (^BM^PLUS TS
              (^BM^TIMES W (^BM^QUOTIENT (^BM^DIFFERENCE TR+ TS) W)))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP X)
   (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
    (^BM^AND (^BM^NUMBERP R)
     (^BM^AND (^BM^NOT (^BM^NENDP N TS (^BM^PLUS R (^BM^PLUS TS X)) W))
      (^BM^AND (^BM^NUMBERP N)
       (^BM^AND (^BM^NUMBERP TS)
        (^BM^AND (^BM^NUMBERP W)
         (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
          (^BM^AND (^BM^NOT (^BM^LESSP (^BM^PLUS TS X) TS))
           (^BM^LESSP (^BM^PLUS TS X) (^BM^PLUS TS W)))))))))))
  (EQUAL (^BM^ADD1
          (^BM^QUOTIENT
           (^BM^DIFFERENCE
            (^BM^TIMES W (^BM^NLST+ N TS (^BM^PLUS R (^BM^PLUS TS X)) W))
            (^BM^DIFFERENCE (^BM^PLUS R (^BM^PLUS TS X))
             (^BM^NTS+ N TS (^BM^PLUS R (^BM^PLUS TS X)) W)))
           R))
         (^BM^QUOTIENT (^BM^DIFFERENCE (^BM^TIMES N W) X) R))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NENDP N TS (^BM^PLUS R TR) W)
   (^BM^AND (^BM^NUMBERP N)
    (^BM^AND (^BM^NUMBERP TS)
     (^BM^AND (^BM^NUMBERP TR)
      (^BM^AND (^BM^NUMBERP W)
       (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
        (^BM^AND (^BM^NUMBERP R)
         (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
          (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
           (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
            (^BM^NOT
             (^BM^LESSP (^BM^TIMES N W) (^BM^DIFFERENCE TR TS)))))))))))))
  (EQUAL (^BM^LESSP (^BM^DIFFERENCE (^BM^TIMES N W) (^BM^DIFFERENCE TR TS)) R)
         (^BM^TRUE))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP N)
   (^BM^AND (^BM^NUMBERP TS)
    (^BM^AND (^BM^NUMBERP TR)
     (^BM^AND (^BM^NOT (^BM^ZEROP W))
      (^BM^AND (^BM^NOT (^BM^ZEROP R))
       (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
        (^BM^LESSP TR (^BM^PLUS TS W))))))))
  (EQUAL (^BM^N* N TS TR W R)
         (^BM^QUOTIENT (^BM^DIFFERENCE (^BM^TIMES N W) (^BM^DIFFERENCE TR TS))
          R))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP N)
   (^BM^AND (^BM^NUMBERP TS)
    (^BM^AND (^BM^NUMBERP TR)
     (^BM^AND (^BM^NOT (^BM^ZEROP W))
      (^BM^AND (^BM^NOT (^BM^ZEROP R))
       (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
        (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
         (^BM^AND (^BM^RATE-PROXIMITY W R)
          (^BM^LESSP N
           (^INT (^BM^CONS (^1) (^BM^CONS (^8) (^BM^ZERO)))))))))))))
  (^BM^NOT (^BM^LESSP N (^BM^N* N TS TR W R)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP N)
   (^BM^AND (^BM^NUMBERP TS)
    (^BM^AND (^BM^NUMBERP TR)
     (^BM^AND (^BM^NOT (^BM^ZEROP W))
      (^BM^AND (^BM^NOT (^BM^ZEROP R))
       (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
        (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
         (^BM^AND (^BM^RATE-PROXIMITY W R)
          (^BM^LESSP N
           (^INT (^BM^CONS (^1) (^BM^CONS (^8) (^BM^ZERO)))))))))))))
  (^BM^NOT (^BM^LESSP (^BM^N* N TS TR W R) (^BM^SUB1 (^BM^SUB1 N))))))

(LEMMA (EQUAL (^BM^LEN (^BM^DET LST ORACLE)) (^BM^LEN LST)))

(DEFINE (^BM^DET-LISTN-HINT NQ ORACLE)
 (IF (^BM^ZEROP NQ)
     (^BM^TRUE)
     (^BM^DET-LISTN-HINT (^BM^SUB1 NQ) (^BM^CDR ORACLE))))

(DEFINE (^BM^NO FLG NQ ORACLE)
 (IF (^BM^ZEROP NQ)
     (^INT (^BM^ZERO))
     (IF (^BM^B-XOR FLG (^BM^CAR ORACLE))
         NQ
         (^BM^NO FLG (^BM^SUB1 NQ) (^BM^CDR ORACLE)))))

(LEMMA
 (^BM^IMPLIES (^BM^NUMBERP NQ)
  (EQUAL (^BM^NO FLG NQ ORACLE)
         (^BM^LEN
          (^BM^SCAN FLG
           (^BM^DET (^BM^LISTN NQ (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
            ORACLE))))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^LESSP (^INT (^BM^ZERO)) N) (^BM^B-XOR FLG1 FLG2))
  (EQUAL (^BM^SCAN FLG1 (^BM^APP (^BM^LISTN N FLG2) REST))
         (^BM^APP (^BM^LISTN N FLG2) REST))))

(DEFINE (^BM^SCAN-ORACLE FLG NQ ORACLE)
 (IF (^BM^ZEROP NQ)
     ORACLE
     (IF (^BM^B-XOR FLG (^BM^CAR ORACLE))
         ORACLE
         (^BM^SCAN-ORACLE FLG (^BM^SUB1 NQ) (^BM^CDR ORACLE)))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^LESSP (^INT (^BM^ZERO)) N) (^BM^B-XOR FLG1 FLG2))
  (EQUAL (^BM^SCAN FLG1
          (^BM^APP
           (^BM^DET (^BM^LISTN NQ (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
            ORACLE)
           (^BM^APP (^BM^LISTN N FLG2) REST)))
         (^BM^APP
          (^BM^DET
           (^BM^LISTN (^BM^NO FLG1 NQ ORACLE)
            (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
           (^BM^SCAN-ORACLE FLG1 NQ ORACLE))
          (^BM^APP (^BM^LISTN N FLG2) REST)))))

(LEMMA
 (EQUAL (^BM^CDRN N (^BM^APP A B))
        (IF (^BM^LESSP N (^BM^LEN A))
            (^BM^APP (^BM^CDRN N A) B)
            (^BM^CDRN (^BM^DIFFERENCE N (^BM^LEN A)) B))))

(LEMMA (^BM^NOT (^BM^LESSP N (^BM^NO FLG N ORACLE))))

(LEMMA
 (^BM^IMPLIES (^BM^BOOLP FLG)
  (EQUAL (^BM^DET (^BM^LISTN N FLG) ORACLE) (^BM^LISTN N FLG))))

(LEMMA
 (EQUAL (^BM^LEN (^BM^WARP LST TS TR W R)) (^BM^N* (^BM^LEN LST) TS TR W R)))

(LEMMA
 (EQUAL (^BM^LEN
         (^BM^WARP (^BM^LISTN (^BM^DIFFERENCE J DWG) (^BM^FALSE)) TS TR W R))
        (^BM^N* (^BM^DIFFERENCE J DWG) TS TR W R)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP TS)
   (^BM^AND (^BM^NUMBERP TR)
    (^BM^AND (^BM^NOT (^BM^ZEROP W))
     (^BM^AND (^BM^NOT (^BM^ZEROP R))
      (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
       (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
        (^BM^AND (^BM^LESSP W (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) R))
         (^BM^AND (^BM^LESSP R (^BM^TIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) W))
          (^BM^AND (^BM^LESSP (^INT (^BM^CONS (^2) (^BM^ZERO))) J)
           (^BM^AND (^BM^NUMBERP I) (^BM^NUMBERP J)))))))))))
  (EQUAL (^BM^PLUS (^BM^N* I TS TR W R)
          (^BM^PLUS
           (^BM^NQG (^BM^NLST* I TS TR W R) (^BM^NTS* I TS TR W R)
            (^BM^NTR* I TS TR W R) W R)
           (^BM^N*
            (^BM^DIFFERENCE J
             (^BM^DWG (^BM^NLST* I TS TR W R) (^BM^NTS* I TS TR W R)
              (^BM^NTR* I TS TR W R) W R))
            (^BM^TSG (^BM^NLST* I TS TR W R) (^BM^NTS* I TS TR W R)
             (^BM^NTR* I TS TR W R) W R)
            (^BM^TRG (^BM^NLST* I TS TR W R) (^BM^NTS* I TS TR W R)
             (^BM^NTR* I TS TR W R) W R)
            W R)))
         (^BM^N* (^BM^ADD1 (^BM^PLUS I J)) TS TR W R))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^LISTP MSG)
   (^BM^AND (^BM^BOOLP (^BM^CAR MSG))
    (^BM^AND (^BM^BVP (^BM^CDR MSG))
     (^BM^AND (^BM^NUMBERP TS)
      (^BM^AND (^BM^NUMBERP TR)
       (^BM^AND (^BM^NOT (^BM^ZEROP W))
        (^BM^AND (^BM^NOT (^BM^ZEROP R))
         (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
          (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
           (^BM^AND (^BM^RATE-PROXIMITY W R)
            (^BM^AND (^BM^NUMBERP NQ)
             (^BM^AND
              (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^3) (^BM^ZERO))) NQ))
              (^BM^AND (^BM^NUMBERP DW)
               (^BM^AND
                (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) DW))
                (^BM^AND (^BM^BOOLP FLG1) (^BM^B-XOR FLG1 FLG2))))))))))))))))
  (EQUAL (^BM^CDRN (^INT (^BM^CONS (^1) (^BM^CONS (^0) (^BM^ZERO))))
          (^BM^SCAN FLG1
           (^BM^APP
            (^BM^DET (^BM^LISTN NQ (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
             ORACLE1)
            (^BM^APP
             (^BM^DET
              (^BM^WARP
               (^BM^SMOOTH FLG2
                (^BM^CELL FLG1
                 (^BM^DIFFERENCE (^INT (^BM^CONS (^4) (^BM^ZERO))) DW)
                 (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO))))
                 (^BM^CAR MSG)))
               TS TR W R)
              ORACLE2)
             REST))))
         (^BM^APP
          (^BM^LISTN
           (^BM^DIFFERENCE
            (^BM^PLUS (^BM^NO FLG1 NQ ORACLE1)
             (^BM^N*
              (^BM^DIFFERENCE (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO))))
               DW)
              TS TR W R))
            (^INT (^BM^CONS (^1) (^BM^CONS (^0) (^BM^ZERO)))))
           (^BM^CSIG FLG1 (^BM^CAR MSG)))
          REST))))

(LEMMA
 (EQUAL (^BM^CAR
         (^BM^DET (^BM^LISTN N (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO)))) ORACLE))
        (IF (^BM^ZEROP N)
            (^INT (^BM^ZERO))
            (IF (^BM^CAR ORACLE) (^BM^TRUE) (^BM^FALSE)))))

(LEMMA (EQUAL (^BM^LISTP (^BM^DET LST ORACLE)) (^BM^LISTP LST)))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP (^BM^NO FLG NQ ORACLE)))
  (^BM^IFF (^BM^CAR (^BM^SCAN-ORACLE FLG NQ ORACLE)) (^BM^B-NOT FLG))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^LISTP MSG)
   (^BM^AND (^BM^BOOLP (^BM^CAR MSG))
    (^BM^AND (^BM^BVP (^BM^CDR MSG))
     (^BM^AND (^BM^NUMBERP TS)
      (^BM^AND (^BM^NUMBERP TR)
       (^BM^AND (^BM^NOT (^BM^ZEROP W))
        (^BM^AND (^BM^NOT (^BM^ZEROP R))
         (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
          (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
           (^BM^AND (^BM^RATE-PROXIMITY W R)
            (^BM^AND (^BM^NUMBERP NQ)
             (^BM^AND
              (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^3) (^BM^ZERO))) NQ))
              (^BM^AND (^BM^NUMBERP DW)
               (^BM^AND
                (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) DW))
                (^BM^AND (^BM^BOOLP FLG1)
                 (^BM^AND (^BM^BOOLP FLG2)
                  (^BM^B-XOR FLG1 FLG2)))))))))))))))))
  (EQUAL (^BM^CAR
          (^BM^SCAN FLG1
           (^BM^APP
            (^BM^DET (^BM^LISTN NQ (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
             ORACLE1)
            (^BM^APP
             (^BM^DET
              (^BM^WARP
               (^BM^SMOOTH FLG2
                (^BM^CELL FLG1
                 (^BM^DIFFERENCE (^INT (^BM^CONS (^4) (^BM^ZERO))) DW)
                 (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO))))
                 (^BM^CAR MSG)))
               TS TR W R)
              ORACLE)
             REST))))
         (^BM^B-NOT FLG1))))

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

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^LISTP MSG)
   (^BM^AND (^BM^BOOLP (^BM^CAR MSG))
    (^BM^AND (^BM^BVP (^BM^CDR MSG))
     (^BM^AND (^BM^NUMBERP TS)
      (^BM^AND (^BM^NUMBERP TR)
       (^BM^AND (^BM^NOT (^BM^ZEROP W))
        (^BM^AND (^BM^NOT (^BM^ZEROP R))
         (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
          (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
           (^BM^AND (^BM^RATE-PROXIMITY W R)
            (^BM^AND (^BM^NUMBERP NQ)
             (^BM^AND
              (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^3) (^BM^ZERO))) NQ))
              (^BM^AND (^BM^NUMBERP DW)
               (^BM^AND
                (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) DW))
                (^BM^AND (^BM^BOOLP FLG1)
                 (^BM^AND (^BM^BOOLP FLG2)
                  (^BM^B-XOR FLG1 FLG2)))))))))))))))))
  (EQUAL (^BM^RECV-BIT (^INT (^BM^CONS (^1) (^BM^CONS (^0) (^BM^ZERO))))
          (^BM^SCAN FLG1
           (^BM^APP
            (^BM^DET (^BM^LISTN NQ (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
             ORACLE1)
            (^BM^APP
             (^BM^DET
              (^BM^WARP
               (^BM^SMOOTH FLG2
                (^BM^CELL FLG1
                 (^BM^DIFFERENCE (^INT (^BM^CONS (^4) (^BM^ZERO))) DW)
                 (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO))))
                 (^BM^CAR MSG)))
               TS TR W R)
              ORACLE)
             REST))))
         (^BM^CAR MSG))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^LISTP MSG)
   (^BM^AND (^BM^BOOLP (^BM^CAR MSG))
    (^BM^AND (^BM^BVP (^BM^CDR MSG))
     (^BM^AND (^BM^NUMBERP TS)
      (^BM^AND (^BM^NUMBERP TR)
       (^BM^AND (^BM^NOT (^BM^ZEROP W))
        (^BM^AND (^BM^NOT (^BM^ZEROP R))
         (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
          (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
           (^BM^AND (^BM^RATE-PROXIMITY W R)
            (^BM^AND (^BM^NUMBERP NQ)
             (^BM^AND
              (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^3) (^BM^ZERO))) NQ))
              (^BM^AND (^BM^NUMBERP DW)
               (^BM^NOT
                (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) DW)))))))))))))))
  (EQUAL (^BM^CAR
          (^BM^APP
           (^BM^LISTN
            (^BM^DIFFERENCE
             (^BM^PLUS (^BM^NO FLG1 NQ ORACLE1)
              (^BM^N*
               (^BM^DIFFERENCE
                (^INT (^BM^CONS (^1) (^BM^CONS (^7) (^BM^ZERO)))) DW)
               TS TR W R))
             (^INT (^BM^CONS (^1) (^BM^CONS (^0) (^BM^ZERO)))))
            (^BM^CSIG FLG1 (^BM^CAR MSG)))
           REST))
         (^BM^CSIG FLG1 (^BM^CAR MSG)))))

(LEMMA
 (EQUAL (^BM^RECV N FLG K (^BM^APP (^BM^LISTN M FLG) REST))
        (^BM^RECV N FLG K REST)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^LISTP MSG)
   (^BM^AND (^BM^BOOLP (^BM^CAR MSG))
    (^BM^AND (^BM^BVP (^BM^CDR MSG))
     (^BM^AND (^BM^NUMBERP TS)
      (^BM^AND (^BM^NUMBERP TR)
       (^BM^AND (^BM^NOT (^BM^ZEROP W))
        (^BM^AND (^BM^NOT (^BM^ZEROP R))
         (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
          (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
           (^BM^AND (^BM^RATE-PROXIMITY W R)
            (^BM^AND (^BM^NUMBERP NQ)
             (^BM^AND
              (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^3) (^BM^ZERO))) NQ))
              (^BM^AND (^BM^NUMBERP DW)
               (^BM^AND
                (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) DW))
                (^BM^AND (^BM^BOOLP FLG1)
                 (^BM^AND (^BM^BOOLP FLG2)
                  (^BM^B-XOR FLG1 FLG2)))))))))))))))))
  (EQUAL (^BM^RECV (^BM^LEN MSG) FLG1
          (^INT (^BM^CONS (^1) (^BM^CONS (^0) (^BM^ZERO))))
          (^BM^APP
           (^BM^DET (^BM^LISTN NQ (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
            ORACLE1)
           (^BM^APP
            (^BM^DET
             (^BM^WARP
              (^BM^SMOOTH FLG2
               (^BM^CELL FLG1
                (^BM^DIFFERENCE (^INT (^BM^CONS (^4) (^BM^ZERO))) DW)
                (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO))))
                (^BM^CAR MSG)))
              TS TR W R)
             ORACLE)
            REST)))
         (^BM^CONS (^BM^CAR MSG)
          (^BM^RECV (^BM^LEN (^BM^CDR MSG)) (^BM^CSIG FLG1 (^BM^CAR MSG))
           (^INT (^BM^CONS (^1) (^BM^CONS (^0) (^BM^ZERO)))) REST)))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^ZEROP M))
  (EQUAL (^BM^CDR (^BM^APP (^BM^CELL FLG1 M N BIT) REST))
         (^BM^APP (^BM^CELL FLG1 (^BM^SUB1 M) N BIT) REST))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^NOT (^BM^ZEROP N)) (^BM^B-XOR FLG2 FLG1))
  (EQUAL (^BM^SMOOTH FLG2 (^BM^APP (^BM^CELL FLG1 M N BIT) REST))
         (^BM^APP (^BM^SMOOTH FLG2 (^BM^CELL FLG1 M N BIT))
          (^BM^SMOOTH (^BM^CSIG FLG1 BIT) REST)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^LISTP MSG)
   (^BM^AND (^BM^BOOLP (^BM^CAR MSG))
    (^BM^AND (EQUAL (^BM^CDR MSG) (^NIL))
     (^BM^AND (^BM^NUMBERP TS)
      (^BM^AND (^BM^NUMBERP TR)
       (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
        (^BM^AND (^BM^NUMBERP W)
         (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
          (^BM^AND (^BM^NUMBERP R)
           (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
            (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
             (^BM^AND (^BM^RATE-PROXIMITY W R)
              (^BM^AND (^BM^NUMBERP NQ)
               (^BM^AND
                (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^3) (^BM^ZERO))) NQ))
                (^BM^AND (^BM^NUMBERP DW)
                 (^BM^AND
                  (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) DW))
                  (^BM^AND (^BM^BOOLP FLG1)
                   (^BM^AND (^BM^BOOLP FLG2)
                    (^BM^B-XOR FLG1 FLG2)))))))))))))))))))
  (EQUAL (^BM^RECV (^BM^LEN MSG) FLG1
          (^INT (^BM^CONS (^1) (^BM^CONS (^0) (^BM^ZERO))))
          (^BM^APP
           (^BM^DET (^BM^LISTN NQ (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
            ORACLE1)
           (^BM^DET
            (^BM^TARGET
             (^BM^WARP
              (^BM^CDRN DW
               (^BM^SMOOTH FLG2
                (^BM^APP
                 (^BM^CDR
                  (^BM^CELLS FLG1 (^INT (^BM^CONS (^5) (^BM^ZERO)))
                   (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO)))) MSG))
                 (^BM^LISTN P2 (^BM^TRUE)))))
              TS TR W R))
            ORACLE2)))
         MSG)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^LISTP MSG)
   (^BM^AND (^BM^BOOLP (^BM^CAR MSG))
    (^BM^AND (EQUAL (^BM^CDR MSG) (^NIL))
     (^BM^AND (^BM^NUMBERP TS)
      (^BM^AND (^BM^NUMBERP TR)
       (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
        (^BM^AND (^BM^NUMBERP W)
         (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
          (^BM^AND (^BM^NUMBERP R)
           (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
            (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
             (^BM^AND (^BM^RATE-PROXIMITY W R)
              (^BM^AND (^BM^NUMBERP NQ)
               (^BM^AND
                (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^3) (^BM^ZERO))) NQ))
                (^BM^AND (^BM^NUMBERP DW)
                 (^BM^AND
                  (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) DW))
                  (^BM^AND (^BM^BOOLP FLG1)
                   (^BM^AND (^BM^BOOLP FLG2)
                    (^BM^B-XOR FLG1 FLG2)))))))))))))))))))
  (EQUAL (^BM^RECV (^BM^LEN MSG) FLG1
          (^INT (^BM^CONS (^1) (^BM^CONS (^0) (^BM^ZERO))))
          (^BM^APP
           (^BM^DET (^BM^LISTN NQ (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
            ORACLE1)
           (^BM^DET
            (^BM^WARP
             (^BM^CDRN DW
              (^BM^SMOOTH FLG2
               (^BM^APP
                (^BM^CDR
                 (^BM^CELLS FLG1 (^INT (^BM^CONS (^5) (^BM^ZERO)))
                  (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO)))) MSG))
                (^BM^LISTN P2 (^BM^TRUE)))))
             TS TR W R)
            ORACLE2)))
         MSG)))

(LEMMA (^BM^BOOLP (^BM^B-NOT X)))

(LEMMA (^BM^IMPLIES (^BM^BOOLP FLG) (^BM^BOOLP (^BM^CSIG FLG BIT))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^BVP MSG)
   (^BM^AND (^BM^NUMBERP TS)
    (^BM^AND (^BM^NUMBERP TR)
     (^BM^AND (^BM^NOT (^BM^ZEROP W))
      (^BM^AND (^BM^NOT (^BM^ZEROP R))
       (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
        (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
         (^BM^AND (^BM^RATE-PROXIMITY W R)
          (^BM^AND (^BM^NUMBERP NQ)
           (^BM^AND (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^3) (^BM^ZERO))) NQ))
            (^BM^AND (^BM^NUMBERP DW)
             (^BM^AND
              (^BM^NOT (^BM^LESSP (^INT (^BM^CONS (^1) (^BM^ZERO))) DW))
              (^BM^AND (^BM^BOOLP FLG1)
               (^BM^AND (^BM^BOOLP FLG2) (^BM^B-XOR FLG1 FLG2)))))))))))))))
  (EQUAL (^BM^RECV (^BM^LEN MSG) FLG1
          (^INT (^BM^CONS (^1) (^BM^CONS (^0) (^BM^ZERO))))
          (^BM^APP
           (^BM^DET (^BM^LISTN NQ (^BM^PACK (^BM^CONS (^Q) (^BM^ZERO))))
            ORACLE1)
           (^BM^DET
            (^BM^WARP
             (^BM^CDRN DW
              (^BM^SMOOTH FLG2
               (^BM^APP
                (^BM^CDR
                 (^BM^CELLS FLG1 (^INT (^BM^CONS (^5) (^BM^ZERO)))
                  (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO)))) MSG))
                (^BM^LISTN P2 (^BM^TRUE)))))
             TS TR W R)
            ORACLE2)))
         MSG)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^BVP MSG)
   (^BM^AND (^BM^NUMBERP TS)
    (^BM^AND (^BM^NUMBERP TR)
     (^BM^AND (^BM^NOT (^BM^ZEROP W))
      (^BM^AND (^BM^NOT (^BM^ZEROP R))
       (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
        (^BM^AND (^BM^LESSP TR (^BM^PLUS TS W))
         (^BM^AND (^BM^RATE-PROXIMITY W R) (^BM^NUMBERP P1)))))))))
  (EQUAL (^BM^RECV (^BM^LEN MSG) (^BM^TRUE)
          (^INT (^BM^CONS (^1) (^BM^CONS (^0) (^BM^ZERO))))
          (^BM^ASYNC
           (^BM^SEND MSG P1 (^INT (^BM^CONS (^5) (^BM^ZERO)))
            (^INT (^BM^CONS (^1) (^BM^CONS (^3) (^BM^ZERO)))) P2)
           TS TR W R ORACLE))
         MSG)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP X)
   (^BM^AND (EQUAL (^BM^TIMES N W) (^BM^PLUS R X))
    (^BM^AND (^BM^NUMBERP N)
     (^BM^AND (^BM^NUMBERP TS)
      (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
       (^BM^AND (^BM^NUMBERP W)
        (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO)))) (^BM^NUMBERP R))))))))
  (^BM^NOT (^BM^NENDP N TS (^BM^PLUS R (^BM^PLUS TS X)) W))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP X)
   (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
    (^BM^AND (^BM^NUMBERP R)
     (^BM^AND (^BM^NOT (^BM^NENDP N TS (^BM^PLUS R (^BM^PLUS TS X)) W))
      (^BM^AND (^BM^NUMBERP N)
       (^BM^AND (^BM^NUMBERP TS)
        (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
         (^BM^AND (^BM^NUMBERP W)
          (^BM^AND (^BM^NOT (^BM^LESSP (^BM^PLUS TS X) TS))
           (^BM^LESSP (^BM^PLUS TS X) (^BM^PLUS TS W)))))))))))
  (EQUAL (^BM^PLUS (^BM^NTS+ N TS (^BM^PLUS R (^BM^PLUS TS X)) W)
          (^BM^TIMES W
           (^BM^QUOTIENT
            (^BM^DIFFERENCE
             (^BM^PLUS R
              (^BM^PLUS TS
               (^BM^PLUS X
                (^BM^TIMES R
                 (^BM^QUOTIENT
                  (^BM^DIFFERENCE
                   (^BM^TIMES W
                    (^BM^NLST+ N TS (^BM^PLUS R (^BM^PLUS TS X)) W))
                   (^BM^DIFFERENCE (^BM^PLUS R (^BM^PLUS TS X))
                    (^BM^NTS+ N TS (^BM^PLUS R (^BM^PLUS TS X)) W)))
                  R)))))
             (^BM^NTS+ N TS (^BM^PLUS R (^BM^PLUS TS X)) W))
            W)))
         (^BM^PLUS TS
          (^BM^TIMES W
           (^BM^QUOTIENT
            (^BM^PLUS X
             (^BM^TIMES R (^BM^QUOTIENT (^BM^DIFFERENCE (^BM^TIMES N W) X) R)))
            W))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP N)
   (^BM^AND (^BM^NUMBERP TS)
    (^BM^AND (^BM^NUMBERP TR)
     (^BM^AND (^BM^NOT (^BM^ZEROP W))
      (^BM^AND (^BM^NOT (^BM^ZEROP R))
       (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
        (^BM^LESSP TR (^BM^PLUS TS W))))))))
  (EQUAL (^BM^NTS* N TS TR W R)
         (^BM^PLUS TS
          (^BM^TIMES W
           (^BM^QUOTIENT
            (^BM^DIFFERENCE
             (^BM^PLUS TR
              (^BM^TIMES R
               (^BM^QUOTIENT
                (^BM^DIFFERENCE (^BM^TIMES N W) (^BM^DIFFERENCE TR TS)) R)))
             TS)
            W))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP X)
   (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
    (^BM^AND (^BM^NUMBERP R)
     (^BM^AND (^BM^NOT (^BM^NENDP N TS (^BM^PLUS R (^BM^PLUS TS X)) W))
      (^BM^AND (^BM^NUMBERP N)
       (^BM^AND (^BM^NUMBERP TS)
        (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
         (^BM^AND (^BM^NUMBERP W)
          (^BM^AND (^BM^NOT (^BM^LESSP (^BM^PLUS TS X) TS))
           (^BM^LESSP (^BM^PLUS TS X) (^BM^PLUS TS W)))))))))))
  (EQUAL (^BM^PLUS R
          (^BM^PLUS TS
           (^BM^PLUS X
            (^BM^TIMES R
             (^BM^QUOTIENT
              (^BM^DIFFERENCE
               (^BM^TIMES W (^BM^NLST+ N TS (^BM^PLUS R (^BM^PLUS TS X)) W))
               (^BM^DIFFERENCE (^BM^PLUS R (^BM^PLUS TS X))
                (^BM^NTS+ N TS (^BM^PLUS R (^BM^PLUS TS X)) W)))
              R)))))
         (^BM^PLUS TS
          (^BM^PLUS X
           (^BM^TIMES R
            (^BM^QUOTIENT (^BM^DIFFERENCE (^BM^TIMES N W) X) R)))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP N)
   (^BM^AND (^BM^NUMBERP TS)
    (^BM^AND (^BM^NUMBERP TR)
     (^BM^AND (^BM^NOT (^BM^ZEROP W))
      (^BM^AND (^BM^NOT (^BM^ZEROP R))
       (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
        (^BM^LESSP TR (^BM^PLUS TS W))))))))
  (EQUAL (^BM^NTR* N TS TR W R)
         (^BM^PLUS TR
          (^BM^TIMES R
           (^BM^QUOTIENT
            (^BM^DIFFERENCE (^BM^TIMES N W) (^BM^DIFFERENCE TR TS)) R))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP X)
   (^BM^AND (^BM^NOT (EQUAL R (^INT (^BM^ZERO))))
    (^BM^AND (^BM^NUMBERP R)
     (^BM^AND (^BM^NOT (^BM^NENDP N TS (^BM^PLUS R (^BM^PLUS TS X)) W))
      (^BM^AND (^BM^NUMBERP N)
       (^BM^AND (^BM^NUMBERP TS)
        (^BM^AND (^BM^NOT (EQUAL W (^INT (^BM^ZERO))))
         (^BM^AND (^BM^NUMBERP W)
          (^BM^AND (^BM^NOT (^BM^LESSP (^BM^PLUS TS X) TS))
           (^BM^LESSP (^BM^PLUS TS X) (^BM^PLUS TS W)))))))))))
  (EQUAL (^BM^DIFFERENCE (^BM^NLST+ N TS (^BM^PLUS R (^BM^PLUS TS X)) W)
          (^BM^QUOTIENT
           (^BM^DIFFERENCE
            (^BM^PLUS TS
             (^BM^PLUS X
              (^BM^TIMES R
               (^BM^QUOTIENT (^BM^DIFFERENCE (^BM^TIMES N W) X) R))))
            (^BM^NTS+ N TS (^BM^PLUS R (^BM^PLUS TS X)) W))
           W))
         (^BM^DIFFERENCE N
          (^BM^QUOTIENT
           (^BM^PLUS X
            (^BM^TIMES R (^BM^QUOTIENT (^BM^DIFFERENCE (^BM^TIMES N W) X) R)))
           W)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP N)
   (^BM^AND (^BM^NUMBERP TS)
    (^BM^AND (^BM^NUMBERP TR)
     (^BM^AND (^BM^NOT (^BM^ZEROP W))
      (^BM^AND (^BM^NOT (^BM^ZEROP R))
       (^BM^AND (^BM^NOT (^BM^LESSP TR TS))
        (^BM^LESSP TR (^BM^PLUS TS W))))))))
  (EQUAL (^BM^NLST* N TS TR W R)
         (^BM^DIFFERENCE N
          (^BM^QUOTIENT
           (^BM^DIFFERENCE
            (^BM^PLUS TR
             (^BM^TIMES R
              (^BM^QUOTIENT
               (^BM^DIFFERENCE (^BM^TIMES N W) (^BM^DIFFERENCE TR TS)) R)))
            TS)
           W)))))

(DEFINE (^BM^XP X)
 (IF (CONSP X) (IF (EQUAL (CAR X) '^BM^X) (EQUAL (CDR X) 'NIL) 'FALSE) 'FALSE))

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

(DEFINE (^BM^F-NOT A) (IF (^BM^BOOLP A) (^BM^NOT A) (^BM^X)))

(DEFINE (^BM^F-AND A B)
 (IF (^BM^OR (EQUAL A (^BM^FALSE)) (EQUAL B (^BM^FALSE)))
     (^BM^FALSE)
     (IF (^BM^AND (EQUAL A (^BM^TRUE)) (EQUAL B (^BM^TRUE)))
         (^BM^TRUE)
         (^BM^X))))

(DEFINE (^BM^EXPRP X)
 (IF (^BM^NLISTP X)
     (^BM^OR (EQUAL X (^BM^PACK (^BM^CONS (^T) (^BM^ZERO))))
      (^BM^OR (EQUAL X (^BM^PACK (^BM^CONS (^F) (^BM^ZERO)))) (^BM^NUMBERP X)))
     (IF (EQUAL (^BM^CAR X)
                (^BM^PACK
                 (^BM^CONS (^F)
                  (^BM^CONS (^-)
                   (^BM^CONS (^N)
                    (^BM^CONS (^O) (^BM^CONS (^T) (^BM^ZERO))))))))
         (^BM^AND (^BM^EXPRP (^BM^CAR (^BM^CDR X)))
          (EQUAL (^BM^CDR (^BM^CDR X)) (^NIL)))
         (^BM^AND
          (EQUAL (^BM^CAR X)
                 (^BM^PACK
                  (^BM^CONS (^F)
                   (^BM^CONS (^-)
                    (^BM^CONS (^A)
                     (^BM^CONS (^N) (^BM^CONS (^D) (^BM^ZERO))))))))
          (^BM^AND (^BM^EXPRP (^BM^CAR (^BM^CDR X)))
           (^BM^AND (^BM^EXPRP (^BM^CAR (^BM^CDR (^BM^CDR X))))
            (EQUAL (^BM^CDR (^BM^CDR (^BM^CDR X))) (^NIL))))))))

(DEFINE (^BM^MAX-VAR X)
 (IF (^BM^NLISTP X)
     (IF (^BM^OR (EQUAL X (^BM^PACK (^BM^CONS (^T) (^BM^ZERO))))
          (EQUAL X (^BM^PACK (^BM^CONS (^F) (^BM^ZERO)))))
         (^INT (^BM^ZERO))
         X)
     (IF (EQUAL (^BM^CAR X)
                (^BM^PACK
                 (^BM^CONS (^F)
                  (^BM^CONS (^-)
                   (^BM^CONS (^N)
                    (^BM^CONS (^O) (^BM^CONS (^T) (^BM^ZERO))))))))
         (^BM^MAX-VAR (^BM^CAR (^BM^CDR X)))
         (^BM^MAX (^BM^MAX-VAR (^BM^CAR (^BM^CDR X)))
          (^BM^MAX-VAR (^BM^CAR (^BM^CDR (^BM^CDR X))))))))

(DEFINE (^BM^WIDTH X) (^BM^ADD1 (^BM^MAX-VAR X)))

(DEFINE (^BM^VAR-VAL N VECTOR)
 (IF (^BM^BOOLP (^BM^NTH N VECTOR)) (^BM^NTH N VECTOR) (^BM^X)))

(DEFINE (^BM^VAL X VECTOR)
 (IF (^BM^NLISTP X)
     (IF (EQUAL X (^BM^PACK (^BM^CONS (^T) (^BM^ZERO))))
         (^BM^TRUE)
         (IF (EQUAL X (^BM^PACK (^BM^CONS (^F) (^BM^ZERO))))
             (^BM^FALSE)
             (^BM^VAR-VAL X VECTOR)))
     (IF (EQUAL (^BM^CAR X)
                (^BM^PACK
                 (^BM^CONS (^F)
                  (^BM^CONS (^-)
                   (^BM^CONS (^N)
                    (^BM^CONS (^O) (^BM^CONS (^T) (^BM^ZERO))))))))
         (^BM^F-NOT (^BM^VAL (^BM^CAR (^BM^CDR X)) VECTOR))
         (^BM^F-AND (^BM^VAL (^BM^CAR (^BM^CDR X)) VECTOR)
          (^BM^VAL (^BM^CAR (^BM^CDR (^BM^CDR X))) VECTOR)))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (EQUAL (^BM^VAR-VAL X VECTOR) (^BM^X)))
  (^BM^BOOLP (^BM^VAR-VAL X VECTOR))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (EQUAL (^BM^VAL X VECTOR) (^BM^X)))
  (^BM^BOOLP (^BM^VAL X VECTOR))))

(DEFINE (^BM^EDGE K I)
 (IF (^BM^ZEROP K)
     (^NIL)
     (IF (^BM^LESSP I K)
         (^BM^APP (^BM^EDGE (^BM^SUB1 K) I) (^BM^CONS (^BM^FALSE) (^NIL)))
         (IF (EQUAL I K)
             (^BM^APP (^BM^EDGE (^BM^SUB1 K) I) (^BM^CONS (^BM^X) (^NIL)))
             (^BM^APP (^BM^EDGE (^BM^SUB1 K) (^BM^SUB1 I))
              (^BM^CONS (^BM^TRUE) (^NIL)))))))

(LEMMA (EQUAL (^BM^LEN (^BM^EDGE K I)) (^BM^FIX K)))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^LESSP N (^BM^LEN LST)))
  (^BM^NOT (^BM^LISTP (^BM^CDRN N LST)))))

(LEMMA (EQUAL (^BM^LESSP N (^INT (^BM^CONS (^1) (^BM^ZERO)))) (^BM^ZEROP N)))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP N) (^BM^AND (^BM^NUMBERP K) (^BM^NOT (^BM^ZEROP K))))
  (EQUAL (^BM^CAR (^BM^CDRN N (^BM^EDGE K I)))
         (IF (^BM^LESSP N K)
             (IF (^BM^LESSP (^BM^ADD1 N) I)
                 (^BM^TRUE)
                 (IF (EQUAL (^BM^ADD1 N) I) (^BM^X) (^BM^FALSE)))
             (^INT (^BM^ZERO))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NUMBERP N)
   (^BM^AND (^BM^NUMBERP K) (^BM^AND (^BM^NOT (^BM^ZEROP K)) (^BM^LESSP N K))))
  (EQUAL (^BM^VAR-VAL N (^BM^EDGE K I))
         (IF (^BM^LESSP N K)
             (IF (^BM^LESSP (^BM^ADD1 N) I)
                 (^BM^TRUE)
                 (IF (EQUAL (^BM^ADD1 N) I) (^BM^X) (^BM^FALSE)))
             (^BM^X)))))

(DEFINE (^BM^ALL-EDGES K I)
 (IF (^BM^ZEROP I)
     (^BM^CONS (^BM^EDGE K (^INT (^BM^ZERO))) (^NIL))
     (^BM^CONS (^BM^EDGE K I) (^BM^ALL-EDGES K (^BM^SUB1 I)))))

(DEFINE (^BM^WELL-DEFINED1 X TEST-SET)
 (IF (^BM^NLISTP TEST-SET)
     (^BM^TRUE)
     (^BM^AND (^BM^NOT (EQUAL (^BM^VAL X (^BM^CAR TEST-SET)) (^BM^X)))
      (^BM^WELL-DEFINED1 X (^BM^CDR TEST-SET)))))

(DEFINE (^BM^WELL-DEFINED X)
 (^BM^WELL-DEFINED1 X (^BM^ALL-EDGES (^BM^WIDTH X) (^BM^ADD1 (^BM^WIDTH X)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^EXPRP X)
   (^BM^AND (^BM^NOT (^BM^ZEROP I))
    (^BM^AND (^BM^NOT (^BM^LESSP K (^BM^WIDTH X)))
     (^BM^AND (^BM^NOT (EQUAL (^BM^VAL X (^BM^EDGE K I)) (^BM^X)))
      (^BM^NOT (EQUAL (^BM^VAL X (^BM^EDGE K (^BM^SUB1 I))) (^BM^X)))))))
  (EQUAL (^BM^VAL X (^BM^EDGE K I)) (^BM^VAL X (^BM^EDGE K (^BM^SUB1 I))))))

(LEMMA (^BM^IMPLIES (^BM^EXPRP X) (^BM^NUMBERP (^BM^MAX-VAR X))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^NOT (EQUAL (^BM^VAL X VECTOR) (^BM^X))) (^BM^VAL X VECTOR))
  (EQUAL (^BM^VAL X VECTOR) (^BM^TRUE))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^ZEROP ZERO)
   (^BM^AND (^BM^EXPRP X) (^BM^NOT (^BM^LESSP K (^BM^WIDTH X)))))
  (^BM^NOT (EQUAL (^BM^VAL X (^BM^EDGE K ZERO)) (^BM^X)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^EXPRP X)
   (^BM^AND (^BM^NOT (^BM^LESSP K (^BM^WIDTH X)))
    (^BM^AND (^BM^WELL-DEFINED1 X (^BM^ALL-EDGES K I))
     (^BM^NOT (^BM^LESSP I J)))))
  (^BM^NOT (EQUAL (^BM^VAL X (^BM^EDGE K J)) (^BM^X)))))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^NUMBERP I))
  (EQUAL (^BM^EDGE K I) (^BM^EDGE K (^INT (^BM^ZERO))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^EXPRP X)
   (^BM^AND (^BM^NOT (^BM^LESSP K (^BM^WIDTH X)))
    (^BM^AND (^BM^WELL-DEFINED1 X (^BM^ALL-EDGES K I))
     (^BM^NOT (^BM^LESSP I J)))))
  (EQUAL (^BM^VAL X (^BM^EDGE K J))
         (^BM^VAL X (^BM^EDGE K (^INT (^BM^ZERO)))))))

(LEMMA
 (^BM^IMPLIES (^BM^LESSP (^BM^ADD1 K) I)
  (EQUAL (^BM^EDGE K I) (^BM^EDGE K (^BM^ADD1 K)))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^EXPRP X) (^BM^WELL-DEFINED X))
  (EQUAL (^BM^VAL X (^BM^EDGE (^BM^WIDTH X) I))
         (^BM^VAL X (^BM^EDGE (^BM^WIDTH X) (^INT (^BM^ZERO)))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^EXPRP X) (^BM^NOT (EQUAL (^BM^VAL X (^NIL)) (^BM^X))))
  (EQUAL (^BM^VAL X VECTOR) (^BM^VAL X (^NIL)))))