(BOOT-STRAP NQTHM)

[ 0.0 0.1 0.0 ]

GROUND-ZERO


(DEFN DIVIDES
      (X Y)
      (ZEROP (REMAINDER Y X)))

     Note that (OR (FALSEP (DIVIDES X Y)) (TRUEP (DIVIDES X Y))) is a theorem.




[ 0.0 0.0 0.0 ]

DIVIDES


(DEFN PRIME1
      (X Y)
      (IF (ZEROP Y)
          F
          (IF (EQUAL Y 1)
              T
              (AND (NOT (DIVIDES Y X))
                   (PRIME1 X (SUB1 Y))))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT Y) decreases according to the well-founded
relation LESSP in each recursive call.  Hence, PRIME1 is accepted under the
definitional principle.  Observe that:
      (OR (FALSEP (PRIME1 X Y))
          (TRUEP (PRIME1 X Y)))
is a theorem.




[ 0.0 0.0 0.0 ]

PRIME1


(DEFN PRIME
      (X)
      (AND (NOT (ZEROP X))
           (NOT (EQUAL X 1))
           (PRIME1 X (SUB1 X))))

     Note that (OR (FALSEP (PRIME X)) (TRUEP (PRIME X))) is a theorem.




[ 0.0 0.0 0.0 ]

PRIME


(DEFN DELETE
      (X Y)
      (IF (LISTP Y)
          (IF (EQUAL X (CAR Y))
              (CDR Y)
              (CONS (CAR Y) (DELETE X (CDR Y))))
          Y))

     Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT Y) decreases according to the well-founded relation LESSP in each
recursive call.  Hence, DELETE is accepted under the principle of definition.




[ 0.3 0.0 0.0 ]

DELETE


(DEFN PERM
      (A B)
      (IF (NLISTP A)
          (NLISTP B)
          (IF (MEMBER (CAR A) B)
              (PERM (CDR A) (DELETE (CAR A) B))
              F)))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP establish that the measure (COUNT A) decreases according
to the well-founded relation LESSP in each recursive call.  Hence, PERM is
accepted under the principle of definition.  From the definition we can
conclude that (OR (FALSEP (PERM A B)) (TRUEP (PERM A B))) is a theorem.




[ 0.0 0.0 0.0 ]

PERM


(DEFN PRIME-LIST
      (L)
      (IF (NLISTP L)
          T
          (AND (PRIME (CAR L))
               (PRIME-LIST (CDR L)))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT L) decreases according
to the well-founded relation LESSP in each recursive call.  Hence, PRIME-LIST
is accepted under the definitional principle.  Observe that:
      (OR (FALSEP (PRIME-LIST L))
          (TRUEP (PRIME-LIST L)))
is a theorem.




[ 0.0 0.0 0.0 ]

PRIME-LIST


(DEFN TIMES-LIST
      (L)
      (IF (NLISTP L)
          1
          (TIMES (CAR L) (TIMES-LIST (CDR L)))))

     Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the
definition of NLISTP inform us that the measure (COUNT L) decreases according
to the well-founded relation LESSP in each recursive call.  Hence, TIMES-LIST
is accepted under the definitional principle.  From the definition we can
conclude that (NUMBERP (TIMES-LIST L)) is a theorem.




[ 0.0 0.0 0.0 ]

TIMES-LIST


(PROVE-LEMMA PLUS-RIGHT-ID2
             (REWRITE)
             (IMPLIES (NOT (NUMBERP Y))
                      (EQUAL (PLUS X Y) (FIX X))))

This simplifies, unfolding the definition of FIX, to the following two new
goals:

Case 2. (IMPLIES (AND (NOT (NUMBERP Y))
                      (NOT (NUMBERP X)))
                 (EQUAL (PLUS X Y) 0)).

  This again simplifies, opening up the definitions of PLUS and EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (NUMBERP Y)) (NUMBERP X))
                 (EQUAL (PLUS X Y) X)),

  which we will name *1.


     We will appeal to induction.  There is only one plausible induction.  We
will induct according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p X Y))
           (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y))
                    (p X Y))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definition
of ZEROP establish that the measure (COUNT X) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme generates the following two new formulas:

Case 2. (IMPLIES (AND (ZEROP X)
                      (NOT (NUMBERP Y))
                      (NUMBERP X))
                 (EQUAL (PLUS X Y) X)).

  This simplifies, expanding the functions ZEROP, NUMBERP, EQUAL, and PLUS, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (PLUS (SUB1 X) Y) (SUB1 X))
                      (NOT (NUMBERP Y))
                      (NUMBERP X))
                 (EQUAL (PLUS X Y) X)).

  This simplifies, using linear arithmetic, to the new conjecture:

        (IMPLIES (AND (EQUAL X 0)
                      (NOT (ZEROP X))
                      (EQUAL (PLUS (SUB1 X) Y) (SUB1 X))
                      (NOT (NUMBERP Y))
                      (NUMBERP X))
                 (EQUAL (PLUS X Y) X)),

  which again simplifies, expanding the function ZEROP, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

PLUS-RIGHT-ID2


(PROVE-LEMMA PLUS-ADD1
             (REWRITE)
             (EQUAL (PLUS X (ADD1 Y))
                    (IF (NUMBERP Y)
                        (ADD1 (PLUS X Y))
                        (ADD1 X))))

This simplifies, obviously, to two new formulas:

Case 2. (IMPLIES (NOT (NUMBERP Y))
                 (EQUAL (PLUS X (ADD1 Y)) (ADD1 X))),

  which again simplifies, rewriting with the lemma SUB1-TYPE-RESTRICTION, to
  the conjecture:

        (IMPLIES (NOT (NUMBERP Y))
                 (EQUAL (PLUS X 1) (ADD1 X))).

  But this again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (NUMBERP Y)
                 (EQUAL (PLUS X (ADD1 Y))
                        (ADD1 (PLUS X Y)))),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PLUS-ADD1


(PROVE-LEMMA COMMUTATIVITY2-OF-PLUS
             (REWRITE)
             (EQUAL (PLUS X (PLUS Y Z))
                    (PLUS Y (PLUS X Z))))

This simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

COMMUTATIVITY2-OF-PLUS


(PROVE-LEMMA COMMUTATIVITY-OF-PLUS
             (REWRITE)
             (EQUAL (PLUS X Y) (PLUS Y X)))

WARNING:  the newly proposed lemma, COMMUTATIVITY-OF-PLUS, could be applied
whenever the previously added lemma COMMUTATIVITY2-OF-PLUS could.




WARNING:  the newly proposed lemma, COMMUTATIVITY-OF-PLUS, could be applied
whenever the previously added lemma PLUS-ADD1 could.




WARNING:  the newly proposed lemma, COMMUTATIVITY-OF-PLUS, could be applied
whenever the previously added lemma PLUS-RIGHT-ID2 could.




This formula simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

COMMUTATIVITY-OF-PLUS


(PROVE-LEMMA ASSOCIATIVITY-OF-PLUS
             (REWRITE)
             (EQUAL (PLUS (PLUS X Y) Z)
                    (PLUS X (PLUS Y Z))))

WARNING:  the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied
whenever the newly proposed ASSOCIATIVITY-OF-PLUS could!


This simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

ASSOCIATIVITY-OF-PLUS


(PROVE-LEMMA PLUS-EQUAL-0
             (REWRITE)
             (EQUAL (EQUAL (PLUS A B) 0)
                    (AND (ZEROP A) (ZEROP B))))

This simplifies, opening up the functions ZEROP and AND, to six new
conjectures:

Case 6. (IMPLIES (AND (NOT (EQUAL (PLUS A B) 0))
                      (NOT (NUMBERP A)))
                 (NOT (EQUAL B 0))),

  which again simplifies, applying PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS,
  and unfolding the functions NUMBERP and EQUAL, to:

        T.

Case 5. (IMPLIES (AND (NOT (EQUAL (PLUS A B) 0))
                      (NOT (NUMBERP A)))
                 (NUMBERP B)).

  However this again simplifies, applying PLUS-RIGHT-ID2, and unfolding the
  function EQUAL, to:

        T.

Case 4. (IMPLIES (AND (NOT (EQUAL (PLUS A B) 0))
                      (EQUAL A 0))
                 (NOT (EQUAL B 0))).

  This again simplifies, using linear arithmetic, to:

        T.

Case 3. (IMPLIES (AND (NOT (EQUAL (PLUS A B) 0))
                      (EQUAL A 0))
                 (NUMBERP B)),

  which again simplifies, applying the lemma PLUS-RIGHT-ID2, and opening up
  the definitions of NUMBERP and EQUAL, to:

        T.

Case 2. (IMPLIES (AND (EQUAL (PLUS A B) 0)
                      (NOT (EQUAL A 0)))
                 (NOT (NUMBERP A))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (EQUAL (PLUS A B) 0)
                      (NOT (EQUAL B 0)))
                 (NOT (NUMBERP B))),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PLUS-EQUAL-0


(PROVE-LEMMA DIFFERENCE-X-X
             (REWRITE)
             (EQUAL (DIFFERENCE X X) 0))

This conjecture simplifies, using linear arithmetic, to:

      (IMPLIES (LESSP X X)
               (EQUAL (DIFFERENCE X X) 0)).

But this again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-X-X


(PROVE-LEMMA DIFFERENCE-PLUS
             (REWRITE)
             (AND (EQUAL (DIFFERENCE (PLUS X Y) X)
                         (FIX Y))
                  (EQUAL (DIFFERENCE (PLUS Y X) X)
                         (FIX Y))))

WARNING:  Note that the proposed lemma DIFFERENCE-PLUS is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and two replacement rules.


This formula can be simplified, using the abbreviation AND, to the following
two new conjectures:

Case 2. (EQUAL (DIFFERENCE (PLUS X Y) X)
               (FIX Y)).

  This simplifies, unfolding the function FIX, to the following two new
  formulas:

  Case 2.2.
          (IMPLIES (NOT (NUMBERP Y))
                   (EQUAL (DIFFERENCE (PLUS X Y) X) 0)).

    However this again simplifies, applying PLUS-RIGHT-ID2, to the following
    two new goals:

    Case 2.2.2.
            (IMPLIES (AND (NOT (NUMBERP Y))
                          (NOT (NUMBERP X)))
                     (EQUAL (DIFFERENCE 0 X) 0)).

      But this again simplifies, expanding EQUAL and DIFFERENCE, to:

            T.

    Case 2.2.1.
            (IMPLIES (AND (NOT (NUMBERP Y)) (NUMBERP X))
                     (EQUAL (DIFFERENCE X X) 0)),

      which again simplifies, using linear arithmetic, to:

            (IMPLIES (AND (LESSP X X)
                          (NOT (NUMBERP Y))
                          (NUMBERP X))
                     (EQUAL (DIFFERENCE X X) 0)).

      However this again simplifies, using linear arithmetic, to:

            T.

  Case 2.1.
          (IMPLIES (NUMBERP Y)
                   (EQUAL (DIFFERENCE (PLUS X Y) X) Y)),

    which again simplifies, using linear arithmetic, to the conjecture:

          (IMPLIES (AND (LESSP (PLUS X Y) X) (NUMBERP Y))
                   (EQUAL (DIFFERENCE (PLUS X Y) X) Y)).

    This again simplifies, using linear arithmetic, to:

          T.

Case 1. (EQUAL (DIFFERENCE (PLUS Y X) X)
               (FIX Y)),

  which simplifies, applying the lemma COMMUTATIVITY-OF-PLUS, and unfolding
  FIX, to two new conjectures:

  Case 1.2.
          (IMPLIES (NOT (NUMBERP Y))
                   (EQUAL (DIFFERENCE (PLUS X Y) X) 0)),

    which again simplifies, rewriting with the lemma PLUS-RIGHT-ID2, to two
    new formulas:

    Case 1.2.2.
            (IMPLIES (AND (NOT (NUMBERP Y))
                          (NOT (NUMBERP X)))
                     (EQUAL (DIFFERENCE 0 X) 0)),

      which again simplifies, expanding the definitions of EQUAL and
      DIFFERENCE, to:

            T.

    Case 1.2.1.
            (IMPLIES (AND (NOT (NUMBERP Y)) (NUMBERP X))
                     (EQUAL (DIFFERENCE X X) 0)),

      which again simplifies, using linear arithmetic, to:

            (IMPLIES (AND (LESSP X X)
                          (NOT (NUMBERP Y))
                          (NUMBERP X))
                     (EQUAL (DIFFERENCE X X) 0)).

      However this again simplifies, using linear arithmetic, to:

            T.

  Case 1.1.
          (IMPLIES (NUMBERP Y)
                   (EQUAL (DIFFERENCE (PLUS X Y) X) Y)),

    which again simplifies, using linear arithmetic, to the formula:

          (IMPLIES (AND (LESSP (PLUS X Y) X) (NUMBERP Y))
                   (EQUAL (DIFFERENCE (PLUS X Y) X) Y)).

    This again simplifies, using linear arithmetic, to:

          T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-PLUS


(PROVE-LEMMA PLUS-CANCELLATION
             (REWRITE)
             (EQUAL (EQUAL (PLUS A B) (PLUS A C))
                    (EQUAL (FIX B) (FIX C))))

This conjecture simplifies, expanding the definition of FIX, to the following
seven new formulas:

Case 7. (IMPLIES (AND (NUMBERP C)
                      (NUMBERP B)
                      (NOT (EQUAL B C)))
                 (NOT (EQUAL (PLUS A B) (PLUS A C)))).

  This again simplifies, using linear arithmetic, to:

        T.

Case 6. (IMPLIES (AND (NUMBERP C)
                      (NOT (NUMBERP B))
                      (NOT (EQUAL 0 C)))
                 (NOT (EQUAL (PLUS A B) (PLUS A C)))),

  which again simplifies, rewriting with PLUS-RIGHT-ID2, to the following two
  new conjectures:

  Case 6.2.
          (IMPLIES (AND (NUMBERP C)
                        (NOT (NUMBERP B))
                        (NOT (EQUAL 0 C))
                        (NOT (NUMBERP A)))
                   (NOT (EQUAL 0 (PLUS A C)))).

    This again simplifies, using linear arithmetic, to:

          T.

  Case 6.1.
          (IMPLIES (AND (NUMBERP C)
                        (NOT (NUMBERP B))
                        (NOT (EQUAL 0 C))
                        (NUMBERP A))
                   (NOT (EQUAL A (PLUS A C)))),

    which again simplifies, using linear arithmetic, to:

          T.

Case 5. (IMPLIES (AND (NOT (NUMBERP C))
                      (NUMBERP B)
                      (NOT (EQUAL B 0)))
                 (NOT (EQUAL (PLUS A B) (PLUS A C)))),

  which again simplifies, rewriting with PLUS-RIGHT-ID2, to the following two
  new goals:

  Case 5.2.
          (IMPLIES (AND (NOT (NUMBERP C))
                        (NUMBERP B)
                        (NOT (EQUAL B 0))
                        (NOT (NUMBERP A)))
                   (NOT (EQUAL (PLUS A B) 0))).

    This again simplifies, using linear arithmetic, to:

          T.

  Case 5.1.
          (IMPLIES (AND (NOT (NUMBERP C))
                        (NUMBERP B)
                        (NOT (EQUAL B 0))
                        (NUMBERP A))
                   (NOT (EQUAL (PLUS A B) A))),

    which again simplifies, using linear arithmetic, to:

          T.

Case 4. (IMPLIES (AND (NOT (NUMBERP C))
                      (NOT (NUMBERP B)))
                 (EQUAL (EQUAL (PLUS A B) (PLUS A C))
                        T)),

  which again simplifies, rewriting with the lemma PLUS-RIGHT-ID2, and opening
  up EQUAL, to:

        T.

Case 3. (IMPLIES (AND (NOT (NUMBERP C)) (EQUAL B 0))
                 (EQUAL (EQUAL (PLUS A B) (PLUS A C))
                        T)),

  which again simplifies, rewriting with COMMUTATIVITY-OF-PLUS and
  PLUS-RIGHT-ID2, and expanding the functions EQUAL and PLUS, to:

        T.

Case 2. (IMPLIES (AND (NOT (NUMBERP B)) (EQUAL 0 C))
                 (EQUAL (EQUAL (PLUS A B) (PLUS A C))
                        T)).

  This again simplifies, applying PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS,
  and opening up EQUAL and PLUS, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP C)
                      (NUMBERP B)
                      (EQUAL B C))
                 (EQUAL (EQUAL (PLUS A B) (PLUS A C))
                        T)).

  But this again simplifies, expanding the function EQUAL, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PLUS-CANCELLATION


(PROVE-LEMMA DIFFERENCE-0
             (REWRITE)
             (IMPLIES (NOT (LESSP Y X))
                      (EQUAL (DIFFERENCE X Y) 0)))


     Name the conjecture *1.


     Let us appeal to the induction principle.  The recursive terms in the
conjecture suggest four inductions.  However, they merge into one likely
candidate induction.  We will induct according to the following scheme:
      (AND (IMPLIES (OR (EQUAL X 0) (NOT (NUMBERP X)))
                    (p X Y))
           (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                         (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
                    (p X Y))
           (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                         (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
                         (p (SUB1 X) (SUB1 Y)))
                    (p X Y))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT can be used to show that the measure (COUNT Y) decreases
according to the well-founded relation LESSP in each induction step of the
scheme.  Note, however, the inductive instance chosen for X.  The above
induction scheme leads to the following four new goals:

Case 4. (IMPLIES (AND (OR (EQUAL X 0) (NOT (NUMBERP X)))
                      (NOT (LESSP Y X)))
                 (EQUAL (DIFFERENCE X Y) 0)).

  This simplifies, expanding the definitions of NOT, OR, EQUAL, LESSP, and
  DIFFERENCE, to:

        T.

Case 3. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                      (OR (EQUAL Y 0) (NOT (NUMBERP Y)))
                      (NOT (LESSP Y X)))
                 (EQUAL (DIFFERENCE X Y) 0)).

  This simplifies, unfolding NOT, OR, EQUAL, and LESSP, to:

        T.

Case 2. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                      (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
                      (LESSP (SUB1 Y) (SUB1 X))
                      (NOT (LESSP Y X)))
                 (EQUAL (DIFFERENCE X Y) 0)).

  This simplifies, using linear arithmetic, to:

        (IMPLIES (AND (LESSP X 1)
                      (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                      (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
                      (LESSP (SUB1 Y) (SUB1 X))
                      (NOT (LESSP Y X)))
                 (EQUAL (DIFFERENCE X Y) 0)),

  which again simplifies, opening up the definitions of SUB1, NUMBERP, EQUAL,
  LESSP, NOT, and OR, to:

        T.

Case 1. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                      (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
                      (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                             0)
                      (NOT (LESSP Y X)))
                 (EQUAL (DIFFERENCE X Y) 0)),

  which simplifies, using linear arithmetic, to three new conjectures:

  Case 1.3.
          (IMPLIES (AND (LESSP X Y)
                        (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                        (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               0)
                        (NOT (LESSP Y X)))
                   (EQUAL (DIFFERENCE X Y) 0)),

    which again simplifies, using linear arithmetic, to two new conjectures:

    Case 1.3.2.
            (IMPLIES (AND (LESSP (SUB1 X) (SUB1 Y))
                          (LESSP X Y)
                          (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                          (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
                          (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                 0)
                          (NOT (LESSP Y X)))
                     (EQUAL (DIFFERENCE X Y) 0)),

      which again simplifies, unfolding the functions LESSP, NOT, OR,
      DIFFERENCE, and EQUAL, to:

            T.

    Case 1.3.1.
            (IMPLIES (AND (LESSP X 1)
                          (LESSP X Y)
                          (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                          (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
                          (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                                 0)
                          (NOT (LESSP Y X)))
                     (EQUAL (DIFFERENCE X Y) 0)),

      which again simplifies, unfolding SUB1, NUMBERP, EQUAL, LESSP, NOT, and
      OR, to:

            T.

  Case 1.2.
          (IMPLIES (AND (LESSP (SUB1 X) (SUB1 Y))
                        (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                        (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               0)
                        (NOT (LESSP Y X)))
                   (EQUAL (DIFFERENCE X Y) 0)),

    which again simplifies, expanding the definitions of NOT, OR, LESSP,
    DIFFERENCE, and EQUAL, to:

          T.

  Case 1.1.
          (IMPLIES (AND (LESSP X 1)
                        (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                        (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
                        (EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
                               0)
                        (NOT (LESSP Y X)))
                   (EQUAL (DIFFERENCE X Y) 0)),

    which again simplifies, opening up the definitions of SUB1, NUMBERP, EQUAL,
    LESSP, NOT, and OR, to:

          T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-0


(PROVE-LEMMA EQUAL-DIFFERENCE-0
             (REWRITE)
             (EQUAL (EQUAL 0 (DIFFERENCE X Y))
                    (NOT (LESSP Y X))))

This conjecture simplifies, unfolding NOT, to two new conjectures:

Case 2. (IMPLIES (NOT (EQUAL 0 (DIFFERENCE X Y)))
                 (LESSP Y X)),

  which again simplifies, rewriting with the lemma DIFFERENCE-0, and opening
  up the definition of EQUAL, to:

        T.

Case 1. (IMPLIES (EQUAL 0 (DIFFERENCE X Y))
                 (NOT (LESSP Y X))),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

EQUAL-DIFFERENCE-0


(PROVE-LEMMA DIFFERENCE-CANCELLATION-0
             (REWRITE)
             (EQUAL (EQUAL X (DIFFERENCE X Y))
                    (AND (NUMBERP X)
                         (OR (EQUAL X 0) (ZEROP Y)))))

This simplifies, opening up the functions ZEROP, OR, and AND, to five new
goals:

Case 5. (IMPLIES (EQUAL X (DIFFERENCE X Y))
                 (NUMBERP X)),

  which again simplifies, obviously, to:

        T.

Case 4. (IMPLIES (AND (EQUAL X (DIFFERENCE X Y))
                      (NOT (EQUAL X 0))
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))).

  But this again simplifies, using linear arithmetic, to the conjecture:

        (IMPLIES (AND (LESSP X Y)
                      (EQUAL X (DIFFERENCE X Y))
                      (NOT (EQUAL X 0))
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))).

  This again simplifies, using linear arithmetic and applying DIFFERENCE-0, to:

        T.

Case 3. (IMPLIES (AND (NOT (EQUAL X (DIFFERENCE X Y)))
                      (NUMBERP X))
                 (NUMBERP Y)).

  But this again simplifies, expanding the definition of DIFFERENCE, to:

        T.

Case 2. (IMPLIES (AND (NOT (EQUAL X (DIFFERENCE X Y)))
                      (NUMBERP X))
                 (NOT (EQUAL Y 0))),

  which again simplifies, using linear arithmetic, to:

        (IMPLIES (AND (LESSP X 0)
                      (NOT (EQUAL X (DIFFERENCE X 0))))
                 (NOT (NUMBERP X))).

  But this again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL X (DIFFERENCE X Y)))
                      (NUMBERP X))
                 (NOT (EQUAL X 0))),

  which again simplifies, using linear arithmetic, applying the lemma
  DIFFERENCE-0, and expanding EQUAL, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-CANCELLATION-0


(PROVE-LEMMA DIFFERENCE-CANCELLATION-1
             (REWRITE)
             (EQUAL (EQUAL (DIFFERENCE X Y)
                           (DIFFERENCE Z Y))
                    (IF (LESSP X Y)
                        (NOT (LESSP Y Z))
                        (IF (LESSP Z Y)
                            (NOT (LESSP Y X))
                            (EQUAL (FIX X) (FIX Z))))))

This simplifies, opening up NOT and FIX, to the following 11 new goals:

Case 11.(IMPLIES (AND (EQUAL (DIFFERENCE X Y)
                             (DIFFERENCE Z Y))
                      (NOT (LESSP X Y))
                      (NOT (LESSP Z Y))
                      (NOT (NUMBERP Z))
                      (NUMBERP X))
                 (EQUAL (EQUAL X 0) T)).

  This again simplifies, using linear arithmetic, applying DIFFERENCE-0 and
  EQUAL-DIFFERENCE-0, and expanding LESSP, to the following two new
  conjectures:

  Case 11.2.
          (IMPLIES (AND (NOT (LESSP Y X))
                        (NOT (LESSP X Y))
                        (EQUAL Y 0)
                        (NOT (NUMBERP Z))
                        (NUMBERP X))
                   (EQUAL X 0)).

    But this again simplifies, using linear arithmetic, to:

          T.

  Case 11.1.
          (IMPLIES (AND (NOT (LESSP Y X))
                        (NOT (LESSP X Y))
                        (NOT (NUMBERP Y))
                        (NOT (NUMBERP Z))
                        (NUMBERP X))
                   (EQUAL X 0)),

    which again simplifies, unfolding the definition of LESSP, to:

          T.

Case 10.(IMPLIES (AND (EQUAL (DIFFERENCE X Y)
                             (DIFFERENCE Z Y))
                      (NOT (LESSP X Y))
                      (NOT (LESSP Z Y))
                      (NUMBERP Z)
                      (NOT (NUMBERP X)))
                 (EQUAL (EQUAL 0 Z) T)),

  which again simplifies, using linear arithmetic, rewriting with DIFFERENCE-0
  and EQUAL-DIFFERENCE-0, and opening up the functions LESSP and EQUAL, to the
  following two new formulas:

  Case 10.2.
          (IMPLIES (AND (NOT (LESSP Y Z))
                        (EQUAL Y 0)
                        (NUMBERP Z)
                        (NOT (NUMBERP X)))
                   (EQUAL 0 Z)).

    But this again simplifies, using linear arithmetic, to:

          T.

  Case 10.1.
          (IMPLIES (AND (NOT (LESSP Y Z))
                        (NOT (NUMBERP Y))
                        (NUMBERP Z)
                        (NOT (NUMBERP X)))
                   (EQUAL 0 Z)),

    which again simplifies, expanding the function LESSP, to:

          T.

Case 9. (IMPLIES (AND (EQUAL (DIFFERENCE X Y)
                             (DIFFERENCE Z Y))
                      (NOT (LESSP X Y))
                      (NOT (LESSP Z Y))
                      (NUMBERP Z)
                      (NUMBERP X))
                 (EQUAL (EQUAL X Z) T)),

  which again simplifies, obviously, to the new formula:

        (IMPLIES (AND (EQUAL (DIFFERENCE X Y)
                             (DIFFERENCE Z Y))
                      (NOT (LESSP X Y))
                      (NOT (LESSP Z Y))
                      (NUMBERP Z)
                      (NUMBERP X))
                 (EQUAL X Z)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 8. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y)
                                  (DIFFERENCE Z Y)))
                      (NOT (LESSP X Y))
                      (NOT (LESSP Z Y))
                      (NOT (NUMBERP Z)))
                 (NOT (EQUAL X 0))),

  which again simplifies, using linear arithmetic, appealing to the lemma
  DIFFERENCE-0, and unfolding the function EQUAL, to:

        T.

Case 7. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y)
                                  (DIFFERENCE Z Y)))
                      (NOT (LESSP X Y))
                      (NOT (LESSP Z Y))
                      (NOT (NUMBERP X)))
                 (NOT (EQUAL 0 Z))),

  which again simplifies, using linear arithmetic, applying DIFFERENCE-0, and
  unfolding the function EQUAL, to:

        T.

Case 6. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y)
                                  (DIFFERENCE Z Y)))
                      (NOT (LESSP X Y))
                      (NOT (LESSP Z Y))
                      (NUMBERP Z)
                      (NUMBERP X))
                 (NOT (EQUAL X Z))).

  This again simplifies, clearly, to:

        T.

Case 5. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y)
                                  (DIFFERENCE Z Y)))
                      (LESSP X Y))
                 (LESSP Y Z)).

  However this again simplifies, using linear arithmetic, applying
  DIFFERENCE-0, and expanding the function EQUAL, to:

        T.

Case 4. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y)
                                  (DIFFERENCE Z Y)))
                      (NOT (LESSP X Y))
                      (NOT (LESSP Z Y))
                      (NOT (NUMBERP Z)))
                 (NUMBERP X)).

  However this again simplifies, using linear arithmetic, applying
  DIFFERENCE-0, and unfolding the definition of EQUAL, to:

        T.

Case 3. (IMPLIES (AND (NOT (EQUAL (DIFFERENCE X Y)
                                  (DIFFERENCE Z Y)))
                      (NOT (LESSP X Y))
                      (LESSP Z Y))
                 (LESSP Y X)).

  But this again simplifies, using linear arithmetic, to three new goals:

  Case 3.3.
          (IMPLIES (AND (NOT (NUMBERP Y))
                        (NOT (EQUAL (DIFFERENCE X Y)
                                    (DIFFERENCE Z Y)))
                        (NOT (LESSP X Y))
                        (LESSP Z Y))
                   (LESSP Y X)),

    which again simplifies, appealing to the lemma DIFFERENCE-0, and expanding
    the definitions of DIFFERENCE and LESSP, to:

          T.

  Case 3.2.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (NOT (EQUAL (DIFFERENCE X Y)
                                    (DIFFERENCE Z Y)))
                        (NOT (LESSP X Y))
                        (LESSP Z Y))
                   (LESSP Y X)),

    which again simplifies, using linear arithmetic, applying DIFFERENCE-0,
    and unfolding the function EQUAL, to:

          T.

  Case 3.1.
          (IMPLIES (AND (NUMBERP X)
                        (NUMBERP Y)
                        (NOT (EQUAL (DIFFERENCE X X)
                                    (DIFFERENCE Z X)))
                        (NOT (LESSP X X))
                        (LESSP Z X))
                   (LESSP X X)).

    However this again simplifies, using linear arithmetic, applying
    DIFFERENCE-0, and expanding the function EQUAL, to:

          T.

Case 2. (IMPLIES (AND (EQUAL (DIFFERENCE X Y)
                             (DIFFERENCE Z Y))
                      (LESSP X Y))
                 (NOT (LESSP Y Z))).

  However this again simplifies, using linear arithmetic and rewriting with
  the lemmas DIFFERENCE-0 and EQUAL-DIFFERENCE-0, to:

        T.

Case 1. (IMPLIES (AND (EQUAL (DIFFERENCE X Y)
                             (DIFFERENCE Z Y))
                      (NOT (LESSP X Y))
                      (LESSP Z Y))
                 (NOT (LESSP Y X))),

  which again simplifies, using linear arithmetic and rewriting with
  DIFFERENCE-0 and EQUAL-DIFFERENCE-0, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-CANCELLATION-1


(PROVE-LEMMA TIMES-ZERO2
             (REWRITE)
             (IMPLIES (NOT (NUMBERP Y))
                      (EQUAL (TIMES X Y) 0)))


     Call the conjecture *1.


     Perhaps we can prove it by induction.  There is only one plausible
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p X Y))
           (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y))
                    (p X Y))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to prove that the measure (COUNT X) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme leads to two new goals:

Case 2. (IMPLIES (AND (ZEROP X) (NOT (NUMBERP Y)))
                 (EQUAL (TIMES X Y) 0)),

  which simplifies, opening up the definitions of ZEROP, EQUAL, and TIMES, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (TIMES (SUB1 X) Y) 0)
                      (NOT (NUMBERP Y)))
                 (EQUAL (TIMES X Y) 0)),

  which simplifies, applying PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS, and
  unfolding ZEROP, TIMES, NUMBERP, and EQUAL, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

TIMES-ZERO2


(PROVE-LEMMA DISTRIBUTIVITY-OF-TIMES-OVER-PLUS
             (REWRITE)
             (EQUAL (TIMES X (PLUS Y Z))
                    (PLUS (TIMES X Y) (TIMES X Z))))


     Call the conjecture *1.


     We will try to prove it by induction.  There are four plausible
inductions.  They merge into two likely candidate inductions.  However, only
one is unflawed.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p X Y Z))
           (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y Z))
                    (p X Y Z))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT X) decreases according to the well-founded relation
LESSP in each induction step of the scheme.  The above induction scheme
generates two new goals:

Case 2. (IMPLIES (ZEROP X)
                 (EQUAL (TIMES X (PLUS Y Z))
                        (PLUS (TIMES X Y) (TIMES X Z)))),

  which simplifies, opening up the functions ZEROP, EQUAL, TIMES, and PLUS, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (TIMES (SUB1 X) (PLUS Y Z))
                             (PLUS (TIMES (SUB1 X) Y)
                                   (TIMES (SUB1 X) Z))))
                 (EQUAL (TIMES X (PLUS Y Z))
                        (PLUS (TIMES X Y) (TIMES X Z)))),

  which simplifies, applying ASSOCIATIVITY-OF-PLUS and COMMUTATIVITY2-OF-PLUS,
  and unfolding the functions ZEROP and TIMES, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

DISTRIBUTIVITY-OF-TIMES-OVER-PLUS


(PROVE-LEMMA TIMES-ADD1
             (REWRITE)
             (EQUAL (TIMES X (ADD1 Y))
                    (IF (NUMBERP Y)
                        (PLUS X (TIMES X Y))
                        (FIX X))))

This conjecture simplifies, unfolding the definition of FIX, to three new
conjectures:

Case 3. (IMPLIES (AND (NOT (NUMBERP Y)) (NUMBERP X))
                 (EQUAL (TIMES X (ADD1 Y)) X)),

  which again simplifies, rewriting with SUB1-TYPE-RESTRICTION, to the new
  formula:

        (IMPLIES (AND (NOT (NUMBERP Y)) (NUMBERP X))
                 (EQUAL (TIMES X 1) X)),

  which we will name *1.

Case 2. (IMPLIES (AND (NOT (NUMBERP Y))
                      (NOT (NUMBERP X)))
                 (EQUAL (TIMES X (ADD1 Y)) 0)).

  However this again simplifies, applying SUB1-TYPE-RESTRICTION, and opening
  up the definitions of TIMES and EQUAL, to:

        T.

Case 1. (IMPLIES (NUMBERP Y)
                 (EQUAL (TIMES X (ADD1 Y))
                        (PLUS X (TIMES X Y)))),

  which we would usually push and work on later by induction.  But if we must
  use induction to prove the input conjecture, we prefer to induct on the
  original formulation of the problem.  Thus we will disregard all that we
  have previously done, give the name *1 to the original input, and work on it.


     So now let us consider:

(EQUAL (TIMES X (ADD1 Y))
       (IF (NUMBERP Y)
           (PLUS X (TIMES X Y))
           (FIX X))),

which we named *1 above.  We will appeal to induction.  The recursive terms in
the conjecture suggest three inductions.  However, they merge into one likely
candidate induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p X Y))
           (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y))
                    (p X Y))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT X) decreases according to the well-founded
relation LESSP in each induction step of the scheme.  The above induction
scheme leads to the following two new formulas:

Case 2. (IMPLIES (ZEROP X)
                 (EQUAL (TIMES X (ADD1 Y))
                        (IF (NUMBERP Y)
                            (PLUS X (TIMES X Y))
                            (FIX X)))).

  This simplifies, rewriting with PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS,
  and expanding the definitions of ZEROP, EQUAL, TIMES, PLUS, FIX, and NUMBERP,
  to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (TIMES (SUB1 X) (ADD1 Y))
                             (IF (NUMBERP Y)
                                 (PLUS (SUB1 X) (TIMES (SUB1 X) Y))
                                 (FIX (SUB1 X)))))
                 (EQUAL (TIMES X (ADD1 Y))
                        (IF (NUMBERP Y)
                            (PLUS X (TIMES X Y))
                            (FIX X)))),

  which simplifies, applying SUB1-TYPE-RESTRICTION and SUB1-ADD1, and
  unfolding the functions ZEROP, FIX, TIMES, and PLUS, to the following two
  new formulas:

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (NUMBERP Y))
                        (EQUAL (TIMES (SUB1 X) (ADD1 Y))
                               (SUB1 X)))
                   (EQUAL (TIMES X 1) X)).

    But this further simplifies, rewriting with SUB1-TYPE-RESTRICTION, and
    unfolding TIMES, to the new formula:

          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (NUMBERP Y))
                        (EQUAL (TIMES (SUB1 X) 1) (SUB1 X)))
                   (EQUAL (PLUS 1 (SUB1 X)) X)),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NUMBERP Y)
                        (EQUAL (TIMES (SUB1 X) (ADD1 Y))
                               (PLUS (SUB1 X) (TIMES (SUB1 X) Y))))
                   (EQUAL (ADD1 (PLUS Y (TIMES (SUB1 X) (ADD1 Y))))
                          (PLUS X Y (TIMES (SUB1 X) Y)))),

    which again simplifies, using linear arithmetic, to:

          T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

TIMES-ADD1


(PROVE-LEMMA COMMUTATIVITY-OF-TIMES
             (REWRITE)
             (EQUAL (TIMES X Y) (TIMES Y X)))

WARNING:  the newly proposed lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the previously added lemma TIMES-ADD1 could.




WARNING:  the newly proposed lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the previously added lemma DISTRIBUTIVITY-OF-TIMES-OVER-PLUS could.




WARNING:  the newly proposed lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the previously added lemma TIMES-ZERO2 could.





     Give the conjecture the name *1.


     We will appeal to induction.  Two inductions are suggested by terms in
the conjecture, both of which are flawed.  We limit our consideration to the
two suggested by the largest number of nonprimitive recursive functions in the
conjecture.  Since both of these are equally likely, we will choose
arbitrarily.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p X Y))
           (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y))
                    (p X Y))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT X) decreases according to the well-founded relation
LESSP in each induction step of the scheme.  The above induction scheme
produces the following two new conjectures:

Case 2. (IMPLIES (ZEROP X)
                 (EQUAL (TIMES X Y) (TIMES Y X))).

  This simplifies, applying TIMES-ZERO2, and opening up the functions ZEROP,
  EQUAL, and TIMES, to:

        (IMPLIES (EQUAL X 0)
                 (EQUAL 0 (TIMES Y 0))).

  This again simplifies, obviously, to:

        (EQUAL 0 (TIMES Y 0)),

  which we will name *1.1.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (TIMES (SUB1 X) Y)
                             (TIMES Y (SUB1 X))))
                 (EQUAL (TIMES X Y) (TIMES Y X))).

  This simplifies, unfolding the definitions of ZEROP and TIMES, to the new
  goal:

        (IMPLIES (AND (NOT (EQUAL X 0))
                      (NUMBERP X)
                      (EQUAL (TIMES (SUB1 X) Y)
                             (TIMES Y (SUB1 X))))
                 (EQUAL (PLUS Y (TIMES Y (SUB1 X)))
                        (TIMES Y X))).

  Applying the lemma SUB1-ELIM, replace X by (ADD1 Z) to eliminate (SUB1 X).
  We employ the type restriction lemma noted when SUB1 was introduced to
  restrict the new variable.  This produces the new goal:

        (IMPLIES (AND (NUMBERP Z)
                      (NOT (EQUAL (ADD1 Z) 0))
                      (EQUAL (TIMES Z Y) (TIMES Y Z)))
                 (EQUAL (PLUS Y (TIMES Y Z))
                        (TIMES Y (ADD1 Z)))),

  which further simplifies, applying the lemma TIMES-ADD1, to:

        T.


     So we now return to:

      (EQUAL 0 (TIMES Y 0)),

which is formula *1.1 above.  We will try to prove it by induction.  There is
only one suggested induction.  We will induct according to the following
scheme:
      (AND (IMPLIES (ZEROP Y) (p Y))
           (IMPLIES (AND (NOT (ZEROP Y)) (p (SUB1 Y)))
                    (p Y))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT Y) decreases according to the well-founded
relation LESSP in each induction step of the scheme.  The above induction
scheme produces two new conjectures:

Case 2. (IMPLIES (ZEROP Y)
                 (EQUAL 0 (TIMES Y 0))),

  which simplifies, unfolding ZEROP, TIMES, and EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP Y))
                      (EQUAL 0 (TIMES (SUB1 Y) 0)))
                 (EQUAL 0 (TIMES Y 0))),

  which simplifies, unfolding the definitions of ZEROP, TIMES, PLUS, and EQUAL,
  to:

        T.


     That finishes the proof of *1.1, which, in turn, finishes the proof of *1.
Q.E.D.


[ 0.0 0.0 0.0 ]

COMMUTATIVITY-OF-TIMES


(PROVE-LEMMA COMMUTATIVITY2-OF-TIMES
             (REWRITE)
             (EQUAL (TIMES X (TIMES Y Z))
                    (TIMES Y (TIMES X Z))))

WARNING:  the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the newly proposed COMMUTATIVITY2-OF-TIMES could!



     Call the conjecture *1.


     Perhaps we can prove it by induction.  Four inductions are suggested by
terms in the conjecture.  They merge into two likely candidate inductions,
both of which are unflawed.  Since both of these are equally likely, we will
choose arbitrarily.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP Y) (p X Y Z))
           (IMPLIES (AND (NOT (ZEROP Y)) (p X (SUB1 Y) Z))
                    (p X Y Z))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to prove that the measure (COUNT Y) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme leads to two new goals:

Case 2. (IMPLIES (ZEROP Y)
                 (EQUAL (TIMES X Y Z) (TIMES Y X Z))),

  which simplifies, applying the lemma COMMUTATIVITY-OF-TIMES, and opening up
  the definitions of ZEROP, EQUAL, and TIMES, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP Y))
                      (EQUAL (TIMES X (SUB1 Y) Z)
                             (TIMES (SUB1 Y) X Z)))
                 (EQUAL (TIMES X Y Z) (TIMES Y X Z))),

  which simplifies, rewriting with DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and
  opening up the functions ZEROP and TIMES, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

COMMUTATIVITY2-OF-TIMES


(PROVE-LEMMA ASSOCIATIVITY-OF-TIMES
             (REWRITE)
             (EQUAL (TIMES (TIMES X Y) Z)
                    (TIMES X (TIMES Y Z))))

WARNING:  the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the newly proposed ASSOCIATIVITY-OF-TIMES could!


This simplifies, rewriting with COMMUTATIVITY-OF-TIMES and
COMMUTATIVITY2-OF-TIMES, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

ASSOCIATIVITY-OF-TIMES


(PROVE-LEMMA EQUAL-TIMES-0
             (REWRITE)
             (EQUAL (EQUAL (TIMES X Y) 0)
                    (OR (ZEROP X) (ZEROP Y))))

This simplifies, opening up the functions ZEROP and OR, to five new
conjectures:

Case 5. (IMPLIES (NOT (EQUAL (TIMES X Y) 0))
                 (NUMBERP Y)),

  which again simplifies, applying TIMES-ZERO2, and unfolding the function
  EQUAL, to:

        T.

Case 4. (IMPLIES (NOT (EQUAL (TIMES X Y) 0))
                 (NOT (EQUAL Y 0))).

  However this again simplifies, applying COMMUTATIVITY-OF-TIMES, and
  unfolding the functions EQUAL and TIMES, to:

        T.

Case 3. (IMPLIES (NOT (EQUAL (TIMES X Y) 0))
                 (NUMBERP X)).

  This again simplifies, opening up the definitions of TIMES and EQUAL, to:

        T.

Case 2. (IMPLIES (NOT (EQUAL (TIMES X Y) 0))
                 (NOT (EQUAL X 0))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (EQUAL (TIMES X Y) 0)
                      (NOT (EQUAL X 0))
                      (NUMBERP X)
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))),

  which we will name *1.


     Perhaps we can prove it by induction.  There is only one plausible
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p Y X))
           (IMPLIES (AND (NOT (ZEROP X)) (p Y (SUB1 X)))
                    (p Y X))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to establish that the measure (COUNT X) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme produces three new conjectures:

Case 3. (IMPLIES (AND (ZEROP X)
                      (EQUAL (TIMES X Y) 0)
                      (NOT (EQUAL X 0))
                      (NUMBERP X)
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))),

  which simplifies, unfolding the function ZEROP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP X))
                      (NOT (EQUAL (TIMES (SUB1 X) Y) 0))
                      (EQUAL (TIMES X Y) 0)
                      (NOT (EQUAL X 0))
                      (NUMBERP X)
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))),

  which simplifies, rewriting with the lemma PLUS-EQUAL-0, and expanding the
  functions ZEROP and TIMES, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (SUB1 X) 0)
                      (EQUAL (TIMES X Y) 0)
                      (NOT (EQUAL X 0))
                      (NUMBERP X)
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))),

  which simplifies, rewriting with the lemma PLUS-EQUAL-0, and expanding the
  definitions of ZEROP and TIMES, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

EQUAL-TIMES-0


(PROVE-LEMMA EQUAL-LESSP
             (REWRITE)
             (EQUAL (EQUAL (LESSP X Y) Z)
                    (IF (LESSP X Y)
                        (EQUAL T Z)
                        (EQUAL F Z))))

This simplifies, clearly, to the following four new formulas:

Case 4. (IMPLIES (AND (EQUAL (LESSP X Y) Z)
                      (NOT (LESSP X Y)))
                 (NOT Z)).

  This again simplifies, trivially, to:

        T.

Case 3. (IMPLIES (AND (NOT (EQUAL (LESSP X Y) Z))
                      (NOT (LESSP X Y)))
                 Z).

  This again simplifies, clearly, to:

        T.

Case 2. (IMPLIES (AND (NOT (EQUAL (LESSP X Y) Z))
                      (LESSP X Y))
                 (NOT (EQUAL T Z))).

  This again simplifies, obviously, to:

        T.

Case 1. (IMPLIES (AND (EQUAL (LESSP X Y) Z)
                      (LESSP X Y))
                 (EQUAL (EQUAL T Z) T)).

  This again simplifies, obviously, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

EQUAL-LESSP


(PROVE-LEMMA DIFFERENCE-ELIM
             (ELIM)
             (IMPLIES (AND (NUMBERP Y) (NOT (LESSP Y X)))
                      (EQUAL (PLUS X (DIFFERENCE Y X)) Y)))

This conjecture simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-ELIM


(PROVE-LEMMA LESSP-TIMES-1
             (REWRITE)
             (IMPLIES (NOT (ZEROP I))
                      (NOT (LESSP (TIMES I J) J))))

WARNING:  Note that the proposed lemma LESSP-TIMES-1 is to be stored as zero
type prescription rules, zero compound recognizer rules, one linear rule, and
zero replacement rules.


This formula can be simplified, using the abbreviations ZEROP, NOT, and
IMPLIES, to:

      (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I))
               (NOT (LESSP (TIMES I J) J))),

which we will name *1.


     We will appeal to induction.  There are two plausible inductions.
However, only one is unflawed.  We will induct according to the following
scheme:
      (AND (IMPLIES (ZEROP I) (p I J))
           (IMPLIES (AND (NOT (ZEROP I)) (p (SUB1 I) J))
                    (p I J))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to show that the measure (COUNT I) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme produces three new conjectures:

Case 3. (IMPLIES (AND (ZEROP I)
                      (NOT (EQUAL I 0))
                      (NUMBERP I))
                 (NOT (LESSP (TIMES I J) J))),

  which simplifies, opening up the definition of ZEROP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP I))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL I 0))
                      (NUMBERP I))
                 (NOT (LESSP (TIMES I J) J))),

  which simplifies, unfolding the functions ZEROP and TIMES, to the goal:

        (IMPLIES (AND (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL I 0))
                      (NUMBERP I))
                 (NOT (LESSP (PLUS J (TIMES (SUB1 I) J))
                             J))).

  However this again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP I))
                      (NOT (LESSP (TIMES (SUB1 I) J) J))
                      (NOT (EQUAL I 0))
                      (NUMBERP I))
                 (NOT (LESSP (TIMES I J) J))),

  which simplifies, opening up ZEROP and TIMES, to:

        (IMPLIES (AND (NOT (LESSP (TIMES (SUB1 I) J) J))
                      (NOT (EQUAL I 0))
                      (NUMBERP I))
                 (NOT (LESSP (PLUS J (TIMES (SUB1 I) J))
                             J))).

  But this again simplifies, using linear arithmetic, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

LESSP-TIMES-1


(PROVE-LEMMA LESSP-TIMES-2
             (REWRITE)
             (IMPLIES (NOT (ZEROP I))
                      (NOT (LESSP (TIMES J I) J))))

WARNING:  Note that the proposed lemma LESSP-TIMES-2 is to be stored as zero
type prescription rules, zero compound recognizer rules, one linear rule, and
zero replacement rules.


This formula can be simplified, using the abbreviations ZEROP, NOT, and
IMPLIES, to:

      (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I))
               (NOT (LESSP (TIMES J I) J))),

which simplifies, rewriting with the lemma COMMUTATIVITY-OF-TIMES, to:

      (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I))
               (NOT (LESSP (TIMES I J) J))).

But this again simplifies, using linear arithmetic and applying the lemma
LESSP-TIMES-1, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

LESSP-TIMES-2


(PROVE-LEMMA DIFFERENCE-PLUS1
             (REWRITE)
             (EQUAL (DIFFERENCE (PLUS X Y) X)
                    (FIX Y)))

WARNING:  the previously added lemma, DIFFERENCE-PLUS, could be applied
whenever the newly proposed DIFFERENCE-PLUS1 could!


This conjecture simplifies, appealing to the lemma DIFFERENCE-PLUS, and
expanding the function FIX, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-PLUS1


(PROVE-LEMMA DIFFERENCE-PLUS2
             (REWRITE)
             (EQUAL (DIFFERENCE (PLUS Y X) X)
                    (FIX Y)))

WARNING:  the previously added lemma, DIFFERENCE-PLUS, could be applied
whenever the newly proposed DIFFERENCE-PLUS2 could!


This conjecture simplifies, appealing to the lemmas COMMUTATIVITY-OF-PLUS and
DIFFERENCE-PLUS1, and expanding the function FIX, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-PLUS2


(PROVE-LEMMA DIFFERENCE-PLUS-CANCELATION
             (REWRITE)
             (EQUAL (DIFFERENCE (PLUS X Y) (PLUS X Z))
                    (DIFFERENCE Y Z)))

This simplifies, using linear arithmetic, to the following two new conjectures:

Case 2. (IMPLIES (LESSP (PLUS X Y) (PLUS X Z))
                 (EQUAL (DIFFERENCE (PLUS X Y) (PLUS X Z))
                        (DIFFERENCE Y Z))).

  But this again simplifies, using linear arithmetic, applying DIFFERENCE-0,
  and opening up the function EQUAL, to:

        T.

Case 1. (IMPLIES (LESSP Y Z)
                 (EQUAL (DIFFERENCE (PLUS X Y) (PLUS X Z))
                        (DIFFERENCE Y Z))).

  But this again simplifies, using linear arithmetic, applying the lemma
  DIFFERENCE-0, and expanding EQUAL, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-PLUS-CANCELATION


(PROVE-LEMMA TIMES-DIFFERENCE
             (REWRITE)
             (EQUAL (TIMES X (DIFFERENCE C W))
                    (DIFFERENCE (TIMES C X) (TIMES W X))))

WARNING:  the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the newly proposed TIMES-DIFFERENCE could!


.

Appealing to the lemma DIFFERENCE-ELIM, we now replace C by (PLUS W Z) to
eliminate (DIFFERENCE C W).  We use the type restriction lemma noted when
DIFFERENCE was introduced to constrain the new variable.  The result is three
new goals:

Case 3. (IMPLIES (LESSP C W)
                 (EQUAL (TIMES X (DIFFERENCE C W))
                        (DIFFERENCE (TIMES C X)
                                    (TIMES W X)))),

  which simplifies, using linear arithmetic, appealing to the lemmas
  DIFFERENCE-0, COMMUTATIVITY-OF-TIMES, and EQUAL-DIFFERENCE-0, and unfolding
  EQUAL and TIMES, to:

        (IMPLIES (LESSP C W)
                 (NOT (LESSP (TIMES W X) (TIMES C X)))),

  which we would usually push and work on later by induction.  But if we must
  use induction to prove the input conjecture, we prefer to induct on the
  original formulation of the problem.  Thus we will disregard all that we
  have previously done, give the name *1 to the original input, and work on it.


     So now let us consider:

(EQUAL (TIMES X (DIFFERENCE C W))
       (DIFFERENCE (TIMES C X) (TIMES W X))),

which we named *1 above.  We will appeal to induction.  There are five
plausible inductions.  They merge into two likely candidate inductions.
However, only one is unflawed.  We will induct according to the following
scheme:
      (AND (IMPLIES (ZEROP C) (p X C W))
           (IMPLIES (AND (NOT (ZEROP C)) (ZEROP W))
                    (p X C W))
           (IMPLIES (AND (NOT (ZEROP C))
                         (NOT (ZEROP W))
                         (p X (SUB1 C) (SUB1 W)))
                    (p X C W))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT C) decreases according to the well-founded
relation LESSP in each induction step of the scheme.  Note, however, the
inductive instance chosen for W.  The above induction scheme produces the
following three new goals:

Case 3. (IMPLIES (ZEROP C)
                 (EQUAL (TIMES X (DIFFERENCE C W))
                        (DIFFERENCE (TIMES C X)
                                    (TIMES W X)))).

  This simplifies, using linear arithmetic, rewriting with DIFFERENCE-0 and
  COMMUTATIVITY-OF-TIMES, and unfolding the functions ZEROP, EQUAL, and TIMES,
  to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP C)) (ZEROP W))
                 (EQUAL (TIMES X (DIFFERENCE C W))
                        (DIFFERENCE (TIMES C X)
                                    (TIMES W X)))),

  which simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES,
  PLUS-EQUAL-0, and EQUAL-TIMES-0, and unfolding the functions ZEROP, EQUAL,
  DIFFERENCE, and TIMES, to four new conjectures:

  Case 2.4.
          (IMPLIES (AND (NOT (EQUAL C 0))
                        (NUMBERP C)
                        (EQUAL W 0)
                        (NOT (NUMBERP X)))
                   (EQUAL (PLUS X (TIMES (SUB1 C) X))
                          0)),

    which again simplifies, applying EQUAL-TIMES-0, and opening up the
    function PLUS, to:

          T.

  Case 2.3.
          (IMPLIES (AND (NOT (EQUAL C 0))
                        (NUMBERP C)
                        (EQUAL W 0)
                        (EQUAL X 0))
                   (EQUAL (PLUS X (TIMES (SUB1 C) X))
                          0)).

    But this again simplifies, applying COMMUTATIVITY-OF-TIMES, and expanding
    the functions EQUAL, TIMES, and PLUS, to:

          T.

  Case 2.2.
          (IMPLIES (AND (NOT (EQUAL C 0))
                        (NUMBERP C)
                        (NOT (NUMBERP W))
                        (NOT (NUMBERP X)))
                   (EQUAL (PLUS X (TIMES (SUB1 C) X))
                          0)).

    This again simplifies, applying EQUAL-TIMES-0, and unfolding the
    definition of PLUS, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NOT (EQUAL C 0))
                        (NUMBERP C)
                        (NOT (NUMBERP W))
                        (EQUAL X 0))
                   (EQUAL (PLUS X (TIMES (SUB1 C) X))
                          0)).

    However this again simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and
    expanding the definitions of EQUAL, TIMES, and PLUS, to:

          T.

Case 1. (IMPLIES (AND (NOT (ZEROP C))
                      (NOT (ZEROP W))
                      (EQUAL (TIMES X
                                    (DIFFERENCE (SUB1 C) (SUB1 W)))
                             (DIFFERENCE (TIMES (SUB1 C) X)
                                         (TIMES (SUB1 W) X))))
                 (EQUAL (TIMES X (DIFFERENCE C W))
                        (DIFFERENCE (TIMES C X)
                                    (TIMES W X)))).

  This simplifies, rewriting with DIFFERENCE-PLUS-CANCELATION, and unfolding
  the definitions of ZEROP, DIFFERENCE, and TIMES, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

TIMES-DIFFERENCE


(PROVE-LEMMA DIFFERENCE-PLUS3
             (REWRITE)
             (EQUAL (DIFFERENCE (PLUS B (PLUS A C)) A)
                    (PLUS B C)))

This simplifies, using linear arithmetic, to:

      (IMPLIES (LESSP (PLUS B A C) A)
               (EQUAL (DIFFERENCE (PLUS B A C) A)
                      (PLUS B C))),

which again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-PLUS3


(PROVE-LEMMA DIFFERENCE-ADD1-CANCELLATION
             (REWRITE)
             (EQUAL (DIFFERENCE (ADD1 (PLUS Y Z)) Z)
                    (ADD1 Y)))

This conjecture simplifies, using linear arithmetic, to:

      (IMPLIES (LESSP (ADD1 (PLUS Y Z)) Z)
               (EQUAL (DIFFERENCE (ADD1 (PLUS Y Z)) Z)
                      (ADD1 Y))),

which again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIFFERENCE-ADD1-CANCELLATION


(PROVE-LEMMA LESSP-PLUS-CANCELATION
             (REWRITE)
             (EQUAL (LESSP (PLUS X Y) (PLUS X Z))
                    (LESSP Y Z)))

This simplifies, rewriting with EQUAL-LESSP, to two new formulas:

Case 2. (IMPLIES (NOT (LESSP (PLUS X Y) (PLUS X Z)))
                 (NOT (LESSP Y Z))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (LESSP (PLUS X Y) (PLUS X Z))
                 (LESSP Y Z)),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

LESSP-PLUS-CANCELATION


(PROVE-LEMMA LESSP-TIMES-CANCELLATION
             (REWRITE)
             (EQUAL (LESSP (TIMES X Z) (TIMES Y Z))
                    (AND (NOT (ZEROP Z)) (LESSP X Y))))

This conjecture simplifies, rewriting with EQUAL-LESSP, and expanding the
definitions of ZEROP, NOT, and AND, to the following four new goals:

Case 4. (IMPLIES (AND (NOT (LESSP (TIMES X Z) (TIMES Y Z)))
                      (NOT (EQUAL Z 0))
                      (NUMBERP Z))
                 (NOT (LESSP X Y))).

  Call the above conjecture *1.

Case 3. (IMPLIES (LESSP (TIMES X Z) (TIMES Y Z))
                 (LESSP X Y)),

  which we would usually push and work on later by induction.  But if we must
  use induction to prove the input conjecture, we prefer to induct on the
  original formulation of the problem.  Thus we will disregard all that we
  have previously done, give the name *1 to the original input, and work on it.


     So now let us consider:

(EQUAL (LESSP (TIMES X Z) (TIMES Y Z))
       (AND (NOT (ZEROP Z)) (LESSP X Y))).

We gave this the name *1 above.  Perhaps we can prove it by induction.  The
recursive terms in the conjecture suggest four inductions.  However, they
merge into one likely candidate induction.  We will induct according to the
following scheme:
      (AND (IMPLIES (ZEROP X) (p X Z Y))
           (IMPLIES (AND (NOT (ZEROP X))
                         (p (SUB1 X) Z (SUB1 Y)))
                    (p X Z Y))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to show that the measure (COUNT X) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  Note,
however, the inductive instance chosen for Y.  The above induction scheme
produces two new conjectures:

Case 2. (IMPLIES (ZEROP X)
                 (EQUAL (LESSP (TIMES X Z) (TIMES Y Z))
                        (AND (NOT (ZEROP Z)) (LESSP X Y)))),

  which simplifies, expanding ZEROP, EQUAL, TIMES, LESSP, NOT, and AND, to ten
  new conjectures:

  Case 2.10.
          (IMPLIES (AND (EQUAL X 0)
                        (EQUAL Z 0)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y))
                   (EQUAL (PLUS Z (TIMES (SUB1 Y) Z))
                          0)),

    which again simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and
    expanding the functions EQUAL, TIMES, and PLUS, to:

          T.

  Case 2.9.
          (IMPLIES (AND (EQUAL X 0)
                        (NOT (NUMBERP Z))
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y))
                   (EQUAL (PLUS Z (TIMES (SUB1 Y) Z))
                          0)).

    This again simplifies, applying EQUAL-TIMES-0, and opening up the
    definition of PLUS, to:

          T.

  Case 2.8.
          (IMPLIES (AND (EQUAL X 0)
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (NOT (EQUAL Y 0))
                        (EQUAL (PLUS Z (TIMES (SUB1 Y) Z)) 0))
                   (EQUAL F (NUMBERP Y))).

    But this again simplifies, using linear arithmetic, to:

          T.

  Case 2.7.
          (IMPLIES (AND (EQUAL X 0)
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (NOT (EQUAL Y 0))
                        (NOT (NUMBERP Y)))
                   (EQUAL F (NUMBERP Y))),

    which again simplifies, trivially, to:

          T.

  Case 2.6.
          (IMPLIES (AND (EQUAL X 0)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL (PLUS Z (TIMES (SUB1 Y) Z))
                                    0)))
                   (EQUAL T (NUMBERP Y))).

    This again simplifies, obviously, to:

          T.

  Case 2.5.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (EQUAL Z 0)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y))
                   (EQUAL (PLUS Z (TIMES (SUB1 Y) Z))
                          0)).

    However this again simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and
    expanding EQUAL, TIMES, and PLUS, to:

          T.

  Case 2.4.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (NOT (NUMBERP Z))
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y))
                   (EQUAL (PLUS Z (TIMES (SUB1 Y) Z))
                          0)).

    However this again simplifies, applying the lemma EQUAL-TIMES-0, and
    expanding PLUS, to:

          T.

  Case 2.3.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (NOT (EQUAL Y 0))
                        (EQUAL (PLUS Z (TIMES (SUB1 Y) Z)) 0))
                   (EQUAL F (NUMBERP Y))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 2.2.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (NOT (EQUAL Y 0))
                        (NOT (NUMBERP Y)))
                   (EQUAL F (NUMBERP Y))),

    which again simplifies, clearly, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL (PLUS Z (TIMES (SUB1 Y) Z))
                                    0)))
                   (EQUAL T (NUMBERP Y))).

    This again simplifies, clearly, to:

          T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (LESSP (TIMES (SUB1 X) Z)
                                    (TIMES (SUB1 Y) Z))
                             (AND (NOT (ZEROP Z))
                                  (LESSP (SUB1 X) (SUB1 Y)))))
                 (EQUAL (LESSP (TIMES X Z) (TIMES Y Z))
                        (AND (NOT (ZEROP Z)) (LESSP X Y)))).

  This simplifies, applying EQUAL-LESSP, TIMES-ZERO2, and
  COMMUTATIVITY-OF-TIMES, and unfolding the definitions of ZEROP, NOT, AND,
  TIMES, LESSP, and EQUAL, to six new goals:

  Case 1.6.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (LESSP (TIMES (SUB1 X) Z)
                                    (TIMES (SUB1 Y) Z)))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y))
                   (NOT (LESSP (PLUS Z (TIMES (SUB1 X) Z))
                               (PLUS Z (TIMES (SUB1 Y) Z))))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.5.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (LESSP (TIMES (SUB1 X) Z)
                                    (TIMES (SUB1 Y) Z)))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (EQUAL Y 0))
                   (NOT (LESSP (PLUS Z (TIMES (SUB1 X) Z))
                               0))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.4.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (LESSP (TIMES (SUB1 X) Z)
                                    (TIMES (SUB1 Y) Z)))
                        (NOT (LESSP (SUB1 X) (SUB1 Y)))
                        (NOT (NUMBERP Y)))
                   (NOT (LESSP (PLUS Z (TIMES (SUB1 X) Z))
                               0))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.3.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (LESSP (TIMES (SUB1 X) Z)
                               (TIMES (SUB1 Y) Z))
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (LESSP (SUB1 X) (SUB1 Y))
                        (NOT (NUMBERP Y)))
                   (NOT (LESSP (PLUS Z (TIMES (SUB1 X) Z))
                               0))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (LESSP (TIMES (SUB1 X) Z)
                               (TIMES (SUB1 Y) Z))
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (LESSP (SUB1 X) (SUB1 Y))
                        (EQUAL Y 0))
                   (NOT (LESSP (PLUS Z (TIMES (SUB1 X) Z))
                               0))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (LESSP (TIMES (SUB1 X) Z)
                               (TIMES (SUB1 Y) Z))
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (LESSP (SUB1 X) (SUB1 Y))
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y))
                   (LESSP (PLUS Z (TIMES (SUB1 X) Z))
                          (PLUS Z (TIMES (SUB1 Y) Z)))),

    which again simplifies, using linear arithmetic, to:

          T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.1 0.0 ]

LESSP-TIMES-CANCELLATION


(PROVE-LEMMA LESSP-PLUS-CANCELLATION3
             (REWRITE)
             (EQUAL (LESSP Y (PLUS X Y))
                    (NOT (ZEROP X))))

This conjecture simplifies, applying EQUAL-LESSP, and unfolding the functions
ZEROP and NOT, to three new goals:

Case 3. (IMPLIES (AND (NOT (LESSP Y (PLUS X Y)))
                      (NOT (EQUAL X 0)))
                 (NOT (NUMBERP X))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 2. (IMPLIES (LESSP Y (PLUS X Y))
                 (NUMBERP X)),

  which again simplifies, expanding PLUS, to two new conjectures:

  Case 2.2.
          (IMPLIES (AND (NOT (NUMBERP Y)) (LESSP Y 0))
                   (NUMBERP X)),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NUMBERP Y) (LESSP Y Y))
                   (NUMBERP X)),

    which again simplifies, using linear arithmetic, to:

          T.

Case 1. (IMPLIES (LESSP Y (PLUS X Y))
                 (NOT (EQUAL X 0))),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

LESSP-PLUS-CANCELLATION3


(PROVE-LEMMA TIMES-ID-IFF-1
             (REWRITE)
             (EQUAL (EQUAL Z (TIMES W Z))
                    (AND (NUMBERP Z)
                         (OR (EQUAL Z 0) (EQUAL W 1)))))

This conjecture simplifies, expanding the functions OR and AND, to the
following four new formulas:

Case 4. (IMPLIES (AND (EQUAL Z (TIMES W Z))
                      (NOT (EQUAL Z 0)))
                 (EQUAL (EQUAL W 1) T)).

  This again simplifies, clearly, to the new conjecture:

        (IMPLIES (AND (EQUAL Z (TIMES W Z))
                      (NOT (EQUAL Z 0)))
                 (EQUAL W 1)).

  We use the above equality hypothesis by substituting (TIMES W Z) for Z and
  keeping the equality hypothesis.  The result is:

        (IMPLIES (AND (EQUAL Z (TIMES W Z))
                      (NOT (EQUAL (TIMES W Z) 0)))
                 (EQUAL W 1)).

  This further simplifies, obviously, to:

        (IMPLIES (AND (EQUAL Z (TIMES W Z))
                      (NOT (EQUAL Z 0)))
                 (EQUAL W 1)),

  which we would normally push and work on later by induction.  But if we must
  use induction to prove the input conjecture, we prefer to induct on the
  original formulation of the problem.  Thus we will disregard all that we
  have previously done, give the name *1 to the original input, and work on it.


     So now let us return to:

(EQUAL (EQUAL Z (TIMES W Z))
       (AND (NUMBERP Z)
            (OR (EQUAL Z 0) (EQUAL W 1)))),

named *1.  Let us appeal to the induction principle.  There is only one
suggested induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP W) (p Z W))
           (IMPLIES (AND (NOT (ZEROP W)) (p Z (SUB1 W)))
                    (p Z W))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT W) decreases according to the well-founded relation
LESSP in each induction step of the scheme.  The above induction scheme
produces two new goals:

Case 2. (IMPLIES (ZEROP W)
                 (EQUAL (EQUAL Z (TIMES W Z))
                        (AND (NUMBERP Z)
                             (OR (EQUAL Z 0) (EQUAL W 1))))),

  which simplifies, expanding the functions ZEROP, EQUAL, TIMES, OR, and AND,
  to four new formulas:

  Case 2.4.
          (IMPLIES (AND (EQUAL W 0) (EQUAL Z 0))
                   (EQUAL (EQUAL Z 0) T)),

    which again simplifies, unfolding EQUAL, to:

          T.

  Case 2.3.
          (IMPLIES (AND (EQUAL W 0) (EQUAL Z 0))
                   (NUMBERP Z)),

    which again simplifies, clearly, to:

          T.

  Case 2.2.
          (IMPLIES (AND (NOT (NUMBERP W)) (EQUAL Z 0))
                   (EQUAL (EQUAL Z 0) T)).

    This again simplifies, opening up EQUAL, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NOT (NUMBERP W)) (EQUAL Z 0))
                   (NUMBERP Z)),

    which again simplifies, trivially, to:

          T.

Case 1. (IMPLIES (AND (NOT (ZEROP W))
                      (EQUAL (EQUAL Z (TIMES (SUB1 W) Z))
                             (AND (NUMBERP Z)
                                  (OR (EQUAL Z 0) (EQUAL (SUB1 W) 1)))))
                 (EQUAL (EQUAL Z (TIMES W Z))
                        (AND (NUMBERP Z)
                             (OR (EQUAL Z 0) (EQUAL W 1))))).

  This simplifies, applying TIMES-ZERO2 and COMMUTATIVITY-OF-TIMES, and
  expanding ZEROP, OR, AND, TIMES, EQUAL, and NUMBERP, to six new goals:

  Case 1.6.
          (IMPLIES (AND (NOT (EQUAL W 0))
                        (NUMBERP W)
                        (EQUAL Z (TIMES (SUB1 W) Z))
                        (NUMBERP Z)
                        (EQUAL (EQUAL (SUB1 W) 1) T)
                        (NOT (EQUAL Z (PLUS Z Z))))
                   (NOT (EQUAL Z 0))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.5.
          (IMPLIES (AND (NOT (EQUAL W 0))
                        (NUMBERP W)
                        (EQUAL Z (TIMES (SUB1 W) Z))
                        (NUMBERP Z)
                        (EQUAL (EQUAL (SUB1 W) 1) T)
                        (NOT (EQUAL Z (PLUS Z Z))))
                   (NOT (EQUAL W 1))),

    which again simplifies, opening up the definitions of EQUAL, NUMBERP, SUB1,
    and TIMES, to:

          T.

  Case 1.4.
          (IMPLIES (AND (NOT (EQUAL W 0))
                        (NUMBERP W)
                        (EQUAL Z (TIMES (SUB1 W) Z))
                        (NUMBERP Z)
                        (EQUAL (EQUAL (SUB1 W) 1) T)
                        (EQUAL Z (PLUS Z Z))
                        (NOT (EQUAL Z 0)))
                   (EQUAL (EQUAL W 1) T)),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.3.
          (IMPLIES (AND (NOT (EQUAL W 0))
                        (NUMBERP W)
                        (NOT (EQUAL Z (TIMES (SUB1 W) Z)))
                        (NOT (EQUAL Z 0))
                        (NOT (EQUAL (SUB1 W) 1))
                        (EQUAL Z (PLUS Z (TIMES (SUB1 W) Z))))
                   (EQUAL (EQUAL W 1) T)),

    which again simplifies, obviously, to the new formula:

          (IMPLIES (AND (NOT (EQUAL W 0))
                        (NUMBERP W)
                        (NOT (EQUAL Z (TIMES (SUB1 W) Z)))
                        (NOT (EQUAL Z 0))
                        (NOT (EQUAL (SUB1 W) 1))
                        (EQUAL Z (PLUS Z (TIMES (SUB1 W) Z))))
                   (EQUAL W 1)),

    which again simplifies, using linear arithmetic and applying LESSP-TIMES-2,
    to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL W 0))
                        (NUMBERP W)
                        (NOT (EQUAL Z (TIMES (SUB1 W) Z)))
                        (NOT (EQUAL Z 0))
                        (NOT (EQUAL (SUB1 W) 1))
                        (NOT (EQUAL Z (PLUS Z (TIMES (SUB1 W) Z))))
                        (NUMBERP Z))
                   (NOT (EQUAL W 1))).

    However this again simplifies, rewriting with the lemma
    COMMUTATIVITY-OF-PLUS, and unfolding EQUAL, NUMBERP, SUB1, TIMES, and PLUS,
    to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL W 0))
                        (NUMBERP W)
                        (NOT (EQUAL Z (TIMES (SUB1 W) Z)))
                        (NOT (EQUAL Z 0))
                        (NOT (EQUAL (SUB1 W) 1))
                        (EQUAL Z (PLUS Z (TIMES (SUB1 W) Z))))
                   (NUMBERP Z)),

    which again simplifies, clearly, to:

          T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

TIMES-ID-IFF-1


(PROVE-LEMMA TIMES-IDENTITY1
             (REWRITE)
             (IMPLIES (AND (NUMBERP Y)
                           (NOT (EQUAL Y 1))
                           (NOT (EQUAL Y 0))
                           (NOT (EQUAL X 0)))
                      (NOT (EQUAL X (TIMES X Y)))))

.

We now use the above equality hypothesis by substituting (TIMES X Y) for X and
keeping the equality hypothesis.  This generates:

      (IMPLIES (AND (NUMBERP Y)
                    (NOT (EQUAL Y 1))
                    (NOT (EQUAL Y 0))
                    (NOT (EQUAL (TIMES X Y) 0)))
               (NOT (EQUAL X (TIMES X Y)))).

This simplifies, clearly, to:

      (IMPLIES (AND (NUMBERP Y)
                    (NOT (EQUAL Y 1))
                    (NOT (EQUAL Y 0))
                    (NOT (EQUAL X 0)))
               (NOT (EQUAL X (TIMES X Y)))),

which we would normally push and work on later by induction.  But if we must
use induction to prove the input conjecture, we prefer to induct on the
original formulation of the problem.  Thus we will disregard all that we have
previously done, give the name *1 to the original input, and work on it.


     So now let us return to:

(IMPLIES (AND (NUMBERP Y)
              (NOT (EQUAL Y 1))
              (NOT (EQUAL Y 0))
              (NOT (EQUAL X 0)))
         (NOT (EQUAL X (TIMES X Y)))),

named *1.  Let us appeal to the induction principle.  There is only one
suggested induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p X Y))
           (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y))
                    (p X Y))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT X) decreases according to the well-founded relation
LESSP in each induction step of the scheme.  The above induction scheme
generates three new conjectures:

Case 3. (IMPLIES (AND (ZEROP X)
                      (NUMBERP Y)
                      (NOT (EQUAL Y 1))
                      (NOT (EQUAL Y 0))
                      (NOT (EQUAL X 0)))
                 (NOT (EQUAL X (TIMES X Y)))),

  which simplifies, unfolding the definition of ZEROP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (SUB1 X) 0)
                      (NUMBERP Y)
                      (NOT (EQUAL Y 1))
                      (NOT (EQUAL Y 0))
                      (NOT (EQUAL X 0)))
                 (NOT (EQUAL X (TIMES X Y)))),

  which simplifies, opening up ZEROP and TIMES, to:

        (IMPLIES (AND (EQUAL (SUB1 X) 0)
                      (NUMBERP Y)
                      (NOT (EQUAL Y 1))
                      (NOT (EQUAL Y 0))
                      (NOT (EQUAL X 0))
                      (NUMBERP X))
                 (NOT (EQUAL X
                             (PLUS Y (TIMES (SUB1 X) Y))))).

  But this again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (NOT (EQUAL (SUB1 X) (TIMES (SUB1 X) Y)))
                      (NUMBERP Y)
                      (NOT (EQUAL Y 1))
                      (NOT (EQUAL Y 0))
                      (NOT (EQUAL X 0)))
                 (NOT (EQUAL X (TIMES X Y)))),

  which simplifies, expanding the functions ZEROP and TIMES, to the formula:

        (IMPLIES (AND (NOT (EQUAL (SUB1 X) (TIMES (SUB1 X) Y)))
                      (NUMBERP Y)
                      (NOT (EQUAL Y 1))
                      (NOT (EQUAL Y 0))
                      (NOT (EQUAL X 0))
                      (NUMBERP X))
                 (NOT (EQUAL X
                             (PLUS Y (TIMES (SUB1 X) Y))))).

  However this again simplifies, using linear arithmetic and rewriting with
  the lemma LESSP-TIMES-2, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

TIMES-IDENTITY1


(PROVE-LEMMA TIMES-IDENTITY
             (REWRITE)
             (EQUAL (EQUAL X (TIMES X Y))
                    (OR (EQUAL X 0)
                        (AND (NUMBERP X) (EQUAL Y 1)))))

This conjecture simplifies, expanding the functions AND and OR, to the
following four new formulas:

Case 4. (IMPLIES (AND (EQUAL X (TIMES X Y))
                      (NOT (EQUAL X 0)))
                 (EQUAL (EQUAL Y 1) T)).

  This again simplifies, clearly, to the new conjecture:

        (IMPLIES (AND (EQUAL X (TIMES X Y))
                      (NOT (EQUAL X 0)))
                 (EQUAL Y 1)).

  We use the above equality hypothesis by substituting (TIMES X Y) for X and
  keeping the equality hypothesis.  The result is:

        (IMPLIES (AND (EQUAL X (TIMES X Y))
                      (NOT (EQUAL (TIMES X Y) 0)))
                 (EQUAL Y 1)).

  This further simplifies, obviously, to:

        (IMPLIES (AND (EQUAL X (TIMES X Y))
                      (NOT (EQUAL X 0)))
                 (EQUAL Y 1)),

  which we would normally push and work on later by induction.  But if we must
  use induction to prove the input conjecture, we prefer to induct on the
  original formulation of the problem.  Thus we will disregard all that we
  have previously done, give the name *1 to the original input, and work on it.


     So now let us return to:

(EQUAL (EQUAL X (TIMES X Y))
       (OR (EQUAL X 0)
           (AND (NUMBERP X) (EQUAL Y 1)))),

named *1.  Let us appeal to the induction principle.  There is only one
suggested induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p X Y))
           (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y))
                    (p X Y))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT X) decreases according to the well-founded relation
LESSP in each induction step of the scheme.  The above induction scheme
produces two new goals:

Case 2. (IMPLIES (ZEROP X)
                 (EQUAL (EQUAL X (TIMES X Y))
                        (OR (EQUAL X 0)
                            (AND (NUMBERP X) (EQUAL Y 1))))),

  which simplifies, expanding the functions ZEROP, EQUAL, TIMES, NUMBERP, AND,
  and OR, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (EQUAL (SUB1 X) (TIMES (SUB1 X) Y))
                             (OR (EQUAL (SUB1 X) 0)
                                 (AND (NUMBERP (SUB1 X))
                                      (EQUAL Y 1)))))
                 (EQUAL (EQUAL X (TIMES X Y))
                        (OR (EQUAL X 0)
                            (AND (NUMBERP X) (EQUAL Y 1))))),

  which simplifies, unfolding ZEROP, AND, OR, and TIMES, to four new formulas:

  Case 1.4.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (EQUAL (SUB1 X) (TIMES (SUB1 X) Y))
                        (EQUAL (EQUAL Y 1) T))
                   (EQUAL X (PLUS Y (SUB1 X)))),

    which again simplifies, applying ADD1-SUB1, and opening up the definitions
    of SUB1, NUMBERP, EQUAL, and PLUS, to:

          T.

  Case 1.3.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (NOT (EQUAL (SUB1 X) (TIMES (SUB1 X) Y)))
                        (NOT (EQUAL (SUB1 X) 0))
                        (NOT (EQUAL Y 1)))
                   (NOT (EQUAL X
                               (PLUS Y (TIMES (SUB1 X) Y))))).

    This again simplifies, clearly, to:

          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NOT (EQUAL (SUB1 X) (TIMES (SUB1 X) Y)))
                        (NOT (EQUAL (SUB1 X) 0))
                        (NOT (EQUAL Y 1)))
                   (NOT (EQUAL X
                               (PLUS Y (TIMES (SUB1 X) Y))))),

    which further simplifies, rewriting with COMMUTATIVITY-OF-TIMES and
    TIMES-ID-IFF-1, to:

          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NOT (EQUAL (SUB1 X) 0))
                        (NOT (EQUAL Y 1)))
                   (NOT (EQUAL X
                               (PLUS Y (TIMES Y (SUB1 X)))))).

    Applying the lemma SUB1-ELIM, replace X by (ADD1 Z) to eliminate (SUB1 X).
    We employ the type restriction lemma noted when SUB1 was introduced to
    restrict the new variable.  This produces the following two new
    conjectures:

    Case 1.3.2.
            (IMPLIES (AND (NOT (NUMBERP X))
                          (NOT (EQUAL X 0))
                          (NOT (EQUAL (SUB1 X) 0))
                          (NOT (EQUAL Y 1)))
                     (NOT (EQUAL X
                                 (PLUS Y (TIMES Y (SUB1 X)))))).

      This further simplifies, clearly, to:

            T.

    Case 1.3.1.
            (IMPLIES (AND (NUMBERP Z)
                          (NOT (EQUAL (ADD1 Z) 0))
                          (NOT (EQUAL Z 0))
                          (NOT (EQUAL Y 1)))
                     (NOT (EQUAL (ADD1 Z)
                                 (PLUS Y (TIMES Y Z))))).

      This further simplifies, obviously, to the new formula:

            (IMPLIES (AND (NUMBERP Z)
                          (NOT (EQUAL Z 0))
                          (NOT (EQUAL Y 1)))
                     (NOT (EQUAL (ADD1 Z)
                                 (PLUS Y (TIMES Y Z))))),

      which we will finally name *1.1.

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (EQUAL (SUB1 X) (TIMES (SUB1 X) Y))
                        (EQUAL (SUB1 X) 0)
                        (NOT (EQUAL Y 1)))
                   (NOT (EQUAL X (PLUS Y (SUB1 X))))).

    This again simplifies, using linear arithmetic, to:

          (IMPLIES (AND (NOT (NUMBERP Y))
                        (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (EQUAL 0 (TIMES 0 Y))
                        (EQUAL (SUB1 X) 0)
                        (NOT (EQUAL Y 1)))
                   (NOT (EQUAL X (PLUS Y 0)))).

    But this again simplifies, rewriting with PLUS-RIGHT-ID2 and
    COMMUTATIVITY-OF-PLUS, and unfolding the definitions of NUMBERP and EQUAL,
    to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (EQUAL (SUB1 X) (TIMES (SUB1 X) Y))
                        (EQUAL (SUB1 X) 0)
                        (EQUAL Y 1))
                   (EQUAL (EQUAL X (PLUS Y (SUB1 X)))
                          T)).

    This again simplifies, unfolding the functions TIMES, EQUAL, and PLUS, to:

          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (EQUAL (SUB1 X) 0))
                   (EQUAL X 1)).

    This again simplifies, using linear arithmetic, to:

          T.


     So let us turn our attention to:

      (IMPLIES (AND (NUMBERP Z)
                    (NOT (EQUAL Z 0))
                    (NOT (EQUAL Y 1)))
               (NOT (EQUAL (ADD1 Z)
                           (PLUS Y (TIMES Y Z))))),

named *1.1 above.  We will try to prove it by induction.  The recursive terms
in the conjecture suggest two inductions.  However, they merge into one likely
candidate induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP Y) (p Z Y))
           (IMPLIES (AND (NOT (ZEROP Y)) (p Z (SUB1 Y)))
                    (p Z Y))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT Y) decreases according to the well-founded
relation LESSP in each induction step of the scheme.  The above induction
scheme generates three new formulas:

Case 3. (IMPLIES (AND (ZEROP Y)
                      (NUMBERP Z)
                      (NOT (EQUAL Z 0))
                      (NOT (EQUAL Y 1)))
                 (NOT (EQUAL (ADD1 Z)
                             (PLUS Y (TIMES Y Z))))),

  which simplifies, applying PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS, and
  expanding the functions ZEROP, EQUAL, TIMES, PLUS, and NUMBERP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP Y))
                      (EQUAL (SUB1 Y) 1)
                      (NUMBERP Z)
                      (NOT (EQUAL Z 0))
                      (NOT (EQUAL Y 1)))
                 (NOT (EQUAL (ADD1 Z)
                             (PLUS Y (TIMES Y Z))))).

  This simplifies, unfolding the functions ZEROP and TIMES, to:

        (IMPLIES (AND (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (EQUAL (SUB1 Y) 1)
                      (NUMBERP Z)
                      (NOT (EQUAL Z 0))
                      (NOT (EQUAL Y 1)))
                 (NOT (EQUAL (ADD1 Z)
                             (PLUS Y Z (TIMES (SUB1 Y) Z))))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP Y))
                      (NOT (EQUAL (ADD1 Z)
                                  (PLUS (SUB1 Y) (TIMES (SUB1 Y) Z))))
                      (NUMBERP Z)
                      (NOT (EQUAL Z 0))
                      (NOT (EQUAL Y 1)))
                 (NOT (EQUAL (ADD1 Z)
                             (PLUS Y (TIMES Y Z))))),

  which simplifies, expanding the definitions of ZEROP and TIMES, to:

        (IMPLIES (AND (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NOT (EQUAL (ADD1 Z)
                                  (PLUS (SUB1 Y) (TIMES (SUB1 Y) Z))))
                      (NUMBERP Z)
                      (NOT (EQUAL Z 0))
                      (NOT (EQUAL Y 1)))
                 (NOT (EQUAL (ADD1 Z)
                             (PLUS Y Z (TIMES (SUB1 Y) Z))))).

  This again simplifies, using linear arithmetic and rewriting with the lemma
  LESSP-TIMES-2, to:

        T.


     That finishes the proof of *1.1, which finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

TIMES-IDENTITY


(PROVE-LEMMA TIMES-EQUAL-1
             (REWRITE)
             (EQUAL (EQUAL (TIMES A B) 1)
                    (AND (NOT (EQUAL A 0))
                         (NOT (EQUAL B 0))
                         (NUMBERP A)
                         (NUMBERP B)
                         (EQUAL (SUB1 A) 0)
                         (EQUAL (SUB1 B) 0))))

This conjecture simplifies, applying COMMUTATIVITY-OF-TIMES, and opening up
the definitions of TIMES, NOT, and AND, to the following five new formulas:

Case 5. (IMPLIES (AND (NOT (EQUAL A 0))
                      (NUMBERP A)
                      (NOT (EQUAL B 0))
                      (NUMBERP B)
                      (EQUAL (PLUS B
                                   (SUB1 A)
                                   (TIMES (SUB1 A) (SUB1 B)))
                             1))
                 (EQUAL (EQUAL (SUB1 B) 0) T)).

  But this again simplifies, using linear arithmetic, to the conjecture:

        (IMPLIES (AND (NOT (EQUAL 1 0))
                      (NUMBERP 1)
                      (NOT (EQUAL B 0))
                      (NUMBERP B)
                      (EQUAL (PLUS B
                                   (SUB1 1)
                                   (TIMES (SUB1 1) (SUB1 B)))
                             1))
                 (EQUAL (EQUAL (SUB1 B) 0) T)).

  This again simplifies, applying the lemma COMMUTATIVITY-OF-PLUS, and opening
  up the functions EQUAL, NUMBERP, SUB1, TIMES, and PLUS, to:

        T.

Case 4. (IMPLIES (AND (NOT (EQUAL A 0))
                      (NUMBERP A)
                      (NOT (EQUAL B 0))
                      (NUMBERP B)
                      (NOT (EQUAL (PLUS B
                                        (SUB1 A)
                                        (TIMES (SUB1 A) (SUB1 B)))
                                  1))
                      (EQUAL (SUB1 A) 0))
                 (NOT (EQUAL (SUB1 B) 0))),

  which again simplifies, rewriting with the lemma COMMUTATIVITY-OF-PLUS, and
  expanding the functions TIMES, PLUS, and EQUAL, to the goal:

        (IMPLIES (AND (NOT (EQUAL A 0))
                      (NUMBERP A)
                      (NOT (EQUAL B 0))
                      (NUMBERP B)
                      (NOT (EQUAL B 1))
                      (EQUAL (SUB1 A) 0))
                 (NOT (EQUAL (SUB1 B) 0))).

  But this again simplifies, using linear arithmetic, to:

        T.

Case 3. (IMPLIES (AND (NOT (EQUAL A 0))
                      (NUMBERP A)
                      (EQUAL B 0))
                 (NOT (EQUAL (PLUS B 0) 1))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 2. (IMPLIES (AND (NOT (EQUAL A 0))
                      (NUMBERP A)
                      (NOT (NUMBERP B)))
                 (NOT (EQUAL (PLUS B 0) 1))),

  which again simplifies, applying PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS,
  and expanding NUMBERP and EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL A 0))
                      (NUMBERP A)
                      (NOT (EQUAL B 0))
                      (NUMBERP B)
                      (EQUAL (PLUS B
                                   (SUB1 A)
                                   (TIMES (SUB1 A) (SUB1 B)))
                             1))
                 (EQUAL (SUB1 A) 0)).

  But this again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

TIMES-EQUAL-1


(PROVE-LEMMA DELETE-NON-MEMBER
             (REWRITE)
             (IMPLIES (NOT (MEMBER X Y))
                      (EQUAL (DELETE X Y) Y)))


     Give the conjecture the name *1.


     We will try to prove it by induction.  There are two plausible inductions.
However, they merge into one likely candidate induction.  We will induct
according to the following scheme:
      (AND (IMPLIES (NLISTP Y) (p X Y))
           (IMPLIES (AND (NOT (NLISTP Y))
                         (EQUAL X (CAR Y)))
                    (p X Y))
           (IMPLIES (AND (NOT (NLISTP Y))
                         (NOT (EQUAL X (CAR Y)))
                         (p X (CDR Y)))
                    (p X Y))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT Y) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme generates four new goals:

Case 4. (IMPLIES (AND (NLISTP Y) (NOT (MEMBER X Y)))
                 (EQUAL (DELETE X Y) Y)),

  which simplifies, expanding NLISTP, MEMBER, and DELETE, to:

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP Y))
                      (EQUAL X (CAR Y))
                      (NOT (MEMBER X Y)))
                 (EQUAL (DELETE X Y) Y)),

  which simplifies, opening up the functions NLISTP and MEMBER, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP Y))
                      (NOT (EQUAL X (CAR Y)))
                      (MEMBER X (CDR Y))
                      (NOT (MEMBER X Y)))
                 (EQUAL (DELETE X Y) Y)),

  which simplifies, opening up the definitions of NLISTP and MEMBER, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP Y))
                      (NOT (EQUAL X (CAR Y)))
                      (EQUAL (DELETE X (CDR Y)) (CDR Y))
                      (NOT (MEMBER X Y)))
                 (EQUAL (DELETE X Y) Y)),

  which simplifies, rewriting with the lemma CONS-CAR-CDR, and unfolding the
  functions NLISTP, MEMBER, and DELETE, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

DELETE-NON-MEMBER


(PROVE-LEMMA MEMBER-DELETE
             (REWRITE)
             (IMPLIES (MEMBER X (DELETE U V))
                      (MEMBER X V)))

WARNING:  Note that MEMBER-DELETE contains the free variable U which will be
chosen by instantiating the hypothesis (MEMBER X (DELETE U V)).



     Give the conjecture the name *1.


     Let us appeal to the induction principle.  Two inductions are suggested
by terms in the conjecture.  However, they merge into one likely candidate
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP V) (EQUAL U (CAR V)))
                    (p X V U))
           (IMPLIES (AND (LISTP V)
                         (NOT (EQUAL U (CAR V)))
                         (p X (CDR V) U))
                    (p X V U))
           (IMPLIES (NOT (LISTP V)) (p X V U))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT V)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  The above induction scheme generates four new conjectures:

Case 4. (IMPLIES (AND (LISTP V)
                      (EQUAL U (CAR V))
                      (MEMBER X (DELETE U V)))
                 (MEMBER X V)),

  which simplifies, expanding the functions DELETE and MEMBER, to:

        T.

Case 3. (IMPLIES (AND (LISTP V)
                      (NOT (EQUAL U (CAR V)))
                      (NOT (MEMBER X (DELETE U (CDR V))))
                      (MEMBER X (DELETE U V)))
                 (MEMBER X V)),

  which simplifies, appealing to the lemmas CDR-CONS and CAR-CONS, and
  expanding DELETE and MEMBER, to:

        T.

Case 2. (IMPLIES (AND (LISTP V)
                      (NOT (EQUAL U (CAR V)))
                      (MEMBER X (CDR V))
                      (MEMBER X (DELETE U V)))
                 (MEMBER X V)),

  which simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS, and
  opening up the functions DELETE and MEMBER, to:

        T.

Case 1. (IMPLIES (AND (NOT (LISTP V))
                      (MEMBER X (DELETE U V)))
                 (MEMBER X V)),

  which simplifies, applying DELETE-NON-MEMBER, and unfolding the definition
  of MEMBER, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

MEMBER-DELETE


(PROVE-LEMMA COMMUTATIVITY-OF-DELETE
             (REWRITE)
             (EQUAL (DELETE X (DELETE Y Z))
                    (DELETE Y (DELETE X Z))))


     Call the conjecture *1.


     Perhaps we can prove it by induction.  Two inductions are suggested by
terms in the conjecture.  However, they merge into one likely candidate
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (AND (LISTP Z) (EQUAL Y (CAR Z)))
                    (p X Y Z))
           (IMPLIES (AND (LISTP Z)
                         (NOT (EQUAL Y (CAR Z)))
                         (p X Y (CDR Z)))
                    (p X Y Z))
           (IMPLIES (NOT (LISTP Z)) (p X Y Z))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT Z) decreases according to the well-founded relation LESSP in
each induction step of the scheme.  The above induction scheme leads to three
new goals:

Case 3. (IMPLIES (AND (LISTP Z) (EQUAL Y (CAR Z)))
                 (EQUAL (DELETE X (DELETE Y Z))
                        (DELETE Y (DELETE X Z)))),

  which simplifies, opening up the definition of DELETE, to two new
  conjectures:

  Case 3.2.
          (IMPLIES (AND (LISTP Z)
                        (NOT (EQUAL X (CAR Z))))
                   (EQUAL (DELETE X (CDR Z))
                          (DELETE (CAR Z)
                                  (CONS (CAR Z) (DELETE X (CDR Z)))))),

    which again simplifies, rewriting with CDR-CONS and CAR-CONS, and opening
    up the function DELETE, to:

          T.

  Case 3.1.
          (IMPLIES (AND (LISTP Z) (EQUAL X (CAR Z)))
                   (EQUAL (DELETE X (CDR Z))
                          (DELETE (CAR Z) (CDR Z)))).

    This again simplifies, obviously, to:

          T.

Case 2. (IMPLIES (AND (LISTP Z)
                      (NOT (EQUAL Y (CAR Z)))
                      (EQUAL (DELETE X (DELETE Y (CDR Z)))
                             (DELETE Y (DELETE X (CDR Z)))))
                 (EQUAL (DELETE X (DELETE Y Z))
                        (DELETE Y (DELETE X Z)))).

  This simplifies, applying CDR-CONS and CAR-CONS, and opening up DELETE, to:

        (IMPLIES (AND (LISTP Z)
                      (NOT (EQUAL Y (CAR Z)))
                      (EQUAL (DELETE X (DELETE Y (CDR Z)))
                             (DELETE Y (DELETE X (CDR Z))))
                      (NOT (EQUAL X (CAR Z))))
                 (EQUAL (CONS (CAR Z)
                              (DELETE X (DELETE Y (CDR Z))))
                        (DELETE Y
                                (CONS (CAR Z) (DELETE X (CDR Z)))))).

  But this again simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS,
  and expanding the definition of DELETE, to:

        T.

Case 1. (IMPLIES (NOT (LISTP Z))
                 (EQUAL (DELETE X (DELETE Y Z))
                        (DELETE Y (DELETE X Z)))),

  which simplifies, applying DELETE-NON-MEMBER, and expanding the definition
  of MEMBER, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

COMMUTATIVITY-OF-DELETE


(PROVE-LEMMA LESSP-COUNT-DELETE
             (REWRITE)
             (IMPLIES (MEMBER N L)
                      (LESSP (COUNT (DELETE N L))
                             (COUNT L))))

WARNING:  Note that the proposed lemma LESSP-COUNT-DELETE is to be stored as
zero type prescription rules, zero compound recognizer rules, one linear rule,
and zero replacement rules.



     Name the conjecture *1.


     Let us appeal to the induction principle.  The recursive terms in the
conjecture suggest two inductions.  However, they merge into one likely
candidate induction.  We will induct according to the following scheme:
      (AND (IMPLIES (NLISTP L) (p N L))
           (IMPLIES (AND (NOT (NLISTP L))
                         (EQUAL N (CAR L)))
                    (p N L))
           (IMPLIES (AND (NOT (NLISTP L))
                         (NOT (EQUAL N (CAR L)))
                         (p N (CDR L)))
                    (p N L))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to show that the measure (COUNT L) decreases according to
the well-founded relation LESSP in each induction step of the scheme.  The
above induction scheme leads to the following four new goals:

Case 4. (IMPLIES (AND (NLISTP L) (MEMBER N L))
                 (LESSP (COUNT (DELETE N L))
                        (COUNT L))).

  This simplifies, expanding the definitions of NLISTP and MEMBER, to:

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP L))
                      (EQUAL N (CAR L))
                      (MEMBER N L))
                 (LESSP (COUNT (DELETE N L))
                        (COUNT L))).

  This simplifies, unfolding NLISTP, MEMBER, and DELETE, to the new formula:

        (IMPLIES (LISTP L)
                 (LESSP (COUNT (CDR L)) (COUNT L))),

  which again simplifies, using linear arithmetic and applying the lemma
  CDR-LESSP, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (EQUAL N (CAR L)))
                      (NOT (MEMBER N (CDR L)))
                      (MEMBER N L))
                 (LESSP (COUNT (DELETE N L))
                        (COUNT L))),

  which simplifies, unfolding the definitions of NLISTP and MEMBER, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (EQUAL N (CAR L)))
                      (LESSP (COUNT (DELETE N (CDR L)))
                             (COUNT (CDR L)))
                      (MEMBER N L))
                 (LESSP (COUNT (DELETE N L))
                        (COUNT L))),

  which simplifies, applying the lemmas COUNT-CONS and SUB1-ADD1, and opening
  up the functions NLISTP, MEMBER, DELETE, and LESSP, to two new goals:

  Case 1.2.
          (IMPLIES (AND (LISTP L)
                        (NOT (EQUAL N (CAR L)))
                        (LESSP (COUNT (DELETE N (CDR L)))
                               (COUNT (CDR L)))
                        (MEMBER N (CDR L)))
                   (NOT (EQUAL (COUNT L) 0))),

    which again simplifies, using linear arithmetic and rewriting with
    CDR-LESSEQP, to:

          T.

  Case 1.1.
          (IMPLIES (AND (LISTP L)
                        (NOT (EQUAL N (CAR L)))
                        (LESSP (COUNT (DELETE N (CDR L)))
                               (COUNT (CDR L)))
                        (MEMBER N (CDR L)))
                   (LESSP (PLUS (COUNT (CAR L))
                                (COUNT (DELETE N (CDR L))))
                          (SUB1 (COUNT L)))).

    Appealing to the lemma CAR-CDR-ELIM, we now replace L by (CONS X Z) to
    eliminate (CAR L) and (CDR L).  We must thus prove:

          (IMPLIES (AND (NOT (EQUAL N X))
                        (LESSP (COUNT (DELETE N Z)) (COUNT Z))
                        (MEMBER N Z))
                   (LESSP (PLUS (COUNT X) (COUNT (DELETE N Z)))
                          (SUB1 (COUNT (CONS X Z))))).

    This further simplifies, applying the lemmas COUNT-CONS, SUB1-ADD1, and
    LESSP-PLUS-CANCELATION, to:

          T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.3 ]

LESSP-COUNT-DELETE


(PROVE-LEMMA REMAINDER-QUOTIENT
             (REWRITE)
             (EQUAL (PLUS (REMAINDER X Y)
                          (TIMES Y (QUOTIENT X Y)))
                    (FIX X)))

WARNING:  the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied
whenever the newly proposed REMAINDER-QUOTIENT could!


This formula simplifies, opening up the function FIX, to the following two new
goals:

Case 2. (IMPLIES (NOT (NUMBERP X))
                 (EQUAL (PLUS (REMAINDER X Y)
                              (TIMES Y (QUOTIENT X Y)))
                        0)).

  However this again simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and
  opening up LESSP, REMAINDER, QUOTIENT, EQUAL, TIMES, and PLUS, to:

        T.

Case 1. (IMPLIES (NUMBERP X)
                 (EQUAL (PLUS (REMAINDER X Y)
                              (TIMES Y (QUOTIENT X Y)))
                        X)).

  Call the above conjecture *1.


     We will appeal to induction.  Three inductions are suggested by terms in
the conjecture.  They merge into two likely candidate inductions.  However,
only one is unflawed.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP Y) (p X Y))
           (IMPLIES (AND (NOT (ZEROP Y)) (LESSP X Y))
                    (p X Y))
           (IMPLIES (AND (NOT (ZEROP Y))
                         (NOT (LESSP X Y))
                         (p (DIFFERENCE X Y) Y))
                    (p X Y))).
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the
definition of ZEROP can be used to show that the measure (COUNT X) decreases
according to the well-founded relation LESSP in each induction step of the
scheme.  The above induction scheme produces three new goals:

Case 3. (IMPLIES (AND (ZEROP Y) (NUMBERP X))
                 (EQUAL (PLUS (REMAINDER X Y)
                              (TIMES Y (QUOTIENT X Y)))
                        X)),

  which simplifies, applying COMMUTATIVITY-OF-PLUS, TIMES-ZERO2, and
  COMMUTATIVITY-OF-TIMES, and unfolding the functions ZEROP, EQUAL, REMAINDER,
  QUOTIENT, TIMES, and PLUS, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP Y))
                      (LESSP X Y)
                      (NUMBERP X))
                 (EQUAL (PLUS (REMAINDER X Y)
                              (TIMES Y (QUOTIENT X Y)))
                        X)).

  This simplifies, rewriting with the lemmas COMMUTATIVITY-OF-TIMES and
  COMMUTATIVITY-OF-PLUS, and opening up the functions ZEROP, REMAINDER,
  QUOTIENT, EQUAL, TIMES, and PLUS, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP Y))
                      (NOT (LESSP X Y))
                      (EQUAL (PLUS (REMAINDER (DIFFERENCE X Y) Y)
                                   (TIMES Y
                                          (QUOTIENT (DIFFERENCE X Y) Y)))
                             (DIFFERENCE X Y))
                      (NUMBERP X))
                 (EQUAL (PLUS (REMAINDER X Y)
                              (TIMES Y (QUOTIENT X Y)))
                        X)).

  This simplifies, rewriting with TIMES-ADD1 and COMMUTATIVITY2-OF-PLUS, and
  opening up the functions ZEROP, REMAINDER, and QUOTIENT, to the goal:

        (IMPLIES (AND (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NOT (LESSP X Y))
                      (EQUAL (PLUS (REMAINDER (DIFFERENCE X Y) Y)
                                   (TIMES Y
                                          (QUOTIENT (DIFFERENCE X Y) Y)))
                             (DIFFERENCE X Y))
                      (NUMBERP X))
                 (EQUAL (PLUS Y (DIFFERENCE X Y)) X)).

  But this again simplifies, using linear arithmetic, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

REMAINDER-QUOTIENT


(PROVE-LEMMA REMAINDER-WRT-1
             (REWRITE)
             (EQUAL (REMAINDER Y 1) 0))


     Call the conjecture *1.


     We will try to prove it by induction.  There is only one suggested
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP 1) (p Y))
           (IMPLIES (AND (NOT (ZEROP 1)) (LESSP Y 1))
                    (p Y))
           (IMPLIES (AND (NOT (ZEROP 1))
                         (NOT (LESSP Y 1))
                         (p (DIFFERENCE Y 1)))
                    (p Y))).
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the
definition of ZEROP can be used to establish that the measure (COUNT Y)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  The above induction scheme generates the following three new
formulas:

Case 3. (IMPLIES (ZEROP 1)
                 (EQUAL (REMAINDER Y 1) 0)).

  This simplifies, expanding the definition of ZEROP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP 1)) (LESSP Y 1))
                 (EQUAL (REMAINDER Y 1) 0)).

  This simplifies, opening up the functions ZEROP, REMAINDER, EQUAL, and
  NUMBERP, to the new goal:

        (IMPLIES (AND (LESSP Y 1) (NUMBERP Y))
                 (EQUAL Y 0)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP 1))
                      (NOT (LESSP Y 1))
                      (EQUAL (REMAINDER (DIFFERENCE Y 1) 1)
                             0))
                 (EQUAL (REMAINDER Y 1) 0)),

  which simplifies, expanding ZEROP, REMAINDER, EQUAL, and NUMBERP, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

REMAINDER-WRT-1


(PROVE-LEMMA REMAINDER-WRT-12
             (REWRITE)
             (IMPLIES (NOT (NUMBERP X))
                      (EQUAL (REMAINDER Y X) (FIX Y))))

This simplifies, unfolding the definitions of REMAINDER and FIX, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

REMAINDER-WRT-12


(PROVE-LEMMA LESSP-REMAINDER2
             (REWRITE GENERALIZE)
             (EQUAL (LESSP (REMAINDER X Y) Y)
                    (NOT (ZEROP Y))))

This conjecture simplifies, applying EQUAL-LESSP, and unfolding the functions
ZEROP and NOT, to three new goals:

Case 3. (IMPLIES (AND (NOT (LESSP (REMAINDER X Y) Y))
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))),

  which we will name *1.

Case 2. (IMPLIES (LESSP (REMAINDER X Y) Y)
                 (NUMBERP Y)).

  This again simplifies, applying REMAINDER-WRT-12, and unfolding the
  definition of LESSP, to:

        T.

Case 1. (IMPLIES (LESSP (REMAINDER X Y) Y)
                 (NOT (EQUAL Y 0))).

  This again simplifies, using linear arithmetic, to:

        T.


     So next consider:

      (IMPLIES (AND (NOT (LESSP (REMAINDER X Y) Y))
                    (NOT (EQUAL Y 0)))
               (NOT (NUMBERP Y))),

named *1 above.  Let us appeal to the induction principle.  The recursive
terms in the conjecture suggest two inductions.  However, only one is unflawed.
We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP Y) (p Y X))
           (IMPLIES (AND (NOT (ZEROP Y)) (LESSP X Y))
                    (p Y X))
           (IMPLIES (AND (NOT (ZEROP Y))
                         (NOT (LESSP X Y))
                         (p Y (DIFFERENCE X Y)))
                    (p Y X))).
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the
definition of ZEROP inform us that the measure (COUNT X) decreases according
to the well-founded relation LESSP in each induction step of the scheme.  The
above induction scheme produces three new conjectures:

Case 3. (IMPLIES (AND (ZEROP Y)
                      (NOT (LESSP (REMAINDER X Y) Y))
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))),

  which simplifies, unfolding the function ZEROP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP Y))
                      (LESSP X Y)
                      (NOT (LESSP (REMAINDER X Y) Y))
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))),

  which simplifies, unfolding ZEROP and REMAINDER, to:

        (IMPLIES (AND (LESSP X Y)
                      (NOT (NUMBERP X))
                      (NOT (LESSP 0 Y))
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))).

  This again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP Y))
                      (NOT (LESSP X Y))
                      (LESSP (REMAINDER (DIFFERENCE X Y) Y)
                             Y)
                      (NOT (LESSP (REMAINDER X Y) Y))
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))),

  which simplifies, expanding the functions ZEROP and REMAINDER, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

LESSP-REMAINDER2


(PROVE-LEMMA REMAINDER-X-X
             (REWRITE)
             (EQUAL (REMAINDER X X) 0))

This conjecture simplifies, rewriting with DIFFERENCE-0, and expanding the
functions NUMBERP, REMAINDER, LESSP, and EQUAL, to:

      (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X))
               (NOT (LESSP X X))),

which again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

REMAINDER-X-X


(PROVE-LEMMA REMAINDER-QUOTIENT-ELIM
             (ELIM)
             (IMPLIES (AND (NOT (ZEROP Y)) (NUMBERP X))
                      (EQUAL (PLUS (REMAINDER X Y)
                                   (TIMES Y (QUOTIENT X Y)))
                             X)))

This formula can be simplified, using the abbreviations ZEROP, NOT, AND, and
IMPLIES, to:

      (IMPLIES (AND (NOT (EQUAL Y 0))
                    (NUMBERP Y)
                    (NUMBERP X))
               (EQUAL (PLUS (REMAINDER X Y)
                            (TIMES Y (QUOTIENT X Y)))
                      X)),

which simplifies, rewriting with REMAINDER-QUOTIENT, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

REMAINDER-QUOTIENT-ELIM


(PROVE-LEMMA LESSP-QUOTIENT1
             (REWRITE)
             (EQUAL (LESSP (QUOTIENT I J) I)
                    (AND (NOT (ZEROP I))
                         (OR (ZEROP J) (NOT (EQUAL J 1))))))

This formula simplifies, rewriting with EQUAL-LESSP, and opening up the
definitions of ZEROP, NOT, OR, and AND, to the following six new formulas:

Case 6. (IMPLIES (AND (NOT (LESSP (QUOTIENT I J) I))
                      (NOT (EQUAL I 0))
                      (NUMBERP I))
                 (NOT (EQUAL J 0))).

  But this again simplifies, opening up EQUAL, QUOTIENT, and LESSP, to:

        T.

Case 5. (IMPLIES (AND (NOT (LESSP (QUOTIENT I J) I))
                      (NOT (EQUAL I 0))
                      (NUMBERP I))
                 (NUMBERP J)),

  which again simplifies, unfolding the definitions of QUOTIENT, EQUAL, and
  LESSP, to:

        T.

Case 4. (IMPLIES (AND (NOT (LESSP (QUOTIENT I J) I))
                      (NOT (EQUAL I 0))
                      (NUMBERP I))
                 (EQUAL J 1)).

  Applying the lemma REMAINDER-QUOTIENT-ELIM, replace I by
  (PLUS Z (TIMES J X)) to eliminate (QUOTIENT I J) and (REMAINDER I J).  We
  employ LESSP-REMAINDER2, the type restriction lemma noted when QUOTIENT was
  introduced, and the type restriction lemma noted when REMAINDER was
  introduced to restrict the new variables.  We thus obtain the following
  three new formulas:

  Case 4.3.
          (IMPLIES (AND (EQUAL J 0)
                        (NOT (LESSP (QUOTIENT I J) I))
                        (NOT (EQUAL I 0))
                        (NUMBERP I))
                   (EQUAL J 1)).

    However this further simplifies, opening up the definitions of EQUAL,
    QUOTIENT, and LESSP, to:

          T.

  Case 4.2.
          (IMPLIES (AND (NOT (NUMBERP J))
                        (NOT (LESSP (QUOTIENT I J) I))
                        (NOT (EQUAL I 0))
                        (NUMBERP I))
                   (EQUAL J 1)),

    which further simplifies, opening up QUOTIENT, EQUAL, and LESSP, to:

          T.

  Case 4.1.
          (IMPLIES (AND (NUMBERP X)
                        (NUMBERP Z)
                        (EQUAL (LESSP Z J) (NOT (ZEROP J)))
                        (NUMBERP J)
                        (NOT (EQUAL J 0))
                        (NOT (LESSP X (PLUS Z (TIMES J X))))
                        (NOT (EQUAL (PLUS Z (TIMES J X)) 0)))
                   (EQUAL J 1)),

    which further simplifies, rewriting with the lemmas EQUAL-TIMES-0 and
    PLUS-EQUAL-0, and expanding the functions ZEROP and NOT, to two new goals:

    Case 4.1.2.
            (IMPLIES (AND (NUMBERP X)
                          (NUMBERP Z)
                          (LESSP Z J)
                          (NUMBERP J)
                          (NOT (EQUAL J 0))
                          (NOT (LESSP X (PLUS Z (TIMES J X))))
                          (NOT (EQUAL Z 0)))
                     (EQUAL J 1)),

      which again simplifies, using linear arithmetic and applying
      LESSP-TIMES-1, to:

            T.

    Case 4.1.1.
            (IMPLIES (AND (NUMBERP X)
                          (NUMBERP Z)
                          (LESSP Z J)
                          (NUMBERP J)
                          (NOT (EQUAL J 0))
                          (NOT (LESSP X (PLUS Z (TIMES J X))))
                          (NOT (EQUAL X 0)))
                     (EQUAL J 1)),

      which we would usually push and work on later by induction.  But if we
      must use induction to prove the input conjecture, we prefer to induct on
      the original formulation of the problem.  Thus we will disregard all
      that we have previously done, give the name *1 to the original input,
      and work on it.


     So now let us consider:

(EQUAL (LESSP (QUOTIENT I J) I)
       (AND (NOT (ZEROP I))
            (OR (ZEROP J) (NOT (EQUAL J 1))))).

We gave this the name *1 above.  Perhaps we can prove it by induction.  Two
inductions are suggested by terms in the conjecture, both of which are
unflawed.  So we will choose the one suggested by the largest number of
nonprimitive recursive functions.  We will induct according to the following
scheme:
      (AND (IMPLIES (ZEROP J) (p I J))
           (IMPLIES (AND (NOT (ZEROP J)) (LESSP I J))
                    (p I J))
           (IMPLIES (AND (NOT (ZEROP J))
                         (NOT (LESSP I J))
                         (p (DIFFERENCE I J) J))
                    (p I J))).
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the
definition of ZEROP inform us that the measure (COUNT I) decreases according
to the well-founded relation LESSP in each induction step of the scheme.  The
above induction scheme leads to the following three new formulas:

Case 3. (IMPLIES (ZEROP J)
                 (EQUAL (LESSP (QUOTIENT I J) I)
                        (AND (NOT (ZEROP I))
                             (OR (ZEROP J) (NOT (EQUAL J 1)))))).

  This simplifies, expanding the definitions of ZEROP, EQUAL, QUOTIENT, LESSP,
  NOT, OR, and AND, to the following four new goals:

  Case 3.4.
          (IMPLIES (AND (EQUAL J 0)
                        (NOT (EQUAL I 0))
                        (NOT (NUMBERP I)))
                   (EQUAL (NUMBERP I) F)).

    This again simplifies, clearly, to:

          T.

  Case 3.3.
          (IMPLIES (AND (EQUAL J 0)
                        (NOT (EQUAL I 0))
                        (NUMBERP I))
                   (EQUAL (NUMBERP I) T)).

    This again simplifies, clearly, to:

          T.

  Case 3.2.
          (IMPLIES (AND (NOT (NUMBERP J))
                        (NOT (EQUAL I 0))
                        (NOT (NUMBERP I)))
                   (EQUAL (NUMBERP I) F)).

    This again simplifies, clearly, to:

          T.

  Case 3.1.
          (IMPLIES (AND (NOT (NUMBERP J))
                        (NOT (EQUAL I 0))
                        (NUMBERP I))
                   (EQUAL (NUMBERP I) T)).

    This again simplifies, trivially, to:

          T.

Case 2. (IMPLIES (AND (NOT (ZEROP J)) (LESSP I J))
                 (EQUAL (LESSP (QUOTIENT I J) I)
                        (AND (NOT (ZEROP I))
                             (OR (ZEROP J) (NOT (EQUAL J 1)))))).

  This simplifies, expanding the definitions of ZEROP, QUOTIENT, EQUAL, LESSP,
  NOT, OR, and AND, to the following three new goals:

  Case 2.3.
          (IMPLIES (AND (NOT (EQUAL J 0))
                        (NUMBERP J)
                        (LESSP I J)
                        (NOT (EQUAL I 0))
                        (EQUAL J 1))
                   (EQUAL (NUMBERP I) F)).

    This again simplifies, using linear arithmetic, to:

          (IMPLIES (AND (NOT (NUMBERP I))
                        (NOT (EQUAL 1 0))
                        (NUMBERP 1)
                        (LESSP I 1)
                        (NOT (EQUAL I 0)))
                   (EQUAL (NUMBERP I) F)).

    This again simplifies, clearly, to:

          T.

  Case 2.2.
          (IMPLIES (AND (NOT (EQUAL J 0))
                        (NUMBERP J)
                        (LESSP I J)
                        (NOT (EQUAL I 0))
                        (NOT (NUMBERP I)))
                   (EQUAL (NUMBERP I) F)).

    This again simplifies, obviously, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NOT (EQUAL J 0))
                        (NUMBERP J)
                        (LESSP I J)
                        (NOT (EQUAL I 0))
                        (NUMBERP I)
                        (NOT (EQUAL J 1)))
                   (EQUAL (NUMBERP I) T)).

    This again simplifies, obviously, to:

          T.

Case 1. (IMPLIES (AND (NOT (ZEROP J))
                      (NOT (LESSP I J))
                      (EQUAL (LESSP (QUOTIENT (DIFFERENCE I J) J)
                                    (DIFFERENCE I J))
                             (AND (NOT (ZEROP (DIFFERENCE I J)))
                                  (OR (ZEROP J) (NOT (EQUAL J 1))))))
                 (EQUAL (LESSP (QUOTIENT I J) I)
                        (AND (NOT (ZEROP I))
                             (OR (ZEROP J) (NOT (EQUAL J 1)))))).

  This simplifies, applying EQUAL-DIFFERENCE-0, EQUAL-LESSP, and SUB1-ADD1,
  and unfolding the functions ZEROP, NOT, OR, AND, EQUAL, QUOTIENT, and LESSP,
  to four new goals:

  Case 1.4.
          (IMPLIES (AND (NOT (EQUAL J 0))
                        (NUMBERP J)
                        (NOT (LESSP I J))
                        (NOT (LESSP (QUOTIENT (DIFFERENCE I J) J)
                                    (DIFFERENCE I J)))
                        (EQUAL J 1))
                   (NOT (LESSP (QUOTIENT I 1) I))),

    which again simplifies, unfolding EQUAL and NUMBERP, to the goal:

          (IMPLIES (AND (NOT (LESSP I 1))
                        (NOT (LESSP (QUOTIENT (DIFFERENCE I 1) 1)
                                    (DIFFERENCE I 1))))
                   (NOT (LESSP (QUOTIENT I 1) I))).

    However this again simplifies, applying SUB1-ADD1, and opening up the
    functions NUMBERP, EQUAL, QUOTIENT, and LESSP, to the new formula:

          (IMPLIES (AND (NOT (LESSP I 1))
                        (NOT (LESSP (QUOTIENT (DIFFERENCE I 1) 1)
                                    (DIFFERENCE I 1)))
                        (NOT (EQUAL I 0))
                        (NUMBERP I))
                   (NOT (LESSP (QUOTIENT (DIFFERENCE I 1) 1)
                               (SUB1 I)))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.3.
          (IMPLIES (AND (NOT (EQUAL J 0))
                        (NUMBERP J)
                        (NOT (LESSP I J))
                        (NOT (LESSP (QUOTIENT (DIFFERENCE I J) J)
                                    (DIFFERENCE I J)))
                        (NOT (LESSP J I))
                        (NOT (EQUAL I 0))
                        (NUMBERP I)
                        (EQUAL J 1))
                   (EQUAL (LESSP (QUOTIENT (DIFFERENCE I J) J)
                                 (SUB1 I))
                          F)),

    which again simplifies, using linear arithmetic, to:

          (IMPLIES (AND (NOT (EQUAL 1 0))
                        (NUMBERP 1)
                        (NOT (LESSP 1 1))
                        (NOT (LESSP (QUOTIENT (DIFFERENCE 1 1) 1)
                                    (DIFFERENCE 1 1)))
                        (NOT (LESSP 1 1))
                        (NOT (EQUAL 1 0))
                        (NUMBERP 1))
                   (EQUAL (LESSP (QUOTIENT (DIFFERENCE 1 1) 1)
                                 (SUB1 1))
                          F)).

    However this again simplifies, unfolding EQUAL, NUMBERP, LESSP, DIFFERENCE,
    QUOTIENT, and SUB1, to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL J 0))
                        (NUMBERP J)
                        (NOT (LESSP I J))
                        (NOT (LESSP (QUOTIENT (DIFFERENCE I J) J)
                                    (DIFFERENCE I J)))
                        (NOT (LESSP J I))
                        (NOT (EQUAL I 0))
                        (NUMBERP I)
                        (NOT (EQUAL J 1)))
                   (EQUAL (LESSP (QUOTIENT (DIFFERENCE I J) J)
                                 (SUB1 I))
                          T)),

    which again simplifies, using linear arithmetic, to the conjecture:

          (IMPLIES (AND (NOT (EQUAL I 0))
                        (NUMBERP I)
                        (NOT (LESSP I I))
                        (NOT (LESSP (QUOTIENT (DIFFERENCE I I) I)
                                    (DIFFERENCE I I)))
                        (NOT (LESSP I I))
                        (NOT (EQUAL I 0))
                        (NUMBERP I)
                        (NOT (EQUAL I 1)))
                   (EQUAL (LESSP (QUOTIENT (DIFFERENCE I I) I)
                                 (SUB1 I))
                          T)).

    This again simplifies, applying DIFFERENCE-0, and expanding the
    definitions of LESSP, EQUAL, and QUOTIENT, to the new formula:

          (IMPLIES (AND (NOT (LESSP I I))
                        (NOT (EQUAL I 0))
                        (NUMBERP I)
                        (NOT (EQUAL I 1)))
                   (NOT (EQUAL (SUB1 I) 0))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL J 0))
                        (NUMBERP J)
                        (NOT (LESSP I J))
                        (LESSP (QUOTIENT (DIFFERENCE I J) J)
                               (DIFFERENCE I J))
                        (LESSP J I)
                        (NOT (EQUAL J 1))
                        (NOT (EQUAL I 0))
                        (NUMBERP I))
                   (EQUAL (LESSP (QUOTIENT (DIFFERENCE I J) J)
                                 (SUB1 I))
                          T)),

    which again simplifies, obviously, to:

          (IMPLIES (AND (NOT (EQUAL J 0))
                        (NUMBERP J)
                        (NOT (LESSP I J))
                        (LESSP (QUOTIENT (DIFFERENCE I J) J)
                               (DIFFERENCE I J))
                        (LESSP J I)
                        (NOT (EQUAL J 1))
                        (NOT (EQUAL I 0))
                        (NUMBERP I))
                   (LESSP (QUOTIENT (DIFFERENCE I J) J)
                          (SUB1 I))),

    which again simplifies, using linear arithmetic, to:

          T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.1 0.0 ]

LESSP-QUOTIENT1


(PROVE-LEMMA LESSP-REMAINDER1
             (REWRITE)
             (EQUAL (LESSP (REMAINDER X Y) X)
                    (AND (NOT (ZEROP Y))
                         (NOT (ZEROP X))
                         (NOT (LESSP X Y)))))

This formula simplifies, rewriting with EQUAL-LESSP, and opening up the
definitions of ZEROP, NOT, and AND, to the following six new formulas:

Case 6. (IMPLIES (AND (NOT (LESSP (REMAINDER X Y) X))
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NOT (EQUAL X 0))
                      (NUMBERP X))
                 (LESSP X Y)).

  Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace X by
  (PLUS Z (TIMES Y V)) to eliminate (REMAINDER X Y) and (QUOTIENT X Y).  We
  rely upon LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER
  was introduced, and the type restriction lemma noted when QUOTIENT was
  introduced to constrain the new variables.  We must thus prove:

        (IMPLIES (AND (NUMBERP Z)
                      (EQUAL (LESSP Z Y) (NOT (ZEROP Y)))
                      (NUMBERP V)
                      (NOT (LESSP Z (PLUS Z (TIMES Y V))))
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NOT (EQUAL (PLUS Z (TIMES Y V)) 0)))
                 (LESSP (PLUS Z (TIMES Y V)) Y)).

  However this further simplifies, appealing to the lemmas
  COMMUTATIVITY-OF-TIMES, EQUAL-TIMES-0, and PLUS-EQUAL-0, and unfolding the
  definitions of ZEROP and NOT, to two new conjectures:

  Case 6.2.
          (IMPLIES (AND (NUMBERP Z)
                        (LESSP Z Y)
                        (NUMBERP V)
                        (NOT (LESSP Z (PLUS Z (TIMES V Y))))
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL Z 0)))
                   (LESSP (PLUS Z (TIMES V Y)) Y)),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 6.1.
          (IMPLIES (AND (NUMBERP Z)
                        (LESSP Z Y)
                        (NUMBERP V)
                        (NOT (LESSP Z (PLUS Z (TIMES V Y))))
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL V 0)))
                   (LESSP (PLUS Z (TIMES V Y)) Y)),

    which again simplifies, using linear arithmetic, to:

          T.

Case 5. (IMPLIES (LESSP (REMAINDER X Y) X)
                 (NOT (LESSP X Y))),

  which again simplifies, unfolding the functions REMAINDER and LESSP, to two
  new formulas:

  Case 5.2.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (LESSP 0 X)
                        (NOT (EQUAL Y 0)))
                   (NOT (NUMBERP Y))),

    which again simplifies, opening up LESSP, to:

          T.

  Case 5.1.
          (IMPLIES (AND (NUMBERP X) (LESSP X X))
                   (NOT (LESSP X Y))),

    which again simplifies, using linear arithmetic, to:

          T.

Case 4. (IMPLIES (LESSP (REMAINDER X Y) X)
                 (NUMBERP X)),

  which again simplifies, expanding the functions LESSP and REMAINDER, to:

        T.

Case 3. (IMPLIES (LESSP (REMAINDER X Y) X)
                 (NOT (EQUAL X 0))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 2. (IMPLIES (LESSP (REMAINDER X Y) X)
                 (NUMBERP Y)),

  which again simplifies, rewriting with REMAINDER-WRT-12, to the following
  two new conjectures:

  Case 2.2.
          (IMPLIES (AND (NOT (NUMBERP X)) (LESSP 0 X))
                   (NUMBERP Y)).

    However this again simplifies, unfolding the function LESSP, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NUMBERP X) (LESSP X X))
                   (NUMBERP Y)),

    which again simplifies, using linear arithmetic, to:

          T.

Case 1. (IMPLIES (LESSP (REMAINDER X Y) X)
                 (NOT (EQUAL Y 0))),

  which again simplifies, opening up the definitions of EQUAL and REMAINDER,
  to two new formulas:

  Case 1.2.
          (IMPLIES (NOT (NUMBERP X))
                   (NOT (LESSP 0 X))),

    which again simplifies, unfolding the function LESSP, to:

          T.

  Case 1.1.
          (IMPLIES (NUMBERP X)
                   (NOT (LESSP X X))),

    which again simplifies, using linear arithmetic, to:

          T.

Q.E.D.


[ 0.0 0.0 0.0 ]

LESSP-REMAINDER1


(PROVE-LEMMA DIVIDES-TIMES
             (REWRITE)
             (EQUAL (REMAINDER (TIMES X Z) Z) 0))


     Name the conjecture *1.


     Perhaps we can prove it by induction.  There is only one plausible
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p X Z))
           (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Z))
                    (p X Z))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT X) decreases according to the well-founded
relation LESSP in each induction step of the scheme.  The above induction
scheme produces the following two new goals:

Case 2. (IMPLIES (ZEROP X)
                 (EQUAL (REMAINDER (TIMES X Z) Z) 0)).

  This simplifies, expanding ZEROP, EQUAL, TIMES, LESSP, NUMBERP, and
  REMAINDER, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (REMAINDER (TIMES (SUB1 X) Z) Z)
                             0))
                 (EQUAL (REMAINDER (TIMES X Z) Z) 0)).

  This simplifies, rewriting with DIFFERENCE-PLUS1, and unfolding the
  definitions of ZEROP, TIMES, and REMAINDER, to three new goals:

  Case 1.3.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (EQUAL (REMAINDER (TIMES (SUB1 X) Z) Z)
                               0)
                        (NOT (NUMBERP Z)))
                   (EQUAL (PLUS Z (TIMES (SUB1 X) Z))
                          0)),

    which again simplifies, applying REMAINDER-WRT-12 and EQUAL-TIMES-0, and
    unfolding the function PLUS, to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (EQUAL (REMAINDER (TIMES (SUB1 X) Z) Z)
                               0)
                        (EQUAL Z 0))
                   (EQUAL (PLUS Z (TIMES (SUB1 X) Z))
                          0)).

    However this again simplifies, applying COMMUTATIVITY-OF-TIMES, and
    unfolding the functions EQUAL, TIMES, REMAINDER, and PLUS, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (EQUAL (REMAINDER (TIMES (SUB1 X) Z) Z)
                               0)
                        (LESSP (PLUS Z (TIMES (SUB1 X) Z)) Z))
                   (EQUAL (PLUS Z (TIMES (SUB1 X) Z))
                          0)).

    However this again simplifies, using linear arithmetic, to:

          T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDES-TIMES


(PROVE-LEMMA REMAINDER-ADD1
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP Y))
                           (NOT (EQUAL Y 1)))
                      (NOT (EQUAL (REMAINDER (ADD1 (TIMES X Y)) Y)
                                  0))))

This conjecture can be simplified, using the abbreviations ZEROP, NOT, AND,
and IMPLIES, to:

      (IMPLIES (AND (NOT (EQUAL Y 0))
                    (NUMBERP Y)
                    (NOT (EQUAL Y 1)))
               (NOT (EQUAL (REMAINDER (ADD1 (TIMES X Y)) Y)
                           0))).

Name the above subgoal *1.


     We will appeal to induction.  There is only one plausible induction.  We
will induct according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p X Y))
           (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y))
                    (p X Y))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT X) decreases according to the well-founded relation
LESSP in each induction step of the scheme.  The above induction scheme leads
to the following two new formulas:

Case 2. (IMPLIES (AND (ZEROP X)
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NOT (EQUAL Y 1)))
                 (NOT (EQUAL (REMAINDER (ADD1 (TIMES X Y)) Y)
                             0))).

  This simplifies, using linear arithmetic, applying the lemma DIFFERENCE-0,
  and opening up the definitions of ZEROP, EQUAL, TIMES, ADD1, NUMBERP,
  REMAINDER, and LESSP, to the following two new goals:

  Case 2.2.
          (IMPLIES (AND (EQUAL X 0)
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL Y 1)))
                   (LESSP 1 Y)).

    This again simplifies, using linear arithmetic, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (NOT (EQUAL Y 0))
                        (NUMBERP Y)
                        (NOT (EQUAL Y 1)))
                   (LESSP 1 Y)),

    which again simplifies, using linear arithmetic, to:

          T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (NOT (EQUAL (REMAINDER (ADD1 (TIMES (SUB1 X) Y))
                                             Y)
                                  0))
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NOT (EQUAL Y 1)))
                 (NOT (EQUAL (REMAINDER (ADD1 (TIMES X Y)) Y)
                             0))),

  which simplifies, expanding the functions ZEROP and TIMES, to:

        (IMPLIES (AND (NOT (EQUAL X 0))
                      (NUMBERP X)
                      (NOT (EQUAL (REMAINDER (ADD1 (TIMES (SUB1 X) Y))
                                             Y)
                                  0))
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NOT (EQUAL Y 1)))
                 (NOT (EQUAL (REMAINDER (ADD1 (PLUS Y (TIMES (SUB1 X) Y)))
                                        Y)
                             0))).

  But this further simplifies, rewriting with the lemma COMMUTATIVITY-OF-TIMES,
  to:

        (IMPLIES (AND (NOT (EQUAL X 0))
                      (NUMBERP X)
                      (NOT (EQUAL (REMAINDER (ADD1 (TIMES Y (SUB1 X)))
                                             Y)
                                  0))
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NOT (EQUAL Y 1)))
                 (NOT (EQUAL (REMAINDER (ADD1 (PLUS Y (TIMES Y (SUB1 X))))
                                        Y)
                             0))).

  Appealing to the lemma SUB1-ELIM, we now replace X by (ADD1 Z) to eliminate
  (SUB1 X).  We employ the type restriction lemma noted when SUB1 was
  introduced to constrain the new variable.  We must thus prove the conjecture:

        (IMPLIES (AND (NUMBERP Z)
                      (NOT (EQUAL (ADD1 Z) 0))
                      (NOT (EQUAL (REMAINDER (ADD1 (TIMES Y Z)) Y)
                                  0))
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NOT (EQUAL Y 1)))
                 (NOT (EQUAL (REMAINDER (ADD1 (PLUS Y (TIMES Y Z)))
                                        Y)
                             0))).

  This further simplifies, trivially, to the new goal:

        (IMPLIES (AND (NUMBERP Z)
                      (NOT (EQUAL (REMAINDER (ADD1 (TIMES Y Z)) Y)
                                  0))
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NOT (EQUAL Y 1)))
                 (NOT (EQUAL (REMAINDER (ADD1 (PLUS Y (TIMES Y Z)))
                                        Y)
                             0))),

  which we generalize by replacing (TIMES Y Z) by A.  We restrict the new
  variable by recalling the type restriction lemma noted when TIMES was
  introduced.  We would thus like to prove:

        (IMPLIES (AND (NUMBERP A)
                      (NUMBERP Z)
                      (NOT (EQUAL (REMAINDER (ADD1 A) Y) 0))
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NOT (EQUAL Y 1)))
                 (NOT (EQUAL (REMAINDER (ADD1 (PLUS Y A)) Y)
                             0))),

  which further simplifies, appealing to the lemmas COMMUTATIVITY-OF-PLUS,
  DIFFERENCE-ADD1-CANCELLATION, and SUB1-ADD1, and unfolding LESSP and
  REMAINDER, to:

        (IMPLIES (AND (NUMBERP A)
                      (NUMBERP Z)
                      (NOT (EQUAL (REMAINDER (ADD1 A) Y) 0))
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NOT (EQUAL Y 1))
                      (LESSP (PLUS A Y) (SUB1 Y)))
                 (NOT (EQUAL (ADD1 (PLUS A Y)) 0))).

  This finally simplifies, using linear arithmetic, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.1 0.0 ]

REMAINDER-ADD1


(PROVE-LEMMA DIVIDES-PLUS-REWRITE1
             (REWRITE)
             (IMPLIES (AND (EQUAL (REMAINDER X Z) 0)
                           (EQUAL (REMAINDER Y Z) 0))
                      (EQUAL (REMAINDER (PLUS X Y) Z) 0)))

.

Applying the lemma REMAINDER-QUOTIENT-ELIM, replace X by (PLUS V (TIMES Z W))
to eliminate (REMAINDER X Z) and (QUOTIENT X Z).  We employ LESSP-REMAINDER2,
the type restriction lemma noted when REMAINDER was introduced, and the type
restriction lemma noted when QUOTIENT was introduced to restrict the new
variables.  We would thus like to prove the following four new conjectures:

Case 4. (IMPLIES (AND (NOT (NUMBERP X))
                      (EQUAL (REMAINDER X Z) 0)
                      (EQUAL (REMAINDER Y Z) 0))
                 (EQUAL (REMAINDER (PLUS X Y) Z) 0)).

  However this simplifies, expanding LESSP, REMAINDER, EQUAL, and PLUS, to the
  conjecture:

        (IMPLIES (AND (NOT (NUMBERP X))
                      (EQUAL (REMAINDER Y Z) 0)
                      (NOT (NUMBERP Y)))
                 (EQUAL (REMAINDER 0 Z) 0)).

  But this again simplifies, expanding the definitions of LESSP, REMAINDER,
  EQUAL, and NUMBERP, to:

        T.

Case 3. (IMPLIES (AND (EQUAL Z 0)
                      (EQUAL (REMAINDER X Z) 0)
                      (EQUAL (REMAINDER Y Z) 0))
                 (EQUAL (REMAINDER (PLUS X Y) Z) 0)),

  which simplifies, applying PLUS-RIGHT-ID2 and COMMUTATIVITY-OF-PLUS, and
  expanding the definitions of EQUAL, REMAINDER, PLUS, and NUMBERP, to:

        T.

Case 2. (IMPLIES (AND (NOT (NUMBERP Z))
                      (EQUAL (REMAINDER X Z) 0)
                      (EQUAL (REMAINDER Y Z) 0))
                 (EQUAL (REMAINDER (PLUS X Y) Z) 0)).

  But this simplifies, applying REMAINDER-WRT-12, PLUS-RIGHT-ID2, and
  COMMUTATIVITY-OF-PLUS, and opening up the definitions of PLUS, NUMBERP, and
  EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP V)
                      (EQUAL (LESSP V Z) (NOT (ZEROP Z)))
                      (NUMBERP W)
                      (NUMBERP Z)
                      (NOT (EQUAL Z 0))
                      (EQUAL V 0)
                      (EQUAL (REMAINDER Y Z) 0))
                 (EQUAL (REMAINDER (PLUS (PLUS V (TIMES Z W)) Y)
                                   Z)
                        0)).

  However this simplifies, applying COMMUTATIVITY-OF-TIMES and
  COMMUTATIVITY-OF-PLUS, and unfolding the functions NUMBERP, EQUAL, LESSP,
  ZEROP, NOT, and PLUS, to the new formula:

        (IMPLIES (AND (NUMBERP W)
                      (NUMBERP Z)
                      (NOT (EQUAL Z 0))
                      (EQUAL (REMAINDER Y Z) 0))
                 (EQUAL (REMAINDER (PLUS Y (TIMES W Z)) Z)
                        0)).

  Applying the lemma REMAINDER-QUOTIENT-ELIM, replace Y by
  (PLUS V (TIMES Z D)) to eliminate (REMAINDER Y Z) and (QUOTIENT Y Z).  We
  rely upon LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER
  was introduced, and the type restriction lemma noted when QUOTIENT was
  introduced to restrict the new variables.  This produces the following two
  new formulas:

  Case 1.2.
          (IMPLIES (AND (NOT (NUMBERP Y))
                        (NUMBERP W)
                        (NUMBERP Z)
                        (NOT (EQUAL Z 0))
                        (EQUAL (REMAINDER Y Z) 0))
                   (EQUAL (REMAINDER (PLUS Y (TIMES W Z)) Z)
                          0)).

    However this further simplifies, rewriting with DIVIDES-TIMES, and opening
    up LESSP, REMAINDER, EQUAL, and PLUS, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NUMBERP V)
                        (EQUAL (LESSP V Z) (NOT (ZEROP Z)))
                        (NUMBERP D)
                        (NUMBERP W)
                        (NUMBERP Z)
                        (NOT (EQUAL Z 0))
                        (EQUAL V 0))
                   (EQUAL (REMAINDER (PLUS (PLUS V (TIMES Z D))
                                           (TIMES W Z))
                                     Z)
                          0)).

    However this further simplifies, applying COMMUTATIVITY-OF-TIMES, and
    opening up NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to:

          (IMPLIES (AND (NUMBERP D)
                        (NUMBERP W)
                        (NUMBERP Z)
                        (NOT (EQUAL Z 0)))
                   (EQUAL (REMAINDER (PLUS (TIMES D Z) (TIMES W Z))
                                     Z)
                          0)),

    which we would normally push and work on later by induction.  But if we
    must use induction to prove the input conjecture, we prefer to induct on
    the original formulation of the problem.  Thus we will disregard all that
    we have previously done, give the name *1 to the original input, and work
    on it.


     So now let us return to:

(IMPLIES (AND (EQUAL (REMAINDER X Z) 0)
              (EQUAL (REMAINDER Y Z) 0))
         (EQUAL (REMAINDER (PLUS X Y) Z) 0)).

We named this *1.  We will try to prove it by induction.  There are three
plausible inductions, two of which are unflawed.  So we will choose the one
suggested by the largest number of nonprimitive recursive functions.  We will
induct according to the following scheme:
      (AND (IMPLIES (ZEROP Z) (p X Y Z))
           (IMPLIES (AND (NOT (ZEROP Z)) (LESSP X Z))
                    (p X Y Z))
           (IMPLIES (AND (NOT (ZEROP Z))
                         (NOT (LESSP X Z))
                         (p (DIFFERENCE X Z) Y Z))
                    (p X Y Z))).
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the
definition of ZEROP inform us that the measure (COUNT X) decreases according
to the well-founded relation LESSP in each induction step of the scheme.  The
above induction scheme produces four new goals:

Case 4. (IMPLIES (AND (ZEROP Z)
                      (EQUAL (REMAINDER X Z) 0)
                      (EQUAL (REMAINDER Y Z) 0))
                 (EQUAL (REMAINDER (PLUS X Y) Z) 0)),

  which simplifies, rewriting with the lemmas PLUS-RIGHT-ID2,
  COMMUTATIVITY-OF-PLUS, and REMAINDER-WRT-12, and expanding ZEROP, EQUAL,
  REMAINDER, PLUS, and NUMBERP, to:

        T.

Case 3. (IMPLIES (AND (NOT (ZEROP Z))
                      (LESSP X Z)
                      (EQUAL (REMAINDER X Z) 0)
                      (EQUAL (REMAINDER Y Z) 0))
                 (EQUAL (REMAINDER (PLUS X Y) Z) 0)),

  which simplifies, unfolding ZEROP, REMAINDER, EQUAL, and PLUS, to two new
  conjectures:

  Case 3.2.
          (IMPLIES (AND (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (LESSP X Z)
                        (EQUAL X 0)
                        (EQUAL (REMAINDER Y Z) 0)
                        (NOT (NUMBERP Y)))
                   (EQUAL (REMAINDER 0 Z) 0)),

    which again simplifies, unfolding EQUAL, LESSP, REMAINDER, and NUMBERP, to:

          T.

  Case 3.1.
          (IMPLIES (AND (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (LESSP X Z)
                        (NOT (NUMBERP X))
                        (EQUAL (REMAINDER Y Z) 0)
                        (NOT (NUMBERP Y)))
                   (EQUAL (REMAINDER 0 Z) 0)),

    which again simplifies, unfolding the functions LESSP, REMAINDER, EQUAL,
    and NUMBERP, to:

          T.

Case 2. (IMPLIES (AND (NOT (ZEROP Z))
                      (NOT (LESSP X Z))
                      (NOT (EQUAL (REMAINDER (DIFFERENCE X Z) Z)
                                  0))
                      (EQUAL (REMAINDER X Z) 0)
                      (EQUAL (REMAINDER Y Z) 0))
                 (EQUAL (REMAINDER (PLUS X Y) Z) 0)),

  which simplifies, unfolding the definitions of ZEROP and REMAINDER, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP Z))
                      (NOT (LESSP X Z))
                      (EQUAL (REMAINDER (PLUS (DIFFERENCE X Z) Y)
                                        Z)
                             0)
                      (EQUAL (REMAINDER X Z) 0)
                      (EQUAL (REMAINDER Y Z) 0))
                 (EQUAL (REMAINDER (PLUS X Y) Z) 0)),

  which simplifies, rewriting with COMMUTATIVITY-OF-PLUS, and opening up ZEROP
  and REMAINDER, to:

        (IMPLIES (AND (NOT (EQUAL Z 0))
                      (NUMBERP Z)
                      (NOT (LESSP X Z))
                      (EQUAL (REMAINDER (PLUS Y (DIFFERENCE X Z))
                                        Z)
                             0)
                      (EQUAL (REMAINDER (DIFFERENCE X Z) Z)
                             0)
                      (EQUAL (REMAINDER Y Z) 0))
                 (EQUAL (REMAINDER (PLUS X Y) Z) 0)).

  Applying the lemmas DIFFERENCE-ELIM and REMAINDER-QUOTIENT-ELIM, replace X
  by (PLUS Z V) to eliminate (DIFFERENCE X Z) and V by (PLUS W (TIMES Z D)) to
  eliminate (REMAINDER V Z) and (QUOTIENT V Z).  We use the type restriction
  lemma noted when DIFFERENCE was introduced, LESSP-REMAINDER2, the type
  restriction lemma noted when REMAINDER was introduced, and the type
  restriction lemma noted when QUOTIENT was introduced to restrict the new
  variables.  This produces the following two new conjectures:

  Case 1.2.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (NOT (LESSP X Z))
                        (EQUAL (REMAINDER (PLUS Y (DIFFERENCE X Z))
                                          Z)
                               0)
                        (EQUAL (REMAINDER (DIFFERENCE X Z) Z)
                               0)
                        (EQUAL (REMAINDER Y Z) 0))
                   (EQUAL (REMAINDER (PLUS X Y) Z) 0)).

    This further simplifies, unfolding the function LESSP, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NUMBERP W)
                        (EQUAL (LESSP W Z) (NOT (ZEROP Z)))
                        (NUMBERP D)
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (NOT (LESSP (PLUS Z W (TIMES Z D)) Z))
                        (EQUAL (REMAINDER (PLUS Y W (TIMES Z D)) Z)
                               0)
                        (EQUAL W 0)
                        (EQUAL (REMAINDER Y Z) 0))
                   (EQUAL (REMAINDER (PLUS (PLUS Z W (TIMES Z D)) Y)
                                     Z)
                          0)),

    which further simplifies, rewriting with the lemmas COMMUTATIVITY-OF-TIMES,
    COMMUTATIVITY-OF-PLUS, COMMUTATIVITY2-OF-PLUS, ASSOCIATIVITY-OF-PLUS, and
    DIFFERENCE-PLUS3, and unfolding the functions NUMBERP, EQUAL, LESSP, ZEROP,
    NOT, PLUS, and REMAINDER, to:

          (IMPLIES (AND (NUMBERP D)
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (NOT (LESSP (PLUS Z (TIMES D Z)) Z))
                        (EQUAL (REMAINDER (PLUS Y (TIMES D Z)) Z)
                               0)
                        (EQUAL (REMAINDER Y Z) 0)
                        (LESSP (PLUS Y Z (TIMES D Z)) Z))
                   (EQUAL (PLUS Y Z (TIMES D Z)) 0)).

    However this again simplifies, using linear arithmetic, to:

          T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.1 0.0 ]

DIVIDES-PLUS-REWRITE1


(PROVE-LEMMA DIVIDES-PLUS-REWRITE2
             (REWRITE)
             (IMPLIES (AND (EQUAL (REMAINDER X Z) 0)
                           (NOT (EQUAL (REMAINDER Y Z) 0)))
                      (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))))

.

Applying the lemma REMAINDER-QUOTIENT-ELIM, replace X by (PLUS V (TIMES Z W))
to eliminate (REMAINDER X Z) and (QUOTIENT X Z).  We use LESSP-REMAINDER2, the
type restriction lemma noted when REMAINDER was introduced, and the type
restriction lemma noted when QUOTIENT was introduced to restrict the new
variables.  We would thus like to prove the following four new formulas:

Case 4. (IMPLIES (AND (NOT (NUMBERP X))
                      (EQUAL (REMAINDER X Z) 0)
                      (NOT (EQUAL (REMAINDER Y Z) 0)))
                 (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))).

  But this simplifies, unfolding the definitions of LESSP, REMAINDER, EQUAL,
  and PLUS, to:

        (IMPLIES (AND (NOT (NUMBERP X))
                      (NOT (EQUAL (REMAINDER Y Z) 0))
                      (NOT (NUMBERP Y)))
                 (NOT (EQUAL (REMAINDER 0 Z) 0))).

  This again simplifies, expanding the functions LESSP, REMAINDER, and EQUAL,
  to:

        T.

Case 3. (IMPLIES (AND (EQUAL Z 0)
                      (EQUAL (REMAINDER X Z) 0)
                      (NOT (EQUAL (REMAINDER Y Z) 0)))
                 (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))),

  which simplifies, expanding the functions EQUAL, REMAINDER, and PLUS, to:

        T.

Case 2. (IMPLIES (AND (NOT (NUMBERP Z))
                      (EQUAL (REMAINDER X Z) 0)
                      (NOT (EQUAL (REMAINDER Y Z) 0)))
                 (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))),

  which simplifies, rewriting with REMAINDER-WRT-12, and expanding EQUAL and
  PLUS, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP V)
                      (EQUAL (LESSP V Z) (NOT (ZEROP Z)))
                      (NUMBERP W)
                      (NUMBERP Z)
                      (NOT (EQUAL Z 0))
                      (EQUAL V 0)
                      (NOT (EQUAL (REMAINDER Y Z) 0)))
                 (NOT (EQUAL (REMAINDER (PLUS (PLUS V (TIMES Z W)) Y)
                                        Z)
                             0))).

  This simplifies, rewriting with COMMUTATIVITY-OF-TIMES and
  COMMUTATIVITY-OF-PLUS, and expanding the functions NUMBERP, EQUAL, LESSP,
  ZEROP, NOT, and PLUS, to:

        (IMPLIES (AND (NUMBERP W)
                      (NUMBERP Z)
                      (NOT (EQUAL Z 0))
                      (NOT (EQUAL (REMAINDER Y Z) 0)))
                 (NOT (EQUAL (REMAINDER (PLUS Y (TIMES W Z)) Z)
                             0))).

  Applying the lemma REMAINDER-QUOTIENT-ELIM, replace Y by
  (PLUS V (TIMES Z D)) to eliminate (REMAINDER Y Z) and (QUOTIENT Y Z).  We
  rely upon LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER
  was introduced, and the type restriction lemma noted when QUOTIENT was
  introduced to restrict the new variables.  We thus obtain the following two
  new conjectures:

  Case 1.2.
          (IMPLIES (AND (NOT (NUMBERP Y))
                        (NUMBERP W)
                        (NUMBERP Z)
                        (NOT (EQUAL Z 0))
                        (NOT (EQUAL (REMAINDER Y Z) 0)))
                   (NOT (EQUAL (REMAINDER (PLUS Y (TIMES W Z)) Z)
                               0))).

    This further simplifies, unfolding the definitions of LESSP, REMAINDER,
    and EQUAL, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NUMBERP V)
                        (EQUAL (LESSP V Z) (NOT (ZEROP Z)))
                        (NUMBERP D)
                        (NUMBERP W)
                        (NUMBERP Z)
                        (NOT (EQUAL Z 0))
                        (NOT (EQUAL V 0)))
                   (NOT (EQUAL (REMAINDER (PLUS (PLUS V (TIMES Z D))
                                                (TIMES W Z))
                                          Z)
                               0))),

    which further simplifies, rewriting with COMMUTATIVITY-OF-TIMES and
    ASSOCIATIVITY-OF-PLUS, and opening up ZEROP and NOT, to:

          (IMPLIES (AND (NUMBERP V)
                        (LESSP V Z)
                        (NUMBERP D)
                        (NUMBERP W)
                        (NUMBERP Z)
                        (NOT (EQUAL Z 0))
                        (NOT (EQUAL V 0)))
                   (NOT (EQUAL (REMAINDER (PLUS V (TIMES D Z) (TIMES W Z))
                                          Z)
                               0))),

    which we would normally push and work on later by induction.  But if we
    must use induction to prove the input conjecture, we prefer to induct on
    the original formulation of the problem.  Thus we will disregard all that
    we have previously done, give the name *1 to the original input, and work
    on it.


     So now let us return to:

(IMPLIES (AND (EQUAL (REMAINDER X Z) 0)
              (NOT (EQUAL (REMAINDER Y Z) 0)))
         (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))).

We named this *1.  We will try to prove it by induction.  Three inductions are
suggested by terms in the conjecture, two of which are unflawed.  So we will
choose the one suggested by the largest number of nonprimitive recursive
functions.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP Z) (p X Y Z))
           (IMPLIES (AND (NOT (ZEROP Z)) (LESSP X Z))
                    (p X Y Z))
           (IMPLIES (AND (NOT (ZEROP Z))
                         (NOT (LESSP X Z))
                         (p (DIFFERENCE X Z) Y Z))
                    (p X Y Z))).
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the
definition of ZEROP inform us that the measure (COUNT X) decreases according
to the well-founded relation LESSP in each induction step of the scheme.  The
above induction scheme generates four new formulas:

Case 4. (IMPLIES (AND (ZEROP Z)
                      (EQUAL (REMAINDER X Z) 0)
                      (NOT (EQUAL (REMAINDER Y Z) 0)))
                 (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))),

  which simplifies, rewriting with the lemma REMAINDER-WRT-12, and unfolding
  the definitions of ZEROP, EQUAL, REMAINDER, and PLUS, to:

        T.

Case 3. (IMPLIES (AND (NOT (ZEROP Z))
                      (LESSP X Z)
                      (EQUAL (REMAINDER X Z) 0)
                      (NOT (EQUAL (REMAINDER Y Z) 0)))
                 (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))),

  which simplifies, expanding the functions ZEROP, REMAINDER, EQUAL, and PLUS,
  to two new goals:

  Case 3.2.
          (IMPLIES (AND (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (LESSP X Z)
                        (EQUAL X 0)
                        (NOT (EQUAL (REMAINDER Y Z) 0))
                        (NOT (NUMBERP Y)))
                   (NOT (EQUAL (REMAINDER 0 Z) 0))),

    which again simplifies, opening up EQUAL, LESSP, and REMAINDER, to:

          T.

  Case 3.1.
          (IMPLIES (AND (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (LESSP X Z)
                        (NOT (NUMBERP X))
                        (NOT (EQUAL (REMAINDER Y Z) 0))
                        (NOT (NUMBERP Y)))
                   (NOT (EQUAL (REMAINDER 0 Z) 0))),

    which again simplifies, expanding the functions LESSP, REMAINDER, and
    EQUAL, to:

          T.

Case 2. (IMPLIES (AND (NOT (ZEROP Z))
                      (NOT (LESSP X Z))
                      (NOT (EQUAL (REMAINDER (DIFFERENCE X Z) Z)
                                  0))
                      (EQUAL (REMAINDER X Z) 0)
                      (NOT (EQUAL (REMAINDER Y Z) 0)))
                 (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))),

  which simplifies, unfolding the functions ZEROP and REMAINDER, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP Z))
                      (NOT (LESSP X Z))
                      (NOT (EQUAL (REMAINDER (PLUS (DIFFERENCE X Z) Y)
                                             Z)
                                  0))
                      (EQUAL (REMAINDER X Z) 0)
                      (NOT (EQUAL (REMAINDER Y Z) 0)))
                 (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))),

  which simplifies, rewriting with the lemma COMMUTATIVITY-OF-PLUS, and
  opening up the definitions of ZEROP and REMAINDER, to the goal:

        (IMPLIES (AND (NOT (EQUAL Z 0))
                      (NUMBERP Z)
                      (NOT (LESSP X Z))
                      (NOT (EQUAL (REMAINDER (PLUS Y (DIFFERENCE X Z))
                                             Z)
                                  0))
                      (EQUAL (REMAINDER (DIFFERENCE X Z) Z)
                             0)
                      (NOT (EQUAL (REMAINDER Y Z) 0)))
                 (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))).

  Appealing to the lemmas DIFFERENCE-ELIM and REMAINDER-QUOTIENT-ELIM, we now
  replace X by (PLUS Z V) to eliminate (DIFFERENCE X Z) and V by
  (PLUS W (TIMES Z D)) to eliminate (REMAINDER V Z) and (QUOTIENT V Z).  We
  use the type restriction lemma noted when DIFFERENCE was introduced,
  LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was
  introduced, and the type restriction lemma noted when QUOTIENT was
  introduced to constrain the new variables.  We must thus prove two new
  formulas:

  Case 1.2.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (NOT (LESSP X Z))
                        (NOT (EQUAL (REMAINDER (PLUS Y (DIFFERENCE X Z))
                                               Z)
                                    0))
                        (EQUAL (REMAINDER (DIFFERENCE X Z) Z)
                               0)
                        (NOT (EQUAL (REMAINDER Y Z) 0)))
                   (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))),

    which further simplifies, opening up LESSP, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NUMBERP W)
                        (EQUAL (LESSP W Z) (NOT (ZEROP Z)))
                        (NUMBERP D)
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (NOT (LESSP (PLUS Z W (TIMES Z D)) Z))
                        (NOT (EQUAL (REMAINDER (PLUS Y W (TIMES Z D)) Z)
                                    0))
                        (EQUAL W 0)
                        (NOT (EQUAL (REMAINDER Y Z) 0)))
                   (NOT (EQUAL (REMAINDER (PLUS (PLUS Z W (TIMES Z D)) Y)
                                          Z)
                               0))),

    which further simplifies, applying COMMUTATIVITY-OF-TIMES,
    COMMUTATIVITY-OF-PLUS, COMMUTATIVITY2-OF-PLUS, ASSOCIATIVITY-OF-PLUS, and
    DIFFERENCE-PLUS3, and unfolding the definitions of NUMBERP, EQUAL, LESSP,
    ZEROP, NOT, PLUS, and REMAINDER, to:

          (IMPLIES (AND (NUMBERP D)
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (NOT (LESSP (PLUS Z (TIMES D Z)) Z))
                        (NOT (EQUAL (REMAINDER (PLUS Y (TIMES D Z)) Z)
                                    0))
                        (NOT (EQUAL (REMAINDER Y Z) 0))
                        (LESSP (PLUS Y Z (TIMES D Z)) Z))
                   (NOT (EQUAL (PLUS Y Z (TIMES D Z)) 0))),

    which again simplifies, using linear arithmetic, to:

          T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.1 0.0 ]

DIVIDES-PLUS-REWRITE2


(PROVE-LEMMA DIVIDES-PLUS-REWRITE
             (REWRITE)
             (IMPLIES (EQUAL (REMAINDER X Z) 0)
                      (EQUAL (EQUAL (REMAINDER (PLUS X Y) Z) 0)
                             (EQUAL (REMAINDER Y Z) 0))))

This conjecture simplifies, clearly, to two new conjectures:

Case 2. (IMPLIES (AND (EQUAL (REMAINDER X Z) 0)
                      (NOT (EQUAL (REMAINDER Y Z) 0)))
                 (NOT (EQUAL (REMAINDER (PLUS X Y) Z) 0))),

  which again simplifies, applying DIVIDES-PLUS-REWRITE2, to:

        T.

Case 1. (IMPLIES (AND (EQUAL (REMAINDER X Z) 0)
                      (EQUAL (REMAINDER Y Z) 0))
                 (EQUAL (EQUAL (REMAINDER (PLUS X Y) Z) 0)
                        T)).

  However this again simplifies, applying DIVIDES-PLUS-REWRITE1, and unfolding
  the function EQUAL, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDES-PLUS-REWRITE


(PROVE-LEMMA DIVIDES-PLUS-REWRITE-COMMUTED
             (REWRITE)
             (IMPLIES (EQUAL (REMAINDER X Z) 0)
                      (EQUAL (EQUAL (REMAINDER (PLUS Y X) Z) 0)
                             (EQUAL (REMAINDER Y Z) 0))))

This conjecture simplifies, applying COMMUTATIVITY-OF-PLUS and
DIVIDES-PLUS-REWRITE, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDES-PLUS-REWRITE-COMMUTED


(PROVE-LEMMA EUCLID
             (REWRITE)
             (IMPLIES (EQUAL (REMAINDER X Z) 0)
                      (EQUAL (EQUAL (REMAINDER (DIFFERENCE Y X) Z)
                                    0)
                             (IF (LESSP X Y)
                                 (EQUAL (REMAINDER Y Z) 0)
                                 T))))

This formula simplifies, obviously, to the following three new conjectures:

Case 3. (IMPLIES (AND (EQUAL (REMAINDER X Z) 0)
                      (NOT (EQUAL (REMAINDER (DIFFERENCE Y X) Z)
                                  0)))
                 (LESSP X Y)).

  This again simplifies, applying DIFFERENCE-0, and expanding LESSP, EQUAL,
  NUMBERP, and REMAINDER, to:

        T.

Case 2. (IMPLIES (AND (EQUAL (REMAINDER X Z) 0)
                      (NOT (EQUAL (REMAINDER (DIFFERENCE Y X) Z)
                                  0)))
                 (NOT (EQUAL (REMAINDER Y Z) 0))).

  Appealing to the lemmas DIFFERENCE-ELIM and REMAINDER-QUOTIENT-ELIM, we now
  replace Y by (PLUS X V) to eliminate (DIFFERENCE Y X) and V by
  (PLUS W (TIMES Z D)) to eliminate (REMAINDER V Z) and (QUOTIENT V Z).  We
  rely upon the type restriction lemma noted when DIFFERENCE was introduced,
  LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was
  introduced, and the type restriction lemma noted when QUOTIENT was
  introduced to constrain the new variables.  We must thus prove five new
  goals:

  Case 2.5.
          (IMPLIES (AND (LESSP Y X)
                        (EQUAL (REMAINDER X Z) 0)
                        (NOT (EQUAL (REMAINDER (DIFFERENCE Y X) Z)
                                    0)))
                   (NOT (EQUAL (REMAINDER Y Z) 0))),

    which further simplifies, using linear arithmetic, rewriting with
    DIFFERENCE-0, and expanding the definitions of LESSP, EQUAL, NUMBERP, and
    REMAINDER, to:

          T.

  Case 2.4.
          (IMPLIES (AND (NOT (NUMBERP Y))
                        (EQUAL (REMAINDER X Z) 0)
                        (NOT (EQUAL (REMAINDER (DIFFERENCE Y X) Z)
                                    0)))
                   (NOT (EQUAL (REMAINDER Y Z) 0))).

    However this further simplifies, using linear arithmetic, rewriting with
    the lemma DIFFERENCE-0, and unfolding LESSP, EQUAL, NUMBERP, and REMAINDER,
    to:

          T.

  Case 2.3.
          (IMPLIES (AND (EQUAL Z 0)
                        (NUMBERP V)
                        (NOT (LESSP (PLUS X V) X))
                        (EQUAL (REMAINDER X Z) 0)
                        (NOT (EQUAL (REMAINDER V Z) 0)))
                   (NOT (EQUAL (REMAINDER (PLUS X V) Z) 0))),

    which further simplifies, rewriting with COMMUTATIVITY-OF-PLUS and
    PLUS-RIGHT-ID2, and opening up the functions EQUAL, REMAINDER, and PLUS,
    to:

          T.

  Case 2.2.
          (IMPLIES (AND (NOT (NUMBERP Z))
                        (NUMBERP V)
                        (NOT (LESSP (PLUS X V) X))
                        (EQUAL (REMAINDER X Z) 0)
                        (NOT (EQUAL (REMAINDER V Z) 0)))
                   (NOT (EQUAL (REMAINDER (PLUS X V) Z) 0))).

    But this further simplifies, rewriting with COMMUTATIVITY-OF-PLUS,
    REMAINDER-WRT-12, and PLUS-RIGHT-ID2, and expanding the functions EQUAL
    and PLUS, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NUMBERP W)
                        (EQUAL (LESSP W Z) (NOT (ZEROP Z)))
                        (NUMBERP D)
                        (NUMBERP Z)
                        (NOT (EQUAL Z 0))
                        (NOT (LESSP (PLUS X W (TIMES Z D)) X))
                        (EQUAL (REMAINDER X Z) 0)
                        (NOT (EQUAL W 0)))
                   (NOT (EQUAL (REMAINDER (PLUS X W (TIMES Z D)) Z)
                               0))).

    But this further simplifies, applying the lemmas COMMUTATIVITY-OF-TIMES,
    COMMUTATIVITY2-OF-PLUS, DIVIDES-PLUS-REWRITE1, DIVIDES-TIMES, and
    DIVIDES-PLUS-REWRITE-COMMUTED, and expanding the functions ZEROP, NOT,
    EQUAL, and REMAINDER, to:

          T.

Case 1. (IMPLIES (AND (EQUAL (REMAINDER X Z) 0)
                      (EQUAL (REMAINDER (DIFFERENCE Y X) Z)
                             0)
                      (LESSP X Y))
                 (EQUAL (EQUAL (REMAINDER Y Z) 0) T)),

  which again simplifies, trivially, to the new formula:

        (IMPLIES (AND (EQUAL (REMAINDER X Z) 0)
                      (EQUAL (REMAINDER (DIFFERENCE Y X) Z)
                             0)
                      (LESSP X Y))
                 (EQUAL (REMAINDER Y Z) 0)).

  Applying the lemmas DIFFERENCE-ELIM and REMAINDER-QUOTIENT-ELIM, replace Y
  by (PLUS X V) to eliminate (DIFFERENCE Y X) and V by (PLUS W (TIMES Z D)) to
  eliminate (REMAINDER V Z) and (QUOTIENT V Z).  We use the type restriction
  lemma noted when DIFFERENCE was introduced, LESSP-REMAINDER2, the type
  restriction lemma noted when REMAINDER was introduced, and the type
  restriction lemma noted when QUOTIENT was introduced to restrict the new
  variables.  We would thus like to prove the following five new goals:

  Case 1.5.
          (IMPLIES (AND (LESSP Y X)
                        (EQUAL (REMAINDER X Z) 0)
                        (EQUAL (REMAINDER (DIFFERENCE Y X) Z)
                               0)
                        (LESSP X Y))
                   (EQUAL (REMAINDER Y Z) 0)).

    But this further simplifies, using linear arithmetic, to:

          T.

  Case 1.4.
          (IMPLIES (AND (NOT (NUMBERP Y))
                        (EQUAL (REMAINDER X Z) 0)
                        (EQUAL (REMAINDER (DIFFERENCE Y X) Z)
                               0)
                        (LESSP X Y))
                   (EQUAL (REMAINDER Y Z) 0)),

    which further simplifies, expanding DIFFERENCE, LESSP, EQUAL, NUMBERP, and
    REMAINDER, to:

          T.

  Case 1.3.
          (IMPLIES (AND (EQUAL Z 0)
                        (NUMBERP V)
                        (NOT (LESSP (PLUS X V) X))
                        (EQUAL (REMAINDER X Z) 0)
                        (EQUAL (REMAINDER V Z) 0)
                        (LESSP X (PLUS X V)))
                   (EQUAL (REMAINDER (PLUS X V) Z) 0)),

    which further simplifies, applying the lemmas COMMUTATIVITY-OF-PLUS and
    PLUS-RIGHT-ID2, and opening up the functions EQUAL, REMAINDER, PLUS, LESSP,
    and NUMBERP, to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (NUMBERP Z))
                        (NUMBERP V)
                        (NOT (LESSP (PLUS X V) X))
                        (EQUAL (REMAINDER X Z) 0)
                        (EQUAL (REMAINDER V Z) 0)
                        (LESSP X (PLUS X V)))
                   (EQUAL (REMAINDER (PLUS X V) Z) 0)),

    which further simplifies, applying the lemmas COMMUTATIVITY-OF-PLUS,
    REMAINDER-WRT-12, and PLUS-RIGHT-ID2, and opening up PLUS, LESSP, NUMBERP,
    and EQUAL, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NUMBERP W)
                        (EQUAL (LESSP W Z) (NOT (ZEROP Z)))
                        (NUMBERP D)
                        (NUMBERP Z)
                        (NOT (EQUAL Z 0))
                        (NOT (LESSP (PLUS X W (TIMES Z D)) X))
                        (EQUAL (REMAINDER X Z) 0)
                        (EQUAL W 0)
                        (LESSP X (PLUS X W (TIMES Z D))))
                   (EQUAL (REMAINDER (PLUS X W (TIMES Z D)) Z)
                          0)),

    which further simplifies, applying the lemmas COMMUTATIVITY-OF-TIMES,
    DIVIDES-TIMES, and DIVIDES-PLUS-REWRITE1, and opening up NUMBERP, EQUAL,
    LESSP, ZEROP, NOT, and PLUS, to:

          T.

Q.E.D.


[ 0.0 0.1 0.0 ]

EUCLID


(PROVE-LEMMA REMAINDER-0-CROCK
             (REWRITE)
             (EQUAL (REMAINDER 0 Y) 0)
             NIL)

This simplifies, unfolding LESSP, EQUAL, NUMBERP, and REMAINDER, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

REMAINDER-0-CROCK


(PROVE-LEMMA QUOTIENT-TIMES1
             (REWRITE)
             (IMPLIES (AND (NUMBERP Y)
                           (NUMBERP X)
                           (NOT (EQUAL X 0))
                           (DIVIDES X Y))
                      (EQUAL (TIMES X (QUOTIENT Y X)) Y)))

WARNING:  the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the newly proposed QUOTIENT-TIMES1 could!


This formula can be simplified, using the abbreviations NOT, AND, IMPLIES, and
DIVIDES, to:

      (IMPLIES (AND (NUMBERP Y)
                    (NUMBERP X)
                    (NOT (EQUAL X 0))
                    (EQUAL (REMAINDER Y X) 0))
               (EQUAL (TIMES X (QUOTIENT Y X)) Y)).

Applying the lemma REMAINDER-QUOTIENT-ELIM, replace Y by (PLUS Z (TIMES X V))
to eliminate (REMAINDER Y X) and (QUOTIENT Y X).  We rely upon
LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was
introduced, and the type restriction lemma noted when QUOTIENT was introduced
to restrict the new variables.  We thus obtain:

      (IMPLIES (AND (NUMBERP Z)
                    (EQUAL (LESSP Z X) (NOT (ZEROP X)))
                    (NUMBERP V)
                    (NUMBERP X)
                    (NOT (EQUAL X 0))
                    (EQUAL Z 0))
               (EQUAL (TIMES X V)
                      (PLUS Z (TIMES X V)))),

which simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

QUOTIENT-TIMES1


(PROVE-LEMMA QUOTIENT-LESSP
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP X)) (LESSP X Y))
                      (NOT (EQUAL (QUOTIENT Y X) 0))))

This formula can be simplified, using the abbreviations ZEROP, NOT, AND, and
IMPLIES, to the new conjecture:

      (IMPLIES (AND (NOT (EQUAL X 0))
                    (NUMBERP X)
                    (LESSP X Y))
               (NOT (EQUAL (QUOTIENT Y X) 0))).

Applying the lemma REMAINDER-QUOTIENT-ELIM, replace Y by (PLUS V (TIMES X Z))
to eliminate (QUOTIENT Y X) and (REMAINDER Y X).  We rely upon
LESSP-REMAINDER2, the type restriction lemma noted when QUOTIENT was
introduced, and the type restriction lemma noted when REMAINDER was introduced
to restrict the new variables.  We thus obtain the following two new goals:

Case 2. (IMPLIES (AND (NOT (NUMBERP Y))
                      (NOT (EQUAL X 0))
                      (NUMBERP X)
                      (LESSP X Y))
                 (NOT (EQUAL (QUOTIENT Y X) 0))).

  However this simplifies, opening up the definition of LESSP, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP Z)
                      (NUMBERP V)
                      (EQUAL (LESSP V X) (NOT (ZEROP X)))
                      (NOT (EQUAL X 0))
                      (NUMBERP X)
                      (LESSP X (PLUS V (TIMES X Z))))
                 (NOT (EQUAL Z 0))),

  which simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES and
  COMMUTATIVITY-OF-PLUS, and expanding the definitions of NUMBERP, ZEROP, NOT,
  EQUAL, TIMES, and PLUS, to:

        (IMPLIES (AND (NUMBERP V)
                      (LESSP V X)
                      (NOT (EQUAL X 0))
                      (NUMBERP X))
                 (NOT (LESSP X V))).

  However this again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

QUOTIENT-LESSP


(PROVE-LEMMA DIVIDES-TIMES1
             (REWRITE)
             (IMPLIES (EQUAL A (TIMES Z Y))
                      (EQUAL (REMAINDER A Z) 0)))

WARNING:  Note that DIVIDES-TIMES1 contains the free variable Y which will be
chosen by instantiating the hypothesis (EQUAL A (TIMES Z Y)).


This formula simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES and
DIVIDES-TIMES, and expanding the function EQUAL, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDES-TIMES1


(PROVE-LEMMA QUOTIENT-DIVIDES
             (REWRITE)
             (IMPLIES (AND (NUMBERP Y)
                           (NOT (EQUAL (TIMES X (QUOTIENT Y X)) Y)))
                      (NOT (EQUAL (REMAINDER Y X) 0))))

.

Applying the lemma REMAINDER-QUOTIENT-ELIM, replace Y by (PLUS V (TIMES X Z))
to eliminate (QUOTIENT Y X) and (REMAINDER Y X).  We rely upon
LESSP-REMAINDER2, the type restriction lemma noted when QUOTIENT was
introduced, and the type restriction lemma noted when REMAINDER was introduced
to restrict the new variables.  This produces the following three new
conjectures:

Case 3. (IMPLIES (AND (EQUAL X 0)
                      (NUMBERP Y)
                      (NOT (EQUAL (TIMES X (QUOTIENT Y X)) Y)))
                 (NOT (EQUAL (REMAINDER Y X) 0))).

  But this simplifies, opening up the functions EQUAL, QUOTIENT, TIMES, and
  REMAINDER, to:

        T.

Case 2. (IMPLIES (AND (NOT (NUMBERP X))
                      (NUMBERP Y)
                      (NOT (EQUAL (TIMES X (QUOTIENT Y X)) Y)))
                 (NOT (EQUAL (REMAINDER Y X) 0))),

  which simplifies, rewriting with TIMES-ZERO2, COMMUTATIVITY-OF-TIMES, and
  REMAINDER-WRT-12, and opening up the definition of QUOTIENT, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP Z)
                      (NUMBERP V)
                      (EQUAL (LESSP V X) (NOT (ZEROP X)))
                      (NUMBERP X)
                      (NOT (EQUAL X 0))
                      (NOT (EQUAL (TIMES X Z)
                                  (PLUS V (TIMES X Z)))))
                 (NOT (EQUAL V 0))).

  But this simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

QUOTIENT-DIVIDES


(PROVE-LEMMA QUOTIENT-TIMES
             (REWRITE)
             (EQUAL (QUOTIENT (TIMES Y X) Y)
                    (IF (ZEROP Y) 0 (FIX X))))

This conjecture simplifies, applying COMMUTATIVITY-OF-TIMES, and expanding the
functions ZEROP and FIX, to four new conjectures:

Case 4. (IMPLIES (EQUAL Y 0)
                 (EQUAL (QUOTIENT (TIMES X Y) Y) 0)),

  which again simplifies, applying COMMUTATIVITY-OF-TIMES, and opening up
  EQUAL, TIMES, and QUOTIENT, to:

        T.

Case 3. (IMPLIES (NOT (NUMBERP Y))
                 (EQUAL (QUOTIENT (TIMES X Y) Y) 0)).

  This again simplifies, applying TIMES-ZERO2, and opening up the functions
  QUOTIENT and EQUAL, to:

        T.

Case 2. (IMPLIES (NOT (NUMBERP X))
                 (EQUAL (QUOTIENT (TIMES X Y) Y) 0)).

  However this again simplifies, unfolding the definitions of TIMES, LESSP,
  EQUAL, and QUOTIENT, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NUMBERP X))
                 (EQUAL (QUOTIENT (TIMES X Y) Y) X)),

  which we will name *1.


     We will appeal to induction.  There is only one plausible induction.  We
will induct according to the following scheme:
      (AND (IMPLIES (ZEROP X) (p X Y))
           (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y))
                    (p X Y))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to establish that the measure (COUNT X) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme generates two new goals:

Case 2. (IMPLIES (AND (ZEROP X)
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NUMBERP X))
                 (EQUAL (QUOTIENT (TIMES X Y) Y) X)),

  which simplifies, opening up ZEROP, NUMBERP, EQUAL, TIMES, LESSP, and
  QUOTIENT, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP X))
                      (EQUAL (QUOTIENT (TIMES (SUB1 X) Y) Y)
                             (SUB1 X))
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NUMBERP X))
                 (EQUAL (QUOTIENT (TIMES X Y) Y) X)),

  which simplifies, rewriting with ADD1-SUB1 and DIFFERENCE-PLUS1, and
  expanding the functions ZEROP, TIMES, and QUOTIENT, to the new formula:

        (IMPLIES (AND (NOT (EQUAL X 0))
                      (EQUAL (QUOTIENT (TIMES (SUB1 X) Y) Y)
                             (SUB1 X))
                      (NOT (EQUAL Y 0))
                      (NUMBERP Y)
                      (NUMBERP X))
                 (NOT (LESSP (PLUS Y (TIMES (SUB1 X) Y))
                             Y))),

  which again simplifies, using linear arithmetic, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

QUOTIENT-TIMES


(PROVE-LEMMA DISTRIBUTIVITY-OF-DIVIDES
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP A)) (DIVIDES A W))
                      (EQUAL (TIMES C (QUOTIENT W A))
                             (QUOTIENT (TIMES C W) A))))

WARNING:  the newly proposed lemma, DISTRIBUTIVITY-OF-DIVIDES, could be
applied whenever the previously added lemma QUOTIENT-TIMES1 could.




WARNING:  the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the newly proposed DISTRIBUTIVITY-OF-DIVIDES could!


This conjecture can be simplified, using the abbreviations ZEROP, NOT, AND,
IMPLIES, and DIVIDES, to:

      (IMPLIES (AND (NOT (EQUAL A 0))
                    (NUMBERP A)
                    (EQUAL (REMAINDER W A) 0))
               (EQUAL (TIMES C (QUOTIENT W A))
                      (QUOTIENT (TIMES C W) A))).

Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace W by
(PLUS X (TIMES A Z)) to eliminate (REMAINDER W A) and (QUOTIENT W A).  We use
LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was
introduced, and the type restriction lemma noted when QUOTIENT was introduced
to constrain the new variables.  This generates two new conjectures:

Case 2. (IMPLIES (AND (NOT (NUMBERP W))
                      (NOT (EQUAL A 0))
                      (NUMBERP A)
                      (EQUAL (REMAINDER W A) 0))
                 (EQUAL (TIMES C (QUOTIENT W A))
                        (QUOTIENT (TIMES C W) A))),

  which simplifies, rewriting with COMMUTATIVITY-OF-TIMES and TIMES-ZERO2, and
  opening up LESSP, REMAINDER, EQUAL, QUOTIENT, and TIMES, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP X)
                      (EQUAL (LESSP X A) (NOT (ZEROP A)))
                      (NUMBERP Z)
                      (NOT (EQUAL A 0))
                      (NUMBERP A)
                      (EQUAL X 0))
                 (EQUAL (TIMES C Z)
                        (QUOTIENT (TIMES C (PLUS X (TIMES A Z)))
                                  A))).

  But this simplifies, rewriting with COMMUTATIVITY2-OF-TIMES and
  QUOTIENT-TIMES, and expanding the functions NUMBERP, EQUAL, LESSP, ZEROP,
  NOT, and PLUS, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DISTRIBUTIVITY-OF-DIVIDES


(PROVE-LEMMA TIMES-LIST-APPEND
             (REWRITE)
             (EQUAL (TIMES-LIST (APPEND X Y))
                    (TIMES (TIMES-LIST X)
                           (TIMES-LIST Y))))


     Call the conjecture *1.


     Perhaps we can prove it by induction.  Three inductions are suggested by
terms in the conjecture.  They merge into two likely candidate inductions.
However, only one is unflawed.  We will induct according to the following
scheme:
      (AND (IMPLIES (AND (LISTP X) (p (CDR X) Y))
                    (p X Y))
           (IMPLIES (NOT (LISTP X)) (p X Y))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT X) decreases according to the well-founded relation LESSP in
each induction step of the scheme.  The above induction scheme leads to two
new goals:

Case 2. (IMPLIES (AND (LISTP X)
                      (EQUAL (TIMES-LIST (APPEND (CDR X) Y))
                             (TIMES (TIMES-LIST (CDR X))
                                    (TIMES-LIST Y))))
                 (EQUAL (TIMES-LIST (APPEND X Y))
                        (TIMES (TIMES-LIST X)
                               (TIMES-LIST Y)))),

  which simplifies, applying the lemmas COMMUTATIVITY-OF-TIMES, CDR-CONS,
  CAR-CONS, and ASSOCIATIVITY-OF-TIMES, and opening up the definitions of
  APPEND and TIMES-LIST, to:

        T.

Case 1. (IMPLIES (NOT (LISTP X))
                 (EQUAL (TIMES-LIST (APPEND X Y))
                        (TIMES (TIMES-LIST X)
                               (TIMES-LIST Y)))),

  which simplifies, rewriting with TIMES-ID-IFF-1, and opening up the
  functions APPEND, TIMES-LIST, and EQUAL, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

TIMES-LIST-APPEND


(PROVE-LEMMA PRIME-LIST-APPEND
             (REWRITE)
             (EQUAL (PRIME-LIST (APPEND X Y))
                    (AND (PRIME-LIST X) (PRIME-LIST Y))))

This simplifies, unfolding the definition of AND, to the following two new
goals:

Case 2. (IMPLIES (NOT (PRIME-LIST X))
                 (EQUAL (PRIME-LIST (APPEND X Y)) F)).

  This again simplifies, trivially, to:

        (IMPLIES (NOT (PRIME-LIST X))
                 (NOT (PRIME-LIST (APPEND X Y)))),

  which we will name *1.

Case 1. (IMPLIES (PRIME-LIST X)
                 (EQUAL (PRIME-LIST (APPEND X Y))
                        (PRIME-LIST Y))),

  which we would usually push and work on later by induction.  But if we must
  use induction to prove the input conjecture, we prefer to induct on the
  original formulation of the problem.  Thus we will disregard all that we
  have previously done, give the name *1 to the original input, and work on it.


     So now let us consider:

(EQUAL (PRIME-LIST (APPEND X Y))
       (AND (PRIME-LIST X) (PRIME-LIST Y))),

which we named *1 above.  We will appeal to induction.  The recursive terms in
the conjecture suggest three inductions.  They merge into two likely candidate
inductions.  However, only one is unflawed.  We will induct according to the
following scheme:
      (AND (IMPLIES (AND (LISTP X) (p (CDR X) Y))
                    (p X Y))
           (IMPLIES (NOT (LISTP X)) (p X Y))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT X)
decreases according to the well-founded relation LESSP in each induction step
of the scheme.  The above induction scheme produces the following two new
goals:

Case 2. (IMPLIES (AND (LISTP X)
                      (EQUAL (PRIME-LIST (APPEND (CDR X) Y))
                             (AND (PRIME-LIST (CDR X))
                                  (PRIME-LIST Y))))
                 (EQUAL (PRIME-LIST (APPEND X Y))
                        (AND (PRIME-LIST X) (PRIME-LIST Y)))).

  This simplifies, appealing to the lemmas CDR-CONS and CAR-CONS, and
  expanding the functions AND, APPEND, PRIME, PRIME-LIST, and EQUAL, to:

        T.

Case 1. (IMPLIES (NOT (LISTP X))
                 (EQUAL (PRIME-LIST (APPEND X Y))
                        (AND (PRIME-LIST X) (PRIME-LIST Y)))).

  This simplifies, opening up the functions APPEND, PRIME-LIST, and AND, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.2 0.0 ]

PRIME-LIST-APPEND


(PROVE-LEMMA PRIME-LIST-DELETE
             (REWRITE)
             (IMPLIES (PRIME-LIST L2)
                      (PRIME-LIST (DELETE X L2))))


     Call the conjecture *1.


     We will try to prove it by induction.  The recursive terms in the
conjecture suggest two inductions.  However, they merge into one likely
candidate induction.  We will induct according to the following scheme:
      (AND (IMPLIES (NLISTP L2) (p X L2))
           (IMPLIES (AND (NOT (NLISTP L2)) (p X (CDR L2)))
                    (p X L2))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to establish that the measure (COUNT L2) decreases
according to the well-founded relation LESSP in each induction step of the
scheme.  The above induction scheme generates the following three new formulas:

Case 3. (IMPLIES (AND (NLISTP L2) (PRIME-LIST L2))
                 (PRIME-LIST (DELETE X L2))).

  This simplifies, applying DELETE-NON-MEMBER, and expanding the functions
  NLISTP, PRIME-LIST, and MEMBER, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP L2))
                      (NOT (PRIME-LIST (CDR L2)))
                      (PRIME-LIST L2))
                 (PRIME-LIST (DELETE X L2))),

  which simplifies, opening up the functions NLISTP, PRIME-LIST, and PRIME, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP L2))
                      (PRIME-LIST (DELETE X (CDR L2)))
                      (PRIME-LIST L2))
                 (PRIME-LIST (DELETE X L2))),

  which simplifies, expanding NLISTP, PRIME-LIST, PRIME, and DELETE, to:

        (IMPLIES (AND (LISTP L2)
                      (PRIME-LIST (DELETE X (CDR L2)))
                      (NOT (EQUAL (CAR L2) 0))
                      (NUMBERP (CAR L2))
                      (NOT (EQUAL (CAR L2) 1))
                      (PRIME1 (CAR L2) (SUB1 (CAR L2)))
                      (PRIME-LIST (CDR L2))
                      (NOT (EQUAL X (CAR L2))))
                 (PRIME-LIST (CONS (CAR L2) (DELETE X (CDR L2))))).

  This again simplifies, applying CDR-CONS and CAR-CONS, and expanding the
  functions PRIME and PRIME-LIST, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.1 0.0 ]

PRIME-LIST-DELETE


(PROVE-LEMMA PRIMES-ARE-BIG NIL
             (IMPLIES (PRIME P)
                      (EQUAL (LESSP 1 P) T)))

This formula can be simplified, using the abbreviations PRIME and IMPLIES, to:

      (IMPLIES (AND (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P)))
               (EQUAL (LESSP 1 P) T)),

which simplifies, opening up SUB1, NUMBERP, EQUAL, and LESSP, to:

      (IMPLIES (AND (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P)))
               (NOT (EQUAL (SUB1 P) 0))).

But this again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PRIMES-ARE-BIG


(PROVE-LEMMA LITTLE-STEP-AUX1
             (REWRITE)
             (IMPLIES (AND (PRIME1 P Z)
                           (LESSP 1 Y)
                           (LEQ Y Z))
                      (NOT (DIVIDES Y P)))
             ((DISABLE DIVIDES)))

WARNING:  Note that the rewrite rule LITTLE-STEP-AUX1 will be stored so as to
apply only to terms with the nonrecursive function symbol DIVIDES.


WARNING:  Note that LITTLE-STEP-AUX1 contains the free variable Z which will
be chosen by instantiating the hypothesis (PRIME1 P Z).



     Name the conjecture *1.


     We will appeal to induction.  There is only one plausible induction.  We
will induct according to the following scheme:
      (AND (IMPLIES (ZEROP Z) (p Y P Z))
           (IMPLIES (AND (NOT (ZEROP Z)) (EQUAL Z 1))
                    (p Y P Z))
           (IMPLIES (AND (NOT (ZEROP Z))
                         (NOT (EQUAL Z 1))
                         (p Y P (SUB1 Z)))
                    (p Y P Z))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT Z) decreases according to the well-founded
relation LESSP in each induction step of the scheme.  The above induction
scheme generates the following four new conjectures:

Case 4. (IMPLIES (AND (ZEROP Z)
                      (PRIME1 P Z)
                      (LESSP 1 Y)
                      (NOT (LESSP Z Y)))
                 (NOT (DIVIDES Y P))).

  This simplifies, unfolding the definitions of ZEROP, EQUAL, and PRIME1, to:

        T.

Case 3. (IMPLIES (AND (NOT (ZEROP Z))
                      (EQUAL Z 1)
                      (PRIME1 P Z)
                      (LESSP 1 Y)
                      (NOT (LESSP Z Y)))
                 (NOT (DIVIDES Y P))).

  This simplifies, clearly, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP Z))
                      (NOT (EQUAL Z 1))
                      (NOT (PRIME1 P (SUB1 Z)))
                      (PRIME1 P Z)
                      (LESSP 1 Y)
                      (NOT (LESSP Z Y)))
                 (NOT (DIVIDES Y P))).

  This simplifies, opening up the definitions of ZEROP and PRIME1, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP Z))
                      (NOT (EQUAL Z 1))
                      (LESSP (SUB1 Z) Y)
                      (PRIME1 P Z)
                      (LESSP 1 Y)
                      (NOT (LESSP Z Y)))
                 (NOT (DIVIDES Y P))).

  This simplifies, using linear arithmetic, to the following three new
  conjectures:

  Case 1.3.
          (IMPLIES (AND (NOT (NUMBERP Z))
                        (NOT (ZEROP Z))
                        (NOT (EQUAL Z 1))
                        (LESSP (SUB1 Z) Y)
                        (PRIME1 P Z)
                        (LESSP 1 Y)
                        (NOT (LESSP Z Y)))
                   (NOT (DIVIDES Y P))).

    This again simplifies, opening up the definition of ZEROP, to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (NUMBERP Y))
                        (NOT (ZEROP Z))
                        (NOT (EQUAL Z 1))
                        (LESSP (SUB1 Z) Y)
                        (PRIME1 P Z)
                        (LESSP 1 Y)
                        (NOT (LESSP Z Y)))
                   (NOT (DIVIDES Y P))),

    which again simplifies, expanding the functions ZEROP and LESSP, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NUMBERP Y)
                        (NUMBERP Z)
                        (NOT (ZEROP Y))
                        (NOT (EQUAL Y 1))
                        (LESSP (SUB1 Y) Y)
                        (PRIME1 P Y)
                        (LESSP 1 Y)
                        (NOT (LESSP Y Y)))
                   (NOT (DIVIDES Y P))),

    which again simplifies, expanding ZEROP and PRIME1, to:

          T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.0 0.0 ]

LITTLE-STEP-AUX1


(PROVE-LEMMA LITTLE-STEP-AUX2
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (LESSP 1 Y)
                           (LESSP Y P))
                      (NOT (DIVIDES Y P)))
             ((USE (LITTLE-STEP-AUX1 (P P) (Z (SUB1 P))))
              (DISABLE LITTLE-STEP-AUX1)))

WARNING:  Note that the rewrite rule LITTLE-STEP-AUX2 will be stored so as to
apply only to terms with the nonrecursive function symbol DIVIDES.


This formula can be simplified, using the abbreviations NOT, PRIME, AND,
IMPLIES, and DIVIDES, to:

      (IMPLIES (AND (IMPLIES (AND (PRIME1 P (SUB1 P))
                                  (LESSP 1 Y)
                                  (IF (LESSP (SUB1 P) Y) F T))
                             (NOT (EQUAL (REMAINDER P Y) 0)))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (LESSP 1 Y)
                    (LESSP Y P))
               (NOT (EQUAL (REMAINDER P Y) 0))),

which simplifies, expanding the functions AND, EQUAL, NOT, and IMPLIES, to the
goal:

      (IMPLIES (AND (LESSP (SUB1 P) Y)
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (LESSP 1 Y)
                    (LESSP Y P))
               (NOT (EQUAL (REMAINDER P Y) 0))).

However this again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

LITTLE-STEP-AUX2


(PROVE-LEMMA LITTLE-STEP-AUX3 NIL
             (IMPLIES (AND (LESSP 1 P)
                           (LESSP 1 Y)
                           (DIVIDES Y P))
                      (LEQ Y P)))

This formula can be simplified, using the abbreviations AND, IMPLIES, and
DIVIDES, to:

      (IMPLIES (AND (LESSP 1 P)
                    (LESSP 1 Y)
                    (EQUAL (REMAINDER P Y) 0))
               (NOT (LESSP P Y))),

which simplifies, expanding the functions REMAINDER, EQUAL, and LESSP, to two
new formulas:

Case 2. (IMPLIES (AND (LESSP 1 P)
                      (LESSP 1 Y)
                      (EQUAL P 0)
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (LESSP 1 P)
                      (LESSP 1 Y)
                      (NOT (NUMBERP P))
                      (NOT (EQUAL Y 0)))
                 (NOT (NUMBERP Y))),

  which again simplifies, opening up LESSP, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

LITTLE-STEP-AUX3


(PROVE-LEMMA LITTLE-STEP
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (LESSP 1 Y)
                           (NOT (EQUAL Y P)))
                      (NOT (DIVIDES Y P)))
             ((USE (LITTLE-STEP-AUX3 (P P) (Y Y))
                   (LITTLE-STEP-AUX2 (P P) (Y Y)))
              (DISABLE LITTLE-STEP-AUX2)))

WARNING:  Note that the rewrite rule LITTLE-STEP will be stored so as to apply
only to terms with the nonrecursive function symbol DIVIDES.


This conjecture can be simplified, using the abbreviations NOT, PRIME, IMPLIES,
AND, and DIVIDES, to:

      (IMPLIES (AND (IMPLIES (AND (LESSP 1 P)
                                  (LESSP 1 Y)
                                  (EQUAL (REMAINDER P Y) 0))
                             (IF (LESSP P Y) F T))
                    (IMPLIES (AND (PRIME P)
                                  (LESSP 1 Y)
                                  (LESSP Y P))
                             (NOT (EQUAL (REMAINDER P Y) 0)))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (LESSP 1 Y)
                    (NOT (EQUAL Y P)))
               (NOT (EQUAL (REMAINDER P Y) 0))).

This simplifies, applying REMAINDER-0-CROCK and DIFFERENCE-0, and unfolding
the definitions of SUB1, NUMBERP, EQUAL, LESSP, AND, IMPLIES, PRIME1, PRIME,
NOT, and REMAINDER, to the conjecture:

      (IMPLIES (AND (NOT (LESSP P Y))
                    (NOT (LESSP Y P))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (LESSP 1 Y)
                    (NOT (EQUAL Y P))
                    (NOT (EQUAL Y 0)))
               (NOT (NUMBERP Y))).

However this again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

LITTLE-STEP


(PROVE-LEMMA EXACT-REMAINDER-QUOTIENT
             (REWRITE)
             (IMPLIES (AND (NUMBERP X) (DIVIDES P X))
                      (EQUAL (TIMES P (QUOTIENT X P)) X)))

WARNING:  the newly proposed lemma, EXACT-REMAINDER-QUOTIENT, could be applied
whenever the previously added lemma QUOTIENT-TIMES1 could.




WARNING:  the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the newly proposed EXACT-REMAINDER-QUOTIENT could!


This conjecture can be simplified, using the abbreviations AND, IMPLIES, and
DIVIDES, to:

      (IMPLIES (AND (NUMBERP X)
                    (EQUAL (REMAINDER X P) 0))
               (EQUAL (TIMES P (QUOTIENT X P)) X)).

This simplifies, applying QUOTIENT-DIVIDES, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

EXACT-REMAINDER-QUOTIENT


(PROVE-LEMMA DIVIDES-PRODUCT-AUX1
             (REWRITE)
             (IMPLIES (DIVIDES P X)
                      (EQUAL (TIMES X Y)
                             (TIMES P (TIMES (QUOTIENT X P) Y)))))

WARNING:  Note that DIVIDES-PRODUCT-AUX1 contains the free variable P which
will be chosen by instantiating the hypothesis (DIVIDES P X).


WARNING:  the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the newly proposed DIVIDES-PRODUCT-AUX1 could!


This formula can be simplified, using the abbreviations IMPLIES and DIVIDES,
to:

      (IMPLIES (EQUAL (REMAINDER X P) 0)
               (EQUAL (TIMES X Y)
                      (TIMES P (QUOTIENT X P) Y))),

which simplifies, rewriting with COMMUTATIVITY-OF-TIMES, to:

      (IMPLIES (EQUAL (REMAINDER X P) 0)
               (EQUAL (TIMES X Y)
                      (TIMES P Y (QUOTIENT X P)))).

Applying the lemma REMAINDER-QUOTIENT-ELIM, replace X by (PLUS Z (TIMES P V))
to eliminate (REMAINDER X P) and (QUOTIENT X P).  We use LESSP-REMAINDER2, the
type restriction lemma noted when REMAINDER was introduced, and the type
restriction lemma noted when QUOTIENT was introduced to restrict the new
variables.  We would thus like to prove the following four new goals:

Case 4. (IMPLIES (AND (NOT (NUMBERP X))
                      (EQUAL (REMAINDER X P) 0))
                 (EQUAL (TIMES X Y)
                        (TIMES P Y (QUOTIENT X P)))).

  But this further simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and
  expanding the functions LESSP, REMAINDER, EQUAL, TIMES, and QUOTIENT, to:

        T.

Case 3. (IMPLIES (AND (EQUAL P 0)
                      (EQUAL (REMAINDER X P) 0))
                 (EQUAL (TIMES X Y)
                        (TIMES P Y (QUOTIENT X P)))).

  This further simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and
  expanding the definitions of EQUAL, REMAINDER, TIMES, and QUOTIENT, to:

        T.

Case 2. (IMPLIES (AND (NOT (NUMBERP P))
                      (EQUAL (REMAINDER X P) 0))
                 (EQUAL (TIMES X Y)
                        (TIMES P Y (QUOTIENT X P)))).

  But this further simplifies, appealing to the lemmas REMAINDER-WRT-12,
  COMMUTATIVITY-OF-TIMES, and TIMES-ZERO2, and opening up the definitions of
  EQUAL, TIMES, and QUOTIENT, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP Z)
                      (EQUAL (LESSP Z P) (NOT (ZEROP P)))
                      (NUMBERP V)
                      (NUMBERP P)
                      (NOT (EQUAL P 0))
                      (EQUAL Z 0))
                 (EQUAL (TIMES (PLUS Z (TIMES P V)) Y)
                        (TIMES P Y V))),

  which further simplifies, rewriting with the lemmas ASSOCIATIVITY-OF-TIMES
  and COMMUTATIVITY-OF-TIMES, and expanding NUMBERP, EQUAL, LESSP, ZEROP, NOT,
  and PLUS, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDES-PRODUCT-AUX1


(PROVE-LEMMA DIVIDES-PRODUCT-AUX2
             (REWRITE)
             (EQUAL (DIVIDES P (TIMES P W)) T)
             ((USE (DIVIDES-TIMES (Z P) (X W)))
              (DISABLE DIVIDES-TIMES)
              (DO-NOT-INDUCT T)))

WARNING:  Note that the rewrite rule DIVIDES-PRODUCT-AUX2 will be stored so as
to apply only to terms with the nonrecursive function symbol DIVIDES.


This conjecture can be simplified, using the abbreviation DIVIDES, to:

      (IMPLIES (EQUAL (REMAINDER (TIMES W P) P) 0)
               (EQUAL (EQUAL (REMAINDER (TIMES P W) P) 0)
                      T)).

This simplifies, rewriting with the lemma COMMUTATIVITY-OF-TIMES, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDES-PRODUCT-AUX2


(PROVE-LEMMA DIVIDES-PRODUCT
             (REWRITE)
             (IMPLIES (DIVIDES P X)
                      (DIVIDES P (TIMES X Y)))
             ((DO-NOT-INDUCT T)
              (USE (DIVIDES-PRODUCT-AUX1 (X X)
                                         (Y Y)
                                         (P P))
                   (DIVIDES-PRODUCT-AUX2 (P P)
                                         (W (TIMES (QUOTIENT X P) Y))))
              (DISABLE DIVIDES-PRODUCT-AUX1 DIVIDES-PRODUCT-AUX2)))

WARNING:  Note that the rewrite rule DIVIDES-PRODUCT will be stored so as to
apply only to terms with the nonrecursive function symbol DIVIDES.


This formula can be simplified, using the abbreviations IMPLIES, AND, and
DIVIDES, to:

      (IMPLIES (AND (IMPLIES (EQUAL (REMAINDER X P) 0)
                             (EQUAL (TIMES X Y)
                                    (TIMES P (QUOTIENT X P) Y)))
                    (EQUAL (EQUAL (REMAINDER (TIMES P (QUOTIENT X P) Y)
                                             P)
                                  0)
                           T)
                    (EQUAL (REMAINDER X P) 0))
               (EQUAL (REMAINDER (TIMES X Y) P) 0)),

which simplifies, rewriting with COMMUTATIVITY-OF-TIMES and DIVIDES-TIMES1,
and unfolding the functions EQUAL and IMPLIES, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDES-PRODUCT


(PROVE-LEMMA DIVIDES-SUM
             (REWRITE)
             (IMPLIES (AND (DIVIDES P (PLUS U V))
                           (DIVIDES P V))
                      (DIVIDES P U)))

WARNING:  Note that the rewrite rule DIVIDES-SUM will be stored so as to apply
only to terms with the nonrecursive function symbol DIVIDES.


WARNING:  Note that DIVIDES-SUM contains the free variable V which will be
chosen by instantiating the hypothesis (DIVIDES P (PLUS U V)).


This conjecture can be simplified, using the abbreviations AND, IMPLIES, and
DIVIDES, to the goal:

      (IMPLIES (AND (EQUAL (REMAINDER (PLUS U V) P) 0)
                    (EQUAL (REMAINDER V P) 0))
               (EQUAL (REMAINDER U P) 0)).

This simplifies, applying the lemma DIVIDES-PLUS-REWRITE-COMMUTED, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDES-SUM


(PROVE-LEMMA DIVIDES-REDUCTION-AUX1
             (REWRITE)
             (IMPLIES (LESSP 1 P)
                      (EQUAL (PLUS (REMAINDER P B)
                                   (TIMES B (QUOTIENT P B)))
                             P)))

WARNING:  the previously added lemma, REMAINDER-QUOTIENT, could be applied
whenever the newly proposed DIVIDES-REDUCTION-AUX1 could!


WARNING:  the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied
whenever the newly proposed DIVIDES-REDUCTION-AUX1 could!


This formula simplifies, rewriting with the lemma REMAINDER-QUOTIENT, to:

      (IMPLIES (AND (LESSP 1 P) (NOT (NUMBERP P)))
               (EQUAL 0 P)),

which again simplifies, expanding LESSP, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDES-REDUCTION-AUX1


(PROVE-LEMMA DIVIDES-REDUCTION-AUX2
             (REWRITE)
             (IMPLIES (LESSP 1 P)
                      (EQUAL (PLUS (TIMES A (REMAINDER P B))
                                   (TIMES A (TIMES B (QUOTIENT P B))))
                             (TIMES A P))))

WARNING:  the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied
whenever the newly proposed DIVIDES-REDUCTION-AUX2 could!


.

Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace P by
(PLUS X (TIMES B Z)) to eliminate (REMAINDER P B) and (QUOTIENT P B).  We rely
upon LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was
introduced, and the type restriction lemma noted when QUOTIENT was introduced
to constrain the new variables.  This generates four new goals:

Case 4. (IMPLIES (AND (NOT (NUMBERP P)) (LESSP 1 P))
                 (EQUAL (PLUS (TIMES A (REMAINDER P B))
                              (TIMES A B (QUOTIENT P B)))
                        (TIMES A P))),

  which simplifies, unfolding the function LESSP, to:

        T.

Case 3. (IMPLIES (AND (EQUAL B 0) (LESSP 1 P))
                 (EQUAL (PLUS (TIMES A (REMAINDER P B))
                              (TIMES A B (QUOTIENT P B)))
                        (TIMES A P))),

  which simplifies, applying COMMUTATIVITY-OF-TIMES and COMMUTATIVITY-OF-PLUS,
  and opening up the definitions of EQUAL, REMAINDER, QUOTIENT, TIMES, and
  PLUS, to:

        (IMPLIES (AND (LESSP 1 P) (NOT (NUMBERP P)))
                 (EQUAL (TIMES A 0) (TIMES A P))),

  which again simplifies, expanding the function LESSP, to:

        T.

Case 2. (IMPLIES (AND (NOT (NUMBERP B)) (LESSP 1 P))
                 (EQUAL (PLUS (TIMES A (REMAINDER P B))
                              (TIMES A B (QUOTIENT P B)))
                        (TIMES A P))),

  which simplifies, applying the lemmas REMAINDER-WRT-12, TIMES-ZERO2,
  COMMUTATIVITY-OF-TIMES, and COMMUTATIVITY-OF-PLUS, and expanding the
  functions QUOTIENT, EQUAL, TIMES, and PLUS, to:

        (IMPLIES (AND (NOT (NUMBERP B))
                      (LESSP 1 P)
                      (NOT (NUMBERP P)))
                 (EQUAL (TIMES A 0) (TIMES A P))).

  But this again simplifies, opening up LESSP, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP X)
                      (EQUAL (LESSP X B) (NOT (ZEROP B)))
                      (NUMBERP Z)
                      (NUMBERP B)
                      (NOT (EQUAL B 0))
                      (LESSP 1 (PLUS X (TIMES B Z))))
                 (EQUAL (PLUS (TIMES A X) (TIMES A B Z))
                        (TIMES A (PLUS X (TIMES B Z))))),

  which simplifies, rewriting with DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and
  unfolding ZEROP and NOT, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDES-REDUCTION-AUX2


(PROVE-LEMMA DIVIDES-REDUCTION-AUX3
             (REWRITE)
             (IMPLIES (LESSP 1 P)
                      (DIVIDES P
                               (PLUS (TIMES A (REMAINDER P B))
                                     (TIMES A (TIMES B (QUOTIENT P B)))))))

WARNING:  Note that the rewrite rule DIVIDES-REDUCTION-AUX3 will be stored so
as to apply only to terms with the nonrecursive function symbol DIVIDES.


This formula can be simplified, using the abbreviations IMPLIES and DIVIDES,
to:

      (IMPLIES (LESSP 1 P)
               (EQUAL (REMAINDER (PLUS (TIMES A (REMAINDER P B))
                                       (TIMES A B (QUOTIENT P B)))
                                 P)
                      0)),

which simplifies, rewriting with DIVIDES-REDUCTION-AUX2 and DIVIDES-TIMES, and
expanding the definition of EQUAL, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDES-REDUCTION-AUX3


(PROVE-LEMMA DIVIDES-REDUCTION-AUX4
             (REWRITE)
             (IMPLIES (DIVIDES P (TIMES A B))
                      (DIVIDES P
                               (TIMES A (TIMES B ANYTHING))))
             ((DO-NOT-INDUCT T)
              (USE (DIVIDES-PRODUCT (P P)
                                    (X (TIMES A B))
                                    (Y ANYTHING)))
              (DISABLE DIVIDES-PRODUCT)))

WARNING:  Note that the rewrite rule DIVIDES-REDUCTION-AUX4 will be stored so
as to apply only to terms with the nonrecursive function symbol DIVIDES.


This conjecture can be simplified, using the abbreviations IMPLIES,
ASSOCIATIVITY-OF-TIMES, and DIVIDES, to:

      (IMPLIES (AND (IMPLIES (EQUAL (REMAINDER (TIMES A B) P) 0)
                             (EQUAL (REMAINDER (TIMES A B ANYTHING) P)
                                    0))
                    (EQUAL (REMAINDER (TIMES A B) P) 0))
               (EQUAL (REMAINDER (TIMES A B ANYTHING) P)
                      0)).

This simplifies, rewriting with COMMUTATIVITY-OF-TIMES, and expanding the
functions EQUAL and IMPLIES, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDES-REDUCTION-AUX4


(PROVE-LEMMA DIVIDES-REDUCTION
             (REWRITE)
             (IMPLIES (AND (LESSP 1 P)
                           (DIVIDES P (TIMES A B)))
                      (DIVIDES P (TIMES A (REMAINDER P B))))
             ((DO-NOT-INDUCT T)
              (USE (DIVIDES-REDUCTION-AUX3 (P P)
                                           (A A)
                                           (B B))
                   (DIVIDES-REDUCTION-AUX4 (P P)
                                           (A A)
                                           (B B)
                                           (ANYTHING (QUOTIENT P B)))
                   (DIVIDES-SUM (P P)
                                (U (TIMES A (REMAINDER P B)))
                                (V (TIMES A (TIMES B (QUOTIENT P B))))))
              (DISABLE DIVIDES-REDUCTION-AUX3 DIVIDES-REDUCTION-AUX4
                       DIVIDES-SUM DIVIDES-REDUCTION-AUX2)))

WARNING:  Note that the rewrite rule DIVIDES-REDUCTION will be stored so as to
apply only to terms with the nonrecursive function symbol DIVIDES.


This conjecture can be simplified, using the abbreviations IMPLIES, AND, and
DIVIDES, to:

      (IMPLIES
         (AND (IMPLIES (LESSP 1 P)
                       (EQUAL (REMAINDER (PLUS (TIMES A (REMAINDER P B))
                                               (TIMES A B (QUOTIENT P B)))
                                         P)
                              0))
              (IMPLIES (EQUAL (REMAINDER (TIMES A B) P) 0)
                       (EQUAL (REMAINDER (TIMES A B (QUOTIENT P B))
                                         P)
                              0))
              (IMPLIES (AND (EQUAL (REMAINDER (PLUS (TIMES A (REMAINDER P B))
                                                    (TIMES A B (QUOTIENT P B)))
                                              P)
                                   0)
                            (EQUAL (REMAINDER (TIMES A B (QUOTIENT P B))
                                              P)
                                   0))
                       (EQUAL (REMAINDER (TIMES A (REMAINDER P B))
                                         P)
                              0))
              (LESSP 1 P)
              (EQUAL (REMAINDER (TIMES A B) P) 0))
         (EQUAL (REMAINDER (TIMES A (REMAINDER P B))
                           P)
                0)).

This simplifies, opening up IMPLIES, EQUAL, and AND, to:

      T.

Q.E.D.


[ 0.0 0.2 0.0 ]

DIVIDES-REDUCTION


(PROVE-LEMMA PRIME-DIVIDES-SMALL-PRODUCT-AUX1
             (REWRITE)
             (IMPLIES (DIVIDES P (TIMES A 1))
                      (DIVIDES P A)))

WARNING:  Note that the rewrite rule PRIME-DIVIDES-SMALL-PRODUCT-AUX1 will be
stored so as to apply only to terms with the nonrecursive function symbol
DIVIDES.


This conjecture can be simplified, using the abbreviations IMPLIES and DIVIDES,
to:

      (IMPLIES (EQUAL (REMAINDER (TIMES A 1) P) 0)
               (EQUAL (REMAINDER A P) 0)).

This simplifies, applying COMMUTATIVITY-OF-PLUS and COMMUTATIVITY-OF-TIMES,
and unfolding the functions SUB1, NUMBERP, EQUAL, TIMES, PLUS, LESSP, and
REMAINDER, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PRIME-DIVIDES-SMALL-PRODUCT-AUX1


(PROVE-LEMMA PRIME-DIVIDES-SMALL-PRODUCT-AUX2
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (LESSP 1 B)
                           (LESSP B P))
                      (LESSP 0 (REMAINDER P B)))
             ((USE (LITTLE-STEP (P P) (Y B)))
              (DISABLE LITTLE-STEP)))

WARNING:  Note that the proposed lemma PRIME-DIVIDES-SMALL-PRODUCT-AUX2 is to
be stored as zero type prescription rules, zero compound recognizer rules, one
linear rule, and zero replacement rules.


This formula can be simplified, using the abbreviations PRIME, AND, IMPLIES,
and DIVIDES, to:

      (IMPLIES (AND (IMPLIES (AND (PRIME P)
                                  (LESSP 1 B)
                                  (NOT (EQUAL B P)))
                             (NOT (EQUAL (REMAINDER P B) 0)))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (LESSP 1 B)
                    (LESSP B P))
               (LESSP 0 (REMAINDER P B))),

which simplifies, rewriting with REMAINDER-X-X, and unfolding the functions
PRIME, NOT, AND, IMPLIES, LESSP, and EQUAL, to the new goal:

      (IMPLIES (AND (EQUAL B P)
                    (NOT (EQUAL B 0))
                    (NUMBERP B)
                    (NOT (EQUAL B 1))
                    (PRIME1 B (SUB1 B))
                    (LESSP 1 B))
               (NOT (LESSP B B))),

which again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PRIME-DIVIDES-SMALL-PRODUCT-AUX2


(PROVE-LEMMA PRIME-DIVIDES-SMALL-PRODUCT-AUX3
             (REWRITE)
             (IMPLIES (LESSP 0 B)
                      (OR (LESSP 1 B) (EQUAL 1 B))))

WARNING:  Note that the rewrite rule PRIME-DIVIDES-SMALL-PRODUCT-AUX3 will be
stored so as to apply only to terms with the nonrecursive function symbol OR.


This simplifies, using linear arithmetic, to:

      (IMPLIES (AND (NOT (NUMBERP B))
                    (LESSP 0 B)
                    (NOT (LESSP 1 B)))
               (EQUAL 1 B)),

which again simplifies, unfolding the definition of LESSP, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PRIME-DIVIDES-SMALL-PRODUCT-AUX3


(PROVE-LEMMA PRIME-DIVIDES-SMALL-PRODUCT-AUX4 NIL
             (IMPLIES (AND (LESSP 0 B)
                           (DIVIDES P (TIMES A B))
                           (NOT (DIVIDES P A)))
                      (LESSP 1 B)))

This conjecture can be simplified, using the abbreviations NOT, AND, IMPLIES,
and DIVIDES, to the formula:

      (IMPLIES (AND (LESSP 0 B)
                    (EQUAL (REMAINDER (TIMES A B) P) 0)
                    (NOT (EQUAL (REMAINDER A P) 0)))
               (LESSP 1 B)).

This simplifies, using linear arithmetic, to the following two new conjectures:

Case 2. (IMPLIES (AND (NOT (NUMBERP B))
                      (LESSP 0 B)
                      (EQUAL (REMAINDER (TIMES A B) P) 0)
                      (NOT (EQUAL (REMAINDER A P) 0)))
                 (LESSP 1 B)).

  However this again simplifies, opening up the definition of LESSP, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP B)
                      (LESSP 0 1)
                      (EQUAL (REMAINDER (TIMES A 1) P) 0)
                      (NOT (EQUAL (REMAINDER A P) 0)))
                 (LESSP 1 1)),

  which again simplifies, appealing to the lemmas COMMUTATIVITY-OF-PLUS and
  COMMUTATIVITY-OF-TIMES, and unfolding LESSP, SUB1, NUMBERP, EQUAL, TIMES,
  PLUS, and REMAINDER, to:

        T.

Q.E.D.


[ 0.0 0.2 0.0 ]

PRIME-DIVIDES-SMALL-PRODUCT-AUX4


(PROVE-LEMMA PRIME-DIVIDES-SMALL-PRODUCT-AUX5 NIL
             (IMPLIES (AND (PRIME P) (LESSP 1 B))
                      (LESSP (REMAINDER P B) B)))

This formula can be simplified, using the abbreviations PRIME, AND, and
IMPLIES, to:

      (IMPLIES (AND (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (LESSP 1 B))
               (LESSP (REMAINDER P B) B)),

which simplifies, rewriting with LESSP-REMAINDER2, to the following two new
conjectures:

Case 2. (IMPLIES (AND (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP 1 B))
                 (NOT (EQUAL B 0))).

  This again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP 1 B))
                 (NUMBERP B)),

  which again simplifies, expanding LESSP, to:

        T.

Q.E.D.


[ 0.0 0.1 0.0 ]

PRIME-DIVIDES-SMALL-PRODUCT-AUX5


(PROVE-LEMMA PRIME-DIVIDES-SMALL-PRODUCT-AUX6 NIL
             (IMPLIES (AND (PRIME P)
                           (LESSP 1 B)
                           (LESSP B P))
                      (LESSP 0 (REMAINDER P B))))

This formula can be simplified, using the abbreviations PRIME, AND, and
IMPLIES, to:

      (IMPLIES (AND (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (LESSP 1 B)
                    (LESSP B P))
               (LESSP 0 (REMAINDER P B))),

which simplifies, using linear arithmetic, rewriting with
PRIME-DIVIDES-SMALL-PRODUCT-AUX2, and unfolding PRIME, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PRIME-DIVIDES-SMALL-PRODUCT-AUX6


(PROVE-LEMMA PRIME-DIVIDES-SMALL-PRODUCT-AUX7 NIL
             (IMPLIES (AND (PRIME P)
                           (LESSP 1 B)
                           (LESSP B P))
                      (LESSP (REMAINDER P B) P)))

This formula can be simplified, using the abbreviations PRIME, AND, and
IMPLIES, to the new formula:

      (IMPLIES (AND (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (LESSP 1 B)
                    (LESSP B P))
               (LESSP (REMAINDER P B) P)),

which simplifies, appealing to the lemma LESSP-REMAINDER1, to three new goals:

Case 3. (IMPLIES (AND (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP 1 B)
                      (LESSP B P))
                 (NOT (EQUAL B 0))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 2. (IMPLIES (AND (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP 1 B)
                      (LESSP B P))
                 (NUMBERP B)),

  which again simplifies, opening up LESSP, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP 1 B)
                      (LESSP B P))
                 (NOT (LESSP P B))),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.0 0.3 ]

PRIME-DIVIDES-SMALL-PRODUCT-AUX7


(PROVE-LEMMA PRIME-DIVIDES-SMALL-PRODUCT-AUX8 NIL
             (IMPLIES (AND (PRIME P)
                           (LESSP 1 B)
                           (LESSP B P)
                           (DIVIDES P (TIMES A B))
                           (NOT (DIVIDES P A)))
                      (AND (LESSP (REMAINDER P B) B)
                           (LESSP 0 (REMAINDER P B))
                           (LESSP (REMAINDER P B) P)
                           (DIVIDES P (TIMES A (REMAINDER P B)))
                           (NOT (DIVIDES P A))))
             ((USE (PRIME-DIVIDES-SMALL-PRODUCT-AUX5 (A A)
                                                     (B B)
                                                     (P P))
                   (PRIME-DIVIDES-SMALL-PRODUCT-AUX6 (A A)
                                                     (B B)
                                                     (P P))
                   (PRIME-DIVIDES-SMALL-PRODUCT-AUX7 (A A)
                                                     (B B)
                                                     (P P))
                   (DIVIDES-REDUCTION (A A) (B B) (P P)))
              (DISABLE PRIME-DIVIDES-SMALL-PRODUCT-AUX5
                       PRIME-DIVIDES-SMALL-PRODUCT-AUX6
                       PRIME-DIVIDES-SMALL-PRODUCT-AUX7 DIVIDES-REDUCTION)))

This conjecture can be simplified, using the abbreviations NOT, PRIME, IMPLIES,
AND, and DIVIDES, to:

      (IMPLIES (AND (IMPLIES (AND (PRIME P) (LESSP 1 B))
                             (LESSP (REMAINDER P B) B))
                    (IMPLIES (AND (PRIME P)
                                  (LESSP 1 B)
                                  (LESSP B P))
                             (LESSP 0 (REMAINDER P B)))
                    (IMPLIES (AND (PRIME P)
                                  (LESSP 1 B)
                                  (LESSP B P))
                             (LESSP (REMAINDER P B) P))
                    (IMPLIES (AND (LESSP 1 P)
                                  (EQUAL (REMAINDER (TIMES A B) P) 0))
                             (EQUAL (REMAINDER (TIMES A (REMAINDER P B))
                                               P)
                                    0))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (LESSP 1 B)
                    (LESSP B P)
                    (EQUAL (REMAINDER (TIMES A B) P) 0)
                    (NOT (EQUAL (REMAINDER A P) 0)))
               (AND (LESSP (REMAINDER P B) B)
                    (LESSP 0 (REMAINDER P B))
                    (LESSP (REMAINDER P B) P)
                    (EQUAL (REMAINDER (TIMES A (REMAINDER P B))
                                      P)
                           0)
                    (NOT (EQUAL (REMAINDER A P) 0)))).

This simplifies, rewriting with LESSP-REMAINDER2 and LESSP-REMAINDER1, and
unfolding PRIME, AND, IMPLIES, EQUAL, LESSP, SUB1, NUMBERP, PRIME1, and NOT,
to:

      T.

Q.E.D.


[ 0.0 1.1 0.0 ]

PRIME-DIVIDES-SMALL-PRODUCT-AUX8


(PROVE-LEMMA PRIME-DIVIDES-SMALL-PRODUCT-AUX9 NIL
             (IMPLIES (AND (PRIME P)
                           (LESSP 0 B)
                           (LESSP B P)
                           (DIVIDES P (TIMES A B))
                           (NOT (DIVIDES P A)))
                      (AND (LESSP (REMAINDER P B) B)
                           (LESSP 0 (REMAINDER P B))
                           (LESSP (REMAINDER P B) P)
                           (DIVIDES P (TIMES A (REMAINDER P B)))
                           (NOT (DIVIDES P A))))
             ((USE (PRIME-DIVIDES-SMALL-PRODUCT-AUX8 (A A)
                                                     (B B)
                                                     (P P))
                   (PRIME-DIVIDES-SMALL-PRODUCT-AUX4 (A A)
                                                     (B B)
                                                     (P P)))
              (DISABLE PRIME-DIVIDES-SMALL-PRODUCT-AUX8
                       PRIME-DIVIDES-SMALL-PRODUCT-AUX4)))

This formula can be simplified, using the abbreviations NOT, PRIME, IMPLIES,
AND, and DIVIDES, to:

      (IMPLIES (AND (IMPLIES (AND (PRIME P)
                                  (LESSP 1 B)
                                  (LESSP B P)
                                  (EQUAL (REMAINDER (TIMES A B) P) 0)
                                  (NOT (EQUAL (REMAINDER A P) 0)))
                             (AND (LESSP (REMAINDER P B) B)
                                  (LESSP 0 (REMAINDER P B))
                                  (LESSP (REMAINDER P B) P)
                                  (EQUAL (REMAINDER (TIMES A (REMAINDER P B))
                                                    P)
                                         0)
                                  (NOT (EQUAL (REMAINDER A P) 0))))
                    (IMPLIES (AND (LESSP 0 B)
                                  (EQUAL (REMAINDER (TIMES A B) P) 0)
                                  (NOT (EQUAL (REMAINDER A P) 0)))
                             (LESSP 1 B))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (LESSP 0 B)
                    (LESSP B P)
                    (EQUAL (REMAINDER (TIMES A B) P) 0)
                    (NOT (EQUAL (REMAINDER A P) 0)))
               (AND (LESSP (REMAINDER P B) B)
                    (LESSP 0 (REMAINDER P B))
                    (LESSP (REMAINDER P B) P)
                    (EQUAL (REMAINDER (TIMES A (REMAINDER P B))
                                      P)
                           0)
                    (NOT (EQUAL (REMAINDER A P) 0)))),

which simplifies, rewriting with LESSP-REMAINDER2 and LESSP-REMAINDER1, and
unfolding the definitions of PRIME, EQUAL, NOT, AND, LESSP, and IMPLIES, to:

      T.

Q.E.D.


[ 0.0 0.5 0.0 ]

PRIME-DIVIDES-SMALL-PRODUCT-AUX9


(DEFN KLUDGE
      (B P)
      (IF (NOT (PRIME P))
          0
          (IF (NOT (LESSP 0 B))
              0
              (KLUDGE (REMAINDER P B) P))))

     The lemmas LESSP-REMAINDER2 and COUNT-NUMBERP and the definitions of
LESSP, EQUAL, and PRIME establish that the measure (COUNT B) decreases
according to the well-founded relation LESSP in each recursive call.  Hence,
KLUDGE is accepted under the principle of definition.  From the definition we
can conclude that (NUMBERP (KLUDGE B P)) is a theorem.




[ 0.0 0.0 0.0 ]

KLUDGE


(PROVE-LEMMA PRIME-DIVIDES-SMALL-PRODUCT
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (DIVIDES P (TIMES A B))
                           (LESSP 0 B)
                           (LESSP B P))
                      (DIVIDES P A))
             ((DO-NOT-GENERALIZE T)
              (INDUCT (KLUDGE B P))
              (USE (PRIME-DIVIDES-SMALL-PRODUCT-AUX9 (A A)
                                                     (B B)
                                                     (P P)))
              (DISABLE PRIME-DIVIDES-SMALL-PRODUCT-AUX9)))

WARNING:  Note that the rewrite rule PRIME-DIVIDES-SMALL-PRODUCT will be
stored so as to apply only to terms with the nonrecursive function symbol
DIVIDES.


WARNING:  Note that PRIME-DIVIDES-SMALL-PRODUCT contains the free variable B
which will be chosen by instantiating the hypothesis (DIVIDES P (TIMES A B)).


This formula can be simplified, using the abbreviation DIVIDES, to the new
conjecture:

      (IMPLIES
        (IMPLIES (AND (PRIME P)
                      (LESSP 0 B)
                      (LESSP B P)
                      (EQUAL (REMAINDER (TIMES A B) P) 0)
                      (NOT (EQUAL (REMAINDER A P) 0)))
                 (AND (LESSP (REMAINDER P B) B)
                      (LESSP 0 (REMAINDER P B))
                      (LESSP (REMAINDER P B) P)
                      (EQUAL (REMAINDER (TIMES A (REMAINDER P B))
                                        P)
                             0)
                      (NOT (EQUAL (REMAINDER A P) 0))))
        (AND (OR (PRIME P)
                 (IMPLIES (AND (PRIME P)
                               (EQUAL (REMAINDER (TIMES A B) P) 0)
                               (LESSP 0 B)
                               (LESSP B P))
                          (EQUAL (REMAINDER A P) 0)))
             (OR (NOT (PRIME P))
                 (LESSP 0 B)
                 (IMPLIES (AND (PRIME P)
                               (EQUAL (REMAINDER (TIMES A B) P) 0)
                               (LESSP 0 B)
                               (LESSP B P))
                          (EQUAL (REMAINDER A P) 0)))
             (OR (NOT (PRIME P))
                 (NOT (LESSP 0 B))
                 (NOT (IMPLIES (AND (PRIME P)
                                    (EQUAL (REMAINDER (TIMES A (REMAINDER P B))
                                                      P)
                                           0)
                                    (LESSP 0 (REMAINDER P B))
                                    (LESSP (REMAINDER P B) P))
                               (EQUAL (REMAINDER A P) 0)))
                 (IMPLIES (AND (PRIME P)
                               (EQUAL (REMAINDER (TIMES A B) P) 0)
                               (LESSP 0 B)
                               (LESSP B P))
                          (EQUAL (REMAINDER A P) 0))))),

which simplifies, applying LESSP-REMAINDER2, LESSP-REMAINDER1,
REMAINDER-0-CROCK, DIFFERENCE-0, REMAINDER-WRT-1, EQUAL-TIMES-0,
COMMUTATIVITY-OF-TIMES, REMAINDER-WRT-12, and TIMES-ZERO2, and opening up the
definitions of PRIME, EQUAL, LESSP, NOT, AND, IMPLIES, OR, REMAINDER,
DIFFERENCE, SUB1, NUMBERP, and TIMES, to:

      T.

Q.E.D.


[ 0.0 1.3 0.0 ]

PRIME-DIVIDES-SMALL-PRODUCT


(PROVE-LEMMA DIVIDES-REDUCTION-VAR-AUX1
             (REWRITE)
             (IMPLIES (NUMBERP B)
                      (EQUAL (PLUS (TIMES A (REMAINDER B P))
                                   (TIMES A (TIMES P (QUOTIENT B P))))
                             (TIMES A B))))

WARNING:  the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied
whenever the newly proposed DIVIDES-REDUCTION-VAR-AUX1 could!


.

Applying the lemma REMAINDER-QUOTIENT-ELIM, replace B by (PLUS X (TIMES P Z))
to eliminate (REMAINDER B P) and (QUOTIENT B P).  We rely upon
LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was
introduced, and the type restriction lemma noted when QUOTIENT was introduced
to restrict the new variables.  This produces the following three new
conjectures:

Case 3. (IMPLIES (AND (EQUAL P 0) (NUMBERP B))
                 (EQUAL (PLUS (TIMES A (REMAINDER B P))
                              (TIMES A P (QUOTIENT B P)))
                        (TIMES A B))).

  But this simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES and
  COMMUTATIVITY-OF-PLUS, and unfolding the definitions of EQUAL, REMAINDER,
  QUOTIENT, TIMES, and PLUS, to:

        T.

Case 2. (IMPLIES (AND (NOT (NUMBERP P)) (NUMBERP B))
                 (EQUAL (PLUS (TIMES A (REMAINDER B P))
                              (TIMES A P (QUOTIENT B P)))
                        (TIMES A B))),

  which simplifies, applying REMAINDER-WRT-12, TIMES-ZERO2,
  COMMUTATIVITY-OF-TIMES, and COMMUTATIVITY-OF-PLUS, and unfolding the
  functions QUOTIENT, EQUAL, TIMES, and PLUS, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP X)
                      (EQUAL (LESSP X P) (NOT (ZEROP P)))
                      (NUMBERP Z)
                      (NUMBERP P)
                      (NOT (EQUAL P 0)))
                 (EQUAL (PLUS (TIMES A X) (TIMES A P Z))
                        (TIMES A (PLUS X (TIMES P Z))))).

  But this simplifies, rewriting with DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and
  opening up the functions ZEROP and NOT, to:

        T.

Q.E.D.


[ 0.0 0.1 0.0 ]

DIVIDES-REDUCTION-VAR-AUX1


(PROVE-LEMMA DIVIDES-REDUCTION-VAR-AUX2
             (REWRITE)
             (DIVIDES P (TIMES P ANYTHING)))

WARNING:  Note that the rewrite rule DIVIDES-REDUCTION-VAR-AUX2 will be stored
so as to apply only to terms with the nonrecursive function symbol DIVIDES.


This conjecture can be simplified, using the abbreviation DIVIDES, to:

      (EQUAL (REMAINDER (TIMES P ANYTHING) P)
             0).

This simplifies, rewriting with COMMUTATIVITY-OF-TIMES and DIVIDES-TIMES, and
unfolding EQUAL, to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

DIVIDES-REDUCTION-VAR-AUX2


(PROVE-LEMMA DIVIDES-REDUCTION-VAR-AUX3
             (REWRITE)
             (EQUAL (TIMES A (TIMES P ANYTHING))
                    (TIMES P (TIMES A ANYTHING))))

WARNING:  the previously added lemma, COMMUTATIVITY2-OF-TIMES, could be
applied whenever the newly proposed DIVIDES-REDUCTION-VAR-AUX3 could!


WARNING:  the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the newly proposed DIVIDES-REDUCTION-VAR-AUX3 could!


This simplifies, rewriting with COMMUTATIVITY-OF-TIMES and
COMMUTATIVITY2-OF-TIMES, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDES-REDUCTION-VAR-AUX3


(PROVE-LEMMA DIVIDES-REDUCTION-VAR-AUX4
             (REWRITE)
             (DIVIDES P
                      (TIMES A (TIMES P ANYTHING)))
             ((DO-NOT-INDUCT T)
              (USE (DIVIDES-REDUCTION-VAR-AUX2 (P P)
                                               (ANYTHING (TIMES A ANYTHING)))
                   (DIVIDES-REDUCTION-VAR-AUX3 (P P)
                                               (ANYTHING ANYTHING)
                                               (A A)))
              (DISABLE DIVIDES-REDUCTION-VAR-AUX2 DIVIDES-REDUCTION-VAR-AUX3)))

WARNING:  Note that the rewrite rule DIVIDES-REDUCTION-VAR-AUX4 will be stored
so as to apply only to terms with the nonrecursive function symbol DIVIDES.


This conjecture can be simplified, using the abbreviations AND and DIVIDES, to:

      (IMPLIES (AND (EQUAL (REMAINDER (TIMES P A ANYTHING) P)
                           0)
                    (EQUAL (TIMES A P ANYTHING)
                           (TIMES P A ANYTHING)))
               (EQUAL (REMAINDER (TIMES A P ANYTHING) P)
                      0)).

This simplifies, rewriting with COMMUTATIVITY-OF-TIMES and
COMMUTATIVITY2-OF-TIMES, and expanding the function EQUAL, to:

      T.

Q.E.D.


[ 0.0 0.7 0.0 ]

DIVIDES-REDUCTION-VAR-AUX4


(PROVE-LEMMA DIVIDES-REDUCTION-VAR
             (REWRITE)
             (IMPLIES (AND (NUMBERP B)
                           (DIVIDES P (TIMES A B)))
                      (DIVIDES P (TIMES A (REMAINDER B P))))
             ((DO-NOT-INDUCT T)
              (USE (DIVIDES-REDUCTION-VAR-AUX1 (P P)
                                               (B B))
                   (DIVIDES-REDUCTION-VAR-AUX4 (P P)
                                               (ANYTHING (QUOTIENT B P))
                                               (A A))
                   (DIVIDES-SUM (U (TIMES A (REMAINDER B P)))
                                (V (TIMES A (TIMES P (QUOTIENT B P))))))
              (DISABLE DIVIDES-REDUCTION-VAR-AUX1 DIVIDES-REDUCTION-VAR-AUX4
                       DIVIDES-SUM)))

WARNING:  Note that the rewrite rule DIVIDES-REDUCTION-VAR will be stored so
as to apply only to terms with the nonrecursive function symbol DIVIDES.


This conjecture can be simplified, using the abbreviations IMPLIES, AND, and
DIVIDES, to:

      (IMPLIES
         (AND (IMPLIES (NUMBERP B)
                       (EQUAL (PLUS (TIMES A (REMAINDER B P))
                                    (TIMES A P (QUOTIENT B P)))
                              (TIMES A B)))
              (EQUAL (REMAINDER (TIMES A P (QUOTIENT B P))
                                P)
                     0)
              (IMPLIES (AND (EQUAL (REMAINDER (PLUS (TIMES A (REMAINDER B P))
                                                    (TIMES A P (QUOTIENT B P)))
                                              P)
                                   0)
                            (EQUAL (REMAINDER (TIMES A P (QUOTIENT B P))
                                              P)
                                   0))
                       (EQUAL (REMAINDER (TIMES A (REMAINDER B P))
                                         P)
                              0))
              (NUMBERP B)
              (EQUAL (REMAINDER (TIMES A B) P) 0))
         (EQUAL (REMAINDER (TIMES A (REMAINDER B P))
                           P)
                0)).

This simplifies, expanding the functions IMPLIES, EQUAL, and AND, to:

      T.

Q.E.D.


[ 0.0 0.9 0.0 ]

DIVIDES-REDUCTION-VAR


(PROVE-LEMMA PRIME-DIVIDES-PRODUCT-AUX1
             (REWRITE)
             (IMPLIES (NOT (EQUAL (REMAINDER B P) 0))
                      (EQUAL (LESSP 0 (REMAINDER B P)) T)))

This simplifies, expanding EQUAL and LESSP, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PRIME-DIVIDES-PRODUCT-AUX1


(PROVE-LEMMA PRIME-DIVIDES-PRODUCT-AUX2
             (REWRITE)
             (IMPLIES (PRIME P)
                      (EQUAL (LESSP (REMAINDER B P) P) T)))

WARNING:  the previously added lemma, LESSP-REMAINDER2, could be applied
whenever the newly proposed PRIME-DIVIDES-PRODUCT-AUX2 could!


This conjecture can be simplified, using the abbreviations PRIME and IMPLIES,
to:

      (IMPLIES (AND (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P)))
               (EQUAL (LESSP (REMAINDER B P) P) T)).

This simplifies, applying LESSP-REMAINDER2, and unfolding the definition of
EQUAL, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PRIME-DIVIDES-PRODUCT-AUX2


(PROVE-LEMMA PRIME-DIVIDES-PRODUCT
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (DIVIDES P (TIMES A B))
                           (NOT (DIVIDES P B)))
                      (DIVIDES P A))
             ((DO-NOT-INDUCT T)
              (USE (PRIME-DIVIDES-SMALL-PRODUCT (A A)
                                                (P P)
                                                (B (REMAINDER B P)))
                   (DIVIDES-REDUCTION-VAR (A A)
                                          (B B)
                                          (P P)))
              (DISABLE PRIME-DIVIDES-SMALL-PRODUCT DIVIDES-REDUCTION-VAR)))

WARNING:  Note that the rewrite rule PRIME-DIVIDES-PRODUCT will be stored so
as to apply only to terms with the nonrecursive function symbol DIVIDES.


WARNING:  Note that PRIME-DIVIDES-PRODUCT contains the free variable B which
will be chosen by instantiating the hypothesis (DIVIDES P (TIMES A B)).


This formula can be simplified, using the abbreviations NOT, PRIME, IMPLIES,
AND, and DIVIDES, to:

      (IMPLIES (AND (IMPLIES (AND (PRIME P)
                                  (EQUAL (REMAINDER (TIMES A (REMAINDER B P))
                                                    P)
                                         0)
                                  (LESSP 0 (REMAINDER B P))
                                  (LESSP (REMAINDER B P) P))
                             (EQUAL (REMAINDER A P) 0))
                    (IMPLIES (AND (NUMBERP B)
                                  (EQUAL (REMAINDER (TIMES A B) P) 0))
                             (EQUAL (REMAINDER (TIMES A (REMAINDER B P))
                                               P)
                                    0))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (EQUAL (REMAINDER (TIMES A B) P) 0)
                    (NOT (EQUAL (REMAINDER B P) 0)))
               (EQUAL (REMAINDER A P) 0)),

which simplifies, rewriting with PRIME-DIVIDES-PRODUCT-AUX1,
PRIME-DIVIDES-PRODUCT-AUX2, TIMES-ZERO2, and REMAINDER-0-CROCK, and expanding
PRIME, AND, IMPLIES, EQUAL, LESSP, and REMAINDER, to:

      T.

Q.E.D.


[ 0.0 0.3 0.0 ]

PRIME-DIVIDES-PRODUCT


(PROVE-LEMMA CAR-DIVIDES-TIMES-LIST
             (REWRITE)
             (IMPLIES (LISTP L)
                      (DIVIDES (CAR L) (TIMES-LIST L))))

WARNING:  Note that the rewrite rule CAR-DIVIDES-TIMES-LIST will be stored so
as to apply only to terms with the nonrecursive function symbol DIVIDES.


This conjecture can be simplified, using the abbreviations IMPLIES and DIVIDES,
to the conjecture:

      (IMPLIES (LISTP L)
               (EQUAL (REMAINDER (TIMES-LIST L) (CAR L))
                      0)).

Appealing to the lemma CAR-CDR-ELIM, we now replace L by (CONS X Z) to
eliminate (CAR L) and (CDR L).  The result is:

      (EQUAL (REMAINDER (TIMES-LIST (CONS X Z)) X)
             0).

This simplifies, rewriting with CDR-CONS and CAR-CONS, and unfolding the
function TIMES-LIST, to the new formula:

      (EQUAL (REMAINDER (TIMES X (TIMES-LIST Z)) X)
             0),

which we would normally push and work on later by induction.  But if we must
use induction to prove the input conjecture, we prefer to induct on the
original formulation of the problem.  Thus we will disregard all that we have
previously done, give the name *1 to the original input, and work on it.


     So now let us return to:

(IMPLIES (LISTP L)
         (DIVIDES (CAR L) (TIMES-LIST L))),

named *1.  Let us appeal to the induction principle.  There is only one
suggested induction.  We will induct according to the following scheme:
      (AND (IMPLIES (NLISTP L) (p L))
           (IMPLIES (AND (NOT (NLISTP L)) (p (CDR L)))
                    (p L))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT L) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme leads to three new formulas:

Case 3. (IMPLIES (AND (NLISTP L) (LISTP L))
                 (DIVIDES (CAR L) (TIMES-LIST L))),

  which simplifies, opening up the definition of NLISTP, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (LISTP (CDR L)))
                      (LISTP L))
                 (DIVIDES (CAR L) (TIMES-LIST L))),

  which simplifies, applying the lemma DIVIDES-REDUCTION-VAR-AUX2, and opening
  up the functions NLISTP and TIMES-LIST, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP L))
                      (DIVIDES (CADR L)
                               (TIMES-LIST (CDR L)))
                      (LISTP L))
                 (DIVIDES (CAR L) (TIMES-LIST L))),

  which simplifies, applying DIVIDES-REDUCTION-VAR-AUX2, and expanding the
  definitions of NLISTP, DIVIDES, and TIMES-LIST, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.3 0.0 ]

CAR-DIVIDES-TIMES-LIST


(PROVE-LEMMA DIVIDES-EQUAL
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (PRIME Q)
                           (DIVIDES P Q))
                      (EQUAL (EQUAL P Q) T))
             ((USE (LITTLE-STEP (P P) (Y Q))
                   (LITTLE-STEP (P Q) (Y P)))
              (DISABLE LITTLE-STEP)))

This formula can be simplified, using the abbreviations PRIME, IMPLIES, AND,
and DIVIDES, to:

      (IMPLIES (AND (IMPLIES (AND (PRIME P)
                                  (LESSP 1 Q)
                                  (NOT (EQUAL Q P)))
                             (NOT (EQUAL (REMAINDER P Q) 0)))
                    (IMPLIES (AND (PRIME Q)
                                  (LESSP 1 P)
                                  (NOT (EQUAL P Q)))
                             (NOT (EQUAL (REMAINDER Q P) 0)))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (NOT (EQUAL Q 0))
                    (NUMBERP Q)
                    (NOT (EQUAL Q 1))
                    (PRIME1 Q (SUB1 Q))
                    (EQUAL (REMAINDER Q P) 0))
               (EQUAL (EQUAL P Q) T)),

which simplifies, opening up the definitions of PRIME, SUB1, NUMBERP, EQUAL,
LESSP, NOT, AND, IMPLIES, and PRIME1, to:

      T.

Q.E.D.


[ 0.0 0.2 0.0 ]

DIVIDES-EQUAL


(PROVE-LEMMA PRIME-DIVIDES-LIST-AUX1
             (REWRITE)
             (IMPLIES (AND (PRIME-LIST L)
                           (PRIME P)
                           (LISTP L)
                           (DIVIDES P (TIMES-LIST L))
                           (NOT (DIVIDES P (TIMES-LIST (CDR L)))))
                      (DIVIDES P (CAR L)))
             ((USE (PRIME-DIVIDES-PRODUCT (A (CAR L))
                                          (B (TIMES-LIST (CDR L)))))
              (DISABLE PRIME-DIVIDES-PRODUCT PRIME-DIVIDES-SMALL-PRODUCT-AUX2
                       EXACT-REMAINDER-QUOTIENT DIFFERENCE-0 QUOTIENT-DIVIDES
                       REMAINDER)))

WARNING:  Note that the rewrite rule PRIME-DIVIDES-LIST-AUX1 will be stored so
as to apply only to terms with the nonrecursive function symbol DIVIDES.


This formula can be simplified, using the abbreviations NOT, PRIME, AND,
IMPLIES, and DIVIDES, to the new formula:

      (IMPLIES
       (AND
           (IMPLIES (AND (PRIME P)
                         (EQUAL (REMAINDER (TIMES (CAR L) (TIMES-LIST (CDR L)))
                                           P)
                                0)
                         (NOT (EQUAL (REMAINDER (TIMES-LIST (CDR L)) P)
                                     0)))
                    (EQUAL (REMAINDER (CAR L) P) 0))
           (PRIME-LIST L)
           (NOT (EQUAL P 0))
           (NUMBERP P)
           (NOT (EQUAL P 1))
           (PRIME1 P (SUB1 P))
           (LISTP L)
           (EQUAL (REMAINDER (TIMES-LIST L) P) 0)
           (NOT (EQUAL (REMAINDER (TIMES-LIST (CDR L)) P)
                       0)))
       (EQUAL (REMAINDER (CAR L) P) 0)),

which simplifies, unfolding the definitions of PRIME, NOT, AND, IMPLIES,
PRIME-LIST, and TIMES-LIST, to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

PRIME-DIVIDES-LIST-AUX1


(DISABLE PRIME-DIVIDES-SMALL-PRODUCT-AUX1)

[ 0.0 0.0 0.0 ]

PRIME-DIVIDES-SMALL-PRODUCT-AUX1-OFF


(DISABLE PRIME-DIVIDES-SMALL-PRODUCT-AUX2)

[ 0.0 0.0 0.0 ]

PRIME-DIVIDES-SMALL-PRODUCT-AUX2-OFF


(DISABLE PRIME-DIVIDES-SMALL-PRODUCT)

[ 0.0 0.0 0.0 ]

PRIME-DIVIDES-SMALL-PRODUCT-OFF


(PROVE-LEMMA PRIME-DIVIDES-LIST-AUX2
             (REWRITE)
             (IMPLIES (AND (PRIME-LIST L)
                           (PRIME P)
                           (LISTP L)
                           (DIVIDES P (TIMES-LIST L))
                           (NOT (DIVIDES P (TIMES-LIST (CDR L)))))
                      (EQUAL (CAR L) P))
             ((USE (DIVIDES-EQUAL (P P) (Q (CAR L)))
                   (PRIME-DIVIDES-LIST-AUX1 (P P) (L L)))
              (DISABLE DIVIDES-EQUAL PRIME-DIVIDES-LIST-AUX1 QUOTIENT-DIVIDES)))

WARNING:  Note that PRIME-DIVIDES-LIST-AUX2 contains the free variable P which
will be chosen by instantiating the hypothesis (PRIME P).


This formula can be simplified, using the abbreviations NOT, PRIME, IMPLIES,
AND, and DIVIDES, to:

      (IMPLIES
              (AND (IMPLIES (AND (PRIME P)
                                 (PRIME (CAR L))
                                 (EQUAL (REMAINDER (CAR L) P) 0))
                            (EQUAL (EQUAL P (CAR L)) T))
                   (IMPLIES (AND (PRIME-LIST L)
                                 (PRIME P)
                                 (LISTP L)
                                 (EQUAL (REMAINDER (TIMES-LIST L) P) 0)
                                 (NOT (EQUAL (REMAINDER (TIMES-LIST (CDR L)) P)
                                             0)))
                            (EQUAL (REMAINDER (CAR L) P) 0))
                   (PRIME-LIST L)
                   (NOT (EQUAL P 0))
                   (NUMBERP P)
                   (NOT (EQUAL P 1))
                   (PRIME1 P (SUB1 P))
                   (LISTP L)
                   (EQUAL (REMAINDER (TIMES-LIST L) P) 0)
                   (NOT (EQUAL (REMAINDER (TIMES-LIST (CDR L)) P)
                               0)))
              (EQUAL (CAR L) P)),

which simplifies, using linear arithmetic, applying the lemmas
REMAINDER-0-CROCK and DIFFERENCE-0, and opening up the definitions of PRIME,
AND, EQUAL, IMPLIES, PRIME-LIST, NOT, LESSP, REMAINDER, NUMBERP, and SUB1, to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

PRIME-DIVIDES-LIST-AUX2


(DISABLE PRIME-DIVIDES-LIST-AUX1)

[ 0.0 0.0 0.0 ]

PRIME-DIVIDES-LIST-AUX1-OFF


(PROVE-LEMMA PRIME-DIVIDES-LIST-AUX3
             (REWRITE)
             (IMPLIES (AND (PRIME P) (NLISTP L))
                      (NOT (DIVIDES P (TIMES-LIST L)))))

WARNING:  Note that the rewrite rule PRIME-DIVIDES-LIST-AUX3 will be stored so
as to apply only to terms with the nonrecursive function symbol DIVIDES.


This formula can be simplified, using the abbreviations NOT, NLISTP, PRIME,
AND, IMPLIES, and DIVIDES, to the new conjecture:

      (IMPLIES (AND (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (NOT (LISTP L)))
               (NOT (EQUAL (REMAINDER (TIMES-LIST L) P)
                           0))),

which simplifies, using linear arithmetic, rewriting with REMAINDER-0-CROCK
and DIFFERENCE-0, and opening up TIMES-LIST, LESSP, EQUAL, NUMBERP, SUB1, and
REMAINDER, to the new formula:

      (IMPLIES (AND (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (NOT (LISTP L)))
               (NOT (EQUAL (SUB1 P) 0))),

which again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

PRIME-DIVIDES-LIST-AUX3


(PROVE-LEMMA PRIME-DIVIDES-LIST-AUX4 NIL
             (IMPLIES (AND (PRIME-LIST L)
                           (PRIME P)
                           (DIVIDES P (TIMES-LIST L)))
                      (AND (LISTP L)
                           (OR (EQUAL (CAR L) P)
                               (DIVIDES P (TIMES-LIST (CDR L))))))
             ((USE (PRIME-DIVIDES-LIST-AUX3 (P P) (L L))
                   (PRIME-DIVIDES-LIST-AUX2 (P P) (L L)))
              (DISABLE QUOTIENT-DIVIDES DIVIDES-EQUAL LITTLE-STEP-AUX1
                       PRIME-DIVIDES-LIST-AUX3 PRIME-DIVIDES-LIST-AUX2)))

This conjecture can be simplified, using the abbreviations PRIME, IMPLIES, AND,
and DIVIDES, to:

      (IMPLIES
              (AND (IMPLIES (AND (PRIME P) (NLISTP L))
                            (NOT (EQUAL (REMAINDER (TIMES-LIST L) P)
                                        0)))
                   (IMPLIES (AND (PRIME-LIST L)
                                 (PRIME P)
                                 (LISTP L)
                                 (EQUAL (REMAINDER (TIMES-LIST L) P) 0)
                                 (NOT (EQUAL (REMAINDER (TIMES-LIST (CDR L)) P)
                                             0)))
                            (EQUAL (CAR L) P))
                   (PRIME-LIST L)
                   (NOT (EQUAL P 0))
                   (NUMBERP P)
                   (NOT (EQUAL P 1))
                   (PRIME1 P (SUB1 P))
                   (EQUAL (REMAINDER (TIMES-LIST L) P)
                          0))
              (AND (LISTP L)
                   (OR (EQUAL (CAR L) P)
                       (EQUAL (REMAINDER (TIMES-LIST (CDR L)) P)
                              0)))).

This simplifies, opening up PRIME, NLISTP, AND, EQUAL, NOT, IMPLIES,
PRIME-LIST, TIMES-LIST, OR, and TIMES, to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

PRIME-DIVIDES-LIST-AUX4


(DISABLE PRIME-DIVIDES-LIST-AUX2)

[ 0.0 0.0 0.0 ]

PRIME-DIVIDES-LIST-AUX2-OFF


(DISABLE PRIME-DIVIDES-LIST-AUX3)

[ 0.0 0.0 0.0 ]

PRIME-DIVIDES-LIST-AUX3-OFF


(PROVE-LEMMA PRIME-DIVIDES-LIST
             (REWRITE)
             (IMPLIES (AND (PRIME-LIST L)
                           (PRIME P)
                           (DIVIDES P (TIMES-LIST L)))
                      (MEMBER P L))
             ((INDUCT (PRIME-LIST L))
              (USE (PRIME-DIVIDES-LIST-AUX4 (P P) (L L)))
              (DISABLE QUOTIENT-DIVIDES PRIME1 DIVIDES-PRODUCT DIVIDES-EQUAL
                       TIMES REMAINDER)))

This formula can be simplified, using the abbreviation DIVIDES, to the new
formula:

      (IMPLIES
          (IMPLIES (AND (PRIME-LIST L)
                        (PRIME P)
                        (EQUAL (REMAINDER (TIMES-LIST L) P)
                               0))
                   (AND (LISTP L)
                        (OR (EQUAL (CAR L) P)
                            (EQUAL (REMAINDER (TIMES-LIST (CDR L)) P)
                                   0))))
          (AND (OR (NOT (NLISTP L))
                   (IMPLIES (AND (PRIME-LIST L)
                                 (PRIME P)
                                 (EQUAL (REMAINDER (TIMES-LIST L) P)
                                        0))
                            (MEMBER P L)))
               (OR (NLISTP L)
                   (NOT (IMPLIES (AND (PRIME-LIST (CDR L))
                                      (PRIME P)
                                      (EQUAL (REMAINDER (TIMES-LIST (CDR L)) P)
                                             0))
                                 (MEMBER P (CDR L))))
                   (IMPLIES (AND (PRIME-LIST L)
                                 (PRIME P)
                                 (EQUAL (REMAINDER (TIMES-LIST L) P)
                                        0))
                            (MEMBER P L))))),

which simplifies, rewriting with the lemmas REMAINDER-WRT-12, REMAINDER-WRT-1,
and CDR-NLISTP, and expanding the definitions of PRIME, PRIME-LIST, TIMES-LIST,
AND, OR, IMPLIES, NLISTP, NOT, MEMBER, EQUAL, and LISTP, to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

PRIME-DIVIDES-LIST


(PROVE-LEMMA PRIME-LIST-TIMES-LIST
             (REWRITE)
             (IMPLIES (AND (PRIME C)
                           (PRIME-LIST L2)
                           (NOT (MEMBER C L2)))
                      (NOT (EQUAL (REMAINDER (TIMES-LIST L2) C)
                                  0))))

This conjecture can be simplified, using the abbreviations NOT, PRIME, AND,
and IMPLIES, to the formula:

      (IMPLIES (AND (NOT (EQUAL C 0))
                    (NUMBERP C)
                    (NOT (EQUAL C 1))
                    (PRIME1 C (SUB1 C))
                    (PRIME-LIST L2)
                    (NOT (MEMBER C L2)))
               (NOT (EQUAL (REMAINDER (TIMES-LIST L2) C)
                           0))).

This simplifies, rewriting with PRIME-DIVIDES-LIST, and expanding the
functions DIVIDES, EQUAL, and PRIME, to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

PRIME-LIST-TIMES-LIST


(PROVE-LEMMA PRIME-MEMBER
             (REWRITE)
             (IMPLIES (AND (EQUAL (TIMES C (TIMES-LIST L1))
                                  (TIMES-LIST L2))
                           (PRIME C)
                           (PRIME-LIST L2))
                      (MEMBER C L2))
             ((DISABLE TIMES)))

WARNING:  Note that PRIME-MEMBER contains the free variable L1 which will be
chosen by instantiating the hypothesis:
      (EQUAL (TIMES C (TIMES-LIST L1))
             (TIMES-LIST L2)).



This conjecture can be simplified, using the abbreviations PRIME, AND, and
IMPLIES, to:

      (IMPLIES (AND (EQUAL (TIMES C (TIMES-LIST L1))
                           (TIMES-LIST L2))
                    (NOT (EQUAL C 0))
                    (NUMBERP C)
                    (NOT (EQUAL C 1))
                    (PRIME1 C (SUB1 C))
                    (PRIME-LIST L2))
               (MEMBER C L2)).

This simplifies, rewriting with the lemmas DIVIDES-TIMES1 and
PRIME-DIVIDES-LIST, and expanding the functions DIVIDES, EQUAL, and PRIME, to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

PRIME-MEMBER


(PROVE-LEMMA VOID-CASE
             (REWRITE)
             (IMPLIES (AND (PRIME-LIST L)
                           (EQUAL 1 (TIMES-LIST L)))
                      (NLISTP L))
             ((DO-NOT-INDUCT T)
              (USE (PRIMES-ARE-BIG (P (CAR L))))))

WARNING:  Note that the rewrite rule VOID-CASE will be stored so as to apply
only to terms with the nonrecursive function symbol NLISTP.


This conjecture can be simplified, using the abbreviations NLISTP, AND, and
IMPLIES, to:

      (IMPLIES (AND (IMPLIES (PRIME (CAR L))
                             (EQUAL (LESSP 1 (CAR L)) T))
                    (PRIME-LIST L)
                    (EQUAL 1 (TIMES-LIST L)))
               (NOT (LISTP L))).

This simplifies, unfolding the definitions of PRIME, IMPLIES, and PRIME-LIST,
to the new conjecture:

      (IMPLIES (AND (LESSP 1 (CAR L))
                    (PRIME-LIST L)
                    (EQUAL 1 (TIMES-LIST L)))
               (NOT (LISTP L))).

Applying the lemma CAR-CDR-ELIM, replace L by (CONS X Z) to eliminate (CAR L)
and (CDR L).  We would thus like to prove:

      (IMPLIES (AND (LESSP 1 X)
                    (PRIME-LIST (CONS X Z)))
               (NOT (EQUAL 1 (TIMES-LIST (CONS X Z))))),

which further simplifies, applying CDR-CONS, CAR-CONS, and TIMES-EQUAL-1, and
opening up the definitions of PRIME, PRIME-LIST, and TIMES-LIST, to the new
conjecture:

      (IMPLIES (AND (LESSP 1 X)
                    (NOT (EQUAL X 0))
                    (NUMBERP X)
                    (NOT (EQUAL X 1))
                    (PRIME1 X (SUB1 X))
                    (PRIME-LIST Z)
                    (NOT (EQUAL 0 (TIMES-LIST Z)))
                    (EQUAL 0 (SUB1 X)))
               (NOT (EQUAL 0 (SUB1 (TIMES-LIST Z))))),

which again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.2 0.0 ]

VOID-CASE


(PROVE-LEMMA PRODUCT-DELETE
             (REWRITE)
             (IMPLIES (MEMBER X L)
                      (EQUAL (TIMES-LIST L)
                             (TIMES X (TIMES-LIST (DELETE X L)))))
             ((DISABLE DIVIDES-EQUAL)))

WARNING:  Note that PRODUCT-DELETE contains the free variable X which will be
chosen by instantiating the hypothesis (MEMBER X L).



     Name the conjecture *1.


     Perhaps we can prove it by induction.  Four inductions are suggested by
terms in the conjecture.  They merge into two likely candidate inductions.
However, only one is unflawed.  We will induct according to the following
scheme:
      (AND (IMPLIES (NLISTP L) (p L X))
           (IMPLIES (AND (NOT (NLISTP L))
                         (EQUAL X (CAR L)))
                    (p L X))
           (IMPLIES (AND (NOT (NLISTP L))
                         (NOT (EQUAL X (CAR L)))
                         (p (CDR L) X))
                    (p L X))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT L) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme leads to the following four new conjectures:

Case 4. (IMPLIES (AND (NLISTP L) (MEMBER X L))
                 (EQUAL (TIMES-LIST L)
                        (TIMES X (TIMES-LIST (DELETE X L))))).

  This simplifies, opening up NLISTP and MEMBER, to:

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP L))
                      (EQUAL X (CAR L))
                      (MEMBER X L))
                 (EQUAL (TIMES-LIST L)
                        (TIMES X (TIMES-LIST (DELETE X L))))).

  This simplifies, unfolding the definitions of NLISTP, MEMBER, TIMES-LIST,
  and DELETE, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (EQUAL X (CAR L)))
                      (NOT (MEMBER X (CDR L)))
                      (MEMBER X L))
                 (EQUAL (TIMES-LIST L)
                        (TIMES X (TIMES-LIST (DELETE X L))))).

  This simplifies, expanding NLISTP and MEMBER, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (EQUAL X (CAR L)))
                      (EQUAL (TIMES-LIST (CDR L))
                             (TIMES X
                                    (TIMES-LIST (DELETE X (CDR L)))))
                      (MEMBER X L))
                 (EQUAL (TIMES-LIST L)
                        (TIMES X (TIMES-LIST (DELETE X L))))).

  This simplifies, applying CDR-CONS and CAR-CONS, and opening up the
  definitions of NLISTP, MEMBER, TIMES-LIST, and DELETE, to:

        (IMPLIES (AND (LISTP L)
                      (NOT (EQUAL X (CAR L)))
                      (EQUAL (TIMES-LIST (CDR L))
                             (TIMES X
                                    (TIMES-LIST (DELETE X (CDR L)))))
                      (MEMBER X (CDR L)))
                 (EQUAL (TIMES (CAR L) (TIMES-LIST (CDR L)))
                        (TIMES X
                               (CAR L)
                               (TIMES-LIST (DELETE X (CDR L)))))).

  Appealing to the lemma CAR-CDR-ELIM, we now replace L by (CONS Z V) to
  eliminate (CAR L) and (CDR L).  The result is:

        (IMPLIES (AND (NOT (EQUAL X Z))
                      (EQUAL (TIMES-LIST V)
                             (TIMES X (TIMES-LIST (DELETE X V))))
                      (MEMBER X V))
                 (EQUAL (TIMES Z (TIMES-LIST V))
                        (TIMES X Z
                               (TIMES-LIST (DELETE X V))))).

  We use the above equality hypothesis by substituting:
        (TIMES X (TIMES-LIST (DELETE X V)))
  for (TIMES-LIST V) and throwing away the equality.  We thus obtain:

        (IMPLIES (AND (NOT (EQUAL X Z)) (MEMBER X V))
                 (EQUAL (TIMES Z X (TIMES-LIST (DELETE X V)))
                        (TIMES X Z
                               (TIMES-LIST (DELETE X V))))),

  which further simplifies, rewriting with the lemma
  DIVIDES-REDUCTION-VAR-AUX3, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.3 0.0 ]

PRODUCT-DELETE


(PROVE-LEMMA TIMES-CANCELLATION NIL
             (IMPLIES (AND (LESSP 0 P)
                           (EQUAL (TIMES P X) (TIMES P Y)))
                      (EQUAL (FIX X) (FIX Y)))
             ((DO-NOT-INDUCT T)
              (USE (QUOTIENT-TIMES (Y P) (X X))
                   (QUOTIENT-TIMES (Y P) (X Y)))
              (DISABLE QUOTIENT-TIMES DIVIDES-EQUAL)))

This simplifies, rewriting with TIMES-ZERO2 and COMMUTATIVITY-OF-TIMES, and
opening up the definitions of ZEROP, FIX, EQUAL, TIMES, QUOTIENT, and LESSP,
to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

TIMES-CANCELLATION


(PROVE-LEMMA NUMBER-TIMES-CANCELLATION
             (REWRITE)
             (IMPLIES (AND (NUMBERP X)
                           (NUMBERP Y)
                           (LESSP 0 P)
                           (EQUAL (TIMES P X) (TIMES P Y)))
                      (EQUAL (EQUAL X Y) T))
             ((DO-NOT-INDUCT T)
              (USE (TIMES-CANCELLATION (P P)
                                       (X X)
                                       (Y Y)))))

WARNING:  Note that NUMBER-TIMES-CANCELLATION contains the free variable P
which will be chosen by instantiating the hypothesis (LESSP 0 P).


This simplifies, expanding the functions EQUAL, LESSP, AND, FIX, and IMPLIES,
to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

NUMBER-TIMES-CANCELLATION


(PROVE-LEMMA PRODUCTS-ARE-NUMBERS
             (REWRITE)
             (EQUAL (NUMBERP (TIMES-LIST L)) T))

This formula simplifies, obviously, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PRODUCTS-ARE-NUMBERS


(PROVE-LEMMA DIVIDE-BY-MEMBER-AUX1 NIL
             (IMPLIES (AND (MEMBER P L)
                           (EQUAL (TIMES P X) (TIMES-LIST L)))
                      (EQUAL (TIMES P (TIMES-LIST (DELETE P L)))
                             (TIMES P X)))
             ((DO-NOT-INDUCT T)
              (USE (PRODUCT-DELETE (X P) (L L)))
              (DISABLE QUOTIENT-DIVIDES DIVIDES-EQUAL
                       NUMBER-TIMES-CANCELLATION PRODUCT-DELETE)))

This formula simplifies, opening up IMPLIES, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDE-BY-MEMBER-AUX1


(PROVE-LEMMA DIVIDE-BY-MEMBER-AUX2
             (REWRITE)
             (IMPLIES (AND (EQUAL (TIMES P X) (TIMES-LIST L))
                           (NUMBERP X)
                           (NOT (EQUAL P 0))
                           (NUMBERP P)
                           (EQUAL (TIMES-LIST L)
                                  (TIMES P (TIMES-LIST (DELETE P L)))))
                      (EQUAL (TIMES-LIST (DELETE P L)) X))
             ((USE (NUMBER-TIMES-CANCELLATION (P P)
                                              (X (TIMES-LIST (DELETE P L)))
                                              (Y X)))
              (DISABLE DIVIDES-EQUAL NUMBER-TIMES-CANCELLATION)))

WARNING:  Note that DIVIDE-BY-MEMBER-AUX2 contains the free variable X which
will be chosen by instantiating the hypothesis:
      (EQUAL (TIMES P X) (TIMES-LIST L)).



This conjecture can be simplified, using the abbreviations NOT, AND, IMPLIES,
and PRODUCTS-ARE-NUMBERS, to the formula:

      (IMPLIES (AND (IMPLIES (AND T
                                  (NUMBERP X)
                                  (LESSP 0 P)
                                  (EQUAL (TIMES P (TIMES-LIST (DELETE P L)))
                                         (TIMES P X)))
                             (EQUAL (EQUAL (TIMES-LIST (DELETE P L)) X)
                                    T))
                    (EQUAL (TIMES P X) (TIMES-LIST L))
                    (NUMBERP X)
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (EQUAL (TIMES-LIST L)
                           (TIMES P (TIMES-LIST (DELETE P L)))))
               (EQUAL (TIMES-LIST (DELETE P L)) X)).

This simplifies, unfolding the functions EQUAL, LESSP, AND, and IMPLIES, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDE-BY-MEMBER-AUX2


(PROVE-LEMMA DIVIDE-BY-MEMBER
             (REWRITE)
             (IMPLIES (AND (NUMBERP X)
                           (MEMBER P L)
                           (LESSP 0 P)
                           (EQUAL (TIMES P X) (TIMES-LIST L)))
                      (EQUAL (TIMES-LIST (DELETE P L)) X))
             ((DO-NOT-INDUCT T)
              (USE (DIVIDE-BY-MEMBER-AUX1 (P P)
                                          (X X)
                                          (L L)))
              (DISABLE QUOTIENT-DIVIDES PRIME-DIVIDES-LIST PRODUCT-DELETE
                       PRIME-MEMBER DIVIDES-EQUAL)))

WARNING:  Note that DIVIDE-BY-MEMBER contains the free variable X which will
be chosen by instantiating the hypothesis (NUMBERP X).


This conjecture simplifies, applying the lemma DIVIDE-BY-MEMBER-AUX2, and
opening up the definitions of AND, IMPLIES, EQUAL, and LESSP, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDE-BY-MEMBER


(PROVE-LEMMA DIVIDE-BY-PRIME-MEMBER-AUX1
             (REWRITE)
             (IMPLIES (AND (PRIME-LIST L) (MEMBER P L))
                      (PRIME P))
             ((INDUCT (PRIME-LIST L))
              (DISABLE PRIME PRIME1 QUOTIENT-DIVIDES)))

WARNING:  Note that the rewrite rule DIVIDE-BY-PRIME-MEMBER-AUX1 will be
stored so as to apply only to terms with the nonrecursive function symbol
PRIME.


WARNING:  Note that DIVIDE-BY-PRIME-MEMBER-AUX1 contains the free variable L
which will be chosen by instantiating the hypothesis (PRIME-LIST L).


This formula can be simplified, using the abbreviations IMPLIES, NLISTP, NOT,
OR, and AND, to the following two new formulas:

Case 2. (IMPLIES (AND (NOT (LISTP L))
                      (PRIME-LIST L)
                      (MEMBER P L))
                 (PRIME P)).

  This simplifies, expanding the functions PRIME-LIST and MEMBER, to:

        T.

Case 1. (IMPLIES (AND (LISTP L)
                      (IMPLIES (AND (PRIME-LIST (CDR L))
                                    (MEMBER P (CDR L)))
                               (PRIME P))
                      (PRIME-LIST L)
                      (MEMBER P L))
                 (PRIME P)).

  This simplifies, opening up the definitions of AND, IMPLIES, PRIME-LIST, and
  MEMBER, to:

        (IMPLIES (AND (LISTP L)
                      (NOT (MEMBER P (CDR L)))
                      (PRIME (CAR L))
                      (PRIME-LIST (CDR L))
                      (EQUAL P (CAR L)))
                 (PRIME P)),

  which again simplifies, trivially, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDE-BY-PRIME-MEMBER-AUX1


(PROVE-LEMMA DIVIDE-BY-PRIME-MEMBER
             (REWRITE)
             (IMPLIES (AND (NUMBERP X)
                           (PRIME-LIST L)
                           (MEMBER P L)
                           (EQUAL (TIMES P X) (TIMES-LIST L)))
                      (EQUAL (TIMES-LIST (DELETE P L)) X))
             ((DO-NOT-INDUCT T)
              (USE (PRIMES-ARE-BIG (P P)))
              (DISABLE PRIME LESSP-TIMES-2 DIVIDES-EQUAL PRIME-DIVIDES-LIST
                       QUOTIENT-DIVIDES PRODUCT-DELETE)))

WARNING:  Note that DIVIDE-BY-PRIME-MEMBER contains the free variable X which
will be chosen by instantiating the hypothesis (NUMBERP X).


This formula simplifies, rewriting with the lemma DIVIDE-BY-PRIME-MEMBER-AUX1,
and unfolding the definition of IMPLIES, to the formula:

      (IMPLIES (AND (LESSP 1 P)
                    (NUMBERP X)
                    (PRIME-LIST L)
                    (MEMBER P L)
                    (EQUAL (TIMES P X) (TIMES-LIST L)))
               (EQUAL (TIMES-LIST (DELETE P L)) X)).

This again simplifies, using linear arithmetic and appealing to the lemma
DIVIDE-BY-MEMBER, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

DIVIDE-BY-PRIME-MEMBER


(PROVE-LEMMA REDUCT-PRODUCT
             (REWRITE)
             (IMPLIES (AND (PRIME-LIST L1)
                           (PRIME-LIST L2)
                           (EQUAL (TIMES-LIST L1)
                                  (TIMES-LIST L2))
                           (LISTP L1)
                           (MEMBER (CAR L1) L2))
                      (EQUAL (TIMES-LIST (DELETE (CAR L1) L2))
                             (TIMES-LIST (CDR L1))))
             ((USE (DIVIDE-BY-PRIME-MEMBER (X (TIMES-LIST (CDR L1)))
                                           (P (CAR L1))
                                           (L L2)))
              (DISABLE DIVIDES-EQUAL PRIME1 DIVIDE-BY-PRIME-MEMBER-AUX1
                       PRODUCT-DELETE TIMES DIVIDE-BY-PRIME-MEMBER)
              (DO-NOT-INDUCT T)))

This conjecture can be simplified, using the abbreviations AND, IMPLIES, and
PRODUCTS-ARE-NUMBERS, to:

      (IMPLIES (AND (IMPLIES (AND T
                                  (PRIME-LIST L2)
                                  (MEMBER (CAR L1) L2)
                                  (EQUAL (TIMES (CAR L1) (TIMES-LIST (CDR L1)))
                                         (TIMES-LIST L2)))
                             (EQUAL (TIMES-LIST (DELETE (CAR L1) L2))
                                    (TIMES-LIST (CDR L1))))
                    (PRIME-LIST L1)
                    (PRIME-LIST L2)
                    (EQUAL (TIMES-LIST L1)
                           (TIMES-LIST L2))
                    (LISTP L1)
                    (MEMBER (CAR L1) L2))
               (EQUAL (TIMES-LIST (DELETE (CAR L1) L2))
                      (TIMES-LIST (CDR L1)))).

This simplifies, opening up the definitions of TIMES-LIST, AND, and IMPLIES,
to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

REDUCT-PRODUCT


(DISABLE DIVIDES-EQUAL)

[ 0.0 0.0 0.0 ]

DIVIDES-EQUAL-OFF


(DISABLE DIVIDE-BY-PRIME-MEMBER-AUX1)

[ 0.0 0.0 0.0 ]

DIVIDE-BY-PRIME-MEMBER-AUX1-OFF


(PROVE-LEMMA PRIME-FACTORIZATION-UNIQUENESS-AUX1 NIL
             (IMPLIES (AND (PRIME-LIST L) (LISTP L))
                      (LESSP 1 (TIMES-LIST L))))


     Give the conjecture the name *1.


     We will appeal to induction.  There are two plausible inductions.
However, they merge into one likely candidate induction.  We will induct
according to the following scheme:
      (AND (IMPLIES (NLISTP L) (p L))
           (IMPLIES (AND (NOT (NLISTP L)) (p (CDR L)))
                    (p L))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP establish that the measure (COUNT L) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme produces the following four new formulas:

Case 4. (IMPLIES (AND (NLISTP L)
                      (PRIME-LIST L)
                      (LISTP L))
                 (LESSP 1 (TIMES-LIST L))).

  This simplifies, opening up NLISTP, to:

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (PRIME-LIST (CDR L)))
                      (PRIME-LIST L)
                      (LISTP L))
                 (LESSP 1 (TIMES-LIST L))).

  This simplifies, opening up the definitions of NLISTP, PRIME-LIST, and PRIME,
  to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (LISTP (CDR L)))
                      (PRIME-LIST L)
                      (LISTP L))
                 (LESSP 1 (TIMES-LIST L))).

  This simplifies, opening up the definitions of NLISTP, PRIME-LIST, PRIME,
  and TIMES-LIST, to the new goal:

        (IMPLIES (AND (NOT (LISTP (CDR L)))
                      (NOT (EQUAL (CAR L) 0))
                      (NUMBERP (CAR L))
                      (NOT (EQUAL (CAR L) 1))
                      (PRIME1 (CAR L) (SUB1 (CAR L)))
                      (PRIME-LIST (CDR L))
                      (LISTP L))
                 (LESSP 1
                        (TIMES (CAR L)
                               (TIMES-LIST (CDR L))))),

  which further simplifies, appealing to the lemma COMMUTATIVITY-OF-TIMES, and
  expanding the functions PRIME-LIST and TIMES-LIST, to:

        (IMPLIES (AND (NOT (LISTP (CDR L)))
                      (NOT (EQUAL (CAR L) 0))
                      (NUMBERP (CAR L))
                      (NOT (EQUAL (CAR L) 1))
                      (PRIME1 (CAR L) (SUB1 (CAR L)))
                      (LISTP L))
                 (LESSP 1 (TIMES 1 (CAR L)))).

  But this again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP L))
                      (LESSP 1 (TIMES-LIST (CDR L)))
                      (PRIME-LIST L)
                      (LISTP L))
                 (LESSP 1 (TIMES-LIST L))),

  which simplifies, opening up the functions NLISTP, PRIME-LIST, PRIME, and
  TIMES-LIST, to the goal:

        (IMPLIES (AND (LESSP 1 (TIMES-LIST (CDR L)))
                      (NOT (EQUAL (CAR L) 0))
                      (NUMBERP (CAR L))
                      (NOT (EQUAL (CAR L) 1))
                      (PRIME1 (CAR L) (SUB1 (CAR L)))
                      (PRIME-LIST (CDR L))
                      (LISTP L))
                 (LESSP 1
                        (TIMES (CAR L)
                               (TIMES-LIST (CDR L))))).

  But this again simplifies, using linear arithmetic and applying
  LESSP-TIMES-1, to:

        T.


     That finishes the proof of *1.  Q.E.D.


[ 0.0 0.4 0.0 ]

PRIME-FACTORIZATION-UNIQUENESS-AUX1


(PROVE-LEMMA PRIME-FACTORIZATION-UNIQUENESS-AUX2 NIL
             (IMPLIES (AND (PRIME-LIST L)
                           (EQUAL 1 (TIMES-LIST L)))
                      (NOT (LISTP L)))
             ((USE (PRIME-FACTORIZATION-UNIQUENESS-AUX1 (L L)))))

This formula simplifies, unfolding the definitions of AND, LESSP, and IMPLIES,
to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PRIME-FACTORIZATION-UNIQUENESS-AUX2


(DISABLE PRODUCT-DELETE)

[ 0.0 0.0 0.0 ]

PRODUCT-DELETE-OFF


(PROVE-LEMMA PRIME-FACTORIZATION-UNIQUENESS NIL
             (IMPLIES (AND (PRIME-LIST L1)
                           (PRIME-LIST L2)
                           (EQUAL (TIMES-LIST L1)
                                  (TIMES-LIST L2)))
                      (PERM L1 L2))
             ((USE (PRIME-FACTORIZATION-UNIQUENESS-AUX2 (L L2)))
              (INDUCT (PERM L1 L2))
              (DISABLE QUOTIENT-DIVIDES PRIME PRIME1)))

This formula simplifies, rewriting with the lemma DELETE-NON-MEMBER, and
opening up AND, NOT, IMPLIES, NLISTP, PRIME-LIST, TIMES-LIST, PERM, OR, and
MEMBER, to four new formulas:

Case 4. (IMPLIES (AND (NOT (EQUAL 1 (TIMES-LIST L2)))
                      (LISTP L1)
                      (NOT (MEMBER (CAR L1) L2))
                      (PRIME (CAR L1))
                      (PRIME-LIST (CDR L1))
                      (PRIME-LIST L2))
                 (NOT (EQUAL (TIMES (CAR L1) (TIMES-LIST (CDR L1)))
                             (TIMES-LIST L2)))),

  which again simplifies, applying the lemma PRIME-MEMBER, to:

        T.

Case 3. (IMPLIES (AND (NOT (EQUAL 1 (TIMES-LIST L2)))
                      (LISTP L1)
                      (PRIME-LIST (CDR L1))
                      (NOT (EQUAL (TIMES-LIST (CDR L1))
                                  (TIMES-LIST (DELETE (CAR L1) L2))))
                      (PRIME (CAR L1))
                      (PRIME-LIST L2)
                      (EQUAL (TIMES (CAR L1) (TIMES-LIST (CDR L1)))
                             (TIMES-LIST L2)))
                 (PERM (CDR L1) (DELETE (CAR L1) L2))),

  which again simplifies, rewriting with the lemmas PRIME-MEMBER and
  REDUCT-PRODUCT, and expanding TIMES-LIST and PRIME-LIST, to:

        T.

Case 2. (IMPLIES (AND (NOT (EQUAL 1 (TIMES-LIST L2)))
                      (LISTP L1)
                      (PRIME-LIST (CDR L1))
                      (NOT (PRIME-LIST (DELETE (CAR L1) L2)))
                      (PRIME (CAR L1))
                      (PRIME-LIST L2)
                      (EQUAL (TIMES (CAR L1) (TIMES-LIST (CDR L1)))
                             (TIMES-LIST L2)))
                 (PERM (CDR L1) (DELETE (CAR L1) L2))),

  which again simplifies, applying PRIME-LIST-DELETE, to:

        T.

Case 1. (IMPLIES (AND (NOT (LISTP L2))
                      (LISTP L1)
                      (PRIME (CAR L1))
                      (PRIME-LIST (CDR L1)))
                 (NOT (EQUAL (TIMES (CAR L1) (TIMES-LIST (CDR L1)))
                             1))).

  This again simplifies, applying TIMES-EQUAL-1, to the new conjecture:

        (IMPLIES (AND (NOT (LISTP L2))
                      (LISTP L1)
                      (PRIME (CAR L1))
                      (PRIME-LIST (CDR L1))
                      (NOT (EQUAL (CAR L1) 0))
                      (NOT (EQUAL (TIMES-LIST (CDR L1)) 0))
                      (NUMBERP (CAR L1))
                      (EQUAL (SUB1 (CAR L1)) 0))
                 (NOT (EQUAL (SUB1 (TIMES-LIST (CDR L1)))
                             0))).

  Applying the lemmas CAR-CDR-ELIM and SUB1-ELIM, replace L1 by (CONS X Z) to
  eliminate (CAR L1) and (CDR L1) and X by (ADD1 V) to eliminate (SUB1 X).  We
  rely upon the type restriction lemma noted when SUB1 was introduced to
  restrict the new variables.  We would thus like to prove:

        (IMPLIES (AND (NUMBERP V)
                      (NOT (LISTP L2))
                      (PRIME (ADD1 V))
                      (PRIME-LIST Z)
                      (NOT (EQUAL (ADD1 V) 0))
                      (NOT (EQUAL (TIMES-LIST Z) 0))
                      (EQUAL V 0))
                 (NOT (EQUAL (SUB1 (TIMES-LIST Z)) 0))),

  which further simplifies, opening up the definitions of NUMBERP and PRIME,
  to:

        T.

Q.E.D.


[ 0.0 0.1 0.0 ]

PRIME-FACTORIZATION-UNIQUENESS