#|
 Copyright (C) 1994 by David Russinoff.  All Rights Reserved.

 You may copy and distribute verbatim copies of this Nqthm-1992 event script as
 you receive it, in any medium, including embedding it verbatim in derivative
 works, provided that you conspicuously and appropriately publish on each copy
 a valid copyright notice "Copyright (C) 1994 by David Russinoff.  All Rights
 Reserved."

 NO WARRANTY

 David Russinoff PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS
 PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
 INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
 FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
 PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
 ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.

 IN NO EVENT WILL David Russinoff BE LIABLE TO YOU FOR ANY DAMAGES,
 ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL
 DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT
 NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES
 SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF
 SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.

|#

; Work of David Russinoff.
(NOTE-LIB "rsa" T)
(COMPILE-UNCOMPILED-DEFNS "tmp")
(DEFN INVERSE (J P)
  (IF (EQUAL P 2)
      (REMAINDER J 2)
      (REMAINDER (EXP J (DIFFERENCE P 2))
                 P)))
(PROVE-LEMMA INVERSE-INVERTS-LEMMA (REWRITE)
             (IMPLIES (NOT (ZEROP P))
                      (EQUAL (REMAINDER (TIMES (INVERSE J P)
                                               J)
                                        P)
                             (REMAINDER (EXP J (SUB1 P))
                                        P))))
(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)))
(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))))))
(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)))))))
(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)))
(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)))
(PROVE-LEMMA N-O-I-LEMMA1 (REWRITE)
             (EQUAL (DIFFERENCE (TIMES X X)
                                1)
                    (TIMES (ADD1 X)
                           (SUB1 X))))
(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))))
(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)))
(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)))
(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)))
(PROVE-LEMMA I-O-I-LEMMA NIL
             (EQUAL (SUB1 (TIMES (DIFFERENCE P 2)
                                 (DIFFERENCE P 2)))
                    (TIMES (DIFFERENCE P 3)
                           (SUB1 P))))
(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))))))
(PROVE-LEMMA N-Z-I-LEMMA (REWRITE)
             (IMPLIES (AND (ZEROP I)
                           (LESSP 1 P))
                      (EQUAL (INVERSE I P)
                             0)))
(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)))
(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)))
(PROVE-LEMMA B-I-LEMMA1 NIL (IMPLIES (LESSP 1 P)
                                     (LEQ (INVERSE J P)
                                          (SUB1 P))))
(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)))
(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)))))))
(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)))
(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)))
(PROVE-LEMMA SUBSETP-POSITIVES (REWRITE)
             (SUBSETP (POSITIVES N)
                      (INVERSE-LIST N P)))
(PROVE-LEMMA INVERSE-1 (REWRITE)
             (IMPLIES (LESSP 1 P)
                      (EQUAL (INVERSE 1 P)
                             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)))
(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)))
(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)))
(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)))
(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)))
(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)))
(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)))
(PROVE-LEMMA T-I-L-LEMMA4 (REWRITE)
             (IMPLIES (LEQ I 1)
                      (EQUAL (TIMES-LIST (INVERSE-LIST I P))
                             1)))
(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)))
(PROVE-LEMMA DELETE-X-LEAVE-A (REWRITE)
             (IMPLIES (AND (MEMBER A S)
                           (NOT (EQUAL A X)))
                      (MEMBER A (DELETE X S))))
(PROVE-LEMMA DELETE-MEMBER-LEAVE-SUBSET (REWRITE)
             (IMPLIES (AND (SUBSETP R S)
                           (NOT (MEMBER X R)))
                      (SUBSETP R (DELETE X S))))
(PROVE-LEMMA ALL-LESSEQP-DELETE (REWRITE)
             (IMPLIES (AND (ALL-DISTINCT L)
                           (ALL-LESSEQP L N))
                      (ALL-LESSEQP (DELETE N L)
                                   (SUB1 N))))
(PROVE-LEMMA POSITIVES-BOUNDED (REWRITE)
             (IMPLIES (LESSP N M)
                      (NOT (MEMBER M (POSITIVES N)))))
(PROVE-LEMMA SUBSETP-POSITIVES-DELETE (REWRITE)
             (IMPLIES (SUBSETP (POSITIVES N)
                               L)
                      (SUBSETP (POSITIVES (SUB1 N))
                               (DELETE N L))))
(PROVE-LEMMA NONZEROP-LESSEQP-ZERO (REWRITE)
             (IMPLIES (AND (ZEROP N)
                           (ALL-LESSEQP L N)
                           (ALL-NON-ZEROP L))
                      (NOT (LISTP L))))
(DEFN PIGEONHOLE2-INDUCTION (L N)
  (IF (ZEROP N)
      T
      (PIGEONHOLE2-INDUCTION (DELETE N L)
                             (SUB1 N))))
(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))))
(PROVE-LEMMA PERM-POSITIVES-INVERSE-LIST (REWRITE)
             (IMPLIES (AND (PRIME P)
                           (EQUAL I (DIFFERENCE P 2)))
                      (PERM (POSITIVES I)
                            (INVERSE-LIST I P))))
(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)))
(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))))
(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)))

(make-lib "wilson" t)