(NOTE-LIB "wilson" T) Loading ./basic/wilson.lib Finished loading ./basic/wilson.lib Loading ./basic/wilson.o Finished loading ./basic/wilson.o (#./basic/wilson.lib #./basic/wilson) (DEFN SQUARES (N P) (IF (ZEROP N) (CONS 0 NIL) (CONS (REMAINDER (TIMES N N) P) (SQUARES (SUB1 N) P)))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT N) decreases according to the well-founded relation LESSP in each recursive call. Hence, SQUARES is accepted under the principle of definition. From the definition we can conclude that (LISTP (SQUARES N P)) is a theorem. [ 0.0 0.0 0.0 ] SQUARES (DEFN RESIDUE (A P) (MEMBER (REMAINDER A P) (SQUARES P P))) Observe that (OR (FALSEP (RESIDUE A P)) (TRUEP (RESIDUE A P))) is a theorem. [ 0.0 0.0 0.0 ] RESIDUE (PROVE-LEMMA ALL-SQUARES-1 NIL (IMPLIES (AND (NOT (ZEROP P)) (LEQ M N)) (MEMBER (REMAINDER (TIMES M M) P) (SQUARES N P)))) This formula can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL P 0)) (NUMBERP P) (NOT (LESSP N M))) (MEMBER (REMAINDER (TIMES M M) P) (SQUARES N P))), which we will name *1. Perhaps we can prove it by induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP N) (p M P N)) (IMPLIES (AND (NOT (ZEROP N)) (p M P (SUB1 N))) (p M P N))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us that the measure (COUNT N) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates the following three new formulas: Case 3. (IMPLIES (AND (ZEROP N) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (LESSP N M))) (MEMBER (REMAINDER (TIMES M M) P) (SQUARES N P))). This simplifies, rewriting with REMAINDER-0-CROCK and TIMES-ZERO2, and opening up ZEROP, EQUAL, LESSP, TIMES, SQUARES, and MEMBER, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP N)) (LESSP (SUB1 N) M) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (LESSP N M))) (MEMBER (REMAINDER (TIMES M M) P) (SQUARES N P))), which simplifies, using linear arithmetic, to three new goals: Case 2.3. (IMPLIES (AND (NOT (NUMBERP N)) (NOT (ZEROP N)) (LESSP (SUB1 N) M) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (LESSP N M))) (MEMBER (REMAINDER (TIMES M M) P) (SQUARES N P))), which again simplifies, unfolding the function ZEROP, to: T. Case 2.2. (IMPLIES (AND (NOT (NUMBERP M)) (NOT (ZEROP N)) (LESSP (SUB1 N) M) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (LESSP N M))) (MEMBER (REMAINDER (TIMES M M) P) (SQUARES N P))), which again simplifies, expanding the functions ZEROP and LESSP, to: T. Case 2.1. (IMPLIES (AND (NUMBERP M) (NUMBERP N) (NOT (ZEROP M)) (LESSP (SUB1 M) M) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (LESSP M M))) (MEMBER (REMAINDER (TIMES M M) P) (SQUARES M P))), which again simplifies, expanding the function ZEROP, to: (IMPLIES (AND (NUMBERP M) (NUMBERP N) (NOT (EQUAL M 0)) (LESSP (SUB1 M) M) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (LESSP M M))) (MEMBER (REMAINDER (TIMES M M) P) (SQUARES M P))). Appealing to the lemma SUB1-ELIM, we now replace M by (ADD1 X) to eliminate (SUB1 M). We employ the type restriction lemma noted when SUB1 was introduced to constrain the new variable. We must thus prove the conjecture: (IMPLIES (AND (NUMBERP X) (NUMBERP N) (NOT (EQUAL (ADD1 X) 0)) (LESSP X (ADD1 X)) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (LESSP (ADD1 X) (ADD1 X)))) (MEMBER (REMAINDER (TIMES (ADD1 X) (ADD1 X)) P) (SQUARES (ADD1 X) P))). This further simplifies, applying SUB1-ADD1, REMAINDER-OF-1, CAR-CONS, TIMES-ADD1, COMMUTATIVITY-OF-TIMES, PLUS-ADD1, and COMMUTATIVITY2-OF-PLUS, and opening up LESSP, ADD1, TIMES, SUB1, NUMBERP, EQUAL, SQUARES, MEMBER, and PLUS, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP N)) (MEMBER (REMAINDER (TIMES M M) P) (SQUARES (SUB1 N) P)) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (LESSP N M))) (MEMBER (REMAINDER (TIMES M M) P) (SQUARES N P))). This simplifies, rewriting with CDR-CONS and CAR-CONS, and unfolding ZEROP, SQUARES, and MEMBER, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.3 0.0 ] ALL-SQUARES-1 (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))) This conjecture simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] ALL-SQUARES-2 (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))) This formula can be simplified, using the abbreviations ZEROP, NOT, IMPLIES, and AND, to the new goal: (IMPLIES (AND (IMPLIES (AND (NOT (ZEROP P)) (IF (LESSP P (REMAINDER Y P)) F T)) (MEMBER (REMAINDER (TIMES (REMAINDER Y P) (REMAINDER Y P)) P) (SQUARES P P))) (EQUAL (REMAINDER (TIMES Y Y) P) (REMAINDER (TIMES (REMAINDER Y P) (REMAINDER Y P)) P)) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (MEMBER X (SQUARES P P)))) (NOT (EQUAL X (REMAINDER (TIMES Y Y) P)))), which simplifies, opening up ZEROP, NOT, AND, and IMPLIES, to: (IMPLIES (AND (LESSP P (REMAINDER Y P)) (EQUAL (REMAINDER (TIMES Y Y) P) (REMAINDER (TIMES (REMAINDER Y P) (REMAINDER Y P)) P)) (NOT (EQUAL P 0)) (NUMBERP P)) (MEMBER (REMAINDER (TIMES Y Y) P) (SQUARES P P))). This again simplifies, using linear arithmetic and rewriting with the lemma LESSP-REMAINDER-DIVISOR, to: T. Q.E.D. [ 0.0 0.3 0.0 ] ALL-SQUARES (PROVE-LEMMA EULER-1-1 NIL (IMPLIES (NOT (DIVIDES 2 P)) (EQUAL (TIMES 2 (QUOTIENT P 2)) (SUB1 P)))) This formula can be simplified, using the abbreviations NOT, IMPLIES, and DIVIDES, to the new formula: (IMPLIES (NOT (EQUAL (REMAINDER P 2) 0)) (EQUAL (TIMES 2 (QUOTIENT P 2)) (SUB1 P))), which simplifies, using linear arithmetic, appealing to the lemma LESSP-REMAINDER-DIVISOR, and unfolding the function EQUAL, to: (IMPLIES (AND (EQUAL (REMAINDER P 2) 1) (NOT (EQUAL 1 0))) (EQUAL (TIMES 2 (QUOTIENT P 2)) (SUB1 P))). This again simplifies, rewriting with the lemma TIMES-2, and opening up EQUAL, to: (IMPLIES (EQUAL (REMAINDER P 2) 1) (EQUAL (PLUS (QUOTIENT P 2) (QUOTIENT P 2)) (SUB1 P))). Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace P by (PLUS X (TIMES 2 Z)) to eliminate (REMAINDER P 2) and (QUOTIENT P 2). We employ LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to constrain the new variables. We must thus prove four new goals: Case 4. (IMPLIES (AND (NOT (NUMBERP P)) (EQUAL (REMAINDER P 2) 1)) (EQUAL (PLUS (QUOTIENT P 2) (QUOTIENT P 2)) (SUB1 P))), which further simplifies, opening up the functions LESSP, NUMBERP, EQUAL, and REMAINDER, to: T. Case 3. (IMPLIES (AND (EQUAL 2 0) (EQUAL (REMAINDER P 2) 1)) (EQUAL (PLUS (QUOTIENT P 2) (QUOTIENT P 2)) (SUB1 P))), which further simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP 2)) (EQUAL (REMAINDER P 2) 1)) (EQUAL (PLUS (QUOTIENT P 2) (QUOTIENT P 2)) (SUB1 P))), which further simplifies, obviously, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP X 2) (NOT (ZEROP 2))) (NUMBERP Z) (NOT (EQUAL 2 0)) (EQUAL X 1)) (EQUAL (PLUS Z Z) (SUB1 (PLUS X (TIMES 2 Z))))). But this further simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (PLUS 1 (TIMES 2 Z)) 0) (NUMBERP 1) (EQUAL (LESSP 1 2) (NOT (ZEROP 2))) (NUMBERP Z) (NOT (EQUAL 2 0))) (EQUAL (PLUS Z Z) (SUB1 (PLUS 1 (TIMES 2 Z))))). But this again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.1 0.0 ] EULER-1-1 (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))) This conjecture can be simplified, using the abbreviations NOT, IMPLIES, AND, and DIVIDES, to: (IMPLIES (AND (EQUAL (EXP (EXP I 2) (QUOTIENT P 2)) (EXP I (TIMES 2 (QUOTIENT P 2)))) (IMPLIES (NOT (EQUAL (REMAINDER P 2) 0)) (EQUAL (TIMES 2 (QUOTIENT P 2)) (SUB1 P))) (NOT (EQUAL (REMAINDER P 2) 0))) (EQUAL (EXP (TIMES I I) (QUOTIENT P 2)) (EXP I (SUB1 P)))). This simplifies, using linear arithmetic, applying LESSP-REMAINDER-DIVISOR, and unfolding the definition of EQUAL, to the conjecture: (IMPLIES (AND (EQUAL (REMAINDER P 2) 1) (EQUAL (EXP (EXP I 2) (QUOTIENT P 2)) (EXP I (TIMES 2 (QUOTIENT P 2)))) (IMPLIES (NOT (EQUAL 1 0)) (EQUAL (TIMES 2 (QUOTIENT P 2)) (SUB1 P))) (NOT (EQUAL 1 0))) (EQUAL (EXP (TIMES I I) (QUOTIENT P 2)) (EXP I (SUB1 P)))). However this again simplifies, rewriting with TIMES-2, EXP-PLUS, and EXP-TIMES, and opening up the definitions of EQUAL, NOT, and IMPLIES, to: (IMPLIES (AND (EQUAL (REMAINDER P 2) 1) (EQUAL (EXP (EXP I 2) (QUOTIENT P 2)) (TIMES (EXP I (QUOTIENT P 2)) (EXP I (QUOTIENT P 2)))) (EQUAL (PLUS (QUOTIENT P 2) (QUOTIENT P 2)) (SUB1 P))) (EQUAL (EXP (EXP I 2) (QUOTIENT P 2)) (EXP I (SUB1 P)))). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace P by (PLUS X (TIMES 2 Z)) to eliminate (REMAINDER P 2) and (QUOTIENT P 2). We employ LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to restrict the new variables. We thus obtain the following four new formulas: Case 4. (IMPLIES (AND (NOT (NUMBERP P)) (EQUAL (REMAINDER P 2) 1) (EQUAL (EXP (EXP I 2) (QUOTIENT P 2)) (TIMES (EXP I (QUOTIENT P 2)) (EXP I (QUOTIENT P 2)))) (EQUAL (PLUS (QUOTIENT P 2) (QUOTIENT P 2)) (SUB1 P))) (EQUAL (EXP (EXP I 2) (QUOTIENT P 2)) (EXP I (SUB1 P)))). This further simplifies, unfolding LESSP, NUMBERP, EQUAL, and REMAINDER, to: T. Case 3. (IMPLIES (AND (EQUAL 2 0) (EQUAL (REMAINDER P 2) 1) (EQUAL (EXP (EXP I 2) (QUOTIENT P 2)) (TIMES (EXP I (QUOTIENT P 2)) (EXP I (QUOTIENT P 2)))) (EQUAL (PLUS (QUOTIENT P 2) (QUOTIENT P 2)) (SUB1 P))) (EQUAL (EXP (EXP I 2) (QUOTIENT P 2)) (EXP I (SUB1 P)))), which further simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP 2)) (EQUAL (REMAINDER P 2) 1) (EQUAL (EXP (EXP I 2) (QUOTIENT P 2)) (TIMES (EXP I (QUOTIENT P 2)) (EXP I (QUOTIENT P 2)))) (EQUAL (PLUS (QUOTIENT P 2) (QUOTIENT P 2)) (SUB1 P))) (EQUAL (EXP (EXP I 2) (QUOTIENT P 2)) (EXP I (SUB1 P)))), which further simplifies, trivially, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (EQUAL (LESSP X 2) (NOT (ZEROP 2))) (NUMBERP Z) (NOT (EQUAL 2 0)) (EQUAL X 1) (EQUAL (EXP (EXP I 2) Z) (TIMES (EXP I Z) (EXP I Z))) (EQUAL (PLUS Z Z) (SUB1 (PLUS X (TIMES 2 Z))))) (EQUAL (EXP (EXP I 2) Z) (EXP I (SUB1 (PLUS X (TIMES 2 Z)))))). But this further simplifies, applying TIMES-2 and EXP-PLUS, and expanding the definitions of NUMBERP, LESSP, ZEROP, NOT, and EQUAL, to: T. Q.E.D. [ 0.0 0.1 0.0 ] EULER-1-2 (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))) This conjecture simplifies, clearly, to: T. Q.E.D. [ 0.0 0.1 0.0 ] EULER-1-3 (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))) This formula can be simplified, using the abbreviations NOT, AND, IMPLIES, and DIVIDES, to: (IMPLIES (AND (IMPLIES (NOT (EQUAL (REMAINDER P 2) 0)) (EQUAL (EXP (TIMES I I) (QUOTIENT P 2)) (EXP I (SUB1 P)))) (PRIME P) (NOT (EQUAL (REMAINDER P 2) 0)) (NOT (EQUAL (REMAINDER I P) 0))) (EQUAL (REMAINDER (EXP (TIMES I I) (QUOTIENT P 2)) P) 1)), which simplifies, applying EXP-TIMES and FERMAT-THM, and opening up the functions NOT, IMPLIES, and EQUAL, to: T. Q.E.D. [ 0.0 0.1 0.0 ] EULER-1-4 (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))) This formula can be simplified, using the abbreviations NOT, AND, IMPLIES, and DIVIDES, to: (IMPLIES (AND (IMPLIES (PRIME P) (EQUAL (EQUAL (REMAINDER (TIMES I I) P) 0) (OR (EQUAL (REMAINDER I P) 0) (EQUAL (REMAINDER I P) 0)))) (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (REMAINDER A P) (REMAINDER (TIMES I I) P))) (NOT (EQUAL (REMAINDER I P) 0))), which simplifies, expanding the functions EQUAL, OR, and IMPLIES, to: T. Q.E.D. [ 0.0 0.1 0.0 ] EULER-1-5 (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))) This conjecture can be simplified, using the abbreviations NOT, IMPLIES, AND, and DIVIDES, to the goal: (IMPLIES (AND (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER P 2) 0)) (NOT (EQUAL (REMAINDER I P) 0))) (EQUAL (REMAINDER (EXP (TIMES I I) (QUOTIENT P 2)) P) 1)) (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (REMAINDER A P) (REMAINDER (TIMES I I) P))) (NOT (EQUAL (REMAINDER I P) 0))) (IMPLIES (EQUAL (REMAINDER A P) (REMAINDER (TIMES I I) P)) (EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) (REMAINDER (EXP (TIMES I I) (QUOTIENT P 2)) P))) (PRIME P) (NOT (EQUAL (REMAINDER P 2) 0)) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (REMAINDER A P) (REMAINDER (TIMES I I) P))) (EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) 1)). This simplifies, rewriting with EXP-TIMES, and expanding NOT, AND, IMPLIES, and EQUAL, to: T. Q.E.D. [ 0.0 0.1 0.0 ] EULER-1-6 (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))) WARNING: Note that EULER-1-7 contains the free variable I which will be chosen by instantiating the hypothesis (MEMBER (REMAINDER A P) (SQUARES I P)). This formula can be simplified, using the abbreviation DIVIDES, to: (IMPLIES (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER P 2) 0)) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (REMAINDER A P) (REMAINDER (TIMES I I) P))) (EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) 1)) (AND (OR (NOT (ZEROP I)) (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER P 2) 0)) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER (REMAINDER A P) (SQUARES I P))) (EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) 1))) (OR (ZEROP I) (NOT (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER P 2) 0)) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER (REMAINDER A P) (SQUARES (SUB1 I) P))) (EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) 1))) (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER P 2) 0)) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER (REMAINDER A P) (SQUARES I P))) (EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) 1))))), which simplifies, opening up NOT, AND, IMPLIES, ZEROP, SQUARES, OR, and EQUAL, to three new goals: Case 3. (IMPLIES (AND (NOT (EQUAL (REMAINDER A P) (REMAINDER (TIMES I I) P))) (NOT (NUMBERP I)) (PRIME P) (NOT (EQUAL (REMAINDER P 2) 0)) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER (REMAINDER A P) '(0))) (EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) 1)), which again simplifies, rewriting with TIMES-ZERO2 and REMAINDER-0-CROCK, and unfolding the definitions of CDR, CAR, LISTP, and MEMBER, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL (REMAINDER A P) (REMAINDER (TIMES I I) P))) (EQUAL I 0) (PRIME P) (NOT (EQUAL (REMAINDER P 2) 0)) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER (REMAINDER A P) '(0))) (EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) 1)). However this again simplifies, applying REMAINDER-0-CROCK, and expanding the functions TIMES, CDR, CAR, LISTP, and MEMBER, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL (REMAINDER A P) (REMAINDER (TIMES I I) P))) (NOT (EQUAL I 0)) (NUMBERP I) (PRIME P) (NOT (EQUAL (REMAINDER P 2) 0)) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES (SUB1 I) P))) (MEMBER (REMAINDER A P) (CONS (REMAINDER (TIMES I I) P) (SQUARES (SUB1 I) P)))) (EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) 1)). However this again simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS, and unfolding the function MEMBER, to: T. Q.E.D. [ 0.0 0.2 0.0 ] EULER-1-7 (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))) This formula can be simplified, using the abbreviations NOT, AND, IMPLIES, and DIVIDES, to: (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER P 2) 0)) (NOT (EQUAL (REMAINDER A P) 0)) (RESIDUE A P)) (EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) 1)), which simplifies, using linear arithmetic, appealing to the lemma LESSP-REMAINDER-DIVISOR, and unfolding EQUAL, to the conjecture: (IMPLIES (AND (EQUAL (REMAINDER P 2) 1) (PRIME P) (NOT (EQUAL 1 0)) (NOT (EQUAL (REMAINDER A P) 0)) (RESIDUE A P)) (EQUAL (REMAINDER (EXP A (QUOTIENT P 2)) P) 1)). But this again simplifies, using linear arithmetic, rewriting with the lemmas B-I-LEMMA2 and EULER-1-7, and opening up the definitions of EQUAL, RESIDUE, DIVIDES, SUB1, INVERSE, and PRIME, to: T. Q.E.D. [ 0.0 0.1 0.0 ] EULER-1 (DEFN COMPLEMENT (J A P) (REMAINDER (TIMES (INVERSE J P) A) P)) Note that (NUMBERP (COMPLEMENT J A P)) is a theorem. [ 0.0 0.0 0.0 ] COMPLEMENT (DISABLE INVERSE) [ 0.0 0.0 0.0 ] INVERSE-OFF (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))) This conjecture can be simplified, using the abbreviations NOT, IMPLIES, AND, DIVIDES, and ASSOCIATIVITY-OF-TIMES, to: (IMPLIES (AND (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER J P) 0))) (EQUAL (REMAINDER (TIMES (INVERSE J P) J) P) 1)) (EQUAL (REMAINDER (TIMES (REMAINDER (TIMES J (INVERSE J P)) P) A) P) (REMAINDER (TIMES J (INVERSE J P) A) P)) (PRIME P) (NOT (EQUAL (REMAINDER J P) 0))) (EQUAL (REMAINDER (TIMES J (COMPLEMENT J A P)) P) (REMAINDER A P))). This simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES, INVERSE-IS-UNIQUE, TIMES-MOD-1, TIMES-1, COMMUTATIVITY2-OF-TIMES, TIMES-MOD-2, and EQUAL-TIMES-0, and unfolding NOT, AND, IMPLIES, REMAINDER, LESSP, and COMPLEMENT, to: T. Q.E.D. [ 0.0 0.9 0.0 ] COMPLEMENT-WORKS (PROVE-LEMMA BOUNDED-COMPLEMENT (REWRITE) (IMPLIES (NOT (ZEROP P)) (LESSP (COMPLEMENT J A P) P))) WARNING: Note that the linear lemma BOUNDED-COMPLEMENT is being stored under the term (COMPLEMENT J A P), which is unusual because COMPLEMENT is a nonrecursive function symbol. WARNING: Note that the proposed lemma BOUNDED-COMPLEMENT is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This conjecture can be simplified, using the abbreviations ZEROP, NOT, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL P 0)) (NUMBERP P)) (LESSP (COMPLEMENT J A P) P)). This simplifies, applying COMMUTATIVITY-OF-TIMES and LESSP-REMAINDER2, and unfolding the function COMPLEMENT, to: T. Q.E.D. [ 0.0 0.0 0.0 ] BOUNDED-COMPLEMENT (DISABLE COMPLEMENT) [ 0.0 0.0 0.0 ] COMPLEMENT-OFF (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))) WARNING: Note that the rewrite rule NON-ZEROP-COMPLEMENT will be stored so as to apply only to terms with the nonrecursive function symbol ZEROP. This conjecture can be simplified, using the abbreviations NOT, AND, IMPLIES, and DIVIDES, to: (IMPLIES (AND (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER J P) 0))) (EQUAL (REMAINDER (TIMES J (COMPLEMENT J A P)) P) (REMAINDER A P))) (PRIME P) (NOT (EQUAL (REMAINDER J P) 0)) (NOT (EQUAL (REMAINDER A P) 0))) (NOT (ZEROP (COMPLEMENT J A P)))). This simplifies, opening up the definitions of NOT, AND, IMPLIES, and ZEROP, to: (IMPLIES (AND (EQUAL (REMAINDER (TIMES J (COMPLEMENT J A P)) P) (REMAINDER A P)) (PRIME P) (NOT (EQUAL (REMAINDER J P) 0)) (NOT (EQUAL (REMAINDER A P) 0))) (NOT (EQUAL (COMPLEMENT J A P) 0))), which again simplifies, rewriting with the lemmas COMMUTATIVITY-OF-TIMES and TIMES-IDENTITY, and expanding LESSP, EQUAL, and REMAINDER, to: T. Q.E.D. [ 0.0 0.1 0.0 ] NON-ZEROP-COMPLEMENT (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))) WARNING: Note that COMPLEMENT-IS-UNIQUE contains the free variable X which will be chosen by instantiating the hypothesis: (EQUAL (REMAINDER (TIMES J X) P) (REMAINDER A P)). This formula can be simplified, using the abbreviations NOT, IMPLIES, AND, and DIVIDES, to: (IMPLIES (AND (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER J P) 0))) (EQUAL (REMAINDER (TIMES J (COMPLEMENT J A P)) P) (REMAINDER A P))) (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER J P) 0))) (EQUAL (EQUAL (REMAINDER (TIMES J X) P) (REMAINDER (TIMES J (COMPLEMENT J A P)) P)) (EQUAL (REMAINDER X P) (REMAINDER (COMPLEMENT J A P) P)))) (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (REMAINDER (TIMES J X) P) (REMAINDER A P))) (EQUAL (COMPLEMENT J A P) (REMAINDER X P))), which simplifies, using linear arithmetic, rewriting with REMAINDER-0-CROCK, DIFFERENCE-0, and BOUNDED-COMPLEMENT, and expanding the functions NOT, AND, IMPLIES, EQUAL, and REMAINDER, to the following three new formulas: Case 3. (IMPLIES (AND (EQUAL (REMAINDER J P) 0) (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (REMAINDER (TIMES J X) P) (REMAINDER A P))) (EQUAL (COMPLEMENT J A P) (REMAINDER X P))). Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace J by (PLUS Z (TIMES P V)) to eliminate (REMAINDER J P) and (QUOTIENT J P). We employ LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when QUOTIENT was introduced to constrain the new variables. We must thus prove four new goals: Case 3.4. (IMPLIES (AND (NOT (NUMBERP J)) (EQUAL (REMAINDER J P) 0) (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (REMAINDER (TIMES J X) P) (REMAINDER A P))) (EQUAL (COMPLEMENT J A P) (REMAINDER X P))), which further simplifies, rewriting with EQUAL-TIMES-0, and opening up the definitions of LESSP, REMAINDER, and EQUAL, to: (IMPLIES (AND (NOT (NUMBERP J)) (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (TIMES J X) (REMAINDER A P))) (EQUAL (COMPLEMENT J A P) (REMAINDER X P))). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by (PLUS Z (TIMES P V)) 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 thus obtain the following four new goals: Case 3.4.4. (IMPLIES (AND (NOT (NUMBERP A)) (NOT (NUMBERP J)) (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (TIMES J X) (REMAINDER A P))) (EQUAL (COMPLEMENT J A P) (REMAINDER X P))). This further simplifies, expanding LESSP, REMAINDER, and EQUAL, to: T. Case 3.4.3. (IMPLIES (AND (EQUAL P 0) (NOT (NUMBERP J)) (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (TIMES J X) (REMAINDER A P))) (EQUAL (COMPLEMENT J A P) (REMAINDER X P))), which further simplifies, expanding the definition of PRIME, to: T. Case 3.4.2. (IMPLIES (AND (NOT (NUMBERP P)) (NOT (NUMBERP J)) (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (TIMES J X) (REMAINDER A P))) (EQUAL (COMPLEMENT J A P) (REMAINDER X P))), which further simplifies, applying REMAINDER-WRT-12, to the following two new formulas: Case 3.4.2.2. (IMPLIES (AND (NOT (NUMBERP P)) (NOT (NUMBERP J)) (PRIME P) (NUMBERP A) (NOT (EQUAL A 0)) (EQUAL (TIMES J X) A) (NOT (NUMBERP X))) (EQUAL (COMPLEMENT J A P) 0)). But this finally simplifies, appealing to the lemma TIMES-ZERO2, and unfolding the functions NUMBERP and EQUAL, to: T. Case 3.4.2.1. (IMPLIES (AND (NOT (NUMBERP P)) (NOT (NUMBERP J)) (PRIME P) (NUMBERP A) (NOT (EQUAL A 0)) (EQUAL (TIMES J X) A) (NUMBERP X)) (EQUAL (COMPLEMENT J A P) X)), which finally simplifies, applying EQUAL-TIMES-0, to: T. Case 3.4.1. (IMPLIES (AND (NUMBERP Z) (EQUAL (LESSP Z P) (NOT (ZEROP P))) (NUMBERP V) (NUMBERP P) (NOT (EQUAL P 0)) (NOT (NUMBERP J)) (PRIME P) (NOT (EQUAL Z 0)) (EQUAL (TIMES J X) Z)) (EQUAL (COMPLEMENT J (PLUS Z (TIMES P V)) P) (REMAINDER X P))). However this further simplifies, applying EQUAL-TIMES-0, and opening up LESSP, ZEROP, NOT, and EQUAL, to: T. Case 3.3. (IMPLIES (AND (EQUAL P 0) (EQUAL (REMAINDER J P) 0) (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (REMAINDER (TIMES J X) P) (REMAINDER A P))) (EQUAL (COMPLEMENT J A P) (REMAINDER X P))). But this further simplifies, opening up EQUAL, REMAINDER, and PRIME, to: T. Case 3.2. (IMPLIES (AND (NOT (NUMBERP P)) (EQUAL (REMAINDER J P) 0) (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (REMAINDER (TIMES J X) P) (REMAINDER A P))) (EQUAL (COMPLEMENT J A P) (REMAINDER X P))), which further simplifies, rewriting with REMAINDER-WRT-12, to the following four new goals: Case 3.2.4. (IMPLIES (AND (NOT (NUMBERP P)) (EQUAL J 0) (PRIME P) (NUMBERP A) (NOT (EQUAL A 0)) (EQUAL (TIMES 0 X) A) (NOT (NUMBERP X))) (EQUAL (COMPLEMENT 0 A P) 0)). However this again simplifies, using linear arithmetic, to: T. Case 3.2.3. (IMPLIES (AND (NOT (NUMBERP P)) (EQUAL J 0) (PRIME P) (NUMBERP A) (NOT (EQUAL A 0)) (EQUAL (TIMES 0 X) A) (NUMBERP X)) (EQUAL (COMPLEMENT 0 A P) X)), which again simplifies, using linear arithmetic, to: T. Case 3.2.2. (IMPLIES (AND (NOT (NUMBERP P)) (NOT (NUMBERP J)) (PRIME P) (NUMBERP A) (NOT (EQUAL A 0)) (EQUAL (TIMES J X) A) (NOT (NUMBERP X))) (EQUAL (COMPLEMENT J A P) 0)), which again simplifies, rewriting with TIMES-ZERO2, and opening up the functions NUMBERP and EQUAL, to: T. Case 3.2.1. (IMPLIES (AND (NOT (NUMBERP P)) (NOT (NUMBERP J)) (PRIME P) (NUMBERP A) (NOT (EQUAL A 0)) (EQUAL (TIMES J X) A) (NUMBERP X)) (EQUAL (COMPLEMENT J A P) X)). However this again simplifies, rewriting with the lemma EQUAL-TIMES-0, to: T. Case 3.1. (IMPLIES (AND (NUMBERP Z) (EQUAL (LESSP Z P) (NOT (ZEROP P))) (NUMBERP V) (NUMBERP P) (NOT (EQUAL P 0)) (EQUAL Z 0) (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (REMAINDER (TIMES (PLUS Z (TIMES P V)) X) P) (REMAINDER A P))) (EQUAL (COMPLEMENT (PLUS Z (TIMES P V)) A P) (REMAINDER X P))), which further simplifies, rewriting with the lemmas ASSOCIATIVITY-OF-TIMES and REMAINDER-TIMES, and expanding the functions NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to: T. Case 2. (IMPLIES (AND (EQUAL (REMAINDER (TIMES J (COMPLEMENT J A P)) P) (REMAINDER A P)) (EQUAL (REMAINDER J P) 0) (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (REMAINDER (TIMES J X) P) (REMAINDER A P))) (EQUAL (COMPLEMENT J A P) (REMAINDER X P))). Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by (PLUS Z (TIMES P V)) to eliminate (REMAINDER A P) and (QUOTIENT A 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 would thus like to prove the following four new goals: Case 2.4. (IMPLIES (AND (NOT (NUMBERP A)) (EQUAL (REMAINDER (TIMES J (COMPLEMENT J A P)) P) (REMAINDER A P)) (EQUAL (REMAINDER J P) 0) (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (REMAINDER (TIMES J X) P) (REMAINDER A P))) (EQUAL (COMPLEMENT J A P) (REMAINDER X P))). However this further simplifies, applying PRIME-KEY-REWRITE, and opening up LESSP, REMAINDER, and EQUAL, to: T. Case 2.3. (IMPLIES (AND (EQUAL P 0) (EQUAL (REMAINDER (TIMES J (COMPLEMENT J A P)) P) (REMAINDER A P)) (EQUAL (REMAINDER J P) 0) (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (REMAINDER (TIMES J X) P) (REMAINDER A P))) (EQUAL (COMPLEMENT J A P) (REMAINDER X P))). However this further simplifies, unfolding the definitions of EQUAL, REMAINDER, and PRIME, to: T. Case 2.2. (IMPLIES (AND (NOT (NUMBERP P)) (EQUAL (REMAINDER (TIMES J (COMPLEMENT J A P)) P) (REMAINDER A P)) (EQUAL (REMAINDER J P) 0) (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (REMAINDER (TIMES J X) P) (REMAINDER A P))) (EQUAL (COMPLEMENT J A P) (REMAINDER X P))), which further simplifies, applying the lemma REMAINDER-WRT-12, and unfolding EQUAL, to four new formulas: Case 2.2.4. (IMPLIES (AND (NOT (NUMBERP P)) (NUMBERP A) (EQUAL (TIMES J (COMPLEMENT J A P)) A) (EQUAL J 0) (PRIME P) (NOT (EQUAL A 0)) (EQUAL (TIMES 0 X) A) (NOT (NUMBERP X))) (EQUAL (COMPLEMENT 0 A P) 0)), which again simplifies, using linear arithmetic, to: T. Case 2.2.3. (IMPLIES (AND (NOT (NUMBERP P)) (NUMBERP A) (EQUAL (TIMES J (COMPLEMENT J A P)) A) (EQUAL J 0) (PRIME P) (NOT (EQUAL A 0)) (EQUAL (TIMES 0 X) A) (NUMBERP X)) (EQUAL (COMPLEMENT 0 A P) X)), which again simplifies, using linear arithmetic, to: T. Case 2.2.2. (IMPLIES (AND (NOT (NUMBERP P)) (NUMBERP A) (EQUAL (TIMES J (COMPLEMENT J A P)) A) (NOT (NUMBERP J)) (PRIME P) (NOT (EQUAL A 0)) (EQUAL (TIMES J X) A) (NOT (NUMBERP X))) (EQUAL (COMPLEMENT J A P) 0)), which again simplifies, applying TIMES-ZERO2 and EQUAL-TIMES-0, and opening up NUMBERP and EQUAL, to: T. Case 2.2.1. (IMPLIES (AND (NOT (NUMBERP P)) (NUMBERP A) (EQUAL (TIMES J (COMPLEMENT J A P)) A) (NOT (NUMBERP J)) (PRIME P) (NOT (EQUAL A 0)) (EQUAL (TIMES J X) A) (NUMBERP X)) (EQUAL (COMPLEMENT J A P) X)). But this again simplifies, applying EQUAL-TIMES-0, to: T. Case 2.1. (IMPLIES (AND (NUMBERP Z) (EQUAL (LESSP Z P) (NOT (ZEROP P))) (NUMBERP V) (NUMBERP P) (NOT (EQUAL P 0)) (EQUAL (REMAINDER (TIMES J (COMPLEMENT J (PLUS Z (TIMES P V)) P)) P) Z) (EQUAL (REMAINDER J P) 0) (PRIME P) (NOT (EQUAL Z 0)) (EQUAL (REMAINDER (TIMES J X) P) Z)) (EQUAL (COMPLEMENT J (PLUS Z (TIMES P V)) P) (REMAINDER X P))). This further simplifies, appealing to the lemmas LESSP-REMAINDER2, COMMUTATIVITY-OF-PLUS, and PRIME-KEY-REWRITE, and expanding the functions ZEROP, NOT, and EQUAL, to: T. Case 1. (IMPLIES (AND (EQUAL (REMAINDER (TIMES J (COMPLEMENT J A P)) P) (REMAINDER A P)) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (LESSP (COMPLEMENT J A P) P)) (EQUAL (REMAINDER X P) 0) (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (REMAINDER (TIMES J X) P) (REMAINDER A P))) (EQUAL (COMPLEMENT J A P) 0)), which again simplifies, using linear arithmetic and rewriting with BOUNDED-COMPLEMENT, to: T. Q.E.D. [ 0.0 1.4 0.0 ] COMPLEMENT-IS-UNIQUE (DISABLE SQUARES) [ 0.0 0.0 0.0 ] SQUARES-OFF (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))) This formula can be simplified, using the abbreviations NOT, PRIME, IMPLIES, AND, and DIVIDES, to: (IMPLIES (AND (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER J P) 0))) (EQUAL (REMAINDER (TIMES J (COMPLEMENT J A P)) P) (REMAINDER A P))) (IMPLIES (AND (NOT (ZEROP P)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P)))) (NOT (EQUAL (REMAINDER A P) (REMAINDER (TIMES J J) P)))) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (EQUAL (REMAINDER J P) 0)) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (RESIDUE A P))) (NOT (EQUAL J (COMPLEMENT J A P)))), which simplifies, using linear arithmetic, applying REMAINDER-0-CROCK, DIFFERENCE-0, and BOUNDED-COMPLEMENT, and opening up PRIME, REMAINDER, NOT, AND, IMPLIES, ZEROP, RESIDUE, TIMES, and EQUAL, to: T. Q.E.D. [ 0.0 0.7 0.0 ] NO-SELF-COMPLEMENT (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))) This formula can be simplified, using the abbreviations NOT, PRIME, IMPLIES, AND, and DIVIDES, to: (IMPLIES (AND (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER J P) 0))) (EQUAL (REMAINDER (TIMES J (COMPLEMENT J A P)) P) (REMAINDER A P))) (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL (REMAINDER (TIMES (COMPLEMENT J A P) J) P) (REMAINDER A P))) (EQUAL (COMPLEMENT (COMPLEMENT J A P) A 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 (EQUAL (REMAINDER A P) 0))) (EQUAL (COMPLEMENT (COMPLEMENT J A P) A P) (REMAINDER J P))), which simplifies, applying the lemma COMMUTATIVITY-OF-TIMES, and opening up the definitions of PRIME, NOT, AND, and IMPLIES, to: T. Q.E.D. [ 0.0 1.0 0.0 ] COMPLEMENT-OF-COMPLEMENT (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)))))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be used to show that the measure (COUNT I) decreases according to the well-founded relation LESSP in each recursive call. Hence, COMPLEMENTS is accepted under the principle of definition. From the definition we can conclude that (OR (LITATOM (COMPLEMENTS I A P)) (LISTP (COMPLEMENTS I A P))) is a theorem. [ 0.0 0.0 0.0 ] COMPLEMENTS (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)))) This formula can be simplified, using the abbreviation DIVIDES, to: (IMPLIES (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER I P) 0)) (NOT (EQUAL (REMAINDER A P) 0))) (NOT (ZEROP (COMPLEMENT I A P)))) (AND (OR (NOT (ZEROP I)) (IMPLIES (AND (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0))) (ALL-NON-ZEROP (COMPLEMENTS I A P)))) (OR (ZEROP I) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (NOT (IMPLIES (AND (PRIME P) (LESSP (SUB1 I) P) (NOT (EQUAL (REMAINDER A P) 0))) (ALL-NON-ZEROP (COMPLEMENTS (SUB1 I) A P)))) (IMPLIES (AND (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0))) (ALL-NON-ZEROP (COMPLEMENTS I A P)))) (OR (ZEROP I) (MEMBER I (COMPLEMENTS (SUB1 I) A P)) (NOT (IMPLIES (AND (PRIME P) (LESSP (SUB1 I) P) (NOT (EQUAL (REMAINDER A P) 0))) (ALL-NON-ZEROP (COMPLEMENTS (SUB1 I) A P)))) (IMPLIES (AND (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0))) (ALL-NON-ZEROP (COMPLEMENTS I A P)))))), which simplifies, rewriting with the lemmas REMAINDER-WRT-12 and REMAINDER-WRT-1, and opening up the definitions of PRIME, NOT, AND, ZEROP, IMPLIES, EQUAL, LESSP, REMAINDER, COMPLEMENTS, OR, SUB1, and NUMBERP, to ten new goals: Case 10.(IMPLIES (AND (EQUAL (REMAINDER I P) 0) (NOT (EQUAL I 0)) (NUMBERP I) (MEMBER I (COMPLEMENTS (SUB1 I) A P)) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (LESSP (SUB1 I) P)) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0))) (ALL-NON-ZEROP (COMPLEMENTS (SUB1 I) A P))), which again simplifies, using linear arithmetic, to: T. Case 9. (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 P) (NOT (EQUAL (REMAINDER A P) 0))) (ALL-NON-ZEROP NIL)), which again simplifies, opening up LESSP, REMAINDER, EQUAL, and ALL-NON-ZEROP, to: T. Case 8. (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 P) (NOT (EQUAL (REMAINDER A P) 0))) (ALL-NON-ZEROP NIL)), which again simplifies, rewriting with the lemma REMAINDER-0-CROCK, and expanding EQUAL, LESSP, and ALL-NON-ZEROP, to: T. Case 7. (IMPLIES (AND (EQUAL (REMAINDER I P) 0) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (LESSP (SUB1 I) P)) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0))) (ALL-NON-ZEROP (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))))), which again simplifies, using linear arithmetic, to: T. Case 6. (IMPLIES (AND (EQUAL (REMAINDER I P) 0) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (EQUAL (REMAINDER A P) 0)) (ALL-NON-ZEROP (COMPLEMENTS (SUB1 I) A P)) (LESSP I P)) (ALL-NON-ZEROP (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))))), which again simplifies, expanding the function REMAINDER, to: T. Case 5. (IMPLIES (AND (NOT (EQUAL (COMPLEMENT I A P) 0)) (NOT (EQUAL I 0)) (NUMBERP I) (MEMBER I (COMPLEMENTS (SUB1 I) A P)) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (LESSP (SUB1 I) P)) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0))) (ALL-NON-ZEROP (COMPLEMENTS (SUB1 I) A P))), which again simplifies, using linear arithmetic, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL (COMPLEMENT I A P) 0)) (NOT (NUMBERP I)) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0))) (ALL-NON-ZEROP NIL)), which again simplifies, opening up the definitions of LESSP and ALL-NON-ZEROP, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL (COMPLEMENT I A P) 0)) (EQUAL I 0) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0))) (ALL-NON-ZEROP NIL)), which again simplifies, unfolding the functions EQUAL, LESSP, and ALL-NON-ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL (COMPLEMENT I A P) 0)) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (LESSP (SUB1 I) P)) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0))) (ALL-NON-ZEROP (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL (COMPLEMENT I A P) 0)) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (EQUAL (REMAINDER A P) 0)) (ALL-NON-ZEROP (COMPLEMENTS (SUB1 I) A P)) (LESSP I P)) (ALL-NON-ZEROP (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))))), which again simplifies, appealing to the lemmas CDR-CONS and CAR-CONS, and unfolding the function ALL-NON-ZEROP, to: T. Q.E.D. [ 0.0 1.5 0.0 ] ALL-NON-ZEROP-COMPLEMENTS (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)))) This formula simplifies, applying SUB1-NNUMBERP, and expanding the definitions of ZEROP, NOT, IMPLIES, EQUAL, LESSP, SUB1, OR, AND, and COMPLEMENTS, to the following five new conjectures: Case 5. (IMPLIES (AND (LESSP (COMPLEMENT I A P) P) (NOT (NUMBERP I)) (NOT (EQUAL P 0)) (NUMBERP P)) (ALL-LESSEQP NIL (SUB1 P))). This again simplifies, rewriting with PIGEON-HOLE-PRINCIPLE-LEMMA-2 and ADD1-SUB1, and opening up the functions ALL-LESSEQP, MEMBER, and LISTP, to: T. Case 4. (IMPLIES (AND (LESSP (COMPLEMENT I A P) P) (EQUAL I 0) (NOT (EQUAL P 0)) (NUMBERP P)) (ALL-LESSEQP NIL (SUB1 P))). This again simplifies, applying the lemmas PIGEON-HOLE-PRINCIPLE-LEMMA-2 and ADD1-SUB1, and opening up the definitions of ALL-LESSEQP, MEMBER, and LISTP, to: T. Case 3. (IMPLIES (AND (LESSP (COMPLEMENT I A P) P) (NOT (EQUAL I 0)) (NUMBERP I) (MEMBER I (COMPLEMENTS (SUB1 I) A P)) (NOT (LESSP (SUB1 I) P)) (NOT (EQUAL P 0)) (NUMBERP P) (LESSP (SUB1 I) (SUB1 P))) (ALL-LESSEQP (COMPLEMENTS (SUB1 I) A P) (SUB1 P))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (LESSP (COMPLEMENT I A P) P) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (NOT (LESSP (SUB1 I) P)) (NOT (EQUAL P 0)) (NUMBERP P) (LESSP (SUB1 I) (SUB1 P))) (ALL-LESSEQP (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))) (SUB1 P))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (LESSP (COMPLEMENT I A P) P) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (ALL-LESSEQP (COMPLEMENTS (SUB1 I) A P) (SUB1 P)) (NOT (EQUAL P 0)) (NUMBERP P) (LESSP (SUB1 I) (SUB1 P))) (ALL-LESSEQP (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))) (SUB1 P))), which again simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS, and opening up the function ALL-LESSEQP, to two new formulas: Case 1.2. (IMPLIES (AND (LESSP (COMPLEMENT I A P) P) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (ALL-LESSEQP (COMPLEMENTS (SUB1 I) A P) (SUB1 P)) (NOT (EQUAL P 0)) (NUMBERP P) (LESSP (SUB1 I) (SUB1 P))) (NOT (LESSP (SUB1 P) I))), which again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (LESSP (COMPLEMENT I A P) P) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (ALL-LESSEQP (COMPLEMENTS (SUB1 I) A P) (SUB1 P)) (NOT (EQUAL P 0)) (NUMBERP P) (LESSP (SUB1 I) (SUB1 P))) (NOT (LESSP (SUB1 P) (COMPLEMENT I A P)))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.3 0.0 ] BOUNDED-COMPLEMENTS (PROVE-LEMMA SUBSETP-POSITIVES-COMPLEMENTS (REWRITE) (SUBSETP (POSITIVES N) (COMPLEMENTS N A P))) Give the conjecture the name *1. We will appeal to induction. Two inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP N) (p N A P)) (IMPLIES (AND (NOT (ZEROP N)) (MEMBER N (COMPLEMENTS (SUB1 N) A P)) (p (SUB1 N) A P)) (p N A P)) (IMPLIES (AND (NOT (ZEROP N)) (NOT (MEMBER N (COMPLEMENTS (SUB1 N) A P))) (p (SUB1 N) A P)) (p N A 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 produces the following three new conjectures: Case 3. (IMPLIES (ZEROP N) (SUBSETP (POSITIVES N) (COMPLEMENTS N A P))). This simplifies, expanding the functions ZEROP, POSITIVES, EQUAL, COMPLEMENTS, and SUBSETP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP N)) (MEMBER N (COMPLEMENTS (SUB1 N) A P)) (SUBSETP (POSITIVES (SUB1 N)) (COMPLEMENTS (SUB1 N) A P))) (SUBSETP (POSITIVES N) (COMPLEMENTS N A P))). This simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS, and opening up ZEROP, POSITIVES, COMPLEMENTS, and SUBSETP, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP N)) (NOT (MEMBER N (COMPLEMENTS (SUB1 N) A P))) (SUBSETP (POSITIVES (SUB1 N)) (COMPLEMENTS (SUB1 N) A P))) (SUBSETP (POSITIVES N) (COMPLEMENTS N A P))). This simplifies, rewriting with SUBSETP-CONS, CDR-CONS, and CAR-CONS, and expanding ZEROP, POSITIVES, COMPLEMENTS, MEMBER, and SUBSETP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] SUBSETP-POSITIVES-COMPLEMENTS (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))) This formula can be simplified, using the abbreviation DIVIDES, to the new formula: (IMPLIES (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER I P) 0)) (NOT (EQUAL (REMAINDER A P) 0))) (EQUAL (COMPLEMENT (COMPLEMENT I A P) A P) (REMAINDER I P))) (AND (OR (NOT (ZEROP I)) (IMPLIES (AND (PRIME P) (NOT (ZEROP I)) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER J (COMPLEMENTS I A P))) (MEMBER (COMPLEMENT J A P) (COMPLEMENTS I A P)))) (OR (ZEROP I) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (NOT (IMPLIES (AND (PRIME P) (NOT (ZEROP (SUB1 I))) (LESSP (SUB1 I) P) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER J (COMPLEMENTS (SUB1 I) A P))) (MEMBER (COMPLEMENT J A P) (COMPLEMENTS (SUB1 I) A P)))) (IMPLIES (AND (PRIME P) (NOT (ZEROP I)) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER J (COMPLEMENTS I A P))) (MEMBER (COMPLEMENT J A P) (COMPLEMENTS I A P)))) (OR (ZEROP I) (MEMBER I (COMPLEMENTS (SUB1 I) A P)) (NOT (IMPLIES (AND (PRIME P) (NOT (ZEROP (SUB1 I))) (LESSP (SUB1 I) P) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER J (COMPLEMENTS (SUB1 I) A P))) (MEMBER (COMPLEMENT J A P) (COMPLEMENTS (SUB1 I) A P)))) (IMPLIES (AND (PRIME P) (NOT (ZEROP I)) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER J (COMPLEMENTS I A P))) (MEMBER (COMPLEMENT J A P) (COMPLEMENTS I A P)))))), which simplifies, rewriting with REMAINDER-WRT-12 and REMAINDER-WRT-1, and unfolding the definitions of PRIME, NOT, AND, IMPLIES, ZEROP, EQUAL, LESSP, REMAINDER, COMPLEMENTS, OR, SUB1, and NUMBERP, to the following 20 new formulas: Case 20.(IMPLIES (AND (EQUAL (REMAINDER I P) 0) (NOT (EQUAL I 0)) (NUMBERP I)) (OR F T)). But this again simplifies, opening up OR, to: T. Case 19.(IMPLIES (AND (EQUAL (REMAINDER I P) 0) (EQUAL I 0)) (OR T T)), which again simplifies, rewriting with the lemma REMAINDER-0-CROCK, and opening up EQUAL and OR, to: T. Case 18.(IMPLIES (AND (EQUAL (REMAINDER I P) 0) (NOT (NUMBERP I))) (OR T T)), which again simplifies, unfolding the definitions of LESSP, REMAINDER, EQUAL, and OR, to: T. Case 17.(IMPLIES (AND (EQUAL (REMAINDER I P) 0) (MEMBER I (COMPLEMENTS (SUB1 I) A P)) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER J (COMPLEMENTS (SUB1 I) A P)) (MEMBER (COMPLEMENT J A P) (COMPLEMENTS (SUB1 I) A P)) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I P)) (OR F (MEMBER (COMPLEMENT J A P) (COMPLEMENTS (SUB1 I) A P)))), which again simplifies, expanding REMAINDER, to: T. Case 16.(IMPLIES (AND (EQUAL (REMAINDER I P) 0) (MEMBER I (COMPLEMENTS (SUB1 I) A P)) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (LESSP (SUB1 I) P)) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER J (COMPLEMENTS (SUB1 I) A P))) (OR F (MEMBER (COMPLEMENT J A P) (COMPLEMENTS (SUB1 I) A P)))), which again simplifies, using linear arithmetic, to: T. Case 15.(IMPLIES (AND (EQUAL (REMAINDER I P) 0) (MEMBER I (COMPLEMENTS (SUB1 I) A P)) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (EQUAL (SUB1 I) 0) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER J (COMPLEMENTS (SUB1 I) A P))) (OR F (MEMBER (COMPLEMENT J A P) (COMPLEMENTS (SUB1 I) A P)))), which again simplifies, expanding REMAINDER, to: T. Case 14.(IMPLIES (AND (EQUAL (REMAINDER I P) 0) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (EQUAL (SUB1 I) 0) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER J (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))))) (OR F (MEMBER (COMPLEMENT J A P) (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P)))))), which again simplifies, expanding the definition of REMAINDER, to: T. Case 13.(IMPLIES (AND (EQUAL (REMAINDER I P) 0) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (LESSP (SUB1 I) P)) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER J (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))))) (OR F (MEMBER (COMPLEMENT J A P) (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P)))))), which again simplifies, using linear arithmetic, to: T. Case 12.(IMPLIES (AND (EQUAL (REMAINDER I P) 0) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER (COMPLEMENT J A P) (COMPLEMENTS (SUB1 I) A P)) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I P) (MEMBER J (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))))) (OR F (MEMBER (COMPLEMENT J A P) (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P)))))), which again simplifies, opening up the function REMAINDER, to: T. Case 11.(IMPLIES (AND (EQUAL (REMAINDER I P) 0) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER J (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I P) (MEMBER J (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))))) (OR F (MEMBER (COMPLEMENT J A P) (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P)))))), which again simplifies, expanding REMAINDER, to: T. Case 10.(IMPLIES (AND (EQUAL (COMPLEMENT (COMPLEMENT I A P) A P) (REMAINDER I P)) (NOT (EQUAL I 0)) (NUMBERP I)) (OR F T)), which again simplifies, expanding OR, to: T. Case 9. (IMPLIES (AND (EQUAL (COMPLEMENT (COMPLEMENT I A P) A P) (REMAINDER I P)) (EQUAL I 0)) (OR T T)), which again simplifies, appealing to the lemma REMAINDER-0-CROCK, and opening up the definition of OR, to: T. Case 8. (IMPLIES (AND (EQUAL (COMPLEMENT (COMPLEMENT I A P) A P) (REMAINDER I P)) (NOT (NUMBERP I))) (OR T T)), which again simplifies, opening up the definitions of LESSP, REMAINDER, and OR, to: T. Case 7. (IMPLIES (AND (EQUAL (COMPLEMENT (COMPLEMENT I A P) A P) (REMAINDER I P)) (MEMBER I (COMPLEMENTS (SUB1 I) A P)) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER J (COMPLEMENTS (SUB1 I) A P)) (MEMBER (COMPLEMENT J A P) (COMPLEMENTS (SUB1 I) A P)) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I P)) (OR F (MEMBER (COMPLEMENT J A P) (COMPLEMENTS (SUB1 I) A P)))), which again simplifies, unfolding the functions REMAINDER and OR, to: T. Case 6. (IMPLIES (AND (EQUAL (COMPLEMENT (COMPLEMENT I A P) A P) (REMAINDER I P)) (MEMBER I (COMPLEMENTS (SUB1 I) A P)) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (LESSP (SUB1 I) P)) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER J (COMPLEMENTS (SUB1 I) A P))) (OR F (MEMBER (COMPLEMENT J A P) (COMPLEMENTS (SUB1 I) A P)))), which again simplifies, using linear arithmetic, to: T. Case 5. (IMPLIES (AND (EQUAL (COMPLEMENT (COMPLEMENT I A P) A P) (REMAINDER I P)) (MEMBER I (COMPLEMENTS (SUB1 I) A P)) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (EQUAL (SUB1 I) 0) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER J (COMPLEMENTS (SUB1 I) A P))) (OR F (MEMBER (COMPLEMENT J A P) (COMPLEMENTS (SUB1 I) A P)))), which again simplifies, opening up the functions REMAINDER, EQUAL, COMPLEMENTS, LISTP, and MEMBER, to: T. Case 4. (IMPLIES (AND (EQUAL (COMPLEMENT (COMPLEMENT I A P) A P) (REMAINDER I P)) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (EQUAL (SUB1 I) 0) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER J (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))))) (OR F (MEMBER (COMPLEMENT J A P) (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P)))))), which again simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS, and unfolding the functions REMAINDER, EQUAL, COMPLEMENTS, LISTP, MEMBER, and OR, to: (IMPLIES (AND (EQUAL (COMPLEMENT (COMPLEMENT I A P) A P) I) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (EQUAL (SUB1 I) 0) (NOT (EQUAL I 0)) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (EQUAL J (COMPLEMENT I A P)) (NOT (EQUAL (COMPLEMENT J A P) I))) (EQUAL (COMPLEMENT J A P) J)). This again simplifies, clearly, to: T. Case 3. (IMPLIES (AND (EQUAL (COMPLEMENT (COMPLEMENT I A P) A P) (REMAINDER I P)) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (LESSP (SUB1 I) P)) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER J (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))))) (OR F (MEMBER (COMPLEMENT J A P) (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P)))))). This again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (EQUAL (COMPLEMENT (COMPLEMENT I A P) A P) (REMAINDER I P)) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER (COMPLEMENT J A P) (COMPLEMENTS (SUB1 I) A P)) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I P) (MEMBER J (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))))) (OR F (MEMBER (COMPLEMENT J A P) (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P)))))), which again simplifies, applying CDR-CONS and CAR-CONS, and expanding the definitions of REMAINDER, MEMBER, and OR, to: T. Case 1. (IMPLIES (AND (EQUAL (COMPLEMENT (COMPLEMENT I A P) A P) (REMAINDER I P)) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER J (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL I 0)) (NUMBERP I) (LESSP I P) (MEMBER J (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))))) (OR F (MEMBER (COMPLEMENT J A P) (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P)))))). This again simplifies, appealing to the lemmas CDR-CONS and CAR-CONS, and opening up the definitions of REMAINDER, MEMBER, and OR, to the conjecture: (IMPLIES (AND (EQUAL (COMPLEMENT (COMPLEMENT I A P) A P) I) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER J (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL I 0)) (LESSP I P) (EQUAL J (COMPLEMENT I A P)) (NOT (EQUAL (COMPLEMENT J A P) I)) (NOT (EQUAL (COMPLEMENT J A P) J))) (MEMBER (COMPLEMENT J A P) (COMPLEMENTS (SUB1 I) A P))). This again simplifies, obviously, to: T. Q.E.D. [ 0.0 4.5 0.0 ] COMPLEMENTS-CLOSED-1 (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))) This formula can be simplified, using the abbreviations ZEROP, NOT, PRIME, IMPLIES, AND, and DIVIDES, to the new formula: (IMPLIES (AND (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER J P) 0)) (NOT (EQUAL (REMAINDER A P) 0))) (EQUAL (COMPLEMENT (COMPLEMENT J A P) A P) (REMAINDER J P))) (IMPLIES (AND (PRIME P) (NOT (ZEROP I)) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER (COMPLEMENT J A P) (COMPLEMENTS I A P))) (MEMBER (COMPLEMENT (COMPLEMENT J A P) A P) (COMPLEMENTS I A P))) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL J 0)) (NUMBERP J) (LESSP I P) (LESSP J P) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER (COMPLEMENT J A P) (COMPLEMENTS I A P))) (MEMBER J (COMPLEMENTS I A P))), which simplifies, unfolding the functions PRIME, REMAINDER, NOT, AND, IMPLIES, and ZEROP, to: T. Q.E.D. [ 0.0 0.3 0.0 ] COMPLEMENTS-CLOSED-2 (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))) This formula can be simplified, using the abbreviations NOT, IMPLIES, AND, and DIVIDES, to the new formula: (IMPLIES (AND (IMPLIES (AND (PRIME P) (NOT (ZEROP (SUB1 I))) (NOT (ZEROP I)) (LESSP (SUB1 I) P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (MEMBER (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))) (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER I P) 0)) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (RESIDUE A P))) (NOT (EQUAL I (COMPLEMENT I A P)))) (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (RESIDUE A P)) (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P))) (ALL-DISTINCT (COMPLEMENTS I A P))), which simplifies, rewriting with SUB1-NNUMBERP and REMAINDER-0-CROCK, and opening up the functions ZEROP, NOT, AND, IMPLIES, REMAINDER, RESIDUE, EQUAL, COMPLEMENTS, ALL-DISTINCT, LISTP, MEMBER, LESSP, and SUB1, to the following 11 new goals: Case 11.(IMPLIES (AND (EQUAL (SUB1 I) 0) (NOT (EQUAL I (COMPLEMENT I A P))) (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P))) (NOT (EQUAL I 0)) (NUMBERP I)) (ALL-DISTINCT (LIST I (COMPLEMENT I A P)))). But this again simplifies, using linear arithmetic, applying NO-SELF-COMPLEMENT, CDR-CONS, and CAR-CONS, and opening up the definitions of RESIDUE, DIVIDES, REMAINDER, LISTP, MEMBER, and ALL-DISTINCT, to: T. Case 10.(IMPLIES (AND (EQUAL (SUB1 I) 0) (NOT (EQUAL I (COMPLEMENT I A P))) (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P))) (EQUAL I 0)) (ALL-DISTINCT NIL)). This again simplifies, expanding the definitions of SUB1, EQUAL, LESSP, and ALL-DISTINCT, to: T. Case 9. (IMPLIES (AND (EQUAL (SUB1 I) 0) (NOT (EQUAL I (COMPLEMENT I A P))) (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P))) (NOT (NUMBERP I))) (ALL-DISTINCT NIL)), which again simplifies, appealing to the lemma SUB1-NNUMBERP, and opening up the functions EQUAL, LESSP, and ALL-DISTINCT, to: T. Case 8. (IMPLIES (AND (NOT (LESSP (SUB1 I) P)) (NOT (EQUAL I (COMPLEMENT I A P))) (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P))) (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P)) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P)))) (ALL-DISTINCT (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))))), which again simplifies, using linear arithmetic, to: T. Case 7. (IMPLIES (AND (NOT (LESSP (SUB1 I) P)) (NOT (EQUAL I (COMPLEMENT I A P))) (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P))) (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P)) (EQUAL I 0)) (ALL-DISTINCT NIL)), which again simplifies, unfolding SUB1, EQUAL, LESSP, and PRIME, to: T. Case 6. (IMPLIES (AND (NOT (LESSP (SUB1 I) P)) (NOT (EQUAL I (COMPLEMENT I A P))) (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P))) (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P)) (NOT (NUMBERP I))) (ALL-DISTINCT NIL)), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP I 1) (NOT (LESSP (SUB1 I) P)) (NOT (EQUAL I (COMPLEMENT I A P))) (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P))) (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P)) (NOT (NUMBERP I))) (ALL-DISTINCT NIL)). But this again simplifies, rewriting with SUB1-NNUMBERP, and unfolding NUMBERP, EQUAL, LESSP, and PRIME, to: T. Case 5. (IMPLIES (AND (NOT (MEMBER (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL I (COMPLEMENT I A P))) (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P))) (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P)) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P)))) (ALL-DISTINCT (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))))). However this again simplifies, using linear arithmetic, appealing to the lemmas NO-SELF-COMPLEMENT, CDR-CONS, and CAR-CONS, and expanding the functions RESIDUE, DIVIDES, REMAINDER, MEMBER, and ALL-DISTINCT, to: T. Case 4. (IMPLIES (AND (NOT (MEMBER (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL I (COMPLEMENT I A P))) (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P))) (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P)) (EQUAL I 0)) (ALL-DISTINCT NIL)), which again simplifies, expanding the functions SUB1, EQUAL, COMPLEMENTS, LISTP, MEMBER, LESSP, and ALL-DISTINCT, to: T. Case 3. (IMPLIES (AND (NOT (MEMBER (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL I (COMPLEMENT I A P))) (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P))) (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P)) (NOT (NUMBERP I))) (ALL-DISTINCT NIL)), which again simplifies, rewriting with SUB1-NNUMBERP, and expanding the definitions of EQUAL, COMPLEMENTS, LISTP, MEMBER, LESSP, and ALL-DISTINCT, to: T. Case 2. (IMPLIES (AND (MEMBER I (COMPLEMENTS (SUB1 I) A P)) (NOT (EQUAL I (COMPLEMENT I A P))) (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P))) (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P)) (NOT (NUMBERP I))) (ALL-DISTINCT NIL)). However this again simplifies, applying SUB1-NNUMBERP, and expanding the definitions of EQUAL, COMPLEMENTS, LISTP, and MEMBER, to: T. Case 1. (IMPLIES (AND (MEMBER I (COMPLEMENTS (SUB1 I) A P)) (NOT (EQUAL I (COMPLEMENT I A P))) (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P))) (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P)) (EQUAL I 0)) (ALL-DISTINCT NIL)). But this again simplifies, expanding the definitions of SUB1, EQUAL, COMPLEMENTS, and MEMBER, to: T. Q.E.D. [ 0.0 0.7 0.0 ] ALL-DISTINCT-COMPLEMENTS-1 (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))) This formula can be simplified, using the abbreviation DIVIDES, to the new goal: (IMPLIES (IMPLIES (AND (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (RESIDUE A P)) (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P))) (ALL-DISTINCT (COMPLEMENTS I A P))) (AND (OR (NOT (ZEROP I)) (IMPLIES (AND (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (RESIDUE A P))) (ALL-DISTINCT (COMPLEMENTS I A P)))) (OR (ZEROP I) (NOT (IMPLIES (AND (PRIME P) (LESSP (SUB1 I) P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (RESIDUE A P))) (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P)))) (IMPLIES (AND (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (RESIDUE A P))) (ALL-DISTINCT (COMPLEMENTS I A P)))))), which simplifies, rewriting with SUB1-NNUMBERP, and expanding the functions NOT, RESIDUE, AND, COMPLEMENTS, IMPLIES, ZEROP, LESSP, ALL-DISTINCT, OR, EQUAL, and SUB1, to the following six new formulas: Case 6. (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I) (ALL-DISTINCT (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P)))) (PRIME P) (NOT (LESSP (SUB1 I) P)) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P))) (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P))). This again simplifies, using linear arithmetic, to: T. Case 5. (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I) (MEMBER I (COMPLEMENTS (SUB1 I) A P)) (PRIME P) (NOT (LESSP (SUB1 I) P)) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P)))) (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P))), which again simplifies, using linear arithmetic, to: T. Case 4. (IMPLIES (AND (NOT (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL I 0)) (NUMBERP I) (PRIME P) (NOT (LESSP (SUB1 I) P)) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P)))) (ALL-DISTINCT (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P))))), which again simplifies, using linear arithmetic, to: T. Case 3. (IMPLIES (AND (NOT (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P))) (NOT (EQUAL I 0)) (NUMBERP I) (PRIME P) (NOT (LESSP (SUB1 I) P)) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P)))) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P)))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P))) (EQUAL I 0) (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P)))) (ALL-DISTINCT NIL)), which again simplifies, expanding the definitions of SUB1, EQUAL, COMPLEMENTS, and ALL-DISTINCT, to: T. Case 1. (IMPLIES (AND (NOT (ALL-DISTINCT (COMPLEMENTS (SUB1 I) A P))) (NOT (NUMBERP I)) (PRIME P) (LESSP I P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (MEMBER (REMAINDER A P) (SQUARES P P)))) (ALL-DISTINCT NIL)), which again simplifies, applying SUB1-NNUMBERP, and opening up the functions EQUAL, COMPLEMENTS, and ALL-DISTINCT, to: T. Q.E.D. [ 0.0 0.3 0.0 ] ALL-DISTINCT-COMPLEMENTS (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)))) This conjecture can be simplified, using the abbreviations NOT, PRIME, AND, IMPLIES, and DIVIDES, to: (IMPLIES (AND (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (RESIDUE A P))) (PERM (POSITIVES (SUB1 P)) (COMPLEMENTS (SUB1 P) A P))). This simplifies, using linear arithmetic, appealing to the lemmas SUBSETP-POSITIVES-COMPLEMENTS, BOUNDED-COMPLEMENTS, ALL-NON-ZEROP-COMPLEMENTS, ALL-DISTINCT-COMPLEMENTS, and PIGEONHOLE2, and unfolding RESIDUE, PRIME, and DIVIDES, to: T. Q.E.D. [ 0.0 0.1 0.0 ] PERM-POSITIVES-COMPLEMENTS (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))) This formula can be simplified, using the abbreviations NOT, PRIME, AND, IMPLIES, and DIVIDES, to: (IMPLIES (AND (IMPLIES (PERM (POSITIVES (SUB1 P)) (COMPLEMENTS (SUB1 P) A P)) (EQUAL (TIMES-LIST (COMPLEMENTS (SUB1 P) A P)) (FACT (SUB1 P)))) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (RESIDUE A P))) (EQUAL (TIMES-LIST (COMPLEMENTS (SUB1 P) A P)) (FACT (SUB1 P)))), which simplifies, using linear arithmetic, applying PERM-POSITIVES-COMPLEMENTS, and expanding the functions DIVIDES, PRIME, and IMPLIES, to: T. Q.E.D. [ 0.0 0.1 0.0 ] COMPLEMENTS-FACT (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))) This conjecture can be simplified, using the abbreviations IMPLIES, TIMES-MOD-1, and ASSOCIATIVITY-OF-TIMES, to: (IMPLIES (AND (EQUAL (REMAINDER (TIMES (REMAINDER (TIMES I J) P) K) P) (REMAINDER (TIMES I J K) P)) (EQUAL (REMAINDER (TIMES I J) P) (REMAINDER A P))) (EQUAL (REMAINDER (TIMES I J K) P) (REMAINDER (TIMES A K) P))). This simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES and TIMES-MOD-1, to: T. Q.E.D. [ 0.0 0.1 0.0 ] TIMES-MOD-4 (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))) This formula can be simplified, using the abbreviations ZEROP, NOT, AND, IMPLIES, and TIMES-MOD-1, to: (IMPLIES (AND (IMPLIES (EQUAL (REMAINDER (TIMES I (COMPLEMENT I A P)) P) (REMAINDER A P)) (EQUAL (REMAINDER (TIMES I (COMPLEMENT I A P) (TIMES-LIST (COMPLEMENTS (SUB1 I) A P))) P) (REMAINDER (TIMES A (TIMES-LIST (COMPLEMENTS (SUB1 I) A P))) P))) (EQUAL (REMAINDER (TIMES I (COMPLEMENT I A P)) P) (REMAINDER A P)) (NOT (EQUAL I 0)) (NUMBERP I) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P)))) (EQUAL (REMAINDER (TIMES-LIST (COMPLEMENTS I A P)) P) (REMAINDER (TIMES A (TIMES-LIST (COMPLEMENTS (SUB1 I) A P))) P))), which simplifies, rewriting with CDR-CONS and CAR-CONS, and opening up IMPLIES, COMPLEMENTS, and TIMES-LIST, to: T. Q.E.D. [ 0.0 0.3 0.0 ] TIMES-COMPLEMENTS-1 (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))) This formula can be simplified, using the abbreviations NOT, IMPLIES, AND, DIVIDES, and TIMES-MOD-1, to: (IMPLIES (AND (IMPLIES (AND (EQUAL (REMAINDER (TIMES I (COMPLEMENT I A P)) P) (REMAINDER A P)) (NOT (ZEROP I)) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P)))) (EQUAL (REMAINDER (TIMES-LIST (COMPLEMENTS I A P)) P) (REMAINDER (TIMES A (TIMES-LIST (COMPLEMENTS (SUB1 I) A P))) P))) (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER I P) 0))) (EQUAL (REMAINDER (TIMES I (COMPLEMENT I A P)) P) (REMAINDER A P))) (PRIME P) (NOT (EQUAL (REMAINDER I P) 0)) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P)))) (EQUAL (REMAINDER (TIMES-LIST (COMPLEMENTS I A P)) P) (REMAINDER (TIMES A (TIMES-LIST (COMPLEMENTS (SUB1 I) A P))) P))), which simplifies, applying the lemmas REMAINDER-0-CROCK, TIMES-IDENTITY, and EQUAL-TIMES-0, and unfolding the definitions of ZEROP, NOT, AND, IMPLIES, EQUAL, LESSP, and REMAINDER, to: T. Q.E.D. [ 0.0 0.3 0.0 ] TIMES-COMPLEMENTS-2 (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))))) This conjecture can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (NUMBERP X) (EQUAL Y (PLUS X N))) (EQUAL (QUOTIENT Y N) (ADD1 (QUOTIENT X N)))). This simplifies, applying the lemmas COMMUTATIVITY-OF-PLUS and DIFFERENCE-PLUS1, and opening up QUOTIENT, to: (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (NUMBERP X) (LESSP (PLUS N X) N)) (EQUAL 0 (ADD1 (QUOTIENT X N)))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] QUOTIENT-PLUS-1 (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))))) This conjecture can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to: (IMPLIES (AND (IMPLIES (AND (NOT (ZEROP 2)) (NUMBERP (LENGTH (COMPLEMENTS (SUB1 I) A P))) (EQUAL (LENGTH (COMPLEMENTS I A P)) (PLUS (LENGTH (COMPLEMENTS (SUB1 I) A P)) 2))) (EQUAL (QUOTIENT (LENGTH (COMPLEMENTS I A P)) 2) (ADD1 (QUOTIENT (LENGTH (COMPLEMENTS (SUB1 I) A P)) 2)))) (NOT (EQUAL I 0)) (NUMBERP 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)))). This simplifies, applying CDR-CONS, COMMUTATIVITY-OF-PLUS, DIFFERENCE-2, and SUB1-ADD1, and opening up ZEROP, NOT, COMPLEMENTS, LENGTH, AND, LESSP, SUB1, NUMBERP, EQUAL, QUOTIENT, and IMPLIES, to: T. Q.E.D. [ 0.0 0.1 0.0 ] TIMES-COMPLEMENTS-3 (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))) This formula can be simplified, using the abbreviations ZEROP, NOT, IMPLIES, AND, and DIVIDES, to: (IMPLIES (AND (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER I P) 0)) (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))) (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)))) (EQUAL (REMAINDER (TIMES A (REMAINDER (EXP A (QUOTIENT (LENGTH (COMPLEMENTS (SUB1 I) A P)) 2)) P)) P) (REMAINDER (TIMES A (EXP A (QUOTIENT (LENGTH (COMPLEMENTS (SUB1 I) A P)) 2))) P)) (PRIME P) (NOT (EQUAL I 0)) (NUMBERP 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))), which simplifies, rewriting with EQUAL-MODS-TRICK-2, LESSP-REMAINDER2, REMAINDER-EXP-LEMMA, and EQUAL-MODS-TRICK-1, and expanding the functions REMAINDER, NOT, AND, COMPLEMENTS, IMPLIES, ZEROP, and EQUAL, to the following two new formulas: Case 2. (IMPLIES (AND (EQUAL (REMAINDER (TIMES-LIST (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P)))) P) (REMAINDER (TIMES A (REMAINDER (TIMES-LIST (COMPLEMENTS (SUB1 I) A P)) P)) P)) (EQUAL (QUOTIENT (LENGTH (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P)))) 2) (ADD1 (QUOTIENT (LENGTH (COMPLEMENTS (SUB1 I) A P)) 2))) (PRIME P) (NOT (EQUAL I 0)) (NUMBERP 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)) (NOT (MEMBER I (COMPLEMENTS (SUB1 I) A P)))) (EQUAL (REMAINDER (TIMES-LIST (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P)))) P) (REMAINDER (EXP A (QUOTIENT (LENGTH (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P)))) 2)) P))). But this again simplifies, rewriting with CDR-CONS, DIFFERENCE-2, SUB1-ADD1, EQUAL-MODS-TRICK-2, LESSP-REMAINDER2, REMAINDER-EXP-LEMMA, and EQUAL-MODS-TRICK-1, and opening up the functions LENGTH, LESSP, SUB1, NUMBERP, EQUAL, QUOTIENT, EXP, and REMAINDER, to: T. Case 1. (IMPLIES (AND (EQUAL (REMAINDER (TIMES-LIST (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P)))) P) (REMAINDER (TIMES A (REMAINDER (TIMES-LIST (COMPLEMENTS (SUB1 I) A P)) P)) P)) (EQUAL (QUOTIENT (LENGTH (CONS I (CONS (COMPLEMENT I A P) (COMPLEMENTS (SUB1 I) A P)))) 2) (ADD1 (QUOTIENT (LENGTH (COMPLEMENTS (SUB1 I) A P)) 2))) (PRIME P) (NOT (EQUAL I 0)) (NUMBERP 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)) (MEMBER I (COMPLEMENTS (SUB1 I) A P))) (EQUAL (REMAINDER (TIMES-LIST (COMPLEMENTS (SUB1 I) A P)) P) (REMAINDER (EXP A (QUOTIENT (LENGTH (COMPLEMENTS (SUB1 I) A P)) 2)) P))). This again simplifies, trivially, to: T. Q.E.D. [ 0.0 2.3 0.0 ] TIMES-COMPLEMENTS-4 (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)))) This formula simplifies, rewriting with REMAINDER-OF-1 and EXP-BY-0, and opening up the functions ZEROP, EQUAL, COMPLEMENTS, TIMES-LIST, LENGTH, and QUOTIENT, to: T. Q.E.D. [ 0.0 0.0 0.0 ] TIMES-COMPLEMENTS-5 (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))) This conjecture simplifies, rewriting with SUB1-NNUMBERP, and opening up the functions ZEROP, NOT, AND, IMPLIES, OR, EQUAL, LESSP, and SUB1, to: (IMPLIES (AND (NOT (EQUAL (REMAINDER (TIMES-LIST (COMPLEMENTS (SUB1 I) A P)) P) (REMAINDER (EXP A (QUOTIENT (LENGTH (COMPLEMENTS (SUB1 I) A P)) 2)) P))) (NOT (EQUAL I 0)) (NUMBERP I) (PRIME P) (NOT (LESSP (SUB1 I) P)) (LESSP I P)) (EQUAL (REMAINDER (TIMES-LIST (COMPLEMENTS I A P)) P) (REMAINDER (EXP A (QUOTIENT (LENGTH (COMPLEMENTS I A P)) 2)) P))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.1 0.0 ] TIMES-COMPLEMENTS (PROVE-LEMMA SUB1-LENGTH-DELETE (REWRITE) (IMPLIES (MEMBER X B) (EQUAL (LENGTH (DELETE X B)) (SUB1 (LENGTH B))))) WARNING: the previously added lemma, LENGTH-DELETE, could be applied whenever the newly proposed SUB1-LENGTH-DELETE could! This simplifies, appealing to the lemma LENGTH-DELETE, to the conjecture: (IMPLIES (MEMBER X B) (EQUAL (LENGTH (CDR B)) (SUB1 (LENGTH B)))). This again simplifies, opening up the function LENGTH, to two new formulas: Case 2. (IMPLIES (AND (MEMBER X B) (NOT (LISTP B))) (EQUAL (LENGTH (CDR B)) (SUB1 0))), which again simplifies, opening up MEMBER, to: T. Case 1. (IMPLIES (AND (MEMBER X B) (LISTP B)) (EQUAL (LENGTH (CDR B)) (SUB1 (ADD1 (LENGTH (CDR B)))))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] SUB1-LENGTH-DELETE (PROVE-LEMMA EQUAL-LENGTH-PERM NIL (IMPLIES (PERM A B) (EQUAL (LENGTH A) (LENGTH B))) ((INDUCT (PERM A B)))) This conjecture can be simplified, using the abbreviations IMPLIES, NLISTP, NOT, OR, and AND, to three new conjectures: Case 3. (IMPLIES (AND (NOT (LISTP A)) (PERM A B)) (EQUAL (LENGTH A) (LENGTH B))), which simplifies, opening up the functions PERM, LENGTH, and EQUAL, to: T. Case 2. (IMPLIES (AND (LISTP A) (MEMBER (CAR A) B) (IMPLIES (PERM (CDR A) (DELETE (CAR A) B)) (EQUAL (LENGTH (CDR A)) (LENGTH (DELETE (CAR A) B)))) (PERM A B)) (EQUAL (LENGTH A) (LENGTH B))), which simplifies, rewriting with PERM-MEMBER and SUB1-LENGTH-DELETE, and opening up the definitions of MEMBER, IMPLIES, PERM, and LENGTH, to the new goal: (IMPLIES (AND (LISTP A) (EQUAL (LENGTH (CDR A)) (SUB1 (LENGTH B))) (MEMBER (CAR A) B) (PERM (CDR A) (DELETE (CAR A) B))) (EQUAL (ADD1 (LENGTH (CDR A))) (LENGTH B))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (LENGTH B) 0) (LISTP A) (EQUAL (LENGTH (CDR A)) (SUB1 (LENGTH B))) (MEMBER (CAR A) B) (PERM (CDR A) (DELETE (CAR A) B))) (EQUAL (ADD1 (LENGTH (CDR A))) (LENGTH B))). But this again simplifies, rewriting with the lemma EQUAL-LENGTH-0, and unfolding the functions SUB1 and MEMBER, to: T. Case 1. (IMPLIES (AND (LISTP A) (NOT (MEMBER (CAR A) B)) (PERM A B)) (EQUAL (LENGTH A) (LENGTH B))), which simplifies, appealing to the lemma PERM-MEMBER, and unfolding the definition of MEMBER, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EQUAL-LENGTH-PERM (PROVE-LEMMA LENGTH-POSITIVES (REWRITE) (EQUAL (LENGTH (POSITIVES N)) (FIX N)) ((INDUCT (POSITIVES N)))) This formula can be simplified, using the abbreviations ZEROP, NOT, OR, and AND, to the following two new goals: Case 2. (IMPLIES (ZEROP N) (EQUAL (LENGTH (POSITIVES N)) (FIX N))). This simplifies, expanding ZEROP, POSITIVES, LENGTH, FIX, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (EQUAL (LENGTH (POSITIVES (SUB1 N))) (FIX (SUB1 N)))) (EQUAL (LENGTH (POSITIVES N)) (FIX N))). This simplifies, applying ADD1-SUB1 and CDR-CONS, and expanding the functions FIX, POSITIVES, and LENGTH, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LENGTH-POSITIVES (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))) This conjecture can be simplified, using the abbreviations NOT, PRIME, IMPLIES, AND, and DIVIDES, to: (IMPLIES (AND (IMPLIES (AND (PRIME P) (LESSP (SUB1 P) P)) (EQUAL (REMAINDER (TIMES-LIST (COMPLEMENTS (SUB1 P) A P)) P) (REMAINDER (EXP A (QUOTIENT (LENGTH (COMPLEMENTS (SUB1 P) A P)) 2)) P))) (IMPLIES (AND (PRIME P) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (RESIDUE A P))) (EQUAL (TIMES-LIST (COMPLEMENTS (SUB1 P) A P)) (FACT (SUB1 P)))) (IMPLIES (PRIME P) (EQUAL (REMAINDER (FACT (SUB1 P)) P) (SUB1 P))) (NOT (EQUAL P 0)) (NUMBERP P) (NOT (EQUAL P 1)) (PRIME1 P (SUB1 P)) (NOT (EQUAL (REMAINDER A P) 0)) (NOT (RESIDUE A P))) (EQUAL (REMAINDER (EXP A (QUOTIENT (LENGTH (COMPLEMENTS (SUB1 P) A P)) 2)) P)