(NOTE-LIB "proveall" T)
Loading ./basic/proveall.lib
Finished loading ./basic/proveall.lib
Loading ./basic/proveall.o
Finished loading ./basic/proveall.o

(#./basic/proveall.lib #./basic/proveall)


(COMPILE-UNCOMPILED-DEFNS "tmp")
Loading ./basic/tmp.o
Finished loading ./basic/tmp.o

/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/tmp.lisp


(DISABLE EUCLID)

[ 0.0 0.0 0.0 ]

EUCLID-OFF


(DISABLE QUOTIENT-DIVIDES)

[ 0.0 0.0 0.0 ]

QUOTIENT-DIVIDES-OFF


(DISABLE IF-TIMES-THEN-DIVIDES)

[ 0.0 0.0 0.0 ]

IF-TIMES-THEN-DIVIDES-OFF


(DISABLE TIMES)

[ 0.0 0.0 0.0 ]

TIMES-OFF


(DEFN CRYPT
      (M E N)
      (IF (ZEROP E)
          1
          (IF (EVEN E)
              (REMAINDER (SQUARE (CRYPT M (QUOTIENT E 2) N))
                         N)
              (REMAINDER (TIMES M
                                (REMAINDER (SQUARE (CRYPT M (QUOTIENT E 2) N))
                                           N))
                         N))))

     The lemmas LESSP-QUOTIENT1 and COUNT-NUMBERP and the definitions of
NUMBERP, EQUAL, EVEN, and ZEROP inform us that the measure (COUNT E) decreases
according to the well-founded relation LESSP in each recursive call.  Hence,
CRYPT is accepted under the principle of definition.  From the definition we
can conclude that (NUMBERP (CRYPT M E N)) is a theorem.




[ 0.0 0.0 0.0 ]

CRYPT


(PROVE-LEMMA TIMES-MOD-1
             (REWRITE)
             (EQUAL (REMAINDER (TIMES X (REMAINDER Y N))
                               N)
                    (REMAINDER (TIMES X Y) N)))

.

Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace Y by
(PLUS Z (TIMES N V)) to eliminate (REMAINDER Y N) and (QUOTIENT Y N).  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.  The result is four new goals:

Case 4. (IMPLIES (NOT (NUMBERP Y))
                 (EQUAL (REMAINDER (TIMES X (REMAINDER Y N))
                                   N)
                        (REMAINDER (TIMES X Y) N))),

  which simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES,
  TIMES-IDENTITY, TIMES-ZERO2, and REMAINDER-0-CROCK, and unfolding LESSP,
  REMAINDER, and EQUAL, to:

        T.

Case 3. (IMPLIES (EQUAL N 0)
                 (EQUAL (REMAINDER (TIMES X (REMAINDER Y N))
                                   N)
                        (REMAINDER (TIMES X Y) N))),

  which simplifies, opening up EQUAL and REMAINDER, to:

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

  But this again simplifies, applying the lemmas COMMUTATIVITY-OF-TIMES,
  TIMES-ZERO2, and TIMES-IDENTITY, and opening up the definition of EQUAL, to:

        T.

Case 2. (IMPLIES (NOT (NUMBERP N))
                 (EQUAL (REMAINDER (TIMES X (REMAINDER Y N))
                                   N)
                        (REMAINDER (TIMES X Y) N))),

  which simplifies, rewriting with REMAINDER-WRT-12, to the new conjecture:

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

  which again simplifies, rewriting with COMMUTATIVITY-OF-TIMES, TIMES-ZERO2,
  and TIMES-IDENTITY, and opening up the function EQUAL, to:

        T.

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

  But this simplifies, applying COMMUTATIVITY-OF-TIMES,
  COMMUTATIVITY2-OF-TIMES, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and
  REMAINDER-PLUS-TIMES-2, and opening up the functions ZEROP and NOT, to:

        T.

Q.E.D.


[ 0.0 0.1 0.0 ]

TIMES-MOD-1


(PROVE-LEMMA TIMES-MOD-2
             (REWRITE)
             (EQUAL (REMAINDER (TIMES A (TIMES B (REMAINDER Y N)))
                               N)
                    (REMAINDER (TIMES A B Y) N))
             ((USE (TIMES-MOD-1 (X (TIMES A B))))
              (DISABLE TIMES-MOD-1)))

This conjecture can be simplified, using the abbreviation
ASSOCIATIVITY-OF-TIMES, to:

      T.

This simplifies, clearly, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

TIMES-MOD-2


(PROVE-LEMMA CRYPT-CORRECT
             (REWRITE)
             (IMPLIES (NOT (EQUAL N 1))
                      (EQUAL (CRYPT M E N)
                             (REMAINDER (EXP M E) N))))


     Give the conjecture the name *1.


     Perhaps we can prove it by induction.  The recursive terms in the
conjecture suggest two inductions, 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 E) (p M E N))
           (IMPLIES (AND (NOT (ZEROP E))
                         (EVEN E)
                         (p M (QUOTIENT E 2) N))
                    (p M E N))
           (IMPLIES (AND (NOT (ZEROP E))
                         (NOT (EVEN E))
                         (p M (QUOTIENT E 2) N))
                    (p M E N))).
The lemmas LESSP-QUOTIENT1 and COUNT-NUMBERP and the definitions of NUMBERP,
EQUAL, EVEN, and ZEROP establish that the measure (COUNT E) 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
conjectures:

Case 3. (IMPLIES (AND (ZEROP E) (NOT (EQUAL N 1)))
                 (EQUAL (CRYPT M E N)
                        (REMAINDER (EXP M E) N))).

  This simplifies, appealing to the lemmas EXP-BY-0 and REMAINDER-OF-1, and
  unfolding ZEROP, EQUAL, CRYPT, and EXP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP E))
                      (EVEN E)
                      (EQUAL (CRYPT M (QUOTIENT E 2) N)
                             (REMAINDER (EXP M (QUOTIENT E 2)) N))
                      (NOT (EQUAL N 1)))
                 (EQUAL (CRYPT M E N)
                        (REMAINDER (EXP M E) N))).

  This simplifies, expanding the definitions of ZEROP, EVEN, CRYPT, EQUAL, and
  SQUARE, to:

        (IMPLIES (AND (NOT (EQUAL E 0))
                      (NUMBERP E)
                      (EQUAL 0 (REMAINDER E 2))
                      (EQUAL (CRYPT M (QUOTIENT E 2) N)
                             (REMAINDER (EXP M (QUOTIENT E 2)) N))
                      (NOT (EQUAL N 1)))
                 (EQUAL (REMAINDER (TIMES (CRYPT M (QUOTIENT E 2) N)
                                          (CRYPT M (QUOTIENT E 2) N))
                                   N)
                        (REMAINDER (EXP M E) N))).

  Applying the lemma REMAINDER-QUOTIENT-ELIM, replace E by
  (PLUS X (TIMES 2 Z)) to eliminate (REMAINDER E 2) and (QUOTIENT E 2).  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 formulas:

  Case 2.3.
          (IMPLIES (AND (EQUAL 2 0)
                        (NOT (EQUAL E 0))
                        (NUMBERP E)
                        (EQUAL 0 (REMAINDER E 2))
                        (EQUAL (CRYPT M (QUOTIENT E 2) N)
                               (REMAINDER (EXP M (QUOTIENT E 2)) N))
                        (NOT (EQUAL N 1)))
                   (EQUAL (REMAINDER (TIMES (CRYPT M (QUOTIENT E 2) N)
                                            (CRYPT M (QUOTIENT E 2) N))
                                     N)
                          (REMAINDER (EXP M E) N))).

    This further simplifies, using linear arithmetic, to:

          T.

  Case 2.2.
          (IMPLIES (AND (NOT (NUMBERP 2))
                        (NOT (EQUAL E 0))
                        (NUMBERP E)
                        (EQUAL 0 (REMAINDER E 2))
                        (EQUAL (CRYPT M (QUOTIENT E 2) N)
                               (REMAINDER (EXP M (QUOTIENT E 2)) N))
                        (NOT (EQUAL N 1)))
                   (EQUAL (REMAINDER (TIMES (CRYPT M (QUOTIENT E 2) N)
                                            (CRYPT M (QUOTIENT E 2) N))
                                     N)
                          (REMAINDER (EXP M E) N))),

    which further simplifies, trivially, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NUMBERP X)
                        (EQUAL (LESSP X 2) (NOT (ZEROP 2)))
                        (NUMBERP Z)
                        (NOT (EQUAL 2 0))
                        (NOT (EQUAL (PLUS X (TIMES 2 Z)) 0))
                        (EQUAL 0 X)
                        (EQUAL (CRYPT M Z N)
                               (REMAINDER (EXP M Z) N))
                        (NOT (EQUAL N 1)))
                   (EQUAL (REMAINDER (TIMES (CRYPT M Z N) (CRYPT M Z N))
                                     N)
                          (REMAINDER (EXP M (PLUS X (TIMES 2 Z)))
                                     N))).

    This further simplifies, rewriting with TIMES-2, CORRECTNESS-OF-CANCEL,
    PLUS-EQUAL-0, EXP-BY-0, EXP-PLUS, and TIMES-1, and expanding the functions
    NUMBERP, LESSP, ZEROP, NOT, and EQUAL, to the new conjecture:

          (IMPLIES (AND (NUMBERP Z)
                        (NOT (EQUAL Z 0))
                        (EQUAL (CRYPT M Z N)
                               (REMAINDER (EXP M Z) N))
                        (NOT (EQUAL N 1)))
                   (EQUAL (REMAINDER (TIMES (CRYPT M Z N) (CRYPT M Z N))
                                     N)
                          (REMAINDER (TIMES (EXP M Z) (EXP M Z))
                                     N))).

    We use the above equality hypothesis by substituting
    (REMAINDER (EXP M Z) N) for (CRYPT M Z N) and throwing away the equality.
    We must thus prove:

          (IMPLIES (AND (NUMBERP Z)
                        (NOT (EQUAL Z 0))
                        (NOT (EQUAL N 1)))
                   (EQUAL (REMAINDER (TIMES (REMAINDER (EXP M Z) N)
                                            (REMAINDER (EXP M Z) N))
                                     N)
                          (REMAINDER (TIMES (EXP M Z) (EXP M Z))
                                     N))).

    This further simplifies, rewriting with COMMUTATIVITY-OF-TIMES and
    TIMES-MOD-1, to:

          T.

Case 1. (IMPLIES (AND (NOT (ZEROP E))
                      (NOT (EVEN E))
                      (EQUAL (CRYPT M (QUOTIENT E 2) N)
                             (REMAINDER (EXP M (QUOTIENT E 2)) N))
                      (NOT (EQUAL N 1)))
                 (EQUAL (CRYPT M E N)
                        (REMAINDER (EXP M E) N))).

  This simplifies, applying TIMES-MOD-1, and unfolding ZEROP, EVEN, CRYPT, and
  SQUARE, to:

        (IMPLIES (AND (NOT (EQUAL E 0))
                      (NUMBERP E)
                      (NOT (EQUAL 0 (REMAINDER E 2)))
                      (EQUAL (CRYPT M (QUOTIENT E 2) N)
                             (REMAINDER (EXP M (QUOTIENT E 2)) N))
                      (NOT (EQUAL N 1)))
                 (EQUAL (REMAINDER (TIMES M
                                          (CRYPT M (QUOTIENT E 2) N)
                                          (CRYPT M (QUOTIENT E 2) N))
                                   N)
                        (REMAINDER (EXP M E) N))).

  This again simplifies, using linear arithmetic, rewriting with
  LESSP-REMAINDER-DIVISOR, and expanding the definition of EQUAL, to the new
  goal:

        (IMPLIES (AND (EQUAL (REMAINDER E 2) 1)
                      (NOT (EQUAL E 0))
                      (NUMBERP E)
                      (NOT (EQUAL 0 1))
                      (EQUAL (CRYPT M (QUOTIENT E 2) N)
                             (REMAINDER (EXP M (QUOTIENT E 2)) N))
                      (NOT (EQUAL N 1)))
                 (EQUAL (REMAINDER (TIMES M
                                          (CRYPT M (QUOTIENT E 2) N)
                                          (CRYPT M (QUOTIENT E 2) N))
                                   N)
                        (REMAINDER (EXP M E) N))),

  which again simplifies, unfolding EQUAL, to the formula:

        (IMPLIES (AND (EQUAL (REMAINDER E 2) 1)
                      (NOT (EQUAL E 0))
                      (NUMBERP E)
                      (EQUAL (CRYPT M (QUOTIENT E 2) N)
                             (REMAINDER (EXP M (QUOTIENT E 2)) N))
                      (NOT (EQUAL N 1)))
                 (EQUAL (REMAINDER (TIMES M
                                          (CRYPT M (QUOTIENT E 2) N)
                                          (CRYPT M (QUOTIENT E 2) N))
                                   N)
                        (REMAINDER (EXP M E) N))).

  Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace E by
  (PLUS X (TIMES 2 Z)) to eliminate (REMAINDER E 2) and (QUOTIENT E 2).  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.  The result is three new
  conjectures:

  Case 1.3.
          (IMPLIES (AND (EQUAL 2 0)
                        (EQUAL (REMAINDER E 2) 1)
                        (NOT (EQUAL E 0))
                        (NUMBERP E)
                        (EQUAL (CRYPT M (QUOTIENT E 2) N)
                               (REMAINDER (EXP M (QUOTIENT E 2)) N))
                        (NOT (EQUAL N 1)))
                   (EQUAL (REMAINDER (TIMES M
                                            (CRYPT M (QUOTIENT E 2) N)
                                            (CRYPT M (QUOTIENT E 2) N))
                                     N)
                          (REMAINDER (EXP M E) N))),

    which further simplifies, using linear arithmetic, to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (NUMBERP 2))
                        (EQUAL (REMAINDER E 2) 1)
                        (NOT (EQUAL E 0))
                        (NUMBERP E)
                        (EQUAL (CRYPT M (QUOTIENT E 2) N)
                               (REMAINDER (EXP M (QUOTIENT E 2)) N))
                        (NOT (EQUAL N 1)))
                   (EQUAL (REMAINDER (TIMES M
                                            (CRYPT M (QUOTIENT E 2) N)
                                            (CRYPT M (QUOTIENT E 2) N))
                                     N)
                          (REMAINDER (EXP M E) N))),

    which further simplifies, trivially, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NUMBERP X)
                        (EQUAL (LESSP X 2) (NOT (ZEROP 2)))
                        (NUMBERP Z)
                        (NOT (EQUAL 2 0))
                        (EQUAL X 1)
                        (NOT (EQUAL (PLUS X (TIMES 2 Z)) 0))
                        (EQUAL (CRYPT M Z N)
                               (REMAINDER (EXP M Z) N))
                        (NOT (EQUAL N 1)))
                   (EQUAL (REMAINDER (TIMES M (CRYPT M Z N) (CRYPT M Z N))
                                     N)
                          (REMAINDER (EXP M (PLUS X (TIMES 2 Z)))
                                     N))).

    This further simplifies, applying TIMES-2, PLUS-EQUAL-0,
    COMMUTATIVITY-OF-TIMES, TIMES-1, EXP-BY-0, EXP-PLUS, and
    COMMUTATIVITY2-OF-TIMES, and unfolding the functions NUMBERP, LESSP, ZEROP,
    NOT, EQUAL, SUB1, and EXP, to the following two new formulas:

    Case 1.1.2.
            (IMPLIES (AND (NUMBERP Z)
                          (EQUAL (CRYPT M Z N)
                                 (REMAINDER (EXP M Z) N))
                          (NOT (EQUAL N 1))
                          (NOT (NUMBERP M)))
                     (EQUAL (REMAINDER (TIMES M (CRYPT M Z N) (CRYPT M Z N))
                                       N)
                            (REMAINDER (TIMES (EXP M Z) (EXP M Z) 0)
                                       N))).

      This again simplifies, rewriting with the lemmas EQUAL-TIMES-0,
      COMMUTATIVITY-OF-TIMES, COMMUTATIVITY2-OF-TIMES, and TIMES-IDENTITY, and
      expanding the functions LESSP, REMAINDER, and EQUAL, to the goal:

            (IMPLIES (AND (NUMBERP Z)
                          (EQUAL (CRYPT M Z N)
                                 (REMAINDER (EXP M Z) N))
                          (NOT (EQUAL N 1))
                          (NOT (NUMBERP M)))
                     (EQUAL (TIMES M (CRYPT M Z N) (CRYPT M Z N))
                            (TIMES 0 (EXP M Z) (EXP M Z)))).

      We use the above equality hypothesis by substituting
      (REMAINDER (EXP M Z) N) for (CRYPT M Z N) and throwing away the equality.
      We thus obtain:

            (IMPLIES (AND (NUMBERP Z)
                          (NOT (EQUAL N 1))
                          (NOT (NUMBERP M)))
                     (EQUAL (TIMES M
                                   (REMAINDER (EXP M Z) N)
                                   (REMAINDER (EXP M Z) N))
                            (TIMES 0 (EXP M Z) (EXP M Z)))),

      which we generalize by replacing (EXP M Z) by Y.  We restrict the new
      variable by recalling the type restriction lemma noted when EXP was
      introduced.  This produces the new conjecture:

            (IMPLIES (AND (NUMBERP Y)
                          (NUMBERP Z)
                          (NOT (EQUAL N 1))
                          (NOT (NUMBERP M)))
                     (EQUAL (TIMES M
                                   (REMAINDER Y N)
                                   (REMAINDER Y N))
                            (TIMES 0 Y Y))).

      Applying the lemma REMAINDER-QUOTIENT-ELIM, replace Y by
      (PLUS X (TIMES N V)) to eliminate (REMAINDER Y N) and (QUOTIENT Y N).
      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 thus obtain
      the following three new goals:

      Case 1.1.2.3.
              (IMPLIES (AND (EQUAL N 0)
                            (NUMBERP Y)
                            (NUMBERP Z)
                            (NOT (EQUAL N 1))
                            (NOT (NUMBERP M)))
                       (EQUAL (TIMES M
                                     (REMAINDER Y N)
                                     (REMAINDER Y N))
                              (TIMES 0 Y Y))).

        This further simplifies, opening up the definitions of EQUAL and
        REMAINDER, to the conjecture:

              (IMPLIES (AND (NUMBERP Y)
                            (NUMBERP Z)
                            (NOT (NUMBERP M)))
                       (EQUAL (TIMES M Y Y) (TIMES 0 Y Y))).

        We will try to prove the above formula by generalizing it, replacing
        (TIMES Y Y) 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 Y)
                            (NUMBERP Z)
                            (NOT (NUMBERP M)))
                       (EQUAL (TIMES M A) (TIMES 0 A))),

        which finally simplifies, applying TIMES-ZERO2, COMMUTATIVITY-OF-TIMES,
        and TIMES-IDENTITY, and expanding EQUAL, to:

              T.

      Case 1.1.2.2.
              (IMPLIES (AND (NOT (NUMBERP N))
                            (NUMBERP Y)
                            (NUMBERP Z)
                            (NOT (EQUAL N 1))
                            (NOT (NUMBERP M)))
                       (EQUAL (TIMES M
                                     (REMAINDER Y N)
                                     (REMAINDER Y N))
                              (TIMES 0 Y Y))).

        However this further simplifies, applying REMAINDER-WRT-12, to:

              (IMPLIES (AND (NOT (NUMBERP N))
                            (NUMBERP Y)
                            (NUMBERP Z)
                            (NOT (NUMBERP M)))
                       (EQUAL (TIMES M Y Y) (TIMES 0 Y Y))),

        which we generalize by replacing (TIMES Y Y) by A.  We restrict the
        new variable by recalling the type restriction lemma noted when TIMES
        was introduced.  This produces:

              (IMPLIES (AND (NUMBERP A)
                            (NOT (NUMBERP N))
                            (NUMBERP Y)
                            (NUMBERP Z)
                            (NOT (NUMBERP M)))
                       (EQUAL (TIMES M A) (TIMES 0 A))),

        which finally simplifies, applying the lemmas TIMES-ZERO2,
        COMMUTATIVITY-OF-TIMES, and TIMES-IDENTITY, and unfolding the function
        EQUAL, to:

              T.

      Case 1.1.2.1.
              (IMPLIES (AND (NUMBERP X)
                            (EQUAL (LESSP X N) (NOT (ZEROP N)))
                            (NUMBERP V)
                            (NUMBERP N)
                            (NOT (EQUAL N 0))
                            (NUMBERP Z)
                            (NOT (EQUAL N 1))
                            (NOT (NUMBERP M)))
                       (EQUAL (TIMES M X X)
                              (TIMES 0
                                     (PLUS X (TIMES N V))
                                     (PLUS X (TIMES N V))))),

        which further simplifies, rewriting with COMMUTATIVITY-OF-TIMES,
        COMMUTATIVITY2-OF-TIMES, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS,
        ASSOCIATIVITY-OF-PLUS, and TIMES-IDENTITY, and expanding the functions
        ZEROP, NOT, EQUAL, and PLUS, to the new conjecture:

              (IMPLIES (AND (NUMBERP X)
                            (LESSP X N)
                            (NUMBERP V)
                            (NUMBERP N)
                            (NOT (EQUAL N 0))
                            (NUMBERP Z)
                            (NOT (EQUAL N 1))
                            (NOT (NUMBERP M)))
                       (EQUAL (TIMES M X X)
                              (TIMES 0 N N V V))),

        which has an irrelevant term in it.  By eliminating the term we get:

              (IMPLIES (AND (NUMBERP X)
                            (LESSP X N)
                            (NUMBERP V)
                            (NUMBERP N)
                            (NOT (EQUAL N 0))
                            (NOT (EQUAL N 1))
                            (NOT (NUMBERP M)))
                       (EQUAL (TIMES M X X)
                              (TIMES 0 N N V V))),

        which we will finally name *1.1.

    Case 1.1.1.
            (IMPLIES (AND (NUMBERP Z)
                          (EQUAL (CRYPT M Z N)
                                 (REMAINDER (EXP M Z) N))
                          (NOT (EQUAL N 1))
                          (NUMBERP M))
                     (EQUAL (REMAINDER (TIMES M (CRYPT M Z N) (CRYPT M Z N))
                                       N)
                            (REMAINDER (TIMES (EXP M Z) (EXP M Z) M)
                                       N))).

      However this again simplifies, applying COMMUTATIVITY-OF-TIMES and
      COMMUTATIVITY2-OF-TIMES, to:

            (IMPLIES (AND (NUMBERP Z)
                          (EQUAL (CRYPT M Z N)
                                 (REMAINDER (EXP M Z) N))
                          (NOT (EQUAL N 1))
                          (NUMBERP M))
                     (EQUAL (REMAINDER (TIMES M (CRYPT M Z N) (CRYPT M Z N))
                                       N)
                            (REMAINDER (TIMES M (EXP M Z) (EXP M Z))
                                       N))).

      We use the above equality hypothesis by substituting
      (REMAINDER (EXP M Z) N) for (CRYPT M Z N) and throwing away the equality.
      The result is the goal:

            (IMPLIES (AND (NUMBERP Z)
                          (NOT (EQUAL N 1))
                          (NUMBERP M))
                     (EQUAL (REMAINDER (TIMES M
                                              (REMAINDER (EXP M Z) N)
                                              (REMAINDER (EXP M Z) N))
                                       N)
                            (REMAINDER (TIMES M (EXP M Z) (EXP M Z))
                                       N))).

      But this finally simplifies, applying COMMUTATIVITY-OF-TIMES and
      TIMES-MOD-2, to:

            T.


     So we now return to:

      (IMPLIES (AND (NUMBERP X)
                    (LESSP X N)
                    (NUMBERP V)
                    (NUMBERP N)
                    (NOT (EQUAL N 0))
                    (NOT (EQUAL N 1))
                    (NOT (NUMBERP M)))
               (EQUAL (TIMES M X X)
                      (TIMES 0 N N V V))),

which is formula *1.1 above.  We will appeal to 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 (OR (EQUAL N 0) (NOT (NUMBERP N)))
                    (p M X N V))
           (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
                         (OR (EQUAL X 0) (NOT (NUMBERP X))))
                    (p M X N V))
           (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
                         (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                         (p M (SUB1 X) (SUB1 N) V))
                    (p M X N V))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT inform us 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 N.  The above induction scheme
generates the following six new conjectures:

Case 6. (IMPLIES (AND (OR (EQUAL N 0) (NOT (NUMBERP N)))
                      (NUMBERP X)
                      (LESSP X N)
                      (NUMBERP V)
                      (NUMBERP N)
                      (NOT (EQUAL N 0))
                      (NOT (EQUAL N 1))
                      (NOT (NUMBERP M)))
                 (EQUAL (TIMES M X X)
                        (TIMES 0 N N V V))).

  This simplifies, unfolding the functions NOT and OR, to:

        T.

Case 5. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
                      (OR (EQUAL X 0) (NOT (NUMBERP X)))
                      (NUMBERP X)
                      (LESSP X N)
                      (NUMBERP V)
                      (NUMBERP N)
                      (NOT (EQUAL N 0))
                      (NOT (EQUAL N 1))
                      (NOT (NUMBERP M)))
                 (EQUAL (TIMES M X X)
                        (TIMES 0 N N V V))).

  This simplifies, rewriting with the lemmas TIMES-ZERO2,
  COMMUTATIVITY-OF-TIMES, and TIMES-IDENTITY, and expanding the definitions of
  NOT, OR, NUMBERP, EQUAL, LESSP, and TIMES, to:

        T.

Case 4. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
                      (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                      (NOT (LESSP (SUB1 X) (SUB1 N)))
                      (NUMBERP X)
                      (LESSP X N)
                      (NUMBERP V)
                      (NUMBERP N)
                      (NOT (EQUAL N 0))
                      (NOT (EQUAL N 1))
                      (NOT (NUMBERP M)))
                 (EQUAL (TIMES M X X)
                        (TIMES 0 N N V V))).

  This simplifies, using linear arithmetic, to:

        (IMPLIES (AND (EQUAL X 0)
                      (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
                      (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                      (NOT (LESSP (SUB1 X) (SUB1 N)))
                      (NUMBERP X)
                      (LESSP X N)
                      (NUMBERP V)
                      (NUMBERP N)
                      (NOT (EQUAL N 0))
                      (NOT (EQUAL N 1))
                      (NOT (NUMBERP M)))
                 (EQUAL (TIMES M X X)
                        (TIMES 0 N N V V))),

  which again simplifies, unfolding the definitions of NOT, OR, EQUAL, and
  NUMBERP, to:

        T.

Case 3. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
                      (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                      (EQUAL (SUB1 N) 0)
                      (NUMBERP X)
                      (LESSP X N)
                      (NUMBERP V)
                      (NUMBERP N)
                      (NOT (EQUAL N 0))
                      (NOT (EQUAL N 1))
                      (NOT (NUMBERP M)))
                 (EQUAL (TIMES M X X)
                        (TIMES 0 N N V V))),

  which simplifies, using linear arithmetic, to:

        T.

Case 2. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
                      (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                      (EQUAL (SUB1 N) 1)
                      (NUMBERP X)
                      (LESSP X N)
                      (NUMBERP V)
                      (NUMBERP N)
                      (NOT (EQUAL N 0))
                      (NOT (EQUAL N 1))
                      (NOT (NUMBERP M)))
                 (EQUAL (TIMES M X X)
                        (TIMES 0 N N V V))),

  which simplifies, expanding the definitions of NOT, OR, and LESSP, to the
  conjecture:

        (IMPLIES (AND (NOT (EQUAL X 0))
                      (EQUAL (SUB1 N) 1)
                      (NUMBERP X)
                      (LESSP (SUB1 X) (SUB1 N))
                      (NUMBERP V)
                      (NUMBERP N)
                      (NOT (EQUAL N 0))
                      (NOT (EQUAL N 1))
                      (NOT (NUMBERP M)))
                 (EQUAL (TIMES M X X)
                        (TIMES 0 N N V V))).

  However this again simplifies, using linear arithmetic, to the goal:

        (IMPLIES (AND (NOT (EQUAL 1 0))
                      (EQUAL (SUB1 N) 1)
                      (NUMBERP 1)
                      (LESSP (SUB1 1) 1)
                      (NUMBERP V)
                      (NUMBERP N)
                      (NOT (EQUAL N 0))
                      (NOT (EQUAL N 1))
                      (NOT (NUMBERP M)))
                 (EQUAL (TIMES M 1 1)
                        (TIMES 0 N N V V))).

  This again simplifies, applying the lemmas TIMES-1, COMMUTATIVITY-OF-TIMES,
  and TIMES-IDENTITY, and opening up EQUAL, NUMBERP, SUB1, LESSP, and TIMES,
  to:

        T.

Case 1. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
                      (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
                      (EQUAL (TIMES M (SUB1 X) (SUB1 X))
                             (TIMES 0 (SUB1 N) (SUB1 N) V V))
                      (NUMBERP X)
                      (LESSP X N)
                      (NUMBERP V)
                      (NUMBERP N)
                      (NOT (EQUAL N 0))
                      (NOT (EQUAL N 1))
                      (NOT (NUMBERP M)))
                 (EQUAL (TIMES M X X)
                        (TIMES 0 N N V V))),

  which simplifies, applying COMMUTATIVITY-OF-TIMES and
  COMMUTATIVITY2-OF-TIMES, and unfolding the definitions of NOT, OR, and LESSP,
  to the new conjecture:

        (IMPLIES (AND (NOT (EQUAL X 0))
                      (EQUAL (TIMES M (SUB1 X) (SUB1 X))
                             (TIMES 0 V V (SUB1 N) (SUB1 N)))
                      (NUMBERP X)
                      (LESSP (SUB1 X) (SUB1 N))
                      (NUMBERP V)
                      (NUMBERP N)
                      (NOT (EQUAL N 0))
                      (NOT (EQUAL N 1))
                      (NOT (NUMBERP M)))
                 (EQUAL (TIMES M X X)
                        (TIMES 0 N N V V))).

  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.  We thus obtain the new formula:

        (IMPLIES (AND (NUMBERP Z)
                      (NOT (EQUAL (ADD1 Z) 0))
                      (EQUAL (TIMES M Z Z)
                             (TIMES 0 V V (SUB1 N) (SUB1 N)))
                      (LESSP Z (SUB1 N))
                      (NUMBERP V)
                      (NUMBERP N)
                      (NOT (EQUAL N 0))
                      (NOT (EQUAL N 1))
                      (NOT (NUMBERP M)))
                 (EQUAL (TIMES M (ADD1 Z) (ADD1 Z))
                        (TIMES 0 N N V V))),

  which further simplifies, rewriting with TIMES-ADD1, COMMUTATIVITY-OF-TIMES,
  SUB1-ADD1, PLUS-ADD1, COMMUTATIVITY2-OF-PLUS, EQUAL-TIMES-0, and
  DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and unfolding the definition of PLUS, to
  the new formula:

        (IMPLIES (AND (NUMBERP Z)
                      (EQUAL (TIMES M Z Z)
                             (TIMES 0 V V (SUB1 N) (SUB1 N)))
                      (LESSP Z (SUB1 N))
                      (NUMBERP V)
                      (NUMBERP N)
                      (NOT (EQUAL N 0))
                      (NOT (EQUAL N 1))
                      (NOT (NUMBERP M)))
                 (EQUAL (TIMES M Z Z)
                        (TIMES 0 N N V V))),

  which again simplifies, using linear arithmetic, to:

        T.


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


[ 0.0 1.3 0.1 ]

CRYPT-CORRECT


(PROVE-LEMMA TIMES-MOD-3
             (REWRITE)
             (EQUAL (REMAINDER (TIMES (REMAINDER A N) B)
                               N)
                    (REMAINDER (TIMES A B) N)))

This simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES and
TIMES-MOD-1, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

TIMES-MOD-3


(PROVE-LEMMA REMAINDER-EXP-LEMMA
             (REWRITE)
             (IMPLIES (EQUAL (REMAINDER Y A)
                             (REMAINDER Z A))
                      (EQUAL (EQUAL (REMAINDER (TIMES X Y) A)
                                    (REMAINDER (TIMES X Z) A))
                             T)))

.

Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace Y by
(PLUS V (TIMES A W)) to eliminate (REMAINDER Y A) and (QUOTIENT Y A).  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 Y))
                      (EQUAL (REMAINDER Y A)
                             (REMAINDER Z A)))
                 (EQUAL (REMAINDER (TIMES X Y) A)
                        (REMAINDER (TIMES X Z) A))),

  which further simplifies, rewriting with TIMES-ZERO2 and REMAINDER-0-CROCK,
  and opening up the definitions of LESSP and REMAINDER, to the new goal:

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

  Applying the lemma REMAINDER-QUOTIENT-ELIM, replace Z by
  (PLUS V (TIMES A W)) to eliminate (REMAINDER Z A) and (QUOTIENT Z 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 restrict the new variables.  We would thus like to prove the
  following four new goals:

  Case 4.4.
          (IMPLIES (AND (NOT (NUMBERP Z))
                        (NOT (NUMBERP Y))
                        (EQUAL 0 (REMAINDER Z A)))
                   (EQUAL 0 (REMAINDER (TIMES X Z) A))).

    But this further simplifies, applying TIMES-ZERO2 and REMAINDER-0-CROCK,
    and opening up LESSP, REMAINDER, and EQUAL, to:

          T.

  Case 4.3.
          (IMPLIES (AND (EQUAL A 0)
                        (NOT (NUMBERP Y))
                        (EQUAL 0 (REMAINDER Z A)))
                   (EQUAL 0 (REMAINDER (TIMES X Z) A))).

    But this further simplifies, rewriting with the lemmas
    COMMUTATIVITY-OF-TIMES, REMAINDER-TIMES, and TIMES-ZERO2, and unfolding
    the definitions of EQUAL and REMAINDER, to:

          T.

  Case 4.2.
          (IMPLIES (AND (NOT (NUMBERP A))
                        (NOT (NUMBERP Y))
                        (EQUAL 0 (REMAINDER Z A)))
                   (EQUAL 0 (REMAINDER (TIMES X Z) A))),

    which further simplifies, rewriting with REMAINDER-WRT-12,
    COMMUTATIVITY-OF-TIMES, TIMES-IDENTITY, TIMES-ZERO2, and REMAINDER-0-CROCK,
    and unfolding the function EQUAL, to:

          T.

  Case 4.1.
          (IMPLIES (AND (NUMBERP V)
                        (EQUAL (LESSP V A) (NOT (ZEROP A)))
                        (NUMBERP W)
                        (NUMBERP A)
                        (NOT (EQUAL A 0))
                        (NOT (NUMBERP Y))
                        (EQUAL 0 V))
                   (EQUAL 0
                          (REMAINDER (TIMES X (PLUS V (TIMES A W)))
                                     A))).

    This further simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES,
    COMMUTATIVITY2-OF-TIMES, and REMAINDER-TIMES, and opening up the functions
    NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to:

          T.

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

  which further simplifies, rewriting with TIMES-ZERO2, COMMUTATIVITY-OF-TIMES,
  and REMAINDER-TIMES, and expanding the definitions of EQUAL and REMAINDER,
  to:

        T.

Case 2. (IMPLIES (AND (NOT (NUMBERP A))
                      (EQUAL (REMAINDER Y A)
                             (REMAINDER Z A)))
                 (EQUAL (REMAINDER (TIMES X Y) A)
                        (REMAINDER (TIMES X Z) A))).

  But this further simplifies, appealing to the lemmas REMAINDER-WRT-12,
  TIMES-ZERO2, REMAINDER-0-CROCK, COMMUTATIVITY-OF-TIMES, and TIMES-IDENTITY,
  and unfolding EQUAL, to:

        T.

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

  which further simplifies, applying LESSP-REMAINDER2, COMMUTATIVITY-OF-TIMES,
  COMMUTATIVITY2-OF-TIMES, COMMUTATIVITY-OF-PLUS, and
  DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and expanding the functions ZEROP, NOT,
  and EQUAL, to:

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

  Applying the lemma REMAINDER-QUOTIENT-ELIM, replace Z by
  (PLUS V (TIMES A D)) to eliminate (REMAINDER Z A) and (QUOTIENT Z 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 restrict the new variables.  We would thus like to prove the
  following two new conjectures:

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

    This further simplifies, applying COMMUTATIVITY-OF-TIMES, TIMES-IDENTITY,
    COMMUTATIVITY-OF-PLUS, REMAINDER-TIMES, TIMES-ZERO2, and REMAINDER-0-CROCK,
    and opening up the functions LESSP, REMAINDER, EQUAL, and PLUS, to:

          T.

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

    However this further simplifies, rewriting with COMMUTATIVITY-OF-TIMES,
    COMMUTATIVITY-OF-PLUS, REMAINDER-PLUS-TIMES-2, COMMUTATIVITY2-OF-TIMES,
    and DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and opening up the functions ZEROP
    and NOT, to:

          T.

Q.E.D.


[ 0.0 0.3 0.0 ]

REMAINDER-EXP-LEMMA


(PROVE-LEMMA REMAINDER-EXP
             (REWRITE)
             (EQUAL (REMAINDER (EXP (REMAINDER A N) I) N)
                    (REMAINDER (EXP A I) N)))

.

Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace A by
(PLUS X (TIMES N Z)) to eliminate (REMAINDER A N) and (QUOTIENT A N).  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.  The result is four new goals:

Case 4. (IMPLIES (NOT (NUMBERP A))
                 (EQUAL (REMAINDER (EXP (REMAINDER A N) I) N)
                        (REMAINDER (EXP A I) N))),

  which simplifies, appealing to the lemma EXP-OF-0, and unfolding LESSP and
  REMAINDER, to three new formulas:

  Case 4.3.
          (IMPLIES (AND (NOT (NUMBERP A))
                        (NOT (EQUAL I 0))
                        (NUMBERP I))
                   (EQUAL (REMAINDER 0 N)
                          (REMAINDER (EXP A I) N))),

    which again simplifies, applying REMAINDER-0-CROCK, to the new conjecture:

          (IMPLIES (AND (NOT (NUMBERP A))
                        (NOT (EQUAL I 0))
                        (NUMBERP I))
                   (EQUAL 0 (REMAINDER (EXP A I) N))),

    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 (REMAINDER (EXP (REMAINDER A N) I) N)
       (REMAINDER (EXP A I) N)).

We named this *1.  We will try to prove it by 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 (ZEROP I) (p A N I))
           (IMPLIES (AND (NOT (ZEROP I)) (p A N (SUB1 I)))
                    (p A N I))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to prove 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 the following two new goals:

Case 2. (IMPLIES (ZEROP I)
                 (EQUAL (REMAINDER (EXP (REMAINDER A N) I) N)
                        (REMAINDER (EXP A I) N))).

  This simplifies, appealing to the lemmas EXP-BY-0 and REMAINDER-OF-1, and
  expanding the functions ZEROP and EXP, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP I))
                      (EQUAL (REMAINDER (EXP (REMAINDER A N) (SUB1 I))
                                        N)
                             (REMAINDER (EXP A (SUB1 I)) N)))
                 (EQUAL (REMAINDER (EXP (REMAINDER A N) I) N)
                        (REMAINDER (EXP A I) N))).

  This simplifies, appealing to the lemmas TIMES-MOD-3 and REMAINDER-EXP-LEMMA,
  and expanding the functions ZEROP and EXP, to:

        T.


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


[ 0.0 0.1 0.0 ]

REMAINDER-EXP


(PROVE-LEMMA EXP-MOD-IS-1
             (REWRITE)
             (IMPLIES (EQUAL (REMAINDER (EXP M J) P) 1)
                      (EQUAL (REMAINDER (EXP M (TIMES I J)) P)
                             1))
             ((USE (EXP-EXP (I M) (J J) (K I))
                   (REMAINDER-EXP (A (EXP M J)) (N P)))
              (DISABLE EXP-EXP REMAINDER-EXP)))

This formula simplifies, rewriting with the lemmas COMMUTATIVITY-OF-TIMES,
EXP-OF-1, REMAINDER-OF-1, and REMAINDER-WRT-1, and opening up EQUAL, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

EXP-MOD-IS-1


(DEFN PDIFFERENCE
      (A B)
      (IF (LESSP A B)
          (DIFFERENCE B A)
          (DIFFERENCE A B))
      NIL)

     Note that (NUMBERP (PDIFFERENCE A B)) is a theorem.




[ 0.0 0.0 0.0 ]

PDIFFERENCE


(PROVE-LEMMA TIMES-DISTRIBUTES-OVER-PDIFFERENCE
             (REWRITE)
             (EQUAL (TIMES M (PDIFFERENCE A B))
                    (PDIFFERENCE (TIMES M A)
                                 (TIMES M B))))

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


This simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES and
LESSP-TIMES-CANCELLATION, and opening up the definition of PDIFFERENCE, to
four new goals:

Case 4. (IMPLIES (NOT (LESSP A B))
                 (EQUAL (TIMES M (DIFFERENCE A B))
                        (DIFFERENCE (TIMES A M)
                                    (TIMES B M)))),

  which again simplifies, appealing to the lemma TIMES-DIFFERENCE, to:

        T.

Case 3. (IMPLIES (AND (NOT (NUMBERP M)) (LESSP A B))
                 (EQUAL (TIMES M (DIFFERENCE B A))
                        (DIFFERENCE (TIMES A M)
                                    (TIMES B M)))),

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

        T.

Case 2. (IMPLIES (AND (EQUAL M 0) (LESSP A B))
                 (EQUAL (TIMES M (DIFFERENCE B A))
                        (DIFFERENCE (TIMES A M)
                                    (TIMES B M)))).

  This again simplifies, using linear arithmetic, applying the lemmas
  COMMUTATIVITY-OF-TIMES, DIFFERENCE-0, and TIMES-DIFFERENCE, and opening up
  the definition of EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL M 0))
                      (NUMBERP M)
                      (LESSP A B))
                 (EQUAL (TIMES M (DIFFERENCE B A))
                        (DIFFERENCE (TIMES B M)
                                    (TIMES A M)))),

  which again simplifies, applying TIMES-DIFFERENCE, to:

        T.

Q.E.D.


[ 0.0 0.1 0.0 ]

TIMES-DISTRIBUTES-OVER-PDIFFERENCE


(PROVE-LEMMA EQUAL-MODS-TRICK-1
             (REWRITE)
             (IMPLIES (EQUAL (REMAINDER (PDIFFERENCE A B) P)
                             0)
                      (EQUAL (EQUAL (REMAINDER A P)
                                    (REMAINDER B P))
                             T)))

This formula simplifies, unfolding the function PDIFFERENCE, to two new goals:

Case 2. (IMPLIES (AND (NOT (LESSP A B))
                      (EQUAL (REMAINDER (DIFFERENCE A B) P)
                             0))
                 (EQUAL (REMAINDER A P)
                        (REMAINDER B P))).

  Applying the lemmas DIFFERENCE-ELIM and REMAINDER-QUOTIENT-ELIM, replace A
  by (PLUS B X) to eliminate (DIFFERENCE A B) and X by (PLUS Z (TIMES P V)) to
  eliminate (REMAINDER X P) and (QUOTIENT X P).  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 thus obtain the following four new formulas:

  Case 2.4.
          (IMPLIES (AND (NOT (NUMBERP A))
                        (NOT (LESSP A B))
                        (EQUAL (REMAINDER (DIFFERENCE A B) P)
                               0))
                   (EQUAL (REMAINDER A P)
                          (REMAINDER B P))).

    However this further simplifies, using linear arithmetic, appealing to the
    lemmas DIFFERENCE-0 and REMAINDER-0-CROCK, and unfolding the definitions
    of LESSP, EQUAL, and REMAINDER, to:

          T.

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

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

          T.

  Case 2.2.
          (IMPLIES (AND (NOT (NUMBERP P))
                        (NUMBERP X)
                        (NOT (LESSP (PLUS B X) B))
                        (EQUAL (REMAINDER X P) 0))
                   (EQUAL (REMAINDER (PLUS B X) P)
                          (REMAINDER B P))).

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

          T.

  Case 2.1.
          (IMPLIES (AND (NUMBERP Z)
                        (EQUAL (LESSP Z P) (NOT (ZEROP P)))
                        (NUMBERP V)
                        (NUMBERP P)
                        (NOT (EQUAL P 0))
                        (NOT (LESSP (PLUS B Z (TIMES P V)) B))
                        (EQUAL Z 0))
                   (EQUAL (REMAINDER (PLUS B Z (TIMES P V)) P)
                          (REMAINDER B P))).

    However this further simplifies, rewriting with the lemma
    REMAINDER-PLUS-TIMES-2, and expanding the functions NUMBERP, EQUAL, LESSP,
    ZEROP, NOT, and PLUS, to:

          T.

Case 1. (IMPLIES (AND (LESSP A B)
                      (EQUAL (REMAINDER (DIFFERENCE B A) P)
                             0))
                 (EQUAL (REMAINDER A P)
                        (REMAINDER B P))).

  Applying the lemmas DIFFERENCE-ELIM and REMAINDER-QUOTIENT-ELIM, replace B
  by (PLUS A X) to eliminate (DIFFERENCE B A) and X by (PLUS Z (TIMES P V)) to
  eliminate (REMAINDER X P) and (QUOTIENT X P).  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 restrict the new
  variables.  We would thus like to prove the following five new goals:

  Case 1.5.
          (IMPLIES (AND (LESSP B A)
                        (LESSP A B)
                        (EQUAL (REMAINDER (DIFFERENCE B A) P)
                               0))
                   (EQUAL (REMAINDER A P)
                          (REMAINDER B P))).

    However this further simplifies, using linear arithmetic, to:

          T.

  Case 1.4.
          (IMPLIES (AND (NOT (NUMBERP B))
                        (LESSP A B)
                        (EQUAL (REMAINDER (DIFFERENCE B A) P)
                               0))
                   (EQUAL (REMAINDER A P)
                          (REMAINDER B P))),

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

          T.

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

    which further simplifies, rewriting with COMMUTATIVITY-OF-PLUS, and
    expanding the definitions of EQUAL, REMAINDER, and PLUS, to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (NUMBERP P))
                        (NUMBERP X)
                        (NOT (LESSP (PLUS A X) A))
                        (LESSP A (PLUS A X))
                        (EQUAL (REMAINDER X P) 0))
                   (EQUAL (REMAINDER A P)
                          (REMAINDER (PLUS A X) P))).

    But this further simplifies, rewriting with REMAINDER-WRT-12 and
    COMMUTATIVITY-OF-PLUS, and unfolding the definitions of EQUAL and PLUS, to:

          T.

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

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

          T.

Q.E.D.


[ 0.0 0.2 0.0 ]

EQUAL-MODS-TRICK-1


(PROVE-LEMMA EQUAL-MODS-TRICK-2
             (REWRITE)
             (IMPLIES (EQUAL (REMAINDER A P)
                             (REMAINDER B P))
                      (EQUAL (REMAINDER (PDIFFERENCE A B) P)
                             0))
             ((DISABLE DIFFERENCE-ELIM)))

This formula simplifies, opening up PDIFFERENCE, to the following two new
formulas:

Case 2. (IMPLIES (AND (EQUAL (REMAINDER A P)
                             (REMAINDER B P))
                      (NOT (LESSP A B)))
                 (EQUAL (REMAINDER (DIFFERENCE A B) P)
                        0)).

  Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace A by
  (PLUS X (TIMES P Z)) to eliminate (REMAINDER A P) and (QUOTIENT A P).  We
  employ 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 formulas:

  Case 2.4.
          (IMPLIES (AND (NOT (NUMBERP A))
                        (EQUAL (REMAINDER A P)
                               (REMAINDER B P))
                        (NOT (LESSP A B)))
                   (EQUAL (REMAINDER (DIFFERENCE A B) P)
                          0)),

    which further simplifies, using linear arithmetic, applying the lemmas
    DIFFERENCE-0 and REMAINDER-0-CROCK, and expanding the definitions of LESSP,
    REMAINDER, and EQUAL, to:

          T.

  Case 2.3.
          (IMPLIES (AND (EQUAL P 0)
                        (EQUAL (REMAINDER A P)
                               (REMAINDER B P))
                        (NOT (LESSP A B)))
                   (EQUAL (REMAINDER (DIFFERENCE A B) P)
                          0)),

    which further simplifies, using linear arithmetic, applying DIFFERENCE-0,
    and expanding EQUAL, REMAINDER, and LESSP, to:

          T.

  Case 2.2.
          (IMPLIES (AND (NOT (NUMBERP P))
                        (EQUAL (REMAINDER A P)
                               (REMAINDER B P))
                        (NOT (LESSP A B)))
                   (EQUAL (REMAINDER (DIFFERENCE A B) P)
                          0)).

    However this further simplifies, using linear arithmetic, applying
    REMAINDER-WRT-12, DIFFERENCE-0, and REMAINDER-0-CROCK, and expanding the
    definitions of EQUAL and LESSP, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NUMBERP X)
                        (EQUAL (LESSP X P) (NOT (ZEROP P)))
                        (NUMBERP Z)
                        (NUMBERP P)
                        (NOT (EQUAL P 0))
                        (EQUAL X (REMAINDER B P))
                        (NOT (LESSP (PLUS X (TIMES P Z)) B)))
                   (EQUAL (REMAINDER (DIFFERENCE (PLUS X (TIMES P Z)) B)
                                     P)
                          0)).

    But this further simplifies, applying LESSP-REMAINDER2, and expanding
    ZEROP, NOT, and EQUAL, to:

          (IMPLIES
               (AND (NUMBERP Z)
                    (NUMBERP P)
                    (NOT (EQUAL P 0))
                    (NOT (LESSP (PLUS (REMAINDER B P) (TIMES P Z))
                                B)))
               (EQUAL (REMAINDER (DIFFERENCE (PLUS (REMAINDER B P) (TIMES P Z))
                                             B)
                                 P)
                      0)).

    Applying the lemma REMAINDER-QUOTIENT-ELIM, replace B by
    (PLUS X (TIMES P V)) to eliminate (REMAINDER B P) and (QUOTIENT B P).  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 two new conjectures:

    Case 2.1.2.
            (IMPLIES
               (AND (NOT (NUMBERP B))
                    (NUMBERP Z)
                    (NUMBERP P)
                    (NOT (EQUAL P 0))
                    (NOT (LESSP (PLUS (REMAINDER B P) (TIMES P Z))
                                B)))
               (EQUAL (REMAINDER (DIFFERENCE (PLUS (REMAINDER B P) (TIMES P Z))
                                             B)
                                 P)
                      0)).

      This further simplifies, rewriting with EQUAL-TIMES-0, and expanding the
      definitions of LESSP, REMAINDER, EQUAL, PLUS, and DIFFERENCE, to the
      following two new formulas:

      Case 2.1.2.2.
              (IMPLIES (AND (NOT (NUMBERP B))
                            (NUMBERP Z)
                            (NUMBERP P)
                            (NOT (EQUAL P 0))
                            (NOT (EQUAL Z 0)))
                       (EQUAL (REMAINDER (TIMES P Z) P) 0)).

        This finally simplifies, applying REMAINDER-TIMES, and opening up
        EQUAL, to:

              T.

      Case 2.1.2.1.
              (IMPLIES (AND (NOT (NUMBERP B))
                            (NUMBERP Z)
                            (NUMBERP P)
                            (NOT (EQUAL P 0))
                            (EQUAL Z 0))
                       (EQUAL (REMAINDER 0 P) 0)).

        This finally simplifies, rewriting with REMAINDER-0-CROCK, and opening
        up the functions NUMBERP and EQUAL, to:

              T.

    Case 2.1.1.
            (IMPLIES (AND (NUMBERP X)
                          (EQUAL (LESSP X P) (NOT (ZEROP P)))
                          (NUMBERP V)
                          (NUMBERP Z)
                          (NUMBERP P)
                          (NOT (EQUAL P 0))
                          (NOT (LESSP (PLUS X (TIMES P Z))
                                      (PLUS X (TIMES P V)))))
                     (EQUAL (REMAINDER (DIFFERENCE (PLUS X (TIMES P Z))
                                                   (PLUS X (TIMES P V)))
                                       P)
                            0)).

      However this further simplifies, applying the lemmas
      LESSP-PLUS-CANCELATION, DIFFERENCE-PLUS-CANCELATION, and
      REMAINDER-DIFFERENCE-TIMES, and unfolding the functions ZEROP, NOT, and
      EQUAL, to:

            T.

Case 1. (IMPLIES (AND (EQUAL (REMAINDER A P)
                             (REMAINDER B P))
                      (LESSP A B))
                 (EQUAL (REMAINDER (DIFFERENCE B A) P)
                        0)).

  Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by
  (PLUS X (TIMES P Z)) to eliminate (REMAINDER A P) and (QUOTIENT A 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.  This produces the following four
  new goals:

  Case 1.4.
          (IMPLIES (AND (NOT (NUMBERP A))
                        (EQUAL (REMAINDER A P)
                               (REMAINDER B P))
                        (LESSP A B))
                   (EQUAL (REMAINDER (DIFFERENCE B A) P)
                          0)).

    But this further simplifies, opening up the definitions of LESSP,
    REMAINDER, DIFFERENCE, and EQUAL, to:

          T.

  Case 1.3.
          (IMPLIES (AND (EQUAL P 0)
                        (EQUAL (REMAINDER A P)
                               (REMAINDER B P))
                        (LESSP A B))
                   (EQUAL (REMAINDER (DIFFERENCE B A) P)
                          0)),

    which further simplifies, applying DIFFERENCE-X-X, and unfolding the
    functions EQUAL, REMAINDER, and LESSP, to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (NUMBERP P))
                        (EQUAL (REMAINDER A P)
                               (REMAINDER B P))
                        (LESSP A B))
                   (EQUAL (REMAINDER (DIFFERENCE B A) P)
                          0)).

    However this further simplifies, applying REMAINDER-WRT-12, DIFFERENCE-X-X,
    and REMAINDER-0-CROCK, and unfolding the functions EQUAL and LESSP, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NUMBERP X)
                        (EQUAL (LESSP X P) (NOT (ZEROP P)))
                        (NUMBERP Z)
                        (NUMBERP P)
                        (NOT (EQUAL P 0))
                        (EQUAL X (REMAINDER B P))
                        (LESSP (PLUS X (TIMES P Z)) B))
                   (EQUAL (REMAINDER (DIFFERENCE B (PLUS X (TIMES P Z)))
                                     P)
                          0)).

    This further simplifies, applying the lemma LESSP-REMAINDER2, and opening
    up the definitions of ZEROP, NOT, and EQUAL, to the conjecture:

          (IMPLIES
              (AND (NUMBERP Z)
                   (NUMBERP P)
                   (NOT (EQUAL P 0))
                   (LESSP (PLUS (REMAINDER B P) (TIMES P Z))
                          B))
              (EQUAL (REMAINDER (DIFFERENCE B
                                            (PLUS (REMAINDER B P) (TIMES P Z)))
                                P)
                     0)).

    Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace B by
    (PLUS X (TIMES P V)) to eliminate (REMAINDER B P) and (QUOTIENT B 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 constrain the new variables.  The result is two new goals:

    Case 1.1.2.
            (IMPLIES
              (AND (NOT (NUMBERP B))
                   (NUMBERP Z)
                   (NUMBERP P)
                   (NOT (EQUAL P 0))
                   (LESSP (PLUS (REMAINDER B P) (TIMES P Z))
                          B))
              (EQUAL (REMAINDER (DIFFERENCE B
                                            (PLUS (REMAINDER B P) (TIMES P Z)))
                                P)
                     0)),

      which further simplifies, opening up the definitions of LESSP, REMAINDER,
      EQUAL, and PLUS, to:

            T.

    Case 1.1.1.
            (IMPLIES (AND (NUMBERP X)
                          (EQUAL (LESSP X P) (NOT (ZEROP P)))
                          (NUMBERP V)
                          (NUMBERP Z)
                          (NUMBERP P)
                          (NOT (EQUAL P 0))
                          (LESSP (PLUS X (TIMES P Z))
                                 (PLUS X (TIMES P V))))
                     (EQUAL (REMAINDER (DIFFERENCE (PLUS X (TIMES P V))
                                                   (PLUS X (TIMES P Z)))
                                       P)
                            0)),

      which further simplifies, applying LESSP-PLUS-CANCELATION,
      DIFFERENCE-PLUS-CANCELATION, and REMAINDER-DIFFERENCE-TIMES, and opening
      up the functions ZEROP, NOT, and EQUAL, to:

            T.

Q.E.D.


[ 0.0 0.4 0.0 ]

EQUAL-MODS-TRICK-2


(DISABLE PDIFFERENCE)

[ 0.0 0.0 0.0 ]

PDIFFERENCE-OFF


(PROVE-LEMMA PRIME-KEY-TRICK
             (REWRITE)
             (IMPLIES (AND (EQUAL (REMAINDER (TIMES M A) P)
                                  (REMAINDER (TIMES M B) P))
                           (NOT (EQUAL (REMAINDER M P) 0))
                           (PRIME P))
                      (EQUAL (EQUAL (REMAINDER A P)
                                    (REMAINDER B P))
                             T))
             ((USE (PRIME-KEY-REWRITE (A M)
                                      (B (PDIFFERENCE A B)))
                   (EQUAL-MODS-TRICK-2 (A (TIMES M A))
                                       (B (TIMES M B))))
              (DISABLE PRIME-KEY-REWRITE EQUAL-MODS-TRICK-2)))

WARNING:  Note that PRIME-KEY-TRICK contains the free variable M which will be
chosen by instantiating the hypothesis:
      (EQUAL (REMAINDER (TIMES M A) P)
             (REMAINDER (TIMES M B) P)).



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

      (IMPLIES
          (AND (IMPLIES (PRIME P)
                        (EQUAL (EQUAL (REMAINDER (TIMES M (PDIFFERENCE A B))
                                                 P)
                                      0)
                               (OR (EQUAL (REMAINDER M P) 0)
                                   (EQUAL (REMAINDER (PDIFFERENCE A B) P)
                                          0))))
               (IMPLIES (EQUAL (REMAINDER (TIMES M A) P)
                               (REMAINDER (TIMES M B) P))
                        (EQUAL (REMAINDER (PDIFFERENCE (TIMES M A) (TIMES M B))
                                          P)
                               0))
               (EQUAL (REMAINDER (TIMES M A) P)
                      (REMAINDER (TIMES M B) P))
               (NOT (EQUAL (REMAINDER M P) 0))
               (NOT (EQUAL P 0))
               (NUMBERP P)
               (NOT (EQUAL P 1))
               (PRIME1 P (SUB1 P)))
          (EQUAL (EQUAL (REMAINDER A P)
                        (REMAINDER B P))
                 T)).

This simplifies, rewriting with the lemmas COMMUTATIVITY-OF-TIMES,
TIMES-DISTRIBUTES-OVER-PDIFFERENCE, and EQUAL-MODS-TRICK-1, and unfolding the
definitions of PRIME, OR, IMPLIES, and EQUAL, to:

      T.

Q.E.D.


[ 0.0 0.2 0.0 ]

PRIME-KEY-TRICK


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

This formula simplifies, applying the lemma COMMUTATIVITY-OF-TIMES, to:

      (IMPLIES (EQUAL (REMAINDER X Z) 0)
               (EQUAL (REMAINDER (TIMES X Y) (TIMES 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.  This produces the following four new formulas:

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

  This further simplifies, rewriting with the lemma EQUAL-TIMES-0, and opening
  up LESSP, REMAINDER, and EQUAL, to:

        T.

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

  which further simplifies, rewriting with the lemmas COMMUTATIVITY-OF-TIMES,
  REMAINDER-X-X, TIMES-IDENTITY, and EQUAL-TIMES-0, and expanding EQUAL and
  REMAINDER, to:

        T.

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

  which further simplifies, rewriting with REMAINDER-WRT-12, TIMES-ZERO2,
  REMAINDER-TIMES, and EQUAL-TIMES-0, and unfolding the functions EQUAL and
  REMAINDER, 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 (TIMES (PLUS V (TIMES Z W)) Y)
                                   (TIMES Y Z))
                        0)).

  This further simplifies, applying COMMUTATIVITY-OF-TIMES,
  ASSOCIATIVITY-OF-TIMES, and DIVIDES-TIMES, and opening up NUMBERP, EQUAL,
  LESSP, ZEROP, NOT, and PLUS, to:

        T.

Q.E.D.


[ 0.0 0.1 0.0 ]

PRODUCT-DIVIDES-LEMMA


(PROVE-LEMMA PRODUCT-DIVIDES
             (REWRITE)
             (IMPLIES (AND (EQUAL (REMAINDER X P) 0)
                           (EQUAL (REMAINDER X Q) 0)
                           (PRIME P)
                           (PRIME Q)
                           (NOT (EQUAL P Q)))
                      (EQUAL (REMAINDER X (TIMES P Q)) 0)))

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

      (IMPLIES (AND (EQUAL (REMAINDER X P) 0)
                    (EQUAL (REMAINDER X Q) 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))
                    (NOT (EQUAL P Q)))
               (EQUAL (REMAINDER X (TIMES P Q)) 0)).

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.  This produces the following two new conjectures:

Case 2. (IMPLIES (AND (NOT (NUMBERP X))
                      (EQUAL (REMAINDER X P) 0)
                      (EQUAL (REMAINDER X Q) 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))
                      (NOT (EQUAL P Q)))
                 (EQUAL (REMAINDER X (TIMES P Q)) 0)).

  This simplifies, rewriting with EQUAL-TIMES-0, and opening up LESSP,
  REMAINDER, and EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP Z)
                      (EQUAL (LESSP Z P) (NOT (ZEROP P)))
                      (NUMBERP V)
                      (EQUAL Z 0)
                      (EQUAL (REMAINDER (PLUS Z (TIMES P V)) Q)
                             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))
                      (NOT (EQUAL P Q)))
                 (EQUAL (REMAINDER (PLUS Z (TIMES P V))
                                   (TIMES P Q))
                        0)).

  But this simplifies, rewriting with LITTLE-STEP, PRIME-KEY-REWRITE, and
  PRODUCT-DIVIDES-LEMMA, and opening up the definitions of NUMBERP, EQUAL,
  LESSP, ZEROP, NOT, PLUS, and PRIME, to:

        T.

Q.E.D.


[ 0.0 0.3 0.0 ]

PRODUCT-DIVIDES


(PROVE-LEMMA THM-53-SPECIALIZED-TO-PRIMES NIL
             (IMPLIES (AND (PRIME P)
                           (PRIME Q)
                           (NOT (EQUAL P Q))
                           (EQUAL (REMAINDER A P)
                                  (REMAINDER B P))
                           (EQUAL (REMAINDER A Q)
                                  (REMAINDER B Q)))
                      (EQUAL (REMAINDER A (TIMES P Q))
                             (REMAINDER B (TIMES P Q))))
             NIL)

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

      (IMPLIES (AND (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))
                    (NOT (EQUAL P Q))
                    (EQUAL (REMAINDER A P)
                           (REMAINDER B P))
                    (EQUAL (REMAINDER A Q)
                           (REMAINDER B Q)))
               (EQUAL (REMAINDER A (TIMES P Q))
                      (REMAINDER B (TIMES P Q)))),

which simplifies, applying PRODUCT-DIVIDES, EQUAL-MODS-TRICK-2, and
EQUAL-MODS-TRICK-1, and unfolding the definitions of EQUAL and PRIME, to:

      T.

Q.E.D.


[ 0.0 0.2 0.0 ]

THM-53-SPECIALIZED-TO-PRIMES


(PROVE-LEMMA COROLLARY-53
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (PRIME Q)
                           (NOT (EQUAL P Q))
                           (EQUAL (REMAINDER A P)
                                  (REMAINDER B P))
                           (EQUAL (REMAINDER A Q)
                                  (REMAINDER B Q))
                           (NUMBERP B)
                           (LESSP B (TIMES P Q)))
                      (EQUAL (EQUAL (REMAINDER A (TIMES P Q)) B)
                             T))
             ((USE (THM-53-SPECIALIZED-TO-PRIMES))
              (DISABLE THM-53-SPECIALIZED-TO-PRIMES)))

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

      (IMPLIES (AND (IMPLIES (AND (PRIME P)
                                  (PRIME Q)
                                  (NOT (EQUAL P Q))
                                  (EQUAL (REMAINDER A P)
                                         (REMAINDER B P))
                                  (EQUAL (REMAINDER A Q)
                                         (REMAINDER B Q)))
                             (EQUAL (REMAINDER A (TIMES P Q))
                                    (REMAINDER B (TIMES P Q))))
                    (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))
                    (NOT (EQUAL P Q))
                    (EQUAL (REMAINDER A P)
                           (REMAINDER B P))
                    (EQUAL (REMAINDER A Q)
                           (REMAINDER B Q))
                    (NUMBERP B)
                    (LESSP B (TIMES P Q)))
               (EQUAL (EQUAL (REMAINDER A (TIMES P Q)) B)
                      T)),

which simplifies, rewriting with the lemma EQUAL-TIMES-0, and expanding the
definitions of PRIME, NOT, AND, REMAINDER, and IMPLIES, to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

COROLLARY-53


(PROVE-LEMMA THM-55-SPECIALIZED-TO-PRIMES
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (NOT (EQUAL (REMAINDER M P) 0)))
                      (EQUAL (EQUAL (REMAINDER (TIMES M X) P)
                                    (REMAINDER (TIMES M Y) P))
                             (EQUAL (REMAINDER X P)
                                    (REMAINDER Y P)))))

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

      (IMPLIES (AND (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (NOT (EQUAL (REMAINDER M P) 0)))
               (EQUAL (EQUAL (REMAINDER (TIMES M X) P)
                             (REMAINDER (TIMES M Y) P))
                      (EQUAL (REMAINDER X P)
                             (REMAINDER Y P)))),

which simplifies, trivially, to the following two new formulas:

Case 2. (IMPLIES (AND (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (EQUAL (REMAINDER M P) 0))
                      (NOT (EQUAL (REMAINDER X P)
                                  (REMAINDER Y P))))
                 (NOT (EQUAL (REMAINDER (TIMES M X) P)
                             (REMAINDER (TIMES M Y) P)))).

  But this again simplifies, applying PRIME-KEY-TRICK, and opening up the
  function PRIME, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (EQUAL (REMAINDER M P) 0))
                      (EQUAL (REMAINDER X P)
                             (REMAINDER Y P)))
                 (EQUAL (EQUAL (REMAINDER (TIMES M X) P)
                               (REMAINDER (TIMES M Y) P))
                        T)).

  But this again simplifies, applying the lemmas EQUAL-MODS-TRICK-2,
  REMAINDER-EXP-LEMMA, and EQUAL-MODS-TRICK-1, and opening up the function
  EQUAL, to:

        T.

Q.E.D.


[ 0.0 0.3 0.0 ]

THM-55-SPECIALIZED-TO-PRIMES


(PROVE-LEMMA COROLLARY-55
             (REWRITE)
             (IMPLIES (PRIME P)
                      (EQUAL (EQUAL (REMAINDER (TIMES M X) P)
                                    (REMAINDER M P))
                             (OR (EQUAL (REMAINDER M P) 0)
                                 (EQUAL (REMAINDER X P) 1))))
             ((USE (THM-55-SPECIALIZED-TO-PRIMES (Y 1)))
              (DISABLE THM-55-SPECIALIZED-TO-PRIMES)))

This conjecture can be simplified, using the abbreviations PRIME and IMPLIES,
to the conjecture:

      (IMPLIES (AND (IMPLIES (AND (PRIME P)
                                  (NOT (EQUAL (REMAINDER M P) 0)))
                             (EQUAL (EQUAL (REMAINDER (TIMES M X) P)
                                           (REMAINDER (TIMES M 1) P))
                                    (EQUAL (REMAINDER X P)
                                           (REMAINDER 1 P))))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P)))
               (EQUAL (EQUAL (REMAINDER (TIMES M X) P)
                             (REMAINDER M P))
                      (OR (EQUAL (REMAINDER M P) 0)
                          (EQUAL (REMAINDER X P) 1)))).

This simplifies, applying the lemmas TIMES-1, COMMUTATIVITY-OF-TIMES,
REMAINDER-OF-1, PRIME-KEY-REWRITE, EQUAL-TIMES-0, EQUAL-MODS-TRICK-2, and
EQUAL-MODS-TRICK-1, and expanding the definitions of PRIME, NOT, AND, IMPLIES,
EQUAL, OR, LESSP, and REMAINDER, to the new conjecture:

      (IMPLIES (AND (NOT (EQUAL (REMAINDER X P) 1))
                    (NUMBERP M)
                    (NOT (EQUAL (REMAINDER (TIMES M X) P)
                                (REMAINDER M P)))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P)))
               (NOT (EQUAL (REMAINDER M P) 0))),

which again simplifies, applying PRIME-KEY-REWRITE, and opening up PRIME and
EQUAL, to:

      T.

Q.E.D.


[ 0.0 0.2 0.0 ]

COROLLARY-55


(DEFN ALL-DISTINCT
      (L)
      (IF (NLISTP L)
          T
          (AND (NOT (MEMBER (CAR L) (CDR L)))
               (ALL-DISTINCT (CDR 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 recursive call.  Hence,
ALL-DISTINCT is accepted under the principle of definition.  From the
definition we can conclude that:
      (OR (FALSEP (ALL-DISTINCT L))
          (TRUEP (ALL-DISTINCT L)))
is a theorem.




[ 0.0 0.0 0.0 ]

ALL-DISTINCT


(DEFN ALL-LESSEQP
      (L N)
      (IF (NLISTP L)
          T
          (AND (NOT (LESSP N (CAR L)))
               (ALL-LESSEQP (CDR L) N))))

     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 recursive call.  Hence, ALL-LESSEQP
is accepted under the principle of definition.  From the definition we can
conclude that (OR (FALSEP (ALL-LESSEQP L N)) (TRUEP (ALL-LESSEQP L N))) is a
theorem.




[ 0.0 0.0 0.0 ]

ALL-LESSEQP


(DEFN ALL-NON-ZEROP
      (L)
      (IF (NLISTP L)
          T
          (AND (NOT (ZEROP (CAR L)))
               (ALL-NON-ZEROP (CDR 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 recursive call.  Hence,
ALL-NON-ZEROP is accepted under the definitional principle.  Note that:
      (OR (FALSEP (ALL-NON-ZEROP L))
          (TRUEP (ALL-NON-ZEROP L)))
is a theorem.




[ 0.0 0.0 0.0 ]

ALL-NON-ZEROP


(DEFN POSITIVES
      (N)
      (IF (ZEROP N)
          NIL
          (CONS N (POSITIVES (SUB1 N)))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to establish that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call.  Hence, POSITIVES is
accepted under the principle of definition.  From the definition we can
conclude that (OR (LITATOM (POSITIVES N)) (LISTP (POSITIVES N))) is a theorem.




[ 0.0 0.0 0.0 ]

POSITIVES


(PROVE-LEMMA LISTP-POSITIVES
             (REWRITE)
             (EQUAL (LISTP (POSITIVES N))
                    (NOT (ZEROP N))))

This conjecture simplifies, opening up the functions ZEROP and NOT, to the
following three new goals:

Case 3. (IMPLIES (NOT (NUMBERP N))
                 (EQUAL (LISTP (POSITIVES N)) F)).

  But this again simplifies, expanding the definitions of POSITIVES, LISTP,
  and EQUAL, to:

        T.

Case 2. (IMPLIES (EQUAL N 0)
                 (EQUAL (LISTP (POSITIVES N)) F)),

  which again simplifies, unfolding POSITIVES, LISTP, and EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N))
                 (EQUAL (LISTP (POSITIVES N)) T)),

  which again simplifies, clearly, to the new conjecture:

        (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N))
                 (LISTP (POSITIVES N))),

  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 N) (p N))
           (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
                    (p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to establish that the measure (COUNT N) 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 (ZEROP N)
                      (NOT (EQUAL N 0))
                      (NUMBERP N))
                 (LISTP (POSITIVES N))),

  which simplifies, unfolding the function ZEROP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP N))
                      (EQUAL (SUB1 N) 0)
                      (NOT (EQUAL N 0))
                      (NUMBERP N))
                 (LISTP (POSITIVES N))),

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

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP N))
                      (LISTP (POSITIVES (SUB1 N)))
                      (NOT (EQUAL N 0))
                      (NUMBERP N))
                 (LISTP (POSITIVES N))),

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

        T.


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


[ 0.0 0.0 0.0 ]

LISTP-POSITIVES


(PROVE-LEMMA CAR-POSITIVES
             (REWRITE)
             (EQUAL (CAR (POSITIVES N))
                    (IF (ZEROP N) 0 N)))

This simplifies, unfolding the definition of ZEROP, to the following three new
goals:

Case 3. (IMPLIES (NOT (NUMBERP N))
                 (EQUAL (CAR (POSITIVES N)) 0)).

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

        T.

Case 2. (IMPLIES (EQUAL N 0)
                 (EQUAL (CAR (POSITIVES N)) 0)),

  which again simplifies, opening up the definitions of POSITIVES, CAR, and
  EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N))
                 (EQUAL (CAR (POSITIVES N)) N)),

  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 N) (p N))
           (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
                    (p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT N) decreases according to the well-founded relation
LESSP in each induction step of the scheme.  The above induction scheme
produces the following three new goals:

Case 3. (IMPLIES (AND (ZEROP N)
                      (NOT (EQUAL N 0))
                      (NUMBERP N))
                 (EQUAL (CAR (POSITIVES N)) N)).

  This simplifies, opening up the function ZEROP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP N))
                      (EQUAL (SUB1 N) 0)
                      (NOT (EQUAL N 0))
                      (NUMBERP N))
                 (EQUAL (CAR (POSITIVES N)) N)).

  This simplifies, rewriting with CAR-CONS, and expanding the functions ZEROP
  and POSITIVES, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP N))
                      (EQUAL (CAR (POSITIVES (SUB1 N)))
                             (SUB1 N))
                      (NOT (EQUAL N 0))
                      (NUMBERP N))
                 (EQUAL (CAR (POSITIVES N)) N)),

  which simplifies, rewriting with the lemma CAR-CONS, and expanding the
  definitions of ZEROP and POSITIVES, to:

        T.


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


[ 0.0 0.0 0.0 ]

CAR-POSITIVES


(PROVE-LEMMA MEMBER-POSITIVES
             (REWRITE)
             (EQUAL (MEMBER X (POSITIVES N))
                    (IF (ZEROP X) F (LESSP X (ADD1 N)))))

This simplifies, rewriting with SUB1-ADD1, and opening up ZEROP and LESSP, to
four new conjectures:

Case 4. (IMPLIES (NOT (NUMBERP X))
                 (EQUAL (MEMBER X (POSITIVES N)) F)),

  which again simplifies, trivially, to the new conjecture:

        (IMPLIES (NOT (NUMBERP X))
                 (NOT (MEMBER X (POSITIVES N)))),

  which we will name *1.

Case 3. (IMPLIES (EQUAL X 0)
                 (EQUAL (MEMBER X (POSITIVES N)) F)).

  This again simplifies, obviously, to:

        (NOT (MEMBER 0 (POSITIVES N))),

  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 (MEMBER X (POSITIVES N))
       (IF (ZEROP X) F (LESSP X (ADD1 N)))),

named *1.  Let us appeal to the induction principle.  Two inductions are
suggested by terms in the conjecture, both of which are unflawed.  However,
one of these is more likely than the other.  We will induct according to the
following scheme:
      (AND (IMPLIES (ZEROP N) (p X N))
           (IMPLIES (AND (NOT (ZEROP N)) (p X (SUB1 N)))
                    (p X N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each induction step of the scheme.  The above induction
scheme generates two new formulas:

Case 2. (IMPLIES (ZEROP N)
                 (EQUAL (MEMBER X (POSITIVES N))
                        (IF (ZEROP X) F (LESSP X (ADD1 N))))),

  which simplifies, applying the lemma SUB1-TYPE-RESTRICTION, and opening up
  the definitions of ZEROP, POSITIVES, LISTP, MEMBER, and ADD1, to two new
  formulas:

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

    which again simplifies, using linear arithmetic, to:

          T.

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

    which again simplifies, using linear arithmetic, to:

          T.

Case 1. (IMPLIES (AND (NOT (ZEROP N))
                      (EQUAL (MEMBER X (POSITIVES (SUB1 N)))
                             (IF (ZEROP X)
                                 F
                                 (LESSP X (ADD1 (SUB1 N))))))
                 (EQUAL (MEMBER X (POSITIVES N))
                        (IF (ZEROP X) F (LESSP X (ADD1 N))))),

  which simplifies, applying ADD1-SUB1, CDR-CONS, CAR-CONS, SUB1-ADD1, and
  EQUAL-LESSP, and unfolding the functions ZEROP, POSITIVES, MEMBER, EQUAL,
  and LESSP, to the following four new conjectures:

  Case 1.4.
          (IMPLIES (AND (NOT (EQUAL N 0))
                        (NUMBERP N)
                        (EQUAL X 0)
                        (EQUAL (MEMBER X (POSITIVES (SUB1 N)))
                               F))
                   (NOT (MEMBER 0 (POSITIVES (SUB1 N))))).

    This again simplifies, clearly, to:

          T.

  Case 1.3.
          (IMPLIES (AND (NOT (EQUAL N 0))
                        (NUMBERP N)
                        (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (EQUAL (MEMBER X (POSITIVES (SUB1 N)))
                               (LESSP X N))
                        (NOT (LESSP (SUB1 X) N)))
                   (NOT (LESSP X N))).

    However this again simplifies, using linear arithmetic, to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL N 0))
                        (NUMBERP N)
                        (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (EQUAL (MEMBER X (POSITIVES (SUB1 N)))
                               (LESSP X N))
                        (NOT (LESSP (SUB1 X) N)))
                   (NOT (EQUAL X N))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL N 0))
                        (NUMBERP N)
                        (NOT (EQUAL X 0))
                        (NUMBERP X)
                        (EQUAL (MEMBER X (POSITIVES (SUB1 N)))
                               (LESSP X N))
                        (LESSP (SUB1 X) N)
                        (NOT (EQUAL X N)))
                   (LESSP X N)),

    which again simplifies, using linear arithmetic, to:

          T.


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


[ 0.0 0.1 0.0 ]

MEMBER-POSITIVES


(PROVE-LEMMA ALL-NON-ZEROP-DELETE
             (REWRITE)
             (IMPLIES (ALL-NON-ZEROP L)
                      (ALL-NON-ZEROP (DELETE X L))))


     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 L) (p X L))
           (IMPLIES (AND (NOT (NLISTP L)) (p X (CDR L)))
                    (p X L))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to 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 generates the following three new formulas:

Case 3. (IMPLIES (AND (NLISTP L) (ALL-NON-ZEROP L))
                 (ALL-NON-ZEROP (DELETE X L))).

  This simplifies, applying DELETE-NON-MEMBER, and expanding the functions
  NLISTP, ALL-NON-ZEROP, and MEMBER, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (ALL-NON-ZEROP (CDR L)))
                      (ALL-NON-ZEROP L))
                 (ALL-NON-ZEROP (DELETE X L))),

  which simplifies, opening up the functions NLISTP and ALL-NON-ZEROP, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP L))
                      (ALL-NON-ZEROP (DELETE X (CDR L)))
                      (ALL-NON-ZEROP L))
                 (ALL-NON-ZEROP (DELETE X L))),

  which simplifies, expanding NLISTP, ALL-NON-ZEROP, and DELETE, to:

        (IMPLIES (AND (LISTP L)
                      (ALL-NON-ZEROP (DELETE X (CDR L)))
                      (NOT (EQUAL (CAR L) 0))
                      (NUMBERP (CAR L))
                      (ALL-NON-ZEROP (CDR L))
                      (NOT (EQUAL X (CAR L))))
                 (ALL-NON-ZEROP (CONS (CAR L) (DELETE X (CDR L))))).

  This again simplifies, applying CDR-CONS and CAR-CONS, and expanding the
  function ALL-NON-ZEROP, to:

        T.


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


[ 0.0 0.0 0.0 ]

ALL-NON-ZEROP-DELETE


(PROVE-LEMMA ALL-DISTINCT-DELETE
             (REWRITE)
             (IMPLIES (ALL-DISTINCT L)
                      (ALL-DISTINCT (DELETE X L))))


     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 L) (p X L))
           (IMPLIES (AND (NOT (NLISTP L)) (p X (CDR L)))
                    (p X L))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to 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 generates the following three new formulas:

Case 3. (IMPLIES (AND (NLISTP L) (ALL-DISTINCT L))
                 (ALL-DISTINCT (DELETE X L))).

  This simplifies, applying DELETE-NON-MEMBER, and expanding the functions
  NLISTP, ALL-DISTINCT, and MEMBER, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (ALL-DISTINCT (CDR L)))
                      (ALL-DISTINCT L))
                 (ALL-DISTINCT (DELETE X L))),

  which simplifies, opening up the functions NLISTP and ALL-DISTINCT, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP L))
                      (ALL-DISTINCT (DELETE X (CDR L)))
                      (ALL-DISTINCT L))
                 (ALL-DISTINCT (DELETE X L))),

  which simplifies, expanding NLISTP, ALL-DISTINCT, and DELETE, to:

        (IMPLIES (AND (LISTP L)
                      (ALL-DISTINCT (DELETE X (CDR L)))
                      (NOT (MEMBER (CAR L) (CDR L)))
                      (ALL-DISTINCT (CDR L))
                      (NOT (EQUAL X (CAR L))))
                 (ALL-DISTINCT (CONS (CAR L) (DELETE X (CDR L))))).

  This again simplifies, applying CDR-CONS and CAR-CONS, and expanding the
  function ALL-DISTINCT, to the new conjecture:

        (IMPLIES (AND (LISTP L)
                      (ALL-DISTINCT (DELETE X (CDR L)))
                      (NOT (MEMBER (CAR L) (CDR L)))
                      (ALL-DISTINCT (CDR L))
                      (NOT (EQUAL X (CAR L))))
                 (NOT (MEMBER (CAR L) (DELETE X (CDR L))))),

  which again simplifies, applying the lemma MEMBER-DELETE, to:

        T.


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


[ 0.0 0.0 0.0 ]

ALL-DISTINCT-DELETE


(PROVE-LEMMA PIGEON-HOLE-PRINCIPLE-LEMMA-1
             (REWRITE)
             (IMPLIES (AND (ALL-DISTINCT L)
                           (ALL-LESSEQP L (ADD1 N)))
                      (ALL-LESSEQP (DELETE (ADD1 N) L) N)))


     Call the conjecture *1.


     We will appeal to induction.  There are three plausible 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)) (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 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 generates four new formulas:

Case 4. (IMPLIES (AND (NLISTP L)
                      (ALL-DISTINCT L)
                      (ALL-LESSEQP L (ADD1 N)))
                 (ALL-LESSEQP (DELETE (ADD1 N) L) N)),

  which simplifies, applying DELETE-NON-MEMBER, and expanding the functions
  NLISTP, ALL-DISTINCT, ALL-LESSEQP, and MEMBER, to:

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (ALL-DISTINCT (CDR L)))
                      (ALL-DISTINCT L)
                      (ALL-LESSEQP L (ADD1 N)))
                 (ALL-LESSEQP (DELETE (ADD1 N) L) N)).

  This simplifies, expanding NLISTP and ALL-DISTINCT, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (ALL-LESSEQP (CDR L) (ADD1 N)))
                      (ALL-DISTINCT L)
                      (ALL-LESSEQP L (ADD1 N)))
                 (ALL-LESSEQP (DELETE (ADD1 N) L) N)).

  This simplifies, applying SUB1-ADD1, and expanding the definitions of NLISTP,
  ALL-DISTINCT, ALL-LESSEQP, and LESSP, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP L))
                      (ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
                                   N)
                      (ALL-DISTINCT L)
                      (ALL-LESSEQP L (ADD1 N)))
                 (ALL-LESSEQP (DELETE (ADD1 N) L) N)),

  which simplifies, applying SUB1-ADD1, CDR-CONS, CAR-CONS, and
  SUB1-TYPE-RESTRICTION, and expanding the functions NLISTP, ALL-DISTINCT,
  ALL-LESSEQP, LESSP, DELETE, and EQUAL, to the following three new goals:

  Case 1.3.
          (IMPLIES (AND (LISTP L)
                        (ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
                                     N)
                        (NOT (MEMBER (CAR L) (CDR L)))
                        (ALL-DISTINCT (CDR L))
                        (NUMBERP N)
                        (NOT (LESSP N (SUB1 (CAR L))))
                        (ALL-LESSEQP (CDR L) (ADD1 N))
                        (NOT (EQUAL (ADD1 N) (CAR L))))
                   (ALL-LESSEQP (CONS (CAR L)
                                      (DELETE (ADD1 N) (CDR L)))
                                N)).

    But this again simplifies, applying the lemmas CDR-CONS and CAR-CONS, and
    opening up ALL-LESSEQP, to:

          (IMPLIES (AND (LISTP L)
                        (ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
                                     N)
                        (NOT (MEMBER (CAR L) (CDR L)))
                        (ALL-DISTINCT (CDR L))
                        (NUMBERP N)
                        (NOT (LESSP N (SUB1 (CAR L))))
                        (ALL-LESSEQP (CDR L) (ADD1 N))
                        (NOT (EQUAL (ADD1 N) (CAR L))))
                   (NOT (LESSP N (CAR L)))).

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

          (IMPLIES (AND (NOT (NUMBERP (CAR L)))
                        (LISTP L)
                        (ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
                                     N)
                        (NOT (MEMBER (CAR L) (CDR L)))
                        (ALL-DISTINCT (CDR L))
                        (NUMBERP N)
                        (NOT (LESSP N (SUB1 (CAR L))))
                        (ALL-LESSEQP (CDR L) (ADD1 N))
                        (NOT (EQUAL (ADD1 N) (CAR L))))
                   (NOT (LESSP N (CAR L)))).

    But this again simplifies, applying SUB1-NNUMBERP, and opening up EQUAL
    and LESSP, to:

          T.

  Case 1.2.
          (IMPLIES (AND (LISTP L)
                        (ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
                                     N)
                        (NOT (MEMBER (CAR L) (CDR L)))
                        (ALL-DISTINCT (CDR L))
                        (NUMBERP N)
                        (NOT (LESSP N (SUB1 (CAR L))))
                        (ALL-LESSEQP (CDR L) (ADD1 N))
                        (EQUAL (ADD1 N) (CAR L)))
                   (ALL-LESSEQP (CDR L) N)).

    This again simplifies, rewriting with SUB1-ADD1, to:

          (IMPLIES (AND (LISTP L)
                        (ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
                                     N)
                        (NOT (MEMBER (ADD1 N) (CDR L)))
                        (ALL-DISTINCT (CDR L))
                        (NUMBERP N)
                        (NOT (LESSP N N))
                        (ALL-LESSEQP (CDR L) (ADD1 N))
                        (EQUAL (ADD1 N) (CAR L)))
                   (ALL-LESSEQP (CDR L) N)),

    which further simplifies, rewriting with DELETE-NON-MEMBER, to:

          T.

  Case 1.1.
          (IMPLIES (AND (LISTP L)
                        (ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
                                     N)
                        (NOT (MEMBER (CAR L) (CDR L)))
                        (ALL-DISTINCT (CDR L))
                        (NOT (NUMBERP N))
                        (NOT (LESSP 0 (SUB1 (CAR L))))
                        (ALL-LESSEQP (CDR L) (ADD1 N)))
                   (ALL-LESSEQP (DELETE 1 L) N)).

    However this again simplifies, expanding the definitions of EQUAL and
    LESSP, to:

          (IMPLIES (AND (LISTP L)
                        (ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
                                     N)
                        (NOT (MEMBER (CAR L) (CDR L)))
                        (ALL-DISTINCT (CDR L))
                        (NOT (NUMBERP N))
                        (EQUAL (SUB1 (CAR L)) 0)
                        (ALL-LESSEQP (CDR L) (ADD1 N)))
                   (ALL-LESSEQP (DELETE 1 L) N)).

    However this further simplifies, rewriting with SUB1-TYPE-RESTRICTION, to:

          (IMPLIES (AND (LISTP L)
                        (ALL-LESSEQP (DELETE 1 (CDR L)) N)
                        (NOT (MEMBER (CAR L) (CDR L)))
                        (ALL-DISTINCT (CDR L))
                        (NOT (NUMBERP N))
                        (EQUAL (SUB1 (CAR L)) 0)
                        (ALL-LESSEQP (CDR L) 1))
                   (ALL-LESSEQP (DELETE 1 L) N)),

    which again simplifies, opening up DELETE, to two new conjectures:

    Case 1.1.2.
            (IMPLIES (AND (LISTP L)
                          (ALL-LESSEQP (DELETE 1 (CDR L)) N)
                          (NOT (MEMBER (CAR L) (CDR L)))
                          (ALL-DISTINCT (CDR L))
                          (NOT (NUMBERP N))
                          (EQUAL (SUB1 (CAR L)) 0)
                          (ALL-LESSEQP (CDR L) 1)
                          (NOT (EQUAL 1 (CAR L))))
                     (ALL-LESSEQP (CONS (CAR L) (DELETE 1 (CDR L)))
                                  N)),

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

      Case 1.1.2.2.
              (IMPLIES (AND (LESSP (CAR L) 1)
                            (LISTP L)
                            (ALL-LESSEQP (DELETE 1 (CDR L)) N)
                            (NOT (MEMBER (CAR L) (CDR L)))
                            (ALL-DISTINCT (CDR L))
                            (NOT (NUMBERP N))
                            (EQUAL (SUB1 (CAR L)) 0)
                            (ALL-LESSEQP (CDR L) 1)
                            (NOT (EQUAL 1 (CAR L))))
                       (ALL-LESSEQP (CONS (CAR L) (DELETE 1 (CDR L)))
                                    N)),

        which finally simplifies, rewriting with CDR-CONS, CAR-CONS, and
        SUB1-NNUMBERP, and opening up LESSP, SUB1, NUMBERP, EQUAL, and
        ALL-LESSEQP, to:

              T.

      Case 1.1.2.1.
              (IMPLIES (AND (NOT (NUMBERP (CAR L)))
                            (LISTP L)
                            (ALL-LESSEQP (DELETE 1 (CDR L)) N)
                            (NOT (MEMBER (CAR L) (CDR L)))
                            (ALL-DISTINCT (CDR L))
                            (NOT (NUMBERP N))
                            (EQUAL (SUB1 (CAR L)) 0)
                            (ALL-LESSEQP (CDR L) 1)
                            (NOT (EQUAL 1 (CAR L))))
                       (ALL-LESSEQP (CONS (CAR L) (DELETE 1 (CDR L)))
                                    N)).

        However this finally simplifies, rewriting with SUB1-NNUMBERP,
        CDR-CONS, and CAR-CONS, and expanding the functions EQUAL, LESSP, and
        ALL-LESSEQP, to:

              T.

    Case 1.1.1.
            (IMPLIES (AND (LISTP L)
                          (ALL-LESSEQP (DELETE 1 (CDR L)) N)
                          (NOT (MEMBER (CAR L) (CDR L)))
                          (ALL-DISTINCT (CDR L))
                          (NOT (NUMBERP N))
                          (EQUAL (SUB1 (CAR L)) 0)
                          (ALL-LESSEQP (CDR L) 1)
                          (EQUAL 1 (CAR L)))
                     (ALL-LESSEQP (CDR L) N)).

      This again simplifies, rewriting with DELETE-NON-MEMBER, to:

            T.


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


[ 0.0 0.1 0.0 ]

PIGEON-HOLE-PRINCIPLE-LEMMA-1


(PROVE-LEMMA PIGEON-HOLE-PRINCIPLE-LEMMA-2
             (REWRITE)
             (IMPLIES (AND (NOT (MEMBER (ADD1 N) X))
                           (ALL-LESSEQP X (ADD1 N)))
                      (ALL-LESSEQP X N)))


     Call the conjecture *1.


     We will appeal to induction.  There are three plausible inductions.
However, they merge into one likely candidate induction.  We will induct
according to the following scheme:
      (AND (IMPLIES (NLISTP X) (p X N))
           (IMPLIES (AND (NOT (NLISTP X))
                         (EQUAL (ADD1 N) (CAR X)))
                    (p X N))
           (IMPLIES (AND (NOT (NLISTP X))
                         (NOT (EQUAL (ADD1 N) (CAR X)))
                         (p (CDR X) N))
                    (p X N))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP 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 five new formulas:

Case 5. (IMPLIES (AND (NLISTP X)
                      (NOT (MEMBER (ADD1 N) X))
                      (ALL-LESSEQP X (ADD1 N)))
                 (ALL-LESSEQP X N)),

  which simplifies, expanding the definitions of NLISTP, MEMBER, and
  ALL-LESSEQP, to:

        T.

Case 4. (IMPLIES (AND (NOT (NLISTP X))
                      (EQUAL (ADD1 N) (CAR X))
                      (NOT (MEMBER (ADD1 N) X))
                      (ALL-LESSEQP X (ADD1 N)))
                 (ALL-LESSEQP X N)),

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

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP X))
                      (NOT (EQUAL (ADD1 N) (CAR X)))
                      (MEMBER (ADD1 N) (CDR X))
                      (NOT (MEMBER (ADD1 N) X))
                      (ALL-LESSEQP X (ADD1 N)))
                 (ALL-LESSEQP X N)),

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

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP X))
                      (NOT (EQUAL (ADD1 N) (CAR X)))
                      (NOT (ALL-LESSEQP (CDR X) (ADD1 N)))
                      (NOT (MEMBER (ADD1 N) X))
                      (ALL-LESSEQP X (ADD1 N)))
                 (ALL-LESSEQP X N)),

  which simplifies, rewriting with SUB1-ADD1, and expanding the definitions of
  NLISTP, MEMBER, ALL-LESSEQP, and LESSP, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP X))
                      (NOT (EQUAL (ADD1 N) (CAR X)))
                      (ALL-LESSEQP (CDR X) N)
                      (NOT (MEMBER (ADD1 N) X))
                      (ALL-LESSEQP X (ADD1 N)))
                 (ALL-LESSEQP X N)).

  This simplifies, rewriting with SUB1-ADD1, and opening up the functions
  NLISTP, MEMBER, ALL-LESSEQP, LESSP, and EQUAL, to two new conjectures:

  Case 1.2.
          (IMPLIES (AND (LISTP X)
                        (NOT (EQUAL (ADD1 N) (CAR X)))
                        (ALL-LESSEQP (CDR X) N)
                        (NOT (MEMBER (ADD1 N) (CDR X)))
                        (NUMBERP N)
                        (NOT (LESSP N (SUB1 (CAR X))))
                        (ALL-LESSEQP (CDR X) (ADD1 N)))
                   (NOT (LESSP N (CAR X)))),

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

          (IMPLIES (AND (NOT (NUMBERP (CAR X)))
                        (LISTP X)
                        (NOT (EQUAL (ADD1 N) (CAR X)))
                        (ALL-LESSEQP (CDR X) N)
                        (NOT (MEMBER (ADD1 N) (CDR X)))
                        (NUMBERP N)
                        (NOT (LESSP N (SUB1 (CAR X))))
                        (ALL-LESSEQP (CDR X) (ADD1 N)))
                   (NOT (LESSP N (CAR X)))).

    But this again simplifies, appealing to the lemma SUB1-NNUMBERP, and
    expanding EQUAL and LESSP, to:

          T.

  Case 1.1.
          (IMPLIES (AND (LISTP X)
                        (NOT (EQUAL (ADD1 N) (CAR X)))
                        (ALL-LESSEQP (CDR X) N)
                        (NOT (MEMBER (ADD1 N) (CDR X)))
                        (NOT (NUMBERP N))
                        (NOT (LESSP 0 (SUB1 (CAR X))))
                        (ALL-LESSEQP (CDR X) (ADD1 N))
                        (NOT (EQUAL (CAR X) 0)))
                   (NOT (NUMBERP (CAR X)))),

    which again simplifies, using linear arithmetic, to:

          (IMPLIES (AND (EQUAL (CAR X) 1)
                        (LISTP X)
                        (NOT (EQUAL (ADD1 N) 1))
                        (ALL-LESSEQP (CDR X) N)
                        (NOT (MEMBER (ADD1 N) (CDR X)))
                        (NOT (NUMBERP N))
                        (NOT (LESSP 0 (SUB1 1)))
                        (ALL-LESSEQP (CDR X) (ADD1 N))
                        (NOT (EQUAL 1 0)))
                   (NOT (NUMBERP 1))).

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

          T.


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


[ 0.0 0.0 0.0 ]

PIGEON-HOLE-PRINCIPLE-LEMMA-2


(PROVE-LEMMA PERM-MEMBER
             (REWRITE)
             (IMPLIES (AND (PERM A B) (MEMBER X A))
                      (MEMBER X B)))

WARNING:  Note that PERM-MEMBER contains the free variable A which will be
chosen by instantiating the hypothesis (PERM A B).



     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.  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 (NLISTP A) (p X B A))
           (IMPLIES (AND (NOT (NLISTP A))
                         (MEMBER (CAR A) B)
                         (p X (DELETE (CAR A) B) (CDR A)))
                    (p X B A))
           (IMPLIES (AND (NOT (NLISTP A))
                         (NOT (MEMBER (CAR A) B)))
                    (p X B A))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to prove that the measure (COUNT A) decreases according to
the well-founded relation LESSP in each induction step of the scheme.  Note,
however, the inductive instance chosen for B.  The above induction scheme
leads to five new goals:

Case 5. (IMPLIES (AND (NLISTP A)
                      (PERM A B)
                      (MEMBER X A))
                 (MEMBER X B)),

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

        T.

Case 4. (IMPLIES (AND (NOT (NLISTP A))
                      (MEMBER (CAR A) B)
                      (NOT (PERM (CDR A) (DELETE (CAR A) B)))
                      (PERM A B)
                      (MEMBER X A))
                 (MEMBER X B)),

  which simplifies, expanding NLISTP and PERM, to:

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP A))
                      (MEMBER (CAR A) B)
                      (NOT (MEMBER X (CDR A)))
                      (PERM A B)
                      (MEMBER X A))
                 (MEMBER X B)),

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

        (IMPLIES (AND (LISTP A)
                      (MEMBER (CAR A) B)
                      (NOT (MEMBER X (CDR A)))
                      (PERM (CDR A) (DELETE (CAR A) B))
                      (EQUAL X (CAR A)))
                 (MEMBER X B)).

  This again simplifies, trivially, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP A))
                      (MEMBER (CAR A) B)
                      (MEMBER X (DELETE (CAR A) B))
                      (PERM A B)
                      (MEMBER X A))
                 (MEMBER X B)).

  This simplifies, appealing to the lemma MEMBER-DELETE, and expanding the
  functions NLISTP, PERM, and MEMBER, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP A))
                      (NOT (MEMBER (CAR A) B))
                      (PERM A B)
                      (MEMBER X A))
                 (MEMBER X B)).

  This simplifies, expanding the functions NLISTP and PERM, to:

        T.


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


[ 0.0 0.0 0.0 ]

PERM-MEMBER


(DEFN PIGEON-HOLE-INDUCTION
      (L)
      (IF (LISTP L)
          (IF (MEMBER (LENGTH L) L)
              (PIGEON-HOLE-INDUCTION (DELETE (LENGTH L) L))
              (PIGEON-HOLE-INDUCTION (CDR L)))
          T))

     Linear arithmetic and the lemmas LESSP-COUNT-DELETE and CDR-LESSP inform
us that the measure (COUNT L) decreases according to the well-founded relation
LESSP in each recursive call.  Hence, PIGEON-HOLE-INDUCTION is accepted under
the principle of definition.  Note that (TRUEP (PIGEON-HOLE-INDUCTION L)) is a
theorem.




[ 0.0 0.0 0.0 ]

PIGEON-HOLE-INDUCTION


(PROVE-LEMMA PIGEON-HOLE-PRINCIPLE NIL
             (IMPLIES (AND (ALL-NON-ZEROP L)
                           (ALL-DISTINCT L)
                           (ALL-LESSEQP L (LENGTH L)))
                      (PERM (POSITIVES (LENGTH L)) L))
             ((INDUCT (PIGEON-HOLE-INDUCTION L))))

This conjecture can be simplified, using the abbreviations IMPLIES, NOT, OR,
and AND, to three new formulas:

Case 3. (IMPLIES
               (AND (LISTP L)
                    (MEMBER (LENGTH L) L)
                    (IMPLIES (AND (ALL-NON-ZEROP (DELETE (LENGTH L) L))
                                  (ALL-DISTINCT (DELETE (LENGTH L) L))
                                  (ALL-LESSEQP (DELETE (LENGTH L) L)
                                               (LENGTH (DELETE (LENGTH L) L))))
                             (PERM (POSITIVES (LENGTH (DELETE (LENGTH L) L)))
                                   (DELETE (LENGTH L) L)))
                    (ALL-NON-ZEROP L)
                    (ALL-DISTINCT L)
                    (ALL-LESSEQP L (LENGTH L)))
               (PERM (POSITIVES (LENGTH L)) L)),

  which simplifies, appealing to the lemmas ALL-NON-ZEROP-DELETE,
  ALL-DISTINCT-DELETE, and LENGTH-DELETE, and unfolding AND and IMPLIES, to
  two new conjectures:

  Case 3.2.
          (IMPLIES (AND (LISTP L)
                        (MEMBER (LENGTH L) L)
                        (NOT (ALL-LESSEQP (DELETE (LENGTH L) L)
                                          (LENGTH (CDR L))))
                        (ALL-NON-ZEROP L)
                        (ALL-DISTINCT L)
                        (ALL-LESSEQP L (LENGTH L)))
                   (PERM (POSITIVES (LENGTH L)) L)),

    which again simplifies, appealing to the lemmas SUB1-ADD1, CDR-CONS, and
    CAR-CONS, and opening up the definitions of LENGTH, POSITIVES, and PERM,
    to:

          (IMPLIES (AND (LISTP L)
                        (MEMBER (ADD1 (LENGTH (CDR L))) L)
                        (NOT (ALL-LESSEQP (DELETE (ADD1 (LENGTH (CDR L))) L)
                                          (LENGTH (CDR L))))
                        (ALL-NON-ZEROP L)
                        (ALL-DISTINCT L)
                        (ALL-LESSEQP L
                                     (ADD1 (LENGTH (CDR L)))))
                   (PERM (POSITIVES (LENGTH (CDR L)))
                         (DELETE (ADD1 (LENGTH (CDR L))) L))).

    But this again simplifies, applying PIGEON-HOLE-PRINCIPLE-LEMMA-1, to:

          T.

  Case 3.1.
          (IMPLIES (AND (LISTP L)
                        (MEMBER (LENGTH L) L)
                        (PERM (POSITIVES (LENGTH (CDR L)))
                              (DELETE (LENGTH L) L))
                        (ALL-NON-ZEROP L)
                        (ALL-DISTINCT L)
                        (ALL-LESSEQP L (LENGTH L)))
                   (PERM (POSITIVES (LENGTH L)) L)).

    This again simplifies, applying SUB1-ADD1, CDR-CONS, and CAR-CONS, and
    expanding the functions LENGTH, POSITIVES, and PERM, to:

          T.

Case 2. (IMPLIES (AND (LISTP L)
                      (NOT (MEMBER (LENGTH L) L))
                      (IMPLIES (AND (ALL-NON-ZEROP (CDR L))
                                    (ALL-DISTINCT (CDR L))
                                    (ALL-LESSEQP (CDR L)
                                                 (LENGTH (CDR L))))
                               (PERM (POSITIVES (LENGTH (CDR L)))
                                     (CDR L)))
                      (ALL-NON-ZEROP L)
                      (ALL-DISTINCT L)
                      (ALL-LESSEQP L (LENGTH L)))
                 (PERM (POSITIVES (LENGTH L)) L)).

  This simplifies, applying SUB1-ADD1 and CAR-CONS, and unfolding LENGTH, AND,
  IMPLIES, ALL-NON-ZEROP, ALL-DISTINCT, POSITIVES, and PERM, to two new goals:

  Case 2.2.
          (IMPLIES (AND (LISTP L)
                        (NOT (MEMBER (ADD1 (LENGTH (CDR L))) L))
                        (NOT (ALL-LESSEQP (CDR L)
                                          (LENGTH (CDR L))))
                        (NOT (EQUAL (CAR L) 0))
                        (NUMBERP (CAR L))
                        (ALL-NON-ZEROP (CDR L))
                        (NOT (MEMBER (CAR L) (CDR L)))
                        (ALL-DISTINCT (CDR L)))
                   (NOT (ALL-LESSEQP L
                                     (ADD1 (LENGTH (CDR L)))))).

    Applying the lemma CAR-CDR-ELIM, replace L by (CONS Z X) to eliminate
    (CDR L) and (CAR L).  This produces:

          (IMPLIES (AND (NOT (MEMBER (ADD1 (LENGTH X)) (CONS Z X)))
                        (NOT (ALL-LESSEQP X (LENGTH X)))
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (ALL-NON-ZEROP X)
                        (NOT (MEMBER Z X))
                        (ALL-DISTINCT X))
                   (NOT (ALL-LESSEQP (CONS Z X)
                                     (ADD1 (LENGTH X))))),

    which further simplifies, rewriting with CDR-CONS, CAR-CONS, and SUB1-ADD1,
    and opening up the definitions of MEMBER, LESSP, and ALL-LESSEQP, to:

          (IMPLIES (AND (NOT (EQUAL (ADD1 (LENGTH X)) Z))
                        (NOT (MEMBER (ADD1 (LENGTH X)) X))
                        (NOT (ALL-LESSEQP X (LENGTH X)))
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (ALL-NON-ZEROP X)
                        (NOT (MEMBER Z X))
                        (ALL-DISTINCT X)
                        (NOT (LESSP (LENGTH X) (SUB1 Z))))
                   (NOT (ALL-LESSEQP X (ADD1 (LENGTH X))))),

    which again simplifies, applying PIGEON-HOLE-PRINCIPLE-LEMMA-2, to:

          T.

  Case 2.1.
          (IMPLIES (AND (LISTP L)
                        (NOT (MEMBER (ADD1 (LENGTH (CDR L))) L))
                        (PERM (POSITIVES (LENGTH (CDR L)))
                              (CDR L))
                        (NOT (EQUAL (CAR L) 0))
                        (NUMBERP (CAR L))
                        (ALL-NON-ZEROP (CDR L))
                        (NOT (MEMBER (CAR L) (CDR L)))
                        (ALL-DISTINCT (CDR L)))
                   (NOT (ALL-LESSEQP L
                                     (ADD1 (LENGTH (CDR L)))))).

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

          (IMPLIES (AND (NOT (MEMBER (ADD1 (LENGTH X)) (CONS Z X)))
                        (PERM (POSITIVES (LENGTH X)) X)
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (ALL-NON-ZEROP X)
                        (NOT (MEMBER Z X))
                        (ALL-DISTINCT X))
                   (NOT (ALL-LESSEQP (CONS Z X)
                                     (ADD1 (LENGTH X))))).

    This further simplifies, rewriting with the lemmas CDR-CONS, CAR-CONS, and
    SUB1-ADD1, and expanding the definitions of MEMBER, LESSP, and ALL-LESSEQP,
    to the conjecture:

          (IMPLIES (AND (NOT (EQUAL (ADD1 (LENGTH X)) Z))
                        (NOT (MEMBER (ADD1 (LENGTH X)) X))
                        (PERM (POSITIVES (LENGTH X)) X)
                        (NOT (EQUAL Z 0))
                        (NUMBERP Z)
                        (ALL-NON-ZEROP X)
                        (NOT (MEMBER Z X))
                        (ALL-DISTINCT X)
                        (NOT (LESSP (LENGTH X) (SUB1 Z))))
                   (NOT (ALL-LESSEQP X (ADD1 (LENGTH X))))).

    However this again simplifies, using linear arithmetic and applying
    MEMBER-POSITIVES and PERM-MEMBER, to:

          T.

Case 1. (IMPLIES (AND (NOT (LISTP L))
                      (ALL-NON-ZEROP L)
                      (ALL-DISTINCT L)
                      (ALL-LESSEQP L (LENGTH L)))
                 (PERM (POSITIVES (LENGTH L)) L)).

  This simplifies, appealing to the lemma PIGEON-HOLE-PRINCIPLE-LEMMA-2, and
  expanding the definitions of ALL-NON-ZEROP, ALL-DISTINCT, LENGTH,
  ALL-LESSEQP, MEMBER, ADD1, POSITIVES, LISTP, and PERM, to:

        T.

Q.E.D.


[ 0.0 0.3 0.0 ]

PIGEON-HOLE-PRINCIPLE


(PROVE-LEMMA PERM-TIMES-LIST NIL
             (IMPLIES (PERM L1 L2)
                      (EQUAL (TIMES-LIST L1)
                             (TIMES-LIST L2))))


     Name the conjecture *1.


     We will appeal to induction.  The recursive terms in the conjecture
suggest four inductions.  They merge into two likely candidate inductions,
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 (NLISTP L1) (p L1 L2))
           (IMPLIES (AND (NOT (NLISTP L1))
                         (MEMBER (CAR L1) L2)
                         (p (CDR L1) (DELETE (CAR L1) L2)))
                    (p L1 L2))
           (IMPLIES (AND (NOT (NLISTP L1))
                         (NOT (MEMBER (CAR L1) L2)))
                    (p L1 L2))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT L1) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  Note,
however, the inductive instance chosen for L2.  The above induction scheme
produces the following four new formulas:

Case 4. (IMPLIES (AND (NLISTP L1) (PERM L1 L2))
                 (EQUAL (TIMES-LIST L1)
                        (TIMES-LIST L2))).

  This simplifies, expanding the definitions of NLISTP, PERM, TIMES-LIST, and
  EQUAL, to:

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP L1))
                      (MEMBER (CAR L1) L2)
                      (NOT (PERM (CDR L1) (DELETE (CAR L1) L2)))
                      (PERM L1 L2))
                 (EQUAL (TIMES-LIST L1)
                        (TIMES-LIST L2))).

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

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP L1))
                      (MEMBER (CAR L1) L2)
                      (EQUAL (TIMES-LIST (CDR L1))
                             (TIMES-LIST (DELETE (CAR L1) L2)))
                      (PERM L1 L2))
                 (EQUAL (TIMES-LIST L1)
                        (TIMES-LIST L2))),

  which simplifies, rewriting with the lemma PERM-MEMBER, and opening up the
  functions NLISTP, MEMBER, PERM, and TIMES-LIST, to the goal:

        (IMPLIES (AND (LISTP L1)
                      (EQUAL (TIMES-LIST (CDR L1))
                             (TIMES-LIST (DELETE (CAR L1) L2)))
                      (MEMBER (CAR L1) L2)
                      (PERM (CDR L1) (DELETE (CAR L1) L2)))
                 (EQUAL (TIMES (CAR L1) (TIMES-LIST (CDR L1)))
                        (TIMES-LIST L2))).

  Appealing to the lemma CAR-CDR-ELIM, we now replace L1 by (CONS Z X) to
  eliminate (CDR L1) and (CAR L1).  This generates:

        (IMPLIES (AND (EQUAL (TIMES-LIST X)
                             (TIMES-LIST (DELETE Z L2)))
                      (MEMBER Z L2)
                      (PERM X (DELETE Z L2)))
                 (EQUAL (TIMES Z (TIMES-LIST X))
                        (TIMES-LIST L2))).

  We use the above equality hypothesis by substituting:
        (TIMES-LIST (DELETE Z L2))
  for (TIMES-LIST X) and throwing away the equality.  This produces:

        (IMPLIES (AND (MEMBER Z L2)
                      (PERM X (DELETE Z L2)))
                 (EQUAL (TIMES Z (TIMES-LIST (DELETE Z L2)))
                        (TIMES-LIST L2))),

  which further simplifies, applying TIMES-TIMES-LIST-DELETE, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP L1))
                      (NOT (MEMBER (CAR L1) L2))
                      (PERM L1 L2))
                 (EQUAL (TIMES-LIST L1)
                        (TIMES-LIST L2))).

  This simplifies, applying the lemma PERM-MEMBER, and opening up NLISTP and
  MEMBER, to:

        T.


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


[ 0.0 0.0 0.0 ]

PERM-TIMES-LIST


(PROVE-LEMMA TIMES-LIST-POSITIVES
             (REWRITE)
             (EQUAL (TIMES-LIST (POSITIVES N))
                    (FACT N)))


     Give the conjecture the name *1.


     We will appeal to 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 (ZEROP N) (p N))
           (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
                    (p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT N) 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 N)
                 (EQUAL (TIMES-LIST (POSITIVES N))
                        (FACT N))).

  This simplifies, expanding the functions ZEROP, POSITIVES, TIMES-LIST, FACT,
  and EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP N))
                      (EQUAL (TIMES-LIST (POSITIVES (SUB1 N)))
                             (FACT (SUB1 N))))
                 (EQUAL (TIMES-LIST (POSITIVES N))
                        (FACT N))).

  This simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS, and
  opening up ZEROP, POSITIVES, TIMES-LIST, and FACT, to:

        T.


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


[ 0.0 0.0 0.0 ]

TIMES-LIST-POSITIVES


(PROVE-LEMMA TIMES-LIST-EQUAL-FACT
             (REWRITE)
             (IMPLIES (PERM (POSITIVES N) L)
                      (EQUAL (TIMES-LIST L) (FACT N)))
             ((USE (PERM-TIMES-LIST (L1 (POSITIVES N))
                                    (L2 L)))
              (DISABLE PERM-TIMES-LIST)))

WARNING:  Note that TIMES-LIST-EQUAL-FACT contains the free variable N which
will be chosen by instantiating the hypothesis (PERM (POSITIVES N) L).


This conjecture can be simplified, using the abbreviations IMPLIES and
TIMES-LIST-POSITIVES, to the conjecture:

      (IMPLIES (AND (IMPLIES (PERM (POSITIVES N) L)
                             (EQUAL (FACT N) (TIMES-LIST L)))
                    (PERM (POSITIVES N) L))
               (EQUAL (TIMES-LIST L) (FACT N))).

This simplifies, unfolding the function IMPLIES, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

TIMES-LIST-EQUAL-FACT


(PROVE-LEMMA PRIME-FACT
             (REWRITE)
             (IMPLIES (AND (PRIME P) (LESSP N P))
                      (NOT (EQUAL (REMAINDER (FACT N) P) 0)))
             ((INDUCT (FACT N))))

This formula can be simplified, using the abbreviations ZEROP, PRIME, IMPLIES,
NOT, OR, and AND, to the following two new formulas:

Case 2. (IMPLIES (AND (ZEROP N)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP N P))
                 (NOT (EQUAL (REMAINDER (FACT N) P) 0))).

  This simplifies, rewriting with REMAINDER-OF-1, and unfolding the functions
  ZEROP, EQUAL, LESSP, and FACT, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL N 0))
                      (NUMBERP N)
                      (IMPLIES (AND (PRIME P) (LESSP (SUB1 N) P))
                               (NOT (EQUAL (REMAINDER (FACT (SUB1 N)) P)
                                           0)))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP N P))
                 (NOT (EQUAL (REMAINDER (FACT N) P) 0))),

  which simplifies, rewriting with PRIME-KEY-REWRITE, and opening up the
  definitions of PRIME, AND, NOT, IMPLIES, LESSP, FACT, and REMAINDER, to the
  new conjecture:

        (IMPLIES (AND (NOT (EQUAL N 0))
                      (NUMBERP N)
                      (NOT (LESSP (SUB1 N) P))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP (SUB1 N) (SUB1 P)))
                 (NOT (EQUAL (REMAINDER (FACT (SUB1 N)) P)
                             0))),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.1 0.0 ]

PRIME-FACT


(DEFN S
      (N M P)
      (IF (ZEROP N)
          NIL
          (CONS (REMAINDER (TIMES M N) P)
                (S (SUB1 N) M P))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call.  Hence, S is accepted under the
definitional principle.  Note that (OR (LITATOM (S N M P)) (LISTP (S N M P)))
is a theorem.




[ 0.0 0.0 0.0 ]

S


(PROVE-LEMMA REMAINDER-TIMES-LIST-S NIL
             (EQUAL (REMAINDER (TIMES-LIST (S N M P)) P)
                    (REMAINDER (TIMES (FACT N) (EXP M N))
                               P)))


     Give the conjecture the name *1.


     Perhaps we can prove it by induction.  The recursive terms in the
conjecture suggest three inductions.  However, they merge