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

(#./basic/rsa.lib #./basic/rsa)


(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


(DEFN INVERSE
      (J P)
      (IF (EQUAL P 2)
          (REMAINDER J 2)
          (REMAINDER (EXP J (DIFFERENCE P 2))
                     P)))

     From the definition we can conclude that (NUMBERP (INVERSE J P)) is a
theorem.




[ 0.0 0.0 0.0 ]

INVERSE


(PROVE-LEMMA INVERSE-INVERTS-LEMMA
             (REWRITE)
             (IMPLIES (NOT (ZEROP P))
                      (EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
                             (REMAINDER (EXP J (SUB1 P)) P))))

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

      (IMPLIES (AND (NOT (EQUAL P 0)) (NUMBERP P))
               (EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
                      (REMAINDER (EXP J (SUB1 P)) P))),

which simplifies, rewriting with DIFFERENCE-1 and COMMUTATIVITY-OF-TIMES, and
unfolding DIFFERENCE, EQUAL, NUMBERP, SUB1, and INVERSE, to the following two
new conjectures:

Case 2. (IMPLIES
                (AND (NOT (EQUAL P 0))
                     (NUMBERP P)
                     (NOT (EQUAL P 2)))
                (EQUAL (REMAINDER (TIMES J
                                         (REMAINDER (EXP J (SUB1 (SUB1 P))) P))
                                  P)
                       (REMAINDER (EXP J (SUB1 P)) P))).

  This again simplifies, applying the lemma TIMES-MOD-1, and unfolding EXP, to:

        (IMPLIES (AND (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 2))
                      (EQUAL (SUB1 P) 0))
                 (EQUAL (REMAINDER (TIMES J (EXP J (SUB1 (SUB1 P))))
                                   P)
                        (REMAINDER 1 P))).

  However this again simplifies, rewriting with the lemmas EXP-BY-0, TIMES-1,
  COMMUTATIVITY-OF-TIMES, and REMAINDER-OF-1, and opening up the definition of
  SUB1, to four new formulas:

  Case 2.4.
          (IMPLIES (AND (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (EQUAL P 2))
                        (EQUAL (SUB1 P) 0)
                        (NOT (EQUAL P 1))
                        (NOT (NUMBERP J)))
                   (EQUAL (REMAINDER 0 P) 1)),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 2.3.
          (IMPLIES (AND (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (EQUAL P 2))
                        (EQUAL (SUB1 P) 0)
                        (NOT (EQUAL P 1))
                        (NUMBERP J))
                   (EQUAL (REMAINDER J P) 1)),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 2.2.
          (IMPLIES (AND (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (EQUAL P 2))
                        (EQUAL (SUB1 P) 0)
                        (EQUAL P 1)
                        (NOT (NUMBERP J)))
                   (EQUAL (REMAINDER 0 P) 0)),

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

          T.

  Case 2.1.
          (IMPLIES (AND (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (EQUAL P 2))
                        (EQUAL (SUB1 P) 0)
                        (EQUAL P 1)
                        (NUMBERP J))
                   (EQUAL (REMAINDER J P) 0)),

    which again simplifies, rewriting with REMAINDER-WRT-1, and unfolding
    EQUAL, NUMBERP, and SUB1, to:

          T.

Case 1. (IMPLIES (AND (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (EQUAL P 2))
                 (EQUAL (REMAINDER (TIMES J (REMAINDER J 2))
                                   P)
                        (REMAINDER (EXP J (SUB1 P)) P))).

  However this again simplifies, applying TIMES-MOD-1, COMMUTATIVITY-OF-TIMES,
  TIMES-1, and EXP-BY-0, and opening up the definitions of EQUAL, NUMBERP,
  SUB1, and EXP, to the following two new goals:

  Case 1.2.
          (IMPLIES (NOT (NUMBERP J))
                   (EQUAL (REMAINDER (TIMES J J) 2)
                          (REMAINDER 0 2))).

    This again simplifies, appealing to the lemma TIMES-ZERO2, and unfolding
    the definitions of REMAINDER and EQUAL, to:

          T.

  Case 1.1.
          (IMPLIES (NUMBERP J)
                   (EQUAL (REMAINDER (TIMES J J) 2)
                          (REMAINDER J 2))),

    which again simplifies, rewriting with COROLLARY-55, and opening up PRIME,
    to the new goal:

          (IMPLIES (AND (NUMBERP J)
                        (NOT (EQUAL (REMAINDER J 2) 0)))
                   (EQUAL (REMAINDER J 2) 1)),

    which again simplifies, using linear arithmetic, applying
    LESSP-REMAINDER-DIVISOR, and unfolding the definition of EQUAL, to:

          T.

Q.E.D.


[ 0.0 0.4 0.0 ]

INVERSE-INVERTS-LEMMA


(PROVE-LEMMA INVERSE-INVERTS
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (NOT (EQUAL (REMAINDER J P) 0)))
                      (EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
                             1))
             ((USE (INVERSE-INVERTS-LEMMA))
              (DISABLE INVERSE)))

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

      (IMPLIES (AND (IMPLIES (NOT (ZEROP P))
                             (EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
                                    (REMAINDER (EXP J (SUB1 P)) P)))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (NOT (EQUAL (REMAINDER J P) 0)))
               (EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
                      1)),

which simplifies, rewriting with COMMUTATIVITY-OF-TIMES and FERMAT-THM, and
expanding ZEROP, NOT, PRIME, IMPLIES, and EQUAL, to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

INVERSE-INVERTS


(PROVE-LEMMA INVERSE-IS-UNIQUE
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (EQUAL 1 (REMAINDER (TIMES M X) P)))
                      (EQUAL (INVERSE M P) (REMAINDER X P)))
             ((USE (INVERSE-INVERTS (J M))
                   (THM-55-SPECIALIZED-TO-PRIMES (Y (INVERSE M P))))))

WARNING:  Note that the rewrite rule INVERSE-IS-UNIQUE will be stored so as to
apply only to terms with the nonrecursive function symbol INVERSE.


WARNING:  Note that INVERSE-IS-UNIQUE contains the free variable X which will
be chosen by instantiating the hypothesis (EQUAL 1 (REMAINDER (TIMES M X) P)).


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

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

This simplifies, applying DIFFERENCE-1, COMMUTATIVITY-OF-TIMES, TIMES-MOD-1,
and LESSP-REMAINDER2, and unfolding the functions PRIME, NOT, AND, DIFFERENCE,
EQUAL, NUMBERP, SUB1, INVERSE, IMPLIES, REMAINDER, and PRIME1, to six new
formulas:

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

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

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

    However this further simplifies, applying EQUAL-TIMES-0 and TIMES-EQUAL-1,
    and expanding the definitions of LESSP, REMAINDER, and EQUAL, to:

          T.

  Case 6.1.
          (IMPLIES (AND (NUMBERP Z)
                        (EQUAL (LESSP Z P) (NOT (ZEROP P)))
                        (NUMBERP V)
                        (EQUAL Z 0)
                        (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (EQUAL P 1))
                        (PRIME1 P (SUB1 P))
                        (EQUAL 1
                               (REMAINDER (TIMES (PLUS Z (TIMES P V)) X)
                                          P))
                        (NOT (EQUAL P 2)))
                   (EQUAL (REMAINDER (EXP (PLUS Z (TIMES P V))
                                          (SUB1 (SUB1 P)))
                                     P)
                          (REMAINDER X P))).

    However this further simplifies, rewriting with ASSOCIATIVITY-OF-TIMES and
    REMAINDER-TIMES, and expanding NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS,
    to:

          T.

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

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

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

  However this again simplifies, unfolding the functions EQUAL, NUMBERP, SUB1,
  and PRIME1, to the conjecture:

        (IMPLIES (AND (EQUAL (REMAINDER X 2) 1)
                      (EQUAL (REMAINDER M 2) 0))
                 (NOT (EQUAL 1 (REMAINDER (TIMES M X) 2)))).

  Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace X by
  (PLUS Z (TIMES 2 V)) to eliminate (REMAINDER X 2) and (QUOTIENT X 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 constrain the new variables.  This generates four new
  conjectures:

  Case 5.4.
          (IMPLIES (AND (NOT (NUMBERP X))
                        (EQUAL (REMAINDER X 2) 1)
                        (EQUAL (REMAINDER M 2) 0))
                   (NOT (EQUAL 1 (REMAINDER (TIMES M X) 2)))),

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

          T.

  Case 5.3.
          (IMPLIES (AND (EQUAL 2 0)
                        (EQUAL (REMAINDER X 2) 1)
                        (EQUAL (REMAINDER M 2) 0))
                   (NOT (EQUAL 1 (REMAINDER (TIMES M X) 2)))),

    which further simplifies, using linear arithmetic, to:

          T.

  Case 5.2.
          (IMPLIES (AND (NOT (NUMBERP 2))
                        (EQUAL (REMAINDER X 2) 1)
                        (EQUAL (REMAINDER M 2) 0))
                   (NOT (EQUAL 1 (REMAINDER (TIMES M X) 2)))),

    which further simplifies, clearly, to:

          T.

  Case 5.1.
          (IMPLIES (AND (NUMBERP Z)
                        (EQUAL (LESSP Z 2) (NOT (ZEROP 2)))
                        (NUMBERP V)
                        (NOT (EQUAL 2 0))
                        (EQUAL Z 1)
                        (EQUAL (REMAINDER M 2) 0))
                   (NOT (EQUAL 1
                               (REMAINDER (TIMES M (PLUS Z (TIMES 2 V)))
                                          2)))).

    However this further simplifies, rewriting with the lemmas TIMES-2,
    TIMES-1, COMMUTATIVITY-OF-TIMES, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS,
    COMMUTATIVITY-OF-PLUS, and COMMUTATIVITY2-OF-PLUS, and expanding the
    definitions of NUMBERP, LESSP, ZEROP, NOT, and EQUAL, to two new
    conjectures:

    Case 5.1.2.
            (IMPLIES (AND (NUMBERP V)
                          (EQUAL (REMAINDER M 2) 0)
                          (NOT (NUMBERP M)))
                     (NOT (EQUAL 1
                                 (REMAINDER (PLUS (TIMES M V) (TIMES M V) 0)
                                            2)))),

      which finally simplifies, appealing to the lemmas COMMUTATIVITY-OF-PLUS,
      EQUAL-TIMES-0, and TIMES-EQUAL-1, and unfolding LESSP, NUMBERP, EQUAL,
      REMAINDER, and PLUS, to:

            T.

    Case 5.1.1.
            (IMPLIES (AND (NUMBERP V)
                          (EQUAL (REMAINDER M 2) 0)
                          (NUMBERP M))
                     (NOT (EQUAL 1
                                 (REMAINDER (PLUS (TIMES M V) (TIMES M V) M)
                                            2)))),

      which finally simplifies, rewriting with COMMUTATIVITY-OF-PLUS,
      COMMUTATIVITY2-OF-PLUS, DIVIDES-PLUS-REWRITE1, and PRIME-KEY-REWRITE,
      and opening up PRIME and EQUAL, to:

            T.

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

  This again simplifies, rewriting with TIMES-MOD-1, to:

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

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

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

    However this further simplifies, applying the lemmas TIMES-ZERO2 and
    REMAINDER-0-CROCK, and unfolding the function EQUAL, to:

          T.

  Case 4.1.
          (IMPLIES (AND (NUMBERP Z)
                        (EQUAL (LESSP Z P) (NOT (ZEROP P)))
                        (NUMBERP V)
                        (NOT (EQUAL P 2))
                        (EQUAL (REMAINDER (TIMES M (EXP M (SUB1 (SUB1 P))))
                                          P)
                               1)
                        (EQUAL (REMAINDER M P) 0)
                        (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (EQUAL P 1))
                        (PRIME1 P (SUB1 P))
                        (EQUAL 1
                               (REMAINDER (TIMES M (PLUS Z (TIMES P V)))
                                          P)))
                   (EQUAL (REMAINDER (EXP M (SUB1 (SUB1 P))) P)
                          Z)),

    which further simplifies, applying DISTRIBUTIVITY-OF-TIMES-OVER-PLUS,
    REMAINDER-TIMES-1, PRIME-KEY-REWRITE, and DIVIDES-PLUS-REWRITE1, and
    unfolding the functions ZEROP, NOT, EQUAL, and PRIME, to:

          T.

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

  But this again simplifies, rewriting with the lemma TIMES-MOD-1, to:

        T.

Case 2. (IMPLIES (AND (EQUAL P 2)
                      (EQUAL (REMAINDER (TIMES M (REMAINDER M 2))
                                        P)
                             1)
                      (EQUAL (REMAINDER M 2) 0)
                      (EQUAL 1 (REMAINDER (TIMES M X) 2)))
                 (EQUAL 0 (REMAINDER X 2))),

  which again simplifies, using linear arithmetic, applying
  LESSP-REMAINDER-DIVISOR, and unfolding the function EQUAL, to the new
  conjecture:

        (IMPLIES (AND (EQUAL (REMAINDER X 2) 1)
                      (EQUAL (REMAINDER (TIMES M 0) 2) 1)
                      (EQUAL (REMAINDER M 2) 0)
                      (EQUAL 1 (REMAINDER (TIMES M X) 2)))
                 (EQUAL 0 1)),

  which again simplifies, applying COMMUTATIVITY-OF-TIMES, TIMES-IDENTITY, and
  TIMES-EQUAL-1, and opening up LESSP, NUMBERP, EQUAL, and REMAINDER, to:

        T.

Case 1. (IMPLIES (AND (EQUAL P 2)
                      (EQUAL (REMAINDER (TIMES M (REMAINDER M 2))
                                        P)
                             1)
                      (NOT (EQUAL (REMAINDER X 2)
                                  (REMAINDER M 2)))
                      (NOT (EQUAL 1 (REMAINDER (TIMES M M) 2))))
                 (NOT (EQUAL 1 (REMAINDER (TIMES M X) 2)))).

  But this again simplifies, appealing to the lemma TIMES-MOD-1, to:

        T.

Q.E.D.


[ 0.0 1.4 0.0 ]

INVERSE-IS-UNIQUE


(PROVE-LEMMA S-P-I-I-LEMMA1
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP N))
                           (NOT (EQUAL N 1)))
                      (EQUAL (TIMES (SUB1 N) (SUB1 N))
                             (PLUS 1 (TIMES N (SUB1 (SUB1 N)))))))

WARNING:  the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the newly proposed S-P-I-I-LEMMA1 could!


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

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

which simplifies, expanding SUB1, NUMBERP, EQUAL, and PLUS, to the formula:

      (IMPLIES (AND (NOT (EQUAL N 0))
                    (NUMBERP N)
                    (NOT (EQUAL N 1)))
               (EQUAL (TIMES (SUB1 N) (SUB1 N))
                      (ADD1 (TIMES N (SUB1 (SUB1 N)))))).

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

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

  which further simplifies, trivially, to:

        T.

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

  But this further simplifies, applying ADD1-EQUAL, TIMES-ADD1,
  COMMUTATIVITY-OF-TIMES, SUB1-ADD1, PLUS-ADD1, and COMMUTATIVITY2-OF-PLUS,
  and unfolding NUMBERP and PLUS, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

S-P-I-I-LEMMA1


(PROVE-LEMMA S-P-I-I-LEMMA2
             (REWRITE)
             (IMPLIES (AND (NOT (ZEROP N))
                           (NOT (EQUAL N 1)))
                      (EQUAL (REMAINDER (TIMES (SUB1 N) (SUB1 N))
                                        N)
                             1))
             ((USE (S-P-I-I-LEMMA1)
                   (REMAINDER-PLUS-TIMES-2 (J N)
                                           (X 1)
                                           (I (SUB1 (SUB1 N)))))
              (DISABLE S-P-I-I-LEMMA1 REMAINDER-PLUS-TIMES-2)))

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

      (IMPLIES (AND (IMPLIES (AND (NOT (ZEROP N))
                                  (NOT (EQUAL N 1)))
                             (EQUAL (TIMES (SUB1 N) (SUB1 N))
                                    (PLUS 1 (TIMES N (SUB1 (SUB1 N))))))
                    (EQUAL (REMAINDER (PLUS 1 (TIMES N (SUB1 (SUB1 N))))
                                      N)
                           (REMAINDER 1 N))
                    (NOT (EQUAL N 0))
                    (NUMBERP N)
                    (NOT (EQUAL N 1)))
               (EQUAL (REMAINDER (TIMES (SUB1 N) (SUB1 N))
                                 N)
                      1)),

which simplifies, rewriting with REMAINDER-OF-1, and unfolding the definitions
of ZEROP, NOT, AND, SUB1, NUMBERP, EQUAL, PLUS, and IMPLIES, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

S-P-I-I-LEMMA2


(PROVE-LEMMA SUB1-P-IS-INVOLUTION
             (REWRITE)
             (IMPLIES (PRIME P)
                      (EQUAL (INVERSE (SUB1 P) P) (SUB1 P)))
             ((USE (INVERSE-IS-UNIQUE (M (SUB1 P))
                                      (X (SUB1 P))))
              (DISABLE INVERSE)))

WARNING:  Note that the rewrite rule SUB1-P-IS-INVOLUTION will be stored so as
to apply only to terms with the nonrecursive function symbol INVERSE.


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

      (IMPLIES (AND (IMPLIES (AND (PRIME P)
                                  (EQUAL 1
                                         (REMAINDER (TIMES (SUB1 P) (SUB1 P))
                                                    P)))
                             (EQUAL (INVERSE (SUB1 P) P)
                                    (REMAINDER (SUB1 P) P)))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P)))
               (EQUAL (INVERSE (SUB1 P) P)
                      (SUB1 P))),

which simplifies, using linear arithmetic, applying S-P-I-I-LEMMA1,
REMAINDER-OF-1, REMAINDER-PLUS-TIMES-2, REMAINDER-0-CROCK, and DIFFERENCE-0,
and unfolding the definitions of PRIME, EQUAL, AND, REMAINDER, and IMPLIES, to
the new goal:

      (IMPLIES (AND (NOT (LESSP (SUB1 P) P))
                    (EQUAL (INVERSE (SUB1 P) P) 0)
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P)))
               (EQUAL 0 (SUB1 P))),

which again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

SUB1-P-IS-INVOLUTION


(PROVE-LEMMA N-O-I-LEMMA1
             (REWRITE)
             (EQUAL (DIFFERENCE (TIMES X X) 1)
                    (TIMES (ADD1 X) (SUB1 X))))

WARNING:  the previously added lemma, DIFFERENCE-1, could be applied whenever
the newly proposed N-O-I-LEMMA1 could!


This conjecture can be simplified, using the abbreviation DIFFERENCE-1, to the
goal:

      (EQUAL (SUB1 (TIMES X X))
             (TIMES (ADD1 X) (SUB1 X))).

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

Case 3. (IMPLIES (EQUAL X 0)
                 (EQUAL (SUB1 (TIMES X X))
                        (TIMES (ADD1 X) (SUB1 X)))),

  which simplifies, expanding TIMES, SUB1, and EQUAL, to:

        T.

Case 2. (IMPLIES (NOT (NUMBERP X))
                 (EQUAL (SUB1 (TIMES X X))
                        (TIMES (ADD1 X) (SUB1 X)))),

  which simplifies, applying TIMES-ZERO2, SUB1-TYPE-RESTRICTION, and
  SUB1-NNUMBERP, and opening up the functions SUB1, TIMES, and EQUAL, to:

        T.

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

  But this simplifies, applying the lemmas TIMES-ADD1, COMMUTATIVITY-OF-TIMES,
  SUB1-ADD1, PLUS-ADD1, and COMMUTATIVITY2-OF-PLUS, and expanding PLUS, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

N-O-I-LEMMA1


(PROVE-LEMMA N-O-I-LEMMA2
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (EQUAL (REMAINDER (DIFFERENCE (TIMES J J) 1)
                                             P)
                                  0))
                      (OR (EQUAL (REMAINDER (ADD1 J) P) 0)
                          (EQUAL (REMAINDER (SUB1 J) P) 0))))

WARNING:  Note that the rewrite rule N-O-I-LEMMA2 will be stored so as to
apply only to terms with the nonrecursive function symbol OR.


This formula can be simplified, using the abbreviations OR, PRIME, AND,
IMPLIES, and N-O-I-LEMMA1, to:

      (IMPLIES (AND (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (EQUAL (REMAINDER (TIMES (ADD1 J) (SUB1 J))
                                      P)
                           0)
                    (NOT (EQUAL (REMAINDER (ADD1 J) P) 0)))
               (EQUAL (REMAINDER (SUB1 J) P) 0)),

which simplifies, rewriting with the lemma PRIME-KEY-REWRITE, and expanding
the function PRIME, to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

N-O-I-LEMMA2


(PROVE-LEMMA N-O-I-LEMMA3
             (REWRITE)
             (IMPLIES (AND (NOT (LESSP A 1))
                           (EQUAL (REMAINDER A P) 1))
                      (EQUAL (REMAINDER (SUB1 A) P) 0))
             ((USE (EQUAL-MODS-TRICK-2 (B 1)))
              (DISABLE N-O-I-LEMMA1)))

This formula simplifies, applying REMAINDER-OF-1 and REMAINDER-WRT-1, and
opening up the definitions of IMPLIES, SUB1, NUMBERP, EQUAL, and LESSP, to the
new conjecture:

      (IMPLIES (AND (EQUAL (REMAINDER (PDIFFERENCE A 1) P)
                           0)
                    (NOT (EQUAL A 0))
                    (NUMBERP A)
                    (EQUAL (REMAINDER A P) 1))
               (EQUAL (REMAINDER (SUB1 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.  We would thus like to prove the following three new formulas:

Case 3. (IMPLIES (AND (EQUAL P 0)
                      (EQUAL (REMAINDER (PDIFFERENCE A 1) P)
                             0)
                      (NOT (EQUAL A 0))
                      (NUMBERP A)
                      (EQUAL (REMAINDER A P) 1))
                 (EQUAL (REMAINDER (SUB1 A) P) 0)).

  This further simplifies, expanding EQUAL, REMAINDER, and SUB1, to:

        T.

Case 2. (IMPLIES (AND (NOT (NUMBERP P))
                      (EQUAL (REMAINDER (PDIFFERENCE A 1) P)
                             0)
                      (NOT (EQUAL A 0))
                      (NUMBERP A)
                      (EQUAL (REMAINDER A P) 1))
                 (EQUAL (REMAINDER (SUB1 A) P) 0)),

  which further simplifies, applying REMAINDER-WRT-12 and REMAINDER-0-CROCK,
  and opening up SUB1 and EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NUMBERP X)
                      (EQUAL (LESSP X P) (NOT (ZEROP P)))
                      (NUMBERP Z)
                      (NUMBERP P)
                      (NOT (EQUAL P 0))
                      (EQUAL (REMAINDER (PDIFFERENCE (PLUS X (TIMES P Z)) 1)
                                        P)
                             0)
                      (NOT (EQUAL (PLUS X (TIMES P Z)) 0))
                      (EQUAL X 1))
                 (EQUAL (REMAINDER (SUB1 (PLUS X (TIMES P Z)))
                                   P)
                        0)).

  This further simplifies, rewriting with the lemmas REMAINDER-PLUS-TIMES-2,
  REMAINDER-OF-1, EQUAL-MODS-TRICK-2, and PLUS-EQUAL-0, and opening up the
  functions NUMBERP, ZEROP, NOT, and EQUAL, to:

        (IMPLIES (AND (LESSP 1 P)
                      (NUMBERP Z)
                      (NUMBERP P)
                      (NOT (EQUAL P 0)))
                 (EQUAL (REMAINDER (SUB1 (PLUS 1 (TIMES P Z)))
                                   P)
                        0)),

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


     So now let us consider:

(IF (IMPLIES (EQUAL (REMAINDER A P)
                    (REMAINDER 1 P))
             (EQUAL (REMAINDER (PDIFFERENCE A 1) P)
                    0))
    (IMPLIES (AND (NOT (LESSP A 1))
                  (EQUAL (REMAINDER A P) 1))
             (EQUAL (REMAINDER (SUB1 A) P) 0))
    T),

which we named *1 above.  We will appeal to induction.  There are three
plausible 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 (ZEROP P) (p A P))
           (IMPLIES (AND (NOT (ZEROP P)) (LESSP A P))
                    (p A P))
           (IMPLIES (AND (NOT (ZEROP P))
                         (NOT (LESSP A P))
                         (p (DIFFERENCE A P) P))
                    (p A P))).
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the
definition of ZEROP inform us that the measure (COUNT A) decreases according
to the well-founded relation LESSP in each induction step of the scheme.  The
above induction scheme produces the following three new formulas:

Case 3. (IMPLIES (ZEROP P)
                 (IF (IMPLIES (EQUAL (REMAINDER A P)
                                     (REMAINDER 1 P))
                              (EQUAL (REMAINDER (PDIFFERENCE A 1) P)
                                     0))
                     (IMPLIES (AND (NOT (LESSP A 1))
                                   (EQUAL (REMAINDER A P) 1))
                              (EQUAL (REMAINDER (SUB1 A) P) 0))
                     T)).

  This simplifies, applying REMAINDER-WRT-12 and REMAINDER-OF-1, and expanding
  the definitions of ZEROP, EQUAL, REMAINDER, IMPLIES, SUB1, NUMBERP, LESSP,
  NOT, and AND, to two new goals:

  Case 3.2.
          (IMPLIES (AND (EQUAL P 0)
                        (NUMBERP A)
                        (EQUAL A 1)
                        (EQUAL (PDIFFERENCE A 1) 0)
                        (NOT (EQUAL A 0)))
                   (EQUAL (SUB1 A) 0)),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 3.1.
          (IMPLIES (AND (NOT (NUMBERP P))
                        (NUMBERP A)
                        (EQUAL A 1)
                        (EQUAL (PDIFFERENCE A 1) 0)
                        (NOT (EQUAL A 0)))
                   (EQUAL (SUB1 A) 0)),

    which again simplifies, using linear arithmetic, to:

          T.

Case 2. (IMPLIES (AND (NOT (ZEROP P)) (LESSP A P))
                 (IF (IMPLIES (EQUAL (REMAINDER A P)
                                     (REMAINDER 1 P))
                              (EQUAL (REMAINDER (PDIFFERENCE A 1) P)
                                     0))
                     (IMPLIES (AND (NOT (LESSP A 1))
                                   (EQUAL (REMAINDER A P) 1))
                              (EQUAL (REMAINDER (SUB1 A) P) 0))
                     T)),

  which simplifies, using linear arithmetic, applying REMAINDER-OF-1,
  REMAINDER-0-CROCK, and DIFFERENCE-0, and expanding the definitions of ZEROP,
  REMAINDER, IMPLIES, SUB1, NUMBERP, EQUAL, LESSP, NOT, and AND, to the
  following three new goals:

  Case 2.3.
          (IMPLIES (AND (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (LESSP A P)
                        (LESSP A 1))
                   (IF (IMPLIES (EQUAL (REMAINDER A P)
                                       (REMAINDER 1 P))
                                (EQUAL (REMAINDER (PDIFFERENCE A 1) P)
                                       0))
                       (IMPLIES (AND (NOT (LESSP A 1))
                                     (EQUAL (REMAINDER A P) 1))
                                (EQUAL (REMAINDER (SUB1 A) P) 0))
                       T)).

    This again simplifies, rewriting with REMAINDER-0-CROCK, REMAINDER-OF-1,
    and SUB1-NNUMBERP, and expanding the functions SUB1, NUMBERP, EQUAL, LESSP,
    PDIFFERENCE, IMPLIES, NOT, AND, and REMAINDER, to:

          T.

  Case 2.2.
          (IMPLIES (AND (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (LESSP A P)
                        (NOT (LESSP A 1))
                        (NUMBERP A)
                        (EQUAL A 1)
                        (EQUAL (REMAINDER (PDIFFERENCE A 1) P)
                               0)
                        (NOT (EQUAL A 0))
                        (LESSP (SUB1 A) P))
                   (EQUAL (SUB1 A) 0)).

    However this again simplifies, using linear arithmetic, to:

          T.

  Case 2.1.
          (IMPLIES (AND (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (LESSP A P)
                        (NOT (LESSP A 1))
                        (EQUAL P 1)
                        (NUMBERP A)
                        (NOT (EQUAL A 0))
                        (EQUAL A 1)
                        (LESSP (SUB1 A) P))
                   (EQUAL (SUB1 A) 0)),

    which again simplifies, clearly, to:

          T.

Case 1. (IMPLIES
           (AND (NOT (ZEROP P))
                (NOT (LESSP A P))
                (IF (IMPLIES (EQUAL (REMAINDER (DIFFERENCE A P) P)
                                    (REMAINDER 1 P))
                             (EQUAL (REMAINDER (PDIFFERENCE (DIFFERENCE A P) 1)
                                               P)
                                    0))
                    (IMPLIES (AND (NOT (LESSP (DIFFERENCE A P) 1))
                                  (EQUAL (REMAINDER (DIFFERENCE A P) P)
                                         1))
                             (EQUAL (REMAINDER (SUB1 (DIFFERENCE A P)) P)
                                    0))
                    T))
           (IF (IMPLIES (EQUAL (REMAINDER A P)
                               (REMAINDER 1 P))
                        (EQUAL (REMAINDER (PDIFFERENCE A 1) P)
                               0))
               (IMPLIES (AND (NOT (LESSP A 1))
                             (EQUAL (REMAINDER A P) 1))
                        (EQUAL (REMAINDER (SUB1 A) P) 0))
               T)).

  This simplifies, applying REMAINDER-OF-1 and EQUAL-DIFFERENCE-0, and
  unfolding the definitions of ZEROP, IMPLIES, SUB1, NUMBERP, EQUAL, LESSP,
  NOT, AND, and REMAINDER, to seven new conjectures:

  Case 1.7.
          (IMPLIES (AND (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (LESSP A P))
                        (NOT (EQUAL P 1))
                        (NOT (EQUAL (REMAINDER (PDIFFERENCE (DIFFERENCE A P) 1)
                                               P)
                                    0))
                        (EQUAL (REMAINDER (DIFFERENCE A P) P)
                               1)
                        (EQUAL (REMAINDER (PDIFFERENCE A 1) P)
                               0)
                        (NOT (EQUAL A 0))
                        (NUMBERP A))
                   (EQUAL (REMAINDER (SUB1 A) P) 0)),

    which again simplifies, applying REMAINDER-OF-1 and EQUAL-MODS-TRICK-2,
    and opening up the definition of EQUAL, to:

          T.

  Case 1.6.
          (IMPLIES (AND (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (LESSP A P))
                        (NOT (LESSP P A))
                        (EQUAL P 1)
                        (NOT (EQUAL (REMAINDER (DIFFERENCE A P) P)
                                    0))
                        (NOT (EQUAL A 0))
                        (NUMBERP A)
                        (EQUAL (REMAINDER (DIFFERENCE A P) P)
                               1))
                   (EQUAL (REMAINDER (SUB1 A) P) 0)).

    However this again simplifies, using linear arithmetic, to:

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

    However this again simplifies, opening up EQUAL, NUMBERP, LESSP,
    DIFFERENCE, and REMAINDER, to:

          T.

  Case 1.5.
          (IMPLIES (AND (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (LESSP A P))
                        (NOT (LESSP P A))
                        (EQUAL (REMAINDER (DIFFERENCE A P) P)
                               0)
                        (EQUAL (REMAINDER (PDIFFERENCE A 1) P)
                               0)
                        (NOT (EQUAL A 0))
                        (NUMBERP A)
                        (EQUAL (REMAINDER (DIFFERENCE A P) P)
                               1))
                   (EQUAL (REMAINDER (SUB1 A) P) 0)),

    which again simplifies, using linear arithmetic, to:

          T.

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

    which again simplifies, using linear arithmetic, to:

          (IMPLIES (AND (NOT (EQUAL A 0))
                        (NUMBERP A)
                        (NOT (LESSP A A))
                        (NOT (LESSP A A))
                        (NOT (EQUAL A 1))
                        (EQUAL (REMAINDER (DIFFERENCE A A) A)
                               1)
                        (EQUAL (REMAINDER (PDIFFERENCE A 1) A)
                               0)
                        (NOT (EQUAL A 0))
                        (NUMBERP A))
                   (EQUAL (REMAINDER (SUB1 A) A) 0)).

    But this again simplifies, using linear arithmetic, applying the lemmas
    DIFFERENCE-0 and REMAINDER-0-CROCK, and unfolding the definitions of LESSP
    and EQUAL, to:

          T.

  Case 1.3.
          (IMPLIES (AND (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (LESSP A P))
                        (EQUAL (REMAINDER (SUB1 (DIFFERENCE A P)) P)
                               0)
                        (EQUAL P 1)
                        (NOT (EQUAL (REMAINDER (DIFFERENCE A P) P)
                                    0))
                        (NOT (EQUAL A 0))
                        (NUMBERP A)
                        (EQUAL (REMAINDER (DIFFERENCE A P) P)
                               1))
                   (EQUAL (REMAINDER (SUB1 A) P) 0)),

    which again simplifies, appealing to the lemmas DIFFERENCE-1 and
    REMAINDER-WRT-1, and opening up the definitions of EQUAL, NUMBERP, SUB1,
    and LESSP, to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (LESSP A P))
                        (EQUAL (REMAINDER (SUB1 (DIFFERENCE A P)) P)
                               0)
                        (EQUAL (REMAINDER (DIFFERENCE A P) P)
                               0)
                        (EQUAL (REMAINDER (PDIFFERENCE A 1) P)
                               0)
                        (NOT (EQUAL A 0))
                        (NUMBERP A)
                        (EQUAL (REMAINDER (DIFFERENCE A P) P)
                               1))
                   (EQUAL (REMAINDER (SUB1 A) P) 0)),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (LESSP A P))
                        (EQUAL (REMAINDER (SUB1 (DIFFERENCE A P)) P)
                               0)
                        (NOT (EQUAL P 1))
                        (EQUAL (REMAINDER (DIFFERENCE A P) P)
                               1)
                        (EQUAL (REMAINDER (PDIFFERENCE A 1) P)
                               0)
                        (NOT (EQUAL A 0))
                        (NUMBERP A))
                   (EQUAL (REMAINDER (SUB1 A) P) 0)),

    which again simplifies, appealing to the lemmas REMAINDER-OF-1 and
    EQUAL-MODS-TRICK-2, and unfolding EQUAL and REMAINDER, to:

          (IMPLIES (AND (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (LESSP A P))
                        (EQUAL (REMAINDER (SUB1 (DIFFERENCE A P)) P)
                               0)
                        (NOT (EQUAL P 1))
                        (EQUAL (REMAINDER (DIFFERENCE A P) P)
                               1)
                        (NOT (EQUAL A 0))
                        (NUMBERP A))
                   (EQUAL (REMAINDER (SUB1 A) P) 0)).

    Appealing to the lemmas DIFFERENCE-ELIM, SUB1-ELIM, and
    REMAINDER-QUOTIENT-ELIM, we now replace A by (PLUS P X) to eliminate
    (DIFFERENCE A P), X by (ADD1 Z) to eliminate (SUB1 X), Z by
    (PLUS X (TIMES P V)) to eliminate (REMAINDER Z P) and (QUOTIENT Z P), and
    X by (PLUS Z (TIMES P V)) to eliminate (REMAINDER X P) and (QUOTIENT X P).
    We employ the type restriction lemma noted when DIFFERENCE was introduced,
    the type restriction lemma noted when SUB1 was introduced,
    LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was
    introduced, and the type restriction lemma noted when QUOTIENT was
    introduced to constrain the new variables.  This generates two new
    conjectures:

    Case 1.1.2.
            (IMPLIES (AND (NUMBERP Z)
                          (EQUAL (LESSP Z P) (NOT (ZEROP P)))
                          (NUMBERP V)
                          (EQUAL (PLUS Z (TIMES P V)) 0)
                          (NOT (EQUAL P 0))
                          (NUMBERP P)
                          (NOT (LESSP (PLUS P Z (TIMES P V)) P))
                          (EQUAL (REMAINDER (SUB1 (PLUS Z (TIMES P V)))
                                            P)
                                 0)
                          (NOT (EQUAL P 1))
                          (EQUAL Z 1)
                          (NOT (EQUAL (PLUS P Z (TIMES P V)) 0)))
                     (EQUAL (REMAINDER (SUB1 (PLUS P Z (TIMES P V)))
                                       P)
                            0)),

      which further simplifies, using linear arithmetic, to:

            T.

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

      which further simplifies, applying PLUS-ADD1, SUB1-ADD1, REMAINDER-X-X,
      and REMAINDER-PLUS-TIMES-2, and unfolding NUMBERP, EQUAL, LESSP, ZEROP,
      NOT, and PLUS, to:

            T.


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


[ 0.0 0.6 0.0 ]

N-O-I-LEMMA3


(PROVE-LEMMA N-O-I-LEMMA4
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (NOT (EQUAL (REMAINDER J P) 0))
                           (EQUAL (INVERSE J P) J))
                      (OR (EQUAL (REMAINDER (ADD1 J) P) 0)
                          (EQUAL (REMAINDER (SUB1 J) P) 0)))
             ((USE (INVERSE-INVERTS) (N-O-I-LEMMA2))
              (DISABLE INVERSE N-O-I-LEMMA1)))

WARNING:  Note that the rewrite rule N-O-I-LEMMA4 will be stored so as to
apply only to terms with the nonrecursive function symbol OR.


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

      (IMPLIES (AND (IMPLIES (AND (PRIME P)
                                  (NOT (EQUAL (REMAINDER J P) 0)))
                             (EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
                                    1))
                    (IMPLIES (AND (PRIME P)
                                  (EQUAL (REMAINDER (SUB1 (TIMES J J)) P)
                                         0))
                             (OR (EQUAL (REMAINDER (ADD1 J) P) 0)
                                 (EQUAL (REMAINDER (SUB1 J) P) 0)))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (NOT (EQUAL (REMAINDER J P) 0))
                    (EQUAL (INVERSE J P) J)
                    (NOT (EQUAL (REMAINDER (ADD1 J) P) 0)))
               (EQUAL (REMAINDER (SUB1 J) P) 0)).

This simplifies, rewriting with the lemma INVERSE-IS-UNIQUE, and unfolding the
definitions of PRIME, NOT, AND, IMPLIES, and OR, to:

      (IMPLIES (AND (EQUAL (REMAINDER (TIMES J J) P) 1)
                    (NOT (EQUAL (REMAINDER (SUB1 (TIMES J J)) P)
                                0))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (NOT (EQUAL (REMAINDER J P) 0))
                    (EQUAL (REMAINDER J P) J)
                    (NOT (EQUAL (REMAINDER (ADD1 J) P) 0)))
               (EQUAL (REMAINDER (SUB1 J) P) 0)),

which again simplifies, using linear arithmetic, applying LESSP-TIMES-2 and
N-O-I-LEMMA3, and unfolding the function EQUAL, to:

      T.

Q.E.D.


[ 0.0 0.3 0.0 ]

N-O-I-LEMMA4


(PROVE-LEMMA NO-OTHER-INVOLUTIONS
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (LESSP J (SUB1 P))
                           (LESSP 1 J))
                      (NOT (EQUAL (INVERSE J P) J)))
             ((USE (N-O-I-LEMMA4))
              (DISABLE INVERSE)))

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

      (IMPLIES (AND (IMPLIES (AND (PRIME P)
                                  (NOT (EQUAL (REMAINDER J P) 0))
                                  (EQUAL (INVERSE J P) J))
                             (OR (EQUAL (REMAINDER (ADD1 J) P) 0)
                                 (EQUAL (REMAINDER (SUB1 J) P) 0)))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (LESSP J (SUB1 P))
                    (LESSP 1 J))
               (NOT (EQUAL (INVERSE J P) J))),

which simplifies, using linear arithmetic, applying the lemmas
REMAINDER-0-CROCK, DIFFERENCE-0, and SUB1-ADD1, and expanding the definitions
of PRIME, LESSP, REMAINDER, NOT, AND, OR, IMPLIES, EQUAL, SUB1, and NUMBERP,
to two new conjectures:

Case 2. (IMPLIES (AND (NOT (EQUAL J 0))
                      (NOT (LESSP (SUB1 J) (SUB1 P)))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP J (SUB1 P))
                      (NOT (EQUAL (SUB1 J) 0)))
                 (NOT (EQUAL (INVERSE J P) J))),

  which again simplifies, using linear arithmetic, to:

        (IMPLIES (AND (LESSP J 1)
                      (NOT (EQUAL J 0))
                      (NOT (LESSP (SUB1 J) (SUB1 P)))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP J (SUB1 P))
                      (NOT (EQUAL (SUB1 J) 0)))
                 (NOT (EQUAL (INVERSE J P) J))).

  But this again simplifies, using linear arithmetic, to:

        (IMPLIES (AND (NOT (NUMBERP J))
                      (LESSP J 1)
                      (NOT (EQUAL J 0))
                      (NOT (LESSP (SUB1 J) (SUB1 P)))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP J (SUB1 P))
                      (NOT (EQUAL (SUB1 J) 0)))
                 (NOT (EQUAL (INVERSE J P) J))).

  This again simplifies, obviously, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL J 0))
                      (NOT (LESSP (SUB1 J) P))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP J (SUB1 P))
                      (NOT (EQUAL (SUB1 J) 0)))
                 (NOT (EQUAL (INVERSE J P) J))).

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

        (IMPLIES (AND (LESSP J 1)
                      (NOT (EQUAL J 0))
                      (NOT (LESSP (SUB1 J) P))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP J (SUB1 P))
                      (NOT (EQUAL (SUB1 J) 0)))
                 (NOT (EQUAL (INVERSE J P) J))).

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

        (IMPLIES (AND (NOT (NUMBERP J))
                      (LESSP J 1)
                      (NOT (EQUAL J 0))
                      (NOT (LESSP (SUB1 J) P))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP J (SUB1 P))
                      (NOT (EQUAL (SUB1 J) 0)))
                 (NOT (EQUAL (INVERSE J P) J))).

  This again simplifies, obviously, to:

        T.

Q.E.D.


[ 0.0 0.0 0.0 ]

NO-OTHER-INVOLUTIONS


(PROVE-LEMMA I-O-I-LEMMA NIL
             (EQUAL (SUB1 (TIMES (DIFFERENCE P 2)
                                 (DIFFERENCE P 2)))
                    (TIMES (DIFFERENCE P 3) (SUB1 P))))

This formula simplifies, rewriting with DIFFERENCE-1 and
COMMUTATIVITY-OF-TIMES, and opening up the definitions of SUB1, NUMBERP, EQUAL,
and DIFFERENCE, to the following four new formulas:

Case 4. (IMPLIES (AND (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL (SUB1 P) 0)))
                 (EQUAL (SUB1 (TIMES (SUB1 (SUB1 P))
                                     (SUB1 (SUB1 P))))
                        (TIMES (SUB1 P)
                               (SUB1 (SUB1 (SUB1 P)))))).

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

  Case 4.2.
          (IMPLIES (AND (EQUAL Z 0)
                        (NUMBERP Z)
                        (NOT (EQUAL (ADD1 (ADD1 Z)) 0))
                        (NOT (EQUAL (ADD1 Z) 0)))
                   (EQUAL (SUB1 (TIMES Z Z))
                          (TIMES (ADD1 Z) (SUB1 Z)))),

    which further simplifies, opening up the functions NUMBERP, EQUAL, TIMES,
    and SUB1, to:

          T.

  Case 4.1.
          (IMPLIES (AND (NUMBERP X)
                        (NOT (EQUAL (ADD1 X) 0))
                        (NOT (EQUAL (ADD1 (ADD1 (ADD1 X))) 0))
                        (NOT (EQUAL (ADD1 (ADD1 X)) 0)))
                   (EQUAL (SUB1 (TIMES (ADD1 X) (ADD1 X)))
                          (TIMES (ADD1 (ADD1 X)) X))),

    which further simplifies, applying the lemmas TIMES-ADD1,
    COMMUTATIVITY-OF-TIMES, SUB1-ADD1, PLUS-ADD1, and COMMUTATIVITY2-OF-PLUS,
    and unfolding the function PLUS, to:

          T.

Case 3. (IMPLIES (AND (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (EQUAL (SUB1 P) 0))
                 (EQUAL (SUB1 (TIMES (SUB1 (SUB1 P))
                                     (SUB1 (SUB1 P))))
                        (TIMES (SUB1 P) 0))),

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

        T.

Case 2. (IMPLIES (EQUAL P 0)
                 (EQUAL (SUB1 (TIMES 0 0))
                        (TIMES (SUB1 P) 0))),

  which again simplifies, opening up TIMES, SUB1, and EQUAL, to:

        T.

Case 1. (IMPLIES (NOT (NUMBERP P))
                 (EQUAL (SUB1 (TIMES 0 0))
                        (TIMES (SUB1 P) 0))),

  which again simplifies, rewriting with the lemma SUB1-NNUMBERP, and
  expanding the functions TIMES, SUB1, and EQUAL, to:

        T.

Q.E.D.


[ 0.0 0.1 0.0 ]

I-O-I-LEMMA


(PROVE-LEMMA INVERSE-OF-INVERSE
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (NOT (EQUAL (REMAINDER J P) 0)))
                      (EQUAL (INVERSE (INVERSE J P) P)
                             (REMAINDER J P)))
             ((USE (I-O-I-LEMMA)
                   (EXP-MOD-IS-1 (M J)
                                 (J (SUB1 P))
                                 (I (DIFFERENCE P 3))))))

WARNING:  Note that the rewrite rule INVERSE-OF-INVERSE will be stored so as
to apply only to terms with the nonrecursive function symbol INVERSE.


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

      (IMPLIES
        (AND (EQUAL (SUB1 (TIMES (DIFFERENCE P 2)
                                 (DIFFERENCE P 2)))
                    (TIMES (DIFFERENCE P 3) (SUB1 P)))
             (IMPLIES (EQUAL (REMAINDER (EXP J (SUB1 P)) P)
                             1)
                      (EQUAL (REMAINDER (EXP J
                                             (TIMES (DIFFERENCE P 3) (SUB1 P)))
                                        P)
                             1))
             (NOT (EQUAL P 0))
             (NUMBERP P)
             (NOT (EQUAL P 1))
             (PRIME1 P (SUB1 P))
             (NOT (EQUAL (REMAINDER J P) 0)))
        (EQUAL (INVERSE (INVERSE J P) P)
               (REMAINDER J P))).

This simplifies, rewriting with the lemmas DIFFERENCE-1,
COMMUTATIVITY-OF-TIMES, FERMAT-THM, EXP-BY-0, REMAINDER-OF-1, and DIFFERENCE-0,
and unfolding the functions SUB1, NUMBERP, EQUAL, DIFFERENCE, PRIME, IMPLIES,
INVERSE, LESSP, TIMES, and PRIME1, to the following two new goals:

Case 2. (IMPLIES (AND (NOT (EQUAL (SUB1 P) 0))
                      (EQUAL (SUB1 (TIMES (SUB1 (SUB1 P))
                                          (SUB1 (SUB1 P))))
                             (TIMES (SUB1 P)
                                    (SUB1 (SUB1 (SUB1 P)))))
                      (EQUAL (REMAINDER (EXP J
                                             (TIMES (SUB1 P)
                                                    (SUB1 (SUB1 (SUB1 P)))))
                                        P)
                             1)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (EQUAL (REMAINDER J P) 0))
                      (NOT (EQUAL P 2)))
                 (EQUAL (INVERSE (REMAINDER (EXP J (SUB1 (SUB1 P))) P)
                                 P)
                        (REMAINDER J P))).

  But this again simplifies, using linear arithmetic, rewriting with
  LESSP-REMAINDER-DIVISOR, S-P-I-I-LEMMA1, REMAINDER-EXP, EXP-EXP, EXP-PLUS,
  EXP-BY-0, TIMES-1, COMMUTATIVITY-OF-TIMES, and DIFFERENCE-1, and unfolding
  the definitions of EXP, DIFFERENCE, EQUAL, NUMBERP, SUB1, and INVERSE, to
  the following two new conjectures:

  Case 2.2.
          (IMPLIES
                 (AND (NOT (EQUAL (SUB1 P) 0))
                      (EQUAL (SUB1 (PLUS 1
                                         (TIMES (SUB1 P)
                                                (SUB1 (SUB1 (SUB1 P))))))
                             (TIMES (SUB1 P)
                                    (SUB1 (SUB1 (SUB1 P)))))
                      (EQUAL (REMAINDER (EXP J
                                             (TIMES (SUB1 P)
                                                    (SUB1 (SUB1 (SUB1 P)))))
                                        P)
                             1)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (EQUAL (REMAINDER J P) 0))
                      (NOT (EQUAL P 2))
                      (NOT (NUMBERP J)))
                 (EQUAL (REMAINDER (TIMES 0
                                          (EXP J
                                               (TIMES (SUB1 P)
                                                      (SUB1 (SUB1 (SUB1 P))))))
                                   P)
                        (REMAINDER J P))).

    However this again simplifies, expanding LESSP, REMAINDER, and EQUAL, to:

          T.

  Case 2.1.
          (IMPLIES
                 (AND (NOT (EQUAL (SUB1 P) 0))
                      (EQUAL (SUB1 (PLUS 1
                                         (TIMES (SUB1 P)
                                                (SUB1 (SUB1 (SUB1 P))))))
                             (TIMES (SUB1 P)
                                    (SUB1 (SUB1 (SUB1 P)))))
                      (EQUAL (REMAINDER (EXP J
                                             (TIMES (SUB1 P)
                                                    (SUB1 (SUB1 (SUB1 P)))))
                                        P)
                             1)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (EQUAL (REMAINDER J P) 0))
                      (NOT (EQUAL P 2))
                      (NUMBERP J))
                 (EQUAL (REMAINDER (TIMES J
                                          (EXP J
                                               (TIMES (SUB1 P)
                                                      (SUB1 (SUB1 (SUB1 P))))))
                                   P)
                        (REMAINDER J P))),

    which again simplifies, appealing to the lemma COROLLARY-55, and expanding
    the functions PRIME and EQUAL, to:

          T.

Case 1. (IMPLIES (AND (NOT (EQUAL (SUB1 P) 0))
                      (EQUAL (SUB1 (TIMES (SUB1 (SUB1 P))
                                          (SUB1 (SUB1 P))))
                             (TIMES (SUB1 P)
                                    (SUB1 (SUB1 (SUB1 P)))))
                      (EQUAL (REMAINDER (EXP J
                                             (TIMES (SUB1 P)
                                                    (SUB1 (SUB1 (SUB1 P)))))
                                        P)
                             1)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (EQUAL (REMAINDER J P) 0))
                      (EQUAL P 2))
                 (EQUAL (INVERSE (REMAINDER J 2) P)
                        (REMAINDER J P))),

  which again simplifies, using linear arithmetic and applying
  LESSP-REMAINDER-DIVISOR, to the new conjecture:

        (IMPLIES (AND (EQUAL (REMAINDER J 2) 1)
                      (NOT (EQUAL (SUB1 2) 0))
                      (EQUAL (SUB1 (TIMES (SUB1 (SUB1 2))
                                          (SUB1 (SUB1 2))))
                             (TIMES (SUB1 2)
                                    (SUB1 (SUB1 (SUB1 2)))))
                      (EQUAL (REMAINDER (EXP J
                                             (TIMES (SUB1 2)
                                                    (SUB1 (SUB1 (SUB1 2)))))
                                        2)
                             1)
                      (NOT (EQUAL 2 0))
                      (NUMBERP 2)
                      (NOT (EQUAL 2 1))
                      (PRIME1 2 (SUB1 2))
                      (NOT (EQUAL 1 0)))
                 (EQUAL (INVERSE 1 2) 1)),

  which again simplifies, rewriting with EXP-BY-0, and unfolding SUB1, EQUAL,
  TIMES, REMAINDER, NUMBERP, PRIME1, and INVERSE, to:

        T.

Q.E.D.


[ 0.0 0.5 0.0 ]

INVERSE-OF-INVERSE


(PROVE-LEMMA N-Z-I-LEMMA
             (REWRITE)
             (IMPLIES (AND (ZEROP I) (LESSP 1 P))
                      (EQUAL (INVERSE I P) 0)))

WARNING:  Note that the rewrite rule N-Z-I-LEMMA will be stored so as to apply
only to terms with the nonrecursive function symbol INVERSE.


This simplifies, rewriting with EXP-OF-0 and DIFFERENCE-1, and opening up
ZEROP, DIFFERENCE, EQUAL, NUMBERP, SUB1, REMAINDER, INVERSE, and LESSP, to
seven new conjectures:

Case 7. (IMPLIES (AND (EQUAL I 0)
                      (LESSP 1 P)
                      (NOT (EQUAL P 2))
                      (EQUAL (SUB1 (SUB1 P)) 0))
                 (EQUAL (REMAINDER 1 P) 0)),

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

  Case 7.3.
          (IMPLIES (AND (NOT (NUMBERP P))
                        (LESSP 1 P)
                        (NOT (EQUAL P 2))
                        (EQUAL (SUB1 (SUB1 P)) 0))
                   (EQUAL (REMAINDER 1 P) 0)),

    which again simplifies, opening up the definition of LESSP, to:

          T.

  Case 7.2.
          (IMPLIES (AND (EQUAL (SUB1 P) 0)
                        (LESSP 1 P)
                        (NOT (EQUAL P 2))
                        (EQUAL (SUB1 (SUB1 P)) 0))
                   (EQUAL (REMAINDER 1 P) 0)),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 7.1.
          (IMPLIES (AND (LESSP P 1)
                        (LESSP 1 P)
                        (NOT (EQUAL P 2))
                        (EQUAL (SUB1 (SUB1 P)) 0))
                   (EQUAL (REMAINDER 1 P) 0)),

    which again simplifies, using linear arithmetic, to:

          T.

Case 6. (IMPLIES (AND (EQUAL I 0)
                      (LESSP 1 P)
                      (NOT (EQUAL P 2))
                      (NOT (NUMBERP P)))
                 (EQUAL (REMAINDER 1 P) 0)),

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

        T.

Case 5. (IMPLIES (AND (EQUAL I 0)
                      (LESSP 1 P)
                      (NOT (EQUAL P 2))
                      (EQUAL P 0))
                 (EQUAL (REMAINDER 1 P) 0)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 4. (IMPLIES (AND (EQUAL I 0)
                      (LESSP 1 P)
                      (NOT (EQUAL P 2))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL (SUB1 (SUB1 P)) 0)))
                 (EQUAL (REMAINDER 0 P) 0)),

  which again simplifies, rewriting with the lemma REMAINDER-0-CROCK, and
  opening up the function EQUAL, to:

        T.

Case 3. (IMPLIES (AND (NOT (NUMBERP I))
                      (LESSP 1 P)
                      (NOT (EQUAL P 2))
                      (NOT (NUMBERP P)))
                 (EQUAL (REMAINDER (EXP I 0) P) 0)),

  which again simplifies, opening up the definition of LESSP, to:

        T.

Case 2. (IMPLIES (AND (NOT (NUMBERP I))
                      (LESSP 1 P)
                      (NOT (EQUAL P 2))
                      (EQUAL P 0))
                 (EQUAL (REMAINDER (EXP I 0) P) 0)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (NUMBERP I))
                      (LESSP 1 P)
                      (NOT (EQUAL P 2))
                      (NOT (EQUAL P 0))
                      (NUMBERP P))
                 (EQUAL (REMAINDER (EXP I (SUB1 (SUB1 P))) P)
                        0)).

  Applying the lemma SUB1-ELIM, replace P by (ADD1 X) to eliminate (SUB1 P)
  and X by (ADD1 Z) to eliminate (SUB1 X).  We use the type restriction lemma
  noted when SUB1 was introduced to restrict the new variable.  We thus obtain
  the following two new conjectures:

  Case 1.2.
          (IMPLIES (AND (EQUAL X 0)
                        (NUMBERP X)
                        (NOT (NUMBERP I))
                        (LESSP 1 (ADD1 X))
                        (NOT (EQUAL (ADD1 X) 2))
                        (NOT (EQUAL (ADD1 X) 0)))
                   (EQUAL (REMAINDER (EXP I (SUB1 X)) (ADD1 X))
                          0)).

    But this further simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NUMBERP Z)
                        (NOT (EQUAL (ADD1 Z) 0))
                        (NOT (NUMBERP I))
                        (LESSP 1 (ADD1 (ADD1 Z)))
                        (NOT (EQUAL (ADD1 (ADD1 Z)) 2))
                        (NOT (EQUAL (ADD1 (ADD1 Z)) 0)))
                   (EQUAL (REMAINDER (EXP I Z) (ADD1 (ADD1 Z)))
                          0)),

    which further simplifies, rewriting with SUB1-ADD1 and ADD1-EQUAL, and
    unfolding the definitions of SUB1, NUMBERP, EQUAL, and LESSP, to the new
    conjecture:

          (IMPLIES (AND (NUMBERP Z)
                        (NOT (NUMBERP I))
                        (NOT (EQUAL Z 0)))
                   (EQUAL (REMAINDER (EXP I Z) (ADD1 (ADD1 Z)))
                          0)),

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


     So now let us return to:

(IMPLIES (AND (ZEROP I) (LESSP 1 P))
         (EQUAL (INVERSE I P) 0)),

named *1.  Let us appeal to the induction principle.  There is only one
suggested induction.  We will induct according to the following scheme:
      (AND (IMPLIES (OR (EQUAL P 0) (NOT (NUMBERP P)))
                    (p I P))
           (IMPLIES (AND (NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
                         (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
                    (p I P))
           (IMPLIES (AND (NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
                         (NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
                         (p I (SUB1 P)))
                    (p I P))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT establish that the measure (COUNT P) 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 (OR (EQUAL P 0) (NOT (NUMBERP P)))
                      (ZEROP I)
                      (LESSP 1 P))
                 (EQUAL (INVERSE I P) 0)),

  which simplifies, unfolding the definitions of NOT, OR, ZEROP, and LESSP, to:

        T.

Case 3. (IMPLIES (AND (NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
                      (OR (EQUAL 1 0) (NOT (NUMBERP 1)))
                      (ZEROP I)
                      (LESSP 1 P))
                 (EQUAL (INVERSE I P) 0)),

  which simplifies, opening up NOT, OR, EQUAL, and NUMBERP, to:

        T.

Case 2. (IMPLIES (AND (NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
                      (NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
                      (NOT (LESSP 1 (SUB1 P)))
                      (ZEROP I)
                      (LESSP 1 P))
                 (EQUAL (INVERSE I P) 0)),

  which simplifies, using linear arithmetic, to two new formulas:

  Case 2.2.
          (IMPLIES (AND (NOT (NUMBERP P))
                        (NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
                        (NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
                        (NOT (LESSP 1 (SUB1 P)))
                        (ZEROP I)
                        (LESSP 1 P))
                   (EQUAL (INVERSE I P) 0)),

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

          T.

  Case 2.1.
          (IMPLIES (AND (NUMBERP P)
                        (NOT (OR (EQUAL 2 0) (NOT (NUMBERP 2))))
                        (NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
                        (NOT (LESSP 1 (SUB1 2)))
                        (ZEROP I)
                        (LESSP 1 2))
                   (EQUAL (INVERSE I 2) 0)),

    which again simplifies, unfolding the definitions of EQUAL, NUMBERP, NOT,
    OR, SUB1, LESSP, ZEROP, INVERSE, and REMAINDER, to:

          T.

Case 1. (IMPLIES (AND (NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
                      (NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
                      (EQUAL (INVERSE I (SUB1 P)) 0)
                      (ZEROP I)
                      (LESSP 1 P))
                 (EQUAL (INVERSE I P) 0)),

  which simplifies, rewriting with DIFFERENCE-1, EXP-OF-0, REMAINDER-0-CROCK,
  EXP-BY-0, TIMES-1, and COMMUTATIVITY-OF-TIMES, and expanding the functions
  NOT, OR, EQUAL, NUMBERP, DIFFERENCE, SUB1, INVERSE, ZEROP, LESSP, REMAINDER,
  and EXP, to the following three new conjectures:

  Case 1.3.
          (IMPLIES (AND (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (EQUAL (SUB1 P) 2))
                        (NOT (EQUAL (SUB1 P) 0))
                        (EQUAL (REMAINDER (EXP I (SUB1 (SUB1 (SUB1 P))))
                                          (SUB1 P))
                               0)
                        (EQUAL I 0)
                        (NOT (EQUAL P 2))
                        (EQUAL (SUB1 (SUB1 P)) 0))
                   (EQUAL (REMAINDER 1 P) 0)).

    However this again simplifies, using linear arithmetic, to:

          T.

  Case 1.2.
          (IMPLIES (AND (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (EQUAL (SUB1 P) 2))
                        (NOT (EQUAL (SUB1 P) 0))
                        (EQUAL (REMAINDER (EXP I (SUB1 (SUB1 (SUB1 P))))
                                          (SUB1 P))
                               0)
                        (EQUAL I 0)
                        (NOT (EQUAL P 2))
                        (NOT (EQUAL (SUB1 (SUB1 P)) 0)))
                   (EQUAL (REMAINDER 0 P) 0)),

    which again simplifies, applying EXP-OF-0 and REMAINDER-0-CROCK, and
    expanding EQUAL, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (EQUAL (SUB1 P) 2))
                        (NOT (EQUAL (SUB1 P) 0))
                        (EQUAL (REMAINDER (EXP I (SUB1 (SUB1 (SUB1 P))))
                                          (SUB1 P))
                               0)
                        (NOT (NUMBERP I))
                        (NOT (EQUAL P 2)))
                   (EQUAL (REMAINDER (EXP I (SUB1 (SUB1 P))) P)
                          0)).

    However this again simplifies, opening up the definition of EXP, to two
    new conjectures:

    Case 1.1.2.
            (IMPLIES (AND (NOT (EQUAL P 0))
                          (NUMBERP P)
                          (NOT (EQUAL (SUB1 P) 2))
                          (NOT (EQUAL (SUB1 P) 0))
                          (EQUAL (REMAINDER (EXP I (SUB1 (SUB1 (SUB1 P))))
                                            (SUB1 P))
                                 0)
                          (NOT (NUMBERP I))
                          (NOT (EQUAL P 2))
                          (NOT (EQUAL (SUB1 (SUB1 P)) 0)))
                     (EQUAL (REMAINDER (TIMES I
                                              (EXP I (SUB1 (SUB1 (SUB1 P)))))
                                       P)
                            0)),

      which again simplifies, rewriting with EQUAL-TIMES-0, and unfolding
      LESSP and REMAINDER, to:

            T.

    Case 1.1.1.
            (IMPLIES (AND (NOT (EQUAL P 0))
                          (NUMBERP P)
                          (NOT (EQUAL (SUB1 P) 2))
                          (NOT (EQUAL (SUB1 P) 0))
                          (EQUAL (REMAINDER (EXP I (SUB1 (SUB1 (SUB1 P))))
                                            (SUB1 P))
                                 0)
                          (NOT (NUMBERP I))
                          (NOT (EQUAL P 2))
                          (EQUAL (SUB1 (SUB1 P)) 0))
                     (EQUAL (REMAINDER 1 P) 0)).

      But this again simplifies, using linear arithmetic, to:

            T.


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


[ 0.0 0.3 0.0 ]

N-Z-I-LEMMA


(PROVE-LEMMA NON-ZEROP-INVERSE
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (NOT (EQUAL (REMAINDER J P) 0)))
                      (NOT (ZEROP (INVERSE J P))))
             ((USE (N-Z-I-LEMMA (I (INVERSE J P)))
                   (INVERSE-OF-INVERSE))
              (DISABLE INVERSE)))

WARNING:  Note that the rewrite rule NON-ZEROP-INVERSE will be stored so as to
apply only to terms with the nonrecursive function symbol ZEROP.


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

      (IMPLIES (AND (IMPLIES (AND (ZEROP (INVERSE J P))
                                  (LESSP 1 P))
                             (EQUAL (INVERSE (INVERSE J P) P) 0))
                    (IMPLIES (AND (PRIME P)
                                  (NOT (EQUAL (REMAINDER J P) 0)))
                             (EQUAL (INVERSE (INVERSE J P) P)
                                    (REMAINDER J P)))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (NOT (EQUAL (REMAINDER J P) 0)))
               (NOT (ZEROP (INVERSE J P)))),

which simplifies, using linear arithmetic, rewriting with the lemmas
LESSP-REMAINDER-DIVISOR and N-Z-I-LEMMA, and opening up the functions ZEROP,
SUB1, NUMBERP, EQUAL, LESSP, AND, IMPLIES, PRIME, and NOT, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

NON-ZEROP-INVERSE


(PROVE-LEMMA B-I-LEMMA2
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (NOT (EQUAL (REMAINDER J P) 0))
                           (EQUAL (INVERSE J P) (SUB1 P)))
                      (EQUAL (REMAINDER J P) (SUB1 P)))
             ((USE (INVERSE-OF-INVERSE))
              (DISABLE INVERSE)))

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

      (IMPLIES (AND (IMPLIES (AND (PRIME P)
                                  (NOT (EQUAL (REMAINDER J P) 0)))
                             (EQUAL (INVERSE (INVERSE J P) P)
                                    (REMAINDER J P)))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (NOT (EQUAL (REMAINDER J P) 0))
                    (EQUAL (INVERSE J P) (SUB1 P)))
               (EQUAL (REMAINDER J P) (SUB1 P))),

which simplifies, applying SUB1-P-IS-INVOLUTION, and expanding the functions
PRIME, NOT, AND, and IMPLIES, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

B-I-LEMMA2


(PROVE-LEMMA B-I-LEMMA1 NIL
             (IMPLIES (LESSP 1 P)
                      (LEQ (INVERSE J P) (SUB1 P))))

This simplifies, appealing to the lemma DIFFERENCE-1, and opening up the
functions DIFFERENCE, EQUAL, NUMBERP, SUB1, and INVERSE, to four new formulas:

Case 4. (IMPLIES (AND (LESSP 1 P)
                      (NOT (EQUAL P 2))
                      (NOT (NUMBERP P)))
                 (NOT (LESSP (SUB1 P)
                             (REMAINDER (EXP J 0) P)))),

  which again simplifies, opening up the definition of LESSP, to:

        T.

Case 3. (IMPLIES (AND (LESSP 1 P)
                      (NOT (EQUAL P 2))
                      (EQUAL P 0))
                 (NOT (LESSP (SUB1 P)
                             (REMAINDER (EXP J 0) P)))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 2. (IMPLIES (AND (LESSP 1 P)
                      (NOT (EQUAL P 2))
                      (NOT (EQUAL P 0))
                      (NUMBERP P))
                 (NOT (LESSP (SUB1 P)
                             (REMAINDER (EXP J (SUB1 (SUB1 P)))
                                        P)))),

  which again simplifies, using linear arithmetic and applying
  LESSP-REMAINDER-DIVISOR, to:

        T.

Case 1. (IMPLIES (AND (LESSP 1 P) (EQUAL P 2))
                 (NOT (LESSP (SUB1 P) (REMAINDER J 2)))).

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

        T.

Q.E.D.


[ 0.0 0.1 0.0 ]

B-I-LEMMA1


(PROVE-LEMMA BOUNDED-INVERSE
             (REWRITE)
             (IMPLIES (AND (PRIME P) (LESSP J (SUB1 P)))
                      (LESSP (INVERSE J P) (SUB1 P)))
             ((USE (B-I-LEMMA1) (B-I-LEMMA2))
              (DISABLE INVERSE)))

WARNING:  Note that the linear lemma BOUNDED-INVERSE is being stored under the
term (INVERSE J P), which is unusual because INVERSE is a nonrecursive
function symbol.


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


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

      (IMPLIES (AND (IMPLIES (LESSP 1 P)
                             (IF (LESSP (SUB1 P) (INVERSE J P))
                                 F T))
                    (IMPLIES (AND (PRIME P)
                                  (NOT (EQUAL (REMAINDER J P) 0))
                                  (EQUAL (INVERSE J P) (SUB1 P)))
                             (EQUAL (REMAINDER J P) (SUB1 P)))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (LESSP J (SUB1 P)))
               (LESSP (INVERSE J P) (SUB1 P))),

which simplifies, using linear arithmetic, rewriting with the lemmas
REMAINDER-0-CROCK, DIFFERENCE-0, and N-Z-I-LEMMA, and opening up the functions
SUB1, NUMBERP, EQUAL, LESSP, IMPLIES, PRIME1, PRIME, REMAINDER, NOT, AND, and
ZEROP, to three new conjectures:

Case 3. (IMPLIES (AND (NOT (LESSP (SUB1 P) (INVERSE J P)))
                      (NOT (LESSP J P))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP J (SUB1 P)))
                 (LESSP (INVERSE J P) (SUB1 P))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 2. (IMPLIES (AND (NOT (LESSP (SUB1 P) (INVERSE J P)))
                      (NOT (EQUAL (INVERSE J P) (SUB1 P)))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP J (SUB1 P)))
                 (LESSP (INVERSE J P) (SUB1 P))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (LESSP (SUB1 P) (INVERSE J P)))
                      (EQUAL J (SUB1 P))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P J)
                      (LESSP J J))
                 (LESSP (INVERSE J P) J)),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.1 0.0 ]

BOUNDED-INVERSE


(DEFN INVERSE-LIST
      (I P)
      (IF (ZEROP I)
          NIL
          (IF (EQUAL I 1)
              (CONS 1 NIL)
              (IF (MEMBER I (INVERSE-LIST (SUB1 I) P))
                  (INVERSE-LIST (SUB1 I) P)
                  (CONS I
                        (CONS (INVERSE I P)
                              (INVERSE-LIST (SUB1 I) P)))))))

     Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT I) decreases according to the well-founded
relation LESSP in each recursive call.  Hence, INVERSE-LIST is accepted under
the principle of definition.  Note that:
      (OR (LITATOM (INVERSE-LIST I P))
          (LISTP (INVERSE-LIST I P)))
is a theorem.




[ 0.0 0.0 0.0 ]

INVERSE-LIST


(PROVE-LEMMA ALL-NON-ZEROP-INVERSE-LIST
             (REWRITE)
             (IMPLIES (AND (PRIME P) (LESSP I (SUB1 P)))
                      (ALL-NON-ZEROP (INVERSE-LIST I P)))
             ((USE (NON-ZEROP-INVERSE (J I)))
              (INDUCT (INVERSE-LIST I P))
              (DISABLE INVERSE)))

This simplifies, applying SUB1-NNUMBERP, and opening up the definitions of
PRIME, NOT, AND, ZEROP, IMPLIES, SUB1, EQUAL, LESSP, INVERSE-LIST, and OR, to
the following 12 new formulas:

Case 12.(IMPLIES (AND (EQUAL (REMAINDER I P) 0)
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (MEMBER I (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (LESSP I (SUB1 P)))
                 (ALL-NON-ZEROP (INVERSE-LIST (SUB1 I) P))).

  This again simplifies, using linear arithmetic, to:

        T.

Case 11.(IMPLIES (AND (EQUAL (REMAINDER I P) 0)
                      (NOT (NUMBERP I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P)))
                 (ALL-NON-ZEROP NIL)),

  which again simplifies, expanding the functions LESSP, REMAINDER, EQUAL, and
  ALL-NON-ZEROP, to:

        T.

Case 10.(IMPLIES (AND (EQUAL (REMAINDER I P) 0)
                      (EQUAL I 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P)))
                 (ALL-NON-ZEROP NIL)),

  which again simplifies, rewriting with REMAINDER-0-CROCK, and expanding the
  definitions of EQUAL, LESSP, and ALL-NON-ZEROP, to:

        T.

Case 9. (IMPLIES (AND (EQUAL (REMAINDER I P) 0)
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (EQUAL I 1)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P)))
                 (ALL-NON-ZEROP '(1))).

  However this again simplifies, rewriting with the lemma REMAINDER-OF-1, and
  unfolding EQUAL, to:

        T.

Case 8. (IMPLIES (AND (EQUAL (REMAINDER I P) 0)
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (ALL-NON-ZEROP (INVERSE-LIST (SUB1 I) P))
                      (LESSP I (SUB1 P)))
                 (ALL-NON-ZEROP (CONS I
                                      (CONS (INVERSE I P)
                                            (INVERSE-LIST (SUB1 I) P))))),

  which again simplifies, using linear arithmetic, rewriting with
  REMAINDER-0-CROCK, DIFFERENCE-0, CDR-CONS, and CAR-CONS, and opening up the
  functions LESSP, REMAINDER, and ALL-NON-ZEROP, to the new conjecture:

        (IMPLIES (AND (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (ALL-NON-ZEROP (INVERSE-LIST (SUB1 I) P))
                      (LESSP I (SUB1 P)))
                 (NOT (EQUAL (INVERSE I P) 0))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 7. (IMPLIES (AND (EQUAL (REMAINDER I P) 0)
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (LESSP I (SUB1 P)))
                 (ALL-NON-ZEROP (CONS I
                                      (CONS (INVERSE I P)
                                            (INVERSE-LIST (SUB1 I) P))))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 6. (IMPLIES (AND (NOT (EQUAL (INVERSE I P) 0))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (MEMBER I (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (LESSP I (SUB1 P)))
                 (ALL-NON-ZEROP (INVERSE-LIST (SUB1 I) P))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 5. (IMPLIES (AND (NOT (EQUAL (INVERSE I P) 0))
                      (NOT (NUMBERP I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P)))
                 (ALL-NON-ZEROP NIL)),

  which again simplifies, using linear arithmetic, applying N-Z-I-LEMMA and
  BOUNDED-INVERSE, and opening up the definitions of PRIME, ZEROP, and EQUAL,
  to:

        T.

Case 4. (IMPLIES (AND (NOT (EQUAL (INVERSE I P) 0))
                      (EQUAL I 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P)))
                 (ALL-NON-ZEROP NIL)).

  But this again simplifies, using linear arithmetic, rewriting with
  N-Z-I-LEMMA, and unfolding the definitions of ZEROP and EQUAL, to:

        T.

Case 3. (IMPLIES (AND (NOT (EQUAL (INVERSE I P) 0))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (EQUAL I 1)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P)))
                 (ALL-NON-ZEROP '(1))).

  But this again simplifies, expanding the functions EQUAL, NUMBERP, and
  ALL-NON-ZEROP, to:

        T.

Case 2. (IMPLIES (AND (NOT (EQUAL (INVERSE I P) 0))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (ALL-NON-ZEROP (INVERSE-LIST (SUB1 I) P))
                      (LESSP I (SUB1 P)))
                 (ALL-NON-ZEROP (CONS I
                                      (CONS (INVERSE I P)
                                            (INVERSE-LIST (SUB1 I) P))))),

  which again simplifies, applying the lemmas CDR-CONS and CAR-CONS, and
  opening up the definition of ALL-NON-ZEROP, to:

        T.

Case 1. (IMPLIES (AND (NOT (EQUAL (INVERSE I P) 0))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (LESSP I (SUB1 P)))
                 (ALL-NON-ZEROP (CONS I
                                      (CONS (INVERSE I P)
                                            (INVERSE-LIST (SUB1 I) P))))),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.7 0.0 ]

ALL-NON-ZEROP-INVERSE-LIST


(PROVE-LEMMA BOUNDED-INVERSE-LIST
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (LESSP I (SUB1 P))
                           (EQUAL J (DIFFERENCE P 2)))
                      (ALL-LESSEQP (INVERSE-LIST I P) J))
             ((USE (BOUNDED-INVERSE (J I)))
              (INDUCT (INVERSE-LIST I P))
              (DISABLE INVERSE)))

This conjecture simplifies, using linear arithmetic, applying the lemmas
SUB1-NNUMBERP, DIFFERENCE-0, and DIFFERENCE-1, and expanding PRIME, AND,
IMPLIES, ZEROP, NOT, SUB1, EQUAL, LESSP, DIFFERENCE, OR, INVERSE-LIST, and
NUMBERP, to six new formulas:

Case 6. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (MEMBER I (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (LESSP I (SUB1 P))
                      (EQUAL J (SUB1 (SUB1 P))))
                 (ALL-LESSEQP (INVERSE-LIST (SUB1 I) P)
                              J)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 5. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
                      (NOT (NUMBERP I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (EQUAL J (SUB1 (SUB1 P))))
                 (ALL-LESSEQP NIL J)),

  which again simplifies, using linear arithmetic, appealing to the lemmas
  N-Z-I-LEMMA, PIGEON-HOLE-PRINCIPLE-LEMMA-2, and ADD1-SUB1, and expanding
  ZEROP, EQUAL, LESSP, ALL-LESSEQP, MEMBER, and LISTP, to:

        T.

Case 4. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
                      (EQUAL I 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (EQUAL J (SUB1 (SUB1 P))))
                 (ALL-LESSEQP NIL J)),

  which again simplifies, using linear arithmetic, applying N-Z-I-LEMMA,
  PIGEON-HOLE-PRINCIPLE-LEMMA-2, and ADD1-SUB1, and unfolding ZEROP, EQUAL,
  LESSP, ALL-LESSEQP, MEMBER, and LISTP, to:

        T.

Case 3. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (EQUAL I 1)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (EQUAL J (SUB1 (SUB1 P))))
                 (ALL-LESSEQP '(1) J)).

  However this again simplifies, rewriting with the lemmas
  PIGEON-HOLE-PRINCIPLE-LEMMA-2 and ADD1-SUB1, and opening up the definitions
  of EQUAL, NUMBERP, CDR, CAR, LISTP, ALL-LESSEQP, and MEMBER, to:

        (IMPLIES (AND (LESSP (INVERSE 1 P) (SUB1 P))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP 1 (SUB1 P)))
                 (NOT (LESSP (SUB1 (SUB1 P)) 1))).

  However this again simplifies, using linear arithmetic, to:

        T.

Case 2. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (EQUAL J (SUB1 (SUB1 P)))
                      (ALL-LESSEQP (INVERSE-LIST (SUB1 I) P)
                                   J)
                      (LESSP I (SUB1 P)))
                 (ALL-LESSEQP (CONS I
                                    (CONS (INVERSE I P)
                                          (INVERSE-LIST (SUB1 I) P)))
                              J)),

  which again simplifies, applying CDR-CONS and CAR-CONS, and expanding the
  function ALL-LESSEQP, to the following two new goals:

  Case 2.2.
          (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
                        (NOT (EQUAL I 0))
                        (NUMBERP I)
                        (NOT (EQUAL I 1))
                        (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                        (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (EQUAL P 1))
                        (PRIME1 P (SUB1 P))
                        (ALL-LESSEQP (INVERSE-LIST (SUB1 I) P)
                                     (SUB1 (SUB1 P)))
                        (LESSP I (SUB1 P)))
                   (NOT (LESSP (SUB1 (SUB1 P)) I))).

    This again simplifies, using linear arithmetic, to:

          T.

  Case 2.1.
          (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
                        (NOT (EQUAL I 0))
                        (NUMBERP I)
                        (NOT (EQUAL I 1))
                        (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                        (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (EQUAL P 1))
                        (PRIME1 P (SUB1 P))
                        (ALL-LESSEQP (INVERSE-LIST (SUB1 I) P)
                                     (SUB1 (SUB1 P)))
                        (LESSP I (SUB1 P)))
                   (NOT (LESSP (SUB1 (SUB1 P))
                               (INVERSE I P)))),

    which again simplifies, using linear arithmetic, to:

          T.

Case 1. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (LESSP I (SUB1 P))
                      (EQUAL J (SUB1 (SUB1 P))))
                 (ALL-LESSEQP (CONS I
                                    (CONS (INVERSE I P)
                                          (INVERSE-LIST (SUB1 I) P)))
                              J)),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 0.7 0.0 ]

BOUNDED-INVERSE-LIST


(PROVE-LEMMA SUBSETP-POSITIVES
             (REWRITE)
             (SUBSETP (POSITIVES N)
                      (INVERSE-LIST N P)))


     Name the conjecture *1.


     Let us appeal to the induction principle.  Two inductions are suggested
by terms in the conjecture.  However, they merge into one likely candidate
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (ZEROP N) (p N P))
           (IMPLIES (AND (NOT (ZEROP N)) (EQUAL N 1))
                    (p N P))
           (IMPLIES (AND (NOT (ZEROP N))
                         (NOT (EQUAL N 1))
                         (MEMBER N (INVERSE-LIST (SUB1 N) P))
                         (p (SUB1 N) P))
                    (p N P))
           (IMPLIES (AND (NOT (ZEROP N))
                         (NOT (EQUAL N 1))
                         (NOT (MEMBER N (INVERSE-LIST (SUB1 N) P)))
                         (p (SUB1 N) P))
                    (p N 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 induction step of the scheme.  The above induction scheme leads
to four new conjectures:

Case 4. (IMPLIES (ZEROP N)
                 (SUBSETP (POSITIVES N)
                          (INVERSE-LIST N P))),

  which simplifies, expanding ZEROP, POSITIVES, EQUAL, INVERSE-LIST, and
  SUBSETP, to:

        T.

Case 3. (IMPLIES (AND (NOT (ZEROP N)) (EQUAL N 1))
                 (SUBSETP (POSITIVES N)
                          (INVERSE-LIST N P))),

  which simplifies, unfolding the definitions of ZEROP, POSITIVES, NUMBERP,
  EQUAL, INVERSE-LIST, and SUBSETP, to:

        T.

Case 2. (IMPLIES (AND (NOT (ZEROP N))
                      (NOT (EQUAL N 1))
                      (MEMBER N (INVERSE-LIST (SUB1 N) P))
                      (SUBSETP (POSITIVES (SUB1 N))
                               (INVERSE-LIST (SUB1 N) P)))
                 (SUBSETP (POSITIVES N)
                          (INVERSE-LIST N P))),

  which simplifies, rewriting with CDR-CONS and CAR-CONS, and unfolding ZEROP,
  POSITIVES, INVERSE-LIST, and SUBSETP, to:

        T.

Case 1. (IMPLIES (AND (NOT (ZEROP N))
                      (NOT (EQUAL N 1))
                      (NOT (MEMBER N (INVERSE-LIST (SUB1 N) P)))
                      (SUBSETP (POSITIVES (SUB1 N))
                               (INVERSE-LIST (SUB1 N) P)))
                 (SUBSETP (POSITIVES N)
                          (INVERSE-LIST N P))).

  This simplifies, rewriting with DIFFERENCE-1, SUBSETP-CONS, CDR-CONS, and
  CAR-CONS, and unfolding the definitions of ZEROP, POSITIVES, INVERSE-LIST,
  DIFFERENCE, EQUAL, NUMBERP, SUB1, INVERSE, MEMBER, and SUBSETP, to:

        T.


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


[ 0.0 0.1 0.0 ]

SUBSETP-POSITIVES


(PROVE-LEMMA INVERSE-1
             (REWRITE)
             (IMPLIES (LESSP 1 P)
                      (EQUAL (INVERSE 1 P) 1)))

WARNING:  Note that the rewrite rule INVERSE-1 will be stored so as to apply
only to terms with the nonrecursive function symbol INVERSE.


This simplifies, appealing to the lemmas REMAINDER-OF-1, EXP-OF-1, and
DIFFERENCE-1, and opening up the definitions of DIFFERENCE, EQUAL, NUMBERP,
SUB1, REMAINDER, and INVERSE, to:

      (IMPLIES (AND (LESSP 1 P) (NOT (EQUAL P 2)))
               (NOT (EQUAL P 1))).

This again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

INVERSE-1


(PROVE-LEMMA A-D-I-L-LEMMA1
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (NOT (EQUAL (REMAINDER I P) 0))
                           (LESSP I P)
                           (MEMBER J (INVERSE-LIST I P)))
                      (MEMBER (INVERSE J P)
                              (INVERSE-LIST I P)))
             ((USE (INVERSE-OF-INVERSE (J I)))
              (INDUCT (INVERSE-LIST I P))
              (DISABLE INVERSE)))

This conjecture simplifies, rewriting with REMAINDER-WRT-12 and
REMAINDER-WRT-1, and opening up the functions PRIME, NOT, AND, IMPLIES, ZEROP,
EQUAL, REMAINDER, LESSP, INVERSE-LIST, OR, SUB1, and NUMBERP, to nine new
conjectures:

Case 9. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
                             (REMAINDER I P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (MEMBER I (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (LESSP (SUB1 I) P))
                      (NOT (EQUAL (REMAINDER I P) 0))
                      (LESSP I P)
                      (MEMBER J (INVERSE-LIST (SUB1 I) P)))
                 (MEMBER (INVERSE J P)
                         (INVERSE-LIST (SUB1 I) P))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 8. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
                             (REMAINDER I P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (MEMBER I (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (EQUAL (REMAINDER (SUB1 I) P) 0)
                      (NOT (EQUAL (REMAINDER I P) 0))
                      (LESSP I P)
                      (MEMBER J (INVERSE-LIST (SUB1 I) P)))
                 (MEMBER (INVERSE J P)
                         (INVERSE-LIST (SUB1 I) P))),

  which again simplifies, using linear arithmetic, rewriting with
  INVERSE-OF-INVERSE, REMAINDER-0-CROCK, and DIFFERENCE-0, and opening up the
  definitions of PRIME, REMAINDER, EQUAL, INVERSE-LIST, LISTP, and MEMBER, to
  the new conjecture:

        (IMPLIES (AND (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (MEMBER I (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (LESSP (SUB1 I) P))
                      (LESSP I P)
                      (MEMBER J (INVERSE-LIST (SUB1 I) P)))
                 (MEMBER (INVERSE J P)
                         (INVERSE-LIST (SUB1 I) P))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 7. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
                             (REMAINDER I P))
                      (NOT (NUMBERP I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (EQUAL (REMAINDER I P) 0))
                      (LESSP I P)
                      (MEMBER J NIL))
                 (MEMBER (INVERSE J P) NIL)),

  which again simplifies, using linear arithmetic, rewriting with N-Z-I-LEMMA,
  and opening up the definitions of ZEROP, LESSP, REMAINDER, and EQUAL, to:

        T.

Case 6. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
                             (REMAINDER I P))
                      (EQUAL I 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (EQUAL (REMAINDER I P) 0))
                      (LESSP I P)
                      (MEMBER J NIL))
                 (MEMBER (INVERSE J P) NIL)).

  However this again simplifies, using linear arithmetic, applying N-Z-I-LEMMA
  and REMAINDER-0-CROCK, and expanding ZEROP and EQUAL, to:

        T.

Case 5. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
                             (REMAINDER I P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (EQUAL I 1)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (EQUAL (REMAINDER I P) 0))
                      (LESSP I P)
                      (MEMBER J '(1)))
                 (MEMBER (INVERSE J P) '(1))).

  But this again simplifies, rewriting with INVERSE-1 and REMAINDER-OF-1, and
  unfolding the definitions of EQUAL, NUMBERP, CDR, CAR, LISTP, and MEMBER, to:

        T.

Case 4. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
                             (REMAINDER I P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (EQUAL (REMAINDER (SUB1 I) P) 0)
                      (NOT (EQUAL (REMAINDER I P) 0))
                      (LESSP I P)
                      (MEMBER J
                              (CONS I
                                    (CONS (INVERSE I P)
                                          (INVERSE-LIST (SUB1 I) P)))))
                 (MEMBER (INVERSE J P)
                         (CONS I
                               (CONS (INVERSE I P)
                                     (INVERSE-LIST (SUB1 I) P))))).

  This again simplifies, using linear arithmetic, rewriting with
  INVERSE-OF-INVERSE, REMAINDER-0-CROCK, DIFFERENCE-0, CDR-CONS, and CAR-CONS,
  and opening up the definitions of PRIME, REMAINDER, EQUAL, INVERSE-LIST,
  MEMBER, and LISTP, to the following three new conjectures:

  Case 4.3.
          (IMPLIES (AND (NOT (EQUAL I 0))
                        (NUMBERP I)
                        (NOT (EQUAL I 1))
                        (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                        (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (EQUAL P 1))
                        (PRIME1 P (SUB1 P))
                        (EQUAL (SUB1 I) 0)
                        (LESSP I P)
                        (EQUAL J (INVERSE I P))
                        (NOT (EQUAL (INVERSE J P) I)))
                   (EQUAL (INVERSE J P) J)).

    This again simplifies, using linear arithmetic, to:

          T.

  Case 4.2.
          (IMPLIES (AND (NOT (EQUAL I 0))
                        (NUMBERP I)
                        (NOT (EQUAL I 1))
                        (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                        (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (EQUAL P 1))
                        (PRIME1 P (SUB1 P))
                        (NOT (LESSP (SUB1 I) P))
                        (LESSP I P)
                        (EQUAL J (INVERSE I P))
                        (NOT (EQUAL (INVERSE J P) I))
                        (NOT (EQUAL (INVERSE J P) J)))
                   (MEMBER (INVERSE J P)
                           (INVERSE-LIST (SUB1 I) P))),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 4.1.
          (IMPLIES (AND (NOT (EQUAL I 0))
                        (NUMBERP I)
                        (NOT (EQUAL I 1))
                        (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                        (NOT (EQUAL P 0))
                        (NUMBERP P)
                        (NOT (EQUAL P 1))
                        (PRIME1 P (SUB1 P))
                        (NOT (LESSP (SUB1 I) P))
                        (LESSP I P)
                        (MEMBER J (INVERSE-LIST (SUB1 I) P))
                        (NOT (EQUAL (INVERSE J P) I))
                        (NOT (EQUAL (INVERSE J P) (INVERSE I P))))
                   (MEMBER (INVERSE J P)
                           (INVERSE-LIST (SUB1 I) P))),

    which again simplifies, using linear arithmetic, to:

          T.

Case 3. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
                             (REMAINDER I P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (LESSP (SUB1 I) P))
                      (NOT (EQUAL (REMAINDER I P) 0))
                      (LESSP I P)
                      (MEMBER J
                              (CONS I
                                    (CONS (INVERSE I P)
                                          (INVERSE-LIST (SUB1 I) P)))))
                 (MEMBER (INVERSE J P)
                         (CONS I
                               (CONS (INVERSE I P)
                                     (INVERSE-LIST (SUB1 I) P))))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 2. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
                             (REMAINDER I P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (MEMBER (INVERSE J P)
                              (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL (REMAINDER I P) 0))
                      (LESSP I P)
                      (MEMBER J
                              (CONS I
                                    (CONS (INVERSE I P)
                                          (INVERSE-LIST (SUB1 I) P)))))
                 (MEMBER (INVERSE J P)
                         (CONS I
                               (CONS (INVERSE I P)
                                     (INVERSE-LIST (SUB1 I) P))))),

  which again simplifies, applying INVERSE-OF-INVERSE, CDR-CONS, and CAR-CONS,
  and expanding the functions PRIME, REMAINDER, and MEMBER, to:

        T.

Case 1. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
                             (REMAINDER I P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (MEMBER J (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL (REMAINDER I P) 0))
                      (LESSP I P)
                      (MEMBER J
                              (CONS I
                                    (CONS (INVERSE I P)
                                          (INVERSE-LIST (SUB1 I) P)))))
                 (MEMBER (INVERSE J P)
                         (CONS I
                               (CONS (INVERSE I P)
                                     (INVERSE-LIST (SUB1 I) P))))).

  This again simplifies, rewriting with the lemmas INVERSE-OF-INVERSE,
  CDR-CONS, and CAR-CONS, and expanding PRIME, REMAINDER, and MEMBER, to:

        (IMPLIES (AND (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (MEMBER J (INVERSE-LIST (SUB1 I) P)))
                      (LESSP I P)
                      (EQUAL J (INVERSE I P))
                      (NOT (EQUAL (INVERSE J P) I))
                      (NOT (EQUAL (INVERSE J P) J)))
                 (MEMBER (INVERSE J P)
                         (INVERSE-LIST (SUB1 I) P))).

  This again simplifies, using linear arithmetic, rewriting with
  INVERSE-OF-INVERSE, and unfolding the definitions of REMAINDER and PRIME, to:

        T.

Q.E.D.


[ 0.0 3.1 0.0 ]

A-D-I-L-LEMMA1


(PROVE-LEMMA A-D-I-L-LEMMA2
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (NOT (EQUAL (REMAINDER I P) 0))
                           (NOT (EQUAL (REMAINDER J P) 0))
                           (LESSP I P)
                           (LESSP J P)
                           (MEMBER (INVERSE J P)
                                   (INVERSE-LIST I P)))
                      (MEMBER J (INVERSE-LIST I P)))
             ((USE (INVERSE-OF-INVERSE)
                   (A-D-I-L-LEMMA1 (J (INVERSE J P))))
              (DISABLE INVERSE INVERSE-LIST INVERSE-OF-INVERSE A-D-I-L-LEMMA1)))

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

      (IMPLIES (AND (IMPLIES (AND (PRIME P)
                                  (NOT (EQUAL (REMAINDER J P) 0)))
                             (EQUAL (INVERSE (INVERSE J P) P)
                                    (REMAINDER J P)))
                    (IMPLIES (AND (PRIME P)
                                  (NOT (EQUAL (REMAINDER I P) 0))
                                  (LESSP I P)
                                  (MEMBER (INVERSE J P)
                                          (INVERSE-LIST I P)))
                             (MEMBER (INVERSE (INVERSE J P) P)
                                     (INVERSE-LIST I P)))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (NOT (EQUAL (REMAINDER I P) 0))
                    (NOT (EQUAL (REMAINDER J P) 0))
                    (LESSP I P)
                    (LESSP J P)
                    (MEMBER (INVERSE J P)
                            (INVERSE-LIST I P)))
               (MEMBER J (INVERSE-LIST I P))).

This simplifies, using linear arithmetic, rewriting with REMAINDER-0-CROCK and
N-Z-I-LEMMA, and unfolding the definitions of PRIME, REMAINDER, NOT, AND,
IMPLIES, EQUAL, LESSP, and ZEROP, to:

      T.

Q.E.D.


[ 0.0 0.3 0.0 ]

A-D-I-L-LEMMA2


(PROVE-LEMMA A-D-I-L-LEMMA3
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (LESSP I (SUB1 P))
                           (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
                      (ALL-DISTINCT (INVERSE-LIST I P)))
             ((USE (A-D-I-L-LEMMA2 (J I) (I (SUB1 I)))
                   (NO-OTHER-INVOLUTIONS (J I)))
              (DISABLE INVERSE)))

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

      (IMPLIES (AND (IMPLIES (AND (PRIME P)
                                  (NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
                                  (NOT (EQUAL (REMAINDER I P) 0))
                                  (LESSP (SUB1 I) P)
                                  (LESSP I P)
                                  (MEMBER (INVERSE I P)
                                          (INVERSE-LIST (SUB1 I) P)))
                             (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                    (IMPLIES (AND (PRIME P)
                                  (LESSP I (SUB1 P))
                                  (LESSP 1 I))
                             (NOT (EQUAL (INVERSE I P) I)))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (LESSP I (SUB1 P))
                    (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
               (ALL-DISTINCT (INVERSE-LIST I P))),

which simplifies, using linear arithmetic, rewriting with REMAINDER-0-CROCK,
DIFFERENCE-0, SUB1-NNUMBERP, and N-Z-I-LEMMA, and opening up PRIME, REMAINDER,
NOT, LESSP, AND, IMPLIES, SUB1, NUMBERP, EQUAL, INVERSE-LIST, ALL-DISTINCT,
LISTP, MEMBER, and ZEROP, to the following 43 new goals:

Case 43.(IMPLIES (AND (LESSP I 1)
                      (IMPLIES (AND (PRIME P)
                                    (NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
                                    (NOT (EQUAL (REMAINDER I P) 0))
                                    (LESSP (SUB1 I) P)
                                    (LESSP I P)
                                    (MEMBER (INVERSE I P)
                                            (INVERSE-LIST (SUB1 I) P)))
                               (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1)))
                 (ALL-DISTINCT (LIST I (INVERSE I P)))).

  However this again simplifies, using linear arithmetic, to:

        T.

Case 42.(IMPLIES (AND (LESSP I 1)
                      (IMPLIES (AND (PRIME P)
                                    (NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
                                    (NOT (EQUAL (REMAINDER I P) 0))
                                    (LESSP (SUB1 I) P)
                                    (LESSP I P)
                                    (MEMBER (INVERSE I P)
                                            (INVERSE-LIST (SUB1 I) P)))
                               (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (EQUAL I 1))
                 (ALL-DISTINCT '(1))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 41.(IMPLIES (AND (LESSP I 1)
                      (IMPLIES (AND (PRIME P)
                                    (NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
                                    (NOT (EQUAL (REMAINDER I P) 0))
                                    (LESSP (SUB1 I) P)
                                    (LESSP I P)
                                    (MEMBER (INVERSE I P)
                                            (INVERSE-LIST (SUB1 I) P)))
                               (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (EQUAL I 0))
                 (ALL-DISTINCT NIL)),

  which again simplifies, using linear arithmetic, rewriting with the lemmas
  REMAINDER-0-CROCK and N-Z-I-LEMMA, and expanding the functions LESSP, PRIME,
  EQUAL, NOT, ZEROP, INVERSE-LIST, MEMBER, AND, IMPLIES, SUB1, and
  ALL-DISTINCT, to:

        T.

Case 40.(IMPLIES (AND (LESSP I 1)
                      (IMPLIES (AND (PRIME P)
                                    (NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
                                    (NOT (EQUAL (REMAINDER I P) 0))
                                    (LESSP (SUB1 I) P)
                                    (LESSP I P)
                                    (MEMBER (INVERSE I P)
                                            (INVERSE-LIST (SUB1 I) P)))
                               (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (NUMBERP I)))
                 (ALL-DISTINCT NIL)),

  which again simplifies, using linear arithmetic, applying REMAINDER-0-CROCK,
  N-Z-I-LEMMA, and SUB1-NNUMBERP, and opening up the definitions of NUMBERP,
  EQUAL, LESSP, PRIME, NOT, REMAINDER, ZEROP, INVERSE-LIST, MEMBER, AND, LISTP,
  IMPLIES, and ALL-DISTINCT, to:

        T.

Case 39.(IMPLIES (AND (LESSP I 1)
                      (IMPLIES (AND (PRIME P)
                                    (NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
                                    (NOT (EQUAL (REMAINDER I P) 0))
                                    (LESSP (SUB1 I) P)
                                    (LESSP I P)
                                    (MEMBER (INVERSE I P)
                                            (INVERSE-LIST (SUB1 I) P)))
                               (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
                 (ALL-DISTINCT (CONS I
                                     (CONS (INVERSE I P)
                                           (INVERSE-LIST (SUB1 I) P))))).

  But this again simplifies, using linear arithmetic, to:

        T.

Case 38.(IMPLIES (AND (LESSP I 1)
                      (IMPLIES (AND (PRIME P)
                                    (NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
                                    (NOT (EQUAL (REMAINDER I P) 0))
                                    (LESSP (SUB1 I) P)
                                    (LESSP I P)
                                    (MEMBER (INVERSE I P)
                                            (INVERSE-LIST (SUB1 I) P)))
                               (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (EQUAL I 1))
                 (ALL-DISTINCT '(1))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 37.(IMPLIES (AND (LESSP I 1)
                      (IMPLIES (AND (PRIME P)
                                    (NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
                                    (NOT (EQUAL (REMAINDER I P) 0))
                                    (LESSP (SUB1 I) P)
                                    (LESSP I P)
                                    (MEMBER (INVERSE I P)
                                            (INVERSE-LIST (SUB1 I) P)))
                               (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (EQUAL I 0))
                 (ALL-DISTINCT NIL)),

  which again simplifies, using linear arithmetic, rewriting with
  REMAINDER-0-CROCK and N-Z-I-LEMMA, and expanding LESSP, PRIME, SUB1, EQUAL,
  NOT, ZEROP, INVERSE-LIST, MEMBER, AND, and IMPLIES, to:

        T.

Case 36.(IMPLIES (AND (LESSP I 1)
                      (IMPLIES (AND (PRIME P)
                                    (NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
                                    (NOT (EQUAL (REMAINDER I P) 0))
                                    (LESSP (SUB1 I) P)
                                    (LESSP I P)
                                    (MEMBER (INVERSE I P)
                                            (INVERSE-LIST (SUB1 I) P)))
                               (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (NOT (NUMBERP I)))
                 (ALL-DISTINCT NIL)).

  However this again simplifies, using linear arithmetic, applying
  SUB1-NNUMBERP, REMAINDER-0-CROCK, and N-Z-I-LEMMA, and opening up the
  functions NUMBERP, EQUAL, LESSP, PRIME, NOT, REMAINDER, ZEROP, INVERSE-LIST,
  MEMBER, AND, LISTP, IMPLIES, and ALL-DISTINCT, to:

        T.

Case 35.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (LESSP (SUB1 I) P))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1)))
                 (ALL-DISTINCT (LIST I (INVERSE I P)))).

  However this again simplifies, using linear arithmetic, to:

        T.

Case 34.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (LESSP (SUB1 I) P))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (EQUAL I 1))
                 (ALL-DISTINCT '(1))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 33.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (LESSP (SUB1 I) P))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (EQUAL I 0))
                 (ALL-DISTINCT NIL)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 32.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (LESSP (SUB1 I) P))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (NUMBERP I)))
                 (ALL-DISTINCT NIL)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 31.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (LESSP (SUB1 I) P))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
                 (ALL-DISTINCT (CONS I
                                     (CONS (INVERSE I P)
                                           (INVERSE-LIST (SUB1 I) P))))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 30.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (LESSP (SUB1 I) P))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (EQUAL I 1))
                 (ALL-DISTINCT '(1))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 29.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (LESSP (SUB1 I) P))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (EQUAL I 0))
                 (ALL-DISTINCT NIL)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 28.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (LESSP (SUB1 I) P))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (NOT (NUMBERP I)))
                 (ALL-DISTINCT NIL)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 27.(IMPLIES (AND (NOT (LESSP I 1))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1)))
                 (ALL-DISTINCT (LIST I (INVERSE I P)))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 26.(IMPLIES (AND (NOT (LESSP I 1))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (EQUAL I 1))
                 (ALL-DISTINCT '(1))),

  which again simplifies, opening up the functions LESSP, SUB1, EQUAL, NUMBERP,
  and ALL-DISTINCT, to:

        T.

Case 25.(IMPLIES (AND (NOT (LESSP I 1))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (EQUAL I 0))
                 (ALL-DISTINCT NIL)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 24.(IMPLIES (AND (NOT (LESSP I 1))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (NUMBERP I)))
                 (ALL-DISTINCT NIL)),

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

        T.

Case 23.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1)))
                 (ALL-DISTINCT (LIST I (INVERSE I P)))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 22.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (EQUAL I 1))
                 (ALL-DISTINCT '(1))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 21.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (EQUAL I 0))
                 (ALL-DISTINCT NIL)),

  which again simplifies, obviously, to:

        T.

Case 20.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (NUMBERP I)))
                 (ALL-DISTINCT NIL)).

  However this again simplifies, using linear arithmetic, to:

        T.

Case 19.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
                 (ALL-DISTINCT (CONS I
                                     (CONS (INVERSE I P)
                                           (INVERSE-LIST (SUB1 I) P))))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 18.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (EQUAL I 1))
                 (ALL-DISTINCT '(1))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 17.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (EQUAL I 0))
                 (ALL-DISTINCT NIL)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 16.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (NOT (NUMBERP I)))
                 (ALL-DISTINCT NIL)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 15.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (MEMBER (INVERSE I P)
                                   (INVERSE-LIST (SUB1 I) P)))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1)))
                 (ALL-DISTINCT (LIST I (INVERSE I P)))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 14.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (MEMBER (INVERSE I P)
                                   (INVERSE-LIST (SUB1 I) P)))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (EQUAL I 1))
                 (ALL-DISTINCT '(1))),

  which again simplifies, using linear arithmetic, applying the lemma
  INVERSE-1, and unfolding LESSP, EQUAL, INVERSE-LIST, MEMBER, SUB1, NUMBERP,
  and ALL-DISTINCT, to:

        T.

Case 13.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (MEMBER (INVERSE I P)
                                   (INVERSE-LIST (SUB1 I) P)))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (EQUAL I 0))
                 (ALL-DISTINCT NIL)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 12.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (MEMBER (INVERSE I P)
                                   (INVERSE-LIST (SUB1 I) P)))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (NUMBERP I)))
                 (ALL-DISTINCT NIL)),

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

        T.

Case 11.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (MEMBER (INVERSE I P)
                                   (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
                 (ALL-DISTINCT (CONS I
                                     (CONS (INVERSE I P)
                                           (INVERSE-LIST (SUB1 I) P))))),

  which again simplifies, using linear arithmetic, applying
  NO-OTHER-INVOLUTIONS, CDR-CONS, and CAR-CONS, and opening up the definitions
  of SUB1, NUMBERP, EQUAL, LESSP, PRIME, MEMBER, and ALL-DISTINCT, to:

        T.

Case 10.(IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (MEMBER (INVERSE I P)
                                   (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (EQUAL I 1))
                 (ALL-DISTINCT '(1))).

  However this again simplifies, using linear arithmetic, rewriting with
  INVERSE-1, and unfolding the functions LESSP, SUB1, EQUAL, INVERSE-LIST, and
  MEMBER, to:

        T.

Case 9. (IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (MEMBER (INVERSE I P)
                                   (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (EQUAL I 0))
                 (ALL-DISTINCT NIL)).

  But this again simplifies, using linear arithmetic, to:

        T.

Case 8. (IMPLIES (AND (NOT (LESSP I 1))
                      (NOT (MEMBER (INVERSE I P)
                                   (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (NOT (NUMBERP I)))
                 (ALL-DISTINCT NIL)),

  which again simplifies, expanding NUMBERP, EQUAL, and LESSP, to:

        T.

Case 7. (IMPLIES (AND (NOT (LESSP I 1))
                      (MEMBER I (INVERSE-LIST (SUB1 I) P))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1)))
                 (ALL-DISTINCT (LIST I (INVERSE I P)))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 6. (IMPLIES (AND (NOT (LESSP I 1))
                      (MEMBER I (INVERSE-LIST (SUB1 I) P))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (EQUAL I 1))
                 (ALL-DISTINCT '(1))),

  which again simplifies, unfolding LESSP, EQUAL, INVERSE-LIST, and MEMBER, to:

        T.

Case 5. (IMPLIES (AND (NOT (LESSP I 1))
                      (MEMBER I (INVERSE-LIST (SUB1 I) P))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (EQUAL I 0))
                 (ALL-DISTINCT NIL)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 4. (IMPLIES (AND (NOT (LESSP I 1))
                      (MEMBER I (INVERSE-LIST (SUB1 I) P))
                      (EQUAL (SUB1 I) 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (NOT (NUMBERP I)))
                 (ALL-DISTINCT NIL)),

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

        T.

Case 3. (IMPLIES (AND (NOT (LESSP I 1))
                      (MEMBER I (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (EQUAL I 1))
                 (ALL-DISTINCT '(1))),

  which again simplifies, opening up the definitions of LESSP, SUB1, EQUAL,
  INVERSE-LIST, and MEMBER, to:

        T.

Case 2. (IMPLIES (AND (NOT (LESSP I 1))
                      (MEMBER I (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (EQUAL I 0))
                 (ALL-DISTINCT NIL)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (NOT (LESSP I 1))
                      (MEMBER I (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL (INVERSE I P) I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P))
                      (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
                      (NOT (NUMBERP I)))
                 (ALL-DISTINCT NIL)),

  which again simplifies, opening up the functions NUMBERP, EQUAL, and LESSP,
  to:

        T.

Q.E.D.


[ 0.0 2.1 0.0 ]

A-D-I-L-LEMMA3


(PROVE-LEMMA ALL-DISTINCT-INVERSE-LIST
             (REWRITE)
             (IMPLIES (AND (PRIME P) (LESSP I (SUB1 P)))
                      (ALL-DISTINCT (INVERSE-LIST I P)))
             ((USE (A-D-I-L-LEMMA3))
              (INDUCT (POSITIVES I))
              (DISABLE INVERSE)))

WARNING:  the newly proposed lemma, ALL-DISTINCT-INVERSE-LIST, could be
applied whenever the previously added lemma A-D-I-L-LEMMA3 could.




This formula simplifies, rewriting with SUB1-NNUMBERP, and expanding the
functions PRIME, AND, INVERSE-LIST, IMPLIES, ZEROP, NOT, LESSP, ALL-DISTINCT,
OR, EQUAL, SUB1, and NUMBERP, to the following seven new goals:

Case 7. (IMPLIES (AND (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (ALL-DISTINCT (CONS I
                                          (CONS (INVERSE I P)
                                                (INVERSE-LIST (SUB1 I) P))))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (LESSP I (SUB1 P))
                      (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                 (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))).

  However this again simplifies, using linear arithmetic, to:

        T.

Case 6. (IMPLIES (AND (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL I 1))
                      (MEMBER I (INVERSE-LIST (SUB1 I) P))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (LESSP I (SUB1 P)))
                 (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 5. (IMPLIES (AND (NOT (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (LESSP I (SUB1 P))
                      (NOT (EQUAL I 1)))
                 (ALL-DISTINCT (CONS I
                                     (CONS (INVERSE I P)
                                           (INVERSE-LIST (SUB1 I) P))))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 4. (IMPLIES (AND (NOT (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (LESSP I (SUB1 P))
                      (EQUAL I 1))
                 (ALL-DISTINCT '(1))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 3. (IMPLIES (AND (NOT (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (LESSP (SUB1 I) (SUB1 P)))
                      (LESSP I (SUB1 P))
                      (NOT (EQUAL I 1)))
                 (NOT (MEMBER I
                              (INVERSE-LIST (SUB1 I) P)))),

  which again simplifies, using linear arithmetic, to:

        T.

Case 2. (IMPLIES (AND (NOT (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
                      (EQUAL I 0)
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P)))
                 (ALL-DISTINCT NIL)),

  which again simplifies, opening up the definitions of SUB1, EQUAL,
  INVERSE-LIST, and ALL-DISTINCT, to:

        T.

Case 1. (IMPLIES (AND (NOT (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
                      (NOT (NUMBERP I))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (LESSP I (SUB1 P)))
                 (ALL-DISTINCT NIL)),

  which again simplifies, rewriting with SUB1-NNUMBERP, and opening up EQUAL,
  INVERSE-LIST, and ALL-DISTINCT, to:

        T.

Q.E.D.


[ 0.0 0.6 0.0 ]

ALL-DISTINCT-INVERSE-LIST


(PROVE-LEMMA T-I-L-LEMMA1
             (REWRITE)
             (IMPLIES (EQUAL (REMAINDER (TIMES A B) P) 1)
                      (EQUAL (REMAINDER (TIMES A (TIMES B C)) P)
                             (REMAINDER C P)))
             ((USE (TIMES-MOD-3 (A (TIMES A B))
                                (B C)
                                (N P)))
              (DISABLE TIMES-MOD-3)))

This formula can be simplified, using the abbreviations IMPLIES and
ASSOCIATIVITY-OF-TIMES, to:

      (IMPLIES (AND (EQUAL (REMAINDER (TIMES (REMAINDER (TIMES A B) P) C)
                                      P)
                           (REMAINDER (TIMES A B C) P))
                    (EQUAL (REMAINDER (TIMES A B) P) 1))
               (EQUAL (REMAINDER (TIMES A B C) P)
                      (REMAINDER C P))),

which simplifies, rewriting with TIMES-1, TIMES-ZERO2, COMMUTATIVITY-OF-TIMES,
and TIMES-IDENTITY, and unfolding the functions LESSP, EQUAL, and REMAINDER,
to:

      T.

Q.E.D.


[ 0.0 0.1 0.0 ]

T-I-L-LEMMA1


(PROVE-LEMMA T-I-L-LEMMA
             (REWRITE)
             (IMPLIES (EQUAL (REMAINDER (TIMES I (INVERSE I P)) P)
                             1)
                      (EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
                                        P)
                             (REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                                        P)))
             ((USE (T-I-L-LEMMA1 (A I)
                                 (B (INVERSE I P))
                                 (C (TIMES-LIST (INVERSE-LIST (SUB1 I) P)))))
              (DISABLE T-I-L-LEMMA1 INVERSE INVERSE-INVERTS)))

This simplifies, unfolding EQUAL, IMPLIES, and INVERSE-LIST, to the following
four new formulas:

Case 4. (IMPLIES
         (AND (EQUAL (REMAINDER (TIMES I
                                       (INVERSE I P)
                                       (TIMES-LIST (INVERSE-LIST (SUB1 I) P)))
                                P)
                     (REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                                P))
              (EQUAL (REMAINDER (TIMES I (INVERSE I P)) P)
                     1)
              (NOT (EQUAL I 0))
              (NUMBERP I)
              (NOT (EQUAL I 1))
              (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
         (EQUAL (REMAINDER (TIMES-LIST (CONS I
                                             (CONS (INVERSE I P)
                                                   (INVERSE-LIST (SUB1 I) P))))
                           P)
                (REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                           P))).

  However this again simplifies, rewriting with CDR-CONS and CAR-CONS, and
  expanding TIMES-LIST, to:

        T.

Case 3. (IMPLIES
          (AND (EQUAL (REMAINDER (TIMES I
                                        (INVERSE I P)
                                        (TIMES-LIST (INVERSE-LIST (SUB1 I) P)))
                                 P)
                      (REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                                 P))
               (EQUAL (REMAINDER (TIMES I (INVERSE I P)) P)
                      1)
               (NOT (EQUAL I 0))
               (NUMBERP I)
               (EQUAL I 1))
          (EQUAL (REMAINDER (TIMES-LIST '(1)) P)
                 (REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                            P))).

  This again simplifies, rewriting with TIMES-1, COMMUTATIVITY-OF-TIMES, and
  REMAINDER-OF-1, and expanding SUB1, EQUAL, INVERSE-LIST, TIMES-LIST, NUMBERP,
  INVERSE, TIMES, and REMAINDER, to:

        T.

Case 2. (IMPLIES
          (AND (EQUAL (REMAINDER (TIMES I
                                        (INVERSE I P)
                                        (TIMES-LIST (INVERSE-LIST (SUB1 I) P)))
                                 P)
                      (REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                                 P))
               (EQUAL (REMAINDER (TIMES I (INVERSE I P)) P)
                      1)
               (EQUAL I 0))
          (EQUAL (REMAINDER (TIMES-LIST NIL) P)
                 (REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                            P))).

  But this again simplifies, appealing to the lemmas TIMES-1,
  COMMUTATIVITY-OF-TIMES, TIMES-IDENTITY, and REMAINDER-OF-1, and opening up
  the functions SUB1, EQUAL, INVERSE-LIST, TIMES-LIST, LESSP, REMAINDER,
  INVERSE, and TIMES, to:

        T.

Case 1. (IMPLIES
          (AND (EQUAL (REMAINDER (TIMES I
                                        (INVERSE I P)
                                        (TIMES-LIST (INVERSE-LIST (SUB1 I) P)))
                                 P)
                      (REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                                 P))
               (EQUAL (REMAINDER (TIMES I (INVERSE I P)) P)
                      1)
               (NOT (NUMBERP I)))
          (EQUAL (REMAINDER (TIMES-LIST NIL) P)
                 (REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                            P))),

  which again simplifies, rewriting with the lemmas SUB1-NNUMBERP, TIMES-1,
  COMMUTATIVITY-OF-TIMES, EQUAL-TIMES-0, REMAINDER-OF-1, and REMAINDER-WRT-1,
  and opening up EQUAL, INVERSE-LIST, TIMES-LIST, LESSP, and REMAINDER, to:

        T.

Q.E.D.


[ 0.0 0.5 0.0 ]

T-I-L-LEMMA


(PROVE-LEMMA T-I-L-LEMMA3
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (NOT (EQUAL (REMAINDER I P) 0)))
                      (EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
                                        P)
                             (REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                                        P)))
             ((USE (INVERSE-INVERTS (J I)))
              (DISABLE INVERSE INVERSE-LIST TIMES-LIST REMAINDER PRIME)))

This conjecture simplifies, applying COMMUTATIVITY-OF-TIMES and T-I-L-LEMMA,
and unfolding NOT, AND, and IMPLIES, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

T-I-L-LEMMA3


(PROVE-LEMMA T-I-L-LEMMA4
             (REWRITE)
             (IMPLIES (LEQ I 1)
                      (EQUAL (TIMES-LIST (INVERSE-LIST I P))
                             1)))


     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 (OR (EQUAL I 0) (NOT (NUMBERP I)))
                    (p I P))
           (IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                         (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
                    (p I P))
           (IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                         (NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
                         (p (SUB1 I) P))
                    (p I P))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT 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 leads to the following four new goals:

Case 4. (IMPLIES (AND (OR (EQUAL I 0) (NOT (NUMBERP I)))
                      (NOT (LESSP 1 I)))
                 (EQUAL (TIMES-LIST (INVERSE-LIST I P))
                        1)).

  This simplifies, opening up the definitions of NOT, OR, LESSP, EQUAL,
  INVERSE-LIST, and TIMES-LIST, to:

        T.

Case 3. (IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                      (OR (EQUAL 1 0) (NOT (NUMBERP 1)))
                      (NOT (LESSP 1 I)))
                 (EQUAL (TIMES-LIST (INVERSE-LIST I P))
                        1)).

  This simplifies, expanding NOT, OR, EQUAL, and NUMBERP, to:

        T.

Case 2. (IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                      (NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
                      (LESSP 1 (SUB1 I))
                      (NOT (LESSP 1 I)))
                 (EQUAL (TIMES-LIST (INVERSE-LIST I P))
                        1)).

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

        (IMPLIES (AND (LESSP I 1)
                      (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                      (NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
                      (LESSP 1 (SUB1 I))
                      (NOT (LESSP 1 I)))
                 (EQUAL (TIMES-LIST (INVERSE-LIST I P))
                        1)),

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

        T.

Case 1. (IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
                      (NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
                      (EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                             1)
                      (NOT (LESSP 1 I)))
                 (EQUAL (TIMES-LIST (INVERSE-LIST I P))
                        1)),

  which simplifies, applying DIFFERENCE-1, and expanding the functions NOT, OR,
  EQUAL, NUMBERP, LESSP, SUB1, INVERSE-LIST, DIFFERENCE, REMAINDER, and
  INVERSE, to the following five new formulas:

  Case 1.5.
          (IMPLIES (AND (NOT (EQUAL I 0))
                        (NUMBERP I)
                        (EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                               1)
                        (EQUAL (SUB1 I) 0)
                        (NOT (EQUAL I 1))
                        (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                        (NOT (EQUAL P 2))
                        (NOT (NUMBERP P)))
                   (EQUAL (TIMES-LIST (CONS I
                                            (CONS (REMAINDER (EXP I 0) P)
                                                  (INVERSE-LIST (SUB1 I) P))))
                          1)).

    But this again simplifies, using linear arithmetic, to:

          T.

  Case 1.4.
          (IMPLIES (AND (NOT (EQUAL I 0))
                        (NUMBERP I)
                        (EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                               1)
                        (EQUAL (SUB1 I) 0)
                        (NOT (EQUAL I 1))
                        (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                        (NOT (EQUAL P 2))
                        (EQUAL P 0))
                   (EQUAL (TIMES-LIST (CONS I
                                            (CONS (REMAINDER (EXP I 0) P)
                                                  (INVERSE-LIST (SUB1 I) P))))
                          1)),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.3.
          (IMPLIES
           (AND (NOT (EQUAL I 0))
                (NUMBERP I)
                (EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                       1)
                (EQUAL (SUB1 I) 0)
                (NOT (EQUAL I 1))
                (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                (NOT (EQUAL P 2))
                (NOT (EQUAL P 0))
                (NUMBERP P))
           (EQUAL (TIMES-LIST (CONS I
                                    (CONS (REMAINDER (EXP I (SUB1 (SUB1 P))) P)
                                          (INVERSE-LIST (SUB1 I) P))))
                  1)),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.2.
          (IMPLIES
                  (AND (NOT (EQUAL I 0))
                       (NUMBERP I)
                       (EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                              1)
                       (EQUAL (SUB1 I) 0)
                       (NOT (EQUAL I 1))
                       (NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
                       (EQUAL P 2))
                  (EQUAL (TIMES-LIST (CONS I
                                           (CONS I (INVERSE-LIST (SUB1 I) P))))
                         1)),

    which again simplifies, using linear arithmetic, to:

          T.

  Case 1.1.
          (IMPLIES (AND (NOT (EQUAL I 0))
                        (NUMBERP I)
                        (EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                               1)
                        (EQUAL (SUB1 I) 0)
                        (EQUAL I 1))
                   (EQUAL (TIMES-LIST '(1)) 1)),

    which again simplifies, unfolding EQUAL, NUMBERP, INVERSE-LIST, TIMES-LIST,
    and SUB1, to:

          T.


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


[ 0.0 0.1 0.0 ]

T-I-L-LEMMA4


(PROVE-LEMMA TIMES-INVERSE-LIST
             (REWRITE)
             (IMPLIES (AND (PRIME P) (LESSP I P))
                      (EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
                                        P)
                             1))
             ((USE (T-I-L-LEMMA3) (T-I-L-LEMMA4))
              (INDUCT (POSITIVES I))
              (DISABLE INVERSE INVERSE-LIST TIMES-LIST T-I-L-LEMMA3
                       T-I-L-LEMMA4)))

This formula simplifies, rewriting with REMAINDER-WRT-12, REMAINDER-OF-1, and
REMAINDER-WRT-1, and unfolding PRIME, NOT, AND, IMPLIES, SUB1, NUMBERP, EQUAL,
LESSP, ZEROP, REMAINDER, and OR, to the following three new formulas:

Case 3. (IMPLIES (AND (EQUAL (REMAINDER I P) 0)
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL (SUB1 I) 0))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                                        P)
                             1)
                      (LESSP I P))
                 (EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
                                   P)
                        1)).

  But this again simplifies, expanding REMAINDER, to:

        T.

Case 2. (IMPLIES (AND (EQUAL (REMAINDER I P) 0)
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL (SUB1 I) 0))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (LESSP (SUB1 I) P))
                      (LESSP I P))
                 (EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
                                   P)
                        1)),

  which again simplifies, using linear arithmetic, to:

        T.

Case 1. (IMPLIES (AND (EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
                                        P)
                             (REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
                                        P))
                      (NOT (EQUAL I 0))
                      (NUMBERP I)
                      (NOT (EQUAL (SUB1 I) 0))
                      (NOT (EQUAL P 0))
                      (NUMBERP P)
                      (NOT (EQUAL P 1))
                      (PRIME1 P (SUB1 P))
                      (NOT (LESSP (SUB1 I) P))
                      (LESSP I P))
                 (EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
                                   P)
                        1)),

  which again simplifies, using linear arithmetic, to:

        T.

Q.E.D.


[ 0.0 2.5 0.0 ]

TIMES-INVERSE-LIST


(PROVE-LEMMA DELETE-X-LEAVE-A
             (REWRITE)
             (IMPLIES (AND (MEMBER A S) (NOT (EQUAL A X)))
                      (MEMBER A (DELETE X S))))


     Give the conjecture the name *1.


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

Case 4. (IMPLIES (AND (NLISTP S)
                      (MEMBER A S)
                      (NOT (EQUAL A X)))
                 (MEMBER A (DELETE X S))).

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

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP S))
                      (EQUAL A (CAR S))
                      (MEMBER A S)
                      (NOT (EQUAL A X)))
                 (MEMBER A (DELETE X S))).

  This simplifies, rewriting with CAR-CONS, and opening up the definitions of
  NLISTP, MEMBER, and DELETE, to:

        T.

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

  which simplifies, unfolding the functions NLISTP and MEMBER, to:

        T.

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

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

        (IMPLIES (AND (LISTP S)
                      (NOT (EQUAL A (CAR S)))
                      (MEMBER A (DELETE X (CDR S)))
                      (MEMBER A (CDR S))
                      (NOT (EQUAL A X))
                      (NOT (EQUAL X (CAR S))))
                 (MEMBER A
                         (CONS (CAR S) (DELETE X (CDR S))))).

  But this again simplifies, rewriting with CDR-CONS and CAR-CONS, and opening
  up the definition of MEMBER, to:

        T.


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


[ 0.0 0.0 0.0 ]

DELETE-X-LEAVE-A


(PROVE-LEMMA DELETE-MEMBER-LEAVE-SUBSET
             (REWRITE)
             (IMPLIES (AND (SUBSETP R S) (NOT (MEMBER X R)))
                      (SUBSETP R (DELETE X S))))


     Give the conjecture the name *1.


     Let us appeal to the induction principle.  The recursive terms in the
conjecture suggest four inductions.  They merge into two likely candidate
inductions.  However, only one is unflawed.  We will induct according to the
following scheme:
      (AND (IMPLIES (AND (LISTP R)
                         (MEMBER (CAR R) S)
                         (p (CDR R) X S))
                    (p R X S))
           (IMPLIES (AND (LISTP R)
                         (NOT (MEMBER (CAR R) S)))
                    (p R X S))
           (IMPLIES (NOT (LISTP R)) (p R X S))).
Linear arithmetic and the lemma CDR-LESSP can be used to show that the measure
(COUNT R) decreases according to the well-founded relation LESSP in each
induction step of the scheme.  The above induction scheme generates the
following five new conjectures:

Case 5. (IMPLIES (AND (LISTP R)
                      (MEMBER (CAR R) S)
                      (NOT (SUBSETP (CDR R) S))
                      (SUBSETP R S)
                      (NOT (MEMBER X R)))
                 (SUBSETP R (DELETE X S))).

  This simplifies, opening up the function SUBSETP, to:

        T.

Case 4. (IMPLIES (AND (LISTP R)
                      (MEMBER (CAR R) S)
                      (MEMBER X (CDR R))
                      (SUBSETP R S)
                      (NOT (MEMBER X R)))
                 (SUBSETP R (DELETE X S))).

  This simplifies, unfolding the functions SUBSETP and MEMBER, to:

        T.

Case 3. (IMPLIES (AND (LISTP R)
                      (MEMBER (CAR R) S)
                      (SUBSETP (CDR R) (DELETE X S))
                      (SUBSETP R S)
                      (NOT (MEMBER X R)))
                 (SUBSETP R (DELETE X S))).

  This simplifies, applying DELETE-X-LEAVE-A, and unfolding the functions
  SUBSETP and MEMBER, to:

        T.

Case 2. (IMPLIES (AND (LISTP R)
                      (NOT (MEMBER (CAR R) S))
                      (SUBSETP R S)
                      (NOT (MEMBER X R)))
                 (SUBSETP R (DELETE X S))),

  which simplifies, unfolding the definition of SUBSETP, to:

        T.

Case 1. (IMPLIES (AND (NOT (LISTP R))
                      (SUBSETP R S)
                      (NOT (MEMBER X R)))
                 (SUBSETP R (DELETE X S))),

  which simplifies, opening up SUBSETP and MEMBER, to:

        T.


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


[ 0.0 0.0 0.0 ]

DELETE-MEMBER-LEAVE-SUBSET


(PROVE-LEMMA ALL-LESSEQP-DELETE
             (REWRITE)
             (IMPLIES (AND (ALL-DISTINCT L)
                           (ALL-LESSEQP L N))
                      (ALL-LESSEQP (DELETE N L) (SUB1 N))))

.

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

Case 3. (IMPLIES (AND (EQUAL N 0)
                      (ALL-DISTINCT L)
                      (ALL-LESSEQP L N))
                 (ALL-LESSEQP (DELETE N L) (SUB1 N))).

  This simplifies, unfolding the function SUB1, to:

        (IMPLIES (AND (ALL-DISTINCT L)
                      (ALL-LESSEQP L 0))
                 (ALL-LESSEQP (DELETE 0 L) 0)),

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


     So now let us consider:

(IMPLIES (AND (ALL-DISTINCT L)
              (ALL-LESSEQP L N))
         (ALL-LESSEQP (DELETE N L) (SUB1 N))).

We gave this the name *1 above.  Perhaps we can prove it by induction.  The
recursive terms in the conjecture suggest three inductions.  However, they
merge into one likely candidate induction.  We will induct according to the
following scheme:
      (AND (IMPLIES (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 conjectures:

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

  which simplifies, rewriting with PIGEON-HOLE-PRINCIPLE-LEMMA-2,
  DELETE-NON-MEMBER, and ADD1-SUB1, and expanding the definitions of 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 N))
                 (ALL-LESSEQP (DELETE N L) (SUB1 N))).

  This simplifies, unfolding the functions NLISTP and ALL-DISTINCT, to:

        T.

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

  This simplifies, unfolding NLISTP, ALL-DISTINCT, and ALL-LESSEQP, to:

        T.

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

  This simplifies, opening up the definitions of NLISTP, ALL-DISTINCT,
  ALL-LESSEQP, and DELETE, to the following two new conjectures:

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

    However this again simplifies, rewriting with the lemmas CDR-CONS and
    CAR-CONS, and expanding the function ALL-LESSEQP, to:

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

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

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

      which again simplifies, opening up the function LESSP, to:

            T.

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

      which again simplifies, applying SUB1-NNUMBERP, and opening up LESSP, to:

            T.

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

      This again simplifies, clearly, to:

            T.

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

    However this again simplifies, applying DELETE-NON-MEMBER, to:

          T.


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


[ 0.0 0.1 0.0 ]

ALL-LESSEQP-DELETE


(PROVE-LEMMA POSITIVES-BOUNDED
             (REWRITE)
             (IMPLIES (LESSP N M)
                      (NOT (MEMBER M (POSITIVES N)))))

This formula can be simplified, using the abbreviations MEMBER-POSITIVES, NOT,
and IMPLIES, to:

      (IMPLIES (AND (LESSP N M)
                    (NOT (EQUAL M 0))
                    (NUMBERP M))
               (NOT (LESSP M (ADD1 N)))),

which simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

POSITIVES-BOUNDED


(PROVE-LEMMA SUBSETP-POSITIVES-DELETE
             (REWRITE)
             (IMPLIES (SUBSETP (POSITIVES N) L)
                      (SUBSETP (POSITIVES (SUB1 N))
                               (DELETE N L))))

This simplifies, appealing to the lemmas DELETE-MEMBER-LEAVE-SUBSET and
SUB1-NNUMBERP, and opening up the definitions of POSITIVES, SUB1, MEMBER, and
LISTP, to:

      (IMPLIES (AND (NOT (EQUAL N 0))
                    (NUMBERP N)
                    (SUBSETP (CONS N (POSITIVES (SUB1 N)))
                             L))
               (SUBSETP (POSITIVES (SUB1 N))
                        (DELETE N L))).

This again simplifies, using linear arithmetic, appealing to the lemmas
CDR-CONS, CAR-CONS, POSITIVES-BOUNDED, and DELETE-MEMBER-LEAVE-SUBSET, and
unfolding SUBSETP, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

SUBSETP-POSITIVES-DELETE


(PROVE-LEMMA NONZEROP-LESSEQP-ZERO
             (REWRITE)
             (IMPLIES (AND (ZEROP N)
                           (ALL-LESSEQP L N)
                           (ALL-NON-ZEROP L))
                      (NOT (LISTP L))))

WARNING:  Note that NONZEROP-LESSEQP-ZERO contains the free variable N which
will be chosen by instantiating the hypothesis (ZEROP N).


This formula simplifies, expanding ZEROP, to two new conjectures:

Case 2. (IMPLIES (AND (EQUAL N 0)
                      (ALL-LESSEQP L 0)
                      (ALL-NON-ZEROP L))
                 (NOT (LISTP L))),

  which again simplifies, clearly, to:

        (IMPLIES (AND (ALL-LESSEQP L 0)
                      (ALL-NON-ZEROP L))
                 (NOT (LISTP L))),

  which we will name *1.

Case 1. (IMPLIES (AND (NOT (NUMBERP N))
                      (ALL-LESSEQP L N)
                      (ALL-NON-ZEROP L))
                 (NOT (LISTP L))),

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


     So now let us consider:

(IMPLIES (AND (ZEROP N)
              (ALL-LESSEQP L N)
              (ALL-NON-ZEROP L))
         (NOT (LISTP L))).

We gave this the name *1 above.  Perhaps we can prove it by induction.  There
are two plausible inductions.  However, they merge into one likely candidate
induction.  We will induct according to the following scheme:
      (AND (IMPLIES (NLISTP L) (p L N))
           (IMPLIES (AND (NOT (NLISTP L)) (p (CDR L) N))
                    (p 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 induction step of the scheme.  The above
induction scheme generates the following four new formulas:

Case 4. (IMPLIES (AND (NLISTP L)
                      (ZEROP N)
                      (ALL-LESSEQP L N)
                      (ALL-NON-ZEROP L))
                 (NOT (LISTP L))).

  This simplifies, opening up NLISTP, to:

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (ALL-LESSEQP (CDR L) N))
                      (ZEROP N)
                      (ALL-LESSEQP L N)
                      (ALL-NON-ZEROP L))
                 (NOT (LISTP L))).

  This simplifies, opening up the functions NLISTP, ZEROP, ALL-NON-ZEROP,
  ALL-LESSEQP, and LESSP, to:

        (IMPLIES (AND (NOT (ALL-LESSEQP (CDR L) N))
                      (EQUAL N 0)
                      (ALL-LESSEQP L 0)
                      (NOT (EQUAL (CAR L) 0))
                      (NUMBERP (CAR L))
                      (ALL-NON-ZEROP (CDR L)))
                 (NOT (LISTP L))),

  which again simplifies, unfolding the functions LESSP, EQUAL, and
  ALL-LESSEQP, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (ALL-NON-ZEROP (CDR L)))
                      (ZEROP N)
                      (ALL-LESSEQP L N)
                      (ALL-NON-ZEROP L))
                 (NOT (LISTP L))),

  which simplifies, unfolding the functions NLISTP, ZEROP, ALL-NON-ZEROP,
  ALL-LESSEQP, LESSP, and EQUAL, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (LISTP (CDR L)))
                      (ZEROP N)
                      (ALL-LESSEQP L N)
                      (ALL-NON-ZEROP L))
                 (NOT (LISTP L))),

  which simplifies, expanding NLISTP, ZEROP, ALL-NON-ZEROP, ALL-LESSEQP, LESSP,
  and EQUAL, to:

        (IMPLIES (AND (NOT (LISTP (CDR L)))
                      (EQUAL N 0)
                      (ALL-LESSEQP L 0)
                      (NOT (EQUAL (CAR L) 0))
                      (NUMBERP (CAR L))
                      (ALL-NON-ZEROP (CDR L)))
                 (NOT (LISTP L))).

  This again simplifies, expanding LESSP, EQUAL, and ALL-LESSEQP, to:

        T.


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


[ 0.0 0.0 0.0 ]

NONZEROP-LESSEQP-ZERO


(DEFN PIGEONHOLE2-INDUCTION
      (L N)
      (IF (ZEROP N)
          T
          (PIGEONHOLE2-INDUCTION (DELETE N L)
                                 (SUB1 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 recursive call.  Hence, PIGEONHOLE2-INDUCTION is
accepted under the definitional principle.  From the definition we can
conclude that (TRUEP (PIGEONHOLE2-INDUCTION L N)) is a theorem.




[ 0.0 0.0 0.0 ]

PIGEONHOLE2-INDUCTION


(PROVE-LEMMA PIGEONHOLE2
             (REWRITE)
             (IMPLIES (AND (ALL-DISTINCT L)
                           (ALL-NON-ZEROP L)
                           (ALL-LESSEQP L N)
                           (SUBSETP (POSITIVES N) L))
                      (PERM (POSITIVES N) L))
             ((INDUCT (PIGEONHOLE2-INDUCTION L N))))

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

Case 2. (IMPLIES (AND (ZEROP N)
                      (ALL-DISTINCT L)
                      (ALL-NON-ZEROP L)
                      (ALL-LESSEQP L N)
                      (SUBSETP (POSITIVES N) L))
                 (PERM (POSITIVES N) L)),

  which simplifies, expanding ZEROP, POSITIVES, LISTP, SUBSETP, and PERM, to
  two new goals:

  Case 2.2.
          (IMPLIES (AND (EQUAL N 0)
                        (ALL-DISTINCT L)
                        (ALL-NON-ZEROP L)
                        (ALL-LESSEQP L 0))
                   (NOT (LISTP L))),

    which again simplifies, obviously, to:

          (IMPLIES (AND (ALL-DISTINCT L)
                        (ALL-NON-ZEROP L)
                        (ALL-LESSEQP L 0))
                   (NOT (LISTP L))),

    which we will name *1.

  Case 2.1.
          (IMPLIES (AND (NOT (NUMBERP N))
                        (ALL-DISTINCT L)
                        (ALL-NON-ZEROP L)
                        (ALL-LESSEQP L N))
                   (NOT (LISTP L))).

    Call the above conjecture *2.

Case 1. (IMPLIES (AND (NOT (EQUAL N 0))
                      (NUMBERP N)
                      (IMPLIES (AND (ALL-DISTINCT (DELETE N L))
                                    (ALL-NON-ZEROP (DELETE N L))
                                    (ALL-LESSEQP (DELETE N L) (SUB1 N))
                                    (SUBSETP (POSITIVES (SUB1 N))
                                             (DELETE N L)))
                               (PERM (POSITIVES (SUB1 N))
                                     (DELETE N L)))
                      (ALL-DISTINCT L)
                      (ALL-NON-ZEROP L)
                      (ALL-LESSEQP L N)
                      (SUBSETP (POSITIVES N) L))
                 (PERM (POSITIVES N) L)).

  This simplifies, applying the lemmas ALL-DISTINCT-DELETE,
  ALL-NON-ZEROP-DELETE, ALL-LESSEQP-DELETE, SUBSETP-POSITIVES-DELETE, CDR-CONS,
  and CAR-CONS, and opening up AND, IMPLIES, POSITIVES, SUBSETP, and PERM, to:

        T.


     So let us turn our attention to:

      (IMPLIES (AND (NOT (NUMBERP N))
                    (ALL-DISTINCT L)
                    (ALL-NON-ZEROP L)
                    (ALL-LESSEQP L N))
               (NOT (LISTP L))),

which we named *2 above.  We will appeal to induction.  The recursive terms in
the conjecture suggest three inductions.  However, they merge into one likely
candidate induction.  We will induct according to the following scheme:
      (AND (IMPLIES (NLISTP L) (p L N))
           (IMPLIES (AND (NOT (NLISTP L)) (p (CDR L) N))
                    (p L N))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT L) decreases according to the
well-founded relation LESSP in each induction step of the scheme.  The above
induction scheme produces the following five new formulas:

Case 5. (IMPLIES (AND (NLISTP L)
                      (NOT (NUMBERP N))
                      (ALL-DISTINCT L)
                      (ALL-NON-ZEROP L)
                      (ALL-LESSEQP L N))
                 (NOT (LISTP L))).

  This simplifies, expanding NLISTP, to:

        T.

Case 4. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (ALL-DISTINCT (CDR L)))
                      (NOT (NUMBERP N))
                      (ALL-DISTINCT L)
                      (ALL-NON-ZEROP L)
                      (ALL-LESSEQP L N))
                 (NOT (LISTP L))).

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

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (ALL-NON-ZEROP (CDR L)))
                      (NOT (NUMBERP N))
                      (ALL-DISTINCT L)
                      (ALL-NON-ZEROP L)
                      (ALL-LESSEQP L N))
                 (NOT (LISTP L))).

  This simplifies, expanding the functions NLISTP, ALL-DISTINCT, and
  ALL-NON-ZEROP, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (ALL-LESSEQP (CDR L) N))
                      (NOT (NUMBERP N))
                      (ALL-DISTINCT L)
                      (ALL-NON-ZEROP L)
                      (ALL-LESSEQP L N))
                 (NOT (LISTP L))).

  This simplifies, opening up the functions NLISTP, ALL-DISTINCT,
  ALL-NON-ZEROP, ALL-LESSEQP, and LESSP, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (LISTP (CDR L)))
                      (NOT (NUMBERP N))
                      (ALL-DISTINCT L)
                      (ALL-NON-ZEROP L)
                      (ALL-LESSEQP L N))
                 (NOT (LISTP L))).

  This simplifies, opening up the definitions of NLISTP, ALL-DISTINCT, MEMBER,
  ALL-NON-ZEROP, ALL-LESSEQP, and LESSP, to:

        T.


     That finishes the proof of *2.


     So we now return to:

      (IMPLIES (AND (ALL-DISTINCT L)
                    (ALL-NON-ZEROP L)
                    (ALL-LESSEQP L 0))
               (NOT (LISTP L))),

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

Case 5. (IMPLIES (AND (NLISTP L)
                      (ALL-DISTINCT L)
                      (ALL-NON-ZEROP L)
                      (ALL-LESSEQP L 0))
                 (NOT (LISTP L))),

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

        T.

Case 4. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (ALL-DISTINCT (CDR L)))
                      (ALL-DISTINCT L)
                      (ALL-NON-ZEROP L)
                      (ALL-LESSEQP L 0))
                 (NOT (LISTP L))),

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

        T.

Case 3. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (ALL-NON-ZEROP (CDR L)))
                      (ALL-DISTINCT L)
                      (ALL-NON-ZEROP L)
                      (ALL-LESSEQP L 0))
                 (NOT (LISTP L))),

  which simplifies, unfolding the functions NLISTP, ALL-DISTINCT, and
  ALL-NON-ZEROP, to:

        T.

Case 2. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (ALL-LESSEQP (CDR L) 0))
                      (ALL-DISTINCT L)
                      (ALL-NON-ZEROP L)
                      (ALL-LESSEQP L 0))
                 (NOT (LISTP L))),

  which simplifies, opening up the functions NLISTP, ALL-DISTINCT,
  ALL-NON-ZEROP, ALL-LESSEQP, EQUAL, and LESSP, to:

        T.

Case 1. (IMPLIES (AND (NOT (NLISTP L))
                      (NOT (LISTP (CDR L)))
                      (ALL-DISTINCT L)
                      (ALL-NON-ZEROP L)
                      (ALL-LESSEQP L 0))
                 (NOT (LISTP L))),

  which simplifies, opening up the definitions of NLISTP, ALL-DISTINCT, MEMBER,
  ALL-NON-ZEROP, ALL-LESSEQP, EQUAL, and LESSP, to:

        T.


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


[ 0.0 0.1 0.0 ]

PIGEONHOLE2


(PROVE-LEMMA PERM-POSITIVES-INVERSE-LIST
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (EQUAL I (DIFFERENCE P 2)))
                      (PERM (POSITIVES I)
                            (INVERSE-LIST I P))))

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

      (IMPLIES (AND (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (EQUAL I (DIFFERENCE P 2)))
               (PERM (POSITIVES I)
                     (INVERSE-LIST I P))).

This simplifies, using linear arithmetic, rewriting with DIFFERENCE-1,
SUBSETP-POSITIVES, BOUNDED-INVERSE-LIST, ALL-NON-ZEROP-INVERSE-LIST,
ALL-DISTINCT-INVERSE-LIST, and PIGEONHOLE2, and unfolding SUB1, NUMBERP, EQUAL,
DIFFERENCE, and PRIME, to the goal:

      (IMPLIES (AND (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (EQUAL (SUB1 P) 0))
               (PERM (POSITIVES (DIFFERENCE P 2))
                     (INVERSE-LIST (DIFFERENCE P 2) P))).

This again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

PERM-POSITIVES-INVERSE-LIST


(PROVE-LEMMA INVERSE-LIST-FACT
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (EQUAL I (DIFFERENCE P 2)))
                      (EQUAL (TIMES-LIST (INVERSE-LIST I P))
                             (FACT I)))
             ((USE (TIMES-LIST-EQUAL-FACT (N I)
                                          (L (INVERSE-LIST I P))))
              (DISABLE INVERSE-LIST)))

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

      (IMPLIES (AND (IMPLIES (PERM (POSITIVES I)
                                   (INVERSE-LIST I P))
                             (EQUAL (TIMES-LIST (INVERSE-LIST I P))
                                    (FACT I)))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (EQUAL I (DIFFERENCE P 2)))
               (EQUAL (TIMES-LIST (INVERSE-LIST I P))
                      (FACT I))),

which simplifies, applying the lemmas DIFFERENCE-1 and
PERM-POSITIVES-INVERSE-LIST, and opening up the definitions of SUB1, NUMBERP,
EQUAL, DIFFERENCE, PRIME, and IMPLIES, to:

      T.

Q.E.D.


[ 0.0 0.0 0.0 ]

INVERSE-LIST-FACT


(PROVE-LEMMA W-T-LEMMA
             (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (EQUAL I (DIFFERENCE P 2)))
                      (EQUAL (REMAINDER (FACT I) P) 1))
             ((USE (TIMES-INVERSE-LIST))))

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

      (IMPLIES (AND (IMPLIES (AND (PRIME P) (LESSP I P))
                             (EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
                                               P)
                                    1))
                    (NOT (EQUAL P 0))
                    (NUMBERP P)
                    (NOT (EQUAL P 1))
                    (PRIME1 P (SUB1 P))
                    (EQUAL I (DIFFERENCE P 2)))
               (EQUAL (REMAINDER (FACT I) P) 1)).

This simplifies, rewriting with the lemmas DIFFERENCE-1 and INVERSE-LIST-FACT,
and unfolding the definitions of PRIME, SUB1, NUMBERP, EQUAL, DIFFERENCE, AND,
and IMPLIES, to the new goal:

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

which again simplifies, using linear arithmetic, to:

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

But this again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 0.5 0.0 ]

W-T-LEMMA


(PROVE-LEMMA WILSON-THM NIL
             (IMPLIES (PRIME P)
                      (EQUAL (REMAINDER (FACT (SUB1 P)) P)
                             (SUB1 P)))
             ((USE (W-T-LEMMA (I (SUB1 (SUB1 P))))
                   (THM-55-SPECIALIZED-TO-PRIMES (M (SUB1 P))
                                                 (X (FACT (SUB1 (SUB1 P))))
                                                 (Y 1)))
              (DISABLE W-T-LEMMA THM-55-SPECIALIZED-TO-PRIMES)))

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

      (IMPLIES
          (AND (IMPLIES (AND (PRIME P)
                             (EQUAL (SUB1 (SUB1 P))
                                    (DIFFERENCE P 2)))
                        (EQUAL (REMAINDER (FACT (SUB1 (SUB1 P))) P)
                               1))
               (IMPLIES (AND (PRIME P)
                             (NOT (EQUAL (REMAINDER (SUB1 P) P) 0)))
                        (EQUAL (EQUAL (REMAINDER (TIMES (SUB1 P)
                                                        (FACT (SUB1 (SUB1 P))))
                                                 P)
                                      (REMAINDER (TIMES (SUB1 P) 1) P))
                               (EQUAL (REMAINDER (FACT (SUB1 (SUB1 P))) P)
                                      (REMAINDER 1 P))))
               (NOT (EQUAL P 0))
               (NUMBERP P)
               (NOT (EQUAL P 1))
               (PRIME1 P (SUB1 P)))
          (EQUAL (REMAINDER (FACT (SUB1 P)) P)
                 (SUB1 P))),

which simplifies, using linear arithmetic, applying DIFFERENCE-1,
REMAINDER-0-CROCK, REMAINDER-OF-1, DIFFERENCE-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, INVERSE-1, and B-I-LEMMA2, and expanding the functions
PRIME1, DIVIDES, PRIME, SUB1, NUMBERP, EQUAL, DIFFERENCE, AND, IMPLIES, NOT,
FACT, TIMES, LESSP, and REMAINDER, to:

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

which again simplifies, using linear arithmetic, to:

      T.

Q.E.D.


[ 0.0 1.0 0.0 ]

WILSON-THM


(MAKE-LIB "wilson" T)

Making the lib for "wilson".


Compiling the lib for "wilson".

Loading ./basic/wilson.o
Finished loading ./basic/wilson.o

Finished compiling the lib for "wilson".


Finished making the lib for "wilson".


(/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/wilson.lib
 /v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/wilson.lisp)