(NOTE-LIB "proveall" T)
Loading ./basic/proveall.lib
Finished loading ./basic/proveall.lib
Loading ./basic/proveall.o
Finished loading ./basic/proveall.o
(#./basic/proveall.lib #./basic/proveall)
(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
(DISABLE EUCLID)
[ 0.0 0.0 0.0 ]
EUCLID-OFF
(DISABLE QUOTIENT-DIVIDES)
[ 0.0 0.0 0.0 ]
QUOTIENT-DIVIDES-OFF
(DISABLE IF-TIMES-THEN-DIVIDES)
[ 0.0 0.0 0.0 ]
IF-TIMES-THEN-DIVIDES-OFF
(DISABLE TIMES)
[ 0.0 0.0 0.0 ]
TIMES-OFF
(DEFN CRYPT
(M E N)
(IF (ZEROP E)
1
(IF (EVEN E)
(REMAINDER (SQUARE (CRYPT M (QUOTIENT E 2) N))
N)
(REMAINDER (TIMES M
(REMAINDER (SQUARE (CRYPT M (QUOTIENT E 2) N))
N))
N))))
The lemmas LESSP-QUOTIENT1 and COUNT-NUMBERP and the definitions of
NUMBERP, EQUAL, EVEN, and ZEROP inform us that the measure (COUNT E) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
CRYPT is accepted under the principle of definition. From the definition we
can conclude that (NUMBERP (CRYPT M E N)) is a theorem.
[ 0.0 0.0 0.0 ]
CRYPT
(PROVE-LEMMA TIMES-MOD-1
(REWRITE)
(EQUAL (REMAINDER (TIMES X (REMAINDER Y N))
N)
(REMAINDER (TIMES X Y) N)))
.
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace Y by
(PLUS Z (TIMES N V)) to eliminate (REMAINDER Y N) and (QUOTIENT Y N). We use
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. The result is four new goals:
Case 4. (IMPLIES (NOT (NUMBERP Y))
(EQUAL (REMAINDER (TIMES X (REMAINDER Y N))
N)
(REMAINDER (TIMES X Y) N))),
which simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES,
TIMES-IDENTITY, TIMES-ZERO2, and REMAINDER-0-CROCK, and unfolding LESSP,
REMAINDER, and EQUAL, to:
T.
Case 3. (IMPLIES (EQUAL N 0)
(EQUAL (REMAINDER (TIMES X (REMAINDER Y N))
N)
(REMAINDER (TIMES X Y) N))),
which simplifies, opening up EQUAL and REMAINDER, to:
(IMPLIES (NOT (NUMBERP Y))
(EQUAL (TIMES X 0) (TIMES X Y))).
But this again simplifies, applying the lemmas COMMUTATIVITY-OF-TIMES,
TIMES-ZERO2, and TIMES-IDENTITY, and opening up the definition of EQUAL, to:
T.
Case 2. (IMPLIES (NOT (NUMBERP N))
(EQUAL (REMAINDER (TIMES X (REMAINDER Y N))
N)
(REMAINDER (TIMES X Y) N))),
which simplifies, rewriting with REMAINDER-WRT-12, to the new conjecture:
(IMPLIES (AND (NOT (NUMBERP N))
(NOT (NUMBERP Y)))
(EQUAL (TIMES X 0) (TIMES X Y))),
which again simplifies, rewriting with COMMUTATIVITY-OF-TIMES, TIMES-ZERO2,
and TIMES-IDENTITY, and opening up the function EQUAL, to:
T.
Case 1. (IMPLIES (AND (NUMBERP Z)
(EQUAL (LESSP Z N) (NOT (ZEROP N)))
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0)))
(EQUAL (REMAINDER (TIMES X Z) N)
(REMAINDER (TIMES X (PLUS Z (TIMES N V)))
N))).
But this simplifies, applying COMMUTATIVITY-OF-TIMES,
COMMUTATIVITY2-OF-TIMES, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and
REMAINDER-PLUS-TIMES-2, and opening up the functions ZEROP and NOT, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
TIMES-MOD-1
(PROVE-LEMMA TIMES-MOD-2
(REWRITE)
(EQUAL (REMAINDER (TIMES A (TIMES B (REMAINDER Y N)))
N)
(REMAINDER (TIMES A B Y) N))
((USE (TIMES-MOD-1 (X (TIMES A B))))
(DISABLE TIMES-MOD-1)))
This conjecture can be simplified, using the abbreviation
ASSOCIATIVITY-OF-TIMES, to:
T.
This simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
TIMES-MOD-2
(PROVE-LEMMA CRYPT-CORRECT
(REWRITE)
(IMPLIES (NOT (EQUAL N 1))
(EQUAL (CRYPT M E N)
(REMAINDER (EXP M E) N))))
Give the conjecture the name *1.
Perhaps we can prove it by induction. The recursive terms in the
conjecture suggest two 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 E) (p M E N))
(IMPLIES (AND (NOT (ZEROP E))
(EVEN E)
(p M (QUOTIENT E 2) N))
(p M E N))
(IMPLIES (AND (NOT (ZEROP E))
(NOT (EVEN E))
(p M (QUOTIENT E 2) N))
(p M E N))).
The lemmas LESSP-QUOTIENT1 and COUNT-NUMBERP and the definitions of NUMBERP,
EQUAL, EVEN, and ZEROP establish that the measure (COUNT E) decreases
according to the well-founded relation LESSP in each induction step of the
scheme. The above induction scheme leads to the following three new
conjectures:
Case 3. (IMPLIES (AND (ZEROP E) (NOT (EQUAL N 1)))
(EQUAL (CRYPT M E N)
(REMAINDER (EXP M E) N))).
This simplifies, appealing to the lemmas EXP-BY-0 and REMAINDER-OF-1, and
unfolding ZEROP, EQUAL, CRYPT, and EXP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP E))
(EVEN E)
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (CRYPT M E N)
(REMAINDER (EXP M E) N))).
This simplifies, expanding the definitions of ZEROP, EVEN, CRYPT, EQUAL, and
SQUARE, to:
(IMPLIES (AND (NOT (EQUAL E 0))
(NUMBERP E)
(EQUAL 0 (REMAINDER E 2))
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES (CRYPT M (QUOTIENT E 2) N)
(CRYPT M (QUOTIENT E 2) N))
N)
(REMAINDER (EXP M E) N))).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace E by
(PLUS X (TIMES 2 Z)) to eliminate (REMAINDER E 2) and (QUOTIENT E 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 restrict the new variables. This produces the following three
new formulas:
Case 2.3.
(IMPLIES (AND (EQUAL 2 0)
(NOT (EQUAL E 0))
(NUMBERP E)
(EQUAL 0 (REMAINDER E 2))
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES (CRYPT M (QUOTIENT E 2) N)
(CRYPT M (QUOTIENT E 2) N))
N)
(REMAINDER (EXP M E) N))).
This further simplifies, using linear arithmetic, to:
T.
Case 2.2.
(IMPLIES (AND (NOT (NUMBERP 2))
(NOT (EQUAL E 0))
(NUMBERP E)
(EQUAL 0 (REMAINDER E 2))
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES (CRYPT M (QUOTIENT E 2) N)
(CRYPT M (QUOTIENT E 2) N))
N)
(REMAINDER (EXP M E) N))),
which further simplifies, trivially, to:
T.
Case 2.1.
(IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X 2) (NOT (ZEROP 2)))
(NUMBERP Z)
(NOT (EQUAL 2 0))
(NOT (EQUAL (PLUS X (TIMES 2 Z)) 0))
(EQUAL 0 X)
(EQUAL (CRYPT M Z N)
(REMAINDER (EXP M Z) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES (CRYPT M Z N) (CRYPT M Z N))
N)
(REMAINDER (EXP M (PLUS X (TIMES 2 Z)))
N))).
This further simplifies, rewriting with TIMES-2, CORRECTNESS-OF-CANCEL,
PLUS-EQUAL-0, EXP-BY-0, EXP-PLUS, and TIMES-1, and expanding the functions
NUMBERP, LESSP, ZEROP, NOT, and EQUAL, to the new conjecture:
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL Z 0))
(EQUAL (CRYPT M Z N)
(REMAINDER (EXP M Z) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES (CRYPT M Z N) (CRYPT M Z N))
N)
(REMAINDER (TIMES (EXP M Z) (EXP M Z))
N))).
We use the above equality hypothesis by substituting
(REMAINDER (EXP M Z) N) for (CRYPT M Z N) and throwing away the equality.
We must thus prove:
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL Z 0))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES (REMAINDER (EXP M Z) N)
(REMAINDER (EXP M Z) N))
N)
(REMAINDER (TIMES (EXP M Z) (EXP M Z))
N))).
This further simplifies, rewriting with COMMUTATIVITY-OF-TIMES and
TIMES-MOD-1, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP E))
(NOT (EVEN E))
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (CRYPT M E N)
(REMAINDER (EXP M E) N))).
This simplifies, applying TIMES-MOD-1, and unfolding ZEROP, EVEN, CRYPT, and
SQUARE, to:
(IMPLIES (AND (NOT (EQUAL E 0))
(NUMBERP E)
(NOT (EQUAL 0 (REMAINDER E 2)))
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES M
(CRYPT M (QUOTIENT E 2) N)
(CRYPT M (QUOTIENT E 2) N))
N)
(REMAINDER (EXP M E) N))).
This again simplifies, using linear arithmetic, rewriting with
LESSP-REMAINDER-DIVISOR, and expanding the definition of EQUAL, to the new
goal:
(IMPLIES (AND (EQUAL (REMAINDER E 2) 1)
(NOT (EQUAL E 0))
(NUMBERP E)
(NOT (EQUAL 0 1))
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES M
(CRYPT M (QUOTIENT E 2) N)
(CRYPT M (QUOTIENT E 2) N))
N)
(REMAINDER (EXP M E) N))),
which again simplifies, unfolding EQUAL, to the formula:
(IMPLIES (AND (EQUAL (REMAINDER E 2) 1)
(NOT (EQUAL E 0))
(NUMBERP E)
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES M
(CRYPT M (QUOTIENT E 2) N)
(CRYPT M (QUOTIENT E 2) N))
N)
(REMAINDER (EXP M E) N))).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace E by
(PLUS X (TIMES 2 Z)) to eliminate (REMAINDER E 2) and (QUOTIENT E 2). We
use 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. The result is three new
conjectures:
Case 1.3.
(IMPLIES (AND (EQUAL 2 0)
(EQUAL (REMAINDER E 2) 1)
(NOT (EQUAL E 0))
(NUMBERP E)
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES M
(CRYPT M (QUOTIENT E 2) N)
(CRYPT M (QUOTIENT E 2) N))
N)
(REMAINDER (EXP M E) N))),
which further simplifies, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP 2))
(EQUAL (REMAINDER E 2) 1)
(NOT (EQUAL E 0))
(NUMBERP E)
(EQUAL (CRYPT M (QUOTIENT E 2) N)
(REMAINDER (EXP M (QUOTIENT E 2)) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES M
(CRYPT M (QUOTIENT E 2) N)
(CRYPT M (QUOTIENT E 2) N))
N)
(REMAINDER (EXP M E) N))),
which further simplifies, trivially, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X 2) (NOT (ZEROP 2)))
(NUMBERP Z)
(NOT (EQUAL 2 0))
(EQUAL X 1)
(NOT (EQUAL (PLUS X (TIMES 2 Z)) 0))
(EQUAL (CRYPT M Z N)
(REMAINDER (EXP M Z) N))
(NOT (EQUAL N 1)))
(EQUAL (REMAINDER (TIMES M (CRYPT M Z N) (CRYPT M Z N))
N)
(REMAINDER (EXP M (PLUS X (TIMES 2 Z)))
N))).
This further simplifies, applying TIMES-2, PLUS-EQUAL-0,
COMMUTATIVITY-OF-TIMES, TIMES-1, EXP-BY-0, EXP-PLUS, and
COMMUTATIVITY2-OF-TIMES, and unfolding the functions NUMBERP, LESSP, ZEROP,
NOT, EQUAL, SUB1, and EXP, to the following two new formulas:
Case 1.1.2.
(IMPLIES (AND (NUMBERP Z)
(EQUAL (CRYPT M Z N)
(REMAINDER (EXP M Z) N))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (REMAINDER (TIMES M (CRYPT M Z N) (CRYPT M Z N))
N)
(REMAINDER (TIMES (EXP M Z) (EXP M Z) 0)
N))).
This again simplifies, rewriting with the lemmas EQUAL-TIMES-0,
COMMUTATIVITY-OF-TIMES, COMMUTATIVITY2-OF-TIMES, and TIMES-IDENTITY, and
expanding the functions LESSP, REMAINDER, and EQUAL, to the goal:
(IMPLIES (AND (NUMBERP Z)
(EQUAL (CRYPT M Z N)
(REMAINDER (EXP M Z) N))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (CRYPT M Z N) (CRYPT M Z N))
(TIMES 0 (EXP M Z) (EXP M Z)))).
We use the above equality hypothesis by substituting
(REMAINDER (EXP M Z) N) for (CRYPT M Z N) and throwing away the equality.
We thus obtain:
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M
(REMAINDER (EXP M Z) N)
(REMAINDER (EXP M Z) N))
(TIMES 0 (EXP M Z) (EXP M Z)))),
which we generalize by replacing (EXP M Z) by Y. We restrict the new
variable by recalling the type restriction lemma noted when EXP was
introduced. This produces the new conjecture:
(IMPLIES (AND (NUMBERP Y)
(NUMBERP Z)
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M
(REMAINDER Y N)
(REMAINDER Y N))
(TIMES 0 Y Y))).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace Y by
(PLUS X (TIMES N V)) to eliminate (REMAINDER Y N) and (QUOTIENT Y N).
We employ LESSP-REMAINDER2, the type restriction lemma noted when
REMAINDER was introduced, and the type restriction lemma noted when
QUOTIENT was introduced to restrict the new variables. We thus obtain
the following three new goals:
Case 1.1.2.3.
(IMPLIES (AND (EQUAL N 0)
(NUMBERP Y)
(NUMBERP Z)
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M
(REMAINDER Y N)
(REMAINDER Y N))
(TIMES 0 Y Y))).
This further simplifies, opening up the definitions of EQUAL and
REMAINDER, to the conjecture:
(IMPLIES (AND (NUMBERP Y)
(NUMBERP Z)
(NOT (NUMBERP M)))
(EQUAL (TIMES M Y Y) (TIMES 0 Y Y))).
We will try to prove the above formula by generalizing it, replacing
(TIMES Y Y) by A. We restrict the new variable by recalling the type
restriction lemma noted when TIMES was introduced. We would thus like
to prove:
(IMPLIES (AND (NUMBERP A)
(NUMBERP Y)
(NUMBERP Z)
(NOT (NUMBERP M)))
(EQUAL (TIMES M A) (TIMES 0 A))),
which finally simplifies, applying TIMES-ZERO2, COMMUTATIVITY-OF-TIMES,
and TIMES-IDENTITY, and expanding EQUAL, to:
T.
Case 1.1.2.2.
(IMPLIES (AND (NOT (NUMBERP N))
(NUMBERP Y)
(NUMBERP Z)
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M
(REMAINDER Y N)
(REMAINDER Y N))
(TIMES 0 Y Y))).
However this further simplifies, applying REMAINDER-WRT-12, to:
(IMPLIES (AND (NOT (NUMBERP N))
(NUMBERP Y)
(NUMBERP Z)
(NOT (NUMBERP M)))
(EQUAL (TIMES M Y Y) (TIMES 0 Y Y))),
which we generalize by replacing (TIMES Y Y) by A. We restrict the
new variable by recalling the type restriction lemma noted when TIMES
was introduced. This produces:
(IMPLIES (AND (NUMBERP A)
(NOT (NUMBERP N))
(NUMBERP Y)
(NUMBERP Z)
(NOT (NUMBERP M)))
(EQUAL (TIMES M A) (TIMES 0 A))),
which finally simplifies, applying the lemmas TIMES-ZERO2,
COMMUTATIVITY-OF-TIMES, and TIMES-IDENTITY, and unfolding the function
EQUAL, to:
T.
Case 1.1.2.1.
(IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X N) (NOT (ZEROP N)))
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NUMBERP Z)
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M X X)
(TIMES 0
(PLUS X (TIMES N V))
(PLUS X (TIMES N V))))),
which further simplifies, rewriting with COMMUTATIVITY-OF-TIMES,
COMMUTATIVITY2-OF-TIMES, DISTRIBUTIVITY-OF-TIMES-OVER-PLUS,
ASSOCIATIVITY-OF-PLUS, and TIMES-IDENTITY, and expanding the functions
ZEROP, NOT, EQUAL, and PLUS, to the new conjecture:
(IMPLIES (AND (NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NUMBERP Z)
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M X X)
(TIMES 0 N N V V))),
which has an irrelevant term in it. By eliminating the term we get:
(IMPLIES (AND (NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M X X)
(TIMES 0 N N V V))),
which we will finally name *1.1.
Case 1.1.1.
(IMPLIES (AND (NUMBERP Z)
(EQUAL (CRYPT M Z N)
(REMAINDER (EXP M Z) N))
(NOT (EQUAL N 1))
(NUMBERP M))
(EQUAL (REMAINDER (TIMES M (CRYPT M Z N) (CRYPT M Z N))
N)
(REMAINDER (TIMES (EXP M Z) (EXP M Z) M)
N))).
However this again simplifies, applying COMMUTATIVITY-OF-TIMES and
COMMUTATIVITY2-OF-TIMES, to:
(IMPLIES (AND (NUMBERP Z)
(EQUAL (CRYPT M Z N)
(REMAINDER (EXP M Z) N))
(NOT (EQUAL N 1))
(NUMBERP M))
(EQUAL (REMAINDER (TIMES M (CRYPT M Z N) (CRYPT M Z N))
N)
(REMAINDER (TIMES M (EXP M Z) (EXP M Z))
N))).
We use the above equality hypothesis by substituting
(REMAINDER (EXP M Z) N) for (CRYPT M Z N) and throwing away the equality.
The result is the goal:
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL N 1))
(NUMBERP M))
(EQUAL (REMAINDER (TIMES M
(REMAINDER (EXP M Z) N)
(REMAINDER (EXP M Z) N))
N)
(REMAINDER (TIMES M (EXP M Z) (EXP M Z))
N))).
But this finally simplifies, applying COMMUTATIVITY-OF-TIMES and
TIMES-MOD-2, to:
T.
So we now return to:
(IMPLIES (AND (NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M X X)
(TIMES 0 N N V V))),
which is formula *1.1 above. We will appeal to 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 N 0) (NOT (NUMBERP N)))
(p M X N V))
(IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(OR (EQUAL X 0) (NOT (NUMBERP X))))
(p M X N V))
(IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(p M (SUB1 X) (SUB1 N) V))
(p M X N V))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT inform us that the measure (COUNT X) decreases according to the
well-founded relation LESSP in each induction step of the scheme. Note,
however, the inductive instance chosen for N. The above induction scheme
generates the following six new conjectures:
Case 6. (IMPLIES (AND (OR (EQUAL N 0) (NOT (NUMBERP N)))
(NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M X X)
(TIMES 0 N N V V))).
This simplifies, unfolding the functions NOT and OR, to:
T.
Case 5. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(OR (EQUAL X 0) (NOT (NUMBERP X)))
(NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M X X)
(TIMES 0 N N V V))).
This simplifies, rewriting with the lemmas TIMES-ZERO2,
COMMUTATIVITY-OF-TIMES, and TIMES-IDENTITY, and expanding the definitions of
NOT, OR, NUMBERP, EQUAL, LESSP, and TIMES, to:
T.
Case 4. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(NOT (LESSP (SUB1 X) (SUB1 N)))
(NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M X X)
(TIMES 0 N N V V))).
This simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL X 0)
(NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(NOT (LESSP (SUB1 X) (SUB1 N)))
(NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M X X)
(TIMES 0 N N V V))),
which again simplifies, unfolding the definitions of NOT, OR, EQUAL, and
NUMBERP, to:
T.
Case 3. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(EQUAL (SUB1 N) 0)
(NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M X X)
(TIMES 0 N N V V))),
which simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(EQUAL (SUB1 N) 1)
(NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M X X)
(TIMES 0 N N V V))),
which simplifies, expanding the definitions of NOT, OR, and LESSP, to the
conjecture:
(IMPLIES (AND (NOT (EQUAL X 0))
(EQUAL (SUB1 N) 1)
(NUMBERP X)
(LESSP (SUB1 X) (SUB1 N))
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M X X)
(TIMES 0 N N V V))).
However this again simplifies, using linear arithmetic, to the goal:
(IMPLIES (AND (NOT (EQUAL 1 0))
(EQUAL (SUB1 N) 1)
(NUMBERP 1)
(LESSP (SUB1 1) 1)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M 1 1)
(TIMES 0 N N V V))).
This again simplifies, applying the lemmas TIMES-1, COMMUTATIVITY-OF-TIMES,
and TIMES-IDENTITY, and opening up EQUAL, NUMBERP, SUB1, LESSP, and TIMES,
to:
T.
Case 1. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(EQUAL (TIMES M (SUB1 X) (SUB1 X))
(TIMES 0 (SUB1 N) (SUB1 N) V V))
(NUMBERP X)
(LESSP X N)
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M X X)
(TIMES 0 N N V V))),
which simplifies, applying COMMUTATIVITY-OF-TIMES and
COMMUTATIVITY2-OF-TIMES, and unfolding the definitions of NOT, OR, and LESSP,
to the new conjecture:
(IMPLIES (AND (NOT (EQUAL X 0))
(EQUAL (TIMES M (SUB1 X) (SUB1 X))
(TIMES 0 V V (SUB1 N) (SUB1 N)))
(NUMBERP X)
(LESSP (SUB1 X) (SUB1 N))
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M X X)
(TIMES 0 N N V V))).
Applying the lemma SUB1-ELIM, replace X by (ADD1 Z) to eliminate (SUB1 X).
We employ the type restriction lemma noted when SUB1 was introduced to
restrict the new variable. We thus obtain the new formula:
(IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL (ADD1 Z) 0))
(EQUAL (TIMES M Z Z)
(TIMES 0 V V (SUB1 N) (SUB1 N)))
(LESSP Z (SUB1 N))
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M (ADD1 Z) (ADD1 Z))
(TIMES 0 N N V V))),
which further simplifies, rewriting with TIMES-ADD1, COMMUTATIVITY-OF-TIMES,
SUB1-ADD1, PLUS-ADD1, COMMUTATIVITY2-OF-PLUS, EQUAL-TIMES-0, and
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and unfolding the definition of PLUS, to
the new formula:
(IMPLIES (AND (NUMBERP Z)
(EQUAL (TIMES M Z Z)
(TIMES 0 V V (SUB1 N) (SUB1 N)))
(LESSP Z (SUB1 N))
(NUMBERP V)
(NUMBERP N)
(NOT (EQUAL N 0))
(NOT (EQUAL N 1))
(NOT (NUMBERP M)))
(EQUAL (TIMES M Z Z)
(TIMES 0 N N V V))),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1.1, which, in turn, finishes the proof of *1.
Q.E.D.
[ 0.0 1.3 0.1 ]
CRYPT-CORRECT
(PROVE-LEMMA TIMES-MOD-3
(REWRITE)
(EQUAL (REMAINDER (TIMES (REMAINDER A N) B)
N)
(REMAINDER (TIMES A B) N)))
This simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES and
TIMES-MOD-1, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
TIMES-MOD-3
(PROVE-LEMMA REMAINDER-EXP-LEMMA
(REWRITE)
(IMPLIES (EQUAL (REMAINDER Y A)
(REMAINDER Z A))
(EQUAL (EQUAL (REMAINDER (TIMES X Y) A)
(REMAINDER (TIMES X Z) A))
T)))
.
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace Y by
(PLUS V (TIMES A W)) to eliminate (REMAINDER Y A) and (QUOTIENT Y A). 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 goals:
Case 4. (IMPLIES (AND (NOT (NUMBERP Y))
(EQUAL (REMAINDER Y A)
(REMAINDER Z A)))
(EQUAL (REMAINDER (TIMES X Y) A)
(REMAINDER (TIMES X Z) A))),
which further simplifies, rewriting with TIMES-ZERO2 and REMAINDER-0-CROCK,
and opening up the definitions of LESSP and REMAINDER, to the new goal:
(IMPLIES (AND (NOT (NUMBERP Y))
(EQUAL 0 (REMAINDER Z A)))
(EQUAL 0 (REMAINDER (TIMES X Z) A))).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace Z by
(PLUS V (TIMES A W)) to eliminate (REMAINDER Z A) and (QUOTIENT Z A). 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 four new goals:
Case 4.4.
(IMPLIES (AND (NOT (NUMBERP Z))
(NOT (NUMBERP Y))
(EQUAL 0 (REMAINDER Z A)))
(EQUAL 0 (REMAINDER (TIMES X Z) A))).
But this further simplifies, applying TIMES-ZERO2 and REMAINDER-0-CROCK,
and opening up LESSP, REMAINDER, and EQUAL, to:
T.
Case 4.3.
(IMPLIES (AND (EQUAL A 0)
(NOT (NUMBERP Y))
(EQUAL 0 (REMAINDER Z A)))
(EQUAL 0 (REMAINDER (TIMES X Z) A))).
But this further simplifies, rewriting with the lemmas
COMMUTATIVITY-OF-TIMES, REMAINDER-TIMES, and TIMES-ZERO2, and unfolding
the definitions of EQUAL and REMAINDER, to:
T.
Case 4.2.
(IMPLIES (AND (NOT (NUMBERP A))
(NOT (NUMBERP Y))
(EQUAL 0 (REMAINDER Z A)))
(EQUAL 0 (REMAINDER (TIMES X Z) A))),
which further simplifies, rewriting with REMAINDER-WRT-12,
COMMUTATIVITY-OF-TIMES, TIMES-IDENTITY, TIMES-ZERO2, and REMAINDER-0-CROCK,
and unfolding the function EQUAL, to:
T.
Case 4.1.
(IMPLIES (AND (NUMBERP V)
(EQUAL (LESSP V A) (NOT (ZEROP A)))
(NUMBERP W)
(NUMBERP A)
(NOT (EQUAL A 0))
(NOT (NUMBERP Y))
(EQUAL 0 V))
(EQUAL 0
(REMAINDER (TIMES X (PLUS V (TIMES A W)))
A))).
This further simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES,
COMMUTATIVITY2-OF-TIMES, and REMAINDER-TIMES, and opening up the functions
NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to:
T.
Case 3. (IMPLIES (AND (EQUAL A 0)
(EQUAL (REMAINDER Y A)
(REMAINDER Z A)))
(EQUAL (REMAINDER (TIMES X Y) A)
(REMAINDER (TIMES X Z) A))),
which further simplifies, rewriting with TIMES-ZERO2, COMMUTATIVITY-OF-TIMES,
and REMAINDER-TIMES, and expanding the definitions of EQUAL and REMAINDER,
to:
T.
Case 2. (IMPLIES (AND (NOT (NUMBERP A))
(EQUAL (REMAINDER Y A)
(REMAINDER Z A)))
(EQUAL (REMAINDER (TIMES X Y) A)
(REMAINDER (TIMES X Z) A))).
But this further simplifies, appealing to the lemmas REMAINDER-WRT-12,
TIMES-ZERO2, REMAINDER-0-CROCK, COMMUTATIVITY-OF-TIMES, and TIMES-IDENTITY,
and unfolding EQUAL, to:
T.
Case 1. (IMPLIES (AND (NUMBERP V)
(EQUAL (LESSP V A) (NOT (ZEROP A)))
(NUMBERP W)
(NUMBERP A)
(NOT (EQUAL A 0))
(EQUAL V (REMAINDER Z A)))
(EQUAL (REMAINDER (TIMES X (PLUS V (TIMES A W)))
A)
(REMAINDER (TIMES X Z) A))),
which further simplifies, applying LESSP-REMAINDER2, COMMUTATIVITY-OF-TIMES,
COMMUTATIVITY2-OF-TIMES, COMMUTATIVITY-OF-PLUS, and
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and expanding the functions ZEROP, NOT,
and EQUAL, to:
(IMPLIES (AND (NUMBERP W)
(NUMBERP A)
(NOT (EQUAL A 0)))
(EQUAL (REMAINDER (PLUS (TIMES A W X)
(TIMES X (REMAINDER Z A)))
A)
(REMAINDER (TIMES X Z) A))).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace Z by
(PLUS V (TIMES A D)) to eliminate (REMAINDER Z A) and (QUOTIENT Z A). 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 two new conjectures:
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP Z))
(NUMBERP W)
(NUMBERP A)
(NOT (EQUAL A 0)))
(EQUAL (REMAINDER (PLUS (TIMES A W X)
(TIMES X (REMAINDER Z A)))
A)
(REMAINDER (TIMES X Z) A))).
This further simplifies, applying COMMUTATIVITY-OF-TIMES, TIMES-IDENTITY,
COMMUTATIVITY-OF-PLUS, REMAINDER-TIMES, TIMES-ZERO2, and REMAINDER-0-CROCK,
and opening up the functions LESSP, REMAINDER, EQUAL, and PLUS, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP V)
(EQUAL (LESSP V A) (NOT (ZEROP A)))
(NUMBERP D)
(NUMBERP W)
(NUMBERP A)
(NOT (EQUAL A 0)))
(EQUAL (REMAINDER (PLUS (TIMES A W X) (TIMES X V))
A)
(REMAINDER (TIMES X (PLUS V (TIMES A D)))
A))).
However this further simplifies, rewriting with COMMUTATIVITY-OF-TIMES,
COMMUTATIVITY-OF-PLUS, REMAINDER-PLUS-TIMES-2, COMMUTATIVITY2-OF-TIMES,
and DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, and opening up the functions ZEROP
and NOT, to:
T.
Q.E.D.
[ 0.0 0.3 0.0 ]
REMAINDER-EXP-LEMMA
(PROVE-LEMMA REMAINDER-EXP
(REWRITE)
(EQUAL (REMAINDER (EXP (REMAINDER A N) I) N)
(REMAINDER (EXP A I) N)))
.
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace A by
(PLUS X (TIMES N Z)) to eliminate (REMAINDER A N) and (QUOTIENT A N). We use
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. The result is four new goals:
Case 4. (IMPLIES (NOT (NUMBERP A))
(EQUAL (REMAINDER (EXP (REMAINDER A N) I) N)
(REMAINDER (EXP A I) N))),
which simplifies, appealing to the lemma EXP-OF-0, and unfolding LESSP and
REMAINDER, to three new formulas:
Case 4.3.
(IMPLIES (AND (NOT (NUMBERP A))
(NOT (EQUAL I 0))
(NUMBERP I))
(EQUAL (REMAINDER 0 N)
(REMAINDER (EXP A I) N))),
which again simplifies, applying REMAINDER-0-CROCK, to the new conjecture:
(IMPLIES (AND (NOT (NUMBERP A))
(NOT (EQUAL I 0))
(NUMBERP I))
(EQUAL 0 (REMAINDER (EXP A I) N))),
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:
(EQUAL (REMAINDER (EXP (REMAINDER A N) I) N)
(REMAINDER (EXP A I) N)).
We named this *1. We will try to prove it by induction. The recursive terms
in the conjecture suggest three inductions. They merge into two likely
candidate inductions. However, only one is unflawed. We will induct
according to the following scheme:
(AND (IMPLIES (ZEROP I) (p A N I))
(IMPLIES (AND (NOT (ZEROP I)) (p A N (SUB1 I)))
(p A N I))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP 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 produces the following two new goals:
Case 2. (IMPLIES (ZEROP I)
(EQUAL (REMAINDER (EXP (REMAINDER A N) I) N)
(REMAINDER (EXP A I) N))).
This simplifies, appealing to the lemmas EXP-BY-0 and REMAINDER-OF-1, and
expanding the functions ZEROP and EXP, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP I))
(EQUAL (REMAINDER (EXP (REMAINDER A N) (SUB1 I))
N)
(REMAINDER (EXP A (SUB1 I)) N)))
(EQUAL (REMAINDER (EXP (REMAINDER A N) I) N)
(REMAINDER (EXP A I) N))).
This simplifies, appealing to the lemmas TIMES-MOD-3 and REMAINDER-EXP-LEMMA,
and expanding the functions ZEROP and EXP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
REMAINDER-EXP
(PROVE-LEMMA EXP-MOD-IS-1
(REWRITE)
(IMPLIES (EQUAL (REMAINDER (EXP M J) P) 1)
(EQUAL (REMAINDER (EXP M (TIMES I J)) P)
1))
((USE (EXP-EXP (I M) (J J) (K I))
(REMAINDER-EXP (A (EXP M J)) (N P)))
(DISABLE EXP-EXP REMAINDER-EXP)))
This formula simplifies, rewriting with the lemmas COMMUTATIVITY-OF-TIMES,
EXP-OF-1, REMAINDER-OF-1, and REMAINDER-WRT-1, and opening up EQUAL, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
EXP-MOD-IS-1
(DEFN PDIFFERENCE
(A B)
(IF (LESSP A B)
(DIFFERENCE B A)
(DIFFERENCE A B))
NIL)
Note that (NUMBERP (PDIFFERENCE A B)) is a theorem.
[ 0.0 0.0 0.0 ]
PDIFFERENCE
(PROVE-LEMMA TIMES-DISTRIBUTES-OVER-PDIFFERENCE
(REWRITE)
(EQUAL (TIMES M (PDIFFERENCE A B))
(PDIFFERENCE (TIMES M A)
(TIMES M B))))
WARNING: the previously added lemma, COMMUTATIVITY-OF-TIMES, could be applied
whenever the newly proposed TIMES-DISTRIBUTES-OVER-PDIFFERENCE could!
This simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES and
LESSP-TIMES-CANCELLATION, and opening up the definition of PDIFFERENCE, to
four new goals:
Case 4. (IMPLIES (NOT (LESSP A B))
(EQUAL (TIMES M (DIFFERENCE A B))
(DIFFERENCE (TIMES A M)
(TIMES B M)))),
which again simplifies, appealing to the lemma TIMES-DIFFERENCE, to:
T.
Case 3. (IMPLIES (AND (NOT (NUMBERP M)) (LESSP A B))
(EQUAL (TIMES M (DIFFERENCE B A))
(DIFFERENCE (TIMES A M)
(TIMES B M)))),
which again simplifies, applying TIMES-ZERO2 and TIMES-DIFFERENCE, and
unfolding the functions DIFFERENCE and EQUAL, to:
T.
Case 2. (IMPLIES (AND (EQUAL M 0) (LESSP A B))
(EQUAL (TIMES M (DIFFERENCE B A))
(DIFFERENCE (TIMES A M)
(TIMES B M)))).
This again simplifies, using linear arithmetic, applying the lemmas
COMMUTATIVITY-OF-TIMES, DIFFERENCE-0, and TIMES-DIFFERENCE, and opening up
the definition of EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL M 0))
(NUMBERP M)
(LESSP A B))
(EQUAL (TIMES M (DIFFERENCE B A))
(DIFFERENCE (TIMES B M)
(TIMES A M)))),
which again simplifies, applying TIMES-DIFFERENCE, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
TIMES-DISTRIBUTES-OVER-PDIFFERENCE
(PROVE-LEMMA EQUAL-MODS-TRICK-1
(REWRITE)
(IMPLIES (EQUAL (REMAINDER (PDIFFERENCE A B) P)
0)
(EQUAL (EQUAL (REMAINDER A P)
(REMAINDER B P))
T)))
This formula simplifies, unfolding the function PDIFFERENCE, to two new goals:
Case 2. (IMPLIES (AND (NOT (LESSP A B))
(EQUAL (REMAINDER (DIFFERENCE A B) P)
0))
(EQUAL (REMAINDER A P)
(REMAINDER B P))).
Applying the lemmas DIFFERENCE-ELIM and REMAINDER-QUOTIENT-ELIM, replace A
by (PLUS B X) to eliminate (DIFFERENCE A B) and X by (PLUS Z (TIMES P V)) to
eliminate (REMAINDER X P) and (QUOTIENT X P). We use the type restriction
lemma noted when DIFFERENCE was introduced, LESSP-REMAINDER2, the type
restriction lemma noted when REMAINDER was introduced, and the type
restriction lemma noted when QUOTIENT was introduced to restrict the new
variables. We thus obtain the following four new formulas:
Case 2.4.
(IMPLIES (AND (NOT (NUMBERP A))
(NOT (LESSP A B))
(EQUAL (REMAINDER (DIFFERENCE A B) P)
0))
(EQUAL (REMAINDER A P)
(REMAINDER B P))).
However this further simplifies, using linear arithmetic, appealing to the
lemmas DIFFERENCE-0 and REMAINDER-0-CROCK, and unfolding the definitions
of LESSP, EQUAL, and REMAINDER, to:
T.
Case 2.3.
(IMPLIES (AND (EQUAL P 0)
(NUMBERP X)
(NOT (LESSP (PLUS B X) B))
(EQUAL (REMAINDER X P) 0))
(EQUAL (REMAINDER (PLUS B X) P)
(REMAINDER B P))),
which further simplifies, rewriting with COMMUTATIVITY-OF-PLUS, and
opening up EQUAL, REMAINDER, and PLUS, to:
T.
Case 2.2.
(IMPLIES (AND (NOT (NUMBERP P))
(NUMBERP X)
(NOT (LESSP (PLUS B X) B))
(EQUAL (REMAINDER X P) 0))
(EQUAL (REMAINDER (PLUS B X) P)
(REMAINDER B P))).
But this further simplifies, rewriting with REMAINDER-WRT-12 and
COMMUTATIVITY-OF-PLUS, and opening up the functions EQUAL and PLUS, to:
T.
Case 2.1.
(IMPLIES (AND (NUMBERP Z)
(EQUAL (LESSP Z P) (NOT (ZEROP P)))
(NUMBERP V)
(NUMBERP P)
(NOT (EQUAL P 0))
(NOT (LESSP (PLUS B Z (TIMES P V)) B))
(EQUAL Z 0))
(EQUAL (REMAINDER (PLUS B Z (TIMES P V)) P)
(REMAINDER B P))).
However this further simplifies, rewriting with the lemma
REMAINDER-PLUS-TIMES-2, and expanding the functions NUMBERP, EQUAL, LESSP,
ZEROP, NOT, and PLUS, to:
T.
Case 1. (IMPLIES (AND (LESSP A B)
(EQUAL (REMAINDER (DIFFERENCE B A) P)
0))
(EQUAL (REMAINDER A P)
(REMAINDER B P))).
Applying the lemmas DIFFERENCE-ELIM and REMAINDER-QUOTIENT-ELIM, replace B
by (PLUS A X) to eliminate (DIFFERENCE B A) and X by (PLUS Z (TIMES P V)) to
eliminate (REMAINDER X P) and (QUOTIENT X P). We rely upon the type
restriction lemma noted when DIFFERENCE was introduced, 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 five new goals:
Case 1.5.
(IMPLIES (AND (LESSP B A)
(LESSP A B)
(EQUAL (REMAINDER (DIFFERENCE B A) P)
0))
(EQUAL (REMAINDER A P)
(REMAINDER B P))).
However this further simplifies, using linear arithmetic, to:
T.
Case 1.4.
(IMPLIES (AND (NOT (NUMBERP B))
(LESSP A B)
(EQUAL (REMAINDER (DIFFERENCE B A) P)
0))
(EQUAL (REMAINDER A P)
(REMAINDER B P))),
which further simplifies, unfolding the definition of LESSP, to:
T.
Case 1.3.
(IMPLIES (AND (EQUAL P 0)
(NUMBERP X)
(NOT (LESSP (PLUS A X) A))
(LESSP A (PLUS A X))
(EQUAL (REMAINDER X P) 0))
(EQUAL (REMAINDER A P)
(REMAINDER (PLUS A X) P))),
which further simplifies, rewriting with COMMUTATIVITY-OF-PLUS, and
expanding the definitions of EQUAL, REMAINDER, and PLUS, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP P))
(NUMBERP X)
(NOT (LESSP (PLUS A X) A))
(LESSP A (PLUS A X))
(EQUAL (REMAINDER X P) 0))
(EQUAL (REMAINDER A P)
(REMAINDER (PLUS A X) P))).
But this further simplifies, rewriting with REMAINDER-WRT-12 and
COMMUTATIVITY-OF-PLUS, and unfolding the definitions of EQUAL and PLUS, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP Z)
(EQUAL (LESSP Z P) (NOT (ZEROP P)))
(NUMBERP V)
(NUMBERP P)
(NOT (EQUAL P 0))
(NOT (LESSP (PLUS A Z (TIMES P V)) A))
(LESSP A (PLUS A Z (TIMES P V)))
(EQUAL Z 0))
(EQUAL (REMAINDER A P)
(REMAINDER (PLUS A Z (TIMES P V))
P))).
However this further simplifies, applying REMAINDER-PLUS-TIMES-2, and
opening up NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to:
T.
Q.E.D.
[ 0.0 0.2 0.0 ]
EQUAL-MODS-TRICK-1
(PROVE-LEMMA EQUAL-MODS-TRICK-2
(REWRITE)
(IMPLIES (EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER (PDIFFERENCE A B) P)
0))
((DISABLE DIFFERENCE-ELIM)))
This formula simplifies, opening up PDIFFERENCE, to the following two new
formulas:
Case 2. (IMPLIES (AND (EQUAL (REMAINDER A P)
(REMAINDER B P))
(NOT (LESSP A B)))
(EQUAL (REMAINDER (DIFFERENCE A B) P)
0)).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace A by
(PLUS X (TIMES P Z)) to eliminate (REMAINDER A P) and (QUOTIENT A P). We
employ LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was
introduced, and the type restriction lemma noted when QUOTIENT was
introduced to constrain the new variables. This generates four new formulas:
Case 2.4.
(IMPLIES (AND (NOT (NUMBERP A))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(NOT (LESSP A B)))
(EQUAL (REMAINDER (DIFFERENCE A B) P)
0)),
which further simplifies, using linear arithmetic, applying the lemmas
DIFFERENCE-0 and REMAINDER-0-CROCK, and expanding the definitions of LESSP,
REMAINDER, and EQUAL, to:
T.
Case 2.3.
(IMPLIES (AND (EQUAL P 0)
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(NOT (LESSP A B)))
(EQUAL (REMAINDER (DIFFERENCE A B) P)
0)),
which further simplifies, using linear arithmetic, applying DIFFERENCE-0,
and expanding EQUAL, REMAINDER, and LESSP, to:
T.
Case 2.2.
(IMPLIES (AND (NOT (NUMBERP P))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(NOT (LESSP A B)))
(EQUAL (REMAINDER (DIFFERENCE A B) P)
0)).
However this further simplifies, using linear arithmetic, applying
REMAINDER-WRT-12, DIFFERENCE-0, and REMAINDER-0-CROCK, and expanding the
definitions of EQUAL and LESSP, to:
T.
Case 2.1.
(IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X P) (NOT (ZEROP P)))
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(EQUAL X (REMAINDER B P))
(NOT (LESSP (PLUS X (TIMES P Z)) B)))
(EQUAL (REMAINDER (DIFFERENCE (PLUS X (TIMES P Z)) B)
P)
0)).
But this further simplifies, applying LESSP-REMAINDER2, and expanding
ZEROP, NOT, and EQUAL, to:
(IMPLIES
(AND (NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(NOT (LESSP (PLUS (REMAINDER B P) (TIMES P Z))
B)))
(EQUAL (REMAINDER (DIFFERENCE (PLUS (REMAINDER B P) (TIMES P Z))
B)
P)
0)).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace B by
(PLUS X (TIMES P V)) to eliminate (REMAINDER B P) and (QUOTIENT B 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. We would thus like to prove the
following two new conjectures:
Case 2.1.2.
(IMPLIES
(AND (NOT (NUMBERP B))
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(NOT (LESSP (PLUS (REMAINDER B P) (TIMES P Z))
B)))
(EQUAL (REMAINDER (DIFFERENCE (PLUS (REMAINDER B P) (TIMES P Z))
B)
P)
0)).
This further simplifies, rewriting with EQUAL-TIMES-0, and expanding the
definitions of LESSP, REMAINDER, EQUAL, PLUS, and DIFFERENCE, to the
following two new formulas:
Case 2.1.2.2.
(IMPLIES (AND (NOT (NUMBERP B))
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(NOT (EQUAL Z 0)))
(EQUAL (REMAINDER (TIMES P Z) P) 0)).
This finally simplifies, applying REMAINDER-TIMES, and opening up
EQUAL, to:
T.
Case 2.1.2.1.
(IMPLIES (AND (NOT (NUMBERP B))
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(EQUAL Z 0))
(EQUAL (REMAINDER 0 P) 0)).
This finally simplifies, rewriting with REMAINDER-0-CROCK, and opening
up the functions NUMBERP and EQUAL, to:
T.
Case 2.1.1.
(IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X P) (NOT (ZEROP P)))
(NUMBERP V)
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(NOT (LESSP (PLUS X (TIMES P Z))
(PLUS X (TIMES P V)))))
(EQUAL (REMAINDER (DIFFERENCE (PLUS X (TIMES P Z))
(PLUS X (TIMES P V)))
P)
0)).
However this further simplifies, applying the lemmas
LESSP-PLUS-CANCELATION, DIFFERENCE-PLUS-CANCELATION, and
REMAINDER-DIFFERENCE-TIMES, and unfolding the functions ZEROP, NOT, and
EQUAL, to:
T.
Case 1. (IMPLIES (AND (EQUAL (REMAINDER A P)
(REMAINDER B P))
(LESSP A B))
(EQUAL (REMAINDER (DIFFERENCE B 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. This produces the following four
new goals:
Case 1.4.
(IMPLIES (AND (NOT (NUMBERP A))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(LESSP A B))
(EQUAL (REMAINDER (DIFFERENCE B A) P)
0)).
But this further simplifies, opening up the definitions of LESSP,
REMAINDER, DIFFERENCE, and EQUAL, to:
T.
Case 1.3.
(IMPLIES (AND (EQUAL P 0)
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(LESSP A B))
(EQUAL (REMAINDER (DIFFERENCE B A) P)
0)),
which further simplifies, applying DIFFERENCE-X-X, and unfolding the
functions EQUAL, REMAINDER, and LESSP, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP P))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(LESSP A B))
(EQUAL (REMAINDER (DIFFERENCE B A) P)
0)).
However this further simplifies, applying REMAINDER-WRT-12, DIFFERENCE-X-X,
and REMAINDER-0-CROCK, and unfolding the functions EQUAL and LESSP, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X P) (NOT (ZEROP P)))
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(EQUAL X (REMAINDER B P))
(LESSP (PLUS X (TIMES P Z)) B))
(EQUAL (REMAINDER (DIFFERENCE B (PLUS X (TIMES P Z)))
P)
0)).
This further simplifies, applying the lemma LESSP-REMAINDER2, and opening
up the definitions of ZEROP, NOT, and EQUAL, to the conjecture:
(IMPLIES
(AND (NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(LESSP (PLUS (REMAINDER B P) (TIMES P Z))
B))
(EQUAL (REMAINDER (DIFFERENCE B
(PLUS (REMAINDER B P) (TIMES P Z)))
P)
0)).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace B by
(PLUS X (TIMES P V)) to eliminate (REMAINDER B P) and (QUOTIENT B 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 constrain the new variables. The result is two new goals:
Case 1.1.2.
(IMPLIES
(AND (NOT (NUMBERP B))
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(LESSP (PLUS (REMAINDER B P) (TIMES P Z))
B))
(EQUAL (REMAINDER (DIFFERENCE B
(PLUS (REMAINDER B P) (TIMES P Z)))
P)
0)),
which further simplifies, opening up the definitions of LESSP, REMAINDER,
EQUAL, and PLUS, to:
T.
Case 1.1.1.
(IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X P) (NOT (ZEROP P)))
(NUMBERP V)
(NUMBERP Z)
(NUMBERP P)
(NOT (EQUAL P 0))
(LESSP (PLUS X (TIMES P Z))
(PLUS X (TIMES P V))))
(EQUAL (REMAINDER (DIFFERENCE (PLUS X (TIMES P V))
(PLUS X (TIMES P Z)))
P)
0)),
which further simplifies, applying LESSP-PLUS-CANCELATION,
DIFFERENCE-PLUS-CANCELATION, and REMAINDER-DIFFERENCE-TIMES, and opening
up the functions ZEROP, NOT, and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.4 0.0 ]
EQUAL-MODS-TRICK-2
(DISABLE PDIFFERENCE)
[ 0.0 0.0 0.0 ]
PDIFFERENCE-OFF
(PROVE-LEMMA PRIME-KEY-TRICK
(REWRITE)
(IMPLIES (AND (EQUAL (REMAINDER (TIMES M A) P)
(REMAINDER (TIMES M B) P))
(NOT (EQUAL (REMAINDER M P) 0))
(PRIME P))
(EQUAL (EQUAL (REMAINDER A P)
(REMAINDER B P))
T))
((USE (PRIME-KEY-REWRITE (A M)
(B (PDIFFERENCE A B)))
(EQUAL-MODS-TRICK-2 (A (TIMES M A))
(B (TIMES M B))))
(DISABLE PRIME-KEY-REWRITE EQUAL-MODS-TRICK-2)))
WARNING: Note that PRIME-KEY-TRICK contains the free variable M which will be
chosen by instantiating the hypothesis:
(EQUAL (REMAINDER (TIMES M A) P)
(REMAINDER (TIMES M B) P)).
This conjecture can be simplified, using the abbreviations PRIME, NOT, IMPLIES,
and AND, to:
(IMPLIES
(AND (IMPLIES (PRIME P)
(EQUAL (EQUAL (REMAINDER (TIMES M (PDIFFERENCE A B))
P)
0)
(OR (EQUAL (REMAINDER M P) 0)
(EQUAL (REMAINDER (PDIFFERENCE A B) P)
0))))
(IMPLIES (EQUAL (REMAINDER (TIMES M A) P)
(REMAINDER (TIMES M B) P))
(EQUAL (REMAINDER (PDIFFERENCE (TIMES M A) (TIMES M B))
P)
0))
(EQUAL (REMAINDER (TIMES M A) P)
(REMAINDER (TIMES M B) P))
(NOT (EQUAL (REMAINDER M P) 0))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL (EQUAL (REMAINDER A P)
(REMAINDER B P))
T)).
This simplifies, rewriting with the lemmas COMMUTATIVITY-OF-TIMES,
TIMES-DISTRIBUTES-OVER-PDIFFERENCE, and EQUAL-MODS-TRICK-1, and unfolding the
definitions of PRIME, OR, IMPLIES, and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.2 0.0 ]
PRIME-KEY-TRICK
(PROVE-LEMMA PRODUCT-DIVIDES-LEMMA
(REWRITE)
(IMPLIES (EQUAL (REMAINDER X Z) 0)
(EQUAL (REMAINDER (TIMES Y X) (TIMES Y Z))
0)))
This formula simplifies, applying the lemma COMMUTATIVITY-OF-TIMES, to:
(IMPLIES (EQUAL (REMAINDER X Z) 0)
(EQUAL (REMAINDER (TIMES X Y) (TIMES Y Z))
0)).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace X by (PLUS V (TIMES Z W))
to eliminate (REMAINDER X Z) and (QUOTIENT X Z). 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. This produces the following four new formulas:
Case 4. (IMPLIES (AND (NOT (NUMBERP X))
(EQUAL (REMAINDER X Z) 0))
(EQUAL (REMAINDER (TIMES X Y) (TIMES Y Z))
0)).
This further simplifies, rewriting with the lemma EQUAL-TIMES-0, and opening
up LESSP, REMAINDER, and EQUAL, to:
T.
Case 3. (IMPLIES (AND (EQUAL Z 0)
(EQUAL (REMAINDER X Z) 0))
(EQUAL (REMAINDER (TIMES X Y) (TIMES Y Z))
0)),
which further simplifies, rewriting with the lemmas COMMUTATIVITY-OF-TIMES,
REMAINDER-X-X, TIMES-IDENTITY, and EQUAL-TIMES-0, and expanding EQUAL and
REMAINDER, to:
T.
Case 2. (IMPLIES (AND (NOT (NUMBERP Z))
(EQUAL (REMAINDER X Z) 0))
(EQUAL (REMAINDER (TIMES X Y) (TIMES Y Z))
0)),
which further simplifies, rewriting with REMAINDER-WRT-12, TIMES-ZERO2,
REMAINDER-TIMES, and EQUAL-TIMES-0, and unfolding the functions EQUAL and
REMAINDER, to:
T.
Case 1. (IMPLIES (AND (NUMBERP V)
(EQUAL (LESSP V Z) (NOT (ZEROP Z)))
(NUMBERP W)
(NUMBERP Z)
(NOT (EQUAL Z 0))
(EQUAL V 0))
(EQUAL (REMAINDER (TIMES (PLUS V (TIMES Z W)) Y)
(TIMES Y Z))
0)).
This further simplifies, applying COMMUTATIVITY-OF-TIMES,
ASSOCIATIVITY-OF-TIMES, and DIVIDES-TIMES, and opening up NUMBERP, EQUAL,
LESSP, ZEROP, NOT, and PLUS, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
PRODUCT-DIVIDES-LEMMA
(PROVE-LEMMA PRODUCT-DIVIDES
(REWRITE)
(IMPLIES (AND (EQUAL (REMAINDER X P) 0)
(EQUAL (REMAINDER X Q) 0)
(PRIME P)
(PRIME Q)
(NOT (EQUAL P Q)))
(EQUAL (REMAINDER X (TIMES P Q)) 0)))
This formula can be simplified, using the abbreviations NOT, PRIME, AND, and
IMPLIES, to:
(IMPLIES (AND (EQUAL (REMAINDER X P) 0)
(EQUAL (REMAINDER X Q) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q)))
(EQUAL (REMAINDER X (TIMES P Q)) 0)).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace X by (PLUS Z (TIMES P V))
to eliminate (REMAINDER X P) and (QUOTIENT X 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. This produces the following two new conjectures:
Case 2. (IMPLIES (AND (NOT (NUMBERP X))
(EQUAL (REMAINDER X P) 0)
(EQUAL (REMAINDER X Q) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q)))
(EQUAL (REMAINDER X (TIMES P Q)) 0)).
This simplifies, rewriting with EQUAL-TIMES-0, and opening up LESSP,
REMAINDER, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NUMBERP Z)
(EQUAL (LESSP Z P) (NOT (ZEROP P)))
(NUMBERP V)
(EQUAL Z 0)
(EQUAL (REMAINDER (PLUS Z (TIMES P V)) Q)
0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q)))
(EQUAL (REMAINDER (PLUS Z (TIMES P V))
(TIMES P Q))
0)).
But this simplifies, rewriting with LITTLE-STEP, PRIME-KEY-REWRITE, and
PRODUCT-DIVIDES-LEMMA, and opening up the definitions of NUMBERP, EQUAL,
LESSP, ZEROP, NOT, PLUS, and PRIME, to:
T.
Q.E.D.
[ 0.0 0.3 0.0 ]
PRODUCT-DIVIDES
(PROVE-LEMMA THM-53-SPECIALIZED-TO-PRIMES NIL
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER A Q)
(REMAINDER B Q)))
(EQUAL (REMAINDER A (TIMES P Q))
(REMAINDER B (TIMES P Q))))
NIL)
This formula can be simplified, using the abbreviations NOT, PRIME, AND, and
IMPLIES, to the new formula:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER A Q)
(REMAINDER B Q)))
(EQUAL (REMAINDER A (TIMES P Q))
(REMAINDER B (TIMES P Q)))),
which simplifies, applying PRODUCT-DIVIDES, EQUAL-MODS-TRICK-2, and
EQUAL-MODS-TRICK-1, and unfolding the definitions of EQUAL and PRIME, to:
T.
Q.E.D.
[ 0.0 0.2 0.0 ]
THM-53-SPECIALIZED-TO-PRIMES
(PROVE-LEMMA COROLLARY-53
(REWRITE)
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER A Q)
(REMAINDER B Q))
(NUMBERP B)
(LESSP B (TIMES P Q)))
(EQUAL (EQUAL (REMAINDER A (TIMES P Q)) B)
T))
((USE (THM-53-SPECIALIZED-TO-PRIMES))
(DISABLE THM-53-SPECIALIZED-TO-PRIMES)))
This formula can be simplified, using the abbreviations NOT, PRIME, AND, and
IMPLIES, to the new formula:
(IMPLIES (AND (IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER A Q)
(REMAINDER B Q)))
(EQUAL (REMAINDER A (TIMES P Q))
(REMAINDER B (TIMES P Q))))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q))
(EQUAL (REMAINDER A P)
(REMAINDER B P))
(EQUAL (REMAINDER A Q)
(REMAINDER B Q))
(NUMBERP B)
(LESSP B (TIMES P Q)))
(EQUAL (EQUAL (REMAINDER A (TIMES P Q)) B)
T)),
which simplifies, rewriting with the lemma EQUAL-TIMES-0, and expanding the
definitions of PRIME, NOT, AND, REMAINDER, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
COROLLARY-53
(PROVE-LEMMA THM-55-SPECIALIZED-TO-PRIMES
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0)))
(EQUAL (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER (TIMES M Y) P))
(EQUAL (REMAINDER X P)
(REMAINDER Y P)))))
This formula can be simplified, using the abbreviations NOT, PRIME, AND, and
IMPLIES, to:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0)))
(EQUAL (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER (TIMES M Y) P))
(EQUAL (REMAINDER X P)
(REMAINDER Y P)))),
which simplifies, trivially, to the following two new formulas:
Case 2. (IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(NOT (EQUAL (REMAINDER X P)
(REMAINDER Y P))))
(NOT (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER (TIMES M Y) P)))).
But this again simplifies, applying PRIME-KEY-TRICK, and opening up the
function PRIME, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(EQUAL (REMAINDER X P)
(REMAINDER Y P)))
(EQUAL (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER (TIMES M Y) P))
T)).
But this again simplifies, applying the lemmas EQUAL-MODS-TRICK-2,
REMAINDER-EXP-LEMMA, and EQUAL-MODS-TRICK-1, and opening up the function
EQUAL, to:
T.
Q.E.D.
[ 0.0 0.3 0.0 ]
THM-55-SPECIALIZED-TO-PRIMES
(PROVE-LEMMA COROLLARY-55
(REWRITE)
(IMPLIES (PRIME P)
(EQUAL (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER M P))
(OR (EQUAL (REMAINDER M P) 0)
(EQUAL (REMAINDER X P) 1))))
((USE (THM-55-SPECIALIZED-TO-PRIMES (Y 1)))
(DISABLE THM-55-SPECIALIZED-TO-PRIMES)))
This conjecture can be simplified, using the abbreviations PRIME and IMPLIES,
to the conjecture:
(IMPLIES (AND (IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0)))
(EQUAL (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER (TIMES M 1) P))
(EQUAL (REMAINDER X P)
(REMAINDER 1 P))))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER M P))
(OR (EQUAL (REMAINDER M P) 0)
(EQUAL (REMAINDER X P) 1)))).
This simplifies, applying the lemmas TIMES-1, COMMUTATIVITY-OF-TIMES,
REMAINDER-OF-1, PRIME-KEY-REWRITE, EQUAL-TIMES-0, EQUAL-MODS-TRICK-2, and
EQUAL-MODS-TRICK-1, and expanding the definitions of PRIME, NOT, AND, IMPLIES,
EQUAL, OR, LESSP, and REMAINDER, to the new conjecture:
(IMPLIES (AND (NOT (EQUAL (REMAINDER X P) 1))
(NUMBERP M)
(NOT (EQUAL (REMAINDER (TIMES M X) P)
(REMAINDER M P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(NOT (EQUAL (REMAINDER M P) 0))),
which again simplifies, applying PRIME-KEY-REWRITE, and opening up PRIME and
EQUAL, to:
T.
Q.E.D.
[ 0.0 0.2 0.0 ]
COROLLARY-55
(DEFN ALL-DISTINCT
(L)
(IF (NLISTP L)
T
(AND (NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L)))))
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 recursive call. Hence,
ALL-DISTINCT is accepted under the principle of definition. From the
definition we can conclude that:
(OR (FALSEP (ALL-DISTINCT L))
(TRUEP (ALL-DISTINCT L)))
is a theorem.
[ 0.0 0.0 0.0 ]
ALL-DISTINCT
(DEFN ALL-LESSEQP
(L N)
(IF (NLISTP L)
T
(AND (NOT (LESSP N (CAR L)))
(ALL-LESSEQP (CDR 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 recursive call. Hence, ALL-LESSEQP
is accepted under the principle of definition. From the definition we can
conclude that (OR (FALSEP (ALL-LESSEQP L N)) (TRUEP (ALL-LESSEQP L N))) is a
theorem.
[ 0.0 0.0 0.0 ]
ALL-LESSEQP
(DEFN ALL-NON-ZEROP
(L)
(IF (NLISTP L)
T
(AND (NOT (ZEROP (CAR L)))
(ALL-NON-ZEROP (CDR L)))))
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 recursive call. Hence,
ALL-NON-ZEROP is accepted under the definitional principle. Note that:
(OR (FALSEP (ALL-NON-ZEROP L))
(TRUEP (ALL-NON-ZEROP L)))
is a theorem.
[ 0.0 0.0 0.0 ]
ALL-NON-ZEROP
(DEFN POSITIVES
(N)
(IF (ZEROP N)
NIL
(CONS N (POSITIVES (SUB1 N)))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to establish that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call. Hence, POSITIVES is
accepted under the principle of definition. From the definition we can
conclude that (OR (LITATOM (POSITIVES N)) (LISTP (POSITIVES N))) is a theorem.
[ 0.0 0.0 0.0 ]
POSITIVES
(PROVE-LEMMA LISTP-POSITIVES
(REWRITE)
(EQUAL (LISTP (POSITIVES N))
(NOT (ZEROP N))))
This conjecture simplifies, opening up the functions ZEROP and NOT, to the
following three new goals:
Case 3. (IMPLIES (NOT (NUMBERP N))
(EQUAL (LISTP (POSITIVES N)) F)).
But this again simplifies, expanding the definitions of POSITIVES, LISTP,
and EQUAL, to:
T.
Case 2. (IMPLIES (EQUAL N 0)
(EQUAL (LISTP (POSITIVES N)) F)),
which again simplifies, unfolding POSITIVES, LISTP, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N))
(EQUAL (LISTP (POSITIVES N)) T)),
which again simplifies, clearly, to the new conjecture:
(IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N))
(LISTP (POSITIVES N))),
which we will name *1.
Perhaps we can prove it by induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP N) (p N))
(IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
(p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to establish 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 three new formulas:
Case 3. (IMPLIES (AND (ZEROP N)
(NOT (EQUAL N 0))
(NUMBERP N))
(LISTP (POSITIVES N))),
which simplifies, unfolding the function ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP N))
(EQUAL (SUB1 N) 0)
(NOT (EQUAL N 0))
(NUMBERP N))
(LISTP (POSITIVES N))),
which simplifies, expanding the functions ZEROP and POSITIVES, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(LISTP (POSITIVES (SUB1 N)))
(NOT (EQUAL N 0))
(NUMBERP N))
(LISTP (POSITIVES N))),
which simplifies, expanding the functions ZEROP and POSITIVES, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LISTP-POSITIVES
(PROVE-LEMMA CAR-POSITIVES
(REWRITE)
(EQUAL (CAR (POSITIVES N))
(IF (ZEROP N) 0 N)))
This simplifies, unfolding the definition of ZEROP, to the following three new
goals:
Case 3. (IMPLIES (NOT (NUMBERP N))
(EQUAL (CAR (POSITIVES N)) 0)).
This again simplifies, opening up the definitions of POSITIVES, CAR, and
EQUAL, to:
T.
Case 2. (IMPLIES (EQUAL N 0)
(EQUAL (CAR (POSITIVES N)) 0)),
which again simplifies, opening up the definitions of POSITIVES, CAR, and
EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N))
(EQUAL (CAR (POSITIVES N)) N)),
which we will name *1.
We will appeal to induction. There is only one plausible induction. We
will induct according to the following scheme:
(AND (IMPLIES (ZEROP N) (p N))
(IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
(p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT N) decreases according to the well-founded relation
LESSP in each induction step of the scheme. The above induction scheme
produces the following three new goals:
Case 3. (IMPLIES (AND (ZEROP N)
(NOT (EQUAL N 0))
(NUMBERP N))
(EQUAL (CAR (POSITIVES N)) N)).
This simplifies, opening up the function ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP N))
(EQUAL (SUB1 N) 0)
(NOT (EQUAL N 0))
(NUMBERP N))
(EQUAL (CAR (POSITIVES N)) N)).
This simplifies, rewriting with CAR-CONS, and expanding the functions ZEROP
and POSITIVES, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(EQUAL (CAR (POSITIVES (SUB1 N)))
(SUB1 N))
(NOT (EQUAL N 0))
(NUMBERP N))
(EQUAL (CAR (POSITIVES N)) N)),
which simplifies, rewriting with the lemma CAR-CONS, and expanding the
definitions of ZEROP and POSITIVES, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
CAR-POSITIVES
(PROVE-LEMMA MEMBER-POSITIVES
(REWRITE)
(EQUAL (MEMBER X (POSITIVES N))
(IF (ZEROP X) F (LESSP X (ADD1 N)))))
This simplifies, rewriting with SUB1-ADD1, and opening up ZEROP and LESSP, to
four new conjectures:
Case 4. (IMPLIES (NOT (NUMBERP X))
(EQUAL (MEMBER X (POSITIVES N)) F)),
which again simplifies, trivially, to the new conjecture:
(IMPLIES (NOT (NUMBERP X))
(NOT (MEMBER X (POSITIVES N)))),
which we will name *1.
Case 3. (IMPLIES (EQUAL X 0)
(EQUAL (MEMBER X (POSITIVES N)) F)).
This again simplifies, obviously, to:
(NOT (MEMBER 0 (POSITIVES N))),
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:
(EQUAL (MEMBER X (POSITIVES N))
(IF (ZEROP X) F (LESSP X (ADD1 N)))),
named *1. Let us appeal to the induction principle. Two inductions are
suggested by terms in the conjecture, both of which are unflawed. However,
one of these is more likely than the other. We will induct according to the
following scheme:
(AND (IMPLIES (ZEROP N) (p X N))
(IMPLIES (AND (NOT (ZEROP N)) (p X (SUB1 N)))
(p X N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each induction step of the scheme. The above induction
scheme generates two new formulas:
Case 2. (IMPLIES (ZEROP N)
(EQUAL (MEMBER X (POSITIVES N))
(IF (ZEROP X) F (LESSP X (ADD1 N))))),
which simplifies, applying the lemma SUB1-TYPE-RESTRICTION, and opening up
the definitions of ZEROP, POSITIVES, LISTP, MEMBER, and ADD1, to two new
formulas:
Case 2.2.
(IMPLIES (AND (EQUAL N 0)
(NOT (EQUAL X 0))
(NUMBERP X))
(NOT (LESSP X 1))),
which again simplifies, using linear arithmetic, to:
T.
Case 2.1.
(IMPLIES (AND (NOT (NUMBERP N))
(NOT (EQUAL X 0))
(NUMBERP X))
(NOT (LESSP X 1))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(EQUAL (MEMBER X (POSITIVES (SUB1 N)))
(IF (ZEROP X)
F
(LESSP X (ADD1 (SUB1 N))))))
(EQUAL (MEMBER X (POSITIVES N))
(IF (ZEROP X) F (LESSP X (ADD1 N))))),
which simplifies, applying ADD1-SUB1, CDR-CONS, CAR-CONS, SUB1-ADD1, and
EQUAL-LESSP, and unfolding the functions ZEROP, POSITIVES, MEMBER, EQUAL,
and LESSP, to the following four new conjectures:
Case 1.4.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL X 0)
(EQUAL (MEMBER X (POSITIVES (SUB1 N)))
F))
(NOT (MEMBER 0 (POSITIVES (SUB1 N))))).
This again simplifies, clearly, to:
T.
Case 1.3.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL X 0))
(NUMBERP X)
(EQUAL (MEMBER X (POSITIVES (SUB1 N)))
(LESSP X N))
(NOT (LESSP (SUB1 X) N)))
(NOT (LESSP X N))).
However this again simplifies, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL X 0))
(NUMBERP X)
(EQUAL (MEMBER X (POSITIVES (SUB1 N)))
(LESSP X N))
(NOT (LESSP (SUB1 X) N)))
(NOT (EQUAL X N))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL X 0))
(NUMBERP X)
(EQUAL (MEMBER X (POSITIVES (SUB1 N)))
(LESSP X N))
(LESSP (SUB1 X) N)
(NOT (EQUAL X N)))
(LESSP X N)),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
MEMBER-POSITIVES
(PROVE-LEMMA ALL-NON-ZEROP-DELETE
(REWRITE)
(IMPLIES (ALL-NON-ZEROP L)
(ALL-NON-ZEROP (DELETE X L))))
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 (NLISTP L) (p X L))
(IMPLIES (AND (NOT (NLISTP L)) (p X (CDR L)))
(p X 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 the following three new formulas:
Case 3. (IMPLIES (AND (NLISTP L) (ALL-NON-ZEROP L))
(ALL-NON-ZEROP (DELETE X L))).
This simplifies, applying DELETE-NON-MEMBER, and expanding the functions
NLISTP, ALL-NON-ZEROP, and MEMBER, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-NON-ZEROP (CDR L)))
(ALL-NON-ZEROP L))
(ALL-NON-ZEROP (DELETE X L))),
which simplifies, opening up the functions NLISTP and ALL-NON-ZEROP, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L))
(ALL-NON-ZEROP (DELETE X (CDR L)))
(ALL-NON-ZEROP L))
(ALL-NON-ZEROP (DELETE X L))),
which simplifies, expanding NLISTP, ALL-NON-ZEROP, and DELETE, to:
(IMPLIES (AND (LISTP L)
(ALL-NON-ZEROP (DELETE X (CDR L)))
(NOT (EQUAL (CAR L) 0))
(NUMBERP (CAR L))
(ALL-NON-ZEROP (CDR L))
(NOT (EQUAL X (CAR L))))
(ALL-NON-ZEROP (CONS (CAR L) (DELETE X (CDR L))))).
This again simplifies, applying CDR-CONS and CAR-CONS, and expanding the
function ALL-NON-ZEROP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
ALL-NON-ZEROP-DELETE
(PROVE-LEMMA ALL-DISTINCT-DELETE
(REWRITE)
(IMPLIES (ALL-DISTINCT L)
(ALL-DISTINCT (DELETE X L))))
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 (NLISTP L) (p X L))
(IMPLIES (AND (NOT (NLISTP L)) (p X (CDR L)))
(p X 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 the following three new formulas:
Case 3. (IMPLIES (AND (NLISTP L) (ALL-DISTINCT L))
(ALL-DISTINCT (DELETE X L))).
This simplifies, applying DELETE-NON-MEMBER, and expanding the functions
NLISTP, ALL-DISTINCT, and MEMBER, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-DISTINCT (CDR L)))
(ALL-DISTINCT L))
(ALL-DISTINCT (DELETE X L))),
which simplifies, opening up the functions NLISTP and ALL-DISTINCT, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L))
(ALL-DISTINCT (DELETE X (CDR L)))
(ALL-DISTINCT L))
(ALL-DISTINCT (DELETE X L))),
which simplifies, expanding NLISTP, ALL-DISTINCT, and DELETE, to:
(IMPLIES (AND (LISTP L)
(ALL-DISTINCT (DELETE X (CDR L)))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (EQUAL X (CAR L))))
(ALL-DISTINCT (CONS (CAR L) (DELETE X (CDR L))))).
This again simplifies, applying CDR-CONS and CAR-CONS, and expanding the
function ALL-DISTINCT, to the new conjecture:
(IMPLIES (AND (LISTP L)
(ALL-DISTINCT (DELETE X (CDR L)))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (EQUAL X (CAR L))))
(NOT (MEMBER (CAR L) (DELETE X (CDR L))))),
which again simplifies, applying the lemma MEMBER-DELETE, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
ALL-DISTINCT-DELETE
(PROVE-LEMMA PIGEON-HOLE-PRINCIPLE-LEMMA-1
(REWRITE)
(IMPLIES (AND (ALL-DISTINCT L)
(ALL-LESSEQP L (ADD1 N)))
(ALL-LESSEQP (DELETE (ADD1 N) L) N)))
Call the conjecture *1.
We will appeal to induction. There are three plausible 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 formulas:
Case 4. (IMPLIES (AND (NLISTP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L (ADD1 N)))
(ALL-LESSEQP (DELETE (ADD1 N) L) N)),
which simplifies, applying DELETE-NON-MEMBER, and expanding the functions
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 (ADD1 N)))
(ALL-LESSEQP (DELETE (ADD1 N) L) N)).
This simplifies, expanding NLISTP and ALL-DISTINCT, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L))
(NOT (ALL-LESSEQP (CDR L) (ADD1 N)))
(ALL-DISTINCT L)
(ALL-LESSEQP L (ADD1 N)))
(ALL-LESSEQP (DELETE (ADD1 N) L) N)).
This simplifies, applying SUB1-ADD1, and expanding the definitions of NLISTP,
ALL-DISTINCT, ALL-LESSEQP, and LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L))
(ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
N)
(ALL-DISTINCT L)
(ALL-LESSEQP L (ADD1 N)))
(ALL-LESSEQP (DELETE (ADD1 N) L) N)),
which simplifies, applying SUB1-ADD1, CDR-CONS, CAR-CONS, and
SUB1-TYPE-RESTRICTION, and expanding the functions NLISTP, ALL-DISTINCT,
ALL-LESSEQP, LESSP, DELETE, and EQUAL, to the following three new goals:
Case 1.3.
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NUMBERP N)
(NOT (LESSP N (SUB1 (CAR L))))
(ALL-LESSEQP (CDR L) (ADD1 N))
(NOT (EQUAL (ADD1 N) (CAR L))))
(ALL-LESSEQP (CONS (CAR L)
(DELETE (ADD1 N) (CDR L)))
N)).
But this again simplifies, applying the lemmas CDR-CONS and CAR-CONS, and
opening up ALL-LESSEQP, to:
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NUMBERP N)
(NOT (LESSP N (SUB1 (CAR L))))
(ALL-LESSEQP (CDR L) (ADD1 N))
(NOT (EQUAL (ADD1 N) (CAR L))))
(NOT (LESSP N (CAR L)))).
But this again simplifies, using linear arithmetic, to the conjecture:
(IMPLIES (AND (NOT (NUMBERP (CAR L)))
(LISTP L)
(ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NUMBERP N)
(NOT (LESSP N (SUB1 (CAR L))))
(ALL-LESSEQP (CDR L) (ADD1 N))
(NOT (EQUAL (ADD1 N) (CAR L))))
(NOT (LESSP N (CAR L)))).
But this again simplifies, applying SUB1-NNUMBERP, and opening up EQUAL
and LESSP, to:
T.
Case 1.2.
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NUMBERP N)
(NOT (LESSP N (SUB1 (CAR L))))
(ALL-LESSEQP (CDR L) (ADD1 N))
(EQUAL (ADD1 N) (CAR L)))
(ALL-LESSEQP (CDR L) N)).
This again simplifies, rewriting with SUB1-ADD1, to:
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
N)
(NOT (MEMBER (ADD1 N) (CDR L)))
(ALL-DISTINCT (CDR L))
(NUMBERP N)
(NOT (LESSP N N))
(ALL-LESSEQP (CDR L) (ADD1 N))
(EQUAL (ADD1 N) (CAR L)))
(ALL-LESSEQP (CDR L) N)),
which further simplifies, rewriting with DELETE-NON-MEMBER, to:
T.
Case 1.1.
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (NUMBERP N))
(NOT (LESSP 0 (SUB1 (CAR L))))
(ALL-LESSEQP (CDR L) (ADD1 N)))
(ALL-LESSEQP (DELETE 1 L) N)).
However this again simplifies, expanding the definitions of EQUAL and
LESSP, to:
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE (ADD1 N) (CDR L))
N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (NUMBERP N))
(EQUAL (SUB1 (CAR L)) 0)
(ALL-LESSEQP (CDR L) (ADD1 N)))
(ALL-LESSEQP (DELETE 1 L) N)).
However this further simplifies, rewriting with SUB1-TYPE-RESTRICTION, to:
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE 1 (CDR L)) N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (NUMBERP N))
(EQUAL (SUB1 (CAR L)) 0)
(ALL-LESSEQP (CDR L) 1))
(ALL-LESSEQP (DELETE 1 L) N)),
which again simplifies, opening up DELETE, to two new conjectures:
Case 1.1.2.
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE 1 (CDR L)) N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (NUMBERP N))
(EQUAL (SUB1 (CAR L)) 0)
(ALL-LESSEQP (CDR L) 1)
(NOT (EQUAL 1 (CAR L))))
(ALL-LESSEQP (CONS (CAR L) (DELETE 1 (CDR L)))
N)),
which again simplifies, using linear arithmetic, to two new goals:
Case 1.1.2.2.
(IMPLIES (AND (LESSP (CAR L) 1)
(LISTP L)
(ALL-LESSEQP (DELETE 1 (CDR L)) N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (NUMBERP N))
(EQUAL (SUB1 (CAR L)) 0)
(ALL-LESSEQP (CDR L) 1)
(NOT (EQUAL 1 (CAR L))))
(ALL-LESSEQP (CONS (CAR L) (DELETE 1 (CDR L)))
N)),
which finally simplifies, rewriting with CDR-CONS, CAR-CONS, and
SUB1-NNUMBERP, and opening up LESSP, SUB1, NUMBERP, EQUAL, and
ALL-LESSEQP, to:
T.
Case 1.1.2.1.
(IMPLIES (AND (NOT (NUMBERP (CAR L)))
(LISTP L)
(ALL-LESSEQP (DELETE 1 (CDR L)) N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (NUMBERP N))
(EQUAL (SUB1 (CAR L)) 0)
(ALL-LESSEQP (CDR L) 1)
(NOT (EQUAL 1 (CAR L))))
(ALL-LESSEQP (CONS (CAR L) (DELETE 1 (CDR L)))
N)).
However this finally simplifies, rewriting with SUB1-NNUMBERP,
CDR-CONS, and CAR-CONS, and expanding the functions EQUAL, LESSP, and
ALL-LESSEQP, to:
T.
Case 1.1.1.
(IMPLIES (AND (LISTP L)
(ALL-LESSEQP (DELETE 1 (CDR L)) N)
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L))
(NOT (NUMBERP N))
(EQUAL (SUB1 (CAR L)) 0)
(ALL-LESSEQP (CDR L) 1)
(EQUAL 1 (CAR L)))
(ALL-LESSEQP (CDR L) N)).
This again simplifies, rewriting with DELETE-NON-MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
PIGEON-HOLE-PRINCIPLE-LEMMA-1
(PROVE-LEMMA PIGEON-HOLE-PRINCIPLE-LEMMA-2
(REWRITE)
(IMPLIES (AND (NOT (MEMBER (ADD1 N) X))
(ALL-LESSEQP X (ADD1 N)))
(ALL-LESSEQP X N)))
Call the conjecture *1.
We will appeal to induction. There are three plausible inductions.
However, they merge into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (NLISTP X) (p X N))
(IMPLIES (AND (NOT (NLISTP X))
(EQUAL (ADD1 N) (CAR X)))
(p X N))
(IMPLIES (AND (NOT (NLISTP X))
(NOT (EQUAL (ADD1 N) (CAR X)))
(p (CDR X) N))
(p X N))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to establish that the measure (COUNT X) decreases according
to the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme generates five new formulas:
Case 5. (IMPLIES (AND (NLISTP X)
(NOT (MEMBER (ADD1 N) X))
(ALL-LESSEQP X (ADD1 N)))
(ALL-LESSEQP X N)),
which simplifies, expanding the definitions of NLISTP, MEMBER, and
ALL-LESSEQP, to:
T.
Case 4. (IMPLIES (AND (NOT (NLISTP X))
(EQUAL (ADD1 N) (CAR X))
(NOT (MEMBER (ADD1 N) X))
(ALL-LESSEQP X (ADD1 N)))
(ALL-LESSEQP X N)),
which simplifies, opening up the definitions of NLISTP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP X))
(NOT (EQUAL (ADD1 N) (CAR X)))
(MEMBER (ADD1 N) (CDR X))
(NOT (MEMBER (ADD1 N) X))
(ALL-LESSEQP X (ADD1 N)))
(ALL-LESSEQP X N)),
which simplifies, opening up the definitions of NLISTP and MEMBER, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP X))
(NOT (EQUAL (ADD1 N) (CAR X)))
(NOT (ALL-LESSEQP (CDR X) (ADD1 N)))
(NOT (MEMBER (ADD1 N) X))
(ALL-LESSEQP X (ADD1 N)))
(ALL-LESSEQP X N)),
which simplifies, rewriting with SUB1-ADD1, and expanding the definitions of
NLISTP, MEMBER, ALL-LESSEQP, and LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP X))
(NOT (EQUAL (ADD1 N) (CAR X)))
(ALL-LESSEQP (CDR X) N)
(NOT (MEMBER (ADD1 N) X))
(ALL-LESSEQP X (ADD1 N)))
(ALL-LESSEQP X N)).
This simplifies, rewriting with SUB1-ADD1, and opening up the functions
NLISTP, MEMBER, ALL-LESSEQP, LESSP, and EQUAL, to two new conjectures:
Case 1.2.
(IMPLIES (AND (LISTP X)
(NOT (EQUAL (ADD1 N) (CAR X)))
(ALL-LESSEQP (CDR X) N)
(NOT (MEMBER (ADD1 N) (CDR X)))
(NUMBERP N)
(NOT (LESSP N (SUB1 (CAR X))))
(ALL-LESSEQP (CDR X) (ADD1 N)))
(NOT (LESSP N (CAR X)))),
which again simplifies, using linear arithmetic, to the conjecture:
(IMPLIES (AND (NOT (NUMBERP (CAR X)))
(LISTP X)
(NOT (EQUAL (ADD1 N) (CAR X)))
(ALL-LESSEQP (CDR X) N)
(NOT (MEMBER (ADD1 N) (CDR X)))
(NUMBERP N)
(NOT (LESSP N (SUB1 (CAR X))))
(ALL-LESSEQP (CDR X) (ADD1 N)))
(NOT (LESSP N (CAR X)))).
But this again simplifies, appealing to the lemma SUB1-NNUMBERP, and
expanding EQUAL and LESSP, to:
T.
Case 1.1.
(IMPLIES (AND (LISTP X)
(NOT (EQUAL (ADD1 N) (CAR X)))
(ALL-LESSEQP (CDR X) N)
(NOT (MEMBER (ADD1 N) (CDR X)))
(NOT (NUMBERP N))
(NOT (LESSP 0 (SUB1 (CAR X))))
(ALL-LESSEQP (CDR X) (ADD1 N))
(NOT (EQUAL (CAR X) 0)))
(NOT (NUMBERP (CAR X)))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (CAR X) 1)
(LISTP X)
(NOT (EQUAL (ADD1 N) 1))
(ALL-LESSEQP (CDR X) N)
(NOT (MEMBER (ADD1 N) (CDR X)))
(NOT (NUMBERP N))
(NOT (LESSP 0 (SUB1 1)))
(ALL-LESSEQP (CDR X) (ADD1 N))
(NOT (EQUAL 1 0)))
(NOT (NUMBERP 1))).
However this again simplifies, applying SUB1-TYPE-RESTRICTION, and opening
up EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
PIGEON-HOLE-PRINCIPLE-LEMMA-2
(PROVE-LEMMA PERM-MEMBER
(REWRITE)
(IMPLIES (AND (PERM A B) (MEMBER X A))
(MEMBER X B)))
WARNING: Note that PERM-MEMBER contains the free variable A which will be
chosen by instantiating the hypothesis (PERM A B).
Call the conjecture *1.
Perhaps we can prove it by induction. Four inductions are suggested by
terms in the conjecture. 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 (NLISTP A) (p X B A))
(IMPLIES (AND (NOT (NLISTP A))
(MEMBER (CAR A) B)
(p X (DELETE (CAR A) B) (CDR A)))
(p X B A))
(IMPLIES (AND (NOT (NLISTP A))
(NOT (MEMBER (CAR A) B)))
(p X B A))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to prove that the measure (COUNT A) decreases according to
the well-founded relation LESSP in each induction step of the scheme. Note,
however, the inductive instance chosen for B. The above induction scheme
leads to five new goals:
Case 5. (IMPLIES (AND (NLISTP A)
(PERM A B)
(MEMBER X A))
(MEMBER X B)),
which simplifies, opening up the definitions of NLISTP, PERM, and MEMBER, to:
T.
Case 4. (IMPLIES (AND (NOT (NLISTP A))
(MEMBER (CAR A) B)
(NOT (PERM (CDR A) (DELETE (CAR A) B)))
(PERM A B)
(MEMBER X A))
(MEMBER X B)),
which simplifies, expanding NLISTP and PERM, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP A))
(MEMBER (CAR A) B)
(NOT (MEMBER X (CDR A)))
(PERM A B)
(MEMBER X A))
(MEMBER X B)),
which simplifies, opening up the definitions of NLISTP, PERM, and MEMBER, to
the formula:
(IMPLIES (AND (LISTP A)
(MEMBER (CAR A) B)
(NOT (MEMBER X (CDR A)))
(PERM (CDR A) (DELETE (CAR A) B))
(EQUAL X (CAR A)))
(MEMBER X B)).
This again simplifies, trivially, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP A))
(MEMBER (CAR A) B)
(MEMBER X (DELETE (CAR A) B))
(PERM A B)
(MEMBER X A))
(MEMBER X B)).
This simplifies, appealing to the lemma MEMBER-DELETE, and expanding the
functions NLISTP, PERM, and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP A))
(NOT (MEMBER (CAR A) B))
(PERM A B)
(MEMBER X A))
(MEMBER X B)).
This simplifies, expanding the functions NLISTP and PERM, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
PERM-MEMBER
(DEFN PIGEON-HOLE-INDUCTION
(L)
(IF (LISTP L)
(IF (MEMBER (LENGTH L) L)
(PIGEON-HOLE-INDUCTION (DELETE (LENGTH L) L))
(PIGEON-HOLE-INDUCTION (CDR L)))
T))
Linear arithmetic and the lemmas LESSP-COUNT-DELETE and CDR-LESSP inform
us that the measure (COUNT L) decreases according to the well-founded relation
LESSP in each recursive call. Hence, PIGEON-HOLE-INDUCTION is accepted under
the principle of definition. Note that (TRUEP (PIGEON-HOLE-INDUCTION L)) is a
theorem.
[ 0.0 0.0 0.0 ]
PIGEON-HOLE-INDUCTION
(PROVE-LEMMA PIGEON-HOLE-PRINCIPLE NIL
(IMPLIES (AND (ALL-NON-ZEROP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L (LENGTH L)))
(PERM (POSITIVES (LENGTH L)) L))
((INDUCT (PIGEON-HOLE-INDUCTION L))))
This conjecture can be simplified, using the abbreviations IMPLIES, NOT, OR,
and AND, to three new formulas:
Case 3. (IMPLIES
(AND (LISTP L)
(MEMBER (LENGTH L) L)
(IMPLIES (AND (ALL-NON-ZEROP (DELETE (LENGTH L) L))
(ALL-DISTINCT (DELETE (LENGTH L) L))
(ALL-LESSEQP (DELETE (LENGTH L) L)
(LENGTH (DELETE (LENGTH L) L))))
(PERM (POSITIVES (LENGTH (DELETE (LENGTH L) L)))
(DELETE (LENGTH L) L)))
(ALL-NON-ZEROP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L (LENGTH L)))
(PERM (POSITIVES (LENGTH L)) L)),
which simplifies, appealing to the lemmas ALL-NON-ZEROP-DELETE,
ALL-DISTINCT-DELETE, and LENGTH-DELETE, and unfolding AND and IMPLIES, to
two new conjectures:
Case 3.2.
(IMPLIES (AND (LISTP L)
(MEMBER (LENGTH L) L)
(NOT (ALL-LESSEQP (DELETE (LENGTH L) L)
(LENGTH (CDR L))))
(ALL-NON-ZEROP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L (LENGTH L)))
(PERM (POSITIVES (LENGTH L)) L)),
which again simplifies, appealing to the lemmas SUB1-ADD1, CDR-CONS, and
CAR-CONS, and opening up the definitions of LENGTH, POSITIVES, and PERM,
to:
(IMPLIES (AND (LISTP L)
(MEMBER (ADD1 (LENGTH (CDR L))) L)
(NOT (ALL-LESSEQP (DELETE (ADD1 (LENGTH (CDR L))) L)
(LENGTH (CDR L))))
(ALL-NON-ZEROP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L
(ADD1 (LENGTH (CDR L)))))
(PERM (POSITIVES (LENGTH (CDR L)))
(DELETE (ADD1 (LENGTH (CDR L))) L))).
But this again simplifies, applying PIGEON-HOLE-PRINCIPLE-LEMMA-1, to:
T.
Case 3.1.
(IMPLIES (AND (LISTP L)
(MEMBER (LENGTH L) L)
(PERM (POSITIVES (LENGTH (CDR L)))
(DELETE (LENGTH L) L))
(ALL-NON-ZEROP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L (LENGTH L)))
(PERM (POSITIVES (LENGTH L)) L)).
This again simplifies, applying SUB1-ADD1, CDR-CONS, and CAR-CONS, and
expanding the functions LENGTH, POSITIVES, and PERM, to:
T.
Case 2. (IMPLIES (AND (LISTP L)
(NOT (MEMBER (LENGTH L) L))
(IMPLIES (AND (ALL-NON-ZEROP (CDR L))
(ALL-DISTINCT (CDR L))
(ALL-LESSEQP (CDR L)
(LENGTH (CDR L))))
(PERM (POSITIVES (LENGTH (CDR L)))
(CDR L)))
(ALL-NON-ZEROP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L (LENGTH L)))
(PERM (POSITIVES (LENGTH L)) L)).
This simplifies, applying SUB1-ADD1 and CAR-CONS, and unfolding LENGTH, AND,
IMPLIES, ALL-NON-ZEROP, ALL-DISTINCT, POSITIVES, and PERM, to two new goals:
Case 2.2.
(IMPLIES (AND (LISTP L)
(NOT (MEMBER (ADD1 (LENGTH (CDR L))) L))
(NOT (ALL-LESSEQP (CDR L)
(LENGTH (CDR L))))
(NOT (EQUAL (CAR L) 0))
(NUMBERP (CAR L))
(ALL-NON-ZEROP (CDR L))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L)))
(NOT (ALL-LESSEQP L
(ADD1 (LENGTH (CDR L)))))).
Applying the lemma CAR-CDR-ELIM, replace L by (CONS Z X) to eliminate
(CDR L) and (CAR L). This produces:
(IMPLIES (AND (NOT (MEMBER (ADD1 (LENGTH X)) (CONS Z X)))
(NOT (ALL-LESSEQP X (LENGTH X)))
(NOT (EQUAL Z 0))
(NUMBERP Z)
(ALL-NON-ZEROP X)
(NOT (MEMBER Z X))
(ALL-DISTINCT X))
(NOT (ALL-LESSEQP (CONS Z X)
(ADD1 (LENGTH X))))),
which further simplifies, rewriting with CDR-CONS, CAR-CONS, and SUB1-ADD1,
and opening up the definitions of MEMBER, LESSP, and ALL-LESSEQP, to:
(IMPLIES (AND (NOT (EQUAL (ADD1 (LENGTH X)) Z))
(NOT (MEMBER (ADD1 (LENGTH X)) X))
(NOT (ALL-LESSEQP X (LENGTH X)))
(NOT (EQUAL Z 0))
(NUMBERP Z)
(ALL-NON-ZEROP X)
(NOT (MEMBER Z X))
(ALL-DISTINCT X)
(NOT (LESSP (LENGTH X) (SUB1 Z))))
(NOT (ALL-LESSEQP X (ADD1 (LENGTH X))))),
which again simplifies, applying PIGEON-HOLE-PRINCIPLE-LEMMA-2, to:
T.
Case 2.1.
(IMPLIES (AND (LISTP L)
(NOT (MEMBER (ADD1 (LENGTH (CDR L))) L))
(PERM (POSITIVES (LENGTH (CDR L)))
(CDR L))
(NOT (EQUAL (CAR L) 0))
(NUMBERP (CAR L))
(ALL-NON-ZEROP (CDR L))
(NOT (MEMBER (CAR L) (CDR L)))
(ALL-DISTINCT (CDR L)))
(NOT (ALL-LESSEQP L
(ADD1 (LENGTH (CDR L)))))).
Appealing to the lemma CAR-CDR-ELIM, we now replace L by (CONS Z X) to
eliminate (CDR L) and (CAR L). We must thus prove:
(IMPLIES (AND (NOT (MEMBER (ADD1 (LENGTH X)) (CONS Z X)))
(PERM (POSITIVES (LENGTH X)) X)
(NOT (EQUAL Z 0))
(NUMBERP Z)
(ALL-NON-ZEROP X)
(NOT (MEMBER Z X))
(ALL-DISTINCT X))
(NOT (ALL-LESSEQP (CONS Z X)
(ADD1 (LENGTH X))))).
This further simplifies, rewriting with the lemmas CDR-CONS, CAR-CONS, and
SUB1-ADD1, and expanding the definitions of MEMBER, LESSP, and ALL-LESSEQP,
to the conjecture:
(IMPLIES (AND (NOT (EQUAL (ADD1 (LENGTH X)) Z))
(NOT (MEMBER (ADD1 (LENGTH X)) X))
(PERM (POSITIVES (LENGTH X)) X)
(NOT (EQUAL Z 0))
(NUMBERP Z)
(ALL-NON-ZEROP X)
(NOT (MEMBER Z X))
(ALL-DISTINCT X)
(NOT (LESSP (LENGTH X) (SUB1 Z))))
(NOT (ALL-LESSEQP X (ADD1 (LENGTH X))))).
However this again simplifies, using linear arithmetic and applying
MEMBER-POSITIVES and PERM-MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP L))
(ALL-NON-ZEROP L)
(ALL-DISTINCT L)
(ALL-LESSEQP L (LENGTH L)))
(PERM (POSITIVES (LENGTH L)) L)).
This simplifies, appealing to the lemma PIGEON-HOLE-PRINCIPLE-LEMMA-2, and
expanding the definitions of ALL-NON-ZEROP, ALL-DISTINCT, LENGTH,
ALL-LESSEQP, MEMBER, ADD1, POSITIVES, LISTP, and PERM, to:
T.
Q.E.D.
[ 0.0 0.3 0.0 ]
PIGEON-HOLE-PRINCIPLE
(PROVE-LEMMA PERM-TIMES-LIST NIL
(IMPLIES (PERM L1 L2)
(EQUAL (TIMES-LIST L1)
(TIMES-LIST L2))))
Name the conjecture *1.
We will appeal to induction. The recursive terms in the conjecture
suggest four 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 (NLISTP L1) (p L1 L2))
(IMPLIES (AND (NOT (NLISTP L1))
(MEMBER (CAR L1) L2)
(p (CDR L1) (DELETE (CAR L1) L2)))
(p L1 L2))
(IMPLIES (AND (NOT (NLISTP L1))
(NOT (MEMBER (CAR L1) L2)))
(p L1 L2))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT L1) decreases according to the
well-founded relation LESSP in each induction step of the scheme. Note,
however, the inductive instance chosen for L2. The above induction scheme
produces the following four new formulas:
Case 4. (IMPLIES (AND (NLISTP L1) (PERM L1 L2))
(EQUAL (TIMES-LIST L1)
(TIMES-LIST L2))).
This simplifies, expanding the definitions of NLISTP, PERM, TIMES-LIST, and
EQUAL, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP L1))
(MEMBER (CAR L1) L2)
(NOT (PERM (CDR L1) (DELETE (CAR L1) L2)))
(PERM L1 L2))
(EQUAL (TIMES-LIST L1)
(TIMES-LIST L2))).
This simplifies, applying PERM-MEMBER, and expanding the definitions of
NLISTP, MEMBER, and PERM, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP L1))
(MEMBER (CAR L1) L2)
(EQUAL (TIMES-LIST (CDR L1))
(TIMES-LIST (DELETE (CAR L1) L2)))
(PERM L1 L2))
(EQUAL (TIMES-LIST L1)
(TIMES-LIST L2))),
which simplifies, rewriting with the lemma PERM-MEMBER, and opening up the
functions NLISTP, MEMBER, PERM, and TIMES-LIST, to the goal:
(IMPLIES (AND (LISTP L1)
(EQUAL (TIMES-LIST (CDR L1))
(TIMES-LIST (DELETE (CAR L1) L2)))
(MEMBER (CAR L1) L2)
(PERM (CDR L1) (DELETE (CAR L1) L2)))
(EQUAL (TIMES (CAR L1) (TIMES-LIST (CDR L1)))
(TIMES-LIST L2))).
Appealing to the lemma CAR-CDR-ELIM, we now replace L1 by (CONS Z X) to
eliminate (CDR L1) and (CAR L1). This generates:
(IMPLIES (AND (EQUAL (TIMES-LIST X)
(TIMES-LIST (DELETE Z L2)))
(MEMBER Z L2)
(PERM X (DELETE Z L2)))
(EQUAL (TIMES Z (TIMES-LIST X))
(TIMES-LIST L2))).
We use the above equality hypothesis by substituting:
(TIMES-LIST (DELETE Z L2))
for (TIMES-LIST X) and throwing away the equality. This produces:
(IMPLIES (AND (MEMBER Z L2)
(PERM X (DELETE Z L2)))
(EQUAL (TIMES Z (TIMES-LIST (DELETE Z L2)))
(TIMES-LIST L2))),
which further simplifies, applying TIMES-TIMES-LIST-DELETE, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP L1))
(NOT (MEMBER (CAR L1) L2))
(PERM L1 L2))
(EQUAL (TIMES-LIST L1)
(TIMES-LIST L2))).
This simplifies, applying the lemma PERM-MEMBER, and opening up NLISTP and
MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
PERM-TIMES-LIST
(PROVE-LEMMA TIMES-LIST-POSITIVES
(REWRITE)
(EQUAL (TIMES-LIST (POSITIVES N))
(FACT N)))
Give the conjecture the name *1.
We will appeal to induction. Two inductions are suggested by terms in
the conjecture. However, they merge into one likely candidate induction. We
will induct according to the following scheme:
(AND (IMPLIES (ZEROP N) (p N))
(IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N)))
(p N))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT N) decreases according to the well-founded relation
LESSP in each induction step of the scheme. The above induction scheme
produces the following two new conjectures:
Case 2. (IMPLIES (ZEROP N)
(EQUAL (TIMES-LIST (POSITIVES N))
(FACT N))).
This simplifies, expanding the functions ZEROP, POSITIVES, TIMES-LIST, FACT,
and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(EQUAL (TIMES-LIST (POSITIVES (SUB1 N)))
(FACT (SUB1 N))))
(EQUAL (TIMES-LIST (POSITIVES N))
(FACT N))).
This simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS, and
opening up ZEROP, POSITIVES, TIMES-LIST, and FACT, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
TIMES-LIST-POSITIVES
(PROVE-LEMMA TIMES-LIST-EQUAL-FACT
(REWRITE)
(IMPLIES (PERM (POSITIVES N) L)
(EQUAL (TIMES-LIST L) (FACT N)))
((USE (PERM-TIMES-LIST (L1 (POSITIVES N))
(L2 L)))
(DISABLE PERM-TIMES-LIST)))
WARNING: Note that TIMES-LIST-EQUAL-FACT contains the free variable N which
will be chosen by instantiating the hypothesis (PERM (POSITIVES N) L).
This conjecture can be simplified, using the abbreviations IMPLIES and
TIMES-LIST-POSITIVES, to the conjecture:
(IMPLIES (AND (IMPLIES (PERM (POSITIVES N) L)
(EQUAL (FACT N) (TIMES-LIST L)))
(PERM (POSITIVES N) L))
(EQUAL (TIMES-LIST L) (FACT N))).
This simplifies, unfolding the function IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
TIMES-LIST-EQUAL-FACT
(PROVE-LEMMA PRIME-FACT
(REWRITE)
(IMPLIES (AND (PRIME P) (LESSP N P))
(NOT (EQUAL (REMAINDER (FACT N) P) 0)))
((INDUCT (FACT N))))
This formula can be simplified, using the abbreviations ZEROP, PRIME, IMPLIES,
NOT, OR, and AND, to the following two new formulas:
Case 2. (IMPLIES (AND (ZEROP N)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP N P))
(NOT (EQUAL (REMAINDER (FACT N) P) 0))).
This simplifies, rewriting with REMAINDER-OF-1, and unfolding the functions
ZEROP, EQUAL, LESSP, and FACT, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(IMPLIES (AND (PRIME P) (LESSP (SUB1 N) P))
(NOT (EQUAL (REMAINDER (FACT (SUB1 N)) P)
0)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP N P))
(NOT (EQUAL (REMAINDER (FACT N) P) 0))),
which simplifies, rewriting with PRIME-KEY-REWRITE, and opening up the
definitions of PRIME, AND, NOT, IMPLIES, LESSP, FACT, and REMAINDER, to the
new conjecture:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (LESSP (SUB1 N) P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(LESSP (SUB1 N) (SUB1 P)))
(NOT (EQUAL (REMAINDER (FACT (SUB1 N)) P)
0))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
PRIME-FACT
(DEFN S
(N M P)
(IF (ZEROP N)
NIL
(CONS (REMAINDER (TIMES M N) P)
(S (SUB1 N) M 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 recursive call. Hence, S is accepted under the
definitional principle. Note that (OR (LITATOM (S N M P)) (LISTP (S N M P)))
is a theorem.
[ 0.0 0.0 0.0 ]
S
(PROVE-LEMMA REMAINDER-TIMES-LIST-S NIL
(EQUAL (REMAINDER (TIMES-LIST (S N M P)) P)
(REMAINDER (TIMES (FACT N) (EXP M N))
P)))
Give the conjecture the name *1.
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 (ZEROP N) (p N M P))
(IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N) M P))
(p N M P))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each induction step of the scheme. The above induction
scheme leads to the following two new conjectures:
Case 2. (IMPLIES (ZEROP N)
(EQUAL (REMAINDER (TIMES-LIST (S N M P)) P)
(REMAINDER (TIMES (FACT N) (EXP M N))
P))).
This simplifies, appealing to the lemmas REMAINDER-OF-1 and EXP-BY-0, and
unfolding ZEROP, EQUAL, S, TIMES-LIST, FACT, TIMES, and EXP, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(EQUAL (REMAINDER (TIMES-LIST (S (SUB1 N) M P))
P)
(REMAINDER (TIMES (FACT (SUB1 N))
(EXP M (SUB1 N)))
P)))
(EQUAL (REMAINDER (TIMES-LIST (S N M P)) P)
(REMAINDER (TIMES (FACT N) (EXP M N))
P))).
This simplifies, applying CDR-CONS, CAR-CONS, ASSOCIATIVITY-OF-TIMES,
TIMES-MOD-3, COMMUTATIVITY2-OF-TIMES, EQUAL-MODS-TRICK-2,
REMAINDER-EXP-LEMMA, and EQUAL-MODS-TRICK-1, and expanding the definitions
of ZEROP, S, TIMES-LIST, FACT, EXP, and EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
REMAINDER-TIMES-LIST-S
(PROVE-LEMMA ALL-DISTINCT-S-LEMMA
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P))
(NOT (MEMBER (REMAINDER (TIMES M N1) P)
(S N2 M P))))
((INDUCT (S N2 M P))))
This conjecture can be simplified, using the abbreviations ZEROP, PRIME,
IMPLIES, NOT, OR, and AND, to two new formulas:
Case 2. (IMPLIES (AND (ZEROP N2)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P))
(NOT (MEMBER (REMAINDER (TIMES M N1) P)
(S N2 M P)))),
which simplifies, expanding the functions ZEROP, EQUAL, LESSP, S, LISTP, and
MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL N2 0))
(NUMBERP N2)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(NUMBERP N1)
(LESSP (SUB1 N2) N1)
(LESSP N1 P))
(NOT (MEMBER (REMAINDER (TIMES M N1) P)
(S (SUB1 N2) M P))))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P))
(NOT (MEMBER (REMAINDER (TIMES M N1) P)
(S N2 M P)))),
which simplifies, using linear arithmetic, applying CDR-CONS,
THM-55-SPECIALIZED-TO-PRIMES, DIFFERENCE-0, REMAINDER-0-CROCK, and CAR-CONS,
and opening up the definitions of PRIME, NOT, AND, IMPLIES, S, LESSP,
REMAINDER, and MEMBER, to the following five new formulas:
Case 1.5.
(IMPLIES (AND (NOT (EQUAL N2 0))
(NUMBERP N2)
(NOT (LESSP (SUB1 N2) N1))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P)
(NOT (LESSP (SUB1 N2) (SUB1 P))))
(NOT (EQUAL N1 0))).
This again simplifies, using linear arithmetic, to:
T.
Case 1.4.
(IMPLIES (AND (NOT (EQUAL N2 0))
(NUMBERP N2)
(NOT (LESSP (SUB1 N2) N1))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P)
(LESSP (SUB1 N2) (SUB1 P)))
(NOT (EQUAL N1 N2))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.3.
(IMPLIES (AND (NOT (EQUAL N2 0))
(NUMBERP N2)
(NOT (LESSP (SUB1 N2) N1))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P))
(NOT (MEMBER (REMAINDER (TIMES M N1) P)
(S (SUB1 N2) M P)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL N2 0))
(NUMBERP N2)
(NOT (MEMBER (REMAINDER (TIMES M N1) P)
(S (SUB1 N2) M P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P)
(NOT (LESSP (SUB1 N2) (SUB1 P))))
(NOT (EQUAL N1 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL N2 0))
(NUMBERP N2)
(NOT (MEMBER (REMAINDER (TIMES M N1) P)
(S (SUB1 N2) M P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(NUMBERP N1)
(LESSP N2 N1)
(LESSP N1 P)
(LESSP (SUB1 N2) (SUB1 P)))
(NOT (EQUAL N1 N2))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.2 0.0 ]
ALL-DISTINCT-S-LEMMA
(PROVE-LEMMA ALL-DISTINCT-S
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-DISTINCT (S N M P))))
This conjecture can be simplified, using the abbreviations NOT, PRIME, AND,
and IMPLIES, to the formula:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-DISTINCT (S N M P))).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace M by
(PLUS X (TIMES P Z)) to eliminate (REMAINDER M P) and (QUOTIENT M P). We
employ LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was
introduced, and the type restriction lemma noted when QUOTIENT was introduced
to constrain the new variables. This generates two new conjectures:
Case 2. (IMPLIES (AND (NOT (NUMBERP M))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-DISTINCT (S N M P))),
which simplifies, unfolding the functions LESSP, REMAINDER, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X P) (NOT (ZEROP P)))
(NUMBERP Z)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL X 0))
(LESSP N P))
(ALL-DISTINCT (S N (PLUS X (TIMES P Z)) P))),
which simplifies, unfolding ZEROP and NOT, to:
(IMPLIES (AND (NUMBERP X)
(LESSP X P)
(NUMBERP Z)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL X 0))
(LESSP N P))
(ALL-DISTINCT (S N (PLUS X (TIMES P Z)) P))).
Appealing to the lemma SUB1-ELIM, we now replace P by (ADD1 V) to eliminate
(SUB1 P). We employ the type restriction lemma noted when SUB1 was
introduced to constrain the new variable. This generates:
(IMPLIES (AND (NUMBERP V)
(NUMBERP X)
(LESSP X (ADD1 V))
(NUMBERP Z)
(NOT (EQUAL (ADD1 V) 0))
(NOT (EQUAL (ADD1 V) 1))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP N (ADD1 V)))
(ALL-DISTINCT (S N
(PLUS X (TIMES (ADD1 V) Z))
(ADD1 V)))).
But this further simplifies, rewriting with the lemmas SUB1-ADD1, ADD1-EQUAL,
COMMUTATIVITY-OF-TIMES, and TIMES-ADD1, and expanding LESSP, NUMBERP, EQUAL,
S, and ALL-DISTINCT, to the goal:
(IMPLIES (AND (NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP (SUB1 N) V))
(ALL-DISTINCT (S N
(PLUS X Z (TIMES V Z))
(ADD1 V)))).
Appealing to the lemma SUB1-ELIM, we now replace N by (ADD1 W) to eliminate
(SUB1 N). We use the type restriction lemma noted when SUB1 was introduced
to constrain the new variable. The result is three new conjectures:
Case 1.3.
(IMPLIES (AND (EQUAL N 0)
(NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP (SUB1 N) V))
(ALL-DISTINCT (S N
(PLUS X Z (TIMES V Z))
(ADD1 V)))),
which finally simplifies, unfolding SUB1, EQUAL, LESSP, S, and
ALL-DISTINCT, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP N))
(NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP (SUB1 N) V))
(ALL-DISTINCT (S N
(PLUS X Z (TIMES V Z))
(ADD1 V)))),
which finally simplifies, applying SUB1-NNUMBERP, and unfolding EQUAL,
LESSP, S, and ALL-DISTINCT, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP W)
(NOT (EQUAL (ADD1 W) 0))
(NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP W V))
(ALL-DISTINCT (S (ADD1 W)
(PLUS X Z (TIMES V Z))
(ADD1 V)))).
This further simplifies, applying SUB1-ADD1, ASSOCIATIVITY-OF-PLUS,
COMMUTATIVITY2-OF-PLUS, COMMUTATIVITY2-OF-TIMES,
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, TIMES-ADD1, COMMUTATIVITY-OF-TIMES,
CDR-CONS, and CAR-CONS, and opening up the definitions of S and
ALL-DISTINCT, to the following two new goals:
Case 1.1.2.
(IMPLIES (AND (NUMBERP W)
(NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP W V))
(NOT (MEMBER (REMAINDER (PLUS X Z
(TIMES V Z)
(TIMES W X)
(TIMES W Z)
(TIMES V W Z))
(ADD1 V))
(S W
(PLUS X Z (TIMES V Z))
(ADD1 V))))),
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 (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-DISTINCT (S N M P))).
We gave this the name *1 above. Perhaps we can prove it by induction. The
recursive terms in the conjecture suggest four inductions. They merge into
three likely candidate inductions. However, only one is unflawed. We will
induct according to the following scheme:
(AND (IMPLIES (ZEROP N) (p N M P))
(IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N) M P))
(p N M P))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each induction step of the scheme. The above induction
scheme generates the following three new conjectures:
Case 3. (IMPLIES (AND (ZEROP N)
(PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-DISTINCT (S N M P))).
This simplifies, opening up the functions ZEROP, PRIME, EQUAL, LESSP, S, and
ALL-DISTINCT, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP N))
(NOT (LESSP (SUB1 N) P))
(PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-DISTINCT (S N M P))).
This simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP N 1)
(NOT (ZEROP N))
(NOT (LESSP (SUB1 N) P))
(PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-DISTINCT (S N M P))),
which again simplifies, expanding the definitions of SUB1, NUMBERP, EQUAL,
LESSP, and ZEROP, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(ALL-DISTINCT (S (SUB1 N) M P))
(PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-DISTINCT (S N M P))),
which simplifies, using linear arithmetic, applying ALL-DISTINCT-S-LEMMA,
CDR-CONS, and CAR-CONS, and opening up ZEROP, PRIME, S, and ALL-DISTINCT, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.6 0.0 ]
ALL-DISTINCT-S
(PROVE-LEMMA ALL-NON-ZEROP-S
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-NON-ZEROP (S N M P))))
This conjecture can be simplified, using the abbreviations NOT, PRIME, AND,
and IMPLIES, to the formula:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-NON-ZEROP (S N M P))).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace M by
(PLUS X (TIMES P Z)) to eliminate (REMAINDER M P) and (QUOTIENT M P). We
employ LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER was
introduced, and the type restriction lemma noted when QUOTIENT was introduced
to constrain the new variables. This generates two new conjectures:
Case 2. (IMPLIES (AND (NOT (NUMBERP M))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-NON-ZEROP (S N M P))),
which simplifies, unfolding the functions LESSP, REMAINDER, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NUMBERP X)
(EQUAL (LESSP X P) (NOT (ZEROP P)))
(NUMBERP Z)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL X 0))
(LESSP N P))
(ALL-NON-ZEROP (S N (PLUS X (TIMES P Z)) P))),
which simplifies, unfolding ZEROP and NOT, to:
(IMPLIES (AND (NUMBERP X)
(LESSP X P)
(NUMBERP Z)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL X 0))
(LESSP N P))
(ALL-NON-ZEROP (S N (PLUS X (TIMES P Z)) P))).
Appealing to the lemma SUB1-ELIM, we now replace P by (ADD1 V) to eliminate
(SUB1 P). We employ the type restriction lemma noted when SUB1 was
introduced to constrain the new variable. This generates:
(IMPLIES (AND (NUMBERP V)
(NUMBERP X)
(LESSP X (ADD1 V))
(NUMBERP Z)
(NOT (EQUAL (ADD1 V) 0))
(NOT (EQUAL (ADD1 V) 1))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP N (ADD1 V)))
(ALL-NON-ZEROP (S N
(PLUS X (TIMES (ADD1 V) Z))
(ADD1 V)))).
But this further simplifies, rewriting with the lemmas SUB1-ADD1, ADD1-EQUAL,
COMMUTATIVITY-OF-TIMES, and TIMES-ADD1, and expanding LESSP, NUMBERP, EQUAL,
S, and ALL-NON-ZEROP, to the goal:
(IMPLIES (AND (NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP (SUB1 N) V))
(ALL-NON-ZEROP (S N
(PLUS X Z (TIMES V Z))
(ADD1 V)))).
Appealing to the lemma SUB1-ELIM, we now replace N by (ADD1 W) to eliminate
(SUB1 N). We use the type restriction lemma noted when SUB1 was introduced
to constrain the new variable. The result is three new conjectures:
Case 1.3.
(IMPLIES (AND (EQUAL N 0)
(NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP (SUB1 N) V))
(ALL-NON-ZEROP (S N
(PLUS X Z (TIMES V Z))
(ADD1 V)))),
which finally simplifies, unfolding SUB1, EQUAL, LESSP, S, and
ALL-NON-ZEROP, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP N))
(NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP (SUB1 N) V))
(ALL-NON-ZEROP (S N
(PLUS X Z (TIMES V Z))
(ADD1 V)))),
which finally simplifies, applying SUB1-NNUMBERP, and unfolding EQUAL,
LESSP, S, and ALL-NON-ZEROP, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP W)
(NOT (EQUAL (ADD1 W) 0))
(NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP W V))
(ALL-NON-ZEROP (S (ADD1 W)
(PLUS X Z (TIMES V Z))
(ADD1 V)))).
This further simplifies, applying SUB1-ADD1, ASSOCIATIVITY-OF-PLUS,
COMMUTATIVITY2-OF-PLUS, COMMUTATIVITY2-OF-TIMES,
DISTRIBUTIVITY-OF-TIMES-OVER-PLUS, TIMES-ADD1, COMMUTATIVITY-OF-TIMES,
CDR-CONS, and CAR-CONS, and opening up the definitions of S and
ALL-NON-ZEROP, to the following two new goals:
Case 1.1.2.
(IMPLIES (AND (NUMBERP W)
(NUMBERP V)
(NUMBERP X)
(LESSP (SUB1 X) V)
(NUMBERP Z)
(NOT (EQUAL V 0))
(PRIME1 (ADD1 V) V)
(NOT (EQUAL X 0))
(LESSP W V))
(NOT (EQUAL (REMAINDER (PLUS X Z
(TIMES V Z)
(TIMES W X)
(TIMES W Z)
(TIMES V W Z))
(ADD1 V))
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 (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-NON-ZEROP (S N M P))).
We gave this the name *1 above. Perhaps we can prove it by induction. The
recursive terms in the conjecture suggest four inductions. They merge into
three likely candidate inductions. However, only one is unflawed. We will
induct according to the following scheme:
(AND (IMPLIES (ZEROP N) (p N M P))
(IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N) M P))
(p N M P))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each induction step of the scheme. The above induction
scheme generates the following three new conjectures:
Case 3. (IMPLIES (AND (ZEROP N)
(PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-NON-ZEROP (S N M P))).
This simplifies, opening up the functions ZEROP, PRIME, EQUAL, LESSP, S, and
ALL-NON-ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP N))
(NOT (LESSP (SUB1 N) P))
(PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-NON-ZEROP (S N M P))).
This simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP N 1)
(NOT (ZEROP N))
(NOT (LESSP (SUB1 N) P))
(PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-NON-ZEROP (S N M P))),
which again simplifies, expanding the definitions of SUB1, NUMBERP, EQUAL,
LESSP, and ZEROP, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(ALL-NON-ZEROP (S (SUB1 N) M P))
(PRIME P)
(NOT (EQUAL (REMAINDER M P) 0))
(LESSP N P))
(ALL-NON-ZEROP (S N M P))),
which simplifies, applying CDR-CONS, PRIME-KEY-REWRITE, and CAR-CONS, and
opening up ZEROP, PRIME, S, REMAINDER, and ALL-NON-ZEROP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 3.2 0.0 ]
ALL-NON-ZEROP-S
(PROVE-LEMMA ALL-LESSEQP-S
(REWRITE)
(IMPLIES (NOT (ZEROP P))
(ALL-LESSEQP (S N M P) (SUB1 P))))
This conjecture can be simplified, using the abbreviations ZEROP, NOT, and
IMPLIES, to:
(IMPLIES (AND (NOT (EQUAL P 0)) (NUMBERP P))
(ALL-LESSEQP (S N M P) (SUB1 P))).
Appealing to the lemma SUB1-ELIM, we now replace P by (ADD1 X) to eliminate
(SUB1 P). We rely upon the type restriction lemma noted when SUB1 was
introduced to constrain the new variable. The result is the goal:
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL (ADD1 X) 0)))
(ALL-LESSEQP (S N M (ADD1 X)) X)).
This simplifies, obviously, to:
(IMPLIES (NUMBERP X)
(ALL-LESSEQP (S N M (ADD1 X)) X)),
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 (NOT (ZEROP P))
(ALL-LESSEQP (S N M P) (SUB1 P))).
We named this *1. We will try to prove it by induction. There is only one
suggested induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP N) (p N M P))
(IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N) M P))
(p N M 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
generates two new goals:
Case 2. (IMPLIES (AND (ZEROP N) (NOT (ZEROP P)))
(ALL-LESSEQP (S N M P) (SUB1 P))),
which simplifies, applying PIGEON-HOLE-PRINCIPLE-LEMMA-2 and ADD1-SUB1, and
unfolding the functions ZEROP, EQUAL, S, ALL-LESSEQP, MEMBER, and LISTP, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(ALL-LESSEQP (S (SUB1 N) M P)
(SUB1 P))
(NOT (ZEROP P)))
(ALL-LESSEQP (S N M P) (SUB1 P))).
This simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS, and
opening up the definitions of ZEROP, S, and ALL-LESSEQP, to:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(ALL-LESSEQP (S (SUB1 N) M P)
(SUB1 P))
(NOT (EQUAL P 0))
(NUMBERP P))
(NOT (LESSP (SUB1 P)
(REMAINDER (TIMES M N) P)))),
which again simplifies, using linear arithmetic and rewriting with the lemma
LESSP-REMAINDER-DIVISOR, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
ALL-LESSEQP-S
(PROVE-LEMMA LENGTH-S
(REWRITE)
(EQUAL (LENGTH (S N M P)) (FIX N)))
This conjecture simplifies, opening up the function FIX, to the following two
new goals:
Case 2. (IMPLIES (NOT (NUMBERP N))
(EQUAL (LENGTH (S N M P)) 0)).
But this again simplifies, expanding the definitions of S, LENGTH, and EQUAL,
to:
T.
Case 1. (IMPLIES (NUMBERP N)
(EQUAL (LENGTH (S N M P)) N)),
which we will name *1.
We will appeal to induction. There is only one plausible induction. We
will induct according to the following scheme:
(AND (IMPLIES (ZEROP N) (p N M P))
(IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N) M P))
(p N M P))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to establish that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme generates two new goals:
Case 2. (IMPLIES (AND (ZEROP N) (NUMBERP N))
(EQUAL (LENGTH (S N M P)) N)),
which simplifies, expanding ZEROP, NUMBERP, EQUAL, S, and LENGTH, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(EQUAL (LENGTH (S (SUB1 N) M P))
(SUB1 N))
(NUMBERP N))
(EQUAL (LENGTH (S N M P)) N)),
which simplifies, rewriting with ADD1-SUB1 and CDR-CONS, and unfolding the
definitions of ZEROP, S, and LENGTH, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LENGTH-S
(PROVE-LEMMA FERMAT-THM
(REWRITE)
(IMPLIES (AND (PRIME P)
(NOT (EQUAL (REMAINDER M P) 0)))
(EQUAL (REMAINDER (EXP M (SUB1 P)) P)
1))
((USE (PIGEON-HOLE-PRINCIPLE (L (S (SUB1 P) M P)))
(REMAINDER-TIMES-LIST-S (N (SUB1 P))))
(DISABLE PIGEON-HOLE-PRINCIPLE REMAINDER-TIMES-LIST-S)))
This conjecture can be simplified, using the abbreviations NOT, PRIME, IMPLIES,
and AND, to:
(IMPLIES (AND (IMPLIES (AND (ALL-NON-ZEROP (S (SUB1 P) M P))
(ALL-DISTINCT (S (SUB1 P) M P))
(ALL-LESSEQP (S (SUB1 P) M P)
(LENGTH (S (SUB1 P) M P))))
(PERM (POSITIVES (LENGTH (S (SUB1 P) M P)))
(S (SUB1 P) M P)))
(EQUAL (REMAINDER (TIMES-LIST (S (SUB1 P) M P))
P)
(REMAINDER (TIMES (FACT (SUB1 P))
(EXP M (SUB1 P)))
P))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL (REMAINDER M P) 0)))
(EQUAL (REMAINDER (EXP M (SUB1 P)) P)
1)).
This simplifies, using linear arithmetic, applying ALL-NON-ZEROP-S,
ALL-DISTINCT-S, LENGTH-S, ALL-LESSEQP-S, TIMES-LIST-EQUAL-FACT, PRIME-FACT,
and COROLLARY-55, and expanding the definitions of PRIME, AND, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
FERMAT-THM
(PROVE-LEMMA CRYPT-INVERTS-STEP-1 NIL
(IMPLIES (PRIME P)
(EQUAL (REMAINDER (TIMES M (EXP M (TIMES K (SUB1 P))))
P)
(REMAINDER M P))))
This formula can be simplified, using the abbreviations PRIME and IMPLIES, to
the new formula:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL (REMAINDER (TIMES M (EXP M (TIMES K (SUB1 P))))
P)
(REMAINDER M P))),
which simplifies, appealing to the lemmas FERMAT-THM, EXP-MOD-IS-1, and
COROLLARY-55, and unfolding the functions PRIME and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
CRYPT-INVERTS-STEP-1
(PROVE-LEMMA CRYPT-INVERTS-STEP-1A
(REWRITE)
(IMPLIES (PRIME P)
(EQUAL (REMAINDER (TIMES M
(EXP M (TIMES K (SUB1 P) (SUB1 Q))))
P)
(REMAINDER M P)))
((USE (CRYPT-INVERTS-STEP-1 (K (TIMES K (SUB1 Q)))))
(DISABLE CRYPT-INVERTS-STEP-1)))
This conjecture can be simplified, using the abbreviations PRIME, IMPLIES, and
ASSOCIATIVITY-OF-TIMES, to:
(IMPLIES
(AND
(IMPLIES (PRIME P)
(EQUAL (REMAINDER (TIMES M
(EXP M (TIMES K (SUB1 Q) (SUB1 P))))
P)
(REMAINDER M P)))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P)))
(EQUAL (REMAINDER (TIMES M
(EXP M (TIMES K (SUB1 P) (SUB1 Q))))
P)
(REMAINDER M P))).
This simplifies, appealing to the lemmas COMMUTATIVITY-OF-TIMES, COROLLARY-55,
and PRIME-KEY-REWRITE, and opening up PRIME, IMPLIES, and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.2 0.0 ]
CRYPT-INVERTS-STEP-1A
(PROVE-LEMMA CRYPT-INVERTS-STEP-1B
(REWRITE)
(IMPLIES (PRIME Q)
(EQUAL (REMAINDER (TIMES M
(EXP M (TIMES K (SUB1 P) (SUB1 Q))))
Q)
(REMAINDER M Q)))
((USE (CRYPT-INVERTS-STEP-1 (P Q)
(K (TIMES K (SUB1 P)))))
(DISABLE CRYPT-INVERTS-STEP-1)))
This conjecture can be simplified, using the abbreviations PRIME, IMPLIES, and
ASSOCIATIVITY-OF-TIMES, to:
(IMPLIES
(AND
(IMPLIES (PRIME Q)
(EQUAL (REMAINDER (TIMES M
(EXP M (TIMES K (SUB1 P) (SUB1 Q))))
Q)
(REMAINDER M Q)))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q)))
(EQUAL (REMAINDER (TIMES M
(EXP M (TIMES K (SUB1 P) (SUB1 Q))))
Q)
(REMAINDER M Q))).
This simplifies, appealing to the lemmas EXP-MOD-IS-1, FERMAT-THM, and
COROLLARY-55, and opening up PRIME, EQUAL, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
CRYPT-INVERTS-STEP-1B
(PROVE-LEMMA CRYPT-INVERTS-STEP-2
(REWRITE)
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(NUMBERP M)
(LESSP M (TIMES P Q))
(EQUAL (REMAINDER ED
(TIMES (SUB1 P) (SUB1 Q)))
1))
(EQUAL (REMAINDER (EXP M ED) (TIMES P Q))
M)))
This conjecture can be simplified, using the abbreviations NOT, PRIME, AND,
and IMPLIES, to the formula:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q))
(NUMBERP M)
(LESSP M (TIMES P Q))
(EQUAL (REMAINDER ED
(TIMES (SUB1 P) (SUB1 Q)))
1))
(EQUAL (REMAINDER (EXP M ED) (TIMES P Q))
M)).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace ED by:
(PLUS X
(TIMES (TIMES (SUB1 P) (SUB1 Q)) Z))
to eliminate (REMAINDER ED (TIMES (SUB1 P) (SUB1 Q))) and:
(QUOTIENT ED
(TIMES (SUB1 P) (SUB1 Q)))
. We employ LESSP-REMAINDER2, the type restriction lemma noted when REMAINDER
was introduced, and the type restriction lemma noted when QUOTIENT was
introduced to constrain the new variables. We must thus prove four new goals:
Case 4. (IMPLIES (AND (NOT (NUMBERP ED))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q))
(NUMBERP M)
(LESSP M (TIMES P Q))
(EQUAL (REMAINDER ED
(TIMES (SUB1 P) (SUB1 Q)))
1))
(EQUAL (REMAINDER (EXP M ED) (TIMES P Q))
M)),
which simplifies, rewriting with the lemma EQUAL-TIMES-0, and expanding the
functions LESSP, REMAINDER, and EQUAL, to:
T.
Case 3. (IMPLIES (AND (EQUAL (TIMES (SUB1 P) (SUB1 Q)) 0)
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q))
(NUMBERP M)
(LESSP M (TIMES P Q))
(EQUAL (REMAINDER ED
(TIMES (SUB1 P) (SUB1 Q)))
1))
(EQUAL (REMAINDER (EXP M ED) (TIMES P Q))
M)),
which simplifies, using linear arithmetic and appealing to the lemma
LESSP-TIMES-2, to:
T.
Case 2. (IMPLIES (AND (NOT (NUMBERP (TIMES (SUB1 P) (SUB1 Q))))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q))
(NUMBERP M)
(LESSP M (TIMES P Q))
(EQUAL (REMAINDER ED
(TIMES (SUB1 P) (SUB1 Q)))
1))
(EQUAL (REMAINDER (EXP M ED) (TIMES P Q))
M)),
which simplifies, obviously, to:
T.
Case 1. (IMPLIES
(AND (NUMBERP X)
(EQUAL (LESSP X (TIMES (SUB1 P) (SUB1 Q)))
(NOT (ZEROP (TIMES (SUB1 P) (SUB1 Q)))))
(NUMBERP Z)
(NOT (EQUAL (TIMES (SUB1 P) (SUB1 Q)) 0))
(NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q))
(NUMBERP M)
(LESSP M (TIMES P Q))
(EQUAL X 1))
(EQUAL (REMAINDER (EXP M
(PLUS X
(TIMES (TIMES (SUB1 P) (SUB1 Q)) Z)))
(TIMES P Q))
M)).
This simplifies, rewriting with EQUAL-TIMES-0, EQUAL-LESSP,
COMMUTATIVITY-OF-TIMES, TIMES-IDENTITY, COMMUTATIVITY2-OF-TIMES,
ASSOCIATIVITY-OF-TIMES, TIMES-1, EXP-BY-0, EXP-PLUS, CRYPT-INVERTS-STEP-1B,
CRYPT-INVERTS-STEP-1A, and COROLLARY-53, and expanding the functions NUMBERP,
ZEROP, NOT, EQUAL, SUB1, EXP, and PRIME, to:
T.
Q.E.D.
[ 0.0 0.4 0.0 ]
CRYPT-INVERTS-STEP-2
(PROVE-LEMMA CRYPT-INVERTS NIL
(IMPLIES (AND (PRIME P)
(PRIME Q)
(NOT (EQUAL P Q))
(EQUAL N (TIMES P Q))
(NUMBERP M)
(LESSP M N)
(EQUAL (REMAINDER (TIMES E D)
(TIMES (SUB1 P) (SUB1 Q)))
1))
(EQUAL (CRYPT (CRYPT M E N) D N) M))
NIL)
This conjecture can be simplified, using the abbreviations NOT, PRIME, AND,
and IMPLIES, to the goal:
(IMPLIES (AND (NOT (EQUAL P 0))
(NUMBERP P)
(NOT (EQUAL P 1))
(PRIME1 P (SUB1 P))
(NOT (EQUAL Q 0))
(NUMBERP Q)
(NOT (EQUAL Q 1))
(PRIME1 Q (SUB1 Q))
(NOT (EQUAL P Q))
(EQUAL N (TIMES P Q))
(NUMBERP M)
(LESSP M N)
(EQUAL (REMAINDER (TIMES E D)
(TIMES (SUB1 P) (SUB1 Q)))
1))
(EQUAL (CRYPT (CRYPT M E N) D N) M)).
This simplifies, using linear arithmetic, appealing to the lemmas
COMMUTATIVITY-OF-TIMES, LESSP-TIMES-1, CRYPT-CORRECT, EXP-EXP,
CRYPT-INVERTS-STEP-2, and REMAINDER-EXP, and unfolding the function PRIME, to:
T.
Q.E.D.
[ 0.0 0.3 0.0 ]
CRYPT-INVERTS
(MAKE-LIB "rsa" T)
Making the lib for "rsa".
Compiling the lib for "rsa".
Loading ./basic/rsa.o
Finished loading ./basic/rsa.o
Finished compiling the lib for "rsa".
Finished making the lib for "rsa".
(/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/rsa.lib
/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/rsa.lisp)