(NOTE-LIB "rsa" T)
Loading ./basic/rsa.lib
Finished loading ./basic/rsa.lib
Loading ./basic/rsa.o
Finished loading ./basic/rsa.o
(#./basic/rsa.lib #./basic/rsa)
(COMPILE-UNCOMPILED-DEFNS "tmp")
Loading ./basic/tmp.o
Finished loading ./basic/tmp.o
/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/tmp.lisp
(DEFN INVERSE
(J P)
(IF (EQUAL P 2)
(REMAINDER J 2)
(REMAINDER (EXP J (DIFFERENCE P 2))
P)))
From the definition we can conclude that (NUMBERP (INVERSE J P)) is a
theorem.
[ 0.0 0.0 0.0 ]
INVERSE
(PROVE-LEMMA INVERSE-INVERTS-LEMMA
(REWRITE)
(IMPLIES (NOT (ZEROP P))
(EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
(REMAINDER (EXP J (SUB1 P)) P))))
This formula can be simplified, using the abbreviations ZEROP, NOT, and
IMPLIES, to:
(IMPLIES (AND (NOT (EQUAL P 0)) (NUMBERP P))
(EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
(REMAINDER (EXP J (SUB1 P)) P))),
which simplifies, rewriting with DIFFERENCE-1 and COMMUTATIVITY-OF-TIMES, and
unfolding DIFFERENCE, EQUAL, NUMBERP, SUB1, and INVERSE, to the following two
new conjectures:
Case 2. (IMPLIES
(AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 2)))
(EQUAL (REMAINDER (TIMES J
(REMAINDER (EXP J (SUB1 (SUB1 P))) P))
P)
(REMAINDER (EXP J (SUB1 P)) P))).
This again simplifies, applying the lemma TIMES-MOD-1, and unfolding EXP, to:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 P) 0))
(EQUAL (REMAINDER (TIMES J (EXP J (SUB1 (SUB1 P))))
P)
(REMAINDER 1 P))).
However this again simplifies, rewriting with the lemmas EXP-BY-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, and REMAINDER-OF-1, and opening up the definition of
SUB1, to four new formulas:
Case 2.4.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 P) 0)
(NOT (EQUAL P 1))
(NOT (NUMBERP J)))
(EQUAL (REMAINDER 0 P) 1)),
which again simplifies, using linear arithmetic, to:
T.
Case 2.3.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 P) 0)
(NOT (EQUAL P 1))
(NUMBERP J))
(EQUAL (REMAINDER J P) 1)),
which again simplifies, using linear arithmetic, to:
T.
Case 2.2.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 P) 0)
(EQUAL P 1)
(NOT (NUMBERP J)))
(EQUAL (REMAINDER 0 P) 0)),
which again simplifies, expanding the functions EQUAL, NUMBERP, SUB1, and
REMAINDER, to:
T.
Case 2.1.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 P) 0)
(EQUAL P 1)
(NUMBERP J))
(EQUAL (REMAINDER J P) 0)),
which again simplifies, rewriting with REMAINDER-WRT-1, and unfolding
EQUAL, NUMBERP, and SUB1, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(EQUAL P 2))
(EQUAL (REMAINDER (TIMES J (REMAINDER J 2))
P)
(REMAINDER (EXP J (SUB1 P)) P))).
However this again simplifies, applying TIMES-MOD-1, COMMUTATIVITY-OF-TIMES,
TIMES-1, and EXP-BY-0, and opening up the definitions of EQUAL, NUMBERP,
SUB1, and EXP, to the following two new goals:
Case 1.2.
(IMPLIES (NOT (NUMBERP J))
(EQUAL (REMAINDER (TIMES J J) 2)
(REMAINDER 0 2))).
This again simplifies, appealing to the lemma TIMES-ZERO2, and unfolding
the definitions of REMAINDER and EQUAL, to:
T.
Case 1.1.
(IMPLIES (NUMBERP J)
(EQUAL (REMAINDER (TIMES J J) 2)
(REMAINDER J 2))),
which again simplifies, rewriting with COROLLARY-55, and opening up PRIME,
to the new goal:
(IMPLIES (AND (NUMBERP J)
(NOT (EQUAL (REMAINDER J 2) 0)))
(EQUAL (REMAINDER J 2) 1)),
which again simplifies, using linear arithmetic, applying
LESSP-REMAINDER-DIVISOR, and unfolding the definition of EQUAL, to:
T.
Q.E.D.
[ 0.0 0.4 0.0 ]
INVERSE-INVERTS-LEMMA
(PROVE-LEMMA INVERSE-INVERTS
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0)))
(EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
1))
((USE (INVERSE-INVERTS-LEMMA))
(DISABLE INVERSE)))
This formula can be simplified, using the abbreviations NOT, PRIME, AND, and
IMPLIES, to:
(IMPLIES (AND (IMPLIES (NOT (ZEROP P))
(EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
(REMAINDER (EXP J (SUB1 P)) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0)))
(EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
1)),
which simplifies, rewriting with COMMUTATIVITY-OF-TIMES and FERMAT-THM, and
expanding ZEROP, NOT, PRIME, IMPLIES, and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
INVERSE-INVERTS
(PROVE-LEMMA INVERSE-IS-UNIQUE
(REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL 1 (REMAINDER (TIMES M X) P)))
(EQUAL (INVERSE M P) (REMAINDER X P)))
((USE (INVERSE-INVERTS (J M))
(THM-55-SPECIALIZED-TO-PRIMES (Y (INVERSE M P))))))
WARNING: Note that the rewrite rule INVERSE-IS-UNIQUE will be stored so as to
apply only to terms with the nonrecursive function symbol INVERSE.
WARNING: Note that INVERSE-IS-UNIQUE contains the free variable X which will
be chosen by instantiating the hypothesis (EQUAL 1 (REMAINDER (TIMES M X) P)).
This conjecture can be simplified, using the abbreviations PRIME, IMPLIES, and
AND, to the conjecture:
(IMPLIES
(AND (IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0)))
(EQUAL (REMAINDER (TIMES (INVERSE M P) M) P)
1))
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0)))
(EQUAL (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER (TIMES M (INVERSE M P)) P))
(EQUAL (REMAINDER X P)
(REMAINDER (INVERSE M P) P))))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1 (REMAINDER (TIMES M X) P)))
(EQUAL (INVERSE M P)
(REMAINDER X P))).
This simplifies, applying DIFFERENCE-1, COMMUTATIVITY-OF-TIMES, TIMES-MOD-1,
and LESSP-REMAINDER2, and unfolding the functions PRIME, NOT, AND, DIFFERENCE,
EQUAL, NUMBERP, SUB1, INVERSE, IMPLIES, REMAINDER, and PRIME1, to six new
formulas:
Case 6. (IMPLIES (AND (EQUAL (REMAINDER M P) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1 (REMAINDER (TIMES M X) P))
(NOT (EQUAL P 2)))
(EQUAL (REMAINDER (EXP M (SUB1 (SUB1 P))) P)
(REMAINDER X P))).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace M by
(PLUS Z (TIMES P V)) to eliminate (REMAINDER M P) and (QUOTIENT M P). We
rely upon LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER
was introduced, and the type restriction lemma noted when QUOTIENT was
introduced to restrict the new variables. We thus obtain the following two
new goals:
Case 6.2.
(IMPLIES (AND (NOT (NUMBERP M))
(EQUAL (REMAINDER M P) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1 (REMAINDER (TIMES M X) P))
(NOT (EQUAL P 2)))
(EQUAL (REMAINDER (EXP M (SUB1 (SUB1 P))) P)
(REMAINDER X P))).
However this further simplifies, applying EQUAL-TIMES-0 and TIMES-EQUAL-1,
and expanding the definitions of LESSP, REMAINDER, and EQUAL, to:
T.
Case 6.1.
(IMPLIES (AND (NUMBERP Z)
(EQUAL (LESSP Z P) (NOT (ZEROP P)))
(NUMBERP V)
(EQUAL Z 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1
(REMAINDER (TIMES (PLUS Z (TIMES P V)) X)
P))
(NOT (EQUAL P 2)))
(EQUAL (REMAINDER (EXP (PLUS Z (TIMES P V))
(SUB1 (SUB1 P)))
P)
(REMAINDER X P))).
However this further simplifies, rewriting with ASSOCIATIVITY-OF-TIMES and
REMAINDER-TIMES, and expanding NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS,
to:
T.
Case 5. (IMPLIES (AND (EQUAL (REMAINDER M P) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1 (REMAINDER (TIMES M X) P))
(EQUAL P 2))
(EQUAL (REMAINDER M 2)
(REMAINDER X P))).
But this again simplifies, using linear arithmetic and applying the lemma
LESSP-REMAINDER-DIVISOR, to:
(IMPLIES (AND (EQUAL (REMAINDER X 2) 1)
(EQUAL (REMAINDER M 2) 0)
(NOT (EQUAL 2 0))
(NUMBERP 2)
(NOT (EQUAL 2 1))
(PRIME1 2 (SUB1 2))
(EQUAL 1 (REMAINDER (TIMES M X) 2)))
(EQUAL 0 1)).
However this again simplifies, unfolding the functions EQUAL, NUMBERP, SUB1,
and PRIME1, to the conjecture:
(IMPLIES (AND (EQUAL (REMAINDER X 2) 1)
(EQUAL (REMAINDER M 2) 0))
(NOT (EQUAL 1 (REMAINDER (TIMES M X) 2)))).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace X by
(PLUS Z (TIMES 2 V)) to eliminate (REMAINDER X 2) and (QUOTIENT X 2). We
rely upon LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER
was introduced, and the type restriction lemma noted when QUOTIENT was
introduced to constrain the new variables. This generates four new
conjectures:
Case 5.4.
(IMPLIES (AND (NOT (NUMBERP X))
(EQUAL (REMAINDER X 2) 1)
(EQUAL (REMAINDER M 2) 0))
(NOT (EQUAL 1 (REMAINDER (TIMES M X) 2)))),
which further simplifies, opening up the definitions of LESSP, NUMBERP,
EQUAL, and REMAINDER, to:
T.
Case 5.3.
(IMPLIES (AND (EQUAL 2 0)
(EQUAL (REMAINDER X 2) 1)
(EQUAL (REMAINDER M 2) 0))
(NOT (EQUAL 1 (REMAINDER (TIMES M X) 2)))),
which further simplifies, using linear arithmetic, to:
T.
Case 5.2.
(IMPLIES (AND (NOT (NUMBERP 2))
(EQUAL (REMAINDER X 2) 1)
(EQUAL (REMAINDER M 2) 0))
(NOT (EQUAL 1 (REMAINDER (TIMES M X) 2)))),
which further simplifies, clearly, to:
T.
Case 5.1.
(IMPLIES (AND (NUMBERP Z)
(EQUAL (LESSP Z 2) (NOT (ZEROP 2)))
(NUMBERP V)
(NOT (EQUAL 2 0))
(EQUAL Z 1)
(EQUAL (REMAINDER M 2) 0))
(NOT (EQUAL 1
(REMAINDER (TIMES M (PLUS Z (TIMES 2 V)))
2)))).
However this further simplifies, rewriting with the lemmas TIMES-2,
TIMES-1, COMMUTATIVITY-OF-TIMES, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS,
COMMUTATIVITY-OF-PLUS, and COMMUTATIVITY2-OF-PLUS, and expanding the
definitions of NUMBERP, LESSP, ZEROP, NOT, and EQUAL, to two new
conjectures:
Case 5.1.2.
(IMPLIES (AND (NUMBERP V)
(EQUAL (REMAINDER M 2) 0)
(NOT (NUMBERP M)))
(NOT (EQUAL 1
(REMAINDER (PLUS (TIMES M V) (TIMES M V) 0)
2)))),
which finally simplifies, appealing to the lemmas COMMUTATIVITY-OF-PLUS,
EQUAL-TIMES-0, and TIMES-EQUAL-1, and unfolding LESSP, NUMBERP, EQUAL,
REMAINDER, and PLUS, to:
T.
Case 5.1.1.
(IMPLIES (AND (NUMBERP V)
(EQUAL (REMAINDER M 2) 0)
(NUMBERP M))
(NOT (EQUAL 1
(REMAINDER (PLUS (TIMES M V) (TIMES M V) M)
2)))),
which finally simplifies, rewriting with COMMUTATIVITY-OF-PLUS,
COMMUTATIVITY2-OF-PLUS, DIVIDES-PLUS-REWRITE1, and PRIME-KEY-REWRITE,
and opening up PRIME and EQUAL, to:
T.
Case 4. (IMPLIES
(AND (NOT (EQUAL P 2))
(EQUAL (REMAINDER (TIMES M
(REMAINDER (EXP M (SUB1 (SUB1 P))) P))
P)
1)
(EQUAL (REMAINDER M P) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1 (REMAINDER (TIMES M X) P)))
(EQUAL (REMAINDER (EXP M (SUB1 (SUB1 P))) P)
(REMAINDER X P))).
This again simplifies, rewriting with TIMES-MOD-1, to:
(IMPLIES (AND (NOT (EQUAL P 2))
(EQUAL (REMAINDER (TIMES M (EXP M (SUB1 (SUB1 P))))
P)
1)
(EQUAL (REMAINDER M P) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1 (REMAINDER (TIMES M X) P)))
(EQUAL (REMAINDER (EXP M (SUB1 (SUB1 P))) P)
(REMAINDER X P))).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace X by
(PLUS Z (TIMES P V)) to eliminate (REMAINDER X P) and (QUOTIENT X P). We
employ LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was
introduced, and the type restriction lemma noted when QUOTIENT was
introduced to restrict the new variables. This produces the following two
new goals:
Case 4.2.
(IMPLIES (AND (NOT (NUMBERP X))
(NOT (EQUAL P 2))
(EQUAL (REMAINDER (TIMES M (EXP M (SUB1 (SUB1 P))))
P)
1)
(EQUAL (REMAINDER M P) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1 (REMAINDER (TIMES M X) P)))
(EQUAL (REMAINDER (EXP M (SUB1 (SUB1 P))) P)
(REMAINDER X P))).
However this further simplifies, applying the lemmas TIMES-ZERO2 and
REMAINDER-0-CROCK, and unfolding the function EQUAL, to:
T.
Case 4.1.
(IMPLIES (AND (NUMBERP Z)
(EQUAL (LESSP Z P) (NOT (ZEROP P)))
(NUMBERP V)
(NOT (EQUAL P 2))
(EQUAL (REMAINDER (TIMES M (EXP M (SUB1 (SUB1 P))))
P)
1)
(EQUAL (REMAINDER M P) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL 1
(REMAINDER (TIMES M (PLUS Z (TIMES P V)))
P)))
(EQUAL (REMAINDER (EXP M (SUB1 (SUB1 P))) P)
Z)),
which further simplifies, applying DISTRIBUTIVITY-OF-TIMES-OVER-PLUS,
REMAINDER-TIMES-1, PRIME-KEY-REWRITE, and DIVIDES-PLUS-REWRITE1, and
unfolding the functions ZEROP, NOT, EQUAL, and PRIME, to:
T.
Case 3. (IMPLIES
(AND (NOT (EQUAL P 2))
(EQUAL (REMAINDER (TIMES M
(REMAINDER (EXP M (SUB1 (SUB1 P))) P))
P)
1)
(NOT (EQUAL (REMAINDER X P)
(REMAINDER (EXP M (SUB1 (SUB1 P)))
P)))
(NOT (EQUAL 1
(REMAINDER (TIMES M (EXP M (SUB1 (SUB1 P))))
P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(NOT (EQUAL 1 (REMAINDER (TIMES M X) P)))).
But this again simplifies, rewriting with the lemma TIMES-MOD-1, to:
T.
Case 2. (IMPLIES (AND (EQUAL P 2)
(EQUAL (REMAINDER (TIMES M (REMAINDER M 2))
P)
1)
(EQUAL (REMAINDER M 2) 0)
(EQUAL 1 (REMAINDER (TIMES M X) 2)))
(EQUAL 0 (REMAINDER X 2))),
which again simplifies, using linear arithmetic, applying
LESSP-REMAINDER-DIVISOR, and unfolding the function EQUAL, to the new
conjecture:
(IMPLIES (AND (EQUAL (REMAINDER X 2) 1)
(EQUAL (REMAINDER (TIMES M 0) 2) 1)
(EQUAL (REMAINDER M 2) 0)
(EQUAL 1 (REMAINDER (TIMES M X) 2)))
(EQUAL 0 1)),
which again simplifies, applying COMMUTATIVITY-OF-TIMES, TIMES-IDENTITY, and
TIMES-EQUAL-1, and opening up LESSP, NUMBERP, EQUAL, and REMAINDER, to:
T.
Case 1. (IMPLIES (AND (EQUAL P 2)
(EQUAL (REMAINDER (TIMES M (REMAINDER M 2))
P)
1)
(NOT (EQUAL (REMAINDER X 2)
(REMAINDER M 2)))
(NOT (EQUAL 1 (REMAINDER (TIMES M M) 2))))
(NOT (EQUAL 1 (REMAINDER (TIMES M X) 2)))).
But this again simplifies, appealing to the lemma TIMES-MOD-1, to:
T.
Q.E.D.
[ 0.0 1.4 0.0 ]
INVERSE-IS-UNIQUE
(PROVE-LEMMA S-P-I-I-LEMMA1
(REWRITE)
(IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1)))
(EQUAL (TIMES (SUB1 N) (SUB1 N))
(PLUS 1 (TIMES N (SUB1 (SUB1 N)))))))
WARNING: the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the newly proposed S-P-I-I-LEMMA1 could!
This formula can be simplified, using the abbreviations ZEROP, NOT, AND, and
IMPLIES, to:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL N 1)))
(EQUAL (TIMES (SUB1 N) (SUB1 N))
(PLUS 1 (TIMES N (SUB1 (SUB1 N)))))),
which simplifies, expanding SUB1, NUMBERP, EQUAL, and PLUS, to the formula:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL N 1)))
(EQUAL (TIMES (SUB1 N) (SUB1 N))
(ADD1 (TIMES N (SUB1 (SUB1 N)))))).
Appealing to the lemma SUB1-ELIM, we now replace N by (ADD1 X) to eliminate
(SUB1 N) and X by (ADD1 Z) to eliminate (SUB1 X). We employ the type
restriction lemma noted when SUB1 was introduced to constrain the new variable.
We must thus prove two new goals:
Case 2. (IMPLIES (AND (EQUAL X 0)
(NUMBERP X)
(NOT (EQUAL (ADD1 X) 0))
(NOT (EQUAL (ADD1 X) 1)))
(EQUAL (TIMES X X)
(ADD1 (TIMES (ADD1 X) (SUB1 X))))),
which further simplifies, trivially, to:
T.
Case 1. (IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL (ADD1 Z) 0))
(NOT (EQUAL (ADD1 (ADD1 Z)) 0))
(NOT (EQUAL (ADD1 (ADD1 Z)) 1)))
(EQUAL (TIMES (ADD1 Z) (ADD1 Z))
(ADD1 (TIMES (ADD1 (ADD1 Z)) Z)))).
But this further simplifies, applying ADD1-EQUAL, TIMES-ADD1,
COMMUTATIVITY-OF-TIMES, SUB1-ADD1, PLUS-ADD1, and COMMUTATIVITY2-OF-PLUS,
and unfolding NUMBERP and PLUS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
S-P-I-I-LEMMA1
(PROVE-LEMMA S-P-I-I-LEMMA2
(REWRITE)
(IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES (SUB1 N) (SUB1 N))
N)
1))
((USE (S-P-I-I-LEMMA1)
(REMAINDER-PLUS-TIMES-2 (J N)
(X 1)
(I (SUB1 (SUB1 N)))))
(DISABLE S-P-I-I-LEMMA1 REMAINDER-PLUS-TIMES-2)))
This formula can be simplified, using the abbreviations ZEROP, NOT, IMPLIES,
and AND, to:
(IMPLIES (AND (IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1)))
(EQUAL (TIMES (SUB1 N) (SUB1 N))
(PLUS 1 (TIMES N (SUB1 (SUB1 N))))))
(EQUAL (REMAINDER (PLUS 1 (TIMES N (SUB1 (SUB1 N))))
N)
(REMAINDER 1 N))
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES (SUB1 N) (SUB1 N))
N)
1)),
which simplifies, rewriting with REMAINDER-OF-1, and unfolding the definitions
of ZEROP, NOT, AND, SUB1, NUMBERP, EQUAL, PLUS, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
S-P-I-I-LEMMA2
(PROVE-LEMMA SUB1-P-IS-INVOLUTION
(REWRITE)
(IMPLIES (PRIME P)
(EQUAL (INVERSE (SUB1 P) P) (SUB1 P)))
((USE (INVERSE-IS-UNIQUE (M (SUB1 P))
(X (SUB1 P))))
(DISABLE INVERSE)))
WARNING: Note that the rewrite rule SUB1-P-IS-INVOLUTION will be stored so as
to apply only to terms with the nonrecursive function symbol INVERSE.
This formula can be simplified, using the abbreviations PRIME and IMPLIES, to
the new formula:
(IMPLIES (AND (IMPLIES (AND (PRIME P)
(EQUAL 1
(REMAINDER (TIMES (SUB1 P) (SUB1 P))
P)))
(EQUAL (INVERSE (SUB1 P) P)
(REMAINDER (SUB1 P) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL (INVERSE (SUB1 P) P)
(SUB1 P))),
which simplifies, using linear arithmetic, applying S-P-I-I-LEMMA1,
REMAINDER-OF-1, REMAINDER-PLUS-TIMES-2, REMAINDER-0-CROCK, and DIFFERENCE-0,
and unfolding the definitions of PRIME, EQUAL, AND, REMAINDER, and IMPLIES, to
the new goal:
(IMPLIES (AND (NOT (LESSP (SUB1 P) P))
(EQUAL (INVERSE (SUB1 P) P) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL 0 (SUB1 P))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
SUB1-P-IS-INVOLUTION
(PROVE-LEMMA N-O-I-LEMMA1
(REWRITE)
(EQUAL (DIFFERENCE (TIMES X X) 1)
(TIMES (ADD1 X) (SUB1 X))))
WARNING: the previously added lemma, DIFFERENCE-1, could be applied whenever
the newly proposed N-O-I-LEMMA1 could!
This conjecture can be simplified, using the abbreviation DIFFERENCE-1, to the
goal:
(EQUAL (SUB1 (TIMES X X))
(TIMES (ADD1 X) (SUB1 X))).
Appealing to the lemma SUB1-ELIM, we now replace X by (ADD1 Z) to eliminate
(SUB1 X). We use the type restriction lemma noted when SUB1 was introduced to
constrain the new variable. We must thus prove three new goals:
Case 3. (IMPLIES (EQUAL X 0)
(EQUAL (SUB1 (TIMES X X))
(TIMES (ADD1 X) (SUB1 X)))),
which simplifies, expanding TIMES, SUB1, and EQUAL, to:
T.
Case 2. (IMPLIES (NOT (NUMBERP X))
(EQUAL (SUB1 (TIMES X X))
(TIMES (ADD1 X) (SUB1 X)))),
which simplifies, applying TIMES-ZERO2, SUB1-TYPE-RESTRICTION, and
SUB1-NNUMBERP, and opening up the functions SUB1, TIMES, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL (ADD1 Z) 0)))
(EQUAL (SUB1 (TIMES (ADD1 Z) (ADD1 Z)))
(TIMES (ADD1 (ADD1 Z)) Z))).
But this simplifies, applying the lemmas TIMES-ADD1, COMMUTATIVITY-OF-TIMES,
SUB1-ADD1, PLUS-ADD1, and COMMUTATIVITY2-OF-PLUS, and expanding PLUS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
N-O-I-LEMMA1
(PROVE-LEMMA N-O-I-LEMMA2
(REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL (REMAINDER (DIFFERENCE (TIMES J J) 1)
P)
0))
(OR (EQUAL (REMAINDER (ADD1 J) P) 0)
(EQUAL (REMAINDER (SUB1 J) P) 0))))
WARNING: Note that the rewrite rule N-O-I-LEMMA2 will be stored so as to
apply only to terms with the nonrecursive function symbol OR.
This formula can be simplified, using the abbreviations OR, PRIME, AND,
IMPLIES, and N-O-I-LEMMA1, to:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL (REMAINDER (TIMES (ADD1 J) (SUB1 J))
P)
0)
(NOT (EQUAL (REMAINDER (ADD1 J) P) 0)))
(EQUAL (REMAINDER (SUB1 J) P) 0)),
which simplifies, rewriting with the lemma PRIME-KEY-REWRITE, and expanding
the function PRIME, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
N-O-I-LEMMA2
(PROVE-LEMMA N-O-I-LEMMA3
(REWRITE)
(IMPLIES (AND (NOT (LESSP A 1))
(EQUAL (REMAINDER A P) 1))
(EQUAL (REMAINDER (SUB1 A) P) 0))
((USE (EQUAL-MODS-TRICK-2 (B 1)))
(DISABLE N-O-I-LEMMA1)))
This formula simplifies, applying REMAINDER-OF-1 and REMAINDER-WRT-1, and
opening up the definitions of IMPLIES, SUB1, NUMBERP, EQUAL, and LESSP, to the
new conjecture:
(IMPLIES (AND (EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (REMAINDER A P) 1))
(EQUAL (REMAINDER (SUB1 A) P) 0)).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace A by (PLUS X (TIMES P Z))
to eliminate (REMAINDER A P) and (QUOTIENT A P). We use LESSP-REMAINDER2, the
type restriction lemma noted when REMAINDER was introduced, and the type
restriction lemma noted when QUOTIENT was introduced to restrict the new
variables. We would thus like to prove the following three new formulas:
Case 3. (IMPLIES (AND (EQUAL P 0)
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (REMAINDER A P) 1))
(EQUAL (REMAINDER (SUB1 A) P) 0)).
This further simplifies, expanding EQUAL, REMAINDER, and SUB1, to:
T.
Case 2. (IMPLIES (AND (NOT (NUMBERP P))
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (REMAINDER A P) 1))
(EQUAL (REMAINDER (SUB1 A) P) 0)),
which further simplifies, applying REMAINDER-WRT-12 and REMAINDER-0-CROCK,
and opening up SUB1 and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X P) (NOT (ZEROP P)))
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(EQUAL (REMAINDER (PDIFFERENCE (PLUS X (TIMES P Z)) 1)
P)
0)
(NOT (EQUAL (PLUS X (TIMES P Z)) 0))
(EQUAL X 1))
(EQUAL (REMAINDER (SUB1 (PLUS X (TIMES P Z)))
P)
0)).
This further simplifies, rewriting with the lemmas REMAINDER-PLUS-TIMES-2,
REMAINDER-OF-1, EQUAL-MODS-TRICK-2, and PLUS-EQUAL-0, and opening up the
functions NUMBERP, ZEROP, NOT, and EQUAL, to:
(IMPLIES (AND (LESSP 1 P)
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0)))
(EQUAL (REMAINDER (SUB1 (PLUS 1 (TIMES P Z)))
P)
0)),
which we would usually push and work on later by induction. But if we must
use induction to prove the input conjecture, we prefer to induct on the
original formulation of the problem. Thus we will disregard all that we
have previously done, give the name *1 to the original input, and work on it.
So now let us consider:
(IF (IMPLIES (EQUAL (REMAINDER A P)
(REMAINDER 1 P))
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0))
(IMPLIES (AND (NOT (LESSP A 1))
(EQUAL (REMAINDER A P) 1))
(EQUAL (REMAINDER (SUB1 A) P) 0))
T),
which we named *1 above. We will appeal to induction. There are three
plausible inductions. They merge into two likely candidate inductions, both
of which are unflawed. So we will choose the one suggested by the largest
number of nonprimitive recursive functions. We will induct according to the
following scheme:
(AND (IMPLIES (ZEROP P) (p A P))
(IMPLIES (AND (NOT (ZEROP P)) (LESSP A P))
(p A P))
(IMPLIES (AND (NOT (ZEROP P))
(NOT (LESSP A P))
(p (DIFFERENCE A P) P))
(p A P))).
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the
definition of ZEROP inform us that the measure (COUNT A) decreases according
to the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme produces the following three new formulas:
Case 3. (IMPLIES (ZEROP P)
(IF (IMPLIES (EQUAL (REMAINDER A P)
(REMAINDER 1 P))
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0))
(IMPLIES (AND (NOT (LESSP A 1))
(EQUAL (REMAINDER A P) 1))
(EQUAL (REMAINDER (SUB1 A) P) 0))
T)).
This simplifies, applying REMAINDER-WRT-12 and REMAINDER-OF-1, and expanding
the definitions of ZEROP, EQUAL, REMAINDER, IMPLIES, SUB1, NUMBERP, LESSP,
NOT, and AND, to two new goals:
Case 3.2.
(IMPLIES (AND (EQUAL P 0)
(NUMBERP A)
(EQUAL A 1)
(EQUAL (PDIFFERENCE A 1) 0)
(NOT (EQUAL A 0)))
(EQUAL (SUB1 A) 0)),
which again simplifies, using linear arithmetic, to:
T.
Case 3.1.
(IMPLIES (AND (NOT (NUMBERP P))
(NUMBERP A)
(EQUAL A 1)
(EQUAL (PDIFFERENCE A 1) 0)
(NOT (EQUAL A 0)))
(EQUAL (SUB1 A) 0)),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP P)) (LESSP A P))
(IF (IMPLIES (EQUAL (REMAINDER A P)
(REMAINDER 1 P))
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0))
(IMPLIES (AND (NOT (LESSP A 1))
(EQUAL (REMAINDER A P) 1))
(EQUAL (REMAINDER (SUB1 A) P) 0))
T)),
which simplifies, using linear arithmetic, applying REMAINDER-OF-1,
REMAINDER-0-CROCK, and DIFFERENCE-0, and expanding the definitions of ZEROP,
REMAINDER, IMPLIES, SUB1, NUMBERP, EQUAL, LESSP, NOT, and AND, to the
following three new goals:
Case 2.3.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(LESSP A P)
(LESSP A 1))
(IF (IMPLIES (EQUAL (REMAINDER A P)
(REMAINDER 1 P))
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0))
(IMPLIES (AND (NOT (LESSP A 1))
(EQUAL (REMAINDER A P) 1))
(EQUAL (REMAINDER (SUB1 A) P) 0))
T)).
This again simplifies, rewriting with REMAINDER-0-CROCK, REMAINDER-OF-1,
and SUB1-NNUMBERP, and expanding the functions SUB1, NUMBERP, EQUAL, LESSP,
PDIFFERENCE, IMPLIES, NOT, AND, and REMAINDER, to:
T.
Case 2.2.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(LESSP A P)
(NOT (LESSP A 1))
(NUMBERP A)
(EQUAL A 1)
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(LESSP (SUB1 A) P))
(EQUAL (SUB1 A) 0)).
However this again simplifies, using linear arithmetic, to:
T.
Case 2.1.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(LESSP A P)
(NOT (LESSP A 1))
(EQUAL P 1)
(NUMBERP A)
(NOT (EQUAL A 0))
(EQUAL A 1)
(LESSP (SUB1 A) P))
(EQUAL (SUB1 A) 0)),
which again simplifies, clearly, to:
T.
Case 1. (IMPLIES
(AND (NOT (ZEROP P))
(NOT (LESSP A P))
(IF (IMPLIES (EQUAL (REMAINDER (DIFFERENCE A P) P)
(REMAINDER 1 P))
(EQUAL (REMAINDER (PDIFFERENCE (DIFFERENCE A P) 1)
P)
0))
(IMPLIES (AND (NOT (LESSP (DIFFERENCE A P) 1))
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1))
(EQUAL (REMAINDER (SUB1 (DIFFERENCE A P)) P)
0))
T))
(IF (IMPLIES (EQUAL (REMAINDER A P)
(REMAINDER 1 P))
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0))
(IMPLIES (AND (NOT (LESSP A 1))
(EQUAL (REMAINDER A P) 1))
(EQUAL (REMAINDER (SUB1 A) P) 0))
T)).
This simplifies, applying REMAINDER-OF-1 and EQUAL-DIFFERENCE-0, and
unfolding the definitions of ZEROP, IMPLIES, SUB1, NUMBERP, EQUAL, LESSP,
NOT, AND, and REMAINDER, to seven new conjectures:
Case 1.7.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (LESSP A P))
(NOT (EQUAL P 1))
(NOT (EQUAL (REMAINDER (PDIFFERENCE (DIFFERENCE A P) 1)
P)
0))
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1)
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(NUMBERP A))
(EQUAL (REMAINDER (SUB1 A) P) 0)),
which again simplifies, applying REMAINDER-OF-1 and EQUAL-MODS-TRICK-2,
and opening up the definition of EQUAL, to:
T.
Case 1.6.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (LESSP A P))
(NOT (LESSP P A))
(EQUAL P 1)
(NOT (EQUAL (REMAINDER (DIFFERENCE A P) P)
0))
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1))
(EQUAL (REMAINDER (SUB1 A) P) 0)).
However this again simplifies, using linear arithmetic, to:
(IMPLIES (AND (NOT (EQUAL 1 0))
(NUMBERP 1)
(NOT (LESSP 1 1))
(NOT (LESSP 1 1))
(NOT (EQUAL 1 0))
(NOT (EQUAL 1 0))
(NUMBERP 1)
(EQUAL (REMAINDER (DIFFERENCE 1 1) 1)
1))
(EQUAL (REMAINDER (SUB1 1) 1) 0)).
However this again simplifies, opening up EQUAL, NUMBERP, LESSP,
DIFFERENCE, and REMAINDER, to:
T.
Case 1.5.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (LESSP A P))
(NOT (LESSP P A))
(EQUAL (REMAINDER (DIFFERENCE A P) P)
0)
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1))
(EQUAL (REMAINDER (SUB1 A) P) 0)),
which again simplifies, using linear arithmetic, to:
T.
Case 1.4.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (LESSP A P))
(NOT (LESSP P A))
(NOT (EQUAL P 1))
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1)
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(NUMBERP A))
(EQUAL (REMAINDER (SUB1 A) P) 0)),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (LESSP A A))
(NOT (LESSP A A))
(NOT (EQUAL A 1))
(EQUAL (REMAINDER (DIFFERENCE A A) A)
1)
(EQUAL (REMAINDER (PDIFFERENCE A 1) A)
0)
(NOT (EQUAL A 0))
(NUMBERP A))
(EQUAL (REMAINDER (SUB1 A) A) 0)).
But this again simplifies, using linear arithmetic, applying the lemmas
DIFFERENCE-0 and REMAINDER-0-CROCK, and unfolding the definitions of LESSP
and EQUAL, to:
T.
Case 1.3.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (LESSP A P))
(EQUAL (REMAINDER (SUB1 (DIFFERENCE A P)) P)
0)
(EQUAL P 1)
(NOT (EQUAL (REMAINDER (DIFFERENCE A P) P)
0))
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1))
(EQUAL (REMAINDER (SUB1 A) P) 0)),
which again simplifies, appealing to the lemmas DIFFERENCE-1 and
REMAINDER-WRT-1, and opening up the definitions of EQUAL, NUMBERP, SUB1,
and LESSP, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (LESSP A P))
(EQUAL (REMAINDER (SUB1 (DIFFERENCE A P)) P)
0)
(EQUAL (REMAINDER (DIFFERENCE A P) P)
0)
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(NUMBERP A)
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1))
(EQUAL (REMAINDER (SUB1 A) P) 0)),
which again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (LESSP A P))
(EQUAL (REMAINDER (SUB1 (DIFFERENCE A P)) P)
0)
(NOT (EQUAL P 1))
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1)
(EQUAL (REMAINDER (PDIFFERENCE A 1) P)
0)
(NOT (EQUAL A 0))
(NUMBERP A))
(EQUAL (REMAINDER (SUB1 A) P) 0)),
which again simplifies, appealing to the lemmas REMAINDER-OF-1 and
EQUAL-MODS-TRICK-2, and unfolding EQUAL and REMAINDER, to:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (LESSP A P))
(EQUAL (REMAINDER (SUB1 (DIFFERENCE A P)) P)
0)
(NOT (EQUAL P 1))
(EQUAL (REMAINDER (DIFFERENCE A P) P)
1)
(NOT (EQUAL A 0))
(NUMBERP A))
(EQUAL (REMAINDER (SUB1 A) P) 0)).
Appealing to the lemmas DIFFERENCE-ELIM, SUB1-ELIM, and
REMAINDER-QUOTIENT-ELIM, we now replace A by (PLUS P X) to eliminate
(DIFFERENCE A P), X by (ADD1 Z) to eliminate (SUB1 X), Z by
(PLUS X (TIMES P V)) to eliminate (REMAINDER Z P) and (QUOTIENT Z P), and
X by (PLUS Z (TIMES P V)) to eliminate (REMAINDER X P) and (QUOTIENT X P).
We employ the type restriction lemma noted when DIFFERENCE was introduced,
the type restriction lemma noted when SUB1 was introduced,
LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was
introduced, and the type restriction lemma noted when QUOTIENT was
introduced to constrain the new variables. This generates two new
conjectures:
Case 1.1.2.
(IMPLIES (AND (NUMBERP Z)
(EQUAL (LESSP Z P) (NOT (ZEROP P)))
(NUMBERP V)
(EQUAL (PLUS Z (TIMES P V)) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (LESSP (PLUS P Z (TIMES P V)) P))
(EQUAL (REMAINDER (SUB1 (PLUS Z (TIMES P V)))
P)
0)
(NOT (EQUAL P 1))
(EQUAL Z 1)
(NOT (EQUAL (PLUS P Z (TIMES P V)) 0)))
(EQUAL (REMAINDER (SUB1 (PLUS P Z (TIMES P V)))
P)
0)),
which further simplifies, using linear arithmetic, to:
T.
Case 1.1.1.
(IMPLIES
(AND (NUMBERP X)
(EQUAL (LESSP X P) (NOT (ZEROP P)))
(NUMBERP V)
(NOT (EQUAL (ADD1 (PLUS X (TIMES P V))) 0))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (LESSP (PLUS P (ADD1 (PLUS X (TIMES P V))))
P))
(EQUAL X 0)
(NOT (EQUAL P 1))
(EQUAL (REMAINDER (ADD1 (PLUS X (TIMES P V)))
P)
1)
(NOT (EQUAL (PLUS P (ADD1 (PLUS X (TIMES P V))))
0)))
(EQUAL (REMAINDER (SUB1 (PLUS P (ADD1 (PLUS X (TIMES P V)))))
P)
0)),
which further simplifies, applying PLUS-ADD1, SUB1-ADD1, REMAINDER-X-X,
and REMAINDER-PLUS-TIMES-2, and unfolding NUMBERP, EQUAL, LESSP, ZEROP,
NOT, and PLUS, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.6 0.0 ]
N-O-I-LEMMA3
(PROVE-LEMMA N-O-I-LEMMA4
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0))
(EQUAL (INVERSE J P) J))
(OR (EQUAL (REMAINDER (ADD1 J) P) 0)
(EQUAL (REMAINDER (SUB1 J) P) 0)))
((USE (INVERSE-INVERTS) (N-O-I-LEMMA2))
(DISABLE INVERSE N-O-I-LEMMA1)))
WARNING: Note that the rewrite rule N-O-I-LEMMA4 will be stored so as to
apply only to terms with the nonrecursive function symbol OR.
This conjecture can be simplified, using the abbreviations OR, NOT, PRIME,
IMPLIES, AND, and DIFFERENCE-1, to:
(IMPLIES (AND (IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0)))
(EQUAL (REMAINDER (TIMES (INVERSE J P) J) P)
1))
(IMPLIES (AND (PRIME P)
(EQUAL (REMAINDER (SUB1 (TIMES J J)) P)
0))
(OR (EQUAL (REMAINDER (ADD1 J) P) 0)
(EQUAL (REMAINDER (SUB1 J) P) 0)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0))
(EQUAL (INVERSE J P) J)
(NOT (EQUAL (REMAINDER (ADD1 J) P) 0)))
(EQUAL (REMAINDER (SUB1 J) P) 0)).
This simplifies, rewriting with the lemma INVERSE-IS-UNIQUE, and unfolding the
definitions of PRIME, NOT, AND, IMPLIES, and OR, to:
(IMPLIES (AND (EQUAL (REMAINDER (TIMES J J) P) 1)
(NOT (EQUAL (REMAINDER (SUB1 (TIMES J J)) P)
0))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0))
(EQUAL (REMAINDER J P) J)
(NOT (EQUAL (REMAINDER (ADD1 J) P) 0)))
(EQUAL (REMAINDER (SUB1 J) P) 0)),
which again simplifies, using linear arithmetic, applying LESSP-TIMES-2 and
N-O-I-LEMMA3, and unfolding the function EQUAL, to:
T.
Q.E.D.
[ 0.0 0.3 0.0 ]
N-O-I-LEMMA4
(PROVE-LEMMA NO-OTHER-INVOLUTIONS
(REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP J (SUB1 P))
(LESSP 1 J))
(NOT (EQUAL (INVERSE J P) J)))
((USE (N-O-I-LEMMA4))
(DISABLE INVERSE)))
This formula can be simplified, using the abbreviations NOT, PRIME, AND, and
IMPLIES, to:
(IMPLIES (AND (IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0))
(EQUAL (INVERSE J P) J))
(OR (EQUAL (REMAINDER (ADD1 J) P) 0)
(EQUAL (REMAINDER (SUB1 J) P) 0)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P))
(LESSP 1 J))
(NOT (EQUAL (INVERSE J P) J))),
which simplifies, using linear arithmetic, applying the lemmas
REMAINDER-0-CROCK, DIFFERENCE-0, and SUB1-ADD1, and expanding the definitions
of PRIME, LESSP, REMAINDER, NOT, AND, OR, IMPLIES, EQUAL, SUB1, and NUMBERP,
to two new conjectures:
Case 2. (IMPLIES (AND (NOT (EQUAL J 0))
(NOT (LESSP (SUB1 J) (SUB1 P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P))
(NOT (EQUAL (SUB1 J) 0)))
(NOT (EQUAL (INVERSE J P) J))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP J 1)
(NOT (EQUAL J 0))
(NOT (LESSP (SUB1 J) (SUB1 P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P))
(NOT (EQUAL (SUB1 J) 0)))
(NOT (EQUAL (INVERSE J P) J))).
But this again simplifies, using linear arithmetic, to:
(IMPLIES (AND (NOT (NUMBERP J))
(LESSP J 1)
(NOT (EQUAL J 0))
(NOT (LESSP (SUB1 J) (SUB1 P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P))
(NOT (EQUAL (SUB1 J) 0)))
(NOT (EQUAL (INVERSE J P) J))).
This again simplifies, obviously, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL J 0))
(NOT (LESSP (SUB1 J) P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P))
(NOT (EQUAL (SUB1 J) 0)))
(NOT (EQUAL (INVERSE J P) J))).
This again simplifies, using linear arithmetic, to the formula:
(IMPLIES (AND (LESSP J 1)
(NOT (EQUAL J 0))
(NOT (LESSP (SUB1 J) P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P))
(NOT (EQUAL (SUB1 J) 0)))
(NOT (EQUAL (INVERSE J P) J))).
However this again simplifies, using linear arithmetic, to the goal:
(IMPLIES (AND (NOT (NUMBERP J))
(LESSP J 1)
(NOT (EQUAL J 0))
(NOT (LESSP (SUB1 J) P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P))
(NOT (EQUAL (SUB1 J) 0)))
(NOT (EQUAL (INVERSE J P) J))).
This again simplifies, obviously, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
NO-OTHER-INVOLUTIONS
(PROVE-LEMMA I-O-I-LEMMA NIL
(EQUAL (SUB1 (TIMES (DIFFERENCE P 2)
(DIFFERENCE P 2)))
(TIMES (DIFFERENCE P 3) (SUB1 P))))
This formula simplifies, rewriting with DIFFERENCE-1 and
COMMUTATIVITY-OF-TIMES, and opening up the definitions of SUB1, NUMBERP, EQUAL,
and DIFFERENCE, to the following four new formulas:
Case 4. (IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL (SUB1 P) 0)))
(EQUAL (SUB1 (TIMES (SUB1 (SUB1 P))
(SUB1 (SUB1 P))))
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))).
Appealing to the lemma SUB1-ELIM, we now replace P by (ADD1 X) to eliminate
(SUB1 P), X by (ADD1 Z) to eliminate (SUB1 X), and Z by (ADD1 X) to
eliminate (SUB1 Z). We rely upon the type restriction lemma noted when SUB1
was introduced to constrain the new variable. We must thus prove two new
goals:
Case 4.2.
(IMPLIES (AND (EQUAL Z 0)
(NUMBERP Z)
(NOT (EQUAL (ADD1 (ADD1 Z)) 0))
(NOT (EQUAL (ADD1 Z) 0)))
(EQUAL (SUB1 (TIMES Z Z))
(TIMES (ADD1 Z) (SUB1 Z)))),
which further simplifies, opening up the functions NUMBERP, EQUAL, TIMES,
and SUB1, to:
T.
Case 4.1.
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL (ADD1 X) 0))
(NOT (EQUAL (ADD1 (ADD1 (ADD1 X))) 0))
(NOT (EQUAL (ADD1 (ADD1 X)) 0)))
(EQUAL (SUB1 (TIMES (ADD1 X) (ADD1 X)))
(TIMES (ADD1 (ADD1 X)) X))),
which further simplifies, applying the lemmas TIMES-ADD1,
COMMUTATIVITY-OF-TIMES, SUB1-ADD1, PLUS-ADD1, and COMMUTATIVITY2-OF-PLUS,
and unfolding the function PLUS, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(EQUAL (SUB1 P) 0))
(EQUAL (SUB1 (TIMES (SUB1 (SUB1 P))
(SUB1 (SUB1 P))))
(TIMES (SUB1 P) 0))),
which again simplifies, opening up the definitions of SUB1, TIMES, and EQUAL,
to:
T.
Case 2. (IMPLIES (EQUAL P 0)
(EQUAL (SUB1 (TIMES 0 0))
(TIMES (SUB1 P) 0))),
which again simplifies, opening up TIMES, SUB1, and EQUAL, to:
T.
Case 1. (IMPLIES (NOT (NUMBERP P))
(EQUAL (SUB1 (TIMES 0 0))
(TIMES (SUB1 P) 0))),
which again simplifies, rewriting with the lemma SUB1-NNUMBERP, and
expanding the functions TIMES, SUB1, and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
I-O-I-LEMMA
(PROVE-LEMMA INVERSE-OF-INVERSE
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0)))
(EQUAL (INVERSE (INVERSE J P) P)
(REMAINDER J P)))
((USE (I-O-I-LEMMA)
(EXP-MOD-IS-1 (M J)
(J (SUB1 P))
(I (DIFFERENCE P 3))))))
WARNING: Note that the rewrite rule INVERSE-OF-INVERSE will be stored so as
to apply only to terms with the nonrecursive function symbol INVERSE.
This conjecture can be simplified, using the abbreviations NOT, PRIME, IMPLIES,
and AND, to:
(IMPLIES
(AND (EQUAL (SUB1 (TIMES (DIFFERENCE P 2)
(DIFFERENCE P 2)))
(TIMES (DIFFERENCE P 3) (SUB1 P)))
(IMPLIES (EQUAL (REMAINDER (EXP J (SUB1 P)) P)
1)
(EQUAL (REMAINDER (EXP J
(TIMES (DIFFERENCE P 3) (SUB1 P)))
P)
1))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0)))
(EQUAL (INVERSE (INVERSE J P) P)
(REMAINDER J P))).
This simplifies, rewriting with the lemmas DIFFERENCE-1,
COMMUTATIVITY-OF-TIMES, FERMAT-THM, EXP-BY-0, REMAINDER-OF-1, and DIFFERENCE-0,
and unfolding the functions SUB1, NUMBERP, EQUAL, DIFFERENCE, PRIME, IMPLIES,
INVERSE, LESSP, TIMES, and PRIME1, to the following two new goals:
Case 2. (IMPLIES (AND (NOT (EQUAL (SUB1 P) 0))
(EQUAL (SUB1 (TIMES (SUB1 (SUB1 P))
(SUB1 (SUB1 P))))
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))
(EQUAL (REMAINDER (EXP J
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))
P)
1)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0))
(NOT (EQUAL P 2)))
(EQUAL (INVERSE (REMAINDER (EXP J (SUB1 (SUB1 P))) P)
P)
(REMAINDER J P))).
But this again simplifies, using linear arithmetic, rewriting with
LESSP-REMAINDER-DIVISOR, S-P-I-I-LEMMA1, REMAINDER-EXP, EXP-EXP, EXP-PLUS,
EXP-BY-0, TIMES-1, COMMUTATIVITY-OF-TIMES, and DIFFERENCE-1, and unfolding
the definitions of EXP, DIFFERENCE, EQUAL, NUMBERP, SUB1, and INVERSE, to
the following two new conjectures:
Case 2.2.
(IMPLIES
(AND (NOT (EQUAL (SUB1 P) 0))
(EQUAL (SUB1 (PLUS 1
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P))))))
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))
(EQUAL (REMAINDER (EXP J
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))
P)
1)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0))
(NOT (EQUAL P 2))
(NOT (NUMBERP J)))
(EQUAL (REMAINDER (TIMES 0
(EXP J
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P))))))
P)
(REMAINDER J P))).
However this again simplifies, expanding LESSP, REMAINDER, and EQUAL, to:
T.
Case 2.1.
(IMPLIES
(AND (NOT (EQUAL (SUB1 P) 0))
(EQUAL (SUB1 (PLUS 1
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P))))))
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))
(EQUAL (REMAINDER (EXP J
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))
P)
1)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0))
(NOT (EQUAL P 2))
(NUMBERP J))
(EQUAL (REMAINDER (TIMES J
(EXP J
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P))))))
P)
(REMAINDER J P))),
which again simplifies, appealing to the lemma COROLLARY-55, and expanding
the functions PRIME and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL (SUB1 P) 0))
(EQUAL (SUB1 (TIMES (SUB1 (SUB1 P))
(SUB1 (SUB1 P))))
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))
(EQUAL (REMAINDER (EXP J
(TIMES (SUB1 P)
(SUB1 (SUB1 (SUB1 P)))))
P)
1)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0))
(EQUAL P 2))
(EQUAL (INVERSE (REMAINDER J 2) P)
(REMAINDER J P))),
which again simplifies, using linear arithmetic and applying
LESSP-REMAINDER-DIVISOR, to the new conjecture:
(IMPLIES (AND (EQUAL (REMAINDER J 2) 1)
(NOT (EQUAL (SUB1 2) 0))
(EQUAL (SUB1 (TIMES (SUB1 (SUB1 2))
(SUB1 (SUB1 2))))
(TIMES (SUB1 2)
(SUB1 (SUB1 (SUB1 2)))))
(EQUAL (REMAINDER (EXP J
(TIMES (SUB1 2)
(SUB1 (SUB1 (SUB1 2)))))
2)
1)
(NOT (EQUAL 2 0))
(NUMBERP 2)
(NOT (EQUAL 2 1))
(PRIME1 2 (SUB1 2))
(NOT (EQUAL 1 0)))
(EQUAL (INVERSE 1 2) 1)),
which again simplifies, rewriting with EXP-BY-0, and unfolding SUB1, EQUAL,
TIMES, REMAINDER, NUMBERP, PRIME1, and INVERSE, to:
T.
Q.E.D.
[ 0.0 0.5 0.0 ]
INVERSE-OF-INVERSE
(PROVE-LEMMA N-Z-I-LEMMA
(REWRITE)
(IMPLIES (AND (ZEROP I) (LESSP 1 P))
(EQUAL (INVERSE I P) 0)))
WARNING: Note that the rewrite rule N-Z-I-LEMMA will be stored so as to apply
only to terms with the nonrecursive function symbol INVERSE.
This simplifies, rewriting with EXP-OF-0 and DIFFERENCE-1, and opening up
ZEROP, DIFFERENCE, EQUAL, NUMBERP, SUB1, REMAINDER, INVERSE, and LESSP, to
seven new conjectures:
Case 7. (IMPLIES (AND (EQUAL I 0)
(LESSP 1 P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 (SUB1 P)) 0))
(EQUAL (REMAINDER 1 P) 0)),
which again simplifies, using linear arithmetic, to three new goals:
Case 7.3.
(IMPLIES (AND (NOT (NUMBERP P))
(LESSP 1 P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 (SUB1 P)) 0))
(EQUAL (REMAINDER 1 P) 0)),
which again simplifies, opening up the definition of LESSP, to:
T.
Case 7.2.
(IMPLIES (AND (EQUAL (SUB1 P) 0)
(LESSP 1 P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 (SUB1 P)) 0))
(EQUAL (REMAINDER 1 P) 0)),
which again simplifies, using linear arithmetic, to:
T.
Case 7.1.
(IMPLIES (AND (LESSP P 1)
(LESSP 1 P)
(NOT (EQUAL P 2))
(EQUAL (SUB1 (SUB1 P)) 0))
(EQUAL (REMAINDER 1 P) 0)),
which again simplifies, using linear arithmetic, to:
T.
Case 6. (IMPLIES (AND (EQUAL I 0)
(LESSP 1 P)
(NOT (EQUAL P 2))
(NOT (NUMBERP P)))
(EQUAL (REMAINDER 1 P) 0)),
which again simplifies, expanding the definition of LESSP, to:
T.
Case 5. (IMPLIES (AND (EQUAL I 0)
(LESSP 1 P)
(NOT (EQUAL P 2))
(EQUAL P 0))
(EQUAL (REMAINDER 1 P) 0)),
which again simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND (EQUAL I 0)
(LESSP 1 P)
(NOT (EQUAL P 2))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL (SUB1 (SUB1 P)) 0)))
(EQUAL (REMAINDER 0 P) 0)),
which again simplifies, rewriting with the lemma REMAINDER-0-CROCK, and
opening up the function EQUAL, to:
T.
Case 3. (IMPLIES (AND (NOT (NUMBERP I))
(LESSP 1 P)
(NOT (EQUAL P 2))
(NOT (NUMBERP P)))
(EQUAL (REMAINDER (EXP I 0) P) 0)),
which again simplifies, opening up the definition of LESSP, to:
T.
Case 2. (IMPLIES (AND (NOT (NUMBERP I))
(LESSP 1 P)
(NOT (EQUAL P 2))
(EQUAL P 0))
(EQUAL (REMAINDER (EXP I 0) P) 0)),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (NUMBERP I))
(LESSP 1 P)
(NOT (EQUAL P 2))
(NOT (EQUAL P 0))
(NUMBERP P))
(EQUAL (REMAINDER (EXP I (SUB1 (SUB1 P))) P)
0)).
Applying the lemma SUB1-ELIM, replace P by (ADD1 X) to eliminate (SUB1 P)
and X by (ADD1 Z) to eliminate (SUB1 X). We use the type restriction lemma
noted when SUB1 was introduced to restrict the new variable. We thus obtain
the following two new conjectures:
Case 1.2.
(IMPLIES (AND (EQUAL X 0)
(NUMBERP X)
(NOT (NUMBERP I))
(LESSP 1 (ADD1 X))
(NOT (EQUAL (ADD1 X) 2))
(NOT (EQUAL (ADD1 X) 0)))
(EQUAL (REMAINDER (EXP I (SUB1 X)) (ADD1 X))
0)).
But this further simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL (ADD1 Z) 0))
(NOT (NUMBERP I))
(LESSP 1 (ADD1 (ADD1 Z)))
(NOT (EQUAL (ADD1 (ADD1 Z)) 2))
(NOT (EQUAL (ADD1 (ADD1 Z)) 0)))
(EQUAL (REMAINDER (EXP I Z) (ADD1 (ADD1 Z)))
0)),
which further simplifies, rewriting with SUB1-ADD1 and ADD1-EQUAL, and
unfolding the definitions of SUB1, NUMBERP, EQUAL, and LESSP, to the new
conjecture:
(IMPLIES (AND (NUMBERP Z)
(NOT (NUMBERP I))
(NOT (EQUAL Z 0)))
(EQUAL (REMAINDER (EXP I Z) (ADD1 (ADD1 Z)))
0)),
which we would normally push and work on later by induction. But if we
must use induction to prove the input conjecture, we prefer to induct on
the original formulation of the problem. Thus we will disregard all that
we have previously done, give the name *1 to the original input, and work
on it.
So now let us return to:
(IMPLIES (AND (ZEROP I) (LESSP 1 P))
(EQUAL (INVERSE I P) 0)),
named *1. Let us appeal to the induction principle. There is only one
suggested induction. We will induct according to the following scheme:
(AND (IMPLIES (OR (EQUAL P 0) (NOT (NUMBERP P)))
(p I P))
(IMPLIES (AND (NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
(OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(p I P))
(IMPLIES (AND (NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(p I (SUB1 P)))
(p I P))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT establish that the measure (COUNT P) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme generates four new formulas:
Case 4. (IMPLIES (AND (OR (EQUAL P 0) (NOT (NUMBERP P)))
(ZEROP I)
(LESSP 1 P))
(EQUAL (INVERSE I P) 0)),
which simplifies, unfolding the definitions of NOT, OR, ZEROP, and LESSP, to:
T.
Case 3. (IMPLIES (AND (NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
(OR (EQUAL 1 0) (NOT (NUMBERP 1)))
(ZEROP I)
(LESSP 1 P))
(EQUAL (INVERSE I P) 0)),
which simplifies, opening up NOT, OR, EQUAL, and NUMBERP, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(NOT (LESSP 1 (SUB1 P)))
(ZEROP I)
(LESSP 1 P))
(EQUAL (INVERSE I P) 0)),
which simplifies, using linear arithmetic, to two new formulas:
Case 2.2.
(IMPLIES (AND (NOT (NUMBERP P))
(NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(NOT (LESSP 1 (SUB1 P)))
(ZEROP I)
(LESSP 1 P))
(EQUAL (INVERSE I P) 0)),
which again simplifies, unfolding the functions NOT and OR, to:
T.
Case 2.1.
(IMPLIES (AND (NUMBERP P)
(NOT (OR (EQUAL 2 0) (NOT (NUMBERP 2))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(NOT (LESSP 1 (SUB1 2)))
(ZEROP I)
(LESSP 1 2))
(EQUAL (INVERSE I 2) 0)),
which again simplifies, unfolding the definitions of EQUAL, NUMBERP, NOT,
OR, SUB1, LESSP, ZEROP, INVERSE, and REMAINDER, to:
T.
Case 1. (IMPLIES (AND (NOT (OR (EQUAL P 0) (NOT (NUMBERP P))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(EQUAL (INVERSE I (SUB1 P)) 0)
(ZEROP I)
(LESSP 1 P))
(EQUAL (INVERSE I P) 0)),
which simplifies, rewriting with DIFFERENCE-1, EXP-OF-0, REMAINDER-0-CROCK,
EXP-BY-0, TIMES-1, and COMMUTATIVITY-OF-TIMES, and expanding the functions
NOT, OR, EQUAL, NUMBERP, DIFFERENCE, SUB1, INVERSE, ZEROP, LESSP, REMAINDER,
and EXP, to the following three new conjectures:
Case 1.3.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL (SUB1 P) 2))
(NOT (EQUAL (SUB1 P) 0))
(EQUAL (REMAINDER (EXP I (SUB1 (SUB1 (SUB1 P))))
(SUB1 P))
0)
(EQUAL I 0)
(NOT (EQUAL P 2))
(EQUAL (SUB1 (SUB1 P)) 0))
(EQUAL (REMAINDER 1 P) 0)).
However this again simplifies, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL (SUB1 P) 2))
(NOT (EQUAL (SUB1 P) 0))
(EQUAL (REMAINDER (EXP I (SUB1 (SUB1 (SUB1 P))))
(SUB1 P))
0)
(EQUAL I 0)
(NOT (EQUAL P 2))
(NOT (EQUAL (SUB1 (SUB1 P)) 0)))
(EQUAL (REMAINDER 0 P) 0)),
which again simplifies, applying EXP-OF-0 and REMAINDER-0-CROCK, and
expanding EQUAL, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL (SUB1 P) 2))
(NOT (EQUAL (SUB1 P) 0))
(EQUAL (REMAINDER (EXP I (SUB1 (SUB1 (SUB1 P))))
(SUB1 P))
0)
(NOT (NUMBERP I))
(NOT (EQUAL P 2)))
(EQUAL (REMAINDER (EXP I (SUB1 (SUB1 P))) P)
0)).
However this again simplifies, opening up the definition of EXP, to two
new conjectures:
Case 1.1.2.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL (SUB1 P) 2))
(NOT (EQUAL (SUB1 P) 0))
(EQUAL (REMAINDER (EXP I (SUB1 (SUB1 (SUB1 P))))
(SUB1 P))
0)
(NOT (NUMBERP I))
(NOT (EQUAL P 2))
(NOT (EQUAL (SUB1 (SUB1 P)) 0)))
(EQUAL (REMAINDER (TIMES I
(EXP I (SUB1 (SUB1 (SUB1 P)))))
P)
0)),
which again simplifies, rewriting with EQUAL-TIMES-0, and unfolding
LESSP and REMAINDER, to:
T.
Case 1.1.1.
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL (SUB1 P) 2))
(NOT (EQUAL (SUB1 P) 0))
(EQUAL (REMAINDER (EXP I (SUB1 (SUB1 (SUB1 P))))
(SUB1 P))
0)
(NOT (NUMBERP I))
(NOT (EQUAL P 2))
(EQUAL (SUB1 (SUB1 P)) 0))
(EQUAL (REMAINDER 1 P) 0)).
But this again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.3 0.0 ]
N-Z-I-LEMMA
(PROVE-LEMMA NON-ZEROP-INVERSE
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0)))
(NOT (ZEROP (INVERSE J P))))
((USE (N-Z-I-LEMMA (I (INVERSE J P)))
(INVERSE-OF-INVERSE))
(DISABLE INVERSE)))
WARNING: Note that the rewrite rule NON-ZEROP-INVERSE will be stored so as to
apply only to terms with the nonrecursive function symbol ZEROP.
This formula can be simplified, using the abbreviations NOT, PRIME, IMPLIES,
and AND, to:
(IMPLIES (AND (IMPLIES (AND (ZEROP (INVERSE J P))
(LESSP 1 P))
(EQUAL (INVERSE (INVERSE J P) P) 0))
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0)))
(EQUAL (INVERSE (INVERSE J P) P)
(REMAINDER J P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0)))
(NOT (ZEROP (INVERSE J P)))),
which simplifies, using linear arithmetic, rewriting with the lemmas
LESSP-REMAINDER-DIVISOR and N-Z-I-LEMMA, and opening up the functions ZEROP,
SUB1, NUMBERP, EQUAL, LESSP, AND, IMPLIES, PRIME, and NOT, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
NON-ZEROP-INVERSE
(PROVE-LEMMA B-I-LEMMA2
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0))
(EQUAL (INVERSE J P) (SUB1 P)))
(EQUAL (REMAINDER J P) (SUB1 P)))
((USE (INVERSE-OF-INVERSE))
(DISABLE INVERSE)))
This formula can be simplified, using the abbreviations NOT, PRIME, AND, and
IMPLIES, to:
(IMPLIES (AND (IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0)))
(EQUAL (INVERSE (INVERSE J P) P)
(REMAINDER J P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER J P) 0))
(EQUAL (INVERSE J P) (SUB1 P)))
(EQUAL (REMAINDER J P) (SUB1 P))),
which simplifies, applying SUB1-P-IS-INVOLUTION, and expanding the functions
PRIME, NOT, AND, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
B-I-LEMMA2
(PROVE-LEMMA B-I-LEMMA1 NIL
(IMPLIES (LESSP 1 P)
(LEQ (INVERSE J P) (SUB1 P))))
This simplifies, appealing to the lemma DIFFERENCE-1, and opening up the
functions DIFFERENCE, EQUAL, NUMBERP, SUB1, and INVERSE, to four new formulas:
Case 4. (IMPLIES (AND (LESSP 1 P)
(NOT (EQUAL P 2))
(NOT (NUMBERP P)))
(NOT (LESSP (SUB1 P)
(REMAINDER (EXP J 0) P)))),
which again simplifies, opening up the definition of LESSP, to:
T.
Case 3. (IMPLIES (AND (LESSP 1 P)
(NOT (EQUAL P 2))
(EQUAL P 0))
(NOT (LESSP (SUB1 P)
(REMAINDER (EXP J 0) P)))),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (LESSP 1 P)
(NOT (EQUAL P 2))
(NOT (EQUAL P 0))
(NUMBERP P))
(NOT (LESSP (SUB1 P)
(REMAINDER (EXP J (SUB1 (SUB1 P)))
P)))),
which again simplifies, using linear arithmetic and applying
LESSP-REMAINDER-DIVISOR, to:
T.
Case 1. (IMPLIES (AND (LESSP 1 P) (EQUAL P 2))
(NOT (LESSP (SUB1 P) (REMAINDER J 2)))).
This again simplifies, using linear arithmetic, rewriting with the lemma
LESSP-REMAINDER-DIVISOR, and expanding the definition of EQUAL, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
B-I-LEMMA1
(PROVE-LEMMA BOUNDED-INVERSE
(REWRITE)
(IMPLIES (AND (PRIME P) (LESSP J (SUB1 P)))
(LESSP (INVERSE J P) (SUB1 P)))
((USE (B-I-LEMMA1) (B-I-LEMMA2))
(DISABLE INVERSE)))
WARNING: Note that the linear lemma BOUNDED-INVERSE is being stored under the
term (INVERSE J P), which is unusual because INVERSE is a nonrecursive
function symbol.
WARNING: Note that the proposed lemma BOUNDED-INVERSE is to be stored as zero
type prescription rules, zero compound recognizer rules, one linear rule, and
zero replacement rules.
This formula can be simplified, using the abbreviations PRIME, IMPLIES, and
AND, to:
(IMPLIES (AND (IMPLIES (LESSP 1 P)
(IF (LESSP (SUB1 P) (INVERSE J P))
F T))
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0))
(EQUAL (INVERSE J P) (SUB1 P)))
(EQUAL (REMAINDER J P) (SUB1 P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P)))
(LESSP (INVERSE J P) (SUB1 P))),
which simplifies, using linear arithmetic, rewriting with the lemmas
REMAINDER-0-CROCK, DIFFERENCE-0, and N-Z-I-LEMMA, and opening up the functions
SUB1, NUMBERP, EQUAL, LESSP, IMPLIES, PRIME1, PRIME, REMAINDER, NOT, AND, and
ZEROP, to three new conjectures:
Case 3. (IMPLIES (AND (NOT (LESSP (SUB1 P) (INVERSE J P)))
(NOT (LESSP J P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P)))
(LESSP (INVERSE J P) (SUB1 P))),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (LESSP (SUB1 P) (INVERSE J P)))
(NOT (EQUAL (INVERSE J P) (SUB1 P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP J (SUB1 P)))
(LESSP (INVERSE J P) (SUB1 P))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP (SUB1 P) (INVERSE J P)))
(EQUAL J (SUB1 P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P J)
(LESSP J J))
(LESSP (INVERSE J P) J)),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
BOUNDED-INVERSE
(DEFN INVERSE-LIST
(I P)
(IF (ZEROP I)
NIL
(IF (EQUAL I 1)
(CONS 1 NIL)
(IF (MEMBER I (INVERSE-LIST (SUB1 I) P))
(INVERSE-LIST (SUB1 I) P)
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT I) decreases according to the well-founded
relation LESSP in each recursive call. Hence, INVERSE-LIST is accepted under
the principle of definition. Note that:
(OR (LITATOM (INVERSE-LIST I P))
(LISTP (INVERSE-LIST I P)))
is a theorem.
[ 0.0 0.0 0.0 ]
INVERSE-LIST
(PROVE-LEMMA ALL-NON-ZEROP-INVERSE-LIST
(REWRITE)
(IMPLIES (AND (PRIME P) (LESSP I (SUB1 P)))
(ALL-NON-ZEROP (INVERSE-LIST I P)))
((USE (NON-ZEROP-INVERSE (J I)))
(INDUCT (INVERSE-LIST I P))
(DISABLE INVERSE)))
This simplifies, applying SUB1-NNUMBERP, and opening up the definitions of
PRIME, NOT, AND, ZEROP, IMPLIES, SUB1, EQUAL, LESSP, INVERSE-LIST, and OR, to
the following 12 new formulas:
Case 12.(IMPLIES (AND (EQUAL (REMAINDER I P) 0)
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP (INVERSE-LIST (SUB1 I) P))).
This again simplifies, using linear arithmetic, to:
T.
Case 11.(IMPLIES (AND (EQUAL (REMAINDER I P) 0)
(NOT (NUMBERP I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP NIL)),
which again simplifies, expanding the functions LESSP, REMAINDER, EQUAL, and
ALL-NON-ZEROP, to:
T.
Case 10.(IMPLIES (AND (EQUAL (REMAINDER I P) 0)
(EQUAL I 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP NIL)),
which again simplifies, rewriting with REMAINDER-0-CROCK, and expanding the
definitions of EQUAL, LESSP, and ALL-NON-ZEROP, to:
T.
Case 9. (IMPLIES (AND (EQUAL (REMAINDER I P) 0)
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP '(1))).
However this again simplifies, rewriting with the lemma REMAINDER-OF-1, and
unfolding EQUAL, to:
T.
Case 8. (IMPLIES (AND (EQUAL (REMAINDER I P) 0)
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(ALL-NON-ZEROP (INVERSE-LIST (SUB1 I) P))
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which again simplifies, using linear arithmetic, rewriting with
REMAINDER-0-CROCK, DIFFERENCE-0, CDR-CONS, and CAR-CONS, and opening up the
functions LESSP, REMAINDER, and ALL-NON-ZEROP, to the new conjecture:
(IMPLIES (AND (NOT (LESSP (SUB1 I) (SUB1 P)))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(ALL-NON-ZEROP (INVERSE-LIST (SUB1 I) P))
(LESSP I (SUB1 P)))
(NOT (EQUAL (INVERSE I P) 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 7. (IMPLIES (AND (EQUAL (REMAINDER I P) 0)
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which again simplifies, using linear arithmetic, to:
T.
Case 6. (IMPLIES (AND (NOT (EQUAL (INVERSE I P) 0))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP (INVERSE-LIST (SUB1 I) P))),
which again simplifies, using linear arithmetic, to:
T.
Case 5. (IMPLIES (AND (NOT (EQUAL (INVERSE I P) 0))
(NOT (NUMBERP I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP NIL)),
which again simplifies, using linear arithmetic, applying N-Z-I-LEMMA and
BOUNDED-INVERSE, and opening up the definitions of PRIME, ZEROP, and EQUAL,
to:
T.
Case 4. (IMPLIES (AND (NOT (EQUAL (INVERSE I P) 0))
(EQUAL I 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP NIL)).
But this again simplifies, using linear arithmetic, rewriting with
N-Z-I-LEMMA, and unfolding the definitions of ZEROP and EQUAL, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL (INVERSE I P) 0))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP '(1))).
But this again simplifies, expanding the functions EQUAL, NUMBERP, and
ALL-NON-ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL (INVERSE I P) 0))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(ALL-NON-ZEROP (INVERSE-LIST (SUB1 I) P))
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which again simplifies, applying the lemmas CDR-CONS and CAR-CONS, and
opening up the definition of ALL-NON-ZEROP, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL (INVERSE I P) 0))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(LESSP I (SUB1 P)))
(ALL-NON-ZEROP (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.7 0.0 ]
ALL-NON-ZEROP-INVERSE-LIST
(PROVE-LEMMA BOUNDED-INVERSE-LIST
(REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I (SUB1 P))
(EQUAL J (DIFFERENCE P 2)))
(ALL-LESSEQP (INVERSE-LIST I P) J))
((USE (BOUNDED-INVERSE (J I)))
(INDUCT (INVERSE-LIST I P))
(DISABLE INVERSE)))
This conjecture simplifies, using linear arithmetic, applying the lemmas
SUB1-NNUMBERP, DIFFERENCE-0, and DIFFERENCE-1, and expanding PRIME, AND,
IMPLIES, ZEROP, NOT, SUB1, EQUAL, LESSP, DIFFERENCE, OR, INVERSE-LIST, and
NUMBERP, to six new formulas:
Case 6. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(LESSP I (SUB1 P))
(EQUAL J (SUB1 (SUB1 P))))
(ALL-LESSEQP (INVERSE-LIST (SUB1 I) P)
J)),
which again simplifies, using linear arithmetic, to:
T.
Case 5. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
(NOT (NUMBERP I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL J (SUB1 (SUB1 P))))
(ALL-LESSEQP NIL J)),
which again simplifies, using linear arithmetic, appealing to the lemmas
N-Z-I-LEMMA, PIGEON-HOLE-PRINCIPLE-LEMMA-2, and ADD1-SUB1, and expanding
ZEROP, EQUAL, LESSP, ALL-LESSEQP, MEMBER, and LISTP, to:
T.
Case 4. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
(EQUAL I 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL J (SUB1 (SUB1 P))))
(ALL-LESSEQP NIL J)),
which again simplifies, using linear arithmetic, applying N-Z-I-LEMMA,
PIGEON-HOLE-PRINCIPLE-LEMMA-2, and ADD1-SUB1, and unfolding ZEROP, EQUAL,
LESSP, ALL-LESSEQP, MEMBER, and LISTP, to:
T.
Case 3. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL J (SUB1 (SUB1 P))))
(ALL-LESSEQP '(1) J)).
However this again simplifies, rewriting with the lemmas
PIGEON-HOLE-PRINCIPLE-LEMMA-2 and ADD1-SUB1, and opening up the definitions
of EQUAL, NUMBERP, CDR, CAR, LISTP, ALL-LESSEQP, and MEMBER, to:
(IMPLIES (AND (LESSP (INVERSE 1 P) (SUB1 P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP 1 (SUB1 P)))
(NOT (LESSP (SUB1 (SUB1 P)) 1))).
However this again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL J (SUB1 (SUB1 P)))
(ALL-LESSEQP (INVERSE-LIST (SUB1 I) P)
J)
(LESSP I (SUB1 P)))
(ALL-LESSEQP (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
J)),
which again simplifies, applying CDR-CONS and CAR-CONS, and expanding the
function ALL-LESSEQP, to the following two new goals:
Case 2.2.
(IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(ALL-LESSEQP (INVERSE-LIST (SUB1 I) P)
(SUB1 (SUB1 P)))
(LESSP I (SUB1 P)))
(NOT (LESSP (SUB1 (SUB1 P)) I))).
This again simplifies, using linear arithmetic, to:
T.
Case 2.1.
(IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(ALL-LESSEQP (INVERSE-LIST (SUB1 I) P)
(SUB1 (SUB1 P)))
(LESSP I (SUB1 P)))
(NOT (LESSP (SUB1 (SUB1 P))
(INVERSE I P)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (LESSP (INVERSE I P) (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(LESSP I (SUB1 P))
(EQUAL J (SUB1 (SUB1 P))))
(ALL-LESSEQP (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
J)),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.7 0.0 ]
BOUNDED-INVERSE-LIST
(PROVE-LEMMA SUBSETP-POSITIVES
(REWRITE)
(SUBSETP (POSITIVES N)
(INVERSE-LIST N P)))
Name the conjecture *1.
Let us appeal to the induction principle. Two inductions are suggested
by terms in the conjecture. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP N) (p N P))
(IMPLIES (AND (NOT (ZEROP N)) (EQUAL N 1))
(p N P))
(IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1))
(MEMBER N (INVERSE-LIST (SUB1 N) P))
(p (SUB1 N) P))
(p N P))
(IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1))
(NOT (MEMBER N (INVERSE-LIST (SUB1 N) P)))
(p (SUB1 N) P))
(p N P))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT N) decreases according to the well-founded relation
LESSP in each induction step of the scheme. The above induction scheme leads
to four new conjectures:
Case 4. (IMPLIES (ZEROP N)
(SUBSETP (POSITIVES N)
(INVERSE-LIST N P))),
which simplifies, expanding ZEROP, POSITIVES, EQUAL, INVERSE-LIST, and
SUBSETP, to:
T.
Case 3. (IMPLIES (AND (NOT (ZEROP N)) (EQUAL N 1))
(SUBSETP (POSITIVES N)
(INVERSE-LIST N P))),
which simplifies, unfolding the definitions of ZEROP, POSITIVES, NUMBERP,
EQUAL, INVERSE-LIST, and SUBSETP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1))
(MEMBER N (INVERSE-LIST (SUB1 N) P))
(SUBSETP (POSITIVES (SUB1 N))
(INVERSE-LIST (SUB1 N) P)))
(SUBSETP (POSITIVES N)
(INVERSE-LIST N P))),
which simplifies, rewriting with CDR-CONS and CAR-CONS, and unfolding ZEROP,
POSITIVES, INVERSE-LIST, and SUBSETP, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL N 1))
(NOT (MEMBER N (INVERSE-LIST (SUB1 N) P)))
(SUBSETP (POSITIVES (SUB1 N))
(INVERSE-LIST (SUB1 N) P)))
(SUBSETP (POSITIVES N)
(INVERSE-LIST N P))).
This simplifies, rewriting with DIFFERENCE-1, SUBSETP-CONS, CDR-CONS, and
CAR-CONS, and unfolding the definitions of ZEROP, POSITIVES, INVERSE-LIST,
DIFFERENCE, EQUAL, NUMBERP, SUB1, INVERSE, MEMBER, and SUBSETP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
SUBSETP-POSITIVES
(PROVE-LEMMA INVERSE-1
(REWRITE)
(IMPLIES (LESSP 1 P)
(EQUAL (INVERSE 1 P) 1)))
WARNING: Note that the rewrite rule INVERSE-1 will be stored so as to apply
only to terms with the nonrecursive function symbol INVERSE.
This simplifies, appealing to the lemmas REMAINDER-OF-1, EXP-OF-1, and
DIFFERENCE-1, and opening up the definitions of DIFFERENCE, EQUAL, NUMBERP,
SUB1, REMAINDER, and INVERSE, to:
(IMPLIES (AND (LESSP 1 P) (NOT (EQUAL P 2)))
(NOT (EQUAL P 1))).
This again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INVERSE-1
(PROVE-LEMMA A-D-I-L-LEMMA1
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(MEMBER J (INVERSE-LIST I P)))
(MEMBER (INVERSE J P)
(INVERSE-LIST I P)))
((USE (INVERSE-OF-INVERSE (J I)))
(INDUCT (INVERSE-LIST I P))
(DISABLE INVERSE)))
This conjecture simplifies, rewriting with REMAINDER-WRT-12 and
REMAINDER-WRT-1, and opening up the functions PRIME, NOT, AND, IMPLIES, ZEROP,
EQUAL, REMAINDER, LESSP, INVERSE-LIST, OR, SUB1, and NUMBERP, to nine new
conjectures:
Case 9. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) P))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(MEMBER J (INVERSE-LIST (SUB1 I) P)))
(MEMBER (INVERSE J P)
(INVERSE-LIST (SUB1 I) P))),
which again simplifies, using linear arithmetic, to:
T.
Case 8. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL (REMAINDER (SUB1 I) P) 0)
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(MEMBER J (INVERSE-LIST (SUB1 I) P)))
(MEMBER (INVERSE J P)
(INVERSE-LIST (SUB1 I) P))),
which again simplifies, using linear arithmetic, rewriting with
INVERSE-OF-INVERSE, REMAINDER-0-CROCK, and DIFFERENCE-0, and opening up the
definitions of PRIME, REMAINDER, EQUAL, INVERSE-LIST, LISTP, and MEMBER, to
the new conjecture:
(IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) P))
(LESSP I P)
(MEMBER J (INVERSE-LIST (SUB1 I) P)))
(MEMBER (INVERSE J P)
(INVERSE-LIST (SUB1 I) P))),
which again simplifies, using linear arithmetic, to:
T.
Case 7. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(NOT (NUMBERP I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(MEMBER J NIL))
(MEMBER (INVERSE J P) NIL)),
which again simplifies, using linear arithmetic, rewriting with N-Z-I-LEMMA,
and opening up the definitions of ZEROP, LESSP, REMAINDER, and EQUAL, to:
T.
Case 6. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(EQUAL I 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(MEMBER J NIL))
(MEMBER (INVERSE J P) NIL)).
However this again simplifies, using linear arithmetic, applying N-Z-I-LEMMA
and REMAINDER-0-CROCK, and expanding ZEROP and EQUAL, to:
T.
Case 5. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(MEMBER J '(1)))
(MEMBER (INVERSE J P) '(1))).
But this again simplifies, rewriting with INVERSE-1 and REMAINDER-OF-1, and
unfolding the definitions of EQUAL, NUMBERP, CDR, CAR, LISTP, and MEMBER, to:
T.
Case 4. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL (REMAINDER (SUB1 I) P) 0)
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(MEMBER J
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))
(MEMBER (INVERSE J P)
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))).
This again simplifies, using linear arithmetic, rewriting with
INVERSE-OF-INVERSE, REMAINDER-0-CROCK, DIFFERENCE-0, CDR-CONS, and CAR-CONS,
and opening up the definitions of PRIME, REMAINDER, EQUAL, INVERSE-LIST,
MEMBER, and LISTP, to the following three new conjectures:
Case 4.3.
(IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL (SUB1 I) 0)
(LESSP I P)
(EQUAL J (INVERSE I P))
(NOT (EQUAL (INVERSE J P) I)))
(EQUAL (INVERSE J P) J)).
This again simplifies, using linear arithmetic, to:
T.
Case 4.2.
(IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) P))
(LESSP I P)
(EQUAL J (INVERSE I P))
(NOT (EQUAL (INVERSE J P) I))
(NOT (EQUAL (INVERSE J P) J)))
(MEMBER (INVERSE J P)
(INVERSE-LIST (SUB1 I) P))),
which again simplifies, using linear arithmetic, to:
T.
Case 4.1.
(IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) P))
(LESSP I P)
(MEMBER J (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL (INVERSE J P) I))
(NOT (EQUAL (INVERSE J P) (INVERSE I P))))
(MEMBER (INVERSE J P)
(INVERSE-LIST (SUB1 I) P))),
which again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) P))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(MEMBER J
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))
(MEMBER (INVERSE J P)
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(MEMBER (INVERSE J P)
(INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(MEMBER J
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))
(MEMBER (INVERSE J P)
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which again simplifies, applying INVERSE-OF-INVERSE, CDR-CONS, and CAR-CONS,
and expanding the functions PRIME, REMAINDER, and MEMBER, to:
T.
Case 1. (IMPLIES (AND (EQUAL (INVERSE (INVERSE I P) P)
(REMAINDER I P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (MEMBER J (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(MEMBER J
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))))
(MEMBER (INVERSE J P)
(CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))).
This again simplifies, rewriting with the lemmas INVERSE-OF-INVERSE,
CDR-CONS, and CAR-CONS, and expanding PRIME, REMAINDER, and MEMBER, to:
(IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (MEMBER J (INVERSE-LIST (SUB1 I) P)))
(LESSP I P)
(EQUAL J (INVERSE I P))
(NOT (EQUAL (INVERSE J P) I))
(NOT (EQUAL (INVERSE J P) J)))
(MEMBER (INVERSE J P)
(INVERSE-LIST (SUB1 I) P))).
This again simplifies, using linear arithmetic, rewriting with
INVERSE-OF-INVERSE, and unfolding the definitions of REMAINDER and PRIME, to:
T.
Q.E.D.
[ 0.0 3.1 0.0 ]
A-D-I-L-LEMMA1
(PROVE-LEMMA A-D-I-L-LEMMA2
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER I P) 0))
(NOT (EQUAL (REMAINDER J P) 0))
(LESSP I P)
(LESSP J P)
(MEMBER (INVERSE J P)
(INVERSE-LIST I P)))
(MEMBER J (INVERSE-LIST I P)))
((USE (INVERSE-OF-INVERSE)
(A-D-I-L-LEMMA1 (J (INVERSE J P))))
(DISABLE INVERSE INVERSE-LIST INVERSE-OF-INVERSE A-D-I-L-LEMMA1)))
This conjecture can be simplified, using the abbreviations NOT, PRIME, IMPLIES,
and AND, to:
(IMPLIES (AND (IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER J P) 0)))
(EQUAL (INVERSE (INVERSE J P) P)
(REMAINDER J P)))
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP I P)
(MEMBER (INVERSE J P)
(INVERSE-LIST I P)))
(MEMBER (INVERSE (INVERSE J P) P)
(INVERSE-LIST I P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER I P) 0))
(NOT (EQUAL (REMAINDER J P) 0))
(LESSP I P)
(LESSP J P)
(MEMBER (INVERSE J P)
(INVERSE-LIST I P)))
(MEMBER J (INVERSE-LIST I P))).
This simplifies, using linear arithmetic, rewriting with REMAINDER-0-CROCK and
N-Z-I-LEMMA, and unfolding the definitions of PRIME, REMAINDER, NOT, AND,
IMPLIES, EQUAL, LESSP, and ZEROP, to:
T.
Q.E.D.
[ 0.0 0.3 0.0 ]
A-D-I-L-LEMMA2
(PROVE-LEMMA A-D-I-L-LEMMA3
(REWRITE)
(IMPLIES (AND (PRIME P)
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
(ALL-DISTINCT (INVERSE-LIST I P)))
((USE (A-D-I-L-LEMMA2 (J I) (I (SUB1 I)))
(NO-OTHER-INVOLUTIONS (J I)))
(DISABLE INVERSE)))
This formula can be simplified, using the abbreviations PRIME, IMPLIES, and
AND, to:
(IMPLIES (AND (IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP (SUB1 I) P)
(LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(IMPLIES (AND (PRIME P)
(LESSP I (SUB1 P))
(LESSP 1 I))
(NOT (EQUAL (INVERSE I P) I)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
(ALL-DISTINCT (INVERSE-LIST I P))),
which simplifies, using linear arithmetic, rewriting with REMAINDER-0-CROCK,
DIFFERENCE-0, SUB1-NNUMBERP, and N-Z-I-LEMMA, and opening up PRIME, REMAINDER,
NOT, LESSP, AND, IMPLIES, SUB1, NUMBERP, EQUAL, INVERSE-LIST, ALL-DISTINCT,
LISTP, MEMBER, and ZEROP, to the following 43 new goals:
Case 43.(IMPLIES (AND (LESSP I 1)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP (SUB1 I) P)
(LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1)))
(ALL-DISTINCT (LIST I (INVERSE I P)))).
However this again simplifies, using linear arithmetic, to:
T.
Case 42.(IMPLIES (AND (LESSP I 1)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP (SUB1 I) P)
(LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))),
which again simplifies, using linear arithmetic, to:
T.
Case 41.(IMPLIES (AND (LESSP I 1)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP (SUB1 I) P)
(LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL I 0))
(ALL-DISTINCT NIL)),
which again simplifies, using linear arithmetic, rewriting with the lemmas
REMAINDER-0-CROCK and N-Z-I-LEMMA, and expanding the functions LESSP, PRIME,
EQUAL, NOT, ZEROP, INVERSE-LIST, MEMBER, AND, IMPLIES, SUB1, and
ALL-DISTINCT, to:
T.
Case 40.(IMPLIES (AND (LESSP I 1)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP (SUB1 I) P)
(LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)),
which again simplifies, using linear arithmetic, applying REMAINDER-0-CROCK,
N-Z-I-LEMMA, and SUB1-NNUMBERP, and opening up the definitions of NUMBERP,
EQUAL, LESSP, PRIME, NOT, REMAINDER, ZEROP, INVERSE-LIST, MEMBER, AND, LISTP,
IMPLIES, and ALL-DISTINCT, to:
T.
Case 39.(IMPLIES (AND (LESSP I 1)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP (SUB1 I) P)
(LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
(ALL-DISTINCT (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))).
But this again simplifies, using linear arithmetic, to:
T.
Case 38.(IMPLIES (AND (LESSP I 1)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP (SUB1 I) P)
(LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))),
which again simplifies, using linear arithmetic, to:
T.
Case 37.(IMPLIES (AND (LESSP I 1)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP (SUB1 I) P)
(LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(EQUAL I 0))
(ALL-DISTINCT NIL)),
which again simplifies, using linear arithmetic, rewriting with
REMAINDER-0-CROCK and N-Z-I-LEMMA, and expanding LESSP, PRIME, SUB1, EQUAL,
NOT, ZEROP, INVERSE-LIST, MEMBER, AND, and IMPLIES, to:
T.
Case 36.(IMPLIES (AND (LESSP I 1)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER (SUB1 I) P) 0))
(NOT (EQUAL (REMAINDER I P) 0))
(LESSP (SUB1 I) P)
(LESSP I P)
(MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)).
However this again simplifies, using linear arithmetic, applying
SUB1-NNUMBERP, REMAINDER-0-CROCK, and N-Z-I-LEMMA, and opening up the
functions NUMBERP, EQUAL, LESSP, PRIME, NOT, REMAINDER, ZEROP, INVERSE-LIST,
MEMBER, AND, LISTP, IMPLIES, and ALL-DISTINCT, to:
T.
Case 35.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (LESSP (SUB1 I) P))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1)))
(ALL-DISTINCT (LIST I (INVERSE I P)))).
However this again simplifies, using linear arithmetic, to:
T.
Case 34.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (LESSP (SUB1 I) P))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))),
which again simplifies, using linear arithmetic, to:
T.
Case 33.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (LESSP (SUB1 I) P))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL I 0))
(ALL-DISTINCT NIL)),
which again simplifies, using linear arithmetic, to:
T.
Case 32.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (LESSP (SUB1 I) P))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)),
which again simplifies, using linear arithmetic, to:
T.
Case 31.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (LESSP (SUB1 I) P))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
(ALL-DISTINCT (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which again simplifies, using linear arithmetic, to:
T.
Case 30.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (LESSP (SUB1 I) P))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))),
which again simplifies, using linear arithmetic, to:
T.
Case 29.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (LESSP (SUB1 I) P))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(EQUAL I 0))
(ALL-DISTINCT NIL)),
which again simplifies, using linear arithmetic, to:
T.
Case 28.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (LESSP (SUB1 I) P))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)),
which again simplifies, using linear arithmetic, to:
T.
Case 27.(IMPLIES (AND (NOT (LESSP I 1))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1)))
(ALL-DISTINCT (LIST I (INVERSE I P)))),
which again simplifies, using linear arithmetic, to:
T.
Case 26.(IMPLIES (AND (NOT (LESSP I 1))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))),
which again simplifies, opening up the functions LESSP, SUB1, EQUAL, NUMBERP,
and ALL-DISTINCT, to:
T.
Case 25.(IMPLIES (AND (NOT (LESSP I 1))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL I 0))
(ALL-DISTINCT NIL)),
which again simplifies, using linear arithmetic, to:
T.
Case 24.(IMPLIES (AND (NOT (LESSP I 1))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)),
which again simplifies, unfolding the functions NUMBERP, EQUAL, and LESSP,
to:
T.
Case 23.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1)))
(ALL-DISTINCT (LIST I (INVERSE I P)))),
which again simplifies, using linear arithmetic, to:
T.
Case 22.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))),
which again simplifies, using linear arithmetic, to:
T.
Case 21.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL I 0))
(ALL-DISTINCT NIL)),
which again simplifies, obviously, to:
T.
Case 20.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)).
However this again simplifies, using linear arithmetic, to:
T.
Case 19.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
(ALL-DISTINCT (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which again simplifies, using linear arithmetic, to:
T.
Case 18.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))),
which again simplifies, using linear arithmetic, to:
T.
Case 17.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(EQUAL I 0))
(ALL-DISTINCT NIL)),
which again simplifies, using linear arithmetic, to:
T.
Case 16.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)),
which again simplifies, using linear arithmetic, to:
T.
Case 15.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1)))
(ALL-DISTINCT (LIST I (INVERSE I P)))),
which again simplifies, using linear arithmetic, to:
T.
Case 14.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))),
which again simplifies, using linear arithmetic, applying the lemma
INVERSE-1, and unfolding LESSP, EQUAL, INVERSE-LIST, MEMBER, SUB1, NUMBERP,
and ALL-DISTINCT, to:
T.
Case 13.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL I 0))
(ALL-DISTINCT NIL)),
which again simplifies, using linear arithmetic, to:
T.
Case 12.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)),
which again simplifies, unfolding NUMBERP, EQUAL, and LESSP, to:
T.
Case 11.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
(ALL-DISTINCT (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which again simplifies, using linear arithmetic, applying
NO-OTHER-INVOLUTIONS, CDR-CONS, and CAR-CONS, and opening up the definitions
of SUB1, NUMBERP, EQUAL, LESSP, PRIME, MEMBER, and ALL-DISTINCT, to:
T.
Case 10.(IMPLIES (AND (NOT (LESSP I 1))
(NOT (MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))).
However this again simplifies, using linear arithmetic, rewriting with
INVERSE-1, and unfolding the functions LESSP, SUB1, EQUAL, INVERSE-LIST, and
MEMBER, to:
T.
Case 9. (IMPLIES (AND (NOT (LESSP I 1))
(NOT (MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(EQUAL I 0))
(ALL-DISTINCT NIL)).
But this again simplifies, using linear arithmetic, to:
T.
Case 8. (IMPLIES (AND (NOT (LESSP I 1))
(NOT (MEMBER (INVERSE I P)
(INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)),
which again simplifies, expanding NUMBERP, EQUAL, and LESSP, to:
T.
Case 7. (IMPLIES (AND (NOT (LESSP I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1)))
(ALL-DISTINCT (LIST I (INVERSE I P)))),
which again simplifies, using linear arithmetic, to:
T.
Case 6. (IMPLIES (AND (NOT (LESSP I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))),
which again simplifies, unfolding LESSP, EQUAL, INVERSE-LIST, and MEMBER, to:
T.
Case 5. (IMPLIES (AND (NOT (LESSP I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(EQUAL I 0))
(ALL-DISTINCT NIL)),
which again simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND (NOT (LESSP I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(EQUAL (SUB1 I) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)),
which again simplifies, unfolding the definitions of NUMBERP, EQUAL, and
LESSP, to:
T.
Case 3. (IMPLIES (AND (NOT (LESSP I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(ALL-DISTINCT '(1))),
which again simplifies, opening up the definitions of LESSP, SUB1, EQUAL,
INVERSE-LIST, and MEMBER, to:
T.
Case 2. (IMPLIES (AND (NOT (LESSP I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(EQUAL I 0))
(ALL-DISTINCT NIL)),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL (INVERSE I P) I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))
(NOT (NUMBERP I)))
(ALL-DISTINCT NIL)),
which again simplifies, opening up the functions NUMBERP, EQUAL, and LESSP,
to:
T.
Q.E.D.
[ 0.0 2.1 0.0 ]
A-D-I-L-LEMMA3
(PROVE-LEMMA ALL-DISTINCT-INVERSE-LIST
(REWRITE)
(IMPLIES (AND (PRIME P) (LESSP I (SUB1 P)))
(ALL-DISTINCT (INVERSE-LIST I P)))
((USE (A-D-I-L-LEMMA3))
(INDUCT (POSITIVES I))
(DISABLE INVERSE)))
WARNING: the newly proposed lemma, ALL-DISTINCT-INVERSE-LIST, could be
applied whenever the previously added lemma A-D-I-L-LEMMA3 could.
This formula simplifies, rewriting with SUB1-NNUMBERP, and expanding the
functions PRIME, AND, INVERSE-LIST, IMPLIES, ZEROP, NOT, LESSP, ALL-DISTINCT,
OR, EQUAL, SUB1, and NUMBERP, to the following seven new goals:
Case 7. (IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(ALL-DISTINCT (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(LESSP I (SUB1 P))
(MEMBER I (INVERSE-LIST (SUB1 I) P)))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))).
However this again simplifies, using linear arithmetic, to:
T.
Case 6. (IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(MEMBER I (INVERSE-LIST (SUB1 I) P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(LESSP I (SUB1 P)))
(ALL-DISTINCT (INVERSE-LIST (SUB1 I) P))),
which again simplifies, using linear arithmetic, to:
T.
Case 5. (IMPLIES (AND (NOT (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(LESSP I (SUB1 P))
(NOT (EQUAL I 1)))
(ALL-DISTINCT (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))),
which again simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND (NOT (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(LESSP I (SUB1 P))
(EQUAL I 1))
(ALL-DISTINCT '(1))),
which again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (NOT (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) (SUB1 P)))
(LESSP I (SUB1 P))
(NOT (EQUAL I 1)))
(NOT (MEMBER I
(INVERSE-LIST (SUB1 I) P)))),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
(EQUAL I 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P)))
(ALL-DISTINCT NIL)),
which again simplifies, opening up the definitions of SUB1, EQUAL,
INVERSE-LIST, and ALL-DISTINCT, to:
T.
Case 1. (IMPLIES (AND (NOT (ALL-DISTINCT (INVERSE-LIST (SUB1 I) P)))
(NOT (NUMBERP I))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP I (SUB1 P)))
(ALL-DISTINCT NIL)),
which again simplifies, rewriting with SUB1-NNUMBERP, and opening up EQUAL,
INVERSE-LIST, and ALL-DISTINCT, to:
T.
Q.E.D.
[ 0.0 0.6 0.0 ]
ALL-DISTINCT-INVERSE-LIST
(PROVE-LEMMA T-I-L-LEMMA1
(REWRITE)
(IMPLIES (EQUAL (REMAINDER (TIMES A B) P) 1)
(EQUAL (REMAINDER (TIMES A (TIMES B C)) P)
(REMAINDER C P)))
((USE (TIMES-MOD-3 (A (TIMES A B))
(B C)
(N P)))
(DISABLE TIMES-MOD-3)))
This formula can be simplified, using the abbreviations IMPLIES and
ASSOCIATIVITY-OF-TIMES, to:
(IMPLIES (AND (EQUAL (REMAINDER (TIMES (REMAINDER (TIMES A B) P) C)
P)
(REMAINDER (TIMES A B C) P))
(EQUAL (REMAINDER (TIMES A B) P) 1))
(EQUAL (REMAINDER (TIMES A B C) P)
(REMAINDER C P))),
which simplifies, rewriting with TIMES-1, TIMES-ZERO2, COMMUTATIVITY-OF-TIMES,
and TIMES-IDENTITY, and unfolding the functions LESSP, EQUAL, and REMAINDER,
to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
T-I-L-LEMMA1
(PROVE-LEMMA T-I-L-LEMMA
(REWRITE)
(IMPLIES (EQUAL (REMAINDER (TIMES I (INVERSE I P)) P)
1)
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P)))
((USE (T-I-L-LEMMA1 (A I)
(B (INVERSE I P))
(C (TIMES-LIST (INVERSE-LIST (SUB1 I) P)))))
(DISABLE T-I-L-LEMMA1 INVERSE INVERSE-INVERTS)))
This simplifies, unfolding EQUAL, IMPLIES, and INVERSE-LIST, to the following
four new formulas:
Case 4. (IMPLIES
(AND (EQUAL (REMAINDER (TIMES I
(INVERSE I P)
(TIMES-LIST (INVERSE-LIST (SUB1 I) P)))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))
(EQUAL (REMAINDER (TIMES I (INVERSE I P)) P)
1)
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P))))
(EQUAL (REMAINDER (TIMES-LIST (CONS I
(CONS (INVERSE I P)
(INVERSE-LIST (SUB1 I) P))))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))).
However this again simplifies, rewriting with CDR-CONS and CAR-CONS, and
expanding TIMES-LIST, to:
T.
Case 3. (IMPLIES
(AND (EQUAL (REMAINDER (TIMES I
(INVERSE I P)
(TIMES-LIST (INVERSE-LIST (SUB1 I) P)))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))
(EQUAL (REMAINDER (TIMES I (INVERSE I P)) P)
1)
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL I 1))
(EQUAL (REMAINDER (TIMES-LIST '(1)) P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))).
This again simplifies, rewriting with TIMES-1, COMMUTATIVITY-OF-TIMES, and
REMAINDER-OF-1, and expanding SUB1, EQUAL, INVERSE-LIST, TIMES-LIST, NUMBERP,
INVERSE, TIMES, and REMAINDER, to:
T.
Case 2. (IMPLIES
(AND (EQUAL (REMAINDER (TIMES I
(INVERSE I P)
(TIMES-LIST (INVERSE-LIST (SUB1 I) P)))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))
(EQUAL (REMAINDER (TIMES I (INVERSE I P)) P)
1)
(EQUAL I 0))
(EQUAL (REMAINDER (TIMES-LIST NIL) P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))).
But this again simplifies, appealing to the lemmas TIMES-1,
COMMUTATIVITY-OF-TIMES, TIMES-IDENTITY, and REMAINDER-OF-1, and opening up
the functions SUB1, EQUAL, INVERSE-LIST, TIMES-LIST, LESSP, REMAINDER,
INVERSE, and TIMES, to:
T.
Case 1. (IMPLIES
(AND (EQUAL (REMAINDER (TIMES I
(INVERSE I P)
(TIMES-LIST (INVERSE-LIST (SUB1 I) P)))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))
(EQUAL (REMAINDER (TIMES I (INVERSE I P)) P)
1)
(NOT (NUMBERP I)))
(EQUAL (REMAINDER (TIMES-LIST NIL) P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))),
which again simplifies, rewriting with the lemmas SUB1-NNUMBERP, TIMES-1,
COMMUTATIVITY-OF-TIMES, EQUAL-TIMES-0, REMAINDER-OF-1, and REMAINDER-WRT-1,
and opening up EQUAL, INVERSE-LIST, TIMES-LIST, LESSP, and REMAINDER, to:
T.
Q.E.D.
[ 0.0 0.5 0.0 ]
T-I-L-LEMMA
(PROVE-LEMMA T-I-L-LEMMA3
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER I P) 0)))
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P)))
((USE (INVERSE-INVERTS (J I)))
(DISABLE INVERSE INVERSE-LIST TIMES-LIST REMAINDER PRIME)))
This conjecture simplifies, applying COMMUTATIVITY-OF-TIMES and T-I-L-LEMMA,
and unfolding NOT, AND, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
T-I-L-LEMMA3
(PROVE-LEMMA T-I-L-LEMMA4
(REWRITE)
(IMPLIES (LEQ I 1)
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
1)))
Call the conjecture *1.
We will try to prove it by induction. The recursive terms in the
conjecture suggest two inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (OR (EQUAL I 0) (NOT (NUMBERP I)))
(p I P))
(IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(p I P))
(IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(p (SUB1 I) P))
(p I P))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT can be used to prove that the measure (COUNT I) decreases
according to the well-founded relation LESSP in each induction step of the
scheme. The above induction scheme leads to the following four new goals:
Case 4. (IMPLIES (AND (OR (EQUAL I 0) (NOT (NUMBERP I)))
(NOT (LESSP 1 I)))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
1)).
This simplifies, opening up the definitions of NOT, OR, LESSP, EQUAL,
INVERSE-LIST, and TIMES-LIST, to:
T.
Case 3. (IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(OR (EQUAL 1 0) (NOT (NUMBERP 1)))
(NOT (LESSP 1 I)))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
1)).
This simplifies, expanding NOT, OR, EQUAL, and NUMBERP, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(LESSP 1 (SUB1 I))
(NOT (LESSP 1 I)))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
1)).
This simplifies, using linear arithmetic, to the new formula:
(IMPLIES (AND (LESSP I 1)
(NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(LESSP 1 (SUB1 I))
(NOT (LESSP 1 I)))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
1)),
which again simplifies, opening up SUB1, NUMBERP, EQUAL, LESSP, NOT, and OR,
to:
T.
Case 1. (IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL 1 0) (NOT (NUMBERP 1))))
(EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
1)
(NOT (LESSP 1 I)))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
1)),
which simplifies, applying DIFFERENCE-1, and expanding the functions NOT, OR,
EQUAL, NUMBERP, LESSP, SUB1, INVERSE-LIST, DIFFERENCE, REMAINDER, and
INVERSE, to the following five new formulas:
Case 1.5.
(IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
1)
(EQUAL (SUB1 I) 0)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 2))
(NOT (NUMBERP P)))
(EQUAL (TIMES-LIST (CONS I
(CONS (REMAINDER (EXP I 0) P)
(INVERSE-LIST (SUB1 I) P))))
1)).
But this again simplifies, using linear arithmetic, to:
T.
Case 1.4.
(IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
1)
(EQUAL (SUB1 I) 0)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 2))
(EQUAL P 0))
(EQUAL (TIMES-LIST (CONS I
(CONS (REMAINDER (EXP I 0) P)
(INVERSE-LIST (SUB1 I) P))))
1)),
which again simplifies, using linear arithmetic, to:
T.
Case 1.3.
(IMPLIES
(AND (NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
1)
(EQUAL (SUB1 I) 0)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(NOT (EQUAL P 2))
(NOT (EQUAL P 0))
(NUMBERP P))
(EQUAL (TIMES-LIST (CONS I
(CONS (REMAINDER (EXP I (SUB1 (SUB1 P))) P)
(INVERSE-LIST (SUB1 I) P))))
1)),
which again simplifies, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES
(AND (NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
1)
(EQUAL (SUB1 I) 0)
(NOT (EQUAL I 1))
(NOT (MEMBER I (INVERSE-LIST (SUB1 I) P)))
(EQUAL P 2))
(EQUAL (TIMES-LIST (CONS I
(CONS I (INVERSE-LIST (SUB1 I) P))))
1)),
which again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
1)
(EQUAL (SUB1 I) 0)
(EQUAL I 1))
(EQUAL (TIMES-LIST '(1)) 1)),
which again simplifies, unfolding EQUAL, NUMBERP, INVERSE-LIST, TIMES-LIST,
and SUB1, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
T-I-L-LEMMA4
(PROVE-LEMMA TIMES-INVERSE-LIST
(REWRITE)
(IMPLIES (AND (PRIME P) (LESSP I P))
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
1))
((USE (T-I-L-LEMMA3) (T-I-L-LEMMA4))
(INDUCT (POSITIVES I))
(DISABLE INVERSE INVERSE-LIST TIMES-LIST T-I-L-LEMMA3
T-I-L-LEMMA4)))
This formula simplifies, rewriting with REMAINDER-WRT-12, REMAINDER-OF-1, and
REMAINDER-WRT-1, and unfolding PRIME, NOT, AND, IMPLIES, SUB1, NUMBERP, EQUAL,
LESSP, ZEROP, REMAINDER, and OR, to the following three new formulas:
Case 3. (IMPLIES (AND (EQUAL (REMAINDER I P) 0)
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL (SUB1 I) 0))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P)
1)
(LESSP I P))
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
1)).
But this again simplifies, expanding REMAINDER, to:
T.
Case 2. (IMPLIES (AND (EQUAL (REMAINDER I P) 0)
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL (SUB1 I) 0))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) P))
(LESSP I P))
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
1)),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
(REMAINDER (TIMES-LIST (INVERSE-LIST (SUB1 I) P))
P))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL (SUB1 I) 0))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (LESSP (SUB1 I) P))
(LESSP I P))
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
1)),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 2.5 0.0 ]
TIMES-INVERSE-LIST
(PROVE-LEMMA DELETE-X-LEAVE-A
(REWRITE)
(IMPLIES (AND (MEMBER A S) (NOT (EQUAL A X)))
(MEMBER A (DELETE X S))))
Give the conjecture the name *1.
Let us appeal to the induction principle. The recursive terms in the
conjecture suggest two inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP S) (p A X S))
(IMPLIES (AND (NOT (NLISTP S))
(EQUAL A (CAR S)))
(p A X S))
(IMPLIES (AND (NOT (NLISTP S))
(NOT (EQUAL A (CAR S)))
(p A X (CDR S)))
(p A X S))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to show that the measure (COUNT S) decreases according to
the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme generates the following four new conjectures:
Case 4. (IMPLIES (AND (NLISTP S)
(MEMBER A S)
(NOT (EQUAL A X)))
(MEMBER A (DELETE X S))).
This simplifies, opening up the functions NLISTP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP S))
(EQUAL A (CAR S))
(MEMBER A S)
(NOT (EQUAL A X)))
(MEMBER A (DELETE X S))).
This simplifies, rewriting with CAR-CONS, and opening up the definitions of
NLISTP, MEMBER, and DELETE, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP S))
(NOT (EQUAL A (CAR S)))
(NOT (MEMBER A (CDR S)))
(MEMBER A S)
(NOT (EQUAL A X)))
(MEMBER A (DELETE X S))),
which simplifies, unfolding the functions NLISTP and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP S))
(NOT (EQUAL A (CAR S)))
(MEMBER A (DELETE X (CDR S)))
(MEMBER A S)
(NOT (EQUAL A X)))
(MEMBER A (DELETE X S))),
which simplifies, unfolding the definitions of NLISTP, MEMBER, and DELETE,
to the goal:
(IMPLIES (AND (LISTP S)
(NOT (EQUAL A (CAR S)))
(MEMBER A (DELETE X (CDR S)))
(MEMBER A (CDR S))
(NOT (EQUAL A X))
(NOT (EQUAL X (CAR S))))
(MEMBER A
(CONS (CAR S) (DELETE X (CDR S))))).
But this again simplifies, rewriting with CDR-CONS and CAR-CONS, and opening
up the definition of MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
DELETE-X-LEAVE-A
(PROVE-LEMMA DELETE-MEMBER-LEAVE-SUBSET
(REWRITE)
(IMPLIES (AND (SUBSETP R S) (NOT (MEMBER X R)))
(SUBSETP R (DELETE X S))))
Give the conjecture the name *1.
Let us appeal to the induction principle. The recursive terms in the
conjecture suggest four inductions. They merge into two likely candidate
inductions. However, only one is unflawed. We will induct according to the
following scheme:
(AND (IMPLIES (AND (LISTP R)
(MEMBER (CAR R) S)
(p (CDR R) X S))
(p R X S))
(IMPLIES (AND (LISTP R)
(NOT (MEMBER (CAR R) S)))
(p R X S))
(IMPLIES (NOT (LISTP R)) (p R X S))).
Linear arithmetic and the lemma CDR-LESSP can be used to show that the measure
(COUNT R) decreases according to the well-founded relation LESSP in each
induction step of the scheme. The above induction scheme generates the
following five new conjectures:
Case 5. (IMPLIES (AND (LISTP R)
(MEMBER (CAR R) S)
(NOT (SUBSETP (CDR R) S))
(SUBSETP R S)
(NOT (MEMBER X R)))
(SUBSETP R (DELETE X S))).
This simplifies, opening up the function SUBSETP, to:
T.
Case 4. (IMPLIES (AND (LISTP R)
(MEMBER (CAR R) S)
(MEMBER X (CDR R))
(SUBSETP R S)
(NOT (MEMBER X R)))
(SUBSETP R (DELETE X S))).
This simplifies, unfolding the functions SUBSETP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (LISTP R)
(MEMBER (CAR R) S)
(SUBSETP (CDR R) (DELETE X S))
(SUBSETP R S)
(NOT (MEMBER X R)))
(SUBSETP R (DELETE X S))).
This simplifies, applying DELETE-X-LEAVE-A, and unfolding the functions
SUBSETP and MEMBER, to:
T.
Case 2. (IMPLIES (AND (LISTP R)
(NOT (MEMBER (CAR R) S))
(SUBSETP R S)
(NOT (MEMBER X R)))
(SUBSETP R (DELETE X S))),
which simplifies, unfolding the definition of SUBSETP, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP R))
(SUBSETP R S)
(NOT (MEMBER X R)))
(SUBSETP R (DELETE X S))),
which simplifies, opening up SUBSETP and MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
DELETE-MEMBER-LEAVE-SUBSET
(PROVE-LEMMA ALL-LESSEQP-DELETE
(REWRITE)
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-LESSEQP L N))
(ALL-LESSEQP (DELETE N L) (SUB1 N))))
.
Applying the lemma SUB1-ELIM, replace N by (ADD1 X) to eliminate (SUB1 N). We
rely upon the type restriction lemma noted when SUB1 was introduced to
restrict the new variable. This produces the following three new conjectures:
Case 3. (IMPLIES (AND (EQUAL N 0)
(ALL-DISTINCT L)
(ALL-LESSEQP L N))
(ALL-LESSEQP (DELETE N L) (SUB1 N))).
This simplifies, unfolding the function SUB1, to:
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-LESSEQP L 0))
(ALL-LESSEQP (DELETE 0 L) 0)),
which we would usually push and work on later by induction. But if we must
use induction to prove the input conjecture, we prefer to induct on the
original formulation of the problem. Thus we will disregard all that we
have previously done, give the name *1 to the original input, and work on it.
So now let us consider:
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-LESSEQP L N))
(ALL-LESSEQP (DELETE N L) (SUB1 N))).
We gave this the name *1 above. Perhaps we can prove it by induction. The
recursive terms in the conjecture suggest three inductions. However, they
merge into one likely candidate induction. We will induct according to the
following scheme:
(AND (IMPLIES (NLISTP L) (p N L))
(IMPLIES (AND (NOT (NLISTP L)) (p N (CDR L)))
(p N L))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to establish that the measure (COUNT L) decreases according
to the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme generates four new conjectures:
Case 4. (IMPLIES (AND (NLISTP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L N))
(ALL-LESSEQP (DELETE N L) (SUB1 N))),
which simplifies, rewriting with PIGEON-HOLE-PRINCIPLE-LEMMA-2,
DELETE-NON-MEMBER, and ADD1-SUB1, and expanding the definitions of NLISTP,
ALL-DISTINCT, ALL-LESSEQP, and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-DISTINCT (CDR L)))
(ALL-DISTINCT L)
(ALL-LESSEQP L N))
(ALL-LESSEQP (DELETE N L) (SUB1 N))).
This simplifies, unfolding the functions NLISTP and ALL-DISTINCT, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-LESSEQP (CDR L) N))
(ALL-DISTINCT L)
(ALL-LESSEQP L N))
(ALL-LESSEQP (DELETE N L) (SUB1 N))).
This simplifies, unfolding NLISTP, ALL-DISTINCT, and ALL-LESSEQP, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L))
(ALL-LESSEQP (DELETE N (CDR L))
(SUB1 N))
(ALL-DISTINCT L)
(ALL-LESSEQP L N))
(ALL-LESSEQP (DELETE N L) (SUB1 N))).
This simplifies, opening up the definitions of NLISTP, ALL-DISTINCT,
ALL-LESSEQP, and DELETE, to the following two new conjectures:
Case 1.2.
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE N (CDR L))
(SUB1 N))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (LESSP N (CAR L)))
(ALL-LESSEQP (CDR L) N)
(NOT (EQUAL N (CAR L))))
(ALL-LESSEQP (CONS (CAR L) (DELETE N (CDR L)))
(SUB1 N))).
However this again simplifies, rewriting with the lemmas CDR-CONS and
CAR-CONS, and expanding the function ALL-LESSEQP, to:
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE N (CDR L))
(SUB1 N))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (LESSP N (CAR L)))
(ALL-LESSEQP (CDR L) N)
(NOT (EQUAL N (CAR L))))
(NOT (LESSP (SUB1 N) (CAR L)))).
But this again simplifies, using linear arithmetic, to three new
conjectures:
Case 1.2.3.
(IMPLIES (AND (NOT (NUMBERP (CAR L)))
(LISTP L)
(ALL-LESSEQP (DELETE N (CDR L))
(SUB1 N))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (LESSP N (CAR L)))
(ALL-LESSEQP (CDR L) N)
(NOT (EQUAL N (CAR L))))
(NOT (LESSP (SUB1 N) (CAR L)))),
which again simplifies, opening up the function LESSP, to:
T.
Case 1.2.2.
(IMPLIES (AND (NOT (NUMBERP N))
(LISTP L)
(ALL-LESSEQP (DELETE N (CDR L))
(SUB1 N))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (LESSP N (CAR L)))
(ALL-LESSEQP (CDR L) N)
(NOT (EQUAL N (CAR L))))
(NOT (LESSP (SUB1 N) (CAR L)))),
which again simplifies, applying SUB1-NNUMBERP, and opening up LESSP, to:
T.
Case 1.2.1.
(IMPLIES (AND (NUMBERP N)
(NUMBERP (CAR L))
(LISTP L)
(ALL-LESSEQP (DELETE (CAR L) (CDR L))
(SUB1 (CAR L)))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (LESSP (CAR L) (CAR L)))
(ALL-LESSEQP (CDR L) (CAR L))
(NOT (EQUAL (CAR L) (CAR L))))
(NOT (LESSP (SUB1 (CAR L)) (CAR L)))).
This again simplifies, clearly, to:
T.
Case 1.1.
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE N (CDR L))
(SUB1 N))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (LESSP N (CAR L)))
(ALL-LESSEQP (CDR L) N)
(EQUAL N (CAR L)))
(ALL-LESSEQP (CDR L) (SUB1 N))).
However this again simplifies, applying DELETE-NON-MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
ALL-LESSEQP-DELETE
(PROVE-LEMMA POSITIVES-BOUNDED
(REWRITE)
(IMPLIES (LESSP N M)
(NOT (MEMBER M (POSITIVES N)))))
This formula can be simplified, using the abbreviations MEMBER-POSITIVES, NOT,
and IMPLIES, to:
(IMPLIES (AND (LESSP N M)
(NOT (EQUAL M 0))
(NUMBERP M))
(NOT (LESSP M (ADD1 N)))),
which simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
POSITIVES-BOUNDED
(PROVE-LEMMA SUBSETP-POSITIVES-DELETE
(REWRITE)
(IMPLIES (SUBSETP (POSITIVES N) L)
(SUBSETP (POSITIVES (SUB1 N))
(DELETE N L))))
This simplifies, appealing to the lemmas DELETE-MEMBER-LEAVE-SUBSET and
SUB1-NNUMBERP, and opening up the definitions of POSITIVES, SUB1, MEMBER, and
LISTP, to:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(SUBSETP (CONS N (POSITIVES (SUB1 N)))
L))
(SUBSETP (POSITIVES (SUB1 N))
(DELETE N L))).
This again simplifies, using linear arithmetic, appealing to the lemmas
CDR-CONS, CAR-CONS, POSITIVES-BOUNDED, and DELETE-MEMBER-LEAVE-SUBSET, and
unfolding SUBSETP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
SUBSETP-POSITIVES-DELETE
(PROVE-LEMMA NONZEROP-LESSEQP-ZERO
(REWRITE)
(IMPLIES (AND (ZEROP N)
(ALL-LESSEQP L N)
(ALL-NON-ZEROP L))
(NOT (LISTP L))))
WARNING: Note that NONZEROP-LESSEQP-ZERO contains the free variable N which
will be chosen by instantiating the hypothesis (ZEROP N).
This formula simplifies, expanding ZEROP, to two new conjectures:
Case 2. (IMPLIES (AND (EQUAL N 0)
(ALL-LESSEQP L 0)
(ALL-NON-ZEROP L))
(NOT (LISTP L))),
which again simplifies, clearly, to:
(IMPLIES (AND (ALL-LESSEQP L 0)
(ALL-NON-ZEROP L))
(NOT (LISTP L))),
which we will name *1.
Case 1. (IMPLIES (AND (NOT (NUMBERP N))
(ALL-LESSEQP L N)
(ALL-NON-ZEROP L))
(NOT (LISTP L))),
which we would usually push and work on later by induction. But if we must
use induction to prove the input conjecture, we prefer to induct on the
original formulation of the problem. Thus we will disregard all that we
have previously done, give the name *1 to the original input, and work on it.
So now let us consider:
(IMPLIES (AND (ZEROP N)
(ALL-LESSEQP L N)
(ALL-NON-ZEROP L))
(NOT (LISTP L))).
We gave this the name *1 above. Perhaps we can prove it by induction. There
are two plausible inductions. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP L) (p L N))
(IMPLIES (AND (NOT (NLISTP L)) (p (CDR L) N))
(p L N))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP establish that the measure (COUNT L) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme generates the following four new formulas:
Case 4. (IMPLIES (AND (NLISTP L)
(ZEROP N)
(ALL-LESSEQP L N)
(ALL-NON-ZEROP L))
(NOT (LISTP L))).
This simplifies, opening up NLISTP, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-LESSEQP (CDR L) N))
(ZEROP N)
(ALL-LESSEQP L N)
(ALL-NON-ZEROP L))
(NOT (LISTP L))).
This simplifies, opening up the functions NLISTP, ZEROP, ALL-NON-ZEROP,
ALL-LESSEQP, and LESSP, to:
(IMPLIES (AND (NOT (ALL-LESSEQP (CDR L) N))
(EQUAL N 0)
(ALL-LESSEQP L 0)
(NOT (EQUAL (CAR L) 0))
(NUMBERP (CAR L))
(ALL-NON-ZEROP (CDR L)))
(NOT (LISTP L))),
which again simplifies, unfolding the functions LESSP, EQUAL, and
ALL-LESSEQP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-NON-ZEROP (CDR L)))
(ZEROP N)
(ALL-LESSEQP L N)
(ALL-NON-ZEROP L))
(NOT (LISTP L))),
which simplifies, unfolding the functions NLISTP, ZEROP, ALL-NON-ZEROP,
ALL-LESSEQP, LESSP, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L))
(NOT (LISTP (CDR L)))
(ZEROP N)
(ALL-LESSEQP L N)
(ALL-NON-ZEROP L))
(NOT (LISTP L))),
which simplifies, expanding NLISTP, ZEROP, ALL-NON-ZEROP, ALL-LESSEQP, LESSP,
and EQUAL, to:
(IMPLIES (AND (NOT (LISTP (CDR L)))
(EQUAL N 0)
(ALL-LESSEQP L 0)
(NOT (EQUAL (CAR L) 0))
(NUMBERP (CAR L))
(ALL-NON-ZEROP (CDR L)))
(NOT (LISTP L))).
This again simplifies, expanding LESSP, EQUAL, and ALL-LESSEQP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
NONZEROP-LESSEQP-ZERO
(DEFN PIGEONHOLE2-INDUCTION
(L N)
(IF (ZEROP N)
T
(PIGEONHOLE2-INDUCTION (DELETE N L)
(SUB1 N))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
inform us that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call. Hence, PIGEONHOLE2-INDUCTION is
accepted under the definitional principle. From the definition we can
conclude that (TRUEP (PIGEONHOLE2-INDUCTION L N)) is a theorem.
[ 0.0 0.0 0.0 ]
PIGEONHOLE2-INDUCTION
(PROVE-LEMMA PIGEONHOLE2
(REWRITE)
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N)
(SUBSETP (POSITIVES N) L))
(PERM (POSITIVES N) L))
((INDUCT (PIGEONHOLE2-INDUCTION L N))))
This conjecture can be simplified, using the abbreviations ZEROP, IMPLIES, NOT,
OR, and AND, to two new goals:
Case 2. (IMPLIES (AND (ZEROP N)
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N)
(SUBSETP (POSITIVES N) L))
(PERM (POSITIVES N) L)),
which simplifies, expanding ZEROP, POSITIVES, LISTP, SUBSETP, and PERM, to
two new goals:
Case 2.2.
(IMPLIES (AND (EQUAL N 0)
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L 0))
(NOT (LISTP L))),
which again simplifies, obviously, to:
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L 0))
(NOT (LISTP L))),
which we will name *1.
Case 2.1.
(IMPLIES (AND (NOT (NUMBERP N))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N))
(NOT (LISTP L))).
Call the above conjecture *2.
Case 1. (IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(IMPLIES (AND (ALL-DISTINCT (DELETE N L))
(ALL-NON-ZEROP (DELETE N L))
(ALL-LESSEQP (DELETE N L) (SUB1 N))
(SUBSETP (POSITIVES (SUB1 N))
(DELETE N L)))
(PERM (POSITIVES (SUB1 N))
(DELETE N L)))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N)
(SUBSETP (POSITIVES N) L))
(PERM (POSITIVES N) L)).
This simplifies, applying the lemmas ALL-DISTINCT-DELETE,
ALL-NON-ZEROP-DELETE, ALL-LESSEQP-DELETE, SUBSETP-POSITIVES-DELETE, CDR-CONS,
and CAR-CONS, and opening up AND, IMPLIES, POSITIVES, SUBSETP, and PERM, to:
T.
So let us turn our attention to:
(IMPLIES (AND (NOT (NUMBERP N))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N))
(NOT (LISTP L))),
which we named *2 above. We will appeal to induction. The recursive terms in
the conjecture suggest three inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP L) (p L N))
(IMPLIES (AND (NOT (NLISTP L)) (p (CDR L) N))
(p L N))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT L) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme produces the following five new formulas:
Case 5. (IMPLIES (AND (NLISTP L)
(NOT (NUMBERP N))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N))
(NOT (LISTP L))).
This simplifies, expanding NLISTP, to:
T.
Case 4. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-DISTINCT (CDR L)))
(NOT (NUMBERP N))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N))
(NOT (LISTP L))).
This simplifies, opening up the functions NLISTP and ALL-DISTINCT, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-NON-ZEROP (CDR L)))
(NOT (NUMBERP N))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N))
(NOT (LISTP L))).
This simplifies, expanding the functions NLISTP, ALL-DISTINCT, and
ALL-NON-ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-LESSEQP (CDR L) N))
(NOT (NUMBERP N))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N))
(NOT (LISTP L))).
This simplifies, opening up the functions NLISTP, ALL-DISTINCT,
ALL-NON-ZEROP, ALL-LESSEQP, and LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L))
(NOT (LISTP (CDR L)))
(NOT (NUMBERP N))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L N))
(NOT (LISTP L))).
This simplifies, opening up the definitions of NLISTP, ALL-DISTINCT, MEMBER,
ALL-NON-ZEROP, ALL-LESSEQP, and LESSP, to:
T.
That finishes the proof of *2.
So we now return to:
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L 0))
(NOT (LISTP L))),
named *1 above. We will appeal to induction. The recursive terms in the
conjecture suggest three inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP L) (p L))
(IMPLIES (AND (NOT (NLISTP L)) (p (CDR L)))
(p L))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to show that the measure (COUNT L) decreases according to
the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme leads to five new formulas:
Case 5. (IMPLIES (AND (NLISTP L)
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L 0))
(NOT (LISTP L))),
which simplifies, opening up the definition of NLISTP, to:
T.
Case 4. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-DISTINCT (CDR L)))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L 0))
(NOT (LISTP L))),
which simplifies, opening up the definitions of NLISTP and ALL-DISTINCT, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-NON-ZEROP (CDR L)))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L 0))
(NOT (LISTP L))),
which simplifies, unfolding the functions NLISTP, ALL-DISTINCT, and
ALL-NON-ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-LESSEQP (CDR L) 0))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L 0))
(NOT (LISTP L))),
which simplifies, opening up the functions NLISTP, ALL-DISTINCT,
ALL-NON-ZEROP, ALL-LESSEQP, EQUAL, and LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L))
(NOT (LISTP (CDR L)))
(ALL-DISTINCT L)
(ALL-NON-ZEROP L)
(ALL-LESSEQP L 0))
(NOT (LISTP L))),
which simplifies, opening up the definitions of NLISTP, ALL-DISTINCT, MEMBER,
ALL-NON-ZEROP, ALL-LESSEQP, EQUAL, and LESSP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
PIGEONHOLE2
(PROVE-LEMMA PERM-POSITIVES-INVERSE-LIST
(REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL I (DIFFERENCE P 2)))
(PERM (POSITIVES I)
(INVERSE-LIST I P))))
This conjecture can be simplified, using the abbreviations PRIME, AND, and
IMPLIES, to the goal:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL I (DIFFERENCE P 2)))
(PERM (POSITIVES I)
(INVERSE-LIST I P))).
This simplifies, using linear arithmetic, rewriting with DIFFERENCE-1,
SUBSETP-POSITIVES, BOUNDED-INVERSE-LIST, ALL-NON-ZEROP-INVERSE-LIST,
ALL-DISTINCT-INVERSE-LIST, and PIGEONHOLE2, and unfolding SUB1, NUMBERP, EQUAL,
DIFFERENCE, and PRIME, to the goal:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL (SUB1 P) 0))
(PERM (POSITIVES (DIFFERENCE P 2))
(INVERSE-LIST (DIFFERENCE P 2) P))).
This again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PERM-POSITIVES-INVERSE-LIST
(PROVE-LEMMA INVERSE-LIST-FACT
(REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL I (DIFFERENCE P 2)))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
(FACT I)))
((USE (TIMES-LIST-EQUAL-FACT (N I)
(L (INVERSE-LIST I P))))
(DISABLE INVERSE-LIST)))
This formula can be simplified, using the abbreviations PRIME, AND, and
IMPLIES, to:
(IMPLIES (AND (IMPLIES (PERM (POSITIVES I)
(INVERSE-LIST I P))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
(FACT I)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL I (DIFFERENCE P 2)))
(EQUAL (TIMES-LIST (INVERSE-LIST I P))
(FACT I))),
which simplifies, applying the lemmas DIFFERENCE-1 and
PERM-POSITIVES-INVERSE-LIST, and opening up the definitions of SUB1, NUMBERP,
EQUAL, DIFFERENCE, PRIME, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INVERSE-LIST-FACT
(PROVE-LEMMA W-T-LEMMA
(REWRITE)
(IMPLIES (AND (PRIME P)
(EQUAL I (DIFFERENCE P 2)))
(EQUAL (REMAINDER (FACT I) P) 1))
((USE (TIMES-INVERSE-LIST))))
This conjecture can be simplified, using the abbreviations PRIME, AND, and
IMPLIES, to the formula:
(IMPLIES (AND (IMPLIES (AND (PRIME P) (LESSP I P))
(EQUAL (REMAINDER (TIMES-LIST (INVERSE-LIST I P))
P)
1))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(EQUAL I (DIFFERENCE P 2)))
(EQUAL (REMAINDER (FACT I) P) 1)).
This simplifies, rewriting with the lemmas DIFFERENCE-1 and INVERSE-LIST-FACT,
and unfolding the definitions of PRIME, SUB1, NUMBERP, EQUAL, DIFFERENCE, AND,
and IMPLIES, to the new goal:
(IMPLIES (AND (NOT (LESSP (SUB1 (SUB1 P)) P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL (REMAINDER (FACT (SUB1 (SUB1 P))) P)
1)),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (SUB1 P) 0)
(NOT (LESSP (SUB1 (SUB1 P)) P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL (REMAINDER (FACT (SUB1 (SUB1 P))) P)
1)).
But this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.5 0.0 ]
W-T-LEMMA
(PROVE-LEMMA WILSON-THM NIL
(IMPLIES (PRIME P)
(EQUAL (REMAINDER (FACT (SUB1 P)) P)
(SUB1 P)))
((USE (W-T-LEMMA (I (SUB1 (SUB1 P))))
(THM-55-SPECIALIZED-TO-PRIMES (M (SUB1 P))
(X (FACT (SUB1 (SUB1 P))))
(Y 1)))
(DISABLE W-T-LEMMA THM-55-SPECIALIZED-TO-PRIMES)))
This formula can be simplified, using the abbreviations PRIME, IMPLIES, and
AND, to the new goal:
(IMPLIES
(AND (IMPLIES (AND (PRIME P)
(EQUAL (SUB1 (SUB1 P))
(DIFFERENCE P 2)))
(EQUAL (REMAINDER (FACT (SUB1 (SUB1 P))) P)
1))
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER (SUB1 P) P) 0)))
(EQUAL (EQUAL (REMAINDER (TIMES (SUB1 P)
(FACT (SUB1 (SUB1 P))))
P)
(REMAINDER (TIMES (SUB1 P) 1) P))
(EQUAL (REMAINDER (FACT (SUB1 (SUB1 P))) P)
(REMAINDER 1 P))))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL (REMAINDER (FACT (SUB1 P)) P)
(SUB1 P))),
which simplifies, using linear arithmetic, applying DIFFERENCE-1,
REMAINDER-0-CROCK, REMAINDER-OF-1, DIFFERENCE-0, TIMES-1,
COMMUTATIVITY-OF-TIMES, INVERSE-1, and B-I-LEMMA2, and expanding the functions
PRIME1, DIVIDES, PRIME, SUB1, NUMBERP, EQUAL, DIFFERENCE, AND, IMPLIES, NOT,
FACT, TIMES, LESSP, and REMAINDER, to:
(IMPLIES (AND (EQUAL (REMAINDER (FACT (SUB1 (SUB1 P))) P)
1)
(NOT (LESSP (SUB1 (SUB1 P)) (SUB1 P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(NOT (EQUAL (SUB1 P) 0))
(LESSP (SUB1 P) (SUB1 (SUB1 P)))
(PRIME1 P (SUB1 (SUB1 P))))
(EQUAL (REMAINDER (TIMES (SUB1 P)
(FACT (SUB1 (SUB1 P))))
P)
(SUB1 P))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 1.0 0.0 ]
WILSON-THM
(MAKE-LIB "wilson" T)
Making the lib for "wilson".
Compiling the lib for "wilson".
Loading ./basic/wilson.o
Finished loading ./basic/wilson.o
Finished compiling the lib for "wilson".
Finished making the lib for "wilson".
(/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/wilson.lib
/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/wilson.lisp)