(BOOT-STRAP NQTHM)
(COMPILE-UNCOMPILED-DEFNS "tmp")
(DEFN FROM-TO (I J)
  (IF (LESSP J I) NIL
      (IF (EQUAL (FIX I) (FIX J))
          (LIST (FIX J))
          (APPEND (FROM-TO I (SUB1 J)) (LIST J)))))
(PROVE-LEMMA PLUS-RIGHT-ID2 (REWRITE)
             (IMPLIES (NOT (NUMBERP Y))
                      (EQUAL (PLUS X Y)
                             (FIX X))))
(PROVE-LEMMA PLUS-ADD1 (REWRITE)
             (EQUAL (PLUS X (ADD1 Y))
                    (IF (NUMBERP Y)
                        (ADD1 (PLUS X Y))
                        (ADD1 X))))
(PROVE-LEMMA COMMUTATIVITY-OF-PLUS (REWRITE)
             (EQUAL (PLUS X Y)
                    (PLUS Y X)))
(PROVE-LEMMA ASSOCIATIVITY-OF-PLUS (REWRITE)
             (EQUAL (PLUS (PLUS X Y)
                          Z)
                    (PLUS X (PLUS Y Z))))