#|
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.
|#
; Mon Sep 17 12:10:54 CDT 1990
; This events file is an addition to the events files described in A
; Computational Logic Handbook.
; This file is a new version of the proof of Gauss's law of quadratic
; reciprocity. It was composed entirely by David Russinoff, who also
; composed the Wilson and Gauss events in basic.events. According to
; Russinoff, the version below is much better than the one in basic.events.
; This version also corresponds to a forthcoming paper of Russinoff in
; the Journal of Automated Reasoning.
(NOTE-LIB "wilson" T)
(DEFN SQUARES (N P)
(IF (ZEROP N) (CONS 0 NIL)
(CONS (REMAINDER (TIMES N N) P) (SQUARES (SUB1 N) P))))
(DEFN RESIDUE (A P)
(MEMBER (REMAINDER A P) (SQUARES P P)))
(PROVE-LEMMA ALL-SQUARES-1 NIL
(IMPLIES (AND (NOT (ZEROP P)) (LEQ M N))
(MEMBER (REMAINDER (TIMES M M) P) (SQUARES N P))))
(PROVE-LEMMA ALL-SQUARES-2 NIL
(EQUAL (REMAINDER (TIMES Y Y) P)
(REMAINDER (TIMES (REMAINDER Y P) (REMAINDER Y P)) P))
((USE (TIMES-MOD-1 (X Y) (N P))
(TIMES-MOD-3 (B (REMAINDER Y P)) (A Y) (N P)))
(DISABLE TIMES-MOD-1 TIMES-MOD-3)))
(PROVE-LEMMA ALL-SQUARES (REWRITE)
(IMPLIES (AND (NOT (ZEROP P)) (NOT (MEMBER X (SQUARES P P))))
(NOT (EQUAL X (REMAINDER (TIMES Y Y) P))))
((USE (ALL-SQUARES-1 (N P) (M (REMAINDER Y P)))
(ALL-SQUARES-2))
(DISABLE TIMES-MOD-1 TIMES-MOD-3)))
(PROVE-LEMMA EULER-1-1 NIL
(IMPLIES (NOT (DIVIDES 2 P))
(EQUAL (TIMES 2 (QUOTIENT P 2)) (SUB1 P))))
(PROVE-LEMMA EULER-1-2 NIL
(IMPLIES (NOT (DIVIDES 2 P))
(EQUAL (EXP (TIMES I I) (QUOTIENT P 2))
(EXP I (SUB1 P))))
((USE (EXP-EXP (J 2) (K (QUOTIENT P 2))) (EULER-1-1))
(DISABLE EXP-EXP)))
(PROVE-LEMMA EULER-1-3 NIL
(IMPLIES (EQUAL (REMAINDER A P) (REMAINDER B P))
(EQUAL (REMAINDER (EXP A C) P) (REMAINDER (EXP B C) P)))
((USE (REMAINDER-EXP (I C) (N P))
(REMAINDER-EXP (A B) (I C) (N P)))
(DISABLE REMAINDER-EXP)))
(PROVE-LEMMA EULER-1-4 NIL
(IMPLIES (AND (PRIME P) (NOT (DIVIDES 2 P)) (NOT (DIVIDES P I)))
(EQUAL (REMAINDER (EXP (TIMES I I) (QUOTIENT P 2)) P)
1))
((USE (EULER-1-2)) (DISABLE LESSP-REMAINDER-DIVISOR PRIME)))
(PROVE-LEMMA EULER-1-5 NIL
(IMPLIES (AND (PRIME P) (NOT (DIVIDES P A))
(EQUAL (REMAINDER A P)
(REMAINDER (TIMES I I) P)))
(NOT (DIVIDES P I)))
((USE (PRIME-KEY-REWRITE (A I) (B I)))
(DISABLE PRIME-KEY-REWRITE PRIME)))
(PROVE-LEMMA EULER-1-6 NIL
(IMPLIES (AND (PRIME P) (NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(EQUAL (REMAINDER A P) (REMAINDER (TIMES I I) P)))
(EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) 1))
((USE (EULER-1-4) (EULER-1-5)
(EULER-1-3 (B (TIMES I I)) (C (QUOTIENT P 2))))
(DISABLE PRIME LESSP-REMAINDER-DIVISOR B-I-LEMMA2 LESSP
SUB1-NNUMBERP REMAINDER-0-CROCK REMAINDER)))
(PROVE-LEMMA EULER-1-7 (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES 2 P))
(NOT (DIVIDES P A))
(MEMBER (REMAINDER A P) (SQUARES I P)))
(EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) 1))
((USE (EULER-1-6)) (INDUCT (SQUARES I P))
(DISABLE PRIME REMAINDER LESSP-REMAINDER-DIVISOR)))
(PROVE-LEMMA EULER-1 (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES 2 P))
(NOT (DIVIDES P A)) (RESIDUE A P))
(EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) 1))
((DISABLE PRIME)))
(DEFN COMPLEMENT (J A P) (REMAINDER (TIMES (INVERSE J P) A) P))
(DISABLE INVERSE)
(PROVE-LEMMA COMPLEMENT-WORKS (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES P J)))
(EQUAL (REMAINDER (TIMES J (COMPLEMENT J A P)) P)
(REMAINDER A P)))
((USE (INVERSE-INVERTS)
(TIMES-MOD-3 (A (TIMES J (INVERSE J P))) (B A) (N P)))
(DISABLE INVERSE-INVERTS TIMES-MOD-3 PRIME)))
(PROVE-LEMMA BOUNDED-COMPLEMENT (REWRITE)
(IMPLIES (NOT (ZEROP P)) (LESSP (COMPLEMENT J A P) P)))
(DISABLE COMPLEMENT)
(PROVE-LEMMA NON-ZEROP-COMPLEMENT (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES P J))
(NOT (DIVIDES P A)))
(NOT (ZEROP (COMPLEMENT J A P))))
((USE (COMPLEMENT-WORKS)) (DISABLE COMPLEMENT-WORKS PRIME)))
(PROVE-LEMMA COMPLEMENT-IS-UNIQUE (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES P A))
(EQUAL (REMAINDER (TIMES J X) P)
(REMAINDER A P)))
(EQUAL (COMPLEMENT J A P) (REMAINDER X P)))
((USE (COMPLEMENT-WORKS)
(THM-55-SPECIALIZED-TO-PRIMES (M J) (Y (COMPLEMENT J A P))))
(DISABLE COMPLEMENT-WORKS THM-55-SPECIALIZED-TO-PRIMES PRIME)))
(DISABLE SQUARES)
(PROVE-LEMMA NO-SELF-COMPLEMENT (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES P J))
(NOT (DIVIDES P A)) (NOT (RESIDUE A P)))
(NOT (EQUAL J (COMPLEMENT J A P))))
((USE (COMPLEMENT-WORKS) (ALL-SQUARES (X (REMAINDER A P)) (Y J)))
(DISABLE COMPLEMENT-WORKS ALL-SQUARES PRIME1)))
(PROVE-LEMMA COMPLEMENT-OF-COMPLEMENT (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES P J)) (NOT (DIVIDES P A)))
(EQUAL (COMPLEMENT (COMPLEMENT J A P) A P)
(REMAINDER J P)))
((USE (COMPLEMENT-WORKS)
(COMPLEMENT-IS-UNIQUE (J (COMPLEMENT J A P)) (X J)))
(DISABLE COMPLEMENT-WORKS COMPLEMENT-IS-UNIQUE)))
(DEFN COMPLEMENTS (I A P)
(IF (ZEROP I) NIL
(IF (MEMBER I (COMPLEMENTS (SUB1 I) A P))
(COMPLEMENTS (SUB1 I) A P)
(CONS I (CONS (COMPLEMENT I A P)
(COMPLEMENTS (SUB1 I) A P))))))
(PROVE-LEMMA ALL-NON-ZEROP-COMPLEMENTS (REWRITE)
(IMPLIES (AND (PRIME P) (LESSP I P) (NOT (DIVIDES P A)))
(ALL-NON-ZEROP (COMPLEMENTS I A P)))
((USE (NON-ZEROP-COMPLEMENT (J I))) (INDUCT (COMPLEMENTS I A P))))
(PROVE-LEMMA BOUNDED-COMPLEMENTS (REWRITE)
(IMPLIES (LESSP I P)
(ALL-LESSEQP (COMPLEMENTS I A P) (SUB1 P)))
((USE (BOUNDED-COMPLEMENT (J I))) (INDUCT (COMPLEMENTS I A P))))
(PROVE-LEMMA SUBSETP-POSITIVES-COMPLEMENTS (REWRITE)
(SUBSETP (POSITIVES N) (COMPLEMENTS N A P)))
(PROVE-LEMMA COMPLEMENTS-CLOSED-1 NIL
(IMPLIES (AND (PRIME P) (NOT (ZEROP I))
(LESSP I P) (NOT (DIVIDES P A))
(MEMBER J (COMPLEMENTS I A P)))
(MEMBER (COMPLEMENT J A P) (COMPLEMENTS I A P)))
((USE (COMPLEMENT-OF-COMPLEMENT (J I))) (INDUCT (COMPLEMENTS I A P))
(DISABLE COMPLEMENT-OF-COMPLEMENT)))
(PROVE-LEMMA COMPLEMENTS-CLOSED-2 NIL
(IMPLIES (AND (PRIME P) (NOT (ZEROP I))
(NOT (ZEROP J)) (LESSP I P)
(LESSP J P) (NOT (DIVIDES P A))
(MEMBER (COMPLEMENT J A P) (COMPLEMENTS I A P)))
(MEMBER J (COMPLEMENTS I A P)))
((USE (COMPLEMENT-OF-COMPLEMENT)
(COMPLEMENTS-CLOSED-1 (J (COMPLEMENT J A P))))
(DISABLE COMPLEMENT-OF-COMPLEMENT COMPLEMENTS)))
(PROVE-LEMMA ALL-DISTINCT-COMPLEMENTS-1 NIL
(IMPLIES (AND (PRIME P) (LESSP I P)
(NOT (DIVIDES P A)) (NOT (RESIDUE A P))
(ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P)))
(ALL-DISTINCT (COMPLEMENTS I A P)))
((USE (COMPLEMENTS-CLOSED-2 (J I) (I (SUB1 I)))
(NO-SELF-COMPLEMENT (J I)))
(DISABLE PRIME)))
(PROVE-LEMMA ALL-DISTINCT-COMPLEMENTS (REWRITE)
(IMPLIES (AND (PRIME P) (LESSP I P)
(NOT (DIVIDES P A)) (NOT (RESIDUE A P)))
(ALL-DISTINCT (COMPLEMENTS I A P)))
((USE (ALL-DISTINCT-COMPLEMENTS-1)) (INDUCT (POSITIVES I))
(DISABLE PRIME)))
(PROVE-LEMMA PERM-POSITIVES-COMPLEMENTS (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES P A))
(NOT (RESIDUE A P)))
(PERM (POSITIVES (SUB1 P))
(COMPLEMENTS (SUB1 P) A P))))
(PROVE-LEMMA COMPLEMENTS-FACT (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES P A))
(NOT (RESIDUE A P)))
(EQUAL (TIMES-LIST (COMPLEMENTS (SUB1 P) A P))
(FACT (SUB1 P))))
((USE (TIMES-LIST-EQUAL-FACT (N (SUB1 P))
(L (COMPLEMENTS (SUB1 P) A P))))
(DISABLE TIMES-LIST-EQUAL-FACT COMPLEMENTS)))
(PROVE-LEMMA TIMES-MOD-4 NIL
(IMPLIES (EQUAL (REMAINDER (TIMES I J) P) (REMAINDER A P))
(EQUAL (REMAINDER (TIMES I (TIMES J K)) P)
(REMAINDER (TIMES A (REMAINDER K P)) P)))
((USE (TIMES-MOD-3 (A (TIMES I J)) (B K) (N P)))
(DISABLE TIMES-MOD-3)))
(PROVE-LEMMA TIMES-COMPLEMENTS-1 NIL
(IMPLIES (AND (EQUAL (REMAINDER (TIMES I (COMPLEMENT I A P)) P)
(REMAINDER A P))
(AND (NOT (ZEROP I))
(NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P)))))
(EQUAL (REMAINDER (TIMES-LIST (COMPLEMENTS I A P)) P)
(REMAINDER
(TIMES A
(REMAINDER
(TIMES-LIST (COMPLEMENTS (SUB1 I) A P))
P))
P)))
((USE (TIMES-MOD-4 (J (COMPLEMENT I A P))
(K (TIMES-LIST (COMPLEMENTS (SUB1 I) A P)))))
(DISABLE COMPLEMENT-WORKS)))
(PROVE-LEMMA TIMES-COMPLEMENTS-2 NIL
(IMPLIES (AND (PRIME P) (NOT (DIVIDES P I))
(NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))))
(EQUAL (REMAINDER (TIMES-LIST (COMPLEMENTS I A P)) P)
(REMAINDER
(TIMES A
(REMAINDER
(TIMES-LIST (COMPLEMENTS (SUB1 I) A P))
P))
P)))
((USE (TIMES-COMPLEMENTS-1) (COMPLEMENT-WORKS (J I)))
(DISABLE COMPLEMENT-WORKS COMPLEMENTS TIMES-LIST PRIME)))
(PROVE-LEMMA QUOTIENT-PLUS-1 NIL
(IMPLIES (AND (NOT (ZEROP N)) (NUMBERP X) (EQUAL Y (PLUS X N)))
(EQUAL (QUOTIENT Y N) (ADD1 (QUOTIENT X N)))))
(PROVE-LEMMA TIMES-COMPLEMENTS-3 NIL
(IMPLIES (AND (NOT (ZEROP I))
(NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))))
(EQUAL (QUOTIENT (LENGTH (COMPLEMENTS I A P)) 2)
(ADD1 (QUOTIENT (LENGTH (COMPLEMENTS (SUB1 I) A P))
2))))
((USE (QUOTIENT-PLUS-1 (X (LENGTH (COMPLEMENTS (SUB1 I) A P)))
(Y (LENGTH (COMPLEMENTS I A P))) (N 2)))))
(PROVE-LEMMA TIMES-COMPLEMENTS-4 NIL
(IMPLIES (AND (PRIME P)
(NOT (ZEROP I))
(LESSP I P)
(EQUAL (REMAINDER
(TIMES-LIST (COMPLEMENTS (SUB1 I) A P))
P)
(REMAINDER
(EXP A
(QUOTIENT
(LENGTH (COMPLEMENTS (SUB1 I) A P))
2))
P)))
(EQUAL (REMAINDER (TIMES-LIST (COMPLEMENTS I A P)) P)
(REMAINDER
(EXP A (QUOTIENT (LENGTH (COMPLEMENTS I A P)) 2))
P)))
((USE (TIMES-COMPLEMENTS-2) (TIMES-COMPLEMENTS-3)
(TIMES-MOD-1
(X A)
(Y (EXP A (QUOTIENT (LENGTH (COMPLEMENTS (SUB1 I) A P)) 2)))
(N P)))
(DISABLE PRIME TIMES-MOD-1 TIMES-LIST)))
(PROVE-LEMMA TIMES-COMPLEMENTS-5 NIL
(IMPLIES (ZEROP I)
(EQUAL (REMAINDER (TIMES-LIST (COMPLEMENTS I A P)) P)
(REMAINDER
(EXP A (QUOTIENT (LENGTH (COMPLEMENTS I A P)) 2))
P))))
(PROVE-LEMMA TIMES-COMPLEMENTS (REWRITE)
(IMPLIES (AND (PRIME P) (LESSP I P))
(EQUAL (REMAINDER (TIMES-LIST (COMPLEMENTS I A P)) P)
(REMAINDER
(EXP A (QUOTIENT (LENGTH (COMPLEMENTS I A P)) 2))
P)))
((USE (TIMES-COMPLEMENTS-4) (TIMES-COMPLEMENTS-5))
(INDUCT (POSITIVES I))
(DISABLE PRIME REMAINDER TIMES-LIST COMPLEMENTS QUOTIENT LENGTH)))
(PROVE-LEMMA SUB1-LENGTH-DELETE (REWRITE)
(IMPLIES (MEMBER X B)
(EQUAL (LENGTH (DELETE X B)) (SUB1 (LENGTH B)))))
(PROVE-LEMMA EQUAL-LENGTH-PERM NIL
(IMPLIES (PERM A B) (EQUAL (LENGTH A) (LENGTH B)))
((INDUCT (PERM A B))))
(PROVE-LEMMA LENGTH-POSITIVES (REWRITE)
(EQUAL (LENGTH (POSITIVES N)) (FIX N))
((INDUCT (POSITIVES N))))
(PROVE-LEMMA EULER-2-1 NIL
(IMPLIES (AND (PRIME P) (NOT (DIVIDES P A)) (NOT (RESIDUE A P)))
(EQUAL (REMAINDER
(EXP A
(QUOTIENT (LENGTH (COMPLEMENTS (SUB1 P) A P))
2))
P)
(SUB1 P)))
((USE (TIMES-COMPLEMENTS (I (SUB1 P))) (COMPLEMENTS-FACT)
(WILSON-THM))
(DISABLE TIMES-COMPLEMENTS COMPLEMENTS-FACT)))
(PROVE-LEMMA EULER-2-2 (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES P A)) (NOT (RESIDUE A P)))
(EQUAL (LENGTH (COMPLEMENTS (SUB1 P) A P)) (SUB1 P)))
((USE (EQUAL-LENGTH-PERM (A (POSITIVES (SUB1 P)))
(B (COMPLEMENTS (SUB1 P) A P)))
(PERM-POSITIVES-COMPLEMENTS))
(DISABLE EQUAL-LENGTH-PERM PERM-POSITIVES-COMPLEMENTS)))
(PROVE-LEMMA EULER-2-3 NIL
(IMPLIES (NOT (ZEROP P))
(EQUAL (DIVIDES 2 P) (NOT (DIVIDES 2 (SUB1 P)))))
((INDUCT (ODD P))))
(PROVE-LEMMA EULER-2-4 (REWRITE)
(IMPLIES (NOT (DIVIDES 2 P))
(EQUAL (QUOTIENT (SUB1 P) 2) (QUOTIENT P 2)))
((USE (EULER-2-3) (REMAINDER-QUOTIENT (X P) (Y 2))
(REMAINDER-QUOTIENT (X (SUB1 P)) (Y 2)))
(DISABLE REMAINDER-QUOTIENT)))
(PROVE-LEMMA EULER-2 (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES 2 P))
(NOT (DIVIDES P A)) (NOT (RESIDUE A P)))
(EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) (SUB1 P)))
((USE (EULER-2-1))
(DISABLE EULER-2-1 PRIME DIVIDES RESIDUE EXP QUOTIENT LENGTH
COMPLEMENTS)))
(DEFN EVENP (X) (IF (ZEROP X) T (NOT (EVENP (SUB1 X)))))
(PROVE-LEMMA EVENP-PLUS (REWRITE)
(EQUAL (EVENP (PLUS A B)) (EQUAL (EVENP A) (EVENP B))))
(PROVE-LEMMA EVENP-DIFF (REWRITE)
(EQUAL (EVENP (DIFFERENCE P X))
(OR (LESSP P X) (EQUAL (EVENP P) (EVENP X)))))
(PROVE-LEMMA EVENP-TIMES (REWRITE)
(EQUAL (EVENP (TIMES A B)) (OR (EVENP A) (EVENP B))))
(PROVE-LEMMA EVENP-EVEN (REWRITE) (EQUAL (EVEN P) (EVENP P)))
(PROVE-LEMMA EVEN-PLUS (REWRITE)
(EQUAL (EVEN (PLUS A B)) (EQUAL (EVEN A) (EVEN B)))
((DISABLE EVEN)))
(PROVE-LEMMA EVEN-DIFF (REWRITE)
(EQUAL (EVEN (DIFFERENCE P X))
(OR (LESSP P X) (EQUAL (EVEN P) (EVEN X))))
((DISABLE EVEN)))
(PROVE-LEMMA EVEN-TIMES (REWRITE)
(EQUAL (EVEN (TIMES A B)) (OR (EVEN A) (EVEN B)))
((DISABLE EVEN)))
(PROVE-LEMMA EVEN-REM (REWRITE)
(IMPLIES (NOT (EVEN P))
(EQUAL (EVEN (DIFFERENCE P (REMAINDER X P)))
(NOT (EVEN (REMAINDER X P)))))
((DISABLE EVEN)))
(PROVE-LEMMA EVEN-ADD1 (REWRITE)
(EQUAL (EVEN (ADD1 X)) (NOT (EVEN X)))
((DISABLE EVEN)))
(DISABLE EVENP-EVEN)
(PROVE-LEMMA EVEN-PRIME-2 (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (EQUAL P 2)))
(NOT (EVEN P))))
(PROVE-LEMMA EVEN-PRIME (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (EQUAL P 2)))
(NOT (EQUAL (REMAINDER P 2) 0)))
((DISABLE PRIME1)))
(PROVE-LEMMA EULER-CRITERION NIL
(IMPLIES (AND (PRIME P) (NOT (EQUAL P 2)) (NOT (DIVIDES P A)))
(EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P)
(IF (RESIDUE A P) 1 (SUB1 P))))
((DISABLE PRIME RESIDUE)))
(DISABLE EULER-1)
(DISABLE EULER-2)
(DEFN RES1 (N A P)
(IF (ZEROP N) T
(IF (LESSP (QUOTIENT P 2) (REMAINDER (TIMES A N) P))
(NOT (RES1 (SUB1 N) A P)) (RES1 (SUB1 N) A P))))
(DEFN REFLECTIONS (N A P)
(IF (ZEROP N) NIL
(IF (LESSP (QUOTIENT P 2) (REMAINDER (TIMES A N) P))
(CONS (DIFFERENCE P (REMAINDER (TIMES A N) P))
(REFLECTIONS (SUB1 N) A P))
(CONS (REMAINDER (TIMES A N) P)
(REFLECTIONS (SUB1 N) A P)))))
(PROVE-LEMMA DIFF-MOD-1 (REWRITE)
(IMPLIES (LEQ B A)
(EQUAL (REMAINDER (DIFFERENCE A (REMAINDER B P)) P)
(REMAINDER (DIFFERENCE A B) P)))
((USE (REMAINDER-QUOTIENT (X B) (Y P))
(REMAINDER-PLUS-TIMES-1 (X (DIFFERENCE A B))
(I (QUOTIENT B P)) (J P)))
(DISABLE REMAINDER-QUOTIENT REMAINDER-PLUS-TIMES-1
REMAINDER-PLUS-TIMES-2)))
(PROVE-LEMMA REM-DIFF-TIMES (REWRITE)
(IMPLIES (AND (LESSP X P) (AND (NOT (ZEROP X)) (NOT (ZEROP B))))
(EQUAL (REMAINDER (DIFFERENCE (TIMES B P) X) P)
(DIFFERENCE P X)))
((USE (REMAINDER-PLUS-TIMES-1 (X (DIFFERENCE P X)) (I (SUB1 B))
(J P)))
(DISABLE REMAINDER-PLUS-TIMES-1 REMAINDER-PLUS-TIMES-2)))
(PROVE-LEMMA REFLECT-COMMUTES-WITH-TIMES-1 (REWRITE)
(IMPLIES (LEQ Y P)
(EQUAL (REMAINDER (TIMES (DIFFERENCE P Y) X) P)
(REMAINDER
(DIFFERENCE P (REMAINDER (TIMES Y X) P))
P)))
((USE (DIFF-MOD-1 (A (TIMES P X)) (B (TIMES Y X)))
(LESSP-TIMES-CANCELLATION (Z X) (X Y) (Y P))
(REM-DIFF-TIMES (B X) (X (REMAINDER (TIMES Y X) P))))
(DISABLE LESSP-TIMES-CANCELLATION REM-DIFF-TIMES DIFF-MOD-1)))
(PROVE-LEMMA REFLECT-COMMUTES-WITH-TIMES-2 (REWRITE)
(IMPLIES (LEQ Y P)
(EQUAL (REMAINDER (TIMES X (DIFFERENCE P Y)) P)
(REMAINDER (DIFFERENCE P (REMAINDER (TIMES X Y) P))
P)))
((USE (REFLECT-COMMUTES-WITH-TIMES-1))
(DISABLE REFLECT-COMMUTES-WITH-TIMES-1)))
(PROVE-LEMMA TIMES-EXP-FACT (REWRITE)
(IMPLIES (NOT (ZEROP N))
(EQUAL (REMAINDER
(TIMES (TIMES A N)
(TIMES (EXP A (SUB1 N))
(FACT (SUB1 N))))
P)
(REMAINDER (TIMES (EXP A N) (FACT N)) P))))
(PROVE-LEMMA REM-REFLECTIONS-1 (REWRITE)
(IMPLIES (AND (NOT (ZEROP P)) (NOT (ZEROP N))
(NOT (LESSP (QUOTIENT P 2)
(REMAINDER (TIMES A N) P)))
(EQUAL (REMAINDER
(TIMES-LIST (REFLECTIONS (SUB1 N) A P)) P)
(REMAINDER
(TIMES (EXP A (SUB1 N)) (FACT (SUB1 N))) P)))
(EQUAL (REMAINDER (TIMES-LIST (REFLECTIONS N A P)) P)
(REMAINDER (TIMES (EXP A N) (FACT N)) P)))
((USE (REMAINDER-EXP-LEMMA (A P) (X (TIMES A N))
(Y (TIMES-LIST (REFLECTIONS (SUB1 N) A P)))
(Z (TIMES (EXP A (SUB1 N)) (FACT (SUB1 N))))))
(HANDS-OFF TIMES DIFFERENCE QUOTIENT EXP FACT)
(DISABLE REMAINDER-EXP-LEMMA)))
(PROVE-LEMMA REM-REFLECTIONS-2 (REWRITE)
(IMPLIES (AND (NOT (ZEROP P))
(NOT (ZEROP N))
(LESSP (QUOTIENT P 2) (REMAINDER (TIMES A N) P))
(EQUAL (REMAINDER
(TIMES-LIST (REFLECTIONS (SUB1 N) A P))
P)
(REMAINDER
(TIMES (EXP A (SUB1 N)) (FACT (SUB1 N)))
P)))
(EQUAL (REMAINDER (TIMES-LIST (REFLECTIONS N A P)) P)
(REMAINDER
(DIFFERENCE
P (REMAINDER (TIMES (EXP A N) (FACT N)) P))
P)))
((USE (REMAINDER-EXP-LEMMA
(A P) (X (TIMES A N))
(Y (TIMES-LIST (REFLECTIONS (SUB1 N) A P)))
(Z (TIMES (EXP A (SUB1 N)) (FACT (SUB1 N))))))
(HANDS-OFF TIMES DIFFERENCE QUOTIENT EXP FACT)
(DISABLE REMAINDER-EXP-LEMMA)))
(PROVE-LEMMA REM-REFLECTIONS-3 (REWRITE)
(IMPLIES (AND (NOT (ZEROP P)) (NOT (ZEROP N))
(LEQ (REMAINDER (TIMES A N) P) (QUOTIENT P 2))
(EQUAL (REMAINDER
(TIMES-LIST (REFLECTIONS (SUB1 N) A P))
P)
(REMAINDER
(DIFFERENCE
P (REMAINDER (TIMES (EXP A (SUB1 N))
(FACT (SUB1 N)))
P))
P)))
(EQUAL (REMAINDER (TIMES-LIST (REFLECTIONS N A P)) P)
(REMAINDER
(DIFFERENCE
P (REMAINDER (TIMES (EXP A N) (FACT N)) P))
P)))
((USE (REMAINDER-EXP-LEMMA
(A P) (X (TIMES A N))
(Y (TIMES-LIST (REFLECTIONS (SUB1 N) A P)))
(Z (DIFFERENCE
P (REMAINDER (TIMES (EXP A (SUB1 N)) (FACT (SUB1 N)))
P)))))
(HANDS-OFF TIMES DIFFERENCE QUOTIENT EXP FACT)
(DISABLE REMAINDER-EXP-LEMMA)))
(PROVE-LEMMA DOUBLE-REFLECT (REWRITE)
(IMPLIES (LEQ A P)
(EQUAL (REMAINDER
(DIFFERENCE P (REMAINDER (DIFFERENCE P A) P))
P)
(REMAINDER A P))))
(PROVE-LEMMA REM-REFLECTIONS-4 (REWRITE)
(IMPLIES (AND (NOT (ZEROP P)) (NOT (ZEROP N))
(LESSP (QUOTIENT P 2) (REMAINDER (TIMES A N) P))
(EQUAL (REMAINDER
(TIMES-LIST (REFLECTIONS (SUB1 N) A P))
P)
(REMAINDER
(DIFFERENCE
P
(REMAINDER (TIMES (EXP A (SUB1 N))
(FACT (SUB1 N)))
P))
P)))
(EQUAL (REMAINDER (TIMES-LIST (REFLECTIONS N A P)) P)
(REMAINDER (TIMES (EXP A N) (FACT N)) P)))
((USE (REMAINDER-EXP-LEMMA
(A P) (X (TIMES A N))
(Y (TIMES-LIST (REFLECTIONS (SUB1 N) A P)))
(Z (DIFFERENCE
P
(REMAINDER (TIMES (EXP A (SUB1 N)) (FACT (SUB1 N)))
P)))))
(HANDS-OFF TIMES DIFFERENCE QUOTIENT EXP FACT)
(DISABLE REMAINDER-EXP-LEMMA)))
(PROVE-LEMMA REM-REFLECTIONS-BASE-CASE (REWRITE)
(IMPLIES (ZEROP N)
(EQUAL (REMAINDER (TIMES-LIST (REFLECTIONS N A P)) P)
(REMAINDER (TIMES (EXP A N) (FACT N)) P))))
(PROVE-LEMMA REM-REFLECTIONS NIL
(IMPLIES (NOT (ZEROP P))
(EQUAL (REMAINDER (TIMES-LIST (REFLECTIONS N A P)) P)
(IF (RES1 N A P)
(REMAINDER (TIMES (EXP A N) (FACT N)) P)
(REMAINDER
(DIFFERENCE
P (REMAINDER (TIMES (EXP A N) (FACT N)) P))
P))))
((HANDS-OFF TIMES-LIST REFLECTIONS QUOTIENT EXP FACT TIMES)))
(PROVE-LEMMA LENGTH-REFLECTIONS (REWRITE)
(EQUAL (LENGTH (REFLECTIONS N A P)) (FIX N))
((INDUCT (POSITIVES N))))
(PROVE-LEMMA ALL-LESSEQP-REFLECTIONS-1 (REWRITE)
(IMPLIES (LESSP (QUOTIENT P 2) X)
(NOT (LESSP (QUOTIENT P 2) (DIFFERENCE P X)))))
(PROVE-LEMMA ALL-LESSEQP-REFLECTIONS (REWRITE)
(ALL-LESSEQP (REFLECTIONS N A P) (QUOTIENT P 2)))
(PROVE-LEMMA ALL-NON-ZEROP-REFLECTIONS (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES P A)) (LESSP B P))
(ALL-NON-ZEROP (REFLECTIONS B A P)))
((INDUCT (REFLECTIONS B A P)) (DISABLE PRIME1)))
(PROVE-LEMMA ALL-DISTINCT-REFLECTIONS-1 (REWRITE)
(IMPLIES (AND (PRIME P) (LESSP J I)
(LESSP I P) (NOT (DIVIDES P A)))
(NOT (EQUAL (REMAINDER (TIMES A I) P)
(REMAINDER (TIMES A J) P))))
((DISABLE PRIME)))
(PROVE-LEMMA ALL-DISTINCT-REFLECTIONS-2 (REWRITE)
(IMPLIES (AND (NUMBERP X) (NUMBERP Y) (LESSP X P) (LESSP Y P))
(EQUAL (EQUAL (DIFFERENCE P X) (DIFFERENCE P Y))
(EQUAL X Y))))
(PROVE-LEMMA NUMBERP-REMAINDER (REWRITE)
(NUMBERP (REMAINDER A P)))
(PROVE-LEMMA ALL-DISTINCT-REFLECTIONS-3 (REWRITE)
(IMPLIES (AND (PRIME P) (LESSP J I)
(LESSP I P) (NOT (DIVIDES P A)))
(NOT (EQUAL (DIFFERENCE P (REMAINDER (TIMES A I) P))
(DIFFERENCE P (REMAINDER (TIMES A J) P)))))
((USE (ALL-DISTINCT-REFLECTIONS-1))
(HANDS-OFF DIFFERENCE REMAINDER TIMES)
(DISABLE ALL-DISTINCT-REFLECTIONS-1 PRIME)))
(PROVE-LEMMA PLUS-MOD-1 (REWRITE)
(EQUAL (REMAINDER (PLUS (REMAINDER X P) Y) P)
(REMAINDER (PLUS X Y) P))
((USE (REMAINDER-QUOTIENT (Y P))
(REMAINDER-PLUS-TIMES-1 (J P) (X (PLUS (REMAINDER X P) Y))
(I (QUOTIENT X P))))
(DISABLE REMAINDER-QUOTIENT REMAINDER-QUOTIENT-ELIM
REMAINDER-PLUS-TIMES-1)))
(PROVE-LEMMA PLUS-MOD-2 (REWRITE)
(EQUAL (REMAINDER (PLUS Y (REMAINDER X P)) P)
(REMAINDER (PLUS X Y) P))
((USE (PLUS-MOD-1)) (DISABLE PLUS-MOD-1)))
(PROVE-LEMMA ALL-DISTINCT-REFLECTIONS-4 NIL
(IMPLIES (AND (EQUAL X (DIFFERENCE P Y)) (LESSP Y P))
(EQUAL (REMAINDER (PLUS X Y) P) '0)))
(PROVE-LEMMA ALL-DISTINCT-REFLECTIONS-5 NIL
(IMPLIES (AND (EQUAL (REMAINDER (TIMES A I) P)
(DIFFERENCE P (REMAINDER (TIMES A J) P)))
(NOT (ZEROP P)))
(EQUAL (REMAINDER (TIMES A (PLUS I J)) P) '0))
((USE (ALL-DISTINCT-REFLECTIONS-4 (X (REMAINDER (TIMES A I) P))
(Y (REMAINDER (TIMES A J) P))))))
(PROVE-LEMMA ALL-DISTINCT-REFLECTIONS-6 NIL
(IMPLIES (AND (LEQ I (QUOTIENT P 2)) (LESSP J I))
(AND (NOT (ZEROP (PLUS I J))) (LESSP (PLUS I J) P))))
(PROVE-LEMMA ALL-DISTINCT-REFLECTIONS-7 (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES P A))
(LEQ I (QUOTIENT P 2)) (LESSP J I))
(NOT (EQUAL (REMAINDER (TIMES A I) P)
(DIFFERENCE P (REMAINDER (TIMES A J) P)))))
((USE (ALL-DISTINCT-REFLECTIONS-5) (ALL-DISTINCT-REFLECTIONS-6))
(HANDS-OFF DIFFERENCE TIMES PLUS) (DISABLE PRIME1)))
(PROVE-LEMMA ALL-DISTINCT-REFLECTIONS-8 (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES P A))
(LEQ I (QUOTIENT P 2)) (LESSP J I))
(NOT (EQUAL (DIFFERENCE P (REMAINDER (TIMES A I) P))
(REMAINDER (TIMES A J) P))))
((USE (ALL-DISTINCT-REFLECTIONS-5 (J I) (I J))
(ALL-DISTINCT-REFLECTIONS-6))
(HANDS-OFF TIMES DIFFERENCE) (DISABLE PRIME1)))
(PROVE-LEMMA ALL-DISTINCT-REFLECTIONS-9 (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES 2 P))
(NOT (DIVIDES P A)) (LEQ I (QUOTIENT P 2))
(LESSP J I))
(NOT (MEMBER (REMAINDER (TIMES A I) P)
(REFLECTIONS J A P))))
((USE (ALL-DISTINCT-REFLECTIONS-1)) (INDUCT (REFLECTIONS J A P))
(HANDS-OFF QUOTIENT REMAINDER TIMES)
(DISABLE PRIME1 ALL-DISTINCT-REFLECTIONS-1)))
(PROVE-LEMMA ALL-DISTINCT-REFLECTIONS-10 (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES 2 P))
(NOT (DIVIDES P A)) (LEQ I (QUOTIENT P 2))
(LESSP J I))
(NOT (MEMBER (DIFFERENCE P (REMAINDER (TIMES A I) P))
(REFLECTIONS J A P))))
((USE (ALL-DISTINCT-REFLECTIONS-3)) (INDUCT (REFLECTIONS J A P))
(HANDS-OFF QUOTIENT REMAINDER TIMES)
(DISABLE PRIME1 ALL-DISTINCT-REFLECTIONS-3)))
(PROVE-LEMMA ALL-DISTINCT-REFLECTIONS (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES 2 P))
(NOT (DIVIDES P A)) (LEQ I (QUOTIENT P 2)))
(ALL-DISTINCT (REFLECTIONS I A P)))
((USE (ALL-DISTINCT-REFLECTIONS-9 (J (SUB1 I)))
(ALL-DISTINCT-REFLECTIONS-10 (J (SUB1 I))))
(INDUCT (REFLECTIONS I A P))
(HANDS-OFF QUOTIENT REMAINDER TIMES)
(DISABLE ALL-DISTINCT-REFLECTIONS-9 ALL-DISTINCT-REFLECTIONS-10
PRIME DIVIDES)))
(PROVE-LEMMA TIMES-REFLECTIONS (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (DIVIDES 2 P)) (NOT (DIVIDES P A)))
(EQUAL (TIMES-LIST (REFLECTIONS (QUOTIENT P 2) A P))
(FACT (QUOTIENT P 2))))
((USE (PIGEON-HOLE-PRINCIPLE (L (REFLECTIONS (QUOTIENT P 2) A P))))
(HANDS-OFF QUOTIENT REMAINDER)
(DISABLE PRIME1 REFLECTIONS TIMES-LIST FACT)))
(PROVE-LEMMA PLUS-X-X-EVEN (REWRITE)
(EQUAL (REMAINDER (PLUS X X) 2) '0))
(PROVE-LEMMA RES1-REM-1-1 NIL
(IMPLIES (AND (NOT (ZEROP X)) (NOT (DIVIDES 2 P)))
(NOT (EQUAL (REMAINDER (DIFFERENCE P X) P) X)))
((USE (DIFFERENCE-ELIM (Y P)))))
(PROVE-LEMMA RES1-REM-1 NIL
(IMPLIES (AND (PRIME P) (NOT (DIVIDES 2 P))
(NOT (DIVIDES P A)) (RES1 (QUOTIENT P 2) A P))
(EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) 1))
((USE (REM-REFLECTIONS (N (QUOTIENT P 2)))
(PRIME-KEY-TRICK (M (FACT (QUOTIENT P 2)))
(A (EXP A (QUOTIENT P 2))) (B 1)))
(DISABLE PRIME-KEY-TRICK LESSP-REMAINDER-DIVISOR PRIME1)))
(PROVE-LEMMA REMAINDER-LESSP NIL
(IMPLIES (LESSP A P) (EQUAL (REMAINDER A P) (FIX A))))
(PROVE-LEMMA RES1-REM-2 NIL
(IMPLIES (AND (PRIME P) (NOT (DIVIDES 2 P))
(NOT (DIVIDES P A)) (NOT (RES1 (QUOTIENT P 2) A P)))
(NOT (EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) 1)))
((USE (REM-REFLECTIONS (N (QUOTIENT P 2)))
(REMAINDER-EXP-LEMMA (A P) (Y (EXP A (QUOTIENT P 2)))
(Z 1) (X (FACT (QUOTIENT P 2))))
(RES1-REM-1-1 (X (REMAINDER (FACT (QUOTIENT P 2)) P)))
(REMAINDER-LESSP (A 1)))
(HANDS-OFF FACT EXP QUOTIENT REMAINDER REFLECTIONS)
(DISABLE LESSP-REMAINDER-DIVISOR PRIME1 DIFFERENCE COROLLARY-55
REMAINDER-EXP-LEMMA)))
(PROVE-LEMMA TWO-EVEN NIL
(IMPLIES (NOT (DIVIDES 2 P)) (NOT (EQUAL (SUB1 P) 1)))
((INDUCT (ODD P))))
(PROVE-LEMMA PERM-REFLECTIONS NIL
(IMPLIES (AND (PRIME P) (NOT (EQUAL P 2)) (NOT (DIVIDES P A)))
(PERM (POSITIVES (QUOTIENT P 2))
(REFLECTIONS (QUOTIENT P 2) A P)))
((USE (PIGEON-HOLE-PRINCIPLE
(L (REFLECTIONS (QUOTIENT P 2) A P))))
(HANDS-OFF QUOTIENT REMAINDER) (DISABLE PRIME1 REFLECTIONS)))
(PROVE-LEMMA GAUSS-LEMMA-LEMMA NIL
(IMPLIES (AND (PRIME P) (NOT (DIVIDES P A)) (NOT (DIVIDES 2 P)))
(EQUAL (RES1 (QUOTIENT P 2) A P) (RESIDUE A P)))
((USE (EULER-CRITERION) (RES1-REM-1) (RES1-REM-2) (TWO-EVEN))
(DISABLE QUOTIENT EXP RESIDUE RES1 PRIME DIVIDES)))
(DEFN MU (N A P)
(IF (ZEROP N) T
(IF (LESSP (QUOTIENT P 2) (REMAINDER (TIMES A N) P))
(ADD1 (MU (SUB1 N) A P)) (MU (SUB1 N) A P))))
(DEFN GAUSS (A P) (EVEN (MU (QUOTIENT P 2) A P)))
(PROVE-LEMMA RES1-GAUSS (REWRITE)
(EQUAL (RES1 N A P) (EVEN (MU N A P)))
((DISABLE EVEN)))
(PROVE-LEMMA GAUSS-LEMMA NIL
(IMPLIES (AND (PRIME P) (NOT (EQUAL P 2)) (NOT (DIVIDES P A)))
(EQUAL (GAUSS A P) (RESIDUE A P)))
((USE (GAUSS-LEMMA-LEMMA))
(DISABLE PRIME QUOTIENT RESIDUE EVEN)))
(DEFN SUM (L)
(IF (LISTP L)
(PLUS (CAR L) (SUM (CDR L)))
0))
(DEFN QUOTIENTS (N A P)
(IF (ZEROP N)
NIL
(CONS (QUOTIENT (TIMES A N) P)
(QUOTIENTS (SUB1 N) A P))))
(DEFN REMAINDERS (N A P)
(IF (ZEROP N)
NIL
(CONS (REMAINDER (TIMES A N) P)
(REMAINDERS (SUB1 N) A P))))
(PROVE-LEMMA QUOTIENT-REMAINDER-SUM ()
(EQUAL (TIMES A (SUM (POSITIVES N)))
(PLUS (TIMES P (SUM (QUOTIENTS N A P)))
(SUM (REMAINDERS N A P)))))
(PROVE-LEMMA QUOTIENT-REMAINDER-SUM-PARITY ()
(EQUAL (EVEN (TIMES A (SUM (POSITIVES N))))
(EVEN (PLUS (TIMES P (SUM (QUOTIENTS N A P)))
(SUM (REMAINDERS N A P)))))
((USE (QUOTIENT-REMAINDER-SUM))))
(PROVE-LEMMA EVEN-MU (REWRITE)
(IMPLIES (NOT (EVEN P))
(EQUAL (EVEN (MU N A P))
(IFF (EVEN (SUM (REMAINDERS N A P)))
(EVEN (SUM (REFLECTIONS N A P))))))
((DISABLE EVEN)))
(PROVE-LEMMA PERM-SUM-LEMMA (REWRITE)
(IMPLIES (MEMBER X M)
(EQUAL (PLUS X (SUM (DELETE X M))) (SUM M))))
(PROVE-LEMMA PERM-SUM ()
(IMPLIES (PERM L M) (EQUAL (SUM L) (SUM M))))
(PROVE-LEMMA SUM-REFLECTIONS (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (EQUAL P 2)) (NOT (DIVIDES P A)))
(EQUAL (SUM (REFLECTIONS (QUOTIENT P 2) A P))
(SUM (POSITIVES (QUOTIENT P 2)))))
((USE (PERM-SUM (M (REFLECTIONS (QUOTIENT P 2) A P))
(L (POSITIVES (QUOTIENT P 2))))
(PERM-REFLECTIONS))
(DISABLE PRIME)))
(PROVE-LEMMA GAUSS-QUOTIENTS NIL
(IMPLIES (AND (PRIME P) (NOT (EQUAL P 2))
(NOT (EVEN A)) (NOT (DIVIDES P A)))
(EQUAL (GAUSS A P)
(EVEN (SUM (QUOTIENTS (QUOTIENT P 2) A P)))))
((USE (QUOTIENT-REMAINDER-SUM-PARITY (N (QUOTIENT P 2))))
(DISABLE PRIME EVEN)))
(PROVE-LEMMA EQUAL-RESIDUE-EVEN-PLUS (REWRITE)
(IMPLIES (AND (PRIME P) (NOT (EQUAL P 2))
(PRIME Q) (NOT (EQUAL Q 2))
(NOT (EQUAL P Q)))
(EQUAL (EQUAL (RESIDUE Q P) (RESIDUE P Q))
(EVEN (PLUS (SUM (QUOTIENTS (QUOTIENT P 2) Q P))
(SUM (QUOTIENTS (QUOTIENT Q 2) P Q))))))
((USE (GAUSS-LEMMA (A Q)) (GAUSS-LEMMA (A P) (P Q))
(GAUSS-QUOTIENTS (A Q)) (GAUSS-QUOTIENTS (A P) (P Q)))
(DISABLE PRIME1 EVEN GAUSS RESIDUE)))
(DEFN W (X L)
(IF (LISTP L)
(IF (LESSP (CAR L) X)
(ADD1 (W X (CDR L)))
(W X (CDR L)))
0))
(DEFN WINS (K L)
(IF (LISTP K)
(PLUS (W (CAR K) L) (WINS (CDR K) L))
0))
(DEFN ALL-NUMBERP (L)
(IF (LISTP L)
(AND (NUMBERP (CAR L)) (ALL-NUMBERP (CDR L)))
T))
(DEFN L (X L)
(IF (LISTP L)
(IF (LESSP X (CAR L))
(ADD1 (L X (CDR L)))
(L X (CDR L)))
0))
(DEFN LOSSES (K L)
(IF (LISTP K)
(PLUS (L (CAR K) L) (LOSSES (CDR K) L))
0))
(PROVE-LEMMA PLUS-L-W (REWRITE)
(IMPLIES (AND (NOT (MEMBER X L)) (NUMBERP X) (ALL-NUMBERP L))
(EQUAL (PLUS (L X L) (W X L))
(LENGTH L))))
(PROVE-LEMMA PLUS-WINS-LOSSES (REWRITE)
(IMPLIES (AND (NLISTP (INTERSECT L M))
(ALL-NUMBERP L) (ALL-NUMBERP M))
(EQUAL (PLUS (WINS L M) (LOSSES L M))
(TIMES (LENGTH L) (LENGTH M)))))
(PROVE-LEMMA EQUAL-WINS-LOSSES ()
(EQUAL (LOSSES L M) (WINS M L)))
(PROVE-LEMMA PLUS-WINS-WINS (REWRITE)
(IMPLIES (AND (NLISTP (INTERSECT L M))
(ALL-NUMBERP L) (ALL-NUMBERP M))
(EQUAL (PLUS (WINS L M) (WINS M L))
(TIMES (LENGTH L) (LENGTH M))))
((USE (EQUAL-WINS-LOSSES))))
(DEFN MULTS (N P)
(IF (ZEROP N) NIL (CONS (TIMES N P) (MULTS (SUB1 N) P))))
(PROVE-LEMMA ALL-NUMBERP-MULTS (REWRITE)
(IMPLIES (NOT (ZEROP P)) (ALL-NUMBERP (MULTS N P))))
(PROVE-LEMMA EMPTY-INTERSECT-MULTS-LEMMA (REWRITE)
(IMPLIES (AND (PRIME P) (PRIME Q) (NOT (EQUAL P Q))
(LESSP I Q) (LESSP J P))
(NOT (MEMBER (TIMES I P) (MULTS J Q))))
((INDUCT (MULTS J Q))))
(PROVE-LEMMA EMPTY-INTERSECT-MULTS (REWRITE)
(IMPLIES (AND (PRIME P) (PRIME Q) (NOT (EQUAL P Q))
(LESSP I Q))
(NOT (LISTP (INTERSECT (MULTS I P)
(MULTS (QUOTIENT P 2) Q)))))
((DISABLE PRIME1 QUOTIENT)
(INDUCT (MULTS I P))))
(PROVE-LEMMA LENGTH-MULTS (REWRITE)
(IMPLIES (NUMBERP N) (EQUAL (LENGTH (MULTS N P)) N)))
(PROVE-LEMMA LESSP-A ()
(IMPLIES (NOT (ZEROP P))
(LESSP A (TIMES (ADD1 (QUOTIENT A P)) P))))
(PROVE-LEMMA LEQ-W-N (REWRITE)
(NOT (LESSP N (W A (MULTS N P)))))
(PROVE-LEMMA LESSP-REWRITE (REWRITE)
(IMPLIES (AND (LESSP A (TIMES M P))
(LEQ M N))
(LESSP A (TIMES N P))))
(PROVE-LEMMA LESSP-W-M ()
(IMPLIES (LESSP A (TIMES M P))
(LESSP (W A (MULTS N P)) M)))
(PROVE-LEMMA LEQ-W-QUOTIENT ()
(IMPLIES (NOT (ZEROP P))
(LEQ (W A (MULTS N P)) (QUOTIENT A P)))
((USE (LESSP-A)
(LESSP-W-M (M (ADD1 (QUOTIENT A P)))))))
(PROVE-LEMMA MONOTONE-W NIL
(IMPLIES (LEQ M N)
(LEQ (W A (MULTS M P)) (W A (MULTS N P))))
((INDUCT (MULTS N P))))
(PROVE-LEMMA LEQ-N-W NIL
(IMPLIES (LESSP (TIMES N P) A)
(LEQ N (W A (MULTS N P))))
((INDUCT (MULTS N P))))
(PROVE-LEMMA LEQ-QUOTIENT-W ()
(IMPLIES (AND (NOT (ZEROP P))
(NOT (DIVIDES P A))
(LEQ (QUOTIENT A P) N))
(LEQ (QUOTIENT A P) (W A (MULTS N P))))
((USE (MONOTONE-W (M (QUOTIENT A P)))
(LEQ-N-W (N (QUOTIENT A P))))))
(DEFN LQQ-INDUCT (A B C D)
(IF (ZEROP B) T
(IF (ZEROP D) T
(IF (LESSP A D) T
(IF (LESSP C B) T
(LQQ-INDUCT (DIFFERENCE A D) B
(DIFFERENCE C B) D))))))
(PROVE-LEMMA LEQ-TIMES-QUOT NIL
(IMPLIES (AND (NOT (ZEROP B))
(LEQ (TIMES A B) (TIMES C D)))
(LEQ (QUOTIENT A D) (QUOTIENT C B)))
((INDUCT (LQQ-INDUCT A B C D))))
(PROVE-LEMMA LEQ-J-A ()
(IMPLIES (LEQ J A)
(LEQ (TIMES J Q) (TIMES A Q))))
(PROVE-LEMMA LEQ-QUOT-TIMES NIL
(IMPLIES (LEQ J (QUOTIENT P 2))
(LEQ (QUOTIENT (TIMES J Q) P) (QUOTIENT Q 2)))
((USE (LEQ-TIMES-QUOT (A (TIMES J Q)) (B 2) (C Q) (D P))
(LEQ-J-A (A (QUOTIENT P 2))))))
(PROVE-LEMMA EQUAL-QUOT-W (REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P Q))
(NOT (ZEROP J))
(LEQ J (QUOTIENT P 2)))
(EQUAL (W (TIMES J Q) (MULTS (QUOTIENT Q 2) P))
(QUOTIENT (TIMES J Q) P)))
((USE (LEQ-QUOTIENT-W (A (TIMES J Q)) (N (QUOTIENT Q 2)))
(LEQ-W-QUOTIENT (A (TIMES J Q)) (N (QUOTIENT Q 2)))
(LEQ-QUOT-TIMES))))
(PROVE-LEMMA EQUAL-WINS-SUM-QUOTIENTS (REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (DIVIDES P Q))
(LEQ J (QUOTIENT P 2)))
(EQUAL (SUM (QUOTIENTS J Q P))
(WINS (MULTS J Q) (MULTS (QUOTIENT Q 2) P))))
((INDUCT (MULTS J Q))))
(PROVE-LEMMA LAW-OF-QUADRATIC-RECIPROCITY ()
(IMPLIES (AND (PRIME P) (NOT (EQUAL P 2))
(PRIME Q) (NOT (EQUAL Q 2))
(NOT (EQUAL P Q)))
(EQUAL (EQUAL (RESIDUE Q P) (RESIDUE P Q))
(EVEN (TIMES (QUOTIENT P 2) (QUOTIENT Q 2)))))
((DISABLE RESIDUE INTERSECT)))