(NOTE-LIB "fortran")

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

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

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

(DEFINE (^BM^VEHICLE-STATEP X)
 (IF (CONSP X)
     (IF (EQUAL (CAR X) '^BM^VEHICLE-STATE)
         (IF (CONSP (CDR X))
             (IF (^BM^NOT 'FALSE)
                 (IF (CONSP (CDR (CDR X)))
                     (IF (^BM^NOT 'FALSE)
                         (IF (CONSP (CDR (CDR (CDR X))))
                             (IF (^BM^NOT 'FALSE)
                                 (EQUAL (CDR (CDR (CDR (CDR X)))) 'NIL)
                                 'FALSE)
                             'FALSE)
                         'FALSE)
                     'FALSE)
                 'FALSE)
             'FALSE)
         'FALSE)
     'FALSE))

(DEFINE (^BM^VEHICLE-STATE T1607 T1608 T1609)
 (CONS '^BM^VEHICLE-STATE
       (CONS (IF (^BM^NOT 'FALSE) T1607 (^BM^ZERO))
             (CONS (IF (^BM^NOT 'FALSE) T1608 (^BM^ZERO))
                   (CONS (IF (^BM^NOT 'FALSE) T1609 (^BM^ZERO)) 'NIL)))))

(DEFINE (^BM^W X) (IF (^BM^VEHICLE-STATEP X) (CAR (CDR X)) (^BM^ZERO)))

(DEFINE (^BM^Y X) (IF (^BM^VEHICLE-STATEP X) (CAR (CDR (CDR X))) (^BM^ZERO)))

(DEFINE (^BM^V X)
 (IF (^BM^VEHICLE-STATEP X) (CAR (CDR (CDR (CDR X)))) (^BM^ZERO)))

(DEFINE (^BM^HD X) (^BM^CAR X))

(DEFINE (^BM^TL X) (^BM^CDR X))

(DEFINE (^BM^EMPTY X) (^BM^NOT (^BM^LISTP X)))

(LEMMA (EQUAL (^BM^TL X) (^BM^CDR X)))

(LEMMA
 (^BM^IMPLIES (^BM^NOT (^BM^EMPTY X))
  (^BM^LESSP (^BM^COUNT (^BM^TL X)) (^BM^COUNT X))))

(DEFINE (^BM^RANDOM-DELTA-WS LST)
 (IF (^BM^EMPTY LST)
     (^BM^TRUE)
     (^BM^AND
      (^BM^OR
       (EQUAL (^BM^HD LST) (^BM^MINUS (^INT (^BM^CONS (^1) (^BM^ZERO)))))
       (^BM^OR (EQUAL (^BM^HD LST) (^INT (^BM^ZERO)))
        (EQUAL (^BM^HD LST) (^INT (^BM^CONS (^1) (^BM^ZERO))))))
      (^BM^RANDOM-DELTA-WS (^BM^TL LST)))))

(DEFINE (^BM^CONTROLLER SGN-Y SGN-OLD-Y)
 (^BM^ZPLUS (^BM^ZTIMES (^BM^MINUS (^INT (^BM^CONS (^3) (^BM^ZERO)))) SGN-Y)
  (^BM^ZTIMES (^INT (^BM^CONS (^2) (^BM^ZERO))) SGN-OLD-Y)))

(DEFINE (^BM^SGN X)
 (IF (^BM^NEGATIVEP X)
     (IF (EQUAL (^BM^NEGATIVE-GUTS X) (^INT (^BM^ZERO)))
         (^INT (^BM^ZERO))
         (^BM^MINUS (^INT (^BM^CONS (^1) (^BM^ZERO)))))
     (IF (^BM^ZEROP X) (^INT (^BM^ZERO)) (^INT (^BM^CONS (^1) (^BM^ZERO))))))

(DEFINE (^BM^NEXT-STATE DELTA-W STATE)
 (^BM^VEHICLE-STATE (^BM^ZPLUS (^BM^W STATE) DELTA-W)
  (^BM^ZPLUS (^BM^Y STATE)
   (^BM^ZPLUS (^BM^V STATE) (^BM^ZPLUS (^BM^W STATE) DELTA-W)))
  (^BM^ZPLUS (^BM^V STATE)
   (^BM^CONTROLLER
    (^BM^SGN
     (^BM^ZPLUS (^BM^Y STATE)
      (^BM^ZPLUS (^BM^V STATE) (^BM^ZPLUS (^BM^W STATE) DELTA-W))))
    (^BM^SGN (^BM^Y STATE))))))

(DEFINE (^BM^FINAL-STATE-OF-VEHICLE DELTA-WS STATE)
 (IF (^BM^EMPTY DELTA-WS)
     STATE
     (^BM^FINAL-STATE-OF-VEHICLE (^BM^TL DELTA-WS)
      (^BM^NEXT-STATE (^BM^HD DELTA-WS) STATE))))

(DEFINE (^BM^GOOD-STATEP STATE)
 (IF (EQUAL (^BM^Y STATE) (^INT (^BM^ZERO)))
     (^BM^OR
      (EQUAL (^BM^ZPLUS (^BM^V STATE) (^BM^W STATE))
             (^BM^MINUS (^INT (^BM^CONS (^1) (^BM^ZERO)))))
      (^BM^OR (EQUAL (^BM^ZPLUS (^BM^V STATE) (^BM^W STATE)) (^INT (^BM^ZERO)))
       (EQUAL (^BM^ZPLUS (^BM^V STATE) (^BM^W STATE))
              (^INT (^BM^CONS (^1) (^BM^ZERO))))))
     (IF (EQUAL (^BM^Y STATE) (^INT (^BM^CONS (^1) (^BM^ZERO))))
         (^BM^OR
          (EQUAL (^BM^ZPLUS (^BM^V STATE) (^BM^W STATE))
                 (^BM^MINUS (^INT (^BM^CONS (^2) (^BM^ZERO)))))
          (EQUAL (^BM^ZPLUS (^BM^V STATE) (^BM^W STATE))
                 (^BM^MINUS (^INT (^BM^CONS (^3) (^BM^ZERO))))))
         (IF (EQUAL (^BM^Y STATE) (^INT (^BM^CONS (^2) (^BM^ZERO))))
             (^BM^OR
              (EQUAL (^BM^ZPLUS (^BM^V STATE) (^BM^W STATE))
                     (^BM^MINUS (^INT (^BM^CONS (^1) (^BM^ZERO)))))
              (EQUAL (^BM^ZPLUS (^BM^V STATE) (^BM^W STATE))
                     (^BM^MINUS (^INT (^BM^CONS (^2) (^BM^ZERO))))))
             (IF (EQUAL (^BM^Y STATE) (^INT (^BM^CONS (^3) (^BM^ZERO))))
                 (EQUAL (^BM^ZPLUS (^BM^V STATE) (^BM^W STATE))
                        (^BM^MINUS (^INT (^BM^CONS (^1) (^BM^ZERO)))))
                 (IF (EQUAL (^BM^Y STATE)
                            (^BM^MINUS (^INT (^BM^CONS (^3) (^BM^ZERO)))))
                     (EQUAL (^BM^ZPLUS (^BM^V STATE) (^BM^W STATE))
                            (^INT (^BM^CONS (^1) (^BM^ZERO))))
                     (IF (EQUAL (^BM^Y STATE)
                                (^BM^MINUS (^INT (^BM^CONS (^2) (^BM^ZERO)))))
                         (^BM^OR
                          (EQUAL (^BM^ZPLUS (^BM^V STATE) (^BM^W STATE))
                                 (^INT (^BM^CONS (^1) (^BM^ZERO))))
                          (EQUAL (^BM^ZPLUS (^BM^V STATE) (^BM^W STATE))
                                 (^INT (^BM^CONS (^2) (^BM^ZERO)))))
                         (IF (EQUAL (^BM^Y STATE)
                                    (^BM^MINUS
                                     (^INT (^BM^CONS (^1) (^BM^ZERO)))))
                             (^BM^OR
                              (EQUAL (^BM^ZPLUS (^BM^V STATE) (^BM^W STATE))
                                     (^INT (^BM^CONS (^2) (^BM^ZERO))))
                              (EQUAL (^BM^ZPLUS (^BM^V STATE) (^BM^W STATE))
                                     (^INT (^BM^CONS (^3) (^BM^ZERO)))))
                             (^BM^FALSE)))))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^GOOD-STATEP STATE)
   (^BM^OR (EQUAL R (^BM^MINUS (^INT (^BM^CONS (^1) (^BM^ZERO)))))
    (^BM^OR (EQUAL R (^INT (^BM^ZERO)))
     (EQUAL R (^INT (^BM^CONS (^1) (^BM^ZERO)))))))
  (^BM^GOOD-STATEP (^BM^NEXT-STATE R STATE))))

(DEFINE (^BM^ZERO-DELTA-WS LST)
 (IF (^BM^EMPTY LST)
     (^BM^TRUE)
     (^BM^AND (EQUAL (^BM^HD LST) (^INT (^BM^ZERO)))
      (^BM^ZERO-DELTA-WS (^BM^TL LST)))))

(DEFINE (^BM^CONCAT X Y)
 (IF (^BM^EMPTY X) Y (^BM^CONS (^BM^HD X) (^BM^CONCAT (^BM^TL X) Y))))

(DEFINE (^BM^LENGTH X)
 (IF (^BM^EMPTY X) (^INT (^BM^ZERO)) (^BM^ADD1 (^BM^LENGTH (^BM^TL X)))))

(LEMMA (EQUAL (EQUAL (^BM^LENGTH X) (^INT (^BM^ZERO))) (^BM^EMPTY X)))

(LEMMA
 (^BM^IMPLIES (^BM^ZERO-DELTA-WS LST)
  (EQUAL (^BM^LESSP (^BM^LENGTH LST) (^INT (^BM^CONS (^4) (^BM^ZERO))))
         (^BM^NOT
          (EQUAL LST
                 (^BM^CONCAT
                  (^BM^CONS (^INT (^BM^ZERO))
                   (^BM^CONS (^INT (^BM^ZERO))
                    (^BM^CONS (^INT (^BM^ZERO))
                     (^BM^CONS (^INT (^BM^ZERO))
                      (^BM^PACK
                       (^BM^CONS (^N)
                        (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))))
                  (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR LST))))))))))

(LEMMA
 (^BM^IMPLIES (^BM^GOOD-STATEP STATE)
  (EQUAL (^BM^Y
          (^BM^FINAL-STATE-OF-VEHICLE
           (^BM^CONS (^INT (^BM^ZERO))
            (^BM^CONS (^INT (^BM^ZERO))
             (^BM^CONS (^INT (^BM^ZERO))
              (^BM^CONS (^INT (^BM^ZERO))
               (^BM^PACK
                (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))))
           STATE))
         (^INT (^BM^ZERO)))))

(LEMMA
 (^BM^IMPLIES (^BM^GOOD-STATEP STATE)
  (EQUAL (^BM^ZPLUS
          (^BM^V
           (^BM^FINAL-STATE-OF-VEHICLE
            (^BM^CONS (^INT (^BM^ZERO))
             (^BM^CONS (^INT (^BM^ZERO))
              (^BM^CONS (^INT (^BM^ZERO))
               (^BM^CONS (^INT (^BM^ZERO))
                (^BM^PACK
                 (^BM^CONS (^N)
                  (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))))
            STATE))
          (^BM^W
           (^BM^FINAL-STATE-OF-VEHICLE
            (^BM^CONS (^INT (^BM^ZERO))
             (^BM^CONS (^INT (^BM^ZERO))
              (^BM^CONS (^INT (^BM^ZERO))
               (^BM^CONS (^INT (^BM^ZERO))
                (^BM^PACK
                 (^BM^CONS (^N)
                  (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))))
            STATE)))
         (^INT (^BM^ZERO)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^ZERO-DELTA-WS LST)
   (^BM^AND (EQUAL (^BM^Y STATE) (^INT (^BM^ZERO)))
    (EQUAL (^BM^ZPLUS (^BM^W STATE) (^BM^V STATE)) (^INT (^BM^ZERO)))))
  (^BM^AND
   (EQUAL (^BM^Y (^BM^FINAL-STATE-OF-VEHICLE LST STATE)) (^INT (^BM^ZERO)))
   (EQUAL (^BM^ZPLUS (^BM^V (^BM^FINAL-STATE-OF-VEHICLE LST STATE))
           (^BM^W (^BM^FINAL-STATE-OF-VEHICLE LST STATE)))
          (^INT (^BM^ZERO))))))

(LEMMA
 (EQUAL (^BM^FINAL-STATE-OF-VEHICLE (^BM^CONCAT A B) STATE)
        (^BM^FINAL-STATE-OF-VEHICLE B (^BM^FINAL-STATE-OF-VEHICLE A STATE))))

(LEMMA
 (EQUAL (^BM^ZERO-DELTA-WS
         (^BM^CONCAT
          (^BM^CONS (^INT (^BM^ZERO))
           (^BM^CONS (^INT (^BM^ZERO))
            (^BM^CONS (^INT (^BM^ZERO))
             (^BM^CONS (^INT (^BM^ZERO))
              (^BM^PACK
               (^BM^CONS (^N) (^BM^CONS (^I) (^BM^CONS (^L) (^BM^ZERO)))))))))
          V))
        (^BM^ZERO-DELTA-WS V)))

(LEMMA
 (^BM^IMPLIES (^BM^GOOD-STATEP STATE)
  (^BM^NOT (^BM^ZLESSP (^INT (^BM^CONS (^3) (^BM^ZERO))) (^BM^Y STATE)))))

(LEMMA
 (^BM^IMPLIES (^BM^GOOD-STATEP STATE)
  (^BM^NOT
   (^BM^ZLESSP (^BM^Y STATE) (^BM^MINUS (^INT (^BM^CONS (^3) (^BM^ZERO))))))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^NUMBERP X) (^BM^NUMBERP Y))
  (EQUAL (^BM^ZLESSP X Y) (^BM^LESSP X Y))))

(DEFINE (^BM^FSV D S)
 (IF (^BM^EMPTY D) S (^BM^FSV (^BM^TL D) (^BM^NEXT-STATE (^BM^HD D) S))))

(LEMMA
 (^BM^IMPLIES (^BM^AND (^BM^RANDOM-DELTA-WS LST) (^BM^GOOD-STATEP STATE))
  (^BM^GOOD-STATEP (^BM^FINAL-STATE-OF-VEHICLE LST STATE))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^RANDOM-DELTA-WS LST)
   (EQUAL STATE
          (^BM^FINAL-STATE-OF-VEHICLE LST
           (^BM^VEHICLE-STATE (^INT (^BM^ZERO)) (^INT (^BM^ZERO))
            (^INT (^BM^ZERO))))))
  (^BM^AND
   (^BM^ZLESSEQP (^BM^MINUS (^INT (^BM^CONS (^3) (^BM^ZERO)))) (^BM^Y STATE))
   (^BM^ZLESSEQP (^BM^Y STATE) (^INT (^BM^CONS (^3) (^BM^ZERO)))))))

(LEMMA
 (^BM^IMPLIES (^BM^ZERO-DELTA-WS X)
  (^BM^ZERO-DELTA-WS (^BM^CDR (^BM^CDR (^BM^CDR (^BM^CDR X)))))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^GOOD-STATEP STATE)
   (^BM^AND (^BM^ZERO-DELTA-WS LST2)
    (^BM^NOT (^BM^LESSP (^BM^LENGTH LST2) (^INT (^BM^CONS (^4) (^BM^ZERO)))))))
  (EQUAL (^BM^Y (^BM^FINAL-STATE-OF-VEHICLE LST2 STATE)) (^INT (^BM^ZERO)))))

(LEMMA
 (^BM^IMPLIES
  (^BM^AND (^BM^RANDOM-DELTA-WS LST1)
   (^BM^AND (^BM^ZERO-DELTA-WS LST2)
    (^BM^AND
     (^BM^ZGREATEREQP (^BM^LENGTH LST2) (^INT (^BM^CONS (^4) (^BM^ZERO))))
     (EQUAL STATE
            (^BM^FINAL-STATE-OF-VEHICLE (^BM^CONCAT LST1 LST2)
             (^BM^VEHICLE-STATE (^INT (^BM^ZERO)) (^INT (^BM^ZERO))
              (^INT (^BM^ZERO))))))))
  (EQUAL (^BM^Y STATE) (^INT (^BM^ZERO)))))